Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

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

Remove almost all by/so proofs in addition

parent 082d207d
......@@ -830,7 +830,6 @@ let rinv (a:t)
end
end
module LinearDecisionRational
use import RationalCoeffs
......@@ -1074,18 +1073,21 @@ let mmul (a b:t)
= match a, b with
| (q1,e1), (q2,e2) ->
let q = Q.rmul q1 q2 in
let e = add_exp e1 e2 in
assert { forall y. minterp (q,e) y = minterp a y *. minterp b y
by let p1 = pow rradix (from_int (interp_exp e1 y)) in
let p2 = pow rradix (from_int (interp_exp e2 y)) in
let p = pow rradix (from_int (interp_exp e y)) in
interp_exp e y = interp_exp e1 y + interp_exp e2 y
so p = p1 *. p2
so minterp (q,e) y = qinterp q *. p
= (qinterp q1 *. qinterp q2) *. p
= (qinterp q1 *. qinterp q2) *. p1 *. p2
= minterp a y *. minterp b y };
(q,e)
if Q.req q Q.rzero then mzero
else begin
let e = add_exp e1 e2 in
assert { forall y. minterp (q,e) y = minterp a y *. minterp b y
by let p1 = pow rradix (from_int (interp_exp e1 y)) in
let p2 = pow rradix (from_int (interp_exp e2 y)) in
let p = pow rradix (from_int (interp_exp e y)) in
interp_exp e y = interp_exp e1 y + interp_exp e2 y
so p = p1 *. p2
so minterp (q,e) y = qinterp q *. p
= (qinterp q1 *. qinterp q2) *. p
= (qinterp q1 *. qinterp q2) *. p1 *. p2
= minterp a y *. minterp b y };
(q,e)
end
end
let mopp (a:t)
......@@ -1282,6 +1284,16 @@ goal g': forall a b i j: int.
i+1 = j ->
(power radix j) * a = radix*b
goal g'': forall r r' i c x x' y l: int.
c = 0 ->
r + power radix i * c = x + y ->
r' = r + power radix i * l ->
x' = x + power radix i * l ->
r' + power radix (i+1) * c = x' + y
(*tries to add power radix i and power radix (i+1), fails
-> cst propagation ? *)
end
module TI
......
......@@ -1895,7 +1895,7 @@
</transf>
</goal>
</theory>
<theory name="MP64Coeffs" proved="true" sum="59e49ba42437c8635bc3d6235c8d7438">
<theory name="MP64Coeffs" proved="true" sum="3a8c8b51b01ad073535e1a8f5b36fc15">
<goal name="VC mzero" expl="VC for mzero" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -2144,38 +2144,41 @@
</goal>
<goal name="VC mmul" expl="VC for mmul" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC mmul.0" expl="assertion" proved="true">
<goal name="VC mmul.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC mmul.1" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC mmul.0.0" expl="assertion" proved="true">
<goal name="VC mmul.1.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mmul.0.1" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="10"/></proof>
<goal name="VC mmul.1.1" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="13"/></proof>
</goal>
<goal name="VC mmul.0.2" expl="VC for mmul" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC mmul.1.2" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="VC mmul.0.3" expl="VC for mmul" proved="true">
<goal name="VC mmul.1.3" expl="VC for mmul" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mmul.0.4" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="8"/></proof>
<goal name="VC mmul.1.4" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="9"/></proof>
</goal>
<goal name="VC mmul.0.5" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="9"/></proof>
<goal name="VC mmul.1.5" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="12"/></proof>
</goal>
<goal name="VC mmul.0.6" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
<goal name="VC mmul.1.6" expl="VC for mmul" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="13"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mmul.1" expl="postcondition" proved="true">
<goal name="VC mmul.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mmul.2" expl="exceptional postcondition" proved="true">
<goal name="VC mmul.3" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mmul.3" expl="exceptional postcondition" proved="true">
<goal name="VC mmul.4" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
......@@ -2438,7 +2441,7 @@
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
</theory>
<theory name="TestMP" proved="true" sum="affc07b7daa8e76697c500d698debc64">
<theory name="TestMP" sum="e261877e08f5a8ba4f1586cc3e8e3b4f">
<goal name="g" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="g.0" expl="reification check" proved="true">
......@@ -2514,6 +2517,22 @@
</goal>
</transf>
</goal>
<goal name="g&#39;&#39;">
<transf name="replace" arg1="c" arg2="0">
<goal name="g&#39;&#39;.0">
<transf name="replace" arg1="c" arg2="0" arg3="in" arg4="H2">
<goal name="g&#39;&#39;.0.0">
</goal>
<goal name="g&#39;&#39;.0.1" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="g&#39;&#39;.1" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="TI" sum="f65ffb4d889019a8435ba0d47668c91d">
<goal name="g">
......
......@@ -509,14 +509,12 @@ module N
value x !i + value y !i
by value r !i = (value r !i at StartLoop) };
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);
value_sub_tail (pelts y) y.offset (y.offset + k);
assert { value r !i + (power radix !i) * !c =
value x !i + value y !i
by
value_tail r !i;
value_tail x !i;
value_tail y !i;
assert { value r (!i+1) + (power radix (!i+1)) * !c =
value x (!i+1) + value y (!i+1)
(*by
value r !i + (power radix !i) * !c
= value r k + (power radix k) * res
+ (power radix !i) * !c
......@@ -535,7 +533,8 @@ module N
+ value y k + (power radix k) * !ly
= value x !i
+ (value y k + (power radix k) * !ly)
= value x !i + value y !i }
= value x !i + value y !i*) };
i := Int32.(+) !i (Int32.of_int 1);
done;
!c
......@@ -571,14 +570,12 @@ module N
assert { value r !i + (power radix !i) * !c =
value x !i + value y !i };
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);
value_sub_tail (pelts y) y.offset (y.offset + k);
assert { value r !i + (power radix !i) * !c =
value x !i + value y !i
by
value_tail r !i;
value_tail x !i;
value_tail y !i;
assert { value r (!i+1) + (power radix (!i+1)) * !c =
value x (!i+1) + value y (!i+1)
(*by
value r !i + (power radix !i) * !c
= value r k + (power radix k) * res
+ (power radix !i) * !c
......@@ -597,7 +594,8 @@ module N
+ value y k + (power radix k) * !ly
= value x !i
+ (value y k + (power radix k) * !ly)
= value x !i + value y !i };
= value x !i + value y !i*) };
i := Int32.(+) !i (Int32.of_int 1);
done;
try
begin while Int32.(<) !i sx do
......@@ -614,13 +612,11 @@ module N
assert { value r !i + (power radix !i) * !c =
value x !i + value y sy };
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 + value y sy
by
value_tail r !i;
value_tail x !i;
assert { value r (!i+1) + (power radix (!i+1)) * !c =
value x (!i+1) + value y sy
(*by
value r !i + (power radix !i) * !c
= value r k + (power radix k) * res
+ (power radix !i) * !c
......@@ -634,7 +630,8 @@ module N
= value x k + value y sy
+ (power radix k) * !lx
= value x !i
+ value y sy }
+ value y sy*) };
i := Int32.(+) !i (Int32.of_int 1);
done;
assert { !i = sx }
end
......@@ -649,12 +646,14 @@ module N
assert { !c = 0 by !i < sx };
lx := get_ofs x !i;
set_ofs r !i !lx;
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 + value y sy
(*assert { value r !i + (power radix !i) * !c =
value x !i + value y sy };*) (* false without this, cannotreduce with this *)
value_tail r !i;
value_tail x !i;
assert { value r !i = value x !i + value y sy }; (* true with this, should not be needed *)
assert { value r (!i+1) + power radix (!i+1) * !c
= value x (!i+1) + value y sy
(*
by
value r !i + power radix !i * !c
= value r !i
......@@ -663,8 +662,8 @@ module N
= value x k + power radix k * !lx
so value r k
= value r k + power radix k * !c
= value x k + value y sy
}
= value x k + value y sy*) };
i := Int32.(+) !i (Int32.of_int 1);
done;
!c
......@@ -697,7 +696,7 @@ module N
(pelts x)[j] = (pelts (old x))[j] }
label StartLoop in
lx := get_ofs x !i;
assert { !lx = (pelts ox)[x.offset + !i] };
assert { !lx = (pelts ox)[ox.offset + !i] };
ly := get_ofs y !i;
let res, carry = add_with_carry !lx !ly !c in
set_ofs x !i res;
......@@ -709,14 +708,12 @@ module N
= (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
i := Int32.(+) !i (Int32.of_int 1);
value_sub_tail (pelts x) x.offset (x.offset + k);
value_sub_tail (pelts ox) x.offset (x.offset + k);
value_sub_tail (pelts y) y.offset (y.offset + k);
assert { value x !i + (power radix !i) * !c =
value ox !i + value y !i
by value ox k + (power radix k) * !lx
value_tail x !i;
value_tail ox !i;
value_tail y !i;
assert { value x (!i+1) + (power radix (!i+1)) * !c =
value ox (!i+1) + value y (!i+1)
(*by value ox k + (power radix k) * !lx
= value ox !i
so value x !i + (power radix !i) * !c
= value x k + (power radix k) * res
......@@ -736,7 +733,8 @@ module N
+ (value y k + (power radix k) * !ly)
= value ox !i
+ (value y k + (power radix k) * !ly)
= value ox !i + value y !i };
= value ox !i + value y !i*) };
i := Int32.(+) !i (Int32.of_int 1);
done;
try
while Int32.(<) !i sx do
......@@ -752,7 +750,7 @@ module N
(if (Limb.(=) !c limb_zero) then raise ReturnLimb limb_zero);
label StartLoop2 in
lx := get_ofs x !i;
assert { !lx = (pelts ox)[x.offset + !i] };
assert { !lx = (pelts ox)[ox.offset + !i] };
let res, carry = add_with_carry !lx limb_zero !c in
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
......@@ -760,15 +758,13 @@ module N
set_ofs x !i res;
assert { value x !i + (power radix !i) * !c = value ox !i + value y sy };
c := carry;
let ghost k = p2i !i in
i := Int32.(+) !i (Int32.of_int 1);
assert { forall j. !i <= j < sx ->
assert { forall j. !i < j < sx ->
(pelts x)[x.offset + j] = (pelts ox) [x.offset + j] };
value_sub_tail (pelts ox) x.offset (x.offset + k);
value_sub_tail (pelts x) x.offset (x.offset + k);
assert { value x !i + (power radix !i) * !c =
value ox !i + value y sy
by value ox k + (power radix k) * !lx
value_tail ox !i;
value_tail x !i;
assert { value x (!i+1) + (power radix (!i+1)) * !c =
value ox (!i+1) + value y sy
(*by value ox k + (power radix k) * !lx
= value ox !i
so
value x !i + (power radix !i) * !c
......@@ -784,7 +780,8 @@ module N
= value ox k + value y sy
+ (power radix k) * !lx
= value ox !i
+ value y sy }
+ value y sy*) };
i := Int32.(+) !i (Int32.of_int 1);
done;
assert { !i = sx };
!c
......@@ -798,17 +795,7 @@ module N
value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sx);
value_sub_concat (pelts x) x.offset (x.offset + p2i !i) (x.offset + p2i sx);
value_sub_concat (pelts ox) x.offset (x.offset + p2i !i) (x.offset + p2i sx);
assert { value x sx = value (old x) sx + value y sy
by value x sx
= value x !i
+ (power radix !i)
* value_sub (pelts ox) (x.offset + !i) (x.offset + sx)
= value ox !i
+ (power radix !i)
* value_sub (pelts ox) (x.offset + !i) (x.offset + sx)
+ value y sy
= value_sub (pelts ox) x.offset (x.offset + sx) + value y sy
= value ox sx + value y sy };
assert { value x sx = value (old x) sx + value y sy };
n
end
end
......@@ -843,13 +830,11 @@ module N
assert { value r !i - power radix !i * !b =
value x !i - y };
b := borrow;
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 * !b
= value x !i - y
by
value_tail r !i;
value_tail x !i;
assert { value r (!i+1) - power radix (!i+1) * !b
= value x (!i+1) - y
(*by
value r !i - power radix !i * !b
= value r k + power radix k * res
- power radix !i * !b
......@@ -861,8 +846,9 @@ module N
= value r k - power radix k * (!b 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 !b
else begin
......
......@@ -162,7 +162,7 @@ let rec reify_term renv t rt =
| _ -> t (* FIXME some cases missing *)
in
t_label ?loc:t.t_loc Slab.empty t
in
in
let t = rm t in
(* remove labels to identify terms that are equal modulo labels *)
if Mterm.mem t renv.store
......@@ -486,7 +486,10 @@ open Expr
open Ity
exception CannotReduce
exception Raised of string * string
let append l = List.fold_left (fun acc s -> acc^":"^s) "" l
type value =
| Vconstr of rsymbol * field list
| Vint of BigInt.t
......@@ -560,20 +563,17 @@ let get_decl env mm rs =
if debug then Format.printf "pmodule %s@."
(pm.Pmodule.mod_theory.Theory.th_name.id_string);
let tm = translate_module pm in
if Mid.mem id tm.mod_known
then Mid.find id tm.mod_known
else
let pd = Mid.find id tm.mod_from.from_km in
match pd.pd_node with
| PDtype l ->
let rec aux = function
| [] -> raise Not_found
| d::t -> if List.mem rs d.itd_constructors then raise Constructor
else if List.mem rs d.itd_fields then raise Field
else aux t
in
aux l
| _ -> raise Not_found
let pd = Mid.find id tm.mod_from.from_km in
match pd.pd_node with
| PDtype l ->
let rec aux = function
| [] -> raise Not_found
| d::t -> if List.mem rs d.itd_constructors then raise Constructor
else if List.mem rs d.itd_fields then raise Field
else aux t
in
aux l
| _ -> Mid.find id tm.mod_known
let builtin_progs = Hrs.create 17
......@@ -801,6 +801,7 @@ type info = {
vars: value Mid.t;
recs: rsymbol Mrs.t;
funs: decl Mrs.t;
cs: string list; (* callstack for debugging *)
}
let print_id fmt id = fprintf fmt "%s" id.id_string
......@@ -854,7 +855,7 @@ let rec interp_expr info (e:Mltree.expr) : value =
raise CannotReduce)
| Eapp (rs, le) -> begin
if debug then Format.printf "Eapp %a@." Expr.print_rs rs;
let eval_call info vl e =
let eval_call info vl e rs =
if debug then Format.printf "eval params@.";
let info' =
List.fold_left2
......@@ -865,7 +866,7 @@ let rec interp_expr info (e:Mltree.expr) : value =
then Format.printf "arg %a : %a@." print_id id print_value v;
add_id id v info)
info le vl in
interp_expr info' e in
interp_expr { info' with cs = rs.rs_name.id_string::(info'.cs) } e in
if debug then Format.printf "eval call@.";
let res = try begin
let rs = if Mrs.mem rs info.recs then Mrs.find rs info.recs else rs in
......@@ -879,11 +880,11 @@ let rec interp_expr info (e:Mltree.expr) : value =
with Not_found -> get_decl info.env info.mm rs in
if debug then Format.printf "decl found@.";
match decl with
| Dlet (Lsym (_rs, _ty, vl, e)) ->
eval_call info vl e
| Dlet (Lsym (rs, _ty, vl, e)) ->
eval_call info vl e rs
| Dlet(Lrec([{rec_args = vl; rec_exp = e;
rec_sym = rs; rec_rsym = rrs; rec_res=_ty}])) ->
eval_call { info with recs = Mrs.add rrs rs info.recs } vl e
eval_call { info with recs = Mrs.add rrs rs info.recs } vl e rs
| Dlet (Lrec _) ->
if debug
then Format.printf "unhandled mutually recursive functions@.";
......@@ -1006,7 +1007,7 @@ let rec interp_expr info (e:Mltree.expr) : value =
interp_expr info e
| Eraise (xs,_) ->
if debug then Format.printf "Eraise %s@." xs.xs_name.id_string;
raise CannotReduce
raise (Raised (xs.xs_name.id_string, append info.cs))
| Eexn _ -> if debug then Format.printf "Eexn@.";
raise CannotReduce
| Eabsurd -> if debug then Format.printf "Eabsurd@.";
......@@ -1125,7 +1126,8 @@ let reflection_by_function s env = Trans.store (fun task ->
mm = mm;
funs = Mrs.empty;
recs = Mrs.empty;
vars = vars
vars = vars;
cs = [];
} in
if debug then Format.printf "eval_fun@.";
let res = term_of_value (eval_fun decl info) in
......
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