Would a logic-programming layer earn its place? #

Answers the open question in roadmap.md "Whether the thesis holds at all" on a logic-programming layer in the substrate. Research as of September 2026.

Verdict #

Adopt narrowly, as an oracle for intermediate facts about margin collapsing and box existence; defer everything else; reject Prolog and miniKanren as the substrate. The roadmap is right that such a layer can never be the engine, and wrong that margin collapsing is the obstacle — it is the best candidate. The real obstacles are floats, inline layout, and the cost of keeping rules in step with the spec. For generating inputs backwards, an SMT solver is the right tool, not a logic program.

Claimed benefit 1: a second implementation for differential testing #

Prior art says this works when the formal model is cheap to keep in step with the spec or is derived from it mechanically.

JEST and ESMeta treat ECMA-262 as an additional implementation; JEST found 44 engine bugs and 27 spec bugs, and ESMeta now runs on ECMA-262 and Test262 pull requests. That works because ECMA-262's algorithms are structured pseudo-code compiled mechanically. CSS prose (CSS 2.1 §10.3.3, §8.3.1) is not, so an encoding would be hand- or model-written.
KJS passed all 2,782 core ES5.1 conformance tests and exposed untested areas of the suite; new tests written from that found bugs in V8, WebKit and SpiderMonkey. That is a coverage benefit more than a cross-check.
Cassius formalized a CSS 2.1 fragment (box model, margin collapsing, floats, positioning) as linear real arithmetic solved by Z3 and disagreed with Firefox on 6 of 2,075 tests, at the cost of about 7.4k lines of Racket for 42 properties. Its value was verifying pages across all viewport sizes (VizAssert), not checking an engine.
The Wasm reference interpreter was dropped as Wasmtime's fuzzing oracle because it would not trade spec closeness for speed; a verified interpreter replaced it.
Independence is limited. Versions written independently from one spec fail together far more often than chance (Knight and Leveson, 1986). If the same model writes both the Rust and the rules from the same text, their misreadings tend to coincide.

For geometry visible from outside, rules add little beyond three browsers plus WPT. The real gap is intermediate facts the geometry dump cannot show: which margins adjoin, which box establishes a new block formatting context, which boxes exist before anonymous boxes are flattened. A wrong adjoining set can produce correct geometry by coincidence on one case and fail on another, and the browser diff reports only the resulting offset. A rule layer emitting those facts attributes failures below the level of a node.

Claimed benefit 2: running rules backwards to generate inputs #

crates/harness/src/cases.rs already does by hand what a constraint solver does: each recipe draws from fixed value pools chosen so its defining relation holds. The measured weakness is which values are picked (the enumerated set found no disagreements where the seeded-random set found six), not which branches are reached.

The width equation, min/max clamping and percentages are linear inequalities over five to ten variables, which SMT solves instantly once percentage-times-unknown is fixed on one side. Prolog's is cannot run backwards; CLP over integers works with lengths in 1/64 px units. miniKanren arithmetic is slow.
Structural cases (margins collapsing through several empty blocks, stopped by a new block formatting context) are the legitimate case for relational search, but running a tree relation backwards blows up quickly; whole-page SMT verification took hours before modular proofs (Troika). Bounded enumeration is the practical form.
Float placement is an optimization and line breaking needs shaping; backwards search is not tractable there at useful sizes.
A new branch still needs someone to encode it as a rule, which costs about what writing a recipe does.

Cheaper alternatives: sample values from each recipe's constraint region (SMT or rejection sampling), and use branch coverage of the generated Rust with coverage-guided fuzzing.

Claimed benefit 3: a formalization that survives regeneration #

It survives engine regeneration but not spec change, and becomes a second artifact to keep current; per-section provenance hashes already detect spec change. The narrower lasting value is a machine-checkable case analysis that could drive cases.rs Category and check recipes for exhaustiveness.

Which spec surface is rule-shaped #

Area	Fit	Notes
Selector matching	Excellent	Stylo is linked, so no current payoff
Cascade	Good	Same
Box tree generation	Good	Pairs with the box-existence check in Phase 1
Margin collapsing	Best in layout	§8.3.1 defines adjoining as a recursive, transitive relation; engines implement it imperatively, the spec states it declaratively
Width equation, clamping	Linear arithmetic	Better as SMT or plain Rust
Floats, clearance	Poor	Order-dependent optimization
Inline layout, line breaking	Not rule-shaped	Depends on shaping

Forward Datalog with Rust expressions can use the engine's own 1/64 px fixed-point type, so arithmetic costs nothing going forward; the awkwardness is only in running backwards.

Implementation options #

ascent — the pick: in-process macro-compiled Datalog with aggregates, lattices, stratified negation, arbitrary Rust in rules, and a parallel mode.
crepe lacks aggregates, which makes collapsed-margin computation awkward.
datafrog is a bare join engine. Soufflé is out of process and C++. egglog pays off only with equivalence reasoning. scryer-prolog embeds but has no API stability promise and carries the cut and ordering leaks. miniKanren is slow on arithmetic. The K framework is heavy and outside Rust.
For the backwards direction, Z3 as Cassius used; answer-set programming only if bounded structural enumeration becomes necessary.

Experiment that settles it (about a week, inside the harness) #

Encode §8.3.1 (the adjoining relation and the collapsed value: the largest positive margin plus the most negative) with blocking by new block formatting contexts, in ascent, over the tree cases.rs builds, computing each box's parent-relative block offset in 1/64 px fixed point.
Run it over the recipe corpus against a three-engine vote. It passes if it agrees on every trusted measurement. (The original 235-document set no longer regenerates; the run used the corpus as it stood.)
Seed 20–30 single-rule mutants (drop the block-formatting-context condition, drop self-collapsing, ignore the sign of negatives) and measure how many each input set catches: enumerated, seeded-random, and SMT-sampled within each recipe's constraints.

If the rules catch or localize mutants the geometry corpus misses, adopt them for the Phase 1 layout step. If SMT-sampled inputs catch materially more, add constraint-based value selection to cases.rs with no logic layer. If neither, close the question.

Run: docs/margin-collapse-experiment.md. Verdict: adopt — the rules agreed with a live three-engine vote on all 1195 trustworthy measurements over the 227-case corpus (1235 on an earlier 225-case run), and localized several mutants (most clearly parent-bottom-adjoin-off) that the geometry vote missed outright. The rules now gate margin-collapse admission in the generation loop.