Store, Adapter, Replay, Bridge

Four small modules carrying the framework's generic guarantees.

Store

Encapp/Store.lean — the store as an effect interpreter.

TEA leaves the interpreter of Cmd abstract. Encapp makes it first-class.

structure World (H : Type) where
  empty : H
  run   : Cmd → H → H × List Event     -- interpret one command
  log   : H → List Event               -- the observable committed log

The spec

def emulator : World (List Event) where
  empty := []
  run c h := match c with
    | .submit e => (h ++ [e], [e])
    | .none     => (h, [])
  log h := h

The emulator's state is the log. Every real adapter is judged against it.

Running a sequence

def World.runAll (w : World H) : List Cmd → H → H × List Event

Written without let so the recursion equations project cleanly in proofs.

structure Refines (w : World H) (R : H → List Event → Prop) : Prop where
  start : R w.empty emulator.empty
  step  : ∀ c h s, R h s → R (w.run c h).1 (emulator.run c s).1
                          ∧ (w.run c h).2 = (emulator.run c s).2
  obs   : ∀ h s, R h s → w.log h = emulator.log s

Three obligations a real backend must discharge: start related, stay related while emitting identical events, and observe identically.

The theorems

theorem refines_sound (w : World H) (R) (hr : Refines w R) :
    ∀ cs h s, R h s →
      (w.runAll cs h).2 = (emulator.runAll cs s).2
      ∧ R (w.runAll cs h).1 (emulator.runAll cs s).1
 
theorem refines_log (w : World H) (R) (hr : Refines w R) (cs : List Cmd) :
    w.log (w.runAll cs w.empty).1 = emulator.log (emulator.runAll cs emulator.empty).1

For any command sequence, a refining world emits byte-identical event traces and ends with the same observable log. An app cannot detect which backend ran it.

The proof is a closed simulation argument by induction on the command list — the pure form of the "in-memory mode ≡ real backend mode" claim that frameworks usually assert and never discharge.

Adapter

Encapp/Adapter.lean — a witness that refinement is not vacuous.

Without this module, Refines and refines_sound are proven but empty: only the emulator trivially refines the emulator.

def reversedWorld : World (List Event) where
  empty := []
  run c h := match c with
    | .submit e => (e :: h, [e])     -- O(1) cons, like a real journal backend
    | .none     => (h, [])
  log h := h.reverse
 
def reversedRel (h s : List Event) : Prop := h.reverse = s
 
theorem reversedWorld_refines : Refines reversedWorld reversedRel

The internal states are never literally equal — one is the reverse of the other — so the refinement is genuine rather than an identity in disguise. The corollary then costs nothing:

theorem reversedWorld_same_log (cs : List Cmd) :
    reversedWorld.log (reversedWorld.runAll cs reversedWorld.empty).1
      = emulator.log (emulator.runAll cs emulator.empty).1

This is the template a real adapter follows: pick your representation, exhibit the relation to the emulator's log, discharge start / step / obs.

Replay

Encapp/Replay.lean — event-sourced state.

def applyEv (s : List Event) (e : Event) : List Event :=
  if s.any (fun x => x.id == e.id) then s else s ++ [e]
 
theorem applyEv_idem (s : List Event) (e : Event) :
    applyEv (applyEv s e) e = applyEv s e

Re-delivering an event is a no-op. Networks duplicate and optimistic local writes race the server echo; this is the law that makes both collapse to one row.

def replayLog (init log : List Event) : List Event := log.foldl applyEv init
 
theorem replayLog_append (init l₁ l₂ : List Event) :
    replayLog init (l₁ ++ l₂) = replayLog (replayLog init l₁) l₂

Reload equivalence for the committed event log — the counterpart of App.ofMsgLog_append for the message log.

Bridge

Encapp/Bridge.lean — the interpreter as a Foundation World.

Connects the proven keystone (Foundation.Layer.mono) to the actual Encapp interpreter, so the store-vs-emulator result is discharged by the keystone rather than re-proved.

def reflWorld (a : ReflApp β) : World Doc (String × Atom) Doc
def emuWorld : World Doc (String × Atom) Doc := reflWorld EmuGen.emuApp

The real reflStep interpreter is a Foundation.World: state is a Doc, input is a tagged message, output is the rendered Doc.

Two store representations that refine:

def storeSpec : World Nat SCmd SEvt          -- state is just a sequence number
def storeLog  : World (List SCmd) SCmd SEvt  -- state is the actual append-log
 
theorem store_ok : Refines storeLog storeSpec

A UI layer over the store, lifted for free:

def postLayer (table : String) : Layer Doc (String × Atom) Doc SCmd SEvt
 
theorem ui_over_store_ok :
    Refines ((postLayer "feed").on storeLog) ((postLayer "feed").on storeSpec) :=
  Refines.layer (postLayer "feed") store_ok
 
theorem ui_over_store_observable (msgs : List (String × Atom)) :
    ((postLayer "feed").on storeLog).trace msgs
      = ((postLayer "feed").on storeSpec).trace msgs

The payoff, on real Encapp types: the deployed app renders Docs identical to the emulator's, for any message stream — one line, from Layer.mono.

Foundation.Layer.mono is pinned by test/axiom-audit.mjs to exactly zero axioms.