Library mcertikos.layerlib.SoundnessAux
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.PTreeSemantics.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import LAsmModuleSem.
Require Import LAsmModuleSemAux.
Require Import LAsmModuleSemMakeProgram.
Require Import LAsmModuleSemSim.
Require Import LAsmModuleSemInvariants.
Require Import LAsm.
Require Import CommonTactic.
Require Import InitMem.
Require Import RefinementTactic.
Require Import AuxLemma.
Section WITHLAYERS.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Context `{make_program_ops: !MakeProgramOps LAsm.function Ctypes.type LAsm.fundef unit}.
Context `{make_program_prf: !MakeProgram LAsm.function Ctypes.type LAsm.fundef unit}.
Inductive match_states {D1: compatdata} {D2: compatdata} {R: compatrel D1 D2}:
stencil → (state (mem:= mwd D1)) → (state (mem:= mwd D2)) → Prop :=
| match_states_intro:
∀ s f rs m d rs´ m´ d´,
MatchPrimcallStates R s f rs m d rs´ m´ d´ →
high_level_invariant d →
high_level_invariant d´ →
low_level_invariant (Mem.nextblock m´) d´ →
asm_invariant (mem:= mwd D2) s rs´ (m´, d´) →
match_states s (State rs (m, d)) (State rs´ (m´, d´)).
Lemma one_step_sim_monotonic_alt {D1: compatdata} {D2: compatdata}
{L1} {L2} {R: compatrel D1 D2}
`{acc_def_prf1: !AccessorsDefined L1}
`{names1: !LayerNamesMatch D1 L1}
`{acc_def_prf2: !AccessorsDefined L2}
`{names2: !LayerNamesMatch D2 L2}:
∀ `{memory_model_x: !Mem.MemoryModelX mem},
∀ `{extcall_inv_def_prf1: !ExtcallInvariantsAvailable L1},
∀ `{primcall_inv_def_prf1: !PrimcallInvariantsAvailable L1},
∀ `{extcall_inv_def_prf2: !ExtcallInvariantsAvailable L2},
∀ `{primcall_inv_def_prf2: !PrimcallInvariantsAvailable L2},
∀ `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet},
∀ (s: stencil) ge ge´ rs1 rs1´ m1 m1´ d1 d1´ rs2 m2 d2 t,
∀ (Hglobalenv: ∃ M, make_globalenv (D:=D2) s M L2 = OK ge´),
∀ (Hge_external´:
∀ b ef,
Genv.find_funct_ptr ge´ b = Some (External ef) →
∃ i sg, ef = EF_external i sg),
∀ (OKLayer: LayerOK L2),
∀ (ValidLayer: get_layer_prim_valid L2 s),
stencil_matches s ge →
stencil_matches s ge´ →
ge ≤ ge´ →
cl_sim D1 D2 (freerg_inj _ _ _ R) L1 L2 →
match_states s (State rs1 (m1, d1)) (State rs2 (m2, d2)) →
(step (lcfg_ops:= LC L1))
ge (State rs1 (m1, d1)) t (State rs1´ (m1´, d1´)) →
∃ rs2´ m2´ d2´,
(step (lcfg_ops:= LC L2))
ge´ (State rs2 (m2, d2)) t (State rs2´ (m2´, d2´))
∧ match_states s (State rs1´ (m1´, d1´)) (State rs2´ (m2´, d2´)).
Proof.
intros. inv H3.
exploit (one_step_sim_monotonic´_avail s ge ge´); eauto 1.
intros [f´[rs2´[m2´[d2´[Hstep[Hmatch[Hhigh[Hhigh´[Hlow Hasm]]]]]]]]].
refine_split´; eauto 2.
econstructor; eauto 2.
Qed.
Lemma get_module_function_oplus_ok_left i M1 M2 κ:
ModuleOK (M1 ⊕ M2) →
get_module_function i M1 = OK (Some κ) →
get_module_function i (M1 ⊕ M2) = OK (Some κ).
Proof.
intros HM HM1i.
assert (HMi: res_le (option_le eq) (get_module_function i M1)
(get_module_function i (M1 ⊕ M2))). {
apply get_module_function_monotonic.
apply left_upper_bound.
}
destruct (HM i) as [[κ´ Hκ´] _ _].
destruct HMi as [_ _ [|] | ]; try discriminate.
congruence.
Qed.
Lemma get_module_function_oplus_ok_right i M1 M2 κ:
ModuleOK (M1 ⊕ M2) →
get_module_function i M1 = OK (Some κ) →
get_module_function i (M1 ⊕ M2) = OK (Some κ).
Proof.
intros HM HM1i.
assert (HMi: res_le (option_le eq) (get_module_function i M1)
(get_module_function i (M1 ⊕ M2))). {
apply get_module_function_monotonic.
apply left_upper_bound.
}
destruct (HM i) as [[κ´ Hκ´] _ _].
destruct HMi as [_ _ [|] | ]; try discriminate.
congruence.
Qed.
Lemma res_option_oplus_none_inv {A} (x y: res (option A)):
x ⊕ y = OK None →
x = OK None ∧ y = OK None.
Proof.
destruct x as [[|]|], y as [[|]|];
inversion 1;
split;
reflexivity.
Qed.
Lemma get_module_function_oplus_ok_either i M1 M2 δ:
ModuleOK (M1 ⊕ M2) →
get_module_function i (M1 ⊕ M2) = OK δ →
(get_module_function i M1 = OK δ ∧ isOKNone (get_module_function i M2)) ∨
(isOKNone (get_module_function i M1) ∧ get_module_function i M2 = OK δ).
Proof.
intros HM Hi.
destruct (HM i) as [[f Hf] [v Hv] Hdisj].
revert Hdisj Hf Hv Hi.
get_module_normalize.
unfold isOKNone.
intros [Hdisj|Hdisj] Hf Hv Hδ;
apply res_option_oplus_none_inv in Hdisj;
destruct Hdisj as [H1 H2];
rewrite H1, H2 in ×.
× left.
split; [assumption|reflexivity].
× destruct (get_module_function i M1) as [[|]|];
destruct (get_module_function i M2) as [[|]|];
try discriminate.
+ left.
split; [assumption|reflexivity].
+ right.
split; [reflexivity|assumption].
+ left.
split; [assumption|reflexivity].
Qed.
Lemma get_layer_primitive_oplus_either {D} i L1 L2 σ:
get_layer_primitive (D:=D) i (L1 ⊕ L2) = OK (Some σ) →
get_layer_primitive i L1 = OK (Some σ) ∨
get_layer_primitive i L2 = OK (Some σ).
Proof.
get_layer_normalize.
destruct (get_layer_primitive i L1) as [[|]|];
destruct (get_layer_primitive i L2) as [[|]|];
try discriminate;
intros H.
× left; assumption.
× right; assumption.
Qed.
Lemma make_globalenv_module_ok {D} s M L:
isOK (make_globalenv (D:=D) s M L) →
ModuleOK M.
Proof.
intros [ge Hge].
unfold make_globalenv in Hge.
inv_monad Hge.
eapply make_program_module_ok.
∃ x.
eassumption.
Qed.
Lemma make_globalenv_vertical´ {D} `{L: compatlayer D}:
∀ s CTXT (M: module) ge ge´,
stencil_matches s ge →
stencil_matches s ge´ →
make_globalenv s CTXT (〚 M 〛 L ⊕ L) = ret ge
→ make_globalenv s (CTXT ⊕ M) L = ret ge´
→ (∀ b f, Genv.find_funct_ptr ge b = Some (Internal f)
→ Genv.find_funct_ptr ge´ b = Some (Internal f))
∧ (∀ b id sg,
isOKNone (get_module_function id M)
→ Genv.find_funct_ptr ge b = Some (External (EF_external id sg))
→ Genv.find_funct_ptr ge´ b = Some (External (EF_external id sg)))
∧ (∀ b id sg f,
get_module_function id M = OK (Some f) →
Genv.find_funct_ptr ge b = Some (External (EF_external id sg))
→ Genv.find_funct_ptr ge´ b = Some (Internal f)).
Proof.
intros until ge´.
intros Hsge Hsge´ Hge Hge´.
assert (MOK: ModuleOK (CTXT ⊕ M)).
{
eapply make_globalenv_module_ok.
eexists; eassumption.
}
split.
{
intros.
exploit @make_globalenv_find_funct_ptr.
{ eexact Hge. }
{ eassumption. }
destruct 1 as (j & SYMB & K).
destruct K as [K | K].
{
destruct K as (? & MOD & INT).
exploit @make_globalenv_get_module_function.
{ eexact Hge´. }
{
instantiate (2 := j).
instantiate (1 := f).
apply get_module_function_oplus_ok_left; eauto.
simpl in INT; destruct (instrs_OK (fn_code x)); congruence.
}
{
simpl in *; destruct (instrs_OK (fn_code x)) eqn:Heq; inv INT.
rewrite Heq; reflexivity.
}
destruct 1 as (b´ & SYMB´ & FUNCT´).
erewrite stencil_matches_symbols in SYMB by eauto using make_globalenv_stencil_matches.
erewrite stencil_matches_symbols in SYMB´ by eauto using make_globalenv_stencil_matches.
replace b´ with b in × by congruence.
assumption.
}
{
exfalso.
destruct K as (? & ? & ?). discriminate.
}
}
split.
{
intros.
exploit @make_globalenv_find_funct_ptr.
{ eexact Hge. }
{ eassumption. }
destruct 1 as (j & SYMB & K).
destruct K as [K | K].
{
exfalso.
destruct K as (x & ? & ?); simpl in *; destruct (instrs_OK (fn_code x)); congruence.
}
destruct K as (? & LAY & EXT).
edestruct (make_globalenv_get_layer_primitive s (CTXT ⊕ M) L ge´); eauto.
{
edestruct (get_layer_primitive_oplus_either j (〚M〛L) L);
try eassumption.
exfalso.
unfold isOKNone in H.
rewrite get_semof_primitive in H1.
unfold semof_function in H1.
inversion EXT; subst; clear EXT.
rewrite H in H1.
discriminate.
}
destruct H1 as [Hjx0 Hx0id].
erewrite stencil_matches_symbols in Hjx0 by eassumption.
erewrite stencil_matches_symbols in SYMB by eassumption.
congruence.
}
{
intros.
exploit @make_globalenv_find_funct_ptr.
{ eexact Hge. }
{ eassumption. }
destruct 1 as (j & SYMB & K).
destruct K as [K | K].
{
exfalso.
destruct K as (x & ? & ?); simpl in *; destruct (instrs_OK (fn_code x)); congruence.
}
destruct K as (? & LAY & EXT).
generalize EXT.
inversion 1; subst.
exploit @make_globalenv_get_module_function.
{ eexact Hge´. }
{
instantiate (2 := id).
instantiate (1 := f).
exploit @get_module_function_monotonic.
{
apply (right_upper_bound CTXT M).
}
instantiate (1 := id).
rewrite H.
inversion 1; subst.
{
inv H4.
inv H1.
inv H5.
× simpl in ×.
congruence.
× destruct (MOK id) as [[a Ha] _ _].
simpl in ×.
congruence.
}
exfalso.
symmetry in H4.
destruct (MOK id) as [MOK_FUN _ _].
generalize MOK_FUN.
simpl.
rewrite H4.
destruct 1; discriminate.
}
{
exploit @make_program_get_module_function_prop; [|eassumption|].
× unfold make_globalenv in Hge´; inv_monad Hge´.
rename H2 into Hmp; eapply make_program_monotonic_exists.
apply right_upper_bound.
reflexivity.
eassumption.
× intros [[? ?] [_ _]]; simpl in ×.
destruct (instrs_OK (fn_code f)); [eauto|discriminate].
}
destruct 1 as (b´ & SYMB´ & FUNCT´).
erewrite stencil_matches_symbols in SYMB by eauto using make_globalenv_stencil_matches.
erewrite stencil_matches_symbols in SYMB´ by eauto using make_globalenv_stencil_matches.
replace b´ with b in × by congruence.
assumption.
}
Qed.
Lemma res_option_oplus_some_inv {A} (x: A) (y: res (option A)) (z: A):
(OK (Some x)) ⊕ y = OK (Some z) →
x = z.
Proof.
intros H.
destruct y as [[|]|]; inversion H.
reflexivity.
Qed.
Lemma get_layer_primitive_right_eq´ {D} `{L: compatlayer D}:
∀ i (σ: compatsem D) M f,
get_layer_primitive i (〚 M 〛 L ⊕ L) = OK (Some σ) →
get_module_function i M = OK (Some f) →
LayerOK L →
semof_fundef D M L i f = OK σ.
Proof.
intros.
rewrite get_layer_primitive_oplus in H.
rewrite get_semof_primitive in H.
unfold semof_function in H.
rewrite H0 in H.
monad_norm.
destruct (semof_fundef _ _ _ _ _) as [σ´|err]; try discriminate.
monad_norm.
apply res_option_oplus_some_inv in H.
congruence.
Qed.
Lemma get_layer_primitive_right_neq´ {D} `{L: compatlayer D}:
∀ i (σi: compatsem D) M,
get_layer_primitive i (〚 M 〛 L ⊕ L) = OK (Some σi) →
isOKNone (get_module_function i M) →
get_layer_primitive i L = OK (Some σi).
Proof.
intros.
rewrite get_layer_primitive_oplus in H.
rewrite get_semof_primitive in H.
unfold isOKNone in *; rewrite H0 in H.
unfold semof_function in H.
monad_norm.
rewrite id_left in H.
assumption.
Qed.
Lemma one_step_vertical_composition {D} `{L: compatlayer D} {M}
(L_ACC_DEF: LAsm.AccessorsDefined L)
(L_NAMES: LayerNamesMatch D L)
(L_ACC_DEF´: LAsm.AccessorsDefined (〚M 〛 L ⊕ L)):
∀ s ge ge´ CTXT r r´ (m m´: mem) (d d´: D) t,
∀ (extinv: ExtcallInvariantsDefined L),
∀ (priminv: PrimcallInvariantsDefined L),
∀ (valid_prim: get_layer_prim_valid L s),
make_globalenv s CTXT (〚 M 〛 L ⊕ L) = ret ge
→ make_globalenv s (CTXT ⊕ M) L = ret ge´
→ step (lcfg_ops:= LC (〚 M 〛 L ⊕ L)) ge (State r (m, d)) t (State r´ (m´, d´))
→ plus (step (lcfg_ops:= LC L)) ge´
(State r (m, d)) t (State r´ (m´, d´)).
Proof.
intros. pose proof H0 as Hge_match´. pose proof H as Hge_match.
apply make_globalenv_stencil_matches in H0.
apply make_globalenv_stencil_matches in H.
pose proof H as Hge. pose proof H0 as Hge´.
inv H. inv H0.
assert (Hsymbol: ∀ i, Genv.find_symbol ge´ i = Genv.find_symbol ge i).
{
intros; abstract congruence.
}
unfold fundef in ×.
assert (Hgenv_next: Genv.genv_next ge´ = Genv.genv_next ge).
{
unfold fundef.
intros; abstract congruence.
}
assert(Hvolatile: ∀ b1 : block, block_is_volatile ge´ b1 = block_is_volatile ge b1).
{
unfold fundef.
intros; abstract congruence.
}
generalize Hge_match. intro HgeL_dup.
eapply make_globalenv_vertical´ in HgeL_dup; eauto.
destruct HgeL_dup as [Hinternal [Hext Hext´]].
assert (Hge_external´:
∀ b ef,
Genv.find_funct_ptr ge b = Some (External ef) →
∃ i sg, ef = EF_external i sg).
{
intros until ef; eapply ge_external_valid; eauto.
}
assert (mk_prog´: isOK (make_program s (CTXT ⊕ M) L)).
{
unfold make_globalenv in Hge_match´.
inv_monad Hge_match´.
esplit; eauto.
}
assert (mk_prog: isOK(make_program s M L)).
{
destruct mk_prog´ as [? mk_prog´].
eapply make_program_monotonic_exists; try eassumption; try reflexivity.
apply right_upper_bound.
}
assert (Hmoduleok: ModuleOK M).
{
eapply make_program_module_ok; eassumption.
}
assert (Hlayerok: LayerOK L).
{
eapply make_program_layer_ok; try eassumption.
}
assert (Hget: ∀ i,
(∃ func, get_module_function i M = OK (Some func))
∨ (isOKNone (get_module_function i M))).
{
intros.
destruct (Hmoduleok i) as [Hfun _ _].
revert Hfun.
destruct (get_module_function i M); eauto.
destruct o; eauto.
destruct 1.
discriminate.
}
eapply vcomp_step; try eapply H2; eauto 2; intros.
- assert(HW: acc_exec_load (〚M 〛 L ⊕ L) = acc_exec_load L).
{
unfold acc_exec_load.
destruct (acc_exec_load_strong (〚M 〛 L ⊕ L)).
simpl in e.
destruct (acc_exec_load_strong L).
rewrite e0 in e. abstract (inversion e; trivial).
}
rewrite <- HW.
erewrite exec_load_symbols_preserved; eauto.
- assert(HW´: acc_exec_store (〚M 〛 L ⊕ L) = acc_exec_store L).
{
unfold acc_exec_store.
destruct (acc_exec_store_strong (〚M 〛 L ⊕ L)).
simpl in e.
destruct (acc_exec_store_strong L).
rewrite e0 in e. abstract (inversion e; trivial).
}
rewrite <- HW´.
erewrite exec_store_symbols_preserved; eauto.
- eapply Hge_external´ in H.
destruct H as [?[? ?]]; subst. inv H0.
-
destruct (Hget i) as [?|?].
destruct H2 as [funcp ?].
specialize (Hext´ _ _ _ _ H2 H).
eapply (get_layer_primitive_right_eq´) in H0; eauto; subst.
inv H0.
split; eauto.
eapply get_layer_primitive_right_neq´; eauto.
-
destruct (Hget i) as [?|?].
+
destruct H5 as [funcp ?].
specialize (Hext´ _ _ _ _ H5 H).
eapply (get_layer_primitive_right_eq´) in H0; eauto. subst.
exploit (compatsem_primcall_le (D:= D)); eauto.
× reflexivity.
× econstructor; eauto.
× inv H0. simpl.
intros.
eapply stencil_matches_unique in H0; try apply Hge. subst.
destruct (Decision.decide (ExtcallInvariantsDefined L)).
destruct (Decision.decide (PrimcallInvariantsDefined L)).
destruct (Decision.decide (LayerNamesMatch D L)).
destruct (Decision.decide (get_layer_prim_valid L s1)).
rewrite accessors_defined_weak; try assumption.
destruct mk_prog as [? mk_prog].
rewrite mk_prog. reflexivity.
elim n; assumption.
elim n; assumption.
elim n; assumption.
elim n; assumption.
× intros Hsem´; inv Hsem´.
eapply stencil_matches_unique in H2; try apply Hge. subst.
inv H0; simpl in H4.
inv H4.
pose proof Hge0 as Hge0´.
apply make_globalenv_stencil_matches in Hge0.
apply make_globalenv_split_module_right in Hge_match´.
destruct Hge_match´ as [?[HgeL Hle´´]].
unfold fundef in ×.
rewrite Hge0´ in HgeL. inv HgeL.
eapply one_sim_plus; eauto. intros.
eapply one_step_monotonic; eauto.
+
exploit Hext; eauto. intros Hfind.
apply plus_one.
eapply exec_step_prim_call; eauto.
eapply get_layer_primitive_right_neq´ in H0; eauto.
econstructor; eauto.
refine_split´; eauto.
eapply stencil_matches_unique in H2; try apply Hge. subst.
econstructor; eauto.
Qed.
Remark annot_arguments_determ_with_data {D}:
∀ rs (m: mwd D) params args1 args2,
annot_arguments rs m params args1 → annot_arguments rs m params args2 → args1 = args2.
Proof.
unfold annot_arguments. intros. revert params args1 H args2 H0.
induction 1; intros.
inv H0; auto.
inv H1. decEq; eauto. inv H; inv H4. auto. congruence.
Qed.
Remark extcall_arguments_determ_with_data {D}:
∀ rs (m: mwd D) sg args1 args2,
extcall_arguments rs m sg args1 → extcall_arguments rs m sg args2 → args1 = args2.
Proof.
intros until m.
assert (∀ ll vl1, list_forall2 (extcall_arg rs m) ll vl1 →
∀ vl2, list_forall2 (extcall_arg rs m) ll vl2 → vl1 = vl2).
induction 1; intros vl2 EA; inv EA.
auto.
f_equal; auto.
inv H; inv H3; congruence.
intros. red in H0; red in H1. eauto.
Qed.
Lemma external_prim_false {D} `{L: compatlayer D}
(acc_def_prf: LAsm.AccessorsDefined L):
∀ ge ef WB args t1 t2 res (m m´ m´0: mwd D) rs rs´,
external_call´ (external_calls_ops:= compatlayer_extcall_ops L) WB ef ge args m t1 res m´ →
primitive_call (LayerConfigurationOps:= LC (acc_def_prf:= acc_def_prf) L) ef ge rs m t2 rs´ m´0 →
False.
Proof.
intros.
inv H. inv H0. destruct H as [?[?[?[? ?]]]]; subst.
simpl in ×. destruct H1 as [?[? ?]].
rewrite H in H0. inv H0.
inv H1. inv H2. destruct H0 as [?[?[?[? _]]]].
inv H4.
Qed.
Lemma make_program_ok_disjoint {D} s M L p:
make_program (D:=D) s M L = OK p →
module_layer_disjoint M L.
Proof.
intros.
unfold module_layer_disjoint.
assert (pOK: isOK (make_program s M L)).
{
esplit. eassumption.
}
intros i.
pose proof (make_program_layer_ok s M L pOK) as LOK.
destruct (LOK i) as [Lprim Lvar _].
destruct Lprim as [x Lprim].
destruct x.
{
left. eapply make_program_get_layer_primitive_prop; eassumption.
}
{
destruct Lvar as [? Lvar].
destruct x.
{
left. eapply make_program_get_layer_globalvar_prop; eassumption.
}
right.
rewrite Lprim, Lvar.
split; constructor.
}
Qed.
Lemma get_layer_primitive_semof {D} i M (L: compatlayer D) σ:
get_layer_primitive i (〚M〛 L ⊕ L) = OK (Some σ) →
(∃ σ´, get_layer_primitive i L = OK (Some σ´)) ∨
(∃ κ, get_module_function i M = OK (Some κ)).
Proof.
intros Hi.
edestruct (get_layer_primitive_oplus_either i (〚M〛L) L) as [H|H].
+ eassumption.
+ right.
rewrite get_semof_primitive in H.
unfold semof_function in H.
destruct (get_module_function i M) as [[|]|]; inversion H.
eauto.
+ left.
eauto.
Qed.
Lemma res_option_oplus_ok_inv {A} (x y: res (option A)) (z: option A):
x ⊕ y = OK z → (isOK x ∧ isOKNone y) ∨ (isOK y ∧ isOKNone x).
Proof.
destruct x as [[|]|], y as [[|]|]; try discriminate; eauto.
Qed.
Lemma res_option_oplus_ok_some_inv {A} (x y: res (option A)) (z: A):
x ⊕ y = OK (Some z) →
(x = OK (Some z) ∧ y = OK None) ∨
(x = OK None ∧ y = OK (Some z)).
Proof.
destruct x as [[|]|], y as [[|]|]; try discriminate; eauto.
Qed.
Lemma res_option_oplus_ok_none_inv {A} (x y: res (option A)):
isOKNone (x ⊕ y) →
isOKNone x ∧ isOKNone y.
Proof.
destruct x as [[|]|], y as [[|]|]; try discriminate; eauto.
Qed.
Lemma make_program_vertical´:
∀ D (LL: compatlayer D) s M CTXT p
(Hlayer_mo: LayerOK (〚 M 〛 LL ⊕ LL)),
make_program s (CTXT ⊕ M) LL = OK p
→ ∃ p´, make_program s CTXT (〚 M 〛 LL ⊕ LL) = OK p´.
Proof.
intros until p.
intros Hlayer_mo MKP.
assert (MKP´: isOK (make_program s (CTXT ⊕ M) LL))
by (rewrite MKP; unfold isOK; eauto).
pose proof (make_program_module_ok _ _ _ MKP´) as MOK.
pose proof (make_program_layer_ok _ _ _ MKP´) as LOK´.
apply make_program_exists; eauto.
× eapply module_ok_antitonic; eauto.
unfold flip.
apply left_upper_bound.
× intros i fe Hi.
specialize (get_layer_primitive_oplus i (〚M 〛 LL) LL).
intros Hle.
destruct (LOK´ i) as [Lprim Lvar _].
destruct Lprim as [? Lprim].
rewrite Lprim in Hle. rewrite Hi in Hle.
split; [eexists; reflexivity|].
destruct x.
{
exploit (make_program_get_layer_primitive_prop (D:=D)); eauto.
intros ( _ & Hmo & Hva).
split.
- eapply get_module_function_none_oplus in Hmo. eapply Hmo.
- eapply get_module_variable_none_oplus in Hva. eapply Hva.
}
{
destruct (MOK i) as [[κ Hκ] [τ Hτ] _].
get_module_normalize_in Hκ.
get_module_normalize_in Hτ.
clear Hi Lprim Lvar.
rewrite id_right in Hle.
split.
× rewrite get_semof_primitive in Hle.
destruct (get_module_function i M) as [[|]|]; try discriminate.
destruct (res_option_oplus_ok_inv _ _ _ Hκ) as [[HC HM] | [HM HC]].
- discriminate.
- assumption.
× destruct (MOK i) as [_ _ [Hf|Hv]].
- rewrite get_semof_primitive in Hle.
rewrite get_module_function_oplus in Hf.
destruct (get_module_function i M) as [[|]|]; try discriminate.
destruct (get_module_function i CTXT) as [[|]|]; try discriminate.
- rewrite get_module_variable_oplus in Hv.
destruct (get_module_variable i M) as [[|]|];
destruct (get_module_variable i CTXT) as [[|]|];
try discriminate.
reflexivity.
}
× intros i fi Hfi.
split.
{
exploit @make_program_get_module_function_prop.
+ eassumption.
+ destruct (MOK i) as [[? MOK1] _ _].
specialize (get_module_function_oplus i CTXT M).
rewrite Hfi, MOK1.
destruct (get_module_function i M) as [[|]|]; try discriminate.
intros H; inv H; eauto.
+ intuition.
}
destruct (MOK i) as [[κ MOK1] [τ MOK2] Mdisj].
specialize (get_module_function_oplus i CTXT M).
rewrite Hfi. rewrite MOK1.
destruct (get_module_function i M) as [[|]|] eqn:HMi; try discriminate.
intros H; inversion H; subst; clear H.
exploit (make_program_get_module_function_prop (D:=D)); eauto.
intros (Hfalse & Lprim & Lvar).
rewrite MOK1 in Mdisj.
destruct Mdisj as [Mvar|Mvar]; try discriminate.
get_layer_normalize.
unfold isOKNone in ×.
split.
+ rewrite get_semof_primitive.
rewrite HMi.
rewrite Lprim.
reflexivity.
+ rewrite get_semof_globalvar.
rewrite Lvar.
rewrite get_module_variable_oplus in Mvar.
destruct (get_module_variable i M) as [[|]|];
destruct (get_module_variable i CTXT) as [[|]|];
try discriminate.
reflexivity.
× intros i fi Hfi.
rewrite get_layer_globalvar_oplus in Hfi.
rewrite get_semof_globalvar in Hfi.
apply res_option_oplus_ok_some_inv in Hfi.
destruct Hfi as [[HMi HLi] | [HMi HLi]].
+ exploit (make_program_get_module_variable_prop s (CTXT ⊕ M) LL i fi); eauto.
- destruct (MOK i) as [_ [τ Hτ] _].
revert Hτ.
get_module_normalize.
rewrite HMi.
destruct (get_module_variable i CTXT) as [[|]|]; try discriminate.
reflexivity.
- intros (Hfi & Lprim & Lvar).
split;eauto.
split.
{
destruct (MOK i) as [_ _ CMdisj].
get_module_normalize_in CMdisj.
destruct CMdisj as [Hf|Hv].
- apply res_option_oplus_ok_none_inv in Hf.
destruct Hf.
assumption.
- apply res_option_oplus_ok_none_inv in Hv.
destruct Hv.
congruence.
}
{
destruct (MOK i) as [_ [τ CMvar] _].
get_module_normalize_in CMvar.
apply res_option_oplus_ok_inv in CMvar.
destruct CMvar as [[? ?] | [? ?]].
- congruence.
- assumption.
}
+ exploit (make_program_get_layer_globalvar_prop s (CTXT ⊕ M) LL i fi); eauto.
get_module_normalize.
intros (Hgvar & Hf & Hv).
split; eauto.
split.
- apply res_option_oplus_ok_none_inv in Hf.
destruct Hf.
assumption.
- apply res_option_oplus_ok_none_inv in Hv.
destruct Hv.
assumption.
× intros i fi Hfi.
destruct (MOK i) as [MOK1 [? MOK2]].
specialize (get_module_variable_oplus i CTXT M).
rewrite Hfi. rewrite MOK2.
intros Hle.
specialize (get_module_variable_isOK i CTXT M).
rewrite MOK2. intros HW.
exploit HW. esplit; reflexivity.
intros (_ & HM). clear HW.
destruct HM as [? HM].
rewrite HM in Hle.
destruct x0; inv_monad Hle.
exploit (make_program_get_module_variable_prop (D:=D)); eauto.
intros (Hfalse & Lprim & Lvar).
split; try assumption.
specialize (get_module_function_variable_disjoint (CTXT ⊕ M) i).
rewrite MOK2.
intros HW.
destruct HW as [HF|]; try discriminate.
get_module_normalize_in HF.
apply res_option_oplus_ok_none_inv in HF.
destruct HF as [_ HF].
get_layer_normalize.
rewrite get_semof_primitive.
rewrite get_semof_globalvar.
unfold isOKNone in ×.
subrewrite´.
split; reflexivity.
× intros i σ Hiσ.
apply make_program_make_globalenv in MKP.
destruct (get_layer_primitive_semof i M LL _ Hiσ) as [[σ´ Hσ´]|[κ Hκ]].
+ exploit (make_globalenv_get_layer_primitive s (CTXT ⊕ M) LL); eauto.
reflexivity.
intros (b & Hb & _).
erewrite stencil_matches_symbols in Hb.
eexists; eassumption.
eapply make_globalenv_stencil_matches; eauto.
+ exploit (make_globalenv_get_module_function s (CTXT ⊕ M) LL); eauto.
- instantiate (1:=κ); instantiate (1:=i).
destruct (MOK i) as [MOK´ _]; clear MOK.
destruct MOK´ as [? MOK].
specialize (get_module_function_oplus i CTXT M).
rewrite MOK. rewrite Hκ.
intros Hle.
Transparent oplus.
destruct (get_module_function i CTXT); try destruct o;
inv_monad Hle. reflexivity.
- exploit @make_program_get_module_function_prop.
eassumption.
destruct (MOK i) as [[? MOK1] _ _].
specialize (get_module_function_oplus i CTXT M).
rewrite Hκ, MOK1.
destruct (get_module_function i CTXT) as [[|]|]; try discriminate.
intros H; inv H; eauto.
intros [[? ?] _]; simpl in ×.
destruct (instrs_OK (fn_code κ)); [eauto|discriminate].
- intros (b & Hb & _).
eapply make_globalenv_stencil_matches in MKP; eauto.
inv MKP. rewrite stencil_matches_symbols in Hb.
rewrite Hb. esplit; reflexivity.
× intros i σ Hiσ.
apply make_program_make_globalenv in MKP.
destruct (LOK´ i) as [LOK1 LOK2].
destruct LOK2 as [? LOK2].
specialize (get_layer_globalvar_oplus i (〚M 〛 LL) LL).
rewrite Hiσ. rewrite LOK2.
intros Hle.
exploit (make_globalenv_stencil_matches (D:=D)); eauto.
intros Hsten. inv Hsten.
destruct x.
{
exploit (make_globalenv_get_layer_globalvar (D:=D)); eauto.
intros (? & Hsym & _).
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
}
{
destruct LOK1 as [? LOK1].
destruct x.
{
exploit (make_globalenv_get_layer_primitive (D:=D)); eauto.
reflexivity.
intros (? & Hsym & _).
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
}
{
destruct (MOK i) as [MOK1 MOK2].
destruct MOK1 as [? MOK1].
destruct x.
{
exploit (make_globalenv_get_module_function (D:=D)); eauto.
exploit @make_program_get_module_function_prop.
eassumption.
inv MOK2; eassumption.
intros [[? ?] _]; simpl in ×.
destruct (instrs_OK (fn_code f)); [eauto|discriminate].
intros (? & Hsym & _).
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
}
{
eapply get_module_function_none_oplus in MOK1.
destruct MOK1 as [MOK11 MOK12].
rewrite get_layer_globalvar_oplus, get_semof_globalvar in Hiσ.
apply res_option_oplus_ok_some_inv in Hiσ.
destruct Hiσ as [[HMi HLi] | [HMi HLi]]; try congruence.
destruct MOK2 as [σ´ Hσ´].
rewrite get_module_variable_oplus in Hσ´.
rewrite HMi in Hσ´.
destruct (get_module_variable i CTXT) as [[|]|] eqn:HCi;
try discriminate.
exploit (make_globalenv_get_module_variable (D:=D)); eauto.
{
instantiate (2:=i).
get_module_normalize.
rewrite HCi, HMi.
reflexivity.
}
intros (? & Hsym & _).
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
}
}
}
× intros i σ Hiσ.
apply make_program_make_globalenv in MKP.
destruct (MOK i) as [MOK1 MOK2 _].
destruct MOK1 as [? MOK1].
specialize (get_module_function_oplus i CTXT M).
rewrite Hiσ. rewrite MOK1.
intros Hle.
destruct (get_module_function i M); try destruct o; inv_monad Hle.
exploit (make_globalenv_get_module_function (D:=D)); eauto.
exploit @make_program_get_module_function_prop.
eassumption.
inv MOK2; eassumption.
intros [[? ?] _]; simpl in ×.
destruct (instrs_OK (fn_code σ)); [eauto|discriminate].
intros (? & Hsym & _).
exploit (make_globalenv_stencil_matches (D:=D)); eauto.
intros Hsten. inv Hsten.
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
× intros i σ Hiσ.
apply make_program_make_globalenv in MKP.
destruct (MOK i) as [_ MOK1 _].
destruct MOK1 as [? MOK1].
specialize (get_module_variable_oplus i CTXT M).
rewrite Hiσ. rewrite MOK1.
intros Hle.
destruct (get_module_variable i M); try destruct o; inv_monad Hle.
exploit (make_globalenv_get_module_variable (D:=D)); eauto.
intros (? & Hsym & _).
exploit (make_globalenv_stencil_matches (D:=D)); eauto.
intros Hsten. inv Hsten.
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
Qed.
Lemma accessors_monotonic_plus_none {D: compatdata}
{L1 L2: compatlayer D}:
AccessorsDefined L1 →
cl_exec_load L2 = OK None →
cl_exec_store L2 = OK None →
AccessorsDefined (L2 ⊕ L1).
Proof.
intros.
apply accessors_defined_true in H.
econstructor.
unfold accessors_defined in ×.
simpl. rewrite H0, H1.
caseEq (cl_exec_load L1); intros; rewrite H2 in H; simpl in *; try discriminate.
destruct o; simpl in *; try discriminate.
caseEq (cl_exec_store L1); intros; rewrite H3 in H; simpl in *; try discriminate.
destruct o; simpl in *; try discriminate.
reflexivity.
Qed.
Lemma LayerOK_not_None `{D: compatdata} (L: compatlayer D):
∀ i,
LayerOK L →
¬isOKNone (get_layer_primitive i L) →
∃ func, get_layer_primitive i L = OK (Some func).
Proof.
intros. destruct (H i) as [[σ Hσ] _ _].
rewrite Hσ in *; clear Hσ.
destruct σ as [|]; eauto.
elim H0; reflexivity.
Qed.
Lemma LayerOK_elim `{D: compatdata} (L: compatlayer D):
∀ i v,
LayerOK L →
get_layer_globalvar i L = OK (Some v) →
get_layer_primitive i L = OK None.
Proof.
intros.
destruct (H i) as [Hlayer _ Hdisj].
rewrite H0 in Hdisj.
destruct Hdisj; try discriminate.
assumption.
Qed.
Instance lasm_semantics_names_match {D} (M: module) (L: compatlayer D):
LayerOK (〚M〛 L) →
LayerNamesMatch D (〚M〛 L).
Proof.
split.
× assumption.
× intros i j σ Hi Hj.
rewrite get_semof_primitive in Hi.
destruct (get_module_function i M) as [[|]|]; try discriminate.
inversion Hi; subst; clear Hi.
simpl in ×.
congruence.
Qed.
Instance layer_names_match_oplus {D} (L1 L2: compatlayer D):
LayerOK (L1 ⊕ L2) →
LayerNamesMatch D L1 →
LayerNamesMatch D L2 →
LayerNamesMatch D (L1 ⊕ L2).
Proof.
intros HLplus [HL1ok HL1match] [HL2ok HL2match].
split; try assumption.
intros i j σ Hi Hj.
specialize (HL1match i j σ).
specialize (HL2match i j σ).
edestruct (get_layer_primitive_oplus_either i L1 L2); eauto.
Qed.
End WITHLAYERS.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.PTreeSemantics.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import LAsmModuleSem.
Require Import LAsmModuleSemAux.
Require Import LAsmModuleSemMakeProgram.
Require Import LAsmModuleSemSim.
Require Import LAsmModuleSemInvariants.
Require Import LAsm.
Require Import CommonTactic.
Require Import InitMem.
Require Import RefinementTactic.
Require Import AuxLemma.
Section WITHLAYERS.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Context `{make_program_ops: !MakeProgramOps LAsm.function Ctypes.type LAsm.fundef unit}.
Context `{make_program_prf: !MakeProgram LAsm.function Ctypes.type LAsm.fundef unit}.
Inductive match_states {D1: compatdata} {D2: compatdata} {R: compatrel D1 D2}:
stencil → (state (mem:= mwd D1)) → (state (mem:= mwd D2)) → Prop :=
| match_states_intro:
∀ s f rs m d rs´ m´ d´,
MatchPrimcallStates R s f rs m d rs´ m´ d´ →
high_level_invariant d →
high_level_invariant d´ →
low_level_invariant (Mem.nextblock m´) d´ →
asm_invariant (mem:= mwd D2) s rs´ (m´, d´) →
match_states s (State rs (m, d)) (State rs´ (m´, d´)).
Lemma one_step_sim_monotonic_alt {D1: compatdata} {D2: compatdata}
{L1} {L2} {R: compatrel D1 D2}
`{acc_def_prf1: !AccessorsDefined L1}
`{names1: !LayerNamesMatch D1 L1}
`{acc_def_prf2: !AccessorsDefined L2}
`{names2: !LayerNamesMatch D2 L2}:
∀ `{memory_model_x: !Mem.MemoryModelX mem},
∀ `{extcall_inv_def_prf1: !ExtcallInvariantsAvailable L1},
∀ `{primcall_inv_def_prf1: !PrimcallInvariantsAvailable L1},
∀ `{extcall_inv_def_prf2: !ExtcallInvariantsAvailable L2},
∀ `{primcall_inv_def_prf2: !PrimcallInvariantsAvailable L2},
∀ `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet},
∀ (s: stencil) ge ge´ rs1 rs1´ m1 m1´ d1 d1´ rs2 m2 d2 t,
∀ (Hglobalenv: ∃ M, make_globalenv (D:=D2) s M L2 = OK ge´),
∀ (Hge_external´:
∀ b ef,
Genv.find_funct_ptr ge´ b = Some (External ef) →
∃ i sg, ef = EF_external i sg),
∀ (OKLayer: LayerOK L2),
∀ (ValidLayer: get_layer_prim_valid L2 s),
stencil_matches s ge →
stencil_matches s ge´ →
ge ≤ ge´ →
cl_sim D1 D2 (freerg_inj _ _ _ R) L1 L2 →
match_states s (State rs1 (m1, d1)) (State rs2 (m2, d2)) →
(step (lcfg_ops:= LC L1))
ge (State rs1 (m1, d1)) t (State rs1´ (m1´, d1´)) →
∃ rs2´ m2´ d2´,
(step (lcfg_ops:= LC L2))
ge´ (State rs2 (m2, d2)) t (State rs2´ (m2´, d2´))
∧ match_states s (State rs1´ (m1´, d1´)) (State rs2´ (m2´, d2´)).
Proof.
intros. inv H3.
exploit (one_step_sim_monotonic´_avail s ge ge´); eauto 1.
intros [f´[rs2´[m2´[d2´[Hstep[Hmatch[Hhigh[Hhigh´[Hlow Hasm]]]]]]]]].
refine_split´; eauto 2.
econstructor; eauto 2.
Qed.
Lemma get_module_function_oplus_ok_left i M1 M2 κ:
ModuleOK (M1 ⊕ M2) →
get_module_function i M1 = OK (Some κ) →
get_module_function i (M1 ⊕ M2) = OK (Some κ).
Proof.
intros HM HM1i.
assert (HMi: res_le (option_le eq) (get_module_function i M1)
(get_module_function i (M1 ⊕ M2))). {
apply get_module_function_monotonic.
apply left_upper_bound.
}
destruct (HM i) as [[κ´ Hκ´] _ _].
destruct HMi as [_ _ [|] | ]; try discriminate.
congruence.
Qed.
Lemma get_module_function_oplus_ok_right i M1 M2 κ:
ModuleOK (M1 ⊕ M2) →
get_module_function i M1 = OK (Some κ) →
get_module_function i (M1 ⊕ M2) = OK (Some κ).
Proof.
intros HM HM1i.
assert (HMi: res_le (option_le eq) (get_module_function i M1)
(get_module_function i (M1 ⊕ M2))). {
apply get_module_function_monotonic.
apply left_upper_bound.
}
destruct (HM i) as [[κ´ Hκ´] _ _].
destruct HMi as [_ _ [|] | ]; try discriminate.
congruence.
Qed.
Lemma res_option_oplus_none_inv {A} (x y: res (option A)):
x ⊕ y = OK None →
x = OK None ∧ y = OK None.
Proof.
destruct x as [[|]|], y as [[|]|];
inversion 1;
split;
reflexivity.
Qed.
Lemma get_module_function_oplus_ok_either i M1 M2 δ:
ModuleOK (M1 ⊕ M2) →
get_module_function i (M1 ⊕ M2) = OK δ →
(get_module_function i M1 = OK δ ∧ isOKNone (get_module_function i M2)) ∨
(isOKNone (get_module_function i M1) ∧ get_module_function i M2 = OK δ).
Proof.
intros HM Hi.
destruct (HM i) as [[f Hf] [v Hv] Hdisj].
revert Hdisj Hf Hv Hi.
get_module_normalize.
unfold isOKNone.
intros [Hdisj|Hdisj] Hf Hv Hδ;
apply res_option_oplus_none_inv in Hdisj;
destruct Hdisj as [H1 H2];
rewrite H1, H2 in ×.
× left.
split; [assumption|reflexivity].
× destruct (get_module_function i M1) as [[|]|];
destruct (get_module_function i M2) as [[|]|];
try discriminate.
+ left.
split; [assumption|reflexivity].
+ right.
split; [reflexivity|assumption].
+ left.
split; [assumption|reflexivity].
Qed.
Lemma get_layer_primitive_oplus_either {D} i L1 L2 σ:
get_layer_primitive (D:=D) i (L1 ⊕ L2) = OK (Some σ) →
get_layer_primitive i L1 = OK (Some σ) ∨
get_layer_primitive i L2 = OK (Some σ).
Proof.
get_layer_normalize.
destruct (get_layer_primitive i L1) as [[|]|];
destruct (get_layer_primitive i L2) as [[|]|];
try discriminate;
intros H.
× left; assumption.
× right; assumption.
Qed.
Lemma make_globalenv_module_ok {D} s M L:
isOK (make_globalenv (D:=D) s M L) →
ModuleOK M.
Proof.
intros [ge Hge].
unfold make_globalenv in Hge.
inv_monad Hge.
eapply make_program_module_ok.
∃ x.
eassumption.
Qed.
Lemma make_globalenv_vertical´ {D} `{L: compatlayer D}:
∀ s CTXT (M: module) ge ge´,
stencil_matches s ge →
stencil_matches s ge´ →
make_globalenv s CTXT (〚 M 〛 L ⊕ L) = ret ge
→ make_globalenv s (CTXT ⊕ M) L = ret ge´
→ (∀ b f, Genv.find_funct_ptr ge b = Some (Internal f)
→ Genv.find_funct_ptr ge´ b = Some (Internal f))
∧ (∀ b id sg,
isOKNone (get_module_function id M)
→ Genv.find_funct_ptr ge b = Some (External (EF_external id sg))
→ Genv.find_funct_ptr ge´ b = Some (External (EF_external id sg)))
∧ (∀ b id sg f,
get_module_function id M = OK (Some f) →
Genv.find_funct_ptr ge b = Some (External (EF_external id sg))
→ Genv.find_funct_ptr ge´ b = Some (Internal f)).
Proof.
intros until ge´.
intros Hsge Hsge´ Hge Hge´.
assert (MOK: ModuleOK (CTXT ⊕ M)).
{
eapply make_globalenv_module_ok.
eexists; eassumption.
}
split.
{
intros.
exploit @make_globalenv_find_funct_ptr.
{ eexact Hge. }
{ eassumption. }
destruct 1 as (j & SYMB & K).
destruct K as [K | K].
{
destruct K as (? & MOD & INT).
exploit @make_globalenv_get_module_function.
{ eexact Hge´. }
{
instantiate (2 := j).
instantiate (1 := f).
apply get_module_function_oplus_ok_left; eauto.
simpl in INT; destruct (instrs_OK (fn_code x)); congruence.
}
{
simpl in *; destruct (instrs_OK (fn_code x)) eqn:Heq; inv INT.
rewrite Heq; reflexivity.
}
destruct 1 as (b´ & SYMB´ & FUNCT´).
erewrite stencil_matches_symbols in SYMB by eauto using make_globalenv_stencil_matches.
erewrite stencil_matches_symbols in SYMB´ by eauto using make_globalenv_stencil_matches.
replace b´ with b in × by congruence.
assumption.
}
{
exfalso.
destruct K as (? & ? & ?). discriminate.
}
}
split.
{
intros.
exploit @make_globalenv_find_funct_ptr.
{ eexact Hge. }
{ eassumption. }
destruct 1 as (j & SYMB & K).
destruct K as [K | K].
{
exfalso.
destruct K as (x & ? & ?); simpl in *; destruct (instrs_OK (fn_code x)); congruence.
}
destruct K as (? & LAY & EXT).
edestruct (make_globalenv_get_layer_primitive s (CTXT ⊕ M) L ge´); eauto.
{
edestruct (get_layer_primitive_oplus_either j (〚M〛L) L);
try eassumption.
exfalso.
unfold isOKNone in H.
rewrite get_semof_primitive in H1.
unfold semof_function in H1.
inversion EXT; subst; clear EXT.
rewrite H in H1.
discriminate.
}
destruct H1 as [Hjx0 Hx0id].
erewrite stencil_matches_symbols in Hjx0 by eassumption.
erewrite stencil_matches_symbols in SYMB by eassumption.
congruence.
}
{
intros.
exploit @make_globalenv_find_funct_ptr.
{ eexact Hge. }
{ eassumption. }
destruct 1 as (j & SYMB & K).
destruct K as [K | K].
{
exfalso.
destruct K as (x & ? & ?); simpl in *; destruct (instrs_OK (fn_code x)); congruence.
}
destruct K as (? & LAY & EXT).
generalize EXT.
inversion 1; subst.
exploit @make_globalenv_get_module_function.
{ eexact Hge´. }
{
instantiate (2 := id).
instantiate (1 := f).
exploit @get_module_function_monotonic.
{
apply (right_upper_bound CTXT M).
}
instantiate (1 := id).
rewrite H.
inversion 1; subst.
{
inv H4.
inv H1.
inv H5.
× simpl in ×.
congruence.
× destruct (MOK id) as [[a Ha] _ _].
simpl in ×.
congruence.
}
exfalso.
symmetry in H4.
destruct (MOK id) as [MOK_FUN _ _].
generalize MOK_FUN.
simpl.
rewrite H4.
destruct 1; discriminate.
}
{
exploit @make_program_get_module_function_prop; [|eassumption|].
× unfold make_globalenv in Hge´; inv_monad Hge´.
rename H2 into Hmp; eapply make_program_monotonic_exists.
apply right_upper_bound.
reflexivity.
eassumption.
× intros [[? ?] [_ _]]; simpl in ×.
destruct (instrs_OK (fn_code f)); [eauto|discriminate].
}
destruct 1 as (b´ & SYMB´ & FUNCT´).
erewrite stencil_matches_symbols in SYMB by eauto using make_globalenv_stencil_matches.
erewrite stencil_matches_symbols in SYMB´ by eauto using make_globalenv_stencil_matches.
replace b´ with b in × by congruence.
assumption.
}
Qed.
Lemma res_option_oplus_some_inv {A} (x: A) (y: res (option A)) (z: A):
(OK (Some x)) ⊕ y = OK (Some z) →
x = z.
Proof.
intros H.
destruct y as [[|]|]; inversion H.
reflexivity.
Qed.
Lemma get_layer_primitive_right_eq´ {D} `{L: compatlayer D}:
∀ i (σ: compatsem D) M f,
get_layer_primitive i (〚 M 〛 L ⊕ L) = OK (Some σ) →
get_module_function i M = OK (Some f) →
LayerOK L →
semof_fundef D M L i f = OK σ.
Proof.
intros.
rewrite get_layer_primitive_oplus in H.
rewrite get_semof_primitive in H.
unfold semof_function in H.
rewrite H0 in H.
monad_norm.
destruct (semof_fundef _ _ _ _ _) as [σ´|err]; try discriminate.
monad_norm.
apply res_option_oplus_some_inv in H.
congruence.
Qed.
Lemma get_layer_primitive_right_neq´ {D} `{L: compatlayer D}:
∀ i (σi: compatsem D) M,
get_layer_primitive i (〚 M 〛 L ⊕ L) = OK (Some σi) →
isOKNone (get_module_function i M) →
get_layer_primitive i L = OK (Some σi).
Proof.
intros.
rewrite get_layer_primitive_oplus in H.
rewrite get_semof_primitive in H.
unfold isOKNone in *; rewrite H0 in H.
unfold semof_function in H.
monad_norm.
rewrite id_left in H.
assumption.
Qed.
Lemma one_step_vertical_composition {D} `{L: compatlayer D} {M}
(L_ACC_DEF: LAsm.AccessorsDefined L)
(L_NAMES: LayerNamesMatch D L)
(L_ACC_DEF´: LAsm.AccessorsDefined (〚M 〛 L ⊕ L)):
∀ s ge ge´ CTXT r r´ (m m´: mem) (d d´: D) t,
∀ (extinv: ExtcallInvariantsDefined L),
∀ (priminv: PrimcallInvariantsDefined L),
∀ (valid_prim: get_layer_prim_valid L s),
make_globalenv s CTXT (〚 M 〛 L ⊕ L) = ret ge
→ make_globalenv s (CTXT ⊕ M) L = ret ge´
→ step (lcfg_ops:= LC (〚 M 〛 L ⊕ L)) ge (State r (m, d)) t (State r´ (m´, d´))
→ plus (step (lcfg_ops:= LC L)) ge´
(State r (m, d)) t (State r´ (m´, d´)).
Proof.
intros. pose proof H0 as Hge_match´. pose proof H as Hge_match.
apply make_globalenv_stencil_matches in H0.
apply make_globalenv_stencil_matches in H.
pose proof H as Hge. pose proof H0 as Hge´.
inv H. inv H0.
assert (Hsymbol: ∀ i, Genv.find_symbol ge´ i = Genv.find_symbol ge i).
{
intros; abstract congruence.
}
unfold fundef in ×.
assert (Hgenv_next: Genv.genv_next ge´ = Genv.genv_next ge).
{
unfold fundef.
intros; abstract congruence.
}
assert(Hvolatile: ∀ b1 : block, block_is_volatile ge´ b1 = block_is_volatile ge b1).
{
unfold fundef.
intros; abstract congruence.
}
generalize Hge_match. intro HgeL_dup.
eapply make_globalenv_vertical´ in HgeL_dup; eauto.
destruct HgeL_dup as [Hinternal [Hext Hext´]].
assert (Hge_external´:
∀ b ef,
Genv.find_funct_ptr ge b = Some (External ef) →
∃ i sg, ef = EF_external i sg).
{
intros until ef; eapply ge_external_valid; eauto.
}
assert (mk_prog´: isOK (make_program s (CTXT ⊕ M) L)).
{
unfold make_globalenv in Hge_match´.
inv_monad Hge_match´.
esplit; eauto.
}
assert (mk_prog: isOK(make_program s M L)).
{
destruct mk_prog´ as [? mk_prog´].
eapply make_program_monotonic_exists; try eassumption; try reflexivity.
apply right_upper_bound.
}
assert (Hmoduleok: ModuleOK M).
{
eapply make_program_module_ok; eassumption.
}
assert (Hlayerok: LayerOK L).
{
eapply make_program_layer_ok; try eassumption.
}
assert (Hget: ∀ i,
(∃ func, get_module_function i M = OK (Some func))
∨ (isOKNone (get_module_function i M))).
{
intros.
destruct (Hmoduleok i) as [Hfun _ _].
revert Hfun.
destruct (get_module_function i M); eauto.
destruct o; eauto.
destruct 1.
discriminate.
}
eapply vcomp_step; try eapply H2; eauto 2; intros.
- assert(HW: acc_exec_load (〚M 〛 L ⊕ L) = acc_exec_load L).
{
unfold acc_exec_load.
destruct (acc_exec_load_strong (〚M 〛 L ⊕ L)).
simpl in e.
destruct (acc_exec_load_strong L).
rewrite e0 in e. abstract (inversion e; trivial).
}
rewrite <- HW.
erewrite exec_load_symbols_preserved; eauto.
- assert(HW´: acc_exec_store (〚M 〛 L ⊕ L) = acc_exec_store L).
{
unfold acc_exec_store.
destruct (acc_exec_store_strong (〚M 〛 L ⊕ L)).
simpl in e.
destruct (acc_exec_store_strong L).
rewrite e0 in e. abstract (inversion e; trivial).
}
rewrite <- HW´.
erewrite exec_store_symbols_preserved; eauto.
- eapply Hge_external´ in H.
destruct H as [?[? ?]]; subst. inv H0.
-
destruct (Hget i) as [?|?].
destruct H2 as [funcp ?].
specialize (Hext´ _ _ _ _ H2 H).
eapply (get_layer_primitive_right_eq´) in H0; eauto; subst.
inv H0.
split; eauto.
eapply get_layer_primitive_right_neq´; eauto.
-
destruct (Hget i) as [?|?].
+
destruct H5 as [funcp ?].
specialize (Hext´ _ _ _ _ H5 H).
eapply (get_layer_primitive_right_eq´) in H0; eauto. subst.
exploit (compatsem_primcall_le (D:= D)); eauto.
× reflexivity.
× econstructor; eauto.
× inv H0. simpl.
intros.
eapply stencil_matches_unique in H0; try apply Hge. subst.
destruct (Decision.decide (ExtcallInvariantsDefined L)).
destruct (Decision.decide (PrimcallInvariantsDefined L)).
destruct (Decision.decide (LayerNamesMatch D L)).
destruct (Decision.decide (get_layer_prim_valid L s1)).
rewrite accessors_defined_weak; try assumption.
destruct mk_prog as [? mk_prog].
rewrite mk_prog. reflexivity.
elim n; assumption.
elim n; assumption.
elim n; assumption.
elim n; assumption.
× intros Hsem´; inv Hsem´.
eapply stencil_matches_unique in H2; try apply Hge. subst.
inv H0; simpl in H4.
inv H4.
pose proof Hge0 as Hge0´.
apply make_globalenv_stencil_matches in Hge0.
apply make_globalenv_split_module_right in Hge_match´.
destruct Hge_match´ as [?[HgeL Hle´´]].
unfold fundef in ×.
rewrite Hge0´ in HgeL. inv HgeL.
eapply one_sim_plus; eauto. intros.
eapply one_step_monotonic; eauto.
+
exploit Hext; eauto. intros Hfind.
apply plus_one.
eapply exec_step_prim_call; eauto.
eapply get_layer_primitive_right_neq´ in H0; eauto.
econstructor; eauto.
refine_split´; eauto.
eapply stencil_matches_unique in H2; try apply Hge. subst.
econstructor; eauto.
Qed.
Remark annot_arguments_determ_with_data {D}:
∀ rs (m: mwd D) params args1 args2,
annot_arguments rs m params args1 → annot_arguments rs m params args2 → args1 = args2.
Proof.
unfold annot_arguments. intros. revert params args1 H args2 H0.
induction 1; intros.
inv H0; auto.
inv H1. decEq; eauto. inv H; inv H4. auto. congruence.
Qed.
Remark extcall_arguments_determ_with_data {D}:
∀ rs (m: mwd D) sg args1 args2,
extcall_arguments rs m sg args1 → extcall_arguments rs m sg args2 → args1 = args2.
Proof.
intros until m.
assert (∀ ll vl1, list_forall2 (extcall_arg rs m) ll vl1 →
∀ vl2, list_forall2 (extcall_arg rs m) ll vl2 → vl1 = vl2).
induction 1; intros vl2 EA; inv EA.
auto.
f_equal; auto.
inv H; inv H3; congruence.
intros. red in H0; red in H1. eauto.
Qed.
Lemma external_prim_false {D} `{L: compatlayer D}
(acc_def_prf: LAsm.AccessorsDefined L):
∀ ge ef WB args t1 t2 res (m m´ m´0: mwd D) rs rs´,
external_call´ (external_calls_ops:= compatlayer_extcall_ops L) WB ef ge args m t1 res m´ →
primitive_call (LayerConfigurationOps:= LC (acc_def_prf:= acc_def_prf) L) ef ge rs m t2 rs´ m´0 →
False.
Proof.
intros.
inv H. inv H0. destruct H as [?[?[?[? ?]]]]; subst.
simpl in ×. destruct H1 as [?[? ?]].
rewrite H in H0. inv H0.
inv H1. inv H2. destruct H0 as [?[?[?[? _]]]].
inv H4.
Qed.
Lemma make_program_ok_disjoint {D} s M L p:
make_program (D:=D) s M L = OK p →
module_layer_disjoint M L.
Proof.
intros.
unfold module_layer_disjoint.
assert (pOK: isOK (make_program s M L)).
{
esplit. eassumption.
}
intros i.
pose proof (make_program_layer_ok s M L pOK) as LOK.
destruct (LOK i) as [Lprim Lvar _].
destruct Lprim as [x Lprim].
destruct x.
{
left. eapply make_program_get_layer_primitive_prop; eassumption.
}
{
destruct Lvar as [? Lvar].
destruct x.
{
left. eapply make_program_get_layer_globalvar_prop; eassumption.
}
right.
rewrite Lprim, Lvar.
split; constructor.
}
Qed.
Lemma get_layer_primitive_semof {D} i M (L: compatlayer D) σ:
get_layer_primitive i (〚M〛 L ⊕ L) = OK (Some σ) →
(∃ σ´, get_layer_primitive i L = OK (Some σ´)) ∨
(∃ κ, get_module_function i M = OK (Some κ)).
Proof.
intros Hi.
edestruct (get_layer_primitive_oplus_either i (〚M〛L) L) as [H|H].
+ eassumption.
+ right.
rewrite get_semof_primitive in H.
unfold semof_function in H.
destruct (get_module_function i M) as [[|]|]; inversion H.
eauto.
+ left.
eauto.
Qed.
Lemma res_option_oplus_ok_inv {A} (x y: res (option A)) (z: option A):
x ⊕ y = OK z → (isOK x ∧ isOKNone y) ∨ (isOK y ∧ isOKNone x).
Proof.
destruct x as [[|]|], y as [[|]|]; try discriminate; eauto.
Qed.
Lemma res_option_oplus_ok_some_inv {A} (x y: res (option A)) (z: A):
x ⊕ y = OK (Some z) →
(x = OK (Some z) ∧ y = OK None) ∨
(x = OK None ∧ y = OK (Some z)).
Proof.
destruct x as [[|]|], y as [[|]|]; try discriminate; eauto.
Qed.
Lemma res_option_oplus_ok_none_inv {A} (x y: res (option A)):
isOKNone (x ⊕ y) →
isOKNone x ∧ isOKNone y.
Proof.
destruct x as [[|]|], y as [[|]|]; try discriminate; eauto.
Qed.
Lemma make_program_vertical´:
∀ D (LL: compatlayer D) s M CTXT p
(Hlayer_mo: LayerOK (〚 M 〛 LL ⊕ LL)),
make_program s (CTXT ⊕ M) LL = OK p
→ ∃ p´, make_program s CTXT (〚 M 〛 LL ⊕ LL) = OK p´.
Proof.
intros until p.
intros Hlayer_mo MKP.
assert (MKP´: isOK (make_program s (CTXT ⊕ M) LL))
by (rewrite MKP; unfold isOK; eauto).
pose proof (make_program_module_ok _ _ _ MKP´) as MOK.
pose proof (make_program_layer_ok _ _ _ MKP´) as LOK´.
apply make_program_exists; eauto.
× eapply module_ok_antitonic; eauto.
unfold flip.
apply left_upper_bound.
× intros i fe Hi.
specialize (get_layer_primitive_oplus i (〚M 〛 LL) LL).
intros Hle.
destruct (LOK´ i) as [Lprim Lvar _].
destruct Lprim as [? Lprim].
rewrite Lprim in Hle. rewrite Hi in Hle.
split; [eexists; reflexivity|].
destruct x.
{
exploit (make_program_get_layer_primitive_prop (D:=D)); eauto.
intros ( _ & Hmo & Hva).
split.
- eapply get_module_function_none_oplus in Hmo. eapply Hmo.
- eapply get_module_variable_none_oplus in Hva. eapply Hva.
}
{
destruct (MOK i) as [[κ Hκ] [τ Hτ] _].
get_module_normalize_in Hκ.
get_module_normalize_in Hτ.
clear Hi Lprim Lvar.
rewrite id_right in Hle.
split.
× rewrite get_semof_primitive in Hle.
destruct (get_module_function i M) as [[|]|]; try discriminate.
destruct (res_option_oplus_ok_inv _ _ _ Hκ) as [[HC HM] | [HM HC]].
- discriminate.
- assumption.
× destruct (MOK i) as [_ _ [Hf|Hv]].
- rewrite get_semof_primitive in Hle.
rewrite get_module_function_oplus in Hf.
destruct (get_module_function i M) as [[|]|]; try discriminate.
destruct (get_module_function i CTXT) as [[|]|]; try discriminate.
- rewrite get_module_variable_oplus in Hv.
destruct (get_module_variable i M) as [[|]|];
destruct (get_module_variable i CTXT) as [[|]|];
try discriminate.
reflexivity.
}
× intros i fi Hfi.
split.
{
exploit @make_program_get_module_function_prop.
+ eassumption.
+ destruct (MOK i) as [[? MOK1] _ _].
specialize (get_module_function_oplus i CTXT M).
rewrite Hfi, MOK1.
destruct (get_module_function i M) as [[|]|]; try discriminate.
intros H; inv H; eauto.
+ intuition.
}
destruct (MOK i) as [[κ MOK1] [τ MOK2] Mdisj].
specialize (get_module_function_oplus i CTXT M).
rewrite Hfi. rewrite MOK1.
destruct (get_module_function i M) as [[|]|] eqn:HMi; try discriminate.
intros H; inversion H; subst; clear H.
exploit (make_program_get_module_function_prop (D:=D)); eauto.
intros (Hfalse & Lprim & Lvar).
rewrite MOK1 in Mdisj.
destruct Mdisj as [Mvar|Mvar]; try discriminate.
get_layer_normalize.
unfold isOKNone in ×.
split.
+ rewrite get_semof_primitive.
rewrite HMi.
rewrite Lprim.
reflexivity.
+ rewrite get_semof_globalvar.
rewrite Lvar.
rewrite get_module_variable_oplus in Mvar.
destruct (get_module_variable i M) as [[|]|];
destruct (get_module_variable i CTXT) as [[|]|];
try discriminate.
reflexivity.
× intros i fi Hfi.
rewrite get_layer_globalvar_oplus in Hfi.
rewrite get_semof_globalvar in Hfi.
apply res_option_oplus_ok_some_inv in Hfi.
destruct Hfi as [[HMi HLi] | [HMi HLi]].
+ exploit (make_program_get_module_variable_prop s (CTXT ⊕ M) LL i fi); eauto.
- destruct (MOK i) as [_ [τ Hτ] _].
revert Hτ.
get_module_normalize.
rewrite HMi.
destruct (get_module_variable i CTXT) as [[|]|]; try discriminate.
reflexivity.
- intros (Hfi & Lprim & Lvar).
split;eauto.
split.
{
destruct (MOK i) as [_ _ CMdisj].
get_module_normalize_in CMdisj.
destruct CMdisj as [Hf|Hv].
- apply res_option_oplus_ok_none_inv in Hf.
destruct Hf.
assumption.
- apply res_option_oplus_ok_none_inv in Hv.
destruct Hv.
congruence.
}
{
destruct (MOK i) as [_ [τ CMvar] _].
get_module_normalize_in CMvar.
apply res_option_oplus_ok_inv in CMvar.
destruct CMvar as [[? ?] | [? ?]].
- congruence.
- assumption.
}
+ exploit (make_program_get_layer_globalvar_prop s (CTXT ⊕ M) LL i fi); eauto.
get_module_normalize.
intros (Hgvar & Hf & Hv).
split; eauto.
split.
- apply res_option_oplus_ok_none_inv in Hf.
destruct Hf.
assumption.
- apply res_option_oplus_ok_none_inv in Hv.
destruct Hv.
assumption.
× intros i fi Hfi.
destruct (MOK i) as [MOK1 [? MOK2]].
specialize (get_module_variable_oplus i CTXT M).
rewrite Hfi. rewrite MOK2.
intros Hle.
specialize (get_module_variable_isOK i CTXT M).
rewrite MOK2. intros HW.
exploit HW. esplit; reflexivity.
intros (_ & HM). clear HW.
destruct HM as [? HM].
rewrite HM in Hle.
destruct x0; inv_monad Hle.
exploit (make_program_get_module_variable_prop (D:=D)); eauto.
intros (Hfalse & Lprim & Lvar).
split; try assumption.
specialize (get_module_function_variable_disjoint (CTXT ⊕ M) i).
rewrite MOK2.
intros HW.
destruct HW as [HF|]; try discriminate.
get_module_normalize_in HF.
apply res_option_oplus_ok_none_inv in HF.
destruct HF as [_ HF].
get_layer_normalize.
rewrite get_semof_primitive.
rewrite get_semof_globalvar.
unfold isOKNone in ×.
subrewrite´.
split; reflexivity.
× intros i σ Hiσ.
apply make_program_make_globalenv in MKP.
destruct (get_layer_primitive_semof i M LL _ Hiσ) as [[σ´ Hσ´]|[κ Hκ]].
+ exploit (make_globalenv_get_layer_primitive s (CTXT ⊕ M) LL); eauto.
reflexivity.
intros (b & Hb & _).
erewrite stencil_matches_symbols in Hb.
eexists; eassumption.
eapply make_globalenv_stencil_matches; eauto.
+ exploit (make_globalenv_get_module_function s (CTXT ⊕ M) LL); eauto.
- instantiate (1:=κ); instantiate (1:=i).
destruct (MOK i) as [MOK´ _]; clear MOK.
destruct MOK´ as [? MOK].
specialize (get_module_function_oplus i CTXT M).
rewrite MOK. rewrite Hκ.
intros Hle.
Transparent oplus.
destruct (get_module_function i CTXT); try destruct o;
inv_monad Hle. reflexivity.
- exploit @make_program_get_module_function_prop.
eassumption.
destruct (MOK i) as [[? MOK1] _ _].
specialize (get_module_function_oplus i CTXT M).
rewrite Hκ, MOK1.
destruct (get_module_function i CTXT) as [[|]|]; try discriminate.
intros H; inv H; eauto.
intros [[? ?] _]; simpl in ×.
destruct (instrs_OK (fn_code κ)); [eauto|discriminate].
- intros (b & Hb & _).
eapply make_globalenv_stencil_matches in MKP; eauto.
inv MKP. rewrite stencil_matches_symbols in Hb.
rewrite Hb. esplit; reflexivity.
× intros i σ Hiσ.
apply make_program_make_globalenv in MKP.
destruct (LOK´ i) as [LOK1 LOK2].
destruct LOK2 as [? LOK2].
specialize (get_layer_globalvar_oplus i (〚M 〛 LL) LL).
rewrite Hiσ. rewrite LOK2.
intros Hle.
exploit (make_globalenv_stencil_matches (D:=D)); eauto.
intros Hsten. inv Hsten.
destruct x.
{
exploit (make_globalenv_get_layer_globalvar (D:=D)); eauto.
intros (? & Hsym & _).
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
}
{
destruct LOK1 as [? LOK1].
destruct x.
{
exploit (make_globalenv_get_layer_primitive (D:=D)); eauto.
reflexivity.
intros (? & Hsym & _).
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
}
{
destruct (MOK i) as [MOK1 MOK2].
destruct MOK1 as [? MOK1].
destruct x.
{
exploit (make_globalenv_get_module_function (D:=D)); eauto.
exploit @make_program_get_module_function_prop.
eassumption.
inv MOK2; eassumption.
intros [[? ?] _]; simpl in ×.
destruct (instrs_OK (fn_code f)); [eauto|discriminate].
intros (? & Hsym & _).
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
}
{
eapply get_module_function_none_oplus in MOK1.
destruct MOK1 as [MOK11 MOK12].
rewrite get_layer_globalvar_oplus, get_semof_globalvar in Hiσ.
apply res_option_oplus_ok_some_inv in Hiσ.
destruct Hiσ as [[HMi HLi] | [HMi HLi]]; try congruence.
destruct MOK2 as [σ´ Hσ´].
rewrite get_module_variable_oplus in Hσ´.
rewrite HMi in Hσ´.
destruct (get_module_variable i CTXT) as [[|]|] eqn:HCi;
try discriminate.
exploit (make_globalenv_get_module_variable (D:=D)); eauto.
{
instantiate (2:=i).
get_module_normalize.
rewrite HCi, HMi.
reflexivity.
}
intros (? & Hsym & _).
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
}
}
}
× intros i σ Hiσ.
apply make_program_make_globalenv in MKP.
destruct (MOK i) as [MOK1 MOK2 _].
destruct MOK1 as [? MOK1].
specialize (get_module_function_oplus i CTXT M).
rewrite Hiσ. rewrite MOK1.
intros Hle.
destruct (get_module_function i M); try destruct o; inv_monad Hle.
exploit (make_globalenv_get_module_function (D:=D)); eauto.
exploit @make_program_get_module_function_prop.
eassumption.
inv MOK2; eassumption.
intros [[? ?] _]; simpl in ×.
destruct (instrs_OK (fn_code σ)); [eauto|discriminate].
intros (? & Hsym & _).
exploit (make_globalenv_stencil_matches (D:=D)); eauto.
intros Hsten. inv Hsten.
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
× intros i σ Hiσ.
apply make_program_make_globalenv in MKP.
destruct (MOK i) as [_ MOK1 _].
destruct MOK1 as [? MOK1].
specialize (get_module_variable_oplus i CTXT M).
rewrite Hiσ. rewrite MOK1.
intros Hle.
destruct (get_module_variable i M); try destruct o; inv_monad Hle.
exploit (make_globalenv_get_module_variable (D:=D)); eauto.
intros (? & Hsym & _).
exploit (make_globalenv_stencil_matches (D:=D)); eauto.
intros Hsten. inv Hsten.
rewrite stencil_matches_symbols in Hsym.
rewrite Hsym. esplit; reflexivity.
Qed.
Lemma accessors_monotonic_plus_none {D: compatdata}
{L1 L2: compatlayer D}:
AccessorsDefined L1 →
cl_exec_load L2 = OK None →
cl_exec_store L2 = OK None →
AccessorsDefined (L2 ⊕ L1).
Proof.
intros.
apply accessors_defined_true in H.
econstructor.
unfold accessors_defined in ×.
simpl. rewrite H0, H1.
caseEq (cl_exec_load L1); intros; rewrite H2 in H; simpl in *; try discriminate.
destruct o; simpl in *; try discriminate.
caseEq (cl_exec_store L1); intros; rewrite H3 in H; simpl in *; try discriminate.
destruct o; simpl in *; try discriminate.
reflexivity.
Qed.
Lemma LayerOK_not_None `{D: compatdata} (L: compatlayer D):
∀ i,
LayerOK L →
¬isOKNone (get_layer_primitive i L) →
∃ func, get_layer_primitive i L = OK (Some func).
Proof.
intros. destruct (H i) as [[σ Hσ] _ _].
rewrite Hσ in *; clear Hσ.
destruct σ as [|]; eauto.
elim H0; reflexivity.
Qed.
Lemma LayerOK_elim `{D: compatdata} (L: compatlayer D):
∀ i v,
LayerOK L →
get_layer_globalvar i L = OK (Some v) →
get_layer_primitive i L = OK None.
Proof.
intros.
destruct (H i) as [Hlayer _ Hdisj].
rewrite H0 in Hdisj.
destruct Hdisj; try discriminate.
assumption.
Qed.
Instance lasm_semantics_names_match {D} (M: module) (L: compatlayer D):
LayerOK (〚M〛 L) →
LayerNamesMatch D (〚M〛 L).
Proof.
split.
× assumption.
× intros i j σ Hi Hj.
rewrite get_semof_primitive in Hi.
destruct (get_module_function i M) as [[|]|]; try discriminate.
inversion Hi; subst; clear Hi.
simpl in ×.
congruence.
Qed.
Instance layer_names_match_oplus {D} (L1 L2: compatlayer D):
LayerOK (L1 ⊕ L2) →
LayerNamesMatch D L1 →
LayerNamesMatch D L2 →
LayerNamesMatch D (L1 ⊕ L2).
Proof.
intros HLplus [HL1ok HL1match] [HL2ok HL2match].
split; try assumption.
intros i j σ Hi Hj.
specialize (HL1match i j σ).
specialize (HL2match i j σ).
edestruct (get_layer_primitive_oplus_either i L1 L2); eauto.
Qed.
End WITHLAYERS.