Margin-collapse experiment #

Runs docs/logic-layer.md -> "Experiment that settles it": CSS 2.1 8.3.1 margin collapsing written as Datalog rules, checked against a live three-engine vote and scored against deliberately broken copies of the rules (mutants), to decide whether a logic-programming layer earns its place as an oracle for intermediate layout facts.

Result: adopt. The rules agree with the browsers on every measurement (1195/1195), and on a seeded bug they usually know one level earlier than the geometry diff does — in one case the geometry vote never notices at all.

flowchart LR
  doc["case document"] --> facts["facts.rs<br/>tree shape + style"]
  facts --> rules["rules.rs<br/>Datalog (ascent)"]
  rules --> coll["collapsed<br/>(which margins adjoin)"]
  rules --> off["rel_top / rel_bottom<br/>(offsets)"]
  off --> vote{"matches the<br/>3-engine vote?"}
  coll --> fact{"mutant's collapsed<br/>differs?"}
  vote --> geom["geom-caught"]
  fact --> fc["fact-caught"]

What was built #

crates/logic, which depends on dom, layout and harness and runs without a browser:

• src/facts.rs — turns a parsed document and its box tree into Facts: tree shape (parent_of, first_child, last_child, next_sibling, no_children) plus margins, padding, borders, height (explicit, auto or unresolved), border-box sizing, and whether a box starts a new block formatting context. The box tree's root is treated as overflow: hidden, since there is nothing above it for a margin to escape into.
• src/rules.rs — MarginCollapseRules, an ascent program: 8.3.1's four adjoining cases, each gated by a feature_* relation a mutant can switch off; the collapsed value of a group (largest positive plus most negative, via max/min/sum aggregators); how much margin separates parent and child after escaping; a running max/min through chains of self-collapsing siblings (chain_pos/chain_neg); and 10.6.3's auto and border-box height. run() returns rel_top/rel_bottom (parent-relative offsets in 1/64 px) and collapsed.
• src/mutants.rs — 15 single-rule mutants, each switching off exactly one condition or picking one wrong arithmetic arm, so a caught mutant points at one spec condition.
• src/vote_check.rs — compares the rules' offsets with the vote's trustworthy OffsetY measurements within harness's tolerance.
• crates/harness/src/smt.rs (feature smt) — Z3 sampling backward from 4 of the 9 margin recipes, the ones defined by independent sign/range constraints.
• src/bin/crosscheck.rs, src/bin/mutation_score.rs produce the numbers below; tests/against_cases.rs runs the rules offline.
• The 1/64 px integer type these use now lives in crates/dom/src/px64.rs, shared with layout.

z3 is built through its gh-release feature (a prebuilt binary), because the bundled feature needs cmake, which this host lacks without root.

Agreement with the browsers #

227 cases (27 enumerated plus 200 seeded-random, seed 0xC0FFEE) against a live vote:

Overall: 1195/1195 trustworthy OffsetY measurements agreed, 0 with no verdict, 0 untrustworthy, 0 shape mismatches.

Mutant detection #

Per case, two checks: fact-caught — the mutant's collapsed relation differs from the correct rules' (no browser needed); geom-caught — the mutant's final offsets disagree with the vote for some box.

Enumerated (n=27) #

Seeded-random (n=200, seed 0xC0FFEE) #

SMT-sampled (n=20, seed 0xC0FFEE, 4 of the 9 margin-collapsing recipes) #

Fact-caught is at or above geom-caught for every mutant either check catches, and strictly above for most. parent-bottom-adjoin-off is the sharpest: the geometry vote misses it in all 227 cases, the collapsed fact catches it in 1/27 and 11/200. SMT inputs push drop-positive-margins and sign-flip to 20/20, against roughly a third on the fixed sets, because every sampled case has a nonzero adjoining margin to get wrong.

Closing the corpus gaps #

An earlier run left three mutants at 0 on every check. Three recipes closed them:

• zero-height-not-self-collapsing (treats height: 0 differently from auto): no recipe gave a self-collapsing box an explicit height: 0. recipe_collapse_self_collapsing_zero_height does; now 1/27 and 4/200 on both checks.
• box-sizing-ignored: collapsed never depends on border-box sizing, so the fact check cannot catch it by construction. The geometry check could, but the only border-box box had nothing after it. recipe_box_sizing_border_box_with_sibling adds a sibling; now 1/27 and 2/200 on geometry.
• sum-instead-of-min-negative (sums negative margins instead of taking the most negative): identical whenever a group has one negative margin, and no recipe had two. recipe_collapse_negative_sum puts a parent's and its first child's negative top margins in one group; now 1/27 and 5/200 on both checks.

Verdict #

docs/logic-layer.md's rule: "If the rules catch or localize mutants the geometry corpus misses, adopt them for the Phase 1 layout step." They do: 8 of 15 mutants are fact-caught strictly more often than geom-caught, and parent-bottom-adjoin-off is caught only by the facts. Adopt, narrowly, as an oracle for intermediate facts (docs/logic-layer.md -> "Verdict"). The rules now gate margin-collapse admission in the generation loop (crates/generation/src/margin_runner.rs).

Caveats #

• The 235-document Phase 0 baseline no longer regenerates; every number here is from the 227-case corpus (which grew from 222 through the three recipes above and two unrelated ones, recipe_border_width_without_style and recipe_display_none_with_child).
• SMT sampling covers 4 of 9 margin recipes; the other five are built by nesting, which backward solving does not suit (docs/logic-layer.md -> "Claimed benefit 2").
• The self-collapsing chain rules follow next_sibling only; a self-collapsing first child with a later sibling is not covered.
• A percentage or calc() height gives no border_box_height fact, so that box and those after it get no verdict — excluded, not counted as failures.
• Mutation scoring costs corpus size × mutant count; fine at 227 cases.