Repository navigation
Implement output provenance inference for non-recursive functions - #405
Conversation
ChatGPT ReviewGrounded in the thesis, this PR is pushing on the right bottleneck: output provenance on function signatures is the stated M1 blocker, and the end-state architecture is to compute these facts in inference and carry them through the IR rather than reconstruct them later. So the direction is right. I would still request changes before merge, because the new path can currently attach the wrong cause to a value, which is below the repo’s “if it compiles, the intent is sound” bar. chatgpt-review-7f6f605a-0b86-44… chatgpt-review-201af2a9-c029-46… The biggest problem is name-based provenance collapsing. In both chatgpt-review-201af2a9-c029-46… Second, positional call composition is wrong in chatgpt-review-201af2a9-c029-46… Third, chatgpt-review-7f6f605a-0b86-44… Fourth, match destructuring is still lossy. In the There is also a non-blocking but important compositional concern in chatgpt-review-a1219665-489d-48… The testing delta is too thin for the amount of semantics being added. The only test change in the PR is the diagnostic ratchet moving from 424 to 421 with a comment attributing the drop to non-recursive output provenance inference. That matches the roadmap direction, but it will not catch the specific regressions above. I’d want direct behavioral tests for shadowing, two positional arguments, branch merges with one constant branch, and match destructuring through named field bindings. A ratchet is a good outer signal; it is not a substitute for localized correctness tests. chatgpt-review-201af2a9-c029-46… chatgpt-review-69aefb79-6853-41… Roadmap alignment is otherwise good. My recommendation: request changes. The architecture choice is correct, but the current implementation still loses or misattributes provenance in several concrete cases, and that is exactly the kind of causal slippage this project is trying to remove. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0cb3f4e722
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| let arg_expr_opt = match v2_rt::map_get(&arg_by_name, callee_pname.clone()) { | ||
| Some(ae) => Some(ae.clone()), | ||
| None => positional_args.clone().first().cloned(), |
There was a problem hiding this comment.
In compose_call_body_provenance, unnamed arguments are resolved with positional_args.first() for every callee parameter, so a call like f(a, b) will compute provenance for both parameters from a. This misattributes output provenance whenever a callee has multiple positional arguments and can propagate incorrect caller/callee composition into descent analysis.
Useful? React with 👍 / 👎.
|
|
||
| pub fn merge_provenance_branches(maps: Rc<Vec<Rc<HashMap<String, Rc<SubValueRelation>>>>>) -> Rc<HashMap<String, Rc<SubValueRelation>>> { | ||
| { | ||
| let non_empty = Rc::new({ let mut __result = Vec::new(); for m in maps.iter().cloned() { if ((Rc::new(v2_rt::map_keys(&m)).len() as i64) > 0) { __result.push(m); } } __result }); |
There was a problem hiding this comment.
merge_provenance_branches filters out empty maps before intersecting branches, but empty maps are also the fallback for unhandled expressions. This means if/match expressions with one analyzable branch and one unanalyzable branch can still produce non-empty provenance (for example, if c { x } else { 0 }), which is unsound because the output is not guaranteed to derive from x on all paths.
Useful? React with 👍 / 👎.
| param_set: c.param_set.clone(), | ||
| binding_provs: v2_rt::rc_map_insert(c.binding_provs.clone(), bname.clone(), scrut_provs.clone()), | ||
| type_env: c.type_env.clone(), |
There was a problem hiding this comment.
When building arm_ctx for MatchPattern::VariantPattern, each bound field name is inserted with scrut_provs directly, so field bindings are treated as if they preserve the whole scrutinee. Returning a bound field (e.g. tail from Cons { tail }) should carry field-composed subvalue provenance; otherwise strict subvalue/shrink information is lost and helper provenance becomes less accurate.
Useful? React with 👍 / 👎.
0cb3f4e to
cff6f98
Compare
ChatGPT ReviewI reviewed the attached PR #405 diff. The direction is right. The thesis says correctness dimensions should be computed at binding sites during inference and then carried through the IR, not reconstructed later; the roadmap names output provenance on function signatures as the key M1 blocker, and explicitly calls the current body walker a temporary bootstrap authority while param identity remains string-keyed. This PR is moving in that intended direction by reusing chatgpt-review-201af2a9-c029-46… I would still request changes before merge. The first blocking issue is renamed match destructuring. The language already supports bindings like chatgpt-review-201af2a9-c029-46… chatgpt-review-7d905c07-a872-42… The second blocking issue is the new fallback for non-inductive match fields. When no inductive field matches, the code currently inherits chatgpt-review-7d905c07-a872-42… The third blocking issue is block-scope leakage in the new chatgpt-review-7d905c07-a872-42… On invariants: I’d classify the second issue as a direct violation of “No fallbacks that fabricate,” and the first and third as boundary-sufficiency / lost-structure problems. The invariants doc is explicit that when a downstream stage has to guess from names or partial shape, the real fix is to surface the missing fact structurally, not improve the guess. That is the core concern here: this PR improves the output-provenance walker, but two of the new branches still guess where the model should carry exact pattern facts. chatgpt-review-7d905c07-a872-42… chatgpt-review-7d905c07-a872-42… On compositional modeling quality: there are no std-library or extdeps modeling changes in this PR, so I do not see a chatgpt-review-201af2a9-c029-46… On roadmap alignment: The test delta is too thin for semantics this sensitive. In the diff, the only test change is the diagnostic ratchet going from 421 to 416. That is useful as an outer signal, but it does not protect the new behavior. This PR needs direct regression tests for renamed field destructuring, non-inductive-field fallback, and let-with-body scoping inside blocks. The thesis and modeling docs both push toward verification falling out from structure; this is exactly the class of change that should have focused semantic tests, not only a ratchet update. chatgpt-review-e460addd-59a7-46… chatgpt-review-a1219665-489d-48… So my recommendation is: request changes. The architecture is aligned with the thesis, but the new walker still introduces provenance facts in places where the structure does not fully justify them, and it conflates two identities in renamed destructuring. In this codebase, those are merge blockers. |
cff6f98 to
38f611b
Compare
ChatGPT ReviewI read the thesis first. Verdict: request changes. I reviewed the attached PR diff and a numbered copy. Directionally, the PR is pointed the right way. The thesis says correctness dimensions should be computed at binding sites during inference and then carried through the IR, and the roadmap calls output provenance on function signatures the M1 blocker. Reusing chatgpt-review-6206c230-b328-43… The blocking problem is the new chatgpt-review-5d0dc841-2293-4c… There is a second bug inside that same block: the lookup only filters inductive fields by The fallback at numbered diff lines 70–75 and 235–237 is also not mergeable. When no inductive field matches, it copies chatgpt-review-cb8189ff-88ef-40… I also think the new On tests, the diff only changes the bootstrap ratchet from 421 to 416, with no focused regression coverage for the new semantics. For a provenance change this central, a ratchet alone is too weak. The thesis’s whole promise is “sound by construction,” not “ratchet got smaller.” I would want direct tests for renamed destructuring, field-vs-binder identity, non-inductive-field fallback, and block scoping before merge. chatgpt-review-5843fdf0-06a9-46… chatgpt-review-5d0dc841-2293-4c… On compositional modeling quality: there are no std-library/extdeps/ROADMAP model changes in this PR, so there is no library chatgpt-review-cb8189ff-88ef-40… On roadmap alignment: My recommendation is: request changes. The fix direction is right, but this diff still violates the project’s standard in three concrete ways:
The shape of the fix is straightforward: carry both field label and binder name, resolve arm fields by full structural witness rather than field-name-only lookup, delete the generic inherit-scrutinee fallback, and make block accumulation preserve only statement-level lets. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · 38f611b3
Review (INVARIANTS: 4, MODELING: 1+/1-, ROADMAP: 1✓/1!)
INVARIANTS — Violations (4)
ROOT CAUSE ANALYSIS
src/v2/04_infer.dagThe new body walker re-derives pattern scope from string proxies instead of reusing the existing structural authority in extend_scope_with_pattern_node and derive_field_provenance (M8/M9): field label, binder name, and variant identity are available upstream in MatchPattern and InductiveField, but the new map builder collapses them into one name string, which then propagates wrong output provenance into call-site CX reasoning; the upstream fix is to derive arm let_prov from the typed pattern-scope pipeline, or call those helpers directly, so provenance is keyed by structural bindings rather than strings.src/v2/04_infer.dagTransparent wrapper or unwrapping behavior is not surfaced as a first-class field witness, so the walker guesses after lookup failure; that missing upstream fact propagates into false helper contracts and then into descent analysis. The upstream fix is to model transparent fields explicitly in the existing InductiveField/SubValueRelation vocabulary (M1/M9) and otherwise fail closed instead of inheriting scrutinee provenance.src/v2/04_infer.dagLexical scope is already computed upstream at binding sites, but classify_body_provenance rebuilds a second name-keyed scope machine for blocks; that parallel authority drops the let-statement versus let-expression distinction and leaks provenance downstream. The upstream fix is to derive body provenance from InferScope and TypeBinding.provenance, or at minimum restore state.prov after let_body-scoped lets so block threading matches the compiler's single scope authority (M1/M8/M9).
MODELING — Strengths
src/v2/04_infer.dagBlockProvFoldState is a flat product accumulator rather than a new recursive semantic type or bespoke result or error shape, so it stays within the bounded-kernel rule and composes with fold.
MODELING — Improvements
src/v2/04_infer.dagBlockProvFoldState hardcodes binding and parameter identity as Map<String,...>; per M4/M9 and ROADMAP Track 3, this accumulator should use structural binding references or dissolve into the existing InferScope and TypeBinding.provenance pipeline instead of becoming a second string-keyed authority.
ROADMAP — Verified
- M1 body inference active for non-recursive functions: The diff materially extends classify_body_provenance to cover match arm context, block threading, casts, and returns, which is real Track 1 progress.
ROADMAP — Incomplete
- M1 output provenance on function signatures: The new body walker still collapses pattern identities, fabricates unmatched-field provenance, and leaks let-body scope, so the blocker is only partially addressed and not yet sound enough for the thesis's zero-bugs standard.
ROADMAP — Unclaimed
- M1 ratchet baseline: src/v2/tests/src/bootstrap.rs lowers DIAG_RATCHET to 416, but ROADMAP.md still says currently 421, ratchet 421 and does not record the new baseline or the remaining unsoundness.
Track 1 direction is correct and algebraically aligned, but I would not merge this version because the new provenance walker still reconstructs pattern and scope facts unsoundly.
| 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 their fields. | ||
| let arm_let_prov = match arm_pattern(n: arm) { | ||
| VariantPattern { name: vname, parent_enum: _, field_bindings: bindings } => |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| _ => "" | ||
| } | ||
| } | ||
| if lookup_type != "" { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| Some { value: ind_field } => map_insert(fp_acc, pname, compose_sub_value(base: scrut_rel, field: ind_field)) | ||
| None => | ||
| // Field is not inductive — inherit scrutinee relation as-is. | ||
| // This handles Optional.Some { value: v } where "value" is the |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| 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.
This comment was marked as resolved.
Sorry, something went wrong.
|
Review (INVARIANTS: 4, MODELING: 1+/1-, ROADMAP: 1✓/1!) INVARIANTS — Violations (4) ROOT CAUSE ANALYSIS
MODELING — Strengths
MODELING — Improvements
ROADMAP — Verified
ROADMAP — Incomplete
ROADMAP — Unclaimed
Track 1 direction is correct and algebraically aligned, but I would not merge this version because the new provenance walker still reconstructs pattern and scope facts unsoundly. |
38f611b to
d529802
Compare
|
ChatGPT review in progress... (view conversation) |
Four soundness fixes to classify_body_provenance:
1. Shadowing: check let_prov before param_names in ExprVar. A local
`let x = y` in scope of parameter `x` now uses the local's
provenance, not the parameter's.
2. Match destructuring: compose field bindings through inductive fields
with variant_name in the filter. Uses field_binding_pattern (Bind
{ name }) for the introduced binding name, field_binding_name_at
for the field label. Fails closed on unmatched fields (no fabricated
fallback).
3. ExprBlock: fold with BlockProvFoldState tracks block-level let
bindings. Let-with-body restores outer scope so bindings don't
leak into subsequent statements.
4. ExprCast/ExprReturn: transparent wrappers delegate to inner
expression provenance.
https://claude.ai/code/session_01SnVJJPJua86vgbS96hcvmW
d529802 to
378dcb2
Compare
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · d5298027
Review (INVARIANTS: 1, MODELING: 1+/1-, ROADMAP: 1✓/1!)
INVARIANTS — Violations (1)
ROOT CAUSE ANALYSIS
src/v2/04_infer.dagThe upstream gap is that body provenance still rebuilds match scope from a lossy Map<String,...> instead of consuming the existing structural authority in extend_scope_with_pattern_node and derive_field_provenance; that lossy reconstruction turns any non-Bind field pattern into "", drops the nested binder from the arm scope, and downstream output_provenance underreports true source-to-drain links; the upstream fix is to derive arm scope from PatternScopeResult/InferScope and reuse the std/induction.dag SubValueRelation composition path per M4/M8/M9 rather than re-walking bindings ad hoc.
MODELING — Strengths
src/v2/04_infer.dagBlockProvFoldState is a local non-recursive product helper in src/v2 and the new walker stays inside the existing SubValueRelation/meet algebra, so the layering and algebraic attachment point are right.
MODELING — Improvements
src/v2/04_infer.dagBlockProvFoldState and arm_let_prov use Map<String,...> as identity proxies; per M4/M9 this should collapse into InferScope/PatternScopeResult or structural binding references so body inference reuses the compiler's single scope/provenance authority.
ROADMAP — Verified
- M1 body inference for non-recursive functions: The diff materially extends non-recursive body inference to cover match-arm scope extension, sequential blocks, casts, and returns.
ROADMAP — Incomplete
- M1 key blocker: OUTPUT PROVENANCE on function signatures: Nested match destructuring is still dropped during body inference, so the output provenance boundary is still lossy and not yet zero-bug safe.
ROADMAP — Unclaimed
- M1 body inference coverage update: ROADMAP.md was not updated to record this additional body-form coverage or the remaining nested-pattern limitation.
Directionally correct and materially closer to M1, but the new body walker still drops nested match binders and therefore does not yet meet the thesis's zero-bugs-by-construction bar.
| expr: Node | ||
| let_prov: Map<String, Map<String, SubValueRelation>> | ||
| } | ||
| ExprCast => |
There was a problem hiding this comment.
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.
|
Review (INVARIANTS: 1, MODELING: 1+/1-, ROADMAP: 1✓/1!) INVARIANTS — Violations (1) ROOT CAUSE ANALYSIS
MODELING — Strengths
MODELING — Improvements
ROADMAP — Verified
ROADMAP — Incomplete
ROADMAP — Unclaimed
Directionally correct and materially closer to M1, but the new body walker still drops nested match binders and therefore does not yet meet the thesis's zero-bugs-by-construction bar. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · 378dcb2f
Review (INVARIANTS: 2, MODELING: 2+/1-, ROADMAP: 1✓/2!)
INVARIANTS — Violations (2)
ROOT CAUSE ANALYSIS
src/v2/04_infer.dagMatch and block scope facts already originate upstream in extend_scope_with_pattern_node, derive_field_provenance, scope_after_stmt_node, and TypeBinding.provenance, but the new body walker rebuilds a second String-keyed scope machine; that re-derivation is what drops nested binders now and will keep creating shadow/merge bugs downstream in output_provenance. Upstream fix: make body provenance consume the existing pattern-scope/infer-scope authority end-to-end, then migrate that single authority to structural binding references for Track 3, per M4/M8/M9.
MODELING — Strengths
src/v2/00_core.dagRemoving ident from Node deletes a duplicate identity channel and makes the kernel more faithful to single-authority structural identity.src/v2/04_infer.dagBlockProvFoldState is a non-recursive product accumulator, so the new block walk stays algebraically grounded as fold state rather than introducing a second recursive semantic type.
MODELING — Improvements
src/v2/04_infer.dagBlockProvFoldState should dissolve into the existing scope pipeline or carry structural binding references, not Map<String,...> identity proxies, so the fold state matches M4/M9 instead of reifying a second scope model.
ROADMAP — Verified
- M1 non-recursive body-walker coverage: The diff really does add ExprMatch arm context, sequential ExprBlock threading, ExprCast passthrough, and ExprReturn passthrough to classify_body_provenance.
ROADMAP — Incomplete
- M1 body inference for non-recursive functions: The same diff still rebuilds scope ad hoc and leaves nested match destructuring outside the authoritative pattern-scope pipeline, so this blocker is only partially complete.
- M1 status line currently 420, ratchet 420: The same head commit still has src/v2/tests/src/bootstrap.rs at DIAG_RATCHET = 423, so the roadmap numbers are stale.
The PR resolves four concrete soundness bugs and materially advances M1, but the new body walker still duplicates scope authority instead of consuming the existing one, so it remains short of the thesis's zero-bugs-by-construction bar.
| // 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) { |
There was a problem hiding this comment.
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.
| // 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) => |
There was a problem hiding this comment.
Invariant violation: ExprBlock threads a second ad-hoc provenance scope through BlockProvFoldState instead of the existing inference scope, violating No duplicate representations.
|
Review (INVARIANTS: 2, MODELING: 2+/1-, ROADMAP: 1✓/2!) INVARIANTS — Violations (2) ROOT CAUSE ANALYSIS
MODELING — Strengths
MODELING — Improvements
ROADMAP — Verified
ROADMAP — Incomplete
The PR resolves four concrete soundness bugs and materially advances M1, but the new body walker still duplicates scope authority instead of consuming the existing one, so it remains short of the thesis's zero-bugs-by-construction bar. |
2 participants
Summary
This PR implements full output provenance inference for non-recursive function bodies, replacing the previous stub implementation. The system now walks typed expression trees to determine how function outputs relate to their parameters, enabling more precise data flow analysis.
Key Changes
New
BodyProvenanceCtxstruct: Carries state through expression walks including parameter set, binding provenances, type environment, and function signatures.Expression provenance inference (
infer_expr_provenance): Recursively walks typed expressions to compute output provenance maps. Handles:filter,map)Branch merging (
merge_provenance_branches): Implements lattice meet semantics for control flow joins. Parameters appear in results only if present in all non-empty branches, with values merged viameet_sub_value.Call composition (
compose_call_body_provenance): Maps callee parameters to caller arguments (by name or position) and composes output relations transitively. Uses non-recursive argument classification to avoid mutual recursion.Argument classification (
classify_arg_body_provenance): Lightweight provenance lookup for call arguments without recursion, handling variables and falling back to empty for complex expressions.Integration in
populate_output_provenance: Body inference is attempted first for non-recursive functions with bodies. Falls back to hardcoded tables (child accessors, size-reducing functions) when inference produces empty results, maintaining backward compatibility.Implementation Details
stacker::maybe_growininfer_expr_provenanceto handle deep expression trees safely.populate_output_provenance.Testing
Diagnostic ratchet updated from 424 to 421, reflecting improved inference reducing diagnostic count.
https://claude.ai/code/session_01SnVJJPJua86vgbS96hcvmW