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

Require Import Conventions.

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

Section ALINITGEN_DEFINE.

  Context `{multi_oracle_prop: MultiOracleProp}.

  Notation LDATAOps := (cdata RData).

  Inductive incr_now_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    incr_now_spec_low_intro s (WB: _ → Prop) m m´ b i n d d´ ofs pos:
      ∀ (Hsymbol: find_symbol s TICKET_LOCK_LOC = Some b)
             (Hspec: log_incr_spec (Int.unsigned i) (Int.unsigned ofs) d = Some d´)
             (Hpos: index2Z (Int.unsigned i) (Int.unsigned ofs) = Some pos)
             (Hload0: Mem.load Mint32 m b (pos × 8 + 4) = Some (Vint n))
             (Hstore1: Mem.store Mint32 m b (pos × 8 + 4) (Vint (Int.add n Int.one)) = Some m´)
             (Hkern: kernel_mode d),
             incr_now_spec_low_step s WB (Vint i :: Vint ofs :: nil) (m, d) Vundef (m´, d´).

  Inductive init_ticket_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    init_ticket_spec_low_intro s (WB: _ → Prop) m m0 m´ b i d d´ ofs pos:
      ∀ (Hsymbol: find_symbol s TICKET_LOCK_LOC = Some b)
             (Hspec: log_init_spec (Int.unsigned i) (Int.unsigned ofs) d = Some d´)
             (Hpos: index2Z (Int.unsigned i) (Int.unsigned ofs) = Some pos)
             (Hstore0: Mem.store Mint32 m b (pos × 8) Vzero = Some m0)
             (Hstore1: Mem.store Mint32 m0 b (pos × 8 + 4) Vzero = Some m´)
             (Hkern: kernel_mode d),
             init_ticket_spec_low_step s WB (Vint i :: Vint ofs :: nil) (m, d) Vundef (m´, d´).

  Inductive get_now_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
    get_now_spec_low_intro s m m0 m´ b b0 i t n d d´ rs sig ofs pos:
      ∀ (Hsymbol0: find_symbol s get_now = Some b0)
             (HPC: rs PC = Vptr b0 Int.zero)
             (Hsymbol: find_symbol s TICKET_LOCK_LOC = Some b)
             (Hspec: log_get_spec (Int.unsigned i) (Int.unsigned ofs) d = Some (d´, (t, n)))
             (Hpos: index2Z (Int.unsigned i) (Int.unsigned ofs) = Some pos)
             (Hstore0: Mem.store Mint32 m b (pos × 8) (Vint (Int.repr t)) = Some m0)
             (Hstore1: Mem.store Mint32 m0 b (pos × 8 + 4) (Vint (Int.repr n)) = Some m´)
             (Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m, d))
             (Hlow: low_level_invariant (Mem.nextblock m) d)
             (Hhigh: high_level_invariant d)
             
             (Hsig: sig = mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default)
             (Harg: extcall_arguments rs m sig (Vint i ::Vint ofs :: nil)),
             let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                        :: RA :: nil)
                                    (undef_regs (List.map preg_of destroyed_at_call) rs)) in
             get_now_spec_low_step s rs (m, d) (rs´#PC <- (rs#RA) #EAX <- (Vint (Int.repr n))) (m´, d´).

  Inductive incr_ticket_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
    incr_ticket_spec_low_intro s m m0 m´ b b0 bound i t n d d´ rs sig ofs pos:
      ∀ (Hsymbol0: find_symbol s incr_ticket = Some b0)
             (HPC: rs PC = Vptr b0 Int.zero)
             (Hsymbol: find_symbol s TICKET_LOCK_LOC = Some b)
             (Hspec: atomic_FAI_spec (Int.unsigned bound) (Int.unsigned i) (Int.unsigned ofs)
                                     d = Some (d´, (t, n)))
             (Hpos: index2Z (Int.unsigned i) (Int.unsigned ofs) = Some pos)
             (Hstore0: Mem.store Mint32 m b (pos × 8) (Vint (Int.repr (Int.unsigned (Int.repr (t + 1))))) = Some m0)
             (Hstore1: Mem.store Mint32 m0 b (pos × 8 + 4) (Vint (Int.repr n)) = Some m´)
             (Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m, d))
             (Hlow: low_level_invariant (Mem.nextblock m) d)
             (Hhigh: high_level_invariant d)
             
             (Hsig: sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default)
             (Harg: extcall_arguments rs m sig (Vint bound :: Vint i :: Vint ofs :: nil)),
             let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                        :: RA :: nil)
                                    (undef_regs (List.map preg_of destroyed_at_call) rs)) in
             incr_ticket_spec_low_step s rs (m, d) (rs´#PC <- (rs#RA) #EAX <- (Vint (Int.repr t))) (m´, d´).


  Section WITHMEM.

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

    Definition incr_now_spec_low: compatsem LDATAOps :=
      csem incr_now_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition init_ticket_spec_low: compatsem LDATAOps :=
      csem init_ticket_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition get_now_spec_low: compatsem LDATAOps :=
      asmsem_withsig get_now get_now_spec_low_step
                     (mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default).

    Definition incr_ticket_spec_low: compatsem LDATAOps :=
      asmsem_withsig incr_ticket incr_ticket_spec_low_step
                     (mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default).


  End WITHMEM.

End ALINITGEN_DEFINE.