[cjen1-msft]

Stacked on #8728.

The consensus replayer rejects every trace captured from a real CCF node at its second record; this lets it check them. A real node runs genesis asynchronously after force_become_primary, so it traces ticks between become_leader and the genesis replicate. Its genesis entry carries the constitution and exceeds append_entries_size_limit, so replicate() also traces a batch_flush. cft_driver writes a small genesis entry immediately, so driver captures never showed either.

Bootstrap now accepts only those bare ticks, unobserved because the model starts after genesis, and one optional flush that must send nothing.

Why skipping pre-genesis ticks is sound

Before genesis the leader has no peers or configurations (the traced become_leader lists none), so a tick sends nothing and its check-quorum passes trivially; the next observation still checks the state the ticks leave. replicate() holds the consensus lock across the genesis batch, from its replicate event through add_configuration and batch_flush, so no other event on that node falls between them. A send after the flush is rejected as an ungrouped event, since no rule claims it.

[Copilot]

🟢 Approval recommended

No active review issues block approval of the bootstrap trace replay changes.

No open issues 🎉

What changed in this PR

Updates the Lean consensus replayer to accept real CCF node bootstrap traces, extending replay support beyond the driver's immediate, small genesis entry.

Changes:

• Accepts bare ticks before genesis and one optional genesis flush, while rejecting sends from that flush.
• Adds valid and invalid fixtures covering the bootstrap sequence.
• Documents the expanded bootstrap contract and fixture expectations.

Custom instructions used

Applied the CCF repository guidance supplied in the review context. No additional instruction files were loaded.

File	Description
lean/​consensus/​replay/​README.md	Documents accepted pre-genesis ticks and genesis flushing.
lean/​consensus/​replay/​fixtures/​valid/​bootstrap.ndjson	Adds a valid real-node-style bootstrap trace.
lean/​consensus/​replay/​fixtures/​README.md	Describes the new bootstrap fixtures.
lean/​consensus/​replay/​fixtures/​invalid/​bootstrap-flush-send.ndjson	Covers rejection of sends during the genesis flush.
lean/​consensus/​replay/​fixtures/​invalid/​bootstrap-event.ndjson	Covers rejection of non-tick events before genesis.
lean/​consensus/​Consensus/​Replay/​Reduction.lean	Allows pre-genesis ticks and an optional bootstrap flush.

_{Review effort: Balanced}

[Copilot]

🟢 Approval recommended

No active review issues were identified for the bootstrap trace handling changes.

No open issues 🎉

_{Review effort: Balanced}

[Copilot]

🟢 Approval recommended

No active review issues were identified for the bootstrap replay changes.

No open issues 🎉

_{Review effort: Balanced}