# 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.

```mermaid
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:

| Category | Agreed/Checked |
|---|---|
| WidthAuto | 28/28 |
| FillAvailable | 28/28 |
| MarginAutoLeft | 40/40 |
| MarginAutoRight | 24/24 |
| MarginAutoBoth | 32/32 |
| OverConstrained | 52/52 |
| ExplicitWidth | 176/176 |
| MinMaxClamp | 28/28 |
| MinExceedsMax | 52/52 |
| PercentageWidth | 32/32 |
| PercentageHeight | 28/28 |
| PercentageHeightAutoParent | 52/52 |
| CollapseSiblings | 30/30 |
| CollapseParentFirstChild | 70/70 |
| CollapseParentLastChild | 60/60 |
| CollapseSelfCollapsingEmpty | 54/54 |
| CollapseThroughChain | 126/126 |
| CollapseNegative | 105/105 |
| CollapseBfcRoot | 60/60 |
| BoxSizingBorderBox | 59/59 |
| BoxSizingContentBox | 32/32 |
| PaddingBorderPercentage | 28/28 |
| NestingDepth | 280/280 |
| FixedBox | 107/107 |

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)

| mutant | fact-caught | geom-caught |
|---|---|---|
| bfc-blocks-top-off | 4/27 | 4/27 |
| bfc-blocks-bottom-off | 2/27 | 1/27 |
| parent-top-adjoin-off | 3/27 | 3/27 |
| parent-bottom-adjoin-off | 1/27 | 0/27 |
| sibling-adjoin-off | 4/27 | 1/27 |
| self-collapsing-off | 3/27 | 2/27 |
| self-collapsing-ignores-children | 4/27 | 1/27 |
| zero-height-not-self-collapsing | 1/27 | 1/27 |
| box-sizing-ignored | 0/27 | 1/27 |
| ignore-negative-sign | 2/27 | 2/27 |
| drop-negative-margins | 2/27 | 2/27 |
| drop-positive-margins | 8/27 | 7/27 |
| sum-instead-of-max-positive | 6/27 | 5/27 |
| sum-instead-of-min-negative | 1/27 | 1/27 |
| sign-flip | 9/27 | 8/27 |

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

| mutant | fact-caught | geom-caught |
|---|---|---|
| bfc-blocks-top-off | 31/200 | 31/200 |
| bfc-blocks-bottom-off | 19/200 | 8/200 |
| parent-top-adjoin-off | 23/200 | 23/200 |
| parent-bottom-adjoin-off | 11/200 | 0/200 |
| sibling-adjoin-off | 25/200 | 15/200 |
| self-collapsing-off | 15/200 | 9/200 |
| self-collapsing-ignores-children | 34/200 | 11/200 |
| zero-height-not-self-collapsing | 4/200 | 4/200 |
| box-sizing-ignored | 0/200 | 2/200 |
| ignore-negative-sign | 19/200 | 19/200 |
| drop-negative-margins | 19/200 | 19/200 |
| drop-positive-margins | 63/200 | 52/200 |
| sum-instead-of-max-positive | 29/200 | 25/200 |
| sum-instead-of-min-negative | 5/200 | 5/200 |
| sign-flip | 68/200 | 57/200 |

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

| mutant | fact-caught | geom-caught |
|---|---|---|
| bfc-blocks-top-off | 6/20 | 6/20 |
| bfc-blocks-bottom-off | 0/20 | 0/20 |
| parent-top-adjoin-off | 6/20 | 6/20 |
| parent-bottom-adjoin-off | 0/20 | 0/20 |
| sibling-adjoin-off | 11/20 | 8/20 |
| self-collapsing-off | 6/20 | 6/20 |
| self-collapsing-ignores-children | 6/20 | 0/20 |
| zero-height-not-self-collapsing | 0/20 | 0/20 |
| box-sizing-ignored | 0/20 | 0/20 |
| ignore-negative-sign | 3/20 | 3/20 |
| drop-negative-margins | 3/20 | 3/20 |
| drop-positive-margins | 20/20 | 20/20 |
| sum-instead-of-max-positive | 8/20 | 8/20 |
| sum-instead-of-min-negative | 0/20 | 0/20 |
| sign-flip | 20/20 | 20/20 |

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.