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 PAbQueueAtomic.
Require Import ObjCV.
Require Export Conventions.

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

Section Refinement.

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

  Notation LDATA := RData.

  Notation LDATAOps := (cdata LDATA).


  Definition IDQ_START := 0.
  Definition CV_START := num_proc × 8 + IDQ_START.
  Definition CH_START := num_cv × 28 + CV_START.
  Definition CH_SIZE := num_cv × 12 + CH_START.

  Inductive get_sync_chan_to_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    get_sync_chan_to_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 chanid to:
      find_symbol s SYNCCHPOOL_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 ((Int.unsigned chanid) × 16) = Some (Vint to) →
      0 ≤ (Int.unsigned chanid) < num_chan →
      kernel_mode (snd m´0) →
      get_sync_chan_to_spec_low_step s WB (Vint chanid :: nil) m´0 (Vint to) m´0.

  Inductive get_sync_chan_paddr_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    get_sync_chan_paddr_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 chanid paddr:
      find_symbol s SYNCCHPOOL_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 ((Int.unsigned chanid) × 16 + 4) = Some (Vint paddr) →
      0 ≤ (Int.unsigned chanid) < num_chan →
      kernel_mode (snd m´0) →
      get_sync_chan_paddr_spec_low_step s WB (Vint chanid :: nil) m´0 (Vint paddr) m´0.

  Inductive get_sync_chan_count_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    get_sync_chan_count_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 chanid count:
      find_symbol s SYNCCHPOOL_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 ((Int.unsigned chanid) × 16 + 8) = Some (Vint count) →
      0 ≤ (Int.unsigned chanid) < num_chan →
      kernel_mode (snd m´0) →
      get_sync_chan_count_spec_low_step s WB (Vint chanid :: nil) m´0 (Vint count) m´0.

  Inductive get_sync_chan_busy_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    get_sync_chan_busy_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 chanid busy:
      find_symbol s SYNCCHPOOL_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 ((Int.unsigned chanid) × 16 + 12) = Some (Vint busy) →
      0 ≤ (Int.unsigned chanid) < num_chan →
      kernel_mode (snd m´0) →
      get_sync_chan_busy_spec_low_step s WB (Vint chanid :: nil) m´0 (Vint busy) m´0.

  Inductive set_sync_chan_to_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    set_sync_chan_to_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 chanid to:
      find_symbol s SYNCCHPOOL_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 ((Int.unsigned chanid) × 16) (Vint to) = Some m0 →
      0 ≤ (Int.unsigned chanid) < num_chan →
      kernel_mode (snd m´0) →
      set_sync_chan_to_spec_low_step s WB (Vint chanid :: Vint to :: nil) m´0 Vundef m0.

  Inductive set_sync_chan_paddr_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    set_sync_chan_paddr_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 chanid paddr:
      find_symbol s SYNCCHPOOL_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 ((Int.unsigned chanid) × 16 + 4) (Vint paddr) = Some m0 →
      0 ≤ (Int.unsigned chanid) < num_chan →
      kernel_mode (snd m´0) →
      set_sync_chan_paddr_spec_low_step s WB (Vint chanid :: Vint paddr :: nil) m´0 Vundef m0.

  Inductive set_sync_chan_count_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    set_sync_chan_count_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 chanid count:
      find_symbol s SYNCCHPOOL_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 ((Int.unsigned chanid) × 16 + 8) (Vint count) = Some m0 →
      0 ≤ (Int.unsigned chanid) < num_chan →
      kernel_mode (snd m´0) →
      set_sync_chan_count_spec_low_step s WB (Vint chanid :: Vint count :: nil) m´0 Vundef m0.

  Inductive set_sync_chan_busy_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    set_sync_chan_busy_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 chanid busy:
      find_symbol s SYNCCHPOOL_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 ((Int.unsigned chanid) × 16 + 12) (Vint busy) = Some m0 →
      0 ≤ (Int.unsigned chanid) < num_chan →
      kernel_mode (snd m´0) →
      set_sync_chan_busy_spec_low_step s WB (Vint chanid :: Vint busy :: nil) m´0 Vundef m0.


  Inductive init_sync_chan_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    init_sync_chan_spec_low_intro s (WB: _ → Prop) (m0 m1 m2 m3 m4: mwd LDATAOps) b0 chanid:
      find_symbol s SYNCCHPOOL_LOC = Some b0 →
      Mem.store Mint32 m0 b0 (Int.unsigned chanid × 16) (Vint (Int.repr num_chan)) = Some m1 →
      Mem.store Mint32 m1 b0 (Int.unsigned chanid × 16 + 4) (Vint Int.zero) = Some m2 →
      Mem.store Mint32 m2 b0 (Int.unsigned chanid × 16 + 8) (Vint Int.zero) = Some m3 →
      Mem.store Mint32 m3 b0 (Int.unsigned chanid × 16 + 12) (Vint Int.zero) = Some m4 →
      0 ≤ (Int.unsigned chanid) < num_chan →
      kernel_mode (snd m0) →
      init_sync_chan_spec_low_step s WB (Vint chanid :: nil) m0 Vundef m4.


  Inductive get_kernel_pa_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    get_kernel_pa_spec_low_intro s (WB: _ → Prop) m´0 labd pid vaddr pa:
      get_kernel_pa_spec (Int.unsigned pid) (Int.unsigned vaddr) labd = Some (Int.unsigned pa) →
      0 ≤ (Int.unsigned pid) < num_proc →
      kernel_mode labd →
      get_kernel_pa_spec_low_step s WB (Vint pid :: Vint vaddr :: nil) (m´0, labd) (Vint pa) (m´0, labd).










  Inductive acquire_lock_SC_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
  | acquire_lock_SC_spec_low_intro
      s m´0 m0 b b0 l id adt adt´ rs sig index
      (Hsymbol_PC: find_symbol s acquire_lock_CHAN = Some b)
      (HPC: rs PC = Vptr b Int.zero)
      (Hspec: acquire_lock_spec2 (Z.of_nat local_lock_bound)
                                 ID_SC (Int.unsigned index) 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)
      (Hsig: sig = mksignature (AST.Tint::nil) None cc_default)
      (Hargs: extcall_arguments rs m´0 sig (Vint index :: nil))
      (Hrange: 0 ≤ Int.unsigned index < num_chan)
      (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_SC_spec_low_step s rs (m´0, adt) (rs´#RA <- Vundef #PC <- (rs#RA)) (m0, adt´).

  Inductive release_lock_SC_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
  | release_lock_SC_spec_low_intro
      s m´0 b b0 l id adt adt´ rs size sig index
      (Hsymbol_PC: find_symbol s release_lock_CHAN = Some b)
      (HPC: rs PC = Vptr b Int.zero)
      (Hspec: release_lock_spec2 ID_SC (Int.unsigned index) l adt = Some adt´)
      (Hsize: id2size ID_SC = Some (size, id))
      (Hsymbol: find_symbol s id = Some b0)
      (Hloadbytes: Mem.loadbytes m´0 b0 0 size = Some (ByteList l))
      (Hsig: sig = mksignature (AST.Tint::nil) None cc_default)
      (Hargs: extcall_arguments rs m´0 sig (Vint index :: nil))
      (Hrange: 0 ≤ Int.unsigned index < num_chan)
      (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_SC_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_sync_chan_to_spec_low: compatsem LDATAOps :=
      csem get_sync_chan_to_spec_low_step (type_of_list_type (Tint32::nil)) Tint32.

    Definition get_sync_chan_paddr_spec_low: compatsem LDATAOps :=
      csem get_sync_chan_paddr_spec_low_step (type_of_list_type (Tint32::nil)) Tint32.

    Definition get_sync_chan_count_spec_low: compatsem LDATAOps :=
      csem get_sync_chan_count_spec_low_step (type_of_list_type (Tint32::nil)) Tint32.

    Definition get_sync_chan_busy_spec_low: compatsem LDATAOps :=
      csem get_sync_chan_busy_spec_low_step (type_of_list_type (Tint32::nil)) Tint32.

    Definition set_sync_chan_to_spec_low: compatsem LDATAOps :=
      csem set_sync_chan_to_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition set_sync_chan_paddr_spec_low: compatsem LDATAOps :=
      csem set_sync_chan_paddr_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition set_sync_chan_count_spec_low: compatsem LDATAOps :=
      csem set_sync_chan_count_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition set_sync_chan_busy_spec_low: compatsem LDATAOps :=
      csem set_sync_chan_busy_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition init_sync_chan_spec_low: compatsem LDATAOps :=
      csem init_sync_chan_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.

    Definition get_kernel_pa_spec_low: compatsem LDATAOps :=
      csem get_kernel_pa_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tint32.


    Definition acquire_lock_SC_spec_low: compatsem LDATAOps :=
      asmsem_withsig acquire_lock_CHAN acquire_lock_SC_spec_low_step
                     (mksignature (AST.Tint::nil) None cc_default).

    Definition release_lock_SC_spec_low: compatsem LDATAOps :=
      asmsem_withsig release_lock_CHAN release_lock_SC_spec_low_step
                     (mksignature (AST.Tint::nil) None cc_default).

  End WITHMEM.

End Refinement.