State-transition specifications and adaptive clients

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

The relational semantics is demonic for callers and angelic for implementations:

• An adaptive client p : D.Client α is demonically admissible (D.DemonicValid s p) when each issued operation is admissible (D.valid) and the continuation remains admissible under every outcome (s', a) permitted by D.step.
• Specifications whose step is the graph of a function f, with exactly one outcome f s o for every (s, o), admissible or not, are constructed via StateTransitionSpec.ofFn and recognized by the StateTransitionSpec.HasStepFn typeclass. It implies StateTransitionSpec.Deterministic and StateTransitionSpec.Total, but not conversely: those two together still allow an inadmissible input to have no outcome. It equips these specifications with functional execution helpers (StateTransitionSpec.stepFn, StateTransitionSpec.toFLTS, StateTransitionSpec.run, StateTransitionSpec.ValidHistory, StateTransitionSpec.totalCost, StateTransitionSpec.runClient, eval) and equivalence lemmas connecting the relational and functional views.

Main definitions

• StateTransitionSpec: relational stateful operation semantics with typed answers and admissibility.
• StateTransitionSpec.Total, StateTransitionSpec.Deterministic: totality on admissible inputs and transition determinism.
• StateTransitionSpec.toLTS: the underlying labelled transition system (Cslib.LTS) of input-output transitions.
• StateTransitionSpec.Step, StateTransitionSpec.Transcript, StateTransitionSpec.ValidTranscript, StateTransitionSpec.ValidOpSeq, StateTransitionSpec.totalCostTranscript, StateTransitionSpec.totalCostOutcome: execution transcripts, demonic operation-sequence admissibility, and transcript cost accounting.
• StateTransitionSpec.signature, StateTransitionSpec.Client, StateTransitionSpec.call, StateTransitionSpec.ClientRun, StateTransitionSpec.DemonicValid: adaptive clients, relational client runs, and demonic client admissibility.
• StateTransitionSpec.ofFn, StateTransitionSpec.HasStepFn, StateTransitionSpec.stepFn: constructor and typeclass for specifications given by a transition function.
• StateTransitionSpec.toFLTS, StateTransitionSpec.run, StateTransitionSpec.ValidHistory, StateTransitionSpec.totalCost, StateTransitionSpec.runClient, StateTransitionSpec.clientResult, StateTransitionSpec.clientState, StateTransitionSpec.clientHistory, eval: functional execution and history interpretation under [StateTransitionSpec.HasStepFn].
• product: independent abstract components; concrete independence is an implementation obligation.

Main results

• StateTransitionSpec.Transcript.labels_map_fst, StateTransitionSpec.ValidTranscript.append, StateTransitionSpec.totalCostTranscript_append: transcript projection and composition laws.
• StateTransitionSpec.exists_validTranscript_of_validOpSeq, StateTransitionSpec.DemonicValid.exists_clientRun: existence of valid runs under [StateTransitionSpec.Total].
• StateTransitionSpec.ClientRun.bind, StateTransitionSpec.clientRun_bind_iff, StateTransitionSpec.DemonicValid.bind, StateTransitionSpec.DemonicValid.of_bind: sequential composition and decomposition for relational adaptive clients.
• StateTransitionSpec.validOpSeq_iff_validHistory, StateTransitionSpec.validTranscript_iff_run, StateTransitionSpec.demonicValid_iff_validHistory_runClient, StateTransitionSpec.clientRun_iff_runClient: equivalence of relational and functional semantics under [StateTransitionSpec.HasStepFn].
• StateTransitionSpec.fst_run_eq_toFLTS_mtr, StateTransitionSpec.run_append, StateTransitionSpec.validHistory_append, StateTransitionSpec.totalCost_append, StateTransitionSpec.run_runClient, StateTransitionSpec.runClient_bind, StateTransitionSpec.clientResult_bind, StateTransitionSpec.clientState_bind, StateTransitionSpec.clientHistory_bind, StateTransitionSpec.clientResult_pure, StateTransitionSpec.clientState_pure, StateTransitionSpec.clientHistory_pure, eval_bind, eval_eq_liftM: functional history and client laws under [StateTransitionSpec.HasStepFn].
• StateTransitionSpec.fst_snd_runClient_bind, StateTransitionSpec.snd_snd_runClient_bind, StateTransitionSpec.fst_snd_runClient_pure, StateTransitionSpec.snd_snd_runClient_pure: the state and history laws in the form that simp indexes. With clientResult_bind, clientResult_pure, run_runClient, totalCost_append, validHistory_append and PFunctor.FreeM.bind_eq_bind they form the simp set client_simps: simp only [client_simps] splits the result, final state, history, cost and admissibility of a sequential client at its binds.

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.
• D. Sangiorgi, Introduction to Bisimulation and Coinduction.

structure Cslib.DataStructure.StateTransitionSpec : Type (max (max (u + 1) (v + 1)) (w + 1))

A relational abstract state machine with operation-dependent observations. step s o s' a holds when transitioning from s to s' and returning a : Result o is a permitted outcome of operation o. Only admissible operations (valid s o) 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 → Prop

  Relational state transition and observation specification.

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

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

def Cslib.DataStructure.StateTransitionSpec.outcomes (D : StateTransitionSpec) (s : D.State) (o : D.Op) : Set (D.State × D.Result o)

The set of permitted (nextState, result) outcomes of operation o from state s.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.mem_outcomes_iff (D : StateTransitionSpec) (s : D.State) (o : D.Op) (p : D.State × D.Result o) : p ∈ D.outcomes s o ↔ D.step s o p.1 p.2

Membership in D.outcomes s o unfolds to D.step s o.

class Cslib.DataStructure.StateTransitionSpec.Total (D : StateTransitionSpec) : Prop

A specification is total on admissible inputs if every valid (s, o) admits at least one permitted outcome (s', a).

• step_total (s : D.State) (o : D.Op) : D.valid s o → ∃ (s' : D.State) (a : D.Result o), D.step s o s' a

  Every admissible operation call has at least one permitted post-state and result.

theorem Cslib.DataStructure.StateTransitionSpec.exists_step (D : StateTransitionSpec) [D.Total] {s : D.State} {o : D.Op} (hv : D.valid s o) : ∃ (s' : D.State) (a : D.Result o), D.step s o s' a

Obtain a permitted outcome (s', a) for an admissible operation under [D.Total].

class Cslib.DataStructure.StateTransitionSpec.Deterministic (D : StateTransitionSpec) : Prop

A specification is deterministic if each (s, o) admits at most one outcome (s', a).

• step_deterministic {s : D.State} {o : D.Op} {s₁ : D.State} {a₁ : D.Result o} {s₂ : D.State} {a₂ : D.Result o} : D.step s o s₁ a₁ → D.step s o s₂ a₂ → s₁ = s₂ ∧ a₁ = a₂

  Any two permitted outcomes for the same state and operation coincide.

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.signature (D : StateTransitionSpec) : PFunctor.{v, w}

The polynomial operation signature, shared with upstream effectful programs.

@[instance_reducible]

instance Cslib.DataStructure.StateTransitionSpec.instCoePFunctor : Coe StateTransitionSpec PFunctor.{v, w}

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.Client (D : StateTransitionSpec) (α : 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.

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.call (D : StateTransitionSpec) (o : D.Op) : D.Client (D.Result o)

Invoke a single operation o : D.Op in an adaptive D.Client.

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.Label (D : StateTransitionSpec) : Type (max v w)

An input-output transition label pairing an operation o : D.Op with its result a.

def Cslib.DataStructure.StateTransitionSpec.toLTS (D : StateTransitionSpec) : LTS D.State D.Label

View a stateful specification as a labelled transition system (Cslib.LTS) labelled by input-output pairs ⟨o, a⟩ : Σ o : D.Op, D.Result o.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.toLTS_tr (D : StateTransitionSpec) (s s' : D.State) (lbl : D.Label) : D.toLTS.Tr s lbl s' ↔ D.step s lbl.fst s' lbl.snd

A transition in D.toLTS is a step of D.

instance Cslib.DataStructure.StateTransitionSpec.instDeterministicStateLabelToLTSOfDeterministic (D : StateTransitionSpec) [D.Deterministic] : D.toLTS.Deterministic

Transcripts, non-adaptive operation sequences, and cost accounting

structure Cslib.DataStructure.StateTransitionSpec.Step (D : StateTransitionSpec) : Type (max u v w)

One recorded step of a specification: the issued operation op, its returned observation result, and the resulting post-state nextState.

• op : D.Op

  The operation invoked at this step.

• result : D.Result self.op

  The observation returned by op.

• nextState : D.State

  The abstract post-state reached after op.

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.Transcript (D : StateTransitionSpec) : Type (max u v w)

A finite execution transcript is a list of recorded steps.

def Cslib.DataStructure.StateTransitionSpec.Transcript.ops {D : StateTransitionSpec} (tr : D.Transcript) : List D.Op

Extract the underlying sequence of operations from a transcript.

def Cslib.DataStructure.StateTransitionSpec.Transcript.labels {D : StateTransitionSpec} (tr : D.Transcript) : List D.Label

Extract the Cslib.LTS input-output labels from a transcript.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.Transcript.ops_nil {D : StateTransitionSpec} : ops [] = []

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.Transcript.ops_cons {D : StateTransitionSpec} (st : D.Step) (tr : D.Transcript) : ops (st :: tr) = st.op :: tr.ops

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.Transcript.ops_append {D : StateTransitionSpec} (tr₁ tr₂ : D.Transcript) : (tr₁ ++ tr₂).ops = tr₁.ops ++ tr₂.ops

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.Transcript.length_ops {D : StateTransitionSpec} (tr : D.Transcript) : tr.ops.length = List.length tr

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.Transcript.labels_nil {D : StateTransitionSpec} : labels [] = []

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.Transcript.labels_cons {D : StateTransitionSpec} (st : D.Step) (tr : D.Transcript) : labels (st :: tr) = ⟨st.op, st.result⟩ :: tr.labels

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.Transcript.labels_append {D : StateTransitionSpec} (tr₁ tr₂ : D.Transcript) : (tr₁ ++ tr₂).labels = tr₁.labels ++ tr₂.labels

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.Transcript.length_labels {D : StateTransitionSpec} (tr : D.Transcript) : tr.labels.length = List.length tr

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.Transcript.labels_map_fst {D : StateTransitionSpec} (tr : D.Transcript) : List.map Sigma.fst tr.labels = tr.ops

Projecting the first component of Transcript.labels recovers Transcript.ops.

inductive Cslib.DataStructure.StateTransitionSpec.ValidTranscript (D : StateTransitionSpec) : D.State → D.Transcript → D.State → Prop

D.ValidTranscript s tr s' holds when tr is a valid step-by-step execution starting at s and ending at s', where each step is admissible (D.valid) and permitted by D.step.

• nil {D : StateTransitionSpec} (s : D.State) : D.ValidTranscript s [] s
• cons {D : StateTransitionSpec} {s : D.State} (st : D.Step) {tr : D.Transcript} {s_fin : D.State} : D.valid s st.op → D.step s st.op st.nextState st.result → D.ValidTranscript st.nextState tr s_fin → D.ValidTranscript s (st :: tr) s_fin

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.validTranscript_nil_iff {D : StateTransitionSpec} (s s' : D.State) : D.ValidTranscript s [] s' ↔ s = s'

The empty transcript is valid iff the initial and final states coincide.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.validTranscript_cons_iff {D : StateTransitionSpec} (s s' : D.State) (st : D.Step) (tr : D.Transcript) : D.ValidTranscript s (st :: tr) s' ↔ D.valid s st.op ∧ D.step s st.op st.nextState st.result ∧ D.ValidTranscript st.nextState tr s'

A nonempty transcript is valid iff its head step is admissible and permitted and its tail is valid from st.nextState.

theorem Cslib.DataStructure.StateTransitionSpec.ValidTranscript.append {D : StateTransitionSpec} {s s₁ s₂ : D.State} {tr₁ tr₂ : D.Transcript} (h₁ : D.ValidTranscript s tr₁ s₁) (h₂ : D.ValidTranscript s₁ tr₂ s₂) : D.ValidTranscript s (tr₁ ++ tr₂) s₂

Valid transcripts compose across concatenation.

theorem Cslib.DataStructure.StateTransitionSpec.ValidTranscript.toLTS_mtr {D : StateTransitionSpec} {s s' : D.State} {tr : D.Transcript} (h : D.ValidTranscript s tr s') : D.toLTS.MTr s tr.labels s'

Every valid transcript projects to a multi-step transition in D.toLTS.

def Cslib.DataStructure.StateTransitionSpec.ValidOpSeq (D : StateTransitionSpec) (s : D.State) : List D.Op → Prop

Demonic admissibility of a non-adaptive operation sequence ops : List D.Op from s: the head operation is admissible at s, and the tail sequence remains admissible from every permitted post-state s' of the head operation.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.validOpSeq_nil (D : StateTransitionSpec) (s : D.State) : D.ValidOpSeq s [] ↔ True

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.validOpSeq_cons (D : StateTransitionSpec) (s : D.State) (o : D.Op) (ops : List D.Op) : D.ValidOpSeq s (o :: ops) ↔ D.valid s o ∧ ∀ (s' : D.State) (a : D.Result o), D.step s o s' a → D.ValidOpSeq s' ops

theorem Cslib.DataStructure.StateTransitionSpec.validOpSeq_of_forall_valid (D : StateTransitionSpec) (h : ∀ (s : D.State) (o : D.Op), D.valid s o) (s : D.State) (ops : List D.Op) : D.ValidOpSeq s ops

On a specification where every operation is valid in every state, every operation sequence is demonically admissible.

theorem Cslib.DataStructure.StateTransitionSpec.validOpSeq_append {D : StateTransitionSpec} {s : D.State} {xs ys : List D.Op} (h : D.ValidOpSeq s (xs ++ ys)) : D.ValidOpSeq s xs ∧ ∀ {tr : D.Transcript} {s' : D.State}, tr.ops = xs → D.ValidTranscript s tr s' → D.ValidOpSeq s' ys

Demonic operation-sequence admissibility splits across concatenation across all valid transcripts of the prefix.

theorem Cslib.DataStructure.StateTransitionSpec.exists_validTranscript_of_validOpSeq (D : StateTransitionSpec) [D.Total] {s : D.State} {ops : List D.Op} (hv : D.ValidOpSeq s ops) : ∃ (tr : D.Transcript) (s' : D.State), tr.ops = ops ∧ D.ValidTranscript s tr s'

Under [D.Total], every demonically admissible operation sequence admits at least one valid transcript.

def Cslib.DataStructure.StateTransitionSpec.totalCostTranscript (D : StateTransitionSpec) (charge : D.State → D.Op → ℕ) : D.State → D.Transcript → ℕ

State-dependent charges summed along a transcript.

def Cslib.DataStructure.StateTransitionSpec.totalCostOutcome (D : StateTransitionSpec) (charge : D.State → (o : D.Op) → D.State → D.Result o → ℕ) : D.State → D.Transcript → ℕ

Outcome-dependent charges summed along a transcript, where each step charge may also inspect the post-state st.nextState and result st.result.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_nil (D : StateTransitionSpec) (charge : D.State → D.Op → ℕ) (s : D.State) : D.totalCostTranscript charge s [] = 0

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_cons (D : StateTransitionSpec) (charge : D.State → D.Op → ℕ) (s : D.State) (st : D.Step) (tr : D.Transcript) : D.totalCostTranscript charge s (st :: tr) = charge s st.op + D.totalCostTranscript charge st.nextState tr

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.totalCostOutcome_nil (D : StateTransitionSpec) (charge : D.State → (o : D.Op) → D.State → D.Result o → ℕ) (s : D.State) : D.totalCostOutcome charge s [] = 0

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.totalCostOutcome_cons (D : StateTransitionSpec) (charge : D.State → (o : D.Op) → D.State → D.Result o → ℕ) (s : D.State) (st : D.Step) (tr : D.Transcript) : D.totalCostOutcome charge s (st :: tr) = charge s st.op st.nextState st.result + D.totalCostOutcome charge st.nextState tr

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_eq_totalCostOutcome (D : StateTransitionSpec) (charge : D.State → D.Op → ℕ) (s : D.State) (tr : D.Transcript) : D.totalCostTranscript charge s tr = D.totalCostOutcome (fun (s : D.State) (o : D.Op) (x : D.State) (x_1 : D.Result o) => charge s o) s tr

totalCostTranscript is the special case of totalCostOutcome that ignores the post-state and result.

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_append {D : StateTransitionSpec} (charge : D.State → D.Op → ℕ) {s s₁ : D.State} {tr₁ : D.Transcript} (h₁ : D.ValidTranscript s tr₁ s₁) (tr₂ : D.Transcript) : D.totalCostTranscript charge s (tr₁ ++ tr₂) = D.totalCostTranscript charge s tr₁ + D.totalCostTranscript charge s₁ tr₂

Along a valid transcript prefix D.ValidTranscript s tr₁ s₁, totalCostTranscript splits additively at the intermediate state s₁.

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_le_length_mul {D : StateTransitionSpec} (charge : D.State → D.Op → ℕ) (T : ℕ) (h : ∀ (s : D.State) (o : D.Op), D.valid s o → charge s o ≤ T) {s s' : D.State} {tr : D.Transcript} (hv : D.ValidTranscript s tr s') : D.totalCostTranscript charge s tr ≤ List.length tr * T

Uniform per-operation bounds scale by the transcript length on any valid transcript.

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_const (D : StateTransitionSpec) (K : ℕ) (s : D.State) (tr : D.Transcript) : D.totalCostTranscript (fun (x : D.State) (x_1 : D.Op) => K) s tr = List.length tr * K

A constant charge K per operation totals tr.length * K.

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_one (D : StateTransitionSpec) (s : D.State) (tr : D.Transcript) : D.totalCostTranscript (fun (x : D.State) (x_1 : D.Op) => 1) s tr = List.length tr

A unit charge per operation totals the transcript length.

Adaptive clients (ClientRun and DemonicValid)

inductive Cslib.DataStructure.StateTransitionSpec.ClientRun (D : StateTransitionSpec) {α : Type y} : D.State → D.Client α → α → D.State → D.Transcript → Prop

D.ClientRun s p v s' tr holds when running the adaptive client p : D.Client α from initial state s can produce return value v : α, final state s' : D.State, and transcript tr by making admissible and permitted transitions at each operation call.

• pure {D : StateTransitionSpec} {α : Type y} (s : D.State) (a : α) : D.ClientRun s (PFunctor.FreeM.pure a) a s []
• liftBind {D : StateTransitionSpec} {α : Type y} {s s₁ s₂ : D.State} (o : D.Op) (k : D.Result o → D.Client α) (a : D.Result o) {v : α} {tr : D.Transcript} : D.valid s o → D.step s o s₁ a → D.ClientRun s₁ (k a) v s₂ tr → D.ClientRun s (PFunctor.FreeM.liftBind o k) v s₂ ({ op := o, result := a, nextState := s₁ } :: tr)

theorem Cslib.DataStructure.StateTransitionSpec.ClientRun.validTranscript {α : Type y} {D : StateTransitionSpec} {s s' : D.State} {p : D.Client α} {v : α} {tr : D.Transcript} (h : D.ClientRun s p v s' tr) : D.ValidTranscript s tr s'

Every ClientRun produces a valid transcript.

theorem Cslib.DataStructure.StateTransitionSpec.clientRun_pure_iff {α : Type y} {D : StateTransitionSpec} (s : D.State) (a v : α) (s' : D.State) (tr : D.Transcript) : D.ClientRun s (PFunctor.FreeM.pure a) v s' tr ↔ v = a ∧ s' = s ∧ tr = []

theorem Cslib.DataStructure.StateTransitionSpec.clientRun_liftBind_iff {α : Type y} {D : StateTransitionSpec} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) (v : α) (s₂ : D.State) (tr : D.Transcript) : D.ClientRun s (PFunctor.FreeM.liftBind o k) v s₂ tr ↔ D.valid s o ∧ ∃ (a : D.Result o) (s₁ : D.State) (tr' : D.Transcript), D.step s o s₁ a ∧ D.ClientRun s₁ (k a) v s₂ tr' ∧ tr = { op := o, result := a, nextState := s₁ } :: tr'

theorem Cslib.DataStructure.StateTransitionSpec.ClientRun.bind {α β : Type y} {D : StateTransitionSpec} {s s₁ s₂ : D.State} {p : D.Client α} {k : α → D.Client β} {a : α} {b : β} {tr₁ tr₂ : D.Transcript} (h₁ : D.ClientRun s p a s₁ tr₁) (h₂ : D.ClientRun s₁ (k a) b s₂ tr₂) : D.ClientRun s (PFunctor.FreeM.bind p k) b s₂ (tr₁ ++ tr₂)

Sequential client runs compose by concatenating their transcripts.

theorem Cslib.DataStructure.StateTransitionSpec.clientRun_bind_iff {α β : Type y} {D : StateTransitionSpec} {s s₂ : D.State} {p : D.Client α} {k : α → D.Client β} {b : β} {tr : D.Transcript} : D.ClientRun s (PFunctor.FreeM.bind p k) b s₂ tr ↔ ∃ (a : α) (s₁ : D.State) (tr₁ : D.Transcript) (tr₂ : D.Transcript), D.ClientRun s p a s₁ tr₁ ∧ D.ClientRun s₁ (k a) b s₂ tr₂ ∧ tr = tr₁ ++ tr₂

A client run of p.bind k splits into a run of p and a run of k from the intermediate result and state.

inductive Cslib.DataStructure.StateTransitionSpec.DemonicValid (D : StateTransitionSpec) {α : Type y} : D.State → D.Client α → Prop

Demonic admissibility of an adaptive client p from state s:

• .pure a is always admissible;
• .liftBind o k requires D.valid s o now, and for every permitted outcome (s', a) of o from s, the continuation k a must be demonically admissible from s'.

• pure {D : StateTransitionSpec} {α : Type y} (s : D.State) (a : α) : D.DemonicValid s (PFunctor.FreeM.pure a)
• liftBind {D : StateTransitionSpec} {α : Type y} {s : D.State} (o : D.Op) (k : D.Result o → D.Client α) : D.valid s o → (∀ (s' : D.State) (a : D.Result o), D.step s o s' a → D.DemonicValid s' (k a)) → D.DemonicValid s (PFunctor.FreeM.liftBind o k)

theorem Cslib.DataStructure.StateTransitionSpec.demonicValid_pure_iff {α : Type y} {D : StateTransitionSpec} (s : D.State) (a : α) : D.DemonicValid s (PFunctor.FreeM.pure a) ↔ True

theorem Cslib.DataStructure.StateTransitionSpec.demonicValid_liftBind_iff {α : Type y} {D : StateTransitionSpec} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) : D.DemonicValid s (PFunctor.FreeM.liftBind o k) ↔ D.valid s o ∧ ∀ (s' : D.State) (a : D.Result o), D.step s o s' a → D.DemonicValid s' (k a)

theorem Cslib.DataStructure.StateTransitionSpec.demonicValid_of_forall_valid (D : StateTransitionSpec) {α : Type y} (h : ∀ (s : D.State) (o : D.Op), D.valid s o) (s : D.State) (p : D.Client α) : D.DemonicValid s p

On a specification where every operation is valid in every state, every client is demonically admissible.

theorem Cslib.DataStructure.StateTransitionSpec.DemonicValid.exists_clientRun {α : Type y} {D : StateTransitionSpec} [D.Total] {s : D.State} {p : D.Client α} (hv : D.DemonicValid s p) : ∃ (v : α) (s' : D.State) (tr : D.Transcript), D.ClientRun s p v s' tr

Under [D.Total], every demonically admissible client admits at least one valid ClientRun.

theorem Cslib.DataStructure.StateTransitionSpec.DemonicValid.bind {α β : Type y} {D : StateTransitionSpec} {s : D.State} {p : D.Client α} {k : α → D.Client β} (hp : D.DemonicValid s p) (hk : ∀ (a : α) (s' : D.State) (tr : D.Transcript), D.ClientRun s p a s' tr → D.DemonicValid s' (k a)) : D.DemonicValid s (PFunctor.FreeM.bind p k)

Demonic admissibility composes across bind when the continuation is demonically admissible after every valid run of the first client.

theorem Cslib.DataStructure.StateTransitionSpec.DemonicValid.of_bind {α β : Type y} {D : StateTransitionSpec} {s : D.State} {p : D.Client α} {k : α → D.Client β} (h : D.DemonicValid s (PFunctor.FreeM.bind p k)) : D.DemonicValid s p ∧ ∀ (a : α) (s' : D.State) (tr : D.Transcript), D.ClientRun s p a s' tr → D.DemonicValid s' (k a)

Demonic admissibility of p.bind k splits: p is demonically admissible, and so is the continuation after every valid run of p. This is the converse of DemonicValid.bind.

Specifications given by a transition function (StateTransitionSpec.ofFn,

StateTransitionSpec.HasStepFn) and functional helpers

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.ofFn {State : Type u} {Op : Type v} {Result : Op → Type w} (stepFn : State → (o : Op) → State × Result o) (valid : State → Op → Prop := fun (x : State) (x_1 : Op) => True) : StateTransitionSpec

Construct a deterministic StateTransitionSpec from a pure transition function stepFn : (s : State) → (o : Op) → State × Result o and an optional admissibility predicate valid.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.ofFn_state {State : Type u} {Op : Type v} {Result : Op → Type w} (stepFn : State → (o : Op) → State × Result o) (valid : State → Op → Prop := fun (x : State) (x_1 : Op) => True) : (ofFn stepFn valid).State = State

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.ofFn_op {State : Type u} {Op : Type v} {Result : Op → Type w} (stepFn : State → (o : Op) → State × Result o) (valid : State → Op → Prop := fun (x : State) (x_1 : Op) => True) : (ofFn stepFn valid).Op = Op

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.ofFn_result {State : Type u} {Op : Type v} {Result : Op → Type w} (stepFn : State → (o : Op) → State × Result o) (valid : State → Op → Prop := fun (x : State) (x_1 : Op) => True) : (ofFn stepFn valid).Result = Result

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.ofFn_step_iff {State : Type u} {Op : Type v} {Result : Op → Type w} (stepFn : State → (o : Op) → State × Result o) (valid : State → Op → Prop := fun (x : State) (x_1 : Op) => True) (s : State) (o : Op) (s' : State) (a : Result o) : (ofFn stepFn valid).step s o s' a ↔ (s', a) = stepFn s o

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.ofFn_valid {State : Type u} {Op : Type v} {Result : Op → Type w} (stepFn : State → (o : Op) → State × Result o) (valid : State → Op → Prop := fun (x : State) (x_1 : Op) => True) (s : State) (o : Op) : (ofFn stepFn valid).valid s o ↔ valid s o

class Cslib.DataStructure.StateTransitionSpec.HasStepFn (D : StateTransitionSpec) (f : outParam (D.State → (o : D.Op) → D.State × D.Result o)) : Prop

Typeclass witnessing that a specification D : StateTransitionSpec is governed by a pure transition function f : (s : D.State) → (o : D.Op) → D.State × D.Result o: the only outcome of o from s is f s o, whether or not D.valid s o holds.

• step_iff (s : D.State) (o : D.Op) (s' : D.State) (a : D.Result o) : D.step s o s' a ↔ (s', a) = f s o

  A transition D.step s o s' a holds if and only if (s', a) = f s o.

instance Cslib.DataStructure.StateTransitionSpec.instHasStepFnOfFn {State : Type u} {Op : Type v} {Result : Op → Type w} (f : State → (o : Op) → State × Result o) (valid : State → Op → Prop) : (ofFn f valid).HasStepFn f

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.stepFn (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (o : D.Op) : D.State × D.Result o

The functional transition (s : D.State) → (o : D.Op) → D.State × D.Result o of a specification D with [D.HasStepFn f].

theorem Cslib.DataStructure.StateTransitionSpec.step_iff_stepFn (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (o : D.Op) (s' : D.State) (a : D.Result o) : D.step s o s' a ↔ (s', a) = D.stepFn s o

theorem Cslib.DataStructure.StateTransitionSpec.step_stepFn (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (o : D.Op) : D.step s o (D.stepFn s o).1 (D.stepFn s o).2

instance Cslib.DataStructure.StateTransitionSpec.instTotalOfHasStepFn (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] : D.Total

instance Cslib.DataStructure.StateTransitionSpec.instDeterministicOfHasStepFn (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] : D.Deterministic

def Cslib.DataStructure.StateTransitionSpec.toFLTS (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] : FLTS D.State D.Op

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

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.toFLTS_tr (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (o : D.Op) : D.toFLTS.tr s o = (D.stepFn s o).1

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

theorem Cslib.DataStructure.StateTransitionSpec.toLTS_tr_iff_toFLTS (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s s' : D.State) (o : D.Op) (a : D.Result o) : D.toLTS.Tr s ⟨o, a⟩ s' ↔ s' = D.toFLTS.tr s o ∧ a = (D.stepFn s o).2

Transitions in D.toLTS agree with D.toFLTS on states and (D.stepFn s o).2 on observations.

def Cslib.DataStructure.StateTransitionSpec.run (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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.DataStructure.StateTransitionSpec.ValidHistory (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) : List D.Op → Prop

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

def Cslib.DataStructure.StateTransitionSpec.totalCost (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (charge : D.State → D.Op → ℕ) (s : D.State) : List D.Op → ℕ

State-dependent charges summed along the abstract execution.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.run_nil (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) : D.run s [] = (s, [])

Running the empty history keeps the state and observes nothing.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.run_cons (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (o : D.Op) (os : List D.Op) : D.run s (o :: os) = ((D.run (D.stepFn s o).1 os).1, ⟨o, (D.stepFn s o).2⟩ :: (D.run (D.stepFn s o).1 os).2)

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

theorem Cslib.DataStructure.StateTransitionSpec.fst_run_eq_toFLTS_mtr (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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.

theorem Cslib.DataStructure.StateTransitionSpec.toLTS_mtr_run (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (os : List D.Op) : D.toLTS.MTr s (D.run s os).2 (D.toFLTS.mtr s os)

Multi-step execution D.run produces a valid multi-step trace in D.toLTS ending at D.toFLTS.mtr s os.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.validHistory_nil (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) : D.ValidHistory s [] ↔ True

The empty history is admissible in every state.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.validHistory_cons (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (o : D.Op) (os : List D.Op) : D.ValidHistory s (o :: os) ↔ D.valid s o ∧ D.ValidHistory (D.stepFn 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.DataStructure.StateTransitionSpec.validHistory_of_forall_valid (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (h : ∀ (s : D.State) (o : D.Op), D.valid s o) (s : D.State) (os : List D.Op) : D.ValidHistory s os

On a specification where every operation is valid in every state, every history is admissible.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.totalCost_nil (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (charge : D.State → D.Op → ℕ) (s : D.State) : D.totalCost charge s [] = 0

The empty history costs nothing.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.totalCost_cons (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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.stepFn 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.DataStructure.StateTransitionSpec.run_append (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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.DataStructure.StateTransitionSpec.totalCost_append (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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. The element type D.Op is not indexed, so simp also uses this for a concrete specification such as Memory.spec w, whose Op reduces.

theorem Cslib.DataStructure.StateTransitionSpec.totalCost_le_length_mul (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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.DataStructure.StateTransitionSpec.totalCost_const (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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.DataStructure.StateTransitionSpec.totalCost_one (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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.

def Cslib.DataStructure.StateTransitionSpec.runClient (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) : D.Client α → α × D.State × List D.Op

Interpret a client mathematically, retaining its chosen operation history.

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.clientResult (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (p : D.Client α) : α

Value returned by a deterministic client run D.runClient s p.

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.clientState (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (p : D.Client α) : D.State

Final abstract state reached by a deterministic client run D.runClient s p.

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.clientHistory (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (p : D.Client α) : List D.Op

Operation history selected by a deterministic client run D.runClient s p.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.runClient_pure (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : 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.DataStructure.StateTransitionSpec.runClient_pure' (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : 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.DataStructure.StateTransitionSpec.runClient_lift (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (o : D.Op) : D.runClient s (PFunctor.FreeM.lift o) = ((D.stepFn s o).2, (D.stepFn s o).1, [o])

Interpreting a single lifted operation steps the specification once.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.runClient_liftBind (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) : D.runClient s (PFunctor.FreeM.liftBind o k) = match D.runClient (D.stepFn s o).1 (k (D.stepFn s o).2) with | (v, s', os) => (v, s', o :: os)

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

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.runClient_lift_bind (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) : D.runClient s ((PFunctor.FreeM.lift o).bind k) = match D.runClient (D.stepFn s o).1 (k (D.stepFn s o).2) with | (v, s', os) => (v, s', o :: os)

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

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.runClient_lift_bind' (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type w} (s : D.State) (o : D.Op) (k : D.Result o → D.Client α) : D.runClient s (PFunctor.FreeM.lift o >>= k) = match D.runClient (D.stepFn s o).1 (k (D.stepFn s o).2) with | (v, s', os) => (v, s', o :: os)

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

theorem Cslib.DataStructure.StateTransitionSpec.run_runClient (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (p : D.Client α) (s : D.State) : (D.run s (D.clientHistory s p)).1 = D.clientState s p

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

theorem Cslib.DataStructure.StateTransitionSpec.validHistory_append {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (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. The element type D.Op is not indexed, as in totalCost_append.

theorem Cslib.DataStructure.StateTransitionSpec.runClient_bind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α β : Type y} (p : D.Client α) (k : α → D.Client β) (s : D.State) : D.runClient s (PFunctor.FreeM.bind p k) = match D.runClient s p with | (v₁, s₁, os₁) => match D.runClient s₁ (k v₁) with | (v₂, s₂, os₂) => (v₂, s₂, os₁ ++ os₂)

Sequential interpretation concatenates the histories actually selected by the client.

theorem Cslib.DataStructure.StateTransitionSpec.clientResult_bind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α β : Type y} (p : D.Client α) (k : α → D.Client β) (s : D.State) : D.clientResult s (p >>= k) = D.clientResult (D.clientState s p) (k (D.clientResult s p))

A sequential client answers as its continuation, run from where the first client stopped.

theorem Cslib.DataStructure.StateTransitionSpec.clientState_bind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α β : Type y} (p : D.Client α) (k : α → D.Client β) (s : D.State) : D.clientState s (p >>= k) = D.clientState (D.clientState s p) (k (D.clientResult s p))

A sequential client stops where its continuation, run from where the first client stopped, stops.

theorem Cslib.DataStructure.StateTransitionSpec.clientHistory_bind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α β : Type y} (p : D.Client α) (k : α → D.Client β) (s : D.State) : D.clientHistory s (p >>= k) = D.clientHistory s p ++ D.clientHistory (D.clientState s p) (k (D.clientResult s p))

The history of a sequential client is the first client's history, then its continuation's.

theorem Cslib.DataStructure.StateTransitionSpec.clientResult_pure {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (a : α) : D.clientResult s (pure a) = a

A client that only returns a value answers with it.

theorem Cslib.DataStructure.StateTransitionSpec.clientState_pure {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (a : α) : D.clientState s (pure a) = s

A client that only returns a value leaves the state unchanged.

theorem Cslib.DataStructure.StateTransitionSpec.clientHistory_pure {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (a : α) : D.clientHistory s (pure a) = []

A client that only returns a value issues no operation.

clientState and clientHistory unfold to a match on D.runClient s p. Under its metavariables simp cannot reduce that match, so it would index clientState_bind and clientHistory_bind under a key that no goal has; in a goal it sees (D.runClient s p).2.1. The following restatements have that form, and put the simp set client_simps in the normal form of clientState and clientHistory.

theorem Cslib.DataStructure.StateTransitionSpec.fst_snd_runClient_bind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α β : Type y} (p : D.Client α) (k : α → D.Client β) (s : D.State) : (D.runClient s (p >>= k)).2.1 = D.clientState (D.clientState s p) (k (D.clientResult s p))

clientState_bind, stated in the form that simp indexes.

theorem Cslib.DataStructure.StateTransitionSpec.snd_snd_runClient_bind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α β : Type y} (p : D.Client α) (k : α → D.Client β) (s : D.State) : (D.runClient s (p >>= k)).2.2 = D.clientHistory s p ++ D.clientHistory (D.clientState s p) (k (D.clientResult s p))

clientHistory_bind, stated in the form that simp indexes.

theorem Cslib.DataStructure.StateTransitionSpec.fst_snd_runClient_pure {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (a : α) : (D.runClient s (pure a)).2.1 = s

clientState_pure, stated in the form that simp indexes.

theorem Cslib.DataStructure.StateTransitionSpec.snd_snd_runClient_pure {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (a : α) : (D.runClient s (pure a)).2.2 = []

clientHistory_pure, stated in the form that simp indexes.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.validOpSeq_iff_validHistory {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (ops : List D.Op) : D.ValidOpSeq s ops ↔ D.ValidHistory s ops

Under [D.HasStepFn f], demonic operation-sequence admissibility ValidOpSeq coincides with D.ValidHistory.

def Cslib.DataStructure.StateTransitionSpec.canonicalTranscript (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) : List D.Op → D.Transcript

The unique canonical transcript determined by a specification D with [D.HasStepFn f] on an operation list os from state s.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.canonicalTranscript_nil {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) : D.canonicalTranscript s [] = []

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.canonicalTranscript_cons {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (o : D.Op) (os : List D.Op) : D.canonicalTranscript s (o :: os) = { op := o, result := (D.stepFn s o).2, nextState := (D.stepFn s o).1 } :: D.canonicalTranscript (D.stepFn s o).1 os

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.canonicalTranscript_ops {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (os : List D.Op) : (D.canonicalTranscript s os).ops = os

The underlying operation list of D.canonicalTranscript s os is os.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.canonicalTranscript_labels {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (os : List D.Op) : (D.canonicalTranscript s os).labels = (D.run s os).2

The labels of D.canonicalTranscript s os coincide with (D.run s os).2.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_canonicalTranscript {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (charge : D.State → D.Op → ℕ) (s : D.State) (os : List D.Op) : D.totalCostTranscript charge s (D.canonicalTranscript s os) = D.totalCost charge s os

totalCostTranscript along D.canonicalTranscript s os equals D.totalCost charge s os.

theorem Cslib.DataStructure.StateTransitionSpec.validTranscript_canonicalTranscript {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {s : D.State} {os : List D.Op} (hv : D.ValidHistory s os) : D.ValidTranscript s (D.canonicalTranscript s os) (D.run s os).1

Every admissible operation history executes canonically to (D.run s os).1.

theorem Cslib.DataStructure.StateTransitionSpec.validTranscript_iff_run {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (tr : D.Transcript) (s' : D.State) : D.ValidTranscript s tr s' ↔ D.ValidHistory s tr.ops ∧ s' = (D.run s tr.ops).1 ∧ tr = D.canonicalTranscript s tr.ops

Under [D.HasStepFn f], ValidTranscript s tr s' collapses uniquely to D.ValidHistory s tr.ops, s' = (D.run s tr.ops).1, and tr = D.canonicalTranscript s tr.ops.

theorem Cslib.DataStructure.StateTransitionSpec.demonicValid_iff_validHistory_runClient {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (p : D.Client α) : D.DemonicValid s p ↔ D.ValidHistory s (D.clientHistory s p)

Under [D.HasStepFn f], demonic client admissibility DemonicValid s p is equivalent to D.ValidHistory s (D.clientHistory s p).

theorem Cslib.DataStructure.StateTransitionSpec.clientRun_canonical {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (p : D.Client α) (hv : D.ValidHistory s (D.clientHistory s p)) : D.ClientRun s p (D.clientResult s p) (D.clientState s p) (D.canonicalTranscript s (D.clientHistory s p))

Every client with an admissible deterministic history executes canonically.

theorem Cslib.DataStructure.StateTransitionSpec.clientRun_iff_runClient {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type y} (s : D.State) (p : D.Client α) (v : α) (s' : D.State) (tr : D.Transcript) : D.ClientRun s p v s' tr ↔ D.ValidHistory s (D.clientHistory s p) ∧ v = D.clientResult s p ∧ s' = D.clientState s p ∧ tr = D.canonicalTranscript s (D.clientHistory s p)

Under [D.HasStepFn f], ClientRun collapses uniquely to D.clientResult, D.clientState, D.clientHistory, and D.ValidHistory.

def Cslib.DataStructure.eval {α : Type y} (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (p : D.Client α) (s : D.State) : α × D.State

Observe results and state without displaying the operation history.

@[simp]

theorem Cslib.DataStructure.eval_pure {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : 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.DataStructure.eval_pure' {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : 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.DataStructure.eval_lift {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s : D.State) (o : D.Op) : eval D (PFunctor.FreeM.lift o) s = ((D.stepFn s o).2, (D.stepFn s o).1)

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

@[simp]

theorem Cslib.DataStructure.eval_liftBind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : 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.stepFn s o).2) (D.stepFn s o).1

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

@[simp]

theorem Cslib.DataStructure.eval_lift_bind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : 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.stepFn s o).2) (D.stepFn s o).1

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

@[simp]

theorem Cslib.DataStructure.eval_lift_bind' {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : 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.stepFn s o).2) (D.stepFn s o).1

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

theorem Cslib.DataStructure.eval_bind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α β : 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.DataStructure.eval_eq_liftM {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type u} (p : D.Client α) (s : D.State) : StateT.run (PFunctor.FreeM.liftM (fun (o : D.signature.A) (s : D.State) => ((D.stepFn s o).2, (D.stepFn 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.DataStructure.product (D E : StateTransitionSpec) : StateTransitionSpec

Two independent abstract components. A backend must separately justify their independence. The answer types are Sum.elim D.Result E.Result, so the signature of a product depends only on the signatures of its components: clients of product D E are clients of product D' E' when D, D' and E, E' differ only in their states' admissibility.

@[simp]

theorem Cslib.DataStructure.product_step_inl (D E : StateTransitionSpec) (s s' : D.State × E.State) (o : D.Op) (a : D.Result o) : (product D E).step s (Sum.inl o) s' a ↔ D.step s.1 o s'.1 a ∧ s'.2 = s.2

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

@[simp]

theorem Cslib.DataStructure.product_step_inr (D E : StateTransitionSpec) (s s' : D.State × E.State) (o : E.Op) (a : E.Result o) : (product D E).step s (Sum.inr o) s' a ↔ s'.1 = s.1 ∧ E.step s.2 o s'.2 a

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

@[simp]

theorem Cslib.DataStructure.product_valid_inl (D E : StateTransitionSpec) (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.DataStructure.product_valid_inr (D E : StateTransitionSpec) (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.

Instances on products

product is an abbrev, so an instance stated on product D E would be indexed by the unfolded structure, whose state type is the projection D.State × E.State. A nested product such as product (product D E) F has state type (D.State × E.State) × F.State after unfolding, which that index does not match. The product instances therefore index their specification with no_index, and products of any depth find them by unification.

instance Cslib.DataStructure.instTotalProduct (D E : StateTransitionSpec) [D.Total] [E.Total] : (product D E).Total

Product of two total specifications is total.

instance Cslib.DataStructure.instDeterministicProduct (D E : StateTransitionSpec) [D.Deterministic] [E.Deterministic] : (product D E).Deterministic

Product of two deterministic specifications is deterministic.

@[reducible, inline]

abbrev Cslib.DataStructure.productStepFn (D E : StateTransitionSpec) (fD : D.State → (o : D.Op) → D.State × D.Result o) (fE : E.State → (o : E.Op) → E.State × E.Result o) (s : (product D E).State) (o : (product D E).Op) : (product D E).State × (product D E).Result o

The canonical transition function of a product of two specifications with transition functions fD and fE.

instance Cslib.DataStructure.instHasStepFnProduct (D E : StateTransitionSpec) {fD : D.State → (o : D.Op) → D.State × D.Result o} {fE : E.State → (o : E.Op) → E.State × E.Result o} [D.HasStepFn fD] [E.HasStepFn fE] : (product D E).HasStepFn (productStepFn D E fD fE)

A product of specifications with HasStepFn has HasStepFn with the componentwise transition function, at any nesting depth.

instance Cslib.DataStructure.instHasStepFnProductOfFn {State₁ : Type u} {Op₁ : Type v} {Result₁ : Op₁ → Type w} {State₂ : Type u} {Op₂ : Type v} {Result₂ : Op₂ → Type w} (fD : State₁ → (o : Op₁) → State₁ × Result₁ o) (validD : State₁ → Op₁ → Prop) (fE : State₂ → (o : Op₂) → State₂ × Result₂ o) (validE : State₂ → Op₂ → Prop) : (product (StateTransitionSpec.ofFn fD validD) (StateTransitionSpec.ofFn fE validE)).HasStepFn (productStepFn (StateTransitionSpec.ofFn fD validD) (StateTransitionSpec.ofFn fE validE) fD fE)

The product of two ofFn specifications, with their transition functions named. It is tried before instHasStepFnProduct, so such products keep this form of the transition function.

@[simp]

theorem Cslib.DataStructure.product_stepFn_inl (D E : StateTransitionSpec) {fD : D.State → (o : D.Op) → D.State × D.Result o} {fE : E.State → (o : E.Op) → E.State × E.Result o} [D.HasStepFn fD] [E.HasStepFn fE] (s : D.State × E.State) (o : D.Op) : (product D E).stepFn s (Sum.inl o) = (((D.stepFn s.1 o).1, s.2), (D.stepFn s.1 o).2)

@[simp]

theorem Cslib.DataStructure.product_stepFn_inr (D E : StateTransitionSpec) {fD : D.State → (o : D.Op) → D.State × D.Result o} {fE : E.State → (o : E.Op) → E.State × E.Result o} [D.HasStepFn fD] [E.HasStepFn fE] (s : D.State × E.State) (o : E.Op) : (product D E).stepFn s (Sum.inr o) = ((s.1, (E.stepFn s.2 o).1), (E.stepFn s.2 o).2)