Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import PrimSemantics.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.

Require Import AbstractDataType.
Require Import MContainer.

Require Import Conventions.

Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.

Section ALINITGEN_DEFINE.

  Context `{real_params: RealParams}.
  Context `{oracle_prop: MultiOracleProp}.

  Notation LDATAOps := (cdata RData).

  Inductive getnps_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    getnps_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 n:
      find_symbol s NPS_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 0 = Some (Vint n) →
      kernel_mode (snd m´0) →
      getnps_spec_low_step s WB nil m´0 (Vint n) m´0.

  Inductive setnps_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    setnps_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 n:
      find_symbol s NPS_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 0 (Vint n) = Some m0 →
      kernel_mode (snd m´0) →
      setnps_spec_low_step s WB (Vint n :: nil) m´0 Vundef m0.

  Inductive getatu_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    getatu_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 n v v´:
      find_symbol s AT_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 (Int.unsigned n × 8 + 4) = Some (Vint v´) →
      Int.unsigned v = IntToBoolZ v´ →
      0 ≤ (Int.unsigned n) < maxpage →
      kernel_mode (snd m´0) →
      getatu_spec_low_step s WB (Vint n :: nil) m´0 (Vint v) m´0.

  Inductive setatu_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    setatu_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 n v:
      find_symbol s AT_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 (Int.unsigned n × 8 + 4) (Vint v) = Some m0 →
      0 ≤ (Int.unsigned n) < maxpage →
      kernel_mode (snd m´0) →
      setatu_spec_low_step s WB (Vint n :: Vint v :: nil) m´0 Vundef m0.

  Inductive getatc_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    getatc_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 n v:
      find_symbol s ATC_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 (Int.unsigned n × 4) = Some (Vint v) →
      0 ≤ (Int.unsigned n) < maxpage →
      kernel_mode (snd m´0) →
      getatc_spec_low_step s WB (Vint n :: nil) m´0 (Vint v) m´0.

  Inductive setatc_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    setatc_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 n v:
      find_symbol s ATC_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 (Int.unsigned n × 4) (Vint v) = Some m0 →
      0 ≤ (Int.unsigned n) < maxpage →
      kernel_mode (snd m´0) →
      setatc_spec_low_step s WB (Vint n :: Vint v :: nil) m´0 Vundef m0.

  Inductive getatnorm_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    getatnorm_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 n v v´:
      find_symbol s AT_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 (Int.unsigned n × 8) = Some (Vint v´) →
      Int.unsigned v = ZToATTypeZ (Int.unsigned v´) →
      0 ≤ (Int.unsigned n) < maxpage →
      kernel_mode (snd m´0) →
      getatnorm_spec_low_step s WB (Vint n :: nil) m´0 (Vint v) m´0.

  Inductive setatnorm_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    setatnorm_spec_low_intro s (WB: _ → Prop) (m´0 m0 m1 m2: mwd LDATAOps) b0 b1 n v:
      find_symbol s AT_LOC = Some b0 →
      find_symbol s ATC_LOC = Some b1 →
      Mem.store Mint32 m´0 b0 (Int.unsigned n × 8) (Vint v) = Some m0 →
      Mem.store Mint32 m0 b0 (Int.unsigned n × 8 + 4) Vzero = Some m1 →
      Mem.store Mint32 m1 b1 (Int.unsigned n × 4) Vzero = Some m2 →
      0 ≤ (Int.unsigned n) < maxpage →
      kernel_mode (snd m´0) →
      setatnorm_spec_low_step s WB (Vint n :: Vint v :: nil) m´0 Vundef m2.

  Inductive acquire_lock_AT_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
  | acquire_lock_AT_spec_low_intro
      s m´0 m0 b b0 l id adt adt´ rs
      (Hsymbol_PC: find_symbol s acquire_lock_AT = Some b)
      (HPC: rs PC = Vptr b Int.zero)
      (Hspec: acquire_lock_spec0 (Z.of_nat local_lock_bound)
                                 lock_AT_start 0 adt = Some (adt´, id, l))
      (Hsymbol: find_symbol s id = Some b0)
      (Hstorebytes: match l with
                      | Some l´ ⇒ Mem.storebytes m´0 b0 0 (ByteList l´) = Some m0
                      | _ ⇒ m0 = m´0
                    end)
      (Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m´0, adt))
      (Hlow: low_level_invariant (Mem.nextblock m´0) adt):
      let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                 :: IR EAX :: RA :: nil)
                             (undef_regs (List.map preg_of destroyed_at_call) rs)) in
      acquire_lock_AT_spec_low_step s rs (m´0, adt) (rs´#RA <- Vundef #PC <- (rs#RA)) (m0, adt´).

  Inductive release_lock_AT_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
  | release_lock_AT_spec_low_intro
      s m´0 b b0 l id adt adt´ rs size
      (Hsymbol_PC: find_symbol s release_lock_AT = Some b)
      (HPC: rs PC = Vptr b Int.zero)
      (Hspec: release_lock_spec0 lock_AT_start 0 l adt = Some adt´)
      (Hsize: id2size lock_AT_start = Some (size, id))
      (Hsymbol: find_symbol s id = Some b0)
      (Hloadbytes: Mem.loadbytes m´0 b0 0 size = Some (ByteList l))
      (Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m´0, adt))
      (Hlow: low_level_invariant (Mem.nextblock m´0) adt):
      let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                 :: IR EAX :: RA :: nil)
                             (undef_regs (List.map preg_of destroyed_at_call) rs)) in
      release_lock_AT_spec_low_step s rs (m´0, adt) (rs´#RA <- Vundef #PC <- (rs#RA)) (m´0, adt´).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

    Definition get_nps_spec_low: compatsem LDATAOps :=
      csem getnps_spec_low_step Tnil Tint32.

    Definition set_nps_spec_low: compatsem LDATAOps :=
      csem setnps_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.

    Definition at_get_spec_low: compatsem LDATAOps :=
      csem getatu_spec_low_step (type_of_list_type (Tint32::nil)) Tint32.

    Definition at_set_spec_low: compatsem LDATAOps :=
      csem setatu_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition is_norm_spec_low: compatsem LDATAOps :=
      csem getatnorm_spec_low_step (type_of_list_type (Tint32::nil)) Tint32.

    Definition set_norm_spec_low: compatsem LDATAOps :=
      csem setatnorm_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition at_get_c_spec_low: compatsem LDATAOps :=
      csem getatc_spec_low_step (type_of_list_type (Tint32::nil)) Tint32.

    Definition at_set_c_spec_low: compatsem LDATAOps :=
      csem setatc_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition acquire_lock_AT_spec_low: compatsem LDATAOps :=
      asmsem acquire_lock_AT acquire_lock_AT_spec_low_step.

    Definition release_lock_AT_spec_low: compatsem LDATAOps :=
      asmsem release_lock_AT release_lock_AT_spec_low_step.

  End WITHMEM.

End ALINITGEN_DEFINE.