Commit 16b1f0f4 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

remove old abandoned attempts

parent de64bfd8
......@@ -27,9 +27,6 @@ use import bv.Pow2int
lemma register_file_invariant_strengthen:
forall m: map int int. (forall i. 0 <= m[i] < 256) -> (forall i j. 0 <= m[i]*m[j] <= 255*255)
goal mul_postcondition_strengthen:
forall x y. 0 <= x < 256 -> 0 <= y < 256 -> div (x*y) 256 < 255
lemma pow_split: forall k. k >= 0 -> pow2 (2*k) = pow2 k*pow2 k
end
......@@ -62,8 +59,7 @@ let mul16 (): unit
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r23;
()
adc r15 r23
let mul24_flat (): unit
ensures { uint 6 reg 12 = old (uint 3 reg 2 * uint 3 reg 7) }
......@@ -110,384 +106,6 @@ let mul24_flat (): unit
adc r16 r1;
adc r17 r25
let mul24_new_new (): unit
ensures { uint 6 reg 12 = old (uint 3 reg 2 * uint 3 reg 7) }
= 'S:
abstract
ensures { uint 4 reg 12 = old(reg[2] * uint 3 reg 7) }
ensures { reg[23] = 0 }
ensures { eq 3 reg (at reg 'S) 2 }
ensures { eq 3 reg (at reg 'S) 7 }
'B:
clr r23;
mul r2 r9;
movw r14 r0;
mul r2 r7;
movw r12 r0;
mul r2 r8;
add r13 r0;
adc r14 r1;
adc r15 r23;
end;
abstract
ensures { uint 5 reg 12 = old (uint 4 reg 12) + at(pow2 8*reg[3]*uint 3 reg 7)'S }
ensures { reg[23] = 0 }
ensures { eq 3 reg (at reg 'S) 2 }
ensures { eq 3 reg (at reg 'S) 7 }
'B:
clr r16;
mul r3 r9;
movw r24 r0;
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r24;
adc r25 r23;
mul r3 r8;
add r14 r0;
adc r15 r1;
adc r16 r25;
assert { uint 4 reg 13 = at(uint 3 reg 13)'B + at(reg[3]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B
= at(uint 3 reg 13)'B + at(reg[3]*uint 3 reg 7)'S };
end;
abstract
ensures { uint 6 reg 12 = old (uint 5 reg 12) + at(pow2 16 * reg[4] * uint 3 reg 7)'S }
ensures { eq 3 reg (at reg 'S) 2 }
ensures { eq 3 reg (at reg 'S) 7 }
'B:
clr r17;
mul r4 r9;
movw r24 r0;
mul r4 r7;
add r14 r0;
adc r15 r1;
adc r16 r24;
adc r25 r23;
mul r4 r8;
add r15 r0;
adc r16 r1;
adc r17 r25;
assert { uint 4 reg 14 = at(uint 3 reg 14)'B + at(reg[4]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B
= at(uint 3 reg 14)'B + at(reg[4]*uint 3 reg 7)'S };
end;
()
let mul24_new (): unit
ensures { uint 6 reg 12 = old (uint 3 reg 2 * uint 3 reg 7) }
= 'S:
abstract
ensures { uint 4 reg 12 = old(reg[2] * uint 3 reg 7) }
ensures { reg[23] = 0 }
ensures { eq 3 reg (at reg 'S) 2 }
ensures { eq 3 reg (at reg 'S) 7 }
'B:
clr r23;
mul r2 r9;
movw r14 r0;
mul r2 r7;
movw r12 r0;
mul r2 r8;
add r13 r0;
adc r14 r1;
adc r15 r23;
end;
abstract
ensures { uint 5 reg 12 = old (uint 4 reg 12) + at(pow2 8*reg[3]*uint 3 reg 7)'S }
ensures { reg[23] = 0 }
ensures { eq 3 reg (at reg 'S) 2 }
ensures { eq 3 reg (at reg 'S) 7 }
'B:
clr r16;
mul r3 r9;
movw r24 r0;
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r24;
adc r25 r23;
mul r3 r8;
add r14 r0;
adc r15 r1;
adc r16 r25;
assert { uint 4 reg 13 + ?cf*pow2 32 = at(uint 3 reg 13)'B + at(reg[3]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B
<= at(uint 3 reg 13)'B + at(255*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B };
(*
check { uint 4 reg 13 + ?cf * pow2 32 = at(uint 3 reg 13 + reg[3]*uint 3 reg 7)'B <= at(uint 3 reg 13 + 255*uint 3 reg 7)'B < pow2 32 };
check { uint 4 reg 13 + ?cf * pow2 32 = at(uint 3 reg 13 + reg[3]*uint 3 reg 7)'B <= at(uint 3 reg 13 + 255*uint 3 reg 7)'B };
check { uint 4 reg 13 + ?cf * pow2 32 = at(uint 3 reg 13 + reg[3]*uint 3 reg 7)'B < pow2 32 };
*)
assert { uint 4 reg 13 = at(uint 3 reg 13)'B + at(reg[3]*uint 3 reg 7)'B
= at(uint 3 reg 13)'B + at(reg[3]*uint 3 reg 7)'S };
end;
abstract
ensures { uint 6 reg 12 = old (uint 5 reg 12) + at(pow2 16 * reg[4] * uint 3 reg 7)'S }
ensures { eq 3 reg (at reg 'S) 2 }
ensures { eq 3 reg (at reg 'S) 7 }
'B:
clr r17;
mul r4 r9;
movw r24 r0;
mul r4 r7;
add r14 r0;
adc r15 r1;
adc r16 r24;
adc r25 r23;
mul r4 r8;
add r15 r0;
adc r16 r1;
adc r17 r25;
assert { uint 4 reg 14 + ?cf*pow2 32 = at(uint 3 reg 14 + reg[4]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B
<= at(uint 3 reg 14 + 255*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B };
assert { uint 4 reg 14 = at(uint 3 reg 14)'B + at(reg[4]*uint 3 reg 7)'B
= at(uint 3 reg 14)'B + at(reg[4]*uint 3 reg 7)'S };
end;
(*
check { uint 6 reg 12 = at((reg[2] + pow2 8*reg[3] + pow2 16*reg[4])*uint 3 reg 7) 'S };
*)
()
let mul24 (): unit
ensures { uint 6 reg 12 = old (uint 3 reg 2 * uint 3 reg 7) }
= 'S:
abstract
ensures { uint 4 reg 12 = old(reg[2] * uint 3 reg 7) }
ensures { reg[23] = 0 }
ensures { eq 3 reg (at reg 'S) 2 }
ensures { eq 3 reg (at reg 'S) 7 }
'B:
clr r23;
mul r2 r9;
movw r14 r0;
mul r2 r7;
movw r12 r0;
mul r2 r8;
add r13 r0;
adc r14 r1;
adc r15 r23;
end;
abstract
ensures { uint 5 reg 12 = old (uint 4 reg 12) + old(pow2 8*reg[3]*uint 3 reg 7) }
ensures { reg[23] = 0 }
ensures { eq 3 reg (at reg 'S) 2 }
ensures { eq 3 reg (at reg 'S) 7 }
'B:
clr r16;
mul r3 r9;
movw r24 r0;
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r24;
adc r25 r23;
mul r3 r8;
add r14 r0;
adc r15 r1;
adc r16 r25;
assert { uint 4 reg 13 + ?cf*pow2 32 = at(uint 3 reg 13)'B + at(reg[3]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B
<= at(uint 3 reg 13)'B + at(255*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B };
(*
check { uint 4 reg 13 + ?cf * pow2 32 = at(uint 3 reg 13 + reg[3]*uint 3 reg 7)'B <= at(uint 3 reg 13 + 255*uint 3 reg 7)'B < pow2 32 };
check { uint 4 reg 13 + ?cf * pow2 32 = at(uint 3 reg 13 + reg[3]*uint 3 reg 7)'B <= at(uint 3 reg 13 + 255*uint 3 reg 7)'B };
check { uint 4 reg 13 + ?cf * pow2 32 = at(uint 3 reg 13 + reg[3]*uint 3 reg 7)'B < pow2 32 };
*)
assert { uint 4 reg 13 = at(uint 3 reg 13)'B + at(reg[3]*uint 3 reg 7)'B };
end;
abstract
ensures { uint 6 reg 12 = old (uint 5 reg 12) + old(pow2 16 * reg[4] * uint 3 reg 7) }
ensures { eq 3 reg (at reg 'S) 2 }
ensures { eq 3 reg (at reg 'S) 7 }
'B:
clr r17;
mul r4 r9;
movw r24 r0;
mul r4 r7;
add r14 r0;
adc r15 r1;
adc r16 r24;
adc r25 r23;
mul r4 r8;
add r15 r0;
adc r16 r1;
adc r17 r25;
assert { uint 4 reg 14 + ?cf*pow2 32 = at(uint 3 reg 14 + reg[4]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B
<= at(uint 3 reg 14 + 255*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B };
assert { uint 4 reg 14 = at(uint 3 reg 14 + reg[4]*uint 3 reg 7)'B };
end;
assert { uint 6 reg 12 = at((reg[2] + pow2 8*reg[3] + pow2 16*reg[4])*uint 3 reg 7) 'S };
()
let mul32_orig(): unit
ensures { uint 8 reg 12 = old (uint 4 reg 2 * uint 4 reg 7) }
= 'S:
abstract
ensures { uint 4 reg 12 = at(reg[2] * uint 3 reg 7)'S }
ensures { reg[23] = 0 }
ensures { eq 4 reg (at reg 'S) 2 }
ensures { eq 4 reg (at reg 'S) 7 }
'B:
clr r23;
mul r2 r9;
movw r14 r0;
mul r2 r7;
movw r12 r0;
mul r2 r8;
add r13 r0;
adc r14 r1;
adc r15 r23;
end;
abstract
ensures { uint 7 reg 12 = old(uint 4 reg 12) + at(pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 32*reg[10]) + reg[4]*pow2 40*reg[10])'S }
ensures { reg[23] = 0 }
ensures { eq 4 reg (at reg 'S) 2 }
ensures { eq 4 reg (at reg 'S) 7 }
'B:
(* !! *)
check { pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8]) <= pow2 24*255*255 + 255*(pow2 8*255 + pow2 16*255) };
mul r3 r10;
movw r16 r0;
check { uint 6 reg 12 = at(uint 4 reg 12 + pow2 32*reg[3]*reg[10])'B };
clr r18;
check { uint 7 reg 12 = at(uint 4 reg 12 + pow2 32*reg[3]*reg[10])'B };
mul r2 r10;
movw r24 r0;
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r24;
adc r25 r23;
check { uint 7 reg 12 + pow2 32*reg[25] = at(uint 4 reg 12 + pow2 8*reg[3]*reg[7] + pow2 24*reg[2]*reg[10] + pow2 32*reg[3]*reg[10])'B };
check { uint 7 reg 12 + pow2 32*reg[25] = at(uint 4 reg 12 + pow2 8*reg[3]*reg[7] + pow2 24*reg[2]*reg[10] + pow2 32*reg[3]*reg[10])'B };
mul r3 r8;
add r14 r0;
adc r15 r1;
adc r25 r23;
check { uint 7 reg 12 + pow2 32*reg[25] + ?cf*pow2 40 = at(uint 4 reg 12 + pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 32*reg[10]))'B
<= at(uint 4 reg 12 + pow2 24*255*reg[10] + 255*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 32*reg[10]))'B
= at(uint 4 reg 12 + 255*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 24*reg[10] + pow2 32*reg[10]))'B
= at(uint 4 reg 12 + 255*pow2 8*(reg[7] + pow2 8*reg[8] + pow2 16*reg[10] + pow2 24*reg[10]))'B
< at(uint 4 reg 12 + 255*pow2 40)'B
};
check { uint 4 reg 12 + pow2 32*reg[25] + ?cf*pow2 40 = at(uint 4 reg 12 + pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8]))'B
<= at(uint 4 reg 12 + pow2 24*255*reg[10] + 255*(pow2 8*reg[7] + pow2 16*reg[8]))'B
};
check { uint 7 reg 12 + pow2 32*reg[25] = at(uint 4 reg 12 + pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 32*reg[10]))'B };
mul r4 r10;
add r16 r25;
adc r17 r0;
adc r18 r1;
assert { uint 7 reg 12 = at(uint 4 reg 12 + pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 32*reg[10]) + reg[4]*pow2 40*reg[10])'B }
end;
abstract
ensures { uint 8 reg 12 + ?cf*pow2 64 = old(uint 7 reg 12) + at(pow2 24*reg[5]*uint 4 reg 7 + pow2 16*reg[4]*uint 3 reg 7 + pow2 24*reg[3]*reg[9])'S }
ensures { eq 4 reg (at reg 'S) 2 }
ensures { eq 4 reg (at reg 'S) 7 }
'B:
(* !! *)
check { at(reg[4]*reg[7] + reg[4]*pow2 16*reg[9] + pow2 8*reg[3]*reg[9])'B <= 255*255 + 255*pow2 16*255 + pow2 8*255*255 };
check { at(pow2 8*reg[5]*reg[8] + reg[4]*reg[8] + reg[5]*reg[7])'B <= pow2 8*255*255 + 255*255 + 255*255 };
assert { at(pow2 24*reg[5]*uint 4 reg 7 + pow2 16*reg[4]*uint 3 reg 7 + pow2 24*reg[3]*reg[9])'B = at(pow2 24*reg[5]*uint 4 reg 7 + pow2 16*reg[4]*uint 3 reg 7 + pow2 24*reg[3]*reg[9])'S };
clr r19;
mul r4 r9;
movw r24 r0;
mul r4 r7;
add r14 r0;
adc r15 r1;
check { uint 2 reg 14 + ?cf*pow2 16 = at(uint 2 reg 14 + reg[4]*reg[7])'B };
(* check { uint 4 reg 12 + ?cf*pow2 32 = at(uint 4 reg 12 + pow2 16*reg[4]*reg[7])'B }; *)
adc r16 r24;
adc r25 r23;
mul r3 r9;
add r15 r0;
adc r16 r1;
adc r25 r23;
(* ! *)
check { uint 3 reg 14 + reg[25]*pow2 24 + ?cf*pow2 32 = at(uint 3 reg 14 + reg[4]*reg[7] + reg[4]*pow2 16*reg[9] + pow2 8*reg[3]*reg[9])'B
<= at(uint 3 reg 14 + 255*255 + 255*pow2 16*255 + pow2 8*255*255)'B };
check { ?cf = 0 };
check { uint 3 reg 14 + reg[25]*pow2 24 = at(uint 3 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9])'B };
check { uint 4 reg 14 + reg[25]*pow2 24 = at(uint 4 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9])'B };
mul r5 r10;
add r17 r25;
check { uint 4 reg 14 + ?cf * pow2 32 = at(uint 4 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9])'B };
check { uint 5 reg 14 + ?cf * pow2 32 = at(uint 5 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9])'B };
check { uint 6 reg 14 + ?cf * pow2 32 = at(uint 5 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9])'B };
adc r18 r0;
adc r19 r1;
check { uint 6 reg 14 + ?cf * pow2 48 = at(uint 5 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 32*reg[5]*reg[10])'B };
'X:
mul r5 r8;
movw r24 r0;
mul r4 r8;
add r15 r0;
adc r24 r1;
adc r25 r23;
check { uint 6 reg 14 + pow2 16*uint 2 reg 24 = at(uint 5 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 32*reg[5]*reg[10] + pow2 16*reg[5]*reg[8] + pow2 8*reg[4]*reg[8])'B };
check { reg[15] + pow2 8*uint 2 reg 24 + ?cf*pow2 24 = at(reg[15])'X + at(pow2 8*reg[5]*reg[8] + reg[4]*reg[8])'B };
mul r5 r7;
add r15 r0;
adc r24 r1;
adc r25 r23;
check { uint 6 reg 14 + pow2 16*uint 2 reg 24 + ?cf*pow2 32 = at(uint 5 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 32*reg[5]*reg[10] + pow2 16*reg[5]*reg[8] + pow2 8*reg[4]*reg[8] + pow2 8*reg[5]*reg[7])'B };
(* ! *)
check { reg[15] + pow2 8*uint 2 reg 24 + ?cf*pow2 24 = at(reg[15])'X + at(pow2 8*reg[5]*reg[8] + reg[4]*reg[8] + reg[5]*reg[7])'B
<= 255 + pow2 8*255*255 + 255*255 + 255*255
};
check { uint 6 reg 14 + pow2 16*uint 2 reg 24 = at(uint 5 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 32*reg[5]*reg[10] + pow2 16*reg[5]*reg[8] + pow2 8*reg[4]*reg[8] + pow2 8*reg[5]*reg[7])'B };
check { ?cf = 0 };
(* 'Y: *)
mul r5 r9;
add r16 r24;
adc r0 r25;
adc r1 r23;
check { ? cf = 0 };
add r17 r0;
adc r18 r1;
adc r19 r23;
(* check { uint 4 reg 16 + ?cf*pow2 32 = at(uint 4 reg 16)'Y + pow2 8*reg[5]*reg[9] + at(uint 2 reg 24)'Y }; *)
assert { uint 6 reg 14 + ?cf*pow2 48
= at(uint 5 reg 14 + pow2 24*reg[5]*reg[9] + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 32*reg[5]*reg[10] + pow2 16*reg[5]*reg[8] + pow2 8*reg[4]*reg[8] + pow2 8*reg[5]*reg[7])'B
(*= at(uint 5 reg 14 + pow2 8*pow2 16*reg[5]*reg[9] + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 24*pow2 8*reg[5]*reg[10] + pow2 8*pow2 8*reg[5]*reg[8] + pow2 8*reg[4]*reg[8] + pow2 8*reg[5]*reg[7])'B
= at(uint 5 reg 14 + pow2 8*reg[5]*(pow2 16*reg[9] + pow2 24*reg[10] + pow2 8*reg[8] + reg[7]) + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 8*reg[4]*reg[8])'B
= at(uint 5 reg 14 + pow2 8*reg[5]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9] + pow2 24*reg[10]) + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 8*reg[4]*reg[8])'B
= at(uint 5 reg 14 + pow2 8*reg[5]*uint 4 reg 7 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 8*reg[4]*reg[8])'B
= at(uint 5 reg 14 + pow2 8*reg[5]*uint 4 reg 7 + reg[4]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]) + pow2 8*reg[3]*reg[9])'B *)
= at(uint 5 reg 14 + pow2 8*reg[5]*uint 4 reg 7 + reg[4]*uint 3 reg 7 + pow2 8*reg[3]*reg[9])'B };
check { uint 6 reg 14 + ?cf*pow2 48 = at(uint 5 reg 14 + pow2 8*reg[5]*uint 4 reg 7 + reg[4]*uint 3 reg 7 + pow2 8*reg[3]*reg[9])'B };
assert { uint 8 reg 12 + ?cf*pow2 64 = at(uint 7 reg 12 + pow2 24*reg[5]*uint 4 reg 7 + pow2 16*reg[4]*uint 3 reg 7 + pow2 24*reg[3]*reg[9])'B };
end;
assert { at(0 <= uint 4 reg 2 < pow2 32)'S };
assert { at(0 <= uint 4 reg 7 < pow2 32)'S };
assert { uint 8 reg 12 + ?cf*pow2 64 = at (uint 4 reg 2 * uint 4 reg 7)'S < pow2 32 * pow2 32 };
()
let mul32_flat(): unit
ensures { uint 8 reg 12 = old (uint 4 reg 2 * uint 4 reg 7) }
=
......@@ -762,8 +380,7 @@ let mul40_flat(): unit
mul r6 r11;
add r19 r25;
adc r20 r0;
adc r21 r1;
()
adc r21 r1
let mul48 (): unit
ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) }
......@@ -920,7 +537,6 @@ ensures { eq 6 reg (at reg 'S) 8 }
adc r24 r0;
adc r25 r1;
(* assert { uint 9 reg 17 = at(uint 9 reg 17 + uint 3 reg 5*uint 6 reg 8)'B }; *)
()
end
let mul48_flat (): unit
......@@ -1063,8 +679,7 @@ assert { pow2 96 = 0x1000000000000000000000000 };
add r22 r26;
adc r23 r27;
adc r24 r0;
adc r25 r1;
()
adc r25 r1
use import int.Abs
......@@ -1345,12 +960,14 @@ end;
adc r21 r0;
adc r22 r0;
(* the following 5 asserts re-state some trivial facts *)
assert { at(uint 3 reg 2)'L00 = at(uint 3 reg 2)'L11 };
assert { at(uint 3 reg 5)'L00 = at(uint 3 reg 5)'L11 };
assert { at(uint 3 reg 2*uint 3 reg 5)'L00 = at(uint 3 reg 2*uint 3 reg 5)'L11 };
assert { at((uint 3 reg 2 + pow2 24*uint 3 reg 14))'L11 = at(uint 6 mem (uint 2 reg rX))'S };
assert { at((uint 3 reg 5 + pow2 24*uint 3 reg 17))'L11 = at(uint 6 mem (uint 2 reg rY))'S };
(* the following 3 asserts establish a bounds result about multiplying uint's -- can't this be put in a lemma? *)
assert { 0 <= at((uint 3 reg 2 + pow2 24*uint 3 reg 14))'L11 <= pow2 48-1 };
assert { 0 <= at((uint 3 reg 5 + pow2 24*uint 3 reg 17))'L11 <= pow2 48-1 };
assert { 0 <= at((uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17))'L11 <= (pow2 48-1)*(pow2 48-1) };
......@@ -1366,7 +983,6 @@ assert { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 +
std rZ 8 r13;
std rZ 9 r20;
std rZ 10 r21;
std rZ 11 r22;
()
std rZ 11 r22
end
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