Library mcertikos.multithread.flatmem.FlatLoadStoreSemPHB

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 LoadStoreDefPHB.

Section Load_Store.

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


  Context `{HD: CompatData PData}.

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

  Context `{single_flatmem_store: PData → memory_chunk → Z → val → option (cdata PData)}.

  Definition single_exec_flatmem_load (chunk: memory_chunk) (m: mwd HDATAOps)
             (adr: Z) (rs: regset) (rd: preg) :=
    let h:= (HP (snd (snd m))) in
    Next (nextinstr_nf (rs#rd <- (FlatMem.load chunk h adr))) m.

  Lemma single_exec_flatmem_load_mem:
    ∀ chunk m adr rs rd rs´ m´,
      single_exec_flatmem_load chunk m adr rs rd = Next rs´ m´ →
      m´ = m.
  Proof. unfold single_exec_flatmem_load; simpl; intros; congruence. Qed.

  Lemma single_exec_flatmem_load_asm_invariant:
    ∀ chunk rd,
    ∀ TYP: subtype (type_of_chunk chunk) (typ_of_preg rd) = true,
    ∀ m adr rs rs´ m´,
      single_exec_flatmem_load chunk m adr rs rd = Next rs´ m´ →
      ∀ {F V} (ge: _ F V),
        AsmX.asm_invariant ge rs m →
        AsmX.asm_invariant ge rs´ m´.
  Proof.
    unfold single_exec_flatmem_load; simpl.
    inversion 2; subst.
    inversion 1; subst.
    inversion inv_inject_neutral; subst.
    constructor.
    - constructor; auto.
      apply nextinstr_nf_inject.
      apply set_reg_inject; auto.
      generalize (Mem.flat_inj (Mem.nextblock m´)).
      generalize (HP (@snd sharedData privData (@snd mem (@PData (@single_data oracle_ops big_ops)) m´))).
      clear.
      intros.
      destruct (FlatMem.load chunk f adr) eqn:?; try constructor.
      edestruct FlatMem.load_valid; eauto.
    - apply nextinstr_nf_wt; auto.
      apply set_reg_wt; auto.
      eapply Val.has_subtype; try eassumption.
      eapply FlatMem.load_type; auto.
  Qed.

  Definition single_exec_flatmem_store (chunk: memory_chunk) (m: mwd HDATAOps)
             (adr: Z) (rs: regset) (r1: preg) (destroyed: list preg) : Asm.outcome (mem:= mwd HDATAOps):=
    let abd := snd m in
    match single_flatmem_store abd chunk adr (rs r1) with
      | Some abd´ ⇒ Next (nextinstr_nf (undef_regs destroyed rs)) (fst m, abd´)
      | _ ⇒ Stuck
    end.

  Lemma single_exec_flatmem_store_fst_mem:
    ∀ chunk m adr rs r1 rs´ ds m´,
      single_exec_flatmem_store chunk m adr rs r1 ds = Next rs´ m´ →
      fst m´ = fst m.
  Proof.
    unfold single_exec_flatmem_store; intros.
    destruct (single_flatmem_store ((snd m): PData) chunk adr (rs r1)); contra_inv.
    inv H; reflexivity.
  Qed.

  Lemma single_exec_flatmem_store_asm_invariant:
    ∀ chunk m adr rs r1 rs´ ds m´,
      single_exec_flatmem_store chunk m adr rs r1 ds = Next rs´ m´ →
      ∀ {F V} (ge: _ F V),
        AsmX.asm_invariant ge rs m →
        AsmX.asm_invariant ge rs´ m´.
  Proof.
    unfold single_exec_flatmem_store; intros.
    destruct (single_flatmem_store ((snd m): PData) chunk adr (rs r1)); contra_inv.
    inv H.
    inv H0.
    inv inv_inject_neutral.
    constructor.
    - constructor; auto.
      apply nextinstr_nf_inject; auto.
      val_inject_simpl.
    - apply nextinstr_nf_wt; auto.
      apply undef_regs_wt; auto.
  Qed.

  Context {single_flat_inv: Single_FlatmemStoreInvariant (single_flatmem_store:= single_flatmem_store)}.

  Lemma single_exec_flatmem_store_low_level_invariant´:
    ∀ chunk m adr rs r1 rs´ ds m´,
      single_exec_flatmem_store chunk m adr rs r1 ds = Next rs´ m´ →
      ∀ n,
        CompatData.low_level_invariant n (snd m) →
        CompatData.low_level_invariant n (snd m´).
  Proof.
    unfold single_exec_flatmem_store; intros.
    destruct (single_flatmem_store ((snd m): PData) chunk adr (rs r1)) eqn: HST; contra_inv.
    inv H; simpl.
    eapply single_flatmem_store_low_level_invariant; eauto.
  Qed.

  Lemma single_exec_flatmem_store_low_level_invariant:
    ∀ chunk m adr rs r1 rs´ ds m´,
      single_exec_flatmem_store chunk m adr rs r1 ds = Next rs´ m´ →
      CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
      CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
  Proof.
    intros until 1.
    replace (Mem.nextblock m´) with (Mem.nextblock m).
    eapply single_exec_flatmem_store_low_level_invariant´; eauto.
    exploit single_exec_flatmem_store_fst_mem; eauto.
    clear.
    simpl; lift_trivial.
    congruence.
  Qed.

  Lemma single_exec_flatmem_store_high_level_invariant:
    ∀ chunk m adr rs r1 rs´ ds m´,
      single_exec_flatmem_store chunk m adr rs r1 ds = Next rs´ m´ →
      (adr mod PgSize ≤ PgSize - size_chunk chunk)%Z →
      high_level_invariant (snd m) →
      high_level_invariant (snd m´).
  Proof.
    unfold single_exec_flatmem_store; intros.
    destruct (single_flatmem_store ((snd m): PData) chunk adr (rs r1)) eqn: HST; contra_inv.
    inv H.
    simpl.
    eapply single_flatmem_store_high_level_invariant; eauto.
  Qed.

End Load_Store.