Native executions and semantic realizations

A backend chooses concrete states and native execution evidence. Realizations assert existence of executions and correctness of every supplied terminating execution, independently of cost. For nondeterministic backends existence is not demonic termination.

Main definitions

• Execution: one native operation with typed answer and execution evidence.
• Executes: sequential adaptive execution, retaining native evidence in order.
• Realization: representation simulation and existence without resource assumptions.

Main results

• Realization.run: admissible clients have correct executions.
• Realization.correct_client: every supplied client execution has the specified result.
• executes_bind_iff: sequential execution splits exactly at the intermediate state.

@[reducible, inline]

abbrev Cslib.Stateful.Execution (D : Spec) (C Trace : Type x) : Type (max (max x v) w)

A backend chooses its own execution evidence, independently of a resource measure.

inductive Cslib.Stateful.Executes {D : Spec} {C τ : Type x} {α : Type y} (exec : Execution D C τ) : D.Client α → C → α → C → List τ → Prop

Clients collect native execution evidence in call order; no costs occur in this semantics.

• pure {D : Spec} {C τ : Type x} {α : Type y} {exec : Execution D C τ} (a : α) (c : C) : Executes exec (PFunctor.FreeM.pure a) c a c []
• call {D : Spec} {C τ : Type x} {α : Type y} {exec : Execution D C τ} {o : D.Op} {k : D.signature.B o → D.signature.FreeM α} {c : C} {a : D.Result o} {c' : C} {trace : τ} {b : α} {c'' : C} {traces : List τ} : exec c o a c' trace → Executes exec (k a) c' b c'' traces → Executes exec (PFunctor.FreeM.liftBind o k) c b c'' (trace :: traces)

structure Cslib.Stateful.Realization (D : Spec) {C τ : Type x} (exec : Execution D C τ) : Type (max u x)

Functional correctness and existence of executions, without a resource claim. For nondeterministic backends this is not a demonic termination assertion.

• rep : D.State → C → Prop

  The relation between mathematical states and concrete backend states.

• total {s : D.State} {c : C} (o : D.Op) : self.rep s c → D.valid s o → ∃ (a : D.Result o) (c' : C) (trace : τ), exec c o a c' trace
• correct {s : D.State} {c : C} {o : D.Op} {a : D.Result o} {c' : C} {trace : τ} : self.rep s c → D.valid s o → exec c o a c' trace → a = (D.step s o).2 ∧ self.rep (D.step s o).1 c'

theorem Cslib.Stateful.Realization.run {D : Spec} {C τ : Type x} {α : Type y} {exec : Execution D C τ} (R : Realization D exec) (p : D.Client α) {s : D.State} {c : C} (hr : R.rep s c) (hv : D.ValidHistory s (D.runClient s p).2.2) : ∃ (c' : C) (traces : List τ), Executes exec p c (D.runClient s p).1 c' traces ∧ R.rep (D.runClient s p).2.1 c'

From related states, a client whose history is admissible has a native execution that returns the specified result and ends in a state related to the specified final state.

theorem Cslib.Stateful.Realization.correct_client {D : Spec} {C τ : Type x} {α : Type y} {exec : Execution D C τ} (R : Realization D exec) {p : D.Client α} {s : D.State} {c c' : C} {a : α} {traces : List τ} (hr : R.rep s c) (hv : D.ValidHistory s (D.runClient s p).2.2) (he : Executes exec p c a c' traces) : a = (D.runClient s p).1 ∧ R.rep (D.runClient s p).2.1 c'

From related states, every native execution of a client whose history is admissible returns the specified result and ends in a state related to the specified final state.

theorem Cslib.Stateful.executes_bind_iff {D : Spec} {C τ : Type x} {α β : Type y} (exec : Execution D C τ) (p : D.Client α) (k : α → D.Client β) {c c' : C} {b : β} {ts : List τ} : Executes exec (PFunctor.FreeM.bind p k) c b c' ts ↔ ∃ (a : α) (mid : C) (front : List τ) (back : List τ), Executes exec p c a mid front ∧ Executes exec (k a) mid b c' back ∧ ts = front ++ back

Execution of a sequential composition splits its native trace at the call boundary.