8.4. Chain Selection (GP §19)🔗

Chain selection determines which fork to follow. The protocol uses a scoring metric based on how many blocks were sealed via the ticket mechanism (vs fallback). Blocks must pass acceptability checks before being considered.

def

Jar.Consensus.ChainAncestry : Type
Jar.Consensus.ChainAncestry : Type

Chain ancestry data: maps header hash → (parent hash, timeslot). Represents the set of known headers for ancestry traversal.

opaque

Jar.Consensus.ancestors (chain : ChainAncestry) (headerHash : Hash) :
  List Hash
Jar.Consensus.ancestors
  (chain : ChainAncestry)
  (headerHash : Hash) : List Hash

A(H) : Ancestor set of a block. GP §19. Traces parent links back through known headers.

def

Jar.Consensus.chainMetric (chain : ChainAncestry) (headerHash : Hash)
  (isTicketed : Hash → Bool) : Nat
Jar.Consensus.chainMetric
  (chain : ChainAncestry)
  (headerHash : Hash)
  (isTicketed : Hash → Bool) : Nat

Best chain metric: count of ticketed (non-fallback) seals among ancestors. GP §19. m = Σ_{H^A ∈ A♭} T^A. Select B♭ to maximize this value.

def

Jar.Consensus.isAcceptable (chain : ChainAncestry)
  (headerHash finalizedHash : Hash) (isAudited : Bool) : Bool
Jar.Consensus.isAcceptable
  (chain : ChainAncestry)
  (headerHash finalizedHash : Hash)
  (isAudited : Bool) : Bool

Check if a block is acceptable for best chain consideration. GP §19. A block must:

Be a descendant of the finalized block: A(H♭) ∋ H♮
Have all reports audited: U♭ ≡ ⊤
Not contain equivocating headers in unfinalized range: ¬∃ H^A ≠ H^B : H^A_T = H^B_T ∧ H^A ∈ A(H♭) ∧ H^A ∉ A(H♮)