Commit ff2bbfca authored by MARCHE Claude's avatar MARCHE Claude

Square root using Von Neumann's algorithm, first proof

See also Warren's "Hacker's Delight" Figure 11.4
parent 5e00fc66
module VonNeumann
(*
algorithm from Warren's "Hacker's Delight" Figure 11.4
int isqrt4(unsigned x) {
unsigned m, y, b;
m = 0x40000000;
y = 0;
while(m != 0) { // Do 16 times.
b = y | m;
y = y >> 1;
if (x >= b) {
x = x - b;
y = y | m;
}
m = m >> 2;
}
return y;
}
*)
use import ref.Ref
use import bv.BV32
function sqr (x:t) : t = mul x x
function succ (x:t) : t = add x (1:t)
function pred (x:t) : t = sub x (1:t)
function pow2 (n:t) : t = lsl_bv (1:t) n
predicate is_pow2 (x:t) (n:t) = bw_and x (pred (pow2 n)) = (0:t)
lemma sqr_add: forall x y.
sqr (add x y) = add (sqr x) (add (sqr y) (mul (2:t) (mul x y)))
let isqrt4 (x:t) : t
ensures { ule (sqr result) x }
(* ensures { ult x (sqr (succ result)) } *)
= let num = ref x in
let bits = ref (0x4000_0000:t) in
let res = ref (0:t) in
let ghost m = ref (16:t) in
let ghost bits_g = ref (0x8000:t) in (* 2^{m-1} *)
let ghost res_g = ref (0:t) in (* res / 2^m *)
while !bits <> (0:t) do
variant { t'int !bits }
(* 0 <= m <= 16 *)
invariant { ule !m (16:t) }
(* bits_g = 2^{m-1} ou 0 si m=0 *)
invariant { !bits_g = if !m=(0:t) then (0:t) else pow2 (pred !m) }
(* bits = bits_g^2 *)
invariant { !bits = sqr !bits_g }
(* res_g multiple de 2^m *)
invariant { is_pow2 !res_g !m }
(* res_g smaller than 2^16 *)
invariant { ult !res_g (0x1_0000:t) }
(* res = res_g * 2^m *)
invariant { !res = mul !res_g (pow2 !m) }
(* num <= x *)
invariant { ule !num x }
(* (x - num) est le carré de (res / 2^m) *)
invariant { sub x !num = sqr !res_g }
(* m is not null, let's subtract 1 *)
assert { !m <> (0:t) };
'L1:
ghost m := pred !m;
assert { (at !m 'L1) = succ !m };
assert { !res = mul !res_g (pow2 (succ !m)) };
assert { !bits_g = pow2 !m };
let b = bw_or !res !bits in
assert { b = add !res !bits };
assert { b = mul (add (mul (2:t) !res_g) !bits_g) (pow2 !m) };
res := lsr_bv !res (1:t);
assert { !res = mul !res_g (pow2 !m) };
if uge !num b then
begin
num := sub !num b;
'L:
res := bw_or !res !bits;
assert { !res = add (at !res 'L) !bits };
assert { !res = mul (add !res_g !bits_g) (pow2 !m) };
res_g := add !res_g !bits_g
end;
bits := lsr_bv !bits (2:t);
ghost bits_g := lsr_bv !bits_g (1:t)
done;
assert { !m = (0:t) };
assert { !bits = (0:t) };
!res
end
(*
(*
let ghost i = ref (0:t) in
let ghost bits = ref (30:t) in
*)
invariant { !bits = sub (30:t) (add !i !i) }
invariant { !i = (16:t) /\ !m = (0:t)
\/
ult !i (16:t) /\ !m = lsl_bv (1:t) !bits }
invariant { let ly = lsr_bv !y !bits in
ule (mul ly ly) x0 }
*)
<?xml version="1.0" encoding="UTF-8"?>
<!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="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../isqrt_von_neumann.mlw" proved="true">
<theory name="VonNeumann" proved="true" sum="f33b7734ac92ae691813086354d1b47c">
<goal name="sqr_add" proved="true">
<proof prover="2"><result status="valid" time="4.70"/></proof>
</goal>
<goal name="WP_parameter isqrt4" expl="VC for isqrt4" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter isqrt4.0" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt4.1" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.2" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt4.3" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt4.4" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.5" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.6" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.7" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt4.8" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.9" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter isqrt4.10" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.11" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.12" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter isqrt4.13" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter isqrt4.14" expl="assertion" proved="true">
<transf name="subst" proved="true" arg1="res">
<goal name="WP_parameter isqrt4.14.0" expl="assertion" proved="true">
<transf name="subst" proved="true" arg1="res1">
<goal name="WP_parameter isqrt4.14.0.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter isqrt4.15" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="WP_parameter isqrt4.16" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="WP_parameter isqrt4.17" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter isqrt4.18" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter isqrt4.19" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="WP_parameter isqrt4.20" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter isqrt4.21" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="WP_parameter isqrt4.22" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(m = (0:t))">
<goal name="WP_parameter isqrt4.22.0" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.22.1" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter isqrt4.23" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter isqrt4.24" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="6.96"/></proof>
</goal>
<goal name="WP_parameter isqrt4.25" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="WP_parameter isqrt4.26" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter isqrt4.27" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter isqrt4.28" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="WP_parameter isqrt4.29" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter isqrt4.30" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.31" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.32" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.33" expl="loop invariant preservation" proved="true">
<transf name="subst" proved="true" arg1="num">
<goal name="WP_parameter isqrt4.33.0" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter isqrt4.34" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter isqrt4.35" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.36" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt4.37" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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