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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
briansrls merged 7 commits into from
Jun 9, 2026
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
33bad33
WIP: Mgr-SYNTH lower-bound-attaining synthesis + the provenance-produ…
Jun 9, 2026
7dd28ae
WIP: Mgr-SYNTH lower-bound-attaining synthesis + the provenance-produ…
Jun 9, 2026
aefadf8
WIP: Mgr-SYNTH lower-bound-attaining synthesis + the provenance-produ…
Jun 9, 2026
c3f67b7
WIP: Mgr-SYNTH lower-bound-attaining synthesis + the provenance-produ…
Jun 9, 2026
64eff6d
WIP: Mgr-SYNTH lower-bound-attaining synthesis + the provenance-produ…
Jun 9, 2026
87c1fd2
Tighten source provenance fixture authority
Jun 9, 2026
07cd0f1
WIP: Mgr-SYNTH lower-bound-attaining synthesis + the provenance-produ…
Jun 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 56 additions & 0 deletions src/v4/compiler/source_authority.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ import v4.extdeps.languages.dag {
DagLanguageModel,
dag_language_model_wave1_modeled
}
import v4.std.artifact { Artifact, NodeArtifactProvenance, SourceFile }
import v4.std.diagnostic {
Diagnostic,
ExternalContractUnknown,
Expand All @@ -25,6 +26,7 @@ import v4.std.diagnostic {
bind_outcome,
diagnostics_singleton,
outcome_accepted,
outcome_rejected,
port_locus
}
import v4.std.grammar { ParseTree }
Expand All @@ -50,6 +52,11 @@ type DagSemanticIr {
tree: ResolvedTree
}

type DagSourceReadWitness {

@briansrls briansrls Jun 9, 2026

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.

@briansrls briansrls Jun 9, 2026

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

source: DagSource
artifact: Artifact
}

type SourceAstEqual {
original: DagSourceAst
reparsed: DagSourceAst
Expand Down Expand Up @@ -90,6 +97,7 @@ data source_authority_ast_mismatch: Symbol = source_authority_ast_mismatch
data source_authority_ir_mismatch: Symbol = source_authority_ir_mismatch
data source_authority_normalized_ast_mismatch: Symbol = source_authority_normalized_ast_mismatch
data source_authority_serializer_nondeterministic: Symbol = source_authority_serializer_nondeterministic
data source_authority_read_artifact_not_source_file: Symbol = source_authority_read_artifact_not_source_file


fn source_authority_diagnostic(reason: Symbol) -> Diagnostic {
Expand Down Expand Up @@ -146,6 +154,54 @@ fn semantic_ir_from_ast_with_model(ast: DagSourceAst, lm: DagLanguageModel) -> O
}


fn semantic_ir_from_source_with_model(source: DagSource, lm: DagLanguageModel) -> Outcome<DagSemanticIr> {
bind_outcome(
o: parse_dag_source_ast_with_model(source: source, lm: lm),
f: fn(ast) {
semantic_ir_from_ast_with_model(ast: ast, lm: lm)
}
)
}


fn semantic_ir_from_source(source: DagSource) -> Outcome<DagSemanticIr> {
semantic_ir_from_source_with_model(source: source, lm: dag_language_model_wave1_modeled())
}


fn source_ir_node_artifact_provenance_from_model(
source_read: DagSourceReadWitness,
lm: DagLanguageModel
) -> Outcome<NodeArtifactProvenance> {
match source_read.artifact.kind {
SourceFile =>
bind_outcome(
o: semantic_ir_from_source_with_model(source: source_read.source, lm: lm),
f: fn(ir) {
outcome_accepted(
value: NodeArtifactProvenance {
node: ir.tree,
artifact: source_read.artifact
}
)
}
)
_ =>
outcome_rejected(d: source_authority_diagnostic(reason: source_authority_read_artifact_not_source_file))
}
}


fn source_ir_node_artifact_provenance(
source_read: DagSourceReadWitness
) -> Outcome<NodeArtifactProvenance> {
source_ir_node_artifact_provenance_from_model(
source_read: source_read,
lm: dag_language_model_wave1_modeled()
)
}


fn source_ast_equal_witness(
original: DagSourceAst,
reparsed: DagSourceAst
Expand Down
97 changes: 95 additions & 2 deletions src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,19 @@ import v4.lens.edit_locus {
PathRegex,
RepoPath,
affected_set_reading_from_git_diff,
affected_set_reading_from_git_diff_provenance,
resolve_edit_locus
}
import v4.compiler.source_authority {
DagSource,
DagSourceReadWitness,
source_ir_node_artifact_provenance
}
import v4.std.artifact { Artifact, SourceFile }
import v4.std.diagnostic { Accepted, Rejected }
import v4.std.logic { Bool }
import v4.std.algebra { Empty, length }
import v4.std.node { Symbol }
import v4.std.algebra { Empty, count_equal, length }
import v4.std.node { Node, Symbol }
import v4.std.text { String }
import v4.std.witness { Holds, Violates, Witness }
import v4.test.claim.lens_affected_set.node_precision {
Expand All @@ -24,10 +32,37 @@ import v4.test.claim.lens_affected_set.node_precision {
affected_set_mid_to_leaf_frontier_dependency,
affected_set_root_to_mid_frontier_dependency
}
import v4.test.claim.lens_common.infer_fixture {
claim_inferred_facts,
claim_inferred_tree
}

data edit_locus_path_src_v4_affected_set: RepoPath = "src/v4/lens/affected_set.dag"
data edit_locus_path_source_producer_fixture: RepoPath = "src/v4/test/claim/lens_affected_set/source_producer_fixture.dag"
data edit_locus_path_unknown: RepoPath = "src/v4/lens/unknown_path.dag"
data edit_locus_pattern_v4_lens: PathRegex = edit_locus_pattern_v4_lens
data edit_locus_source_producer_fixture_source: DagSource = "module edit.locus\nfn add(x:Int, y:Int) -> Int { x + y }"
data edit_locus_source_producer_malformed_source: DagSource = "fn add(x:Int, y:Int) -> Int { x + y }"

data edit_locus_source_producer_fixture_artifact: Artifact = Artifact {
kind: SourceFile,
id: ^edit_locus_source_producer_fixture_artifact,
file_path: edit_locus_path_source_producer_fixture
}

data edit_locus_source_producer_fixture_source_read: DagSourceReadWitness = DagSourceReadWitness {
source: edit_locus_source_producer_fixture_source,
artifact: edit_locus_source_producer_fixture_artifact
}

data edit_locus_source_producer_malformed_source_read: DagSourceReadWitness = DagSourceReadWitness {
source: edit_locus_source_producer_malformed_source,
artifact: edit_locus_source_producer_fixture_artifact
}

data edit_locus_source_producer_git_diff: GitDiffNameOnly = GitDiffNameOnly {
changed_paths: [edit_locus_path_source_producer_fixture]
}

fn edit_locus_fixture_path_regex_matches(changed: RepoPath, pattern: PathRegex) -> Bool {
match pattern {
Expand Down Expand Up @@ -102,7 +137,65 @@ fn edit_locus_affected_set_wire_fail_closed_holds() -> Bool {
}
}

fn edit_locus_source_provenance_producer_holds() -> Bool {
match source_ir_node_artifact_provenance(
source_read: edit_locus_source_producer_fixture_source_read
) {
Accepted { value: provenance, diagnostics: _ } =>
provenance.artifact.file_path == edit_locus_path_source_producer_fixture
Rejected { diagnostics: _ } => false
}
}

fn edit_locus_source_provenance_node_eq(left: Node, right: Node) -> Bool {
left == right
}

fn edit_locus_source_provenance_affected_set_wire_holds() -> Bool {
match source_ir_node_artifact_provenance(
source_read: edit_locus_source_producer_fixture_source_read
) {
Accepted { value: provenance, diagnostics: _ } =>
let producer_graph = claim_inferred_tree(
root: provenance.node,
facts: claim_inferred_facts(
type_symbol: ^edit_locus_source_producer_type_symbol,
algebra_symbol: ^edit_locus_source_producer_algebra_symbol,
descent_symbol: ^edit_locus_source_producer_descent_symbol,
)
)
match affected_set_reading_from_git_diff_provenance(
graph: producer_graph,
git_diff: edit_locus_source_producer_git_diff,
provenance: [provenance]
) {
Holds { value: reading } =>
(producer_graph.root == provenance.node)
&& (reading.edit_locus == producer_graph.root)
&& (count_equal(
xs: reading.affected,
item: producer_graph.root,
eq: edit_locus_source_provenance_node_eq
) == 1)
Violates { diagnostic: _ } => false
}
Rejected { diagnostics: _ } => false
}
}

fn edit_locus_source_provenance_producer_rejects_malformed_source_holds() -> Bool {
match source_ir_node_artifact_provenance(
source_read: edit_locus_source_producer_malformed_source_read
) {
Accepted { value: _, diagnostics: _ } => false
Rejected { diagnostics: _ } => true
}
}

data edit_locus_narrow_resolution_claim_passes: Bool = edit_locus_narrow_resolution_holds()
data edit_locus_fail_closed_claim_passes: Bool = edit_locus_fail_closed_holds()
data edit_locus_affected_set_wire_claim_passes: Bool = edit_locus_affected_set_wire_holds()
data edit_locus_affected_set_wire_fail_closed_claim_passes: Bool = edit_locus_affected_set_wire_fail_closed_holds()
data edit_locus_source_provenance_producer_claim_passes: Bool = edit_locus_source_provenance_producer_holds()
data edit_locus_source_provenance_affected_set_wire_claim_passes: Bool = edit_locus_source_provenance_affected_set_wire_holds()
data edit_locus_source_provenance_producer_rejects_malformed_source_claim_passes: Bool = edit_locus_source_provenance_producer_rejects_malformed_source_holds()
56 changes: 52 additions & 4 deletions src/v4/test/claim/workflow/v4_roster_pilot.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,9 @@ data coordination_obligation_settlement_arm_sharp_holds: Symbol = coordination_o
data discriminant_intrinsic_is_payload_blind_and_arm_sharp: Symbol = discriminant_intrinsic_is_payload_blind_and_arm_sharp
data edit_locus_fail_closed_holds: Symbol = edit_locus_fail_closed_holds
data edit_locus_narrow_resolution_holds: Symbol = edit_locus_narrow_resolution_holds
data edit_locus_source_provenance_affected_set_wire_holds: Symbol = edit_locus_source_provenance_affected_set_wire_holds
data edit_locus_source_provenance_producer_holds: Symbol = edit_locus_source_provenance_producer_holds
data edit_locus_source_provenance_producer_rejects_malformed_source_holds: Symbol = edit_locus_source_provenance_producer_rejects_malformed_source_holds
data extdeps_react_composite_element_declares_key_and_ref_holds: Symbol = extdeps_react_composite_element_declares_key_and_ref_holds
data extdeps_react_create_element_child_element_arm_wraps_react_element_holds: Symbol = extdeps_react_create_element_child_element_arm_wraps_react_element_holds
data extdeps_react_effect_hooks_require_setup_ref_holds: Symbol = extdeps_react_effect_hooks_require_setup_ref_holds
Expand Down Expand Up @@ -94,7 +97,10 @@ fn v4_roster_pilot_witness_function_spellings() -> Map<Symbol, String> {
let m0 = empty_map()
let m1 = map_insert(m0, edit_locus_narrow_resolution_holds, "edit_locus_narrow_resolution_holds")
let m2 = map_insert(m1, edit_locus_fail_closed_holds, "edit_locus_fail_closed_holds")
let m3 = map_insert(m2, witness_lens_testgen_scheduled_generators_carry_provenance_green, "witness_lens_testgen_scheduled_generators_carry_provenance_green")
let m2a = map_insert(m2, edit_locus_source_provenance_producer_holds, "edit_locus_source_provenance_producer_holds")
let m2b = map_insert(m2a, edit_locus_source_provenance_affected_set_wire_holds, "edit_locus_source_provenance_affected_set_wire_holds")
let m2c = map_insert(m2b, edit_locus_source_provenance_producer_rejects_malformed_source_holds, "edit_locus_source_provenance_producer_rejects_malformed_source_holds")
let m3 = map_insert(m2c, witness_lens_testgen_scheduled_generators_carry_provenance_green, "witness_lens_testgen_scheduled_generators_carry_provenance_green")
let m4 = map_insert(m3, witness_lens_testgen_shadow_ci_run_receipt_green, "witness_lens_testgen_shadow_ci_run_receipt_green")
let m5 = map_insert(m4, witness_lens_testgen_schedules_dag_input_surface_green, "witness_lens_testgen_schedules_dag_input_surface_green")
let m6 = map_insert(m5, witness_lens_testgen_bootstrap_generator_reifies_dag_input_surface_green, "witness_lens_testgen_bootstrap_generator_reifies_dag_input_surface_green")
Expand Down Expand Up @@ -211,6 +217,27 @@ data v4_roster_pilot_row_edit_locus_fail_closed: V4RosterPilotClaimRunRow = V4Ro
function_symbol: edit_locus_fail_closed_holds
}

data v4_roster_pilot_row_edit_locus_source_provenance_producer: V4RosterPilotClaimRunRow = V4RosterPilotClaimRunRow {
label: "edit-locus source provenance producer",
entry: "src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag",
function: "edit_locus_source_provenance_producer_holds",
function_symbol: edit_locus_source_provenance_producer_holds
}

data v4_roster_pilot_row_edit_locus_source_provenance_wire: V4RosterPilotClaimRunRow = V4RosterPilotClaimRunRow {
label: "edit-locus source provenance affected-set wire",
entry: "src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag",
function: "edit_locus_source_provenance_affected_set_wire_holds",
function_symbol: edit_locus_source_provenance_affected_set_wire_holds
}

data v4_roster_pilot_row_edit_locus_source_provenance_rejects_malformed: V4RosterPilotClaimRunRow = V4RosterPilotClaimRunRow {
label: "edit-locus source provenance rejects malformed source",
entry: "src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag",
function: "edit_locus_source_provenance_producer_rejects_malformed_source_holds",
function_symbol: edit_locus_source_provenance_producer_rejects_malformed_source_holds
}

data v4_roster_pilot_row_generator_provenance: V4RosterPilotClaimRunRow = V4RosterPilotClaimRunRow {
label: "generator provenance",
entry: "src/v4/test/claim/lens_testgen/generator_provenance.dag",
Expand Down Expand Up @@ -760,6 +787,9 @@ data v4_roster_pilot_row_scheduler_runnable_frontier: V4RosterPilotClaimRunRow =
data v4_roster_pilot_claim_run_rows: List<V4RosterPilotClaimRunRow> = [
v4_roster_pilot_row_edit_locus_narrow,
v4_roster_pilot_row_edit_locus_fail_closed,
v4_roster_pilot_row_edit_locus_source_provenance_producer,
v4_roster_pilot_row_edit_locus_source_provenance_wire,
v4_roster_pilot_row_edit_locus_source_provenance_rejects_malformed,
v4_roster_pilot_row_generator_provenance,
v4_roster_pilot_row_lens_testgen_shadow_ci,
v4_roster_pilot_row_lens_testgen_dag_input_scheduled,
Expand Down Expand Up @@ -846,7 +876,7 @@ fn v4_roster_pilot_claim_run_row_transport_symbol_consistency_holds() -> Bool {


// Host transport projection: shell reads this count and list member names only (not free awk scan).
data v4_roster_pilot_claim_run_row_count: String = "73"
data v4_roster_pilot_claim_run_row_count: String = "76"


fn v4_roster_pilot_row_matches(
Expand All @@ -872,6 +902,9 @@ fn v4_roster_pilot_claim_run_list_contains_once(
fn v4_roster_pilot_claim_run_list_composition_holds() -> Bool {
v4_roster_pilot_claim_run_list_contains_once(row: v4_roster_pilot_row_edit_locus_narrow)
&& v4_roster_pilot_claim_run_list_contains_once(row: v4_roster_pilot_row_edit_locus_fail_closed)
&& v4_roster_pilot_claim_run_list_contains_once(row: v4_roster_pilot_row_edit_locus_source_provenance_producer)
&& v4_roster_pilot_claim_run_list_contains_once(row: v4_roster_pilot_row_edit_locus_source_provenance_wire)
&& v4_roster_pilot_claim_run_list_contains_once(row: v4_roster_pilot_row_edit_locus_source_provenance_rejects_malformed)
&& v4_roster_pilot_claim_run_list_contains_once(row: v4_roster_pilot_row_generator_provenance)
&& v4_roster_pilot_claim_run_list_contains_once(row: v4_roster_pilot_row_lens_testgen_shadow_ci)
&& v4_roster_pilot_claim_run_list_contains_once(row: v4_roster_pilot_row_lens_testgen_dag_input_scheduled)
Expand Down Expand Up @@ -947,8 +980,8 @@ fn v4_roster_pilot_claim_run_list_composition_holds() -> Bool {


fn witness_v4_roster_pilot_declares_claim_run_rows() -> Bool {
(length(xs: v4_roster_pilot_claim_run_rows) == 73)
&& (v4_roster_pilot_claim_run_row_count == "73")
(length(xs: v4_roster_pilot_claim_run_rows) == 76)
&& (v4_roster_pilot_claim_run_row_count == "76")
&& v4_roster_pilot_claim_run_row_transport_symbol_consistency_holds()
&& v4_roster_pilot_claim_run_list_composition_holds()
&& v4_roster_pilot_row_matches(
Expand All @@ -961,6 +994,21 @@ fn witness_v4_roster_pilot_declares_claim_run_rows() -> Bool {
entry: "src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag",
function: "edit_locus_fail_closed_holds"
)
&& v4_roster_pilot_row_matches(
row: v4_roster_pilot_row_edit_locus_source_provenance_producer,
entry: "src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag",
function: "edit_locus_source_provenance_producer_holds"
)
&& v4_roster_pilot_row_matches(
row: v4_roster_pilot_row_edit_locus_source_provenance_wire,
entry: "src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag",
function: "edit_locus_source_provenance_affected_set_wire_holds"
)
&& v4_roster_pilot_row_matches(
row: v4_roster_pilot_row_edit_locus_source_provenance_rejects_malformed,
entry: "src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag",
function: "edit_locus_source_provenance_producer_rejects_malformed_source_holds"
)
&& v4_roster_pilot_row_matches(
row: v4_roster_pilot_row_generator_provenance,
entry: "src/v4/test/claim/lens_testgen/generator_provenance.dag",
Expand Down
Loading