Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

RFD 0055 — The conformance corpus: a standing golden differential-correctness gate

  • State: accepted
  • Depends on: RFD 0048 (the test atom — the in-language golden vehicle), RFD 0050 (documentation architecture / “every package compiles and runs in CI”), RFD 0018 / RFD 0020 (the reasoner and Engine::evaluate the corpus exercises), RFD 0005 (refined collections / field projection — the keystone bug’s home), RFD 0025 (mutation delta-guard — the write-path goldens)
  • Tracks: issues #1024, #1025, #1026; guards #1014, #1015, #991, #1001, #1005, #996
  • Prior art: differential testing (McKeeman 1998); metamorphic testing (Chen et al.); golden / characterization tests (Feathers); SQL logic tests (SQLite’s sqllogictest); the project’s own Lean batched oracle (engine_agrees_with_batched_lean_oracle) and pipeline differential audit (pipeline_differential_audit_over_corpus)

Question

A 2026-06 maturity audit and a real-ontology dogfood found roughly nine silent-wrong engine bugs — wrong answer, no error — that 3,200+ unit tests, the Lean differential oracle, and the pipeline differential audit all passed over. The field-projection P0 (#1014) is the archetype: a field read aliasing across two co-classifying concepts with same-named fields, whose regression test had been #[ignore]d and whose shape no oracle covered.

Why did every oracle miss them, and what gate closes the class?

Context

Every existing correctness oracle attaches at or below Engine::evaluate:

  • the Lean batched oracle and the golden replay vectors check the reasoner over already-elaborated programs;
  • the pipeline differential audit checks direct ≡ pipeline ≡ frozen — three evaluation routes over the same compiled rules;
  • the FullRecomputeMaintainer IVM oracle checks incremental maintenance against from-scratch recompute.

The silent-wrong bugs live in the front half of the pipeline — elaboration (value-fn inlining #991/#1001/#1005), lowering and materialization (field-projection concept-keying #1014, defined-concept extent ordering #1015), the mutate write path (#992, #996), and serialization (#993–#995). A self-differential oracle is structurally incapable of catching a front-end defect: when a lowering bug corrupts the input, every downstream route inherits it and they agree — on the wrong answer. The pipeline audit passes the #1014 buggy state for exactly this reason.

The gap was therefore not oracle existence but corpus breadth at the surface, checked against a truth the oracles cannot derive: the program’s intended meaning.

Decision

Add a standing conformance corpus of small, clean, documented ontologies whose expected results are hand-pinned and checked end-to-end through the real ox CLI, gated in CI. Golden (human-anchored) is the primary method; the existing oracles remain the floor underneath for the reasoning core and the optimizer/IVM paths. This is the front-half layer they cannot reach.

It lives Argon-side (Tide depends on Argon, not the reverse — the gate must stand alone), in a new top-level conformance/ directory, separate from examples/: examples/ is the teaching corpus gated on compilation (ox check); the conformance corpus is adversarial, gated on golden output, and enforces a rule that would be wrong for teaching examples — no entry without a golden.

Design

  • Tree. conformance/corpus/<entry>/ — an ordinary ox package (ox.toml, root.ar, model modules) plus its golden: a tests/ directory (the test atom) and/or a demo.toml scenario with expect assertions. A README.md carries provenance (guards: / feature: / method:). Refusal fixtures carry a refuses.txt listing the OE#### code(s) the build must be refused with.
  • Gate. compiler/crates/oxc-driver/tests/conformance_corpus_gate.rs — a cargo nextest test that discovers every ox.toml under corpus/ and shells out to CARGO_BIN_EXE_ox (always source HEAD, never a stale installed toolchain). Positive entries must ox build then pass ox test and ox run-scenario; refusal fixtures must be refused by ox check --codes with each pinned code.
  • Three guarantees beyond the examples gate. Correctness not just compilation; no entry without a golden (the #[ignore]d-test failure mode, prevented structurally); refusals pinned by code.
  • Methodology. “Correct” is established per entry by a hand-specified golden encoding the program’s intended answer — so a front-end bug that corrupts every route still fails against the human-known truth. Where an oracle is independent (the reasoning fragment), it remains a second check.

The keystone multi_classification_fields is the acceptance witness for #1014: on a toolchain without the fix both version projections return both type-confused rows and the equals golden fails (got 2, expected 1); with the fix, green.

This RFD also records the stratify.rs fix it carries: the refusal Display strings for AggregateCycle (OE1317), NegatedWfsRelation (OE1365), and NafCycle (OE1309) now embed their code prefix, so ox check --codes names them — the eval-time variants already did; the stratify-path ones silently dropped the code the corpus pins (#1025).

Alternatives considered

  • Tide-side workflow corpus. Rejected: Argon’s correctness gate must not depend on a downstream repo. The wire/serialization bugs (#993–#995) live in Argon crates (oxc-connection, oxc-gen) and are checkable Argon-side.
  • Extend the Lean fuzzer instead. Rejected as the primary fix: the fuzzer generates post-elaboration ProgramFeature rules, bypassing the surface fn/lowering/mutate paths where the bugs live. It remains the right tool for the reasoning fragment.
  • Fold into examples/. Rejected: conflates teaching with adversarial regression and makes the no-golden rule impossible to enforce (teaching examples legitimately lack goldens).

Open follow-ups

  • #1024 — write-side enum/option value literals (None, Some(x), enum constants) error at runtime despite building clean; blocks the real absent-optional write entry (optional_iteration guards the nearest expressible contract meanwhile).
  • #1026 — the scenario harness drops the Truth4 verdict from federated rows, so expect cannot assert it; standpoint_federation pins membership + scoped views meanwhile.
  • The corpus may later sweep examples/ goldens (their demo.toml/tests are not currently run wholesale in CI) and register reasoning-evaluable entries into the pipeline differential audit for the free route-equivalence check.