Library mcertikos.multithread.flatmem.LoadStoreDefPHB

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.

Section DEF.

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

  Function single_trapinfo_set (d: PData) (addr: int) (ra: val) : PData := ((fst d), (snd d) {pv_ti: (addr, ra)}).

  Class Single_KernelModeImplies: Prop :=
    {
      single_kernel_mode_implies: ∀ (d : PData),
        kernel_mode d → (ikern (snd d) = true ∧ ihost (snd d) = true)
    }.

  Class Single_TrapinfoSetInvariant: Prop :=
    {
      single_trapinfo_set_high_level_invariant:
        ∀ abd,
          high_level_invariant abd →
          ∀ adr v,
            high_level_invariant (single_trapinfo_set abd adr v)
      ;

      single_trapinfo_set_low_level_invariant:
        ∀ n abd,
          CompatData.low_level_invariant n abd →
          ∀ v,
            Val.has_type v AST.Tint →
            val_inject (Mem.flat_inj n) v v →
            ∀ adr,
              CompatData.low_level_invariant n (single_trapinfo_set abd adr v)
    }.

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

  Class Single_FlatmemStoreInvariant: Prop :=
    {
      single_flatmem_store_low_level_invariant:
        ∀ abd n,
          CompatData.low_level_invariant n abd →
          ∀ chunk adr v abd´,
            single_flatmem_store abd chunk adr v = Some abd´ →
            CompatData.low_level_invariant n abd´
      ;

      single_flatmem_store_high_level_invariant:
        ∀ abd,
          high_level_invariant abd →
          ∀ chunk adr v abd´,
            (adr mod PgSize ≤ PgSize - size_chunk chunk)%Z →
            single_flatmem_store abd chunk adr v = Some abd´ →
            high_level_invariant abd´
    }.

  Lemma single_PTADDR_mod_lt:
    ∀ adr n,
      (adr mod PgSize ≤ PgSize - n)%Z →
      ∀ i,
        (PTADDR i adr mod PgSize ≤ PgSize - n)%Z.
  Proof.
    unfold PTADDR. intros. rewrite Zplus_comm.
    rewrite Z_mod_plus_full. rewrite Zmod_mod.
    assumption.
  Qed.

End DEF.

Hint Extern 10 (Single_KernelModeImplies) ⇒
(constructor; simpl; tauto):
  typeclass_instances.