Commit e5944d8b authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

reflection printfs and add_limbs example

parent c66c91e5
......@@ -362,7 +362,11 @@ let rec add_expr (e1 e2: expr) : expr
= C.(+) (interp e1 y z) (interp e2 y z) }
variant { e2 }
raises { C.Unknown -> true }
= let rec add_atom (e a:expr) : (expr, bool)
=
let term_or_cst c i
ensures { forall y z. interp result y z = interp (Term c i) y z }
= if C.eq C.czero c then Cst C.czero else Term c i in
let rec add_atom (e a:expr) : (expr, bool)
requires { atom a }
returns { r,b -> forall y z. interp r y z
= C.(+) (interp e y z) (interp a y z) }
......@@ -370,9 +374,19 @@ let rec add_expr (e1 e2: expr) : expr
raises { C.Unknown -> true }
= match (e,a) with
| Term ce ie, Term ca ia ->
if ie = ia then (Term (C.add ce ca) ie, True) else (Add e a, False)
if ie = ia then (term_or_cst (C.add ce ca) ie, True)
else if C.eq ce C.czero then (term_or_cst ca ia, True)
else if C.eq ca C.czero then (e,True)
else (Add e a, False)
| Cst ce, Cst ca -> Cst (C.add ce ca), True
| Cst _, _ | _, Cst _ -> Add e a, False
| Cst ce, Term ca _ ->
if C.eq ca C.czero then (e, True)
else if C.eq ce C.czero then (a, True)
else (Add e a, False)
| Term ce _, Cst ca ->
if C.eq ce C.czero then (a, True)
else if C.eq ca C.czero then (e, True)
else (Add e a, False)
| Add e1 e2, _ ->
let r, b = add_atom e1 a in
if b
......@@ -460,13 +474,16 @@ let sub_expr (e1 e2:expr)
= C.(+) (C.(+) v1 (C.(-_) v2)) v2 = v1 };
r
use import debug.Debug
let rec same_eq (eq1 eq2: equality) : bool
ensures { result -> forall y z. interp_eq eq1 y z -> interp_eq eq2 y z }
raises { C.Unknown -> true }
= let (e1,c1) = norm_eq eq1 in
let (e2,c2) = norm_eq eq2 in
let e = sub_expr e1 e2 in
zero_expr e && C.eq c1 c2
if zero_expr e && C.eq c1 c2 then true
else (print (add_expr (Cst C.czero) e); print c1; print c2; false)
use import option.Option
......@@ -481,6 +498,16 @@ let rec norm_context (l:context) : context
Cons (ex, Cst c) (norm_context t)
end
let rec print_lc ctx v : unit variant { ctx }
= match ctx, v with
| Nil, Nil -> ()
| Cons l t, Cons v t2 ->
(if C.eq C.czero v then ()
else (print l; print v));
print_lc t t2
| _ -> ()
end
let check_combination (ctx:context) (g:equality) (v:list coeff) : bool
ensures { result = true -> forall y z. interp_ctx ctx g y z}
raises { C.Unknown -> true }
......@@ -510,7 +537,7 @@ let check_combination (ctx:context) (g:equality) (v:list coeff) : bool
end
in
match aux ctx Nil (Cst C.czero, Cst C.czero) v with
| Some sum -> same_eq sum g
| Some sum -> if same_eq sum g then true else (print_lc ctx v; false)
| None -> false
end
......@@ -559,7 +586,7 @@ let a_breakpoint (v:array coeff) : unit
let gauss_jordan (a: matrix coeff) : option (array coeff)
(*AX=B, a=(A|B), result=X*)
returns { Some r -> Array.length r = a.columns - 1 | None -> true }
returns { Some r -> Array.length r = a.columns | None -> true }
requires { 1 <= a.rows /\ 1 <= a.columns }
raises { C.Unknown -> true }
=
......@@ -578,7 +605,7 @@ let gauss_jordan (a: matrix coeff) : option (array coeff)
else i in
let pivots = Array.make n 0 in
let r = ref (-1) in
for j = 0 to m-1 do
for j = 0 to m-2 do
invariant { -1 <= !r < n }
invariant { forall i. 0 <= i <= !r -> 0 <= pivots[i] }
invariant { forall i1 i2: int. 0 <= i1 < i2 <= !r -> pivots[i1] < pivots[i2] }
......@@ -598,14 +625,13 @@ let gauss_jordan (a: matrix coeff) : option (array coeff)
end
done;
if !r < 0 then None (* matrix is all zeroes *)
else if pivots[!r] >= m-1 then None (*pivot on last column, no solution*)
else begin
let v = Array.make (m-1) C.czero in
let v = Array.make m(*(m-1)*) C.czero in
for i = 0 to !r do
v[pivots[i]] <- get a i (m-1)
done;
(* a_breakpoint v;*)
Some v
Some v (*pivots[!r] < m-1*) (*pivot on last column, no solution*)
end
use import array.ToList
......@@ -1069,6 +1095,8 @@ use import real.PowerReal
use RationalCoeffs as Q
use import int.Int
use import debug.Debug
type evars = int -> int
type exp = Lit int | Var int | Plus exp exp | Minus exp
......@@ -1106,18 +1134,6 @@ function minterp (t:t) (y:evars) : real
exception Unknown
let rec predicate same_exp (e1 e2: exp)
ensures { result -> forall y. interp_exp e1 y = interp_exp e2 y }
variant { e1, e2 }
= match e1, e2 with
| Lit n1, Lit n2 -> n1 = n2
| Var v1, Var v2 -> v1 = v2
| Plus a1 b1, Plus a2 b2 ->
((same_exp a1 a2) && (same_exp b1 b2))
|| ((same_exp a1 b2) && (same_exp b1 a2))
| Minus e1', Minus e2' -> same_exp e1' e2'
| _ -> false
end
let rec add_exp (e1 e2:exp)
ensures { forall y. interp_exp result y = interp_exp e1 y + interp_exp e2 y }
......@@ -1168,6 +1184,35 @@ let rec opp_exp (e:exp)
| Var _ -> Minus e
end
let rec zero_exp (e:exp) : bool
ensures { result -> forall y. interp_exp e y = 0 }
variant { e }
raises { Unknown -> true }
=
let rec all_zero (e:exp) : bool
ensures { result -> forall y. interp_exp e y = 0 }
variant { e }
= match e with
| Lit n -> n = 0
| Var _ -> false
| Minus e -> all_zero e
| Plus e1 e2 -> all_zero e1 && all_zero e2
end
in
let e' = add_exp (Lit 0) e in (* simplifies exp *)
all_zero e'
let rec same_exp (e1 e2: exp)
ensures { result -> forall y. interp_exp e1 y = interp_exp e2 y }
variant { e1, e2 }
raises { Unknown -> true }
= match e1, e2 with
| Lit n1, Lit n2 -> n1 = n2
| Var v1, Var v2 -> v1 = v2
| Minus e1', Minus e2' -> same_exp e1' e2'
| _ -> zero_exp (add_exp e1 (opp_exp e2))
end
let madd (a b:t)
ensures { forall y. minterp result y = minterp a y +. minterp b y }
raises { Unknown -> true }
......@@ -1217,10 +1262,23 @@ let mopp (a:t)
ensures { forall y. minterp result y = -. minterp a y }
= match a with (q,e) -> (Q.ropp q, e) end
let rec predicate pure_same_exp (e1 e2: exp)
ensures { result -> forall y. interp_exp e1 y = interp_exp e2 y }
variant { e1, e2 }
= match e1, e2 with
| Lit n1, Lit n2 -> n1 = n2
| Var v1, Var v2 -> v1 = v2
| Minus e1', Minus e2' -> pure_same_exp e1' e2'
| Plus a1 a2, Plus b1 b2 ->
(pure_same_exp a1 b1 && pure_same_exp a2 b2) ||
(pure_same_exp a1 b2 && pure_same_exp a2 b1)
| _ -> false
end
let predicate meq (a b:t)
ensures { result -> forall y. minterp a y = minterp b y }
= match (a,b) with
| (q1,e1), (q2,e2) -> (Q.req q1 q2 && same_exp e1 e2) || (Q.req q1 Q.rzero && Q.req q2 Q.rzero)
| (q1,e1), (q2,e2) -> (Q.req q1 q2 && pure_same_exp e1 e2) || (Q.req q1 Q.rzero && Q.req q2 Q.rzero)
end
let minv (a:t)
......@@ -1435,4 +1493,16 @@ goal g'': forall r r' i c x x' y l: int.
(*tries to add power radix i and power radix (i+1), fails
-> cst propagation ? *)
end
module Test2
use import int.Int
use import LinearDecisionInt
goal g: forall x y z: int.
x + y = 0 ->
y - z = 0 ->
x = 0
end
\ No newline at end of file
......@@ -1444,6 +1444,8 @@ module N
variant { sz - !i }
label StartLoop in
value_concat r !i (!i + sz);
assert { value !rp sz
= value_sub (pelts r) (offset r + !i) (offset r + (!i + sz)) };
ly := get_ofs y !i;
let c' = addmul_limb !rp x !ly sz in
assert { value !rp sz + power radix sz * c'
......@@ -2140,19 +2142,20 @@ module N
let retval, h = lsld_ext !high tnc in
let low = ref h in
let i = ref zero in
let ghost c = power 2 (l2i tnc) in
while (Int32.(<) !i msb) do
variant { sz - !i }
invariant { 0 <= !i <= msb }
invariant { retval + radix * (value r !i
+ (power radix !i) * !low)
= value x (1 + !i) * (power 2 (tnc)) }
= value x (!i+1) * c }
invariant { (!rp).offset = r.offset + !i }
invariant { (!xp).offset = x.offset + !i }
invariant { plength !rp = plength r }
invariant { plength !xp = plength x }
invariant { pelts !rp = pelts r }
invariant { pelts !xp = pelts x }
invariant { !low < power 2 (tnc) }
invariant { !low < c}
label StartLoop in
xp.contents <- C.incr !xp one;
high := C.get !xp;
......@@ -2166,13 +2169,17 @@ module N
value_tail x (!i+1);
assert { (pelts r)[r.offset + !i] = !low + l };
low := h;
let ghost k = p2i !i in
i := Int32.(+) !i one;
(*todo let c = power 2 tnc in... replace occurences by c and try reflection*)
assert { retval + radix * (value r !i
+ (power radix !i) * !low)
= value x (!i+1) * (power 2 tnc)
by
assert { value x (!i+2) * c = value x (!i+1) * c
+ power radix (!i+1) * l + power radix (!i+2) * h
by (pelts x)[offset x + !i + 1] = !high
so value x (!i+2) * c =
(value x (!i+1) + power radix (!i+1)* !high) * c
so !high * c = l + radix * h };
(*nonlinear part*)
assert { retval + radix * (value r (!i+1)
+ (power radix (!i+1)) * !low)
= value x (!i+2) * c
(* by
(pelts r)[r.offset + k]
= (pelts r)[(!rp.offset at StartLoop)]
= (!low at StartLoop) + l
......@@ -2215,14 +2222,15 @@ module N
= (value x !i
+ power radix !i * (pelts x)[x.offset + !i])
* power 2 (tnc)
= value x (1 + !i) * power 2 (tnc)
= value x (1 + !i) * power 2 (tnc) *)
};
i := Int32.(+) !i one;
rp.contents <- C.incr !rp one;
done;
label EndLoop in
assert { retval + radix * (value r msb
+ (power radix msb) * !low)
= value x sz * (power 2 (tnc)) };
= value x sz * c };
value_sub_tail (pelts r) r.offset (r.offset + p2i msb);
assert { (!rp).offset = r.offset + msb };
value_sub_shift_no_change (pelts r) r.offset
......@@ -2666,7 +2674,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
i := Int32.(-) !i one;
value_sub_head (pelts x) (x.offset + k) (x.offset + p2i sz);
value_sub_head (pelts q) (q.offset + k) (q.offset + p2i sz);
assert { mult * value_sub (pelts x) (x.offset + !i + 1)
assert { mult * value_sub (pelts x) (x.offset + !i + 1) (* TODO refl*)
(x.offset + sz)
= value_sub (pelts q) (q.offset + !i + 1) (q.offset + sz)
* ry
......@@ -4067,6 +4075,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
= value xd (sy - 1)
+ power radix (sy - 1) * !x1
};
(* refl *)
assert { value (old x) sx =
(value !qp (sx - sy - !i)
+ qh * power radix (sx - sy - !i))
......@@ -4551,6 +4560,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
+ power radix (sy - 2) * !x0
= value xd (sy - 2)
+ power radix (sy - 2) * !x0 };
(* TODO refl *)
assert { value xd (sy - 2)
- power radix (sy - 2) * cy
+ power radix (sy - 2) *
......@@ -4866,6 +4876,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
};
end;
ql := Limb.(-) !ql uone;
(* todo refl *)
assert { value xd (sy - 1) + power radix (sy - 1) * !x1
= value (xd at SubProd) sy
+ power radix sy * (!x1 at StartLoop)
......@@ -4897,6 +4908,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
((!qp).offset + p2i sx - p2i sy - p2i !i);
value_sub_tail (pelts x) x.offset (x.offset + p2i sy + p2i !i - 1);
value_sub_concat (pelts x) x.offset xd.offset (x.offset + s);
(* todo refl *)
assert { value (old x) sx =
(value !qp (sx - sy - !i)
+ qh * power radix (sx - sy - !i))
......@@ -5198,6 +5210,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
((!qp).offset + p2i sx - p2i sy - p2i !i);
value_sub_tail (pelts x) x.offset (x.offset + p2i sy + p2i !i - 1);
value_sub_concat (pelts x) x.offset xd.offset (x.offset + s);
(* todo refl *)
assert { value (old x) sx =
(value !qp (sx - sy - !i)
+ qh * power radix (sx - sy - !i))
......@@ -5590,6 +5603,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
value (x at EndLoop) (sy - 1)
by pelts x = Map.set (pelts x at EndLoop) (x.offset + sy - 1) !x1 };
value_sub_tail (pelts x) x.offset (!xp.offset+1);
(* todo refl *)
assert { value (old x) sx =
(value q (sx - sy)
+ power radix (sx - sy) * qh)
......
......@@ -11,7 +11,7 @@ exception Exit
let debug = false
let print_id fmt id = Format.fprintf fmt "%s" id.id_string
let expl_reification_check = Ident.create_label "expl:reification check"
type reify_env = { kn: known_map;
......@@ -92,7 +92,33 @@ let rec reify_term renv t rt =
aux la1 la2
| _ -> raise NoReification
in
let renv, mvs = Svs.fold (rt_of_var p.pat_vars f t) p.pat_vars (renv, Mvs.empty) in
let rec check_nonvar f t =
match f.t_node, t.t_node with
| Tapp (ls1, la1), Tapp (ls2, la2) ->
if Svs.for_all (fun v -> t_v_occurs v f = 0) p.pat_vars
then (if not (ls_equal ls1 ls2)
then raise NoReification);
if ls_equal ls1 ls2 then List.iter2 check_nonvar la1 la2;
| Tapp (ls,_), Tconst _ ->
(* reject constants that do not match the
definitions of logic constants*)
if Svs.for_all (fun v -> t_v_occurs v f = 0) p.pat_vars
then
match find_logic_definition renv.kn ls with
| None -> raise NoReification
| Some ld -> let v,f = open_ls_defn ld in
assert (v = []);
check_nonvar f t
else ()
| Tconst (Number.ConstInt c1), Tconst (Number.ConstInt c2) ->
let open Number in
if not (BigInt.eq (compute_int_constant c1) (compute_int_constant c2))
then raise NoReification
| _ -> () (* FIXME add more failure cases if needed *)
in
check_nonvar f t;
let renv, mvs = Svs.fold (rt_of_var p.pat_vars f t) p.pat_vars
(renv, Mvs.empty) in
let lrt = List.map (function | {pat_node = Pvar v} -> Mvs.find v mvs
| _ -> assert false) pl in
renv, t_app cs lrt (Some p.pat_ty)
......@@ -462,7 +488,7 @@ let build_goals prev prs subst env lp g rt =
l rl
| _,_ when g.t_ty <> None -> t_equ (t_subst subst rt) g
| _ -> raise Exit in
if debug then Format.printf "cut ok@.";
if debug then Format.printf "cut ok@.";
Trans.apply (Cut.cut ci (Some "interp")) task_r
with _ ->
if debug then Format.printf "no cut found@.";
......@@ -483,7 +509,7 @@ let build_goals prev prs subst env lp g rt =
try Lists.apply (Trans.apply (rewrite pr)) acc
with _ -> acc)
lt (List.rev prs)
| [] -> []
| _ -> assert false in
let lt = List.map (fun ng -> Task.add_decl prev
......@@ -534,19 +560,19 @@ and field = Fimmutable of value | Fmutable of value ref
open Format
let rec print_value fmt = function
| Vvoid -> fprintf fmt "Vvoid"
| Vbool b -> fprintf fmt "Vbool %b" b
| Vint i -> fprintf fmt "Vint %a" Number.print_constant (Number.const_of_big_int i)
| Vconstr (rs, lf) -> fprintf fmt "Vconstr(%a, %a)"
| Vvoid -> fprintf fmt "()"
| Vbool b -> fprintf fmt "%b" b
| Vint i -> fprintf fmt "%a" Number.print_constant (Number.const_of_big_int i)
| Vconstr (rs, lf) -> fprintf fmt "@[<hov 2>(%a@ %a)@]"
Expr.print_rs rs
(Pp.print_list Pp.space print_field) lf
| Varray a -> fprintf fmt "Varray [|%a|]"
| Varray a -> fprintf fmt "[|%a|]"
(Pp.print_list Pp.space print_value) (Array.to_list a)
| Vmatrix m -> fprintf fmt "Vmatrix %a" print_matrix m
| Vref r -> fprintf fmt "Vref %a" print_value !r
and print_field fmt = function
| Fimmutable v -> fprintf fmt "Fimmutable %a" print_value v
| Fimmutable v -> fprintf fmt "%a" print_value v
| Fmutable vr -> fprintf fmt "Fmutable %a" print_value !vr
and print_matrix fmt m =
Array.iter (fun a -> fprintf fmt "[|%a|]\n"
......@@ -752,6 +778,11 @@ let exec_ref_set _ args =
Vvoid
| _ -> raise CannotReduce
let exec_print _ args =
List.iter (eprintf "%a@." print_value) args;
Vvoid
let built_in_modules =
[
["bool"],"Bool", [],
......@@ -805,6 +836,9 @@ let built_in_modules =
"prefix !", exec_ref_get;
"infix :=", exec_ref_set;
] ;
["debug"],"Debug",
[],
["print", exec_print ] ;
]
let add_builtin_mo env (l,n,t,d) =
......@@ -1158,7 +1192,7 @@ let reflection_by_function s env = Trans.store (fun task ->
cs = [];
} in
if debug then Format.printf "eval_fun@.";
let res = term_of_value (eval_fun decl info) in
let res = term_of_value (eval_fun decl info) (*(try eval_fun decl info with Raised _ -> Vbool false)*) in
if debug then Format.printf "res %a@." Pretty.print_term res;
let rinfo = {renv with subst = Mvs.add vres res renv.subst} in
rinfo, lp, lv, rt
......
module Debug
type t = { mutable foo: unit }
val t: t
val print (x:'a) : unit writes { t }
end
\ No newline at end of file
......@@ -305,7 +305,7 @@ module PowerReal
use import FromInt
use import int.Power
axiom pow_from_int: forall x y: int. Int.(<=) 0 x -> Int.(<=) 0 y ->
lemma pow_from_int: forall x y: int. Int.(<) 0 x -> Int.(<=) 0 y ->
pow (from_int x) (from_int y) = from_int (power x y)
......
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