[P2] Add deterministic grammar-driven differential compiler tests with shrinking

[wsdt]

Audit: 2026-09-05, commit 2b3b1ee24da2.
Classification: Regression-prevention enhancement grounded in audit results and prior failures. Priority: P2.

Motivation and current evidence

The repository has extensive example, hostile-input, and property tests. tests/property_tests_v1.rs tests the language's property-generation surface; it is not a replacement for systematically generating compiler inputs across syntax/ownership combinations.

Earlier issues #21–#47 include backend local-indexing errors, checked-arithmetic mismatches, frontend stack failure, and superlinear analysis. During this audit, 72 independently generated small programs across i64/i32/u8/usize/f32/f64 produced the expected 42 in both the interpreter and ordinary Wasm runtime. That is useful focused evidence, not exhaustive correctness. No dedicated continuously exercised compiler fuzz target/job was found in the inspected tree/workflows.

Proposed first slice

Build a seedable typed grammar generator for the commonly admitted scalar subset, with shrinking that preserves enough structure to reproduce a discrepancy. Generate nested operands, parameterized helper calls, branches, loops with explicit bounds, shadowing/mutation, contracts, checked failure, and lazy evaluation.

Compare canonical parse-format-parse stability and graph identity, verifier/HIR agreement, interpreter outcomes, native O0/O2, and Wasm outcomes only where each target admits the same profile. Normalize expected arithmetic/contract failures; distinguish capacity rejection from semantic disagreement. Add an invalid-input mutation lane for the parser and protocol boundaries, with strict process/time/memory bounds.

Acceptance criteria

• Fixed seeds run in PR CI, while a larger bounded campaign can run separately.
• A discrepancy produces source, seed, compiler commit, toolchain identities, exact commands, expected/observed outcomes, and a minimized case.
• Imported earlier regression cases remain deterministic seeds.
• Unsupported profiles and absent provisioned tools are explicit outcomes, never silently counted as parity passes.
• Failure injection proves the differential checker notices a wrong backend value, incorrect failure selection, and an abort.
• Add work/allocation counters or scaling fixtures to catch complexity regressions without flaky global time thresholds.
• No fuzzer-generated file is executed with ambient network, filesystem, process, or signing effects.

Reuse existing backend/parity harness modules rather than adding hundreds of standalone integration binaries. The first tranche can be scalar-only; owned cleanup and task schedules should be separate incremental extensions.

Agent handoff

Recheck the working revision and existing issues first. Read AGENTS.md, the relevant completion-matrix row, and the owning versioned specifications. This proposed slice must preserve canonical source, independent replay, precise target admission, and separately granted authority. Place regressions in the existing owning harness. Execute the applicable quality gates and record what actually ran; unrun native, hosted, or device evidence must stay unpromoted.

Audit revision scope

Runtime observations in this ticket belong to commit 2b3b1ee. A final source-tree comparison against e1c5b56 was used to check for obvious superseding changes. That later snapshot was not rebuilt or exhaustively retested. Reproduce on the intended fixing revision before implementation.

Audit ID: SPX-AUDIT-20260905-20

Suggested scope: M then L. Dependencies: None required.

[wsdt]

First tranche landed in dd4905fe (on main as 3f7e4d47).

Added as a module of the existing tests/scalar_status_backend_equivalence.rs harness, not a new top-level binary, under tests/scalar_status_backend_equivalence/differential/:

• grammar.rs — seedable typed generator (SplitMix64, no new dependency) over i64/i32/u8/bool: nested operands, parameterized helper calls into a strictly-lower-index DAG, if/else, bounded counted while, let mut + assignment, requires/ensures, deliberate zero divisors, and lazy &&/||. A Coverage struct is asserted so a refactor cannot quietly narrow what is generated.
• shrink.rs — structure-preserving shrinker with a fixed predicate budget: drop cases, drop unreferenced helpers, drop statements and contract clauses, reduce loop bounds, collapse an expression to a neutral literal or one of its own same-typed operands.
• observe.rs — a closed observation vocabulary (Returned / Failed{domain,code} / Capacity / Refused / Aborted) and lane status (Observed / Unavailable{reason} / Aborted{detail}), with frontend (parse → verify → canonical parse-format-parse stability → graph JSON and revision identity → HIR resolve/validate) and reference-interpreter lanes.
• backends.rs — native C11 O0/O2 and Core-Wasm/Node lanes that report rather than assert.
• report.rs — discrepancy reports carrying seed, source, compiler commit, compiler version, rustc/clang/node identities, exact per-lane commands, lanes compared, lanes unavailable with reasons, per-case expected/observed, and the minimized module.
• 16 fixed PR seeds wired into .github/workflows/ci.yml, a 64-seed frontend+interpreter sweep, and an #[ignore]d bounded campaign via SEMAPRAX_DIFFERENTIAL_SEEDS.

The criterion that makes the harness trustworthy: failure injection

The injection tests assert exact classes and exact expected/observed strings. To show they are not vacuous, the checker was temporarily sabotaged in three separate places (then restored; tree verified clean):

Sabotage	Result
compare() swallows every per-case disagreement	wrong-value, failure-selection and lane-abort tests all FAILED (4 passed, 3 failed)
LaneStatus::Aborted treated as agreement	both abort tests FAILED (5 passed, 2 failed)
LaneStatus::Unavailable pushed into compared	the absent-tool test FAILED

The three required wrongnesses concretely:

1. Wrong backend value — a mutant source (helper(41) → helper(42)) compiled and executed by a real lane and presented under the NativeO0 label: reported value_disagreement, expected returned i64 42, observed returned i64 43.
2. Incorrect failure selection — 7 / 0 → 7 % 0 gives expected semaprax.arithmetic.v1#4 / observed #6; helper(-1) → helper(0) gives expected semaprax.contract.v1#1 / observed returned i64 1. Both classified failure_selection_disagreement and asserted as exact tuples.
3. Abort — three ways, including a real process that really exits non-zero (launched with an argument libtest rejects) mapped through the real transcript_status, and a real native link failure asserted to produce Aborted, never observations.

Stated plainly in the code and here: the value and failure-selection injections use a mutant source executed by a real lane and relabelled — they are not an actually miscompiled backend binary. That is the strongest injection reachable without shipping a deliberately broken backend, and it exercises generation → execution → envelope decode → normalization → compare.

It detects the real open divergence in #75

Pointed at #75's nine-line record module, the checker reports:

interpreter: Refused { code: "SPX-F102", detail: "interpreter admission failed (record_construction)…" }
findings:    admission_disagreement, case app.main, lane NativeO0,
             expected "refused SPX-F102: …", observed "returned i64 42"
unavailable: (CoreWasm, "SPX-W115: Public Scalar Export Profile v1 does not admit
             authored resource, record, or variant declarations")

It finds the divergence and records the Wasm lane as unavailable with its exact reason rather than counting it as parity. #[ignore]d so fixing #75 does not turn the tree red; #75 itself is untouched.

Coordinator-verified

cargo test --locked -p semaprax --test scalar_status_backend_equivalence --test harness_isolation -- --test-threads=1 with SEMAPRAX_REQUIRE_SCALAR_BACKEND_EQUIVALENCE=1 → 16 passed, 0 failed, 2 ignored (174.89 s) and 2 passed, 0 failed, re-run by me after rebasing onto current main. cargo fmt --all --check clean.

Both provisioned tools were present and both lanes really ran (Apple clang 21.0.0, node v24.3.0); the fixed-seed test prints every backend lane ran for every fixed seed. Bounded campaigns of 128 and 96 seeds agreed across interpreter, native O0, native O2 and Core-Wasm — no new compiler bug in the scalar subset. Shrinking: seed 0x24, 2545 bytes → 207 bytes in 13 steps, 44 predicate calls. Scaling counters are exactly linear (144−76 == 2·(76−42)), asserted as equality with no wall clock.

Two real language rules the generator had to respect

• % is admitted on i64 only; on i32/u8 it is SPX-T208. The operator table is now per type.
• SEMAPRAX does not admit shadowing — rebinding a live local is SPX-T209. This issue names "shadowing/mutation"; only mutation is expressible. The generator never emits shadowing, Coverage.shadowed_bindings is asserted to stay 0, and a hostile fixture pins SPX-T209 so admitting it later must be deliberate.

Acceptance criteria NOT satisfied

• "Imported earlier regression cases remain deterministic seeds" — not done; Wasm backend: scratch locals ignore the parameter offset, producing invalid modules (i32) and silent wrong results (u8/usize) #21–Verifier accepts usize + 1 with an unsuffixed literal; backends fail with internal SPX-H006 inconsistent resolved types #47 cases were not re-expressed as seeds.
• "An invalid-input mutation lane for the parser and protocol boundaries, with strict process/time/memory bounds" — only one hostile fixture. No systematic mutation lane and no per-process rlimits; bounds present are structural (fixed shape limits, interpreter fuel, fixed shrink budget).
• The routed quality profile was not run. scripts/quality.sh --plan changed resolved to effective full (workspace check/clippy/test/doctest/rustdoc, release build, package, example checks) because ci.yml and tests/* route as unmapped-or-wide; that needs well over 10 GB and this machine has ~1.7 GB free. Unrun evidence, not a pass — the owning harnesses were run directly instead.
• The scalar subset is narrower than "commonly admitted": usize, char, f32, f64, string, [u8; N] and match are not generated. Owned cleanup and task schedules are out, as this issue permits.
• One documented -Werror omission: the generated-C differential lane compiles with -Wall -Wextra but not -Werror, since a warning in generated code is not the subject of a differential comparison. The pre-existing fixed fixture keeps -Werror.

One allowlist entry, extended not weakened

tests/harness_isolation.rs flags any harness module containing current_exe. differential/injection.rs was added to its SELF_INVOKING list — the mechanism that gate documents — because the call selects no test at all: it passes --test-threads=0, which libtest rejects, purely to obtain a real non-zero-exit process. I verified that in the source. There is no selector for a harness prefix to break, the entry is keyed by exact path so it cannot spread, and the gate's logic is unchanged and still fires for any other module.

Follow-on tranches (imported regression seeds, the parser/protocol mutation lane, and the wider scalar set) remain open work; the issue's own framing is "M then L".