Investigate nil-precommit timeout certificates for Tenderlink fork recovery

[zmanian]

Summary

Tenderlink currently treats 2f+1 nil precommits as evidence that the current round did not decide, but not as evidence that validators should stop carrying the round's prior PoW finalization candidate.

This is normal Tendermint-style behavior, but Crosslink has an extra liveness pressure: the value being finalized is a PoW checkpoint sampled from the node's current best chain. During fork recovery, the PoW best chain may move forward or switch forks while BFT is stuck around an older candidate.

The design question is whether a 2f+1 PRECOMMIT nil certificate for (height, round) should explicitly cancel the liveness momentum created by that same round's prevotes, allowing a later round to sample a fresher tip - sigma checkpoint from the PoW chain.

Current behavior

At a Tenderlink BFT height, each round runs:

Propose -> Prevote -> Precommit

Current code behavior at the pinned Tenderlink rev:

• 2f+1 yes prevotes set locked_value_round and valid_value_round, then precommit that value.
• 2f+1 nil prevotes cause a nil precommit.
• 2f+1 precommits of any kind only start the precommit timeout.
• Only 2f+1 yes precommits decide a value and advance the BFT height.
• locked_value_round and valid_value_round reset only after a value is decided.

Relevant local areas:

• zebra-crosslink/Cargo.toml pins the external tenderlink dependency.
• Tenderlink TMState::bft_update handles the Tendermint conditions for prevote, precommit, decision, catch-up, and timeouts.
• Zebra's proposer closure samples the current PoW tip and proposes tip - sigma only when Tenderlink does not already have a carried valid_value_round.

Why this matters

During fork recovery, the PoW best chain may move forward or switch forks while the BFT round is between prevote and precommit.

The conservative behavior is:

1. If a value got 2f+1 prevotes, keep it sticky.
2. If it never got 2f+1 yes precommits, keep trying to complete or repropose it in later rounds.
3. After it decides, the next BFT height can jump forward to a fresher PoW checkpoint.

That preserves the familiar Tendermint safety argument, but it can make Crosslink finalization chase a stale checkpoint even after validators have effectively nil-precommitted the round.

A stronger nil-precommit rule may have better liveness: a 2f+1 PRECOMMIT nil certificate is evidence that this round is dead as a finalization attempt. If the protocol keeps carrying that round's valid_value_round or same-round lock momentum forward anyway, it can keep trying to finalize a PoW snapshot that the live network has already moved past.

Validator-set scaling intuition

The larger motivation is validator-set size.

For a globally distributed validator set, the time to reach GST-like effective synchrony grows with communication delay across the validator set, and the worst-case message pattern can be quadratic. As the validator set grows, the prevote-to-precommit window is more likely to overlap with a PoW stream change: a new longest chain appears, or the current tip - sigma candidate advances.

In the current protocol shape, that stream change can turn into a halt. Validators may have enough prevotes to carry a stale candidate, but not enough matching precommits to decide it. The later rounds then keep trying to recover around stale BFT state rather than simply sampling the current PoW stream.

With nil-precommit resampling, a stream change does not have to halt the BFT height. It can just cause the round number to increment until the network and the PoW stream are stable enough for one candidate to survive through prevote and precommit.

This matches the current Crosslink implementation model: proposals are sampled as head - sigma. The PoW stream continues progressing uninterrupted between BFT rounds, and the BFT layer should be able to re-enter that stream after an abandoned round instead of staying pinned to an obsolete sample.

Ebb-and-Flow composition

This rule is best understood as a liveness bridge between the two Crosslink pieces:

• The PoW side is the flow layer. It keeps producing availability and may reveal a fresher tip - sigma candidate after a partition heals or a longer fork appears.
• The BFT side is the ebb/finality layer. It decides which PoW snapshot becomes finalized and must preserve monotonic finality.
• A nil-precommit certificate says the BFT layer failed to finalize this round, so the next round should be allowed to resample from the current PoW flow.

So the intended behavior is not "flow overrides finality". It is "failed ebb attempts should not force future ebb attempts to keep using stale flow input".

The safety boundary is important:

• A nil-precommit certificate should cancel same-round prevote momentum.
• It should allow later proposals to ignore the abandoned round's stale valid_value_round.
• It may be safe to unlock validators whose lock was created by that same round, because a same-round 2f+1 PRECOMMIT nil certificate should rule out a same-round value commit certificate unless validators equivocate.
• It should not automatically cancel locks from older rounds. Older locks still need the usual Tendermint-compatible unlock proof.

Proposed rule shape

Introduce a formal nil-precommit certificate:

• A 2f+1 PRECOMMIT nil certificate for (height, round) is recorded as an abandon certificate for that round.
• Later proposals may carry this certificate.
• Validators that verify the certificate may clear round-local carried state derived from that same round.
• At minimum, this should clear the corresponding stale valid_value_round so proposers can sample the latest PoW tip - sigma.
• Optionally, the rule may also unlock validators whose locked_value_round was created in the same round as the nil-precommit certificate.
• The rule must not unlock validators locked in an earlier round unless the proposal carries an independently valid Tendermint-compatible unlock proof.

One crisp formulation:

For a fixed BFT height and round r, 2f+1 PRECOMMIT nil cancels the finalization attempt for round r. It can cancel state created by round r, but it cannot cancel safety locks from rounds < r.

Safety obligations

This should not be implemented as local cleanup without a protocol rule.

The analysis should prove or reject at least the following:

• For fixed (height, round), 2f+1 PRECOMMIT nil and 2f+1 PRECOMMIT value cannot both exist unless more than f voting power equivocates or an honest validator violates the protocol.
• A same-round nil-precommit certificate is sufficient evidence that a value locked due to that round's prevotes cannot still be decided in that round.
• Unlocking only same-round locks does not allow conflicting commits across later rounds.
• Validators that do not immediately see the nil-precommit certificate remain safe, and later converge when a proposal carries the certificate.
• Clearing valid_value_round without clearing locked_value_round is safe but may leave liveness on the table; clearing same-round locks may improve liveness further and needs the stronger proof.
• Proposal validation must define exactly which certificates can be carried and when they are accepted.

Acceptance criteria

• Document the intended behavior for 2f+1 nil precommits in Crosslink/Tenderlink.
• Decide whether nil precommit should:
  • only advance the round, as in the current Tendermint-like behavior;
  • clear valid_value_round but not unlock;
  • unlock only same-round locks via a formal nil-precommit certificate;
  • unlock older locks only with a separate Tendermint-compatible proof; or
  • be left unchanged until Crosslink proposal-validity rules are fully implemented.
• If a new rule is chosen, specify the certificate format, verification rules, and required updates to proposal validation.
• Add targeted tests covering:
  • stale PoW checkpoint carried across rounds after yes prevotes;
  • nil-precommit quorum with no decision;
  • fork recovery where the best PoW chain changes between prevote and precommit;
  • same-round nil-precommit certificate clearing stale proposal state;
  • safety against conflicting commits across rounds.

Recommendation

Treat this as a protocol-design improvement, not a local bug fix.

My current bias is:

1. Model 2f+1 PRECOMMIT nil as a first-class round-abandon certificate.
2. Use it to clear stale valid_value_round so Crosslink can resample from the current PoW flow after a failed finality attempt.
3. Investigate same-round unlock as the liveness-improving version of the rule.
4. Preserve older locks unless the protocol has a clear Tendermint-compatible unlock proof.

This version appears to compose well with Ebb-and-Flow: PoW availability keeps moving, BFT finality remains monotonic, and a failed BFT round does not keep dragging stale PoW input into future rounds.

[zmanian]

I think one implication of this change is that Tenderlink would have strong liveness with a much larger validator set

[zmanian]

Posted the current Quint spec bundle here:

https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf

Contents:

• CrosslinkResampling.qnt: nil-precommit timeout certificate behavior, lock preservation, and stream resampling.
• CrosslinkForkFinality.qnt: fork-prefix finality behavior and explicit no-skipped-height finality checks.
• CrosslinkComposed.qnt: composed resample -> decide -> finalize flow.
• README.md: proof scope and the commands used for typecheck, Rust backend tests/simulations, and bounded Apalache checks.

This is the working model bundle for exploring whether 2f+1 nil precommits can safely unlock/resample without losing Tendermint lock safety.

[zmanian]

One accountability note from the Quint/spec pass:

This proposal changes the Tendermint accountability surface, but it does not need to weaken it.

The useful framing is that 2f+1 nil precommits become first-class lock-transition evidence. They can justify moving to the next round with a resampled Crosslink stream/head, but they must not erase or invalidate historical vote evidence.

Suggested accountability constraints:

1. A nil precommit is only valid under the round rule: the validator failed to observe 2f+1 prevotes for a single value, or observed Crosslink stream/head instability under the protocol-defined condition.
2. A 2f+1 nil-precommit certificate can justify resampling for the next round.
3. A nil-precommit certificate cannot invalidate an already completed value commit.
4. It cannot excuse equivocation: double-prevoting, double-precommitting, or signing conflicting commits at the same height/round/step remains accountable.
5. It should only unlock future voting behavior. It must not retroactively authorize conflicting votes in the same round.

So the spec should treat a nil-precommit certificate as an explicit higher-round unlock/resampling certificate. Validators may use it to leave the old sampled stream/head and vote on the next sampled candidate, but all prior signed prevotes/precommits remain available for fork-accountability analysis.

The property to preserve from Tendermint is: if two different values finalize at the same height, the evidence trail must still identify either equivocation or an invalid unlock transition. The proposed rule is a good fit only if the nil certificate composes with that invariant.

[zmanian]

Fork implementation branches are up on Zaki’s personal GitHub forks:

• Crosslink fork branch: https://github.com/zmanian/zebra/tree/quint-crosslink-spec
  • commit: 2b5f4c5312430d7af96084f9bc89aeb5cdc5bde6
  • pins Tenderlink to cbf1bc5b2109518711deaf6ac635d017bbfe6271
• Tenderlink fork branch: https://github.com/zmanian/tenderlink/tree/nil-precommit-resampling
  • commit: cbf1bc5b2109518711deaf6ac635d017bbfe6271

No upstream PR has been opened. These are fork-only branches for continuing review and iteration.

Current verification on the fork branches:

• cargo test -p zebra-crosslink
• cargo test nil_precommit --manifest-path forks/tenderlink/Cargo.toml
• cargo test stale_precommit_validation --manifest-path forks/tenderlink/Cargo.toml
• Quint typechecks for CrosslinkResampling.qnt, CrosslinkForkFinality.qnt, and CrosslinkComposed.qnt
• Quint Rust-backend witness tests: sticky 3, resampling 9, fork-finality 4, composed 1

[zmanian]

Updated the public Quint spec gist with the current full spec/quint bundle:

https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf

Current fork branch:

• https://github.com/zmanian/zebra/tree/quint-crosslink-spec
• latest commit: f1ef5b00292b7474ea4369903c9c5111a1c19b20

Notable additions since the earlier gist snapshot:

• Dynamic-sigma controller models, including hash-power participation as an explicit sigma floor.
• PoW fork-schedule and branch-competition models that derive rollback depth from best-tip/work transitions.
• Full dynamic-sigma + nil-precommit resampling + Crosslink finality composition.
• Production-shaped telemetry contract with rollback-risk and expected-loss targets.
• New dynamic-sigma telemetry integration note mapping the Quint inputs to production data sources and calling out the consensus-safety requirement for any deployed controller.
• spec/quint/check.sh for reproducible quick and bounded symbolic checks.

For the latest telemetry increment I re-ran:

• git diff --check / git diff --cached --check
• quint typecheck spec/quint/CrosslinkDynamicSigmaTelemetry.qnt
• quint test spec/quint/CrosslinkDynamicSigmaTelemetry.qnt --main=CrosslinkDynamicSigmaTelemetryModel --backend=rust

The telemetry witness suite is currently 10/10 passing. The branch has no upstream PR; this remains personal-fork work for review and iteration.

[zmanian]

Follow-up after the telemetry docs update: I added an executable Rust-side dynamic-sigma controller prototype on the personal fork.

Branch commit:

• zmanian@0c358ba44

What changed:

• Added zebra-crosslink/src/dynamic_sigma.rs, a pure controller that validates a supplied telemetry window and selects sigma from the same component floors as CrosslinkDynamicSigmaTelemetry.qnt.
• Hash participation is work-weighted and conservative: underreported coverage risk is rejected before a sigma decision is accepted.
• The controller also rejects underreported Tenderlink round-failure rates and non-monotone rollback-risk curves.
• The Rust tests mirror the nine-window Quint telemetry fixture, including marginal hash participation, critical participation, combined risk, deep reorg, expected-loss, and unreachable-target cases.
• Consensus behavior is intentionally unchanged; bc_confirmation_depth_sigma is still fixed in proposal/validation. The remaining production work is wiring consensus-safe telemetry producers and deciding whether economic exposure is shared protocol policy or service-local policy.

Validation for this increment:

• git diff --cached --check
• cargo test -p zebra-crosslink --lib -> 10/10 passing
• cargo clippy -p zebra-crosslink --lib completes, with existing warnings in older workspace code.

I also refreshed the public Quint gist after the README/integration-note edits:

https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf

[zmanian]

Small follow-up on the Rust dynamic-sigma controller work:

• Added raw telemetry counter conversion in zmanian@dbd28223a
• DynamicSigmaRawTelemetry::into_window now derives conservative coverage-risk and round-failure estimates from raw counters, with explicit safety margins and 100% saturation.
• The controller tests now cover 13 library tests total, including raw-counter construction feeding the same hash-participation sigma floor.
• Gist refreshed again at https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf

Still intentionally not wired into consensus proposal/validation; the remaining production gap is real telemetry/event sources plus deterministic or proposal-verifiable agreement on those inputs.

[zmanian]

Added the proposal-carried evidence verifier for the dynamic-sigma controller:

• Commit: zmanian@2c66c9216
• validate_dynamic_sigma_evidence reconstructs the conservative telemetry window from raw counters, runs the controller, and rejects selected sigma values outside the ladder or below the required floor.
• Tests now cover accepting exact required sigma, accepting a more conservative ladder sigma, deterministic validation for identical evidence, below-floor rejection, and outside-ladder rejection.
• cargo test -p zebra-crosslink --lib is now 18/18 passing.
• Gist refreshed again: https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf

This is still scaffolding for the proposal-carried controller-evidence path; it does not yet serialize evidence in BFT proposals or replace the fixed bc_confirmation_depth_sigma validation path.

[zmanian]

Added the selected-sigma BFT block construction hook:

• Commit: zmanian@cb22b45ab
• BftBlock::try_from(params, ...) still uses fixed bc_confirmation_depth_sigma.
• New BftBlock::try_from_with_confirmation_depth(selected_sigma, ...) validates the header count against a selected sigma.
• This gives the proposal-carried dynamic-sigma evidence path a concrete block-construction boundary without changing live proposal/validation behavior.
• cargo test -p zebra-crosslink --lib is now 21/21 passing; clippy still completes with the same existing older warnings.
• Gist refreshed: https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf

[zmanian]

Update: the dynamic-sigma branch now composes proposal-carried evidence validation with BFT block construction.

Branch commit: 34a33ee8f (Compose dynamic sigma evidence with block construction)

What changed:

• Added BftBlock::try_from_with_dynamic_sigma_evidence(...).
• The helper validates DynamicSigmaProposalEvidence against shared controller parameters first.
• If the selected sigma is valid and at least the controller-required floor, the selected sigma becomes the required PoW header depth for the BFT proposal.
• Added tests covering accepted selected sigma, below-floor selected sigma rejection, and the important more-conservative case where selected sigma is higher than the computed floor and therefore requires the larger header count.
• Updated the Quint README and telemetry integration note to distinguish this checked helper from the still-missing live consensus proposal serialization/validation wiring.

Validation:

• cargo test -p zebra-crosslink chain::tests --lib passed: 6/6.
• cargo test -p zebra-crosslink --lib passed: 24/24.
• cargo clippy -p zebra-crosslink --lib exits successfully, with the existing warning backlog still present.
• git diff --check and git diff --cached --check passed before commit.

Gist refreshed: https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf
Latest gist version: 29f32ab4f3df2e8e4520abbecf2a986d382a407b

[zmanian]

Update: added a small live-path seam for selected sigma.

Branch commit: 53dd7abc9 (Factor candidate height by selected sigma)

What changed:

• Introduced finality_candidate_height_at_depth(tip_height, confirmation_depth).
• Reused it in the existing fixed-sigma proposal creation path and voting-time stale-proposal check.
• This preserves current behavior because both callers still pass PROTOTYPE_PARAMETERS.bc_confirmation_depth_sigma, but removes the duplicated tip - sigma calculation and gives the dynamic-sigma path a checked helper for selected confirmation depth.
• The helper uses checked u64 -> i64 conversion before constructing HeightDiff, avoiding silent wrap for invalidly large selected sigma values.

Validation:

• Red/green tests added for selected-depth subtraction and underflow.
• cargo test -p zebra-crosslink finality_candidate_height_at_depth --lib passed: 2/2.
• cargo test -p zebra-crosslink --lib passed: 26/26.
• cargo clippy -p zebra-crosslink --lib exits successfully, with the existing warning backlog still present.
• git diff --check and git diff --cached --check passed before commit.

[zmanian]

Update: dynamic-sigma proposal evidence now has deterministic serialization.

Branch commit: 6951aaae2 (Serialize dynamic sigma evidence)

What changed:

• Implemented Zcash serialization/deserialization for DynamicSigmaProposalEvidence and its proposal-carried components: raw telemetry, estimate margins, and rollback-risk curve.
• The encoding is deterministic little-endian and intentionally covers evidence, not shared controller parameters.
• Added a round-trip test that exercises u128 telemetry values and checks the encoded length (123 bytes) so accidental shape changes are visible.
• Updated the telemetry integration note: the remaining wire-format question is no longer how to serialize evidence, but where to carry or commit those evidence bytes in the Malachite value/proposal encoding.

Validation:

• cargo test -p zebra-crosslink dynamic_sigma::tests::proposal_evidence_zcash_serialization_round_trips --lib passed: 1/1.
• cargo test -p zebra-crosslink --lib passed: 27/27.
• cargo clippy -p zebra-crosslink --lib exits successfully, with the existing warning backlog still present.
• git diff --check and git diff --cached --check passed before commit.

Gist refreshed: https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf
Latest gist version: f0fe422144d88acc29451f48bace388fe707c8b9

[zmanian]

Update: added a tagged dynamic-sigma BFT payload envelope.

Branch commit: eaf1e578e (Add dynamic sigma block payload envelope)

What changed:

• Added DynamicSigmaBftBlockPayload, carrying DynamicSigmaProposalEvidence plus the evidence-selected BftBlock.
• Added the CLDSIG01 magic prefix so dynamic-sigma payload bytes cannot be accidentally parsed as the legacy fixed-sigma BftBlock value.
• The constructor routes through BftBlock::try_from_with_dynamic_sigma_evidence(...), so payload construction still validates selected sigma before building the block.
• Added serialization/deserialization for the tagged envelope and tests for canonical byte round-trip plus wrong-magic rejection.
• Updated the telemetry integration note: evidence bytes and the dynamic payload envelope now exist; remaining live work is adopting the envelope in the Tenderlink propose/validate/decided callbacks.

Validation:

• cargo test -p zebra-crosslink dynamic_sigma_bft_block_payload --lib passed: 2/2.
• cargo test -p zebra-crosslink --lib passed: 29/29.
• cargo clippy -p zebra-crosslink --lib exits successfully, with the existing warning backlog still present.
• git diff --check and git diff --cached --check passed before commit.

Gist refreshed: https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf
Latest gist version: 73f687c15a4d2fbc635e620d34a630feb6169e1b

[zmanian]

Update on dynamic-sigma hash participation and payload validation:

• The dynamic-sigma controller already treats Crosslink-participating hash power as a first-class sigma factor: total_hash_work vs crosslink_participating_hash_work derives conservative coverage risk, with target and critical participation thresholds selecting the hash-participation floor.
• Latest branch commit: zmanian/zebra@08a2bfa88 (Validate dynamic sigma payload blocks).
• This adds DynamicSigmaBftBlockPayload::validate(...), which replays evidence validation and rejects payloads whose carried BftBlock does not match the evidence-selected block. This is one more guard before live Tenderlink callback wiring.
• Refreshed gist: https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf at aa06266168325f9c00367ca2c57bf464484f7b72.
• Fresh checks:
  • cargo test -p zebra-crosslink dynamic_sigma --lib: 23 passed
  • cargo test -p zebra-crosslink --lib: 31 passed
  • cargo clippy -p zebra-crosslink --lib: exit 0 with the existing warning backlog

Design implication: the production remaining work is not deciding whether participation is a factor; it is defining a consensus-safe or proposal-verifiable source for CrosslinkParticipatingHashWork and TotalHashWork, plus conservative hidden-work margins.

[zmanian]

Update on Tenderlink payload routing:

• Latest branch commit: zmanian/zebra@61d87f42c (Route Tenderlink BFT payload formats).
• Added BftBlockPayload, an explicit decoder that routes legacy fixed-sigma BftBlock bytes separately from tagged DynamicSigmaBftBlockPayload bytes.
• Updated the live Tenderlink validation and decided-block callbacks to use the decoder. The current fixed-sigma prototype still accepts legacy BftBlock bytes, while dynamic-sigma tagged payloads are recognized and rejected until shared dynamic-sigma parameters and proposal-verifiable telemetry are wired in.
• This avoids the unsafe middle state where dynamic payload bytes could be silently parsed through the fixed-sigma path.
• Refreshed gist: https://gist.github.com/zmanian/14d77cf1deda43a5b889bc22f8f0cfaf at 893747a3fd07dfcafdaf7401df3552d39f6d66ea.
• Fresh checks:
  • cargo test -p zebra-crosslink bft_block_payload --lib: 6 passed
  • cargo test -p zebra-crosslink fixed_sigma_tenderlink_payload_decoder --lib: 2 passed
  • cargo test -p zebra-crosslink --lib: 35 passed
  • cargo clippy -p zebra-crosslink --lib: exit 0 with the existing warning backlog
  • git diff --check / git diff --cached --check: clean

Remaining production work: replace the rejection branch with dynamic-sigma acceptance once the callback path has shared controller parameters, proposal evidence validation, and a consensus-safe or proposal-verifiable telemetry source for hash participation and total work.