Upper 96 bits are done

karatsuba64.mlw

@@ -189,7 +189,10 @@ 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 { ?tf = 0 <-> old((uint 4 reg 2 < uint 4 reg 18) <-> (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 { valid_addr_space reg }
 
 label B in
@@ -434,7 +437,7 @@ 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 { 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 }
@@ -448,6 +451,7 @@ ensures { valid_addr_space reg }
 label B in
 assert { reg[27] = 0 };
   bld r27 0;
+assert { reg[27] = ?tf };
   dec 27;
 assert { reg[27] = 0xFF*(1 - ?tf) by mod (- 1) 256 = 0xFF };
 
@@ -521,7 +525,8 @@ 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 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 };
 
@@ -545,7 +550,7 @@ assert { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96
 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) + 
+(?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) };
 
 
@@ -555,13 +560,13 @@ 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) + 
+(?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) + (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) + 
+(?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)) 
 };
 
@@ -569,13 +574,13 @@ 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) + 
+(?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) + (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) + 
+(?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) 
 };
 
@@ -583,13 +588,13 @@ 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) - 
+(?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) + (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) + 
+(?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) 
 };
 
@@ -597,66 +602,56 @@ 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)
+(?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) + 
-(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) + 
+(?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))  + 
-(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 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)) + 
-(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 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) + 
-(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 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) + 
-(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
+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 + 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 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 + 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
+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 { 
-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