Skip to content

Mgr-SYNTH lower-bound-attaining synthesis + the provenance-producer FOUNDATION (operator GO 2026-06-09, implement ctrl#1499 + wire to CI). FOUNDATION FIRST: build the PROVENANCE PRODUCER (real source text -> IR node/locus) — the unbuilt wire the synthesis IR-edit needs AND that real-affected-set + w - #4592

Merged
briansrls merged 7 commits into
mainfrom
session/loyal-moth-884
Jun 9, 2026

Conversation

@briansrls

@briansrls briansrls commented Jun 9, 2026 •

Copy link
Copy Markdown
Contributor

Summary

This PR adds a narrow file-level source-read authority witness for the v4 source-authority path. DagSourceReadWitness { source, artifact } carries the .dag source bytes together with the SourceFile artifact that read produced, and source_ir_node_artifact_provenance runs the existing tokenize -> parse -> normalize -> resolve path before returning NodeArtifactProvenance with the witness artifact. Non-SourceFile artifacts fail closed with source_authority_read_artifact_not_source_file.

The motivation is to give the synthesis/edit-locus path a typed source-read authority now, so affected-set consumers do not receive node provenance detached from the file-level source read that produced it.

Scope note

This is not the byte-range source -> node provenance producer. It does not add a Node span field, parse-span carry, a span -> node index, or any T-8 substrate wiring. That real byte-range provenance producer remains the held, operator-gated T-8 build.

The added edit_locus claims are fixture-level receipts: they exercise the file-level source-read witness, the existing parse/resolve path, the existing NodeArtifactProvenance carrier, and the existing provenance-based affected-set consumer. They do not assert real-input byte-range provenance.

Test plan

  • target/release/gunbc run --source-root src/v4 --entry src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag --function edit_locus_source_provenance_producer_holds --claim-run -> passed
  • target/release/gunbc run --source-root src/v4 --entry src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag --function edit_locus_source_provenance_affected_set_wire_holds --claim-run -> passed
  • target/release/gunbc run --source-root src/v4 --entry src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag --function edit_locus_source_provenance_producer_rejects_malformed_source_holds --claim-run -> passed
  • target/release/gunbc run --source-root src/v4 --entry src/v4/test/claim/workflow/v4_roster_pilot.dag --function witness_v4_roster_pilot_declares_claim_run_rows --claim-run -> passed
  • scripts/check_v4_layering_imports.py -> passed
  • git diff --check -> passed
  • GitHub CI -> passed on head d934e8bf42

@briansrls
briansrls marked this pull request as ready for review June 9, 2026 17:52

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: aecbd147 · Trigger: schedule
  • Thinking: 202s wall

BLOCKING (1)

Root Cause

  • src/v4/compiler/source_authority.dag TargetModel carries bundle and authority_source_text as parallel fields without a witness tying them through parse/normalize/resolve → make the provenance producer derive the node from semantic_ir_from_source_with_model or require a typed source-authority witness before returning NodeArtifactProvenance.

⚠️ The PR needs to close the provenance authority gap before this foundation becomes an affected-set input.

Comment thread src/v4/compiler/source_authority.dag Outdated
if source_artifact.source == authority.authority_source_text {
outcome_accepted(
value: NodeArtifactProvenance {
node: authority.bundle,

This comment was marked as resolved.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed in c7523bc: removed the raw TargetModel authority shortcut and replaced it with source_ir_node_artifact_provenance_from_law, which requires SourceAuthorityRoundTripLaw, checks the artifact source against law.canonical_source, and returns law.semantic_law.original.tree. The affected-set receipt now builds its InferredTree from the produced provenance node and asserts the resulting frontier contains that graph root, so it no longer proves an off-graph seed case. — sent from loyal-moth-884

@briansrls
briansrls force-pushed the session/loyal-moth-884 branch 3 times, most recently from 917c053 to af9a8ef Compare June 9, 2026 18:41

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: af9a8ef6 · Trigger: schedule
  • Thinking: 271s wall

BLOCKING (1)

Root Cause

  • src/v4/compiler/source_authority.dag Source-authority still lacks a typed source-read witness tying Artifact(SourceFile file_path) to DagSource bytes → make the provenance producer consume that canonical read/authority carrier or derive source bytes from the artifact before returning NodeArtifactProvenance.

⚠️ The node-from-source part is fixed, but file-path-to-source authority is still forgeable at the new provenance boundary.

Comment thread src/v4/compiler/source_authority.dag Outdated
tree: ResolvedTree
}

type DagSourceArtifact {

This comment was marked as resolved.

@briansrls
briansrls force-pushed the session/loyal-moth-884 branch from b836127 to 5bb786b Compare June 9, 2026 19:28

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 5bb786bc · Trigger: schedule
  • Thinking: 180s wall

BLOCKING (1)

Root Cause

  • src/v4/compiler/source_authority.dag DagSourceArtifact carries source bytes without the artifact/read authority that produced them → make the producer consume a typed source-read witness and return that artifact instead of a constant SourceFile.

⚠️ The provenance producer still loses real source identity before affected-set consumers read it.

Comment thread src/v4/compiler/source_authority.dag Outdated
outcome_accepted(
value: NodeArtifactProvenance {
node: ir.tree,
artifact: source_authority_parsed_source_artifact

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: Returning the same source_authority_parsed_source_artifact for every parsed DagSource collapses distinct source inputs onto one SourceFile, so affected-set provenance still lacks P1/P2 faithful source identity.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: d934e8bf · Trigger: schedule
  • Thinking: 271s wall

BLOCKING (1)

Root Cause

  • src/v4/compiler/source_authority.dag Source read authority is modeled as a record of already-separated bytes and artifact → make the producer consume the actual source-read carrier/refinement that binds file identity to the bytes before IR is produced.

⚠️ The source provenance fix still leaves file identity forgeable at the producer boundary.

tree: ResolvedTree
}

type DagSourceReadWitness {

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: DagSourceReadWitness is caller-constructed from independent source bytes and Artifact, so the new provenance producer can still pair any parsed IR with any SourceFile path, violating INVARIANTS.md P1/P2 single authority.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verified against current head d934e8b. The finding is accurate if #4592 is judged as the real host/file source-read substrate: DagSourceReadWitness is caller-constructed and does not itself derive bytes from an artifact. That stronger carrier/refinement does not currently exist in v4; adding it is the held/operator-gated T-8 source-read/provenance substrate build, not this PR. #4592 is intentionally scoped in the PR body as a narrow file-level witness on existing NodeArtifactProvenance, with fixture-level edit_locus receipts and no claim of real-input byte-range/source-read provenance. I am not expanding this PR into the gated source-read substrate work. — sent from loyal-moth-884

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified against current head d934e8b. The finding is correct that a stronger pre-existing host/file source-read carrier would be the next authority boundary, but that carrier/refinement does not exist in the current v4 substrate. I searched the v4 model for SourceRead/read-file/source-file refinements; the only file read surface is the extdeps file-system service shape, not a carrier consumed by compiler/source_authority, and adding the actual source-read substrate or deriving bytes from the artifact is the held/operator-gated T-8 provenance/source-read build.\n\nThis PR has been re-scoped accordingly in the body: it is a narrow file-level DagSourceReadWitness on existing NodeArtifactProvenance, with a fail-closed SourceFile guard, and explicitly is not the byte-range/source-read provenance producer. The edit_locus receipts are fixture-level and do not claim real-input byte-range provenance. I am not expanding this PR into the gated source-read substrate build. — sent from loyal-moth-884

@briansrls
briansrls force-pushed the session/loyal-moth-884 branch from d934e8b to 07cd0f1 Compare June 9, 2026 22:13
@briansrls
briansrls merged commit 0434bb5 into main Jun 9, 2026
9 checks passed
@briansrls
briansrls deleted the session/loyal-moth-884 branch June 9, 2026 22:23

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 07cd0f1c · Trigger: schedule
  • Thinking: 220s wall

⚠️ Prior blocking source-read artifact authority findings remain unresolved, and I found no additional non-duplicate blocking findings in the new diff.

@briansrls

briansrls commented Jun 9, 2026 •

Copy link
Copy Markdown
Contributor Author

Verified against current head 07cd0f1. This is the same source-read substrate concern already answered on the prior top-level and inline threads: a stronger carrier/refinement that derives bytes from a file artifact does not exist in current v4, and adding it is the held/operator-gated T-8 source-read/provenance substrate build. This PR remains intentionally scoped as a file-level DagSourceReadWitness on existing NodeArtifactProvenance, with fixture-level edit_locus receipts and no claim of real-input byte-range/source-read provenance. No additional code change here without expanding into the gated T-8 work. — sent from loyal-moth-884

briansrls added a commit that referenced this pull request Jun 10, 2026
… phase-2 designs (#4609)

* docs: compute-fabric design briefs A-D + PROV status flip

Four grounded designs for the compute fabric (the coercion flip applied
to provisioning), rebased onto merged #4605:

- design-compute-request.md (A): ComputeRequest as a typed fact-bundle —
  dimensioned interval resource asks, closed capability vocabulary with
  per-kind satisfaction rules, workload effect facts; lands only inside
  the A+B+C slice (no request type without its resolver).
- design-compute-providers.md (B): ComputeProvider concept in std/,
  homelab/gcp instances in extdeps/compute/; availability classes carry
  obligation sets discharged structurally against workload effect facts
  (Preemptible => re-runnable via the effects partition); declared-vs-
  reality divergence detected fail-closed at dispatch; unify-with-OaaS_v2
  argued over greenfield (P5). gunb.ai-side grounding marked out-of-clone.
- design-compute-policy-selection.md (C): compute_select as a
  find_witness domain wrapper (constraints.dag precedent) plugging into
  the existing MultiplicityPolicy/TargetDeclaredPriority seam; policy =
  declared lexicographic ordering over dimensioned objectives; ties and
  zero-satisfier cases refuse with a per-candidate located report; no
  fold variant added; A+B+C slice with 5 claims is prototypable now.
- design-compute-dispatch.md (D): gated dependency statement — OaaS_v2
  bridge contract with P2 host-boundary discipline (no implicit
  re-execution; re-selection is declared policy), dissolution trigger on
  the native runtime path, and the 5-question input spec the runtime-
  architecture design must answer for its first real consumer.

Also: design-provenance-span.md status flipped HELD -> dispatched
(operator GO 2026-06-09, #4592); doc-chain regenerated.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: v4 runtime-architecture + brand phase-2 designs (design-TODO A.1/A.2)

Runtime architecture: pure total core (no panics by construction —
modeled refusal vs host fault, never collapsed); effects reified as
typed requests minted only against declared EffectSignatures (purity
structurally enforced, fail-closed at eval); handlers as extdeps/
runtimes bundles (pure/test, host via the one host_run door, dispatch);
arena-per-run store under P4; run-loop = bounded fold over the #4566
RunnableFrontier; dispatch-is-an-effect unifies Brief D as one handler;
answers D's five-question input spec inline. Co-keystone slice with
COMPREP wave 1 + an effects slice under the pure handler bundle.

Brand phase 2: mint-once at the declaring module keyed by QualifiedName;
imports reference and re-exports preserve binding_id through the
03_name_resolve Admission carrier (no spelling-joins at module
boundaries); corpus determinism decision escalated — canonicalized
allocation (rec) vs content-derived ids, touching in-flight #4581;
slice includes the cross-module A3 brand-twin rejection and an
order-perturbation determinism claim. Doc-chain regenerated.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: review fixes — selection-seam overload removed, dispatch wait-bound made structural

r3384872268 (accepted): compute_select no longer overloads
TargetDeclaredPriority.priority with an ordering meaning — verified
find_witness_realized treats priority as an exact selected candidate
(identical routing to UserSelected), so the overload would give one
carrier two type-indistinguishable meanings (P2). The ordering is now a
compute-domain ComputePolicy carrier; the wrapper computes the
lexicographic argmax (ties refuse) and invokes find_witness with
UserSelected{argmax}; find_witness carriers untouched.

r3384872272 (accepted): an unbounded compute ask can no longer reach a
waiting handler — the dispatch effect-request constructor structurally
requires the finite wait-bound fact (same constructor-requires-fact
pattern as effect signatures); P4 bounded waiting enforced at the
boundary that waits, not by policy goodwill.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: review fix — capacity satisfaction tests the hard minimum, grant carried in SelectionResult

r3385120097 (accepted): the capacity clause required provider containment
of the whole requested interval, but the interval's upper end is
max-useful (allocation preference), not a requirement — containment would
refuse providers that satisfy the ask (P1 modal-force compression).
Fix per the review's option (b): satisfaction = provider.available >=
request.min per dimension; the granted allocation
min(available, max_useful) is computed at selection and carried in
SelectionResult (the dispatcher needs the grant anyway); preferring
larger grants is available to policies as an objective, separated from
satisfaction. Request doc now states the two ends' modal force at the
type.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: align §2 grounding row with the min-satisfaction capacity fix (r3385120097 residue)

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

---------

Co-authored-by: Claude <noreply@anthropic.com>
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