[v0.4] Extend vv for production compiler, GNAF certificates, Rust artifacts, and oracle falsification

Scope

Make every new v0.4 claim part of the existing falsifiable vv discipline; no separate weaker acceptance path.

Work

Add model IDs/scenarios/named conformance tests for every v0.4 capability.
Extend golden/reproducibility checks to production calculus, certificates, Rust/package outputs, model/reasoning artifacts, and compiler semantic IDs.
Add structural audits ensuring new semantic variants are handled exhaustively by validation, serialization, Lean, LaTeX, snapshots, coverage, and production eligibility.
Add negative fixtures for every new diagnostic class.
Record planted-defect evidence in VERIFICATION.md.
Add anti-vacuity gates for GNAF universe/certificate coverage and oracle corpus coverage.

DoD

just vv is the only normative v0.4 acceptance gate.
A new semantic variant cannot be added with an unhandled backend/serializer/optimizer branch.
A missing GNAF competitor/certificate row or empty oracle corpus cannot pass vacuously.
No test is skipped silently on the normative Linux x86-64 host.

Acceptance criteria

Planted defects independently demonstrate failure of semantic preservation, global-optimality completeness, Rust rendering, model contracts, reasoning rules, oracle comparison, deterministic output, and new diagnostics.
Verification documentation records exact commands and expected failure signatures.
Complete just vv passes only after all defects are removed.

Depends on all implementation issues; may be built incrementally but closes last.

Recorded as item L2.4 of the completion plan #106, extended to every new item of that plan: each of #111–#127 needs its gate and a recorded planted defect.

Generated by Claude Code

@afflom

@afflom, here is a read-only audit of v0.4 against this issue, on main 8765feea and the heads of #167, #172 and #171. The goal is to turn "closes last" into a short finish list now, while the train is still open.

First, none of this has to ride the train's final regeneration. Every item below leaves generated bytes and identities unchanged. The train's new ToInt and ToNat are named explicitly in the Lean backend and in eligibility. The #33-relevant blockers on #167 are the ones already in my review (SP-15 record, OR-04 plant, SM-32 records).

Scope. Your note extends this issue to each of #111–#127, but all of them are milestone v0.5. Four reach v0.4 anyway, each with its gate and record (or will once the train's review fixes land): #114 (SM-32), #117 (PF-20..23), #118 (MD-13) and #126 stage 1 (SL-02, #172). Proposal: #33 closes on the v0.4 milestone's capabilities, and the #111–#127 rule moves to a v0.5 vv issue or to #128's DoD.

Finish list for v0.4:

Exhaustiveness audit (DoD 2). repo_model::exhaustive reads only eligibility.rs and the four preservation sources. Silent catch-alls remain in:
- the Lean backend: backend/semantic.rs:759, _ => "graphTopological";
- the elaboration charge: ir/semantic.rs:1976, type_node_count, _ => 0;
- calculus/realization.rs:1277.
No audit names the calculus Rust AST (Item, Callee, Lit, Expr), which [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 stage 2 is about to grow. Fix: add the backend, LaTeX, snapshot and charge files and the calculus AST to the audit, replace the silent arms, plant a wildcard, and record it. No Lean is needed. It is best landed before [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 stage 2 part 2.
Records for 25 merged IDs that VERIFICATION.md never names.
- The case already makes its negative, so only the record is missing (16): DF-18, GL-18, PD-03, PF-19, SM-24, SM-27, TC-01, TC-02, TC-05, MD-01, MD-03, MD-05, MD-10, LM-01, LM-02, LM-03.
- The case is positive only and needs a plant (9): GL-17, SM-26, PD-01, PD-02, PD-06, NE-01, MD-11, LM-13, PK-05.
The four LM rows are mine; [v0.4] Add language-model semantic components and compositional text-processing pipeline #30's slice 4 will carry them.
Negative fixtures for the 18 codes added since v0.3 that only conformance cases reach:
- LLB6005–6007
- LLC0105–0108
- LLC0201–0204
- LLR3009
- LLT4013–4015
- LLV7018
- LLV7101
- LLV7102
I propose fixtures for the codes the CLI can reach, and a recorded reason for the rest.
Milestone v0.4 for [v0.4] RT-04: blank only test items, never the code after a cfg(test) that is not on an item (follow-up to #156) #169 and [v0.4] The tracked tree holds nothing the repository walkers skip (CACHEDIR.TAG, target, .lexlean, .lake) (follow-up to #156) #170. They are false negatives of the gates themselves (DoD 4).
VERIFICATION.md:17. It still says "all 351 conformance tests" (404 on main). I propose dropping the number, since the count lives in four gated places already.
Each planned item arrives with its row, scenario, test, plant record and golden: [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91, production: the collection and iteration primitives are realized by self-recursive functions but registered recursion = false; a root overflows the stack at about 40k iterations #105, [v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software #92, [v0.4] #27 stage 5: certificates A, B, E and the audit modules as typed data, with no Lean text template in the production compiler #89 stage 4, [v0.4] Refuse the data form (\semanticdata, \toolingdata, \coredata) under language 1.2: the last change of the milestone #149, [v0.4] Add language-model semantic components and compositional text-processing pipeline #30, [v0.4] Build model/reasoning stdlib composition and PrismPM application fixture #32 and [v0.4] End-to-end release closure, examples, documentation, packaging, and clean-checkout reproducibility #34. [v0.4] Build model/reasoning stdlib composition and PrismPM application fixture #32 has no owner yet.

The other DoD and acceptance items are met on main:

a recorded plant for each acceptance class, partial only for new diagnostics (item 3);
no vacuous GNAF or oracle pass;
vv as the only gate, with its out-of-vv recipes mirrored in bdd;
no time targets in SPEC or the register.

Item 1, item 3 and the non-LM records of item 2 have no owner. Do you keep them in your #33 lane, or shall I take some?

@humuhumu33

Gap audit of #33 against main efea57d85 (register 414 IDs, 85 codes). It complements @humuhumu33's audit above and re-checks its findings on the current tree. Read-only; nothing built yet.

#	#33 bullet	Status	What discharges it / what is missing
W1	IDs, scenarios and named tests for every v0.4 capability	Met for merged IDs	`model/ids.toml` ↔ SPEC §31 ↔ `features/suites` ↔ `conformance_<id>` (R3, `validate-spec-links`, `bdd` meta-gate). Open items arrive with their own rows (#91, #105, #92, #89 st.4, #149, #30, #32, #34).
W2	Golden and reproducibility over calculus, certificates, Rust, model/reasoning artifacts and semantic IDs	Met (not re-verified)	`check-golden`, `check-reproducibility`, `check-calculus`, `verify-examples` expected records; VERIFICATION.md "GNAF/rust determinism/identity" records (`rust cross-root determinism`, `GNAF universe identity`).
W3	Exhaustiveness audit for validation, serialization, Lean, LaTeX, snapshots, coverage, eligibility	Partial / missing	`repo_model::exhaustive` reads only `eligibility.rs` + 4 preservation sources (`PRESERVATION_SOURCES`, `exhaustive.rs:277`). Silent wildcards remain unaudited: `backend/semantic.rs:778` (`_ => "graphTopological"`), `ir/semantic.rs:2003` (`type_node_count`, `_ => 0`), `calculus/realization.rs:753, 808, 1301`. The calculus Rust AST (`Item`, `Callee`, `Lit`, `Expr`) is named by no audit. No plant recorded.
W4	Negative fixtures for every new diagnostic class	Partial	44 of 85 codes have no fixture under `tests/negative` or `tests/fixtures`. Of those, these 18 were added since v0.3 and are reached only by conformance cases: LLB6005–6007, LLC0105–0108, LLC0201–0204, LLR3009, LLT4013–4015, LLV7018, LLV7101, LLV7102. The other 26 are older: LLB6001–6004, LLC0001/0002/0104, LLF5002/5004, LLI9001, LLL1001/1003/1005/1006, LLP2001/2004, LLR3002/3006, LLS8003, LLT4002/4004, LLV7006–7010.
W5	Planted-defect evidence in VERIFICATION.md	Partial	~9000 lines of records exist. 25 merged IDs are not named anywhere in it: DF-18, GL-18, PD-03, PF-19, SM-24, SM-27, TC-01, TC-02, TC-05, MD-01, MD-03, MD-05, MD-10, LM-01..03 (case already makes its negative, record missing); GL-17, SM-26, PD-01, PD-02, PD-06, NE-01, MD-11, LM-13, PK-05 (case is positive-only, needs a plant).
W6	Anti-vacuity: GNAF universe/certificate coverage; oracle corpus coverage	Met (not re-verified)	`GN-02`/`GC-02` completeness and premise-for-every-system cases, "check-calculus covers the GNAF fixtures/Gnaf model/schemas", `OR-01..08` (corpus of every production root + one probe per construct, unavailable ≠ agreement, planted discrepancies).
D1	`just vv` is the only normative acceptance gate	Met	`Justfile` `vv`; out-of-`vv` recipes (`fixtures`, `calculus`, `verify-write`) are mirrored in `bdd`/`inventory` (RP-13).
D2	A new semantic variant cannot reach an unhandled backend/serializer/optimizer branch	Not met	Same gap as W3.
D3	Missing GNAF competitor/certificate row or empty oracle corpus cannot pass vacuously	Met (not re-verified)	See W6.
D4	No test skipped silently on Linux x86-64	Met	`support::lean_backed` makes the toolchain mandatory there and other hosts print what they skipped; 4 `#[ignore]` in `crates`/`xtask` (not yet inspected, so unconfirmed as zero). #169/#170 (gate false-negatives) still need milestone v0.4.
A1	Plants for semantic preservation, global-optimality completeness, Rust rendering, model contracts, reasoning rules, oracle comparison, determinism, new diagnostics	Met except diagnostics	VERIFICATION.md `### certificate A/B/E … can fail`, `GNAF … can fail`, `rust … can fail`, `audit-oracle-isolation can fail`, `rust cross-root determinism`, model/reasoning records near lines 5238–5568. New-diagnostics class is the W4/W5 gap.
A2	Exact commands and expected failure signatures recorded	Met (not re-verified per record)	Each record names the planted edit, the `cargo test … conformance_<id>` command and the failing output.
A3	Complete `just vv` passes only after defects removed	Not checked here	~700 runner-minutes; left to CI.
–	`VERIFICATION.md:17` still says "all 351 conformance tests"	Missing	Stale (414 registered).

Proposed PRs, one topic each, all draft, no language or compiled-record changes:

Exhaustiveness audit (W3/D2): add the Lean backend, snapshot/charge and calculus-AST sources to repo_model::exhaustive, replace the silent arms, plant a wildcard, record it. Needs a decision: does the audit also name the LaTeX backend, and is it a new register row or an extension of PD-07?
VERIFICATION.md records (W5): the 16 IDs whose negative already exists, then the 9 that need a plant.
Negative fixtures (W4): the CLI-reachable codes among the 18, with a recorded reason for the rest. Fixtures add expected records, not new diagnostics on committed sources.
VERIFICATION.md:17: drop the stale count.

Per my brief I'll start on the items that need no design decision (3, 4, and the record-only half of 2) if I hear nothing in 2 hours. 1 waits on your scope call.

Generated by Claude Code

Draft PR #194 (80deecbeb): planted-defect records in VERIFICATION.md for 17 of the 25 unrecorded IDs, plus the stale "351" count. Each plant was run alone, observed failing, and restored.

Eight IDs are not covered: DF-18, PF-19, TC-05, NE-01, MD-03, MD-05, MD-11, LM-02. Their cases reach a Lean-backed gate before the negative assertions, and this session's host has no pinned toolchain, so they need a plant run on a host with Lean. The PR names them as not recorded.

Next: negative fixtures for the 18 codes added since v0.3.

Generated by Claude Code

Draft PR #195 (e06283b27): negative fixtures for LLC0108, LLC0201–0204 and LLT4013, each planted against and recorded. The other twelve codes of the list cannot be expressed as a §28.2 fixture (the reason per code is in VERIFICATION.md; mainly the workspace file must be in a strict ancestor of the project root, and a fixture only carries project/). The 26 older codes are not started.

Next: the exhaustiveness audit (new register row, one plant).

Generated by Claude Code

Draft PR #199 (160d9ed88): new row SM-34, the exhaustiveness audit (DoD 2). One whole-tree audit in validate-model: a match naming ≥5 variants of a closed IR/calculus/Rust-AST enum must name all of them. It found 27 silent catch-alls (the Lean backend's _ => "graphTopological" among them); 25 are now explicit, with generated output unchanged (goldens, check-calculus, unit tests equal). Plants are recorded in VERIFICATION.md.

Two catch-alls remain in calculus/rust/{lower,validate}.rs: their bytes are recorded in the compiler-semantics ID (rust_renderer), so editing them moves that ID. The audit tolerates exactly those two files and fails as soon as either is clean. Maintainer decision requested in the PR body (fold into the next renderer change, or move the record now).

Status of the plan: #194 (records, 25 IDs), #195 (6 fixtures), #199 (SM-34) are all draft. Not started: the older 26 codes without fixtures.

Generated by Claude Code

Draft PR #205 (ddbcf7de5): negative fixtures for 14 of the 26 older codes (LLL1001/1003/1006, LLP2001/2004, LLF5002/5004, LLC0002, LLS8003, LLR3002/3006, LLB6002, LLT4004, LLV7007), each planted against; conformance_ex_07 passes in full with Lean. The other 12 are listed with reasons in VERIFICATION.md.

One finding for the maintainer: LLC0001 diagnostics have no primary span, but diagnostic.schema.json requires one, so no usage-error fixture can pass EX-07's schema check. Either the emitter or the schema needs to move; I changed neither.

Summary of my #33 PRs, all draft: #194 (records, 25 IDs), #195 (6 fixtures), #199 (RP-15 audit; moves rust_renderer), #205 (14 fixtures).

Generated by Claude Code

Renumber the devcontainer pin row to RP-16

Draft PR #209 (8659837ed): the diagnostic schema now requires primary except for the eight codes the emitter issues without a source position (LLC0001, LLC0101, LLC0108, LLC0201, LLS8001, LLV7008, LLV7010, LLV7102), listed in the schema and SPEC §20.1, with the LLC0001 fixture and two recorded plants. It moves the compiler-semantics identity (the schema is hashed); nothing is regenerated.

Correction to #195: its LLC0201 and LLC0108 fixtures also omit primary, so they would have failed EX-07's schema check; they pass once #209 lands.

All five #33 PRs are draft: #194, #195, #199, #205, #209.

Generated by Claude Code

Closing status of my #33 lane (all PRs draft; waves as the maintainer set them).

PR	Discharges (audit row)	Wave
#194	W5: planted-defect records for all 25 merged IDs the audit named, plus the stale "351 tests" count	non-identity
#205	W4: fixtures for 14 older codes (LLL1001/1003/1006, LLP2001/2004, LLF5002/5004, LLC0002, LLS8003, LLR3002/3006, LLB6002, LLT4004, LLV7007), each planted; `conformance_ex_07` green with Lean	non-identity
#195	W4: fixtures for 6 newer codes (LLC0108, LLC0201–0204, LLT4013)	identity wave, after #209
#209	W4: `diagnostic.schema.json` makes `primary` optional only for the 8 codes issued without a position (SPEC §20.1), plus the LLC0001 fixture and two plants	identity wave
#199	W3 / DoD 2: row `RP-15`, the classification-exhaustiveness audit; 27 silent catch-alls made explicit; moves `rust_renderer`	identity wave

Still missing, for the last pass (#34):

Fixtures: 12 of the 18 newer codes and 11 of the 26 older ones have none, with the reason per code in VERIFICATION.md (most are bound by the §28.2 runner, which gives a fixture only project/; the four source-package codes would need a workspace in an ancestor directory). The one I could not classify is LLT4002: its single emission site needs overloaded entry candidates none of which fits, and I found no input that reaches it.
DoD 4: [v0.4] RT-04: blank only test items, never the code after a cfg(test) that is not on an item (follow-up to #156) #169 and [v0.4] The tracked tree holds nothing the repository walkers skip (CACHEDIR.TAG, target, .lexlean, .lake) (follow-up to #156) #170 still need milestone v0.4 (the maintainer's to set).
A3: a complete just vv on the final heads. I ran the individual gates named in each PR body, not just vv.
The eight Lean-gated plant records in #33: planted-defect records for 25 merged IDs; drop stale test count #194 and the whole fixture suite were run with Lean 4.32.1; the identity-wave PRs will need their records regenerated before their fixture phases can run green.

Generated by Claude Code

Wave 4: SL-02 (SHA-256), BS-03 (primitive scanner), PD-08 (stack boun…

Navigation Menu

Repository navigation

[v0.4] Extend vv for production compiler, GNAF certificates, Rust artifacts, and oracle falsification #33

Scope

Work

DoD

Acceptance criteria

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[v0.4] Extend vv for production compiler, GNAF certificates, Rust artifacts, and oracle falsification #33

Description

Scope

Work

DoD

Acceptance criteria

Activity

afflom commented on Oct 15, 2026

humuhumu33 commented on Oct 18, 2026

afflom commented on Oct 18, 2026

afflom commented on Oct 18, 2026

afflom commented on Oct 18, 2026

afflom commented on Oct 18, 2026

afflom commented on Oct 18, 2026

afflom commented on Oct 18, 2026

afflom commented on Oct 18, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions