Skip to content

RQ-58-MIRRORS (#242): generate, don't mirror — the freshness gate can now see template-vs-code drift - #993

Merged
avrabe merged 10 commits into
mainfrom
feat/generate-dont-mirror-242
Aug 18, 2026
Merged

RQ-58-MIRRORS (#242): generate, don't mirror — the freshness gate can now see template-vs-code drift#993
avrabe merged 10 commits into
mainfrom
feat/generate-dont-mirror-242

Conversation

@avrabe

@avrabe avrabe commented Aug 18, 2026

Copy link
Copy Markdown
Contributor

Lane 3 of the v0.58 hub — artifact RQ-58-MIRRORS, epic #242.

The counts, reproduced

The spec's figures reproduce exactly, and their scope is the first finding:

git ls-files 'crates/*' | grep '\.rs$' | xargs grep -lIi mirror                 -> 57
                                       | xargs grep -lIi hand-maintained        -> 11
                                       | xargs grep -lIi 'single source of truth'->  1

Repo-wide over all tracked text files the same three greps give 125 / 22 / 8. The 68 files outside crates/**/*.rs include scripts/ (18) and docs (18) — where the FEATURE_MATRIX rot actually lived. And "mentions the word mirror" is not "is a mirror": neither exec_trap_subset_op's allowlist nor the referenced_locals triplication would be found by that grep. The ranked inventory below was built by searching the shapes ("keep in sync", "must match", allowlist/decline-list literals, one enum matched exhaustively in several files).

What the freshness gate can now catch

check_generated_fresh byte-compares the rendered matrix against the template, and render_feature_matrix only substitutes {{...}}. It proves the render is faithful to the template and never that the template is faithful to the code.

Two mechanisms close different halves of that:

1. Derivation (catches code drift). artifacts/aarch64-op-surface.json is EMITTED by the op-parity oracle running the real select_typed_cf_calls over every WasmOp representative — 197 probe labels, 185 lowered / 12 declined, 0 unprobed. The template substitutes it. This is the #667 pattern, and it is what would have caught the v0.57 failure: the shipped capability that was still listed as a decline was local.set/local.tee on a param, which the artifact now records as lowered.

2. Exhaustiveness (catches unclassified assertions). check_template_facts requires every number in the template to be one of DERIVED ({{field}}), PINNED (a claim whose doc: is the template — the #880 mechanism, which existed but had no exhaustiveness), UNCHECKED (declared with a ≥20-char rationale) or MASKED (an identifier token, each mask declared with a why:). Dead entries and dead masks are red too.

Census: 25 derived · 12 pinned · 21 unchecked · 208 masked.

What remains explicitly UNCHECKED

  • check_template_facts is NUMBERS-ONLY. Non-numeric prose assertions are outside its reach — including the whole module/shape-level aarch64 decline list, the exact class that went stale twice. What covers that class now is the derivation, not this gate.
  • 21 declared unchecked template numbers, each with its rationale and, where one exists, the specific conversion that would close it. That list is the risk register.
  • The gate does not prove a pinned or unchecked claim true. It proves every assertion was classified on purpose and fails closed on new ones. The mask list is the residual trust, in claims.yaml so it is reviewable.
  • Module/shape-level aarch64 declines were verified once here (18/18 declined, one probe module each) and are re-checked by nothing per commit.

Two findings about this lane's own work

  • The matrix was already stale. It said 221-variant no-wildcard tripwire while both copies of ARM_OP_VARIANT_COUNT said 222 — rotted, behind a green 43/43, in the release about doc rot. Now derived ({{a32_tripwire_variants}}), renders 222.
  • I cited a gate that does not exist. An early commit referenced scripts/repro/aarch64_decline_claims_242.py in a Rust comment and in the _scope string emitted into the artifact whose entire claim is "derived, never a hand list". No such file. Both replaced with the honest statement.

Ranked inventory

Full 21-entry version with paths, the wrong-ANSWER vs wrong-DOC discriminator, and what checks each today is a comment block at the head of claims.yaml. Tier 1 (wrong answer, nothing checked it):

# Mirror Status
1 count_params × 3 backends — three byte-equivalent copies of an unsound read-before-write heuristic CONVERTEDsynth_core::count_params_heuristic
2 aarch64 decline list: code vs FEATURE_MATRIX CONVERTED → derived artifact + substitution
3 ARM_OP_VARIANT_COUNT × 2 tripwire files, guarded only by a comment CONVERTEDfields-equal
4 all_wasm_op_representatives() hand-maintained Vec — and this lane made it feed a generated doc CONVERTED → length pinned to the enum (279 == 279)
5 exec_trap_subset_op allowlist ↔ encode_op arms ↔ the test's re-list ("one hand-maintained mirror guarding another") NOT converted; mitigated by ArmState::unmodeled at runtime
6 shrink_callee_saved_savesbody_uses_callee_saved allowlists NOT converted; guard is the comment
7 ResolvedBranchGeometry's Label = 0 table vs the estimator NOT converted
8 reg_effectrewrite_op positional mirror mutual-consistency oracle, "no third ground truth"

Tier 2 (checked): estimator↔encoder (the model to copy), RV32 sizing, WCET cycle literals, sel_dsl::RULES↔manifest↔.v, trap.rs↔ordeal, WasmOp in 5 places / ArmOp in 9 (pairwise only). Tier 3 (doc): known_divergences "18 entries" prose, ORACLE_WIRING's count-min-pinned "145 wired" (so it can silently understate), CRATES_TO_PUBLISH, RV32↔ARM startup/linker mirrors, a cross-repo STPA ABI constraint.

Red-first evidence — every new gate

Gate Negative control Result
op-surface artifact freshness add a MemoryFill lowering arm to the aarch64 selector, touch nothing else red: memory.fill flips declined→lowered
…→ render chain regenerate the artifact only red: status.json and FEATURE_MATRIX stale
check_template_facts type a new unpinned number into template prose red: UNCLASSIFIED number '4212'
" delete an unchecked span from the template red: dead-entry
" delete three {{}} substitutions red: derived floor 21 < 24
" point a mask at a string that never appears red: dead mask + 52 newly unclassified
fields-equal set one ARM_OP_VARIANT_COUNT copy to 223 red: "copies of one constant DISAGREE: 222, 223"
anti-regrowth count-max 0 re-grow a private count_params in the aarch64 backend red: "trusted base grew: 1 > recorded max 0"
representative coverage delete I32Sub from the Vec red: "278 entries but WasmOp declares 279"

Each restored → green. The {{}}-deletion control is the vacuity control: without the floors, an empty template classifies perfectly, so deleting assertions would have been the cheapest way to green the gate.

And the byte-identity evidence was itself needle-tested. count_params_heuristic only runs on the no-declared-count path, so a 512-object md5 sweep that never reaches it would print a perfect zero diff and prove nothing (v0.56's "a mutation test that never mutated printed ok"). Negative control: return a constant 7 → 174 of 510 hashes move, 2 compiles fail. The sweep does exercise it; the zero diff is evidence.

Gates

cargo test --workspace ok (142 suites) · cargo clippy --workspace --all-targets -- -D warnings ok · cargo fmt --check ok · claim_check 45/45 · model_coverage_audit --check ok · oracle_wiring_check ok · check_version_pins ok. Each run without a pipe. Derived docs regenerated with --emit-status; FEATURE_MATRIX.md never hand-edited.

Bazel runs zero rust_test targets (crates/BUILD.bazel globs src/**), so the two new tests' repo-relative reads are not exposed to a sandboxed rust_test.

No [Unreleased] CHANGELOG edit, no version bump.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L


Addendum after merging origin/main (#991 RQ-58-METRIC + #992)

60/60 checks pass; merge state CLEAN.

MC/DC (RQ-57-MCDC) fired on this lane, correctly, and the fix was scope — not a floor. The count_params collapse moved decisions out of synth_backend_riscv::backend::, which is a scored prefix. Measured on ubuntu-latest / rustc 1.96.1 / witness 0.42.0, 56 rows:

dec cond proved dead
main 22 130 57 50
after the collapse, no scope change 21 131 56 45
+ the whole synth_core::wasm_op:: 26 145 57 54 (ceiling 50)
+ only count_params_heuristic 22 135 57 48

Scoping to the relocated function meets every floor. The module-wide form would drag in rewrite_memory_grow_zero and referenced_locals — 9 conditions no row reaches, a real gap, but widening scope needs its own rows and its own re-measured ceiling. Named as a follow-up, not smuggled in. No floor lowered, no ceiling raised.

origin/main was red on its own subtraction ratchet, and this PR is the first to carry the fix. #992 merged first (102 code-region selector lines, one _ => arm); #991 pinned 18480/62 from a base predating it. Re-derived from main's own blob: 18582 lines / 63 arms / 29839 total / 106 total arms. Pins moved here with waivers attributing the growth to #992, not to this lane — the classic stale-base merge.

mirror_marker_files 57 → 58 is this lane's, and is waived rather than laundered. The added file is crates/synth-core/src/wasm_op.rs, and what it says is a retirement notice: count_params went from three copies to one. The proxied population went down by two copies while the file count went up by one — exactly the over-count that metric's own comment predicts. Deleting the word to go green would trade an accurate doc for a nicer number.

avrabe and others added 7 commits August 18, 2026 20:57
… selector

`check_generated_fresh` byte-compares the RENDERED FEATURE_MATRIX against the
TEMPLATE, so it proves the render is faithful to the template and never that
the template is faithful to the CODE. The aarch64 decline list is the class
that cost the most under that blind spot: it went stale twice and at v0.57
still named a capability that release had shipped.

Derive it instead. `a64_op_surface_artifact_is_fresh_242` probes the REAL
`select_typed_cf_calls` for every `WasmOp` representative (union of the
extended-surface probe and the integer-core parity probe — both matches are
wildcard-free, and the test asserts 0 representatives fall through both) and
emits `artifacts/aarch64-op-surface.json`. The committed artifact must equal
re-derivation or the test fails with regenerate instructions
(`SYNTH_EMIT_A64_SURFACE=1`).

Measured: 197 probe labels, 185 lowered / 12 declined, 0 unprobed. The 185
independently reproduces the existing grep-derived `aarch64_selector_ops`
field via a completely different method (real probe outcome vs distinct
`WasmOp::` tokens in selector.rs).

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… weaker derivation

The feature-matrix template's aarch64 decline enumeration was hand-typed prose
that the freshness gate structurally could not check. The OP-LEVEL half of it
is now `{{aarch64_declined_ops}}`, selected out of the derived
`artifacts/aarch64-op-surface.json` by a new `json-list` status-field kind
(fails loudly when the selection matches nothing, so an empty list can never
render as a green claim).

SUBTRACTION, not addition: `aarch64_selector_ops` (distinct `WasmOp::` tokens
in selector.rs before `mod tests` — a measure of which names APPEAR in a file)
is DELETED and replaced by `aarch64_ops_lowered` / `aarch64_ops_probed` /
`aarch64_ops_declined`, read off the real probe outcomes. Both derivations
produce 185, so the swap is byte-invisible in the rendered number while being
strictly stronger evidence.

RED-FIRST, mutating the CODE (not the template) — the property being added is
"the gate sees code drift":
  * add a `MemoryFill` lowering arm to the aarch64 selector, touch nothing else
  * LINK 1 red: a64_op_surface_artifact_is_fresh_242 fails (memory.fill flips
    declined -> lowered)
  * regenerate the artifact only
  * LINK 2 red: claim_check reports status.json AND FEATURE_MATRIX.md stale
  * revert the selector: artifact byte-identical, 43/43 claims hold, 9/9
    parity tests pass

The failure message reports differing ROWS rather than two 11 kB blobs.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…-code drift

`check_generated_fresh` byte-compares the RENDER against the TEMPLATE, so it
proves the render is faithful to the template and NEVER that the template is
faithful to the code. That is why v0.57 shipped three stale numbers behind a
green 43/43.

The repo already had the right MECHANISM for the missing half (#880: a claim
whose `doc:` is the template, pinning prose to a re-derivation). What it
lacked was EXHAUSTIVENESS — nothing said which assertions it covered, so an
unpinned number looked exactly like a pinned one.

`check_template_facts` supplies that. Every number in the template must be
DERIVED (a `{{field}}`), PINNED (a template-doc claim span), UNCHECKED
(declared with a >=20-char rationale) or MASKED (an identifier-shaped token,
each mask declared with a `why:`). Anything else is red. Dead entries and dead
masks are red too, so the ledger cannot rot in the other direction.

CENSUS as landed: 24 derived · 11 pinned · 22 unchecked · 208 masked.
The 22 UNCHECKED entries are the deliverable as much as the gate is — they are
the named risk register of what no derivation covers, each with the reason and,
where one exists, the specific conversion that would close it.

HONEST SCOPE: this gate does not prove a pinned or unchecked claim TRUE. It
proves every assertion was classified on purpose and fails closed on new ones.
The mask list is the residual trust and lives in claims.yaml so it is
reviewable.

RED-FIRST, four negative controls (each: break, observe red, restore, green):
  A  type a new unpinned number into template prose -> UNCLASSIFIED '4212'
  B  delete an unchecked span from the template     -> dead-entry failure
  C  delete three `{{}}` substitutions              -> derived floor 21 < 24
  D  point a mask at a string that never appears    -> dead-mask + 52 newly
                                                       unclassified issue refs
Control C is the vacuity control: without the floors an EMPTY template
classifies perfectly, so deleting assertions would have been the cheapest way
to green it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…te I cited that did not exist

Two findings from the inventory sweep, both about work in this very lane:

1. THE FEATURE MATRIX WAS ALREADY STALE. It said "221-variant no-wildcard
   tripwire" while BOTH copies of `ARM_OP_VARIANT_COUNT` said 222 — a rotted
   doc number sitting behind a green 43/43, in the release whose subject is
   doc rot. Classifying it `unchecked` (as this lane first did) documents the
   rot without fixing it, so it is now DERIVED instead:
   `{{a32_tripwire_variants}}`, captured from the constant. Renders 222.

   The constant is deliberately declared TWICE (two independent soundness
   tripwires each re-scan rules.rs against their own copy). Its only guard was
   a comment: "bump ARM_OP_VARIANT_COUNT here AND in a32_no_silent_nop_615.rs".
   A desync silently disables one tripwire while the other stays green. New
   `fields-equal` evidence kind makes the comment a check — it compares VALUES,
   so unlike a count-same over a literal it cannot go vacuously green when both
   copies are edited to the same wrong number.

   RED-FIRST (code mutation): set the sp-leg constant to 223, leave everything
   else -> "hand-maintained copies of one constant DISAGREE:
   a32_tripwire_variants=222, a32_tripwire_variants_sp_leg=223". Restore -> 44/44.

2. A GATE THAT DOES NOT EXIST WAS CITED AS EVIDENCE. The previous commit
   referred to `scripts/repro/aarch64_decline_claims_242.py` in a Rust comment
   AND in the `_scope` string emitted into artifacts/aarch64-op-surface.json —
   a vacuous gate reference shipped inside the artifact whose whole claim is
   "derived, never a hand list". No such file exists. Both references replaced
   with the honest statement: those refusals are hand-written prose, declared
   unchecked, verified once at v0.58 and re-checked by nothing.

Census: 25 derived / 12 pinned / 21 unchecked / 208 masked. Floors ratcheted.
Gates: cargo test --workspace ok (142 suites), clippy -D warnings ok,
fmt --check ok, claim_check 44/44.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… mirror inventory

SUBTRACTION. #974 centralised `referenced_locals` — the FIX — and left
`count_params`, the UNSOUND read-before-write heuristic it replaced on the
declared-count path, as three byte-equivalent private copies (arm_backend.rs,
riscv backend.rs, aarch64 backend.rs) differing only in local names and
rustfmt line breaks. Three copies of an unsound rule is the worse case: a
correction applied to one silently does not reach the other two.

Collapsed to `synth_core::count_params_heuristic`, with the unsoundness NAMED
in its doc comment rather than implied away.

GATED ON BYTE-IDENTITY, per the release's own subtraction rule: 512 objects
(every scripts/repro/*.wat x {cortex-m4, self-contained --cortex-m,
--relocatable, rv32, aarch64}) are md5-identical before and after. Zero diff.

ANTI-REGROWTH, red-first: SYNTH-COUNT-PARAMS-SINGLE-SOURCE pins exactly one
definition repo-wide and count-max 0 on the heuristic's distinctive local
(`let mut first_access`) across the three backend crates. Re-growing a private
copy in the aarch64 backend -> "trusted base grew: 1 > recorded max 0";
restored -> 45/45.

THE INVENTORY is now a comment block at the head of claims.yaml: 21 ranked
entries plus the already-converted patterns, converted AND unconverted, with
the wrong-ANSWER vs wrong-DOC discriminator and what checks each today. The
derived counts and their scope are recorded there too — the spec's 57/11/1
reproduces exactly over crates/**/*.rs, and is 125/22/8 repo-wide, the gap
being scripts/ and docs/ where the FEATURE_MATRIX rot actually lived.

Highest-value REMAINING conversion, named not done:
`all_wasm_op_representatives()` is a hand-maintained Vec mirroring the WasmOp
enum, and an op missing from it is silently never parity-probed AND silently
absent from the derived op-surface artifact this lane added.

Gates: cargo test --workspace ok (142 suites), clippy -D warnings ok,
fmt --check ok, claim_check 45/45.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…to the enum

`all_wasm_op_representatives()` says of itself "this Vec, by contrast, is
HAND-MAINTAINED", and its safety argument is that a new WasmOp variant fails
to compile in `classify`, which points the author here. That argument covers
ADDING a variant. It does not cover a variant that is classified but never
given a representative, and it never covered DELETION.

The consequence got worse when this lane made the same Vec the source of
`artifacts/aarch64-op-surface.json`: an op missing from it is now silently
absent from a derived artifact whose whole claim is "derived, never a hand
list", which the feature matrix then substitutes. A hand list feeding a
generated doc is precisely the shape this release exists to kill — and this
lane had just built one.

`representatives_cover_every_wasm_op_variant_242` pins the list's LENGTH to
`WasmOp`'s own declaration, parsed out of synth-core/src/wasm_op.rs at test
time: 279 variants == 279 representatives. Narrow by design — it cannot check
that the RIGHT ops are present, only that none is missing or duplicated, which
is exactly what the compile error does not catch. A >=250 floor on the parse
stops a formatting change from silently making it measure nothing.

RED-FIRST: delete `I32Sub` from the Vec -> "has 278 entries but WasmOp declares
279 variants"; restore -> 10/10 pass. Re-confirmed after simplifying the
variant-matching rule, so the green is not an artifact of the parse.

Gates: cargo test --workspace ok, clippy -D warnings ok, fmt --check ok,
claim_check 45/45.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…idence claim

Two honesty corrections to this lane's own evidence, both the kind of thing
this release is about.

1. THE BYTE-IDENTITY CLAIM COULD HAVE BEEN VACUOUS. `count_params_heuristic`
   only runs on the NO-declared-count path, so a 512-object md5 sweep that
   never reaches it would print a perfect zero diff and prove nothing — v0.56's
   "a mutation test that never mutated printed ok", exactly.

   Negative control run: make the function return a constant 7, re-run the same
   sweep. 174 of 510 hashes MOVE and 2 compiles fail outright. The sweep does
   exercise it, on ~34 % of the corpus, so the zero diff is evidence. Recorded
   next to the claim rather than left implicit.

2. "185 INDEPENDENTLY REPRODUCES 185" WAS AN OVERCLAIM. The retired grep counts
   distinct `WasmOp::` tokens; the new probe counts lowering labels (197 total,
   one of which covers several variants). Different universes — the equality is
   almost certainly coincidence. It was already correctly NOT pinned with
   count-same; the ledger now says why, so nobody later reads it as
   corroboration and builds a false 1:1 invariant on it.

Also checked and recorded: Bazel runs ZERO rust_test targets (crates/BUILD.bazel
globs `src/**` only), so the two new tests' repo-relative reads via
CARGO_MANIFEST_DIR are not exposed to a sandboxed rust_test.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@codecov

codecov Bot commented Aug 18, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 90.47619% with 2 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-backend-aarch64/src/backend.rs 0.00% 2 Missing ⚠️

📢 Thoughts on this report? Let us know!

avrabe and others added 3 commits August 18, 2026 21:51
The count_params collapse tripped the MC/DC floors, and the gate was right to
fire. The RV32 copy of that heuristic lived in `synth_backend_riscv::backend::`
and was therefore scored; collapsing the three copies into
`synth_core::count_params_heuristic` moved its decisions out of every scored
prefix, so scored counts fell.

The logic did not disappear — it relocated. So the SCOPE follows it:
`synth_core::wasm_op::` joins SCORED_PREFIXES. That file also owns
`referenced_locals` (the #970 param-classification rule every backend shares)
and `rewrite_memory_grow_zero` (#539), neither of which was scored anywhere
before — small, shared, correctness-critical decision logic is exactly what
this gate exists to measure.

Explicitly NOT the fix the file forbids: no floor was lowered.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… not its module

Correcting the previous commit, which widened MC/DC scope to all of
`synth_core::wasm_op::` and tripped the dead-conditions ceiling.

Measured on ubuntu-latest / rustc 1.96.1 / witness 0.42.0, 56 rows:

  main                                  22 dec · 130 cond · 57 proved · 50 dead
  after the collapse, no scope change   21 · 131 · 56 · 45   (dec + proved trip)
  + the whole `synth_core::wasm_op::`   26 · 145 · 57 · 54   (dead ceiling trips)
  + only `count_params_heuristic`       22 · 135 · 57 · 48   (all floors met)

The module-wide form drags in `rewrite_memory_grow_zero` (#539) and
`referenced_locals` (#970) — 9 conditions no row reaches. That is a real
coverage gap and worth closing, but widening scope needs its own rows and its
own re-measured dead ceiling. Doing it as a side effect of a mirror collapse
would be exactly the sloppiness this lane exists to stop, so it is named as a
follow-up rather than smuggled in.

Still no floor lowered, and no ceiling raised: scope follows the function that
moved, and stops there.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… defeated gates

Conflict resolution (claims.yaml, scripts/claim_check.py): union of the two
lanes — main's RQ-58-METRIC ratchet engine + this branch's RQ-58-MIRRORS
fields (the retired aarch64_selector_ops derivation stays deleted; the
branch-only fields-equal evidence kind is ported into main's _check_evidence
dispatcher).

Two gates were silently defeated on main and are re-armed here:

1. MC/DC rustc pin (#984): dependabot bumped dtolnay/rust-toolchain
   1.96.1 -> 1.100.0 — for that action the ref IS the compiler, so the
   MC/DC job's deliberate measurement pin was changed with no re-measure
   of the floors. Restored to 1.96.1 and excluded from dependabot with the
   reason in both files.

2. Subtraction ratchet stale-base cross (#991 x #992): #992 merged 19:50
   adding 102 code-region selector lines and one _ => None helper arm;
   #991 pinned the ratchet values at 20:07 from a base that predated it,
   so main itself derives 18582/29839/63/106 against a ledger saying
   18480/29616/62/105 and is red on its own queued push CI. This PR is the
   first to carry the union; the pins move here with waivers attributing
   the growth to #992's #973 miscompile fix, not to this lane.
   mirror_marker_files 57 -> 58 is waived as the surviving single
   count_params copy's own RQ-58-MIRRORS retirement-provenance comment —
   the heuristic's documented prose over-count, not a new mirror.

status.json + FEATURE_MATRIX.md regenerated via --emit-status; 49/49
claims hold on the merged tree.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@avrabe
avrabe merged commit 4b7eb9a into main Aug 18, 2026
61 checks passed
@avrabe
avrabe deleted the feat/generate-dont-mirror-242 branch August 18, 2026 20:44
avrabe added a commit that referenced this pull request Aug 19, 2026
… can run (#1001)

#1000, from a toolchain-wide CLI survey: `synth verify` exists in the tree and
in `--help`, fails closed with an exemplary message — and is in NO artifact a
user can obtain. Reproduced by the reporter on the layer build (0.55.0) AND the
current release (0.57.0), whose four platform tarballs all lack the feature.

THE ISSUE'S OWN ESCAPE HATCH IS DEAD, AND I MEASURED IT RATHER THAN ASSUMING.

#1000 offers: "or, if the Z3 dependency makes that undesirable for the default
artifact, publish a variant". There is no Z3 dependency:

  cargo tree -p synth-cli --features verify                    ->  0 z3 nodes
  cargo tree -p synth-cli --features verify,…/z3-solver        ->  2 z3 nodes

`verify = ["synth-verify"]` and nothing more. `z3-solver = ["z3"]` is a separate
opt-in with `optional = true`, and even enabled it links the SYSTEM libz3 rather
than bundling it (#553). Ordeal (pure Rust QF_BV) has been the default engine
since v0.27.0. Shipping `--features verify` costs no Z3, no libz3, no C++
toolchain — so this is a release-workflow change, not a trade-off.

README.md:98 IS THE OTHER HALF OF THE FINDING, and it is corrected here. It
said the CLI `verify` feature "currently also enables the feature-gated Z3
differential oracle (statically linked)". False since v0.27.0 — and it is
exactly the sentence that would make a maintainer accept #1000's escape hatch
and NOT ship the feature. Prose that was true once, quietly stopped being, and
stayed load-bearing on a release decision: the class the v0.57 cold review kept
turning up, found again by a user asking a good question about a stale premise.

Artifact scope, three parts, with the middle one carrying the weight:
  1. build the released binaries (four tarballs + npm) with `--features verify`
  2. a NON-VACUITY GATE — a released-artifact smoke test that actually RUNS
     `synth verify` on a freshly compiled module and asserts a VERDICT, not the
     capability-missing error. Red-first against a binary built without the
     feature. Without this, "we shipped the feature" regresses silently to "we
     shipped the help text", which is the class this whole release closes.
  3. move the capability check AHEAD of the banner — today the four
     `Translation validation:` lines including `Strategy: Per-rule SMT
     verification (ASIL D path)` print BEFORE the tool discovers it cannot
     verify, so a log-scraper finds the ASIL-D line in a run that verified
     nothing. Exit code is already correct.

Out of scope, named not dropped: #1000's `synthesize`-vs-`compile` description
overlap, `--format json`, help-line width.

Also re-graded RQ-58-MIRRORS (#993) and RQ-58-SELECT973 (#992) proposed ->
implemented; both merged and the ledger had not caught up.

rivet: 50 errors before AND after (unchanged); warnings +2, the standard pair
every artifact carries. claim_check 49/49.

Refs #1000, #242


Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant