From 3c7dfab8ba561113db3e685b70b7c93d579dfe81 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Thu, 22 Oct 2026 15:45:50 +0100
Subject: [PATCH] Bundle Lean transition system state and action types

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>
---
 lean/ccf-raft/CCFRaft/Model.lean              |  4 +-
 .../CCFRaft/Proofs/Direct/Framework.lean      |  8 +++-
 .../CCFRaft/Proofs/Safety/History.lean        |  4 +-
 lean/ccf-raft/CCFRaft/Proofs/Witnesses.lean   | 46 +++++++++----------
 lean/common/CCF/Execution.lean                | 28 ++++++-----
 .../common/CCF/MultiNodeTransitionSystem.lean |  6 ++-
 lean/common/CCF/TransitionSystem.lean         | 19 +++++---
 lean/common/README.md                         |  8 ++++
 .../DisasterRecovery/Model.lean               |  2 +-
 .../DisasterRecovery/Proofs/Execution.lean    |  4 +-
 .../Proofs/ExecutionLocal.lean                |  5 +-
 .../DisasterRecovery/Proofs/Gossip.lean       |  6 ++-
 .../DisasterRecovery/Proofs/History.lean      |  3 +-
 .../DisasterRecovery/Proofs/Invariants.lean   |  6 ++-
 .../DisasterRecovery/Proofs/Lifting.lean      | 11 +++--
 .../DisasterRecovery/Proofs/Observed.lean     |  3 +-
 .../DisasterRecovery/Proofs/Quorum.lean       |  3 +-
 .../DisasterRecovery/Proofs/Trace.lean        | 14 +++---
 .../DisasterRecovery/Proofs/Witnesses.lean    |  4 +-
 .../Tests/CanonicalTests.lean                 |  6 ++-
 .../DisasterRecovery/Tests/Execution.lean     | 35 ++++++++++----
 .../DisasterRecovery/Tests/Network.lean       |  4 +-
 .../DisasterRecovery/Tests/Trace.lean         |  4 +-
 23 files changed, 143 insertions(+), 90 deletions(-)

diff --git a/lean/ccf-raft/CCFRaft/Model.lean b/lean/ccf-raft/CCFRaft/Model.lean
index 696b8aa8664..038fe863445 100644
--- a/lean/ccf-raft/CCFRaft/Model.lean
+++ b/lean/ccf-raft/CCFRaft/Model.lean
@@ -71,8 +71,8 @@ def protocol (initialConfiguration : Finset NodeID)
   internal := .internal
 
 /-- The network of `nodes`, initialized from a nonempty membership configuration. -/
-def transitionSystem (initialConfiguration : Finset NodeID) (nodes : List NodeID)
-    : TransitionSystem State Action :=
+abbrev transitionSystem (initialConfiguration : Finset NodeID) (nodes : List NodeID)
+    : TransitionSystem :=
   let system := MultiNodeTransitionSystem.lift (protocol initialConfiguration)
   {
     system with
diff --git a/lean/ccf-raft/CCFRaft/Proofs/Direct/Framework.lean b/lean/ccf-raft/CCFRaft/Proofs/Direct/Framework.lean
index 1b1414638c0..0a1e53566bf 100644
--- a/lean/ccf-raft/CCFRaft/Proofs/Direct/Framework.lean
+++ b/lean/ccf-raft/CCFRaft/Proofs/Direct/Framework.lean
@@ -40,7 +40,9 @@ theorem NodeInvariant.reachable {P : NodeID -> NodeState -> Prop}
     (reachable
       : (Model.transitionSystem Config.INITIAL_CONFIGURATION nodes).Reachable state)
     : forall node local_, (node, local_) ∈ state.nodes -> P node local_ := by
-  induction reachable with
+  induction reachable
+    using @TransitionSystem.Reachable.rec
+      (Model.transitionSystem Config.INITIAL_CONFIGURATION nodes) with
   | initial initialized =>
       intro node local_ member
       have initial : local_ = initialNodeState Config.INITIAL_CONFIGURATION node := initialized.2.2.2.2 (node, local_) member
@@ -72,7 +74,9 @@ theorem keys_nodup {nodes : List NodeID} {state : Model.State}
     (reachable
       : (Model.transitionSystem Config.INITIAL_CONFIGURATION nodes).Reachable state)
     : (state.nodes.map Prod.fst).Nodup := by
-  induction reachable with
+  induction reachable
+    using @TransitionSystem.Reachable.rec
+      (Model.transitionSystem Config.INITIAL_CONFIGURATION nodes) with
   | initial initialized => exact initialized.2.2.1
   | @step before after action _ stepped ih =>
       cases action with
diff --git a/lean/ccf-raft/CCFRaft/Proofs/Safety/History.lean b/lean/ccf-raft/CCFRaft/Proofs/Safety/History.lean
index 657c00b2d63..120c5050256 100644
--- a/lean/ccf-raft/CCFRaft/Proofs/Safety/History.lean
+++ b/lean/ccf-raft/CCFRaft/Proofs/Safety/History.lean
@@ -40,7 +40,9 @@ theorem exec_of_reachable {nodes : List NodeID} {state : Model.State}
     (reachable
       : (Model.transitionSystem Config.INITIAL_CONFIGURATION nodes).Reachable state)
     : exists history, Exec nodes (state :: history) := by
-  induction reachable with
+  induction reachable
+    using @TransitionSystem.Reachable.rec
+      (Model.transitionSystem Config.INITIAL_CONFIGURATION nodes) with
   | initial initialized => exact ⟨[], .initial initialized⟩
   | step _ stepped ih =>
       obtain ⟨history, prior⟩ := ih
diff --git a/lean/ccf-raft/CCFRaft/Proofs/Witnesses.lean b/lean/ccf-raft/CCFRaft/Proofs/Witnesses.lean
index 448d1feda9a..60f424be921 100644
--- a/lean/ccf-raft/CCFRaft/Proofs/Witnesses.lean
+++ b/lean/ccf-raft/CCFRaft/Proofs/Witnesses.lean
@@ -27,20 +27,19 @@ open CCFRaft.Model (initialNodeState)
 
 section Runs
 
-variable {State Action : Type}
-
 /-- The final state of choosing each action from the current state, when every
 chosen action is enabled. -/
-def run (system : TransitionSystem State Action) (start : State)
-    : List (State -> Action) -> Option State
+def run (system : TransitionSystem) (start : system.State)
+    : List (system.State -> system.Action) -> Option system.State
   | [] => some start
   | choose :: rest =>
       (system.step start (choose start)).bind fun next => run system next rest
 
 /-- Each prefix of a finished run finishes, and its next choice is enabled. -/
-theorem run_take_step {system : TransitionSystem State Action} {start final : State}
-    {choices : List (State -> Action)} (finished : run system start choices = some final)
-    {index : Nat} (bounded : index < choices.length)
+theorem run_take_step {system : TransitionSystem} {start final : system.State}
+    {choices : List (system.State -> system.Action)}
+    (finished : run system start choices = some final) {index : Nat}
+    (bounded : index < choices.length)
     : exists before after,
         run system start (choices.take index) = some before
         /\ run system start (choices.take (index + 1)) = some after
@@ -69,9 +68,9 @@ theorem run_take_step {system : TransitionSystem State Action} {start final : St
 The states of running `stem` from `start` and then repeating `cycle` forever.
 The default `start` is never used when the runs finish.
 -/
-def lasso (system : TransitionSystem State Action) (start : State)
-    (stem cycle : List (State -> Action)) (index : Nat)
-    : State :=
+def lasso (system : TransitionSystem) (start : system.State)
+    (stem cycle : List (system.State -> system.Action)) (index : Nat)
+    : system.State :=
   if index < stem.length then
     (run system start (stem.take index)).getD start
   else
@@ -80,21 +79,21 @@ def lasso (system : TransitionSystem State Action) (start : State)
       start
 
 /-- The lasso as an infinite trace. -/
-def lassoTrace (system : TransitionSystem State Action) (start : State)
-    (stem cycle : List (State -> Action))
-    : Trace State :=
+def lassoTrace (system : TransitionSystem) (start : system.State)
+    (stem cycle : List (system.State -> system.Action))
+    : Trace system.State :=
   Stream'.Seq.ofStream (lasso system start stem cycle)
 
-theorem lassoTrace_get? {system : TransitionSystem State Action} {start : State}
-    {stem cycle : List (State -> Action)} (index : Nat)
+theorem lassoTrace_get? {system : TransitionSystem} {start : system.State}
+    {stem cycle : List (system.State -> system.Action)} (index : Nat)
     : (lassoTrace system start stem cycle).get? index
       = some (lasso system start stem cycle index) :=
   rfl
 
 /-- A finished stem followed by a nonempty cycle back to its final state is a
 valid infinite trace. -/
-theorem lasso_valid {system : TransitionSystem State Action} {start final : State}
-    {stem cycle : List (State -> Action)} (initialized : system.init start)
+theorem lasso_valid {system : TransitionSystem} {start final : system.State}
+    {stem cycle : List (system.State -> system.Action)} (initialized : system.init start)
     (stemRun : run system start stem = some final)
     (cycleRun : run system final cycle = some final) (nonempty : cycle ≠ [])
     : (lassoTrace system start stem cycle).Valid system := by
@@ -150,9 +149,10 @@ theorem lasso_valid {system : TransitionSystem State Action} {start final : Stat
       exact enabled
 
 /-- Every state reached by a prefix of the stem occurs in the lasso. -/
-theorem lasso_mem {system : TransitionSystem State Action} {start final state : State}
-    {stem cycle : List (State -> Action)} (stemRun : run system start stem = some final)
-    {index : Nat} (bounded : index <= stem.length)
+theorem lasso_mem {system : TransitionSystem} {start final state : system.State}
+    {stem cycle : List (system.State -> system.Action)}
+    (stemRun : run system start stem = some final) {index : Nat}
+    (bounded : index <= stem.length)
     (reached : run system start (stem.take index) = some state)
     : state ∈ lassoTrace system start stem cycle := by
   apply Stream'.Seq.get?_mem (n := index)
@@ -272,7 +272,7 @@ elab "kernel_rfl" : tactic => closeMainGoalUsing `kernel_rfl fun target _ => do
 
 section Election
 
-def electionSystem := CCFRaft.Model.transitionSystem {0, 1, 2} [0, 1, 2]
+abbrev electionSystem := CCFRaft.Model.transitionSystem {0, 1, 2} [0, 1, 2]
 
 def electionStart := start {0, 1, 2} [0, 1, 2]
 
@@ -338,7 +338,7 @@ end Election
 
 section Commit
 
-def commitSystem := CCFRaft.Model.transitionSystem {0, 1} [0, 1]
+abbrev commitSystem := CCFRaft.Model.transitionSystem {0, 1} [0, 1]
 
 def commitStart := start {0, 1} [0, 1]
 
@@ -415,7 +415,7 @@ end Commit
 
 section Single
 
-def singleSystem := CCFRaft.Model.transitionSystem {0} [0]
+abbrev singleSystem := CCFRaft.Model.transitionSystem {0} [0]
 
 def singleStart := start {0} [0]
 
diff --git a/lean/common/CCF/Execution.lean b/lean/common/CCF/Execution.lean
index d305fe498d5..12f2ad4633b 100644
--- a/lean/common/CCF/Execution.lean
+++ b/lean/common/CCF/Execution.lean
@@ -16,12 +16,13 @@ quantified where needed.
 -/
 
 /-- `Run system start actions final`: executing `actions` from `start` reaches `final`. -/
-inductive Run {State Action : Type} (system : TransitionSystem State Action)
-    : State -> List Action -> State -> Prop where
+inductive Run (system : TransitionSystem)
+    : system.State -> List system.Action -> system.State -> Prop where
   /-- An empty action list leaves the state unchanged. -/
-  | nil (state : State) : Run system state [] state
+  | nil (state : system.State) : Run system state [] state
   /-- Prepend one enabled action to the rest of an execution. -/
-  | cons {before middle after : State} {action : Action} {actions : List Action}
+  | cons {before middle after : system.State} {action : system.Action}
+    {actions : List system.Action}
     (step : system.step before action = some middle)
     (rest : Run system middle actions after)
     : Run system before (action :: actions) after
@@ -32,9 +33,7 @@ abbrev Trace (State : Type) := Stream'.Seq State
 
 /-- The trace is nonempty, its first state is initial, and each later state
 follows its predecessor by some enabled action. -/
-def Trace.Valid {State Action : Type} (trace : Trace State)
-    (system : TransitionSystem State Action)
-    : Prop :=
+def Trace.Valid (system : TransitionSystem) (trace : Trace system.State) : Prop :=
   (exists initial, trace.get? 0 = some initial /\ system.init initial)
   /\ forall i before after,
       trace.get? i = some before
@@ -42,9 +41,9 @@ def Trace.Valid {State Action : Type} (trace : Trace State)
       -> exists action, system.step before action = some after
 
 /-- Every state in a valid trace is reachable. -/
-theorem Trace.Valid.reachable {State Action : Type}
-    {system : TransitionSystem State Action}
-    {trace : Trace State} (valid : trace.Valid system) {state : State}
+theorem Trace.Valid.reachable
+    {system : TransitionSystem}
+    {trace : Trace system.State} (valid : trace.Valid system) {state : system.State}
     (member : state ∈ trace)
     : system.Reachable state := by
   obtain ⟨index, found⟩ := Stream'.Seq.mem_iff_exists_get?.mp member
@@ -64,14 +63,13 @@ theorem Trace.Valid.reachable {State Action : Type}
 
 /-- Valid traces cover exactly the reachable states. Every reachable state is the
 last state of some valid finite trace. -/
-theorem reachable_iff_trace {State Action : Type}
-    {system : TransitionSystem State Action} {state : State}
+theorem reachable_iff_trace {system : TransitionSystem} {state : system.State}
     : system.Reachable state
-      <-> exists trace : Trace State, trace.Valid system /\ state ∈ trace := by
+      <-> exists trace : Trace system.State, trace.Valid system /\ state ∈ trace := by
   constructor
   · intro reachable
-    suffices finite : exists states : List State,
-        Trace.Valid (Stream'.Seq.ofList (states ++ [state])) system by
+    suffices finite : exists states : List system.State,
+        Trace.Valid system (Stream'.Seq.ofList (states ++ [state])) by
       obtain ⟨states, valid⟩ := finite
       exact ⟨_, valid, Stream'.Seq.get?_mem (n := states.length) (by simp [Stream'.Seq.ofList_get?])⟩
     induction reachable with
diff --git a/lean/common/CCF/MultiNodeTransitionSystem.lean b/lean/common/CCF/MultiNodeTransitionSystem.lean
index 85be7f59810..4ce67d0f445 100644
--- a/lean/common/CCF/MultiNodeTransitionSystem.lean
+++ b/lean/common/CCF/MultiNodeTransitionSystem.lean
@@ -114,10 +114,12 @@ def next {Node Message LocalState LocalAction Notification Input : Type}
 /-- The network as a `TransitionSystem`. Initially node identities are distinct,
 every node has an initial local state, and the network is empty. Protocols
 choose which nodes must exist and which may act. -/
-def lift {Node Message LocalState LocalAction Notification Input : Type}
+abbrev lift {Node Message LocalState LocalAction Notification Input : Type}
     [BEq Node] [BEq Message]
     (protocol : Protocol Node LocalState LocalAction Message Notification Input)
-    : TransitionSystem (State Node LocalState Message) (Action Node Message Input) where
+    : TransitionSystem where
+  State := State Node LocalState Message
+  Action := Action Node Message Input
   init state :=
     (state.nodes.map Prod.fst).Nodup
     /\ state.network = []
diff --git a/lean/common/CCF/TransitionSystem.lean b/lean/common/CCF/TransitionSystem.lean
index 13249cd5497..cbbb3ae79bd 100644
--- a/lean/common/CCF/TransitionSystem.lean
+++ b/lean/common/CCF/TransitionSystem.lean
@@ -7,13 +7,18 @@ public import Std
 namespace CCF
 
 /-!
-The minimal interface every model implements. `init` picks out the initial
+The minimal interface every model implements, bundling its state and action types.
+`init` picks out the initial
 states; `step` applies one action. Every other shared definition (traces,
 reachability, the multi-node network) is built on these two fields.
 -/
 
 /-- `none` disables an action; `some state` may be an enabled stutter. -/
-structure TransitionSystem (State Action : Type) where
+structure TransitionSystem where
+  /-- The states of the model. -/
+  State : Type
+  /-- The actions that may be applied to a state. -/
+  Action : Type
   /-- The states from which an execution may start. -/
   init : State -> Prop
   /-- Applies an action, returning `none` exactly when the action is disabled. -/
@@ -22,14 +27,14 @@ structure TransitionSystem (State Action : Type) where
 namespace TransitionSystem
 
 /-- States reached from an initial state by finitely many enabled steps. -/
-inductive Reachable {State Action : Type} (system : TransitionSystem State Action)
-    : State -> Prop where
+inductive Reachable (system : TransitionSystem) : system.State -> Prop where
   /-- An initial state is reachable without taking any steps. -/
-  | initial {state : State} (initialized : system.init state) : Reachable system state
+  | initial {state : system.State} (initialized : system.init state)
+    : Reachable system state
   /-- An enabled step preserves reachability. -/
   | step
-    {state nextState : State}
-    {action : Action}
+    {state nextState : system.State}
+    {action : system.Action}
     (reachable : Reachable system state)
     (transition : system.step state action = some nextState)
     : Reachable system nextState
diff --git a/lean/common/README.md b/lean/common/README.md
index 0506bca152b..12713f6ec57 100644
--- a/lean/common/README.md
+++ b/lean/common/README.md
@@ -12,6 +12,14 @@ The `ccf_common` Lake package exposes protocol-independent definitions in the `C
 `CCF.Execution` represents traces as Mathlib's `Stream'.Seq`, so the package depends on Mathlib.
 `reachable_iff_trace` shows that valid finite traces reach exactly the reachable states.
 
+## Transition systems
+
+`CCF.TransitionSystem` bundles the `State` and `Action` types with the initial-state predicate `init` and the partial transition function `step`.
+Define a model as `system : TransitionSystem`, setting `State` and `Action` in the structure rather than supplying type parameters.
+Use `abbrev` for concrete systems so Lean can unfold their bundled types during typeclass inference.
+Generic helpers use `system.State` and `system.Action`, while `system.Reachable state` and `Execution.Run system start actions final` describe executions.
+Traces remain state sequences of type `Execution.Trace system.State`; `Execution.Trace.Valid system trace` (or `trace.Valid system`) checks them against the bundled system.
+
 ## Import coverage
 
 After `lake build`, run `lake exe check-imports` from any package using `ccf_common`.
diff --git a/lean/disaster-recovery/DisasterRecovery/Model.lean b/lean/disaster-recovery/DisasterRecovery/Model.lean
index 5186e386c54..6ed85ca5fa1 100644
--- a/lean/disaster-recovery/DisasterRecovery/Model.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Model.lean
@@ -66,7 +66,7 @@ def protocol (config : Config)
 
 /-- Composes recovery nodes.
 Initial states include every expected location but may also contain unused nodes. -/
-def transitionSystem (config : Config) : TransitionSystem State Action :=
+abbrev transitionSystem (config : Config) : TransitionSystem :=
   let network := MultiNodeTransitionSystem.lift (protocol config)
   {
     network with
diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Execution.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Execution.lean
index 90472050f7b..4bf52ad183c 100644
--- a/lean/disaster-recovery/DisasterRecovery/Proofs/Execution.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Execution.lean
@@ -169,7 +169,9 @@ def next (config : Config) (state : State) : Action -> Option State
       pure (recordEffects target output.state output.effects { state with system })
 
 /-- The decorated execution system with valid recovery configurations. -/
-def transitionSystem (config : Config) : TransitionSystem State Action where
+abbrev transitionSystem (config : Config) : TransitionSystem where
+  State := State
+  Action := Action
   init :=
     fun state =>
       config.Valid
diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/ExecutionLocal.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/ExecutionLocal.lean
index f9f2e68d637..d4af5af7588 100644
--- a/lean/disaster-recovery/DisasterRecovery/Proofs/ExecutionLocal.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Proofs/ExecutionLocal.lean
@@ -132,8 +132,9 @@ def rejected (state : NodeState) (reason : String) : StepOutput :=
   { state, effects := [.rejected reason], accepted := false }
 
 /-- Local instrumentation whose disabled transitions are converted to stutters by `step`. -/
-def transitionSystem (config : Config) (location : Location)
-    : TransitionSystem StepOutput Event where
+abbrev transitionSystem (config : Config) (location : Location) : TransitionSystem where
+  State := StepOutput
+  Action := Event
   init := fun current => current = { state := initialNode location }
   step current event :=
     let state := current.state
diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Gossip.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Gossip.lean
index 4a895c9ceea..223fbf31b36 100644
--- a/lean/disaster-recovery/DisasterRecovery/Proofs/Gossip.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Gossip.lean
@@ -244,7 +244,8 @@ lemma next_frozen {config : Config} {before after : State} {action : Action}
 lemma reachable_gossip_invariant {config : Config} {state : State}
     (reachable : Reachable config state)
     : Genuine config state.system.nodes /\ FrozenVotes state := by
-  induction reachable with
+  induction reachable
+    using @CCF.TransitionSystem.Reachable.rec (transitionSystem config) with
   | initial initialized =>
       obtain ⟨_, nodes, _, _, rfl⟩ := initialized
       constructor
@@ -271,7 +272,8 @@ lemma steps_evolve {config : Model.Config} {before after : Model.State} {steps}
     (reachable : (Model.transitionSystem config).Reachable before)
     {node : Location} {current : NodeState} (member : (node, current) ∈ before.nodes)
     : exists updated, (node, updated) ∈ after.nodes /\ Evolves current updated := by
-  induction run generalizing current with
+  induction run
+    using @Trace.Path.rec (Model.transitionSystem config) generalizing current with
   | nil => exact ⟨current, member, evolves_refl current⟩
   | cons transition _ ih =>
       obtain ⟨middle, present, evolves⟩ := model_step_evolves reachable transition member
diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/History.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/History.lean
index ca94b420617..3ebf570cac0 100644
--- a/lean/disaster-recovery/DisasterRecovery/Proofs/History.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Proofs/History.lean
@@ -29,7 +29,8 @@ lemma trace_lifts {config : Model.Config} {before after : Model.State} {tail}
         Decoration config ghost tail final
         /\ Execution.Global.Reachable config final
         /\ erase final = after := by
-  induction path generalizing ghost with
+  induction path
+    using @Trace.Path.rec (Model.transitionSystem config) generalizing ghost with
   | nil => exact ⟨ghost, .nil _, reachable, linked⟩
   | @cons before middle after tail action step _ ih =>
       obtain ⟨ghostAction, ghostMiddle, _, ghostStep, middleEq⟩ :=
diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Invariants.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Invariants.lean
index 6c2f02e96b4..728bf044243 100644
--- a/lean/disaster-recovery/DisasterRecovery/Proofs/Invariants.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Invariants.lean
@@ -807,7 +807,8 @@ lemma reachable_well_formed
     {state : State}
     (reachable : Reachable config state)
     : WellFormed config state := by
-  induction reachable with
+  induction reachable
+    using @CCF.TransitionSystem.Reachable.rec (transitionSystem config) with
   | initial initialized =>
       rcases initialized with
         ⟨valid, nodes, nodesNodup, covered, rfl⟩
@@ -820,7 +821,8 @@ lemma reachable_config_valid
     {state : State}
     (reachable : Reachable config state)
     : config.Valid := by
-  induction reachable with
+  induction reachable
+    using @CCF.TransitionSystem.Reachable.rec (transitionSystem config) with
   | initial initialized =>
       rcases initialized with ⟨valid, _⟩
       exact valid
diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Lifting.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Lifting.lean
index 4bdd594f51c..04dae1c6af7 100644
--- a/lean/disaster-recovery/DisasterRecovery/Proofs/Lifting.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Lifting.lean
@@ -126,7 +126,7 @@ lemma step_erases (config : Config) (recovered : TxID) (state : NodeState) (even
   all_goals cases phase : state.phase
   all_goals
     dsimp only [Execution.Local.step]
-    simp [step, Execution.Local.transitionSystem,
+    simp [step,
       Execution.Local.rejectionReason, Execution.Local.rejected, rejected,
       advance, Execution.Local.advance, phase, validTimeout, guard, failure] at h ⊢
   all_goals
@@ -558,7 +558,8 @@ theorem model_reachable_lifts {config : Model.Config} {state : Model.State}
     (reachable : (Model.transitionSystem config).Reachable state)
     : exists decorated,
         Execution.Global.Reachable config decorated /\ erase decorated = state := by
-  induction reachable with
+  induction reachable
+    using @CCF.TransitionSystem.Reachable.rec (Model.transitionSystem config) with
   | initial initialized =>
       obtain ⟨decorated, init, projected⟩ := model_initial_lifts config _ initialized
       exact ⟨decorated, .initial init, projected⟩
@@ -601,8 +602,10 @@ lemma execution_lifts {config : Model.Config}
         Run (Execution.Global.transitionSystem config) decorated ghostActions ghostAfter
         /\ ghostActions.map eraseAction = actions
         /\ erase ghostAfter = after := by
-  induction run generalizing decorated with
-  | nil state => exact ⟨[], decorated, .nil decorated, rfl, linked⟩
+  induction run using @Run.rec (Model.transitionSystem config) generalizing decorated with
+  | nil state =>
+      exact ⟨[], decorated, .nil (system := Execution.Global.transitionSystem config) decorated,
+        rfl, linked⟩
   | @cons before middle after action actions step _ ih =>
       obtain ⟨ghostAction, ghostMiddle, erasedAction, ghostStep, erasedMiddle⟩ :=
         step_lifts config decorated action middle
diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Observed.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Observed.lean
index 9d5902dc615..0c938f9a5ac 100644
--- a/lean/disaster-recovery/DisasterRecovery/Proofs/Observed.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Observed.lean
@@ -105,7 +105,8 @@ lemma next_preserves_opening_thresholds (config : Model.Config) (before after :
 lemma reachable_opening_thresholds {config : Model.Config} {state : State}
     (reachable : Reachable config state)
     : OpeningThresholds config state := by
-  induction reachable with
+  induction reachable
+    using @CCF.TransitionSystem.Reachable.rec (transitionSystem config) with
   | initial initialized =>
       rcases initialized with ⟨_, nodes, _, _, rfl⟩
       simp [OpeningThresholds, initial, initialNode]
diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Quorum.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Quorum.lean
index 6919d5b69db..613e8fd1e8f 100644
--- a/lean/disaster-recovery/DisasterRecovery/Proofs/Quorum.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Quorum.lean
@@ -1243,7 +1243,8 @@ lemma reachable_quorum_invariant
     {state : State}
     (reachable : Reachable config state)
     : QuorumInvariant config state := by
-  induction reachable with
+  induction reachable
+    using @CCF.TransitionSystem.Reachable.rec (transitionSystem config) with
   | initial initialized =>
       rcases initialized with ⟨_, nodes, _, _, rfl⟩
       exact initial_quorum_invariant config nodes
diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Trace.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Trace.lean
index 8ce9ff1ffe2..48436f3c689 100644
--- a/lean/disaster-recovery/DisasterRecovery/Proofs/Trace.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Trace.lean
@@ -9,11 +9,11 @@ namespace DisasterRecovery.Proofs.Trace
 
 open CCF
 
-variable {State Action : Type}
+variable {State : Type}
 
 /-- Enabled steps through the listed successor states, from a start state to a final state. -/
-inductive Path (system : TransitionSystem State Action)
-    : State -> List State -> State -> Prop where
+inductive Path (system : TransitionSystem)
+    : system.State -> List system.State -> system.State -> Prop where
   /-- An empty path starts and ends at the same state. -/
   | nil (state) : Path system state [] state
   /-- Prepend one enabled step and its successor to the remaining path. -/
@@ -22,14 +22,14 @@ inductive Path (system : TransitionSystem State Action)
     (rest : Path system middle tail after)
     : Path system before (middle :: tail) after
 
-lemma Path.reachable {system : TransitionSystem State Action} {before tail after}
+lemma Path.reachable {system : TransitionSystem} {before tail after}
     (path : Path system before tail after) (reachable : system.Reachable before)
     : system.Reachable after := by
   induction path with
   | nil => exact reachable
   | cons step _ ih => exact ih (.step reachable step)
 
-lemma Path.run {system : TransitionSystem State Action} {before tail after}
+lemma Path.run {system : TransitionSystem} {before tail after}
     (path : Path system before tail after)
     : exists actions, Execution.Run system before actions after := by
   induction path with
@@ -39,8 +39,8 @@ lemma Path.run {system : TransitionSystem State Action} {before tail after}
       exact ⟨_, .cons step rest⟩
 
 /-- Enabled steps connect a state of a valid trace to every later state of the trace. -/
-lemma valid_path {system : TransitionSystem State Action} {trace : Execution.Trace State}
-    (valid : trace.Valid system) (start count : Nat) {before after : State}
+lemma valid_path {system : TransitionSystem} {trace : Execution.Trace system.State}
+    (valid : trace.Valid system) (start count : Nat) {before after : system.State}
     (first : trace.get? start = some before)
     (last : trace.get? (start + count) = some after)
     : exists tail, Path system before tail after := by
diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Witnesses.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Witnesses.lean
index 7c1b1d9ece2..a77d03b5bbc 100644
--- a/lean/disaster-recovery/DisasterRecovery/Proofs/Witnesses.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Witnesses.lean
@@ -24,8 +24,8 @@ private theorem valid_of_adjacent {config : Model.Config} {states : List Model.S
           exists action,
             (Model.transitionSystem config).step (states[i.val]'(by omega)) action
             = some (states[i.val + 1]'(by omega)))
-    : Execution.Trace.Valid (Stream'.Seq.ofList states)
-        (Model.transitionSystem config) := by
+    : Execution.Trace.Valid (Model.transitionSystem config)
+        (Stream'.Seq.ofList states) := by
   refine ⟨by simpa only [Stream'.Seq.ofList_get?] using initialized, ?_⟩
   intro i before after atBefore atAfter
   rw [Stream'.Seq.ofList_get?] at atBefore atAfter
diff --git a/lean/disaster-recovery/DisasterRecovery/Tests/CanonicalTests.lean b/lean/disaster-recovery/DisasterRecovery/Tests/CanonicalTests.lean
index 01745b1ccbe..e283192dc40 100644
--- a/lean/disaster-recovery/DisasterRecovery/Tests/CanonicalTests.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Tests/CanonicalTests.lean
@@ -15,8 +15,10 @@ open DisasterRecovery
 open CCF
 open DisasterRecovery.Model.Local
 
-private def localMachine (config : Config) (recovered : TxID) (location : Location)
-    : TransitionSystem NodeState Event where
+private abbrev localMachine (config : Config) (recovered : TxID) (location : Location)
+    : TransitionSystem where
+  State := NodeState
+  Action := Event
   init := fun state => state = initialNode location
   step :=
     fun state event =>
diff --git a/lean/disaster-recovery/DisasterRecovery/Tests/Execution.lean b/lean/disaster-recovery/DisasterRecovery/Tests/Execution.lean
index 4908de83351..9e35b430bda 100644
--- a/lean/disaster-recovery/DisasterRecovery/Tests/Execution.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Tests/Execution.lean
@@ -9,10 +9,23 @@ namespace DisasterRecovery.Tests.Execution
 open CCF
 open CCF.Execution
 
-private def counter : TransitionSystem Nat Bool where
+private abbrev counter : TransitionSystem where
+  State := Nat
+  Action := Bool
   init state := state = 0
   step state increment := if increment then some (state + 1) else some state
 
+example : counter.State = Nat := rfl
+
+example : counter.Action = Bool := rfl
+
+-- Generic executions use only the types carried by the system.
+example (system : TransitionSystem) (state : system.State) : Run system state [] state :=
+  .nil state
+
+example : Run counter 0 [true, false, true] 2 :=
+  .cons rfl (.cons rfl (.cons rfl (.nil (system := counter) 2)))
+
 -- Stutters are allowed: each adjacent pair needs only some enabled action.
 private def counting : Trace Nat := Stream'.Seq.ofList [0, 0, 1, 2]
 
@@ -33,26 +46,32 @@ example (state : Nat)
   reachable_iff_trace
 
 -- An empty trace has no initial state.
-example : ¬ Trace.Valid (Stream'.Seq.ofList []) counter := by
+example : ¬ Trace.Valid counter (Stream'.Seq.ofList []) := by
   rintro ⟨⟨_, first, _⟩, _⟩
   simp at first
 
-example : ¬ Trace.Valid (Stream'.Seq.ofList [1]) counter := by
+example : ¬ Trace.Valid counter (Stream'.Seq.ofList [1]) := by
   rintro ⟨⟨initial, first, initialized⟩, _⟩
   simp at first
   subst first
-  simp [counter] at initialized
+  simp at initialized
 
 -- Adjacent states must be related by an enabled action.
-example : ¬ Trace.Valid (Stream'.Seq.ofList [0, 2]) counter := by
+example : ¬ Trace.Valid counter (Stream'.Seq.ofList [0, 2]) := by
   rintro ⟨_, steps⟩
   obtain ⟨action, step⟩ := steps 0 0 2 rfl rfl
   cases action <;> simp [counter] at step
 
 example
-    : ¬ Trace.Valid (Stream'.Seq.ofList [0, 0])
-          ({ init := fun state => state = 0, step := fun _ _ => none }
-            : TransitionSystem Nat Unit) := by
+    : ¬ Trace.Valid
+          ({
+              State := Nat,
+              Action := Unit,
+              init := fun state => state = 0,
+              step := fun _ _ => none
+            }
+            : TransitionSystem)
+          (Stream'.Seq.ofList [0, 0]) := by
   rintro ⟨_, steps⟩
   obtain ⟨_, step⟩ := steps 0 0 0 rfl rfl
   cases step
diff --git a/lean/disaster-recovery/DisasterRecovery/Tests/Network.lean b/lean/disaster-recovery/DisasterRecovery/Tests/Network.lean
index 0919b9184e1..1be9a22970d 100644
--- a/lean/disaster-recovery/DisasterRecovery/Tests/Network.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Tests/Network.lean
@@ -115,11 +115,11 @@ private def initial : MultiNodeTransitionSystem.State Nat Nat Nat :=
 
 example
     : (MultiNodeTransitionSystem.lift protocol).init { nodes := [(9, 0), (1, 0)] } := by
-  simp [MultiNodeTransitionSystem.lift, protocol, or_imp, and_imp]
+  simp [protocol, or_imp, and_imp]
 
 example
     : ¬ (MultiNodeTransitionSystem.lift protocol).init { nodes := [(1, 0), (1, 0)] } := by
-  simp [MultiNodeTransitionSystem.lift]
+  simp
 
 private def expect (condition : Bool) (message : String) : IO Unit :=
   unless condition do throw (IO.userError message)
diff --git a/lean/disaster-recovery/DisasterRecovery/Tests/Trace.lean b/lean/disaster-recovery/DisasterRecovery/Tests/Trace.lean
index 4463ca2c647..a8a9fc37250 100644
--- a/lean/disaster-recovery/DisasterRecovery/Tests/Trace.lean
+++ b/lean/disaster-recovery/DisasterRecovery/Tests/Trace.lean
@@ -239,8 +239,8 @@ example
     ⟩
 
 example
-    : ¬ Execution.Trace.Valid (Stream'.Seq.ofList [ready, voteSent])
-          (Model.transitionSystem config) := by
+    : ¬ Execution.Trace.Valid (Model.transitionSystem config)
+          (Stream'.Seq.ofList [ready, voteSent]) := by
   rintro ⟨⟨start, first, _, _, _, _, nodes⟩, _⟩
   have same : start = ready := by simpa using first.symm
   subst start