def CordialMiners.blockDeps {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq Hash] (L : Blocklace P Wave Slot Hash) (h : Hash) : Finset Hash

The dependency graph a blocklace induces on hashes: the parent hashes of the block(s) carrying h. In a hash-unique blocklace this is just the parents of the one block with hash h.

Equations

• CordialMiners.blockDeps L h = {b ∈ L | b.blockHash = h}.biUnion CordialMiners.Block.parents

def CordialMiners.blockOrder {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [LinearOrder Hash] (L : Blocklace P Wave Slot Hash) : List Hash

The concrete blocklace ordering: topologically sort the present hashes by the parent graph, with canonical least-first tie-breaking. As a function of the blocklace it is an Ordering, realized by the verified topoSort.

Equations

• CordialMiners.blockOrder L = CordialMiners.topoSort (CordialMiners.hashesOf L) (CordialMiners.blockDeps L)

theorem CordialMiners.blockOrder_nodup {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [LinearOrder Hash] (L : Blocklace P Wave Slot Hash) : (blockOrder L).Nodup

The order has no duplicate positions.

theorem CordialMiners.blockOrder_subset {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [LinearOrder Hash] {L : Blocklace P Wave Slot Hash} {h : Hash} (hh : h ∈ blockOrder L) : h ∈ hashesOf L

Output-validity: every hash in the order is present in the blocklace.

theorem CordialMiners.blockOrder_topoSorted {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [LinearOrder Hash] (L : Blocklace P Wave Slot Hash) : TopoSorted (blockDeps L) (blockOrder L)

The order is topologically sorted for the parent graph: no parent hash is placed after the hash that depends on it.

theorem CordialMiners.blockOrder_deterministic {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [LinearOrder Hash] {L₁ L₂ : Blocklace P Wave Slot Hash} (h : L₁ = L₂) : blockOrder L₁ = blockOrder L₂

Determinism: equal blocklaces give equal orders (the ordering is a pure function).

theorem CordialMiners.blockOrder_complete {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [LinearOrder Hash] {L : Blocklace P Wave Slot Hash} {rank : Hash → ℕ} (hrank : ∀ (h p : Hash), p ∈ blockDeps L h → rank p < rank h) {h : Hash} (hh : h ∈ hashesOf L) : h ∈ blockOrder L

Completeness: under a strict rank on the parent graph (a parent ranks below its child, e.g. by round), every present hash appears in the order. With blockOrder_subset and blockOrder_nodup, the order lists exactly the present hashes, once each.

theorem CordialMiners.parentEdge_mem_blockDeps {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [LinearOrder Hash] [DecidableEq P] [DecidableEq Wave] [DecidableEq Slot] {L : Blocklace P Wave Slot Hash} {child parent : Block P Wave Slot Hash} (h : ParentEdge L child parent) : parent.blockHash ∈ blockDeps L child.blockHash

A real parent edge becomes a dependency in the induced graph: if child points to parent, then parent's hash is a dependency of child's hash.

theorem CordialMiners.blockOrder_parentEdge_not_after {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [LinearOrder Hash] [DecidableEq P] [DecidableEq Wave] [DecidableEq Slot] {L : Blocklace P Wave Slot Hash} {child parent : Block P Wave Slot Hash} (h : ParentEdge L child parent) {l₁ l₂ : List Hash} (hsplit : blockOrder L = l₁ ++ child.blockHash :: l₂) : parent.blockHash ∉ l₂

Causal consistency for real parent edges: wherever a block's hash sits in the order, the hash of any block it points to as a parent is never after it. The published order respects the blocklace DAG.