State Queue Implementation

State queue is implemented as a heterogeneous key-unordered linked list. The root element keeps a summary of the history of the protocol, while the list itself keeps the upcoming block headers. If nobody challenges them, and the time window passes, the first block header commits and updates the summary (root node.)

def StateQueue.MergeToConfirmed (st_init : State.StateQueue) (st_q : MUList.State.ListST (State.ConfirmedState ⊕ State.HashHeader)) (header rootId : Tokens.Elem.TId) (mat_dur lower_bound : PosixTime) : Prop

Equations

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

def StateQueue.EmptyL1Data (header : Tokens.Elem.TId) (st : State.StateQueue) : Prop

Equations

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

def StateQueue.NonEmptyL1Data (header : Tokens.Elem.TId) (st : State.StateQueue) : Prop

Equations

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

inductive StateQueue.Relation (p : MidgardParameters) (sch : Scheduler.State.SchedulerDatum) (fraudproofs : FraudProofTokens.State.FraudProofTokens) (i : InputInfo) (s : State.StateQueue) : State.Actions → State.StateQueue → Prop

• CommitBlockHeader {p : MidgardParameters} {sch : Scheduler.State.SchedulerDatum} {fraudproofs : FraudProofTokens.State.FraudProofTokens} {i : InputInfo} {s : State.StateQueue} (opId : OperatorId) (header : State.HashHeader) (res_ist : MUList.State.ListST (State.ConfirmedState ⊕ State.HashHeader)) (up_bound prev_end_time : PosixTime) (lastTkn : Tokens.Elem.TId) : i.validator = opId → MUList.Relation.Rel s (MUList.State.Actions.UnsafeAppend (State.hash_header header) (Sum.inr header) lastTkn) res_ist → header.header.operator_vkey = opId → sch.operator_id = opId → sch.shift_start ≤ header.header.end_time → header.header.end_time < sch.shift_start + p.shift_duration → i.validityInternal.upper = some up_bound → header.header.end_time = up_bound → MUList.State.ListST.get_data lastTkn (Sum.elim (fun (x : State.ConfirmedState) => x.end_time) fun (x : State.HashHeader) => x.header.end_time) s = some prev_end_time → header.header.start_time = prev_end_time → Relation p sch fraudproofs i s (State.Actions.CommitBlock opId header lastTkn) res_ist
• MergeToConfirmed {p : MidgardParameters} {sch : Scheduler.State.SchedulerDatum} {fraudproofs : FraudProofTokens.State.FraudProofTokens} {i : InputInfo} {s : State.StateQueue} (st_q : MUList.State.ListST (State.ConfirmedState ⊕ State.HashHeader)) (lower_bound : PosixTime) (rootid header : Tokens.Elem.TId) : StateQueue.MergeToConfirmed s st_q header rootid p.maturity_duration lower_bound → i.validityInternal.lower = some lower_bound → Relation p sch fraudproofs i s (State.Actions.MergeToConfirmed header rootid) st_q
• RemoveFraudulentBlock {p : MidgardParameters} {sch : Scheduler.State.SchedulerDatum} {fraudproofs : FraudProofTokens.State.FraudProofTokens} {i : InputInfo} {s : State.StateQueue} (header_tkn : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key (State.ConfirmedState ⊕ State.HashHeader))) (hd_tkn anch_tkn : Tokens.Elem.TId) (fopId : OperatorId) (fproof : Tokens.Elem.TId) (st_queue' : MUList.State.ListST (State.ConfirmedState ⊕ State.HashHeader)) : MUList.Relation.Rel s (MUList.State.Actions.Remove hd_tkn anch_tkn) st_queue' → Tokens.State.Tokens.get hd_tkn s = some header_tkn → Sum.map (fun (x : State.ConfirmedState) => ()) (fun (x : State.HashHeader) => x.header.operator_vkey) header_tkn.data.data = Sum.inr fopId → FraudProofTokens.Operations.get_block_id fproof fraudproofs = some anch_tkn ∨ FraudProofTokens.Operations.get_block_id fproof fraudproofs = some hd_tkn ∧ MUList.State.midgard_is_last_node header_tkn = true → Relation p sch fraudproofs i s (State.Actions.RemoveFraudulentBlock fproof fopId hd_tkn anch_tkn) st_queue'

def StateQueue.StateQueueStep : StepMachines.StepMachine (MidgardParameters × Scheduler.State.SchedulerDatum × FraudProofTokens.State.FraudProofTokens) (InputInfo × State.Actions) State.StateQueue

Equations

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

def StateQueue.Notation.«term_=>STQ⟨_,_,_,_;_⟩_» : Lean.TrailingParserDescr

Equations

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