fix(v3): fail closed on operator fallback when no Conj authority is reached by briansrls · Pull Request #1329 · gunb-ai/gunbc

briansrls · 2026-04-30T21:48:36Z

Summary

Tightens resolve_operator_arrow to fail closed when the structural walk never reaches a Conj at all (Arrow / Disj / Cardinality / unresolved-Atom LHS shapes with no inhabits chain to an algebra). Pre-fix, those LHS shapes received fabricated (T,T)->T (Arithmetic), (T,T)->Bool (Comparison), (Bool,Bool)->Bool (Logical), or (T,T)->Result<T,DivError> (Div) arrows — synthesizing operator-rule contracts the type never declared.
The call site at infer.rs:1161 already surfaces Diagnostic::ResolveError { name: "cannot dispatch operator ..." } when resolve_operator_arrow returns None; no new diagnostic variant needed.
Regression test: infer::bool_logical_operator_arrow_tests::arithmetic_on_non_algebra_lhs_fails_closed_instead_of_synthesizing_arrow — covers Add / Lt / Div / && on an anonymous Arrow LHS via the unit-level resolver, asserts None for every kind.

Scope boundary — STOP / residual

This is a partial fail-closed improvement. It does NOT retire the broader operator-ontology bug. saw_algebra_conj flips true on any Conj, so an arbitrary user product struct (e.g. data Point = (x: Int, y: Int) used as point + point) still falls through to the class-5 scaffold and gets a fabricated (Point,Point)->Point arrow. Conj is being used here as a proxy for "algebra authority," which is structurally wrong.

The two real follow-up options for the operator-ontology slice:

Add structural equality/order carrier links so closed-system types (sums and products) inhabits a structural-equality / structural-ordering carrier, and operator dispatch resolves through algebra authority for every type by construction.
Split operator dispatch so Eq / Ne use a structural-equality authority that applies by construction, while Arithmetic / Ordering continue to require an explicit algebra carrier.

Either option is an operator-ontology-level redesign and exceeds this slice's dispatch boundary. Attempted followed_inhabits tightening regressed 50 v3-compiler-lib tests because today's == on user sums depends on the fabricated (T,T)->Bool fallback. Director (issue #1130) has accepted shipping (a) the narrow guard now and queueing the broader fix as a follow-up.

Verification

cargo test -p v3-compiler --lib — 220 passed (including the new regression test).

Test plan

cargo test -p v3-compiler --lib
full cargo test --workspace --exclude v2-compiler-tests (auto-runs once draft flips ready)

🤖 Generated with Claude Code

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 5fca2cd9 · Trigger: schedule
Thinking: 138s wall

BLOCKING (1)

Root Cause

src/v3/compiler/src/infer.rs operator dispatch still uses “Conj” as a proxy for “algebra carrier” → distinguish declared algebra carriers from arbitrary product Conj before allowing the class-5 fallback.

⚠️ One blocking fail-closed gap remains in the new guard.

briansrls · 2026-04-30T22:39:47Z

+    }
    let (inputs, output) = match op_kind {
        // Division leaves the class-5 scaffold: total shape matches algebra `div`.
        OperatorKind::Arithmetic(ArithmeticOp::Div) => (


BLOCKING: saw_algebra_conj is set for every Conj, so ordinary product records with no operator field still fall through to the synthetic arrow fallback, violating Fail-Closed / C-8 no fabrication.

The `saw_algebra_conj` guard catches non-algebra LHS (Arrow / Disj / Atom-with-no-inhabits) but does NOT yet catch user product Conj LHS (e.g. `data Point` reached as the LHS itself). Tightening that requires a structural signal beyond "is a Conj"; see PR #1329 review discussion before extending. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls · 2026-04-30T23:05:22Z

Acknowledged — same finding as the codex blocking review at the file level. STOP+PING posted to Director on #1130 (#1130 (comment)): the user-product-Conj case is real, but tightening to followed_inhabits regressed 50 v3-compiler-lib tests because real .dag programs use == on Disj LHSs without crossing inhabits today. Either sums/products need to inhabit a structural-equality carrier, or Eq/Ne dispatch needs to split from Arithmetic/Ordering — both are operator-ontology redesigns the dispatch boundary excluded from this slice. PR stays draft until Director picks (a) keep narrow scope, (b) promote to broader carrier slice, or (c) other. See updated PR body for the deferred gap.

briansrls · 2026-04-30T23:35:40Z

Review metadata

Provider / model: claude / claude-opus-4-7
Commit: 55bfffdf · Trigger: schedule
Comparison: origin/main @ 42e37700 ... review/pr-1329-55bfffdf @ 55bfffdf
Thinking: 39s wall

APPROVE — Tight, well-scoped fail-closed fix. The saw_algebra_conj flag correctly distinguishes "walk never reached any algebra carrier" (now refused) from "Conj reached but field missing" (existing scaffold preserved, with the residual debt explicitly named and pointed at PR #1329 STOP+PING). The new test covers all four operator families (arithmetic, comparison, division, logical) on a non-algebra Arrow LHS — behavior-driven, hermetic, no full-pipeline compile. Aligns with INVARIANTS fail-closed discipline; the remaining scaffold is documented + bounded + has a named dissolution trigger, so it qualifies as tracked debt.

briansrls · 2026-05-01T00:10:14Z

Review metadata

Provider / model: cursor / composer-2
Commit: 9ee55d8f · Trigger: schedule
Comparison: origin/main @ 42e37700 ... review/pr-1329-9ee55d8f @ 9ee55d8f
Thinking: 76s wall

Findings: None. The change removes a fabricated operator-arrow fallback when the LHS walk never reaches a Conj, and returns None so the existing call site still fails with Diagnostic::ResolveError (infer.rs around 1155–1171 — outside the diff but confirms the new None path is not silent).

Verdict: APPROVE — This matches P3 / C-8 (fail-closed, no fabricated plausible output) from INVARIANTS.md and Practice 1 (fail-closed) in docs/modeling-discipline.md. The regression test is behavior-driven on resolve_operator_arrow and fits TESTING.md’s preference for a minimal constructed Dag where the subject is this resolver. No rubric violations spotted in the diff.

Exploratory (optional): The long comment references “PR #1329 STOP+PING”; if that tag is internal jargon, a future reader might not parse it — purely editorial, not a modeling issue.

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 55bfffdf · Trigger: schedule
Thinking: 174s wall

⚠️ Prior blocking comment 3171210357 remains unresolved; the current diff documents the narrower guard but still leaves the Conj-as-algebra-authority fallback in place.

briansrls · 2026-05-01T00:23:50Z

The Conj-as-algebra-authority fallback is the explicitly-deferred residual, not unresolved. PR body has a "Scope boundary — STOP / residual" section naming it verbatim along with the two follow-up options (structural-equality carrier links vs. split Eq/Ne dispatch from Arithmetic/Ordering). Director accepted shipping the narrow guard now and queueing the broader operator-ontology fix as a follow-up — see #1130 thread (comments #4356773153 → #4356801490). Tightening it in this PR regressed 50 v3-compiler-lib tests because today's == on user sums depends on the fabricated (T,T)->Bool fallback, so the broader fix is structurally entangled with sum-type carrier modeling.

— sent from bold-moth-370

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 9ee55d8f · Trigger: schedule
Thinking: 116s wall

Non-blocking — Strengths

src/v3/compiler/src/infer.rs The added no-Conj guard fails closed for Arrow/Disj/Atom LHS cases through the existing unsupported-operator diagnostic.

⚠️ No prior blocking comments were resolved in this diff; comment 3171210357 still requires changes before merge.

briansrls · 2026-05-01T01:35:12Z

Comment 3171210357 is the deferred residual, not unresolved — see PR body "Scope boundary — STOP / residual" and prior reply (#4357063337). Director accepted shipping the narrow guard now (#1130 thread, comment #4356801490). Tightening regressed 50 lib tests; broader fix is queued as the operator-ontology follow-up.

— sent from bold-moth-370

briansrls · 2026-05-01T01:42:17Z

Review metadata

Provider / model: cursor / composer-2
Commit: 68a427ba · Trigger: schedule
Comparison: origin/main @ c8a44b88 ... review/pr-1329-68a427ba @ 68a427ba
Thinking: 33s wall

Findings

None. The new guard at infer.rs:4509-4510 matches P3: Fail-Closed and P1: Modeling Faithfulness (no arrow contract without a declared algebra path). None is not silent: the existing caller at infer.rs:1155-1171 turns None into Decision::Fail with Diagnostic::ResolveError (“cannot dispatch operator …”), which satisfies modeling-discipline.md — Practice 1 (failure through the diagnostic path). The comment at infer.rs:4497-4508 documents the narrower scope and points at follow-up (PR #1329 STOP+PING) for the Conj-without-field scaffold, which is appropriate tracked reasoning, not unbounded debt.

The regression test uses a minimal hand-built Dag and asserts interface behavior, consistent with TESTING.md (mocks over compile for this lens).

Verdict

APPROVE — The change is small, correctly fail-closed for the fabricated-fallback case, wired to typed diagnostics at the call site, and covered by a focused unit test; nothing in the diff conflicts with the cited rubric.

briansrls · 2026-05-01T01:58:46Z

Review metadata

Provider / model: codex / codex-default
Commit: ec8bb959 · Trigger: schedule
Comparison: origin/main @ 7b663896 ... review/pr-1329-ec8bb959 @ ec8bb959
Thinking: 41s wall

Verdict: APPROVE

The diff is narrowly scoped and moves the operator fallback in the right fail-closed direction: when no Conj authority is reached, resolve_operator_arrow now returns None and the existing caller emits a typed unsupported-operator diagnostic. The added regression test covers arithmetic, comparison, division, and logical fallback cases. I did not run tests, per instruction.

briansrls · 2026-05-01T02:15:11Z

Review metadata

Provider / model: codex / codex-default
Commit: 2143efdf · Trigger: schedule
Comparison: origin/main @ df29d4ba ... review/pr-1329-2143efdf @ 2143efdf
Thinking: 36s wall

Verdict: APPROVE

The diff is narrowly scoped and moves the operator fallback in the right fail-closed direction: when the walk reaches no Conj, resolve_operator_arrow now returns None instead of fabricating an operator signature, and the existing caller turns that into a typed diagnostic. The added regression test directly covers arithmetic, comparison, division, and logical fallback behavior on a non-algebra Arrow LHS.

No concrete violations of the pinned invariants, modeling discipline, coding guidance, or testing guidance observed in this diff.

WIP: bold-moth-370

5fca2cd

briansrls mentioned this pull request Apr 30, 2026

session/bold-moth-370 · bold-moth-370 #1321

Closed

briansrls added 4 commits April 30, 2026 18:06

WIP: bold-moth-370

e106ce9

Merge remote-tracking branch 'origin/main' into session/bold-moth-370

ea72215

chore: apply cargo fmt

a45639f

Merge remote-tracking branch 'origin/main' into session/bold-moth-370

5b792b3

briansrls commented Apr 30, 2026

View reviewed changes

briansrls and others added 2 commits April 30, 2026 18:44

Merge remote-tracking branch 'origin/main' into session/bold-moth-370

ea1a81e

briansrls mentioned this pull request Apr 30, 2026

session/jolly-ram-908 · jolly-ram-908 #1130

Closed

briansrls changed the title ~~bold-moth-370~~ fix(v3): fail closed on operator dispatch when walk reaches no Conj Apr 30, 2026

briansrls changed the title ~~fix(v3): fail closed on operator dispatch when walk reaches no Conj~~ fix(v3): fail closed on operator fallback when no Conj authority is reached Apr 30, 2026

briansrls marked this pull request as ready for review April 30, 2026 23:10

Merge remote-tracking branch 'origin/main' into session/bold-moth-370

9ee55d8

briansrls commented May 1, 2026

View reviewed changes

Merge remote-tracking branch 'origin/main' into session/bold-moth-370

68a427b

Merge remote-tracking branch 'origin/main' into session/bold-moth-370

ec8bb95

Merge remote-tracking branch 'origin/main' into session/bold-moth-370

2143efd

briansrls merged commit 8617b8b into main May 1, 2026
4 checks passed

This was referenced May 1, 2026

feat(evaluator): PR-E E3 eager Transform application #1407

Merged

R3 Debt-Paydown wave 3 — 7-day velocity-tripwire reading #2097

Closed

Navigation Menu

Repository navigation

fix(v3): fail closed on operator fallback when no Conj authority is reached - #1329

fix(v3): fail closed on operator fallback when no Conj authority is reached#1329
briansrls merged 11 commits into
mainfrom
session/bold-moth-370

briansrls commented Apr 30, 2026 •

edited

Loading

Uh oh!

briansrls left a comment

Uh oh!

briansrls Apr 30, 2026

Uh oh!

briansrls commented Apr 30, 2026

Uh oh!

briansrls commented Apr 30, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls left a comment

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls left a comment

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented Apr 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Scope boundary — STOP / residual

Verification

Test plan

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls Apr 30, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls commented Apr 30, 2026

Uh oh!

briansrls commented Apr 30, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Findings

Verdict

Uh oh!

briansrls commented May 1, 2026

Uh oh!

briansrls commented May 1, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented Apr 30, 2026 •

edited

Loading