tests: RecursiveSemiNaive boundary (Amara P0 — executably document monotone-only + retraction-leak scenarios) by AceHack · Pull Request #214 · Lucent-Financial-Group/Zeta

AceHack · 2026-04-23T23:13:29Z

Summary

Amara's 2026-04-23 ZSet-semantics courier report (absorbed as PR #211) called the RecursiveSemiNaive monotone-only boundary the highest-priority technical gap — "must remain explicitly labeled" as a boundary against Zeta's core retraction-native claim. The code and spec already document it; this PR adds executable documentation.

What landed

tests/Tests.FSharp/Operators/RecursiveSemiNaive.Boundary.Tests.fs (~170 lines, 2 tests)
Registered in Tests.FSharp.fsproj after the existing recursive-counting test

Two tests matching spec scenarios

From openspec/specs/retraction-safe-recursion/spec.md § "Requirement: semi-naïve recursion is monotone-only":

RecursiveSemiNaive matches Recursive on monotone inputs (acyclic DAG) — spec scenario deps: Bump FsUnit.xUnit from 7.1.0 to 7.1.1 #1. Positive-weight support equality between Recursive and RecursiveSemiNaive on a monotone edge seed.
RecursiveSemiNaive leaks stale facts after retraction (documented boundary) — spec scenario Round 26 — rename tail, §18 memory clarification, three dispatches #2. Asserts (1,3) remains after retracting (2,3), encoding the documented leak. Test-body comment names the investigation path if the assertion ever inverts (gap-monotone signed-delta replacement OR harness-mask investigation).

Reading note (in the test file)

the leak test is not a bug being asserted; it is a boundary being recorded.

This protects RecursiveSemiNaive's documented semantics from silent drift. If the algorithm is ever replaced with a retraction-safe variant (the research plan in docs/research/retraction-safe-semi-naive.md), the test will fail and prompt removing the leak-assertion alongside the algorithm replacement — they move together.

Verification

$ dotnet build tests/Tests.FSharp/Tests.FSharp.fsproj -c Release
    0 Warning(s)
    0 Error(s)
    Time Elapsed 00:00:05.36

$ dotnet test ... --filter "RecursiveSemiNaiveBoundary"
Passed!  - Failed: 0, Passed: 2, Skipped: 0, Total: 2, Duration: 46 ms

What this PR is NOT

Not a fix for the leak — the leak is intended per the algorithm's monotone-only contract; fixing it requires the gap-monotone signed-delta variant (research arc).
Not a breaking API change — RecursiveSemiNaive still works exactly as before.
Not an ADR on replacing the combinator — that's separate research.

Test plan

Both tests pass locally (net10.0 Release)
0 warnings (TreatWarningsAsErrors discipline preserved)

🤖 Generated with Claude Code

…utably Amara's 2026-04-23 ZSet-semantics courier report (absorbed as PR #211) called out the `RecursiveSemiNaive` monotone-only boundary as a "must remain explicitly labeled" gap. The code (src/Core/Recursive.fs XML doc WARNING section) and the spec (openspec/specs/retraction- safe-recursion/spec.md § "Requirement: semi-naïve recursion is monotone-only") already document it; this PR adds the *executable* documentation so the boundary cannot silently drift. New file: `tests/Tests.FSharp/Operators/RecursiveSemiNaive. Boundary.Tests.fs` (~170 lines, 2 tests, 0 warnings): Test 1 — `RecursiveSemiNaive matches Recursive on monotone inputs (acyclic DAG)`: encodes spec scenario #1. Compares positive-weight support between `Recursive` and `RecursiveSemiNaive` on a monotone edge seed; they must agree. Test 2 — `RecursiveSemiNaive leaks stale facts after retraction (documented boundary)`: encodes spec scenario #2. Feeds an edge retraction after initial closure and ASSERTS that the derived closure row (1,3) remains with positive weight. **Reading note: the leak test is not a bug being asserted; it is a boundary being recorded.** If a future change ever makes the test fail (i.e., the leak gets fixed), the investigation is documented in the test body — replace combinator with gap-monotone signed-delta variant OR investigate harness masking. Build + test verification: dotnet build tests/Tests.FSharp/Tests.FSharp.fsproj -c Release = 0 Warning(s) + 0 Error(s) in 5.4s dotnet test ... --filter "RecursiveSemiNaiveBoundary" = 2 Passed, 0 Failed Companion register: file registered in Tests.FSharp.fsproj after `Operators/RecursiveCounting.MultiSeed.Tests.fs` per existing section convention. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 0bed4df450

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

chatgpt-codex-connector · 2026-04-23T23:15:43Z

+        |> Seq.map (fun e -> e.Key)
+        |> Set.ofSeq
+
+    supportOf snResult |> should equal (supportOf refResult)


Enforce weight equality in monotone equivalence test

This scenario is meant to encode the spec requirement that RecursiveSemiNaive and Recursive “agree” after stabilization, but the assertion only compares positive-key support and ignores Z-weights. That means a regression where semi-naïve returns incorrect weights (for example, if distinct-clamping is accidentally removed) would still pass as long as the same keys are present, so the test would not actually guard the stated contract.

Useful? React with 👍 / 👎.

chatgpt-codex-connector · 2026-04-23T23:15:43Z

+    let outSN = OutputHandle closureSN.Op
+    cSN.Build()
+    edgesSN.Send (ZSet.ofKeys edges)
+    let struct (_, _) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)


Assert convergence before reading fixed-point outputs

IterateToFixedPointWithConvergence returns whether the iteration cap was hit before stabilization, but this result is discarded. Because both scenarios are defined in terms of behavior after the operators have stabilized, the test can silently validate transient state if a future change causes non-convergence within 20 steps, reducing its ability to catch real regressions.

Useful? React with 👍 / 👎.

Copilot

Pull request overview

Adds executable tests to document the monotone-only boundary of Circuit.RecursiveSemiNaive within Zeta’s retraction-safe recursion story, aligning test behavior with the OpenSpec retraction-safe-recursion capability scenarios.

Changes:

Adds a new operator test suite covering (1) monotone equivalence vs Recursive and (2) the documented retraction leak boundary.
Registers the new test file in tests/Tests.FSharp/Tests.FSharp.fsproj.

Reviewed changes

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

File	Description
tests/Tests.FSharp/Tests.FSharp.fsproj	Registers the new boundary test file in the test project compile list.
tests/Tests.FSharp/Operators/RecursiveSemiNaive.Boundary.Tests.fs	Adds two tests that executable-document monotone correctness and the retraction leak boundary for `RecursiveSemiNaive`.

Copilot · 2026-04-23T23:18:01Z

+// Motivation: Amara's 2026-04-23 ZSet-semantics courier report
+// (absorbed as `docs/aurora/2026-04-23-amara-zset-semantics-
+// operator-algebra.md` via PR #211) called out the
+// `RecursiveSemiNaive` monotone-only boundary as a "must remain
+// explicitly labeled" gap. Code and spec already document it; this


P0: This file’s header comment includes direct contributor name attribution (“Amara's …”). Repo policy forbids contributor names in code/docs/skills outside memory/persona/** (see docs/AGENT-BEST-PRACTICES.md operational rules). Please rewrite this motivation text using a role reference (e.g., “courier report” / “external semantics report”) without naming the contributor.

Copilot · 2026-04-23T23:18:02Z

+    // (Weight magnitudes may differ — `Recursive` uses `Distinct`
+    // internally so all weights clamp to 1; `RecursiveSemiNaive`
+    // may carry higher counts.)


P1: The comment claims RecursiveSemiNaive “may carry higher counts” than Recursive, but RecursiveSemiNaive uses Distinct inside the loop (same as Recursive), so output weights are clamped to {0,1}. Please fix or remove this misleading explanation.

Suggested change

// (Weight magnitudes may differ — `Recursive` uses `Distinct`

// internally so all weights clamp to 1; `RecursiveSemiNaive`

// may carry higher counts.)

// In this case the comparison is about the reachable support,

// not differing multiplicities: both combinators clamp output

// weights to positive support here.

Copilot · 2026-04-23T23:18:02Z

+    edgesRef.Send (ZSet.ofKeys edges)
+    let struct (_, _) = cRef.IterateToFixedPointWithConvergence(closureRef, 20)
+    let refResult = outRef.Current


P1: IterateToFixedPointWithConvergence returns a converged flag but it’s ignored here. Other tests in this repo assert convergence; please capture the boolean and assert it’s True so the test can’t silently pass with a non-converged intermediate state.

Copilot · 2026-04-23T23:18:02Z

+    edgesSN.Send (ZSet.ofKeys edges)
+    let struct (_, _) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)
+    let snResult = outSN.Current


P1: IterateToFixedPointWithConvergence’s convergence result is discarded here as well. Please assert converged = true (or raise the iteration cap with an explanation) to avoid comparing outputs from a non-fixed-point state.

Copilot · 2026-04-23T23:18:02Z

+    supportOf snResult |> should equal (supportOf refResult)
+
+


P1: This assertion only checks that Recursive and RecursiveSemiNaive agree with each other; it would still pass if both were wrong in the same way (e.g., both empty). Please also assert the expected closure support explicitly ((1,2), (2,3), (1,3)) and then check both results against that oracle.

Suggested change

supportOf snResult |> should equal (supportOf refResult)

let expectedSupport =

set [

struct (1, 2)

struct (2, 3)

struct (1, 3)

]

let refSupport = supportOf refResult

let snSupport = supportOf snResult

refSupport |> should equal expectedSupport

snSupport |> should equal expectedSupport

snSupport |> should equal refSupport

Copilot · 2026-04-23T23:18:03Z

+    let struct (_, _) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)
+    let after0 = outSN.Current
+    after0.[struct (1, 3)] |> should be (greaterThan 0L)
+
+    // tick 1: retract edge (2,3). Under semi-naïve, the positive-
+    // integrated `total` cannot be reversed — (1,3) leaks.
+    edgesSN.Send (ZSet.ofPairs [ struct (struct (2, 3), -1L) ])
+    let struct (_, _) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)


P1: Convergence is ignored here too (IterateToFixedPointWithConvergence). Please assert the returned converged flag so the leak assertion is evaluated on the stabilized output (and so failures diagnose cap/termination issues clearly).

Suggested change

let struct (_, _) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)

let after0 = outSN.Current

after0.[struct (1, 3)] |> should be (greaterThan 0L)

// tick 1: retract edge (2,3). Under semi-naïve, the positive-

// integrated `total` cannot be reversed — (1,3) leaks.

edgesSN.Send (ZSet.ofPairs [ struct (struct (2, 3), -1L) ])

let struct (_, _) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)

let struct (_, converged0) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)

converged0 |> should equal true

let after0 = outSN.Current

after0.[struct (1, 3)] |> should be (greaterThan 0L)

// tick 1: retract edge (2,3). Under semi-naïve, the positive-

// integrated `total` cannot be reversed — (1,3) leaks.

edgesSN.Send (ZSet.ofPairs [ struct (struct (2, 3), -1L) ])

let struct (_, converged1) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)

converged1 |> should equal true

Copilot · 2026-04-23T23:18:03Z

+    let struct (_, _) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)
+    let after0 = outSN.Current
+    after0.[struct (1, 3)] |> should be (greaterThan 0L)
+
+    // tick 1: retract edge (2,3). Under semi-naïve, the positive-
+    // integrated `total` cannot be reversed — (1,3) leaks.
+    edgesSN.Send (ZSet.ofPairs [ struct (struct (2, 3), -1L) ])
+    let struct (_, _) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)


P1: Same issue on the retraction tick: the converged flag is discarded. Please assert convergence (or document/raise the cap) before reading outSN.Current so the test can’t accidentally validate an intermediate state.

Suggested change

let struct (_, _) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)

let after0 = outSN.Current

after0.[struct (1, 3)] |> should be (greaterThan 0L)

// tick 1: retract edge (2,3). Under semi-naïve, the positive-

// integrated `total` cannot be reversed — (1,3) leaks.

edgesSN.Send (ZSet.ofPairs [ struct (struct (2, 3), -1L) ])

let struct (_, _) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)

let struct (_, converged0) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)

Assert.True(converged0, "Semi-naïve closure did not converge within 20 iterations on tick 0.")

let after0 = outSN.Current

after0.[struct (1, 3)] |> should be (greaterThan 0L)

// tick 1: retract edge (2,3). Under semi-naïve, the positive-

// integrated `total` cannot be reversed — (1,3) leaks.

edgesSN.Send (ZSet.ofPairs [ struct (struct (2, 3), -1L) ])

let struct (_, converged1) = cSN.IterateToFixedPointWithConvergence(closureSN, 20)

Assert.True(converged1, "Semi-naïve closure did not converge within 20 iterations on the retraction tick.")

Copilot AI review requested due to automatic review settings April 23, 2026 23:13

AceHack enabled auto-merge (squash) April 23, 2026 23:13

Copilot started reviewing on behalf of AceHack April 23, 2026 23:13 View session

AceHack merged commit 74b74fb into main Apr 23, 2026
13 checks passed

AceHack deleted the tests/recursive-seminaive-boundary-docs-spec-scenario branch April 23, 2026 23:15

chatgpt-codex-connector Bot reviewed Apr 23, 2026

View reviewed changes

Copilot AI reviewed Apr 23, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

tests: RecursiveSemiNaive boundary (Amara P0 — executably document monotone-only + retraction-leak scenarios)#214

tests: RecursiveSemiNaive boundary (Amara P0 — executably document monotone-only + retraction-leak scenarios)#214
AceHack merged 1 commit intomainfrom
tests/recursive-seminaive-boundary-docs-spec-scenario

AceHack commented Apr 23, 2026

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

chatgpt-codex-connector Bot Apr 23, 2026

Uh oh!

chatgpt-codex-connector Bot Apr 23, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Apr 23, 2026

Uh oh!

Copilot AI Apr 23, 2026

Uh oh!

Copilot AI Apr 23, 2026

Uh oh!

Copilot AI Apr 23, 2026

Uh oh!

Copilot AI Apr 23, 2026

Uh oh!

Copilot AI Apr 23, 2026

Uh oh!

Copilot AI Apr 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

-    supportOf snResult |> should equal (supportOf refResult)
+    let expectedSupport =
+        set [
+            struct (1, 2)
+            struct (2, 3)
+            struct (1, 3)
+        ]
+    let refSupport = supportOf refResult
+    let snSupport = supportOf snResult
+    refSupport |> should equal expectedSupport
+    snSupport |> should equal expectedSupport
+    snSupport |> should equal refSupport

Conversation

AceHack commented Apr 23, 2026

Summary

What landed

Two tests matching spec scenarios

Reading note (in the test file)

Verification

What this PR is NOT

Test plan

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Apr 23, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot Apr 23, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Apr 23, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 23, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 23, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 23, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 23, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 23, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 23, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants