Library mcertikos.multithread.flatmem.GuestAccessIntelDefPHB

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 GlobalOracleProp.
Require Import AuxSingleAbstractDataType.
Require Import SingleAbstractDataType.

Require Import FlatLoadStoreSemPHB.
Require Import LoadStoreDefPHB.

Require Import SingleOracle.

Section Load_Store.

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

  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{threads_conf_ops: ThreadsConfigurationOps}.

  Context `{HD: CompatData PData}.

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

  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 single_exec_guest_intel_accessor (adr: int) (chunk: memory_chunk) (m: mwd HDATAOps) (rs: regset) (rd: preg) :=
        let ofs := (Int.unsigned adr) in
        let adt:= (snd m) in
        let sh_adt := fst adt in
        let pv_adt := snd adt in
        if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid then
          match ZMap.get (EPT_PML4_INDEX ofs) (ept pv_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 single_exec_guest_intel_accessor_high_level_invariant:
        ∀ adr chunk m rs rd rs´ m´,
          single_exec_guest_intel_accessor 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 single_exec_guest_intel_accessor. intros. subdestruct.
        intros. eauto.
      Qed.

      Lemma single_exec_guest_intel_accessor_asm_invariant:
        ∀ chunk rd,
        ∀ adr m rs rs´ m´,
          single_exec_guest_intel_accessor 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 single_exec_guest_intel_accessor. intros. subdestruct.
        intros; eauto.
      Qed.

      Lemma single_exec_guest_intel_accessor_low_level_invariant:
        ∀ adr chunk m rs rd rs´ m´,
          single_exec_guest_intel_accessor 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 single_exec_guest_intel_accessor. intros. subdestruct.
        intros; eauto.
      Qed.

    End Accessor.

  End GE.

End Load_Store.