Write consensus scenarios in Lean by achamayou · Pull Request #8773 · microsoft/CCF

Amaury Chamayou (achamayou) · 2026-11-13T17:00:09Z

Consensus scenarios were written in an ad-hoc comma-separated language, parsed by a switch in cft_driver.
They are now Lean programs which call the driver through bindings, so scenarios get a real language and the parser is gone.

initialize scenario "startup" do
  startNode 0
  assertDetail 0 "leadership_state" "Leader"
  replicate 2 [signature]
  assertCommitIdx 0 2

tests/cft_scenarios/CftDriver.lean declares one @[extern] per driver command, and driver.cpp is now only the matching extern "C" functions.
CMake has lake compile the scenarios to a static library, which defines main, and links it with the bindings and the Lean runtime.
The existing scenarios are translated mechanically, and their traces are unchanged, so the captures replayed against the Lean model are the same.

Points for review:

Building cft_driver now needs Lean. Without lake, CMake warns, does not build it, and disables cft_scenario_test.
A new install-lean action is added to the jobs which run the scenario test in ci.yml, ci-al4.yml, coverage.yml, long-test.yml and lean.yml. Only ci.yml and lean.yml are exercised by this PR's default checks.
Measured cost in ci.yml: about 10 s in VMSS Virtual C, of which Install Lean is 8 s. VMSS Virtual A remains the longest job, so the workflow does not take longer. See "CI time impact" below.
release.yml does not install Lean, so the release build no longer runs the scenario test.
Failures report Step N (command) rather than a line number, so driver.h loses its lineno parameters.
The random scenario generator (cft_scenarios_gen.py, --gen-scenarios) and the ==== early termination marker are removed.

Build and tooling details

libgcc_s precedes libleanshared.so on the link line. The Lean runtime exports its own unwinder, and C++ exceptions thrown by the driver terminate the process if it is found first.
driver.cpp sets LeakSanitizer defaults which suppress leaks allocated by libleanshared.so. The Lean runtime keeps its GMP constants in memory which LeakSanitizer does not scan.
The scenarios are a Lake package without dependencies, outside lean/. scripts/lean-format-checks.sh builds it and adds it to LEAN_PATH, because leanfmt loads the modules a file imports.
scripts/test-buckets-checks.sh now reads the test name rather than the last field, so a disabled test stays in the inventory.

CI time impact

The two ci.yml runs on this PR (27f8dec, d93eb98) are compared with the 30 merge queue runs for main from 11 to 13 November 2026, which all passed at the first attempt.
ci.yml only runs for main in the merge queue and on a weekly schedule, not on pushes.
Times are job execution times, without queueing.

Job	`main`: median (p10 to p90)	This PR
VMSS Virtual A	12m48s (12m38s to 13m10s)	12m36s, 12m44s
VMSS Virtual B	12m12s (12m06s to 12m20s)	12m03s, 11m59s
VMSS Virtual C	11m24s (11m13s to 11m51s)	11m40s, 11m47s
ACI SNP Genoa	9m24s (9m17s to 9m37s)	9m21s, 9m26s
Sum of the four jobs	45m50s (45m29s to 46m25s)	45m40s, 45m56s

VMSS Virtual C is the job which gains Install Lean, and the only one which builds cft_driver. In its logs, Install Lean takes 8.3 s and 8.2 s, cmake and ninja take 75.9 s and 73.9 s against a median of 73.0 s, and cft_scenario_test takes 7.2 s and 7.1 s against 6.7 s. That is about 10 s, or 1.5% of the job. The job is 16 s and 24 s over its median, and the remainder is in dependency installation and tests which this PR does not change.
VMSS Virtual A does not install Lean, and is the longest job in all 32 runs.
lean.yml does not run for main, so it has no such baseline. On this PR, Install Lean takes 8 s in its scenario captures job, and the disaster-recovery format check spends 5 s to 7 s building the scenarios.
ci-al4.yml, coverage.yml and long-test.yml do not run on this PR, so they are not measured.

Alternatives

Generate the comma-separated files from Lean and keep the parser. This avoids linking the Lean runtime, but the language survives as a wire format, and scenarios cannot call the driver directly.
Put the scenarios in a package under lean/, following the conventions for model packages. That needs the leanfmt dependency, so building cft_driver would clone it from GitHub during the C++ build.
Keep main in C++ and call an exported Lean entry point. That needs runtime initialisation code whose names and signatures change between Lean releases, where linking the main which Lean generates needs none.

Replace the comma-separated scenario language parsed by cft_driver with Lean bindings to the driver. Each scenario in tests/cft_scenarios/Scenarios is now a Lean program, calling the commands declared in CftDriver.lean, which driver.cpp implements. lake compiles the scenarios to a static library defining main, which CMake links with the bindings and the Lean runtime. The 56 existing scenarios are translated mechanically, and produce the same traces as before. Without lake, CMake does not build cft_driver and disables cft_scenario_test. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

…-lamp Resolve conflicts with "Replay each native replicate batch as one model append" (#8738), which changed the scenario language and every scenario: - driver.h: take the batched replicate, without its lineno parameter. - driver.cpp and CftDriver.lean: replicate takes a list of entries, and emitSignature is removed, as emit_signature was. - Scenarios: translate the updated scenarios again, including the new batched_append. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot

🟡 Changes recommended

The string conversion truncates replicated entries at embedded NUL bytes, corrupting transaction data and potentially misclassifying entries as signatures.

1 open issue

Preserve embedded NUL bytes in Lean string bindings · New

What changed in this PR

This PR replaces CCF's ad-hoc consensus scenario language with Lean programs that call the native driver through bindings, integrating scenario authoring with the existing Lean verification tooling.

Changes:

Translates scenarios to Lean and runs them by registered name rather than file path.
Adds Lake build integration and Lean installation in relevant CI jobs; disables the scenario test when Lake is unavailable.
Removes random scenario generation and updates documentation, debugging, and tooling.

Custom instructions used: .github/instructions/reviewing.instructions.md.

File	Description
`tests/cft_trace.py`	Runs named scenarios and checks successful trace capture.
`tests/cft_scenarios/swap_single_node`	Removes legacy node-swap scenario.
`tests/cft_scenarios/suffix_collision.2`	Removes legacy multi-term suffix scenario.
`tests/cft_scenarios/suffix_collision.1`	Removes legacy suffix-collision scenario.
`tests/cft_scenarios/startup_2nodes`	Removes legacy two-node startup scenario.
`tests/cft_scenarios/startup`	Removes legacy startup scenario.
`tests/cft_scenarios/soft_rollback`	Removes legacy soft-rollback scenario.
`tests/cft_scenarios/Scenarios/swap_single_node.lean`	Translates node replacement to Lean.
`tests/cft_scenarios/Scenarios/suffix_collision_1.lean`	Translates suffix conflict recovery to Lean.
`tests/cft_scenarios/Scenarios/startup.lean`	Translates single-node startup to Lean.
`tests/cft_scenarios/Scenarios/startup_2nodes.lean`	Translates two-node startup to Lean.
`tests/cft_scenarios/Scenarios/retirement_rollback.lean`	Translates retirement rollback to Lean.
`tests/cft_scenarios/Scenarios/retirement_nominates_most_replicated.lean`	Translates successor-selection checks to Lean.
`tests/cft_scenarios/Scenarios/retirement_commit_below_signature.lean`	Translates retirement commit-boundary checks to Lean.
`tests/cft_scenarios/Scenarios/retired_node_delayed_responses.lean`	Translates delayed-response checks to Lean.
`tests/cft_scenarios/Scenarios/retired_committed_delayed_nomination.lean`	Translates post-retirement nomination checks to Lean.
`tests/cft_scenarios/Scenarios/retire_one.lean`	Translates single-peer retirement to Lean.
`tests/cft_scenarios/Scenarios/retire_backup.lean`	Translates backup retirement and reconnection to Lean.
`tests/cft_scenarios/Scenarios/retire_backup_pre_vote.lean`	Translates retired-backup pre-vote checks to Lean.
`tests/cft_scenarios/Scenarios/replicate.lean`	Translates replication checks to Lean.
`tests/cft_scenarios/Scenarios/replicate_on_latest_leader.lean`	Translates latest-leader selection checks to Lean.
`tests/cft_scenarios/Scenarios/reelection.lean`	Translates re-election checks to Lean.
`tests/cft_scenarios/Scenarios/reconnect.lean`	Translates reconnection and catch-up to Lean.
`tests/cft_scenarios/Scenarios/reconfiguration.lean`	Translates membership expansion to Lean.
`tests/cft_scenarios/Scenarios/reconfig_01_el2_23.lean`	Translates replacement with node 2 elected.
`tests/cft_scenarios/Scenarios/reconfig_01_el2_12.lean`	Translates partial replacement with node 2 elected.
`tests/cft_scenarios/Scenarios/reconfig_01_el1_12.lean`	Translates partial replacement with node 1 elected.
`tests/cft_scenarios/Scenarios/reconfig_01_el0_23.lean`	Translates replacement with node 0 re-elected.
`tests/cft_scenarios/Scenarios/reconfig_01_el0_12.lean`	Translates partial replacement with node 0 re-elected.
`tests/cft_scenarios/Scenarios/reconfig_01_23.lean`	Translates full membership replacement to Lean.
`tests/cft_scenarios/Scenarios/reconfig_01_12.lean`	Translates partial membership replacement to Lean.
`tests/cft_scenarios/Scenarios/reconfig_0_1.lean`	Translates single-node replacement to Lean.
`tests/cft_scenarios/Scenarios/pre_vote.lean`	Translates pre-vote behavior checks to Lean.
`tests/cft_scenarios/Scenarios/pre_vote_split.lean`	Translates partitioned pre-vote elections to Lean.
`tests/cft_scenarios/Scenarios/nominate_without_successor.lean`	Translates nomination without an eligible peer.
`tests/cft_scenarios/Scenarios/nominate_successor.lean`	Translates successor nomination to Lean.
`tests/cft_scenarios/Scenarios/multi_election.lean`	Translates repeated elections and recovery to Lean.
`tests/cft_scenarios/Scenarios/message_type_summaries.lean`	Translates message diagnostic scenarios to Lean.
`tests/cft_scenarios/Scenarios/matching_partial.lean`	Translates partially matching append regression to Lean.
`tests/cft_scenarios/Scenarios/liveness_through_conflict.lean`	Translates conflict-resolution liveness checks to Lean.
`tests/cft_scenarios/Scenarios/leadership_race.lean`	Translates leaderless-operation checks to Lean.
`tests/cft_scenarios/Scenarios/late_nomination.lean`	Translates stale nomination checks to Lean.
`tests/cft_scenarios/Scenarios/indirect_commit_stale_leader.lean`	Translates indirect-commit safety checks to Lean.
`tests/cft_scenarios/Scenarios/follower_rollback_match_index.lean`	Translates follower rollback regression to Lean.
`tests/cft_scenarios/Scenarios/fancy_election_2.lean`	Translates the Raft Figure 8 scenario.
`tests/cft_scenarios/Scenarios/election.lean`	Translates basic leader election to Lean.
`tests/cft_scenarios/Scenarios/election_while_reconfiguration.lean`	Translates joint-configuration election checks to Lean.
`tests/cft_scenarios/Scenarios/delayed_vote_requests.lean`	Translates delayed-vote handling to Lean.
`tests/cft_scenarios/Scenarios/check_quorum.lean`	Translates quorum-loss checks to Lean.
`tests/cft_scenarios/Scenarios/check_quorum_012_0.lean`	Translates quorum checks during membership contraction.
`tests/cft_scenarios/Scenarios/check_quorum_0_012.lean`	Translates quorum checks during membership expansion.
`tests/cft_scenarios/Scenarios/batched_append.lean`	Translates batched replication checks to Lean.
`tests/cft_scenarios/Scenarios/append.lean`	Translates local append and commit checks to Lean.
`tests/cft_scenarios/Scenarios.lean`	Imports scenarios and defines the executable entry point.
`tests/cft_scenarios/rollback_safety`	Removes legacy rollback-safety scenario.
`tests/cft_scenarios/retirement_rollback`	Removes legacy retirement-rollback scenario.
`tests/cft_scenarios/retirement_nominates_most_replicated`	Removes legacy successor-selection scenario.
`tests/cft_scenarios/retirement_commit_below_signature`	Removes legacy retirement commit-boundary scenario.
`tests/cft_scenarios/retired_node_delayed_responses`	Removes legacy delayed-response scenario.
`tests/cft_scenarios/retired_committed_delayed_nomination`	Removes legacy post-retirement nomination scenario.
`tests/cft_scenarios/retire_one`	Removes legacy single-peer retirement scenario.
`tests/cft_scenarios/retire_backup_pre_vote`	Removes legacy retired-backup pre-vote scenario.
`tests/cft_scenarios/retire_backup`	Removes legacy backup-retirement scenario.
`tests/cft_scenarios/replicate_on_latest_leader`	Removes legacy latest-leader selection scenario.
`tests/cft_scenarios/replicate`	Removes legacy replication scenario.
`tests/cft_scenarios/reelection`	Removes legacy re-election scenario.
`tests/cft_scenarios/reconnect`	Removes legacy reconnection scenario.
`tests/cft_scenarios/reconfiguration`	Removes legacy membership-expansion scenario.
`tests/cft_scenarios/reconfig_01_el2_23`	Removes legacy replacement/election scenario.
`tests/cft_scenarios/reconfig_01_el2_12`	Removes legacy partial-replacement/election scenario.
`tests/cft_scenarios/reconfig_01_el1_12`	Removes legacy node-1 election scenario.
`tests/cft_scenarios/reconfig_01_el0_23`	Removes legacy replacement/re-election scenario.
`tests/cft_scenarios/reconfig_01_el0_12`	Removes legacy partial-replacement/re-election scenario.
`tests/cft_scenarios/reconfig_01_23`	Removes legacy full-replacement scenario.
`tests/cft_scenarios/reconfig_01_12`	Removes legacy partial-replacement scenario.
`tests/cft_scenarios/reconfig_0_1`	Removes legacy single-node replacement scenario.
`tests/cft_scenarios/README.md`	Documents authoring, building, running, and bindings.
`tests/cft_scenarios/pre_vote_split`	Removes legacy partitioned pre-vote scenario.
`tests/cft_scenarios/pre_vote_double_leader`	Removes legacy election-safety regression scenario.
`tests/cft_scenarios/pre_vote`	Removes legacy pre-vote scenario.
`tests/cft_scenarios/nominate_without_successor`	Removes legacy no-successor nomination scenario.
`tests/cft_scenarios/nominate_successor`	Removes legacy successor nomination scenario.
`tests/cft_scenarios/multi_election`	Removes legacy repeated-election scenario.
`tests/cft_scenarios/message_type_summaries`	Removes legacy message-diagnostics scenario.
`tests/cft_scenarios/matching_partial`	Removes legacy partial-append regression scenario.
`tests/cft_scenarios/liveness_through_conflict`	Removes legacy conflict-liveness scenario.
`tests/cft_scenarios/leadership_race`	Removes legacy leadership-race scenario.
`tests/cft_scenarios/late_nomination`	Removes legacy stale-nomination scenario.
`tests/cft_scenarios/lakefile.toml`	Defines the standalone scenario library package.
`tests/cft_scenarios/lake-manifest.json`	Records the dependency-free Lake package.
`tests/cft_scenarios/indirect_commit_stale_leader`	Removes legacy indirect-commit scenario.
`tests/cft_scenarios/follower_rollback_match_index`	Removes legacy follower-rollback regression scenario.
`tests/cft_scenarios/fancy_election.2`	Removes legacy Raft Figure 8 scenario.
`tests/cft_scenarios/fancy_election.1`	Removes legacy partitioned-election scenario.
`tests/cft_scenarios/election_while_reconfiguration`	Removes legacy joint-configuration election scenario.
`tests/cft_scenarios/election`	Removes legacy basic-election scenario.
`tests/cft_scenarios/delayed_vote_requests`	Removes legacy delayed-vote scenario.
`tests/cft_scenarios/check_quorum_012_0`	Removes legacy contraction-quorum scenario.
`tests/cft_scenarios/check_quorum_0_012`	Removes legacy expansion-quorum scenario.
`tests/cft_scenarios/check_quorum`	Removes legacy quorum-loss scenario.
`tests/cft_scenarios/batched_append`	Removes legacy batched-replication scenario.
`tests/cft_scenarios/bad_network`	Removes legacy unreliable-network scenario.
`tests/cft_scenarios/append`	Removes legacy local-append scenario.
`tests/cft_scenarios/ackuracy`	Removes legacy stale-acknowledgment scenario.
`tests/cft_scenarios_runner.py`	Discovers Lean files and executes registered names.
`tests/cft_scenarios_gen.py`	Removes random legacy scenario generation.
`scripts/test-buckets-checks.sh`	Preserves disabled tests in the test inventory.
`scripts/lean-format-checks.sh`	Makes scenario modules available to the formatter.
`scripts/ascii-checks.sh`	Updates an explanatory comment about excluded files.
`lean/consensus/replay/README.md`	Documents Lake as a capture-generation prerequisite.
`doc/architecture/verification.rst`	Describes Lean scenarios and optional build support.
`CMakeLists.txt`	Builds and links Lean scenarios when Lake is available.
`.vscode/launch.json`	Launches scenarios by filename stem.
`.gitignore`	Ignores scenario Lake build artifacts.
`.github/workflows/README.md`	Documents Lean setup and workflow coverage.
`.github/workflows/long-test.yml`	Installs Lean before relevant builds.
`.github/workflows/lean.yml`	Installs Lean for captures and tracks action changes.
`.github/workflows/coverage.yml`	Installs Lean for the coverage build.
`.github/workflows/ci.yml`	Installs Lean for the relevant CI build.
`.github/workflows/ci-al4.yml`	Installs Lean for Azure Linux CI.
`.github/skills/testing/SKILL.md`	Documents the scenario test's Lean prerequisite.
`.github/actions/install-lean/action.yml`	Adds shared installation of the pinned Lean toolchain.

_{Review effort: Balanced}

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Copilot

🟡 Changes recommended

On fresh CI runners, the Lake invocation has no selected toolchain, causing CMake configuration to fail; the affected commands need a package-local pin or explicit selection of the existing pinned toolchain.

1 open issue

Select a pinned Lean toolchain for scenario builds · New

1 resolved since last review

Preserve embedded NUL bytes in Lean string bindings

_{Review effort: Balanced}

Amaury Chamayou (achamayou) and others added 2 commits November 13, 2026 16:59

Amaury Chamayou (achamayou) marked this pull request as ready for review November 13, 2026 18:03

Amaury Chamayou (achamayou) requested a review from a team as a code owner November 13, 2026 18:03

Copilot AI balanced review requested due to automatic review settings November 13, 2026 18:03

Copilot started reviewing on behalf of Amaury Chamayou (achamayou) November 13, 2026 18:04

View session

Copilot AI reviewed Nov 13, 2026

View reviewed changes

Comment thread src/consensus/aft/test/driver.cpp Resolved

Fix string conversion to exclude null terminator

d93eb98

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Copilot AI balanced review requested due to automatic review settings November 13, 2026 18:18

Copilot started reviewing on behalf of Amaury Chamayou (achamayou) November 13, 2026 18:18

View session

Copilot AI reviewed Nov 13, 2026

View reviewed changes

Comment thread CMakeLists.txt Resolved

Navigation Menu

Repository navigation

Write consensus scenarios in Lean - #8773

Write consensus scenarios in Lean#8773
Amaury Chamayou (achamayou) wants to merge 3 commits into
mainfrom
achamayou-symmetrical-lamp

Amaury Chamayou (achamayou) commented Nov 13, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

Amaury Chamayou (achamayou) commented Nov 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Alternatives

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

🟡 Changes recommended

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

🟡 Changes recommended

Uh oh!

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Amaury Chamayou (achamayou) commented Nov 13, 2026 •

edited

Loading