Commit 9e2e0084 by Marc Schoolderman

### reran proofs (on single core), moved lemma about lsr to the top

parent ab4186f5
 ... ... @@ -10,6 +10,9 @@ lemma asr_0: eq (asr zeros 1) zeros lemma asr_1: eq (asr (of_int 1) 1) zeros lemma asr_f: eq (asr ones 1) ones lemma lsr_0: eq (lsr zeros 1) zeros lemma lsr_1: eq (lsr (of_int 1) 1) zeros lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w ... ... @@ -42,16 +45,6 @@ lemma pow2_256: pow2 256 = 0x100000000000000000000000000000000000000000000000000 end module BV_lsr_Lemmas use import bv.BV8 use import int.Int lemma lsr_0: eq (lsr zeros 1) zeros lemma lsr_1: eq (lsr (of_int 1) 1) zeros end module AvrModelLemmas use import int.Int ... ... @@ -721,14 +714,6 @@ by ldd r25 rY 15; (* TODO: optimize this *) (* abstract ensures { uint 3 reg 18 + pow2 24*mem[uint 2 reg rX] = at (uint 4 mem (uint 2 reg rX+12))'S } ensures { uint 4 reg 22 = at (uint 4 mem (uint 2 reg rY+12))'S } assert { "expl:temp" eq 8 mem (at mem 'S) (at (uint 2 reg rX+8)'S) }; assert { "expl:temp" eq 8 mem (at mem 'S) (at (uint 2 reg rY+8)'S) }; end; *) assert { "expl:memory" eq 8 mem (at mem 'S) (at (uint 2 reg rX+8)'S) }; assert { "expl:memory" eq 8 mem (at mem 'S) (at (uint 2 reg rY+8)'S) }; ... ... @@ -2044,10 +2029,6 @@ check { (?cf+reg[28])*pow2 64 + uint 8 mem (uint 2 reg rZ+8) = at(uint 8 mem (ui clr r2; adc r2 r2; (* TODO enable the theory in the next big re-load *) assume { "expl:removeme" BV8.eq (BV8.lsr BV8.zeros 1) BV8.zeros }; assume { "expl:removeme" BV8.eq (BV8.lsr (BV8.of_int 1) 1) BV8.zeros }; check { reg[28] = 0 \/ reg[28] = 1 }; 'Q: lsr r28; ... ...
This diff is collapsed.
No preview for this file type
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!