Library mcertikos.driver.lsamep_PHBThread_PHThread
Require Import MakeProgram.
Require Import CompatLayers.
Require Import PHBThread.
Require Import SingleConfiguration.
Require Import SingleAbstractDataType.
Require Import AuxStateDataType.
Require Import GlobalOracle.
Require Import BigStepGlobalOracle.
Require Import GlobalOracleProp.
Require Import AuxSingleAbstractDataType.
Require Import SingleConfiguration.
Require Import ObjPHBFlatMem.
Require Import ObjPHBThreadVMM.
Require Import ObjPHBThreadDEV.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadSCHED.
Require Import ObjPHBThreadINTELVIRT.
Require Import CertiKOSAux.
Require Import PHThread.
Require Import RealParams.
Require Import GlobalOracleProp.
Require Import AlgebraicMemImpl.
Require Import SingleOracle.
Require Import SingleConfiguration.
Require Import SingleOracleImpl.
Require Import StencilImpl.
Require Import CompCertiKOSproof.
Require Import MemimplX.
Remove Hints
MemimplX.memory_model_ops
MemimplX.memory_model
MemimplX.memory_model_x
StencilImpl.ptree_stencil_ops
StencilImpl.ptree_stencil_prf
: typeclass_instances.
Existing Instance CompCertiKOSproof.memory_model_ops.
Require Import LAsmAbsDataProperty.
Require Import PHThread2TGenDef.
Require Import PHThread2TGen.
Require Import E2PBThreadGenDef.
Require Import E2PBThreadGen.
Require Import SingleProcessor_Refinement.
Require Import Concurrent_Linking.
Section CERTIKOSCORRECT.
Context `{multi_oracle_prop : MultiOracleProp}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Existing Instance SingleOracleImpl.s_oracle_prf.
Existing Instance SingleOracleImpl.s_oracle_prop_prf.
Existing Instance SingleOracleImpl.s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Existing Instance SingleOracleImpl.s_link_config.
Context `{multi_oracle_link: !MultiOracleLink}.
Context `{phthread2tgen_prop: !PHThraed2TGenProp s_oracle_prf}.
Existing Instance PHThread2TGen.abs_relT.
Existing Instance algebraicmem.
Require Import CompatGenSem.
Transparent compatlayer_ops ptree_layer_ops.
Existing Instance LAsm.module_ops.
Typeclasses eauto := debug.
Definition f {D} (x : ident × res (compatsem D)) : ident × res (option (globdef LAsm.fundef unit)) :=
match x with (i, y) ⇒
(i, match y with
| OK def ⇒ primitive_globdef i (Some def)
| Error msg ⇒ Error msg
end)
end.
Lemma f_elements_unique {D} i x y (t: PTree.t (res (compatsem D))):
In (i, x) (map f (PTree.elements t)) →
In (i, y) (map f (PTree.elements t)) →
x = y.
Proof.
pose proof (PTree.elements_keys_norepet t).
induction (PTree.elements t); inv H.
- simpl. contradiction.
- simpl.
intros [Hx|Hx] [Hy|Hy]; subst.
+ congruence.
+ exfalso. apply H2. revert Hy. destruct a. simpl. inv Hx. clear.
induction l; simpl; eauto; intros [?|?]; eauto.
left. destruct a. inv H. reflexivity.
+ exfalso. apply H2. revert Hx. destruct a. simpl. inv Hy. clear.
induction l; simpl; eauto; intros [?|?]; eauto.
left. destruct a. inv H. reflexivity.
+ eauto.
Qed.
Lemma elements_lsamepp {D1 D2} (L1: compatlayer D1) (L2: compatlayer D2):
map f (PTree.elements (fst (cl_base_layer L1))) =
map f (PTree.elements (fst (cl_base_layer L2))) →
lsamepp (Fm:=LAsm.function) (Vm:=Ctypes.type) (Fp:=LAsm.fundef) (Vp:=unit) L1 L2.
Proof.
intros H i _.
unfold lsamepp.
simpl.
unfold ptree_layer_primitive.
destruct ((fst (cl_base_layer L1)) ! i) eqn:H1;
destruct ((fst (cl_base_layer L2)) ! i) eqn:H2.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H1.
apply PTree.elements_correct in H2.
apply (in_map f) in H1.
apply (in_map f) in H2.
rewrite H in H1.
pose proof (f_elements_unique _ _ _ _ H1 H2).
simpl.
destruct r, r0; monad_norm; eauto.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H1.
apply (in_map f) in H1.
rewrite H in H1.
apply in_map_iff in H1.
destruct H1 as ([a b] & ? & H1).
apply PTree.elements_complete in H1.
inv H0. congruence.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H2.
apply (in_map f) in H2.
rewrite <- H in H2.
apply in_map_iff in H2.
destruct H2 as ([a b] & ? & H2).
apply PTree.elements_complete in H2.
inv H0. congruence.
- setoid_rewrite H1.
setoid_rewrite H2.
reflexivity.
Qed.
Definition g (x : ident × res (globvar Ctypes.type)) : ident × res (option (globdef LAsm.fundef unit)) :=
match x with (i, y) ⇒
(i, match y with
| OK def ⇒ globalvar_globdef (Some def)
| Error msg ⇒ Error msg
end)
end.
Lemma g_elements_unique i x y (t: PTree.t (res (globvar Ctypes.type))):
In (i, x) (map g (PTree.elements t)) →
In (i, y) (map g (PTree.elements t)) →
x = y.
Proof.
pose proof (PTree.elements_keys_norepet t).
induction (PTree.elements t); inv H.
- simpl. contradiction.
- simpl.
intros [Hx|Hx] [Hy|Hy]; subst.
+ congruence.
+ exfalso. apply H2. revert Hy. destruct a. simpl. inv Hx. clear.
induction l; simpl; eauto; intros [?|?]; eauto.
left. destruct a. inv H. reflexivity.
+ exfalso. apply H2. revert Hx. destruct a. simpl. inv Hy. clear.
induction l; simpl; eauto; intros [?|?]; eauto.
left. destruct a. inv H. reflexivity.
+ eauto.
Qed.
Lemma elements_lsamepv {D1 D2} (L1: compatlayer D1) (L2: compatlayer D2):
map g (PTree.elements (snd (cl_base_layer L1))) =
map g (PTree.elements (snd (cl_base_layer L2))) →
lsamepv (Fm:=LAsm.function) (Vm:=Ctypes.type) (Fp:=LAsm.fundef) (Vp:=unit) L1 L2.
Proof.
intros H i _.
unfold lsamepp.
simpl.
unfold ptree_layer_globalvar.
destruct ((snd (cl_base_layer L1)) ! i) eqn:H1;
destruct ((snd (cl_base_layer L2)) ! i) eqn:H2.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H1.
apply PTree.elements_correct in H2.
apply (in_map g) in H1.
apply (in_map g) in H2.
rewrite H in H1.
pose proof (g_elements_unique _ _ _ _ H1 H2).
simpl.
destruct r, r0; monad_norm; eauto.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H1.
apply (in_map g) in H1.
rewrite H in H1.
apply in_map_iff in H1.
destruct H1 as ([a b] & ? & H1).
apply PTree.elements_complete in H1.
inv H0. congruence.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H2.
apply (in_map g) in H2.
rewrite <- H in H2.
apply in_map_iff in H2.
destruct H2 as ([a b] & ? & H2).
apply PTree.elements_complete in H2.
inv H0. congruence.
- setoid_rewrite H1.
setoid_rewrite H2.
reflexivity.
Qed.
Lemma phbthread_phthread_lsamep:
lsamep (Fm:=LAsm.function) (Vm:=Ctypes.type) (Fp:=LAsm.fundef) (Vp:=unit)
(phbthread ⊕ L64)
(phthread ⊕ L64).
Proof.
repeat apply conj.
- apply lsamepp_iff.
split; apply elements_lsamepp; reflexivity.
- apply lsamepv_iff.
split; apply elements_lsamepv; reflexivity.
- decision.
- decision.
- decision.
- decision.
Qed.
End CERTIKOSCORRECT.
Require Import CompatLayers.
Require Import PHBThread.
Require Import SingleConfiguration.
Require Import SingleAbstractDataType.
Require Import AuxStateDataType.
Require Import GlobalOracle.
Require Import BigStepGlobalOracle.
Require Import GlobalOracleProp.
Require Import AuxSingleAbstractDataType.
Require Import SingleConfiguration.
Require Import ObjPHBFlatMem.
Require Import ObjPHBThreadVMM.
Require Import ObjPHBThreadDEV.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadSCHED.
Require Import ObjPHBThreadINTELVIRT.
Require Import CertiKOSAux.
Require Import PHThread.
Require Import RealParams.
Require Import GlobalOracleProp.
Require Import AlgebraicMemImpl.
Require Import SingleOracle.
Require Import SingleConfiguration.
Require Import SingleOracleImpl.
Require Import StencilImpl.
Require Import CompCertiKOSproof.
Require Import MemimplX.
Remove Hints
MemimplX.memory_model_ops
MemimplX.memory_model
MemimplX.memory_model_x
StencilImpl.ptree_stencil_ops
StencilImpl.ptree_stencil_prf
: typeclass_instances.
Existing Instance CompCertiKOSproof.memory_model_ops.
Require Import LAsmAbsDataProperty.
Require Import PHThread2TGenDef.
Require Import PHThread2TGen.
Require Import E2PBThreadGenDef.
Require Import E2PBThreadGen.
Require Import SingleProcessor_Refinement.
Require Import Concurrent_Linking.
Section CERTIKOSCORRECT.
Context `{multi_oracle_prop : MultiOracleProp}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Existing Instance SingleOracleImpl.s_oracle_prf.
Existing Instance SingleOracleImpl.s_oracle_prop_prf.
Existing Instance SingleOracleImpl.s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Existing Instance SingleOracleImpl.s_link_config.
Context `{multi_oracle_link: !MultiOracleLink}.
Context `{phthread2tgen_prop: !PHThraed2TGenProp s_oracle_prf}.
Existing Instance PHThread2TGen.abs_relT.
Existing Instance algebraicmem.
Require Import CompatGenSem.
Transparent compatlayer_ops ptree_layer_ops.
Existing Instance LAsm.module_ops.
Typeclasses eauto := debug.
Definition f {D} (x : ident × res (compatsem D)) : ident × res (option (globdef LAsm.fundef unit)) :=
match x with (i, y) ⇒
(i, match y with
| OK def ⇒ primitive_globdef i (Some def)
| Error msg ⇒ Error msg
end)
end.
Lemma f_elements_unique {D} i x y (t: PTree.t (res (compatsem D))):
In (i, x) (map f (PTree.elements t)) →
In (i, y) (map f (PTree.elements t)) →
x = y.
Proof.
pose proof (PTree.elements_keys_norepet t).
induction (PTree.elements t); inv H.
- simpl. contradiction.
- simpl.
intros [Hx|Hx] [Hy|Hy]; subst.
+ congruence.
+ exfalso. apply H2. revert Hy. destruct a. simpl. inv Hx. clear.
induction l; simpl; eauto; intros [?|?]; eauto.
left. destruct a. inv H. reflexivity.
+ exfalso. apply H2. revert Hx. destruct a. simpl. inv Hy. clear.
induction l; simpl; eauto; intros [?|?]; eauto.
left. destruct a. inv H. reflexivity.
+ eauto.
Qed.
Lemma elements_lsamepp {D1 D2} (L1: compatlayer D1) (L2: compatlayer D2):
map f (PTree.elements (fst (cl_base_layer L1))) =
map f (PTree.elements (fst (cl_base_layer L2))) →
lsamepp (Fm:=LAsm.function) (Vm:=Ctypes.type) (Fp:=LAsm.fundef) (Vp:=unit) L1 L2.
Proof.
intros H i _.
unfold lsamepp.
simpl.
unfold ptree_layer_primitive.
destruct ((fst (cl_base_layer L1)) ! i) eqn:H1;
destruct ((fst (cl_base_layer L2)) ! i) eqn:H2.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H1.
apply PTree.elements_correct in H2.
apply (in_map f) in H1.
apply (in_map f) in H2.
rewrite H in H1.
pose proof (f_elements_unique _ _ _ _ H1 H2).
simpl.
destruct r, r0; monad_norm; eauto.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H1.
apply (in_map f) in H1.
rewrite H in H1.
apply in_map_iff in H1.
destruct H1 as ([a b] & ? & H1).
apply PTree.elements_complete in H1.
inv H0. congruence.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H2.
apply (in_map f) in H2.
rewrite <- H in H2.
apply in_map_iff in H2.
destruct H2 as ([a b] & ? & H2).
apply PTree.elements_complete in H2.
inv H0. congruence.
- setoid_rewrite H1.
setoid_rewrite H2.
reflexivity.
Qed.
Definition g (x : ident × res (globvar Ctypes.type)) : ident × res (option (globdef LAsm.fundef unit)) :=
match x with (i, y) ⇒
(i, match y with
| OK def ⇒ globalvar_globdef (Some def)
| Error msg ⇒ Error msg
end)
end.
Lemma g_elements_unique i x y (t: PTree.t (res (globvar Ctypes.type))):
In (i, x) (map g (PTree.elements t)) →
In (i, y) (map g (PTree.elements t)) →
x = y.
Proof.
pose proof (PTree.elements_keys_norepet t).
induction (PTree.elements t); inv H.
- simpl. contradiction.
- simpl.
intros [Hx|Hx] [Hy|Hy]; subst.
+ congruence.
+ exfalso. apply H2. revert Hy. destruct a. simpl. inv Hx. clear.
induction l; simpl; eauto; intros [?|?]; eauto.
left. destruct a. inv H. reflexivity.
+ exfalso. apply H2. revert Hx. destruct a. simpl. inv Hy. clear.
induction l; simpl; eauto; intros [?|?]; eauto.
left. destruct a. inv H. reflexivity.
+ eauto.
Qed.
Lemma elements_lsamepv {D1 D2} (L1: compatlayer D1) (L2: compatlayer D2):
map g (PTree.elements (snd (cl_base_layer L1))) =
map g (PTree.elements (snd (cl_base_layer L2))) →
lsamepv (Fm:=LAsm.function) (Vm:=Ctypes.type) (Fp:=LAsm.fundef) (Vp:=unit) L1 L2.
Proof.
intros H i _.
unfold lsamepp.
simpl.
unfold ptree_layer_globalvar.
destruct ((snd (cl_base_layer L1)) ! i) eqn:H1;
destruct ((snd (cl_base_layer L2)) ! i) eqn:H2.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H1.
apply PTree.elements_correct in H2.
apply (in_map g) in H1.
apply (in_map g) in H2.
rewrite H in H1.
pose proof (g_elements_unique _ _ _ _ H1 H2).
simpl.
destruct r, r0; monad_norm; eauto.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H1.
apply (in_map g) in H1.
rewrite H in H1.
apply in_map_iff in H1.
destruct H1 as ([a b] & ? & H1).
apply PTree.elements_complete in H1.
inv H0. congruence.
- setoid_rewrite H1.
setoid_rewrite H2.
apply PTree.elements_correct in H2.
apply (in_map g) in H2.
rewrite <- H in H2.
apply in_map_iff in H2.
destruct H2 as ([a b] & ? & H2).
apply PTree.elements_complete in H2.
inv H0. congruence.
- setoid_rewrite H1.
setoid_rewrite H2.
reflexivity.
Qed.
Lemma phbthread_phthread_lsamep:
lsamep (Fm:=LAsm.function) (Vm:=Ctypes.type) (Fp:=LAsm.fundef) (Vp:=unit)
(phbthread ⊕ L64)
(phthread ⊕ L64).
Proof.
repeat apply conj.
- apply lsamepp_iff.
split; apply elements_lsamepp; reflexivity.
- apply lsamepv_iff.
split; apply elements_lsamepv; reflexivity.
- decision.
- decision.
- decision.
- decision.
Qed.
End CERTIKOSCORRECT.