diff --git a/src/Core/LawRunner.fs b/src/Core/LawRunner.fs index 87b0ff81a0..c8da464862 100644 --- a/src/Core/LawRunner.fs +++ b/src/Core/LawRunner.fs @@ -131,6 +131,129 @@ module LawRunner = tick <- tick + 1 result) + /// Bilinearity — three sub-properties, each per-tick: + /// + /// L1 (left-linearity): op(a₁ + a₂, b) ≡ op(a₁, b) + op(a₂, b) + /// L2 (right-linearity): op(a, b₁ + b₂) ≡ op(a, b₁) + op(a, b₂) + /// L3 (sign-distribution): op(-a, b) ≡ -op(a, b) + /// + /// **Math note on L3.** Over an abelian group with standard + /// addition (as `(+)` is for `int`, and as `ZSet.add` is for + /// `ZSet<'K>`), L1 + L2 *imply* L3: setting `a₁ = a, a₂ = -a` + /// in L1 gives `op(0, b) = op(a, b) + op(-a, b)`, so the + /// classical bilinear condition `op(0, b) = 0` collapses to L3. + /// In that regime L3 is the "first failure to fire" line of + /// defense — an affine offset like `op(a, b) = a*b + c` breaks + /// L1 (the constant lands once on LHS, twice on RHS) AND L3 + /// (the constant survives negation), so L1 usually trips first + /// by check-order; L3 is the cleanup law. + /// + /// L3 becomes load-bearing — not redundant — when the caller- + /// supplied `(addOut, negOut)` pair doesn't actually form an + /// abelian group: `negOut` might not be a true inverse of + /// `addOut`, the operations might not be associative or + /// commutative on `'TOut`, or there might be hidden state in + /// the supplied functions. In such cases L1 + L2 can pass while + /// L3 catches the broken algebra — and a failure here may + /// reflect the *supplied algebra operations* rather than the + /// operator under test. Checking all three sub-properties keeps + /// `checkBilinear` correct across the full range of `'TOut` + /// algebras a plugin author might supply, not just `int` / + /// `ZSet<_>` where the abelian-group assumption holds by + /// construction. + /// + /// - `samples` — number of (A₁, A₂, B₁, B₂) quadruples. + /// - `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). + /// - `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. + /// - `negOut` — needed to form `-op(a, b)` for the L3 equality. + let checkBilinear<'TIn1, 'TIn2, 'TOut> + (seed: int) + (samples: int) + (scheduleLength: int) + (makeOp: Stream<'TIn1> -> Stream<'TIn2> -> IOperator<'TOut>) + (genInput1: System.Random -> 'TIn1) + (genInput2: System.Random -> 'TIn2) + (addIn1: 'TIn1 -> 'TIn1 -> 'TIn1) + (negIn1: 'TIn1 -> 'TIn1) + (addIn2: 'TIn2 -> 'TIn2 -> 'TIn2) + (addOut: 'TOut -> 'TOut -> 'TOut) + (negOut: 'TOut -> 'TOut) + (equalOut: 'TOut -> 'TOut -> bool) + : Result = + if samples < 1 then + Error (badArgs seed "samples must be >= 1") + elif scheduleLength < 1 then + Error (badArgs seed "scheduleLength must be >= 1") + else + runSamples seed samples (fun rng i -> + // Four independent traces for the per-arg laws. + let traceA1 = generateTrace rng scheduleLength genInput1 + let traceA2 = generateTrace rng scheduleLength genInput1 + let traceB1 = generateTrace rng scheduleLength genInput2 + let traceB2 = generateTrace rng scheduleLength genInput2 + + let traceASum = List.map2 addIn1 traceA1 traceA2 + let traceBSum = List.map2 addIn2 traceB1 traceB2 + let traceANeg = traceA1 |> List.map negIn1 + + // 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). + let outA1B1 = PluginHarness.runTwoInputs makeOp traceA1 traceB1 |> List.toArray + let outA2B1 = PluginHarness.runTwoInputs makeOp traceA2 traceB1 |> List.toArray + let outASumB1 = PluginHarness.runTwoInputs makeOp traceASum traceB1 |> List.toArray + let outA1B2 = PluginHarness.runTwoInputs makeOp traceA1 traceB2 |> List.toArray + let outA1BSum = PluginHarness.runTwoInputs makeOp traceA1 traceBSum |> List.toArray + let outANegB1 = PluginHarness.runTwoInputs makeOp traceANeg traceB1 |> List.toArray + + let mutable result = None + let mutable tick = 0 + while result.IsNone && tick < scheduleLength do + // L1: op(a₁+a₂, b) ≡ op(a₁, b) + op(a₂, b) + let l1Lhs = outASumB1.[tick] + let l1Rhs = addOut outA1B1.[tick] outA2B1.[tick] + if not (equalOut l1Lhs l1Rhs) then + result <- + Some (sprintf + "Left-linearity broke at sample %d, tick %d: \ + op(a₁+a₂, b) != op(a₁, b) + op(a₂, b)." + i tick) + else + // L2: op(a, b₁+b₂) ≡ op(a, b₁) + op(a, b₂) + let l2Lhs = outA1BSum.[tick] + let l2Rhs = addOut outA1B1.[tick] outA1B2.[tick] + if not (equalOut l2Lhs l2Rhs) then + result <- + Some (sprintf + "Right-linearity broke at sample %d, tick %d: \ + op(a, b₁+b₂) != op(a, b₁) + op(a, b₂)." + i tick) + else + // L3: op(-a, b) ≡ -op(a, b) + let l3Lhs = outANegB1.[tick] + let l3Rhs = negOut outA1B1.[tick] + if not (equalOut l3Lhs l3Rhs) then + result <- + Some (sprintf + "Sign-distribution broke at sample %d, tick %d: \ + op(-a, b) != -op(a, b). This is the failure \ + mode where a plugin claims IBilinearOperator \ + but smuggles an additive offset; the three-term \ + incremental-join rewrite will produce \ + wrong-but-quiet results under retraction." + i tick) + // nosemgrep: plain-tick-increment -- method-local loop counter, not shared across threads + tick <- tick + 1 + result) + /// Retraction completeness via state restoration. /// A forward trace of random Z-sets is cancelled by its /// elementwise negation; a continuation trace is then fed diff --git a/src/Core/PluginHarness.fs b/src/Core/PluginHarness.fs index 6c5cd4ff3c..43779ff267 100644 --- a/src/Core/PluginHarness.fs +++ b/src/Core/PluginHarness.fs @@ -73,6 +73,78 @@ module PluginHarness = "PluginHarness: tick %d expected exactly one Publish; saw %d." tick delta) outputs.Add adapter.Value + // Strict-op post-step hook — see runTwoInputs for the + // rationale; same fix applies symmetrically to single- + // input strict plugins (e.g. IStrictOperator-tagged + // ops exercised via LawRunner.checkLinear). + let postVt = (adapter :> Op).AfterStepAsync ct + if not postVt.IsCompletedSuccessfully then + postVt.AsTask().GetAwaiter().GetResult() + // nosemgrep: plain-tick-increment -- method-local loop counter, not shared across threads + tick <- tick + 1 + List.ofSeq outputs + + /// Drive a two-input plugin operator through a pair of parallel + /// input sequences. Each tick advances BOTH inputs in lock-step; + /// the shorter sequence determines the run length (`Seq.zip` + /// semantics). + /// + /// Used by `LawRunner.checkBilinear` to exercise per-argument + /// linearity and sign-distribution. Same exactly-one-`Publish` + /// assertion as `runSingleInput`. + let runTwoInputs<'TIn1, 'TIn2, 'TOut> + (makeOp: Stream<'TIn1> -> Stream<'TIn2> -> IOperator<'TOut>) + (inputs1: seq<'TIn1>) + (inputs2: seq<'TIn2>) + : 'TOut list = + let source1 = HarnessSourceOp<'TIn1>() + let source2 = HarnessSourceOp<'TIn2>() + // Synthetic ids — sources at 0+1, adapter at 2. Real circuits + // assign these during `Circuit.Build`; the harness mirrors + // the layout so the adapter's per-tick state semantics match + // production exactly. + source1.idField <- 0 + source2.idField <- 1 + let stream1 = Stream<'TIn1>(source1) + let stream2 = Stream<'TIn2>(source2) + let plugin = makeOp stream1 stream2 + + let inputOps : Op array = + plugin.ReadDependencies + |> Array.map (fun h -> h.op) + let adapter = PluginOperatorAdapter<'TOut>(plugin, inputOps) + adapter.idField <- 2 + + let outputs = ResizeArray<'TOut>() + let ct = CancellationToken.None + let mutable tick = 0 + let zipped = Seq.zip inputs1 inputs2 + for (in1, in2) in zipped do + source1.Feed in1 + source2.Feed in2 + let before = adapter.PublishCount.Value + let vt = (adapter :> Op).StepAsync ct + if not vt.IsCompletedSuccessfully then + vt.AsTask().GetAwaiter().GetResult() + let after = adapter.PublishCount.Value + let delta = after - before + if delta <> 1 then + invalidOp ( + sprintf + "PluginHarness: tick %d expected exactly one Publish; saw %d." + tick delta) + outputs.Add adapter.Value + // Mirror Circuit.Step/StepAsync's strict-op post-step + // hook: after StepAsync completes, invoke AfterStepAsync + // so strict bilinear/stateful ops commit per-tick state + // before the next tick begins. Without this, plugins + // implementing IStrictOperator would see different + // semantics in `runTwoInputs` than in real circuit + // execution, and `LawRunner.checkBilinear` would + // validate against incorrect strict-op state. + let postVt = (adapter :> Op).AfterStepAsync ct + if not postVt.IsCompletedSuccessfully then + postVt.AsTask().GetAwaiter().GetResult() // nosemgrep: plain-tick-increment -- method-local loop counter, not shared across threads tick <- tick + 1 List.ofSeq outputs diff --git a/tests/Tests.FSharp/Plugin/LawRunner.Tests.fs b/tests/Tests.FSharp/Plugin/LawRunner.Tests.fs index 46b44dae2f..83e11eae45 100644 --- a/tests/Tests.FSharp/Plugin/LawRunner.Tests.fs +++ b/tests/Tests.FSharp/Plugin/LawRunner.Tests.fs @@ -201,3 +201,198 @@ let ``checkRetractionCompleteness reproduces bit-exact on the same seed`` () = let first = run () let second = run () first |> should equal second + + +// ──────────────────────────────────────────────────────────────── +// Bilinearity fixtures +// +// `checkBilinear` exercises three sub-properties: +// 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) +// +// **Math note for these fixtures.** Over the abelian-group output +// types used here (`int` with standard `(+)`), L1 + L2 *imply* L3 — +// any algebraic failure that violates L3 also violates L1 first +// (the affine-offset case below illustrates this). So the L1 and L2 +// fixtures below cover both linearity failure modes and most +// classical bilinearity failures; L3 is the cleanup law that +// becomes load-bearing only when the caller supplies a non-abelian- +// group `(addOut, negOut)` pair — outside the scope of these +// fixtures. See `LawRunner.checkBilinear` docstring for the full +// math note. +// ──────────────────────────────────────────────────────────────── + +/// Genuine bilinear: integer multiplication. Satisfies L1, L2, +/// and L3 over the integer ring (with `op(0, b) = 0`). +type private BilinearMultOp(a: Stream, b: Stream) = + let deps = [| a.AsDependency(); b.AsDependency() |] + interface IBilinearOperator with + member _.Name = "bilinear-mult" + member _.ReadDependencies = deps + member _.StepAsync(out, _ct) = + out.Publish (a.Current * b.Current) + ValueTask.CompletedTask + + +/// **L1 liar** — adds the inputs before multiplying. Fails left- +/// linearity for any nonzero `b`: +/// op(a₁+a₂, b) = (a₁+a₂+b)*2 +/// op(a₁, b)+op(a₂, b) = 2(a₁+b)+2(a₂+b) = 2a₁+2a₂+4b +/// Falsely tagged `IBilinearOperator` so the law catches the lie. +type private LinearOffsetLiar(a: Stream, b: Stream) = + let deps = [| a.AsDependency(); b.AsDependency() |] + interface IBilinearOperator with + member _.Name = "linear-offset-liar" + member _.ReadDependencies = deps + member _.StepAsync(out, _ct) = + out.Publish ((a.Current + b.Current) * 2) + ValueTask.CompletedTask + + +/// **Affine offset liar** — `op(a, b) = a*b + 7`. The constant +/// offset breaks bilinearity in *multiple* ways; over the integer +/// abelian group L1 fails first (the constant lands once on LHS: +/// `(a₁+a₂)*b + 7`, twice on RHS: `(a₁*b + 7) + (a₂*b + 7)`, so +/// the difference is `7`, never equal). L3 would also fail +/// independently (`op(-a, b) = -a*b + 7` vs `-op(a, b) = -a*b - 7`) +/// but in the check ordering L1 trips first. The fixture catches +/// the additive-offset failure mode regardless of which sub-law +/// fires first; the test below documents which one fires for `int`. +type private AffineBilinearLiar(a: Stream, b: Stream) = + let deps = [| a.AsDependency(); b.AsDependency() |] + interface IBilinearOperator with + member _.Name = "affine-bilinear-liar" + member _.ReadDependencies = deps + member _.StepAsync(out, _ct) = + out.Publish (a.Current * b.Current + 7) + ValueTask.CompletedTask + + +// ──────────────────────────────────────────────────────────────── +// Bilinearity tests +// ──────────────────────────────────────────────────────────────── + +[] +let ``checkBilinear passes on a genuine bilinear op (integer multiplication)`` () = + let result = + LawRunner.checkBilinear + 42 20 8 + (fun a b -> BilinearMultOp(a, b) :> IOperator) + genInt genInt + (+) (~-) + (+) + (+) (~-) (=) + match result with + | Ok () -> () + | Error v -> Assert.Fail (sprintf "expected Ok, got %A" v) + + +[] +let ``checkBilinear catches an L1 (left-linearity) violation`` () = + let result = + LawRunner.checkBilinear + 42 20 8 + (fun a b -> LinearOffsetLiar(a, b) :> IOperator) + genInt genInt + (+) (~-) + (+) + (+) (~-) (=) + match result with + | Ok () -> Assert.Fail "expected L1 violation" + | Error v -> + v.Seed |> should equal 42 + // The first failing law per sample wins — for LinearOffsetLiar + // the L1 case fires before L2 or L3 are checked. + v.Message |> should haveSubstring "Left-linearity" + + +[] +let ``checkBilinear catches the affine-offset liar (additive constant breaks bilinearity)`` () = + let result = + LawRunner.checkBilinear + 42 20 8 + (fun a b -> AffineBilinearLiar(a, b) :> IOperator) + genInt genInt + (+) (~-) + (+) + (+) (~-) (=) + match result with + | Ok () -> Assert.Fail "expected bilinearity violation" + | Error v -> + v.Seed |> should equal 42 + // Math note: over an abelian group (the integer case here), + // L1 + L2 jointly *imply* L3 — the additive offset that + // breaks `op(0, b) = 0` also breaks `op(a₁+a₂, b) = op(a₁, + // b) + op(a₂, b)` because the constant is added once on the + // LHS and twice on the RHS. So the affine liar trips L1 + // first; L3 is the cleanup law for pathological cases where + // the user supplies a non-group addOut/negOut pair. + // L1 fires first per the check ordering in checkBilinear. + v.Message |> should haveSubstring "Left-linearity" + + +[] +let ``checkBilinear reproduces bit-exact on the same seed`` () = + let run () = + LawRunner.checkBilinear 99 10 5 + (fun a b -> AffineBilinearLiar(a, b) :> IOperator) + genInt genInt + (+) (~-) + (+) + (+) (~-) (=) + let first = run () + let second = run () + first |> should equal second + + +[] +let ``checkBilinear returns Error on bad samples arg`` () = + let result = + LawRunner.checkBilinear 0 0 1 + (fun a b -> BilinearMultOp(a, b) :> IOperator) + genInt genInt + (+) (~-) + (+) + (+) (~-) (=) + match result with + | Ok () -> Assert.Fail "expected bad-args Error" + | Error v -> v.Message |> should haveSubstring "samples" + + +[] +let ``checkBilinear returns Error on bad scheduleLength arg`` () = + let result = + LawRunner.checkBilinear 0 1 0 + (fun a b -> BilinearMultOp(a, b) :> IOperator) + genInt genInt + (+) (~-) + (+) + (+) (~-) (=) + match result with + | Ok () -> Assert.Fail "expected bad-args Error" + | Error v -> v.Message |> should haveSubstring "scheduleLength" + + +// ──────────────────────────────────────────────────────────────── +// PluginHarness.runTwoInputs tests +// ──────────────────────────────────────────────────────────────── + +[] +let ``runTwoInputs drives a two-input plugin in lock-step`` () = + let outputs = + PluginHarness.runTwoInputs + (fun a b -> BilinearMultOp(a, b) :> IOperator) + [ 1; 2; 3; 10 ] + [ 5; 5; 5; 100 ] + outputs |> should equal [ 5; 10; 15; 1000 ] + + +[] +let ``runTwoInputs truncates to the shorter input sequence`` () = + let outputs = + PluginHarness.runTwoInputs + (fun a b -> BilinearMultOp(a, b) :> IOperator) + [ 1; 2; 3; 4; 5 ] + [ 10; 20 ] + outputs |> should equal [ 10; 40 ]