Make the vacuity lens honest and live: real-corpus classifier, bound consumer witness, typed falsification roster (4/4/4 correction), self-application

[briansrls]

Auto-opened by session-dashboard for session jolly-fox-325.
Pushing to session/jolly-fox-325 advances this PR.

Worker attestation

• Title describes the change (not the session id or branch).
• PR body summarises what and why (replace the TODO below).
• Tests run: name the command (e.g. npm test, cargo test) and the result.
• If this closes a work item, the body contains a Closes #N directive.
• No commits on this branch are surprises (no fork/cherry-pick I did not make).
• No secrets / credentials / large binaries staged.

Summary

Makes the vacuity lens (v2.lens.vacuity, which classifies whether a test is a genuine
check or a redundant restatement of the code it tests) honest and live, per the operator
ruling triggered by PR #7614.

Headline finding, not a footnote: the falsification suite's hand-reconciled 4/6/2
distribution pin wasn't merely non-diagnostic — it asserted a FALSE fact about the
classifier, and nothing executed it so nobody could tell. Three suite rows are
labeled _behavioral (diagnostic_behavioral, round_trip_behavioral,
compiles_unknown_provenance), but all three actually pass
operand_provenance: OperandProvenanceUnknown, not BehavioralComputation — the label
names the TestClaim variant under test (DiagnosticClaim/RoundTripClaim), not an
asserted provenance. classify_test_claim_vacuity's DiagnosticClaim/RoundTripClaim
arms and the CompilesClaim same-eval unknown-provenance path therefore correctly
return Unknown for all three, not the ProvenIndependent the stale 4/6/2 pin
implicitly assumed. The real, execution-confirmed distribution is 4/4/4
(proven_duplicate=4, proven_independent=4, unknown=4), confirmed twice: once by
hand-tracing the classifier's decision tree against every row's actual inputs, and
independently by direct execution (three isolated debug assertions against the real
computed census, since removed in favor of the permanent roster below).

Seven changes:

1. LiveSurfaceSnapshot provenance added.
2. Ordinary BoolWitnessClaim bodies now route through a real-corpus classifier
   (filesystem_read → tokenize/parse_module/normalize), with two documented,
   empirically-confirmed ceilings (a bare-==-body shape, and — broader — fn-declaration
   collection itself, both tracing to the same DESIGN.md "general body producer" open
   thread, not two separate ones).
3. Two fail-open classifier bugs fixed.
4. lens_contract_vacuity.mode stays AuditOnly (staging constraint, untouched).
5. lens_contract_vacuity.consumer_witness is now a real BoundConsumerWitness
   pointing at the strongest available RED-control test
   (vacuity_consumer_witness_pr7614_shape_red_control_classifies_proven_duplicate).
6. The falsification suite's hardcoded distribution pin is replaced with a typed
   VacuityFalsificationCaseId/VacuityFalsificationCase roster whose per-case
   expected field is derived by hand-tracing the classifier, verified by execution.
   The census test's aggregate counts (proven_duplicate_count, etc.) are now
   derived from the roster's own expected column via vacuity_falsification_expected_count
   (a count_where fold) — never hardcoded a second time — so the two representations
   of the same fact can never silently drift apart again.
7. Self-application: the live-corpus census now genuinely walks vacuity-owned content
   via a real compile-time symbol reference from a discovered witness
   (vacuity_consumer_witness_fixture_module_reached_by_direct_call), not merely a
   filesystem_read string path — closing an inert-lens hygiene gap the module-graph
   walk (DESIGN.md §6) caught mid-PR.

Honest disclosure, kept prominent (not softened or buried): the consumer-witness
identity join (vacuity_consumer_witness_test.dag) currently reconciles by real
execution, but the derived-site side is legitimately empty today — fn-declaration
collection over normalize() output returns empty for real corpus files corpus-wide
(see vacuity_bool_witness_fn_decl_collection_ceiling_note in v2.lens.vacuity and
vacuity_consumer_witness_derived_sites_ceiling_note in the witness file). So the join
currently holds vacuously (empty == empty), not because the mechanism is proven
against a nonempty real-corpus example. The classifier's ProvenDuplicate-detection
logic itself is proven correct separately and non-vacuously by a direct-call RED control
that bypasses the ingest pipeline
(vacuity_consumer_witness_pr7614_shape_red_control_classifies_proven_duplicate).
Mechanism correctness and real-corpus reachability are two different claims, and only
the first is non-vacuous today; the second stays ceilinged on the same "general body
producer" DESIGN.md open thread until that lands.

Known-red CI check, inherited (not introduced by this diff)

ci currently fails on extdeps_scope_placement_gate_passes. Root cause (confirmed by
calm-badger-682, the extdeps-frontier lane owner): dag/extdeps/session_dashboard.dag
is the only extdeps file added since the frontier freeze anchor and is not enrolled in
any of the three frontier rosters on main — every context that sees main's current
content reds on this gate, independent of this PR's own diff. A merge of origin/main
into this branch (423f789755) was attempted per initial guidance and did not clear it
(root cause is upstream of the merge, not a stale-branch artifact) — that guidance was
retracted once the real cause was found. This is being tracked and owned upstream; no
action is being taken on it from this PR, and dag/gunbc/legacy_extdeps_scope_frontier.tsv
is deliberately untouched here.

A second, unrelated pre-existing defect was found as a side effect of this PR's
real-corpus classifier work and is being tracked/owned separately (not fixed here):
cost_coverage's own already-merged witnesses (cost_coverage_dag_logic_has_three_fn_bodies,
cost_coverage_v2_tree_receipt_by_execution) fail by direct execution on a pristine
origin/main checkout — reported to calm-badger-682 as its own standalone finding.

Test plan

All claims below verified green by direct execution via
./target/release/claim_batch --source-root dag --source-root src/v2 --entry <file> --functions <fn>
(built locally with CTRL_BUILD_BYPASS_SHIMS=1 cargo build --release --bin claim_batch
— plain cargo build in this environment silently discards its output to a remote
sandbox and does not produce a runnable local binary).

• src/v2/lens/vacuity_test.dag — all 10 test fns PASS, including the new
  vacuity_falsification_cases_each_match_expected_evidence (every case's classifier
  output matches its declared expected) and the rewritten
  vacuity_advisory_census_partitions_falsification_suite (aggregate counts now
  derived from the roster, confirmed 4/4/4).
• src/v2/test/claim/vacuity_consumer_witness_test.dag — all 6 relevant test fns PASS,
  including the fixture-module-reach test and the direct-call RED control.
• CI: build, regen, heal_generated_artifacts pass on the current head; ci fails
  only on the inherited, upstream-owned extdeps_scope_placement_gate_passes gate
  described above.

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

[gunbai-bot]

Addressed both findings from review 46886, verified against the current code and fixed:

1. Consumer-witness overclaim (contract.dag:509). Confirmed: lens_contract_vacuity.consumer_witness was bound to vacuity_consumer_witness_pr7614_shape_red_control_classifies_proven_duplicate, which hand-constructs a VacuityEvidenceRecord and calls classify_vacuity_same_eval_record directly — it never runs corpus ingestion. Rebound the contract to vacuity_consumer_witness_derived_equals_classified_sites, which actually executes the real-corpus path (filesystem_read → ingest → vacuity_collect_fn_decls → classify) and performs the derived/classified join. The RED control stays enrolled (it's the only proof that classify_vacuity_same_eval_record correctly detects ProvenDuplicate when reached) but is no longer what the contract cites as the bound consumer, since "mechanism is correct when reached" and "a live corpus consumer is bound" are different claims. Updated vacuity_consumer_witness_note to state this precisely rather than leaving it ambiguous. Verified by execution: claim_batch over all 5 witnesses in the file, all PASS, including the newly-bound function.

2. Untracked coproduct predicate (vacuity.dag:173). Confirmed: vacuity_operand_provenance_is_live_snapshot_duplicate_partner is a hand-matched predicate over TestClaimOperandProvenance with no disposition of its own — its sibling operand_provenance_is_independent_oracle carries a 🟡 dissolve-on note (line 51) but that note doesn't cover the new predicate. Added vacuity_operand_provenance_live_snapshot_duplicate_partner_predicate_dissolution_note, same dissolution trigger as the sibling (containment-tree-projected provenance / a single canonical accessor replacing both hand-matched predicates at once).

Pushed as part of 4e8ee4439b.

— sent from jolly-fox-325

[gunbai-bot]

Addressed review 46910 in e9a89d0.

Both findings confirmed against current code and fixed, not just acknowledged:

• vacuity_consumer_witness_classified_sites was a pure passthrough of vacuity_consumer_witness_live_derived_sites() — confirmed the derived_equals_classified_sites witness was literally x == x, structurally incapable of RED regardless of what the ingest/classify pipeline does. Fixed by restructuring classified_sites to fold every derived site through vacuity_consumer_witness_evidence_for_site (which calls classify_unified_test_claim_vacuity) with an exhaustive match over VacuityEvidence, so the result now depends on classification genuinely executing. The set membership still coincides with derived_sites under today's total classifier (no site is ever dropped by classification), so the join stays honestly vacuous while the corpus-wide fn-decl-collection ceiling holds (unchanged) — but it is no longer definitionally identical, and a future regression that made classification skip or crash on a site would now be observable here.
• Took recommendation (a): rebound lens_contract_vacuity.consumer_witness to vacuity_consumer_witness_fixture_ingest_is_accepted_by_execution, which genuinely runs filesystem_read + the real ingest pipeline and returns false (RED) on Rejected. This is the witness in the file that can actually fail on a real ingest/parse regression, independent of the fn-decl-collection ceiling that keeps any fold-based join vacuous today.

Both fixes verified by real claim_batch execution (not typecheck-only) — all 5 witnesses in vacuity_consumer_witness_test.dag PASS, including derived_equals_classified_sites (now genuinely exercising classification) and fixture_ingest_is_accepted_by_execution (the new bound witness).

Updated vacuity_consumer_witness_note to describe the current binding and both corrections (46886 then 46910) rather than leaving it describing the superseded review-46886-era state.

— sent from jolly-fox-325

[gunbai-bot]

Addressed review 46930 in b11df77.

Both findings verified against current code and fixed:

• Confirmed: fixture_ingest_is_accepted_by_execution (the witness bound at the time of this review) only proves the fixture file ingests — it never calls classify_unified_test_claim_vacuity or checks its output, so a real classifier regression could stay green under that binding. Rebound lens_contract_vacuity.consumer_witness to vacuity_consumer_witness_real_test_fn_gap_stays_unknown_by_execution, which does call the classifier with a BoolWitnessClaim naming a real file/function; that call performs real filesystem_read + ingest + fn-decl lookup internally (vacuity_bool_witness_evidence, vacuity.dag:454) before classifying, and the test asserts the returned VacuityEvidence equals Unknown — the honest current answer given the documented fn-decl-collection ceiling. A classifier regression that returned ProvenDuplicate/ProvenIndependent here instead of failing closed would RED this witness. Verified by real claim_batch execution (all 5 witnesses PASS).
• Confirmed: the vacuity_operand_provenance_is_live_snapshot_duplicate_partner predicate's dissolution note named a trigger but no bounded owner/lane. Added a companion disposition note in the Owner/Lane/Dissolve-trigger shape precedented by docs/plans/e0599-implementation-proposal.md §3.0 (rather than inventing a new format) — Owner: v2.lens.vacuity, Lane: the vacuity-lens item-5 consumer-witness lane (this PR and its direct follow-ons), Dissolve trigger unchanged from the existing note.

— sent from jolly-fox-325

[gunbai-bot]

Addressed review 46947 (both findings), commit 47f4ac8.

Finding 1 (witness ambiguity): confirmed — vacuity_bool_witness_evidence has two independent Unknown-producing branches (ingest Rejected, fn-lookup Absent) plus the genuine-inconclusive-body branches, and the previously-bound witness asserted only the collapsed == Unknown result, so it couldn't distinguish honest fail-closed classification from total pipeline breakage. Fixed by rewriting vacuity_consumer_witness_real_test_fn_gap_stays_unknown_by_execution to assert three independent facts rather than the collapsed one: (1) ingest of the target file is Accepted, (2) the target fn symbol is genuinely Absent from real fn-decl lookup (vacuity_find_fn_decl_by_name over vacuity_collect_fn_decls) on that same parsed module, and (3) classification on the identical claim still returns exactly Unknown. An ingest regression, a fn-decl-collection change, or a classifier bug that fabricated a non-Unknown result despite genuine Absent each independently red this witness now.

I could not honestly go further to "reach a supported real-corpus case" with a non-Unknown classification, per the request's most literal reading: vacuity_bool_witness_fn_decl_collection_ceiling_note documents, by direct execution on this branch and on a pristine origin/main checkout, that fn-declaration collection returns empty for every real corpus file today regardless of body shape — so no real file/function pair currently exists for which the classifier can honestly reach its body-evidence path at all via the real ingest pipeline. Asserting a non-Unknown result would itself be the fabricated-plausible-output failure DESIGN.md §5 forbids. The three-part shape above is the strongest honest witness available at the current ceiling — see vacuity_consumer_witness_real_test_fn_gap_distinguishes_failure_note in the diff for the full rationale, and vacuity_consumer_witness_note for the fourth-correction history.

Also swapped the target file/fn from src/v2/lens/vacuity_test.dag (which itself contains test fn declarations and rejects at the file-parse stage per the grammar ceiling — verified by execution, this made the old Rejected-path Unknown, not a genuine Absent-path Unknown) to the already-established Accepted-ingesting fixture (vacuity_consumer_witness_scan_file()) with a plainly nonexistent probe-target symbol, so the "genuinely Absent" assertion is honestly meaningful.

Finding 2 (positional citations): confirmed all three — vacuity.dag's pre-existing "line 51's note" reference, my own newly-added "line 51's note" reference, and my own newly-added vacuity.dag:454 reference in the test file. All replaced with the actual symbol names (vacuity_operand_provenance_independent_oracle_predicate_dissolution_note, vacuity_bool_witness_evidence) per DESIGN.md §3. Verified none remain via grep.

Verified by real claim_batch execution: all 5 witnesses in vacuity_consumer_witness_test.dag PASS, including the strengthened one.

— sent from jolly-fox-325

[gunbai-bot]

Addressed review 47124 in 6a2cdef (both findings, verified by real claim_batch execution, not just typecheck):

1. vacuity_consumer_witness_classified_sites was appending every site regardless of evidence (including Unknown), making the derived/classified set-equality check invariant to classifier output. Fixed: Unknown-classified sites are now dropped instead of kept.

2. The bound witness only ever exercised classify_unified_test_claim_vacuity's Absent-fn arm, whose honest answer is Unknown — so a wholesale collapse of the dispatcher to _ => Unknown would still have passed. Added a second, independent assertion inside the same bound function that drives the same public dispatcher through its NodeCorpus{EqualsClaim} arm with LiveSurfaceSnapshot/LiteralOracle provenance (the PR Repair main red: interpreter primitive surface census #7614 shape) and asserts ProvenDuplicate.

Proved the fix actually closes the gap by mutation: temporarily collapsed classify_unified_test_claim_vacuity to unconditionally return Unknown, confirmed the witness reds by execution, then restored the real classifier (verified byte-identical via git diff --stat) and confirmed all 5 witnesses in this file pass again.

Reviews 47136 and 47143 (APPROVE, non-blocking) don't call for further changes beyond this.

— sent from jolly-fox-325

[gunbai-bot]

review 47204 addressed: fixed at 400245a. The consumer-witness function real_test_fn_gap_stays_unknown_by_execution moved to src/v2/test/claim/long/vacuity_consumer_witness_long_test.dag as part of the fix for the eval-budget CI failure on this branch (that fn measures ~89s, well over the 5s fast-lane ceiling — DESIGN.md's operator 5s rule). lens_contract_vacuity's ScheduleWitnessEntry.entry was left pointing at the old vacuity_consumer_witness_test.dag path in that same commit, exactly the stale pointer you found. Repointed to the long-lane file; verified the contract record resolves cleanly by execution.

— sent from jolly-fox-325

[gunbai-bot]

Addressed review 47215: vacuity_falsification_suite_rows was a manually maintained roster duplicating the same 12 rows already carried by vacuity_falsification_suite_cases's row field. Fixed in 9ffa89c by deriving it via list_map(xs: vacuity_falsification_suite_cases, f: fn(c) { c.row }), so the two can no longer independently drift. Verified by execution: vacuity_falsification_cases_each_match_expected_evidence, vacuity_advisory_census_partitions_falsification_suite, and vacuity_falsification_suite_nonempty all PASS.

— sent from jolly-fox-325

[gunbai-bot]

review 47233 addressed in 99739dd.

Confirmed the finding: lens_contract_vacuity.consumer_witness (src/v2/lens/enforcement/contract.dag) binds to vacuity_consumer_witness_real_test_fn_gap_stays_unknown_by_execution, which lives in src/v2/test/claim/long/vacuity_consumer_witness_long_test.dag. That directory is excluded from per-PR fast-lane discovery, and the witness was absent from falsifier_substrate_long_lane_rows — so it had zero scheduled execution anywhere in CI, only a manual local claim_batch recipe. That's the exact DESIGN.md §5 specification-without-execution class the vacuity lens itself exists to catch, reproduced in its own bound consumer witness.

Fix: enrolled all 4 witness fns in that file into falsifier_substrate_long_lane_rows (dag/gunbc/ci_layer_roots.dag), each with a reason citing this review and its measured cold-eval time, and a dissolve_on matching the sibling rows' pattern. This gives the bound witness (and its 3 fixture-ingest siblings in the same file) a genuine nightly falsifier execution path via falsifier_substrate_long_lane_entries, per the existing pattern at ci_layer_roots.dag around the fallback_arm_census_self_applies_holds row.

Checked consumer_observed_for (src/v2/lens/enforcement/receipts.dag:115-131): its ci_entries/prepush_entries params are the explicit commit-gate roster, disjoint from the falsifier long-lane roster — so this fix does not (and should not) change the witness's ConsumerKind classification; it correctly stays WitnessOnly, now backed by real scheduled execution instead of none.

Verified by execution:

• claim_batch --entry dag/gunbc/ci_layer_roots.dag --functions falsifier_substrate_long_lane_entries resolves/typechecks cleanly and the roster now carries 21 entries (17 prior + 4 new), correct field values.
• falsifier_substrate_long_lane_batch_holds (the batch-shape invariant test at src/v2/test/claim/ci_floor_plan_witness_test.dag:489, self-referentially length-checked against falsifier_substrate_long_lane_entries()) PASSes against the enlarged roster.
• All 4 new rows' measured cold evals (88996ms / 88996ms / 32423ms / 29754ms) sit comfortably under the falsifier lane's existing 180s dated budget ceiling — no re-basis needed.

— sent from jolly-fox-325