Commit 95d5a31f authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

reflection test on wmp

parent c06d6dbe
......@@ -376,7 +376,28 @@ let rec add_expr (e1 e2: expr) : expr
| Cst _, _ | _, Cst _ -> Add e a, False
| Add e1 e2, _ ->
let r, b = add_atom e1 a in
if b then Add r e2, True else let r,b = add_atom e2 a in Add e1 r, b
if b
then
match r with
| Cst c ->
if C.eq c C.czero
then begin
assert { forall y z. C.(+) (interp e1 y z) (interp a y z) = C.azero };
e2, True end
else Add r e2, True
| _ -> Add r e2, True
end
else
let r,b = add_atom e2 a in
match r with
| Cst c ->
if C.eq c C.czero
then begin
assert { forall y z. C.(+) (interp e2 y z) (interp a y z) = C.azero };
e1, True end
else Add e1 r, b
| _ -> Add e1 r, b
end
| _, Add _ _ -> absurd
end
in
......@@ -412,32 +433,18 @@ let rec zero_expr (e:expr) : bool
variant { e }
raises { C.Unknown -> true }
=
let nv = max_var e in
let coeffs = Array.make (nv+1) C.czero in
let rec fill_c (e:expr) : unit
let rec all_zero (e:expr) : bool
ensures { result -> forall y z. interp e y z = C.azero }
variant { e }
raises { C.Unknown -> true }
(*define interp_sub for coeff array as sum, ensures interp coeffs = interp e*)
= match e with
| Cst c -> coeffs[nv] <- C.add c coeffs[nv]
| Term c i -> coeffs[i] <- C.add c coeffs[i]
| UTerm i -> coeffs[i] <- C.add C.cone coeffs[i]
| Add e1 e2 -> fill_c e1; fill_c e2
end
| Cst c -> C.eq c C.czero
| Term c _ -> C.eq c C.czero
| UTerm _ -> false
| Add e1 e2 -> all_zero e1 && all_zero e2
end
in
fill_c e;
let res = ref true in
for i = 0 to nv do
(* invariant res -> interp_sub 0 i = C.azero *)
if not (C.eq coeffs[i] C.czero) then res := false;
done;
!res
(* match e with
| Cst c -> C.eq c C.czero
| Term c _ -> C.eq c C.czero
| UTerm _ -> false
| Add e1 e2 -> zero_expr e1 && zero_expr e2
end *)
let e' = add_expr (Cst C.czero) e in (* simplifies expr *)
all_zero e'
let sub_expr (e1 e2:expr)
ensures { forall y z. C.(+) (interp result y z) (interp e2 y z)
......
......@@ -90,6 +90,8 @@ module N
use import int.Int
use import int.Power
meta compute_max_steps 0x100000
(** {3 Long integers as arrays of libs} *)
type limb = uint64
......@@ -246,6 +248,13 @@ module N
function value (x:t) (sz:int) : int =
value_sub (pelts x) x.offset (x.offset + sz)
let lemma value_tail (x:t) (sz:int32)
requires { 0 <= sz }
ensures { value x (sz+1) = value x sz + (pelts x)[x.offset + sz] * power radix sz }
= value_sub_tail (pelts x) x.offset (x.offset + p2i sz)
meta remove_prop axiom value_tail
function compare_int (x y:int) : int =
if x < y then -1 else if x=y then 0 else 1
......@@ -423,18 +432,19 @@ module N
variant { sz - !i }
label StartLoop in
lx := get_ofs x !i;
assert { (pelts x)[offset x + !i] = !lx };
let (res, carry) = add_with_carry !lx !c limb_zero in
set_ofs r !i res;
assert { value r !i + (power radix !i) * !c =
value x !i + y };
assert { res + radix * carry = !lx + !c }; (* add_with_carry post *)
c := carry;
let ghost k = p2i !i in
i := Int32.(+) !i (Int32.of_int 1);
value_sub_tail (pelts r) r.offset (r.offset + k);
value_sub_tail (pelts x) x.offset (x.offset + k);
assert { value r !i + (power radix !i) * !c
= value x !i + y
by
assert { (pelts r)[offset r + !i] = res };
value_tail r !i;
value_tail x !i;
assert { value r (!i+1) + (power radix (!i+1)) * !c
= value x (!i+1) + y
(* by
value r !i + (power radix !i) * !c
= value r k + (power radix k) * res
+ (power radix !i) * !c
......@@ -446,7 +456,8 @@ module N
= value r k + (power radix k) * (!c at StartLoop)
+ (power radix k) * !lx
= value x k + y + (power radix k) * !lx
= value x !i + y }
= value x !i + y*) };
i := Int32.(+) !i (Int32.of_int 1);
done;
if Int32.(=) !i sz then !c
else begin
......@@ -693,6 +704,12 @@ module N
ly := get_ofs y !i;
let res, carry = add_with_carry !lx !ly !c in
set_ofs x !i res;
assert { forall j. !i < j < sx ->
(pelts x)[x.offset + j]
= (pelts ox)[x.offset + j]
by (pelts x)[x.offset + j]
= (pelts (x at StartLoop))[x.offset + j]
= (pelts ox)[x.offset + j]};
assert { value x !i + (power radix !i) * !c = value ox !i + value y !i };
c := carry;
let ghost k = p2i !i in
......@@ -1096,6 +1113,12 @@ module N
ly := get_ofs y !i;
let res, borrow = sub_with_borrow !lx !ly !b in
set_ofs x !i res;
assert { forall j. !i < j < sx ->
(pelts x)[x.offset + j]
= (pelts ox)[x.offset + j]
by (pelts x)[x.offset + j]
= (pelts (x at StartLoop))[x.offset + j]
= (pelts ox)[x.offset + j]};
assert { value x !i - power radix !i * !b = value ox !i - value y !i };
b := borrow;
let ghost k = p2i !i in
......@@ -6550,3 +6573,9 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
free ny;
end
(*
Local Variables:
compile-command: "why3 ide -L . mp2.mlw"
End:
*)
......@@ -5,16 +5,10 @@ open Ident
open Task
open Args_wrapper
let rec fold_left3 f accu l1 l2 l3 =
match (l1, l2, l3) with
| a1::l1, a2::l2, a3::l3 -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3
| [], [], [] -> accu
| _ -> raise (Invalid_argument "fold_left3")
exception NoReification
exception Exit
let debug = true
let debug = false
let expl_reification_check = Ident.create_label "expl:reification check"
......@@ -24,18 +18,20 @@ type reify_env = { kn: known_map;
subst: term Mvs.t;
lv: vsymbol list;
var_maps: ty Mvs.t; (* type of values pointed by each map*)
crc_map: Coercion.t;
ty_to_map: vsymbol Mty.t;
env: Env.env;
task: Task.task;
}
let init_renv kn lv env task =
let init_renv kn crc lv env task =
{ kn=kn;
store = Mterm.empty;
fr = 0;
subst = Mvs.empty;
lv = lv;
var_maps = Mvs.empty;
crc_map = crc;
ty_to_map = Mty.empty;
env = env;
task = task;
......@@ -53,15 +49,7 @@ let rec is_const t =
let rec reify_term renv t rt =
let is_pvar p = match p.pat_node with Pvar _ -> true | _ -> false in
let rec find_var vl v p (renv, acc) f t =
if acc = None
then if t_v_occurs v f > 0
then let renv, rt = (invert_pat vl renv (p, f) t) in
renv, Some rt
else renv, acc
else (assert (t_v_occurs v f = 0);
renv, acc)
and invert_nonvar_pat vl (renv:reify_env) (p,f) t =
let rec invert_nonvar_pat vl (renv:reify_env) (p,f) t =
if debug
then Format.printf
"invert_nonvar_pat p %a f %a t %a@."
......@@ -70,27 +58,6 @@ let rec reify_term renv t rt =
| Pwild , _, _ | Pvar _,_,_ when t_equal_nt_nl f t ->
if debug then Format.printf "case equal@.";
renv, t
(*| Papp (cs, pl), Tapp(ls1, la1), Tapp(ls2, la2)
when ls_equal ls1 ls2 && List.length pl = List.length la1
->
if debug then Format.printf "case app@.";
(* same head symbol, match parameters *)
let renv, rl =
fold_left3
(fun (renv, acc) p f t ->
let renv, nt = invert_pat vl renv (p, f) t in
if debug
then Format.printf "param %a matched@." Pretty.print_term t;
(renv, nt::acc))
(renv, []) pl la1 la2 in
if debug then Format.printf "building app %a of type %a with args %a@."
Pretty.print_ls cs
Pretty.print_ty p.pat_ty
(Pp.print_list Pp.comma Pretty.print_term)
(List.rev rl);
let t = t_app cs (List.rev rl) (Some p.pat_ty) in
if debug then Format.printf "app ok@.";
renv, t*)
| Papp (cs, pl), Tapp(ls1, _), Tapp(ls2, _)
when ls_equal ls1 ls2
&& Svs.for_all (fun v -> t_v_occurs v f = 1) p.pat_vars
......@@ -126,8 +93,8 @@ let rec reify_term renv t rt =
when ls_equal ls1 ls2 && t_v_occurs v f = 1
-> if debug then Format.printf "case app_var@.";
let renv, rt =
List.fold_left2 (find_var vl v p) (renv, None) la1 la2 in
(*(fun (renv, acc) f t ->
List.fold_left2
(fun (renv, acc) f t ->
if acc = None
then if t_v_occurs v f > 0
then let renv, rt = (invert_pat vl renv (p, f) t) in
......@@ -135,15 +102,8 @@ let rec reify_term renv t rt =
else renv, acc
else (assert (t_v_occurs v f = 0);
renv, acc))
(renv,None) la1 la2
in*)
(renv,None) la1 la2 in
renv, Opt.get rt
(*| Papp(cs, [({pat_node = Pvar v} as vp)]), Tapp (ls1, la1), Tapp(ls2, la2)
when ls_equal ls1 ls2 && t_v_occurs v f = 1
-> if debug then Format.printf "case capp_var@.";
let renv, rt =
List.fold_left2 (find_var vl v vp) (renv, None) la1 la2 in
renv, t_app cs [(Opt.get rt)] (Some p.pat_ty)*)
| Por (p1, p2), _, _ ->
if debug then Format.printf "case or@.";
begin try invert_pat vl renv (p1, f) t
......@@ -210,20 +170,31 @@ let rec reify_term renv t rt =
end
| _ -> raise NoReification
and invert_pat vl renv (p,f) t =
(if not (oty_equal f.t_ty t.t_ty)
then
(if debug
then Format.printf "type mismatch between %a and %a@."
Pretty.print_ty (Opt.get f.t_ty)
Pretty.print_ty (Opt.get t.t_ty);
raise NoReification)); (*FIXME at least check coercions ?*)
try invert_nonvar_pat vl renv (p,f) t
with NoReification -> invert_var_pat vl renv (p,f) t
if (oty_equal f.t_ty t.t_ty)
then
try invert_nonvar_pat vl renv (p,f) t
with NoReification -> invert_var_pat vl renv (p,f) t
else begin
try
let crc = Coercion.find renv.crc_map
(Opt.get t.t_ty) (Opt.get f.t_ty) in
let apply_crc t ls = t_app_infer ls [t] in
let crc_t = List.fold_left apply_crc t crc in
assert (oty_equal f.t_ty crc_t.t_ty);
invert_pat vl renv (p,f) crc_t
with Not_found ->
if debug
then Format.printf "type mismatch between %a and %a@."
Pretty.print_ty (Opt.get f.t_ty)
Pretty.print_ty (Opt.get t.t_ty);
raise NoReification
end
and invert_interp renv ls (t:term) = (*la ?*)
let ld = try Opt.get (find_logic_definition renv.kn ls)
with _ ->
if debug
then Format.printf "did not find def of %a@." Pretty.print_ls ls;
then Format.printf "did not find def of %a@."
Pretty.print_ls ls;
raise NoReification
in
let vl, f = open_ls_defn ld in
......@@ -489,7 +460,9 @@ let reflection_by_lemma pr env : Task.task Trans.tlist = Trans.store (fun task -
let d = Opt.get d in
let l = Apply.term_decl d in
let (lp, lv, rt) = Apply.intros l in
let renv = reify_term (init_renv kn lv env prev) g rt in
let nt = Args_wrapper.build_naming_tables task in
let crc = nt.Trans.coercion in
let renv = reify_term (init_renv kn crc lv env prev) g rt in
let subst, prev = build_vars_map renv prev in
build_goals prev subst lp g rt
with NoReification | Exit -> [task])
......@@ -1064,6 +1037,8 @@ let rec term_of_value = function
let reflection_by_function s env = Trans.store (fun task ->
if debug then Format.printf "reflection_f start@.";
let kn = task_known task in
let nt = Args_wrapper.build_naming_tables task in
let crc = nt.Trans.coercion in
let g, prev = Task.task_separate_goal task in
let g = Apply.term_decl g in
let ths = Task.used_theories task in
......@@ -1112,7 +1087,7 @@ let reflection_by_function s env = Trans.store (fun task ->
Pretty.print_vs vres Pretty.print_term p;
let (lp, lv, rt) = Apply.intros p in
let lv = lv @ args in
let renv = reify_term (init_renv kn lv env prev) g rt in
let renv = reify_term (init_renv kn crc lv env prev) g rt in
(*ignore (build_vars_map renv prev);
Mvs.iter (fun v t -> if debug then Format.printf "%a %a@."
Pretty.print_vs v
......
module C
use import map.Map
use import mach.int.Unsigned
use import mach.int.Int32
use import mach.int.UInt32
use import array.Array
use import map.Map
use import int.Int
predicate in_us_bounds (n:int) = 0 <= n <= max_uint32
predicate in_bounds (n:int) = min_int32 <= n <= max_int32
......@@ -38,16 +38,18 @@ module C
val incr (p:ptr 'a) (ofs:int32) : ptr 'a
requires { p.offset + ofs <= plength p }
ensures { result.offset = p.offset + Int32.to_int ofs }
ensures { plength result = plength p }
ensures { pelts result = pelts p }
ensures { result.data = p.data }
alias { p.data with result.data }
val get (p:ptr 'a) : 'a
requires { 0 <= p.offset < plength p }
ensures { result = (p.data)[p.offset] }
ensures { result = (pelts p)[p.offset] }
let get_ofs (p:ptr 'a) (ofs:int32) : 'a
requires { 0 <= p.offset + Int32.to_int ofs < plength p }
ensures { result = (p.data)[p.offset + Int32.to_int ofs] }
ensures { result = (pelts p)[p.offset + Int32.to_int ofs] }
= get (incr p ofs)
val set (p:ptr 'a) (v:'a) : unit
......@@ -93,7 +95,7 @@ module C
ensures { plength result = Int32.to_int sz -> plength p = 0 }
ensures { plength result = Int32.to_int sz ->
forall i:int. 0 <= i < plength (old p) /\ i < Int32.to_int sz ->
(result.data)[i] = ((old p).data)[i] }
(pelts result)[i] = (pelts (old p))[i] }
ensures { plength result <> Int32.to_int sz -> p = old p }
val predicate is_not_null (p:ptr 'a) : bool
......
......@@ -200,14 +200,14 @@ module Int32
function to_int = int32'int,
lemma to_int_in_bounds,
lemma extensionality
(*
use bv.BV32
val to_bv (x: int32) : BV32.t
ensures { BV32.to_int result = to_int x }
val of_bv (x: BV32.t) : int32
ensures { to_int result = BV32.to_int x }
*)
end
module UInt32
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment