merged avr_code22 into karatsuba48/64

karatsuba48.mlw

@@ -137,8 +137,6 @@ end;
   std rZ 1 r9;
   std rZ 2 r10;
 '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 };
 
 S.init();
 abstract
@@ -282,15 +280,12 @@ end;
 (* S.init(); *)
 abstract
 ensures { S.synchronized S.shadow reg }
-ensures { old(uint 3 reg 8) + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 72 = (pow2 24+1)*(at(uint 3 reg 2*uint 3 reg 5)'L00 + at(pow2 24*uint 3 reg 14*uint 3 reg 17)'L11) }
-ensures { reg[26] = 0xFF -> uint 6 reg 14 = at((uint 3 reg 2 - uint 3 reg 14)*(uint 3 reg 5 - uint 3 reg 17))'L11 }
-ensures { reg[26] = 0x00 -> uint 6 reg 14 = -at((uint 3 reg 2 - uint 3 reg 14)*(uint 3 reg 5 - uint 3 reg 17))'L11 }
-ensures { reg[26] = 0x00 \/ reg[26] = 0xFF }
+ensures { uint 6 reg 8 + pow2 48*uint 3 reg 20 + ?cf*pow2 48 = old (uint 6 reg 8 + pow2 48*uint 3 reg 20 + uint 3 reg 11 + pow2 24*uint 3 reg 20) }
+ensures { reg[26] = if old(reg[26] = reg[27]) then 0xFF else 0x00 }
 'Pre:
 (*  ;--- process sign bit --- *)
   eor r26 r27;
   com r26;
-assert { reg[26] = 0xFF <-> at((uint 3 reg 2 < uint 3 reg 14) <-> (uint 3 reg 5 < uint 3 reg 17))'L11 };
  (* ;--- add l3+h0 to l0 and h3 --- *)
   add r8 r11;
   adc r9 r12;
@@ -298,7 +293,6 @@ assert { reg[26] = 0xFF <-> at((uint 3 reg 2 < uint 3 reg 14) <-> (uint 3 reg 5
   adc r11 r20;
   adc r12 r21;
   adc r13 r22;
-assert { uint 6 reg 8 + pow2 48*uint 3 reg 20 + ?cf*pow2 48 = at (uint 6 reg 8 + pow2 48*uint 3 reg 20 + uint 3 reg 11 + pow2 24*uint 3 reg 20)'Pre };
   S.modify_r26();
   S.modify_r8(); S.modify_r9(); S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13();
 end;
@@ -306,7 +300,7 @@ end;
 (* S.init(); *)
 abstract
 ensures { S.synchronized S.shadow reg }
-ensures { uint 6 reg 14 = ?cf*(pow2 48 - 1) - at((uint 3 reg 2 - uint 3 reg 14)*(uint 3 reg 5 - uint 3 reg 17))'L11 }
+ensures { uint 6 reg 14 = ?cf*(pow2 48 - 1) + (if old (reg[26] = 0xFF) then -1 else 1)*old(uint 6 reg 14) }
 ensures { let cor = reg[23] + (pow2 8+pow2 16)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 24 + old ?cf - ?cf }
 (*  ; merge carry and borrow *)
   adc r23 r26;
@@ -327,6 +321,8 @@ ensures { let cor = reg[23] + (pow2 8+pow2 16)*reg[0] in cor = old ?cf - ?cf \/
   S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19();
 end;
 (*  ; add in M *)
+abstract ensures { S.synchronized S.shadow reg }
+ensures { uint 6 reg 8 + pow2 48*uint 3 reg 20 + ?cf*pow2 72 = old(?cf + uint 6 reg 8 + pow2 48*uint 3 reg 20 + uint 6 reg 14 + pow2 48*(reg[23] + (pow2 8+pow2 16)*reg[0])) }
   adc  r8 r14;
   adc  r9 r15;
   adc r10 r16;
@@ -337,15 +333,36 @@ end;
   adc r20 r23;
   adc r21 r0;
   adc r22 r0;
+S.modify_r8(); S.modify_r9(); S.modify_r10();
+S.modify_r11(); S.modify_r12(); S.modify_r13();
+S.modify_r20(); S.modify_r21(); S.modify_r22();
+end;
 
-(* the following 3 asserts establish a bounds result about multiplying uint's -- can't this be put in a lemma? *)
+(* the following 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) };
 
-assert {   at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
+assert { 0 <= at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 < pow2 96 };
+
+(* these checks can be useful in debugging when porting to a new version, but are not needed at the moment if we
+   add the above assert, which is much simpler to comprehend *)
+
+(*
+check {   at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
+         = at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11 \/
+           at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
+         = at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11 + pow2 96
+       };
+
+check {   at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20
+         = at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11
+       };
+
+check {   at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
          = at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11 + ?cf*pow2 96
        };
+*)
 
   std rZ 3 r8;
   std rZ 4 r9;

karatsuba64.mlw

@@ -55,7 +55,7 @@ use avrmodel.Shadow as S
 lemma mul_bound_preserve:
   forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l
 
-let karatsuba64_marked() 
+let karatsuba64_marked()
   requires { 32 <= uint 2 reg rX < pow2 15 }
   requires { 32 <= uint 2 reg rY < pow2 15 }
   requires { 32 <= uint 2 reg rZ < pow2 15 }
@@ -173,14 +173,11 @@ end;
   std rZ 3 r13;
 
 'L11:
-assert { at(uint 4 reg 2*uint 4 reg 6)'L00 = at(uint 4 reg 2*uint 4 reg 6)'L11 };
-assert { at(uint 4 reg 2 + pow2 32*uint 4 reg 18)'L11 = at(uint 8 mem (uint 2 reg rX))'S };
-
 S.init();
 abstract 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 { ?tf = 0 <-> at((uint 4 reg 2 < uint 4 reg 18) <-> (uint 4 reg 6 < uint 4 reg 22))'L11 }
+ensures { ?tf = 0 <-> old((uint 4 reg 2 < uint 4 reg 18) <-> (uint 4 reg 6 < uint 4 reg 22)) }
 
 'B:
  (*    subtract a0 a4      *)
@@ -305,7 +302,7 @@ ensures { uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18 = old (u
   adc r19 r1;
 
   S.modify_r0(); S.modify_r1();
-  S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19(); 
+  S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19();
   S.modify_r28(); S.modify_r29();
 end;
 
@@ -391,7 +388,7 @@ end;
 S.init();
 abstract
 ensures { S.synchronized S.shadow reg }
-ensures { old(uint 4 reg 10) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf*pow2 96 = (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*uint 4 reg 18*uint 4 reg 22)'L11) }
+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) }
  (*    add l4 h0 to l0 and h4    *)
 'B:
   add r10 r14;
@@ -402,23 +399,27 @@ ensures { old(uint 4 reg 10) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + p
   adc r15 r29;
   adc r16 r18;
   adc r17 r19;
-assert { uint 8 reg 10 + ?cf*pow2 64 
-         = at(uint 8 reg 10 + uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18) 'B };
  (* store carrrY in r26 *)
   S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
 end;
+'CC:
 
 (* TODO optimise me *)
 S.init();
 abstract
 ensures { S.synchronized S.shadow reg }
+ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) + (if ?tf = 0 then -1 else 1)*old(uint 6 reg 20 + pow2 48*uint 2 reg 2) }
+(*
 ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) - at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11 }
+ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = ?cf*(1-old ?cf)*pow2 32 + old ?cf - ?cf }
+*)
 ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 32 + old ?cf - ?cf }
+
  (*    process sign bit      *)
 'B:
   bld r27 0;
   dec 27;
- assert { reg[27] = 0xFF*(1 - ?tf) };
+assert { reg[27] = 0xFF*(1 - ?tf) };
 
  (* merge carry and borrow *)
   adc r26 r27;
@@ -435,17 +436,21 @@ ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = old ?cf -
   eor r25 r27;
   eor r2  r27;
   eor r3  r27;
- (* decide *)
- assert { reg[27] = 0x00 -> uint 6 reg 20 + pow2 48*uint 2 reg 2 = at(uint 6 reg 20 + pow2 48*uint 2 reg 2)'B };
- assert { reg[27] = 0xFF -> uint 6 reg 20 + pow2 48*uint 2 reg 2 = pow2 64 - 1 - at(uint 6 reg 20 + pow2 48*uint 2 reg 2)'B };
 'B:
   add r27 r27; (* sets carry flag if r27 = 0xff *)
- assert { ?cf = 1 - ?tf };
   S.modify_r0(); S.modify_r26(); S.modify_r27();
   S.modify_r2(); S.modify_r3();
   S.modify_r20(); S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25();
 end;
+(*
+'DD:
+check { "expl:temp"
+at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + at ?cf 'CC *pow2 96 = (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*uint 4 reg 18*uint 4 reg 22)'L11) };
+*)
 
+S.init();
+abstract 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])) }
  (* add in m *)
   adc r10 r20;
   adc r11 r21;
@@ -461,14 +466,42 @@ end;
   adc r29 r0;
   adc r18 r0;
   adc r19 r0;
+S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
+S.modify_r28(); S.modify_r29(); S.modify_r18(); S.modify_r19();
+end;
+(*
+assert { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf = at(?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]))'DD };
+check {
+at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11
+= (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*uint 4 reg 18*uint 4 reg 22)'L11) - pow2 32*at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11
+};
+check {
+at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 = (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*uint 4 reg 18*uint 4 reg 22)'L11) - pow2 32*at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11
+\/
+at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 = (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*uint 4 reg 18*uint 4 reg 22)'L11) - pow2 32*at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11
++ pow2 128
+};
+*)
+assert { 0 <= at(uint 4 reg 10)'L11 /\ 0 <= uint 8 reg 10 /\ 0 <= uint 2 reg 28 /\ 0 <= pow2 16*uint 2 reg 18 };
+assert { 0 <= at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 < pow2 128 };
 
 assert { 0 <= at((uint 4 reg 2 + pow2 32*uint 4 reg 18))'L11 <= pow2 64-1 };
 assert { 0 <= at((uint 4 reg 6 + pow2 32*uint 4 reg 22))'L11 <= pow2 64-1 };
 assert { 0 <= at((uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22))'L11 <= (pow2 64-1)*(pow2 64-1) };
 
-assert {   at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf*pow2 128
-         = at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11 + ?cf*pow2 128
+assert {
+	at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
+	at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11
+	\/
+	at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
+	at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11
+	+ pow2 128
+};
+
+assert {   at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18
+         = at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11
        };
+
   std rZ 4 r10;
   std rZ 5 r11;
   std rZ 6 r12;