Library mcertikos.layerlib.Soundness
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.
Require Export SoundnessAux.
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}.
Local Existing Instance lasm_semantics_names_match.
Local Existing Instance layer_names_match_oplus.
Local Existing Instance extcall_invariants_oplus.
Local Existing Instance primcall_invariants_oplus.
Lemma lasm_semantics_receptive (ph: program) DH (LH: compatlayer DH) `{is: !AsmInitialState (mwd DH)}:
∀
(LH_ACC_DEF: LAsm.AccessorsDefined LH)
(LH_RECEPT: ExternalCallsXDefined (LH)),
receptive (LAsm.semantics (lcfg_ops := LC LH) ph).
Proof.
intros.
assert(externalcall_prf: ExternalCalls (mwd DH)
(external_calls_ops:= compatlayer_extcall_ops LH)).
{
eapply compatlayer_extcall_strong; assumption.
}
split.
inversion 1; subst.
+ inversion 1; subst; eauto.
+ intros. inv H3.
exploit (external_call_receptive
(mem:= mwd DH)
(external_calls_ops:= compatlayer_extcall_ops LH)); eauto.
intros [? [? ?]]. esplit. econstructor; eauto. econstructor; eauto.
+ intros. inv H4.
exploit (external_call_receptive
(mem:= mwd DH)
(external_calls_ops:= compatlayer_extcall_ops LH)); eauto.
intros [? [? ?]]. esplit. eapply exec_step_annot; eauto. econstructor; eauto.
+ intros. inv H3.
exploit (external_call_receptive
(mem:= mwd DH)
(external_calls_ops:= compatlayer_extcall_ops LH)); eauto.
intros [? [? ?]]. esplit. eapply exec_step_external; eauto. econstructor; eauto.
+ intros. pose proof H2 as Hprim. inv Hprim.
destruct H4 as [?[?[?[? Hsem]]]]; subst.
inv Hsem. inv H3.
esplit. eapply exec_step_prim_call; eauto.
+
red; intros; inv H; simpl.
omega.
inv H3. eapply external_call_trace_length; eauto.
inv H4. eapply external_call_trace_length; eauto.
inv H3. eapply external_call_trace_length; eauto.
inv H2. destruct H as [?[?[?[? Hsem]]]]; subst.
inv Hsem. simpl. omega.
Qed.
Lemma primcall_determ {DL} {LL: compatlayer DL} {ef ge rs m t1 rs1 m1 t2 rs2 m2}:
∀ `{Had: !AccessorsDefined LL},
primitive_call (LayerConfigurationOps := LC LL) ef ge rs m t1 rs1 m1 →
primitive_call (LayerConfigurationOps := LC LL) ef ge rs m t2 rs2 m2 →
PrimitiveCallsXDefined LL →
t1 = E0 ∧ t2 = E0 ∧ State rs1 m1 = State rs2 m2.
Proof.
intros Had Hpc1 Hpc2 Hdet.
destruct Hpc1 as (i1 & sg1 & σ1 & Hef1 & Hσ1 & Hstep1).
destruct Hstep1 as [σ1 ge1 s1 rs1 m1 rs1´ m1´ Hs1 Hstep1].
destruct Hpc2 as (i2 & sg2 & σ2 & Hef2 & Hσ2 & Hstep2).
destruct Hstep2 as [σ2 ge2 s2 rs2 m2 rs2´ m2´ Hs2 Hstep2].
split; eauto.
split; eauto.
assert (s1 = s2) by eauto using stencil_matches_unique.
rewrite Hef2 in Hef1; inv Hef1.
rewrite Hσ2 in Hσ1; inv Hσ1.
specialize (Hdet i1).
rewrite Hσ2 in Hdet.
simpl in Hdet.
destruct (sprimcall_props DL σ1); try discriminate.
destruct (primitive_call_determ s2 rs2 m2 rs1´ m1´ rs2´ m2´); eauto.
congruence.
Qed.
Lemma lasm_semantics_determinate (pl: program) DL (LL: compatlayer DL) `{is: !AsmInitialState (mwd DL)}:
∀
(LL_ACC_DEF: LAsm.AccessorsDefined LL)
(LL_RECEPT: ExternalCallsXDefined (LL))
(LL_DETERM´: PrimitiveCallsXDefined LL),
determinate (LAsm.semantics (lcfg_ops := LC LL) pl).
Proof.
intros.
assert(externalcall_prf: ExternalCalls (mwd DL)
(external_calls_ops:= compatlayer_extcall_ops LL)).
{
eapply compatlayer_extcall_strong; assumption.
}
intros; constructor; simpl; intros.
+
inv H; inv H0; Equalities.
× split. constructor. auto.
× discriminate.
× discriminate.
× inv H11.
× inv H4. inv H9.
specialize (Events.external_call_determ (external_calls_ops:= compatlayer_extcall_ops LL)
_ _ _ _ _ _ _ _ _ _ _ H H0).
intros [? ?]. esplit; eauto.
intros. destruct H4 as [? ?]; subst; trivial.
× discriminate.
× inv H5. inv H13.
assert (vargs0 = vargs) by (eapply annot_arguments_determ_with_data; eauto). subst.
specialize (Events.external_call_determ (external_calls_ops:= compatlayer_extcall_ops LL)
_ _ _ _ _ _ _ _ _ _ _ H H0).
intros [? ?]. esplit; eauto.
intros. destruct H5 as [? ?]; subst; trivial.
× inv H4. inv H9.
assert (args0 = args) by (eapply extcall_arguments_determ_with_data; eauto). subst.
specialize (Events.external_call_determ (external_calls_ops:= compatlayer_extcall_ops LL)
_ _ _ _ _ _ _ _ _ _ _ H H0).
intros [? ?]. esplit; eauto.
intros. destruct H4 as [? ?]; subst; trivial.
× specialize (external_prim_false _ _ _ _ _ _ _ _ _ _ _ _ _ H4 H10).
intros HF; inv HF.
× specialize (external_prim_false _ _ _ _ _ _ _ _ _ _ _ _ _ H8 H3).
intros HF; inv HF.
× destruct (primcall_determ H3 H9) as (Ht1 & Ht2 & H); eauto.
subst.
split; [constructor | eauto].
+
red; intros; inv H; simpl.
omega.
inv H3. eapply external_call_trace_length; eauto.
inv H4. eapply external_call_trace_length; eauto.
inv H3. eapply external_call_trace_length; eauto.
inv H2. destruct H as [?[?[?[? Hsem]]]]; subst.
inv Hsem. simpl. omega.
+
eapply asm_init_state_determ; eauto.
+
contradiction.
+
contradiction.
Qed.
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.
Require Export SoundnessAux.
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}.
Local Existing Instance lasm_semantics_names_match.
Local Existing Instance layer_names_match_oplus.
Local Existing Instance extcall_invariants_oplus.
Local Existing Instance primcall_invariants_oplus.
Lemma lasm_semantics_receptive (ph: program) DH (LH: compatlayer DH) `{is: !AsmInitialState (mwd DH)}:
∀
(LH_ACC_DEF: LAsm.AccessorsDefined LH)
(LH_RECEPT: ExternalCallsXDefined (LH)),
receptive (LAsm.semantics (lcfg_ops := LC LH) ph).
Proof.
intros.
assert(externalcall_prf: ExternalCalls (mwd DH)
(external_calls_ops:= compatlayer_extcall_ops LH)).
{
eapply compatlayer_extcall_strong; assumption.
}
split.
inversion 1; subst.
+ inversion 1; subst; eauto.
+ intros. inv H3.
exploit (external_call_receptive
(mem:= mwd DH)
(external_calls_ops:= compatlayer_extcall_ops LH)); eauto.
intros [? [? ?]]. esplit. econstructor; eauto. econstructor; eauto.
+ intros. inv H4.
exploit (external_call_receptive
(mem:= mwd DH)
(external_calls_ops:= compatlayer_extcall_ops LH)); eauto.
intros [? [? ?]]. esplit. eapply exec_step_annot; eauto. econstructor; eauto.
+ intros. inv H3.
exploit (external_call_receptive
(mem:= mwd DH)
(external_calls_ops:= compatlayer_extcall_ops LH)); eauto.
intros [? [? ?]]. esplit. eapply exec_step_external; eauto. econstructor; eauto.
+ intros. pose proof H2 as Hprim. inv Hprim.
destruct H4 as [?[?[?[? Hsem]]]]; subst.
inv Hsem. inv H3.
esplit. eapply exec_step_prim_call; eauto.
+
red; intros; inv H; simpl.
omega.
inv H3. eapply external_call_trace_length; eauto.
inv H4. eapply external_call_trace_length; eauto.
inv H3. eapply external_call_trace_length; eauto.
inv H2. destruct H as [?[?[?[? Hsem]]]]; subst.
inv Hsem. simpl. omega.
Qed.
Lemma primcall_determ {DL} {LL: compatlayer DL} {ef ge rs m t1 rs1 m1 t2 rs2 m2}:
∀ `{Had: !AccessorsDefined LL},
primitive_call (LayerConfigurationOps := LC LL) ef ge rs m t1 rs1 m1 →
primitive_call (LayerConfigurationOps := LC LL) ef ge rs m t2 rs2 m2 →
PrimitiveCallsXDefined LL →
t1 = E0 ∧ t2 = E0 ∧ State rs1 m1 = State rs2 m2.
Proof.
intros Had Hpc1 Hpc2 Hdet.
destruct Hpc1 as (i1 & sg1 & σ1 & Hef1 & Hσ1 & Hstep1).
destruct Hstep1 as [σ1 ge1 s1 rs1 m1 rs1´ m1´ Hs1 Hstep1].
destruct Hpc2 as (i2 & sg2 & σ2 & Hef2 & Hσ2 & Hstep2).
destruct Hstep2 as [σ2 ge2 s2 rs2 m2 rs2´ m2´ Hs2 Hstep2].
split; eauto.
split; eauto.
assert (s1 = s2) by eauto using stencil_matches_unique.
rewrite Hef2 in Hef1; inv Hef1.
rewrite Hσ2 in Hσ1; inv Hσ1.
specialize (Hdet i1).
rewrite Hσ2 in Hdet.
simpl in Hdet.
destruct (sprimcall_props DL σ1); try discriminate.
destruct (primitive_call_determ s2 rs2 m2 rs1´ m1´ rs2´ m2´); eauto.
congruence.
Qed.
Lemma lasm_semantics_determinate (pl: program) DL (LL: compatlayer DL) `{is: !AsmInitialState (mwd DL)}:
∀
(LL_ACC_DEF: LAsm.AccessorsDefined LL)
(LL_RECEPT: ExternalCallsXDefined (LL))
(LL_DETERM´: PrimitiveCallsXDefined LL),
determinate (LAsm.semantics (lcfg_ops := LC LL) pl).
Proof.
intros.
assert(externalcall_prf: ExternalCalls (mwd DL)
(external_calls_ops:= compatlayer_extcall_ops LL)).
{
eapply compatlayer_extcall_strong; assumption.
}
intros; constructor; simpl; intros.
+
inv H; inv H0; Equalities.
× split. constructor. auto.
× discriminate.
× discriminate.
× inv H11.
× inv H4. inv H9.
specialize (Events.external_call_determ (external_calls_ops:= compatlayer_extcall_ops LL)
_ _ _ _ _ _ _ _ _ _ _ H H0).
intros [? ?]. esplit; eauto.
intros. destruct H4 as [? ?]; subst; trivial.
× discriminate.
× inv H5. inv H13.
assert (vargs0 = vargs) by (eapply annot_arguments_determ_with_data; eauto). subst.
specialize (Events.external_call_determ (external_calls_ops:= compatlayer_extcall_ops LL)
_ _ _ _ _ _ _ _ _ _ _ H H0).
intros [? ?]. esplit; eauto.
intros. destruct H5 as [? ?]; subst; trivial.
× inv H4. inv H9.
assert (args0 = args) by (eapply extcall_arguments_determ_with_data; eauto). subst.
specialize (Events.external_call_determ (external_calls_ops:= compatlayer_extcall_ops LL)
_ _ _ _ _ _ _ _ _ _ _ H H0).
intros [? ?]. esplit; eauto.
intros. destruct H4 as [? ?]; subst; trivial.
× specialize (external_prim_false _ _ _ _ _ _ _ _ _ _ _ _ _ H4 H10).
intros HF; inv HF.
× specialize (external_prim_false _ _ _ _ _ _ _ _ _ _ _ _ _ H8 H3).
intros HF; inv HF.
× destruct (primcall_determ H3 H9) as (Ht1 & Ht2 & H); eauto.
subst.
split; [constructor | eauto].
+
red; intros; inv H; simpl.
omega.
inv H3. eapply external_call_trace_length; eauto.
inv H4. eapply external_call_trace_length; eauto.
inv H3. eapply external_call_trace_length; eauto.
inv H2. destruct H as [?[?[?[? Hsem]]]]; subst.
inv Hsem. simpl. omega.
+
eapply asm_init_state_determ; eauto.
+
contradiction.
+
contradiction.
Qed.
The soundness theorem needs to know that the two instances of
AsmInitialState are compatible in the following sense.
Class AsmInitialStatesCompatible D1 D2 (R : compatrel D1 D2) CTXT LH M LL
`{is1: !AsmInitialState (mwd D1)}
`{is2: !AsmInitialState (mwd D2)} :=
{
asm_init_state_match (s: stencil) (p1 p2 : AST.program _ _) s1:
make_program s CTXT LH = OK p1 →
make_program s (CTXT ⊕ M) LL = OK p2 →
LayerOK (〚 M 〛 LL ⊕ LL) →
stencil_matches s (Genv.globalenv p1) →
stencil_matches s (Genv.globalenv p2) →
prog_main p1 = prog_main p2 →
prog_defs_le (prog_defs p1) (prog_defs p2) →
cl_sim _ _ (freerg_inj _ _ _ R) LH (〚 M 〛 LL ⊕ LL) →
cl_init_sim_def D1 D2 R LH M LL →
asm_init_state p1 s1 →
∃ s2,
asm_init_state p2 s2 ∧
match_states (R := R) s s1 s2
}.
We show that the default initial states are indeed compatible.
Global Instance asm_init_default_compat DH DL R CTXT LH M LL:
AsmInitialStatesCompatible DH DL R CTXT LH M LL.
Proof.
constructor.
intros s ph pl s1 Hph Hpl HLOK Hge1 Hge2 Hprog_main Hprog_defs REFINE INIT_SIM Hs1.
destruct Hs1.
rename H into H0.
assert (Hinit_mem_exists: ∃ m´: mwd DL, Genv.init_mem pl = Some m´).
{
eapply (Genv.init_mem_exists pl).
intros.
exploit (make_program_gvar (D:=DL)); try eassumption.
intros [vi[Hg Hor]].
inv INIT_SIM.
destruct Hor as [Hor|Hor].
- specialize (get_module_variable_oplus i CTXT M).
rewrite Hor. intros Hle.
simpl in Hle.
caseEq (get_module_variable i CTXT); intros;
rewrite H1 in Hle; try destruct o;
caseEq (get_module_variable i M); intros;
rewrite H2 in Hle; try destruct o; inv_monad Hle;
try discriminate; inv H4.
+ rewrite (Genv.init_data_list_valid_symbols_preserved _ (Genv.globalenv ph)).
× specialize (Genv.init_mem_valid _ _ H0).
intros HW. specialize (HW i (globvar_map make_varinfo vi)).
apply HW.
eapply make_program_get_module_variable; try eassumption.
× intros. erewrite !stencil_matches_symbols by eauto. congruence.
+ simpl. eauto 2.
- specialize (cl_init_sim_low i).
congruence.
}
destruct Hinit_mem_exists as [? ?].
destruct m0, x. erewrite init_mem_with_data in H0.
assert(Hcl_init_mem: cl_init_sim_mem DH DL R s m0).
{
inv INIT_SIM.
eapply cl_init_sim_init_mem with (CTXT:= CTXT) ; eauto.
erewrite Hpl. erewrite init_mem_with_data in H.
caseEq (Genv.init_mem pl); intros; rewrite H1 in H; try discriminate.
inv H. rewrite <- H1.
reflexivity.
}
pose proof H as Hinit_mem´.
erewrite init_mem_with_data in H.
caseEq (Genv.init_mem ph); intros; rewrite H1 in H0; contra_inv.
caseEq (Genv.init_mem pl); intros; rewrite H2 in H; contra_inv.
inv H. inv H0.
exploit (Genv.init_mem_le_genv_next _ _ Hprog_defs); eauto.
intros Hnextblock.
assert(Hgenv_next: Mem.nextblock m = genv_next s).
{
eapply Genv.init_mem_genv_next in H1.
rewrite <- H1.
eauto using stencil_matches_genv_next.
}
assert(Hgenv_next´: Mem.nextblock m0 = genv_next s).
{
eapply Genv.init_mem_genv_next in H2.
rewrite <- H2.
eauto using stencil_matches_genv_next.
}
assert (Hval_inj: ∀ reg,
(val_inject (Mem.flat_inj (genv_next s)))
(Pregmap.get reg (Pregmap.init Vundef))
(Pregmap.get reg (Pregmap.init Vundef))).
{
intros. unfold Pregmap.get. rewrite Pregmap.gi.
constructor.
}
esplit. split; eauto.
econstructor; eauto.
subst rs0.
econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
×
rewrite <- Hgenv_next.
exploit (Genv.init_mem_le_inject _ _ Hprog_defs); eauto.
×
eapply cl_init_sim_relate; eauto.
×
eapply cl_init_sim_match; eauto.
×
unfold Mem.flat_inj. intros.
destruct (plt b1 (genv_next s)); contra_inv.
inv H. split; reflexivity.
×
rewrite Hnextblock. xomega.
×
inv INIT_SIM.
red; intros. specialize (cl_init_sim_glbl _ H).
apply make_program_make_globalenv in Hph.
assert (HmOK: ModuleOK (CTXT ⊕ M)).
{
eapply make_program_module_ok.
esplit; eauto.
}
assert (MOK: ModuleOK M).
{
eapply module_ok_antitonic; try eassumption.
apply right_upper_bound.
}
eapply Genv.init_mem_no_perm; eauto.
erewrite stencil_matches_symbols; now eauto.
{
caseEq (Genv.find_funct_ptr (Genv.globalenv ph) b); intros; try reflexivity.
{
eapply make_globalenv_find_funct_ptr in H4; eauto.
destruct H4 as [i0[Hf Hmo]].
erewrite stencil_matches_symbols in Hf by eauto.
specialize (genv_vars_inj _ _ _ _ H0 Hf).
intros; subst.
specialize (cl_init_sim_glbl_module _ H).
destruct cl_init_sim_glbl_module as [vi Hmo´].
destruct Hmo as [ Hmo| Hmo].
{
destruct Hmo as [i´[Hmo _]].
destruct (HmOK i0) as [Hmog Hmov HNone].
destruct HNone.
{
unfold isOKNone in ×.
rewrite get_module_function_oplus in H4.
rewrite Hmo in H4.
destruct (get_module_function i0 M) as [[|]|]; discriminate.
}
{
specialize (get_module_variable_oplus i0 CTXT M).
unfold isOKNone in H4. rewrite H4.
rewrite Hmo´. intros Hle. simpl in Hle.
destruct (get_module_variable i0 CTXT) as [[|]|]; discriminate.
}
}
inv REFINE.
eapply cl_sim_layer_pointwise in cl_sim_layer.
destruct Hmo as [fe[Hmo _]].
destruct cl_sim_layer as [cl_layer _].
specialize (cl_layer i0).
rewrite Hmo in cl_layer.
assert (¬ isOKNone (get_layer_primitive i0 (〚M 〛 LL ⊕ LL))).
{
simpl; inv cl_layer; try discriminate.
inv H6. discriminate.
}
exploit (LayerOK_not_None (D:= DL)); eauto.
intros [func Hl].
specialize (get_layer_primitive_oplus i0 (〚M 〛 LL) LL).
rewrite Hl. intros Hle.
caseEq (get_layer_primitive i0 LL); intros;
rewrite H5 in Hle; try destruct o;
caseEq (get_layer_primitive i0 (〚M 〛 LL)); intros;
rewrite H6 in Hle; try destruct o; inv Hle.
{
specialize (cl_init_sim_glbl_prim _ H).
rewrite Hmo in cl_init_sim_glbl_prim.
inv cl_init_sim_glbl_prim.
}
{
destruct (MOK i0) as [MOK1 MOK2 _].
exploit get_module_function_variable_disjoint; eauto.
intros HT. inv HT.
{
rewrite get_semof_primitive in H6.
unfold isOKNone in H7; rewrite H7 in H6.
discriminate.
}
{
rewrite Hmo´ in H7. inv H7.
}
}
}
}
{
caseEq (Genv.find_var_info (Genv.globalenv ph) b); intros; try reflexivity.
{
eapply make_globalenv_find_var_info in H4; eauto.
destruct H4 as [i0[Hf Hmo]].
destruct Hmo as [vi0[_ Hmo]].
erewrite stencil_matches_symbols in Hf by eauto.
specialize (genv_vars_inj _ _ _ _ H0 Hf).
intros; subst.
specialize (cl_init_sim_glbl_module _ H).
destruct cl_init_sim_glbl_module as [vi Hmo´].
destruct Hmo as [ Hmo| Hmo].
{
destruct (HmOK i0) as [_ Hmov _].
specialize (get_module_variable_oplus i0 CTXT M).
rewrite Hmo. rewrite Hmo´.
destruct Hmov as [? Hmov]. rewrite Hmov.
intros Hle. inv Hle.
}
rewrite Hmo in cl_init_sim_glbl.
inv cl_init_sim_glbl.
}
}
×
intros. rewrite Hgenv_next.
eapply genv_symb_range in H0.
xomega.
×
val_inject_simpl.
simpl.
unfold symbol_offset.
erewrite !stencil_matches_symbols by eauto.
rewrite Hprog_main.
caseEq (find_symbol s (prog_main pl)); intros.
assert (Mem.flat_inj (genv_next s) b = Some (b, 0%Z)).
{
eapply stencil_find_symbol_inject´; eauto.
}
econstructor; eauto.
constructor.
×
eapply empty_data_high_level_invariant.
×
eapply empty_data_high_level_invariant.
×
eapply empty_data_low_level_invariant.
×
split; eauto.
econstructor; eauto.
lift_unfold. rewrite Hgenv_next´. xomega.
lift_unfold. eapply Genv.initmem_inject_neutral; eauto.
lift_unfold. rewrite Hgenv_next´.
val_inject_simpl.
unfold symbol_offset.
erewrite stencil_matches_symbols by eauto.
caseEq (find_symbol s (prog_main pl)); intros.
assert (Mem.flat_inj (genv_next s) b = Some (b, 0%Z)).
{
eapply stencil_find_symbol_inject´; eauto.
}
econstructor; eauto.
constructor.
repeat (eapply AsmX.set_reg_wt; try constructor).
simpl.
unfold symbol_offset.
destruct (Genv.find_symbol (Genv.globalenv pl) (prog_main pl)); constructor.
Qed.
Now, we first prove a generic version of the soundness theorem
that works with any kinds of compatible initial states.
Theorem soundness_generic:
∀ {DH DL: compatdata}
(R: compatrel DH DL)
`{ish: !AsmInitialState (mwd DH)}
`{isl: !AsmInitialState (mwd DL)}
(LH: compatlayer DH)
(LL: compatlayer DL)
(LH_ACC_DEF: LAsm.AccessorsDefined LH)
(LL_ACC_DEF: LAsm.AccessorsDefined LL)
(LH_RECEPT: ExternalCallsXDefined (LH))
(LL_DETERM: ExternalCallsXDefined (LL))
(LL_DETERM´: PrimitiveCallsXDefined LL)
(LH_INV: ExtcallInvariantsDefined LH)
(LL_INV: ExtcallInvariantsDefined LL)
(LH_PRIM_INV: PrimcallInvariantsDefined LH)
(LL_PRIM_INV: PrimcallInvariantsDefined LL)
(LH_NAMES: LayerNamesMatch DH LH)
(LL_NAMSE: LayerNamesMatch DL LL)
(M: LAsm.module)
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet)
(REFINE: cl_sim _ _ (freerg_inj _ _ _ R) LH (〚 M 〛 LL ⊕ LL))
(INIT_SIM: cl_init_sim _ _ (freerg_inj _ _ _ R) LH M LL)
(CTXT: LAsm.module) s pl
(PL: make_program s (CTXT ⊕ M) LL = OK pl)
(prim_valid: get_layer_prim_valid LL s)
ph
(PH: make_program s CTXT LH = OK ph)
(His: AsmInitialStatesCompatible DH DL R CTXT LH M LL)
(HLayerOK´: LayerOK (〚 M 〛 LL ⊕ LL)),
backward_simulation
(LAsm.semantics (lcfg_ops := LC LH) ph)
(LAsm.semantics (lcfg_ops := LC LL) pl).
Proof.
intros.
assert (acc_def_prf2: AccessorsDefined (〚M 〛 LL ⊕ LL)).
{
eapply accessors_monotonic_plus_none; try assumption; simpl; reflexivity.
}
eapply forward_to_backward_simulation; eauto.
-
eapply forward_simulation_plus with (match_states:= match_states s).
+
intros.
assert (Hge: make_globalenv s (CTXT ⊕ M) LL = ret (Genv.globalenv pl)).
{
unfold make_globalenv. rewrite PL.
reflexivity.
}
assert (Hge´: make_globalenv s CTXT LH = ret (Genv.globalenv ph)).
{
unfold make_globalenv. rewrite PH.
reflexivity.
}
apply make_globalenv_stencil_matches in Hge.
apply make_globalenv_stencil_matches in Hge´.
inv Hge. inv Hge´.
erewrite stencil_matches_symbols.
erewrite stencil_matches_symbols0.
trivial.
+
intros. rename H into H0. assert (Hge: make_globalenv s CTXT LH = ret (Genv.globalenv ph)).
{
unfold make_globalenv. rewrite PH.
reflexivity.
}
apply make_globalenv_stencil_matches in Hge.
pose proof Hge as Hgeh.
inv Hge.
assert (Hge: make_globalenv s (CTXT ⊕ M) LL = ret (Genv.globalenv pl)).
{
unfold make_globalenv. rewrite PL.
reflexivity.
}
apply make_globalenv_stencil_matches in Hge.
pose proof Hge as Hgel.
inv Hge.
assert(Hprog_main: (prog_main ph) = (prog_main pl)).
{
erewrite make_program_prog_main; try eassumption.
erewrite make_program_prog_main; try eassumption.
reflexivity.
}
assert(Hprog_defs: prog_defs_le (prog_defs ph) (prog_defs pl)).
{
inv REFINE.
eapply cl_sim_layer_pointwise in cl_sim_layer.
destruct cl_sim_layer as [Hprim Hvar].
assert (HLayerOK: LayerOK LH).
{
eapply make_program_layer_ok.
esplit. eassumption.
}
eapply make_program_init_mem_le; try eassumption;
intros.
- destruct H.
+ eapply LayerOK_not_None in HLayerOK; eauto.
destruct HLayerOK as [func Hprim´].
specialize (Hprim i).
rewrite Hprim´ in Hprim.
specialize (get_layer_primitive_oplus i (〚M 〛 LL) LL).
intros Heq.
destruct (HLayerOK´ i) as [HLayerOK _ _].
destruct HLayerOK as [? HLayerOK].
rewrite HLayerOK in Hprim. rewrite HLayerOK in Heq.
Opaque mapsto semof.
inv Hprim. inv H3.
simpl in Heq.
caseEq (get_layer_primitive i LL); intros; simpl in H1; rewrite H1 in ×.
destruct o.
×
left. red; intros. inv H3.
×
right. red; intros.
specialize (get_module_function_oplus i CTXT M).
unfold isOKNone in H3.
rewrite H3. intros Hle. simpl in Hle.
caseEq (get_module_function i M); intros; rewrite H4 in *;
try destruct o; destruct (get_module_function i CTXT);
try destruct o; inv_monad Hle; try discriminate.
rewrite get_layer_primitive_oplus in HLayerOK.
rewrite get_semof_primitive in HLayerOK.
rewrite H4 in HLayerOK.
simpl in HLayerOK.
rewrite H1 in HLayerOK.
discriminate.
× left; discriminate.
+ right. red; intros. elim H.
specialize (get_module_function_oplus i CTXT M).
unfold isOKNone in H1. rewrite H1.
intros Hle. simpl in Hle.
destruct (get_module_function i CTXT).
destruct o. destruct (get_module_function i M); try destruct o; inv_monad Hle; try discriminate.
reflexivity.
destruct (get_module_function i M); try destruct o; inv_monad Hle; try discriminate.
- destruct H.
+ clear HLayerOK.
specialize (Hvar i).
rewrite H in Hvar.
specialize (get_layer_globalvar_oplus i (〚M 〛 LL) LL).
intros Heq.
specialize (LayerOK_elim _ i v HLayerOK´). intros Him.
destruct (HLayerOK´ i) as [_ HLayerOK _].
destruct HLayerOK as [? HLayerOK].
rewrite HLayerOK in Hvar. rewrite HLayerOK in Heq.
Opaque mapsto semof.
inv Hvar. inv H3. specialize (Him HLayerOK).
simpl in Heq.
caseEq (get_layer_globalvar i LL); intros; simpl in H1; rewrite H1 in ×.
destruct o.
×
caseEq (get_layer_globalvar i (〚M 〛 LL)); intros; simpl in H2; rewrite H2 in Heq;
try destruct o; inv_monad Heq.
discriminate.
inv H4. left; reflexivity.
×
right.
rewrite get_layer_globalvar_oplus in HLayerOK.
rewrite get_semof_globalvar in HLayerOK.
setoid_rewrite H1 in HLayerOK.
rewrite id_right in HLayerOK.
assert (MCOK: ModuleOK (CTXT ⊕ M)).
{
eapply make_program_module_ok.
eexists.
eassumption.
}
destruct (MCOK i) as [_ [y´ Hy´] _].
get_module_normalize_in Hy´.
apply res_option_oplus_ok_inv in Hy´.
destruct Hy´ as [[HC HM] | [HM HC]]; try congruence.
get_module_normalize.
rewrite HC.
rewrite id_left.
assumption.
×
caseEq (get_layer_globalvar i (〚M 〛 LL)); intros; simpl in H2;
rewrite H2 in Heq; try destruct o; inv_monad Heq.
+ right.
specialize (get_module_variable_oplus i CTXT M).
intros Hle.
exploit (make_program_module_ok s (CTXT ⊕ M) LL).
esplit; eassumption.
intros [_ Hmo _].
destruct Hmo as [? Hmo]. rewrite Hmo in Hle.
simpl in ×. unfold module in ×.
rewrite H in Hle.
destruct (get_module_variable i M); try destruct o;
inv_monad Hle.
× discriminate.
× inv H2.
assumption.
}
eapply @asm_init_state_match; eauto.
+
intros. inv H0.
+
intros. simpl in H. simpl.
assert (Hle: CTXT ≤ CTXT) by reflexivity.
assert (Hge: make_globalenv s CTXT LH = ret (Genv.globalenv ph)).
{
unfold make_globalenv. rewrite PH.
reflexivity.
}
assert (Hp: isOK (make_program s CTXT (〚M 〛 LL ⊕ LL))).
{
eapply make_program_vertical´; eassumption.
}
assert (Hge´: isOK (make_globalenv s CTXT (〚M 〛 LL ⊕ LL))).
{
destruct Hp as [p Hp].
eapply make_program_make_globalenv in Hp.
esplit. eauto.
}
destruct Hge´ as [ge´ Hge´].
specialize (make_globlenv_monotonic_weak _ _ _ _ Hle REFINE Hge ge´ Hge´); eauto 2.
intros Hle´.
pose proof Hge as Hge_match.
apply make_globalenv_stencil_matches in Hge.
pose proof Hge´ as Hge_match´.
apply make_globalenv_stencil_matches in Hge´.
destruct s1, s2, s1´. destruct m, m0, m1.
assert (Hge_external´:
∀ b ef,
Genv.find_funct_ptr ge´ b = Some (External ef) →
∃ i sg, ef = EF_external i sg) by
abstract
(intros until ef; eapply ge_external_valid; eauto).
assert (OKLayer: LayerOK (〚M 〛 LL ⊕ LL)).
{
eapply make_program_layer_ok; eassumption.
}
assert (Hnames: LayerNamesMatch DL (〚M〛 LL ⊕ LL)). {
apply layer_names_match_oplus; eauto.
apply lasm_semantics_names_match; eauto.
rewrite <- left_upper_bound in OKLayer.
eassumption.
}
exploit (one_step_sim_monotonic_alt s (Genv.globalenv ph) ge´); eauto 2.
pose proof prim_valid as prim_valid´.
{
unfold get_layer_prim_valid in ×.
intros.
specialize (get_layer_primitive_oplus i (〚M 〛 LL) LL). rewrite H1.
intros Heq.
caseEq (get_layer_primitive i (〚M 〛 LL)); intros; rewrite H2 in Heq;
try destruct o; caseEq (get_layer_primitive i LL); intros; rewrite H3 in Heq;
try destruct o; inv_monad Heq; try discriminate.
{
assert (MOK: ModuleOK M).
{
assert (HmOK: ModuleOK (CTXT ⊕ M)).
{
eapply make_program_module_ok.
esplit; eauto.
}
eapply module_ok_antitonic; try eassumption.
apply right_upper_bound.
}
destruct (MOK i) as [[[|] MOK´] _ _].
{
assert (mk_prog: isOK(make_program s M LL)).
{
eapply make_program_monotonic_exists; try eassumption; try reflexivity.
apply right_upper_bound.
}
rewrite get_semof_primitive in H2.
rewrite MOK´ in H2.
unfold semof_function in H2; monad_norm.
unfold module, module_ops in ×.
simpl in ×.
inv_monad H2.
inv H2.
subst.
simpl.
destruct (Decision.decide (ExtcallInvariantsDefined LL)).
destruct (Decision.decide (PrimcallInvariantsDefined LL)).
destruct (Decision.decide (LayerNamesMatch DL LL)).
destruct (Decision.decide (get_layer_prim_valid LL s)).
rewrite accessors_defined_weak; try assumption.
destruct mk_prog as [? mk_prog].
unfold module, module_ops in ×.
rewrite mk_prog. reflexivity.
elim n; assumption.
elim n; assumption.
elim n; assumption.
elim n; assumption.
}
{
rewrite get_semof_primitive in H2.
rewrite MOK´ in H2.
discriminate.
}
}
eauto.
}
intros [rs2´ [m2´[d2´[Hstep´ Hmatch´]]]].
refine_split´; eauto 2.
assert (Hge´´: make_globalenv s (CTXT ⊕ M) LL = ret (Genv.globalenv pl)).
{
unfold make_globalenv. rewrite PL.
reflexivity.
}
eapply one_step_vertical_composition; eauto.
-
eapply lasm_semantics_receptive; eauto.
-
eapply lasm_semantics_determinate; eauto.
Qed.
Next we can specialize the soundness theorem to the default
AsmInitialState instance.
Theorem soundness:
∀ {DH DL: compatdata}
(R: freerg compatrel DH DL)
(LH: compatlayer DH)
(LL: compatlayer DL)
(LH_ACC_DEF: LAsm.AccessorsDefined LH)
(LL_ACC_DEF: LAsm.AccessorsDefined LL)
(LH_RECEPT: ExternalCallsXDefined (LH))
(LL_DETERM: ExternalCallsXDefined (LL))
(LL_DETERM´: PrimitiveCallsXDefined LL)
(LH_INV: ExtcallInvariantsDefined LH)
(LL_INV: ExtcallInvariantsDefined LL)
(LH_PRIM_INV: PrimcallInvariantsDefined LH)
(LL_PRIM_INV: PrimcallInvariantsDefined LL)
(LH_NAMES: LayerNamesMatch DH LH)
(LL_NAMSE: LayerNamesMatch DL LL)
(M: LAsm.module)
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet)
(REFINE: cl_sim _ _ R LH (〚 M 〛 LL ⊕ LL))
(INIT_SIM: cl_init_sim _ _ R LH M LL)
(CTXT: LAsm.module) s pl
(PL: make_program s (CTXT ⊕ M) LL = OK pl)
(prim_valid: get_layer_prim_valid LL s)
ph
(PH: make_program s CTXT LH = OK ph)
(HLayerOK´: LayerOK (〚 M 〛 LL ⊕ LL)),
backward_simulation
(LAsm.semantics (lcfg_ops := LC LH) ph)
(LAsm.semantics (lcfg_ops := LC LL) pl).
Proof.
intros.
Thanks to INIT_SIM, we know that R cannot be the identity relation.
destruct R as [| DL R].
{
simpl in ×.
elim INIT_SIM.
}
eapply soundness_generic; eauto.
typeclasses eauto.
Qed.
End WITHLAYERS.
{
simpl in ×.
elim INIT_SIM.
}
eapply soundness_generic; eauto.
typeclasses eauto.
Qed.
End WITHLAYERS.