Litepaper — why this methodology stands

The claim, in one paragraph

A client application that holds keys and signs commits should have a trusted computing base you can list. In a conventional UI framework you cannot list it, because a component reaches window, localStorage or fetch by ambient reference and nothing at the call site records that it did. encapp's position is that the UI layer should be written in a decidable subset of a familiar language, so that what the layer can reach is a build artifact rather than a review outcome. This document states what that buys, what it costs, and — precisely — what is proven, what is merely trusted, and what is not built yet.

The problem is not that developers are careless

It is that review capacity is the scarce resource, and it does not scale with the volume of code being produced.

That was already true when code was written by hand. It is sharper now: machine-written volume grows faster than the attention available to read it. The usual answers — more linting, more review, more tests — all consume the resource that is scarce. A decision procedure does not. It moves the question from did someone notice to did the checker exit 0, and that is a property which improves as generated volume rises rather than degrading under it.

For a crypto client specifically the argument compresses to one line: the boundary of what the UI layer can reach should be a build artifact, not a review outcome.

Why an unbounded framework cannot be the substrate

React is not the problem; unboundedness is. In a language where a hook may run any effect at any time, a handler may close over any mutable value, and a component may compute its children's types, there is no denotation you can write down. Without a denotation there is nothing to prove against, and the only available check is a screenshot.

That is worth stating flatly because this project spent real time in it: a pixel comparison tells you how far one render lands from another. It never tells you whether the second is a legitimate rendering of the app at all. A screen can match to within 184 pixels out of 329,160 and still be a tree the port invented.

The construction

Three objects:

R is the origin, not the reference: it is unformalizable, so nothing can be proved against it, and if it stayed the reference the bounding would have bought nothing. F is the object of record. The claim to discharge is

⟦E⟧ = F

and R does not appear in it. Once F exists, R's job is finished.

The subset is a program, not a style guide. A file is freact iff freact-check exits 0 on it. Each rule is stated against the target construct it protects — no image in RView, no image in Eff, no image in Doc — which is what stops the bound from being taste. The withheld capabilities are literal closed sets in the checker's source.

And the capabilities are relocated, not deleted. They move into a closed effect algebra, so an application's authority becomes an enumerable list rather than whatever the ambient environment exposes. Today that list is twelve Eff constructors, and every one writes state:

setConst · setInput · pushDraft · pushInput · setFromRow · setFromScalar
pushInputWith · routeIfHex64 · lookupRoute · appendFromScalars
appendFromScalarsIfAbsent · setUniqueFromScalar

Not one names a host capability. A view layer built from these reads off as: this app's UI can change its own state and nothing else. That is a manifest derived from source.

The ledger — proven, trusted, unbuilt

A methodology that reports only its wins is a marketing document. Here is the whole board.

Proven, as theorems, for every app on the framework

refines_sound and refines_log (a refining world emits equal event traces and ends with the same committed log) · reversedWorld_refines (a genuinely different representation does refine, so the machinery is not vacuous) · applyEv_idem (re-applying a seen event is a no-op) · replayLog_append and App.ofMsgLog_append (reload equivalence) · store_ok and ui_over_store_ok · Layer.mono, pinned to exactly zero axioms by test/axiom-audit.mjs.

Per constructor, exactly two have their meaning pinned by proof rather than by test: pinned_perm and reversed_perm — ordering is a permutation, so a list cannot invent, drop or duplicate a row. That is the most security-relevant theorem in the system, because a UI that can silently drop a row from a transaction list is a UI that can lie to a signer.

Trusted, and the list is short — which is the point

1. freact-check itself. A JavaScript program with hand-written closed sets. If it misses a way to reach window, everything downstream inherits the miss. It is the TCB of the entire capability argument and has no theorem about itself.
2. The renderers, and the browser. No formal model here of CSS layout, font metrics or rasterization.
3. Part of the proof-to-artifact seam. The style emitter's byte-identity is proved — 741 obligations of the form example : toCss [...] = "..." := by native_decide — but native_decide trusts the compiler's evaluator, introducing Lean.ofReduceBool, which the axiom audit permits by name. Proved modulo a declared axiom, not kernel-checked. The whole-artifact fingerprint is a test.
4. R ≡ F can never be a theorem. R is opaque by necessity; that obligation permanently leaves the proof system and is discharged by the regression corpus.
5. Everything outside the model: key-handling correctness, supply chain, the Lean compiler, the machine.

Not built yet

F has not been produced. The subset is enforced at zero on four renderer files, and the reference application currently sits at:

node tools/freact-check.mjs --summary ../impl-super/apps/web/src/superapp/
# 2323 constructs outside the subset      (from 2404)

A denotation for the subset and a proved translation ⟦·⟧ : RView → Freact also do not exist. A gate not pointed at the code confines nothing — any version of this argument that omits that number is refuted by the first person who runs the tool.

Why the method converges

The distance is 2323 occurrences. Deduplicated across all 54 files it is nothing like that: no-dom-globals 387 → 6 distinct, no-timers-promises 360 → 7, no-untyped-state 161 → 1, no-effect-hooks 84 → 2, no-ref-dom 52 → 1.

The entire data-flow half — 1128 occurrences — is eighteen distinct constructs: six host globals, seven forms of asynchrony, and four React hooks whose job Doc and Eff already do. That is not 1128 problems; it is one missing layer, named in eighteen words, whose destination already exists.

Four rules keep the closing of that gap from becoming a licence:

1. When the app needs a construct the subset cannot say, the subset is too narrow. The application is working and tested; a rejection is evidence about the vocabulary. The order is expand the subset first, rewrite the app second, forbid last and rarely.
2. Every addition carries a denotation, not just a name. One constructor meaning "run this arbitrary JS" reinstates every excluded capability and would be invisible in a green build. This is not style advice; it is the security invariant, and the first thing a reviewer should check. A theorem over an escape hatch is not a theorem.
3. Attempt and fail — never audit. Every constructor added here was found by writing a value and having it not typecheck, not by reading the type and guessing what was missing.
4. Prove nothing moved before proving something new. An artifact fingerprint and a byte-identity corpus exist for exactly this.

The method has been run, and it holds

Six CSS properties had each been encoded as a single value wearing a constructor name (whiteSpaceNowrap), so white-space: normal was not a property the vocabulary lacked — it was one it had, spelled shut. Widening the six to enums, plus one enum short a member, moved the count 2404 → 2393 → 2365 → 2326 → 2323 across 55 rewritten call sites and 63 fixture literals — and the emitted artifact stayed byte-identical to its pin at every step, with 741 style obligations still discharging and a 23-step gate green.

That is the loop working as designed: the vocabulary grew, the app did not move, and both facts were checked rather than asserted.

What checks the rewrite — the corpus, not a camera

The specs do not drive a DOM. They drive typed state and named handlers:

alice.type('profile_name', 'Alice')       // a Doc scalar
alice.fire('saveProfile', null)           // a NAMED handler with a payload
assert.equal(String(alice.S.scalars.agent_installed || ''), '1')

That is precisely the interface being inside the subset means. So the moment R is in the subset, F has typed state and named handlers, and the existing corpus — 120 in-memory specs, 153 protocol checks — drives it without being rewritten. The seam is not something to build; it is the definition of the subset seen from the test side. A rewrite that keeps every spec green on both sides asserts data flow, behaviour, structure and position: four axes, where a pixel count is one, at one viewport, in one browser.

Composition with a formalized protocol

The ENC protocol is itself specified in Lean. Having both sides formalized is the unusual part, because it means the boundary can be stated: a protocol proof holds given well-formed messages, and app confinement is what bounds the sender. Composed, you get a claim neither has alone — the set of messages a client can emit is finite and derived from source.

Three seams composition does not close, stated so no one is surprised by them:

• The two proof systems do not currently meet. A protocol theorem quantifies over its message type; an app theorem over Eff. Those are different Lean types, and the app package does not depend on the protocol package. Composition needs a proved mapping, or the theorems are about different things and the chain does not join.
• What a user authorizes is not what the app sends. The app can be confined and the protocol sound while a signer still approves something they misread, because the pixels said one thing and the payload said another. pinned_perm is a fragment of exactly this; the general form needs the rendering chain, which is unformalized. This is the seam a WYSIWYS attack lives in.
• Trusted components stay trusted. The list above applies on both sides of the join.

The honest summary

You do not get "secure." You get: the set of things this UI layer can do is finite, derived from source, and checked at build time; here is the complete list of what you must still trust, and it is short.

That is a rare property, and it is the one worth claiming — because the other phrasing invites a reader to find the thing you forgot, and there always is one.

What would refute this document

# the render path is inside the subset — fails if any construct leaves it
node tools/freact-check.mjs --summary --max 0 \
  ../impl-super/sdk/emulator/{freact-tree,tree-pure,index,registry}.ts
 
# the distance from the reference app to the subset
node tools/freact-check.mjs --summary ../impl-super/apps/web/src/superapp/
 
# every style literal emits itself, byte for byte
lake env lean test/StyleFixtures.lean
 
# no keystone theorem gained a sorry or drifted from its expected axioms
node test/axiom-audit.mjs

If the first returns non-zero, the render path is not bounded. If the second stops falling, the method is not converging. If the third fails, the emitter moved. If the fourth fails, a theorem on this page is not what it says it is.