Skip to content

GitLab

why3
why3
Commit 0c28085b authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft
Browse files
Options

wmp: modular exponentiation proof

parent 05b27250
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 8945 additions and 1892 deletions
drivers/c.drv
View file @ 0c28085b
......@@ -201,6 +201,7 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
syntax val add_mod "%1 + %2" prec 4 4 3
syntax val sub_mod "%1 - %2" prec 4 4 3
syntax val minus_mod "-%2" prec 2 1
syntax val mul_mod "%1 * %2" prec 3 3 2
syntax val div2by1
......@@ -213,6 +214,7 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
syntax val is_msb_set "%1 & 0x80000000U" prec 8 8
syntax val count_leading_zeros "__builtin_clz(%1)" prec 1 15
syntax val count_trailing_zeros "__builtin_ctz(%1)" prec 1 15
syntax val of_int32 "(uint32_t)%1" prec 2 2
......@@ -420,6 +422,7 @@ static inline struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
syntax val add_mod "%1 + %2" prec 4 4 3
syntax val sub_mod "%1 - %2" prec 4 4 3
syntax val minus_mod "-%2" prec 2 1
syntax val mul_mod "%1 * %2" prec 3 3 2
syntax val lsl "%1 << %2" prec 5 5 2
......@@ -430,6 +433,7 @@ static inline struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
syntax val is_msb_set "%1 & 0x8000000000000000UL" prec 8 7
syntax val count_leading_zeros "__builtin_clzll(%1)" prec 1 15
syntax val count_trailing_zeros "__builtin_ctzll(%1)" prec 1 15
syntax val to_int32 "(int32_t)%1" prec 2 2
syntax val of_int32 "(uint64_t)%1" prec 2 2
......
examples/multiprecision/div/why3session.xml
View file @ 0c28085b
......@@ -3386,7 +3386,7 @@
<goal name="VC div_sb_qr.44" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC div_sb_qr.44.0" expl="VC for div_sb_qr" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="1.52" steps="221"/></proof>
<proof prover="5" timelimit="1"><result status="valid" time="1.16" steps="221"/></proof>
</goal>
<goal name="VC div_sb_qr.44.1" expl="VC for div_sb_qr" proved="true">
<proof prover="9"><result status="valid" time="0.08" steps="22252"/></proof>
......@@ -5063,13 +5063,13 @@
<proof prover="3"><result status="valid" time="0.02" steps="16126"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.138" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="16118"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="16118"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.139" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="16118"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.140" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="16118"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="16118"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.141" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="16126"/></proof>
......@@ -5087,13 +5087,13 @@
<proof prover="3"><result status="valid" time="0.02" steps="16126"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.146" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="16118"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="16118"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.147" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="16118"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.148" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="16118"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="16118"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.149" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="16126"/></proof>
......@@ -6736,20 +6736,20 @@
<proof prover="9"><result status="valid" time="0.22" steps="86449"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.137" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.27" steps="84489"/></proof>
<proof prover="9"><result status="valid" time="0.22" steps="84859"/></proof>
<proof prover="2"><result status="valid" time="0.23" steps="84489"/></proof>
<proof prover="9"><result status="valid" time="0.21" steps="84859"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.138" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24" steps="84357"/></proof>
<proof prover="9"><result status="valid" time="0.33" steps="84727"/></proof>
<proof prover="2"><result status="valid" time="0.27" steps="84357"/></proof>
<proof prover="9"><result status="valid" time="0.23" steps="84727"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.139" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18" steps="84369"/></proof>
<proof prover="9"><result status="valid" time="0.22" steps="84739"/></proof>
<proof prover="2"><result status="valid" time="0.19" steps="84369"/></proof>
<proof prover="9"><result status="valid" time="0.33" steps="84739"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.140" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.17" steps="84369"/></proof>
<proof prover="9"><result status="valid" time="0.27" steps="84739"/></proof>
<proof prover="9"><result status="valid" time="0.21" steps="84739"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.141" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.29" steps="84489"/></proof>
......@@ -6768,20 +6768,20 @@
<proof prover="9"><result status="valid" time="0.22" steps="84739"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.145" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23" steps="84489"/></proof>
<proof prover="9"><result status="valid" time="0.21" steps="84859"/></proof>
<proof prover="2"><result status="valid" time="0.27" steps="84489"/></proof>
<proof prover="9"><result status="valid" time="0.22" steps="84859"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.146" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.27" steps="84357"/></proof>
<proof prover="9"><result status="valid" time="0.23" steps="84727"/></proof>
<proof prover="2"><result status="valid" time="0.24" steps="84357"/></proof>
<proof prover="9"><result status="valid" time="0.33" steps="84727"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.147" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19" steps="84369"/></proof>
<proof prover="9"><result status="valid" time="0.33" steps="84739"/></proof>
<proof prover="2"><result status="valid" time="0.18" steps="84369"/></proof>
<proof prover="9"><result status="valid" time="0.22" steps="84739"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.148" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.17" steps="84369"/></proof>
<proof prover="9"><result status="valid" time="0.21" steps="84739"/></proof>
<proof prover="9"><result status="valid" time="0.27" steps="84739"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.149" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18" steps="84492"/></proof>
......@@ -6800,8 +6800,8 @@
<proof prover="9"><result status="valid" time="0.30" steps="84739"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.153" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25" steps="84169"/></proof>
<proof prover="9"><result status="valid" time="0.29" steps="84539"/></proof>
<proof prover="2"><result status="valid" time="0.17" steps="84169"/></proof>
<proof prover="9"><result status="valid" time="0.22" steps="84539"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.154" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24" steps="84167"/></proof>
......@@ -6852,36 +6852,36 @@
<proof prover="9"><result status="valid" time="0.29" steps="86449"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.166" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18" steps="84489"/></proof>
<proof prover="9"><result status="valid" time="0.21" steps="84859"/></proof>
<proof prover="2"><result status="valid" time="0.19" steps="84489"/></proof>
<proof prover="9"><result status="valid" time="0.29" steps="84859"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.167" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.28" steps="84357"/></proof>
<proof prover="9"><result status="valid" time="0.23" steps="84727"/></proof>
<proof prover="9"><result status="valid" time="0.33" steps="84727"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.168" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.26" steps="84366"/></proof>
<proof prover="9"><result status="valid" time="0.29" steps="84736"/></proof>
<proof prover="2"><result status="valid" time="0.28" steps="84366"/></proof>
<proof prover="9"><result status="valid" time="0.32" steps="84736"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.169" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19" steps="84366"/></proof>
<proof prover="9"><result status="valid" time="0.26" steps="84736"/></proof>
<proof prover="2"><result status="valid" time="0.31" steps="84366"/></proof>
<proof prover="9"><result status="valid" time="0.27" steps="84736"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.170" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19" steps="84489"/></proof>
<proof prover="9"><result status="valid" time="0.29" steps="84859"/></proof>
<proof prover="2"><result status="valid" time="0.18" steps="84489"/></proof>
<proof prover="9"><result status="valid" time="0.21" steps="84859"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.171" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.28" steps="84357"/></proof>
<proof prover="9"><result status="valid" time="0.33" steps="84727"/></proof>
<proof prover="9"><result status="valid" time="0.23" steps="84727"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.172" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.28" steps="84366"/></proof>
<proof prover="9"><result status="valid" time="0.32" steps="84736"/></proof>
<proof prover="2"><result status="valid" time="0.26" steps="84366"/></proof>
<proof prover="9"><result status="valid" time="0.29" steps="84736"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.173" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.31" steps="84366"/></proof>
<proof prover="9"><result status="valid" time="0.27" steps="84736"/></proof>
<proof prover="2"><result status="valid" time="0.19" steps="84366"/></proof>
<proof prover="9"><result status="valid" time="0.26" steps="84736"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.174" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.30" steps="84492"/></proof>
......@@ -6952,8 +6952,8 @@
<proof prover="9"><result status="valid" time="0.20" steps="84536"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.191" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.17" steps="84169"/></proof>
<proof prover="9"><result status="valid" time="0.22" steps="84539"/></proof>
<proof prover="2"><result status="valid" time="0.25" steps="84169"/></proof>
<proof prover="9"><result status="valid" time="0.29" steps="84539"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.192" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18" steps="84169"/></proof>
......
examples/multiprecision/lineardecision.mlw
View file @ 0c28085b
......@@ -1725,7 +1725,7 @@ let rec lemma interp_ctx_impl' (ctx: context') (g1 g2:equality')
variant { ctx }
= match ctx with Nil -> () | Cons _ t -> interp_ctx_impl' t g1 g2 end
let lemma impl_cons (c1 c2:context') (e:equality') (y z:vars)
let lemma impl_cons (c1 c2:context') (e:equality')
requires { ctx_impl_ctx' c1 c2 }
requires { forall y z. interp_ctx' c1 e y z }
ensures { ctx_impl_ctx' c1 (Cons e c2) }
......
examples/multiprecision/powm.mlw 0 → 100644
View file @ 0c28085b
This diff is collapsed.
examples/multiprecision/powm/why3session.xml 0 → 100644
View file @ 0c28085b
This diff is collapsed.
examples/multiprecision/sqrtrem.mlw
View file @ 0c28085b
......@@ -246,7 +246,6 @@ module Sqrt
requires { valid scratch (1 + div n 2) }
requires { (pelts np)[offset np + n + n - 1] >= power 2 (Limb.length - 2) }
requires { 4 * n < max_int32 }
raises { StackOverflow -> true }
(* writes { np, sp, scratch }*)
ensures { (value sp n) * (value sp n)
+ value np n + (power radix n) * result
......@@ -857,7 +856,6 @@ module Sqrt
requires { 1 <= n }
requires { 4 * n < max_int32 }
requires { (pelts np)[offset np + n - 1] > 0 }
raises { StackOverflow -> true }
ensures { value np n = value sp (ceilhalf n) * value sp (ceilhalf n)
+ value rp result }
ensures { 0 <= result <= n }
......
examples/multiprecision/sqrtrem/why3session.xml
View file @ 0c28085b
......@@ -2945,12 +2945,6 @@
<goal name="VC wmpn_dc_sqrtrem.300" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.35" steps="37816"/></proof>
</goal>
<goal name="VC wmpn_dc_sqrtrem.301" expl="exceptional postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.07" steps="27820"/></proof>
</goal>
<goal name="VC wmpn_dc_sqrtrem.302" expl="exceptional postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="22935"/></proof>
</goal>
</transf>
</goal>
<goal name="VC ceilhalf" expl="VC for ceilhalf" proved="true">
......@@ -4689,257 +4683,242 @@
<goal name="VC wmpn_sqrtrem.296" expl="postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.22" steps="34250"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.297" expl="exceptional postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.06" steps="24911"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.298" expl="exceptional postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.06" steps="24424"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.299" expl="exceptional postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.07" steps="23159"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.300" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.297" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.05" steps="23503"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.301" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.298" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.06" steps="23506"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.302" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.299" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC wmpn_sqrtrem.302.0" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.299.0" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.11" steps="25893"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.302.1" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.299.1" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="6"><result status="valid" time="0.11" steps="25690"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.302.2" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.299.2" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="3"><result status="valid" time="0.07" steps="127"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.302.3" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.299.3" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="3"><result status="valid" time="0.16" steps="129"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.302.4" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.299.4" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="6"><result status="valid" time="0.12" steps="26938"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.302.5" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.299.5" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="3"><result status="valid" time="0.16" steps="133"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.302.6" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.299.6" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="6"><result status="valid" time="0.15" steps="33838"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_sqrtrem.303" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.300" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC wmpn_sqrtrem.303.0" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.300.0" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.14" steps="26002"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.303.1" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.300.1" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="3"><result status="valid" time="0.20" steps="129"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_sqrtrem.304" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.301" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.15" steps="34123"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.305" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.302" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.10" steps="26223"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.306" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.303" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.18" steps="25912"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.307" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.304" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.24" steps="47945"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.308" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.305" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.10" steps="24554"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.309" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.306" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.20" steps="26045"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.310" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.307" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="1.62"/></proof>
<proof prover="6"><result status="valid" time="0.11" steps="26967"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.311" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.308" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="6"><result status="valid" time="0.07" steps="24642"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.312" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.309" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.25" steps="36555"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.313" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.310" expl="precondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.22" steps="27069"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.314" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.311" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC wmpn_sqrtrem.314.0" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.311.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.314.1" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.311.1" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="6"><result status="valid" time="0.20" steps="27031"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.314.2" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.311.2" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="6"><result status="valid" time="0.16" steps="27277"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_sqrtrem.315" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.312" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC wmpn_sqrtrem.315.0" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.312.0" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.19" steps="27243"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.315.1" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.312.1" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.11" steps="191"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_sqrtrem.316" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.313" expl="precondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.19" steps="27055"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.317" expl="integer overflow" proved="true">
<goal name="VC wmpn_sqrtrem.314" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.25" steps="37660"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.318" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.315" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="195"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.319" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.316" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.17" steps="27391"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.320" expl="loop invariant init" proved="true">
<goal name="VC wmpn_sqrtrem.317" expl="loop invariant init" proved="true">
<proof prover="6"><result status="valid" time="0.15" steps="24830"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.321" expl="loop invariant init" proved="true">
<goal name="VC wmpn_sqrtrem.318" expl="loop invariant init" proved="true">
<proof prover="6"><result status="valid" time="0.13" steps="24852"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.322" expl="integer overflow" proved="true">
<goal name="VC wmpn_sqrtrem.319" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.18" steps="38496"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.323" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.320" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.17" steps="38808"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.324" expl="integer overflow" proved="true">
<goal name="VC wmpn_sqrtrem.321" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.24" steps="38904"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.325" expl="precondition" proved="true">
<goal name="VC wmpn_sqrtrem.322" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.09" steps="27589"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.326" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.323" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.12" steps="213"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.327" expl="integer overflow" proved="true">
<goal name="VC wmpn_sqrtrem.324" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.17" steps="40215"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.328" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.325" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC wmpn_sqrtrem.328.0" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.325.0" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.47" steps="68930"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.328.1" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.325.1" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.17" steps="28866"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.328.2" expl="assertion" proved="true">
<goal name="VC wmpn_sqrtrem.325.2" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.13" steps="29279"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.328.3" expl="VC for wmpn_sqrtrem" proved="true">
<goal name="VC wmpn_sqrtrem.325.3" expl="VC for wmpn_sqrtrem" proved="true">
<proof prover="6"><result status="valid" time="0.07" steps="25204"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_sqrtrem.329" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.326" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.34" steps="68304"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.330" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.327" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.11" steps="27921"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.331" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.328" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.18" steps="29291"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.332" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.329" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.10" steps="28520"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.333" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.330" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.09" steps="25266"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.334" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.331" expl="postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.07" steps="25267"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.335" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.332" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.09" steps="25268"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.336" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.333" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.16" steps="28235"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.337" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.334" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.15" steps="28247"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.338" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.335" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.16" steps="28674"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.339" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.336" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.11" steps="25566"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.340" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.337" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.12" steps="25569"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.341" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.338" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.09" steps="25529"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.342" expl="loop variant decrease" proved="true">
<goal name="VC wmpn_sqrtrem.339" expl="loop variant decrease" proved="true">
<proof prover="6"><result status="valid" time="0.13" steps="27651"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.343" expl="loop invariant preservation" proved="true">
<goal name="VC wmpn_sqrtrem.340" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.11" steps="28458"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.344" expl="loop invariant preservation" proved="true">
<goal name="VC wmpn_sqrtrem.341" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.14" steps="27956"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.345" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.342" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.346" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.343" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.20" steps="27688"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.347" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.344" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.11" steps="215"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.348" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.345" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.48" steps="219"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.349" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.346" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.14" steps="25141"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.350" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.347" expl="postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.08" steps="25142"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.351" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.348" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.10" steps="25143"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.352" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.349" expl="postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.09" steps="27993"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.353" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.350" expl="postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.17" steps="28005"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.354" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.351" expl="postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.21" steps="28432"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.355" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.352" expl="postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.08" steps="25441"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.356" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.353" expl="postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.08" steps="25444"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.357" expl="postcondition" proved="true">
<goal name="VC wmpn_sqrtrem.354" expl="postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.12" steps="25404"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.358" expl="exceptional postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.06" steps="24010"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.359" expl="exceptional postcondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="22907"/></proof>
</goal>
</transf>
</goal>
</theory>
......
examples/multiprecision/toom.mlw
View file @ 0c28085b
......@@ -60,7 +60,6 @@ let rec wmpn_toom22_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
-> (pelts r)[j] = old (pelts r)[j] }
ensures { forall j. min scratch <= j < offset scratch
-> (pelts scratch)[j] = old (pelts scratch)[j] }
raises { StackOverflow -> true }