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

Update sessions

parent d7f70bf2
...@@ -654,6 +654,8 @@ let predicate eq0_int (x:int) = x = 0 ...@@ -654,6 +654,8 @@ let predicate eq0_int (x:int) = x = 0
clone export ringdecision.AssocAlgebraDecision with type r = int, type a = mat, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = (*), val azero = mzero, val aone = id, val aplus = add, val aopp = opp, val atimes = mul, val asub = sub, val ($) = extp, goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc, goal A.Mul_distr_l, goal A.Mul_distr_r, goal asub_def, goal A.Inv_def_l, goal A.Inv_def_r, clone export ringdecision.AssocAlgebraDecision with type r = int, type a = mat, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = (*), val azero = mzero, val aone = id, val aplus = add, val aopp = opp, val atimes = mul, val asub = sub, val ($) = extp, goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc, goal A.Mul_distr_l, goal A.Mul_distr_r, goal asub_def, goal A.Inv_def_l, goal A.Inv_def_r,
axiom . (* FIXME: replace with "goal" and prove *) axiom . (* FIXME: replace with "goal" and prove *)
meta reflection val norm_f
end end
module MatrixTests module MatrixTests
......
...@@ -328,7 +328,7 @@ ...@@ -328,7 +328,7 @@
<goal name="VC wmpn_add_n.12.0.0" expl="assertion" proved="true"> <goal name="VC wmpn_add_n.12.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision"> <transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC wmpn_add_n.12.0.0.0" expl="assertion" proved="true"> <goal name="VC wmpn_add_n.12.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.22"/></proof> <proof prover="0"><result status="valid" time="0.36"/></proof>
</goal> </goal>
<goal name="VC wmpn_add_n.12.0.0.1" proved="true"> <goal name="VC wmpn_add_n.12.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof> <proof prover="3"><result status="valid" time="0.17"/></proof>
...@@ -428,7 +428,7 @@ ...@@ -428,7 +428,7 @@
<goal name="VC wmpn_add.12.0.0" expl="assertion" proved="true"> <goal name="VC wmpn_add.12.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision"> <transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC wmpn_add.12.0.0.0" expl="assertion" proved="true"> <goal name="VC wmpn_add.12.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.23"/></proof> <proof prover="0"><result status="valid" time="0.36"/></proof>
</goal> </goal>
<goal name="VC wmpn_add.12.0.0.1" proved="true"> <goal name="VC wmpn_add.12.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof> <proof prover="3"><result status="valid" time="0.16"/></proof>
......
This diff is collapsed.
...@@ -988,6 +988,8 @@ use real.FromInt ...@@ -988,6 +988,8 @@ use real.FromInt
clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = QError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal . clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = QError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal .
meta reflection val decision
end end
module LinearDecisionInt module LinearDecisionInt
...@@ -1110,6 +1112,8 @@ let int_decision (l: context') (g: equality') : bool ...@@ -1110,6 +1112,8 @@ let int_decision (l: context') (g: equality') : bool
= let l',g' = m_ctx l g in = let l',g' = m_ctx l g in
R.decision l' g' R.decision l' g'
meta reflection val int_decision
end end
...@@ -1555,6 +1559,8 @@ let mp_decision (l: context') (g: equality') : bool ...@@ -1555,6 +1559,8 @@ let mp_decision (l: context') (g: equality') : bool
= =
R.decision (m_ctx l) (m_eq g) R.decision (m_ctx l) (m_eq g)
meta reflection val mp_decision
end end
module EqPropMP module EqPropMP
...@@ -1968,6 +1974,8 @@ let prop_ctx (l:context') (g:equality') : (context', equality') ...@@ -1968,6 +1974,8 @@ let prop_ctx (l:context') (g:equality') : (context', equality')
= let l', g' = prop_ctx l g in = let l', g' = prop_ctx l g in
mp_decision l' g' mp_decision l' g'
meta reflection val prop_mp_decision
end end
module TestMP module TestMP
...@@ -2048,6 +2056,9 @@ function interp (f:fmla) (b: int -> value) : bool = ...@@ -2048,6 +2056,9 @@ function interp (f:fmla) (b: int -> value) : bool =
let f (f:fmla) : bool let f (f:fmla) : bool
ensures { result -> forall b. interp f b } ensures { result -> forall b. interp f b }
= false = false
meta reflection val f
end end
(* (*
module TestFmla module TestFmla
......
This diff is collapsed.
...@@ -496,7 +496,7 @@ ...@@ -496,7 +496,7 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.44" steps="59"/></proof> <proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.44" steps="59"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub.36" expl="loop invariant init" proved="true"> <goal name="VC wmpn_sub.36" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof> <proof prover="2"><result status="valid" time="0.20"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub.37" expl="assertion" proved="true"> <goal name="VC wmpn_sub.37" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof> <proof prover="2"><result status="valid" time="0.05"/></proof>
...@@ -505,7 +505,7 @@ ...@@ -505,7 +505,7 @@
<proof prover="5"><result status="valid" time="0.47" steps="82"/></proof> <proof prover="5"><result status="valid" time="0.47" steps="82"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub.39" expl="precondition" proved="true"> <goal name="VC wmpn_sub.39" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.12"/></proof> <proof prover="2"><result status="valid" time="0.24"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub.40" expl="precondition" proved="true"> <goal name="VC wmpn_sub.40" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof> <proof prover="3"><result status="valid" time="0.04"/></proof>
...@@ -520,7 +520,7 @@ ...@@ -520,7 +520,7 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.30" steps="78"/></proof> <proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.30" steps="78"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub.44" expl="integer overflow" proved="true"> <goal name="VC wmpn_sub.44" expl="integer overflow" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.52" steps="96"/></proof> <proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.34" steps="96"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub.45" expl="loop variant decrease" proved="true"> <goal name="VC wmpn_sub.45" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
...@@ -544,7 +544,7 @@ ...@@ -544,7 +544,7 @@
<proof prover="2"><result status="valid" time="0.25"/></proof> <proof prover="2"><result status="valid" time="0.25"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub.52" expl="postcondition" proved="true"> <goal name="VC wmpn_sub.52" expl="postcondition" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.48" steps="67"/></proof> <proof prover="5" timelimit="5"><result status="valid" time="0.27" steps="67"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub.53" expl="assertion" proved="true"> <goal name="VC wmpn_sub.53" expl="assertion" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.19" steps="54"/></proof> <proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.19" steps="54"/></proof>
...@@ -782,7 +782,7 @@ ...@@ -782,7 +782,7 @@
<goal name="VC wmpn_sub_in_place.15.0.0" expl="assertion" proved="true"> <goal name="VC wmpn_sub_in_place.15.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision"> <transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC wmpn_sub_in_place.15.0.0.0" expl="assertion" proved="true"> <goal name="VC wmpn_sub_in_place.15.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="4.32"/></proof> <proof prover="0"><result status="valid" time="3.70"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub_in_place.15.0.0.1" proved="true"> <goal name="VC wmpn_sub_in_place.15.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.30"/></proof> <proof prover="3"><result status="valid" time="0.30"/></proof>
...@@ -861,7 +861,7 @@ ...@@ -861,7 +861,7 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.05" steps="52"/></proof> <proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.05" steps="52"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub_in_place.35" expl="assertion" proved="true"> <goal name="VC wmpn_sub_in_place.35" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.61"/></proof> <proof prover="0"><result status="valid" time="0.43"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub_in_place.36" expl="assertion" proved="true"> <goal name="VC wmpn_sub_in_place.36" expl="assertion" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
...@@ -1083,10 +1083,10 @@ ...@@ -1083,10 +1083,10 @@
<proof prover="3"><result status="valid" time="0.13"/></proof> <proof prover="3"><result status="valid" time="0.13"/></proof>
</goal> </goal>
<goal name="VC wmpn_decr.20" expl="assertion" proved="true"> <goal name="VC wmpn_decr.20" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof> <proof prover="2"><result status="valid" time="0.36"/></proof>
</goal> </goal>
<goal name="VC wmpn_decr.21" expl="assertion" proved="true"> <goal name="VC wmpn_decr.21" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.53" steps="55"/></proof> <proof prover="5"><result status="valid" time="0.86" steps="55"/></proof>
</goal> </goal>
<goal name="VC wmpn_decr.22" expl="precondition" proved="true"> <goal name="VC wmpn_decr.22" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.07"/></proof> <proof prover="2"><result status="valid" time="0.07"/></proof>
...@@ -1163,7 +1163,7 @@ ...@@ -1163,7 +1163,7 @@
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC wmpn_decr.36" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_decr.36" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.60"/></proof> <proof prover="0"><result status="valid" time="0.44"/></proof>
</goal> </goal>
<goal name="VC wmpn_decr.37" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_decr.37" expl="loop invariant preservation" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.06"/></proof> <proof prover="2" timelimit="5"><result status="valid" time="0.06"/></proof>
...@@ -1463,7 +1463,7 @@ ...@@ -1463,7 +1463,7 @@
<proof prover="2"><result status="valid" time="0.15"/></proof> <proof prover="2"><result status="valid" time="0.15"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub_1_in_place.15" expl="assertion" proved="true"> <goal name="VC wmpn_sub_1_in_place.15" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.76"/></proof> <proof prover="2"><result status="valid" time="0.99"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub_1_in_place.16" expl="precondition" proved="true"> <goal name="VC wmpn_sub_1_in_place.16" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof> <proof prover="2"><result status="valid" time="0.05"/></proof>
...@@ -1475,10 +1475,10 @@ ...@@ -1475,10 +1475,10 @@
<proof prover="2"><result status="valid" time="0.16"/></proof> <proof prover="2"><result status="valid" time="0.16"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub_1_in_place.19" expl="assertion" proved="true"> <goal name="VC wmpn_sub_1_in_place.19" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.41"/></proof> <proof prover="2"><result status="valid" time="0.26"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub_1_in_place.20" expl="assertion" proved="true"> <goal name="VC wmpn_sub_1_in_place.20" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="1.10" steps="52"/></proof> <proof prover="5"><result status="valid" time="0.73" steps="52"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub_1_in_place.21" expl="precondition" proved="true"> <goal name="VC wmpn_sub_1_in_place.21" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof> <proof prover="2"><result status="valid" time="0.05"/></proof>
...@@ -1505,7 +1505,7 @@ ...@@ -1505,7 +1505,7 @@
<proof prover="2"><result status="valid" time="0.06"/></proof> <proof prover="2"><result status="valid" time="0.06"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub_1_in_place.29" expl="assertion" proved="true"> <goal name="VC wmpn_sub_1_in_place.29" expl="assertion" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="1.22" steps="66"/></proof> <proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="1.49" steps="66"/></proof>
</goal> </goal>
<goal name="VC wmpn_sub_1_in_place.30" expl="loop variant decrease" proved="true"> <goal name="VC wmpn_sub_1_in_place.30" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.10"/></proof> <proof prover="2"><result status="valid" time="0.10"/></proof>
......
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