Commit 4bd34e25 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Support subtraction in exponents, two long division reflection examples

parent 49a49ca1
...@@ -1091,7 +1091,8 @@ use import debug.Debug ...@@ -1091,7 +1091,8 @@ use import debug.Debug
type evars = int -> int type evars = int -> int
type exp = Lit int | Var int | Plus exp exp | Minus exp
type exp = Lit int | Var int | Plus exp exp | Minus exp | Sub exp exp
type t = (Q.t, exp) type t = (Q.t, exp)
let constant mzero = (Q.rzero, Lit 0) let constant mzero = (Q.rzero, Lit 0)
...@@ -1109,6 +1110,7 @@ function interp_exp (e:exp) (y:evars) : int ...@@ -1109,6 +1110,7 @@ function interp_exp (e:exp) (y:evars) : int
| Lit n -> n | Lit n -> n
| Var v -> y v | Var v -> y v
| Plus e1 e2 -> interp_exp e1 y + interp_exp e2 y | Plus e1 e2 -> interp_exp e1 y + interp_exp e2 y
| Sub e1 e2 -> interp_exp e1 y - interp_exp e2 y
| Minus e' -> - (interp_exp e' y) | Minus e' -> - (interp_exp e' y)
end end
(* (*
...@@ -1126,56 +1128,101 @@ function minterp (t:t) (y:evars) : real ...@@ -1126,56 +1128,101 @@ function minterp (t:t) (y:evars) : real
exception Unknown exception Unknown
let rec opp_exp (e:exp)
ensures { forall y. interp_exp result y = - interp_exp e y }
variant { e }
= match e with
| Lit n -> Lit (-n)
| Minus e' -> e'
| Plus e1 e2 -> Plus (opp_exp e1) (opp_exp e2)
| Sub e1 e2 -> Sub e2 e1
| Var _ -> Minus e
end
let rec add_exp (e1 e2:exp) let rec add_sub_exp (e1 e2:exp) (s:bool) : exp
ensures { forall y. interp_exp result y = interp_exp e1 y + interp_exp e2 y } ensures { forall y.
if s
then interp_exp result y = interp_exp e1 y + interp_exp e2 y
else interp_exp result y = interp_exp e1 y - interp_exp e2 y }
raises { Unknown -> true } raises { Unknown -> true }
variant { e2, e1 } variant { e2, e1 }
= =
let rec add_atom (e a:exp) : (exp, bool) let rec add_atom (e a:exp) (s:bool) : (exp, bool)
returns { r, b -> forall y. interp_exp r y = interp_exp e y + interp_exp a y } returns { r, b -> forall y.
if s then interp_exp r y = interp_exp e y + interp_exp a y
else interp_exp r y = interp_exp e y - interp_exp a y }
raises { Unknown -> true } raises { Unknown -> true }
variant { e } variant { e }
= match (e,a) with = match (e,a) with
| Lit n1, Lit n2 -> (Lit (n1+n2), true) | Lit n1, Lit n2 -> (if s then Lit (n1+n2) else Lit (n1-n2)), true
| Lit n, Var i | Var i, Lit n | Lit n, Var i
-> if n = 0 then (Var i, true) else (Plus e a, False) -> if n = 0 then (if s then Var i else Minus (Var i)), true
| Lit n, Minus e' | Minus e', Lit n -> else (if s then Plus e a else Sub e a), False
if n = 0 then Minus e', True else Plus e a, False | Var i, Lit n
-> if n = 0 then Var i, true
else (if s then Plus e a else Sub e a), False
| Lit n, Minus e' ->
if n = 0 then (if s then Minus e' else e'), True
else (if s then Plus e a else Sub e a), False
| Minus e', Lit n ->
if n = 0 then Minus e', True
else (if s then Plus e a else Sub e a), False
| Var i, Minus (Var j) | Minus (Var j), Var i -> | Var i, Minus (Var j) | Minus (Var j), Var i ->
if i = j then (Lit 0, true) else (Plus e a, False) if s && (i = j) then (Lit 0, true)
| Var _, Var _ -> Plus e a, False else (if s then Plus e a else Sub e a), False
| Minus _, Minus _ -> Plus e a, False | Var i, Var j -> if s then Plus e a, False
else
if i = j then Lit 0, True
else Sub e a, False
| Minus _, Minus _ -> (if s then Plus e a else Sub e a), False
| Plus e1 e2, _ -> | Plus e1 e2, _ ->
let r, b = add_atom e1 a in let r, b = add_atom e1 a s in
if b then if b then
match r with match r with
| Lit n -> if n = 0 then e2, True else Plus r e2, True | Lit n -> if n = 0 then e2, True else Plus r e2, True
| _ -> Plus r e2, True | _ -> Plus r e2, True
end end
else let r, b = add_atom e2 a in Plus e1 r, b else let r, b = add_atom e2 a s in Plus e1 r, b
| Sub e1 e2, _ ->
let r, b = add_atom e1 a s in
if b then
match r with
| Lit n -> if n = 0 then opp_exp e2, True else Sub r e2, True
| _ -> Sub r e2, True
end
else let r, b = add_atom e2 a (not s) in
if b then Sub e1 r, True
else if s then Sub (Plus e1 a) e2, False
else Sub e1 (Plus e2 a), False
| _ -> raise Unknown | _ -> raise Unknown
end end
in in
match e2 with match e2 with
| Plus e1' e2' -> | Plus e1' e2' ->
let r = add_exp e1 e1' in let r = add_sub_exp e1 e1' s in
match r with match r with
| Lit n -> if n = 0 then e2' else add_exp r e2' | Lit n -> if n = 0
| _ -> add_exp r e2' then (if s then e2' else opp_exp e2')
else add_sub_exp r e2' s
| _ -> add_sub_exp r e2' s
end end
| _ -> let r, _ = add_atom e1 e2 in r | Sub e1' e2' ->
end let r = add_sub_exp e1 e1' s in
let rec opp_exp (e:exp) match r with
ensures { forall y. interp_exp result y = - interp_exp e y } | Lit n -> if n = 0
variant { e } then (if s then opp_exp e2' else e2')
= match e with else add_sub_exp r e2' (not s)
| Lit n -> Lit (-n) | _ -> add_sub_exp r e2' (not s)
| Minus e' -> e' end
| Plus e1 e2 -> Plus (opp_exp e1) (opp_exp e2) | _ -> let r, _ = add_atom e1 e2 s in r
| Var _ -> Minus e
end end
let add_exp (e1 e2:exp) : exp
ensures { forall y. interp_exp result y = interp_exp e1 y + interp_exp e2 y }
raises { Unknown -> True }
= add_sub_exp e1 e2 True
let rec zero_exp (e:exp) : bool let rec zero_exp (e:exp) : bool
ensures { result -> forall y. interp_exp e y = 0 } ensures { result -> forall y. interp_exp e y = 0 }
variant { e } variant { e }
...@@ -1189,6 +1236,7 @@ let rec zero_exp (e:exp) : bool ...@@ -1189,6 +1236,7 @@ let rec zero_exp (e:exp) : bool
| Var _ -> false | Var _ -> false
| Minus e -> all_zero e | Minus e -> all_zero e
| Plus e1 e2 -> all_zero e1 && all_zero e2 | Plus e1 e2 -> all_zero e1 && all_zero e2
| Sub e1 e2 -> all_zero e1 && all_zero e2
end end
in in
let e' = add_exp (Lit 0) e in (* simplifies exp *) let e' = add_exp (Lit 0) e in (* simplifies exp *)
......
...@@ -4525,16 +4525,28 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb ...@@ -4525,16 +4525,28 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
assert { power radix sy assert { power radix sy
= power radix (sy - 2) * radix * radix }; = power radix (sy - 2) * radix * radix };
assert { xp0 + radix * xp1 assert { xp0 + radix * xp1
+ radix * radix * !x1 at StartLoop + power radix 2 * !x1 at StartLoop (* radix * radix *)
- !ql * (dl + radix * dh) - !ql * (dl + radix * dh)
= rl + radix * rh }; = rl + radix * rh };
assert { value (xd at SubProd) sy begin ensures { value (xd at SubProd) sy
+ power radix sy * (!x1 at StartLoop) + power radix sy * (!x1 at StartLoop)
- !ql * vy - !ql * vy
= value xd (sy - 2) = value xd (sy - 2)
- power radix (sy - 2) * cy - power radix (sy - 2) * cy
+ power radix (sy - 2) * + power radix (sy - 2) *
(rl + radix * rh) (rl + radix * rh) }
assert { value (xd at SubProd) sy
= vlx + power radix (sy - 2) * xp0
+ power radix (sy - 1) * xp1 }; (*nonlinear*)
assert { !ql * vy = !ql * vly
+ power radix (sy - 2)
* (!ql * (dl + radix * dh)) }; (*nonlinear*)
(*assert { value (xd at SubProd) sy
+ power radix sy * (!x1 at StartLoop)
- !ql * vy
= value xd (sy - 2)
- power radix (sy - 2) * cy
+ power radix (sy - 2) * (rl + radix * rh)
by by
value (xd at SubProd) sy value (xd at SubProd) sy
+ power radix sy * (!x1 at StartLoop) + power radix sy * (!x1 at StartLoop)
...@@ -4573,7 +4585,14 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb ...@@ -4573,7 +4585,14 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
- power radix (sy - 2) * cy - power radix (sy - 2) * cy
+ power radix (sy - 2) * + power radix (sy - 2) *
(rl + radix * rh) (rl + radix * rh)
}; } *)
end;
begin ensures { value xd (sy - 2)
- power radix (sy - 2) * cy
+ power radix (sy - 2) * (rl + radix * rh)
= value xd (sy - 1)
+ power radix (sy - 1) * !x1
- power radix sy * cy2 }
value_sub_tail (pelts xd) xd.offset (xd.offset + p2i sy - 2); value_sub_tail (pelts xd) xd.offset (xd.offset + p2i sy - 2);
assert { value xd (sy - 1) assert { value xd (sy - 1)
= value xd (sy - 2) = value xd (sy - 2)
...@@ -4585,8 +4604,27 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb ...@@ -4585,8 +4604,27 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
+ power radix (sy - 2) * !x0 + power radix (sy - 2) * !x0
= value xd (sy - 2) = value xd (sy - 2)
+ power radix (sy - 2) * !x0 }; + power radix (sy - 2) * !x0 };
(* TODO refl *) assert { rl + radix * rh - cy
assert { value xd (sy - 2) = !x0 + radix * !x1 - power radix 2 * cy2
by
(!x0 - radix * cy1 = rl - cy
by
!x0 = mod (rl - cy) radix
so - radix < rl - cy < radix
so (if rl < cy
then cy1 = 1
/\ (- radix < rl - cy < 0
so
div (rl - cy) radix = - 1
so rl - cy
= radix * div (rl - cy) radix
+ mod (rl - cy) radix
= !x0 - radix
= !x0 - radix * cy1)
else cy1 = 0 /\ rl - cy = l2i !x0)) }
(* nonlinear *)
(* refl example *)
(* assert { value xd (sy - 2)
- power radix (sy - 2) * cy - power radix (sy - 2) * cy
+ power radix (sy - 2) * + power radix (sy - 2) *
(rl + radix * rh) (rl + radix * rh)
...@@ -4650,7 +4688,8 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb ...@@ -4650,7 +4688,8 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
= value xd (sy - 1) = value xd (sy - 1)
+ power radix (sy - 1) * !x1 + power radix (sy - 1) * !x1
- power radix sy * cy2 - power radix sy * cy2
}; }*)
end;
end; end;
if "ex:unlikely" (not (Limb.(=) cy2 limb_zero)) if "ex:unlikely" (not (Limb.(=) cy2 limb_zero))
then begin then begin
......
...@@ -6,7 +6,7 @@ open Task ...@@ -6,7 +6,7 @@ open Task
open Args_wrapper open Args_wrapper
exception NoReification exception NoReification
exception Exit exception Exit of string
let debug = false let debug = false
...@@ -443,7 +443,7 @@ let build_vars_map renv prev = ...@@ -443,7 +443,7 @@ let build_vars_map renv prev =
then Format.printf "vars not matched: %a@." then Format.printf "vars not matched: %a@."
(Pp.print_list Pp.space Pretty.print_vs) (Pp.print_list Pp.space Pretty.print_vs)
(List.filter (fun v -> not (Mvs.mem v subst)) renv.lv); (List.filter (fun v -> not (Mvs.mem v subst)) renv.lv);
raise Exit); raise (Exit "vars not matched"));
if debug then Format.printf "all vars matched@."; if debug then Format.printf "all vars matched@.";
let prev, prs = let prev, prs =
Mterm.fold Mterm.fold
...@@ -487,7 +487,7 @@ let build_goals prev prs subst env lp g rt = ...@@ -487,7 +487,7 @@ let build_goals prev prs subst env lp g rt =
(t_equ (t_subst subst rh) h) (t_equ (t_subst subst rh) h)
l rl l rl
| _,_ when g.t_ty <> None -> t_equ (t_subst subst rt) g | _,_ when g.t_ty <> None -> t_equ (t_subst subst rt) g
| _ -> raise Exit in | _ -> raise Not_found in
if debug then Format.printf "cut ok@."; if debug then Format.printf "cut ok@.";
Trans.apply (Cut.cut ci (Some "interp")) task_r Trans.apply (Cut.cut ci (Some "interp")) task_r
with _ -> with _ ->
...@@ -523,19 +523,17 @@ let reflection_by_lemma pr env : Task.task Trans.tlist = Trans.store (fun task - ...@@ -523,19 +523,17 @@ let reflection_by_lemma pr env : Task.task Trans.tlist = Trans.store (fun task -
let kn = task_known task in let kn = task_known task in
let g, prev = Task.task_separate_goal task in let g, prev = Task.task_separate_goal task in
let g = Apply.term_decl g in let g = Apply.term_decl g in
try if debug then Format.printf "start@.";
if debug then Format.printf "start@."; let d = Apply.find_hypothesis pr.pr_name prev in
let d = Apply.find_hypothesis pr.pr_name prev in if d = None then raise (Exit "lemma not found");
if d = None then raise Exit; let d = Opt.get d in
let d = Opt.get d in let l = Apply.term_decl d in
let l = Apply.term_decl d in let (lp, lv, rt) = Apply.intros l in
let (lp, lv, rt) = Apply.intros l in let nt = Args_wrapper.build_naming_tables task in
let nt = Args_wrapper.build_naming_tables task in let crc = nt.Trans.coercion in
let crc = nt.Trans.coercion in let renv = reify_term (init_renv kn crc lv env prev) g rt in
let renv = reify_term (init_renv kn crc lv env prev) g rt in let subst, prev, prs= build_vars_map renv prev in
let subst, prev, prs= build_vars_map renv prev in build_goals prev prs subst env lp g rt)
build_goals prev prs subst env lp g rt
with NoReification | Exit -> [task])
open Mltree open Mltree
open Expr open Expr
...@@ -1127,7 +1125,7 @@ let reflection_by_function s env = Trans.store (fun task -> ...@@ -1127,7 +1125,7 @@ let reflection_by_function s env = Trans.store (fun task ->
let rs = Pmodule.ns_find_rs pmod.Pmodule.mod_export [s] in let rs = Pmodule.ns_find_rs pmod.Pmodule.mod_export [s] in
if o = None then Some (pmod, rs) if o = None then Some (pmod, rs)
else (if debug then Format.printf "Name conflict %s@." s; else (if debug then Format.printf "Name conflict %s@." s;
raise Exit) raise (Exit "module found twice"))
with Not_found -> o) with Not_found -> o)
ths None in ths None in
let (_pmod, rs) = if o = None let (_pmod, rs) = if o = None
...@@ -1138,7 +1136,7 @@ let reflection_by_function s env = Trans.store (fun task -> ...@@ -1138,7 +1136,7 @@ let reflection_by_function s env = Trans.store (fun task ->
let lpost = List.map open_post rs.rs_cty.cty_post in let lpost = List.map open_post rs.rs_cty.cty_post in
if List.exists (fun pv -> pv.pv_ghost) rs.rs_cty.cty_args if List.exists (fun pv -> pv.pv_ghost) rs.rs_cty.cty_args
then (if debug then Format.printf "ghost parameter@."; then (if debug then Format.printf "ghost parameter@.";
raise Exit); raise (Exit "function has ghost parameters"));
if debug then Format.printf "building module map@."; if debug then Format.printf "building module map@.";
let mm = Mid.fold let mm = Mid.fold
(fun id th acc -> (fun id th acc ->
......
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