Skip to content
Logo

Glossary of terms

This glossary defines the core vocabulary of the Encapp framework. Each term lives in a specific module and is grounded in the actual source — not aspirational descriptions. If a definition here cannot be verified by reading the referenced file, it is marketing and should be an issue.

Adapter

Module: Encapp/Adapter.lean

A concrete store backend that provably refines the emulator. The framework does not dictate how state is stored — it only requires a proof that the adapter's observable behavior equals the emulator's. The reversedWorld example stores the committed log reversed internally (like an append-at-head journal), then reverses on read, and discharges Refines to prove that this representationally different backend is nonetheless indistinguishable from the spec. A real enc-flow adapter follows this template: pick your state representation, exhibit the relation to the emulator, and prove start / step / obs hold. See Refinement.

Atom

Module: Encapp/Doc.lean

A typed leaf value, the atomic unit of app state. An Atom is one of four constructors: str String, int Int, bool Bool, or null. Every scalar field and row field in a Doc holds an Atom. This typed algebra keeps state decidable (no stringly-typed cells) and thereby provable — the same property that makes workflows decidable and turn them into native_decide theorems.

Binding (host)

Module: Encapp/AppGen.lean

A typed, declared extension point: the metadata an app carries so a deployment knows what the app expects of its host. Deliberately opaque — Encapp does not know what a binding means; it only serializes it to JSON via toJson : β → String. Before binding, the store-write seam was an untyped hole (window.ENC_ADAPTER), and nothing declared what a deployment owed the app. A hand-written protocol could fill it silently. A typed, declared binding is an invitation to be checked, not to be filled by hand.

Coverage gates

Module: test/page-coverage.mjs, test/handler-coverage.mjs, test/nav-integrity.mjs

Machine-enforced completeness checks that fail the build if any screen, handler, or navigation link is untested. Each caught a real gap the day it was added: uncovered pages, unfired handlers, broken nav graphs. page-coverage is bijective — every registered page must be reached and every path a workflow reaches must be registered. handler-coverage requires every handler tag to be fired by some workflow. nav-integrity walks page views and fails if a static nav target is not a registered page. See Testing and coverage gates.

Doc

Module: Encapp/Doc.lean

The document model a real app needs: named scalar fields and named tables of rows. Where Spec used key → Int (sufficient for Counter), Doc holds scalars : List (String × Atom) and tables : List (String × List Row). This is the expressive power needed for messaging apps — every field and every row carries a typed Atom, so state is decidable and provable. Both workflow checks and handler effects operate on Doc; it is the hub of the proof semantics.

Eff

Module: Encapp/AppGen.lean

A reflected effect: the defunctionalized image of one update step. An Eff describes what one handler should do — set a scalar, append a row, navigate, etc. — entirely as data. Examples: setConst "path" (.str "/messages") sets the path scalar to a constant, pushDraft "posts" appends a post row, setConvId derives a conversation ID, lookupRoute searches a table for a peer. The handler table is a list of (tag, List Eff) pairs; reflStep applies a tag by running its effects through applyEff. This defunctionalization is what makes the app data, serializable, and codegen-able.

Emulator

Module: Encapp/Store.lean

The denotational spec: a World whose internal state is the committed event log. When a Cmd.submit is run, the emulator appends to its log and emits the event. Cmd.none does nothing. Every real adapter is judged against this: it must refine the emulator, meaning for every command sequence the adapter emits identical event traces and ends with a related state. refines_sound proves that a refining adapter is observationally indistinguishable from the emulator — the property that lets a real backend drop in for the spec without changing meaning.

Gate (route)

Module: Encapp/AppGen.lean (in ReflApp)

A declared guard that runs before the path lookup. Gates are pairs (scalar, page) that say: whenever this scalar is empty, render this page, whatever the path says. They evaluate in order. Without gates, every page is reachable by setting path, so nothing forces a user through onboarding. Gates are data, not code — the framework checks them once per render, and a workflow that navigates to a gated page while the gate scalar is empty will prove it lands on the guard page. Example: gates := [("identity", "/connect"), ("onboarded", "/profile")] forces a user through connection and onboarding.

Handler

Module: Encapp/AppGen.lean (as RHandler)

A reflected handler: a message tag and the effects it runs. A RHandler is tag : String and effs : List Eff. When a user fires a handler (by clicking a button with that tag), reflStep finds the handler in the table, then folds its effects through applyEff to update the Doc. Handlers are pure data; they live in the app's emitted artifact and are executed identically on every runtime.

native_decide

Module: Lean core

A Lean tactic that compiles a decide-able proposition all the way down to computation. A workflow proof has the shape by native_decide — the workflow is run through the reflected interpreter, all checks are evaluated against the resulting Doc, and the theorem is discharged by reduction. This costs the axiom Lean.ofReduceBool; the axiom audit pins that explicitly. Workflow theorems prove app logic once at lake build time; the same logic then runs on four independent runtimes.

Payload

Module: Encapp/AppGen.lean

Message data: the value a handler receives when it fires. A Payload is either atom : Atom (a scalar — typically a navigation path or a user input) or row : Row (the fields of a row from a table). This generalization matters for "select this row" interactions: the handler needs the row's fields so it can lift them into scalars. Payload.asAtom projects a row to .null, and Payload.field looks up a named field.

ReflApp

Module: Encapp/AppGen.lean

A fully reflected, codegen-ready app. A ReflApp β holds init : Doc (initial state), pages : List (String × RView) (path to view), handlers : List RHandler (handler table), gates : List (String × String) (route guards), and binding : Option β (host expectations). It is the serializable image of a typed App — all functions defunctionalized to data. Codegen.emit walks a ReflApp and emits HTML + JavaScript; the emitted runtime mirrors the Lean interpreter reflStep, checked empirically against four replayers.

Refinement

Module: Encapp/Store.lean (as Refines)

The proof obligation a real store backend must discharge. A World w refines the emulator under relation R when three hold: (1) the relation starts true, (2) every command preserves it with identical emitted events, and (3) the observable logs are equal whenever the relation holds. refines_sound proves that if a world refines, it is indistinguishable from the emulator for every command sequence. This is the pure form of enc-ui-kit's "Mode A ≡ Mode B" claim, proven as a simulation argument by induction, not asserted in roadmap text.

Replay tiers

Module: test/encapp-replay-dom.mjs, test/encapp-replay.mjs, test/encapp-replay-rnweb.mjs, test/encapp-replay-electron.mjs

Four independent runtimes that execute the same workflow corpus without per-tier test code. The dom tier uses happy-dom for speed (no browser). hl runs headless Chromium via Playwright. rnweb executes the React Native emit under React-Native-web. electron uses a real Electron main + renderer. All four drive the app through the emitted hook window.__enc = { S, step, render } and assert the same DOM-level checks. This is where the framework catches divergences between Lean and the JS runtime — what the proof tier cannot see.

Row

Module: Encapp/Doc.lean

A table row: an ordered list of named Atom fields. Row is a type alias for List (String × Atom). A Doc holds named tables of rows, and workflows can assert the contents of specific rows with checks like rowField "messages" 0 "body" (.str "hello"). Handlers can read row fields with Payload.field and write rows with effects like appendFromRow (append a row copying fields from the payload row).

RView

Module: Encapp/AppGen.lean

A reflected view: the defunctionalized image of a typed View Msg. An RView carries the same layout constructors (text, input, button, list, etc.) but with typed messages defunctionalized to (tag, payload) pairs. Codegen.emit walks a ReflApp and defunctionalizes its typed View into RView, then emits an interpreter in JavaScript that renders any RView to DOM. The same interpreter drives web, React-Native-web, and Electron.

Spec

Module: Encapp/Spec.lean

A serializable reflected app with a simple state model: init : List (String × Int) (the store), view : Ui String (the view), and update : List Handler (the handler table). Spec.toApp lifts it into the abstract App algebra, so theorems about App — reload equivalence, etc. — apply to it. Unlike ReflApp, Spec uses Int state (sufficient for Counter); it is the simplest playground for the proof framework. Apps that need rows and scalar fields use ReflApp + Doc instead.

Workflow

Module: Encapp/Workflow.lean

A named list of interaction steps plus the checks that must hold afterwards. A Workflow has two simultaneous meanings: (1) a proof — Workflow.holds app w = true is decidable, so by native_decide discharges it as a theorem; (2) a corpus entry — Workflow.toJson w renders the same workflow as runner-shaped JSON. Define once, prove once, run everywhere. The interpreter that runs the app is the interpreter that proves the test. A workflow step is either fire tag payload (dispatch a handler) or input field value (set a scalar).

World

Module: Encapp/Store.lean

An abstract store backend with opaque internal state H. A World H defines empty : H (initial state), run : Cmd → H → H × List Event (interpret a command), and log : H → List Event (extract the observable log). The emulator is one World (state = log); a real enc-flow adapter is another. Both implement this interface, and refines_sound proves they behave identically if the adapter refines the emulator under some relation R.

Recap

  • Proof layer: Apps are ReflApp or Spec — typed, data-driven, serializable structures.
  • State layer: Doc holds scalars and tables of rows; each value is a typed Atom.
  • Logic layer: Handlers are (tag, Eff) pairs; effects are data, not functions.
  • View layer: View Msg types down to RView (tagged messages); the same interpreter renders on all platforms.
  • Test layer: Workflows are proofs and corpus entries; the same definition is native_decide theorem and JSON-emitted test.
  • Store layer: World is an abstract store backend; the emulator is the spec; a real adapter refines it under a relation R.
  • Coverage layer: Three gates (page, handler, nav) enforce completeness; four replayers catch divergences the proof tier cannot see.

Next steps