Skip to content

Implement output provenance inference for non-recursive functions #405

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 1 commit into from
Apr 12, 2026
Merged

Implement output provenance inference for non-recursive functions #405

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
100 changes: 89 additions & 11 deletions src/v2/04_infer.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3852,13 +3852,15 @@ fn classify_body_provenance(expr: Node, param_names: List<String>, param_types:
match expr.expr_data {
ExprVar { binding_kind: _ } =>
let vname = expr_var_name_at(texpr: expr, source_indices: type_env.source_indices)
if param_names |> any(pn => pn == vname) {
map_insert(empty_map(), vname, PreservedValue)
} else {
match map_get(let_prov, vname) {
Some { value: prov } => prov
None => empty_map()
}
// Check let_prov first: locals shadow params (Track 3 limitation).
match map_get(let_prov, vname) {
Some { value: prov } => prov
None =>
if param_names |> any(pn => pn == vname) {
map_insert(empty_map(), vname, PreservedValue)
} else {
empty_map()
}
}

ExprFieldAccess { summary: _ } =>
Expand Down Expand Up @@ -3895,9 +3897,51 @@ fn classify_body_provenance(expr: Node, param_names: List<String>, param_types:
compose_callee_provenance(callee: mname, arg_by_name: method_call_args_by_name(call: expr, func_sigs: func_sigs, source_indices: type_env.source_indices), param_names: param_names, param_types: param_types, type_env: type_env, func_sigs: func_sigs, let_prov: let_prov)

ExprMatch =>
let scrut = match_scrutinee(texpr: expr)
let scrut_prov = classify_body_provenance(expr: scrut, param_names: param_names, param_types: param_types, type_env: type_env, func_sigs: func_sigs, let_prov: let_prov)
let arms = match_arm_nodes(texpr: expr)
let arm_provs = arms |> map(arm =>
classify_body_provenance(expr: arm_body(n: arm), param_names: param_names, param_types: param_types, type_env: type_env, func_sigs: func_sigs, let_prov: let_prov)
// Extend let_prov with arm bindings composed through inductive fields.
// Uses field_binding_pattern (Bind { name }) for the introduced binding name,
// field_binding_name_at for the field label in inductive field lookup.
// Includes variant_name in the filter. Fails closed on unmatched fields.
let arm_let_prov = match arm_pattern(n: arm) {

@briansrls briansrls Apr 12, 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.

Invariant violation: ExprMatch rebuilds arm scope into let_prov by binder names instead of consuming the authoritative pattern-scope machinery, violating Boundary sufficiency and No parallel implementations.

VariantPattern { name: vname, parent_enum: _, field_bindings: bindings } =>

This comment was marked as resolved.

Sign in to view

fold(bindings, init: let_prov, f: (acc, binding) =>
let field_label = field_binding_name_at(n: binding, source_indices: type_env.source_indices)
let bind_name = match field_binding_pattern(n: binding) {
Bind { name: bn } => bn
_ => ""
}
if bind_name != "" && field_label != "" {
let field_prov = fold(map_keys(scrut_prov), init: empty_prov_map(), f: (fp_acc, pname) =>
match map_get(scrut_prov, pname) {
Some { value: scrut_rel } =>
let lookup_type = match scrut_rel {
PreservedValue => match map_get(param_types, pname) { Some { value: t } => t None => "" }
StrictSubValue { field: f, factor: _ } => f.element_type
IteratedSubValue { field: f } => f.element_type
_ => ""
}
if lookup_type != "" {

This comment was marked as resolved.

Sign in to view

let ind_fields = inductive_fields_for(env: type_env, type_name: lookup_type)
let matching = ind_fields |> filter(f => f.field_name == field_label && (f.variant_name == vname || f.variant_name == "")) |> first
match matching {
Some { value: ind_field } => map_insert(fp_acc, pname, compose_sub_value(base: scrut_rel, field: ind_field))
None => fp_acc
}
} else { fp_acc }
None => fp_acc
}
)
map_insert(acc, bind_name, field_prov)
} else { acc }
)
Bind { name: bname } =>
map_insert(let_prov, bname, scrut_prov)
_ => let_prov
}
classify_body_provenance(expr: arm_body(n: arm), param_names: param_names, param_types: param_types, type_env: type_env, func_sigs: func_sigs, let_prov: arm_let_prov)
)
meet_body_provenance_maps(provs: arm_provs)

Expand All @@ -3922,16 +3966,50 @@ fn classify_body_provenance(expr: Node, param_names: List<String>, param_types:
}

ExprBlock =>
match expr.children |> last {
Some { value: last_stmt } =>
classify_body_provenance(expr: last_stmt, param_names: param_names, param_types: param_types, type_env: type_env, func_sigs: func_sigs, let_prov: let_prov)
// Fold over block statements: extend let_prov for block-level let-bindings,
// return last statement's provenance. Let-with-body restores outer scope
// so the binding does not leak into subsequent statements.
let block_result = fold(expr.children, init: BlockProvFoldState { prov: let_prov, last: empty_prov_map() }, f: (state, stmt) =>

@briansrls briansrls Apr 12, 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.

Invariant violation: ExprBlock threads a second ad-hoc provenance scope through BlockProvFoldState instead of the existing inference scope, violating No duplicate representations.

match stmt.expr_data {
ExprLet =>
let bname = let_binding_name_at(texpr: stmt, source_indices: type_env.source_indices)
let value = let_value(texpr: stmt)
let value_prov = classify_body_provenance(expr: value, param_names: param_names, param_types: param_types, type_env: type_env, func_sigs: func_sigs, let_prov: state.prov)
let updated_prov = map_insert(state.prov, bname, value_prov)
match let_body(texpr: stmt) {

This comment was marked as resolved.

Sign in to view

Some { value: body } =>
// Let-with-body: binding scoped to body only; restore state.prov after.
BlockProvFoldState { prov: state.prov, last: classify_body_provenance(expr: body, param_names: param_names, param_types: param_types, type_env: type_env, func_sigs: func_sigs, let_prov: updated_prov) }
None =>
// Block-level let: binding persists for subsequent statements.
BlockProvFoldState { prov: updated_prov, last: value_prov }
}
_ =>
BlockProvFoldState { prov: state.prov, last: classify_body_provenance(expr: stmt, param_names: param_names, param_types: param_types, type_env: type_env, func_sigs: func_sigs, let_prov: state.prov) }
}
)
block_result.last

ExprCast =>

@briansrls briansrls Apr 12, 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.

Invariant violation: ExprMatch only records arm bindings when field_binding_pattern is a direct Bind, so nested destructuring binders vanish from arm_let_prov and body inference loses real sources, violating Boundary sufficiency.

classify_body_provenance(expr: cast_expr(texpr: expr), param_names: param_names, param_types: param_types, type_env: type_env, func_sigs: func_sigs, let_prov: let_prov)

ExprReturn =>
match expr.children |> first {
Some { value: inner } =>
classify_body_provenance(expr: inner, param_names: param_names, param_types: param_types, type_env: type_env, func_sigs: func_sigs, let_prov: let_prov)
None => empty_map()
}

_ => empty_map()
}
}

// Accumulator for ExprBlock fold in classify_body_provenance.
type BlockProvFoldState {
prov: Map<String, Map<String, SubValueRelation>>
last: Map<String, SubValueRelation>
}

// Build named-arg map for ExprCall: all children are named arg nodes.
fn call_args_by_name(call: Node, source_indices: Map<String, NewlineIndex>) -> Map<String, Node> {
fold(call.children, init: empty_map(), f: (acc, arg_node) =>
Expand Down
Loading
Loading