Commit da1032e3 authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Rebase and update karatsuba128.mlw

parent dcadaed8
......@@ -163,7 +163,7 @@ let neg (dst: register): unit
ensures { ?cf = -div (old (-reg[dst])) 256 }
*)
= let sum = - Map.get reg.data dst in
reg.data <- Map.set reg.data dst (mod sum 256);
reg.data <- data_set reg.data dst (mod sum 256);
assert { -255 <= sum <= 255 };
cf.value <- (-div sum 256 <> 0);
()
......@@ -492,7 +492,7 @@ let lsr (dst: register): unit
ensures { ?cf = mod (old reg[dst]) 2 }
ensures { cf.value = BV8.nth (BV8.of_int (old reg[dst])) 0 }
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0;
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.lsr (BV8.of_int (Map.get reg.data dst)) 1))
reg.data <- data_set reg.data dst (bv8_to_int (BV8.lsr (BV8.of_int (Map.get reg.data dst)) 1))
let lsl (dst: register): unit
writes { reg, cf }
......@@ -500,7 +500,7 @@ let lsl (dst: register): unit
ensures { ?cf = 0 <-> old reg[dst] < 128 }
ensures { cf.value = BV8.nth (BV8.of_int (old reg[dst])) 7 }
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 7;
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.lsl (BV8.of_int (Map.get reg.data dst)) 1))
reg.data <- data_set reg.data dst (bv8_to_int (BV8.lsl (BV8.of_int (Map.get reg.data dst)) 1))
(* t flag operations *)
val tf: cpu_flag
......
This diff is collapsed.
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