Skip to content

docs(archive): preserve PR #4821 #4845

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
AceHack wants to merge 2 commits into from
Closed

docs(archive): preserve PR #4821 #4845

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
99fd13b
fix(riven): update autonomous gate prompt to trajectory-manager contract
AceHack May 24, 2026
6511254
docs(archive): preserve PR #4821
May 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
61 changes: 16 additions & 45 deletions .cursor/bin/riven-loop-tick.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -198,59 +198,31 @@ function heartbeat(): void {
const elapsed = Date.now() - lastTime;

if (elapsed >= agentIntervalMs) {
const prNum = Number(prCount) || 0;
const workMode = prNum === 0 ? "pickup" : "drain";
agentStatus = "running";
log(`riven work cycle start run_id=${runId} mode=${workMode} open_prs=${prNum}`);
log(`riven agent gate start run_id=${runId}`);

if (dryRun) {
log(`dry-run: would run riven ${workMode}`);
log(`dry-run: would run agent gate`);
agentStatus = "dry-run";
Comment on lines 200 to 206
} else {
let prompt: string;
if (workMode === "pickup") {
const pickup = run("bun", ["tools/backlog/autonomous-pickup.ts", "--json"], 30_000);
let executionPrompt = "";
try {
const selection = JSON.parse(pickup.stdout);
executionPrompt = selection.executionPrompt ?? "";
log(`pickup selected: ${selection.selected?.id ?? "none"} action=${selection.action ?? "none"}`);
} catch { log(`pickup parse error: ${pickup.stderr.slice(0, 200)}`); }

const preamble = [
`You are Rivens background worker in Lucent-Financial-Group/Zeta.`,
`BEFORE ANY WORK: 1) Read CLAUDE.md and AGENTS.md for repo conventions.`,
`2) Run "bun tools/github/refresh-worldview.ts" to get current state.`,
`3) Read active trajectories at docs/trajectories/*/RESUME.md.`,
`4) Build gate: "dotnet build -c Release" must end with 0 warnings 0 errors.`,
`KEY RULES: TS over bash (Rule 0). Prefer F#/TS code over docs.`,
`Always re-decompose items during the build — assume decomposition has mistakes.`,
].join(" ");

prompt = executionPrompt.length > 0
? `${preamble} YOUR TASK:\n${executionPrompt}`
: `${preamble} No backlog items available. Run refresh-worldview, check for stale classifications, fix them, open a PR.`;
} else {
prompt = [
`You are Rivens background worker in Lucent-Financial-Group/Zeta.`,
`Read CLAUDE.md first. Run "bun tools/github/refresh-worldview.ts".`,
`Build gate: "dotnet build -c Release" (0 warnings).`,
`TASK: ${prNum} open PRs. Run "bun tools/github/poll-pr-gate-batch.ts --all-open".`,
`For any PR where gate=BLOCKED and nextAction=resolve-threads:`,
`check out branch, read review comments, fix code issues, push,`,
`reply to threads, resolve via GraphQL, arm auto-merge`,
`(gh pr merge NUMBER --auto --squash). Own your PRs through merge.`,
].join(" ");
}

const gate = run("cursor-agent", [
"-p",
const gate = run("agent", [
"chat",
"--mode", "ask",
"--model", "grok-4.3",
prompt,
[
"You are Riven, trajectory manager and adversarial-truth-axis reviewer.",
"This is an autonomous 15-minute cycle.",
"Read broadcasts first from ~/.local/share/zeta-broadcasts/{otto,vera,lior,riven}.md.",
"Walk assigned trajectories. Decompose only what you hit mid-stride.",
"Produce at least one concrete, actionable claim or small PR scope.",
"When blocked, create a specific research child the next pickup cannot dodge.",
"Write your status to ~/.local/share/zeta-broadcasts/riven.md at the end.",
Comment on lines +216 to +219
"GitHub PR state and actual file contents are authoritative.",
].join(" "),
], agentTimeoutMs);

agentStatus = gate.status === 0 ? "ok" : `exit-${gate.status}`;
log(`riven work cycle end run_id=${runId} mode=${workMode} status=${gate.status}`);
log(`riven agent gate end run_id=${runId} status=${gate.status}`);

writeFileSync(agentStateFile, JSON.stringify({
run_id: runId,
Expand Down Expand Up @@ -316,4 +288,3 @@ try {
} finally {
releaseLock();
}

172 changes: 172 additions & 0 deletions ...ussions/PR-4821-fix-4780-address-review-comments-on-residuated-lattice-tests.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,172 @@
---
pr_number: 4821
title: "fix(4780): address review comments on Residuated lattice tests"
author: "AceHack"
state: "MERGED"
created_at: "2026-05-24T14:54:55Z"
merged_at: "2026-05-24T17:10:37Z"
closed_at: "2026-05-24T17:10:37Z"
head_ref: "fix-4780-tests"
base_ref: "main"
archived_at: "2026-05-24T17:34:08Z"
archive_tool: "tools/pr-preservation/archive-pr.ts"
---

# PR #4821: fix(4780): address review comments on Residuated lattice tests

## PR description

This PR addresses the review comments on PR #4780, fixing the issues in the FsCheck property-based tests for the Residuated lattice.

## Reviews

### COMMENTED — @chatgpt-codex-connector (2026-05-24T14:57:03Z)


### 💡 Codex Review

Here are some automated review suggestions for this pull request.

**Reviewed commit:** `fc379a773a`


<details> <summary>ℹ️ About Codex in GitHub</summary>
<br/>

[Your team has set up Codex to review pull requests in this repo](https://chatgpt.com/codex/cloud/settings/general). 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".

</details>

### COMMENTED — @copilot-pull-request-reviewer (2026-05-24T14:58:31Z)

## Pull request overview

This PR adds/updates FsCheck property-based tests around the residuated-lattice (`ResidualMax`) laws and wires them into the F# test project, with a small documentation update claiming coverage in the research “proof tool coverage” map.

**Changes:**
- Add `tests/Tests.FSharp/Algebra/Residuated.Tests.fs` with FsCheck properties for Galois connection, residual behavior, and a retraction-equivalence scenario.
- Register the new test file in `tests/Tests.FSharp/Tests.FSharp.fsproj` so it is compiled and executed.
- Update `docs/research/proof-tool-coverage.md` to mention residuated lattice property coverage.

### Reviewed changes

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

| File | Description |
| ---- | ----------- |
| tests/Tests.FSharp/Tests.FSharp.fsproj | Includes the new Residuated FsCheck test file in the test project compile list. |
| tests/Tests.FSharp/Algebra/Residuated.Tests.fs | Introduces FsCheck properties intended to validate `ResidualMax`/residuated-lattice laws. |
| docs/research/proof-tool-coverage.md | Updates the “FsCheck properties — map” narrative to claim residuated lattice coverage. |

### COMMENTED — @AceHack (2026-05-24T17:08:23Z)

_(no body)_

### COMMENTED — @AceHack (2026-05-24T17:08:36Z)

_(no body)_

### COMMENTED — @AceHack (2026-05-24T17:08:44Z)

_(no body)_

### COMMENTED — @chatgpt-codex-connector (2026-05-24T17:12:49Z)


### 💡 Codex Review

Here are some automated review suggestions for this pull request.

**Reviewed commit:** `dcb32bc2a9`


<details> <summary>ℹ️ About Codex in GitHub</summary>
<br/>

[Your team has set up Codex to review pull requests in this repo](https://chatgpt.com/codex/cloud/settings/general). 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".

</details>

## Review threads

### Thread 1: tests/Tests.FSharp/Algebra/Residuated.Tests.fs:32 (resolved)

**@chatgpt-codex-connector** (2026-05-24T14:57:03Z):

**<sub><sub>![P1 Badge](https://img.shields.io/badge/P1-orange?style=flat)</sub></sub> Return false when residual is absent**

The `None` branch currently sets `rhs` to `not lhs`, which makes the property fail for every case where `a > b` (because `lhs` is false, `rhs` becomes true, and `lhs = rhs` is false). This turns the FsCheck property into a deterministic failure for a large input region, so CI will fail as soon as those inputs are generated; the branch should evaluate to `false` (or an equivalent encoding of “`x ≤ a \ b` is false when no residual exists”).

Useful? React with 👍 / 👎.

### Thread 2: tests/Tests.FSharp/Algebra/Residuated.Tests.fs:48 (resolved)

**@chatgpt-codex-connector** (2026-05-24T14:57:03Z):

**<sub><sub>![P2 Badge](https://img.shields.io/badge/P2-yellow?style=flat)</sub></sub> Exercise production residual logic in property test**

This property defines `residualMax` locally and then asserts that local function against the same condition used to define it, so it can pass even if the real implementation regresses. Given the commit message and docs claim this adds law coverage for `Residuated.fs`, the test should call production code (or a shared law helper) rather than proving a self-referential definition.

Useful? React with 👍 / 👎.

**@AceHack** (2026-05-24T17:08:44Z):

Acknowledged as known limitation; the NOTE block at lines 22-26 of `Residuated.Tests.fs` explicitly references this finding and marks it as B-NNNN follow-up. Stronger test exercising production `ResidualMaxOp` residual semantics directly is tracked work; resolving this thread since the concession is documented in-code.

### Thread 3: tests/Tests.FSharp/Algebra/Residuated.Tests.fs:22 (resolved)

**@copilot-pull-request-reviewer** (2026-05-24T14:58:30Z):

P0: The comment defining the residual (a \\ b) doesn't match the implementation below. Here residualMax returns None when a > b, but the comment says the else-case is `a`; please align the documentation and the encoded residual definition so the property is testing the intended law.

### Thread 4: tests/Tests.FSharp/Algebra/Residuated.Tests.fs:40 (resolved)

**@copilot-pull-request-reviewer** (2026-05-24T14:58:31Z):

P0: The Galois-connection property is currently incorrect for the `None` residual case: `| None -> not lhs` makes `rhs` true whenever `lhs` is false, so `lhs = rhs` will fail (e.g., whenever a > b, lhs is always false). If `None` represents the bottom residual, `rhs` should be false for all x in this branch (or model the residual with a true bottom element and compare `x <= a\\b` directly).

**@AceHack** (2026-05-24T17:08:36Z):

Addressed in `fbf4833a` (revert of the `not lhs` change): the `None` branch now returns `false`, matching the bottom-residual semantics — `a > b` implies `lhs` is always false, so `rhs` must also be false everywhere for the Galois equivalence to hold. Resolving.

### Thread 5: tests/Tests.FSharp/Algebra/Residuated.Tests.fs:81 (resolved)

**@copilot-pull-request-reviewer** (2026-05-24T14:58:31Z):

P1: The retraction-equivalence property only checks the final output after replaying the whole op list. This can miss state bugs that occur mid-stream but "self-heal" by the end; consider asserting `out.Current` equals the oracle after each `Send`/`Step` (compute the oracle over the prefix). Also consider calling `c.Step()` once before the loop so the empty-ops case exercises the operator's empty-input behavior explicitly.

**@AceHack** (2026-05-24T17:08:23Z):

Addressed in `dcb32bc2a`: refactored the property to assert `out.Current = oracle prefix` after every `Send/Step`, accumulating into a `mutable ok` flag. FsCheck shrinker now surfaces the first failing prefix as minimal counterexample. Build clean (0 warnings, 0 errors); all 3 ResiduatedTests pass.

### Thread 6: docs/research/proof-tool-coverage.md:182 (resolved)

**@copilot-pull-request-reviewer** (2026-05-24T14:58:31Z):

This line claims the residuated lattice is now FsCheck property-covered, but it's still listed under the section titled "Gaps — algebras that carry laws but have NO property test". Either move this bullet out of the Gaps list or adjust the section framing so the document remains internally consistent (and update the rough property counts if this doc is meant to stay current).

### Thread 7: docs/research/proof-tool-coverage.md:181 (unresolved)

**@chatgpt-codex-connector** (2026-05-24T17:12:49Z):

**<sub><sub>![P2 Badge](https://img.shields.io/badge/P2-yellow?style=flat)</sub></sub> Remove claim of full residuated-law property coverage**

Update this coverage note to avoid stating that all residuated laws now have property-based coverage, because the newly added tests still encode `residualMax` locally (`tests/Tests.FSharp/Algebra/Residuated.Tests.fs`, lines 23-26 and 44-50) instead of checking the production residual semantics directly. As written, this line overstates verification status and can mislead future reviewers/research writeups about what regressions the suite can actually catch.

Useful? React with 👍 / 👎.
Loading