Commit 717697a1 authored by Guillaume Melquiond's avatar Guillaume Melquiond Committed by Raphael Rieu-Helft

Prove the main error bound.

parent 1a0e9e92
......@@ -35,28 +35,30 @@ let sqrt1 (rp: ptr uint64) (a0: uint64): uint64
let ghost e0 = (rval x0 -. rsa) /. rsa in
let a1 = fxp_lsr a 31 in
let ghost ea1 = (rval a1 -. rval a) /. rval a in
let t1' =
fxp_sub
(fxp_sub (fxp_init 0x2000000000000 (-49)) (fxp_init 0x30000 (-49)))
(fxp_mul (fxp_mul x0 x0) a1) in
let ghost m1 = 0x3.p-33 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) *. (m1 +. (1. +. e0) *. (1. +. e0) *. ea1)) };
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 a2 = fxp_lsr a 24 in
let ghost ea2 = (rval a2 -. rval a) /. rval a in
let u1 = fxp_mul x1 a2 in
assert { rsa *. rval a = sa };
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 t2 = fxp_asr (fxp_sub (fxp_sub (fxp_lsl a 14) (fxp_mul u2 u2)) (fxp_init 0x10000000000 (-78))) 24 in
let ghost m2 = 0x1.p-38 in
let ghost mt2 = rval a -. (rval x1 *. rval a2) *. (rval x1 *. rval a2) -. m2 in
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 x1 *. rval a2 +. rval x1 *. mt2 *. 0.5 in
assert { (mx2 -. sa) /. sa = ea2 *. (1. +. e1) *. (-. e1 *. (2. +. e1) -. (1. +. e1) *. (1. +. e1) *. 0.5 *. ea2) -. 0.5 *. m2 /. rval a *. (1. +. e1) -. e1 *. e1 *. 0.5 *. (3. +. e1) };
let ghost mx2 = rval u1 +. rval x1 *. rval 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. };
let x = fxp_lsr x2 32 in
let ghost sa = trunc_at sa (-32) in
assert { -0x1.p-32 <=. rval x -. sa <=. 0. };
......
......@@ -7,7 +7,7 @@
<file>
<path name=".."/>
<path name="sqrt.mlw"/>
<theory name="Top">
<theory name="Sqrt1">
<goal name="VC sqrt1" expl="VC for sqrt1">
<transf name="split_vc" >
<goal name="VC sqrt1.0" expl="assertion">
......@@ -19,103 +19,138 @@
<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.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sqrt1.4" expl="fxp overflow" proved="true">
<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">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.6" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<goal name="VC sqrt1.6" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sqrt1.7" expl="fxp alignment" proved="true">
<goal name="VC sqrt1.7" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.8" expl="fxp overflow" proved="true">
<goal name="VC sqrt1.8" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.9" expl="fxp overflow" 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.10" expl="fxp alignment" proved="true">
<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="assertion" proved="true">
<proof prover="1" edited="sqrt_Top_VC_sqrt1_2.v"><result status="valid" time="0.50"/></proof>
<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.12" expl="precondition" proved="true">
<goal name="VC sqrt1.12" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.13" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<goal name="VC sqrt1.13" 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="assertion" proved="true">
<proof prover="1" edited="sqrt_Top_VC_sqrt1_5.v"><result status="valid" time="0.46"/></proof>
<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="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="VC sqrt1.16" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sqrt1.17" expl="assertion" proved="true">
<proof prover="1" edited="sqrt_Top_VC_sqrt1_7.v"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="VC sqrt1.18" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="1" edited="sqrt_Sqrt1_VC_sqrt1_1.v"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="VC sqrt1.19" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<goal name="VC sqrt1.18" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sqrt1.20" expl="fxp overflow" proved="true">
<goal name="VC sqrt1.19" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC sqrt1.21" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<goal name="VC sqrt1.20" 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.22" expl="fxp alignment" proved="true">
<goal name="VC sqrt1.21" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.23" expl="assertion" proved="true">
<proof prover="1" edited="sqrt_Top_VC_sqrt1_6.v"><result status="valid" time="0.47"/></proof>
</goal>
<goal name="VC sqrt1.24" expl="fxp overflow">
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<goal name="VC sqrt1.22" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.25" expl="assertion">
<proof prover="2" obsolete="true"><result status="unknown" time="2.31"/></proof>
<goal name="VC sqrt1.23" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC sqrt1.26" expl="assertion">
<goal name="VC sqrt1.24" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC sqrt1.27" expl="integer overflow">
<goal name="VC sqrt1.25" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.28" expl="assertion">
<goal name="VC sqrt1.26" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC sqrt1.26.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">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sqrt1.26.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">
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC sqrt1.28" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC sqrt1.29" expl="assertion">
</goal>
<goal name="VC sqrt1.30" expl="integer overflow">
</goal>
<goal name="VC sqrt1.31" expl="integer overflow">
<goal name="VC sqrt1.31" expl="assertion">
</goal>
<goal name="VC sqrt1.32" expl="integer overflow">
<goal name="VC sqrt1.32" expl="assertion">
</goal>
<goal name="VC sqrt1.33" expl="assertion">
<goal name="VC sqrt1.33" expl="integer overflow">
</goal>
<goal name="VC sqrt1.34" expl="integer overflow">
</goal>
<goal name="VC sqrt1.35" expl="integer overflow">
</goal>
<goal name="VC sqrt1.36" expl="integer overflow">
<goal name="VC sqrt1.36" expl="assertion">
</goal>
<goal name="VC sqrt1.37" expl="integer overflow">
</goal>
<goal name="VC sqrt1.38" expl="assertion">
<goal name="VC sqrt1.38" expl="integer overflow">
</goal>
<goal name="VC sqrt1.39" expl="integer overflow">
</goal>
<goal name="VC sqrt1.40" expl="integer overflow">
</goal>
<goal name="VC sqrt1.41" expl="assertion">
</goal>
<goal name="VC sqrt1.42" expl="integer overflow">
</goal>
<goal name="VC sqrt1.43" expl="precondition">
</goal>
<goal name="VC sqrt1.44" expl="postcondition">
</goal>
<goal name="VC sqrt1.45" expl="postcondition">
</goal>
<goal name="VC sqrt1.46" expl="postcondition">
</goal>
<goal name="VC sqrt1.47" expl="integer overflow">
</goal>
<goal name="VC sqrt1.48" expl="precondition">
</goal>
<goal name="VC sqrt1.49" expl="postcondition">
</goal>
<goal name="VC sqrt1.39" expl="postcondition">
<goal name="VC sqrt1.50" expl="postcondition">
</goal>
<goal name="VC sqrt1.40" expl="postcondition">
<goal name="VC sqrt1.51" 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