Midgard State

Here we detail the complete Midgard state. The state itself is the composition of all other modules state. In a way, it is the Midgrad Hub Oracle, since each module of a concrete Midgard instance (from the poin of view of this library) communicate through their state.

structure Midgard.State.SimpleMState : Type

• scheduler : Scheduler.State.SchedulerDatum
• operators_dir : OperatorDirectory.State.OperatorDirectory
• user_event : Bridge.State.EventMap
• state_queue : StateQueue.State.StateQueue
• fraud_proof : FraudProofTokens.State.FraudProofTokens
• settlements : Settlement.State.SettlementSt
• da : DataLayer.DA
• utxo_outref : UtxoSet
• block_header : SimpleHeader

def Midgard.State.InitialState : SimpleMState

Equations

• One or more equations did not get rendered due to their size.

def Midgard.State.SimpleMState.time_interval (s : SimpleMState) : TimeInterval

Equations

• s.time_interval = { lower := some s.block_header.start_time, upper := some s.block_header.end_time }

Actions

There is a dispatch choosing (and building) the correct type for each action triggering sub-state machines. Synchronous actions at different machines are put together as one step (at this level), and independent actions are group together.

inductive Midgard.State.StQOnly : Type

• MergeToConfimedEmptyL1 (header root : Tokens.Elem.TId) : StQOnly

inductive Midgard.State.StQAndOp : Type

• CommitAndUpdate (opId : OperatorId) (hashHeader : StateQueue.State.HashHeader) (last toUpd : Tokens.Elem.TId) : StQAndOp
• FraudulentActiveAndRemBad (fpId : Tokens.Elem.TId) (opId : OperatorId) (blkRem anch actTkn : Tokens.Elem.TId) : Tokens.Elem.TId → StQAndOp
• FraudulentRetAndRemBad (fpId : Tokens.Elem.TId) (opId : OperatorId) (blkRem anch retTkn : Tokens.Elem.TId) : Tokens.Elem.TId → StQAndOp

inductive Midgard.State.StQAndSettlement : Type

• MergeAndSpawn (header root : Tokens.Elem.TId) : StQAndSettlement

@[reducible, inline]

abbrev Midgard.State.SumStQInt : Type

Equations

• Midgard.State.SumStQInt = (Midgard.State.StQAndSettlement ⊕ Midgard.State.StQAndOp ⊕ Midgard.State.StQOnly)

inductive Midgard.State.OpsDirAndSettlement : Type

• UpdBondHoldAndResolvClaim (act_tid sett_tid : Tokens.Elem.TId) (res_time : PosixTime) (opkey : VKeyHash) : OpsDirAndSettlement
• SlashAndDisprove : OpsDirAndSettlement

def Midgard.State.OpDirOnly (a : OperatorDirectory.State.OperActions) : Option OperatorDirectory.State.OperActions

Listing of operations that the opdir module can do alone

Equations

• Midgard.State.OpDirOnly (OperatorDirectory.State.OperActions.UpdateBondHold a_2) = none
• Midgard.State.OpDirOnly (OperatorDirectory.State.OperActions.ActRemoveOperatorBad a_2 a_3) = none
• Midgard.State.OpDirOnly (OperatorDirectory.State.OperActions.RetRemoveOperatorBad a_2 a_3) = none
• Midgard.State.OpDirOnly a = some a

inductive Midgard.State.Actions : Type

• StateQueueAndOps : StQAndOp → Actions
• StateQueueSettlement : StQAndSettlement → Actions
• OpDirAndSett : OpsDirAndSettlement → Actions
• SchedulerAct : Scheduler.State.Sch_Actions → Actions
• OperatorsAct : OperatorDirectory.State.OperActions → Actions
• StateAct : StQOnly → Actions
• FraudProof : FraudProofTokens.Computation.Actions → Actions

def Midgard.State.InjectOps (st : StateQueue.State.StateQueue × OperatorDirectory.State.OperatorDirectory) (a : StQAndOp) : Option (StateQueue.State.Actions × OperatorDirectory.State.OperActions)

Equations

• One or more equations did not get rendered due to their size.

def Midgard.State.InjectStQandSett (st : StateQueue.State.StateQueue × Settlement.State.SettlementSt) (a : StQAndSettlement) : Option (StateQueue.State.Actions × Settlement.State.Actions)

Equations

• One or more equations did not get rendered due to their size.

def Midgard.State.InjectStQOnly (st : StateQueue.State.StateQueue) (a : StQOnly) : Option StateQueue.State.Actions

Equations

• One or more equations did not get rendered due to their size.

def Midgard.State.InjectOpsSetts (st : OperatorDirectory.State.OperatorDirectory × Settlement.State.SettlementSt) (a : OpsDirAndSettlement) : Option (OperatorDirectory.State.OperActions × Settlement.State.Actions)

Equations

• One or more equations did not get rendered due to their size.
• Midgard.State.InjectOpsSetts st Midgard.State.OpsDirAndSettlement.SlashAndDisprove = sorry