Library compcertx.common.MemoryX
Require compcert.common.Memory.
Import Coqlib.
Import Values.
Export Memory.
Module Mem.
Export Memtype.Mem.
Import Coqlib.
Import Values.
Export Memory.
Module Mem.
Export Memtype.Mem.
General-purpose properties on the existing memory model
Lemma val_inject_flat_inj_lessdef:
∀ n v1 v2,
Val.inject (flat_inj n) v1 v2 →
Val.lessdef v1 v2.
Proof.
inversion 1; subst; try (constructor; fail).
unfold flat_inj in H0. destruct (plt b1 n); try discriminate. inv H0.
rewrite Integers.Ptrofs.add_zero. constructor.
Qed.
Section WITHMEM.
Context `{memory_model: MemoryModel}.
Lemma load_inject_neutral:
∀ m,
Mem.inject_neutral (Mem.nextblock m) m →
∀ chunk b o v,
Mem.load chunk m b o = Some v →
Val.inject (Mem.flat_inj (Mem.nextblock m)) v v.
Proof.
intros.
apply Mem.neutral_inject in H.
assert (Mem.flat_inj (Mem.nextblock m) b = Some (b, 0)).
{
unfold Mem.flat_inj.
destruct (plt b (Mem.nextblock m)); eauto.
destruct n.
eapply Mem.valid_access_valid_block.
eapply Mem.valid_access_implies.
eapply Mem.load_valid_access.
eassumption.
constructor.
}
exploit Mem.load_inject; eauto.
replace (o + 0) with o by omega.
destruct 1 as [? [? ?]].
congruence.
Qed.
Lemma loadv_inject_neutral:
∀ m,
Mem.inject_neutral (Mem.nextblock m) m →
∀ chunk a v,
Mem.loadv chunk m a = Some v →
Val.inject (Mem.flat_inj (Mem.nextblock m)) v v.
Proof.
intros.
destruct a; try discriminate.
eapply load_inject_neutral; eauto.
Qed.
Lemma loadbytes_inject_neutral:
∀ m,
Mem.inject_neutral (Mem.nextblock m) m →
∀ b o n l,
Mem.loadbytes m b o n = Some l →
Mem.valid_block m b →
list_forall2 (memval_inject (Mem.flat_inj (Mem.nextblock m))) l l.
Proof.
intros.
apply Mem.neutral_inject in H.
exploit Mem.loadbytes_inject; eauto.
unfold flat_inj. destruct (plt b (nextblock m)); try reflexivity.
contradiction.
destruct 1 as (bytes2 & LOAD2 & INJ).
replace (o + 0) with o in × by omega.
congruence.
Qed.
End WITHMEM.
Additional properties on the memory model required by CompCertX
Class MemoryModelX
(mem: Type)
`{memory_model_ops: MemoryModelOps mem}
: Prop :=
{
memory_model_x_memory_model :> MemoryModel mem;
The following are needed by SmallstepX
extends_extends_compose:
∀ m1 m2 m3,
extends m1 m2 → extends m2 m3 → extends m1 m3
;
inject_extends_compose:
∀ f m1 m2 m3,
inject f m1 m2 → extends m2 m3 → inject f m1 m3
;
inject_compose:
∀ f f' m1 m2 m3,
inject f m1 m2 → inject f' m2 m3 →
inject (compose_meminj f f') m1 m3
;
extends_inject_compose:
∀ f m1 m2 m3,
extends m1 m2 → inject f m2 m3 → inject f m1 m3
;
∀ m1 m2 m3,
extends m1 m2 → extends m2 m3 → extends m1 m3
;
inject_extends_compose:
∀ f m1 m2 m3,
inject f m1 m2 → extends m2 m3 → inject f m1 m3
;
inject_compose:
∀ f f' m1 m2 m3,
inject f m1 m2 → inject f' m2 m3 →
inject (compose_meminj f f') m1 m3
;
extends_inject_compose:
∀ f m1 m2 m3,
extends m1 m2 → inject f m2 m3 → inject f m1 m3
;
The following are needed by AsmX, to prove the preservation of inject_neutral_invariant
inject_neutral_incr:
∀ m thr, inject_neutral thr m → ∀ thr', Ple thr thr' → inject_neutral thr' m
;
free_inject_neutral:
∀ m b lo hi m' thr,
free m b lo hi = Some m' →
inject_neutral thr m →
Plt b thr →
inject_neutral thr m'
;
The following are needed by CertiKOS, to prove Mem.extends between initial memories
drop_perm_right_extends:
∀ m1 m2 b lo hi p m2',
extends m1 m2 →
drop_perm m2 b lo hi p = Some m2' →
(∀ ofs k p, perm m1 b ofs k p → lo ≤ ofs < hi → False) →
extends m1 m2'
;
drop_perm_parallel_extends:
∀ m1 m2 b lo hi p m1',
extends m1 m2 →
drop_perm m1 b lo hi p = Some m1' →
∃ m2',
drop_perm m2 b lo hi p = Some m2'
∧ extends m1' m2'
;
storebytes_inject_neutral:
∀ m b o l m' thr,
storebytes m b o l = Some m' →
list_forall2 (memval_inject (Mem.flat_inj thr)) l l →
Plt b thr →
inject_neutral thr m →
inject_neutral thr m'
;
∀ m b o l m' thr,
storebytes m b o l = Some m' →
list_forall2 (memval_inject (Mem.flat_inj thr)) l l →
Plt b thr →
inject_neutral thr m →
inject_neutral thr m'
;
The following is needed by CertiKOS, to prove LAsm.exec_instr
Idem
The following is needed by LayerLib, to prove transitivity of
ec_mem_extends