1 goal done, 4 to go (and two goals are now dependent on removing stuff)

... which is not good.

karatsuba64.mlw

@@ -211,6 +211,8 @@ label B in
   sbc r9 r25;
  (* 0xff if carry and 0x00 if no carry *)
   sbc r1 r1;
+  assert { reg[0] = if (uint 4 reg 2 < uint 4 reg 18) at B then 0xFF else 0x00 };
+  assert { reg[1] = if (uint 4 reg 6 < uint 4 reg 22) at B then 0xFF else 0x00 };
 
  (*    absolute values    *)
   eor r2 r0;
@@ -233,6 +235,12 @@ label B in
 
   eor r0 r1;
   bst r0 0 ;
+  assert { 
+  let a = (uint 4 reg 2 < uint 4 reg 18) at B in 
+  let b = (uint 4 reg 6 < uint 4 reg 22) at B in
+  reg[0] = if (a \/ b) /\ not (a /\ b) then 0xFF else 0x00 
+  };
+  assert { !tf = (reg[0] = 0xFF) };
   S.modify_r0(); S.modify_r1();
   S.modify_r2(); S.modify_r3(); S.modify_r4(); S.modify_r5();
   S.modify_r6(); S.modify_r7(); S.modify_r8(); S.modify_r9();