Skip to content

why3
why3
Commit 76d42ea4 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files
Options

Add more GMP primitives

parent f0b904bf
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 2559 additions and 2522 deletions
drivers/c.drv
View file @ 76d42ea4
......@@ -225,7 +225,8 @@ struct __add64_with_carry_result
uint64_t __field_1;
};
struct __add64_with_carry_result add64_with_carry(uint64_t x, uint64_t y, uint64_t c)
struct __add64_with_carry_result
add64_with_carry(uint64_t x, uint64_t y, uint64_t c)
{
struct __add64_with_carry_result result;
uint64_t r = x + y + c;
......@@ -235,12 +236,26 @@ struct __add64_with_carry_result add64_with_carry(uint64_t x, uint64_t y, uint64
return result;
}
struct __add64_double_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __add64_double_result
add64_double(uint64_t a1, uint64_t a0, uint64_t b1, uint64_t b0)
{
struct __add64_double_result result;
add_ssaaaa(result.__field_0, result.__field_1, a1, a0, b1, b0);
return result;
}
struct __sub64_with_borrow_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __sub64_with_borrow_result sub64_with_borrow(uint64_t x, uint64_t y, uint64_t b)
struct __sub64_with_borrow_result
sub64_with_borrow(uint64_t x, uint64_t y, uint64_t b)
{
struct __sub64_with_borrow_result result;
uint64_t r = x - y - b;
......@@ -251,6 +266,19 @@ struct __sub64_with_borrow_result sub64_with_borrow(uint64_t x, uint64_t y, uint
return result;
}
struct __sub64_double_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __sub64_double_result
sub64_double(uint64_t a1, uint64_t a0, uint64_t b1, uint64_t b0)
{
struct __sub64_double_result result;
sub_ddmmss(result.__field_0, result.__field_1, a1, a0, b1, b0);
return result;
}
struct __mul64_double_result
{ uint64_t __field_0;
uint64_t __field_1;
......@@ -317,6 +345,12 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
syntax val (>) "%1 > %2"
syntax val add_with_carry "add64_with_carry"
syntax val add_double "add64_double"
syntax val add_double_nc "add64_double"
syntax val add_double_gc "add64_double"
syntax val sub_double "sub64_double"
syntax val sub_double_nb "sub64_double"
syntax val sub_double_gb "sub64_double"
syntax val sub_with_borrow "sub64_with_borrow"
syntax val mul_double "mul64_double"
syntax val div2by1 "div64_2by1"
......
examples/in_progress/multiprecision/mp2.mlw
View file @ 76d42ea4
......@@ -2519,16 +2519,12 @@ module N
returns { q, r -> l2i q * d + l2i r = ul + radix * uh }
returns { _q, r -> 0 <= l2i r < d }
=
let zero = Limb.of_int 0 in
let one = Limb.of_int 1 in
let ghost k = radix * radix - (radix + l2i v) * l2i d in
let ghost u = l2i ul + radix * l2i uh in
assert { 1 <= k <= d };
let l,h = mul_double v uh in
let sl,c = add_with_carry l ul zero in
let (sh,ghost c') = add_with_carry uh h c in (* <c',sh,sl> = <uh, ul> + <h,l> *)
assert { sl + radix * sh + radix * radix * c'
= l + radix * h + ul + radix * uh };
let (ghost c', sh, sl) = add_double_gc h l uh ul in
assert { c' = 0
by
uh < d
......@@ -3038,8 +3034,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let r0 = ref zero in
let r1 = ref zero in
let l,h = mul_double v uh in
let sl, c = add_with_carry um l zero in
let sh, ghost c' = add_with_carry uh h c in
let (ghost c', sh, sl) = add_double_gc uh um h l in
assert { sl + radix * sh + radix * radix * c'
= um + radix * uh + v * uh };
assert { c' = 0
......@@ -3069,14 +3064,10 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
(*assert { um - dh * sh = a * radix + !r1
by !r1 = mod (um - dh * sh) radix };*)
let tl, th = mul_double sh dl in
let il, b = sub_with_borrow ul tl zero in
let (ih, ghost b') = sub_with_borrow !r1 th b in
let (ghost b', ih, il) = sub_double_gb !r1 ul th tl in
assert { il + radix * ih - radix * radix * b'
= ul + radix * !r1 - sh * dl };
let bl,b2 = sub_with_borrow il dl zero in
let bh, ghost b2' = sub_with_borrow ih dh b2 in
assert { bl + radix * bh - radix * radix * b2'
= il + radix * ih - dl - radix * dh };
let (bh, bl) = sub_double ih il dh dl in
mod_mult (radix * radix) (l2i b')
(l2i ul + radix * l2i !r1 - l2i sh * l2i dl - l2i dl
- radix * l2i dh);
......@@ -3445,8 +3436,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
so (!q1 at PreCorrections) = cq
so !q1 = mod (cq - 1) radix = cq - 1
};
let rl, c = add_with_carry !r0 dl zero in
let rh, ghost c' = add_with_carry !r1 dh c in
let (ghost c', rh, rl) = add_double_gc !r1 !r0 dh dl in
assert { rl + radix * rh = mod (r' + d) (radix * radix)
by radix * radix * c' + rl + radix * rh
= r' + d
......@@ -3502,9 +3492,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
label PreRemAdjust in
if [@ex:unlikely] (Limb.(>) !r1 dh) || (Limb.(=) !r1 dh && Limb.(>=) !r0 dl)
then begin
let bl, b = sub_with_borrow !r0 dl zero in
let bh, ghost b'= sub_with_borrow !r1 dh b in
assert { b' = 0 };
let (bh, bl) = sub_double_nb !r1 !r0 dh dl in
assert { bl + radix * bh = !r0 + radix * !r1 - d };
assert { !q1 < radix - 1
by !q1 * d + !r0 + radix * !r1 = u
......@@ -5962,9 +5950,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
+ power radix !i * (!rl + radix * !rh) }
ensures { !rl + radix * !rh < dl + radix * dh }
ensures { !qh = 1 }
let (r0, b) = sub_with_borrow !rl dl uzero in
let (r1, ghost b') = sub_with_borrow !rh dh b in
assert { b' = 0 };
let (r1,r0) = sub_double_nb !rh !rl dh dl in
assert { r0 + radix * r1 = !rl + radix * !rh - (dl + radix * dh) };
value_sub_tail (pelts x) x.offset (x.offset + p2i sx - 1);
value_sub_tail (pelts x) x.offset (x.offset + p2i sx - 2);
......
examples/multiprecision/add/why3session.xml
View file @ 76d42ea4
This diff is collapsed.
examples/multiprecision/div/why3session.xml
View file @ 76d42ea4
This diff is collapsed.
examples/multiprecision/logical/why3session.xml
View file @ 76d42ea4
......@@ -88,7 +88,7 @@
<goal name="VC lsld_ext.5" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC lsld_ext.5.0" expl="assertion" proved="true">
<proof prover="0" memlimit="1000"><result status="valid" time="0.06"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="0.18"/></proof>
</goal>
</transf>
</goal>
......@@ -449,19 +449,19 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC lshift.34.13" expl="VC for lshift" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC lshift.34.14" expl="VC for lshift" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC lshift.34.13.0" expl="VC for lshift" proved="true">
<transf name="rewrite" proved="true" arg1="H">
<goal name="VC lshift.34.13.0.0" expl="VC for lshift" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<goal name="VC lshift.34.14.0" expl="VC for lshift" proved="true">
<transf name="rewrite" proved="true" arg1="&lt;-" arg2="H">
<goal name="VC lshift.34.14.0.0" expl="VC for lshift" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC lshift.34.14" expl="VC for lshift" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC lshift.34.15" expl="VC for lshift" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -490,7 +490,7 @@
<proof prover="2" timelimit="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC lshift.37" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="2.54"/></proof>
<proof prover="0"><result status="valid" time="2.16"/></proof>
</goal>
<goal name="VC lshift.38" expl="loop invariant preservation" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.10"/></proof>
......@@ -549,7 +549,7 @@
</transf>
</goal>
<goal name="VC lshift.54" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="1.98"/></proof>
<proof prover="1"><result status="valid" time="1.60"/></proof>
</goal>
</transf>
</goal>
......
examples/multiprecision/mul/why3session.xml
View file @ 76d42ea4
......@@ -284,7 +284,7 @@
<goal name="VC addmul_limb.22.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC addmul_limb.22.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.23"/></proof>
<proof prover="0"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="VC addmul_limb.22.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.27"/></proof>
......@@ -435,7 +435,7 @@
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="57"/></proof>
</goal>
<goal name="VC mul_limbs.21" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="4.10"/></proof>
<proof prover="4"><result status="valid" time="4.68"/></proof>
</goal>
<goal name="VC mul_limbs.22" expl="precondition" proved="true">
<proof prover="5" memlimit="2000"><result status="valid" time="0.04" steps="58"/></proof>
......@@ -524,7 +524,7 @@
<proof prover="0"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="VC mul_limbs.38.0.0.0.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="2.06"/></proof>
<proof prover="3"><result status="valid" time="1.35"/></proof>
</goal>
</transf>
</goal>
......@@ -992,7 +992,7 @@
<proof prover="5" memlimit="2000"><result status="valid" time="0.14" steps="67"/></proof>
</goal>
<goal name="VC mul.27" expl="assertion" proved="true">
<proof prover="5" memlimit="2000"><result status="valid" time="0.84" steps="137"/></proof>
<proof prover="5" memlimit="2000"><result status="valid" time="0.59" steps="137"/></proof>
</goal>
<goal name="VC mul.28" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.60"/></proof>
......@@ -1112,7 +1112,7 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.15" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.16" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -1121,7 +1121,7 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.18" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.19" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1136,7 +1136,7 @@
<proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.23" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.24" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1253,10 +1253,10 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.62" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.63" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.64" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1304,7 +1304,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.79" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mul.41.0.0.0.0.0.0.80" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......
examples/multiprecision/sub/why3session.xml
View file @ 76d42ea4
This diff is collapsed.
examples/multiprecision/util/why3session.xml
View file @ 76d42ea4
......@@ -76,14 +76,14 @@
</goal>
<goal name="VC copy.22" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="213"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC copy.23" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC copy.24" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="101"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC copy.25" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
......@@ -105,7 +105,7 @@
</goal>
<goal name="VC copy.31" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="108"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC copy.32" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -137,11 +137,11 @@
</goal>
<goal name="VC is_zero.6" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC is_zero.7" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC is_zero.8" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -157,7 +157,7 @@
</goal>
<goal name="VC is_zero.12" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC is_zero.13" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -170,7 +170,7 @@
</goal>
<goal name="VC is_zero.16" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="36"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC is_zero.17" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -202,7 +202,7 @@
</goal>
<goal name="VC zero.5" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC zero.6" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -221,11 +221,11 @@
</goal>
<goal name="VC zero.11" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="110"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC zero.12" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="51"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC zero.13" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
......
stdlib/mach/int.mlw
View file @ 76d42ea4
......@@ -144,6 +144,22 @@ module UnsignedGMP
to_int x + to_int y + to_int c
/\ 0 <= to_int d <= 1 }
(* add_ssaaaa *)
val add_double (a1 a0 b1 b0:t) : (t,t)
returns { (h,l) -> l + radix * h
= mod (a0 + radix * a1 + b0 + radix * b1) (radix * radix) }
(* add_ssaaaa with no overflow *)
val add_double_nc (a1 a0 b1 b0:t) : (t,t)
requires { a0 + radix * a1 + b0 + radix * b1 < radix * radix }
returns { (h, l) -> l + radix * h = a0 + radix * a1 + b0 + radix * b1 }
(* add_ssaaaa with ghost carry *)
val add_double_gc (a1 a0 b1 b0:t) : (ghost t, t, t)
returns { (c,h,l) -> l + radix * h + radix * radix * c
= a0 + radix * a1 + b0 + radix * b1
/\ 0 <= to_int c <= 1 }
val sub_mod (x y:t) : t
ensures { to_int result = mod (to_int x - to_int y) radix }
......@@ -154,6 +170,23 @@ module UnsignedGMP
to_int x - to_int y - to_int b
/\ 0 <= to_int d <= 1 }
(* sub_ddmmss *)
val sub_double (a1 a0 b1 b0:t) : (t,t)
returns { (h,l) -> l + radix * h
= mod ((a0 + radix * a1) - (b0 + radix * b1))
(radix * radix) }
(* sub_ddmmss with no underflow *)
val sub_double_nb (a1 a0 b1 b0:t) : (t,t)
requires { 0 <= ((a0 + radix * a1) - (b0 + radix * b1)) }
returns { (h,l) -> l + radix * h = ((a0 + radix * a1) - (b0 + radix * b1)) }
(* sub_ddmmss with ghost borrow *)
val sub_double_gb (a1 a0 b1 b0:t) : (ghost t,t,t)
returns { (b,h,l) -> l + radix * h - radix*radix*b
= ((a0 + radix * a1) - (b0 + radix * b1))
/\ 0 <= b <= 1 }
val add3 (x y z:t) : (t,t)
returns { (r,d) ->
to_int r + radix * to_int d =
......@@ -163,7 +196,7 @@ module UnsignedGMP
val mul_mod (x y:t) : t
ensures { to_int result = mod (to_int x * to_int y) radix }
val mul_double (x y:t) : (t,t)
val mul_double (x y:t) : (t,t) (* umul_ppmm *)
returns { (r,d) ->
to_int r + radix * to_int d =
to_int x * to_int y }
......
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