Skip to content
Logo

Workflows and proofs

A Workflow is a named list of interaction steps plus the checks that must hold afterwards. The same value is used two ways:

  • Proof tier — Workflow.holds app w is a Bool, so by native_decide turns it into a theorem checked at lake build time.
  • Execution tier — Workflow.toJson w renders runner-shaped JSON that the replayers execute against the emitted artifacts on four runtimes.

Define once, prove once, run everywhere. The interpreter that runs the app is the interpreter that proves the test.

The DSL

structure Workflow where
  name   : String
  users  : List String := ["alice"]
  steps  : List WStep
  checks : List WCheck := []
  ui     : List UICheck := []

Steps — the two real interaction primitives

inductive WStep where
  | fire  : String → Payload → WStep   -- click / nav → step(tag, payload)
  | input : String → Atom → WStep      -- typing → set a scalar
  | back  : WStep                      -- browser history back

These mirror the runtime exactly. input sets a scalar with no re-render, matching the emitted oninput binding; fire dispatches and then renders, matching step. back is identity in the proof — history is a runtime concern, not part of the Doc — and is genuinely executed by the replayers.

Checks — provable post-conditions

inductive WCheck where
  | scalarEq : String → Atom → WCheck                 -- scalar k equals v
  | tableLen : String → Nat → WCheck                  -- table t has exactly n rows
  | rowField : String → Nat → String → Atom → WCheck  -- table t, row i, field f equals v

All decidable, which is what makes the theorem discharge by computation.

UI checks — replay-only DOM assertions

inductive UICheck where
  | seesText     : String → UICheck   -- the visible text contains this
  | namedControl : String → UICheck   -- a control with this accessible name exists

These are not part of the native_decide proof — they are about the rendered page, which the Doc model does not describe. The replayers evaluate them against the live DOM.

A complete example

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

If a handler or the interpreter drifts, this stops compiling. That is the difference between a test that fails in CI and a proof that fails the build.

The corpus

Collect workflows into a list and prove the whole thing at once:

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)

corpus_single_user is not decoration. Workflow.toJson emits steps as a single user, so if a workflow ever declared two users the emitted corpus would silently misrepresent it. The theorem makes that boundary explicit instead of implied.

Emitted JSON

{ "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": [] }

Emit it from a small script and pipe it to a replayer:

~/.elan/bin/lake env lean --run test/emit-hello-corpus.lean > /tmp/corpus.json
node test/encapp-replay-dom.mjs dist /tmp/corpus.json
node test/encapp-replay.mjs     dist /tmp/corpus.json     # headless chromium

Coverage is enforced, not encouraged

A screen or handler with no workflow is untested surface, so the gates fail on gaps:

  • page-coverage.mjs — bijective. Every registered page must be reached by a workflow, and every path a workflow reaches must be a registered page.
  • handler-coverage.mjs — every handler tag must be fired by some workflow. An input X step credits the input-binding handler set:X.
  • nav-integrity.mjs — every static nav target in a page view must be a registered page.

All three are app-generic: the same tools drive hello and the flagship app.

Honest boundary

reflRun has single-Doc semantics, so the proof tier is single-app-instance logic. Multi-user and cross-enclave stories belong to the node layer; the emitted corpus carries a users list so a multi-client runner can project it, but the theorem is about one instance. Live behaviour that needs a real backend and real crypto is a separate corpus, kept separately and deliberately not claimed as covered here.

Recap

  • Workflows are single-value objects used as both native_decide theorems (proof tier) and JSON test specifications (execution tier)
  • The three step primitives (fire, input, back) mirror runtime behavior exactly; checks are decidable post-conditions on state
  • Coverage gates prove bijection between registered pages and workflows, and between handlers and fire steps — untested surfaces fail the build
  • The honest boundary: proofs are single-instance logic; multi-user and crypto-backed behavior belong to separate corpora
  • Collect workflows into a list and prove all of them at once; the theorem is your guarantee that the emitted corpus is sound

Next steps