Native executions and semantic implementations

A backend chooses concrete states and native execution evidence. Implementations assert existence of executions and angelic step correctness of every supplied terminating execution, independently of cost:

• total: every represented state and admissible operation admits a native execution;
• correct: every native execution from a represented state on an admissible operation realizes some permitted abstract post-state s' with D.step s o s' a ∧ rep s' c'.

For deterministic specifications ([D.HasStepFn f]), StateTransitionImpl.ofFn constructs a StateTransitionImpl from a functional step-correctness proof (a = (D.stepFn s o).2 ∧ rep (D.stepFn s o).1 c'), and StateTransitionImpl.exists_executes and StateTransitionImpl.correct_client recover the functional runClient characterizations directly.

Main definitions

• Execution: one native operation with typed answer and execution evidence.
• Executes: sequential adaptive execution, retaining native evidence in order.
• StateTransitionImpl: angelic representation simulation and existence without resource assumptions.
• StateTransitionImpl.ofFn: constructor for deterministic specifications ([D.HasStepFn f]).

Main results

• StateTransitionImpl.correct_demonic, StateTransitionImpl.exists_demonic: soundness and existence of native client executions under D.DemonicValid.
• StateTransitionImpl.exists_executes, StateTransitionImpl.correct_client: deterministic specializations for [D.HasStepFn f].
• executes_bind_iff: sequential execution splits exactly at the intermediate state.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, Chapter 17.

@[reducible, inline]

abbrev Cslib.DataStructure.Execution (S : PFunctor.{v, w}) (C Trace : Type x) : Type (max (max x v) w)

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

inductive Cslib.DataStructure.Executes {S : PFunctor.{v, w}} {C τ : Type x} {α : Type y} (exec : Execution S C τ) : S.FreeM α → C → α → C → List τ → Prop

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

• pure {S : PFunctor.{v, w}} {C τ : Type x} {α : Type y} {exec : Execution S C τ} (a : α) (c : C) : Executes exec (PFunctor.FreeM.pure a) c a c []
• call {S : PFunctor.{v, w}} {C τ : Type x} {α : Type y} {exec : Execution S C τ} {o : S.A} {k : S.B o → S.FreeM α} {c : C} {a : S.B 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.DataStructure.StateTransitionImpl (D : StateTransitionSpec) {C τ : Type x} (exec : Execution D.signature C τ) : Type (max u x)

Angelic semantic implementation of a relational specification D : StateTransitionSpec:

• total: every represented state and admissible operation admits a native execution;
• correct: every native execution from a represented state on an admissible operation realizes some permitted abstract post-state s' with D.step s o s' a ∧ rep s' c'.

• 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.signature.B o) (c' : C) (trace : τ), exec c o a c' trace

  Existence of a native execution for every represented state and admissible operation.

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

  Angelic step correctness: every native execution realizes some permitted abstract step.

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionImpl.ofFn {D : StateTransitionSpec} {C τ : Type x} {exec : Execution D.signature C τ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (rep : D.State → C → Prop) (total : ∀ {s : D.State} {c : C} (o : D.Op), rep s c → D.valid s o → ∃ (a : D.signature.B o) (c' : C) (trace : τ), exec c o a c' trace) (correct : ∀ {s : D.State} {c : C} {o : D.Op} {a : D.signature.B o} {c' : C} {trace : τ}, rep s c → D.valid s o → exec c o a c' trace → a = (D.stepFn s o).2 ∧ rep (D.stepFn s o).1 c') : StateTransitionImpl D exec

Construct a StateTransitionImpl for a deterministic specification ([D.HasStepFn f]) from a functional step-correctness proof.

theorem Cslib.DataStructure.StateTransitionImpl.correct_demonic {D : StateTransitionSpec} {C τ : Type x} {α : Type y} {exec : Execution D.signature C τ} (R : StateTransitionImpl D exec) {p : D.Client α} {s : D.State} {c c' : C} {a : α} {traces : List τ} (hr : R.rep s c) (hv : D.DemonicValid s p) (he : Executes exec p c a c' traces) : ∃ (s' : D.State) (tr : D.Transcript), D.ClientRun s p a s' tr ∧ R.rep s' c' ∧ traces.length = List.length tr

From related states, every native execution of a demonically admissible client realizes a valid ClientRun ending in a related state.

theorem Cslib.DataStructure.StateTransitionImpl.exists_demonic {D : StateTransitionSpec} {C τ : Type x} {α : Type y} {exec : Execution D.signature C τ} (R : StateTransitionImpl D exec) (p : D.Client α) {s : D.State} {c : C} (hr : R.rep s c) (hv : D.DemonicValid s p) : ∃ (a : α) (c' : C) (traces : List τ) (s' : D.State) (tr : D.Transcript), Executes exec p c a c' traces ∧ D.ClientRun s p a s' tr ∧ R.rep s' c' ∧ traces.length = List.length tr

From related states, every demonically admissible client admits a native execution realizing a valid ClientRun ending in a related state.

theorem Cslib.DataStructure.StateTransitionImpl.correct_ofFn {D : StateTransitionSpec} {C τ : Type x} {exec : Execution D.signature C τ} (R : StateTransitionImpl D exec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {s : D.State} {c c' : C} {o : D.Op} {a : D.Result o} {trace : τ} (hr : R.rep s c) (hv : D.valid s o) (he : exec c o a c' trace) : a = (D.stepFn s o).2 ∧ R.rep (D.stepFn s o).1 c'

On a deterministic specification ([D.HasStepFn f]), every native step returns (D.stepFn s o).2 and reaches (D.stepFn s o).1.

theorem Cslib.DataStructure.StateTransitionImpl.exists_executes {D : StateTransitionSpec} {C τ : Type x} {α : Type y} {exec : Execution D.signature C τ} (R : StateTransitionImpl D exec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (p : D.Client α) {s : D.State} {c : C} (hr : R.rep s c) (hv : D.ValidHistory s (D.clientHistory s p)) : ∃ (c' : C) (traces : List τ), Executes exec p c (D.clientResult s p) c' traces ∧ R.rep (D.clientState s p) 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.DataStructure.StateTransitionImpl.correct_client {D : StateTransitionSpec} {C τ : Type x} {α : Type y} {exec : Execution D.signature C τ} (R : StateTransitionImpl D exec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {p : D.Client α} {s : D.State} {c c' : C} {a : α} {traces : List τ} (hr : R.rep s c) (hv : D.ValidHistory s (D.clientHistory s p)) (he : Executes exec p c a c' traces) : a = D.clientResult s p ∧ R.rep (D.clientState s p) 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.DataStructure.executes_bind_iff {S : PFunctor.{v, w}} {C τ : Type x} {α β : Type y} (exec : Execution S C τ) (p : S.FreeM α) (k : α → S.FreeM β) {c c' : C} {b : β} {ts : List τ} : Executes exec (p.bind 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.