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.

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

Require Import AbstractDataType.
Require Import MHTicketLockOp.
Require Import Conventions.
Require Import ObjQLock.

Section TICKETLOCK_DEFINE.

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

  Notation LDATAOps := (cdata RData).

  Inductive acquire_lock_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
  | acquire_lock_spec_low_intro
      s m´0 m0 b b0 l id adt adt´ rs i ofs bound sig
      (Hsymbol_PC: find_symbol s acquire_lock = Some b)
      (HPC: rs PC = Vptr b Int.zero)
      (Hspec: acquire_lock_spec0 (Int.unsigned bound) (Int.unsigned i) (Int.unsigned ofs) 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)
      (Hhinv: high_level_invariant adt)
      (Hsig: sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default)
      (Hargs: extcall_arguments rs m´0 sig (Vint bound ::Vint i ::Vint ofs :: nil)):
      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_spec_low_step s rs (m´0, adt) (rs´#RA <- Vundef #PC <- (rs#RA)) (m0, adt´).

  Inductive release_lock_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
  | release_lock_spec_low_intro
      s m´0 b b0 l id adt adt´ rs i ofs sig size
      (Hsymbol_PC: find_symbol s release_lock = Some b)
      (HPC: rs PC = Vptr b Int.zero)
      (Hspec: release_lock_spec0 (Int.unsigned i) (Int.unsigned ofs) l adt = Some adt´)
      (Hsize: id2size (Int.unsigned i) = 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)
      (Hhinv: high_level_invariant adt)
      (Hsig: sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default)
      (Hargs: extcall_arguments rs m´0 sig (Vint i ::Vint ofs :: nil)):
      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_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 acquire_lock_spec_low: compatsem LDATAOps :=
      asmsem_withsig acquire_lock acquire_lock_spec_low_step
                     (mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default).

    Definition release_lock_spec_low: compatsem LDATAOps :=
      asmsem_withsig release_lock release_lock_spec_low_step
                     (mksignature (AST.Tint::AST.Tint::nil) None cc_default).

  End WITHMEM.

End TICKETLOCK_DEFINE.