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

Simplify sqrt proof

parent 9bb0a1d1
......@@ -117,16 +117,9 @@ let sqrt1 (rp: ptr uint64) (a0: uint64): uint64
= from_int ((c+2) * (c+2))
};
let ref s = c * c in
assert { (c+1) * (c+1) <= radix
so iexp x = -32
so pow2 32 *. x <. pow2 32
so 0 <= Trunc.floor (pow2 32 *. x)
< power 2 32
so c < power 2 32
so c+1 <= power 2 32
so (c+1) * (c+1) <= power 2 32 * power 2 32 = radix };
assert { (c+1) * (c+1) <= radix };
assert { s + c <= s + c + c < (c+1) * (c+1) <= radix };
if (s + c + c <= a0 - 1)
if (s + 2 * c <= a0 - 1)
then begin
assert { (c+1) * (c+1) <= a0 };
s <- s + 2 * c + 1;
......
......@@ -27,7 +27,7 @@
<proof prover="8"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC trunc_lower_bound.0.2" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.14" steps="477"/></proof>
<proof prover="6"><result status="valid" time="0.14" steps="120"/></proof>
</goal>
<goal name="VC trunc_lower_bound.0.3" expl="assertion" proved="true">
<transf name="unfold" proved="true" arg1="trunc_at">
......@@ -42,7 +42,7 @@
</transf>
</goal>
<goal name="VC trunc_lower_bound.1" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.05" steps="135"/></proof>
<proof prover="6"><result status="valid" time="0.05" steps="141"/></proof>
<proof prover="8" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
......@@ -52,24 +52,16 @@
<goal name="VC sqrt1.0" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC sqrt1.0.0" expl="assertion" proved="true">
<transf name="rewrite" proved="true" arg1="H1">
<transf name="compute_hyp" proved="true" arg1="in" arg2="H1">
<goal name="VC sqrt1.0.0.0" expl="assertion" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="VC sqrt1.0.0.0.0" expl="assertion" proved="true">
<proof prover="7"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="VC sqrt1.0.1" expl="assertion" proved="true">
<transf name="rewrite" proved="true" arg1="H1">
<transf name="compute_hyp" proved="true" arg1="in" arg2="H1">
<goal name="VC sqrt1.0.1.0" expl="assertion" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="VC sqrt1.0.1.0.0" expl="assertion" proved="true">
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
......@@ -141,7 +133,7 @@
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC sqrt1.20.2" expl="VC for sqrt1" proved="true">
<proof prover="5" edited="sqrt_Sqrt1_VC_sqrt1_4.v"><result status="valid" time="0.58"/></proof>
<proof prover="5" edited="sqrt_Sqrt1_VC_sqrt1_4.v"><result status="valid" time="0.77"/></proof>
</goal>
</transf>
</goal>
......@@ -192,10 +184,10 @@
<goal name="VC sqrt1.24" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC sqrt1.24.0" expl="assertion" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.33"/></proof>
<proof prover="0" memlimit="2000"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC sqrt1.24.1" expl="VC for sqrt1" proved="true">
<proof prover="3"><result status="valid" time="2.81"/></proof>
<proof prover="3"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="VC sqrt1.24.2" expl="VC for sqrt1" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.20"/></proof>
......@@ -240,7 +232,7 @@
</transf>
</goal>
<goal name="VC sqrt1.24.14" expl="VC for sqrt1" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.61"/></proof>
<proof prover="0" memlimit="2000"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="VC sqrt1.24.15" expl="VC for sqrt1" proved="true">
<proof prover="8"><result status="valid" time="0.42"/></proof>
......@@ -273,7 +265,7 @@
</transf>
</goal>
<goal name="VC sqrt1.24.22" expl="VC for sqrt1" proved="true">
<proof prover="3"><result status="valid" time="1.28"/></proof>
<proof prover="3"><result status="valid" time="1.56"/></proof>
</goal>
<goal name="VC sqrt1.24.23" expl="VC for sqrt1" proved="true">
<proof prover="8"><result status="valid" time="0.04"/></proof>
......@@ -289,43 +281,7 @@
<goal name="VC sqrt1.26" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC sqrt1.26.0" expl="assertion" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="VC sqrt1.26.1" expl="VC for sqrt1" proved="true">
<proof prover="8"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC sqrt1.26.2" expl="VC for sqrt1" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC sqrt1.26.3" expl="VC for sqrt1" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC sqrt1.26.4" expl="VC for sqrt1" proved="true">
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC sqrt1.26.5" expl="VC for sqrt1" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.36"/></proof>
<proof prover="8"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC sqrt1.26.6" expl="VC for sqrt1" proved="true">
<proof prover="8"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC sqrt1.26.7" expl="VC for sqrt1" proved="true">
<transf name="apply" proved="true" arg1="prod_compat_lr">
<goal name="VC sqrt1.26.7.0" expl="apply premises" proved="true">
<proof prover="8"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC sqrt1.26.7.1" expl="apply premises" proved="true">
<proof prover="8"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
<goal name="VC sqrt1.26.8" expl="VC for sqrt1" proved="true">
<transf name="use_th" proved="true" arg1="logical.Logical">
<goal name="VC sqrt1.26.8.0" expl="VC for sqrt1" proved="true">
<proof prover="8"><result status="valid" time="0.20"/></proof>
</goal>
</transf>
<proof prover="0" memlimit="2000"><result status="valid" time="0.24"/></proof>
</goal>
</transf>
</goal>
......@@ -336,10 +292,10 @@
<proof prover="8"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC sqrt1.29" expl="integer overflow" proved="true">
<proof prover="8"><result status="valid" time="0.18"/></proof>
<proof prover="8"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC sqrt1.30" expl="integer overflow" proved="true">
<proof prover="8"><result status="valid" time="0.21"/></proof>
<proof prover="8"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC sqrt1.31" expl="assertion" proved="true">
<proof prover="8"><result status="valid" time="0.13"/></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