Skip to content

GitLab

Commit 336a5988 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

isqrt von neumann, slightly better looking specs

parent f372f1fd
Hide whitespace changes
Inline Side-by-side
Showing with 55 additions and 92 deletions
examples/in_progress/isqrt_von_neumann.mlw
View file @ 336a5988
......@@ -37,11 +37,10 @@ module VonNeumann16
lemma sqr_add: forall x y.
sqr (add x y) = add (sqr x) (add (sqr y) (mul (2:t) (mul x y)))
lemma sqr_aux: forall x. pred (sqr x) = mul (succ x) (pred x)
let isqrt16 (x:t) : t
ensures { ule (sqr result) x }
ensures { result = (0xff:t) \/ ult x (sqr (succ result)) }
ensures { ule x (pred (sqr (succ result))) }
= let num = ref x in
let bits = ref (0x4000:t) in
let res = ref (0:t) in
......@@ -64,10 +63,10 @@ module VonNeumann16
invariant { !res = mul !res_g (pow2 !m) }
(* num <= x *)
invariant { ule !num x }
(* (x - num) est le carré de (res / 2^m) *)
(* (x - num) is the square of (res / 2^m) *)
invariant { sub x !num = sqr !res_g }
(* x < (res_g + 2^m)^2 *)
invariant { ule x (mul (succ (add !res_g (pow2 !m))) (pred (add !res_g (pow2 !m)))) }
invariant { ule x (pred (sqr (add !res_g (pow2 !m)))) }
(* m is not null, let's subtract 1 *)
assert { !m <> (0:t) };
......@@ -93,15 +92,6 @@ module VonNeumann16
bits := lsr_bv !bits (2:t);
ghost bits_g := lsr_bv !bits_g (1:t)
done;
assert { !m = (0:t) };
assert { !bits = (0:t) };
assert { !res = !res_g };
assert { pred (sqr (add !res_g (pow2 !m))) =
mul (succ (add !res_g (pow2 !m))) (pred (add !res_g (pow2 !m))) };
assert { ule x (pred (sqr (add !res_g (pow2 !m)))) };
assert { !res_g <> (0xff:t) -> sqr (add !res_g (pow2 !m)) <> (0:t) };
assert { !res_g <> (0xff:t) -> ult x (sqr (add !res_g (pow2 !m))) };
assert { sqr (succ !res) = add (sqr !res_g) (succ (mul (2:t) !res_g)) };
!res
......@@ -127,7 +117,7 @@ module VonNeumann32
let isqrt32 (x:t) : t
ensures { ule (sqr result) x }
(* ensures { ult x (sqr (succ result)) } *)
ensures { ule x (pred (sqr (succ result))) }
= let num = ref x in
let bits = ref (0x4000_0000:t) in
let res = ref (0:t) in
......@@ -153,7 +143,7 @@ module VonNeumann32
(* (x - num) est le carré de (res / 2^m) *)
invariant { sub x !num = sqr !res_g }
(* x < (res_g + 2^m)^2 *)
(* invariant { ule x (mul (succ (add !res_g (pow2 !m))) (pred (add !res_g (pow2 !m)))) } *)
invariant { ule x (pred (sqr (add !res_g (pow2 !m)))) }
(* m is not null, let's subtract 1 *)
assert { !m <> (0:t) };
......@@ -179,10 +169,6 @@ module VonNeumann32
bits := lsr_bv !bits (2:t);
ghost bits_g := lsr_bv !bits_g (1:t)
done;
assert { !m = (0:t) };
assert { !bits = (0:t) };
assert { !res = !res_g };
(* assert { sqr (succ !res) = add (sqr !res_g) (succ (mul (2:t) !res_g)) }; *)
!res
......
examples/in_progress/isqrt_von_neumann/why3session.xml
View file @ 336a5988
......@@ -2,16 +2,13 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="10" steplimit="0" memlimit="4000"/>
<prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.5.0" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../isqrt_von_neumann.mlw">
<theory name="VonNeumann16" proved="true" sum="e6a5a1392e4ffc4ff0165c0a97c9c6bb">
<theory name="VonNeumann16" proved="true" sum="32580a96cc2876e931733b50e7669e08">
<goal name="sqr_add" proved="true">
<proof prover="2"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="sqr_aux" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="WP_parameter isqrt16" expl="VC for isqrt16" proved="true">
<transf name="split_goal_wp" proved="true" >
......@@ -91,10 +88,10 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt16.25" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.19"/></proof>
<proof prover="3"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="WP_parameter isqrt16.26" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter isqrt16.27" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
......@@ -124,45 +121,21 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt16.36" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.30"/></proof>
<proof prover="3"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="WP_parameter isqrt16.37" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter isqrt16.38" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter isqrt16.39" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt16.40" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt16.41" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter isqrt16.42" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt16.43" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter isqrt16.44" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter isqrt16.45" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter isqrt16.46" expl="postcondition" proved="true">
<goal name="WP_parameter isqrt16.38" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt16.47" expl="postcondition" proved="true">
<goal name="WP_parameter isqrt16.39" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="VonNeumann32" proved="true" sum="8e1a9d900bdb355c2842f839332b3c88">
<theory name="VonNeumann32" proved="true" sum="dd1a80231290e50bf0fd34021caba643">
<goal name="sqr_add" proved="true">
<proof prover="2" timelimit="10" memlimit="4000"><result status="valid" time="6.44"/></proof>
</goal>
......@@ -192,11 +165,11 @@
<goal name="WP_parameter isqrt32.7" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt32.8" expl="assertion" proved="true">
<goal name="WP_parameter isqrt32.8" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt32.9" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt32.10" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -205,64 +178,64 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt32.12" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.11"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt32.13" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="WP_parameter isqrt32.14" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof>
<proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter isqrt32.15" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.18"/></proof>
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter isqrt32.16" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.19"/></proof>
<proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="WP_parameter isqrt32.17" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.10"/></proof>
<goal name="WP_parameter isqrt32.17" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="WP_parameter isqrt32.18" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.12"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter isqrt32.19" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.25"/></proof>
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter isqrt32.20" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.14"/></proof>
<proof prover="3"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="WP_parameter isqrt32.21" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.11"/></proof>
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter isqrt32.22" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="WP_parameter isqrt32.23" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.18"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt32.24" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="6.90"/></proof>
<proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="WP_parameter isqrt32.25" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
<goal name="WP_parameter isqrt32.25" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="8.37"/></proof>
</goal>
<goal name="WP_parameter isqrt32.26" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.10"/></proof>
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter isqrt32.27" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.11"/></proof>
<goal name="WP_parameter isqrt32.27" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter isqrt32.28" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.24"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter isqrt32.29" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.15"/></proof>
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="WP_parameter isqrt32.30" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter isqrt32.31" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter isqrt32.32" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -270,27 +243,30 @@
<goal name="WP_parameter isqrt32.33" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt32.34" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter isqrt32.35" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter isqrt32.36" expl="assertion" proved="true">
<goal name="WP_parameter isqrt32.34" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt32.37" expl="assertion" proved="true">
<goal name="WP_parameter isqrt32.35" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt32.36" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="53.70"/></proof>
</goal>
<goal name="WP_parameter isqrt32.37" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter isqrt32.38" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter isqrt32.39" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="VonNeumann64" sum="42db8390aa6dc4c5529653c2244d8e31">
<goal name="sqr_add">
<proof prover="2" timelimit="60"><result status="timeout" time="60.00"/></proof>
<proof prover="2"><result status="timeout" time="60.00"/></proof>
</goal>
<goal name="WP_parameter isqrt64" expl="VC for isqrt64">
<transf name="split_goal_wp" >
......@@ -367,6 +343,7 @@
<proof prover="3"><result status="valid" time="0.72"/></proof>
</goal>
<goal name="WP_parameter isqrt64.24" expl="loop invariant preservation">
<proof prover="0"><result status="unknown" time="59.92"/></proof>
</goal>
<goal name="WP_parameter isqrt64.25" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="1.21"/></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