Repository navigation
lean: Bundle state and action types in transition systems - #8624
Merged
Heidi Howard (heidihoward) merged 3 commits intoOct 22, 2026
Merged
Heidi Howard (heidihoward) merged 3 commits into
Heidi Howard (heidihoward) merged 3 commits into
Conversation
Update execution helpers, network composition, models, and proofs to use the bundled types, with regression coverage and migration documentation. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…transition-system-with-state-action
Contributor
There was a problem hiding this comment.
🔵 Needs a closer look
The shared formal-model interface affects both protocol packages, and whole-package kernel and axiom checks remain unverified.
No open issues 🎉
What changed in this PR
This PR updates CCF's shared Lean transition-system interface to bundle state and action types, then adapts the Raft and disaster-recovery models and proofs without changing transition behavior.
Changes:
- Move
StateandActionintoTransitionSystemand update execution, reachability, and network composition. - Adapt both protocol models and dependent proofs, using
abbrevfor concrete systems. - Add bundled-type regression examples and document the updated API.
Custom instructions used
Applied the CCF repository instructions supplied in the review context; no additional instruction files were loaded.
| File | Description |
|---|---|
lean/disaster-recovery/DisasterRecovery/Tests/Trace.lean |
Update trace-validity argument order. |
lean/disaster-recovery/DisasterRecovery/Tests/Network.lean |
Adapt simplification to the network abbreviation. |
lean/disaster-recovery/DisasterRecovery/Tests/Execution.lean |
Add bundled-type examples and migrate validity checks. |
lean/disaster-recovery/DisasterRecovery/Tests/CanonicalTests.lean |
Bundle local-machine types. |
lean/disaster-recovery/DisasterRecovery/Proofs/Witnesses.lean |
Update trace-validity construction. |
lean/disaster-recovery/DisasterRecovery/Proofs/Trace.lean |
Express paths using bundled state types. |
lean/disaster-recovery/DisasterRecovery/Proofs/Quorum.lean |
Specify the bundled-system induction recursor. |
lean/disaster-recovery/DisasterRecovery/Proofs/Observed.lean |
Adapt reachability induction. |
lean/disaster-recovery/DisasterRecovery/Proofs/Lifting.lean |
Adapt lifting proofs and execution constructors. |
lean/disaster-recovery/DisasterRecovery/Proofs/Invariants.lean |
Adapt invariant induction proofs. |
lean/disaster-recovery/DisasterRecovery/Proofs/History.lean |
Specify the path induction recursor. |
lean/disaster-recovery/DisasterRecovery/Proofs/Gossip.lean |
Adapt reachability and path induction. |
lean/disaster-recovery/DisasterRecovery/Proofs/ExecutionLocal.lean |
Bundle local instrumentation types. |
lean/disaster-recovery/DisasterRecovery/Proofs/Execution.lean |
Bundle decorated execution types. |
lean/disaster-recovery/DisasterRecovery/Model.lean |
Expose the recovery system as an abbreviation. |
lean/common/README.md |
Document bundled types and API usage. |
lean/common/CCF/TransitionSystem.lean |
Bundle types and update reachability. |
lean/common/CCF/MultiNodeTransitionSystem.lean |
Bundle network types in lift. |
lean/common/CCF/Execution.lean |
Update runs, trace validity, and reachability proofs. |
lean/ccf-raft/CCFRaft/Proofs/Witnesses.lean |
Migrate execution helpers and concrete witness systems. |
lean/ccf-raft/CCFRaft/Proofs/Safety/History.lean |
Adapt history reachability induction. |
lean/ccf-raft/CCFRaft/Proofs/Direct/Framework.lean |
Adapt invariant and node-uniqueness induction. |
lean/ccf-raft/CCFRaft/Model.lean |
Expose the Raft system as an abbreviation. |
Review effort: Balanced
Amaury Chamayou (achamayou)
approved these changes
Oct 22, 2026
Heidi Howard (heidihoward)
enabled auto-merge (squash)
October 22, 2026 15:37
cjen1-msft
added a commit
that referenced
this pull request
Oct 23, 2026
Follow #8624: TransitionSystem now bundles its State and Action types. Generalize the witness run helper over the bundled system, make the witness systems abbreviations, and name the Reachable recursor explicitly when inducting over reachability of the Raft transition system. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This change folds the state and action types into the definition of
TransitionSystem, bringing it more in line with standard definitions of transition systems.StateandActionfields of the structure rather than external type parameters.system.Stateandsystem.Action, preserving existing transition behavior.Concrete systems use
abbrevso Lean can unfold the bundled types during typeclass inference.Validation
lake build --wfail --fail-fast.lake check --inadvisably-no-sandboxpasses for all three packages: common (4m44s), disaster recovery (18m54s), and CCF-Raft (19m34s). Lean's kernel accepts each export; only the permitted axiomspropext,Quot.sound, andClassical.choiceare used. Earlier timeouts were too short for the export and kernel replay; no code changes were required.uv/uvxand CMake; required CI checks remain necessary.