Library mcertikos.flatmem.GuestAccessIntelDef2high

Require Import Coqlib.
Require Import Maps.
Require Import Globalenvs.
Require Import ASTExtra.
Require Import AsmX.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import LAsm.
Require Import AuxStateDataType.
Require Import Constant.
Require Import FlatMemory.
Require Import GlobIdent.
Require Import Integers.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import AsmImplLemma.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.ClightModules.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatClightSem.
Require Import liblayers.compcertx.MemWithData.

Require Import AbstractDataType.
Require Import FlatLoadStoreSem.
Require Import LoadStoreDef.

Require Import SingleOracle.

Section Load_Store.

  Context `{Hmem: Mem.MemoryModel}.
  Context `{HD: CompatData RData}.
  Context `{Hmwd: UseMemWithData mem}.

  Context `{threads_conf_ops: ThreadsConfigurationOps}.

  Notation HDATAOps := (cdata (cdata_ops := data_ops) RData).

  Section GE.

    Context {F V} (ge: Genv.t F V).

    Section Accessor.

      Variable accessor: Z → Z → memory_chunk → (mwd HDATAOps) → regset → preg → Asm.outcome (mem:= mwd HDATAOps).

      Definition exec_guest_intel_accessor2high (adr: int) (chunk: memory_chunk) (m: mwd HDATAOps) (rs: regset) (rd: preg) :=
        let ofs := (Int.unsigned adr) in
        let adt:= (snd m) in
        if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid then
          match ZMap.get (EPT_PML4_INDEX ofs) (ZMap.get (CPU_ID adt) (ept adt)) with
            | EPML4EValid epdpt ⇒
              match ZMap.get (EPT_PDPT_INDEX ofs) epdpt with
                | EPDPTEValid epdt ⇒
                  match ZMap.get (EPT_PDIR_INDEX ofs) epdt with
                    | EPDTEValid eptab ⇒
                      match ZMap.get (EPT_PTAB_INDEX ofs) eptab with
                        | EPTEValid n ⇒
                          accessor n ofs chunk m rs rd
                        | _ ⇒ Stuck
                      end
                    | _ ⇒ Stuck
                  end
                | _ ⇒ Stuck
              end
            | _ ⇒ Stuck
          end
        else Stuck.

      Lemma exec_guest_intel_accessor2high_high_level_invariant:
        ∀ adr chunk m rs rd rs´ m´,
          exec_guest_intel_accessor2high adr chunk m rs rd = Next rs´ m´ →
          high_level_invariant (snd m) →
          (∀ i i´,
             accessor i i´ chunk m rs rd = Next rs´ m´ →
             high_level_invariant (snd m´)) →
          high_level_invariant (snd m´).
      Proof.
        unfold exec_guest_intel_accessor2high. intros. subdestruct.
        intros. eauto.
      Qed.

      Lemma exec_guest_intel_accessor2high_asm_invariant:
        ∀ chunk rd,
        ∀ adr m rs rs´ m´,
          exec_guest_intel_accessor2high adr chunk m rs rd = Next rs´ m´ →
          AsmX.asm_invariant ge rs m →
          (∀ i i´,
             accessor i i´ chunk m rs rd = Next rs´ m´ →
             AsmX.asm_invariant ge rs´ m´) →
          AsmX.asm_invariant ge rs´ m´.
      Proof.
        unfold exec_guest_intel_accessor2high. intros. subdestruct.
        intros; eauto.
      Qed.

      Lemma exec_guest_intel_accessor2high_low_level_invariant:
        ∀ adr chunk m rs rd rs´ m´,
          exec_guest_intel_accessor2high adr chunk m rs rd = Next rs´ m´ →
          CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
          (∀ i i´,
             accessor i i´ chunk m rs rd = Next rs´ m´ →
             CompatData.low_level_invariant (Mem.nextblock m´) (snd m´)) →
          CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
      Proof.
        unfold exec_guest_intel_accessor2high. intros. subdestruct.
        intros; eauto.
      Qed.

    End Accessor.

  End GE.


End Load_Store.

Section Refinement.

  Context `{Hmem: Mem.MemoryModel}.
  Context `{Hmwd: UseMemWithData mem}.
  Context `{HD: CompatData RData}.
  Context `{HD0: CompatData RData}.

  Context `{threads_conf_ops: ThreadsConfigurationOps}.

  Notation HDATAOps := (cdata (cdata_ops := data_ops) RData).
  Notation LDATAOps := (cdata (cdata_ops := data_ops0) RData).
  Context `{rel_prf: CompatRel (mem:=mem) (memory_model_ops:= memory_model_ops) (D1 := HDATAOps) (D2:=LDATAOps)}.
  Context `{Hstencil: Stencil stencil (stencil_ops:= stencil_ops)}.

  Context `{haccessor: Z → Z → memory_chunk → (mwd HDATAOps) → regset → preg → Asm.outcome (mem:= mwd HDATAOps)}.
  Context `{laccessor: Z → Z → memory_chunk → (mwd LDATAOps) → regset → preg → Asm.outcome (mem:= mwd LDATAOps)}.

  Section General.

    Opaque align_chunk Z.mul Z.div Z.sub.

    Context {inv: relate_impl_ept}.
    Context {inv2: relate_impl_CPU_ID}.
    Context {inv3: relate_impl_cid}.

    Lemma guest_intel_correct2high:
      ∀ m1 m1´ m2 d1 d2 d1´ rs1 rs2 rs1´ f s rd t i,
        exec_guest_intel_accessor2high haccessor i t (m1, d1) rs1 rd = Next rs1´ (m1´, d1´)
        → MatchPrimcallStates (one_crel HDATAOps LDATAOps) s f rs1 m1 d1 rs2 m2 d2
        → ∀ ACCESSOR_CORRECT:
                    (∀ i i´, haccessor i i´ t (m1, d1) rs1 rd = Next rs1´ (m1´, d1´) →
                                  ∃ r´0 m2´ d2´,
                                    laccessor i i´ t (m2, d2) rs2 rd = Next r´0 (m2´, d2´) ∧
                                    MatchPrimcallStates (one_crel HDATAOps LDATAOps) s f rs1´ m1´ d1´ r´0 m2´ d2´),
           ∃ r´0 m2´ d2´,
             exec_guest_intel_accessor2high laccessor i t (m2, d2) rs2 rd = Next r´0 (m2´, d2´)
             ∧ MatchPrimcallStates (one_crel HDATAOps LDATAOps) s f rs1´ m1´ d1´ r´0 m2´ d2´.
    Proof.
      unfold exec_guest_intel_accessor2high; simpl. intros.
      pose proof H0 as Hmatch.
      inv H0. inv match_extcall_states.
      erewrite <- relate_impl_ept_eq; eauto.
      erewrite <- relate_impl_CPU_ID_eq; eauto.
      erewrite <- relate_impl_cid_eq; eauto.
      subdestruct. eauto.
    Qed.

  End General.

End Refinement.