Commit 927e6350 authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Prove avrmodel using 1 additional axiom

parent da1032e3
......@@ -403,6 +403,7 @@ let adiw (dst: register) (k: int): unit
ensures { ?cf*pow2 16 + uint 2 reg dst = old (uint 2 reg dst + k) }
= let sum = Map.get reg.data dst + 256*Map.get reg.data (dst+1) +k in
reg.data <- data_set reg.data dst (mod sum 256);
assert { mod sum 256 = mod (old (reg[dst] + k)) 256 };
reg.data <- data_set reg.data (dst+1) (mod (div sum 256) 256);
cf.value <- (sum > 65535)
......@@ -428,6 +429,8 @@ use bv.BV8
val bv8_to_int (x: BV8.t): int
ensures { result = BV8.t'int x }
axiom bv8_nth_def: forall x y. BV8.nth (BV8.of_int x) y <-> mod (div x (pow2 y)) 2 = 1
let add_ (dst src: register): unit
writes { reg, cf }
ensures { reg = old (reg[dst <- mod (reg[dst] + reg[src]) 256]) }
......
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!
Please register or to comment