alternative justification of add

avrmodel.mlw

@@ -355,6 +355,21 @@ let ghost uint_combine (reg: address_space) (b w w': int)
 
 use bv.BV8
 
+let add_ (dst src: register): unit
+  writes { reg, cf }
+  ensures { reg = old (reg[dst <- mod (reg[dst] + reg[src]) 256]) }
+  ensures { ?cf = old (div (reg[dst] + reg[src]) 256) }
+= let r1 = BV8.of_int (M.get reg.data dst) in
+  let r2 = BV8.of_int (M.get reg.data src) in
+  let r3 = BV8.add r1 r2 in
+  reg.data <- M.set reg.data dst (BV8.to_uint r3);
+  if BV8.nth r1 7 && BV8.nth r2 7 || BV8.nth r1 7 && not BV8.nth r3 7 || not BV8.nth r3 7 && BV8.nth r2 7
+  then
+     cf.value <- 1
+  else
+     cf.value <- 0
+
+
 let eor (dst src: register): unit
   writes { reg }
   ensures { reg = old reg[dst <- BV8.to_uint (BV8.bw_xor (BV8.of_int reg[dst]) (BV8.of_int reg[src])) ] }

prodscan.mlw

@@ -27,7 +27,7 @@ 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)
 
-lemma mul_postcondition_strengthen:
+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
@@ -662,7 +662,7 @@ ensures { eq 5 reg (at reg 'S) 7 }
 	add r19 r25;
 	adc r20 r0;
 	adc r21 r1;
-assert { uint 7 reg 15 = at(uint 7 reg 15 + uint 2 reg 5*uint 5 reg 7)'B };
+(*assert { uint 7 reg 15 = at(uint 7 reg 15 + uint 2 reg 5*uint 5 reg 7)'B };*)
 end
 
 let mul40_flat(): unit
@@ -867,7 +867,7 @@ ensures { eq 6 reg (at reg 'S) 8 }
 	adc r21 r27;
 	adc r22 r0;
 	adc r23 r1;
-check { uint 9 reg 17 = at(uint 9 reg 17 + uint 1 reg 5*uint 6 reg 8)'B };
+(* check { uint 9 reg 17 = at(uint 9 reg 17 + uint 1 reg 5*uint 6 reg 8)'B }; *)
 	mul r6 r10;
 	movw r26  r0;
 	mul r6 r8;
@@ -891,7 +891,7 @@ check { uint 9 reg 17 = at(uint 9 reg 17 + uint 1 reg 5*uint 6 reg 8)'B };
 	adc r22 r27;
 	adc r23 r0;
 	adc r24 r1;
-check { uint 9 reg 17 = at(uint 9 reg 17 + uint 2 reg 5*uint 6 reg 8)'B };
+(* check { uint 9 reg 17 = at(uint 9 reg 17 + uint 2 reg 5*uint 6 reg 8)'B }; *)
 	mul r7 r10;
 	movw r26  r0;
 	mul r7 r8;
@@ -945,7 +945,6 @@ assert { pow2 96 = 0x1000000000000000000000000 };
 	mul r2 r13;
 	add r19  r0;
 	adc r20  r1;
-check { uint 12 reg 14 = at(uint 1 reg 2*uint 6 reg 8)'S };
 	mul r3 r10;
 	movw r26  r0;
 	mul r3 r8;
@@ -969,7 +968,6 @@ check { uint 12 reg 14 = at(uint 1 reg 2*uint 6 reg 8)'S };
 	adc r19 r27;
 	adc r20 r0;
 	adc r21 r1;
-check { uint 12 reg 14 = at(uint 2 reg 2*uint 6 reg 8)'S };
 	mul r4 r10;
 	movw r26  r0;
 	mul r4 r8;
@@ -993,8 +991,6 @@ check { uint 12 reg 14 = at(uint 2 reg 2*uint 6 reg 8)'S };
 	adc r20 r27;
 	adc r21 r0;
 	adc r22 r1;
-check { uint 12 reg 14 = at(uint 3 reg 2*uint 6 reg 8)'S };
-'B:
 	mul r5 r10;
 	movw r26  r0;
 	mul r5 r8;
@@ -1018,8 +1014,6 @@ check { uint 12 reg 14 = at(uint 3 reg 2*uint 6 reg 8)'S };
 	adc r21 r27;
 	adc r22 r0;
 	adc r23 r1;
-check { uint 12 reg 14 = at(uint 4 reg 2*uint 6 reg 8)'S };
-check { uint 9 reg 17 = at(uint 9 reg 17 + uint 1 reg 5*uint 6 reg 8)'B };
 	mul r6 r10;
 	movw r26  r0;
 	mul r6 r8;
@@ -1043,8 +1037,6 @@ check { uint 9 reg 17 = at(uint 9 reg 17 + uint 1 reg 5*uint 6 reg 8)'B };
 	adc r22 r27;
 	adc r23 r0;
 	adc r24 r1;
-check { uint 12 reg 14 = at(uint 5 reg 2*uint 6 reg 8)'S };
-check { uint 9 reg 17 = at(uint 9 reg 17 + uint 2 reg 5*uint 6 reg 8)'B };
 	mul r7 r10;
 	movw r26  r0;
 	mul r7 r8;
@@ -1068,7 +1060,6 @@ check { uint 9 reg 17 = at(uint 9 reg 17 + uint 2 reg 5*uint 6 reg 8)'B };
 	adc r23 r27;
 	adc r24 r0;
 	adc r25 r1;
-check { uint 9 reg 17 = at(uint 9 reg 17 + uint 3 reg 5*uint 6 reg 8)'B };
 	()
 
 use import int.Abs