T-13 — lens family expansion: lens/parallelism.dag + lens/effect.dag + lens/ownership.dag + lens/idempotency.dag (one mechanism, projection-only per Practice 11; lens-over-substrate enforced; reads InferredTree + dependency-graph projection; produces Witness<dimension>; canonical reference = T-12 PR by briansrls · Pull Request #3468 · gunb-ai/gunbc

briansrls · 2026-05-21T01:30:42Z

Summary

Fills the T-13 v4 lens family for parallelism, effects, ownership, and idempotency as projection-only readers over InferredTree and the existing dependency graph projection. Each lens now exposes a Witness<...Fact> carrier and shares the same dependency-driven shape rather than adding a parallel substrate mechanism.

Adds compile-only claim fixtures under src/v4/test/claim/lens_{parallelism,effect,ownership,idempotency}/ to mirror the T-12 claim pattern for the new dimensions.

Test plan

target/debug/v2-compiler compile --source-root src/v4 --output-dir /tmp/gunbc-v4-t13-check -> compiled 100 files, 0 diagnostics
python3 scripts/strict_deprose_dag.py --check -> OK
rg -n "import v4\.lens\.(parallelism|effect|ownership|idempotency)|v4\.lens\.(parallelism|effect|ownership|idempotency)" src/v4/compiler src/v4/std src/v4/extdeps -> no matches
rg -n "WholeFile|Whole[A-Z][A-Za-z]*" src/v4/lens/parallelism.dag src/v4/lens/effect.dag src/v4/lens/ownership.dag src/v4/lens/idempotency.dag src/v4/test/claim/lens_parallelism src/v4/test/claim/lens_effect src/v4/test/claim/lens_ownership src/v4/test/claim/lens_idempotency -> no matches

….dag + l

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 1b1f691d · Trigger: schedule
Thinking: 323s wall

BLOCKING (5)

Root Cause

src/v4/lens/effect.dag T-13 was authored against an unlanded DependencyView substrate → land the dependency projection carrier in this PR or retarget these lenses to an existing v4 std carrier.
src/v4/test/claim/lens_effect/effect_depends_on.dag The claim fixtures duplicate InferredFacts construction instead of using a shared current infer fixture → add the cost witness once in a shared helper or update every new claim constructor.
src/v4/lens/effect.dag DependencyKind-to-effect mapping has no closed structural carrier or unknown/violation path → make the mapping exhaustive over the dependency substrate or carry an explicit violation witness.
src/v4/lens/effect.dag EffectKind collapses signature/resource/algebra facts into ReadEffect/WriteEffect/BarrierEffect → carry or consume the algebraic effect law witness before deriving IdempotencyVerdict.
src/v4/lens/effect.dag T-13 claim predicates need a canonical structural equality/content_hash surface → use the canonical equality operator/runner or add a tracked feature gate for the missing primitive before hand-written eq helpers spread across lenses.

⚠️ The PR introduces unresolved substrate imports, stale infer facts, and lens projections that bypass the modeled algebraic authority.

….dag + l

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 993c8ff9 · Trigger: schedule
Thinking: 306s wall

BLOCKING (3)

Root Cause

src/v4/lens/parallelism.dag ParallelismRelation conflates edge-blocker evidence with pairwise non-edge independence → split dependency-blocker facts from independent-pair proofs or derive independence through the canonical graph query.
src/v4/lens/idempotency.dag IdempotencyVerdict has no required algebra-law witness for positive idempotency → make Idempotent carry or consume the effect-algebra law witness, or leave dependency-only cases requiring algebra evidence.
src/v4/lens/ownership.dag DependencyView carries only broad dependency kind where ownership needs access and alias-mode facts → add or consume resource-access facts before deriving ExclusiveMutation.

⚠️ The PR still has substrate-level modeling issues in the new lens carriers.

….dag + l

briansrls

Review metadata

Provider / model: codex / unknown
Commit: eefc5a75 · Trigger: schedule
Thinking: 319s wall

BLOCKING (5)

Root Cause

src/v4/lens/effect.dag lens fact carriers copy endpoint identities out of DependencyView → make the dependency edge the sole endpoint authority and derive at/owner/source/dependent through accessors.
src/v4/lens/ownership.dag ownership projects from broad dependency edges but re-authors endpoint identity locally → remove copied endpoints or replace DependencyView with a typed ownership edge that owns them once.
src/v4/lens/parallelism.dag parallelism facts are modeled as enriched copies of DependencyView → keep one canonical edge and attach only the dimension-specific relation/evidence.
src/v4/lens/idempotency.dag idempotency lacks a first-class idempotence-law carrier from std/algebra → introduce or consume a typed law witness rather than reusing generic InferredFacts.
src/v4/lens/ownership.dag lens claim equality helpers reify structural identity as local predicates → use derived == or add a valid Practice 10 disposition/gate before reusable helpers land.

⚠️ Blocking substrate modeling issues remain in the new lens carriers.

briansrls · 2026-05-21T04:18:26Z

+// dependency projection and the inferred root, not authored as a second
+// OperationEffect taxonomy.
+type EffectDependencyFact {
+  at: Node


BLOCKING: EffectDependencyFact stores at beside dependency.source, so the substrate can represent a fact whose location disagrees with its dependency edge, violating P2 illegal states unrepresentable/single authority.

briansrls · 2026-05-21T04:18:26Z

+  | UnknownOwnership
+
+type OwnershipDependencyFact {
+  owner: Node


BLOCKING: OwnershipDependencyFact duplicates owner and subject beside dependency.source and dependency.dependent, so ownership facts can drift from the edge they claim to project from.

briansrls · 2026-05-21T04:18:26Z

+  | UnknownCoupling
+
+type ParallelismDependencyFact {
+  source: Node


BLOCKING: ParallelismDependencyFact duplicates source and dependent beside dependency.source and dependency.dependent, preserving the same illegal split-authority state in the parallelism carrier.

briansrls · 2026-05-21T04:18:26Z

+// effect projection and algebraic laws. A dependency edge alone never
+// proves the positive algebraic law; it only routes to the witness need.
+type IdempotencyVerdict
+  = AlgebraicIdempotenceProven { law: Witness<InferredFacts> }


BLOCKING: AlgebraicIdempotenceProven accepts Witness, so any inference bundle can inhabit a positive idempotence proof instead of a typed algebra-law witness, violating M9/API-level enforcement.

briansrls · 2026-05-21T04:18:26Z

+  }
+}
+
+fn ownership_mode_eq(a: OwnershipMode, b: OwnershipMode) -> Bool {


BLOCKING: ownership_mode_eq hand-rolls equality over the new OwnershipMode coproduct even though structural identity is derived and the helper has no Practice 10 disposition/receipt.

…er (B3 single-authority) Addresses codex REQUEST_CHANGES on PR #3506 (sha 7eac547, 2026-05-21 09:37:16Z): the previous `EffectClassification` enum mapped `DependencyKind` to effect kinds (EffectDependsOn ⇒ WriteEffect, etc.), which re-authored effect kinds from dependency kinds — a second authority contradicting B3 ("the type signature is the effect authority"). Fixing the parallel-payload defect by introducing a parallel-kind-authority defect would have been the same Practice 5 / INVARIANTS P2 trap in a different shape. Fix: `EffectClassification` is now an empty signature-deferred marker (`type EffectClassification {}`). The per-edge row carries the typed dependency reference plus this marker; the actual effect kind is read at use-sites from `tree.facts.lookup(dependency.source)`, never derived from `DependencyKind`. The dependency kind has no role in effect classification — single authority preserved. Decoding `InferredFacts` into a closed effect-kind carrier (the full fix for #3468's collapse-of-signature/resource/algebra BLOCKING) remains the follow-up lane; this PR no longer pretends to settle it. Claim updated: effect_depends_on.dag expects `EffectClassification {}` for the EffectDependsOn case (every dependency kind would produce the same row — the lens is intentionally signature-deferred). Acceptance: v2-compiler compile src/v4 → 120 modules / 124 files / 0 diagnostics. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

… Phase 1 proposal: (1) ClassifiedDependencyView<C> in v4.std.dependency; (2) migrate all 5 T-13 lenses + claims; (3) split-contract via composition (rollup_unused ∘ use_classification_fact); (4) test-claim template; (5) Practice 11 (#3506) * WIP: T-13 Phase 2 family-wide migration ratchet — implement crisp-boar-896 Ph * T-13 family-wide migration: ClassifiedDependencyView<C> substrate + 5 lenses + claims + test-claim template + Practice 11 sub-rule Phase 1 implementation per crisp-boar-896 design (operator-ratified 2026-05-21 via PM smart-lynx-142). Dissolves the recurring parallel-payload-vs-typed-reference anti-pattern (5th instance) on the T-13 lens family. Substrate (v4.std.dependency): - ClassifiedDependencyView<C> { dependency: DependencyView; classification: C } is now the one parametric T-13 lens row. Endpoints live on the inner DependencyView (single authority); per-lens C is the projection. - classified_source/dependent/usage_site accessors + classified_dependency_view_eq (parametric over a classification-eq comparator). Lens family (one mechanism, N projections): - v4.lens.parallelism — ClassifiedDependencyView<ParallelismRelation> - v4.lens.effect — ClassifiedDependencyView<EffectClassification> - v4.lens.ownership — ClassifiedDependencyView<OwnershipMode> - v4.lens.idempotency — ClassifiedDependencyView<IdempotencyVerdict> - v4.lens.unused_parameters — split-contract: PROJECTION: Witness<UseClassificationFact> (T-13 family shape) BEHAVIORAL: Witness<UnusedParametersFact> (registry roll-up aligned with LensIdV0::UnusedParameters / v3 query) Behavioral = composition: unused_parameters_fact = rollup_unused ∘ use_classification_fact (single mechanism, no parallel authority). UnusedParameterFact = { declaration, declaration_facts }. Endpoint duplication removed from every row: no more source/dependent/at/ owner/subject/use_site/declaration parallel-payload fields on lens rows; endpoints read through dependency.* accessors. Per-node InferredFacts no longer copied onto rows; read at use-sites via tree.facts.lookup(...) (Practice 3 — facts flow forward by reference). Test-claim template (Phase 1 step 4): - src/v4/test/claim/lens_common/infer_fixture.dag — claim_atom_node, claim_inferred_facts, claim_inferred_facts_map, claim_inferred_tree. All 6 T-13 claim files migrated to this fixture: substrate shape changes (e.g. InferredFacts field evolution) need a single edit, not N (cost-of-change = 1). Claim updates (all 5 lenses + new roll-up claim): - parallelism / effect / ownership / idempotency: PROJECTION on the new ClassifiedDependencyView<C> shape via the shared fixture. - unused_parameters/binds_to_edge.dag: PROJECTION — BindsTo ⇒ IsUseOfDeclaration on UseClassificationFact. - unused_parameters/non_use_edges.dag: PROJECTION partition — Contains/ DataDependsOn/GeneratedFrom ⇒ {IsStructuralComposition / IsNonUseDependency / RequiresResolutionWitness}. - unused_parameters/rollup_unused_declaration.dag (NEW): BEHAVIORAL — declaration with only non-USE edges rolls up into UnusedParametersFact.unused. Practice 11 sub-rule: - docs/modeling-discipline.md — new "Parallel-payload vs typed-reference" section under Practice 11, with worked instance + mechanical test + family-wide-ratchet disposition + 5-instance recurring table (memory- grounded). Operator-direct standing 2026-05-19, ratified for this ratchet 2026-05-21. Acceptance criteria run locally: target/debug/v2-compiler compile --source-root src/v4 \ --output-dir /tmp/gunbc-v4-final → 120 modules / 124 files emitted / 0 diagnostics python3 scripts/strict_deprose_dag.py --check → OK rg 'WholeFile|Whole[A-Z][A-Za-z]*' over the migrated files → no matches No external consumers of the old *DependencyFact types (grep confirmed pre-migration); only lens files + claim files used them. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: T-13 Phase 2 family-wide migration ratchet — implement crisp-boar-896 Ph * unused_parameters: refresh stale rollup_unused comment to match Contains-dependent candidate scope Addresses cursor APPROVE exploratory observation on PR #3506 at src/v4/lens/unused_parameters.dag:107-109: the roll-up scope comment still described the prior `source == N` candidate identification. Refresh to match the corrected behavior (Contains-dependent candidates under P6). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: T-13 Phase 2 family-wide migration ratchet — implement crisp-boar-896 Ph * effect lens: collapse EffectClassification to signature-deferred marker (B3 single-authority) Addresses codex REQUEST_CHANGES on PR #3506 (sha 7eac547, 2026-05-21 09:37:16Z): the previous `EffectClassification` enum mapped `DependencyKind` to effect kinds (EffectDependsOn ⇒ WriteEffect, etc.), which re-authored effect kinds from dependency kinds — a second authority contradicting B3 ("the type signature is the effect authority"). Fixing the parallel-payload defect by introducing a parallel-kind-authority defect would have been the same Practice 5 / INVARIANTS P2 trap in a different shape. Fix: `EffectClassification` is now an empty signature-deferred marker (`type EffectClassification {}`). The per-edge row carries the typed dependency reference plus this marker; the actual effect kind is read at use-sites from `tree.facts.lookup(dependency.source)`, never derived from `DependencyKind`. The dependency kind has no role in effect classification — single authority preserved. Decoding `InferredFacts` into a closed effect-kind carrier (the full fix for #3468's collapse-of-signature/resource/algebra BLOCKING) remains the follow-up lane; this PR no longer pretends to settle it. Claim updated: effect_depends_on.dag expects `EffectClassification {}` for the EffectDependsOn case (every dependency kind would produce the same row — the lens is intentionally signature-deferred). Acceptance: v2-compiler compile src/v4 → 120 modules / 124 files / 0 diagnostics. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: T-13 Phase 2 family-wide migration ratchet — implement crisp-boar-896 Ph * UnusedParameterFact: drop declaration_facts — facts flow by reference (Practice 3) Addresses BLOCKING inline review at src/v4/lens/unused_parameters.dag:57 (briansrls 2026-05-21T11:19:28Z): UnusedParameterFact carried declaration_facts beside declaration, duplicating tree.facts.lookup(declaration) and reintroducing the same Practice 3 / P2 facts-flow-by-copy defect this PR is meant to dissolve. The Phase-1 design proposed declaration_facts on this row, but the operator-direct sharpening is that Practice 3 reference-not-copy applies *strictly* — even on the registry-aligned behavioral row. declaration_facts == tree.facts.lookup(declaration) is a derivable lookup, not a separately-authoritative fact. Fix: - UnusedParameterFact = { declaration: Node } only. - unused_parameter_for_declaration drops the tree parameter. - unused_parameter_fact_eq compares declaration only. - rollup_unused drops the unused InferredTree parameter — matches the Phase-1 composition shape exactly: unused_parameters_fact(tree, deps) = rollup_unused(use_classification_fact(tree, deps)) - InferredFacts import dropped (unused). - Rollup claim updated: expected entry is just { declaration: rollup_parameter }. Acceptance: v2-compiler compile src/v4 → 120 modules / 124 files / 0 diagnostics. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * rollup_unused: fail-closed on RequiresResolutionWitness — unresolved-use evidence blocks the unused verdict Addresses BLOCKING inline review at src/v4/lens/unused_parameters.dag:170 (briansrls 2026-05-21T11:19:28Z): rollup_unused recognized only IsUseOfDeclaration as "use evidence", so a RequiresResolutionWitness edge with source==candidate (the fail-closed slot for edge kinds the lens couldn't classify — GeneratedFrom / VerifiedBy / PromotedBy / BootstrapDependsOn) was treated as "no use", letting unresolved-use evidence silently become an UnusedParameterFact. Fail-OPEN defect on a fail-closed-by-design slot. Fix: rename and broaden the use predicate. declaration_has_use → declaration_has_use_or_unresolved. The blocker set is {IsUseOfDeclaration, RequiresResolutionWitness}; an edge with source==candidate and either classification blocks the unused verdict. IsStructuralComposition and IsNonUseDependency remain positive non-use evidence and do not block. The fail-closed slot now behaves fail-closed at every consumer of the projection. Acceptance: v2-compiler compile src/v4 → 120 modules / 124 files / 0 diagnostics. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * unused_parameters predicates: Practice 10 dispositions — dissolve one, tag the other 🟡 Addresses BLOCKING inline review at src/v4/lens/unused_parameters.dag:115 (briansrls 2026-05-21T11:19:28Z): use_relation_is_use (now renamed use_relation_blocks_unused) and classification_is_structural_composition were new Bool predicates over the UseRelation coproduct without predicate-dissolution disposition tags (Practice 10 / P5). Two-step fix: 1. **Dissolve** classification_is_structural_composition into the existing `use_relation_eq` — it was just single-variant equality: classification_is_structural_composition(r) ⇒ use_relation_eq(r, IsStructuralComposition) The predicate is removed; `rollup_unused` calls `use_relation_eq` directly. One fewer hand-rolled predicate over the coproduct. 2. **Tag 🟡** use_relation_blocks_unused (the genuinely-needed 2-class partition predicate). Disposition: dissolves on arrival of a substrate variant-tag partition primitive ("partition variants of <Coproduct> by <classifier>" parametric form). Until that lands the match is hand-rolled with the dissolution-on-arrival obligation tracked at the predicate. Acceptance: v2-compiler compile src/v4 → 120 modules / 124 files / 0 diagnostics; strict_deprose_dag --check → OK. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

The plain [FILES FILLED] marker overstated T-13's state. Two sub-lanes remain staged on T-9: effect.dag's EffectClassification is a signature-deferred empty slot (closing the effect-kind carrier is a #3468 BLOCKING follow-up), and structural_resolution.dag's status_for_binding_facts is staged until the T-9 resolve→infer witness bridge lands. Update the table entry and Status line to reflect this. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

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>

- 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>

… effect always return Holds (#3760) * WIP: Fix fail-open Witness lenses: ownership / idempotency / parallelism / ef * fix(v4): collapse tautological effect_dependency_unresolved 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> * fix(v4): T-13 witness lenses propagate upstream diagnostics (P2/P3) - 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> * WIP: Fix fail-open Witness lenses: ownership / idempotency / parallelism / ef * WIP: Fix fail-open Witness lenses: ownership / idempotency / parallelism / ef * WIP: Fix fail-open Witness lenses: ownership / idempotency / parallelism / ef * fix(v4): align Optional<Diagnostic> folds with kernel Some/None 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> * WIP: Fix fail-open Witness lenses: ownership / idempotency / parallelism / ef * chore(v4): document optional_diagnostic_* in collection.dag Owns Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Fix fail-open Witness lenses: ownership / idempotency / parallelism / ef * fix(v4): import Symbol for T-13 lens diagnostic anchor data 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 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> * WIP: Fix fail-open Witness lenses: ownership / idempotency / parallelism / ef * fix(v4): generic Optional helpers with Practice 10 tags (claude RC) 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> * fix(v4): drop optional_is_present; single optional_present_witness match 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> --------- Co-authored-by: Cursor <cursoragent@cursor.com>

…ner contract (#4301) * RR-I Class 1 worksheet — dependency-lens closure posture + corpus-runner contract I.1: ratify single-ClassifiedDependencyView<C> closure contract for the four dependency-runtime lens families (parallelism/effect/ownership/idempotency) landed post-#4264/#4292 — honest unresolved arms, no parallel roster fields, no second classification authority. NON-GOALS: Complexity/Cost/TableDecisionTree registry migration; bulk #3468 scaffold dissolution. I.1.1 (adhoc-8b1709c7-7c0) executes UnknownCoupling collapse against §2 contract / §4 R1–R4. I.3 (design-only): corpus-runner contract for testclaim_corpus_runner.dag two unsupported subject families (ci_pipeline, non_runtime_value) — root-caused as domain mismatch vs run_test_claim's monomorphic (Node, RuntimeValue), promoted only via projection-into-(Node,RuntimeValue) or an escalated parametric-evaluator L2.5 PR; never a per-family run_test_claim fork. §5.0.2 CI-needs predicate gates eval_parallel (p95>15m OR shadow>5m OR queue>3d); no runtime lands here. Mirrors RR-A #4296 format; §8 READY-FOR-WORKER-DISPATCH. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * RR-I review fixes (#4301): live-tree accuracy — 5-row roster + IdempotencyVerdict variants codex REQUEST_CHANGES: two landed-tree survey errors. - manual_corpus_roster is FIVE rows (header :3 "five rows"; 5 entries :25), not 4. Corrected all "4-row wedge" cites (carried from RR-A #4296) to 5-row. - IdempotencyVerdict has only AlgebraicIdempotenceProven { law } | RequiresAlgebraWitness (idempotency.dag:42). The Holds/Violates { diagnostic } pair lives on the inner law Witness, not on IdempotencyVerdict — corrected §2 table. Docs-only; no substrate touched. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: RR-I worksheet (Class 1) — I.1 T-13 lens closure + I.3 corpus runner con --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…esses. Land operator-ratified design doc and activate v2.std.determinism with a closed primitive roster (incl. #5913 construction rows), left-biased determinism_compose, and green determinism_contract_test claims — FLAG 1 locked to bundle into #3468. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls added 3 commits May 20, 2026 21:30

WIP: T-13 — lens family expansion: lens/parallelism.dag + lens/effect…

2cc01cd

….dag + l

WIP: T-13 — lens family expansion: lens/parallelism.dag + lens/effect…

799190a

….dag + l

WIP: T-13 — lens family expansion: lens/parallelism.dag + lens/effect…

46e61fb

….dag + l

briansrls marked this pull request as ready for review May 21, 2026 01:36

briansrls added 4 commits May 20, 2026 21:40

WIP: T-13 — lens family expansion: lens/parallelism.dag + lens/effect…

f3ca9ae

….dag + l

Add T-13 lens claim predicates

3bfa3c8

Materialize T-13 lens claim receipts

c7fffd8

WIP: T-13 — lens family expansion: lens/parallelism.dag + lens/effect…

1b1f691

….dag + l

briansrls commented May 21, 2026

View reviewed changes

Comment thread src/v4/lens/effect.dag

Comment thread src/v4/test/claim/lens_effect/effect_depends_on.dag

Comment thread src/v4/lens/effect.dag Outdated

Comment thread src/v4/lens/idempotency.dag Outdated

Comment thread src/v4/lens/effect.dag Outdated

briansrls added 4 commits May 20, 2026 22:13

WIP: T-13 — lens family expansion: lens/parallelism.dag + lens/effect…

16ecf88

….dag + l

Make parallelism dependency coupling explicit

0daecbc

WIP: T-13 — lens family expansion: lens/parallelism.dag + lens/effect…

ff87fa0

….dag + l

Make idempotency dependency handling explicit

993c8ff

briansrls commented May 21, 2026

View reviewed changes

Comment thread src/v4/lens/parallelism.dag Outdated

Comment thread src/v4/lens/idempotency.dag Outdated

Comment thread src/v4/lens/ownership.dag Outdated

WIP: T-13 — lens family expansion: lens/parallelism.dag + lens/effect…

eefc5a7

….dag + l

briansrls merged commit 48bc491 into main May 21, 2026
7 checks passed

briansrls commented May 21, 2026

View reviewed changes

briansrls mentioned this pull request May 26, 2026

T-13 closeout: mark five lens substrates as FILES FILLED in TASKS.md #3695

Closed

briansrls mentioned this pull request May 27, 2026

Fix fail-open Witness lenses: ownership / idempotency / parallelism / effect always return Holds #3760

Merged

3 tasks

This was referenced May 29, 2026

PR-1: Add Deterministic effect arm to substrate (foundation for determinism-as-effect lane) #3922

Merged

PR-2: src/v4/lens/determinism.dag structural verifier (HashMap/now/random/env forbiddens + recursive effect-leak enforcement) #3927

Closed

briansrls deleted the session/sleek-fox-588 branch June 1, 2026 18:43

briansrls mentioned this pull request Jun 2, 2026

RR-I Class 1 worksheet — dependency-lens closure posture + corpus-runner contract #4301

Merged

gunbai-bot Bot mentioned this pull request Jun 29, 2026

DRAFT [design-for-sign] §5 determinism mechanism design #5937

Merged

1 of 3 tasks

gunbai-bot Bot mentioned this pull request Jun 29, 2026

§5 determinism mechanism P1: core axis, roster, compose algebra, witnesses #5941

Closed

2 of 4 tasks

Navigation Menu

Repository navigation

briansrls commented May 21, 2026 •

edited

Loading

Uh oh!

briansrls left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

briansrls left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

briansrls left a comment

Uh oh!

briansrls May 21, 2026

Uh oh!

briansrls May 21, 2026

Uh oh!

briansrls May 21, 2026

Uh oh!

briansrls May 21, 2026

Uh oh!

briansrls May 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

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

Uh oh!

Summary

Test plan

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls May 21, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 21, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 21, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 21, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 21, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented May 21, 2026 •

edited

Loading