|
| 1 | +# 0023 — The first vertical slice: corpus harness and the representation it pins |
| 2 | + |
| 3 | +**Status:** proposed · 2026-07-30 · adversarially reviewed the same day. |
| 4 | +The review verified the WasmGC mechanics it attacked (nullable `ref.eq`, |
| 5 | +`if` with a ref result, singleton identity surviving `wasm-opt -O3`) and |
| 6 | +changed four things, marked *(review)* below: analyzer-side namespace |
| 7 | +isolation, a JVM-message column in the trap table, the i31 rule extended |
| 8 | +from literals to intermediates and results, and an overclaimed truthiness |
| 9 | +example dropped. |
| 10 | + |
| 11 | +## The question |
| 12 | + |
| 13 | +`0022` decided S3's shape and named its first unit: a corpus harness plus |
| 14 | +scalar entries running analyze → emit → both engines, forcing none of the |
| 15 | +open decisions (dev-loop format, boxed-i64 lane, throw representation). |
| 16 | +Building it still requires pinning things `0022` deliberately left to "the |
| 17 | +first corpus entry": the concrete corpus artifacts, and the emitter's value |
| 18 | +representation for everything the slice touches. |
| 19 | + |
| 20 | +## The decision |
| 21 | + |
| 22 | +### The harness (implements `0022` B, adds nothing to it) |
| 23 | + |
| 24 | +- **`corpus/s3.edn`** — the committed corpus. An entry is |
| 25 | + `{:id "…" :forms [f1 … fn]}`; forms evaluate in order, the last one's |
| 26 | + value is the entry's result. Day-one entries are scalar (`0022` B.3). |
| 27 | +- **`test/cljwit/corpus_test.clj`** — the differential oracle, an ordinary |
| 28 | + `clojure.test` so it is in `bb check` from the first entry |
| 29 | + (CI-mandatory, `0022` B). The oracle lane evaluates each entry in a |
| 30 | + fresh, discarded namespace in the test JVM — which *is* real `clojure`, |
| 31 | + satisfying the isolation rule without a second process. **Analysis is |
| 32 | + isolated the same way** *(review)*: each `analyze-forms` call gets its |
| 33 | + own gensym'd namespace and `create-var` interns only there, so a `def` |
| 34 | + in one entry can never resolve during another entry's analysis — the |
| 35 | + oracle-lane leak rule, one lane over. Compiled lanes: emit WAT → |
| 36 | + `wasm-tools parse` → `wasmtime run --invoke entry` and |
| 37 | + `node corpus/run.mjs`, in both `:dev` and `:prod` modes. |
| 38 | + `--invoke`'s printed result is a warned-experimental interface — the |
| 39 | + same one `bench/s0` already stands on; the pinned toolchain makes that |
| 40 | + acceptable, and a format change fails every entry loudly at once |
| 41 | + *(review)*. On a machine without the `wasmtime` CLI on PATH that one |
| 42 | + lane skips with a printed line — the exact trade the FFM tests already |
| 43 | + make with `CLJWIT_WASMTIME_LIB` — while the oracle, analysis, emission |
| 44 | + and the V8 lane always run; CI runs inside the flake, where nothing |
| 45 | + skips. |
| 46 | +- **`corpus/trap_table.edn`** — the numbered trap↔class artifact |
| 47 | + (`0022` B.5). Row 1: `java.lang.ArithmeticException` ↔ the engines' |
| 48 | + division traps, exercised by a corpus entry in the same commit. |
| 49 | + A row carries the **JVM message substring, not just the class** |
| 50 | + *(review)*: `ArithmeticException` also means long overflow, which is |
| 51 | + not a division trap, and class-only matching would equate them the day |
| 52 | + the boxed lane lands. Stack exhaustion's row lands with the first |
| 53 | + depth-sensitive entry, not before (same-commit coverage, `0022` B.1). |
| 54 | +- **Value comparison** is structural: the oracle's `pr-str` and the wasm |
| 55 | + lane's printed integer both go through `clojure.edn/read-string` and |
| 56 | + compare with `=`. An oracle value that `pr-str`→`read-string` cannot |
| 57 | + round-trip is a corpus lint error (`0022` B.4) — this falls out of the |
| 58 | + mechanism rather than being a separate linter. |
| 59 | + |
| 60 | +### The representation (the new pins) |
| 61 | + |
| 62 | +1. **Every Clojure value is `(ref null eq)`.** One uniform type; no |
| 63 | + unboxing pass in the slice. Refinement is a prod-mode optimisation |
| 64 | + later, per binaryen's lowering guidance already cited in `0022` A. |
| 65 | +2. **Fixnums are `i31`** — B3's measured substrate, verbatim. A literal |
| 66 | + outside i31's signed 31-bit range is a **compile error** in the slice: |
| 67 | + that value belongs to the boxed-i64 lane, which is open (`0022` C) |
| 68 | + precisely because it is unmeasured. Runtime arithmetic computes in |
| 69 | + i64 and re-boxes through one guard; a result outside i31 hits |
| 70 | + `(unreachable)` — the same shape B3 measured, and the same honesty: |
| 71 | + the slow path exists and no corpus entry may reach it yet. The |
| 72 | + corresponding **corpus authoring rule covers intermediates and |
| 73 | + results, not just literals** *(review)*: `(quot -1073741824 -1)` or an |
| 74 | + overflowing left-fold would compile, run, and trap where Clojure's |
| 75 | + longs succeed. The harness classifies `unreachable` and cast-failure |
| 76 | + traps as "entry out of contract — fix the entry", so a violated |
| 77 | + authoring rule cannot read as a compiler divergence. |
| 78 | +3. **nil is the null reference.** `(ref null eq)` locals default to it, |
| 79 | + `ref.is_null` is the nil test, and no allocation or global is spent |
| 80 | + on it. |
| 81 | +4. **false and true are two singleton empty-struct globals**, distinct by |
| 82 | + identity (`ref.eq`), not by type. Truthiness — the thing `0022` D said |
| 83 | + the first corpus entry pins — is |
| 84 | + `(not (or (ref.is_null v) (ref.eq v $false)))`, emitted as a call to a |
| 85 | + runtime `$truthy`. `(if 0 …)` is therefore truthy by construction, |
| 86 | + matching Clojure with no special cases — and the shape extends to any |
| 87 | + future non-nil, non-false value, though only fixnums can demonstrate |
| 88 | + it while no other representation exists *(review)*. |
| 89 | +5. **The entry protocol**: each entry compiles to one self-contained |
| 90 | + module exporting `entry : [] -> [i64]`, the last form's value |
| 91 | + unwrapped by `ref.cast (ref i31)` + `i31.get_s`. A non-fixnum result |
| 92 | + traps the cast — which is the mechanical form of `0022` B.3's rule |
| 93 | + that non-scalar entries wait for printing. |
| 94 | +6. **Intrinsics, not a core library**: `+ - * quot <` compile from |
| 95 | + `:invoke`-of-`#'clojure.core/…` (the `:inline`-off contract from |
| 96 | + `0022` E) to runtime functions; `+ - *` fold n-ary to binary with |
| 97 | + Clojure's identities, `<` is binary-only for now. Any other var is a |
| 98 | + loud compile error naming the var. |
| 99 | +7. **Both modes exist from day one and currently emit identical bytes.** |
| 100 | + `:dev`/`:prod` thread the whole pipeline and all four compiled lanes |
| 101 | + run, but nothing in the slice's forms diverges by mode — divergence |
| 102 | + starts with `def`/var emission (`0022` D). Stated here so nobody reads |
| 103 | + four green lanes as mode coverage that does not exist yet. |
| 104 | + |
| 105 | +## Why |
| 106 | + |
| 107 | +- Every mechanism above is inherited from something already measured or |
| 108 | + decided: the WAT→`wasm-tools`→both-engines pipeline is `bench/s0`'s, |
| 109 | + the i31 substrate and the `unreachable` slow path are B3's, the oracle |
| 110 | + contract is `0022` B, the analyzer front end is `0022` E's spike grown |
| 111 | + into `src/`. |
| 112 | +- The pins themselves are chosen for *reversibility*: null-nil, singleton |
| 113 | + false, and `$truthy` are each one emitter function; the boxed lane can |
| 114 | + replace the `unreachable` arm without touching entry, corpus, or |
| 115 | + comparison machinery. |
| 116 | + |
| 117 | +## Alternatives rejected |
| 118 | + |
| 119 | +- **false as a reserved i31 value.** Free identity test, but it steals a |
| 120 | + value from fixnum space and makes every arithmetic fast-path guard also |
| 121 | + a not-false guard. The sibling's lesson that dispatch guards dominate |
| 122 | + makes polluting the fixnum domain the wrong default. |
| 123 | +- **nil as a singleton struct, refs non-nullable.** Binaryen's tips favor |
| 124 | + non-nullable fields, but that is a prod-mode refinement; nullable |
| 125 | + locals need no explicit init, `ref.is_null` is one instruction, and |
| 126 | + nothing measured yet distinguishes them. Revisit when the optimiser |
| 127 | + lane exists. |
| 128 | +- **Running compiled lanes through `cljwit.host` instead of spawning |
| 129 | + engines.** Tempting reuse, but corpus modules are core modules, not |
| 130 | + components (`0007`: components are S4's boundary), `cljwit.host` speaks |
| 131 | + components only, and the V8 lane has no host at all. `bench/s0`'s spawn |
| 132 | + mechanism is validated and already fails on wrong answers. |
| 133 | +- **A standalone corpus runner (`bb corpus`) instead of a test in the |
| 134 | + gate.** `0022` B's own clause: mandatory-ness alone saved the sibling |
| 135 | + nothing, but an opt-in lane is strictly worse. The gate is where the |
| 136 | + oracle lives; a convenience runner can come later if iteration wants it. |
| 137 | +- **Waiting for `fn`/`def` so the slice "does more".** The harness is the |
| 138 | + deliverable; every form it carries today has its corpus lines in the |
| 139 | + same commit, and `fn`'s multi-arity contract (`0022` D) is its own |
| 140 | + unit. |
| 141 | + |
| 142 | +## What would falsify this |
| 143 | + |
| 144 | +- The boxed-lane benchmark (`0022` C) pricing the i31 split out — the |
| 145 | + fixnum pin and the `unreachable` arm both reopen. |
| 146 | +- A corpus entry whose truthiness the `$truthy` shape cannot express — |
| 147 | + none is known; finding one would mean the false-singleton choice leaks. |
| 148 | +- The trap table failing to distinguish two JVM exception classes that |
| 149 | + map to one wasm trap message — expected eventually (e.g. cast failure |
| 150 | + vs NPE); the table gains columns or the entry gains a numbered |
| 151 | + divergence when it happens. |
| 152 | +- Engine trap messages changing across pinned-toolchain upgrades — the |
| 153 | + table rows carry the exact strings, so this fails loudly in the gate. |
0 commit comments