Library mcertikos.multithread.highrefins.PHThread2TGenDef

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.

Section PHThread2TGenDEFINITION.

  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)}.

  Definition CHECKUNCHAGNED (a a´ : AbstractDataType.RData) : Prop :=
    AbstractDataType.CPU_ID a = AbstractDataType.CPU_ID a´ ∧
    AbstractDataType.MM a = AbstractDataType.MM a´ ∧
    AbstractDataType.MMSize a = AbstractDataType.MMSize a´ ∧
    AbstractDataType.vmxinfo a = AbstractDataType.vmxinfo a´ ∧
    AbstractDataType.CR3 a = AbstractDataType.CR3 a´ ∧
    AbstractDataType.ti a = AbstractDataType.ti a´ ∧
    AbstractDataType.pg a = AbstractDataType.pg a´ ∧
    AbstractDataType.ikern a = AbstractDataType.ikern a´ ∧
    AbstractDataType.ihost a = AbstractDataType.ihost a´ ∧

    AbstractDataType.HP a = AbstractDataType.HP a´ ∧
    AbstractDataType.cid a = AbstractDataType.cid a´ ∧
    AbstractDataType.multi_log a = AbstractDataType.multi_log a´ ∧
    AbstractDataType.multi_oracle a = AbstractDataType.multi_oracle a´ ∧
    AbstractDataType.AC a = AbstractDataType.AC a´ ∧
    AbstractDataType.AT a = AbstractDataType.AT a´ ∧
    AbstractDataType.ATC a = AbstractDataType.ATC a´ ∧
    AbstractDataType.nps a = AbstractDataType.nps a´ ∧
    AbstractDataType.init a = AbstractDataType.init a´ ∧
    AbstractDataType.pperm a = AbstractDataType.pperm a´ ∧
    AbstractDataType.PT a = AbstractDataType.PT a´ ∧
    AbstractDataType.ptpool a = AbstractDataType.ptpool a´ ∧
    AbstractDataType.idpde a = AbstractDataType.idpde a´ ∧
    AbstractDataType.ipt a = AbstractDataType.ipt a´ ∧
    AbstractDataType.LAT a = AbstractDataType.LAT a´ ∧
    AbstractDataType.smspool a = AbstractDataType.smspool a´ ∧
    AbstractDataType.kctxt a = AbstractDataType.kctxt a´ ∧
    AbstractDataType.sleeper a = AbstractDataType.sleeper a´ ∧
    AbstractDataType.tcb a = AbstractDataType.tcb a´ ∧
    AbstractDataType.tdq a = AbstractDataType.tdq a´ ∧
    AbstractDataType.abtcb a = AbstractDataType.abtcb a´ ∧
    AbstractDataType.abq a = AbstractDataType.abq a´ ∧
    AbstractDataType.syncchpool a = AbstractDataType.syncchpool a´ ∧
    AbstractDataType.buffer a = AbstractDataType.buffer a´ ∧
    AbstractDataType.big_oracle a = AbstractDataType.big_oracle a´ ∧
    AbstractDataType.uctxt a = AbstractDataType.uctxt a´ ∧
    AbstractDataType.ept a = AbstractDataType.ept a´ ∧
    AbstractDataType.vmcs a = AbstractDataType.vmcs a´ ∧
    AbstractDataType.vmx a = AbstractDataType.vmx a´ ∧
    AbstractDataType.ts a = AbstractDataType.ts a´ ∧
    AbstractDataType.com1 a = AbstractDataType.com1 a´ ∧
    AbstractDataType.drv_serial a = AbstractDataType.drv_serial a´ ∧
    AbstractDataType.console_concrete a = AbstractDataType.console_concrete a´ ∧
    AbstractDataType.console a = AbstractDataType.console a´ ∧
    AbstractDataType.ioapic a = AbstractDataType.ioapic a´ ∧
    AbstractDataType.lapic a = AbstractDataType.lapic a´ ∧
    AbstractDataType.tf a = AbstractDataType.tf a´ ∧
    AbstractDataType.tf_reg a = AbstractDataType.tf_reg a´ ∧
    AbstractDataType.curr_intr_num a = AbstractDataType.curr_intr_num a´ ∧
    AbstractDataType.intr_flag a = AbstractDataType.intr_flag a´ ∧
    AbstractDataType.saved_intr_flags a = AbstractDataType.saved_intr_flags a´ ∧
    AbstractDataType.in_intr a = AbstractDataType.in_intr a´ ∧
    AbstractDataType.i_dev_serial a = AbstractDataType.i_dev_serial a´ ∧
    AbstractDataType.kbd a = AbstractDataType.kbd a´ ∧
    AbstractDataType.kbd_drv a = AbstractDataType.kbd_drv a´.

  Lemma big2_thread_yield_satisfies_CHECKUNCHAGNED:
    ∀ a a´, big2_thread_yield_spec a = Some a´ → CHECKUNCHAGNED a a´.
  Proof.
    unfold CHECKUNCHAGNED.
    intros.
    functional inversion H; subst.
    - simpl; refine_split; try reflexivity.
    - simpl; refine_split; try reflexivity.
  Qed.

  Lemma big2_sleep_yield_satisfies_CHECKUNCHAGNED:
    ∀ i a a´, big2_thread_sleep_spec i a = Some a´ → CHECKUNCHAGNED a a´.
  Proof.
    unfold CHECKUNCHAGNED.
    intros.
    functional inversion H; subst.
    - simpl; refine_split; try reflexivity.
    - simpl; refine_split; try reflexivity.
  Qed.


  Class PHThraed2TGenProp (s_oracle_prf : SingleOracle) :=
    {
      
      
      abs_rel_t_get_env_log_exist_prop :
        ∀ (l : Log) (e : LogEvent),
          lastEvType l ≠ Some LogYieldTy →
          getLogEventType e = LogYieldTy →
          match last_op (e :: l) with
          | Some (LEvent curid´ _) ⇒ proc_id (uRData l) = curid´
          | None ⇒ False
          end → ∃ l´´ : Log,
              TAsm.get_env_log limit (proc_id (uRData l)) (e :: l) = Some l´´ ∧ lastEvType l´´ = Some LogYieldTy;
      
      
      abs_rel_t_thread_yield_match_state_prop:
        ∀ l kctxt ae ev nb a a´ m´ l´´,
          lastEvType l ≠ Some LogYieldTy →
          relate_RData kctxt a l ae →
          TAsm.get_env_log limit (proc_id (uRData l)) (LEvent (proc_id (uRData l)) (LogYield (Mem.nextblock m´)) :: l) = Some l´´ →
          last_op l´´ = Some ev →
          getLogEventNB ev = Some nb →
          big2_thread_yield_spec a = Some a´ →
          CHECKUNCHAGNED a a´ →
          nb = (Mem.nextblock m´) ∧ relate_RData kctxt a´ (LEvent current_curid LogYieldBack :: l´´) ae;

      
      abs_rel_t_thread_sleep_match_state_prop:
        ∀ l kctxt ae ev cv nb a a´ m´ l´´,
          lastEvType l ≠ Some LogYieldTy →
          relate_RData kctxt a l ae →
          TAsm.get_env_log limit (proc_id (uRData l))
                           (LEvent (proc_id (uRData l))
                                   (LogSleep (Int.unsigned cv) (Mem.nextblock m´)
                                             (sync_chpool_check thread_sleep ((Lint cv)::nil) (uRData l) ae))
                                   :: l) = Some l´´ →
          last_op l´´ = Some ev →
          getLogEventNB ev = Some nb →
          big2_thread_sleep_spec (Int.unsigned cv) a = Some a´ →
          CHECKUNCHAGNED a a´ →
          nb = (Mem.nextblock m´) ∧ relate_RData kctxt a´ (LEvent current_curid LogYieldBack :: l´´) ae

    }.

  Lemma snap_rev_func_snap_func_eq_pd:
    ∀ pd, snap_rev_func (snap_func pd) = pd.
  Proof.
    intros.
    destruct pd; simpl.
    unfold snap_rev_func; simpl.
    unfold snap_func; simpl.
    auto.
  Qed.

  Lemma ptRead_related_t :
    ∀ n vadr kctxt l pd a res,
      n = ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) →
      relate_RData kctxt a l pd →
      ptRead_spec n vadr a = Some res →
      ∃ res´,
        single_ptRead_spec n vadr (uRData l, pd) = Some res ∧ res = res´.
  Proof.
    intros.
    unfold ptRead_spec in H1.
    unfold getPDE_spec, getPTE_spec in H1.
    unfold single_ptRead_spec in *; simpl in ×.
    unfold single_getPDE_spec, single_getPTE_spec in *; simpl.
    subdestruct; inv H1; inv H0; simpl; rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- init_re, <- cid_re;
    rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2; rewrite <- ptp_re; rewrite zeq_true, Hdestruct5.
    { rewrite zeq_true; eauto. }
    { rewrite zeq_false; auto; rewrite zlt_lt_true; eauto; rewrite Hdestruct8; auto; eauto. }
    { rewrite zeq_false; auto; rewrite zlt_lt_true; eauto; rewrite Hdestruct8; auto; eauto. }
    { rewrite zeq_true; eauto. }
    { rewrite zeq_true; eauto. }
    { rewrite zeq_true; eauto. }
  Qed.

End PHThread2TGenDEFINITION.