Library mcertikos.multithread.highrefins.PHThread2TGenLemma
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 Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import LoadStoreSem3high.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import I64Layer.
Require Import AlgebraicMem.
Require Import Decision.
Require Import FutureTactic.
Require Import GlobalOracleProp.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import SingleConfiguration.
Require Import ObjPHBFlatMem.
Require Import PHBThread.
Require Import AsmPHThread2T.
Require Import AuxSingleAbstractDataType.
Require Import SingleOracleImpl.
Require Import PHThread2TComposeData.
Require Import LoadStoreSemPHB.
Require Import ObjPHBThreadDEV.
Require Import ObjPHBThreadINTELVIRT.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadReplayFunction.
Require Import ObjPHBThreadSCHED.
Require Import ObjPHBThreadVMM.
Require Import ObjInterruptManagement.
Require Import ObjConsole.
Require Import ObjInterruptController.
Require Import ObjSerialDevice.
Require Import OracleInstances.
Require Import ObjVMMFun.
Require Import ObjVMMGetSet.
Require Import ObjVMMDef.
Require Import ObjCV.
Require Import ObjCPU.
Require Import ObjVMCS.
Require Import ObjVMX.
Require Import ObjEPT.
Require Import ObjBigThread.
Require Import BigLogThreadConfigFunction.
Require Import StencilImpl.
Require Import PHThread2TGenDef.
Section PHTHREAD2TGENLEMMAFILE.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Local Instance s_oracle_prf : SingleOracle := s_oracle_prf.
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)}.
Local Instance s_oracle_prop_prf : SingleOracleProp := SingleOracleImpl.s_oracle_prop_prf.
Context `{Hstencil : Stencil (stencil := stencil)}.
Local Instance s_config : SingleConfiguration mem := SingleOracleImpl.s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_link_prop_prf : SingleOracleLinkProp := SingleOracleImpl.s_oracle_link_prop_prf.
Local Instance s_link_config : SingleLinkConfiguration mem := s_link_config.
Context `{acc_def: !AccessorsDefined (mem := mem) (stencil := stencil) (stencil_ops := stencil_ops)
(memory_model_ops := memory_model_ops)
(phbthread (s_config := s_config) ⊕ L64)}.
Lemma cons_intr_aux_related_t :
∀ kctxt pd a´ a l,
relate_RData kctxt a l pd →
cons_intr_aux a = Some a´ →
∃ l´ pd´,
single_cons_intr_aux (uRData l, pd) = Some (uRData l´, pd´) ∧
relate_RData kctxt a´ l´ pd´ ∧
uRData l = uRData l´.
Proof.
Opaque Z.add Z.sub Z.div Z.mul.
Opaque OracleInstances.SerialEnv.
Opaque cons_buf list_eq_dec Zlength serial_exists.
intros.
functional inversion H0; subst.
- unfold single_cons_intr_aux.
inv H; simpl in *; rewritesb.
rewrite H2, H3, H4, H5, H7.
subdestruct_one.
rewrite H8, H9, H10; ∃ l; esplit; eauto.
split; eauto; split; eauto.
constructor; simpl; auto.
+ inv inv_re.
constructor; simpl; auto.
- unfold single_cons_intr_aux.
inv H; simpl in *; rewritesb.
rewrite H2, H3, H4, H5, H7.
subdestruct_one.
rewrite H8, H9, H10; ∃ l; esplit; eauto.
split; eauto; split; eauto; simpl.
constructor; simpl; auto.
+ inv inv_re.
constructor; simpl; auto.
Qed.
Lemma serial_enable_aux_related_t:
∀ n kctxt l pd a a´,
relate_RData kctxt a l pd →
serial_intr_enable_aux n a = Some a´ →
∃ l´ pd´,
single_serial_intr_enable n (uRData l, pd) = Some (uRData l´, pd´) ∧
relate_RData kctxt a´ l´ pd´ ∧
uRData l = uRData l´.
Proof.
induction n; intros.
- simpl in H0; inv H0; ∃ l, pd; auto.
- simpl in ×.
assert (SerialIrq_eq: SerialIrq (s (com1 pd)) = SerialIrq (s (AbstractDataType.com1 a))).
{ inv H; rewritesb; auto. }
case_eq (SerialIrq (s (com1 pd))); intros.
+ rewrite <- SerialIrq_eq in H0; rewrite H1 in H0.
subdestruct; try (inv H0; fail).
exploit cons_intr_aux_related_t; eauto; try exact H; intros H2.
destruct H2 as (l´ & pd´ & H2a & H2b & H2c).
simpl in H2a; rewrite H2a.
eapply IHn in H0; eauto.
destruct H0 as (l´´ & pd´´ & H2a´ & H2b´ & H2c´).
refine_split´; eauto.
rewrite <- H2c´; auto.
+ rewrite <- SerialIrq_eq in H0.
rewrite H1 in H0; inv H0.
refine_split´; eauto.
Qed.
Lemma serial_disable_aux_true_related_t:
∀ n kctxt pd a a´ l,
relate_RData kctxt a l pd →
serial_intr_disable_aux n true a = Some a´ →
∃ l´ pd´,
single_serial_intr_disable n true (uRData l, pd) = Some (uRData l´, pd´) ∧
relate_RData kctxt a´ l´ pd´ ∧
uRData l = uRData l´.
Proof.
induction n; intros.
- simpl in H0; inv H0; ∃ l, pd; auto.
- assert (relate_RData kctxt (a {com1 : serial_intr (AbstractDataType.com1 a)})
l (pd {pv_com1: single_serial_intr (com1 pd)})).
{ unfold single_serial_intr; simpl.
unfold single_serial_trans_env; simpl.
unfold serial_intr.
unfold serial_trans_env; simpl.
inv H; constructor; auto.
- rewrite <- com1_re; auto.
- inv inv_re.
constructor; simpl; auto. }
simpl in ×.
assert (SerialIrq_eq: SerialIrq (single_serial_trans_env (SerialEnv (l1 (com1 pd))) (s (com1 pd))) =
SerialIrq (serial_trans_env (SerialEnv (l1 (AbstractDataType.com1 a)))
(s (AbstractDataType.com1 a)))).
{ unfold single_serial_trans_env.
unfold serial_trans_env.
inv H; rewritesb; simpl; auto. }
case_eq (SerialIrq (single_serial_trans_env (SerialEnv (l1 (com1 pd))) (s (com1 pd)))); intros.
+ rewrite <- SerialIrq_eq in H0.
rewrite H2 in H0.
generalize H1; intros Htemp.
eapply IHn in Htemp; eauto.
+ rewrite <- SerialIrq_eq in H0.
rewrite H2 in H0; inv H0.
∃ l, pd; split; auto.
Qed.
Lemma serial_disable_aux_false_related_t:
∀ n kctxt a a´ l pd,
relate_RData kctxt a l pd →
serial_intr_disable_aux n false a= Some a´ →
∃ l´ pd´,
single_serial_intr_disable n false (uRData l, pd) = Some (uRData l´, pd´) ∧
relate_RData kctxt a´ l´ pd´ ∧
uRData l = uRData l´.
Proof.
induction n; intros.
- simpl in H0; inv H0; ∃ l, pd; eauto.
- assert (relate_RData kctxt (a {com1 : serial_intr (AbstractDataType.com1 a)})
l (pd {pv_com1: single_serial_intr (com1 pd)})).
{ unfold single_serial_intr; simpl.
unfold single_serial_trans_env; simpl.
unfold serial_intr.
unfold serial_trans_env; simpl.
inv H; constructor; auto.
- rewrite <- com1_re; auto.
- inv inv_re.
constructor; simpl; auto. }
simpl in ×.
assert (SerialIrq_eq: SerialIrq (single_serial_trans_env (SerialEnv (l1 (com1 pd))) (s (com1 pd))) =
SerialIrq (serial_trans_env (OracleInstances.SerialEnv (l1 (AbstractDataType.com1 a)))
(s (AbstractDataType.com1 a)))).
{ unfold single_serial_trans_env.
unfold serial_trans_env.
inv H; rewritesb; simpl; auto. }
case_eq (SerialIrq (single_serial_trans_env (SerialEnv (l1 (com1 pd))) (s (com1 pd)))); intros.
+ rewrite <- SerialIrq_eq in H0.
subdestruct.
exploit cons_intr_aux_related_t; eauto; intros H3.
destruct H3 as (l´ & pd´ & H3a & H3b & H3c).
simpl in *; rewrite <- H3c in H3a; rewrite H3a.
generalize H3b; intros Htemp.
eapply IHn in Htemp; eauto.
destruct Htemp as (l´´ & pd´´ & H4a & H4b & H4c).
∃ l´´, pd´´.
split; eauto.
× rewrite H3c; auto.
× split; auto.
rewrite H3c; auto.
+ rewrite <- SerialIrq_eq in H0.
subdestruct; subst; inv H0.
refine_split´; eauto.
Qed.
Lemma serial_intr_disable_related_t:
∀ kctxt a a´ l pd,
relate_RData kctxt a l pd →
thread_serial_intr_disable_spec a = Some a´ →
∃ l´ pd´,
single_serial_intr_disable_spec (uRData l, pd) = Some (uRData l´, pd´) ∧
relate_RData kctxt a´ l´ pd´ ∧
uRData l = uRData l´.
Proof.
intros.
functional inversion H0.
assert (in_intr_related_true: relate_RData kctxt (a {in_intr: true}) l (pd {pv_in_intr: true})).
{ constructor; inv H; simpl in *; auto.
inv inv_re.
constructor; simpl; auto. }
assert (in_intr_related_false: relate_RData kctxt (a {in_intr: true}) l (pd {pv_in_intr: true})).
{ constructor; inv H; simpl in *; auto.
inv inv_re.
constructor; simpl; auto. }
Opaque single_serial_intr_disable proc_id.
Opaque serial_intr_disable_aux.
unfold serial_intr_disable_spec in H1; unfold single_serial_intr_disable_spec.
subdestruct; simpl in *; inv H1;
try (exploit serial_disable_aux_true_related_t; eauto; intros Hrelated;
destruct Hrelated as (l´ & pd´ & Hrelated_a & Hrelated_b & Hrealted_c); inv H; simpl in *; rewritesb;
rewrite zeq_true, Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4; simpl);
try (rewrite Hrelated_a; simpl; refine_split; eauto; inv Hrelated_b; simpl in *; constructor; auto; rewrite <- ioapic_re0; auto);
try (rewrite Hdestruct9; simpl; rewrite Hrelated_a; simpl; refine_split; eauto; inv Hrelated_b; simpl in *; constructor; auto; rewrite <- ioapic_re0; auto);
try (inv inv_re0; constructor; simpl; auto).
- exploit serial_disable_aux_false_related_t; eauto; intros Hrelated;
destruct Hrelated as (l´ & pd´ & Hrelated_a & Hrelated_b & Hrealted_c).
inv H; simpl in *; rewritesb.
rewrite zeq_true, Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4, Hdestruct9; simpl.
rewrite Hrelated_a; simpl.
refine_split; eauto; inv Hrelated_b; simpl in *; constructor; auto; simpl.
+ rewrite <- ioapic_re0; auto.
+ inv inv_re0; constructor; simpl; auto.
Transparent single_serial_intr_disable proc_id.
Transparent serial_intr_disable_aux.
Qed.
Lemma serial_intr_enable_related_t:
∀ kctxt a a´ l pd,
relate_RData kctxt a l pd →
thread_serial_intr_enable_spec a = Some a´ →
∃ l´ pd´,
single_serial_intr_enable_spec (uRData l, pd) = Some (uRData l´, pd´) ∧
relate_RData kctxt a´ l´ pd´ ∧
uRData l = uRData l´.
Proof.
intros.
functional inversion H0.
functional inversion H1.
assert (Hrelated: relate_RData kctxt (a {in_intr: true}) l (pd {pv_in_intr: true})).
{ constructor; inv H; simpl in *; auto.
inv inv_re.
constructor; simpl; auto. }
Opaque serial_intr_enable_aux.
Opaque single_serial_intr_enable.
unfold single_serial_intr_enable_spec.
simpl in *; inv H3.
exploit serial_enable_aux_related_t; eauto; intros Htemp; destruct Htemp as (l´ & pd´ & Hrelated_a & Hrelated_b & Hrelated_c).
inv H; simpl in *; rewritesb.
rewrite zeq_true, H5, H6, H7, H8, H9, H10, H11.
rewrite Hrelated_a.
refine_split´; eauto.
simpl; eauto.
inv Hrelated_b; simpl; constructor; simpl in *; auto.
- rewrite <- ioapic_re0; auto.
- inv inv_re0; constructor; simpl; auto.
Transparent serial_intr_enable_aux.
Transparent single_serial_intr_enable.
Qed.
Lemma serial_putc_related_t:
∀ c kctxt a a´ l pd,
relate_RData kctxt a l pd →
thread_serial_putc_spec c a = Some a´ →
∃ l´ pd´,
single_serial_putc_spec c (uRData l, pd) = Some (uRData l´, pd´) ∧
relate_RData kctxt a´ l´ pd´ ∧
uRData l = uRData l´.
Proof.
intros.
functional inversion H0.
functional inversion H1; inv H3; unfold single_serial_putc_spec.
- inv H; simpl in *; rewritesb.
rewrite zeq_true, H5, H6, H7, H9.
subdestruct_one.
refine_split´; eauto; constructor; auto; simpl in ×.
+ inv inv_re; constructor; simpl; auto.
- inv H; simpl in *; rewritesb.
rewrite zeq_true, H5, H6, H7, H9, H11.
subdestruct_one.
refine_split´; eauto; constructor; auto; simpl in ×.
+ inv inv_re; constructor; simpl; auto.
- inv H; simpl in *; rewritesb.
rewrite zeq_true, H5, H6, H7, H9.
subdestruct; try (inv H11; fail); try contradiction.
refine_split´; eauto; constructor; auto; simpl in ×.
+ inv inv_re; constructor; simpl; auto.
- inv H; simpl in *; rewritesb.
rewrite zeq_true, H5, H6, H7, H9, H12.
subdestruct; try (inv H11; fail); try contradiction.
refine_split´; eauto; constructor; auto; simpl in ×.
+ inv inv_re; constructor; simpl; auto.
- inv H; simpl in *; rewritesb.
rewrite zeq_true, H5, H6, H7, H8.
refine_split´; eauto; constructor; auto.
Qed.
Lemma cons_buf_read_related_t:
∀ kctxt a a´ l pd res,
relate_RData kctxt a l pd →
thread_cons_buf_read_spec a = Some (a´, res) →
∃ l´ pd´ res´,
single_cons_buf_read_spec (uRData l, pd) = Some ((uRData l´, pd´), res´) ∧
relate_RData kctxt a´ l´ pd´ ∧
uRData l = uRData l´ ∧
res = res´.
Proof.
intros.
functional inversion H0.
functional inversion H1; substx; unfold single_cons_buf_read_spec; simpl in ×.
- inv H; simpl in *; rewritesb.
rewrite zeq_true, H6, H7, H8, H9.
refine_split´; eauto; constructor; auto.
- inv H; simpl in *; rewritesb.
rewrite zeq_true, H6, H7, H8, H9.
refine_split´; eauto; constructor; auto.
inv inv_re; constructor; simpl; auto.
Qed.
Lemma get_kernel_pa_related_t:
∀ n vaddr kctxt l pd a res,
n = ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) →
relate_RData kctxt a l pd →
get_kernel_pa_spec n vaddr a = Some res →
∃ res´,
single_get_kernel_pa_spec n vaddr (uRData l, pd) = Some res´ ∧ res = res´.
Proof.
intros; functional inversion H1; simpl; subst.
unfold single_get_kernel_pa_spec.
exploit ptRead_related_t; eauto; intros.
destruct H as (res´, (H1a, H1b)); subst.
inv H0; simpl in ×.
rewrite <- pg_re; rewrite H3; rewrite H1a.
rewrite zeq_false; eauto.
Qed.
Lemma thread_ptRead_related_t :
∀ n vadr kctxt l pd a res,
relate_RData kctxt a l pd →
thread_ptRead_spec n vadr a = Some res →
∃ res´,
single_ptRead_spec n vadr (uRData l, pd) = Some res ∧ res = res´.
Proof.
intros.
unfold thread_ptRead_spec in H0.
unfold ptRead_spec in H0.
unfold getPDE_spec, getPTE_spec in H0.
unfold single_ptRead_spec in *; simpl in ×.
unfold single_getPDE_spec, single_getPTE_spec in *; simpl.
subdestruct; inv H0; inv H; simpl; rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- init_re, <- cid_re;
rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2; rewrite <- ptp_re; rewrite Hdestruct3, Hdestruct6.
{ rewrite zeq_true; eauto. }
{ rewrite zeq_false; auto; rewrite zlt_lt_true; eauto; rewrite Hdestruct9; auto; eauto. }
{ rewrite zeq_false; auto; rewrite zlt_lt_true; eauto; rewrite Hdestruct9; auto; eauto. }
{ rewrite zeq_true; eauto. }
{ rewrite zeq_true; eauto. }
{ rewrite zeq_true; eauto. }
Qed.
End PHTHREAD2TGENLEMMAFILE.