Commit cdb47d44 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Rework add/sub to be closer to GMP implementation

In particular, inline and simplify uses of add_with_carry/sub_with_borrow with a zero argument.
parent 404521ff
......@@ -30,7 +30,7 @@ module mach.int.Int32
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (-_) "-(%1)"
syntax val (*) "(%1) * (%2)"
syntax val ( * ) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
......@@ -56,7 +56,7 @@ module mach.int.UInt32
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (*) "(%1) * (%2)"
syntax val ( * ) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
......@@ -187,7 +187,7 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (*) "(%1) * (%2)"
syntax val ( * ) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
......@@ -230,7 +230,7 @@ module mach.int.Int64
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (-_) "-(%1)"
syntax val (*) "(%1) * (%2)"
syntax val ( * ) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
......@@ -256,7 +256,7 @@ module mach.int.UInt64
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (-_) "-(%1)"
syntax val (*) "(%1) * (%2)"
syntax val ( * ) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
......@@ -396,67 +396,121 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
#include \"longlong.h\"
#undef invert_limb
struct __add64_with_carry_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __add64_with_carry_result
add64_with_carry(uint64_t x, uint64_t y, uint64_t c);
static 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;
result.__field_0 = r;
if (r == x) result.__field_1 = c;
else result.__field_1 = (r < x);
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);
static 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);
static 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;
result.__field_0 = r;
if (r > x) result.__field_1 = 1;
else if (r == x) result.__field_1 = b;
else result.__field_1 = 0;
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);
static 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;
};
struct __mul64_double_result mul64_double(uint64_t x, uint64_t y);
static struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
{
struct __mul64_double_result result;
umul_ppmm(result.__field_1,result.__field_0,x,y);
return result;
}
uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d);
static uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
{
uint64_t q;
uint64_t _dummy __attribute__((unused));
udiv_qrnnd(q,_dummy,uh,ul,d);
return q;
}
struct __add64_3_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __add64_3_result add64_3(uint64_t x, uint64_t y, uint64_t z);
static struct __add64_3_result add64_3(uint64_t x, uint64_t y, uint64_t z)
{
struct __add64_3_result result;
uint64_t r, c1, c2;
r = x + y;
c1 = r < y;
r += z;
c2 = r < z;
result.__field_1 = c1 + c2;
result.__field_0 = r;
return result;
}
struct __lsld64_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __lsld64_result lsld64(uint64_t x, uint64_t cnt);
static struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
{
struct __lsld64_result result;
result.__field_1 = x >> (64 - cnt);
result.__field_0 = x << cnt;
return result;
}
"
syntax converter of_int "%1ULL"
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (*) "(%1) * (%2)"
syntax val ( * ) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
......
......@@ -26,34 +26,47 @@ module Add
-> (pelts r)[j] = old (pelts r)[j] }
writes { r.data.elts }
=
let limb_zero = Limb.of_int 0 in
let c = ref y in
let lx = ref limb_zero in
let i = ref (Int32.of_int 0) in
while Int32.(<) !i sz && (not (Limb.(=) !c limb_zero)) do
invariant { 0 <= !i <= sz }
invariant { !i > 0 -> 0 <= !c <= 1 }
invariant { value r !i + (power radix !i) * !c =
value x !i + y }
invariant { forall j. (j < offset r \/ offset r + sz <= j)
-> (pelts r)[j] = old (pelts r)[j] }
variant { sz - !i }
lx := get_ofs x !i;
let (res, carry) = add_with_carry !lx !c limb_zero in
set_ofs r !i res;
assert { value r !i + (power radix !i) * !c =
value x !i + y };
c := carry;
value_tail r !i;
value_tail x !i;
assert { value r (!i+1) + (power radix (!i+1)) * !c
= value x (!i+1) + y };
i := Int32.(+) !i (Int32.of_int 1);
done;
if Int32.(=) !i sz then !c
else begin
let lx = ref (C.get x) in
let res = Limb.add_mod !lx y in
let i = ref (1:int32) in
let c = ref (0:limb) in
C.set r res;
if (Limb.(<) res !lx)
then begin
c := 1;
assert { radix + res = !lx + y };
while (Int32.(<) !i sz) do
invariant { 1 <= !i <= sz }
invariant { 0 <= !c <= 1 }
invariant { !i = sz \/ !c = 1 }
invariant { value r !i + (power radix !i) * !c =
value x !i + y }
invariant { forall j. (j < offset r \/ offset r + sz <= j)
-> (pelts r)[j] = old (pelts r)[j] }
variant { sz - !i }
assert { !c = 1 };
lx := get_ofs x !i;
let res = Limb.add_mod !lx 1 in
set_ofs r !i res;
assert { value r !i + (power radix !i) * !c = value x !i + y };
value_tail r !i;
value_tail x !i;
i := Int32.(+) !i 1;
if not (Limb.(=) res 0)
then begin
c := 0;
assert { res = !lx + 1 };
assert { value r !i = value x !i + y };
break
end
else begin
assert { radix + res = !lx + 1 };
assert { value r !i + power radix !i = value x !i + y };
end
done;
end;
while Int32.(<) !i sz do
invariant { !c = 0 }
invariant { !i = sz \/ !c = 0 }
invariant { 0 <= !i <= sz }
invariant { value r !i + (power radix !i) * !c =
value x !i + y }
......@@ -64,14 +77,11 @@ module Add
set_ofs r !i !lx;
assert { value r !i + (power radix !i) * !c =
value x !i + y };
let ghost k = p2i !i in
value_tail r !i;
value_tail x !i;
i := Int32.(+) !i (Int32.of_int 1);
value_sub_tail (pelts r) r.offset (r.offset + k);
value_sub_tail (pelts x) x.offset (x.offset + k);
done;
!c
end
(** `wmpn_add_n r x y sz` adds `x[0..sz-1]` and `y[0..sz-1]` and writes the result in `r`.
Returns the carry, either `0` or `1`. Corresponds to the function `mpn_add_n`. *)
......@@ -161,32 +171,38 @@ module Add
value x (!i+1) + value y (!i+1) };
i := Int32.(+) !i (Int32.of_int 1);
done;
try
begin while Int32.(<) !i sx do
variant { sx - !i }
invariant { sy <= !i <= sx }
invariant { value r !i + (power radix !i) * !c =
value x !i + value y sy }
invariant { 0 <= !c <= 1 }
invariant { forall j. (j < offset r \/ offset r + sx <= j)
if (not (Limb.(=) !c 0))
then begin
while Int32.(<) !i sx do
variant { sx - !i }
invariant { sy <= !i <= sx }
invariant { value r !i + (power radix !i) * !c =
value x !i + value y sy }
invariant { 0 <= !c <= 1 }
invariant { !i = sx \/ !c = 1 }
invariant { forall j. (j < offset r \/ offset r + sx <= j)
-> (pelts r)[j] = old (pelts r)[j] }
(if (Limb.(=) !c (Limb.of_int 0)) then raise Break);
label StartLoop2 in
lx := get_ofs x !i;
let res, carry = add_with_carry !lx limb_zero !c in
set_ofs r !i res;
assert { value r !i + (power radix !i) * !c =
value x !i + value y sy };
c := carry;
value_tail r !i;
value_tail x !i;
assert { value r (!i+1) + (power radix (!i+1)) * !c =
value x (!i+1) + value y sy };
i := Int32.(+) !i (Int32.of_int 1);
done;
assert { !i = sx }
end
with Break -> assert { !c = 0 }
assert { !c = 1 };
lx := get_ofs x !i;
let res = Limb.add_mod !lx (1:limb) in
set_ofs r !i res;
assert { value r !i + (power radix !i) =
value x !i + value y sy };
value_tail r !i;
value_tail x !i;
i := Int32.(+) !i 1;
if (not (Limb.(=) res 0))
then begin
c := 0;
assert { res = !lx + 1 };
assert { value r !i = value x !i + value y sy };
break
end
else begin
assert { !lx + 1 = radix };
assert { value r !i + power radix !i = value x !i + value y sy }
end
done
end;
while Int32.(<) !i sx do
variant { sx - !i }
......@@ -256,52 +272,58 @@ module Add
value ox (!i+1) + value y (!i+1) };
i := Int32.(+) !i (Int32.of_int 1);
done;
try
while Int32.(<) !i sx do
variant { sx - !i }
invariant { sy <= !i <= sx }
invariant { value x !i + (power radix !i) * !c =
value ox !i + value y sy }
invariant { 0 <= !c <= 1 }
invariant { forall j. !i <= j < sx ->
(pelts x)[x.offset + j] = (pelts ox) [x.offset + j] }
invariant { forall j. j < x.offset \/ x.offset + sx <= j ->
(pelts x)[j] = (pelts (old x))[j] }
(if (Limb.(=) !c limb_zero) then raise ReturnLimb limb_zero);
label StartLoop2 in
lx := get_ofs x !i;
assert { !lx = (pelts ox)[ox.offset + !i] };
let res, carry = add_with_carry !lx limb_zero !c in
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sx) res;
set_ofs x !i res;
assert { value x !i + (power radix !i) * !c = value ox !i + value y sy };
c := carry;
assert { forall j. !i < j < sx ->
(pelts x)[x.offset + j] = (pelts ox) [x.offset + j] };
value_tail ox !i;
value_tail x !i;
assert { value x (!i+1) + (power radix (!i+1)) * !c =
value ox (!i+1) + value y sy };
i := Int32.(+) !i (Int32.of_int 1);
done;
assert { !i = sx };
!c
with ReturnLimb n -> begin
assert { n = 0 = !c };
assert { forall j. x.offset + !i <= j < x.offset + sx
if (not (Limb.(=) !c 0))
then begin
while Int32.(<) !i sx do
variant { sx - !i }
invariant { sy <= !i <= sx }
invariant { value x !i + (power radix !i) * !c =
value ox !i + value y sy }
invariant { 0 <= !c <= 1 }
invariant { !i = sx \/ !c = 1 }
invariant { forall j. !i <= j < sx ->
(pelts x)[x.offset + j] = (pelts ox) [x.offset + j] }
invariant { forall j. j < x.offset \/ x.offset + sx <= j ->
(pelts x)[j] = (pelts (old x))[j] }
assert { !c = 1 };
lx := get_ofs x !i;
assert { !lx = (pelts ox)[ox.offset + !i] };
let res = Limb.add_mod !lx 1 in
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sx) res;
set_ofs x !i res;
assert { value x !i + (power radix !i) * !c = value ox !i + value y sy };
assert { forall j. !i < j < sx ->
(pelts x)[x.offset + j] = (pelts ox) [x.offset + j] };
value_tail ox !i;
value_tail x !i;
i := Int32.(+) !i (Int32.of_int 1);
if (not (Limb.(=) res 0))
then begin
c := 0;
assert { res = !lx + 1 };
assert { value x !i = value ox !i + value y sy };
break;
end
else begin
assert { !lx + 1 = radix };
assert { value x !i + power radix !i = value ox !i + value y sy }
end
done
end;
assert { forall j. x.offset + !i <= j < x.offset + sx
-> (pelts x)[j] = (pelts ox)[j]
by !i <= j - x.offset < sx
so (pelts x)[x.offset + (j - x.offset)]
= (pelts ox)[x.offset + (j - x.offset)] };
value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sx);
value_sub_concat (pelts x) x.offset (x.offset + p2i !i) (x.offset + p2i sx);
value_sub_concat (pelts ox) x.offset (x.offset + p2i !i) (x.offset + p2i sx);
assert { value x sx = value (old x) sx + value y sy };
n
end
end
value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i)
(x.offset + p2i sx);
value_sub_concat (pelts x) x.offset (x.offset + p2i !i)
(x.offset + p2i sx);
value_sub_concat (pelts ox) x.offset (x.offset + p2i !i)
(x.offset + p2i sx);
!c
use int.EuclideanDivision
......@@ -318,44 +340,58 @@ module Add
writes { x.data.elts }
=
let ghost ox = { x } in
let c = ref y in
let lx : ref limb = ref 0 in
let i : ref int32 = ref 0 in
while not (Limb.(=) !c 0) do
invariant { 0 <= !i <= sz }
invariant { !i = sz -> !c = 0 }
invariant { !i > 0 -> 0 <= !c <= 1 }
invariant { value x !i + (power radix !i) * !c
= value ox !i + y }
invariant { forall j. !i <= j < sz ->
(pelts x)[x.offset + j] = (pelts ox)[x.offset + j] }
invariant { forall j. j < x.offset \/ x.offset + sz <= j ->
(pelts x)[j] = (pelts ox)[j] }
variant { sz - !i }
label StartLoop in
lx := get_ofs x !i;
assert { !lx = (pelts ox)[ox.offset + !i] };
let (res, carry) = add_with_carry !lx !c 0 in (*TODO*)
assert { res + radix * carry = !lx + !c }; (* TODO remove this *)
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sz) res;
set_ofs x !i res;
assert { forall j. !i < j < sz ->
(pelts x)[x.offset + j]
= (pelts ox)[x.offset + j] };
assert { value x !i + (power radix !i) * !c = value ox !i + y };
c := carry;
value_tail x !i;
value_tail ox !i;
assert { value x (!i+1) + power radix (!i+1) * !c =
value ox (!i+1) + y };
i := Int32.(+) !i 1;
assert { !i = sz -> !c = 0
by value x sz + power radix sz * !c = value ox sz + y
so value ox sz + y < power radix sz
so 0 <= !c <= 1};
done;
let c = ref (0:limb) in
let lx : ref limb = ref (C.get x) in
let i : ref int32 = ref 1 in
let res = Limb.add_mod !lx y in
C.set x res;
if (Limb.(<) res !lx)
then begin
c := 1;
assert { radix + res = !lx + y };
while not (Limb.(=) !c 0) do
invariant { 1 <= !i <= sz }
invariant { !i = sz -> !c = 0 }
invariant { 0 <= !c <= 1 }
invariant { value x !i + (power radix !i) * !c
= value ox !i + y }
invariant { forall j. !i <= j < sz ->
(pelts x)[x.offset + j] = (pelts ox)[x.offset + j] }
invariant { forall j. j < x.offset \/ x.offset + sz <= j ->
(pelts x)[j] = (pelts ox)[j] }
variant { sz - !i }
assert { !c = 1 };
lx := get_ofs x !i;
assert { !lx = (pelts ox)[ox.offset + !i] };
let res = Limb.add_mod !lx 1 in
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sz) res;
set_ofs x !i res;
assert { forall j. !i < j < sz ->
(pelts x)[x.offset + j]
= (pelts ox)[x.offset + j] };
assert { value x !i + (power radix !i) * !c = value ox !i + y };
value_tail x !i;
value_tail ox !i;
i := Int32.(+) !i 1;
if not (Limb.(=) res 0)
then begin
c := 0;
assert { res = !lx + 1 };
assert { value x !i = value ox !i + y };
break
end
else begin
assert { radix + res = !lx + 1 };
assert { value x !i + power radix !i = value ox !i + y };
end;
assert { !i = sz -> !c = 0
by value x sz + power radix sz * !c = value ox sz + y
so value ox sz + y < power radix sz
so 0 <= !c <= 1 };
done
end;
value_concat x !i sz;
value_concat ox !i sz;
assert { forall j. x.offset + !i <= j < x.offset + sz ->
......@@ -437,38 +473,52 @@ module Add
-> (pelts x)[j] = old (pelts x)[j] }
writes { x.data.elts }
= let ghost ox = { x } in
let c = ref y in
let lx = ref 0 in
let i = ref 0 in
while Int32.(<) !i sz && not (Limb.(=) !c 0) do
invariant { 0 <= !i <= sz }
invariant { !i > 0 -> 0 <= !c <= 1 }
invariant { value x !i + (power radix !i) * !c =
value ox !i + y }
invariant { forall j. (j < offset x \/ offset x + !i <= j)
-> (pelts x)[j] = old (pelts x)[j] }
variant { sz - !i }
label StartLoop in
lx := get_ofs x !i;
assert { !lx = (pelts ox)[offset ox + !i] };
let (res, carry) = add_with_carry !lx !c 0 in
assert { res + radix * carry = !lx + !c }; (* TODO remove this *)
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sz) res;
set_ofs x !i res;
assert { forall j. !i < j < sz ->
(pelts x)[x.offset + j]
= (pelts ox)[x.offset + j] };
assert { value x !i = value x !i at StartLoop };
assert { value x !i + (power radix !i) * !c = value ox !i + y };
c := carry;
value_tail x !i;
value_tail ox !i;
assert { value x (!i+1) + (power radix (!i+1)) * !c
= value ox (!i+1) + y };
i := Int32.(+) !i 1;
done;
let c = ref 0 in
let lx = ref (C.get x) in
let i = ref 1 in
let res = Limb.add_mod !lx y in
C.set x res;
if (Limb.(<) res !lx)
then begin
c := 1;
assert { radix + res = !lx + y };
while Int32.(<) !i sz do
invariant { 1 <= !i <= sz }
invariant { 0 <= !c <= 1 }
invariant { !c = 1 \/ !i = sz }
invariant { value x !i + (power radix !i) * !c =
value ox !i + y }
invariant { forall j. (j < offset x \/ offset x + !i <= j)
-> (pelts x)[j] = old (pelts x)[j] }
variant { sz - !i }
assert { !c = 1 };
lx := get_ofs x !i;
assert { !lx = (pelts ox)[offset ox + !i] };
let res = Limb.add_mod !lx 1 in
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sz) res;
set_ofs x !i res;
assert { forall j. !i < j < sz ->
(pelts x)[x.offset + j]
= (pelts ox)[x.offset + j] };
assert { value x !i + (power radix !i) * !c = value ox !i + y };
value_tail x !i;
value_tail ox !i;
i := Int32.(+) !i 1;
if not (Limb.(=) res 0)
then begin
c := 0;
assert { res = !lx + 1 };
assert { value x !i = value ox !i + y };
break
end
else begin
assert { radix + res = !lx + 1 };
assert { value x !i + power radix !i = value ox !i + y };
end;
done;
end;
value_concat x !i sz;
value_concat ox !i sz;
assert { forall j. x.offset + !i <= j < x.offset + sz ->
......
......@@ -11,173 +11,269 @@
<theory name="Add" proved="true">
<goal name="VC wmpn_add_1" expl="VC for wmpn_add_1" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC wmpn_add_1.0" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="20"/></proof>
<goal name="VC wmpn_add_1.0" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC wmpn_add_1.1" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="21"/></proof>
<goal name="VC wmpn_add_1.1" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="20"/></proof>
</goal>
<goal name="VC wmpn_add_1.2" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="11"/></proof>
<goal name="VC wmpn_add_1.2" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_add_1.3" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="21"/></proof>
</goal>
<goal name="VC wmpn_add_1.4" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="70"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC wmpn_add_1.5" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="25"/></proof>
</goal>
<goal name="VC wmpn_add_1.6" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="92"/></proof>
</goal>
<goal name="VC wmpn_add_1.7" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_add_1.6" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.91"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="49"/></proof>
<goal name="VC wmpn_add_1.8" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC wmpn_add_1.7" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="21"/></proof>
<goal name="VC wmpn_add_1.9" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="42"/></proof>
</goal>