Commit 115ac8a6 authored by Guillaume Melquiond's avatar Guillaume Melquiond Committed by Raphael Rieu-Helft

Change ghost into pure to make it possible to use a coercion.

parent 717697a1
......@@ -10,14 +10,16 @@ use mach.c.C
use lemmas.Lemmas
use mach.fxp.Fxp
meta coercion function rval
val rsa_estimate (a: fxp): fxp
requires { 0.25 <=. rval a <=. 0xffffffffffffffffp-64 }
requires { 0.25 <=. a <=. 0xffffffffffffffffp-64 }
requires { iexp a = - 64 }
ensures { iexp result = -8 }
ensures { 256 <= ival result <= 511 }
ensures { 1. <=. rval result <=. 2. }
ensures { let rsa = 1. /. sqrt(rval a) in
let e0 = (rval result -. rsa) /. rsa in -0.00281 <=. e0 <=. 0.002655 }
ensures { 1. <=. result <=. 2. }
ensures { let rsa = 1. /. sqrt a in
let e0 = (result -. rsa) /. rsa in -0.00281 <=. e0 <=. 0.002655 }
let sqrt1 (rp: ptr uint64) (a0: uint64): uint64
requires { valid rp 1 }
......@@ -27,46 +29,45 @@ let sqrt1 (rp: ptr uint64) (a0: uint64): uint64
ensures { (pelts rp)[offset rp] <= 2 * result }
=
let a = fxp_init a0 (-64) in
assert { 0.25 <=. rval a <=. 0xffffffffffffffffp-64 };
assert { 0. <. rval a };
let ghost sa = sqrt (rval a) in
let ghost rsa = 1. /. sa in
assert { 0.25 <=. a <=. 0xffffffffffffffffp-64 };
assert { 0. <. a };
let rsa = pure { 1. /. sqrt a } in
let x0 = rsa_estimate a in
let ghost e0 = (rval x0 -. rsa) /. rsa in
let e0 = pure { (x0 -. rsa) /. rsa } in
let a1 = fxp_lsr a 31 in
let ghost ea1 = (rval a1 -. rval a) /. rval a in
let ea1 = pure { (a1 -. a) /. a } in
let m1 = fxp_sub (fxp_init 0x2000000000000 (-49)) (fxp_init 0x30000 (-49)) in
let t1' = fxp_sub m1 (fxp_mul (fxp_mul x0 x0) a1) in
let t1 = fxp_asr t1' 16 in
let x1 = fxp_add (fxp_lsl x0 16) (fxp_asr' (fxp_mul x0 t1) 18 1) in
let ghost mx1 = rval x0 +. rval x0 *. rval t1' *. 0.5 in
assert { (mx1 -. rsa) /. rsa = -0.5 *. (e0 *. e0 *. (3. +. e0) +. (1. +. e0) *. (1. -. rval m1 +. (1. +. e0) *. (1. +. e0) *. ea1)) };
let ghost e1 = (rval x1 -. rsa) /. rsa in
let mx1 = pure { x0 +. x0 *. t1' *. 0.5 } in
assert { (mx1 -. rsa) /. rsa = -0.5 *. (e0 *. e0 *. (3. +. e0) +. (1. +. e0) *. (1. -. m1 +. (1. +. e0) *. (1. +. e0) *. ea1)) };
let e1 = pure { (x1 -. rsa) /. rsa } in
let a2 = fxp_lsr a 24 in
let ghost ea2 = (rval a2 -. rval a) /. rval a in
let ea2 = pure { (a2 -. a) /. a } in
let u1 = fxp_mul x1 a2 in
assert { rsa *. rval a = sa };
assert { rsa *. a = sqrt a };
let u2 = fxp_lsr u1 25 in
let ghost eu2 = (rval u2 -. rval u1) /. rval u1 in
assert { rval a -. ((rval x1 *. rval a) *. (rval x1 *. rval a)) = -. rval a *. e1 *. (2. +. e1) };
let eu2 = pure { (u2 -. u1) /. u1 } in
assert { a -. (x1 *. a) *. (x1 *. a) = -. a *. e1 *. (2. +. e1) };
let m2 = fxp_init 0x24000000000 (-78) in
let t2' = fxp_sub (fxp_sub (fxp_lsl a 14) (fxp_mul u2 u2)) m2 in
let t2 = fxp_asr t2' 24 in
let x2 = fxp_add u1 (fxp_asr' (fxp_mul x1 t2) 15 1) in
let ghost mx2 = rval u1 +. rval x1 *. rval t2' *. 0.5 in
let mx2 = pure { u1 +. x1 *. t2' *. 0.5 } in
assert { let p1a2 = (1. +. e1) *. (1. +. ea2) in
let e1a2 = p1a2 -. 1. in
let ee = p1a2 *. p1a2 *. eu2 *. (eu2 +. 2.) +. e1a2 *. e1a2 in
(mx2 -. sa) /. sa = -0.5 *. (ee +. rval m2 /. rval a) *. (1. +. e1) -. e1 *. e1a2
by rval x1 <> 0. /\ rval a2 <> 0. };
(mx2 -. sqrt a) /. sqrt a = -0.5 *. (ee +. m2 /. a) *. (1. +. e1) -. e1 *. e1a2
by x1 <> 0. /\ a2 <> 0. };
let x = fxp_lsr x2 32 in
let ghost sa = trunc_at sa (-32) in
assert { -0x1.p-32 <=. rval x -. sa <=. 0. };
let sa = pure { trunc_at (sqrt a) (-32) } in
assert { -0x1.p-32 <=. x -. sa <=. 0. };
let ref c = ival x in
assert { c * c <= a0 < (c+2) * (c+2) };
let ref s = c * c in
assert { (c+1) * (c+1) <= radix
by rval x <=. sa <=. 1.
by x <=. sa <=. 1.
so iexp x = -32
so c < power 2 32
so c+1 <= power 2 32
......
......@@ -16,141 +16,123 @@
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.2" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.3" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sqrt1.4" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.5" expl="precondition" proved="true">
<goal name="VC sqrt1.3" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.6" expl="fxp overflow" proved="true">
<goal name="VC sqrt1.4" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sqrt1.7" expl="precondition" proved="true">
<goal name="VC sqrt1.5" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.8" expl="fxp alignment" proved="true">
<goal name="VC sqrt1.6" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.9" expl="fxp alignment" proved="true">
<goal name="VC sqrt1.7" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.10" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.11" expl="fxp overflow" proved="true">
<goal name="VC sqrt1.8" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sqrt1.12" expl="fxp alignment" proved="true">
<goal name="VC sqrt1.9" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.13" expl="assertion" proved="true">
<goal name="VC sqrt1.10" expl="assertion" proved="true">
<proof prover="1" edited="sqrt_Sqrt1_VC_sqrt1_2.v"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="VC sqrt1.14" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sqrt1.15" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sqrt1.16" expl="precondition" proved="true">
<goal name="VC sqrt1.11" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sqrt1.17" expl="assertion" proved="true">
<goal name="VC sqrt1.12" expl="assertion" proved="true">
<proof prover="1" edited="sqrt_Sqrt1_VC_sqrt1_1.v"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="VC sqrt1.18" expl="fxp overflow" proved="true">
<goal name="VC sqrt1.13" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sqrt1.19" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC sqrt1.20" expl="assertion" proved="true">
<goal name="VC sqrt1.14" expl="assertion" proved="true">
<proof prover="1" edited="sqrt_Sqrt1_VC_sqrt1_3.v"><result status="valid" time="0.47"/></proof>
</goal>
<goal name="VC sqrt1.21" expl="fxp alignment" proved="true">
<goal name="VC sqrt1.15" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.22" expl="fxp alignment" proved="true">
<goal name="VC sqrt1.16" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.23" expl="fxp overflow" proved="true">
<goal name="VC sqrt1.17" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC sqrt1.24" expl="fxp overflow" proved="true">
<goal name="VC sqrt1.18" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC sqrt1.25" expl="fxp alignment" proved="true">
<goal name="VC sqrt1.19" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.26" expl="assertion" proved="true">
<goal name="VC sqrt1.20" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC sqrt1.26.0" expl="VC for sqrt1" proved="true">
<goal name="VC sqrt1.20.0" expl="VC for sqrt1" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC sqrt1.26.1" expl="VC for sqrt1" proved="true">
<goal name="VC sqrt1.20.1" expl="VC for sqrt1" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sqrt1.26.2" expl="VC for sqrt1" proved="true">
<goal name="VC sqrt1.20.2" expl="VC for sqrt1" proved="true">
<proof prover="1" edited="sqrt_Sqrt1_VC_sqrt1_4.v"><result status="valid" time="0.52"/></proof>
</goal>
</transf>
</goal>
<goal name="VC sqrt1.27" expl="fxp overflow" proved="true">
<goal name="VC sqrt1.21" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC sqrt1.28" expl="assertion" proved="true">
<goal name="VC sqrt1.22" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC sqrt1.29" expl="assertion">
<goal name="VC sqrt1.23" expl="assertion">
</goal>
<goal name="VC sqrt1.30" expl="integer overflow">
<goal name="VC sqrt1.24" expl="integer overflow">
</goal>
<goal name="VC sqrt1.31" expl="assertion">
<goal name="VC sqrt1.25" expl="assertion">
</goal>
<goal name="VC sqrt1.32" expl="assertion">
<goal name="VC sqrt1.26" expl="assertion">
</goal>
<goal name="VC sqrt1.33" expl="integer overflow">
<goal name="VC sqrt1.27" expl="integer overflow">
</goal>
<goal name="VC sqrt1.34" expl="integer overflow">
<goal name="VC sqrt1.28" expl="integer overflow">
</goal>
<goal name="VC sqrt1.35" expl="integer overflow">
<goal name="VC sqrt1.29" expl="integer overflow">
</goal>
<goal name="VC sqrt1.36" expl="assertion">
<goal name="VC sqrt1.30" expl="assertion">
</goal>
<goal name="VC sqrt1.37" expl="integer overflow">
<goal name="VC sqrt1.31" expl="integer overflow">
</goal>
<goal name="VC sqrt1.38" expl="integer overflow">
<goal name="VC sqrt1.32" expl="integer overflow">
</goal>
<goal name="VC sqrt1.39" expl="integer overflow">
<goal name="VC sqrt1.33" expl="integer overflow">
</goal>
<goal name="VC sqrt1.40" expl="integer overflow">
<goal name="VC sqrt1.34" expl="integer overflow">
</goal>
<goal name="VC sqrt1.41" expl="assertion">
<goal name="VC sqrt1.35" expl="assertion">
</goal>
<goal name="VC sqrt1.42" expl="integer overflow">
<goal name="VC sqrt1.36" expl="integer overflow">
</goal>
<goal name="VC sqrt1.43" expl="precondition">
<goal name="VC sqrt1.37" expl="precondition">
</goal>
<goal name="VC sqrt1.44" expl="postcondition">
<goal name="VC sqrt1.38" expl="postcondition">
</goal>
<goal name="VC sqrt1.45" expl="postcondition">
<goal name="VC sqrt1.39" expl="postcondition">
</goal>
<goal name="VC sqrt1.46" expl="postcondition">
<goal name="VC sqrt1.40" expl="postcondition">
</goal>
<goal name="VC sqrt1.47" expl="integer overflow">
<goal name="VC sqrt1.41" expl="integer overflow">
</goal>
<goal name="VC sqrt1.48" expl="precondition">
<goal name="VC sqrt1.42" expl="precondition">
</goal>
<goal name="VC sqrt1.49" expl="postcondition">
<goal name="VC sqrt1.43" expl="postcondition">
</goal>
<goal name="VC sqrt1.50" expl="postcondition">
<goal name="VC sqrt1.44" expl="postcondition">
</goal>
<goal name="VC sqrt1.51" expl="postcondition">
<goal name="VC sqrt1.45" expl="postcondition">
</goal>
</transf>
</goal>
......
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