RQ-60-CFOBLIG (#1057) inc 2: proof-inventory manifest — derive, don't guess theorem names (brif_correct is the 29th member of a class)

[avrabe]

What gale asked, and what the measurement says instead

gale's fathom derives theorem names from WASM rule kinds (CamelCase→snake_case) and asked us to rename brif_correct → br_if_correct or document it as intentional. Reproduced independently (script committed as the generator itself), the guess against the 138 wasm_instr constructors and the tree's *_correct theorems:

bucket	count
gale's rule FINDS	40
MISSES but a FUSED name exists (i32_divs_correct, i32_shru_correct, …, brif_correct)	29
no *_correct at all	69

brif_correct is the 29th member of a class (every signed/unsigned div/rem/shift/comparison, both widths), not the odd one out. Renaming it alone trades one inconsistency for another; renaming all 29 re-establishes a hand-maintained naming convention for consumers to re-implement — the hand-written-mirror failure the North Star names.

Two corrections to the briefing, found while building (the measurement changed the answer twice):

1. The "69 with no *_correct at all" are NOT a proof-absence frontier. Every one of them has a Qed'd *_executes theorem (the T2 existence tier: f32/f64, conversions, memory). A *_correct-only reading — mine included, in the first cut — calls 69 proven-to-execute ops "absent". Semantic result: 138/138 constructors bound at Qed; 63 result-correspondence, 75 existence-only. The honest frontier is strength, not absence.
2. Theorem names are not even unique. i64_shl_correct names BOTH the T1 result-correspondence theorem (CorrectnessI64.v) and a T2 existence statement (CorrectnessI64Comparisons.v). Any name-keyed matcher is ambiguous on this tree; the (file, name) pair is the key. And the suffix lies in both directions — select_correct, drop_correct, nop_correct, local_tee_correct, global_{get,set}_correct are existence-only statements despite the _correct name.

The deliverable

artifacts/proof-inventory.json (schema synth-proof-inventory-v1, per synth-wcet-v1 practice), generated by scripts/proof_inventory.py, freshness-gated in the claim-check CI job — the model_coverage_audit.py/#867 shape, which is this repo's closest precedent (closer than the sel_dsl #[test], since the source here is .v text, not a Rust table).

Per entry: constructor, status (qed/admitted/absent), result_correspondence bool, and every discharging theorem with file + terminator + strength.

Design decisions (as briefed, decided and justified)

1. Generated from the proof tree (coq/Synth/**/*.v). Stated residual, in the script and in the artifact's _meta.honesty: the parser is a second reader — it can print Qed for text the kernel would reject, so the manifest is only meaningful alongside a green bazel test //coq:verify_proofs. What bounds drift: _meta.cross_check.rocq_qed_total re-counts Qed. in this script's own code path and claims.yaml pins it EQUAL to the ledger's independent rocq_qed derivation (SYNTH-PROOF-INVENTORY-CROSSCHECK-1057, fields-equal) — disagreement between the two readers is RED, never hand-reconciled.
2. JSON under artifacts/, next to model-coverage.json. A consumer fetches raw.githubusercontent.com/pulseengine/synth/<tag>/artifacts/proof-inventory.json.
3. The constructor list is PARSED from WasmInstructions.v (floor ≥ 100, refuse-to-green on parser drift) — a hand-kept list would be one more mirror.
4. brif_correct is NOT renamed. Once the manifest exists the name is not load-bearing, and the rename would churn a Qed'd proof file to satisfy a convention that holds for 40 of 138 constructors. No independent reason for the rename survived measurement.

Binding is semantic, never name-derived: a theorem discharges a constructor when its statement applies exec_wasm_instr / compile_wasm_to_arm / singleton exec_wasm_seq to that constructor AND runs the ARM-side executor (exec_program/_br/_pc). WASM-side-only lemmas (WasmCertBridge refinements) and multi-instruction program examples deliberately do not bind. Strength is semantic too (bare exists astate', … = Some astate' = existence-only).

Red-first transcript (all four, needle counted before/after each mutation)

1. Rename brif_correct → br_if_correct (needle 3→0, br_if_correct 0→3), no regeneration → --check exit 1 (STALE or hand-edited). Restore → needle 3, ok.
2. Add a theorem (nop2_correct appended, needle 0→1), no regeneration → --check exit 1. Restore → ok.
3. Hand-edit the cross-check (rocq_qed_total 630→629, needles verified) → both gates red: SYNTH-PROOF-INVENTORY-CROSSCHECK-1057 fails with rocq_qed=630, proof_inventory_rocq_qed=629 — update every copy together, and --check exits 1. Restore → 52/52 claims hold.
4. Non-vacuity: neuter the ARM-side anchor in a script copy → generator refuses (only 0 constructors bound (< 50) — refusing to green), writes nothing. Restore → ok.

Gates

• cargo fmt --all -- --check ✅ · cargo clippy --workspace --all-targets -- -D warnings ✅ · cargo test --workspace (running at PR-open; zero Rust files touched — will confirm before hand-off)
• python3 scripts/claim_check.py claims.yaml → 52/52 (new claim included) · --metric ✅ · test_claim_check.py ✅ · model_coverage_audit.py --check ✅ · artifact_citation_check.py ✅ · status_evidence_check.py → 0 failures ✅
• Byte-invisible: no crate code touched; .text cannot move.
• artifacts/status.json regenerated (--emit-status) for the new proof_inventory_rocq_qed capture field — the visible-diff rule, same commit.

Honest residual

• The manifest indexes the tree; the kernel (//coq:verify_proofs) remains the only oracle for whether a Qed is real.
• The strength classifier is textual (an existential through an alias, or a post-state constraint spelled without /\/get_reg/state_correspondence, would misclassify — none exist today); the per-entry theorem list is the audit trail.
• The universe is the Rocq model's constructors, not the shipped WasmOp enum — ops the model doesn't carry (memory.size, br_table, call, …) have no row. Extending the universe to the shipped enum (rows for unmodeled ops) is a named follow-up, not smuggled in here.
• Pre-existing defect found on main, NOT fixed here (out of lane scope): claims.yaml waiver - to: 18910 carries a duplicate reason: key — a hand-merge swallowed the - to: 18288 line of the RQ-59-I64SHIFT waiver, so under PyYAML last-wins the 18910 (VFPPRESSURE +622) waiver's effective reason is the I64SHIFT text and the 18288 waiver is invisible to the parsed ledger. Exactly the duplicate-key-strict-loader class from the v0.59 lessons; flagged to the coordinator.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!