Skip to content

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

Merged
briansrls merged 3 commits into
mainfrom
session/proud-hawk-525
May 30, 2026
Merged

briansrls merged 3 commits into
mainfrom
session/proud-hawk-525

Conversation

@briansrls

@briansrls briansrls commented May 29, 2026 •

Copy link
Copy Markdown
Contributor

Summary

PR-1 of the determinism-as-modeled-effect lane (operator-directive 2026-05-29: make determinism a typed substrate property, not a 5x-matrix test).

Adds src/v4/std/determinism.dag — a closed coproduct carrier classifying whether a function's outputs are a deterministic relation on its inputs.

type NonDetSource     = HashIteration | TimeRead | RandomRead | EnvRead
type DeterminismClass = Deterministic | NonDeterministic { source: NonDetSource }
type DeterminismFact  { signature: Symbol, classification: DeterminismClass }

Why a new file (DFS — MODELING M9 / INVARIANTS P1)

  • DAG-ancestor check: no v4 parent. witness.dag is the generic Witness<C> proof carrier; effects.dag is the orthogonal idempotency partition (IsIdempotent / IsBreaking describe what an effect does to the world; determinism describes whether the implementation produces a single-valued relation on inputs — different axes, per PM vivid-wolf-712).
  • Coproduct-vs-coordinate check: at the determinism axis the variants are alternatives (a fn IS or IS NOT deterministic) — sum type correct. At the cross-axis level idempotency × determinism are coordinates, which is exactly why this carrier is a sibling file rather than a third arm of EffectShape.
  • Canonical-name rule: determinism / referential transparency is a recognized CS concept — earns its own std/ file with Wikipedia anchors.
  • v2 precedent: dsl/std/behavioral.dag already declares type Determinism = Deterministic | NonDeterministic | EventuallyConsistent attached to OperationBehavior. The v4 form refines NonDeterministic with a closed NonDetSource so the PR-2 structural verifier has named sources to forbid.
  • Pattern match: mirrors src/v4/extdeps/coordination.dag (CoordinationEffectKind + obligation lookup) — closed effect-kind carrier in its own file.

Scope discipline (tight diff)

Per manager brief: PR-1 ships only the carrier substrate. Out of scope (sibling PRs):

  • PR-2: src/v4/lens/determinism.dag structural verifier (HashMap/HashSet, now(), random(), env forbidden in Deterministic fns; recursive effect-leak enforcement).
  • PR-3: ordered/unordered List<K,_> refinement in src/v4/std/refinement.dag.
  • PR-4: annotate emit_* / infer_* / translate_* in src/v4/compiler/.
  • PR-5: retire DB-8 5x emit matrix.

UnboundedRecursion was considered for NonDetSource and dropped on manager feedback: termination is a separate axis (pure recursive fns are deterministic regardless of recursion depth); leaving it in would force PR-2's lens to do termination analysis. The four sources listed match exactly the operator-specified PR-2 forbiddens.

Relationship to #3468

EffectClassification in src/v4/lens/effect.dag is a signature-deferred slot whose closure is gated by #3468. Per PM Option A, this PR ships independently — determinism is an orthogonal axis that co-evolves with #3468. Cross-reference noted in the file header.

Test plan

  • v4 whole-tree compile gate (gunbc compile --source-root src/v4) parses the new file successfully. The 24 pre-existing complexity: same-argument recursion in ci_int_offset_authority_projection_node errors in src/v4/test/claim/workflow/pipeline_rejections.dag are unrelated to this PR (same errors land on main; new carrier file has no recursion).
  • No shell / CI touches (PM relay re. shell-elimination: confirmed no-op for this PR).

🤖 Generated with Claude Code

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 0b484333 · Trigger: schedule
  • Thinking: 153s wall

BLOCKING (1)

Root Cause

  • src/v4/std/determinism.dag Substrate-review rationale was written into the carrier instead of kept as PR-review/TASKS/commit receipt → trim the file to the Practice 9 header and required carrier tags, moving rationale and sequencing out of .dag comments.

⚠️ One substrate comment-discipline issue needs fixing before this lands.

Comment thread src/v4/std/determinism.dag Outdated
// Anchor: https://en.wikipedia.org/wiki/Deterministic_algorithm
// Anchor: https://en.wikipedia.org/wiki/Referential_transparency
//
// MODELING NOTE (P1 Step 1 — DAG-ancestor): determinism is **orthogonal** to the

This comment was marked as resolved.

Trim to allowed Practice 9 classes only — file-path, terse Scope/Status,
one Anchor, one-line coproduct tags. Rationale and PR sequencing move to
PR review / commit message.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 30, 2026
…mments

Codex BLOCKING finding 2 (review 21193): the prior comments cited
`v4.std.determinism` / `NonDetSource` / `HashIteration` as authority, but the
PR-1 carrier file is not yet on origin/main (PR #3922 still open). The PR-3
substrate must stand alone — references to nonexistent files violate
INVARIANTS P1 live grounding.

Rewrite the IterationOrdering / IterationClassifier doc comments to be
self-contained: describe orderedness as a type-level carrier property and
unordered-iteration as a hash-iteration-shaped non-determinism source without
naming any cross-file type that hasn't landed. The structural distinction and
the API surface are unchanged.

Also re-frames codex finding 1 (the IterationClassifier<B> classifier-function
parameter): clarifies that the classifier mirrors the existing `Validation<B>` /
`refine` caller-discipline boundary already accepted in this file, with true
structural enforcement (making forgery unrepresentable) deferred to the lens /
compiler retrofit layers where carrier-keyed witness lookup is in scope.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

CI investigation: the failing step is T-22 TestClaim corpus structural bridge — manual .dag corpus in run 26668825780, exit code 143 (SIGTERM from timeout --preserve-status $V4_TESTCLAIM_TIMEOUT_SECS, CI default 240s in scripts/v4-testclaim-corpus-gate.sh). The step times out during gunbc compile --source-root src/v4 --target rust.

This is pre-existing on main, not caused by this PR:

The new file in this PR is a 30-line substrate carrier with no consumers in the corpus — it cannot meaningfully change v4 corpus compile time. Out-of-scope to extend the T-22 timeout from a PR-1 substrate PR.

Suggest re-run; if it persists, the timeout knob (V4_TESTCLAIM_TIMEOUT_SECS) likely needs raising on the infra/CI lane (clever-cat-115 / shell-elimination owner, or T-38 testgen lane).

— sent from proud-hawk-525

@briansrls
briansrls merged commit e332fc2 into main May 30, 2026
5 of 6 checks passed

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 5c82f4c7 · Trigger: schedule
  • Thinking: 145s wall

BLOCKING (1)

Root Cause

  • src/v4/std/determinism.dag DeterminismClass treats the verdict as authored substrate state instead of a structural projection from nondeterminism sources → replace it with one authoritative source-set carrier consumed by downstream determinism queries.

⚠️ One substrate modeling issue needs correction before this carrier should land.



// 🟢 coproduct dissolution
type DeterminismClass

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: NonDeterministic carries only one source, so an operation with multiple nondeterminism causes must either drop facts or duplicate rows; model the canonical source collection and derive the deterministic verdict from emptiness instead (INVARIANTS P1/P2, modeling-discipline Practices 2/4).

briansrls added a commit that referenced this pull request May 30, 2026
…NamingTheLeak diagnostic on unordered iteration in Deterministic context) (#3928)

* WIP: PR-3: ordered/unordered collection refinement in std/refinement.dag (Nam

* v4(determinism PR-3): IterationOrdering refinement + naming_the_leak diagnostic in std/refinement.dag

PR-3 of the determinism-as-modeled-effect lane (operator-directive 2026-05-29).
Companion to PR-1's src/v4/std/determinism.dag carrier (NonDetSource/DeterminismClass/DeterminismFact)
and PR-2's structural lens; this PR seeds the *refinement-level* distinction so an unordered
collection iterated inside a Deterministic context fails closed with a named diagnostic.

Adds to src/v4/std/refinement.dag:
- type IterationOrdering = StructurallyOrdered | StructurallyUnordered
  Closed-coproduct structural marker. Orderedness is a type-level property of the carrier
  (List/BTreeMap/BTreeSet ordered; HashSet/HashMap/FiniteSet leak insertion-order),
  so the existing value-predicate Validation<B>.admits shape doesn't fit — a marker is
  the substrate-canonical structural distinction (mirrors PR-1 NonDetSource shape).
  Unordered arm intentionally carries no payload: today HashIteration is the only
  iteration-shaped NonDetSource and typing the field over the full coproduct would
  admit nonsensical constructions like StructurallyUnordered { source: TimeRead }.
  If a second iteration-leak source emerges, carve a NonDetIterationSource sub-coproduct
  rather than widening this arm.
- data naming_the_leak: Symbol
- fn refine_ordered_iteration<B>(base, ordering, at) -> Outcome<Refined<B>>
  Accepted on StructurallyOrdered; Rejected with naming_the_leak diagnostic on
  StructurallyUnordered. Diagnostic shape matches the existing refine() constructor
  (Unavailable { reason: UserInputBoundary }).

Scope discipline: substrate only. PR-2 (vivid-raven-826) owns the structural lens that
forbids HashMap/HashSet imports; PR-4 retrofits compiler stages; PR-5 retires DB-8.
Does NOT extend EffectShape in std/effects.dag (orthogonal axis per operator).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4(determinism PR-3): bind IterationOrdering to carrier via IterationClassifier<B>

Addresses BLOCKING reviews from briansrls and codex on the prior commit: the
caller-supplied `ordering: IterationOrdering` parameter was a parallel fact
beside `base`, lettting a caller pass `StructurallyOrdered` for an unordered
carrier and bypass the `naming_the_leak` diagnostic (INVARIANTS P2 violation —
ordering wasn't *derived from* the carrier).

Switch to a B-parametric classifier mirroring the existing `Validation<B>` /
`refine` pattern in the same file:

  type IterationClassifier<B> { classify: fn(B) -> IterationOrdering }
  fn refine_ordered_iteration<B>(base: B, by: IterationClassifier<B>, at: Locus)
      -> Outcome<Refined<B>>

The refinement now derives the classification from `base` via the discharged
classifier; per-carrier classifiers (e.g. `IterationClassifier<HashMap<K,V>>`)
are authored at the layer that owns each carrier's identity (PR-2 lens /
PR-4 compiler / std/collection.dag) and always return the structurally-correct
arm — no caller choice. Forging the classifier is the same caller-discipline
boundary as forging `Validation<B>.admits` to always return `true`.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4(determinism PR-3): drop forward-references to PR-1 carrier from comments

Codex BLOCKING finding 2 (review 21193): the prior comments cited
`v4.std.determinism` / `NonDetSource` / `HashIteration` as authority, but the
PR-1 carrier file is not yet on origin/main (PR #3922 still open). The PR-3
substrate must stand alone — references to nonexistent files violate
INVARIANTS P1 live grounding.

Rewrite the IterationOrdering / IterationClassifier doc comments to be
self-contained: describe orderedness as a type-level carrier property and
unordered-iteration as a hash-iteration-shaped non-determinism source without
naming any cross-file type that hasn't landed. The structural distinction and
the API surface are unchanged.

Also re-frames codex finding 1 (the IterationClassifier<B> classifier-function
parameter): clarifies that the classifier mirrors the existing `Validation<B>` /
`refine` caller-discipline boundary already accepted in this file, with true
structural enforcement (making forgery unrepresentable) deferred to the lens /
compiler retrofit layers where carrier-keyed witness lookup is in scope.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4(determinism PR-3): correct FiniteSet classification; drop PR-1 ref from header

Cursor BLOCKING (review 21214): the IterationOrdering doc comment listed
`FiniteSet` alongside `HashSet`/`HashMap` as StructurallyUnordered, but
`src/v4/std/collection.dag:107-109` defines `FiniteSet { head: T, tail: List<T> }`
— a cons-list shape whose iteration order is fixed by structure, not hash
buckets. Conflicts with the same block's "unordered = hash-iteration-shaped"
terminal rationale and would mis-bind downstream IterationClassifier authors.

Replace the prescriptive carrier list with structural-shape descriptions
("cons-list shapes ... ordered; hash-bucket carriers ... unordered") that
match v4.std.collection's actual carriers without enumerating them.

Also drops the lingering PR-1 forward-reference from the Status line on
refinement.dag:3 (claude review 21213 soft observation) — header now describes
PR-3's own additions without naming sibling-PR files that aren't on main.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: PR-3: ordered/unordered collection refinement in std/refinement.dag (Nam

* v4(determinism PR-3): demote to 🟡 gated; collapse prose-as-authority; add behavior receipts

Addresses openai-pro REQUEST_CHANGES (review 21243) findings:

1. LAYER MODEL / INVARIANTS P2 / Practice 6 / TRACKED-vs-UNTRACKED DEBT:
   IterationOrdering and IterationClassifier<B> were marked 🟢 TERMINAL while
   the diff itself named a richer dissolution source ("carrier-keyed witness
   lookup"). Under the dissolution rules, a namable richer source disqualifies
   TERMINAL — convert to 🟡 gated with feature:iteration-ordering-carrier-keyed-
   witness-lookup, bound dissolve-on-arrival path naming the non-forgeable
   `Witness<StructurallyOrdered, B>` target. Forgery is acknowledged as
   representable today and gated, not silently disclaimed as terminal closure.

2. CODING.md Practice 9 / prose-as-authority:
   The ~14-line justification block at refinement.dag:286-302 was a parallel
   authority for the invariant the type cannot enforce. Collapsed to a single
   🟡 gate annotation that states the dissolution target tersely; rationale
   moves to the PR review thread per Practice 9.

3. TESTING.md / behavior receipt:
   Add src/v4/test/claim/manual/refinement_ordered_iteration.dag with two
   TestClaim rows: (a) ordered classifier ⇒ Accepted; (b) unordered classifier
   ⇒ Rejected with reason == naming_the_leak. One claim per test; no
   HashMap-iteration-order assertions.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4(determinism PR-3): split disposition (🟢 on coproduct, 🟡 on classifier); add bind T-25-tail

Cursor REQUEST_CHANGES (review 21259):

1. Disposition conflation: IterationOrdering (the ordered/unordered coproduct) is
   itself the irreducible substrate fact — the dissolution target
   (carrier-keyed `Witness<StructurallyOrdered, B>`) replaces `IterationClassifier<B>`
   (the discharger), not the sum. Split the tag accordingly: IterationOrdering is
   🟢 coproduct dissolution TERMINAL; IterationClassifier<B> carries the 🟡 gate.

2. Missing `bind` lane: the prior 🟡 annotation lacked the `bind T-*` owner-lane
   that sibling gates in this file use (refinement.dag:107, :114 — `bind T-25-tail`).
   Add `bind T-25-tail` matching the opaque-carrier sibling gates — same T-25 tail
   lane will land the substrate witness-lookup mechanism.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls
briansrls deleted the session/proud-hawk-525 branch June 1, 2026 18:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant