| Facts about memories |
Require Import Asm.Util.ArithUtil.
Require Import Asm.Util.Tactics.
Require Import Asm.Bitvector.Bitvector.
Require Import Asm.X86.Defs.
Set Implicit Arguments.
Inverting byte-sized memory operations |
Lemma invert_set_mem' : forall m addr (v : int8),
v = Int32Map.get addr (Int32Map.set addr v m).
Lemma eq_get_mem_neq : forall addr addr' x m (v : int8),
addr <> addr'
-> x = Int32Map.get addr' m
-> x = Int32Map.get addr' (Int32Map.set addr v m).
Lemma neq_sym : forall (n1 n2 : int32),
n1 <> n2
-> n2 <> n1.
Hint Resolve Int32Map.gss invert_set_mem' Int32Map.gso eq_get_mem_neq : x86.
Hint Resolve binc_neq binc2_neq binc3_neq binc_neq' binc2_neq' binc3_neq' neq_sym : x86.
Hint Unfold set_mem32' : x86.
Inverting word-sized memory operations |
Ltac binc_binc :=
let H := fresh in
(intro H; try exact (binc_neq' H); try exact (binc2_neq' H); try exact (binc3_neq' H)).
Hint Extern 1 (?X1 <> ?X2) => binc_binc : x86.
Lemma invert_set_mem32' : forall m addr v,
get_mem32' (set_mem32' m addr v) addr = v.
Lemma invert_set_mem32 : forall st addr v,
get_mem32 (set_mem32 st addr v) addr = v.
Inductive apart : int32 -> int32 -> Prop :=
| apart_lower : forall a a',
bvec_to_nat a' + 4 <= bvec_to_nat a
-> apart a a'
| apart_higher : forall a a',
bvec_to_nat a' >= bvec_to_nat a + 4
-> apart a a'.
Lemma apart_neq : forall n m,
apart n m
-> n <> m.
Lemma apart_binc_neq : forall n m,
belowMax n 1
-> apart n m
-> binc n <> m.
Lemma apart_binc2_neq : forall n m,
belowMax n 2
-> apart n m
-> binc2 n <> m.
Lemma apart_binc3_neq : forall n m,
belowMax n 3
-> apart n m
-> binc3 n <> m.
Definition not_too_high (n : int32) := belowMax n 3.
Lemma invert_set_mem32'_neq' : forall m addr addr' v,
not_too_high addr
-> apart addr addr'
-> Int32Map.get addr' (set_mem32' m addr v) = Int32Map.get addr' m.
Lemma apart_sym : forall n m,
apart n m
-> apart m n.
Ltac btn_conv :=
match goal with
| [ |- ?X <> ?Y ] => (assert (bvec_to_nat X <> bvec_to_nat Y); try congruence)
end.
Ltac prove_bincs_neq :=
btn_conv;
repeat ((rewrite binc_btn_belowMax || rewrite binc2_btn_belowMax || rewrite binc3_btn_belowMax);
myeauto);
inversion Hapart; try omega.
Lemma invert_set_mem32'_binc_neq' : forall m addr addr' v,
not_too_high addr
-> not_too_high addr'
-> apart addr addr'
-> Int32Map.get (binc addr') (set_mem32' m addr v) = Int32Map.get (binc addr') m.
Lemma invert_set_mem32'_binc2_neq' : forall m addr addr' v,
not_too_high addr
-> not_too_high addr'
-> apart addr addr'
-> Int32Map.get (binc (binc addr')) (set_mem32' m addr v) = Int32Map.get (binc (binc addr')) m.
Lemma invert_set_mem32'_binc3_neq' : forall m addr addr' v,
not_too_high addr
-> not_too_high addr'
-> apart addr addr'
-> Int32Map.get (binc (binc (binc addr'))) (set_mem32' m addr v) = Int32Map.get (binc (binc (binc addr'))) m.
Theorem invert_set_mem32'_neq : forall m addr addr' v,
not_too_high addr
-> not_too_high addr'
-> apart addr addr'
-> get_mem32' (set_mem32' m addr v) addr' = get_mem32' m addr'.
Theorem invert_set_mem32_neq : forall st addr addr' v,
not_too_high addr
-> not_too_high addr'
-> apart addr addr'
-> get_mem32 (set_mem32 st addr v) addr' = get_mem32 st addr'.