karatsuba64 done, to be optimized

karatsuba64.mlw

@@ -413,6 +413,8 @@ 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
@@ -553,7 +555,7 @@ assert { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96
 (?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 { 
@@ -651,6 +653,68 @@ 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 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 =