structure CordialMiners.Sim.SimInput : Type

A simulation scenario: the committee snapshot, the parent-dependency graph on block hashes, the candidate blocks, and, per block, the list of approval events (the approving members in arrival order).

• snapshot : CommitteeSnapshot ℕ
• deps : ℕ → Finset ℕ
• candidates : List ℕ
• approvals : ℕ → List ℕ

def CordialMiners.Sim.finalizes (inp : SimInput) (block : ℕ) : Bool

A block is finalized when folding its approvals through the weighted collector closes the certificate (the threshold is crossed).

Equations

• CordialMiners.Sim.finalizes inp block = (List.foldl (CordialMiners.collectorStep inp.snapshot fun (x : ℕ) => true) CordialMiners.WCertState.init (inp.approvals block)).done

def CordialMiners.Sim.simulate (inp : SimInput) : List ℕ

The integrated pipeline: keep the finalized candidates, then order them with the verified topological sort. The output is the published ordered prefix of finalized block hashes.

Equations

• CordialMiners.Sim.simulate inp = CordialMiners.topoSort (List.filter (CordialMiners.Sim.finalizes inp) inp.candidates).toFinset inp.deps

def CordialMiners.Sim.demo : SimInput

A worked scenario: three equal-weight members, simple-majority finality, and four candidate blocks where 2 and 3 depend on 1 and 4 depends on 2 and 3. Blocks 1, 2, 3 each get two approvals (final); the leaf block 4 gets one (not final), so it is dropped.

Equations

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