Repository navigation
test-claim consolidation design: unified resolved-type claim system + one runner + migration/equivalence plan; no implementation before Mgr-C/parent gate - #4553
Conversation
Parent gate feedback: name BoolWitness as first-class arm alongside NodeCorpus, model-first verification.dag substrate delta, one runner with preserved modality boundary, and v4_roster_pilot deletion gated on discovery equivalence. Co-authored-by: Cursor <cursoragent@cursor.com>
Drop receipt field from BoolWitness registration arm; define run artifacts only on BoolWitnessRun inside CorpusEvalReport. Remove undefined BoolWitnessReceipt type; align §3.2 substrate delta. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Addressed both findings in bc8dd2f follow-up:
Phase 1 implementers now have one receipt story: descriptors on — sent from zesty-otter-154 |
…n + equivalence witness Land mechanical bool_witness_from_roster_row projection, compile-time substrate_equivalence_holds tranche, and Mgr-C cut-list so Phase 2 runner dispatch can bind on UnifiedTestClaim without model-after-implement. Co-authored-by: Cursor <cursoragent@cursor.com>
…/UnifiedTestClaim, gated PR with before-after cut-list and execution-equivalence tranche (#4576) * WIP: Consolidation #4553 Phase 1: model-first verification.dag BoolWitness/Un * feat(v4): complete #4553 Phase 1 substrate tranche — roster projection + equivalence witness Land mechanical bool_witness_from_roster_row projection, compile-time substrate_equivalence_holds tranche, and Mgr-C cut-list so Phase 2 runner dispatch can bind on UnifiedTestClaim without model-after-implement. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): use match for UnifiedTestClaimModality checks in substrate equivalence The v4 parser rejects `==` on coproduct variants (EqEq at expression site); discriminate modality with exhaustive match instead so ci_floor_emit M1 probe passes. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Consolidation #4553 Phase 1: model-first verification.dag BoolWitness/Un * WIP: Consolidation #4553 Phase 1: model-first verification.dag BoolWitness/Un * fix(v4): address #4576 review — Symbol witness identity, dissolution receipts, fail-closed projection BoolWitness.function lands as Symbol per design §3.1; roster rows gain function_symbol pins while keeping function String for shell transport. Add coproduct dissolution classifications, replace fabricating total accessors with unified_test_claim_bool_witness Outcome projection. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Consolidation #4553 Phase 1: model-first verification.dag BoolWitness/Un * WIP: Consolidation #4553 Phase 1: model-first verification.dag BoolWitness/Un * WIP: Consolidation #4553 Phase 1: model-first verification.dag BoolWitness/Un * WIP: Consolidation #4553 Phase 1: model-first verification.dag BoolWitness/Un * fix(v4): complete phase1 roster symbol bridge after merge * WIP: Consolidation #4553 Phase 1: model-first verification.dag BoolWitness/Un --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
Land unified runner modality dispatch in testclaim_corpus_runner.dag — NodeCorpus manual wedge + BoolWitness v4_roster_pilot slice with compile-time pilot equivalence witnesses. v4 0-diag verified. Co-authored-by: Cursor <cursoragent@cursor.com>
…r — operator wants it running again ASAP). PRIORITY 1 = glob-discovery / roster-dissolution (consolidation #4553 Phases 2-5, now ownerless): the MODEL landed (#4576: UnifiedTestClaim = NodeCorpus | BoolWitnessClaim in std/verificat (#4600) * WIP: Mgr-C SUCCESSOR (re-establish the auto-archived witty-pike-248 cluster — * Fix unified corpus entry labels * WIP: Mgr-C SUCCESSOR (re-establish the auto-archived witty-pike-248 cluster — * WIP: CONSISTENCY-REVIEW CLEANUP lane (operator wants full capacity; these are * Make bool witness run states exclusive * workflow: add parallel executor frontier batches * fix: bump v4_roster_pilot row count to 75 after adding 2 scaffold claims v4_roster_pilot_claim_run_row_count and the == 73 length assertion in witness_v4_roster_pilot_declares_claim_run_rows were not updated when the structural_similarity and table_decision_tree scaffold claims were added. Now 75; witness confirmed true under --claim-run. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: PARALLEL-EXECUTOR (EXEC arc, un-deferred by operator 2026-06-09): build * document executor run-plan dissolution * WIP: Mgr-C SUCCESSOR (re-establish the auto-archived witty-pike-248 cluster — * WIP: Mgr-C SUCCESSOR (re-establish the auto-archived witty-pike-248 cluster — * Revert "Merge remote-tracking branch 'origin/session/quiet-ant-728' into session/sharp-bear-579" This reverts commit 9b51ce2, reversing changes made to f273168. * Revert "WIP: Mgr-C SUCCESSOR (re-establish the auto-archived witty-pike-248 cluster —" This reverts commit f273168. * Revert "Merge remote-tracking branch 'origin/session/fierce-eagle-903' into session/sharp-bear-579" This reverts commit f8e55dc, reversing changes made to 9da55e9. * WIP: Mgr-C SUCCESSOR (re-establish the auto-archived witty-pike-248 cluster — * WIP: Mgr-C SUCCESSOR (re-establish the auto-archived witty-pike-248 cluster — * WIP: Mgr-C SUCCESSOR (re-establish the auto-archived witty-pike-248 cluster — * Use executable witness symbols for bool claims * Add markers for merged lens roster claims * Add marker for merged parallel executor claim * WIP: Mgr-C SUCCESSOR (re-establish the auto-archived witty-pike-248 cluster — * Remove generated affected receipt --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
Rebased onto main (#4600 substrate). Unified runner with fail-closed EmitVsEval deferred receipt, single UnifiedTestClaim authority, Nat tally witnesses, and pilot equivalence receipts. Co-authored-by: Cursor <cursoragent@cursor.com>
…essClaim marker Address cursor REQUEST_CHANGES on #4624: the eval callee-dispatch keystone executed via run_test_claim but had no discoverable, CI-gated consumer (INVARIANTS E-10). Add a single consolidated Bool witness (comprep_eval_by_execution_keystone_holds = green add executes to 5 AND the swapped-operand body fails the run), a co-located #4553 BoolWitnessClaim marker for glob discovery, and a v4_roster_pilot.dag row (count 79->80) so v4_lens_ci runs it on every PR. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…er transport Fix perturb-check temp paths so the gate actually exercises the perturbed copy; add the gate to v4_lens_gate CI. Drop the glob_discovery preamble claim-run from smoke-roster (135-source compile OOMs in container sessions; list projection + per-row execution still validates the 80-row authority). Co-authored-by: Cursor <cursoragent@cursor.com>
* WIP: Glob-discovery Phase 3-5: prove discovery==roster, repoint consumers, de * WIP: Glob-discovery Phase 3-5: prove discovery==roster, repoint consumers, de * WIP: Glob-discovery Phase 3-5: prove discovery==roster, repoint consumers, de * fix(#4553): wire C9 substrate-equivalence gate and lighten smoke-roster transport Fix perturb-check temp paths so the gate actually exercises the perturbed copy; add the gate to v4_lens_gate CI. Drop the glob_discovery preamble claim-run from smoke-roster (135-source compile OOMs in container sessions; list projection + per-row execution still validates the 80-row authority). Co-authored-by: Cursor <cursoragent@cursor.com> * chore: apply cargo fmt Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Glob-discovery Phase 3-5: prove discovery==roster, repoint consumers, de * WIP: Glob-discovery Phase 3-5: prove discovery==roster, repoint consumers, de --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
- Pin independent Symbol transport authority for field-preservation laws (edit_locus_narrow_resolution_holds_symbol), not tautological self-compare. - Fix claims_root contract in v4-glob-discovery-project.sh (no source-root suffix) so impossible_bug perturb scans the correct tree. - Wire scripts/v4-glob-discovery-project.sh into testclaim corpus affected-set. Co-authored-by: Cursor <cursoragent@cursor.com>
…row.body via real callee dispatch in 05_eval (#4624) * WIP: Mgr-RUNTIME: v4-runtime / IO / compute-fabric / CI-dogfood lane. The big * WIP: Mgr-RUNTIME: v4-runtime / IO / compute-fabric / CI-dogfood lane. The big * comprep(E-10): wire eval-by-execution keystone into roster + BoolWitnessClaim marker Address cursor REQUEST_CHANGES on #4624: the eval callee-dispatch keystone executed via run_test_claim but had no discoverable, CI-gated consumer (INVARIANTS E-10). Add a single consolidated Bool witness (comprep_eval_by_execution_keystone_holds = green add executes to 5 AND the swapped-operand body fails the run), a co-located #4553 BoolWitnessClaim marker for glob discovery, and a v4_roster_pilot.dag row (count 79->80) so v4_lens_ci runs it on every PR. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * fix(comprep #4624): honest keystone relabel + 05_eval 🟡 disposition tags + Node.span integration Addresses codex BLOCKING reviews (P5/E-10, P1/P5) on #4624 via parent-approved Option A: - comprep_eval_by_execution.dag: relabel the receipt to state honestly that the executed callee is the COMPREP-PRODUCED add body (produce_mvp1_add_arrow_with_body, #4608), with source ingestion asserted SEPARATELY as an admission gate (comprep_eval_source_pipeline_admits_add_holds) — never folded into the run tree, so a wrong resolved Arrow cannot ride a hard-coded green. Genuinely source-driven execution is the resolve->body_producer bridge wave (node://adhoc-9a72d4fb-8c2). - 05_eval.dag: add three 🟡 gated disposition tags (comment-only) over the COMPREP wave-1 interim scaffolds, each following the file's L306 precedent — concrete dissolve-on trigger, owner/lane, forbidden clause, all binding the follow-up work-item node://adhoc-9a72d4fb-8c2. - Integrate main (#4604 Node.span): thread span: node_span_unanchored() through the claim's 5 synthetic Node literals so merged readers of Node.span see the carrier. - glob_discovery.dag: bump cardinality pin 80->81 for the keystone BoolWitnessClaim. Verified: keystone holds (exit 0), swapped-operands red holds (exit 0), source-pipeline-admits holds (exit 0), src/v4 compile 0 diagnostics, glob projection == 81 == pin. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… delete v4_roster_pilot (#4632) * fix(#4553): address C9 review blockers on substrate equivalence gate - Pin independent Symbol transport authority for field-preservation laws (edit_locus_narrow_resolution_holds_symbol), not tautological self-compare. - Fix claims_root contract in v4-glob-discovery-project.sh (no source-root suffix) so impossible_bug perturb scans the correct tree. - Wire scripts/v4-glob-discovery-project.sh into testclaim corpus affected-set. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Glob-discovery Phase 3-5: prove discovery==roster, repoint consumers, de --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
C9 gate now fail-closed diffs projected {entry,function} transport rows
against immutable golden and pre-delete roster snapshots; modeled witness
covers sample-marker laws only. Surfaces the +1 discovery row vs roster.
Co-authored-by: Cursor <cursoragent@cursor.com>
Clarify that discovery membership uses resolved-type arms AND the #4553 authored `data unified_claim_*` naming convention — not name-agnostic scan. Co-authored-by: Cursor <cursoragent@cursor.com>
… predicates as test fn (#5272) The 13 `data claim_*: TestClaim = BoolWitnessClaim { witness: BoolWitness { holds: f() } }` rows (timeseries_passive_map_fold_anchor_test ×7, timeseries_signal_passives_test ×6) are triple-malformed dead spec that compiled only because the v1-seed record typechecker is fail-open (`infer_record_lit` silently ignores undefined fields and never validates missing required ones): - `holds` is not a field on `BoolWitness` (which has only `entry`, `function`); - they are typed `: TestClaim`, but `BoolWitnessClaim` is an arm of `UnifiedTestClaim`, not of `TestClaim` (whose arms are Compiles/Diagnostic/Equals/StructuralEquals/RoundTrip); - wrong inner shape. The live floor discovers only `data unified_claim_*` (never `data claim_*`), so these never ran — pure dead specification, and a §3 fork of the canonical `{ entry, function }` form ratified by consolidation #4553. Asymmetry handled per §5 (do not silently drop coverage): - anchor file: its 7 predicates were already live `test fn` (#5257) — pure deletion. - signal file: only 1 of its 6 predicates was a live `test fn`; the other 5 (spice_capacitor/inductor_projects_*, passive_topology_preserves_component_name, named_affine_voltage_preserves_ground_reference, absolute_potential_from_named_preserves_reference) were plain `fn` wired ONLY through the dead `{holds}` rows — re-homed as `test fn` to RESTORE their intended floor coverage rather than orphan the assertions. Drop the now-unused `BoolWitness`/`BoolWitnessClaim` imports from both files. Green by execution: `claim_batch --source-root src/v2` over all 13 witnesses → 13 PASS, including the 5 newly-live signal predicates. Their assertions discriminate on Present/Absent (not tautological), so floor coverage is strictly increased, not faked. Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
…t hole (§5) (#5293) * Delete malformed dead {holds} BoolWitness rows; re-home 5 dark signal predicates as test fn The 13 `data claim_*: TestClaim = BoolWitnessClaim { witness: BoolWitness { holds: f() } }` rows (timeseries_passive_map_fold_anchor_test ×7, timeseries_signal_passives_test ×6) are triple-malformed dead spec that compiled only because the v1-seed record typechecker is fail-open (`infer_record_lit` silently ignores undefined fields and never validates missing required ones): - `holds` is not a field on `BoolWitness` (which has only `entry`, `function`); - they are typed `: TestClaim`, but `BoolWitnessClaim` is an arm of `UnifiedTestClaim`, not of `TestClaim` (whose arms are Compiles/Diagnostic/Equals/StructuralEquals/RoundTrip); - wrong inner shape. The live floor discovers only `data unified_claim_*` (never `data claim_*`), so these never ran — pure dead specification, and a §3 fork of the canonical `{ entry, function }` form ratified by consolidation #4553. Asymmetry handled per §5 (do not silently drop coverage): - anchor file: its 7 predicates were already live `test fn` (#5257) — pure deletion. - signal file: only 1 of its 6 predicates was a live `test fn`; the other 5 (spice_capacitor/inductor_projects_*, passive_topology_preserves_component_name, named_affine_voltage_preserves_ground_reference, absolute_potential_from_named_preserves_reference) were plain `fn` wired ONLY through the dead `{holds}` rows — re-homed as `test fn` to RESTORE their intended floor coverage rather than orphan the assertions. Drop the now-unused `BoolWitness`/`BoolWitnessClaim` imports from both files. Green by execution: `claim_batch --source-root src/v2` over all 13 witnesses → 13 PASS, including the 5 newly-live signal predicates. Their assertions discriminate on Present/Absent (not tautological), so floor coverage is strictly increased, not faked. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Enable strict record-field typecheck: close fail-open infer_record_lit hole The v1-seed typechecker (infer_record_lit) was fail-OPEN on record construction — it silently ignored fields that exist on no variant of the constructed type (DESIGN.md §5: "a wrong answer is a loud error, never a warning"). That hole is what let the malformed `BoolWitness { holds }` rows typecheck green (see #5272). Closing it. Host change (src/v1/stage0/src/v1_compiler_infer.rs): - record_lit_construction_field_names: a *confident* field-name resolver that follows `type X = Y` aliases and searches the expected coproduct's arms before the global fallback (the two resolver-precision gaps the leniency was compensating for: `Set<T> = PointwisePower<T>` alias; variant-vs-collection name collisions like `GrammarExpr.Optional`). Returns None when not confident so anonymous/unresolved records never false-positive. - field_in_any_variant_named: an ambiguity-aware secondary scan, run only on would-be-errors, that suppresses false positives where a field is valid on a same-named variant of *another* coproduct (e.g. TextNode) while keeping teeth on truly-undefined fields. - emit CompilerDiagnostic::FieldNotFound for an unknown constructed field. Real bugs this surfaced (silently tolerated before; field name was wrong): - infer_ground_add_mvp.dag: `NodeLocus { node }` → `node_locus(node:)` (the field is `anchor`). - 3 lens/application tests: `PortLocus { port }` → `port_locus(port:)` (the field is `anchor`). Proven by execution: full claim_batch floor green (439 witnesses) with the check live; probe `BoolWitness { holds }` goes red with "field 'holds' not found in type 'BoolWitness'". Missing-required-field enforcement deferred (optional-cardinality + templating risk, unmeasured). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Strict record-field check: port to .dag authority + de-conflict TextFile (§3/§7) Per the §3/§7 review (cursor): the strict infer_record_lit check lived only in the generated seed .rs (a host hand-edit), not the .dag authority. Port the helpers and the infer_record_lit guard into src/v1/04_infer.dag so the seed is regenerated FROM the model: - record_lit_construction_field_names: confident field-name resolver (alias-follow + expected-coproduct-arm union), SKIPS generic/parametric types (newtype flattening makes their resolved field names non-source-faithful — the algebra-tower false positives). - field_in_any_variant_named: same-named-coproduct-arm ambiguity guard, run only on a would-be error (keeps TextNode-style constructions silent; full teeth elsewhere). - infer_record_lit emits FieldNotFound for a field on no field of a confidently-resolved non-generic record; none-result paths stay silent (no false positives). §3 de-confliction: two 'type TextFile' collided in the bootstrap's combined src/v1+dsl closure — v1 {path, content} (emit output) vs dsl/std {path, document} (markup). The name-keyed type env clobbered one, so the strict check could not resolve 'content'. Rename the dsl one to DocumentFile (it holds a Document; parallel to its sibling RenderedTextFile), the smaller + semantically-correct fix. v1 TextFile {path, content} is now the sole binding. The regenerated .rs follows (regen against current main's seed, post-merge). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Strict record-field check: tighten resolver to confident-only (§5 no false positives) The struct_fields/expected-based resolver false-positived on main's newer types where resolved field names diverge from source under newtype flattening / name collision: - `Watt = Measure<Power,One,Nat>` etc. — concrete aliases of the single-field generic `Measure<Q,S,M> { count: M }`; the wrapper dissolves so `count` isn't in the resolved set. - `Vendor { legal_name }` — a §3 name collision: `extdeps Vendor<Domain> { legal_name }` record vs the std `Vendor = UnknownVendor | ...` enum; lookup grabs the enum. Replace it with a confident-only resolver: fire ONLY when the constructed name resolves to a plain, fully-grounded record (params == 0, connective == Conj, children > 0), reading source field names directly from its own children. Generics, concrete aliases of single-field generics, and coproduct/enum (incl. the losing side of a collision) all return none -> silent. Keeps full teeth on plain records, where every real bug lives (BoolWitness{holds}, NodeLocus{node}, PortLocus{port}). Drops the now-unused record_lit_expected_coproduct_arm. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Regenerate stage0 seed (v1_compiler_infer.rs) from 04_infer.dag The committed seed is the compiler's own emit of the strict 04_infer.dag authority (derived, not hand-edited) — closes the §3/§7 review: the strict infer_record_lit check now lives in the .dag model and the .rs is regenerated from it. Single-file diff (+136/-1, no new module deps): only 04_infer.dag changed, so only its emitted module changes. Proven by execution on the merged tree: - floor (claim_executor over src/v2+dsl): 0 field-not-found false positives - self-compile (src/v1+dsl via regen path): 0 field-not-found - cargo fmt --all --check + cargo clippy --all-targets -D warnings: clean - discriminating probe: `BoolWitness { holds: true }` -> loud 'field holds not found in type BoolWitness' Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Summary
Revised design (per Mgr-C gate feedback): test-claim consolidation as a dual-modality unified system, not Node-corpus-only laundering.
UnifiedTestClaimcoproduct:NodeCorpus { TestClaim + TestClaimEvalSubject + transport }|BoolWitness { entry, function, receipt }— discovered by resolved-type heads.verification.daglandsBoolWitnessarm first (load-bearing L2.5 gate before runner implementation).fn() -> Boolwitnesses stayfn() -> Bool; no mandatory projection toTestClaimEvalSubject<Node>.run_unified_corpus_evaldispatches by modality;CorpusEvalReporttagsNodeCorpusRunvsBoolWitnessRun(modality boundary not erased).v4_roster_pilotdeletion gated on C9–C11: discovered BoolWitness set == roster, run-equivalence, perturb discrimination.Full artifact:
docs/planning/test-claim-consolidation-design-2026-06-08.mdDocs only — no implementation. Subordinate to ctrl#1490.
Test plan