Documentation

FMMidgard.StateQueue.Properties

State Queue Properties #

The State Queue keeps a linked list. In this case, the key component of tokens are hashes of the data containing those nodes. This provides a strong guarantee that such keys are unique.

No collision analysis is made here. If keys are unique, then the data-structure defined in the spec is a list and no breaking is possible. These properties are verified/tested using Plausible (see Test/Lists.lean.)

source
axiom StateQueue.Props.unique_states_keys {s : State.StateQueue} {t1 t2 : Tokens.Elem.TId} {k : MUList.State.Key} (in1 : MUList.State.ListST.is_member k t1 s = true) (in2 : MUList.State.ListST.is_member k t2 s = true) :
t1 = t2

Unique keys. This property does not come from the state machine but from the fact that keys are hashes of data structures. The collition rate/probability is very low (negligible?) since one of the component of the structure is the hash of the previous node in the list.

There is only one Confirmed State token #

We split this invariant into two:

  1. Root nodes have commited history headers
  2. There is only one root node

We prove 1. here and 2. comes from the Midgard Lists properties.

source
def StateQueue.Props.OnlyOneCommitmentInv (s : State.StateQueue) :
Prop
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def StateQueue.Props.OnlyOneInvStep {p : MidgardParameters} {sch : Scheduler.State.SchedulerDatum} {fp : FraudProofTokens.State.FraudProofTokens} {i : InputInfo} {s s' : State.StateQueue} {a : State.Actions} (step : Relation p sch fp i s a s') (pre : OnlyOneCommitmentInv s) :
    OnlyOneCommitmentInv s'
    Equations
    • ⋯ = ⋯
    Instances For
      source
      def StateQueue.Props.inductionOnlyOne {p : MidgardParameters × Scheduler.State.SchedulerDatum × FraudProofTokens.State.FraudProofTokens} :
      StepMachines.InductionStepMachine p StateQueueStep OnlyOneCommitmentInv
      Equations
      • ⋯ = ⋯
      Instances For
        source
        theorem StateQueue.Props.only_one_confirmed_state {p : MidgardParameters} {sch : Scheduler.State.SchedulerDatum} {fp : FraudProofTokens.State.FraudProofTokens} {s : State.StateQueue} (reachable : StateQueueStep.FromInit (p, sch, fp) s) :
        OnlyOneCommitmentInv s
        source
        theorem StateQueue.Props.block_merging_order {p : MidgardParameters} {sch : Scheduler.State.SchedulerDatum} {fp : FraudProofTokens.State.FraudProofTokens} {i : InputInfo} {s s' : State.StateQueue} {header_tid root_tid : Tokens.Elem.TId} (reachable : StateQueueStep.FromInit (p, sch, fp) s) (step : Relation p sch fp i s (State.Actions.MergeToConfirmed header_tid root_tid) s') :
        MUList.State.ListST.is_root_node root_tid s = true ∧ ∃ (key : MUList.State.Key), MUList.State.ListST.get_key header_tid s = some key ∧ MUList.State.ListST.is_anchor key root_tid s = true

        If it is merged, then it is the first block.