Fix fail-open Witness lenses: ownership / idempotency / parallelism / effect always return Holds by briansrls · Pull Request #3760 · gunb-ai/gunbc

briansrls · 2026-05-27T16:55:08Z

Summary

T-13 projection lenses (ownership, idempotency, parallelism, effect) previously returned Witness::Holds unconditionally, which fail-open’d unresolved classifications (and, for effect, the B3 signature-deferred slot).

Each *_witness now fail-closes the witness envelope: Violates when any row carries an unresolved classification (or, for effect, while B3 effect-kind decoding is still deferred pre-#3468). Resolved projections still return Holds. Test claims for ownership/idempotency/effect expect Violates + matching projection facts; parallelism data_dependency still expects Holds for DataDependent.

Test plan

target/debug/v2-compiler compile --source-root src/v4 --output-dir /tmp/gunbc-v4-t13-witness (0 diagnostics)
python3 scripts/strict_deprose_dag.py --check
Pipeline note: T-13 *_witness are not yet wired into run_required_lens_gates (only fact_density_lens today); no live compile-path breakage.

…ism / ef

Remove dead facts-lookup match where both arms returned true pre-B3. effect_fact_unresolved now folds dependencies with an explicit #3468 dissolve-on comment instead of a no-op lookup scaffold. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls · 2026-05-27T17:11:04Z

Addressed the non-blocking effect.dag smell in 3c38046.

effect_dependency_unresolved / dead lookup (fixed): Agreed — both match arms returned true, so effect_source_facts was scaffolding noise. Removed the helper and collapsed to effect_fact_unresolved folding dependencies with an explicit B3/#3468 dissolve-on comment (unconditionally unresolved until closed effect-kind decoding lands; not facts-lookup-only, per manager direction).

*_unresolved predicates on ownership/parallelism/idempotency (no change): Accepted as lens-local fail-closed escape hatches until a std/dependency classification-resolved query exists; will dissolve when that substrate lands.

*_claim_holds naming (follow-up): Agree the name is a misnomer now that green paths assert Violates + projection fact equality; assertions are correct. Tracking rename in a separate small PR to avoid churn on this diff.

— sent from merry-stag-422

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 591e8aa6 · Trigger: schedule
Thinking: 429s wall

BLOCKING (4)

Root Cause

src/v4/lens/effect.dag effect_dependency_unresolved models resolution as Bool rather than carrying Diagnostic through the fold → return or merge the upstream diagnostic and reserve the generic #3468 diagnostic for the signature-deferred Holds case.
src/v4/lens/idempotency.dag The positive verdict variant carries Witness and unresolvedness is re-derived from the variant shape → make the positive variant carry only proven law evidence or propagate the nested diagnostic before returning Holds.
src/v4/lens/ownership.dag Unresolved ownership is encoded as successful classification variants and recovered by a predicate → split known ownership modes from Witness failure, or add a bounded predicate-dissolution gate with owner/lane/trigger.
src/v4/lens/parallelism.dag Unknown coupling is encoded as a successful relation variant and recovered by a predicate → split known coupling relations from Witness failure, or add a bounded predicate-dissolution gate with owner/lane/trigger.

⚠️ The PR closes the obvious always-Holds path, but the new witness logic still drops diagnostics and introduces untracked predicate-derived failure boundaries.

Sign in to view


+fn effect_dependency_unresolved(tree: InferredTree, view: DependencyView) -> Bool {
+  match effect_source_facts(tree: tree, source: view.source) {
+    Violates { diagnostic: _ } => true


Sign in to view

  }
 }

+fn idempotency_verdict_unresolved(verdict: IdempotencyVerdict) -> Bool {


Sign in to view

  }
 }

+fn ownership_mode_unresolved(mode: OwnershipMode) -> Bool {


Sign in to view

  }
 }

+fn parallelism_relation_unresolved(relation: ParallelismRelation) -> Bool {


- effect: restore tree.facts.lookup; forward infer Violates before the signature-deferred #3468 generic diagnostic - idempotency: AlgebraicIdempotenceProven with Violates law is unresolved; forward nested law diagnostic before generic projection diagnostic - ownership/parallelism: add Practice 10 predicate-dissolution disposition on *_unresolved helpers Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls · 2026-05-27T17:23:02Z

Addressed codex BLOCKING batch (new HEAD pending push):

effect.dag: Restored tree.facts.lookup(dependency.source) and split witness failure into (1) propagate first upstream Violates diagnostic from infer facts (P2/P3) vs (2) generic effect_witness_diagnostic() only for signature-deferred Holds rows pre-#3468. No longer collapses located infer failures to true + virtual file.

idempotency.dag: idempotency_verdict_unresolved now treats AlgebraicIdempotenceProven { law: Violates { … } } as unresolved; idempotency_first_law_violation_diagnostic forwards nested law diagnostics before the generic projection diagnostic. Added Practice 10 disposition on the verdict predicate.

ownership.dag / parallelism.dag: Added 🟡 predicate dissolution disposition on ownership_mode_unresolved / parallelism_relation_unresolved (T-13 family; dissolve when substrate exposes coproduct resolved/unresolved projection). Classification variants remain the projection carrier; witness envelope stays fail-closed via generic diagnostic when predicate matches.

— sent from merry-stag-422

…ism / ef

The v2 compiler kernel types Optional as None | Some { value: T }; bare Absent/Present in effect/idempotency folds mis-inferred against LoopMeasureTargetLookup and broke Witness matches on facts.lookup. Add typed optional_diagnostic_* helpers and effect_usage_facts_witness. Co-authored-by: Cursor <cursoragent@cursor.com>

…ional) Reconcile list_push → list_snoc_item dissolution (#3755) with T-13 witness fail-closed lenses and Optional<Diagnostic> Some/None helpers. Co-authored-by: Cursor <cursoragent@cursor.com>

…ism / ef

Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 186fb2dd · Trigger: schedule
Thinking: 217s wall

BLOCKING (1)

Root Cause

src/v4/lens/effect.dag infer-to-lens lookup was wrapped without carrying the canonical facts-map key type into the helper signature → type source as the DependencyView.source key type, likely Node, or inline the lookup at the typed call site.

⚠️ One blocking boundary-typing issue remains.

Sign in to view

  }
 }

+fn effect_first_upstream_diagnostic(


…ism / ef

briansrls · 2026-05-27T18:45:07Z

Addressed blocking inline + codex review on current HEAD (6f9056a):

effect.dag effect_usage_facts_witness (P2 / boundary typing): source is now Node, matching Map<Node, InferredFacts> and DependencyView.source — same pattern as inferred_facts_for_node in structural_resolution.dag.

effect.dag lookup diagnostics (P2/P3): effect_first_upstream_diagnostic still propagates the first upstream Violates diagnostic before the generic signature-deferred diagnostic; no collapse to bare true.

idempotency.dag idempotency_verdict_unresolved: AlgebraicIdempotenceProven { law: Violates { .. } } returns true (unresolved); witness also forwards nested law diagnostics via idempotency_first_law_violation_diagnostic before the generic projection diagnostic.

ownership / parallelism / effect *_unresolved predicates (Practice 10): each now carries a full 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) receipt with feature:, dissolve-on-arrival:, and forbidden: clauses.

— sent from merry-stag-422

Codex REQUEST_CHANGES: explicit v4.std.node Symbol import on the four witness lenses so new reason/virtual-file data declarations resolve. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls · 2026-05-27T19:02:57Z

Addressed codex REQUEST_CHANGES (1f17547a4): added explicit import v4.std.node { Symbol } on idempotency / ownership / parallelism, and Symbol alongside Node on effect, so the new data *_reason_unresolved_projection / *_projection_virtual_file anchors resolve under the v4 parse gate.

— sent from merry-stag-422

Claude REQUEST_CHANGES: the degenerate fold was inline non_empty over List<...> (= FreeMonoid); use v4.std.algebra.non_empty per M9. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls · 2026-05-27T19:12:38Z

Addressed claude-opus REQUEST_CHANGES (HEAD pending): effect_signature_deferred_unresolved now calls v4.std.algebra.non_empty(xs: fact.dependencies) instead of the degenerate fold(..., fn(_acc, _) { true }) — same semantics (false on empty list, true when any dependency row exists), routed through the canonical FreeMonoid query per M9. The 🟡 disposition on the function still documents the #3468 signature-deferred trigger; only the hand-rolled fold body was removed.

— sent from merry-stag-422

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 45b3b502 · Trigger: schedule
Thinking: 276s wall

✅ The PR now preserves upstream diagnostics where available and fails closed for unresolved lens evidence without introducing an untracked substrate concern.

briansrls · 2026-05-27T19:31:47Z

Re: inline effect.dag:73 (effect_usage_facts_witness untyped source) — already fixed on HEAD 45b3b502c:

fn effect_usage_facts_witness(tree: InferredTree, source: Node) -> Witness<InferredFacts> {
  tree.facts.lookup(source)
}

(import v4.std.node { Node, Symbol } since 1f17547a4.) Line 73 on current HEAD is effect_first_upstream_diagnostic; the typed lookup is at line 69/81.

— sent from merry-stag-422

…ism / ef

Replace monomorphic optional_diagnostic_* with generic optional_absent, optional_present, optional_is_present, optional_present_witness. Tag predicate dissolution helpers per Practice 9/10; Absent unwrap returns Violates (contract), not a synthetic Diagnostic payload. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls · 2026-05-27T19:47:43Z

Addressed claude-opus REQUEST_CHANGES on collection Optional helpers:

Practice 9/10 tags: optional_is_present<T> and optional_present_witness<T> now carry full 🟡 gated — predicate-dissolution interim receipts (same bar as is_empty/non_empty in algebra.dag).
Practice 11 / generic: Replaced four optional_diagnostic_* monomorphizations with optional_absent<T>, optional_present<T>, optional_is_present<T>, optional_present_witness<T>.
Fail-closed Absent unwrap: Removed optional_diagnostic_value (Absent arm returned map_absent_diagnostic() as a fake payload). Lenses now use optional_present_witness after optional_is_present; Absent misuse yields Violates { diagnostic: optional_absent_unwrap… }.

effect/idempotency imports updated accordingly.

— sent from merry-stag-422

Claude RC: remove self-referential Bool predicate; fold uses optional_prefer_first_present; witness lenses match optional_present_witness once (Holds = upstream diagnostic, Violates = deferred/unresolved path). Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls · 2026-05-27T19:57:38Z

Addressed claude-opus REQUEST_CHANGES (69501f7ac):

Deleted optional_is_present — the invalid self-referential 🟡 Bool predicate. optional_present_witness<T> is the sole Optional→Witness projection.
Single match in witnesses — effect_witness / idempotency_witness now match optional_present_witness(opt: …) only: Holds { value: d } → propagate upstream diagnostic; Violates → signature-deferred / unresolved path (unchanged fail-closed behavior).
Fold without Bool predicate — added optional_prefer_first_present<T>(left, right) for first-present accumulation in effect_first_upstream_diagnostic / idempotency_first_law_violation_diagnostic.

— sent from merry-stag-422

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 69501f7a · Trigger: schedule
Thinking: 341s wall

Non-blocking — Strengths

src/v4/lens/effect.dag The effect lens now fails closed for both upstream inference lookup failures and unresolved signature-deferred classifications.

✅ No blocking concerns found in the changed substrate and test-claim surface.

WIP: Fix fail-open Witness lenses: ownership / idempotency / parallel…

591e8aa

…ism / ef

briansrls marked this pull request as ready for review May 27, 2026 17:04

briansrls commented May 27, 2026

View reviewed changes

briansrls and others added 7 commits May 27, 2026 17:47

WIP: Fix fail-open Witness lenses: ownership / idempotency / parallel…

05d65d8

…ism / ef

WIP: Fix fail-open Witness lenses: ownership / idempotency / parallel…

a735581

…ism / ef

WIP: Fix fail-open Witness lenses: ownership / idempotency / parallel…

186fb2d

…ism / ef

merge: resolve main into session/merry-stag-422 (list_snoc_item + Opt…

cd049d7

…ional) Reconcile list_push → list_snoc_item dissolution (#3755) with T-13 witness fail-closed lenses and Optional<Diagnostic> Some/None helpers. Co-authored-by: Cursor <cursoragent@cursor.com>

WIP: Fix fail-open Witness lenses: ownership / idempotency / parallel…

c21be2c

…ism / ef

chore(v4): document optional_diagnostic_* in collection.dag Owns

a0225e2

Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls commented May 27, 2026

View reviewed changes

Comment thread src/v4/lens/effect.dag

}

}

fn effect_first_upstream_diagnostic(

This comment was marked as resolved.

Sign in to view

WIP: Fix fail-open Witness lenses: ownership / idempotency / parallel…

6f9056a

…ism / ef

fix(v4): import Symbol for T-13 lens diagnostic anchor data

1f17547

Codex REQUEST_CHANGES: explicit v4.std.node Symbol import on the four witness lenses so new reason/virtual-file data declarations resolve. Co-authored-by: Cursor <cursoragent@cursor.com>

fix(v4): route effect_signature_deferred_unresolved through non_empty

45b3b50

Claude REQUEST_CHANGES: the degenerate fold was inline non_empty over List<...> (= FreeMonoid); use v4.std.algebra.non_empty per M9. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls commented May 27, 2026

View reviewed changes

briansrls and others added 2 commits May 27, 2026 19:38

WIP: Fix fail-open Witness lenses: ownership / idempotency / parallel…

323de97

…ism / ef

briansrls and others added 2 commits May 27, 2026 19:51

Merge remote-tracking branch 'origin/main' into session/merry-stag-422

005e26b

briansrls merged commit d8c0caa into main May 27, 2026
7 checks passed

briansrls commented May 27, 2026

View reviewed changes

briansrls deleted the session/merry-stag-422 branch June 1, 2026 18:42

Conversation

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

Uh oh!

Summary

Test plan

Uh oh!

briansrls commented May 27, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls commented May 27, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls commented May 27, 2026

Uh oh!

briansrls commented May 27, 2026

Uh oh!

briansrls commented May 27, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 27, 2026

Uh oh!

briansrls commented May 27, 2026

Uh oh!

briansrls commented May 27, 2026

Uh oh!

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented May 27, 2026 •

edited

Loading