Skip to content

GitLab

Commit 16c1132c authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Clean up of model and proofs 

Inline pow2, remove a few proof asserts

Improved proof assertions (now depends less on things like reg54)

Remove or contract a few assertions, fixes slow xor assert verifications
parent 48af0fca
Expand all Hide whitespace changes
Inline Side-by-side
karatsuba64.mlw
View file @ 16c1132c
......@@ -5,13 +5,15 @@ use int.Int
use bv.Pow2int
use int.EuclideanDivision
lemma of_int_zeros: (of_int 0 = zeros)
lemma of_int_ones: (of_int 0xFF = ones)
lemma asr_0: (asr zeros 1) == zeros
lemma asr_1: (asr (of_int 1) 1) == zeros
lemma asr_f: (asr ones 1) == ones
lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w
lemma xor_1': forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) (of_int 0xFF)) = 255 - w
lemma or_0: forall w. bw_or zeros w = w
......@@ -60,6 +62,24 @@ lemma mul_bound_preserve:
meta rewrite_def function (!)
meta rewrite lemma pow2_128
meta rewrite lemma pow2_120
meta rewrite lemma pow2_112
meta rewrite lemma pow2_104
meta rewrite lemma pow2_96
meta rewrite lemma pow2_88
meta rewrite lemma pow2_80
meta rewrite lemma pow2_72
meta rewrite lemma pow2_64
meta rewrite lemma pow2_56
meta rewrite lemma pow2_48
meta rewrite lemma pow2_40
meta rewrite lemma pow2_32
meta rewrite lemma pow2_24
meta rewrite lemma pow2_16
meta rewrite lemma pow2_15
meta rewrite lemma pow2_8
let karatsuba64_marked()
requires { 32 <= uint 2 reg rX < pow2 15 }
requires { 32 <= uint 2 reg rY < pow2 15 }
......@@ -176,7 +196,7 @@ end;
ld_inc 18 rX;
ld_inc 19 rX;
ld_inc 20 rX;
ld_inc 21 rX ;
ld_inc 21 rX;
movw r26 r28;
std rZ 0 r10;
......@@ -189,10 +209,17 @@ S.init();
begin ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 2 = old (abs (uint 4 reg 2 - uint 4 reg 18)) }
ensures { uint 4 reg 6 = old (abs (uint 4 reg 6 - uint 4 reg 22)) }
ensures { not !tf <-> old((uint 4 reg 2 < uint 4 reg 18) <-> (uint 4 reg 6 < uint 4 reg 22)) }
ensures { (if !tf then -1 else 1)*(old ((abs (uint 4 reg 2 - uint 4 reg 18) * abs (uint 4 reg 6 - uint 4 reg 22)))) = old (uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22)
by (forall x y. x < 0 /\ y < 0 -> x*y > 0) /\
((old ((abs (uint 4 reg 2 - uint 4 reg 18) * abs (uint 4 reg 6 - uint 4 reg 22))) = (old (abs ((uint 4 reg 2 - uint 4 reg 18) * (uint 4 reg 6 - uint 4 reg 22))))) by (forall x y. abs x * abs y = abs (x*y))) }
ensures {
let oreg = old reg in
let a = uint 4 oreg 2 in
let b = uint 4 oreg 18 in
let c = uint 4 oreg 6 in
let d = uint 4 oreg 22 in
(if !tf then -1 else 1)*((abs (a - b) * abs (c - d))) = (a - b)*(c - d)
by (((abs (a - b) * abs (c - d)) = (abs ((a - b) * (c - d)))) by
(forall x y. x < 0 /\ y < 0 -> x*y > 0) /\
(forall x y. abs x * abs y = abs (x*y)))
/\ not !tf <-> ((a < b) <-> (c < d)) }
ensures { valid_addr_space reg }
label B in
......@@ -413,8 +440,6 @@ ensures { valid_addr_space reg }
S.modify_r20(); S.modify_r20(); S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25();
end;
assert { [@help] uint 8 reg 10 at L11 = uint 4 reg 2 * uint 4 reg 6 at L00};
S.init();
label Tmp3 in
begin
......@@ -440,22 +465,29 @@ label Tmp4 in
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) - ((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) by uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) + (if !tf then 1 else -1)*old(uint 6 reg 20 + pow2 48*uint 2 reg 2) }
(*ensures { let cor = reg[26] + (pow2 8 + pow2 16 + pow2 24)*reg[0] in cor = (old ?cf) - (1 - ?tf) \/ cor = pow2 32 + (old ?cf) - (1 - ?tf) }*)
ensures { let cor = reg[26] + (pow2 8 + pow2 16 + pow2 24)*reg[0] in cor = (old ?cf) - ?cf \/ cor = pow2 32 + (old ?cf) - ?cf }
(*
ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = (old ?cf) - ?cf + (if ?cf > old ?cf then pow2 32 else 0) }
*)
ensures { let cor = reg[26] + (pow2 8 + pow2 16 + pow2 24)*reg[0] in cor = (old ?cf) - ?cf \/ cor = pow2 32 + (old ?cf) - ?cf by
((old !cf) /\ not !tf -> reg[26] = 0)
/\
((old !cf) /\ !tf -> reg[26] = 1)
/\
(not (old !cf) /\ not !tf -> reg[26] = 0xFF)
/\
(not (old !cf) /\ !tf -> reg[26] = 0)
/\
(reg[26] = 0 -> reg[0] = 0)
/\
(reg[26] = 1 -> reg[0] = 0)
/\
(reg[26] = 0xFF -> reg[0] = 0xFF)
}
ensures { valid_addr_space reg }
(* process sign bit *)
label B in
assert { reg[27] = 0 };
bld r27 0;
assert { reg[27] = ?tf };
assert { reg[27] = ?tf by reg[27] at B = 0 };
dec 27;
assert { reg[27] = 0xFF*(1 - ?tf) by mod (- 1) 256 = 0xFF };
assert { reg[27] = 0xFF*(1 - ?tf) };
(* merge carry and borrow *)
adc r26 r27;
......@@ -465,21 +497,33 @@ assert { reg[27] = 0xFF*(1 - ?tf) by mod (- 1) 256 = 0xFF };
label B in
(* invert all bits or do nothing *)
eor r20 r27;
assert {(reg[20] = reg[20] at B /\ reg[27] = 0) \/ (reg[20] = 255 - reg[20] at B /\ reg[27] = 0xFF)};
eor r21 r27;
assert {(reg[21] = reg[21] at B /\ reg[27] = 0) \/ (reg[21] = 255 - reg[21] at B /\ reg[27] = 0xFF)};
eor r22 r27;
assert {(reg[22] = reg[22] at B /\ reg[27] = 0) \/ (reg[22] = 255 - reg[22] at B /\ reg[27] = 0xFF)};
eor r23 r27;
assert {(reg[23] = reg[23] at B /\ reg[27] = 0) \/ (reg[23] = 255 - reg[23] at B /\ reg[27] = 0xFF)};
eor r24 r27;
assert {(reg[24] = reg[24] at B /\ reg[27] = 0) \/ (reg[24] = 255 - reg[24] at B /\ reg[27] = 0xFF)};
eor r25 r27;
assert {(reg[25] = reg[25] at B /\ reg[27] = 0) \/ (reg[25] = 255 - reg[25] at B /\ reg[27] = 0xFF)};
eor r2 r27;
assert {(reg[2] = reg[2] at B /\ reg[27] = 0) \/ (reg[2] = 255 - reg[2] at B /\ reg[27] = 0xFF)};
eor r3 r27;
assert {(reg[3] = reg[3] at B /\ reg[27] = 0) \/ (reg[3] = 255 - reg[3] at B /\ reg[27] = 0xFF)};
assert {reg[27] = 0xFF -> (
reg[3] = 255 - reg[3] at B /\
reg[2] = 255 - reg[2] at B /\
reg[25] = 255 - reg[25] at B /\
reg[24] = 255 - reg[24] at B /\
reg[23] = 255 - reg[23] at B /\
reg[22] = 255 - reg[22] at B /\
reg[21] = 255 - reg[21] at B /\
reg[20] = 255 - reg[20] at B
)};
assert {reg[27] = 0 -> (
reg[3] = reg[3] at B /\
reg[2] = reg[2] at B /\
reg[25] = reg[25] at B /\
reg[24] = reg[24] at B /\
reg[23] = reg[23] at B /\
reg[22] = reg[22] at B /\
reg[21] = reg[21] at B /\
reg[20] = reg[20] at B
)};
label B in
add r27 r27; (* sets carry flag if r27 = 0xff *)
S.modify_r0(); S.modify_r26(); S.modify_r27();
......@@ -520,225 +564,31 @@ assert { 0 <= uint 4 reg 2 + pow2 32*uint 4 reg 18 at L11 <= pow2 64-1 };
assert { 0 <= uint 4 reg 6 + pow2 32*uint 4 reg 22 at L11 <= pow2 64-1 };
assert { 0 <= ((uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22)) at L11 <= (pow2 64-1)*(pow2 64-1) };
assert { (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) at Tmp = (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) at L11 };
assert { uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18 at Tmp2 = (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) at L11 };
assert { uint 4 reg 2 at Tmp2 = (abs (uint 4 reg 2 - uint 4 reg 18)) at L11 };
assert { uint 4 reg 6 at Tmp2 = (abs (uint 4 reg 6 - uint 4 reg 22)) at L11 };
assert { (uint 6 reg 20 + pow2 48*uint 2 reg 2) at Tmp3 = (abs (uint 4 reg 2 - uint 4 reg 18))*(abs (uint 4 reg 6 - uint 4 reg 22)) at L11 };
assert { uint 4 reg 10 at Tmp3 = uint 4 reg 10 at L11 };
assert { uint 8 reg 10 + ?cf*pow2 64 at Tmp4 = uint 4 reg 10 at L11 + pow2 32 * uint 4 reg 14 at Tmp2 + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) at L11 };
assert { uint 6 reg 20 + pow2 48*uint 2 reg 2 at Tmp5 = (?cf at Tmp5)*(pow2 64 - 1) - ((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) };
assert { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf + uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + uint 6 reg 20 + pow2 48*uint 2 reg 2 + pow2 64*(reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0])) at Tmp5 };
assert { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 8 reg 10 at Tmp4) + (pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 at Tmp2) + (uint 6 reg 20 + pow2 48*uint 2 reg 2 + pow2 64*(reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0])) at Tmp5 };
assert { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11 + pow2 32 * uint 4 reg 14 at Tmp2 + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) at L11 - ?cf*pow2 64 at Tmp4) + (pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 at Tmp2) + (uint 6 reg 20 + pow2 48*uint 2 reg 2 + pow2 64*(reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0])) at Tmp5 };
assert { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11 + pow2 32 * uint 4 reg 14 at Tmp2 + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) at L11 - ?cf*pow2 64 at Tmp4) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) - pow2 32 * uint 4 reg 14 at Tmp2) +
(uint 6 reg 20 + pow2 48*uint 2 reg 2 + pow2 64*(reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0])) at Tmp5 };
assert { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11 + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) at L11 - ?cf*pow2 64 at Tmp4) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) +
(uint 6 reg 20 + pow2 48*uint 2 reg 2 at Tmp5) +
(pow2 64*(reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0]) at Tmp5) };
assert { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11 + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) at L11 - ?cf*pow2 64 at Tmp4) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) +
(?cf at Tmp5)*(pow2 64 - 1) - ((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) +
(pow2 64*(reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0]) at Tmp5) };
(*
assert { let cor =reg[26] + (pow2 8 + pow2 16 + pow2 24)*reg[0] at Tmp5 in cor = (?cf at Tmp4) - (?cf at Tmp5) \/ cor = pow2 32 + (?cf at Tmp4) - (?cf at Tmp5) };
assert {
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11) + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) - (?cf*pow2 64 at Tmp4) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) +
(?cf at Tmp5)*(pow2 64 - 1) - ((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) +
pow2 64*((?cf at Tmp4) - (?cf at Tmp5))
\/
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11 + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) at L11 - ?cf*pow2 64 at Tmp4) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) +
(?cf at Tmp5)*(pow2 64 - 1) - ((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) +
pow2 64*(pow2 32 + (?cf at Tmp4) - (?cf at Tmp5))
};
assert {
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11) + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) - (?cf*pow2 64 at Tmp4) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) +
(?cf at Tmp5)*(pow2 64 - 1) - ((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) +
pow2 64*(?cf at Tmp4) - pow2 64*(?cf at Tmp5)
\/
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11 + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) at L11 - ?cf*pow2 64 at Tmp4) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) +
(?cf at Tmp5)*(pow2 64 - 1) - ((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) +
pow2 64*(pow2 32) + pow2 64*(?cf at Tmp4) - pow2 64*(?cf at Tmp5)
};
assert {
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11) + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) +
(?cf at Tmp5)*(pow2 64 - 1) - ((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) -
pow2 64*(?cf at Tmp5)
\/
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11) + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) +
(?cf at Tmp5)*(pow2 64 - 1) - ((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) +
pow2 64*(pow2 32) - pow2 64*(?cf at Tmp5)
};
assert {
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11) + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) -
(?cf at Tmp5) -
((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11)
\/
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(?cf at Tmp5) + (uint 4 reg 10 at L11) + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) -
(?cf at Tmp5) -
((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) +
pow2 64*(pow2 32)
};
assert {
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(uint 4 reg 10 at L11) + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) -
((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11)
\/
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
(uint 4 reg 10 at L11) + (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) -
((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11) +
pow2 64*(pow2 32)
};
assert {
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
uint 4 reg 10 + uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22)) -
(uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) at L11
\/
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
uint 4 reg 10 + uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22)) -
(uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22) +
pow2 96 at L11
};
assert {
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
uint 4 reg 10 + uint 4 reg 14 +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22)) -
uint 4 reg 2 * uint 4 reg 6 + uint 4 reg 2 * uint 4 reg 22 + uint 4 reg 18 * uint 4 reg 6 at L11
\/
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
uint 4 reg 10 + uint 4 reg 14 +
(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22)) -
uint 4 reg 2 * uint 4 reg 6 + uint 4 reg 2 * uint 4 reg 22 + uint 4 reg 18 * uint 4 reg 6 +
pow2 96 at L11
};
*)
assert {
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
uint 4 reg 10 +
uint 4 reg 14 -
uint 4 reg 2 * uint 4 reg 6 +
uint 4 reg 2 * uint 4 reg 22 +
uint 4 reg 18 * uint 4 reg 6 +
pow2 32*uint 4 reg 14 +
pow2 32*uint 4 reg 18*uint 4 reg 22 at L11
\/
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
uint 4 reg 10 +
uint 4 reg 14 -
uint 4 reg 2 * uint 4 reg 6 +
uint 4 reg 2 * uint 4 reg 22 +
uint 4 reg 18 * uint 4 reg 6 +
pow2 32*uint 4 reg 14 +
pow2 32*uint 4 reg 18*uint 4 reg 22 +
pow2 96 at L11
};
assert {
pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
pow2 32*uint 4 reg 10 +
pow2 32*uint 4 reg 14 -
pow2 32*uint 4 reg 2 * uint 4 reg 6 +
pow2 32*uint 4 reg 2 * uint 4 reg 22 +
pow2 32*uint 4 reg 18 * uint 4 reg 6 +
pow2 64*uint 4 reg 14 +
pow2 64*uint 4 reg 18*uint 4 reg 22 at L11
\/
pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
pow2 32*uint 4 reg 10 +
pow2 32*uint 4 reg 14 -
pow2 32*uint 4 reg 2 * uint 4 reg 6 +
pow2 32*uint 4 reg 2 * uint 4 reg 22 +
pow2 32*uint 4 reg 18 * uint 4 reg 6 +
pow2 64*uint 4 reg 14 +
pow2 64*uint 4 reg 18*uint 4 reg 22 +
pow2 128 at L11
};
(*
assert {
uint 4 reg 10 +
pow2 32*uint 4 reg 10 +
pow2 32*uint 4 reg 14 -
pow2 32*uint 4 reg 2 * uint 4 reg 6 +
pow2 32*uint 4 reg 2 * uint 4 reg 22 +
pow2 32*uint 4 reg 18 * uint 4 reg 6 +
pow2 64*uint 4 reg 14 +
pow2 64*uint 4 reg 18*uint 4 reg 22 at L11
=
(uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) at L11
};
*)
assert {uint 8 reg 10 at L11 = uint 4 reg 2 * uint 4 reg 6 at L00};
assert {uint 8 reg 10 at L11 = uint 4 reg 2 * uint 4 reg 6 at L11};
assert {
(uint 4 reg 10 at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) ) at L11
\/
(uint 4 reg 10 at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) ) at L11
+ pow2 128
};
assert { (uint 4 reg 10 at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18
= ( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) ) at L11
(* by
uint 8 reg 10 at L11 = uint 4 reg 2 * uint 4 reg 6 at L11
/\ (
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
uint 4 reg 10 +
uint 4 reg 14 -
uint 4 reg 2 * uint 4 reg 6 +
uint 4 reg 2 * uint 4 reg 22 +
uint 4 reg 18 * uint 4 reg 6 +
pow2 32*uint 4 reg 14 +
pow2 32*uint 4 reg 18*uint 4 reg 22 at L11
\/
uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf =
uint 4 reg 10 +
uint 4 reg 14 -
uint 4 reg 2 * uint 4 reg 6 +
uint 4 reg 2 * uint 4 reg 22 +
uint 4 reg 18 * uint 4 reg 6 +
pow2 32*uint 4 reg 14 +
pow2 32*uint 4 reg 18*uint 4 reg 22 +
pow2 96 at L11)*)
};
(*
assert {
(uint 4 reg 10 at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) ) at L11
\/
(uint 4 reg 10 at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) ) at L11
+ pow2 128
};
*)
label Pre in
std rZ 4 r10;
std rZ 5 r11;
......
karatsuba64/why3session.xml
View file @ 16c1132c
This diff is collapsed.
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