freact — the React subset that bridges to encapp

encapp emits RView, Eff and Doc from Lean. A React application is written in a language with closures, hooks, and arbitrary JavaScript. Those two things cannot be compared until one of them is made sayable in terms of the other.

freact is that middle term: the fragment of React that a verified compiler can carry to encapp's types. It is not a framework, and it is not a style guide. It is a bound, and the bound is a program.

Why bound React at all

Call the three objects:

R is unformalizable. A hook can run any effect at any time, a handler can close over any mutable value, a component can compute its children's types. There is no denotation you can write down for that, which means nothing can be proved against it — and if R stayed the reference, the only available check would be a screenshot.

That is the trap this project spent real time in, and it is worth stating plainly: a pixel comparison tells you how far E's render lands from R's, at one viewport, in one browser. It never tells you whether E is a legitimate rendering of the app at all.

So R is the origin, not the reference. F is the object of record. The claim to prove is

⟦E⟧ = F

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

The definition is a program

A subset nobody can check is not a subset. So the boundary is mechanical:

node tools/freact-check.mjs --summary <files…>     # exit 0 ⟺ every file is freact

A file is freact if and only if that exits 0. Nothing else defines it — not a convention, not a review, not this page.

Each rule is stated against the target construct it protects, which is what keeps the bound from being taste:

The style rule does not restate the grammar — it imports tools/style-parse.mjs, the same module that migrated the Lean app, so one vocabulary governs both authoring surfaces. Without that module the rule reports nothing rather than guessing, because a checker that invents its own list is the second vocabulary it exists to prevent.

Where the bridge actually stands

The render path is freact and its surface is enforced at zero:

node tools/freact-check.mjs --summary --max 0 \
  ../impl-super/sdk/emulator/{freact-tree,tree-pure,index,registry}.ts   # 0

The reference application is a different matter, and this is the honest number:

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

F has not been produced. The checker had only ever been pointed at four emulator files, so the reference operand of ⟦E⟧ = F does not exist yet. Two further pieces are also unbuilt: a denotation for the subset, and a translation ⟦·⟧ : RView → Freact with the equality proved constructor by constructor. Today, exactly two constructors have their meaning pinned by proof rather than by test — pinned_perm and reversed_perm, which guarantee that ordering is a permutation and so cannot invent, drop, or duplicate a row. That is the shape the rest needs.

The count is occurrences, not work

Deduplicated across all 54 files, the shape is nothing like the total:

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

await, at 255 occurrences, is the single largest cause in the corpus — and it is not a timer, it is asynchrony itself. fetch, new Promise, setTimeout, setInterval, requestAnimationFrame and queueMicrotask are its special cases.

How the vocabulary grows

When R needs a construct the subset cannot say, the subset is too narrow — R is the working, tested application, and a rejection is evidence about the vocabulary, not about the app. The order is: expand freact first, rewrite R second, ban last and rarely.

Three rules keep that from becoming a licence:

1. Every addition carries a denotation, not just a name. A constructor meaning "run this arbitrary JS" would admit the construct and destroy the theorem it exists to support. A theorem over an escape hatch is not a theorem.
2. Attempt and fail, do not audit. Every constructor added in this project was found by writing the value and having it not typecheck — never by reading the type and guessing what was missing. The eight constructors that closed the raw-CSS work were found exactly this way.
3. Prove nothing moved. An artifact fingerprint and a byte-identity fixture corpus exist for this. Two recent expansions moved the count 2404 → 2393 → 2365 → 2326 → 2323 across 55 rewritten call sites and 63 fixture literals, and the emitted page stayed byte-identical at every step.

A worked example of the method. Six properties — white-space, flex-direction, font-style, user-select, object-fit, resize — 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 a property it had, spelled shut. Two hundred lines up in the same file, Cursor was already the right shape. Widening the six to enums closed 28 occurrences and applied a pattern the file already contained, rather than designing anything.

What checks the rewrite

Not a screenshot. The existing regression corpus, run against both R and F.

The specs do not drive a DOM — they drive Doc 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 a Doc and named handlers, and the corpus drives it without being rewritten — the seam is the definition of the subset, seen from the test side. A rewrite that keeps 120 in-memory specs and 153 protocol checks green on both sides asserts data flow, behaviour, structure and position: four axes, where a pixel count is one.

Commands that would refute the claims on this page

# the render path is freact — fails if any construct leaves the subset
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
 
# the two renderers agree on the same tree, 224 fixtures
node --test ../impl-super/apps/web/test/dom/freact-diff.test.mjs

Note what the last one does and does not say. It pushes the same resolved node through renderToStaticMarkup(<RenderNode/>) and toHtml(renderTree(…)), so it proves the two renderers agree on whatever tree they are handed. It says nothing about whether two trees are the same tree. That comparison is the work above, and it is not built yet.