lean: Bundle state and action types in transition systems

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

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,19 +33,17 @@ 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
       -> trace.get? (i + 1) = some after
       -> 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

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 = []

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

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`.

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