Library mcertikos.objects.cpulocaldef.BigStepGlobalOracle

Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Memory.
Require Import AuxLemma.
Require Import Constant.
Require Import GlobIdent.
Require Export GlobalOracle.
Require Import Integers.



Inductive BigLockEvent :=
| BWAIT_LOCK (curid : Z) (n: nat)
| BGET_LOCK (curid: Z)
| BREL_LOCK (curid : Z) (s: SyncChanPool) .


Inductive BigSharedMemEvent :=
| BPALLOCE (curid: Z) (b: Z)
| BBUFFERE (curid cv_id: Z) (msg : PageBuffer)
| BTDSPAWN (curid: Z) (new_id: Z) (q: Z)
           (ofs: int)
           (buc: block) (ofs_uc: int)
| BTDYIELD (curid: Z)
| BTDSLEEP (slp_id cv_id: Z)
           (s: SyncChanPool)

| BTDWAKE (curid: Z) (cv_id: Z)
| BTDWAKE_DIFF (curid: Z) (cv_id wk_id cpu_id: Z)

.

Inductive BigOracleEventUnit :=
| TBLOCK (lock_id: Z) (e: BigLockEvent)

| TBSHARED (e: BigSharedMemEvent).

Inductive BigOracleEvent :=
| TBEVENT (i: Z) (e: BigOracleEventUnit).

Inductive BigOracleEventType :=
| EBLOCK

| EBSHARED.

Function GetBigOracleEventType (e: BigOracleEventUnit) :=
  match e with
    | TBLOCK _ _ ⇒ EBLOCK
    
    | TBSHARED _ ⇒ EBSHARED
  end.

Definition BigLog := list BigOracleEvent.
Definition BigOracle := Z → BigLog → BigLog.

Inductive BigLogType :=
| BigUndef
| BigDef (l: BigLog).

Class BigOracleOps :=
  {
    big_oracle0: BigOracle;
    
    big_oracle_env_fun: nat → Z → Z → BigOracle → BigLog → BigLog
  }.