Skip to content
Logo

Documented examples

Encapp ships three fully-proven examples, each demonstrating a different surface: the minimal algebra (Counter), a full messaging app (Hello), and the workflow DSL that proves them both (HelloWorkflow). Every theorem is checked at lake build time.

Counter — two surfaces, one behaviour

Counter is the only non-messaging example, and intentionally so. It shows both the reflected surface and the abstract surface:

/-- The counter as data: `[-]  count  [+]` -/
def counter : Spec where
  init   := [("count", 0)]
  view   := .col [ .button "-" "dec", .bind "count", .button "+" "inc" ]
  update := [ ⟨"inc", "count", .incr⟩, ⟨"dec", "count", .decr⟩ ]

The Spec is the data your codegen reads. But there is also a typed version:

inductive CMsg where | inc | dec
 
def counterApp : App Int CMsg where
  init := 0
  update msg n := match msg with
    | .inc => (n + 1, [])
    | .dec => (n - 1, [])
  view n := .col [ .button "-" .dec, .text (toString n), .button "+" .inc ]

The App is elegant: no strings, no row mutations, no store effects. Both are true. The framework proves them compatible.

What to copy

  • The two-face pattern itself: write the data version first for codegen, then lift to the typed version for clarity.
  • The theorem structure: counter_inc_one and counter_inc_dec_roundtrip are decision procedures — by decide.
  • State is minimal (an Int), so this is your template for any stateless or simple-state app.

What it does not show

Counter does not go through AppGen.emit to become a deployed SPA; it uses the simpler Spec path. No non-messaging app has yet shipped through the full emitter pipeline, so if you are building a non-messaging UI, you will need to extend the effect algebra (see What is proven).

Hello — full app, three layers

Hello is the reimplementation of enc-ui-kit's messaging example in pure Encapp, cleanly separated into logic, view, and reflection:

inductive HMsg where
  | connect : String → HMsg
  | input   : String → HMsg
  | submit  : HMsg
  | nav     : String → HMsg
  deriving DecidableEq, Inhabited
 
def helloInit : Doc where
  scalars := [ ("identity", .null), ("path", .str "/connect"), ("draft", .str "") ]
  tables  := [ ("messages", []), ("my_messages", []) ]

The view routes on path and binds tables:

def helloView (d : Doc) : View HMsg :=
  match asStr (d.getScalar "path") with
  | "/connect"  => .col [ .text "Connect your wallet to use Hello.",
                          .button "Connect" (.connect "79be667ef9dcbbac") ]
  | "/feed"     => .col [ .list "messages" (.rowField "body"),
                          .input "draft", .button "Post" .submit,
                          .button "My posts →" (.nav "/my_posts") ]
  | "/my_posts" => .col [ .list "my_messages" (.rowField "body"),
                          .input "draft", .button "Post" .submit,
                          .button "← Feed" (.nav "/feed") ]
  | _           => .text ""

The logic is a typed App Doc HMsg, no strings:

def helloApp : App Doc HMsg where
  init := helloInit
  update msg d := match msg with
    | .connect w => ((d.setScalar "identity" (.str w)).setScalar "path" (.str "/feed"), [])
    | .input v   => (d.setScalar "draft" (.str v), [])
    | .submit    =>
        let d' := ((d.appendRow "messages" (postRow d)).appendRow "my_messages" (postRow d)).setScalar "draft" .null
        (d', [ .submit { id := short16 (asStr (d.getScalar "identity")), data := asStr (d.getScalar "draft") } ])
    | .nav p     => (d.setScalar "path" (.str p), [])
  view := helloView

The reflection projects it to data the codegen reads:

def reflectView : View HMsg → RView := { -- defunctionalize buttons to (tag, payload) pairs
  | .button l m   => let e := encodeMsg m; .button l e.1 e.2
  -- ... other constructors mirror the types
}
 
def helloReflected : ReflApp Unit where
  init     := helloInit
  pages    := [ ("/connect", reflectView (helloView (helloInit.setScalar "path" (.str "/connect")))), ... ]
  handlers := [ ⟨"connect",   [ .setInput "identity", .setConst "path" (.str "/feed") ]⟩, ... ]

Three theorems prove them compatible:

theorem hello_reflected_matches : reflRun helloHandlers demoSteps helloInit = helloFinal := by native_decide
theorem hello_draft_cleared : helloFinal.getScalar "draft" = .null := by native_decide
theorem hello_one_message : (helloFinal.rows "messages").length = 1 := by native_decide

What to copy

  • The message inductive, the Doc shape (scalars + tables), the view routing pattern.
  • The App definition with type-safe update and view.
  • The reflectView mutual recursion that defunctionalizes typed views to data.
  • The theorem structure: run a canonical workflow, then assert each post-condition.

What it does not show

Hello is codegen-ready: the helloReflected data structure is exactly what AppGen.emit expects. But it has not been run through emit into a real SPA. It proves at the Lean tier and is replayed on four runtimes (happy-dom, Chromium, React Native, Electron) to empirically verify the JS runtime matches. See What is proven.

HelloWorkflow — proofs that are also tests

HelloWorkflow wraps the canonical interactions into the workflow DSL, where each workflow is simultaneously a native_decide theorem and a cross-platform test:

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") ]
 
theorem helloWorkflow_holds : helloWorkflow.holds helloReflected = true := by native_decide

Collect workflows into a corpus:

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 corpus is emitted to JSON and replayed against the bundled app on every platform. If a handler or the interpreter drifts, the proof fails at lake build.

What to copy

  • One workflow per screen or feature path: helloConnect covers the entry screen (no steps, just init), helloWorkflow covers the post flow, helloMyPosts exercises navigation to a second table.
  • The checks pattern: after steps, assert the state shape (which scalar, how many rows, which field value).
  • The aggregate theorem: corpus_all_hold catches any workflow that drifts, and corpus_single_user guards the emit (the corpus JSON assumes one user per step).

What it does not show

Workflows prove single-app-instance logic — one Doc at a time. Multi-user and cross-enclave interactions belong to the node layer. The emitted corpus carries a users list so a multi-client runner can project it, but by native_decide proves one instance. See Workflows and proofs.

Recap

  • Counter — the minimal example, two surfaces (data + typed), three simple theorems. Use it for non-messaging apps or when state is an Int.
  • Hello — a full messaging app, three clean layers (logic, view, reflection), proven to match its codegen-ready data. Use it as your template for any messaging UI.
  • HelloWorkflow — a corpus of workflows that prove the app's paths, emitted to JSON for cross-platform replay. Use it to cover every screen and handler.

No non-messaging app has shipped through AppGen.emit yet; the effect algebra carries chat vocabulary. Counter and Hello are proven; empirical evidence (not Lean theorems) confirms the JS runtimes match the Lean interpreter on four platforms.

Next steps

  • Host bindings — declare what your app needs from the runtime (store, effects, UI).
  • Workflows and proofs — the DSL in detail, with replayer commands.
  • What is proven — the honest boundary between proofs, checks, and hand-written code.