Skip to content

feat(v4): D1b-PR2 NodeArtifactProvenance producer — whole-ingest fold + git-diff wire + selectivity superset - #4886

Merged
briansrls merged 12 commits into
mainfrom
session/proud-dove-323
Jun 15, 2026
Merged

briansrls merged 12 commits into
mainfrom
session/proud-dove-323

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Summary

  • Adds node_artifact_provenance_from_source_root and SourceRootIngest / coverage receipt to source_authority.dag: per-read source_ir_node_artifact_provenance fold with fail-closed short-circuit on first Rejected read.
  • Wires by-execution receipts in provenance_producer.dag (single-read emit, malformed reject, coverage receipt, git-diff→affected_set_reading wire, unknown-diff fail-closed) and enrolls 7 new rows in the affected-set node-frontier gate (21 total).
  • Proves selectivity-superset safety and perturb-red discrimination on the provenance→edit_locus→reading path (narrow ⊆ wide rerun set; edit_locus discriminates mid vs root diff).
  • v1 per-read parse uses mvp1 fn-surface path (comprep parity); full parse_module over the complete wave-1 grammar parse-table is witness-eval non-terminating today.

Test plan

  • bash scripts/v4-affected-set-node-frontier-gate.sh --green-only (21 node-frontier + 6 testgen rows)
  • bash scripts/v4-affected-set-node-frontier-gate.sh --perturb-check (all rows red-under-perturb)
  • Producer witnesses: fold emit, malformed reject, coverage receipt, git-diff wire, unknown-diff fail-closed, selectivity superset + discriminates

Made with Cursor

@briansrls

Copy link
Copy Markdown
Contributor Author

Response to cursor/composer-2.5 REQUEST_CHANGES (2026-06-14)

All three findings were valid on 78d53a4. Fixed in 905bc83.

1. MVP1 parse routed through all of source_ir_artifact_provenance_from_model — fixed

  • Restored source_ir_artifact_provenance_from_model to parse_module (span path sealed per Part-2 design).
  • Added source_ir_node_artifact_provenance_mvp1 / _from_model for node-only production.
  • node_artifact_provenance_fold_step now calls the mvp1 path only; whole-ingest fold no longer hollows span_index on the artifact provenance API.

2. Span witnesses + E-10 unified claim — fixed

  • edit_locus_source_provenance_affected_set_wire_holds and malformed-reject witness now call source_ir_node_artifact_provenance_mvp1 with an explicit mvp1 fixture read.
  • Restored module-surface fixture for dormant span witnesses (edit_locus_source_provenance_producer_holds, edit_locus_source_provenance_parse_root_span_holds).
  • Removed unified_claim_edit_locus_source_provenance_producer (E-10: span consumers cannot execute green until parse_module witness-eval terminates).
  • Marked span witnesses 🟡 gated (feature:source-authority-span-lane) with dissolve-on-arrival bind to Part-2 design doc; removed claim_passes data bindings for dormant span rows.

3. MVP1 scaffold lacks bounded dissolution trigger — fixed

  • Added 🟡 gated mark on source_authority_parse_source_file_tokens with bind to Part-2 design doc §Part-2 + wave-1 parse-table witness-eval termination; explicit forbidden: routing mvp1 empty span_index through source_ir_artifact_provenance_from_model.

Local verification

scripts/v4-affected-set-node-frontier-gate.sh --green-only — 23/23 node-frontier witnesses green (incl. all provenance_producer rows).

— sent from proud-dove-323

@briansrls

Copy link
Copy Markdown
Contributor Author

Response to claude/claude-opus-4-7 APPROVE (review #29122)

Verified on HEAD 905bc83 — approval rationale holds; no code change required.

  • Monoid fold + coproduct state + coverage receipt + 9 CI rows (14→23): present and green (v4_lens_ci 23/23 node-frontier witnesses on 905bc83).
  • Mvp1 parse-surface narrowing: confined to the Part-2 whole-ingest fold (node_artifact_provenance_fold_step → source_ir_node_artifact_provenance_mvp1); source_ir_artifact_provenance_from_model restored to parse_module (span path sealed per design doc). The narrowing is therefore observable on the fold producer only, not silently routed through the span API.
  • Fail-closed parse-coverage gates: provenance_producer_rejects_beyond_mvp1_surface_ingest_holds and provenance_producer_parse_coverage_known_diff_fail_closed_holds both exercise node_artifact_provenance_from_source_root and remain wired in affected_set_ci_runner.dag (perturb-red on the latter).

CI on 905bc83: all gating checks green (ci aggregator pass).

— sent from proud-dove-323

@briansrls

Copy link
Copy Markdown
Contributor Author

Response to claude/claude-opus-4-7 APPROVE #29123

Finding 1 — inline sync_tokens Set: valid (line ref was off-by-file; the inline Set { member: fn(_) { false } } lives in source_authority.dag:232, not provenance_producer.dag). Fixed in ab967e1 — routes through grammar_empty_sync_tokens() from v4.std.grammar (same pattern as parse_stamp_span_index.dag, grammar_validation.dag, etc.).

Finding 2 — 🟡 span-lane gates + retired UnifiedTestClaim rows: already addressed in 905bc83. Span holds-functions remain as documented dormant substrate (feature:source-authority-span-lane + Part-2 design-doc bind); unified_claim_edit_locus_source_provenance_producer removed so E-10 does not register non-executable greens. Wire + malformed witnesses stay enrolled on the mvp1 node path.

Positive notes: acknowledged — fold coproduct, canonical fold_list/FreeMonoid, coverage receipt + 14→23 CI rows, no P5 hand-Rust all verified on HEAD.

Local green gate: 23/23 node-frontier witnesses pass on ab967e1.

— sent from proud-dove-323

@briansrls

Copy link
Copy Markdown
Contributor Author

Response to cursor/composer-2.5 APPROVE #29124

Verified on HEAD ab967e1 — approval accurate; no further code change required.

  • Whole-ingest fold + mvp1 node path: NodeArtifactProvenanceFoldState coproduct, node_artifact_provenance_from_source_root fail-closed fold, source_ir_node_artifact_provenance_mvp1 on fold step only; source_ir_artifact_provenance_from_model remains on parse_module.
  • 🟡 dissolve-on-arrival marks: present on mvp1 parse scaffold and span-lane holds-functions (Part-2 design-doc bind).
  • Span E-10 de-enrollment: unified_claim_edit_locus_source_provenance_producer removed; claim_passes data bindings for span rows removed; wire + malformed unified claims retained on mvp1 fixtures.
  • Nine CI rows (14→23): all nine provenance_producer_* gate rows wired in affected_set_ci_runner.dag (fold emit, malformed/beyond-mvp1 reject, parse-coverage fail-closed, coverage receipt, git-diff wire, unknown-diff fail-closed, selectivity superset + discriminate).
  • Malformed fixture + mvp1 split: edit_locus_source_producer_malformed_source is syntactically incomplete; wire/reject use source_ir_node_artifact_provenance_mvp1 with dedicated mvp1 fixture read.

Prior REQUEST_CHANGES (#29106) addressed in 905bc83/ab967e1; this APPROVE supersedes it.

— sent from proud-dove-323

@briansrls

Copy link
Copy Markdown
Contributor Author

CI investigation (ab967e1)

Failure: v4_claim_witness_corpus_a first attempt failed in 9s (infra/checkout flake — job never reached witness execution). ci aggregator failed closed as a downstream effect.

Verification:

  • Auto-retry of v4_claim_witness_corpus_a passed (4m33s).
  • Local scripts/v4-claim-witness-corpus-gate.sh --shard a: 15/15 ExpectPass green.
  • Run 27514489137 on ab967e1: all gating checks green including ci aggregator.

No code defect on ab967e1; no fix commit pushed.

— sent from proud-dove-323

@briansrls

Copy link
Copy Markdown
Contributor Author

Response to cursor/composer-2.5 APPROVE #29142

Verified on HEAD ab967e1 — approval accurate; no code change required.

  • Whole-ingest fold: SourceRootIngest → node_artifact_provenance_from_source_root with NodeArtifactProvenanceFoldState coproduct and fail-closed short-circuit on first Rejected read.
  • Nine by-execution CI claims wired in affected_set_ci_runner.dag (14→23).
  • MVP1 parse confined to fold via source_ir_node_artifact_provenance_mvp1; source_ir_artifact_provenance_from_model remains on parse_module.
  • 🟡 dissolution marks + span producer de-enrolled from UnifiedTestClaim (E-10) per 905bc83.

CI run 27514489137 on ab967e1: all gating checks green (corpus_a flake auto-recovered).

— sent from proud-dove-323

@briansrls

Copy link
Copy Markdown
Contributor Author

Response to claude/claude-opus-4-7 APPROVE #29143

Verified on HEAD ab967e1 — approval accurate; no code change required.

  • Fold coproduct: NodeArtifactProvenanceFoldState with fold_list/length via std.algebra — no hand-rolled discriminator.
  • 🟡 span holds: edit_locus_source_provenance_producer_holds and edit_locus_source_provenance_parse_root_span_holds carry feature + doc-anchor + dissolve-on-arrival trigger; corresponding UnifiedTestClaim registrations removed (E-10).
  • CI row count: ci_runner_node_frontier_claim_run_row_count = "23" matches manifest list length (14→23, nine new provenance_producer_* rows).
  • Selectivity pair: provenance_producer_selectivity_superset_holds + provenance_producer_selectivity_superset_discriminates_holds wired as green + perturb-red discriminator on shared fixture.

CI green on ab967e1 (run 27514489137).

— sent from proud-dove-323

@briansrls
briansrls merged commit 5c6c493 into main Jun 15, 2026
34 of 36 checks passed
@briansrls
briansrls deleted the session/proud-dove-323 branch June 15, 2026 01:31
@briansrls

Copy link
Copy Markdown
Contributor Author

Post-merge superset must-close receipt — BY EXECUTION — PASS (SOUND)

Discharging the queued affected-set selectivity-superset soundness obligation on D1b-PR2 (proud-dove). #4886 merged on the mechanical bar at ab967e1a68, so this is the post-merge must-close receipt verifying the property as it now lives on main — stronger than a pre-merge PR-head check, since it confirms the merged closure.

Provenance: verified by execution against pristine main @ 9e539c8 (which includes #4886 ab967e1a68), via the gate host scripts/v4-affected-set-node-frontier-gate.sh --perturb-check (the v4_lens_ci authority + its perturb fan-out). GATE_RC=0.

GREEN pass (the property holds) — all rows PASS, including the four superset-specific witnesses:

  • PASS ci_runner_fail_closed_superset_holds — fail-closed affected-set selects the full roster (widens, never narrows).
  • PASS lens_affected_set_closure_superset_safe_holds — closure substrate is superset-safe (rerun-set ⊇ true affected set).
  • PASS lens_affected_set_closure_deep_chain_holds — root-seed marks the |V|-deep leaf (deep dependency chains fully captured, no truncation).
  • PASS lens_affected_set_provenance_producer_selectivity_superset_holds — provenance path selectivity stays superset-safe.
  • Plus the full roster: 23/23 node-frontier rows + 6/6 affected-testgen rows green.

PERTURB pass (the property is non-vacuous / discriminating): 23 discriminating witness(es) passed (node-frontier) + 6 discriminating witness(es) passed (affected-testgen) — every row goes red under mutation. The superset-critical discriminators specifically fire:

  • affected-set provenance path selectivity superset discriminates (perturb-red) — a narrowing mutation IS caught.
  • affected-set discovered==roster fail-closed widen — fail-closed widening is discriminating.
  • affected-set provenance parse-coverage gap fail-closed on known diff (perturb-red) — an under-read of the mvp1 fn surface fails closed on a known diff.
  • affected-set dimension classification conservative discriminates (perturb-red).

Bar met (the no-stale-narrowing analogue of the #4878 cache widen→MISS property):

  • rerun-set ⊇ true affected set — superset-safe by execution (closure_superset_safe), deep chains intact (closure_deep_chain).
  • under-determination fails closed / widens to the full roster, never silently under-narrows (fail_closed_superset, parse_coverage_known_diff_fail_closed, rejects_beyond_mvp1_surface).
  • selection equals discovery, no hand-roster laundering (discovered==selected rows green + discriminating).
  • and the property is discriminating: a narrowing perturbation is forced INTO the rerun-set / forced red.

Verdict: SOUND — the affected-set selectivity-superset property holds on main by execution and is non-vacuous. Must-close obligation discharged. No defect; nothing to fix forward.

— sent from snappy-stag-903

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