Midgrad Relation

The Midgard relation is defined as the composition of different relations. Each relation describe the interaction between different modules.

Midgard Inductive Definition

def Midgard.Ins : Type

Equations

• Midgard.Ins = (Scheduler.State.SchedulerDatum × FraudProofTokens.State.FraudProofTokens × InputInfo)

def Midgard.StateQueueOperatorsJ : MidgardParameters × InputInfo → (Scheduler.State.SchedulerDatum × FraudProofTokens.State.FraudProofTokens) × Unit → StateQueue.State.StateQueue × OperatorDirectory.State.OperatorDirectory → State.StQAndOp → StateQueue.State.StateQueue × OperatorDirectory.State.OperatorDirectory → Prop

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.StateQueueOnlySub : MidgardParameters × InputInfo → Scheduler.State.SchedulerDatum × FraudProofTokens.State.FraudProofTokens → StateQueue.State.StateQueue → State.StQOnly → StateQueue.State.StateQueue → Prop

Independent interaction of the State Queue module. .

Equations

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

def Midgard.StateQAndSettlement : MidgardParameters × InputInfo × Scheduler.State.SchedulerDatum → FraudProofTokens.State.FraudProofTokens × Unit → StateQueue.State.StateQueue × Settlement.State.SettlementSt → State.StQAndSettlement → StateQueue.State.StateQueue × Settlement.State.SettlementSt → Prop

Synchronous interaction between the State Queue and Settlement modules.

Equations

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

inductive Midgard.Relation (p : MidgardParameters) (i : InputInfo) (e : State.SimpleMState) : State.Actions → State.SimpleMState → Prop

Here we list the parallel combination of different relations.

• StateQueueOperator {p : MidgardParameters} {i : InputInfo} {e : State.SimpleMState} {a : State.StQAndOp} {ops' : OperatorDirectory.State.OperatorDirectory} {st' : StateQueue.State.StateQueue} (step : StateQueueOperatorsJ (p, i) ((e.scheduler, e.fraud_proof), ()) (e.state_queue, e.operators_dir) a (st', ops')) : Relation p i e (State.Actions.StateQueueAndOps a) { scheduler := e.scheduler, operators_dir := ops', user_event := e.user_event, state_queue := st', fraud_proof := e.fraud_proof, settlements := e.settlements, da := e.da, utxo_outref := e.utxo_outref, block_header := e.block_header }
• StateQueueSettlement {p : MidgardParameters} {i : InputInfo} {e : State.SimpleMState} {a : State.StQAndSettlement} {st_q : StateQueue.State.StateQueue} {sett : Settlement.State.SettlementSt} (step : StateQAndSettlement (p, i, e.scheduler) (e.fraud_proof, ()) (e.state_queue, e.settlements) a (st_q, sett)) : Relation p i e (State.Actions.StateQueueSettlement a) { scheduler := e.scheduler, operators_dir := e.operators_dir, user_event := e.user_event, state_queue := st_q, fraud_proof := e.fraud_proof, settlements := sett, da := e.da, utxo_outref := e.utxo_outref, block_header := e.block_header }
• OperatorsStep {p : MidgardParameters} {i : InputInfo} {e : State.SimpleMState} (new_ops : OperatorDirectory.State.OperatorDirectory) (a : OperatorDirectory.State.OperActions) : OperatorDirectory.Relation p { act := a, info := i } e.operators_dir new_ops → Relation p i e (State.Actions.OperatorsAct a) { scheduler := e.scheduler, operators_dir := new_ops, user_event := e.user_event, state_queue := e.state_queue, fraud_proof := e.fraud_proof, settlements := e.settlements, da := e.da, utxo_outref := e.utxo_outref, block_header := e.block_header }
• SchedulerStep {p : MidgardParameters} {i : InputInfo} {e : State.SimpleMState} (new_sch : Scheduler.State.SchedulerDatum) (a : Scheduler.State.Sch_Actions) : Scheduler.Relation p e.operators_dir { act := a, info := i } e.scheduler new_sch → Relation p i e (State.Actions.SchedulerAct a) { scheduler := new_sch, operators_dir := e.operators_dir, user_event := e.user_event, state_queue := e.state_queue, fraud_proof := e.fraud_proof, settlements := e.settlements, da := e.da, utxo_outref := e.utxo_outref, block_header := e.block_header }
• StateQueueStep {p : MidgardParameters} {i : InputInfo} {e : State.SimpleMState} {st' : StateQueue.State.StateQueue} {a : State.StQOnly} (step : StateQueueOnlySub (p, i) (e.scheduler, e.fraud_proof) e.state_queue a st') : Relation p i e (State.Actions.StateAct a) { scheduler := e.scheduler, operators_dir := e.operators_dir, user_event := e.user_event, state_queue := st', fraud_proof := e.fraud_proof, settlements := e.settlements, da := e.da, utxo_outref := e.utxo_outref, block_header := e.block_header }
• FraudProofStep {p : MidgardParameters} {i : InputInfo} {e : State.SimpleMState} {x✝ : ComputationThreads.Datum.StepDatum ProofProtocol.Catalogue.Script → FraudProofTokens.State.FraudProofTokens → DataLayer.DA} (fproof : ComputationThreads.Datum.StepDatum ProofProtocol.Catalogue.Script) (s' : FraudProofTokens.State.FraudProofTokens) : FraudProofTokens.Computation.Prod e.fraud_proof e.state_queue (x✝ fproof s') fproof s' → Relation p i e (State.Actions.FraudProof (FraudProofTokens.Computation.Actions.Mint fproof)) { scheduler := e.scheduler, operators_dir := e.operators_dir, user_event := e.user_event, state_queue := e.state_queue, fraud_proof := s', settlements := e.settlements, da := e.da, utxo_outref := e.utxo_outref, block_header := e.block_header }

Step Machine Definition

def Midgard.StepMachine.MidgardSteps : StepMachines.StepMachine MidgardParameters (State.Actions × InputInfo) State.SimpleMState

Equations

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