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

Require Import MQTicketLock.

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.

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

Section DCONSOLEBUFFINTROGEN_DEFINE.

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

  Notation LDATA := RData.

  Notation LDATAOps := (cdata LDATA).

  Inductive cons_buf_init_concrete_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    cons_buf_init_concrete_spec_low_intro s (WB: _ → Prop) (m´0 m0 m1: mwd LDATAOps) b0:
      find_symbol s cons_buf_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 (CONSOLE_BUFFER_SIZE × 4) (Vint (Int.zero)) = Some m0 →
      Mem.store Mint32 m0 b0 ((CONSOLE_BUFFER_SIZE + 1) × 4) (Vint (Int.zero)) = Some m1 →
      kernel_mode (snd m´0) →
      cons_buf_init_concrete_spec_low_step s WB nil m´0 Vundef m1.

  Inductive cons_buf_write_concrete_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | cons_buf_write_concrete_spec_low_intro1 s (WB: _ → Prop) (m´0 m0 m1: mwd LDATAOps) b0 rpos wpos wpos´ c:
      find_symbol s cons_buf_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
      0 ≤ Int.unsigned wpos < CONSOLE_BUFFER_SIZE →
      Mem.store Mint32 m´0 b0 (Int.unsigned wpos × 4) (Vint c) = Some m0 →
      wpos´ = Int.repr ((Int.unsigned wpos + 1) mod CONSOLE_BUFFER_SIZE) →
      Mem.load Mint32 m´0 b0 (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
      Int.unsigned wpos´ ≠ Int.unsigned rpos →
      Mem.store Mint32 m0 b0 ((CONSOLE_BUFFER_SIZE + 1) × 4) (Vint wpos´) = Some m1 →
      kernel_mode (snd m´0) →
      cons_buf_write_concrete_spec_low_step s WB (Vint c :: nil) m´0 Vundef m1
  | cons_buf_write_concrete_spec_low_intro2 s (WB: _ → Prop) (m´0 m0 m1 m2: mwd LDATAOps) b0 rpos rpos´ wpos wpos´ c:
      find_symbol s cons_buf_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
      0 ≤ Int.unsigned wpos < CONSOLE_BUFFER_SIZE →
      Mem.store Mint32 m´0 b0 (Int.unsigned wpos × 4) (Vint c) = Some m0 →
      wpos´ = Int.repr ((Int.unsigned wpos + 1) mod CONSOLE_BUFFER_SIZE) →
      Mem.store Mint32 m0 b0 ((CONSOLE_BUFFER_SIZE + 1) × 4) (Vint wpos´) = Some m1 →
      Mem.load Mint32 m´0 b0 (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
      Int.unsigned wpos´ = Int.unsigned rpos →
      rpos´ = Int.repr ((Int.unsigned rpos + 1) mod CONSOLE_BUFFER_SIZE) →
      Mem.store Mint32 m1 b0 (CONSOLE_BUFFER_SIZE × 4) (Vint rpos´) = Some m2 →
      kernel_mode (snd m´0) →
      cons_buf_write_concrete_spec_low_step s WB (Vint c :: nil) m´0 Vundef m2.

  Inductive cons_buf_read_concrete_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | cons_buf_read_concrete_spec_low_intro1 s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 rpos wpos:
      find_symbol s cons_buf_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
      Mem.load Mint32 m´0 b0 ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
      Int.unsigned rpos = Int.unsigned wpos →
      kernel_mode (snd m´0) →
      cons_buf_read_concrete_spec_low_step s WB nil m´0 (Vint Int.zero) m´0
  | cons_buf_read_concrete_spec_low_intro2 s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 rpos wpos c:
      find_symbol s cons_buf_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
      Mem.load Mint32 m´0 b0 ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
      Int.unsigned rpos ≠ Int.unsigned wpos →
      Mem.load Mint32 m´0 b0 ((Int.unsigned rpos) × 4) = Some (Vint c) →
      Mem.store Mint32 m´0 b0 (CONSOLE_BUFFER_SIZE × 4) (Vint (Int.repr((Int.unsigned rpos + 1) mod CONSOLE_BUFFER_SIZE))) = Some m0 →
      0 ≤ Int.unsigned rpos < CONSOLE_BUFFER_SIZE →
      kernel_mode (snd m´0) →
      cons_buf_read_concrete_spec_low_step s WB nil m´0 (Vint c) m0.

  Inductive cons_buf_wpos_concrete_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    cons_buf_wpos_concrete_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 wpos:
      find_symbol s cons_buf_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
      kernel_mode (snd m´0) →
      cons_buf_wpos_concrete_spec_low_step s WB nil m´0 (Vint wpos) m´0.

  Section WITHMEM.

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

    Definition cons_buf_init_concrete_spec_low: compatsem LDATAOps :=
      csem cons_buf_init_concrete_spec_low_step (type_of_list_type nil) Tvoid.

    Definition cons_buf_write_concrete_spec_low: compatsem LDATAOps :=
      csem cons_buf_write_concrete_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.

    Definition cons_buf_read_concrete_spec_low: compatsem LDATAOps :=
      csem cons_buf_read_concrete_spec_low_step (type_of_list_type nil) Tint32.

    Definition cons_buf_wpos_concrete_spec_low: compatsem LDATAOps :=
      csem cons_buf_wpos_concrete_spec_low_step (type_of_list_type nil) Tint32.

  End WITHMEM.

End DCONSOLEBUFFINTROGEN_DEFINE.