Encapp.Core

The spine: pure TEA with effects as data, and no store or runtime baked in. The merge with the store happens in Encapp.Store.

Event

structure Event where
  id   : String
  data : String
  deriving DecidableEq, Inhabited

The atomic, replayable fact. id gives identity for dedup — it is the basis of idempotent replay. data is an opaque payload.

Cmd

inductive Cmd where
  | submit : Event → Cmd     -- append a fact to the store
  | none   : Cmd             -- no effect
  deriving DecidableEq, Inhabited

The effect algebra. Nothing here performs I/O: an app cannot do anything, it can only describe a store write. What executes the description is chosen downstream and is related to the spec by proof.

App

structure App (Model Msg : Type) where
  init   : Model
  update : Msg → Model → Model × List Cmd
  view   : Model → View Msg

The Elm Architecture, abstract and polymorphic. update is a pure Mealy transition emitting effects-as-data; view is a pure projection into the closed view vocabulary.

This type has function fields, so it cannot be serialized or compiled. The compilable image is ReflApp, and an app ties the two with a theorem — see The app model.

App.ofMsgLog

def App.ofMsgLog (a : App Model Msg) (log : List Msg) : Model :=
  log.foldl (fun m msg => (a.update msg m).1) a.init

The event-sourcing view of state: the model is a fold of update over a message log from init.

Reload equivalence

App.ofMsgLog_append

theorem App.ofMsgLog_append (a : App Model Msg) (l₁ l₂ : List Msg) :
    a.ofMsgLog (l₁ ++ l₂)
      = l₂.foldl (fun m msg => (a.update msg m).1) (a.ofMsgLog l₁)

Replaying l₁ ++ l₂ from init equals replaying l₂ from the snapshot reached after l₁.

So persisting a snapshot and resuming is observationally identical to a full replay — the property that lets a node checkpoint without changing meaning. It is proven generically, once, for every app on the framework.

The event-log analogue of the same law is replayLog_append; the two together cover both the message log and the committed event log.