feat(core): PR 3 of 8 — LawRunner.checkBilinear + PluginHarness.runTwoInputs

[AceHack]

Summary

Closes the algebra-tag verification gap on IBilinearOperator. Until this PR, LawRunner had checkLinear and checkRetractionCompleteness but no checkBilinear — meaning the 3-term incremental-join rewrite in Incremental.IncrementalJoin trusted the bilinear tag without any test-time way to verify it.

PR 3 of 8. Independent of PR 1 (#4558) and PR 2 (#4560) — ships off main directly.

New surface

PluginHarness.runTwoInputs

Drives a two-input plugin operator through paired input sequences in lock-step (Seq.zip semantics — shorter sequence wins). Mirrors runSingleInput with two HarnessSourceOp sources + adapter; same exactly-one-Publish discipline.

LawRunner.checkBilinear

Tests three sub-properties per sample:

• L1 — op(a₁+a₂, b) ≡ op(a₁, b) + op(a₂, b) (left-linearity)
• L2 — op(a, b₁+b₂) ≡ op(a, b₁) + op(a, b₂) (right-linearity)
• L3 — op(-a, b) ≡ -op(a, b) (sign-distribution)

Generates four traces (A₁, A₂, B₁, B₂), runs the operator through six combinations (A₁B₁, A₂B₁, ASumB₁, A₁B₂, A₁BSum, ANegB₁), checks the three laws per tick. (seed, sampleIndex)-reproducibility and Result<unit, LawViolation> return shape match checkLinear.

Math note on L3

Over an abelian group with standard addition (the int and ZSet<'K> case), L1 + L2 imply L3 — setting a₁=a, a₂=-a in L1 gives op(0, b) = op(a, b) + op(-a, b), so op(0, b) = 0 collapses to L3. In that regime L3 is the cleanup law; the affine offset that breaks L3 also breaks L1.

L3 becomes load-bearing when the user supplies a non-abelian-group (addOut, negOut) pair (e.g. a monoid where negOut isn't truly inverse). Checking all three keeps checkBilinear correct across the full range of 'TOut algebras.

Tests (6 new, 15/15 LawRunner pass)

• BilinearMultOp (integer multiplication) — passes
• LinearOffsetLiar ((a+b)*2) — catches L1
• AffineBilinearLiar (a*b + 7) — catches L1 (with docstring explaining why L3-only failure doesn't exist over int)
• Reproducibility on same seed
• Bad-args validation
• runTwoInputs lock-step + truncation behavior

Foundation for later PRs

PR 4's IncrementalAuto dispatcher will read Op.IsBilinear to pick the three-term-bilinear rewrite. A debug-mode Circuit.Build() hook can run checkBilinear against any operator claiming the tag, catching tag-vs-implementation drift early.

Test plan

• dotnet build clean
• dotnet test --filter LawRunnerTests — 15/15 pass (9 pre-existing + 6 new)
• CI green

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 9e410a651b

ℹ️ 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".

[Copilot]

Pull request overview

Adds missing bilinearity verification support for plugin operators by extending the test harness to drive two-input plugins and introducing a new LawRunner.checkBilinear check, with accompanying unit tests to validate both passing and failing fixtures.

Changes:

• Introduces PluginHarness.runTwoInputs to run two-input IOperator<'TOut> plugins over paired input sequences (zip/lock-step semantics) with the existing exactly-one-Publish discipline.
• Adds LawRunner.checkBilinear to validate left-linearity (L1), right-linearity (L2), and sign distribution (L3) across generated traces with deterministic (seed, sampleIndex) reproducibility.
• Adds new LawRunner/PluginHarness tests covering bilinear success, failure modes, bad-args validation, and runTwoInputs truncation behavior.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.

File	Description
tests/Tests.FSharp/Plugin/LawRunner.Tests.fs	Adds bilinearity fixtures/tests and runTwoInputs behavior tests.
src/Core/PluginHarness.fs	Adds runTwoInputs helper mirroring runSingleInput behavior for two-input plugins.
src/Core/LawRunner.fs	Adds checkBilinear law runner for IBilinearOperator-tag verification.

Comments suppressed due to low confidence (4)

tests/Tests.FSharp/Plugin/LawRunner.Tests.fs:250

• This docstring says the affine-constant fixture "Satisfies L1 + L2" and only fails L3, but with standard integer addition the constant offset causes L1 to fail first (as noted later in the test). Update the wording here so the fixture description matches the actual algebra (and the expected failure ordering).

/// **L3 liar** — the load-bearing failure case. Satisfies L1 + L2
/// (because the constant offset is independent of inputs), but
/// fails L3:

src/Core/LawRunner.fs:168

• The rationale for only checking L3 on the first argument is currently not well-supported: "L2 + L3-on-first + abelian-group structure imply L3-on-second" does not follow (sign distribution on the second input is about the input2 additive inverse, which isn't part of the current parameters). Either accept a negIn2 parameter and check sign-distribution on the second argument too, or adjust the comment to avoid claiming an implication that isn't justified by the provided operations.

    /// - `negIn1` — required for the L3 sign-distribution check on
    ///   the first argument. We test L3 only on the first argument
    ///   because L2 + L3-on-first + abelian-group structure imply
    ///   L3-on-second; the asymmetry is intentional, mirroring what
    ///   `IncrementalJoin` actually requires.

src/Core/LawRunner.fs:163

• Doc inconsistency: the scheduleLength bullet says longer traces exercise stateful bilinear ops, but the implementation later says the law is for "STATELESS bilinearity per tick". Please reconcile these comments so it's clear whether stateful operators are intended to be in-scope for this check, and (if not) avoid implying longer schedules help exercise stateful behavior.

    /// - `scheduleLength` — ticks per trace. Each per-argument trace
    ///   uses one fresh draw per tick, so longer schedules exercise
    ///   stateful bilinear ops (e.g. windowed joins).

src/Core/LawRunner.fs:204

• This comment says the bilinear law here applies to "STATELESS bilinearity per tick" and that stateful ops need a separate formulation. Given the check compares full output traces from fresh op instances (similar to checkLinear), this reads misleading—stateful stream operators can still be linear/bilinear as functions of their input histories. Please clarify the intended scope and adjust the wording accordingly.

                // Run all the per-arg cases through the same operator
                // factory. Each run gets a fresh op instance — the
                // bilinear law applies to STATELESS bilinearity per
                // tick; stateful bilinear ops need a stronger
                // formulation (a separate law, not in scope here).

[AceHack]

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 (Core.CSharp.ZetaId.csproj had no .NET test projects directly referencing it). #4571 retargets to Core.CSharp.csproj + drops break-threshold to 0 (observational mode; still records signal + uploads HTML). Once #4571 merges, the cached Stryker.NET mutation test (Core.fsproj) failure on this PR becomes irrelevant (the workflow re-runs against the new C# target on the next push to this branch).

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 PluginHarness.runTwoInputs post-step-hook invocation + IncrementalAuto probe semantics; Copilot flagged docstring claims about monoid/group inverses + test naming mismatches. These need your domain attention, not workflow fixes. Surfacing so the path forward is visible: Stryker bottleneck is on me; substantive threads are yours.