feat(core): PR 4 of 8 — IncrementalAuto capability-aware dispatcher (re-land of #4564)#4567
Conversation
Adds `Circuit.IncrementalAuto<'K>(q, input)`, a dispatcher that picks
the right incrementalization based on the algebra capability tag on
`q`'s resulting operator:
- `IsLinear = true` → `Q^Δ = Q` (deltas pass through unchanged)
- `IsSink = true` → throws (sinks are terminal, can't incrementalize)
- otherwise → fall back to `D ∘ Q ∘ I` via existing
`IncrementalizeZSet`
This makes the algebra-capability system load-bearing on the
incremental-rewrite side — the DBSP paper's central claim "linear ops
incrementalize trivially; bilinear ops use the three-term form; rest
fall back to D∘Q∘I" finally has a dispatcher that mechanizes the first
and third clauses. (The bilinear case has its own richer signature in
`IncrementalJoin`; a future `IncrementalAutoJoin` dispatcher for
bilinear ops can layer on top of that.)
The dispatcher probes `q` by applying to the input directly, then
inspects `Op.IsLinear` / `Op.IsSink` (from PR 1, #4558). The probe
side-effect registers the operator in the circuit; for the
linear-passthrough path this IS the correct wiring. For the
non-linear fallback path, the probed op is orphan (no consumers) — a
small per-tick cost; pruning unreachable operators at `Circuit.Build()`
is a future improvement.
- `IncrementalAuto with linear Map produces same delta stream as
direct Q` — operational correctness check over 4 ticks (insert,
insert, retract, empty)
- `IncrementalAuto with non-linear Distinct falls back to D-Q-I` —
output matches `IncrementalizeZSet` over a 6-tick scenario with
duplicates and retractions
- `IncrementalAuto throws when the operator is a sink` — error
message contains "IncrementalAuto", "sink", and the operator name
- `IncrementalAuto with linear op adds exactly one operator` —
structural check that the fast path was taken (just the Map; no I
or D)
- `IncrementalAuto with non-linear op adds four operators` —
structural check that fallback registered probe + I + new Q + D
(probe is the documented orphan)
No regressions in broader Circuit tests. Build clean.
PR 4 depends on PR 1 (#4558) for `Op.IsLinear` and `Op.IsSink`.
Stacked on `feat/op-capability-tags-2026-05-21`; targets `main`.
PR 5's FusionEngine will use the same `IsLinear`/`IsBilinear` reads
to compose capability tags through fusion. PR 8's standing-query
codegen can generate the `IncrementalAuto` decision tree at compile
time rather than at runtime probe, eliminating the orphan-operator
cost entirely.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e8f193d078
ℹ️ 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".
There was a problem hiding this comment.
Pull request overview
Adds a capability-aware incrementalization dispatcher (Circuit.IncrementalAuto<'K>) to select a cheaper incrementalization strategy at circuit-construction time based on the produced operator’s algebra capability tags (Op.IsLinear / Op.IsSink), plus a focused test suite to validate linear, non-linear fallback, and sink behavior.
Changes:
- Introduces
Circuit.IncrementalAuto<'K>insrc/Core/Incremental.fswith linear fast-path, sink rejection, andD ∘ Q ∘ Ifallback. - Adds
IncrementalAutounit tests covering correctness (linear + fallback) and sink rejection, plus structural operator-count assertions. - Registers the new test file in
Tests.FSharp.fsproj.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 4 comments.
| File | Description |
|---|---|
src/Core/Incremental.fs |
Adds IncrementalAuto dispatcher using Op.IsLinear/Op.IsSink to choose incrementalization strategy. |
tests/Tests.FSharp/Circuit/IncrementalAuto.Tests.fs |
New tests validating semantic equivalence vs reference forms and structural operator-count expectations. |
tests/Tests.FSharp/Tests.FSharp.fsproj |
Includes the new IncrementalAuto test file in compilation order. |
…ed; transitive coverage via cross-verify; unblocks 4 stale PRs (#4570) * fix(stryker): retarget from F# Core.fsproj to C# Core.CSharp.ZetaId.csproj — Stryker.NET 4.x F# unsupported (NotSupportedException Language not supported Fsharp); C# mutation coverage transitively constrains F# substrate via cross-verify harness (PRs #4517 + #4522 + #4548 byte-identical hex agreement); F# coverage remains rich via FsCheck + TLA+ + Z3 + Lean + Alloy + CodeQL; unblocks 4 stale PRs (#4563/#4567/#4568/#4569 BLOCKED on pre-existing F# Stryker bug) * fix(stryker-pr-4570): expand path filter to include src/Core/** (Tests.CSharp.csproj transitive F# reference per Codex P2) + tests/cross-verification/zeta-id/** (CrossVerifyTests reads vectors.yaml per Copilot P1)
|
Coordination signal from Otto-CLI: Stryker workflow blocker: I just shipped PR #4571 (iteration-2 retarget). #4570's iteration-1 landed with 0%-kill-rate target ( Remaining unresolved review threads: these are substantive P1 findings on your LawRunner / IncrementalAuto F# substrate — they're not Stryker-blocked, they're correctness-concerned. Codex flagged |
…dead-code cleanup Addresses 5 reviewer findings on PR #4567: 1. **Codex P1** (Incremental.fs IncrementalAuto): probe `q.Invoke input` runs *before* dispatch decides path, so side-effecting builders (e.g. `AdvancedExtensions.Inspect`) execute unexpected work even on sink/fallback paths. Sink case throws *after* registering the probe op, leaving an orphan sink in the circuit if the caller catches + continues. **Fix**: prominent⚠️ side-effect warning section in docstring naming both implications; sink-throw error message also calls out the orphan-sink left behind. Architectural fix (non-registering probe path) is non-trivial and deferred — acknowledged in the new "future work" line. The docstring now makes the side-effect explicit so callers can avoid the failure mode (use non-side-effecting `q`; don't catch+continue on a sink-rejection). 2. **Copilot** (IncrementalAuto.Tests.fs:39): `feedAndStep` helper was dead code (left after refactoring out the test that used it). **Fix**: removed. 3. **Copilot** (IncrementalAuto.Tests.fs:176): test name said "adds three operators" but assertion + comment expected 4. **Fix**: renamed to "adds four operators (probe-orphan + Integrate + new Q + Differentiate)" matching the assertion. 4. **Copilot** (IncrementalAuto.Tests.fs:142): comment block claimed "output stream is literally the probed op (same reference)" and "zero-allocation" — but the test only asserts operator-count delta, not reference identity. **Fix**: rephrase comment to match what's actually tested (dispatch path verified via operator-count delta; reference-equality assertion would need internal `Stream.Op` accessor exposed). ## Tests 5/5 IncrementalAuto tests pass after fixes. Build clean. No behavioral changes to operator dispatch — the test rename + comment edits + dead-code removal are all annotation-shape; the docstring side-effect warnings are documentation-only. The orphan-sink + probe- side-effect *behavior* is unchanged; the *visibility* of that behavior is improved per Codex's P1. ## Architectural follow-up not in scope The cleanest fix for both Codex's P1 (probe side effects) AND the sink-rejection orphan-sink issue would be a non-registering probe path — e.g., a `Circuit.PreviewOp(q, input)` that runs `q.Invoke` inside a transaction-shaped scope that rolls back registration if the dispatcher rejects. That requires changes to the `Op` / `Circuit` registration contract (today's `Register` doesn't support rollback) and is deferred to a future PR. Worth filing as a backlog row when the architectural cost vs. payoff is clearer.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8230bed78b
ℹ️ 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".
…earity, not just terminal op
Codex's second P1 finding caught a real correctness bug I missed: the
dispatcher was checking `probedOutput.Op.IsLinear`, but `probedOutput.Op`
is only the terminal operator in the chain produced by `q`. A query like
`q(s) = Map(Distinct(s))` ends on a linear Map but the *composed* query
is non-linear; the `Q^Δ = Q` rewrite produces wrong incremental results.
## Fix
Recursive chain check: walk `Inputs` back from the probed terminal op
to the original `input.Op`. If every op in the chain is linear AND we
reach `input.Op` only through linear ops, the chain is linear. Otherwise
fall back to `D ∘ Q ∘ I`. Multi-input ops (Plus, Minus, default
IsLinear=false) correctly route to the fallback path via this check.
```fsharp
let rec isLinearChainToInput (op: Op) (inputOp: Op) : bool =
if System.Object.ReferenceEquals(op, inputOp) then true
elif op.Inputs.Length = 0 then false // source op that isn't the input
elif not op.IsLinear then false
else op.Inputs |> Array.forall (fun dep -> isLinearChainToInput dep inputOp)
```
## Regression test added
`IncrementalAuto with terminal-linear-but-inner-non-linear chain falls back (Map ∘ Distinct)` —
exercises the exact failure mode Codex flagged. Builds Map(Distinct(s)),
runs IncrementalAuto, compares per-tick output to IncrementalizeZSet
(D∘Q∘I reference). The test exercises duplicate-insertion + retraction
scenarios where the broken dispatcher would produce wrong output (Map
of every delta directly, ignoring Distinct's cumulative-state clamping).
Before this fix: subject would emit `Map(delta)` directly each tick →
incorrect when delta has duplicates that Distinct clamps.
After this fix: subject falls back to D∘Q∘I → matches reference.
## Verification
6/6 IncrementalAuto tests pass (5 pre-existing + 1 new regression).
Build clean. The chain-check helper is O(N) in chain depth, called
once at dispatch time; zero per-tick cost.
## Related
Composes with the earlier fix in this PR for the other 5 review threads
(8230bed) — docstring side-effect warnings, test rename, dead-code
removal, comment rewording. This commit addresses the substantive
correctness P1 that the earlier docstring-shape fixes left unaddressed.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: df581fb623
ℹ️ 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".
| let rec isLinearChainToInput (op: Op) (inputOp: Op) : bool = | ||
| if System.Object.ReferenceEquals(op, inputOp) then true | ||
| elif op.Inputs.Length = 0 then false // source op that isn't the input | ||
| elif not op.IsLinear then false | ||
| else op.Inputs |> Array.forall (fun dep -> isLinearChainToInput dep inputOp) |
There was a problem hiding this comment.
Avoid recursive linearity walk on deep operator chains
IncrementalAuto computes linearity with a recursive DFS over Op.Inputs; for long generated pipelines (e.g., thousands of chained linear operators) this can overflow the .NET call stack during dispatch, and because there is no visited/memoized traversal it also repeats work across shared subgraphs. This turns capability detection into a construction-time crash/perf hazard on large circuits before any tick runs.
Useful? React with 👍 / 👎.
| let rec isLinearChainToInput (op: Op) (inputOp: Op) : bool = | ||
| if System.Object.ReferenceEquals(op, inputOp) then true | ||
| elif op.Inputs.Length = 0 then false // source op that isn't the input | ||
| elif not op.IsLinear then false | ||
| else op.Inputs |> Array.forall (fun dep -> isLinearChainToInput dep inputOp) |
| /// **The probe `q.Invoke input` ALWAYS runs once, regardless of | ||
| /// dispatch path.** This has two implications callers must | ||
| /// account for: | ||
| /// | ||
| /// 1. **Side-effecting builders execute**: if `q` is a factory | ||
| /// like `AdvancedExtensions.Inspect` that performs work at | ||
| /// construction time (logging, registering hooks, allocating | ||
| /// external resources), that work runs **even when the | ||
| /// dispatcher throws or falls back**. Use a non-side-effecting | ||
| /// `q` factory, or accept the probe-side-effect cost. |
| // Regression test for the bug Codex flagged: checking only the | ||
| // probed terminal op's IsLinear misses non-linear ops inside the | ||
| // chain. `q(s) = Map(Distinct(s))` ends on a linear Map but the |
…re-land of #4564) (#4567) * feat(core): IncrementalAuto capability-aware dispatcher — PR 4 of 8 Adds `Circuit.IncrementalAuto<'K>(q, input)`, a dispatcher that picks the right incrementalization based on the algebra capability tag on `q`'s resulting operator: - `IsLinear = true` → `Q^Δ = Q` (deltas pass through unchanged) - `IsSink = true` → throws (sinks are terminal, can't incrementalize) - otherwise → fall back to `D ∘ Q ∘ I` via existing `IncrementalizeZSet` This makes the algebra-capability system load-bearing on the incremental-rewrite side — the DBSP paper's central claim "linear ops incrementalize trivially; bilinear ops use the three-term form; rest fall back to D∘Q∘I" finally has a dispatcher that mechanizes the first and third clauses. (The bilinear case has its own richer signature in `IncrementalJoin`; a future `IncrementalAutoJoin` dispatcher for bilinear ops can layer on top of that.) The dispatcher probes `q` by applying to the input directly, then inspects `Op.IsLinear` / `Op.IsSink` (from PR 1, #4558). The probe side-effect registers the operator in the circuit; for the linear-passthrough path this IS the correct wiring. For the non-linear fallback path, the probed op is orphan (no consumers) — a small per-tick cost; pruning unreachable operators at `Circuit.Build()` is a future improvement. - `IncrementalAuto with linear Map produces same delta stream as direct Q` — operational correctness check over 4 ticks (insert, insert, retract, empty) - `IncrementalAuto with non-linear Distinct falls back to D-Q-I` — output matches `IncrementalizeZSet` over a 6-tick scenario with duplicates and retractions - `IncrementalAuto throws when the operator is a sink` — error message contains "IncrementalAuto", "sink", and the operator name - `IncrementalAuto with linear op adds exactly one operator` — structural check that the fast path was taken (just the Map; no I or D) - `IncrementalAuto with non-linear op adds four operators` — structural check that fallback registered probe + I + new Q + D (probe is the documented orphan) No regressions in broader Circuit tests. Build clean. PR 4 depends on PR 1 (#4558) for `Op.IsLinear` and `Op.IsSink`. Stacked on `feat/op-capability-tags-2026-05-21`; targets `main`. PR 5's FusionEngine will use the same `IsLinear`/`IsBilinear` reads to compose capability tags through fusion. PR 8's standing-query codegen can generate the `IncrementalAuto` decision tree at compile time rather than at runtime probe, eliminating the orphan-operator cost entirely. * fix(PR #4567 review threads): probe-side-effect docs + test naming + dead-code cleanup Addresses 5 reviewer findings on PR #4567: 1. **Codex P1** (Incremental.fs IncrementalAuto): probe `q.Invoke input` runs *before* dispatch decides path, so side-effecting builders (e.g. `AdvancedExtensions.Inspect`) execute unexpected work even on sink/fallback paths. Sink case throws *after* registering the probe op, leaving an orphan sink in the circuit if the caller catches + continues. **Fix**: prominent⚠️ side-effect warning section in docstring naming both implications; sink-throw error message also calls out the orphan-sink left behind. Architectural fix (non-registering probe path) is non-trivial and deferred — acknowledged in the new "future work" line. The docstring now makes the side-effect explicit so callers can avoid the failure mode (use non-side-effecting `q`; don't catch+continue on a sink-rejection). 2. **Copilot** (IncrementalAuto.Tests.fs:39): `feedAndStep` helper was dead code (left after refactoring out the test that used it). **Fix**: removed. 3. **Copilot** (IncrementalAuto.Tests.fs:176): test name said "adds three operators" but assertion + comment expected 4. **Fix**: renamed to "adds four operators (probe-orphan + Integrate + new Q + Differentiate)" matching the assertion. 4. **Copilot** (IncrementalAuto.Tests.fs:142): comment block claimed "output stream is literally the probed op (same reference)" and "zero-allocation" — but the test only asserts operator-count delta, not reference identity. **Fix**: rephrase comment to match what's actually tested (dispatch path verified via operator-count delta; reference-equality assertion would need internal `Stream.Op` accessor exposed). ## Tests 5/5 IncrementalAuto tests pass after fixes. Build clean. No behavioral changes to operator dispatch — the test rename + comment edits + dead-code removal are all annotation-shape; the docstring side-effect warnings are documentation-only. The orphan-sink + probe- side-effect *behavior* is unchanged; the *visibility* of that behavior is improved per Codex's P1. ## Architectural follow-up not in scope The cleanest fix for both Codex's P1 (probe side effects) AND the sink-rejection orphan-sink issue would be a non-registering probe path — e.g., a `Circuit.PreviewOp(q, input)` that runs `q.Invoke` inside a transaction-shaped scope that rolls back registration if the dispatcher rejects. That requires changes to the `Op` / `Circuit` registration contract (today's `Register` doesn't support rollback) and is deferred to a future PR. Worth filing as a backlog row when the architectural cost vs. payoff is clearer. * fix(PR #4567 Codex P1 #2): IncrementalAuto must check whole-chain linearity, not just terminal op Codex's second P1 finding caught a real correctness bug I missed: the dispatcher was checking `probedOutput.Op.IsLinear`, but `probedOutput.Op` is only the terminal operator in the chain produced by `q`. A query like `q(s) = Map(Distinct(s))` ends on a linear Map but the *composed* query is non-linear; the `Q^Δ = Q` rewrite produces wrong incremental results. ## Fix Recursive chain check: walk `Inputs` back from the probed terminal op to the original `input.Op`. If every op in the chain is linear AND we reach `input.Op` only through linear ops, the chain is linear. Otherwise fall back to `D ∘ Q ∘ I`. Multi-input ops (Plus, Minus, default IsLinear=false) correctly route to the fallback path via this check. ```fsharp let rec isLinearChainToInput (op: Op) (inputOp: Op) : bool = if System.Object.ReferenceEquals(op, inputOp) then true elif op.Inputs.Length = 0 then false // source op that isn't the input elif not op.IsLinear then false else op.Inputs |> Array.forall (fun dep -> isLinearChainToInput dep inputOp) ``` ## Regression test added `IncrementalAuto with terminal-linear-but-inner-non-linear chain falls back (Map ∘ Distinct)` — exercises the exact failure mode Codex flagged. Builds Map(Distinct(s)), runs IncrementalAuto, compares per-tick output to IncrementalizeZSet (D∘Q∘I reference). The test exercises duplicate-insertion + retraction scenarios where the broken dispatcher would produce wrong output (Map of every delta directly, ignoring Distinct's cumulative-state clamping). Before this fix: subject would emit `Map(delta)` directly each tick → incorrect when delta has duplicates that Distinct clamps. After this fix: subject falls back to D∘Q∘I → matches reference. ## Verification 6/6 IncrementalAuto tests pass (5 pre-existing + 1 new regression). Build clean. The chain-check helper is O(N) in chain depth, called once at dispatch time; zero per-tick cost. ## Related Composes with the earlier fix in this PR for the other 5 review threads (8230bed) — docstring side-effect warnings, test rename, dead-code removal, comment rewording. This commit addresses the substantive correctness P1 that the earlier docstring-shape fixes left unaddressed.
…rdination of load-bearing-substrate changes (#4575) Mechanizes the human-as-coordination-substrate pattern Aaron explicitly named 2026-05-21 ("i'm here right now" — for now ferrying load-bearing- substrate-change notifications between AI surfaces; trajectory is bus- based mechanization). ## The gap this row addresses When one AI surface lands a load-bearing substrate change — capability tags on `Op<'T>` (PR #4558), `IncrementalAuto`'s chain-walk logic (#4567), new files in `.claude/rules/`, new computation expressions — other AI surfaces working in adjacent substrate need to inherit the change for their next session. Today: Aaron ferries. Cluster-scale (10-20 surfaces per Aaron's $100k cluster expansion 2026-05-21): human-ferry breaks empirically. ## The mechanism New bus topic `substrate-surface-change` (extends `tools/bus/`): - **Publish discipline**: after any PR landing that modifies load- bearing surfaces, publishing AI calls `bun tools/bus/publish.ts --topic substrate-surface-change --from <sender-id> --payload <json>`. - **Subscribe discipline (cold-boot)**: AI bootstreams extend to include `bun tools/bus/list.ts --topic substrate-surface-change --since 24h` — recent envelopes show "what load-bearing substrate changed in the last 24h." - **Retention**: 7d default; expired envelopes fall back to auto- loaded rules + commit history. The envelope is the *cache* of recent changes; the *truth* is the substrate itself. ## What this row does NOT do - Does NOT replace auto-loaded `.claude/rules/` inheritance (that stays the durable substrate) - Does NOT replace claim-acquire-before-worktree-work (that stays the per-row collision prevention) - Does NOT replace Knights Guild / KSK (that stays the policy gate) It complements all three by adding the **recent-changes-cache** layer that closes the "I just shipped X; how do other surfaces find out before their next session?" gap. ## Composition with broader trajectory - B-0400 — bus protocol substrate this row extends - B-0689 — Otto-VSCode SENDER_IDS pattern this row leans on for `from` field - B-0695 — fast/life-branch experiment; sibling coordination-cost-reduction - Algebra-campaign PRs (#4558/#4560/#4563/#4566/#4567) — substrate-surface changes that would have benefited from this envelope pattern ## Substrate-honest framing on the file itself Filed per Aaron's explicit "feel free we can'thave too much backlog in my opinion the infinate backlog win when labor=0" framing, applying the `largest-mechanizable-backlog-wins.md` discipline. Recalibrated from earlier "I won't file unilaterally" reasoning — that was a misapplication of the row-collision lesson (which was about coordination, not about backlog overhead).
Summary
Supersedes #4564. Same content; cherry-picked onto current
mainafter PR 1 (#4558) + PR 2 (#4560) merged. The original branch went DIRTY because it carried PR 1's pre-squash commit; this branch carries only PR 4's content on top of cleanmain.Re-land path follows
.claude/rules/blocked-green-ci-investigate-threads.md§ "stale-armed-PR resolution patterns" → Re-land via cherry-pick (matches the empirical anchor pattern from PR #3823 → #3894).What this PR adds
Circuit.IncrementalAuto<'K>(q, input)— a dispatcher that picks the right incrementalization based onq's resulting operator's algebra capability tag (from PR 1, merged):IsLinear = trueQ^Δ = Q(deltas pass through)IsSink = trueD ∘ Q ∘ Ifallback via existingIncrementalizeZSetMechanizes the DBSP paper's first + third incrementalization clauses; bilinear case stays in
IncrementalJoin(richer signature).Implementation note
Probes
qby applying to the input, readsOp.IsLinear/Op.IsSink, then either returns the probed output directly (linear), throws (sink), or rebuilds viaIncrementalizeZSet(fallback — leaves an orphan probe op in the circuit; pruning unreachable ops at Build is future work).Tests (5, all pass)
IncrementalizeZSetover 6 ticks)Build clean; 5/5 tests pass.
Cross-reference
Op.IsLinear/Op.IsSinkTest plan
dotnet buildcleandotnet test --filter IncrementalAutoTests— 5/5 passSuccessor URL referenced in closing comment on #4564.