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

Use some better-looking assertions.

parent 115ac8a6
......@@ -46,19 +46,18 @@ let sqrt1 (rp: ptr uint64) (a0: uint64): uint64
let a2 = fxp_lsr a 24 in
let ea2 = pure { (a2 -. a) /. a } in
let u1 = fxp_mul x1 a2 in
assert { rsa *. a = sqrt a };
let eu1 = pure { (u1 -. sqrt a) /. sqrt a } in
assert { eu1 = (1. +. e1) *. (1. +. ea2) -. 1. };
let u2 = fxp_lsr u1 25 in
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
assert { sqrt a *. sqrt a = a };
let t2 = fxp_asr t2' 24 in
let x2 = fxp_add u1 (fxp_asr' (fxp_mul x1 t2) 15 1) 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 -. sqrt a) /. sqrt a = -0.5 *. (ee +. m2 /. a) *. (1. +. e1) -. e1 *. e1a2
assert { let ee = (1. +. eu1) *. (1. +. eu1) *. eu2 *. (2. +. eu2) +. eu1 *. eu1 in
(mx2 -. sqrt a) /. sqrt a = -0.5 *. (ee +. m2 /. a) *. (1. +. e1) -. e1 *. eu1
by x1 <> 0. /\ a2 <> 0. };
let x = fxp_lsr x2 32 in
let sa = pure { trunc_at (sqrt a) (-32) } in
......
......@@ -593,15 +593,67 @@ Axiom H42 : ((rval u1) = ((rval x1) * (rval a2))%R).
Axiom H43 : ((iexp u1) = ((iexp x1) + (iexp a2))%Z).
Axiom H44 :
((((rval u1) - (Reals.R_sqrt.sqrt (rval a)))%R /
(Reals.R_sqrt.sqrt (rval a)))%R
=
(((1%R +
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
* (1%R + (((rval a2) - (rval a))%R / (rval a))%R)%R)%R
- 1%R)%R).
Parameter u2: fxp.
Axiom H45 : ((rval u2) = (trunc_at (rval u1) ((iexp u1) + 25%Z)%Z)).
Axiom H46 : ((iexp u2) = ((iexp u1) + 25%Z)%Z).
Parameter m2: fxp.
Parameter rliteral2: uint64.
Axiom rliteral_axiom2 : ((uint64'int rliteral2) = 2473901162496%Z).
Axiom H47 : ((ival m2) = rliteral2).
Axiom H48 :
((rval m2) = ((BuiltIn.IZR 2473901162496%Z) * (pow2 (-78%Z)%Z))%R).
Axiom H49 : ((iexp m2) = (-78%Z)%Z).
Parameter o7: fxp.
Axiom H50 : ((rval o7) = ((rval u2) * (rval u2))%R).
Axiom H51 : ((iexp o7) = ((iexp u2) + (iexp u2))%Z).
Parameter o8: fxp.
Axiom H52 : ((rval o8) = (rval a)).
Axiom H53 : ((iexp o8) = ((iexp a) - 14%Z)%Z).
Parameter o9: fxp.
Axiom H54 : ((rval o9) = ((rval o8) - (rval o7))%R).
Axiom H55 : ((iexp o9) = (iexp o8)).
Parameter t2': fxp.
Axiom H56 : ((rval t2') = ((rval o9) - (rval m2))%R).
Axiom H57 : ((iexp t2') = (iexp o9)).
(* Why3 goal *)
Theorem VC_sqrt1 :
(((1%R / (Reals.R_sqrt.sqrt (rval a)))%R * (rval a))%R =
(Reals.R_sqrt.sqrt (rval a))).
(((Reals.R_sqrt.sqrt (rval a)) * (Reals.R_sqrt.sqrt (rval a)))%R =
(rval a)).
Proof.
set (sa := sqrt (rval a)).
replace (rval a) with (sa^2)%R.
field.
apply Rgt_not_eq, sqrt_lt_R0, H6.
rewrite <- Rsqr_pow2.
apply Rsqr_sqrt, Rlt_le, H6.
Qed.
......
......@@ -593,27 +593,18 @@ Axiom H42 : ((rval u1) = ((rval x1) * (rval a2))%R).
Axiom H43 : ((iexp u1) = ((iexp x1) + (iexp a2))%Z).
Axiom H44 :
(((1%R / (Reals.R_sqrt.sqrt (rval a)))%R * (rval a))%R =
(Reals.R_sqrt.sqrt (rval a))).
Parameter u2: fxp.
Axiom H45 : ((rval u2) = (trunc_at (rval u1) ((iexp u1) + 25%Z)%Z)).
Axiom H46 : ((iexp u2) = ((iexp u1) + 25%Z)%Z).
(* Why3 goal *)
Theorem VC_sqrt1 :
(((rval a) - (((rval x1) * (rval a))%R * ((rval x1) * (rval a))%R)%R)%R =
(((-(rval a))%R *
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
*
(2%R +
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R)%R).
((((rval u1) - (Reals.R_sqrt.sqrt (rval a)))%R /
(Reals.R_sqrt.sqrt (rval a)))%R
=
(((1%R +
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
* (1%R + (((rval a2) - (rval a))%R / (rval a))%R)%R)%R
- 1%R)%R).
Proof.
rewrite H42.
set (sa := sqrt (rval a)).
replace (rval a) with (sa^2)%R.
field.
......
......@@ -594,8 +594,14 @@ Axiom H42 : ((rval u1) = ((rval x1) * (rval a2))%R).
Axiom H43 : ((iexp u1) = ((iexp x1) + (iexp a2))%Z).
Axiom H44 :
(((1%R / (Reals.R_sqrt.sqrt (rval a)))%R * (rval a))%R =
(Reals.R_sqrt.sqrt (rval a))).
((((rval u1) - (Reals.R_sqrt.sqrt (rval a)))%R /
(Reals.R_sqrt.sqrt (rval a)))%R
=
(((1%R +
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
* (1%R + (((rval a2) - (rval a))%R / (rval a))%R)%R)%R
- 1%R)%R).
Parameter u2: fxp.
......@@ -603,52 +609,46 @@ Axiom H45 : ((rval u2) = (trunc_at (rval u1) ((iexp u1) + 25%Z)%Z)).
Axiom H46 : ((iexp u2) = ((iexp u1) + 25%Z)%Z).
Axiom H47 :
(((rval a) - (((rval x1) * (rval a))%R * ((rval x1) * (rval a))%R)%R)%R =
(((-(rval a))%R *
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
*
(2%R +
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R)%R).
Parameter m2: fxp.
Parameter rliteral2: uint64.
Axiom rliteral_axiom2 : ((uint64'int rliteral2) = 2473901162496%Z).
Axiom H48 : ((ival m2) = rliteral2).
Axiom H47 : ((ival m2) = rliteral2).
Axiom H49 :
Axiom H48 :
((rval m2) = ((BuiltIn.IZR 2473901162496%Z) * (pow2 (-78%Z)%Z))%R).
Axiom H50 : ((iexp m2) = (-78%Z)%Z).
Axiom H49 : ((iexp m2) = (-78%Z)%Z).
Parameter o7: fxp.
Axiom H51 : ((rval o7) = ((rval u2) * (rval u2))%R).
Axiom H50 : ((rval o7) = ((rval u2) * (rval u2))%R).
Axiom H52 : ((iexp o7) = ((iexp u2) + (iexp u2))%Z).
Axiom H51 : ((iexp o7) = ((iexp u2) + (iexp u2))%Z).
Parameter o8: fxp.
Axiom H53 : ((rval o8) = (rval a)).
Axiom H52 : ((rval o8) = (rval a)).
Axiom H54 : ((iexp o8) = ((iexp a) - 14%Z)%Z).
Axiom H53 : ((iexp o8) = ((iexp a) - 14%Z)%Z).
Parameter o9: fxp.
Axiom H55 : ((rval o9) = ((rval o8) - (rval o7))%R).
Axiom H54 : ((rval o9) = ((rval o8) - (rval o7))%R).
Axiom H56 : ((iexp o9) = (iexp o8)).
Axiom H55 : ((iexp o9) = (iexp o8)).
Parameter t2': fxp.
Axiom H57 : ((rval t2') = ((rval o9) - (rval m2))%R).
Axiom H56 : ((rval t2') = ((rval o9) - (rval m2))%R).
Axiom H57 : ((iexp t2') = (iexp o9)).
Axiom H58 : ((iexp t2') = (iexp o9)).
Axiom H58 :
(((Reals.R_sqrt.sqrt (rval a)) * (Reals.R_sqrt.sqrt (rval a)))%R =
(rval a)).
Parameter t2: fxp.
......@@ -685,29 +685,21 @@ Theorem VC_sqrt1 :
/ (Reals.R_sqrt.sqrt (rval a)))%R
=
((((-(05 / 10)%R)%R *
(((((((1%R +
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
* (1%R + (((rval a2) - (rval a))%R / (rval a))%R)%R)%R
((((((1%R +
(((rval u1) - (Reals.R_sqrt.sqrt (rval a)))%R /
(Reals.R_sqrt.sqrt (rval a)))%R)%R
*
((1%R +
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
* (1%R + (((rval a2) - (rval a))%R / (rval a))%R)%R)%R)%R
(1%R +
(((rval u1) - (Reals.R_sqrt.sqrt (rval a)))%R /
(Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
* (((rval u2) - (rval u1))%R / (rval u1))%R)%R
* ((((rval u2) - (rval u1))%R / (rval u1))%R + 2%R)%R)%R
* (2%R + (((rval u2) - (rval u1))%R / (rval u1))%R)%R)%R
+
((((1%R +
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
* (1%R + (((rval a2) - (rval a))%R / (rval a))%R)%R)%R
- 1%R)%R
((((rval u1) - (Reals.R_sqrt.sqrt (rval a)))%R /
(Reals.R_sqrt.sqrt (rval a)))%R
*
(((1%R +
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
* (1%R + (((rval a2) - (rval a))%R / (rval a))%R)%R)%R
- 1%R)%R)%R)%R
(((rval u1) - (Reals.R_sqrt.sqrt (rval a)))%R /
(Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
+ ((rval m2) / (rval a))%R)%R)%R
*
(1%R +
......@@ -717,14 +709,11 @@ Theorem VC_sqrt1 :
((((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R
*
(((1%R +
(((rval x1) - (1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R /
(1%R / (Reals.R_sqrt.sqrt (rval a)))%R)%R)%R
* (1%R + (((rval a2) - (rval a))%R / (rval a))%R)%R)%R
- 1%R)%R)%R)%R).
(((rval u1) - (Reals.R_sqrt.sqrt (rval a)))%R /
(Reals.R_sqrt.sqrt (rval a)))%R)%R)%R).
Proof.
intros (h1,h2).
rewrite H57, H55, H53, H51, H42.
rewrite H56, H54, H52, H50, H42.
set (sa := sqrt (rval a)).
replace (rval a) with (sa^2)%R.
field.
......
......@@ -46,25 +46,25 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<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>
<proof prover="1" edited="sqrt_Sqrt1_VC_sqrt1_3.v"><result status="valid" time="0.46"/></proof>
</goal>
<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.14" expl="assertion" proved="true">
<proof prover="1" edited="sqrt_Sqrt1_VC_sqrt1_3.v"><result status="valid" time="0.47"/></proof>
<goal name="VC sqrt1.14" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<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.16" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<goal name="VC sqrt1.16" expl="assertion" proved="true">
<proof prover="1" edited="sqrt_Sqrt1_VC_sqrt1_1.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="VC sqrt1.17" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC sqrt1.18" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC sqrt1.19" expl="fxp alignment" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
......@@ -78,12 +78,12 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<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>
<proof prover="1" edited="sqrt_Sqrt1_VC_sqrt1_4.v"><result status="valid" time="0.47"/></proof>
</goal>
</transf>
</goal>
<goal name="VC sqrt1.21" expl="fxp overflow" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC sqrt1.22" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></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