Library mcertikos.flatmem.LoadStoreSem3high

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 HostAccess2high.
Require Import GuestAccessIntel2high.
Require Export LoadStoreDef.
Require Import GuestAccessIntelDef2high.

Require Import SingleOracle.

Section Load_Store.

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

  Context `{threads_conf_ops: ThreadsConfigurationOps}.

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

  Context `{trap_inv: TrapinfoSetInvariant (data_ops := data_ops)}.
  Context `{flatmem_store: RData → memory_chunk → Z → val → option (cdata RData)}.

  Section GE.

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

    Definition exec_loadex3high (chunk: memory_chunk) (m: mwd HDATAOps)
               (a: addrmode) (rs: regset) (rd: preg) :=
      let adt:= (snd m) in
      match (eval_addrmode ge a rs) with
        | Vptr b ofs ⇒
          match (ikern adt, ihost adt) with
            | (true, true) ⇒ Asm.exec_load ge chunk m a rs rd
            | _ ⇒ Stuck
          end
        | Vint adr ⇒
          match (init adt, ihost adt, pg adt, ikern adt) with
            | (true, true, true, false) ⇒ exec_host_load2high ge adr chunk m rs rd
            | (true, false, _, _) ⇒ exec_guest_intel_load2high adr chunk m rs rd
            | _ ⇒ Stuck
          end
        | _ ⇒ Stuck
      end.

      Definition exec_storeex3high (chunk: memory_chunk) (m: mwd HDATAOps)
                 (a: addrmode) (rs: regset) (rd: preg) (destroyed: list preg) :=
        let adt:= (snd m) in
        match (eval_addrmode ge a rs) with
          | Vptr b ofs ⇒
            match (ikern adt, ihost adt) with
              | (true, true) ⇒ Asm.exec_store ge chunk m a rs rd destroyed
              | _ ⇒ Stuck
            end
          | Vint adr ⇒
            match (init adt, ihost adt, pg adt, ikern adt) with
              | (true, true, true, false) ⇒ exec_host_store2high (flatmem_store:= flatmem_store) ge adr chunk m rs rd destroyed
              | (true, false, _, _) ⇒ exec_guest_intel_store2high (flatmem_store:= flatmem_store) adr chunk m rs rd destroyed
              | _ ⇒ Stuck
            end
          | _ ⇒ Stuck
        end.

      Local Existing Instance Asm.mem_accessors_default.
      Local Existing Instance AsmX.mem_accessors_default_invariant.

      Lemma exec_loadex3high_high_level_invariant:
        ∀ adr chunk m rs rd rs´ m´,
          exec_loadex3high chunk m adr rs rd = Next rs´ m´ →
          high_level_invariant (snd m) →
          high_level_invariant (snd m´).
      Proof.
        unfold exec_loadex3high. intros until m´.
        destruct (eval_addrmode ge adr rs); try discriminate.
        - destruct (init (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          destruct (pg (snd m)); destruct (ikern (snd m)); try discriminate.
          + eapply exec_host_load2high_high_level_invariant; eauto.
          + eapply exec_guest_intel_load2high_high_level_invariant; eauto.
        - destruct (ikern (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          unfold Asm.exec_load. destruct (Mem.loadv chunk m (eval_addrmode ge adr rs)); try discriminate.
          congruence.
      Qed.

      Lemma exec_loadex3high_asm_invariant:
        ∀ chunk rd,
        ∀ TYP: subtype (type_of_chunk chunk) (typ_of_preg rd) = true,
        ∀ adr m rs rs´ m´,
          exec_loadex3high chunk m adr rs rd = Next rs´ m´ →
          AsmX.asm_invariant ge rs m →
          AsmX.asm_invariant ge rs´ m´.
      Proof.
        unfold exec_loadex3high. intros until m´.
        destruct (eval_addrmode ge adr rs); try discriminate.
        - destruct (init (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          destruct (pg (snd m)); destruct (ikern (snd m)); try discriminate.
          + eapply exec_host_load2high_asm_invariant; eauto.
          + intros; eapply exec_guest_intel_load2high_asm_invariant; eauto.
        - destruct (ikern (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          intros; eapply exec_load_invariant; eauto.
      Qed.

      Lemma exec_loadex3high_low_level_invariant:
        ∀ adr chunk m rs rd rs´ m´,
          exec_loadex3high chunk m adr rs rd = Next rs´ m´ →
          AsmX.asm_invariant ge rs m →
          CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
          CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
      Proof.
        unfold exec_loadex3high. intros until m´.
        destruct (eval_addrmode ge adr rs); try discriminate.
        - destruct (init (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          destruct (pg (snd m)); destruct (ikern (snd m)); try discriminate.
          + eapply exec_host_load2high_low_level_invariant; eauto.
          + intros; eapply exec_guest_intel_load2high_low_level_invariant; eauto.
        - destruct (ikern (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          unfold Asm.exec_load. destruct (Mem.loadv chunk m (eval_addrmode ge adr rs)); try discriminate.
          congruence.
      Qed.

      Context {flat_inv: FlatmemStoreInvariant (data_ops := data_ops) (flatmem_store:= flatmem_store)}.

      Lemma exec_storeex3high_high_level_invariant:
        ∀ adr chunk m rs rd des rs´ m´,
          exec_storeex3high chunk m adr rs rd des = Next rs´ m´ →
          high_level_invariant (snd m) →
          high_level_invariant (snd m´).
      Proof.
        unfold exec_storeex3high. intros until m´.
        destruct (eval_addrmode ge adr rs); try discriminate.
        - destruct (init (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          destruct (pg (snd m)); destruct (ikern (snd m)); try discriminate.
          + eapply exec_host_store2high_high_level_invariant; eauto.
          + eapply exec_guest_intel_store2high_high_level_invariant; eauto.
        - destruct (ikern (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          unfold Asm.exec_store. destruct (Mem.storev chunk m (eval_addrmode ge adr rs) (rs rd)) eqn:Heqo; try discriminate.
          destruct (eval_addrmode ge adr rs); try discriminate.
          lift_unfold.
          destruct Heqo as [? DATA].
          unfold π_data in DATA. simpl in × |- ×. congruence.
      Qed.

      Lemma exec_storeex3high_asm_invariant:
        ∀ chunk rd,
        ∀ adr m des rs rs´ m´,
          exec_storeex3high chunk m adr rs rd des = Next rs´ m´ →
          AsmX.asm_invariant ge rs m →
          AsmX.asm_invariant ge rs´ m´.
      Proof.
        unfold exec_storeex3high. intros until m´.
        destruct (eval_addrmode ge adr rs); try discriminate.
        - destruct (init (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          destruct (pg (snd m)); destruct (ikern (snd m)); try discriminate.
          + eapply exec_host_store2high_asm_invariant; eauto.
          + intros; eapply exec_guest_intel_store2high_asm_invariant; eauto.
        - destruct (ikern (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          intros; eapply exec_store_invariant; eauto.
      Qed.

      Lemma exec_storeex3high_low_level_invariant:
        ∀ adr chunk m rs rd des rs´ m´,
          exec_storeex3high chunk m adr rs rd des = Next rs´ m´ →
          AsmX.asm_invariant ge rs m →
          CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
          CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
      Proof.
        unfold exec_storeex3high. intros until m´.
        destruct (eval_addrmode ge adr rs); try discriminate.
        - destruct (init (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          destruct (pg (snd m)); destruct (ikern (snd m)); try discriminate.
          + eapply exec_host_store2high_low_level_invariant; eauto.
          + intros; eapply exec_guest_intel_store2high_low_level_invariant; eauto.
        - destruct (ikern (snd m)); try discriminate.
          destruct (ihost (snd m)); try discriminate.
          unfold Asm.exec_store. destruct (Mem.storev chunk m (eval_addrmode ge adr rs) (rs rd)) eqn:Heqo; try discriminate.
          destruct (eval_addrmode ge adr rs); try discriminate.
          lift_unfold.
          destruct Heqo as [? DATA].
          unfold π_data in DATA. simpl in × |- ×.
          injection 1; intros; subst.
          erewrite Mem.nextblock_store; eauto.
          congruence.
      Qed.

  End GE.

  Context `{KernelModeImplies (data_ops:= data_ops)}.
  Context {flat_inv: FlatmemStoreInvariant (data_ops := data_ops) (flatmem_store:= flatmem_store)}.

  Global Instance load_accessor_prf3high:
    LoadAccessor _ (@exec_loadex3high).
  Proof.
    constructor.
    {
      unfold exec_loadex3high; intros.
      erewrite AsmX.eval_addrmode_symbols_preserved; eauto.
      destruct (eval_addrmode ge1 a rs); try reflexivity.
      - destruct (init (snd m)); try reflexivity.
        destruct (ihost (snd m)); try reflexivity.
        destruct (pg (snd m)); destruct (ikern (snd m)); try reflexivity.
        + unfold exec_host_load2high.
          unfold exec_pagefault. rewrite SYMB. reflexivity.
      - unfold Asm.exec_load. erewrite AsmX.eval_addrmode_symbols_preserved; eauto.
    }
    {
      intros. apply kernel_mode_implies in H1.
      destruct H1 as [IKERN IHOST].
      unfold exec_loadex3high.
      unfold Asm.exec_load in H0 |- ×.
      destruct (eval_addrmode ge a rs); try discriminate.
      unfold π_data in IKERN, IHOST.
      rewrite IKERN. rewrite IHOST.
      assumption.
    }
    {
      intros; eapply exec_loadex3high_asm_invariant; eauto.
    }
    {
      intros; eapply exec_loadex3high_low_level_invariant; eauto.
    }
    {
      intros; eapply exec_loadex3high_high_level_invariant; eauto.
    }
  Qed.

  Global Instance store_accessor_prf3high:
    StoreAccessor _ (@exec_storeex3high).
  Proof.
    constructor.
    {
      unfold exec_storeex3high. intros.
      erewrite AsmX.eval_addrmode_symbols_preserved; eauto.
      destruct (eval_addrmode ge1 a rs); try reflexivity.
      - destruct (init (snd m)); try reflexivity.
        destruct (ihost (snd m)); try reflexivity.
        destruct (pg (snd m)); destruct (ikern (snd m)); try reflexivity.
        + unfold exec_host_store2high.
          unfold exec_pagefault. rewrite SYMB. reflexivity.
      - unfold Asm.exec_store. erewrite AsmX.eval_addrmode_symbols_preserved; eauto.
    }
    {
      intros. apply kernel_mode_implies in H1.
      destruct H1 as [IKERN IHOST].
      unfold exec_storeex3high.
      unfold Asm.exec_store in H0 |- ×.
      destruct (eval_addrmode ge a rs); try discriminate.
      unfold π_data in IKERN, IHOST.
      rewrite IKERN. rewrite IHOST.
      assumption.
    }
    {
      intros; eapply exec_storeex3high_asm_invariant; eauto.
    }
    {
      intros; eapply exec_storeex3high_low_level_invariant; eauto.
    }
    {
      intros; eapply exec_storeex3high_high_level_invariant; eauto.
    }
  Qed.

End Load_Store.

Require Import LoadStoreGeneral.

Section Load_Store_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 `{trapinfo_inv: TrapinfoSetInvariant (data_ops:= data_ops)}.
  Context `{kern_inv: KernelModeImplies (data_ops:= data_ops)}.

  Context `{hflatmem_store: RData → memory_chunk → Z → val → option RData}.
  Context `{lflatmem_store: RData → memory_chunk → Z → val → option RData}.

  Section Load_Store3high.

    Context {loadstoreprop: LoadStoreProp (hflatmem_store:= hflatmem_store) (lflatmem_store:= lflatmem_store)}.
    Context {re: relate_impl_CR3}.
    Context {re1: relate_impl_HP´}.
    Context {re2: relate_impl_iflags}.
    Context {re3: relate_impl_PT}.
    Context {re4: relate_impl_ptpool}.
    Context {re5: relate_impl_ept}.
    Context {re6: relate_impl_CPU_ID}.
    Context {re7: relate_impl_cid}.
    Context {re8: relate_impl_init}.
    Context {re9: relate_impl_pperm}.

    Notation hLoad := (fun F V ⇒ exec_loadex3high (F:=F) (V:=V)).
    Notation lLoad := (fun F V ⇒ exec_loadex3high (F:=F) (V:=V)).
    Notation hStore := (fun F V ⇒ exec_storeex3high (F:=F) (V:=V) (flatmem_store:= hflatmem_store)).
    Notation lStore := (fun F V ⇒ exec_storeex3high (F:=F) (V:=V) (flatmem_store:= lflatmem_store)).

    Lemma load_correct3high:
      load_accessor_sim_def HDATAOps LDATAOps (one_crel HDATAOps LDATAOps) hLoad lLoad.
    Proof.
      unfold load_accessor_sim_def. intros.
      pose proof H2 as Hmatch.
      inv H2. inv match_extcall_states.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_init_eq; eauto; intro init_eq.
      pose proof (stencil_matches_preserves_trans _ _ _ _ _ _ _ H0 H) as Hpre.
      erewrite exec_load_symbols_preserved in H1; try eapply Hpre.
      unfold exec_loadex3high in *; simpl in ×.
      rewrite <- init_eq, <- ihost_eq, <- ikern_eq, <- pg_eq.
      exploit (eval_addrmode_correct ge2 ge2 a); eauto. simpl; intros HW.
      destruct (eval_addrmode ge2 a rs1) eqn: HEVAL; contra_inv; inv HW; simpl in *; subdestruct.
      - eapply host_load_correct2high; eauto.
      - eapply guest_intel_load_correct2high; eauto.
      - eapply loadl_correct; eauto.
    Qed.

    Lemma store_correct3high:
      store_accessor_sim_def HDATAOps LDATAOps (one_crel HDATAOps LDATAOps) hStore lStore.
    Proof.
      unfold store_accessor_sim_def. intros.
      pose proof H2 as Hmatch.
      inv H2. inv match_extcall_states.
      exploit relate_impl_iflags_eq; eauto. inversion 1.
      exploit relate_impl_init_eq; eauto; intro init_eq.
      pose proof (stencil_matches_preserves_trans _ _ _ _ _ _ _ H0 H) as Hpre.
      unfold exec_storeex3high in ×. simpl in ×.
      rewrite <- init_eq, <- ihost_eq, <- ikern_eq, <- pg_eq.
      exploit (eval_addrmode_correct ge1 ge2 a); eauto. simpl; intros HW.
      destruct (eval_addrmode ge1 a rs1) eqn: HEVAL; contra_inv; inv HW; simpl in *; subdestruct.
      - eapply host_store_correct2high; eauto.
      - eapply guest_intel_store_correct2high; eauto.
      - eapply storel_correct; eauto.
    Qed.

  End Load_Store3high.

End Load_Store_Refinement.