SG-4b-1

[briansrls]

SG-4b-1 prototype tranche.

This PR takes a bounded Cat-1/Cat-2 helper slice through the existing infer_helpers.dag -> infer_helpers_generated.rs -> infer.rs path. It is not full SG-4 and does not claim infer.rs retirement.

Moved into .dag authority in this tranche:

• template_argument_value
• resolve_template_argument_value

Retained generated helper already on this path:

• behavior_output_port

Generated output is committed in the same PR and consumed from the real inference path.

Remaining authoritative in infer.rs:

• Cat-3/stateful logic remains untouched.
• Refinement/discharge helpers remain in Rust, including predicate_info and collect_conjunct_leaves.
• The following bounded Cat-1/Cat-2 candidates remain in Rust in this prototype: walk_to_optional_cardinality_decl, callable_template_arguments, declaration_is_callable, is_retryable_generic_decl_walk, template_arguments_match.
• Everything else outside this bounded helper slice remains in infer.rs.

Why the remainder stayed in Rust:

• walk_to_optional_cardinality_decl and callable_template_arguments are not moved because the current reflected helper surface does not expose the canonical total Dag::declaration(id) accessor, and rebuilding lookup in .dag would introduce parallel authority.
• predicate_info is not moved because the current reflected BindNode helper path does not expose the needed predicate-body fact honestly.
• is_retryable_generic_decl_walk is not moved because the current lens termination checker cannot prove its mutual-recursion cluster.
• declaration_is_callable and template_arguments_match are not moved because this helper emission path currently generates invalid Rust for those bool-returning helpers.

Verification run on this branch:

• cargo run -p v3-compiler --bin regen_lens -- --lens infer_helpers
• cargo fmt --all --check
• cargo clippy -p v3-compiler --all-targets -- -D warnings
• cargo test -p v3-compiler sg6_infer_helpers_generated_module_matches_checked_in_snapshot -- --nocapture
• cargo test -p v3-compiler infer -- --nocapture

[briansrls]

Latest diff read: this stays inside the intended SG-4b-1 bounds.

Good signs:

• it uses the existing infer_helpers.dag -> generated -> re-export from lib.rs path
• it moves only Cat-1/Cat-2 style helpers into the generated helper surface
• it does not appear to pull Cat-3 mutable-state logic into the tranche

So on scope, this is the right next step after SG-4a.

My only direction note is to keep the receipt explicit:

1. In the PR body, list the exact SG-4a candidate functions this tranche covers.
2. Say explicitly that Cat-3 functions remain in infer.rs untouched.
3. Frame this as SG-4b-1 prototype tranche, not SG-4 closure.

If it stays framed that way, I have no blocker on the current diff from a scope-discipline standpoint.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 004a296c16

ℹ️ 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".

[chatgpt-codex-connector]

Regenerate infer helpers before re-exporting new symbols

This pub(crate) use generated::{...} adds exports that do not exist in src/v3/compiler/src/infer_helpers_generated.rs at this commit, so the crate no longer compiles. Running cargo check -p v3-compiler fails with unresolved imports for each newly re-exported item (callable_template_arguments, PredicateInfo, etc.), which makes the change release-blocking until the generated file is updated (or the re-exports are removed).

Useful? React with 👍 / 👎.

[briansrls]

codex · gpt-5.4 · 004a296c

⚠️ Review (blocking: 1, non-blocking: 0+/0-)

BLOCKING (1)

Root Cause

• src/v3/lenses/infer_helpers.dag the helper authority grew without regenerating and committing its emitted Rust snapshot -> rerun regen_infer_helpers and land the matching src/v3/compiler/src/infer_helpers_generated.rs update in the same change.

⚠️ The helper tranche itself can be reviewed once the committed generated projection is back in lockstep with the .dag authority and lib.rs export surface.

[briansrls]

codex · gpt-5.4 · 25d65220

⚠️ Review (blocking: 1, non-blocking: 0+/0-)

BLOCKING (1)

Root Cause

• src/v3/lenses/infer_helpers.dag the reflected helper surface exposes raw d.declarations but not the authoritative total DeclarationId-to-Declaration accessor, so this tranche reconstructs lookup as maybe-missing -> reflect a total declaration-by-id accessor into .dag helpers or keep these lookups in Rust until that accessor exists.

⚠️ The regen drift is fixed, but this tranche still bakes a new fail-open declaration-lookup state into the authoritative helper path.

[briansrls]

codex · gpt-5.4 · ff97c723

✅ Review (blocking: 0, non-blocking: 1+/0-)

Non-blocking — Strengths

• src/v3/lenses/infer_helpers.dag The tranche boundary is explicitly documented with concrete deferred helpers and named triggers, so the remaining Rust authority reads as tracked scaffold rather than unbounded debt.

⚠️ No new blocking concerns in the added tranche, but the previously flagged declaration-lookup authority problem in infer_helpers is still unresolved.

[briansrls]

codex · gpt-5.4 · ff97c723

✅ Review (blocking: 0, non-blocking: 1+/0-)

Non-blocking — Strengths

• src/v3/lenses/infer_helpers.dag The tranche boundary is explicitly documented with concrete deferred helpers and named triggers, so the remaining Rust authority reads as tracked scaffold rather than unbounded debt.

⚠️ No new blocking concerns in the added tranche, but the previously flagged declaration-lookup authority problem in infer_helpers is still unresolved.

[briansrls]

Findings

• BLOCKING src/v3/lenses/infer_helpers.dag:48, src/v3/lenses/infer_helpers.dag:64, src/v3/lenses/infer_helpers.dag:93 — this tranche adds a second DeclarationId -> Declaration implementation (find_declaration) by walking d.declarations directly, and both migrated helpers read that raw storage field instead of a declared lookup/query surface. That’s a concrete L-7 / DB-5 violation: lens-style helpers are supposed to consume declared substrate queries, not re-derive lookup from storage shape, and it also introduces a parallel implementation of declaration lookup.
• BLOCKING src/v3/lenses/infer_helpers.dag:65, src/v3/lenses/infer_helpers.dag:94 — the new MissingDeclaration branch is collapsed into ordinary success-shaped results (MissingOptionalCardinality or { template: target, arguments: empty() }). If a DeclarationId is invalid, infer now fabricates a normal “not found / not instantiation” answer instead of failing closed, which violates the fail-closed / no-fallbacks-that-fabricate guidance.

Verdict: REQUEST_CHANGES

Nice incremental extraction overall, but I’d fix the declaration lookup authority first. As written, this helper path both bypasses the declared lookup surface and turns structural lookup failure into normal-looking inference results.

[briansrls]

claude-review (director) — ⚠️ REQUEST CHANGES — parallel authority on declaration lookup

Verified the SG manager's read on #609. The brief was "Cat-1/Cat-2 pure-helper tranche via the existing infer_helpers.dag → generated → ratchet pattern." The shape is right; one substantive problem before merge.

The blocker

The PR introduces:

pub enum DeclarationLookup {
    MissingDeclaration,
    FoundDeclaration { _0: Declaration },
}

pub fn find_declaration(p0: &[Declaration], p1: &DeclarationId) -> DeclarationLookup {
    match p0 {
        [] => DeclarationLookup::MissingDeclaration,
        [__list_head, __list_tail @ ..] => {
            if ((__list_head).id == (*(p1))) {
                DeclarationLookup::FoundDeclaration { _0: __list_head.clone() }
            } else {
                find_declaration(__list_tail, p1)
            }
        }
    }
}

and consumers downstream match on MissingDeclaration | FoundDeclaration to thread lookup failure.

Problem: Dag already has pub fn declaration(&self, id: DeclarationId) -> &Declaration as the canonical single-authority declaration accessor. This PR creates a parallel O(n) list-walk path that:

1. Duplicates authority — now there are two ways to resolve DeclarationId → Declaration, the official Dag::declaration and the new find_declaration. Per feedback_parallel_representation_debt: when a canonical source exists, consume it.
2. Changes the failure contract — Dag::declaration panics on unknown id (it's a witness-bearing handle; invalid ids are constructor-layer violations). The new DeclarationLookup treats "not found" as a normal inference outcome, which silently masks substrate-integrity violations — violates C-8 (fail-closed) and the Track 9 constructor-validation invariant.
3. Performance regression on paper — not the main concern, but O(n) list walk where the existing API resolves via typed handle.

What this lane should have done

Per the SG-4a authority map, Cat-1/Cat-2 helpers are structural readers over typed substrate facts that emit typed output. Declaration lookup by id is exactly the kind of thing that should consume Dag::declaration(id) (or a .dag accessor realization that compiles to it), not reconstruct the walk.

The walk-the-Vec pattern is appropriate for the few cases where you're iterating ALL declarations looking for a match by name / shape. For single-id resolution, typed handle access is the right shape.

Required before merge

1. Delete DeclarationLookup + find_declaration.
2. Replace each call site with dag.declaration(id) (or a .dag-authored accessor that realizes to the same Rust call).
3. If the calling code needs to tolerate "id doesn't exist" as a non-error case, that's a deeper issue — STOP and surface it as a substrate-integrity concern, not workaround with a parallel lookup path.
4. Re-run the infer test suite; the behavior should be identical modulo the declaration-lookup path.

The rest is good

The chosen tranche (pure walkers, template-argument helpers) matches SG-4a's Cat-1/Cat-2 set. infer.rs stays authoritative for everything else per brief. The pattern is right; just need to consume the existing declaration authority.

Ready for re-review once the parallel lookup is removed.

[briansrls]

codex · gpt-5.4 · a4d6241f

✅ Review (blocking: 0, non-blocking: 0+/0-)

✅ No new concerns in the added lines; this stays within the documented SG-4b-1 slice and clears the earlier projection-drift and declaration-lookup authority problems.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: a4d6241f · Trigger: schedule
• Thinking: 305s wall

---

✅ I do not see new thesis- or invariant-level concerns in the added lines after those two authority problems were removed.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: a4d6241f · Trigger: schedule
• Thinking: 43s wall

---

Findings

Nothing blocking. A couple of small observations worth naming:

• infer.rs:1490-1493 — The new TemplateArgumentLookup typed carrier is immediately flattened to Option<DeclarationId> at the Rust shim. That's fine as a bridge (the rest of infer.rs still speaks Option), but it means the richer typed distinction the .dag now expresses is not yet visible to consumers. Non-blocking; natural to propagate the typed carrier as more of infer lands on the .dag authority.

• lib.rs:99 — Adding clippy::large_enum_variant to lens_cost's #[allow] list looks orthogonal to the infer_helpers migration bundled in this PR. Not a modeling concern, just flagging it as a drive-by change that's easy to miss.

• infer_helpers_generated.rs:19-34 — The generated template_argument_value is now recursive where the hand-written version was iterator-based. Template argument lists are small in practice so stack depth is a non-issue, but worth noting the representation shift (the behavior claim "linear scan" is preserved; the runtime shape isn't).

The depth → remaining inversion in resolve_template_argument_value (shim passes WALK_DEPTH_LIMIT.saturating_sub(depth) as i64) checks out — depth=0 → remaining=WALK_DEPTH_LIMIT; depth=LIMIT → remaining=0 → returns current, matching the original guard. Termination unchanged.

The infer_helpers.dag preamble does a good job naming what is not moving and why (Cat-3 helpers need substrate work that isn't ready, predicate body port not reflected, etc.) — that's the kind of scaffold-honesty the modeling-discipline doc asks for.

Verdict

APPROVE — small, narrowly-scoped migration of two pure helpers from infer.rs to .dag authority via the already-proven emit_rust_module path. The diff is tight, the remainders are named, and the new typed carrier is a step up from the raw Option even though it's flattened at the boundary today.