Stateful specifications and adaptive clients

Specifications describe mathematical states, typed operations and admissibility. Clients use Quang Dao's upstream PFunctor.FreeM; continuations may depend on earlier answers. The state interpreter and its histories have no computational-model or performance claim. In particular, pure Lean computation in continuations is not charged as a machine instruction.

Main definitions

• Spec: stateful operation semantics with typed answers and admissibility.
• Spec.toFLTS: the underlying functional labelled transition system (Cslib.FLTS) of state transitions.
• Spec.run: the final state and typed observation trace of a history.
• Spec.ValidHistory: each operation of a history is admissible in the state it reaches.
• Spec.totalCost: state-dependent charges summed along a history.
• Spec.signature: the polynomial functor of operations and their observation types.
• Spec.Client: terminating, potentially infinitely branching adaptive clients.
• Spec.runClient: mathematical interpretation with the selected operation history.
• eval: the result and final state of a client, without its history.
• product: independent abstract components; concrete independence is a realization obligation.

Main results

• Spec.fst_run_eq_toFLTS_mtr: the state component of Spec.run agrees with FLTS.mtr.
• Spec.run_append, Spec.validHistory_append, Spec.totalCost_append: history composition laws.
• Spec.totalCost_le_length_mul, Spec.totalCost_const, Spec.totalCost_one: uniform and constant history charge bounds.
• Spec.validHistory_of_forall_valid: total interfaces have no history admissibility obligations.
• Spec.run_runClient: the history recorded by Spec.runClient reaches the computed final state.
• Spec.runClient_bind, eval_bind: sequential composition preserves state, answers and history order.
• eval_eq_liftM: eval agrees with PFunctor.FreeM.liftM into StateM.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, Chapter 17.
• J. E. Hopcroft, R. Motwani, J. D. Ullman, Introduction to Automata Theory, Languages, and Computation.

structure Cslib.Stateful.Spec : Type (max (max (u + 1) (v + 1)) (w + 1))

A deterministic abstract state machine with operation-dependent observations. Only admissible operations are constrained by refinement certificates.

• State : Type u

  Mathematical states, independent of a storage representation.

• Op : Type v

  Operations available to clients.

• Result : self.Op → Type w

  The observation type returned by each operation.

• step (s : self.State) (o : self.Op) : self.State × self.Result o

  The specified state transition and observation.

• valid : self.State → self.Op → Prop

  Preconditions under which an operation's implementation must satisfy its contract.

def Cslib.Stateful.Spec.toFLTS (D : Spec) : FLTS D.State D.Op

Forget typed observations to view state transitions as a functional labelled transition system.

@[simp]

theorem Cslib.Stateful.Spec.toFLTS_tr (D : Spec) (s : D.State) (o : D.Op) : D.toFLTS.tr s o = (D.step s o).1

The transition function of D.toFLTS is the state component of D.step.

def Cslib.Stateful.Spec.run (D : Spec) (s : D.State) : List D.Op → D.State × List (Sigma D.Result)

The final state and complete typed observation trace of a history.

def Cslib.Stateful.Spec.ValidHistory (D : Spec) (s : D.State) : List D.Op → Prop

Each operation is admissible in the state reached by its predecessors.

def Cslib.Stateful.Spec.totalCost (D : Spec) (charge : D.State → D.Op → ℕ) (s : D.State) : List D.Op → ℕ

State-dependent charges summed along the abstract execution.

@[simp]

theorem Cslib.Stateful.Spec.run_nil (D : Spec) (s : D.State) : D.run s [] = (s, [])

Running the empty history keeps the state and observes nothing.

@[simp]

theorem Cslib.Stateful.Spec.run_cons (D : Spec) (s : D.State) (o : D.Op) (os : List D.Op) : D.run s (o :: os) = ((D.run (D.step s o).1 os).1, ⟨o, (D.step s o).2⟩ :: (D.run (D.step s o).1 os).2)

Running a nonempty history steps once and prepends the typed observation.

theorem Cslib.Stateful.Spec.fst_run_eq_toFLTS_mtr (D : Spec) (s : D.State) (os : List D.Op) : (D.run s os).1 = D.toFLTS.mtr s os

The final state of D.run agrees with the multi-step transition of D.toFLTS.

@[simp]

theorem Cslib.Stateful.Spec.validHistory_nil (D : Spec) (s : D.State) : D.ValidHistory s [] ↔ True

The empty history is admissible in every state.

@[simp]

theorem Cslib.Stateful.Spec.validHistory_cons (D : Spec) (s : D.State) (o : D.Op) (os : List D.Op) : D.ValidHistory s (o :: os) ↔ D.valid s o ∧ D.ValidHistory (D.step s o).1 os

A nonempty history is admissible when its first operation is valid and the tail is admissible from the next state.

theorem Cslib.Stateful.Spec.validHistory_of_forall_valid (D : Spec) (h : ∀ (s : D.State) (o : D.Op), D.valid s o) (s : D.State) (os : List D.Op) : D.ValidHistory s os

Total interfaces have no history admissibility obligations.

@[simp]

theorem Cslib.Stateful.Spec.totalCost_nil (D : Spec) (charge : D.State → D.Op → ℕ) (s : D.State) : D.totalCost charge s [] = 0

The empty history costs nothing.

@[simp]

theorem Cslib.Stateful.Spec.totalCost_cons (D : Spec) (charge : D.State → D.Op → ℕ) (s : D.State) (o : D.Op) (os : List D.Op) : D.totalCost charge s (o :: os) = charge s o + D.totalCost charge (D.step s o).1 os

The cost of a nonempty history adds the first operation's charge to the tail cost from the next state.

theorem Cslib.Stateful.Spec.run_append (D : Spec) (s : D.State) (xs ys : List D.Op) : D.run s (xs ++ ys) = ((D.run (D.run s xs).1 ys).1, (D.run s xs).2 ++ (D.run (D.run s xs).1 ys).2)

Concatenation preserves both the state and the observation order.

theorem Cslib.Stateful.Spec.totalCost_append (D : Spec) (charge : D.State → D.Op → ℕ) (s : D.State) (xs ys : List D.Op) : D.totalCost charge s (xs ++ ys) = D.totalCost charge s xs + D.totalCost charge (D.run s xs).1 ys

Charges compose at the intermediate abstract state.

theorem Cslib.Stateful.Spec.totalCost_le_length_mul (D : Spec) (charge : D.State → D.Op → ℕ) (T : ℕ) (h : ∀ (s : D.State) (o : D.Op), D.valid s o → charge s o ≤ T) {s : D.State} {os : List D.Op} (hv : D.ValidHistory s os) : D.totalCost charge s os ≤ os.length * T

Uniform operation bounds imply a bound proportional to history length.

theorem Cslib.Stateful.Spec.totalCost_const (D : Spec) (K : ℕ) (s : D.State) (os : List D.Op) : D.totalCost (fun (x : D.State) (x_1 : D.Op) => K) s os = os.length * K

A constant charge K per operation totals K times the length of the history.

theorem Cslib.Stateful.Spec.totalCost_one (D : Spec) (s : D.State) (os : List D.Op) : D.totalCost (fun (x : D.State) (x_1 : D.Op) => 1) s os = os.length

A unit charge per operation totals the length of the history.

@[reducible, inline]

abbrev Cslib.Stateful.Spec.signature (D : Spec) : PFunctor.{v, w}

The polynomial operation signature, shared with upstream effectful programs.

@[reducible, inline]

abbrev Cslib.Stateful.Spec.Client (D : Spec) (α : Type y) : Type (max v w y)

An adaptive client: each continuation may depend on the observed answer. Inductive clients have no infinite execution branch; branching need not be finite.

def Cslib.Stateful.Spec.runClient (D : Spec) {α : Type y} (s : D.State) : D.Client α → α × D.State × List D.Op

Interpret a client mathematically, retaining its chosen operation history.

@[simp]

theorem Cslib.Stateful.Spec.runClient_pure (D : Spec) {α : Type y} (s : D.State) (a : α) : D.runClient s (PFunctor.FreeM.pure a) = (a, s, [])

Interpreting a pure client returns its value, preserves the state, and records no operations.

@[simp]

theorem Cslib.Stateful.Spec.runClient_pure' (D : Spec) {α : Type y} (s : D.State) (a : α) : D.runClient s (pure a) = (a, s, [])

Interpreting a pure client returns its value, preserves the state, and records no operations.

@[simp]

theorem Cslib.Stateful.Spec.runClient_lift (D : Spec) (s : D.State) (o : D.Op) : D.runClient s (PFunctor.FreeM.lift o) = ((D.step s o).2, (D.step s o).1, [o])

Interpreting a single lifted operation steps the specification once.

@[simp]

theorem Cslib.Stateful.Spec.runClient_liftBind (D : Spec) {α : Type y} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) : D.runClient s (PFunctor.FreeM.liftBind o k) = ((D.runClient (D.step s o).1 (k (D.step s o).2)).1, (D.runClient (D.step s o).1 (k (D.step s o).2)).2.1, o :: (D.runClient (D.step s o).1 (k (D.step s o).2)).2.2)

Interpreting an operation call steps the specification and continues from the resulting state and answer.

@[simp]

theorem Cslib.Stateful.Spec.runClient_lift_bind (D : Spec) {α : Type y} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) : D.runClient s ((PFunctor.FreeM.lift o).bind k) = ((D.runClient (D.step s o).1 (k (D.step s o).2)).1, (D.runClient (D.step s o).1 (k (D.step s o).2)).2.1, o :: (D.runClient (D.step s o).1 (k (D.step s o).2)).2.2)

Interpreting a lifted operation bound to a continuation steps the specification and continues from the resulting state and answer.

@[simp]

theorem Cslib.Stateful.Spec.runClient_lift_bind' (D : Spec) {α : Type w} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) : D.runClient s (PFunctor.FreeM.lift o >>= k) = ((D.runClient (D.step s o).1 (k (D.step s o).2)).1, (D.runClient (D.step s o).1 (k (D.step s o).2)).2.1, o :: (D.runClient (D.step s o).1 (k (D.step s o).2)).2.2)

Interpreting a lifted operation monadically bound to a continuation steps the specification and continues from the resulting state and answer.

theorem Cslib.Stateful.Spec.run_runClient (D : Spec) {α : Type y} (p : D.Client α) (s : D.State) : (D.run s (D.runClient s p).2.2).1 = (D.runClient s p).2.1

The actual history chosen by an adaptive client has its computed final state.

theorem Cslib.Stateful.Spec.validHistory_append {D : Spec} (s : D.State) (xs ys : List D.Op) : D.ValidHistory s (xs ++ ys) ↔ D.ValidHistory s xs ∧ D.ValidHistory (D.run s xs).1 ys

Admissibility splits at the mathematical state reached by the first history.

theorem Cslib.Stateful.Spec.runClient_bind {D : Spec} {α β : Type y} (p : D.Client α) (k : α → D.Client β) (s : D.State) : D.runClient s (PFunctor.FreeM.bind p k) = have first := D.runClient s p; have rest := D.runClient first.2.1 (k first.1); (rest.1, rest.2.1, first.2.2 ++ rest.2.2)

Sequential interpretation concatenates the histories actually selected by the client.

def Cslib.Stateful.eval {α : Type y} (D : Spec) (p : D.Client α) (s : D.State) : α × D.State

Observe results and state without displaying the operation history.

@[simp]

theorem Cslib.Stateful.eval_pure {D : Spec} {α : Type y} (s : D.State) (a : α) : eval D (PFunctor.FreeM.pure a) s = (a, s)

Evaluating a pure client returns its value and leaves the state unchanged.

@[simp]

theorem Cslib.Stateful.eval_pure' {D : Spec} {α : Type y} (s : D.State) (a : α) : eval D (pure a) s = (a, s)

Evaluating a pure client returns its value and leaves the state unchanged.

@[simp]

theorem Cslib.Stateful.eval_lift {D : Spec} (s : D.State) (o : D.Op) : eval D (PFunctor.FreeM.lift o) s = ((D.step s o).2, (D.step s o).1)

Evaluating a single lifted operation steps the state and returns its answer.

@[simp]

theorem Cslib.Stateful.eval_liftBind {D : Spec} {α : Type y} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) : eval D (PFunctor.FreeM.liftBind o k) s = eval D (k (D.step s o).2) (D.step s o).1

Evaluating an operation call steps the state and continues with the observed answer.

@[simp]

theorem Cslib.Stateful.eval_lift_bind {D : Spec} {α : Type y} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) : eval D ((PFunctor.FreeM.lift o).bind k) s = eval D (k (D.step s o).2) (D.step s o).1

Evaluating a lifted operation bound to a continuation steps the state and continues with the observed answer.

@[simp]

theorem Cslib.Stateful.eval_lift_bind' {D : Spec} {α : Type w} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) : eval D (PFunctor.FreeM.lift o >>= k) s = eval D (k (D.step s o).2) (D.step s o).1

Evaluating a lifted operation monadically bound to a continuation steps the state and continues with the observed answer.

theorem Cslib.Stateful.eval_bind {D : Spec} {α β : Type y} (p : D.Client α) (k : α → D.Client β) (s : D.State) : eval D (PFunctor.FreeM.bind p k) s = eval D (k (eval D p s).1) (eval D p s).2

Evaluating p.bind k evaluates p, then the continuation k at its result from the state p reaches.

theorem Cslib.Stateful.eval_eq_liftM {D : Spec} {α : Type u} (p : D.Client α) (s : D.State) : StateT.run (PFunctor.FreeM.liftM (fun (o : D.signature.A) (s : D.State) => ((D.step s o).2, (D.step s o).1)) p) s = eval D p s

eval agrees with interpreting the free monad into StateM D.State via PFunctor.FreeM.liftM when states, operation answers, and client results share a universe.

@[reducible, inline]

abbrev Cslib.Stateful.product (D E : Spec) : Spec

Two independent abstract components. A backend must separately justify their independence.

@[simp]

theorem Cslib.Stateful.product_step_inl (D E : Spec) (s : D.State × E.State) (o : D.Op) : (product D E).step s (Sum.inl o) = (((D.step s.1 o).1, s.2), (D.step s.1 o).2)

Stepping the left component of a product specification preserves the right state.

@[simp]

theorem Cslib.Stateful.product_step_inr (D E : Spec) (s : D.State × E.State) (o : E.Op) : (product D E).step s (Sum.inr o) = ((s.1, (E.step s.2 o).1), (E.step s.2 o).2)

Stepping the right component of a product specification preserves the left state.

@[simp]

theorem Cslib.Stateful.product_valid_inl (D E : Spec) (s : D.State × E.State) (o : D.Op) : (product D E).valid s (Sum.inl o) ↔ D.valid s.1 o

Admissibility of a left operation in a product specification depends only on the left state.

@[simp]

theorem Cslib.Stateful.product_valid_inr (D E : Spec) (s : D.State × E.State) (o : E.Op) : (product D E).valid s (Sum.inr o) ↔ E.valid s.2 o

Admissibility of a right operation in a product specification depends only on the right state.