Compositional semantic implementations

A module implements one interface using operations of another. Linking uses the upstream free-monad interpreter. Behavior proofs neither choose a computational model nor assign costs. Realization composes representation relations and hides intermediate states existentially. Linking uses the upstream interpreter's common universe for operation answers and client results. Native execution itself permits an independent universe for client results.

Main definitions

• Methods: operation bodies over a lower interface.
• Module: admissibility and representation simulation for those bodies.
• link: substitute lower method bodies into an adaptive client.

Main results

• Module.realize: implement a module with any realization of its lower interface.
• link_exec, link_exec_decompose: exact correspondence of chunked and flattened executions.

@[reducible, inline]

abbrev Cslib.Stateful.Methods (D E : Spec) : Type (max v w)

Interface methods are programs over another interface.

def Cslib.Stateful.link {D E : Spec} {α : Type w} (methods : Methods D E) (p : D.Client α) : E.Client α

Substitution reuses upstream free-monad interpretation.

structure Cslib.Stateful.Module (D E : Spec) : Type (max (max u v) w)

Purely semantic module correctness; neither an execution model nor a cost appears.

• methods : Methods D E

  Bodies implementing the upper interface using lower-interface calls.

• rep : D.State → E.State → Prop

  The relation between upper and lower mathematical states.

• valid {s : D.State} {e : E.State} (o : D.Op) : self.rep s e → D.valid s o → E.ValidHistory e (E.runClient e (self.methods o)).2.2
• correct {s : D.State} {e : E.State} (o : D.Op) : self.rep s e → D.valid s o → (E.runClient e (self.methods o)).1 = (D.step s o).2 ∧ self.rep (D.step s o).1 (E.runClient e (self.methods o)).2.1

def Cslib.Stateful.Module.realize {D E : Spec} {C τ : Type x} (M : Module D E) {exec : Execution E C τ} (R : Realization E exec) : Realization D fun (c : C) (o : D.Op) (a : D.Result o) (c' : C) (ts : List τ) => Executes exec (M.methods o) c a c' ts

Module realization hides the intermediate representation and composes at any backend.

theorem Cslib.Stateful.link_exec {D E : Spec} {C τ : Type x} {α : Type w} (methods : Methods D E) (exec : Execution E C τ) {p : D.Client α} {c c' : C} {a : α} {chunks : List (List τ)} (he : Executes (fun (x : C) (o : D.Op) (a : D.Result o) (y : C) (ts : List τ) => Executes exec (methods o) x a y ts) p c a c' chunks) : Executes exec (link methods p) c a c' chunks.flatten

Linking expands every module call and preserves the complete flattened backend trace.

theorem Cslib.Stateful.link_exec_decompose {D E : Spec} {C τ : Type x} {α : Type w} (methods : Methods D E) (exec : Execution E C τ) {p : D.Client α} {c c' : C} {a : α} {ts : List τ} (he : Executes exec (link methods p) c a c' ts) : ∃ (chunks : List (List τ)), Executes (fun (x : C) (o : D.Op) (a : D.Result o) (y : C) (trace : List τ) => Executes exec (methods o) x a y trace) p c a c' chunks ∧ ts = chunks.flatten

Every flattened execution also decomposes into executions of its individual method calls.