Library mcertikos.multithread.phbthread.ObjPHBFlatMem

Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Integers.
Require Import Values.
Require Import ASTExtra.
Require Import Constant.

Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.

Require Import ObjFlatMem.
Require Import SingleAbstractDataType.
Require Import AuxSingleAbstractDataType.
Require Import SingleOracle.
Require Import AlgebraicMem.
Require Import GlobalOracleProp.

Section SINGLE_FLATMEM_SPEC.

  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{big_oracle_ops: BigOracleOps}.
  Context `{real_params_ops: RealParamsOps}.


  Function single_fload_spec (addr: Z) (d : PData) : option Z :=
    let pv_adt := snd d in
    match (ikern pv_adt, ihost pv_adt, ipt pv_adt) with
    | (true, true, true) ⇒
      if zle_lt 0 addr adr_low then
        match (ZMap.get (PageI (addr × 4)) (pperm pv_adt),
               FlatMem.load Mint32 (HP pv_adt) (addr × 4)) with
        | (PGAlloc, Vint n) ⇒ Some (Int.unsigned n)
        | _ ⇒ None
        end
      else None
    | _ ⇒ None
    end.

  Function single_flatmem_store (d: PData) (chunk: memory_chunk) (addr: Z) (v: val): option PData :=
    let pv_adt := snd d in
    match ZMap.get (PageI addr) (pperm pv_adt) with
    | PGAlloc ⇒ Some (fst d, pv_adt {pv_HP: FlatMem.store chunk (HP pv_adt) addr v})
    | _ ⇒ None
    end.

  Function single_fstore_spec (addr v: Z) (d : PData) : option PData :=
    let pv_adt := snd d in
    match (ikern pv_adt, ihost pv_adt, ipt pv_adt) with
      | (true, true, true) ⇒
        if zle_lt 0 addr adr_low
        then single_flatmem_store d Mint32 (addr × 4) (Vint (Int.repr v))
        else None
      | _ ⇒ None
    end.

  Function single_flatmem_copy_spec (count: Z) (from to: Z) (d: PData) : option PData :=
    match (ikern (snd d), ihost (snd d), ipt (snd d)) with
    | (true, true, true) ⇒
      if zle_lt 0 to adr_low then
        if zle_lt 0 from adr_low then
          if zle_le 0 count one_k then
            if Zdivide_dec PgSize to HPS then
              if Zdivide_dec PgSize from HPS then
                match (ZMap.get (PageI from) (pperm (snd d)), ZMap.get (PageI to) (pperm (snd d))) with
                | (PGAlloc, PGAlloc) ⇒
                  match flatmem_copy_aux (Z.to_nat count) from to (HP (snd d)) with
                  | Some h ⇒ Some (fst d, (snd d) {pv_HP: h})
                  | _ ⇒ None
                  end
                | _ ⇒ None
                end
              else None
            else None
          else None
        else None
      else None
    | _ ⇒ None
    end.

End SINGLE_FLATMEM_SPEC.