Midgard State Machine

The Midgard machine is the composition of the different submodules. It also describes the complex interaction between these modules. Some modules are independent and on those we use regular parallel composition. The modules that have synchronous actions, we use the tensor product and the conditional sub-inteface operator.

inductive Midgard.StateMachine.MidgardError : Type

• SchErr : Scheduler.StateMachine.Err → MidgardError
• OpsErr : OperatorDirectory.StateMachine.Err → MidgardError
• SQErr : StateQueue.Machine.Err → MidgardError
• StQAndOps : MidgardError
• StQAndSett : MidgardError
• StQOnly : MidgardError
• OpOnly : MidgardError
• OpsSetts : MidgardError

instance Midgard.StateMachine.instReprMidgardError : Repr MidgardError

Equations

• Midgard.StateMachine.instReprMidgardError = { reprPrec := Midgard.StateMachine.instReprMidgardError.repr }

def Midgard.StateMachine.instReprMidgardError.repr : MidgardError → ℕ → Std.Format

Equations

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

def Midgard.StateMachine.stops_next : MidgardParameters × InputInfo → (Scheduler.State.SchedulerDatum × FraudProofTokens.State.FraudProofTokens) × Unit → StateQueue.State.StateQueue × OperatorDirectory.State.OperatorDirectory → State.StQAndOp → ComputationResult MidgardError (StateQueue.State.StateQueue × OperatorDirectory.State.OperatorDirectory)

Synchronous interaction between the State Queue and Operator Directory modules.

Equations

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

def Midgard.StateMachine.stq_settlement (p : MidgardParameters × InputInfo × Scheduler.State.SchedulerDatum) (e : FraudProofTokens.State.FraudProofTokens × Unit) (s : StateQueue.State.StateQueue × Settlement.State.SettlementSt) (a : State.StQAndSettlement) : ComputationResult MidgardError (StateQueue.State.StateQueue × Settlement.State.SettlementSt)

Synchronous interaction between the State Queue and Settlements modules.

Equations

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

def Midgard.StateMachine.stqonly_next : MidgardParameters × InputInfo → Scheduler.State.SchedulerDatum × FraudProofTokens.State.FraudProofTokens → StateQueue.State.StateQueue → State.StQOnly → ComputationResult (Option StateQueue.Machine.Err) StateQueue.State.StateQueue

Restriction to independent operations of the State Queue module.

Equations

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

def Midgard.StateMachine.SettlementInteraction.opssett (p : MidgardParameters × InputInfo) (e : Unit × Scheduler.State.SchedulerDatum) (s : OperatorDirectory.State.OperatorDirectory × Settlement.State.SettlementSt) (a : State.OpsDirAndSettlement) : ComputationResult MidgardError (OperatorDirectory.State.OperatorDirectory × Settlement.State.SettlementSt)

Synchronous interaction between the Operator directory and Settlements modules.

Equations

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

def Midgard.StateMachine.OperatorDirOnly.onlyops (p : MidgardParameters) (i : OperatorDirectory.State.ODirActs) (s : OperatorDirectory.State.OperatorDirectory) : ComputationResult (Option OperatorDirectory.StateMachine.Err) OperatorDirectory.State.OperatorDirectory

Independent actions by the Operator directory modules.

Equations

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

def Midgard.StateMachine.midgard_next (i : InputInfo) (p : MidgardParameters) (s : State.SimpleMState) (a : State.Actions) : ComputationResult MidgardError State.SimpleMState

Composition of each modules to define the big Midgard Machine.

Equations

• One or more equations did not get rendered due to their size.
• Midgard.StateMachine.midgard_next i p s (Midgard.State.Actions.FraudProof fp_act) = sorry

def Midgard.StateMachine.runMidgard (p : MidgardParameters) (st : State.SimpleMState) (as : List (State.Actions × InputInfo)) : ComputationResult MidgardError State.SimpleMState

Equations

• Midgard.StateMachine.runMidgard p st [] = pure st
• Midgard.StateMachine.runMidgard p st (hd :: tl) = do let x ← Midgard.StateMachine.midgard_next hd.2 p st hd.1 Midgard.StateMachine.runMidgard p x tl

instance Midgard.StateMachine.instMonadEvalComputationResultMidgardErrorIO : MonadEval (ComputationResult MidgardError) IO

Equations

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