Commit dd08bd4c authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

nearly there!

parent 481616e5
......@@ -93,8 +93,6 @@ S.init();
begin ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 = old(uint 4 reg 2 * uint 4 reg 6) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
mul r2 r8; (* a0*b2 *)
movw r12 r0;
mul r2 r6; (* a0*b0 *)
......@@ -193,8 +191,6 @@ 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 { ?tf = 0 <-> old((uint 4 reg 2 < uint 4 reg 18) <-> (uint 4 reg 6 < uint 4 reg 22)) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
label B in
(* subtract a0 a4 *)
......@@ -252,8 +248,6 @@ label Tmp in
begin ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18 = old (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* compute h (l4 l5 l6 l7) *)
mul r18 r22;
......@@ -336,6 +330,7 @@ ensures { valid_addr_space stack }
end;
S.init();
label Tmp2 in
begin ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = old (uint 4 reg 2*uint 4 reg 6) }
ensures { valid_addr_space reg }
......@@ -416,6 +411,7 @@ ensures { valid_addr_space reg }
end;
S.init();
label Tmp3 in
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 + ?cf*pow2 64 = old(uint 8 reg 10 + uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18) }
......@@ -435,18 +431,18 @@ label B in
end;
S.init();
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) + (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 = mod ((old ?cf) - ?cf) 256 \/ cor = pow2 32 + (old ?cf) - ?cf }
(*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 { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* process sign bit *)
label B in
......@@ -486,8 +482,11 @@ label B in
end;
S.init();
label Tmp5 in
begin ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf = old(?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*(uint 1 reg 26 + (pow2 8+pow2 16+pow2 24)*reg[0])) }
(*ensures { pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 = old(pow2 32 * ?cf + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + pow2 32*uint 6 reg 20 + pow2 80*uint 2 reg 2 + pow2 96*(uint 1 reg 26 + (pow2 8+pow2 16+pow2 24)*reg[0])) }*)
ensures { valid_addr_space reg }
(* add in m *)
......@@ -509,26 +508,178 @@ S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14();
S.modify_r28(); S.modify_r29(); S.modify_r18(); S.modify_r19();
end;
assert { 0 <= ((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 < pow2 128 };
assert { 0 <= (uint 4 reg 10 at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 < pow2 128 };
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) + (if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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) + (if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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) + (if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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) + (if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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) + (if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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) + (if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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) + (if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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) + (if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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) +
(if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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) +
(if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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)) +
(if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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)) +
(if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (uint 4 reg 6 - uint 4 reg 22)) at L11) +
pow2 64*(pow2 32)
};
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 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) +
(if !tf at Tmp5 then 1 else -1)*(abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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) +
(if !tf at Tmp5 then 1 else -1)*(abs (uint 4 reg 2 - uint 4 reg 18))*(abs (uint 4 reg 6 - uint 4 reg 22)) at L11 +
pow2 96
};
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) at L11 +
pow2 96
};
(*
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 at L11) + pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) +
pow2 32*(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) +
pow2 32*(if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (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 =
pow2 32*(uint 4 reg 10 at L11) + pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11) +
pow2 32*(pow2 32*(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22 at L11)) +
(if !tf at Tmp5 then 1 else -1)*((abs (uint 4 reg 2 - uint 4 reg 18))*(abs (uint 4 reg 6 - uint 4 reg 22)) at L11) +
pow2 96
};
*)
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
\/
((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)
};
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
};
(*
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;
......@@ -545,11 +696,11 @@ label Pre in
assert { uint 12 mem (uint 2 reg rZ+4) = (uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18) at Pre
};
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
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 16 mem (uint 2 reg rZ)
};
assert { uint 16 mem (uint 2 reg rZ) =
((( (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 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) ) at L11 =
old (uint 8 mem (uint 2 reg rX) * uint 8 mem (uint 2 reg rY))
};
assert { uint 16 mem (old (uint 2 reg rZ)) =
......
This diff is collapsed.
Supports Markdown
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