Skip to content
Logo

Tutorial: build Hello (part 2)

In part 1 you defined the app logic as a ReflApp — the handlers, state, and view tree. Now you'll ship it: compile to three surfaces (web SPA, native, desktop), prove the user stories, and validate them on multiple platforms.

The main entry point: HelloApp.lean

HelloApp.lean is the single file that compiles everything. Here is what it does:

import Encapp
 
open Encapp Encapp.Examples
 
def main : IO Unit := do
  -- The web SPA
  let html := AppGen.emit (DocChrome.light "Hello") helloReflected
  IO.FS.createDirAll "dist"
  IO.FS.writeFile "dist/index.html" html
  IO.println s!"encapp: wrote dist/index.html ({html.length} bytes) — the full hello app"
 
  -- The native target (same reflected app, emitted for React Native)
  let native := AppGen.emitNative helloReflected (baseText := "color:#18181b")
  IO.FS.createDirAll "dist/native"
  IO.FS.writeFile "dist/native/app.cjs" native
  IO.println s!"encapp: wrote dist/native/app.cjs ({native.length} bytes) — the hello app, native target"
 
  -- The desktop trio (Electron shell + preload + package.json)
  let dc : DesktopChrome := { name := "hello-encapp", title := "Hello · encapp" }
  IO.FS.createDirAll "dist/desktop"
  IO.FS.writeFile "dist/desktop/main.cjs" (AppGen.emitDesktopMain dc)
  IO.FS.writeFile "dist/desktop/preload.cjs" AppGen.emitDesktopPreload
  IO.FS.writeFile "dist/desktop/package.json" (AppGen.emitDesktopPackageJson dc)
  IO.println "encapp: wrote dist/desktop/ (main.cjs + preload.cjs + package.json) — the hello app, desktop target"

The pattern is strict: one reflected app, three surfaces. helloReflected (your interpreter from part 1) flows through AppGen.emit, AppGen.emitNative, and AppGen.emitDesktop*. The browser, the native interpreter, and the Electron shell all execute the same compiled logic.

Register this in lakefile.lean:

/-- Compiles the full `hello` app to `dist/index.html`. -/
lean_exe «helloapp» where
  root := `HelloApp

Then run it:

~/.elan/bin/lake exe helloapp

The web SPA lands at dist/index.html and is ready to serve. The native bundle is at dist/native/app.cjs. The desktop files are static and ready to bundle into an Electron build.

Three workflows: proof tier

Now define the user stories. Open Encapp/Examples/HelloWorkflow.lean:

import Encapp.Examples.Hello
import Encapp.Workflow
 
namespace Encapp.Examples
 
/-- The canonical hello post workflow — defined once. -/
def helloWorkflow : Workflow where
  name   := "hello-post"
  users  := ["alice"]
  steps  := [ .fire "connect" (.atom (.str "79be667ef9dcbbac")),
              .input "draft" (.str "hello from node:test"),
              .fire "submit" (.atom .null) ]
  checks := [
    .scalarEq "identity" (.str "79be667ef9dcbbac"),
    .scalarEq "path" (.str "/feed"),
    .scalarEq "draft" .null,
    .tableLen "messages" 1,
    .rowField "messages" 0 "body" (.str "hello from node:test") ]
 
/-- Proof: the app logic holds. -/
theorem helloWorkflow_holds : helloWorkflow.holds helloReflected = true := by native_decide

That one theorem is the proof tier. native_decide discharges at lake build time by running the interpreter on your steps and asserting every check.

Add two more workflows to cover the routing:

/-- Post, then navigate to /my_posts — exercises the nav handler. -/
def helloMyPosts : Workflow where
  name   := "hello-my-posts"
  steps  := [ .fire "connect" (.atom (.str "79be667ef9dcbbac")),
              .input "draft" (.str "note to self"),
              .fire "submit" (.atom .null),
              .fire "nav" (.atom (.str "/my_posts")) ]
  checks := [
    .scalarEq "path" (.str "/my_posts"),
    .tableLen "my_messages" 1,
    .rowField "my_messages" 0 "body" (.str "note to self") ]
  ui     := [ .seesText "← Feed" ]
theorem helloMyPosts_holds : helloMyPosts.holds helloReflected = true := by native_decide
 
/-- The /connect screen renders — no workflow fires, just init. -/
def helloConnect : Workflow where
  name   := "hello-connect"
  steps  := []
  checks := [ .scalarEq "path" (.str "/connect") ]
  ui     := [ .seesText "Connect your wallet" ]
theorem helloConnect_holds : helloConnect.holds helloReflected = true := by native_decide

The ui list (.seesText, .namedControl) is proof-skipped — it is about the rendered DOM, which the Doc model does not describe. The replayers will check it.

The corpus: proof tier + execution tier

Collect them into a single source of truth:

def helloWorkflows : List Workflow := [helloWorkflow, helloMyPosts, helloConnect]
 
theorem helloWorkflows_all_hold : helloWorkflows.all (·.holds helloReflected) = true := 
  by native_decide
 
theorem helloWorkflows_single_user : 
    helloWorkflows.all (fun w => decide (w.users.length ≤ 1)) = true := by native_decide
 
def helloCorpus : List String := helloWorkflows.map (·.toJson)

The single_user theorem is not decoration. Workflow.toJson emits one-user steps, so if a workflow declared two users the emitted JSON would silently misrepresent it. The theorem makes that boundary explicit. If a developer adds a multi-user workflow, the build fails — not in CI, at edit time.

Emit the corpus

Write a small Lean script to serialize the workflows to JSON:

~/.elan/bin/lake env lean --run test/emit-hello-corpus.lean > /tmp/corpus.json

The output is an array of runner-shaped JSON, ready for replayers:

[
  {
    "name": "hello-post",
    "users": ["alice"],
    "steps": [
      {"as":"alice","do":"fire","tag":"connect","payload":"79be667ef9dcbbac"},
      {"as":"alice","do":"input","field":"draft","value":"hello from node:test"},
      {"as":"alice","do":"fire","tag":"submit","payload":null}
    ],
    "checks": [
      {"kind":"scalar","key":"identity","eq":"79be667ef9dcbbac"},
      {"kind":"tableLen","table":"messages","eq":1},
      {"kind":"rowField","table":"messages","i":0,"field":"body","eq":"hello from node:test"}
    ],
    "ui": []
  }
  ...
]

Replay: four tiers

Now run the same corpus on four independent runtimes:

# happy-dom (no browser)
node test/encapp-replay-dom.mjs dist /tmp/corpus.json
 
# headless Chromium
node test/encapp-replay.mjs dist /tmp/corpus.json
 
# React Native web (the native interpreter on the web)
node test/encapp-replay-rnweb.mjs dist /tmp/corpus.json
 
# Real Electron (the emitted desktop shell)
node test/encapp-replay-electron.mjs dist/desktop /tmp/corpus.json

Each replayer is app-generic: the same binary runs the hello corpus and the production corpus. If the app drifts from Lean semantics, one of these fails immediately.

Coverage gates: proof + bijection

The hello-matrix.mjs test orchestrator runs three gates that catch gaps:

1. Page coverage — every registered page must be reached by a workflow:

node test/page-coverage.mjs . test/emit-pages-nav.lean test/emit-hello-corpus.lean

If you add a new route (e.g., /settings) but no workflow navigates to it, the gate fails.

2. Handler coverage — every handler tag must be fired:

node test/handler-coverage.mjs . test/emit-handlers.lean test/emit-hello-corpus.lean

If you add a button that calls a handler submit but the corpus never fires it, the gate fails.

3. Nav integrity — every static nav link must point to a registered page:

node test/nav-integrity.mjs . test/emit-pages-nav.lean

If a page contains a link to /nonexistent, the gate fails.

All three are app-generic. They are the same gates the production app uses.

The full matrix: hello-matrix.mjs

To run everything in one command:

node test/hello-matrix.mjs

This orchestrates:

  1. Axiom audit — verifies that helloWorkflow_holds, helloWorkflows_all_hold, and helloWorkflows_single_user each discharge with exactly the allowed axioms (Lean.ofReduceBool for native_decide, zero for the keystone Foundation.Layer.mono).
  2. Coverage gates — page + handler + nav, as above.
  3. Native core identity — asserts the web and native step engines are byte-identical.
  4. Native locators — proves each handler is locatable by tag on the native app.
  5. Native input sync — visible input values track state on both platforms.
  6. Fuzz parity — differential fuzzing with a curated seed set (each seed once exposed a distinct divergence class).
  7. Replay on four tiers — dom, headless chromium, RN-web, Electron.

If any step fails, you see why immediately.

Honest boundaries

  • Proof tier is single-instance logic. reflRun has single-Doc semantics, so the native_decide theorem proves your app on one interpreter instance. Multi-user and cross-enclave stories are the backend's concern. The emitted corpus carries a users list so a multi-client runner can project it.
  • JS runtime is checked, not proven. There is no Lean theorem equating appCoreJs to reflStep. What exists instead is empirical: the same corpus runs on four independent runtimes, and native-core-identity asserts the web and native cores are byte-identical.
  • Coverage is enforced, not encouraged. An untested screen is a test failure, not a warning.

Recap

  • One reflected app, three surfaces: AppGen.emit for web, emitNative for React Native, emitDesktop* for Electron.
  • Define workflows once: a Workflow is simultaneously a native_decide theorem and runner JSON.
  • Proof-time + runtime validation: the corpus is proven by native_decide, then replayed on happy-dom, Chromium, React-Native-web, and Electron.
  • Coverage gates catch gaps: page, handler, and nav integrity are bijective — untested surfaces fail the build.

Next steps