Skip to content
Logo

Testing and coverage gates

Encapp's verification stack has four tiers, and each exists because the tier above it cannot see a particular class of failure.

TierWhat it checksWhat it cannot see
Proof (lake build)app logic, generically and per workflowwhether the emitted JS matches the Lean
Axiom auditthat a proof is not vacuous or sorry-shapedanything about runtime behaviour
Replaythe emitted artifacts really behave as proven, on four runtimesanything no workflow exercises
Coveragethat no screen, handler or link is unexercisedwhether an assertion is meaningful

Run everything

node test/hello-matrix.mjs

The axiom audit

lake build accepts a proof containing sorry — it only warns. A keystone could therefore rot to unsound and still build green.

node test/axiom-audit.mjs <repo> <module> <decls,comma,separated> <extra-allowed-axioms>

It runs #print axioms on each declaration and fails on sorryAx or any axiom outside the accepted set. Two pins matter:

  • workflow theorems may use Lean.ofReduceBool (that is what native_decide costs) and nothing else;
  • Foundation.Layer.mono — the keystone the bridge leans on — is pinned to exactly zero axioms.

This runs first in the matrix, before anything is built on top of a proof that might not exist.

The replayers

One corpus, four runtimes, no per-tier test code:

RunnerTierRuntime
encapp-replay-dom.mjsdomhappy-dom — fast, no browser
encapp-replay.mjshlheadless Chromium via Playwright
encapp-replay-rnweb.mjsrnwebthe React Native emit, running under React-Native-web
encapp-replay-electron.mjselectrona real Electron main + renderer

All four drive the app through the emitted runtime hook:

window.__enc = { S, step, render }

They mirror the runtime exactly — input sets a scalar with no re-render, fire dispatches and renders. Adding a render after input would make the tests pass against behaviour the real app does not have.

node test/encapp-replay-dom.mjs dist /tmp/corpus.json
node test/encapp-replay.mjs     dist /tmp/corpus.json

The coverage gates

Machine-enforced completeness. Each one caught a real gap the day it was added, which is the only evidence that a gate can fail.

node test/page-coverage.mjs    <appDir> <emit-pages-nav> <emit-corpus>
node test/handler-coverage.mjs <appDir> <emit-handlers>  <emit-corpus>
node test/nav-integrity.mjs    <appDir> <emit-pages-nav>
  • page-coverage — bijective, both directions. Caught an uncovered screen in the flagship app and an uncovered entry route in hello.
  • handler-coverage — every reflected handler tag must be fired. Caught eight unfired handlers in the flagship app.
  • nav-integrity — walks page views; every static nav target must be a registered page, so the nav graph is closed.

They take the app directory and per-app emit scripts as arguments, which is what makes them app-generic rather than tied to one app.

Native parity

The native target shares appCoreJs with web, and these prove that sharing is real rather than intended:

CheckAsserts
native-core-identity.mjsthe web and native emitted cores are byte-identical
native-locators-hello.mjsevery handler tag is locatable on-device, so an on-device driver can find controls
native-input-sync.mjsvisible input values track state on both platforms
fuzz-parity.mjsdifferential fuzzing over seeded synthetic apps: web and native must render the same

fuzz-parity.mjs runs a curated seed set, not just a default seed. Each pinned seed exposed a distinct divergence class during development — relative font weights and line-height, element buttons, in-run element-button flow, inline inputs colliding with keys, and styled{text} inheriting fonts. Pinning them turns one-shot finds into permanent regression coverage:

node test/fuzz-parity.mjs 314159,1,42,303,424242,16180

Writing tests that can fail

Two rules earned the hard way:

A green check that has never been red is indistinguishable from one that cannot fail. Before trusting a new detector, introduce the bug it exists to catch and watch it go red. Several detectors in this repository reported clean before they worked — one counted payload atoms as effects, one treated a skip as a pass, one flagged whitespace differences in colour values.

State exactly what was exercised. "The workflows pass" is a claim about the proof tier. "The corpus replays on dom and hl" is a claim about two runtimes. They are different claims, and collapsing them into "it works" is how confidence gets transferred that was never earned.

Scope

The workflow framework covers ReflApp + Doc apps — those interpreted by reflRun. The Spec / App Int examples such as Counter use a different state model and are out of scope without a rewrite.

Live behaviour that needs a real backend and real cryptography is a separate corpus. Crypto itself is axiomatized: the proofs cover data-plane logic, not the primitives.

Recap

  • Four tiers exist because each one is blind to a different class of failure: proof tier cannot see if emitted JS matches Lean; replay cannot see what workflows don't exercise; coverage cannot see if assertions are meaningful
  • The axiom audit fails on sorryAx or any axiom outside an accepted set; workflow theorems may use only Lean.ofReduceBool, and Foundation.Layer.mono must be axiom-free
  • Four replayers (happy-dom, headless Chromium, RN-web, Electron) all drive the app through window.__enc = { S, step, render } to mirror the runtime exactly
  • Three coverage gates enforce bijection (pages ↔ workflows), handler coverage (every tag is fired), and nav integrity (every link is registered); they are app-generic and caught real gaps in the flagship app
  • Native parity checks prove the cores are byte-identical and that web and native render the same over seeded differential fuzzing — pinned seeds prevent regression on distinct divergence classes

Next steps