Commit 0fde67d6 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Finish square root proof

parent b9405b26
This diff is collapsed.
......@@ -76,7 +76,7 @@
</transf>
</goal>
<goal name="VC wmpn_cmp.16" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="0"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_cmp.17" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -103,7 +103,7 @@
</transf>
</goal>
<goal name="VC wmpn_cmp.21" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.16"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_cmp.22" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......
This diff is collapsed.
This diff is collapsed.
......@@ -78,6 +78,14 @@ module Lemmas
meta remove_prop axiom prod_compat_lr
let lemma simp_compat_strict_l (a b c:int)
requires { 0 <= a * b < a * c }
requires { 0 < a }
ensures { b < c }
= ()
meta remove_prop axiom simp_compat_strict_l
(** {3 Integer value of a natural number} *)
(** `value_sub x n m` denotes the integer represented by
......
......@@ -6,11 +6,12 @@
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file>
<file proved="true">
<path name=".."/>
<path name="lemmas.mlw"/>
<theory name="Lemmas">
<theory name="Lemmas" proved="true">
<goal name="VC map_eq_shift" expl="VC for map_eq_shift" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC map_eq_shift.0" expl="postcondition" proved="true">
......@@ -61,7 +62,11 @@
<goal name="VC prod_compat_strict_lr" expl="VC for prod_compat_strict_lr" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC prod_compat_lr" expl="VC for prod_compat_lr">
<goal name="VC prod_compat_lr" expl="VC for prod_compat_lr" proved="true">
<proof prover="4"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC simp_compat_strict_l" expl="VC for simp_compat_strict_l" proved="true">
<proof prover="4"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC value_sub" expl="VC for value_sub" proved="true">
<transf name="split_goal_right" proved="true" >
......
......@@ -28,6 +28,35 @@ module Logical
ensures { mod (x * y + z) x = mod z x }
=
()
let lsl_mod_ext (x cnt: limb) : limb
requires { 0 <= cnt < Limb.length }
ensures { result = mod (x * power 2 cnt) radix }
ensures { result <= radix - power 2 cnt }
=
let r = lsl_mod x cnt in
let ghost p = power 2 (Limb.to_int cnt) in
let ghost q = power 2 (Limb.length - Limb.to_int cnt) in
assert { p * q = radix };
let ghost d = div (Limb.to_int x * p) radix in
assert { d * q >= 0 by d >= 0 so q >= 0 };
assert { mod r p = 0
by x * p = d * radix + r
so mod (x * p) p = mod (p * x + 0) p = mod 0 p = 0
so mod (d * radix + r) p = 0
so d * radix + r = p * (d * q) + r
so mod (d * radix + r) p = mod (p * (d * q) + r) p = mod r p };
assert { r <= radix - p
by mod r p = 0
so r < radix
so radix = p * power 2 (Limb.length - cnt)
so mod radix p = mod (p * q + 0) p = mod 0 p = 0
so let d1 = div r p in
let d2 = div radix p in
(r <= radix - p by
r = p * d1 so radix = p * d2 so p * d1 < p * d2 so p > 0
so d1 < d2 so d1 <= d2 - 1
so p * d1 <= p * (d2 - 1) = radix - p) };
r
let lsld_ext (x cnt:limb) : (limb,limb)
requires { 0 <= cnt < Limb.length }
......
This diff is collapsed.
......@@ -129,4 +129,5 @@ let sqrt1 (rp: ptr uint64) (a0: uint64): uint64
C.set rp (a0 - s);
c
meta remove_prop axiom trunc_lower_bound
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<why3session shape_version="6">
<prover id="0" name="Gappa" version="1.3.3" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="5" name="Coq" version="8.8.2" timelimit="0" steplimit="0" memlimit="0"/>
......@@ -14,7 +14,7 @@
<theory name="Sqrt1" proved="true">
<goal name="VC real_sqr_compat" expl="VC for real_sqr_compat" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="97"/></proof>
<proof prover="8" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC trunc_lower_bound" expl="VC for trunc_lower_bound" proved="true">
<transf name="split_vc" proved="true" >
......@@ -27,7 +27,7 @@
<proof prover="8"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC trunc_lower_bound.0.2" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.14" steps="120"/></proof>
<proof prover="6"><result status="valid" time="0.30" steps="477"/></proof>
</goal>
<goal name="VC trunc_lower_bound.0.3" expl="assertion" proved="true">
<transf name="unfold" proved="true" arg1="trunc_at">
......@@ -42,8 +42,8 @@
</transf>
</goal>
<goal name="VC trunc_lower_bound.1" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.05" steps="141"/></proof>
<proof prover="8" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="6"><result status="valid" time="0.05" steps="135"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
......@@ -95,13 +95,13 @@
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.10" expl="assertion" proved="true">
<proof prover="5" edited="sqrt_Sqrt1_VC_sqrt1_2.v"><result status="valid" time="0.63"/></proof>
<proof prover="5" edited="sqrt_Sqrt1_VC_sqrt1_2.v"><result status="valid" time="1.08"/></proof>
</goal>
<goal name="VC sqrt1.11" expl="fxp overflow" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sqrt1.12" expl="assertion" proved="true">
<proof prover="5" edited="sqrt_Sqrt1_VC_sqrt1_3.v"><result status="valid" time="0.63"/></proof>
<proof prover="5" edited="sqrt_Sqrt1_VC_sqrt1_3.v"><result status="valid" time="1.08"/></proof>
</goal>
<goal name="VC sqrt1.13" expl="fxp overflow" proved="true">
<proof prover="0"><result status="valid" time="0.08"/></proof>
......@@ -113,7 +113,7 @@
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC sqrt1.16" expl="assertion" proved="true">
<proof prover="5" edited="sqrt_Sqrt1_VC_sqrt1_1.v"><result status="valid" time="0.62"/></proof>
<proof prover="5" edited="sqrt_Sqrt1_VC_sqrt1_1.v"><result status="valid" time="1.01"/></proof>
</goal>
<goal name="VC sqrt1.17" expl="fxp overflow" proved="true">
<proof prover="0"><result status="valid" time="0.09"/></proof>
......@@ -133,7 +133,7 @@
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC sqrt1.20.2" expl="VC for sqrt1" proved="true">
<proof prover="5" edited="sqrt_Sqrt1_VC_sqrt1_4.v"><result status="valid" time="0.77"/></proof>
<proof prover="5" edited="sqrt_Sqrt1_VC_sqrt1_4.v"><result status="valid" time="1.18"/></proof>
</goal>
</transf>
</goal>
......@@ -184,13 +184,13 @@
<goal name="VC sqrt1.24" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC sqrt1.24.0" expl="assertion" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.19"/></proof>
<proof prover="0" memlimit="2000"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="VC sqrt1.24.1" expl="VC for sqrt1" proved="true">
<proof prover="3"><result status="valid" time="0.34"/></proof>
<proof prover="3"><result status="valid" time="3.48"/></proof>
</goal>
<goal name="VC sqrt1.24.2" expl="VC for sqrt1" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.20"/></proof>
<proof prover="0" memlimit="2000"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="VC sqrt1.24.3" expl="VC for sqrt1" proved="true">
<proof prover="7"><result status="valid" time="0.09"/></proof>
......@@ -199,7 +199,7 @@
<proof prover="8"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC sqrt1.24.5" expl="VC for sqrt1" proved="true">
<proof prover="6"><result status="valid" time="1.11" steps="184"/></proof>
<proof prover="6"><result status="valid" time="1.55" steps="184"/></proof>
</goal>
<goal name="VC sqrt1.24.6" expl="VC for sqrt1" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.32"/></proof>
......@@ -232,7 +232,7 @@
</transf>
</goal>
<goal name="VC sqrt1.24.14" expl="VC for sqrt1" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.39"/></proof>
<proof prover="0" memlimit="2000"><result status="valid" time="0.78"/></proof>
</goal>
<goal name="VC sqrt1.24.15" expl="VC for sqrt1" proved="true">
<proof prover="8"><result status="valid" time="0.42"/></proof>
......@@ -265,23 +265,23 @@
</transf>
</goal>
<goal name="VC sqrt1.24.22" expl="VC for sqrt1" proved="true">
<proof prover="3"><result status="valid" time="1.56"/></proof>
<proof prover="3"><result status="valid" time="2.19"/></proof>
</goal>
<goal name="VC sqrt1.24.23" expl="VC for sqrt1" proved="true">
<proof prover="8"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC sqrt1.24.24" expl="VC for sqrt1" proved="true">
<proof prover="8"><result status="valid" time="1.02"/></proof>
<proof prover="8"><result status="valid" time="1.50"/></proof>
</goal>
</transf>
</goal>
<goal name="VC sqrt1.25" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="2.62"/></proof>
<proof prover="3"><result status="valid" time="3.80"/></proof>
</goal>
<goal name="VC sqrt1.26" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC sqrt1.26.0" expl="assertion" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.24"/></proof>
<proof prover="0" memlimit="2000"><result status="valid" time="0.44"/></proof>
</goal>
</transf>
</goal>
......@@ -292,19 +292,19 @@
<proof prover="8"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC sqrt1.29" expl="integer overflow" proved="true">
<proof prover="8"><result status="valid" time="0.21"/></proof>
<proof prover="8"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC sqrt1.30" expl="integer overflow" proved="true">
<proof prover="8"><result status="valid" time="0.18"/></proof>
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC sqrt1.31" expl="assertion" proved="true">
<proof prover="8"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC sqrt1.32" expl="integer overflow" proved="true">
<proof prover="8"><result status="valid" time="0.18"/></proof>
<proof prover="8"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC sqrt1.33" expl="integer overflow" proved="true">
<proof prover="8"><result status="valid" time="0.19"/></proof>
<proof prover="8"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC sqrt1.34" expl="integer overflow" proved="true">
<proof prover="8"><result status="valid" time="0.20"/></proof>
......
This diff is collapsed.
This diff is collapsed.
......@@ -136,7 +136,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_zero_p.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="45"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="43"/></proof>
</goal>
<goal name="VC wmpn_zero_p.9" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -154,7 +154,7 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_zero_p.14" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
</transf>
</goal>
......
......@@ -602,6 +602,14 @@ module UInt64GMP
requires { mod (to_int x) (power 2 (to_int cnt)) = 0 }
ensures { to_int x = (power 2 (to_int cnt)) * to_int result }
val lsr_mod (x cnt: uint64) : uint64
requires { 0 <= cnt < 64 }
ensures { result = div x (power 2 cnt) }
val lsl_mod (x cnt: uint64) : uint64
requires { 0 <= cnt < 64 }
ensures { result = mod (x * power 2 cnt) radix }
val div2by1 (l h d:uint64) : uint64
requires { to_int h < to_int d }
(* this pre implies d > 0 and also
......
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