Architecture

Layer map

       ┌──────────────────────────────────────────────────────────────┐
       │ YOUR APP           Encapp/Examples/Hello.lean                │
       │   typed face   App Model Msg  ·  View Msg                    │
       │   reflected    ReflApp β      ·  RView  ·  Eff  ·  RHandler  │
       │   tied by      theorem hello_reflected_matches               │
       └───────────────┬──────────────────────────────────────────────┘
                       │
  ┌────────────────────┴───────────────────┬─────────────────────────┐
  │ AUTHORING                              │ VERIFICATION            │
  │  Core.lean     App / Cmd / Event       │  Workflow.lean          │
  │  View.lean     the typed vocabulary    │    WStep · WCheck       │
  │  Ui.lean       the minimal vocabulary  │    UICheck · Workflow   │
  │  ViewDsl.lean  authoring sugar         │  → native_decide proof  │
  │  Doc.lean      Atom · Row · Doc        │  → runner JSON corpus   │
  └────────────────────┬───────────────────┴─────────────────────────┘
                       │
  ┌────────────────────┴─────────────────────────────────────────────┐
  │ SEMANTICS + PROOF                                                │
  │  Store.lean    World · Refines · refines_sound · refines_log     │
  │  Adapter.lean  reversedWorld — a real refinement witness         │
  │  Replay.lean   applyEv_idem · replayLog_append                   │
  │  Bridge.lean   the interpreter as a Foundation.World / Layer     │
  └────────────────────┬─────────────────────────────────────────────┘
                       │
  ┌────────────────────┴─────────────────────────────────────────────┐
  │ CODEGEN                                                          │
  │  AppGen.lean   reflStep (the Lean spec)                          │
  │                appCoreJs  — the shared state machine             │
  │                appDomJs   — the web renderer                     │
  │                appRnJs    — the React Native renderer            │
  │                emit · emitNative · emitDesktop*                  │
  │  EmuGen.lean   the ENC emulator authored as RView data           │
  │  Codegen.lean  the minimal Spec → SPA path (counter)             │
  └──────────────────────────────────────────────────────────────────┘

The two faces, and the theorem between them

An app is authored twice and proven identical.

-- typed: a real inductive Msg, type-safe buttons, ergonomic
def helloApp : App Model Msg := …
 
-- reflected: string tags, a finite handler table, serializable
def helloReflected : ReflApp Unit := …
 
-- the tie: the reflected interpreter agrees with the typed update
theorem hello_reflected_matches : … := by native_decide

Without that theorem the reflected form would be a hand-maintained copy, which is exactly the drift the framework exists to prevent.

`Doc` — the state model

Real apps need more than a counter's key → Int. Doc is named scalars plus named tables of rows, where every leaf is a typed Atom:

inductive Atom where
  | str : String → Atom | int : Int → Atom | bool : Bool → Atom | null : Atom
 
abbrev Row := List (String × Atom)
 
structure Doc where
  scalars : List (String × Atom)
  tables  : List (String × List Row)

Everything is DecidableEq, which is what makes native_decide able to settle a workflow's post-conditions. See Encapp.Doc.

From one value to three artifacts

AppGen.emit serializes the ReflApp into JSON, embeds it in an HTML document together with the runtime, and writes one file. The runtime is two concatenated strings:

def appRuntimeJs : String := appCoreJs ++ "\n" ++ appDomJs

appCoreJs — the state machine: S (the Doc), step(tag, payload), the Eff interpreter, gates and routing. It is the operational mirror of reflStep.
appDomJs — the DOM renderer: RView → DOM nodes, event wiring, history.
appRnJs — the React Native renderer: the same RView vocabulary → RN elements.

emitNative emits appCoreJs ++ appRnJs. Because the core string is literally the same Lean definition, a test can assert byte-identity between the web and native cores — and test/native-core-identity.mjs does exactly that.

Desktop does not get a third renderer. emitDesktopMain / emitDesktopPreload / emitDesktopPackageJson produce a generic Electron shell that loads the web artifact, so the desktop renderer cannot drift from web by construction.

The runtime hook

The emitted page exposes a small handle:

window.__enc = { S, step, render }

S is the live Doc, step(tag, payload) dispatches a handler, render() repaints. Every replayer drives the app through this hook, which is why the same corpus runs on happy-dom, Chromium, React-Native-web and Electron without per-tier test code.

The replayers mirror the runtime exactly: an input step sets a scalar with no re-render (matching the emitted oninput, which assigns S.scalars[f]), and a fire step dispatches and then renders (matching step). Adding a render after input would make the test diverge from the real app.

Dependency direction

Encapp depends on Foundation (for the Layer.mono keystone used by Bridge.lean) and on nothing else. It has no dependency on any protocol, SDK or network library. Apps depend on Encapp; Encapp never depends on an app.

The one place an app's world could leak in is the host binding, and that is why HostBinding is a typeclass with a single toJson method and no knowledge of what a binding means.