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.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.runClient_bind: sequential composition preserves state, answers and history order.
• Spec.totalCost_append: state-dependent charges compose along a history.

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.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.totalCost_nil (D : Spec) (charge : D.State → D.Op → ℕ) (s : D.State) : D.totalCost charge s [] = 0

The empty history costs nothing.

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.

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

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.

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.

@[reducible, inline]

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

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

theorem Cslib.Stateful.valid_history_of_total (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.