From 32b3aa9340c1ee89a365a256279d3dfcd02db566 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 4 Oct 2026 02:58:14 +0000 Subject: [PATCH 1/4] Add steward and babysit skills for Math- PR stewardship .claude/skills/steward/SKILL.md summarizes, and links as normative, the rules that already bind this repository (AGENTS.md, main AGENTS.md, OP-WORKFLOW-20260930, OP-PRIVACY-20260927, docs/FORMAL_REQUIRED_CHECKS.md): frozen heads while a nonauthor read is open, AMEND timing and byte-diff readbacks, packet and Lean gates, stacked-base reconciliation, merge commits only, integration by a non-author lane, and the never-list. .claude/skills/babysit/SKILL.md gives the short watching posture and defers to steward. No other path changes; no new rule or register. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .claude/skills/babysit/SKILL.md | 19 ++++++ .claude/skills/steward/SKILL.md | 111 ++++++++++++++++++++++++++++++++ 2 files changed, 130 insertions(+) create mode 100644 .claude/skills/babysit/SKILL.md create mode 100644 .claude/skills/steward/SKILL.md diff --git a/.claude/skills/babysit/SKILL.md b/.claude/skills/babysit/SKILL.md new file mode 100644 index 000000000..e111f7a9e --- /dev/null +++ b/.claude/skills/babysit/SKILL.md @@ -0,0 +1,19 @@ +--- +name: babysit +description: Posture for watching a Math- pull request through CI and review events. Short form; the repository conventions are in the steward skill (`.claude/skills/steward/SKILL.md`), which takes precedence. +--- + +# Babysit: watching a Math- pull request + +Read [`../steward/SKILL.md`](../steward/SKILL.md) first. It holds this repository's conventions: frozen heads, AMEND timing, gates, stacked bases and integration. This file adds only the watching posture. + +- **Never punt.** Every event on a PR you own ends in one of three ways: + - a validated push; + - one comment that names the exact blocker and what is needed; + - a recorded reason that nothing is yours to do, because the PR waits on a reviewer or an integrator. +- **Address every unresolved thread.** Answer each one where it was raised, and resolve the threads you fixed. +- **A failing test is never assumed to be an infra flake.** Reproduce it and root-cause it first (steward §4). +- **A green, mergeable head may wait on people. A red or conflicted head never waits.** +- **Keep the head frozen while a nonauthor read is open**, even when a fix seems obvious. Apply it after the verdict (steward §3). +- **Update the PR body's disposition on every material change** (steward §2), and keep the lane's ledger in main#229 current. +- **Stop following a PR** when it is merged or closed, or when Dylan says stop. diff --git a/.claude/skills/steward/SKILL.md b/.claude/skills/steward/SKILL.md new file mode 100644 index 000000000..005ff50fd --- /dev/null +++ b/.claude/skills/steward/SKILL.md @@ -0,0 +1,111 @@ +--- +name: steward +description: Math- conventions for driving a pull request to a mergeable state. Covers frozen heads while a nonauthor read is open, AMEND timing and readbacks, the packet and Lean gates, stacked-base reconciliation, merge commits only, and integration by a non-author lane. Read before acting on CI, review or merge-state events on a Math- PR that you opened or drive for its author. +--- + +# Steward: driving a Math- pull request + +This skill summarizes rules that already bind this repository. It adds none. On any conflict, these sources win: +- [`AGENTS.md`](../../../AGENTS.md); +- `main` [`AGENTS.md`](https://github.com/d6g8k5htny-coder/main/blob/main/AGENTS.md); +- the [current workflow](https://github.com/d6g8k5htny-coder/main/blob/main/governance/OP-WORKFLOW-20260930.md); +- the [privacy rule](https://github.com/d6g8k5htny-coder/main/blob/main/governance/OP-PRIVACY-20260927.md); +- [`docs/FORMAL_REQUIRED_CHECKS.md`](../../../docs/FORMAL_REQUIRED_CHECKS.md). + +Cross-lane coordination (claims, ledgers, routing, releases) happens in [main#229](https://github.com/d6g8k5htny-coder/main/issues/229). + +## 1. Identity, roles and credit + +- **One GitHub account carries every lane.** Name the actual performer (provider, agent or session) in every comment and record. The owner-facing attribution is "Dylan Roy — delegated AI work" (or "— delegated AI review"), followed immediately by the actual performer. +- **The author never approves or merges its own PR.** Integration is done by a non-author lane. The named integration owner controls branch refresh, readiness changes and the merge. +- **Independence credit.** + - A same-provider read is useful technical work but earns zero organizational-independence credit. A Claude read does not count as the nonauthor read of a Claude-authored packet. + - Grok Bot agent reads count (owner ruling of 2026-10-03, main#229 comment 5974405061). The agreed performer line is "Grok Bot agent N (Grok Bot support agent; non-Claude, nonauthor lane)". +- **xAI/Grok and Cursor agents work here only as support**, at a lane's request ([`AGENTS.md`](../../../AGENTS.md)). Never restart stopped agents, timers or loops ([`OWNER_STOP.md`](../../../OWNER_STOP.md)). Cite only what such agents have published. +- **Never ask Dylan to re-approve autonomy he has already granted.** + +## 2. The PR body is the disposition + +Keep one short current disposition in the PR body: +- the current head and the owner; +- completed review scopes, each linked to its verdict; +- unresolved finding IDs ("none" when none are open); +- validation; +- the next action. + +Update it on every material change. Link evidence rather than copying it. A closed issue or an outdated thread does not discharge an open obligation. + +## 3. Reads, verdicts and AMENDs + +1. **A read starts with a pickup comment** that names the PR, the slice and the exact head SHA. +2. **While a read is open, the head is frozen.** Push nothing to it, not even an optional nit, because that would stale the read. +3. **The verdict is PASS, AMEND (with the exact change) or BLOCK (with the reason)**, followed by the scope actually checked and what was not checked. +4. **Apply an AMEND only after its verdict is posted.** Then: + - push one commit that does exactly what the AMEND says; + - reply on the PR, naming the commit; + - request a byte-diff readback of `old-head..new-head`. + + A readback checks the delta, not the whole packet again. +5. **Optional and non-blocking points never start a push on their own.** + - Reply once (stays as is and why, or rides a later push). + - Carry the plainly correct ones into the next push that changes those files for another reason, or into a stacked successor PR. The reviewed head then stays the one the reads hashed. +6. **Changed reviewed bytes, dependencies or scope invalidate the affected review.** A base-only merge does not. It needs a bounded comparison (the packet bytes are identical to the reviewed head) plus fresh integration checks. + +## 4. Checks + +**Required.** `math-downstream-gates` is the required aggregate. It depends on `downstream-replay` and `formal / formal-evidence` succeeding at the tested commit. Packet workflows add their own jobs, for example `certify-and-reject-mutants` for coefficient packets and `kernel-evidence` for the Lean cap packet. A missing, skipped, neutral or cancelled result is not success. Old receipts are never rebound to a new commit. + +**Packet checkers (Python standard library only).** +- Run `python3 -B -S .py` and `python3 -B -O -S .py`. Their output must be byte-identical to each other and to the packet's `RESULTS.json`. +- Every mutant must be rejected, strictly: exit code 1 and `"passed": false`. +- `SOURCE_FILES.json` records bytes, SHA-256 and git blob. Workflows check its `pins_on_main` against `main`. If `main` changes a pinned file, re-pin and refresh the record as an ordinary reviewed change. Never weaken the check. + +**Lean packets** (`frontiers/cap_first_exit_lean_20261002/`, and `formal/` under its own contract): +- `python3 -B -S gate.py` in source mode; +- `python3 -B -S -m unittest test_gate` and the same with `-O`; +- `python3 gate.py --execute` with the pinned toolchain (`lake` on `PATH`). It builds fresh, replays with `leanchecker`, audits axioms (only `propext`, `Classical.choice` and `Quot.sound` are allowed) and runs three negative controls. All three must be REJECTED. + +After any change to a packet file, regenerate `MANIFEST.json` and run the source gate again. A kernel-checked build is engineering evidence. It is not an alignment review and not scientific acceptance. + +**Red CI on your PR is work now.** +- Reproduce the failure, root-cause it, fix it in scope, validate locally and push. +- "Flake" is not a root cause. Re-run at most once, and only when the job died before any test body ran. +- Never skip, disable or quarantine a test. Never push an empty commit. Never close and reopen a PR to restart CI. +- Some replays are long; the SIDE24 `d = 6` certificate replay takes about 25–45 minutes. Wait for it rather than re-running. + +## 5. Branches and pushes + +- **Merge commits only.** No rebase, no amend, and no force-push on a reviewed or shared branch. +- **Change another owner's branch only after an explicit scoped handoff, a release, or a confirmed lease expiry**, followed by a check of its current state. +- **Verify the remote head after every push** with `git ls-remote origin `. +- **Stacked PRs.** When the lower PR merges: + 1. merge `main` into the next branch with a merge commit; + 2. verify that the packet bytes equal the reviewed head (by diff over the packet directory and its workflow); + 3. run the gates again and push; + 4. post one comment stating the byte-identity, so the earlier review carries forward; + 5. retarget the PR to `main` if GitHub has not done so already. + +## 6. Integration (for the integrator, never the author) + +Immediately before merging, read again: +- the current head and base; +- the complete diff; +- the latest reviews and unresolved threads; +- ownership claims; +- the required checks at the exact head. + +Merge with `expected_head_sha` and a merge commit. If the branch is behind, use a merge-commit update. Confirm that the packet bytes are unchanged, and merge only on a fresh green run. Do not bypass protection or simulate another identity's approval. Record an unexpected merge honestly. + +## 7. Never in a packet PR + +- Edit `STATUS`, `PROOF_INDEX`, `GRAPH`, catalog or register surfaces, or create another status register. +- Flip `lemma_closed`, prize or premise flags. Packet PRs have scientific effect NONE. +- Publish private or personal material. Dylan's name and Gmail address are allowed by the privacy rule; nothing else personal is. +- Approve, merge or resolve a thread on another lane's behalf. + +## 8. Comments and records + +- **Check the latest comments before writing.** Be frugal: one comment per round, at the point where it resolves something, raises a real blocker or asks a question. +- **Answer each review thread where it was raised.** Resolve the threads you addressed. +- **Claims name the exact scope and paths**, carry a lease, and are released when the work finishes. +- **End agent-authored comments with the attribution footer your harness requires.** From 96b43b8654a251a296e3511c7f84476dbde82943 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 4 Oct 2026 03:11:46 +0000 Subject: [PATCH 2/4] Skills: answer the seven Codex findings on #267 - Pin each normative source by repository, commit, path and git blob, with live links for newer revisions (P1 4175942973). - A base-only merge carries a review forward only when the reviewed dependency slice, not just the packet directory, is unchanged (P1 4175942977); the stacked-base step checks the same slice. - Mutant rejection follows each packet's own contract: exit code 1 always, JSON "passed": false only where specified (P2 4175942969). - Split the cap-packet and formal/ recipes; formal/ runs unittest discover -s formal/tests and five negative controls (P2 4175942972). - Drop the SIDE24 d = 6 example, which is not on main (P2 4175942982). - Required checks bind to the tested merge commit of the current head/base pair (P2 4175942980). - Define precedence when CI turns red during an open read: a red head caused by the PR's own bytes is fixed with an announced, single-fix push and the reader re-points; otherwise the head stays frozen (P2 4175942967). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .claude/skills/babysit/SKILL.md | 2 +- .claude/skills/steward/SKILL.md | 52 +++++++++++++++++++++++---------- 2 files changed, 38 insertions(+), 16 deletions(-) diff --git a/.claude/skills/babysit/SKILL.md b/.claude/skills/babysit/SKILL.md index e111f7a9e..f2c97e301 100644 --- a/.claude/skills/babysit/SKILL.md +++ b/.claude/skills/babysit/SKILL.md @@ -14,6 +14,6 @@ Read [`../steward/SKILL.md`](../steward/SKILL.md) first. It holds this repositor - **Address every unresolved thread.** Answer each one where it was raised, and resolve the threads you fixed. - **A failing test is never assumed to be an infra flake.** Reproduce it and root-cause it first (steward §4). - **A green, mergeable head may wait on people. A red or conflicted head never waits.** -- **Keep the head frozen while a nonauthor read is open**, even when a fix seems obvious. Apply it after the verdict (steward §3). +- **Keep the head frozen while a nonauthor read is open**, even when a fix seems obvious. Apply it after the verdict (steward §3). The one exception is a red head caused by this PR's own bytes. Then announce the fix on the PR, push only that fix and ask the reader to re-point to the new head (steward §4). A red check that is not this PR's leaves the head frozen. - **Update the PR body's disposition on every material change** (steward §2), and keep the lane's ledger in main#229 current. - **Stop following a PR** when it is merged or closed, or when Dylan says stop. diff --git a/.claude/skills/steward/SKILL.md b/.claude/skills/steward/SKILL.md index 005ff50fd..9c2e65eab 100644 --- a/.claude/skills/steward/SKILL.md +++ b/.claude/skills/steward/SKILL.md @@ -5,12 +5,20 @@ description: Math- conventions for driving a pull request to a mergeable state. # Steward: driving a Math- pull request -This skill summarizes rules that already bind this repository. It adds none. On any conflict, these sources win: -- [`AGENTS.md`](../../../AGENTS.md); -- `main` [`AGENTS.md`](https://github.com/d6g8k5htny-coder/main/blob/main/AGENTS.md); -- the [current workflow](https://github.com/d6g8k5htny-coder/main/blob/main/governance/OP-WORKFLOW-20260930.md); -- the [privacy rule](https://github.com/d6g8k5htny-coder/main/blob/main/governance/OP-PRIVACY-20260927.md); -- [`docs/FORMAL_REQUIRED_CHECKS.md`](../../../docs/FORMAL_REQUIRED_CHECKS.md). +This skill summarizes rules that already bind this repository. It adds none. On any conflict, the sources win. + +It was written against these exact source identities (repository, commit, path, git blob): + +| Source | Repository @ commit | Path | Git blob | +|---|---|---|---| +| Agent entry | Math- @ `61a67b5dffb5b0b7abe6f14bc96116c54b60ec0c` | [`AGENTS.md`](https://github.com/d6g8k5htny-coder/Math-/blob/61a67b5dffb5b0b7abe6f14bc96116c54b60ec0c/AGENTS.md) | `ca2f0fa247f7052c702de9b4f8e595226468c622` | +| Owner stop (historical) | Math- @ `61a67b5` | [`OWNER_STOP.md`](https://github.com/d6g8k5htny-coder/Math-/blob/61a67b5dffb5b0b7abe6f14bc96116c54b60ec0c/OWNER_STOP.md) | `234a579b64140068d28bb7081ce3c2fa9d5e5417` | +| Required-check contract | Math- @ `61a67b5` | [`docs/FORMAL_REQUIRED_CHECKS.md`](https://github.com/d6g8k5htny-coder/Math-/blob/61a67b5dffb5b0b7abe6f14bc96116c54b60ec0c/docs/FORMAL_REQUIRED_CHECKS.md) | `d4440638bc58134e4f1c941bad62203cba8eb37f` | +| Agent entry | main @ `9093629769f40db76f1311d8ee920d5a82a38b89` | [`AGENTS.md`](https://github.com/d6g8k5htny-coder/main/blob/9093629769f40db76f1311d8ee920d5a82a38b89/AGENTS.md) | `f649d88a8ecd9c6501d3137b5b330985e9c1f701` | +| Current workflow | main @ `9093629` | [`governance/OP-WORKFLOW-20260930.md`](https://github.com/d6g8k5htny-coder/main/blob/9093629769f40db76f1311d8ee920d5a82a38b89/governance/OP-WORKFLOW-20260930.md) | `1fdf548377769d3723a43dfb7f441175d930810d` | +| Privacy rule | main @ `9093629` | [`governance/OP-PRIVACY-20260927.md`](https://github.com/d6g8k5htny-coder/main/blob/9093629769f40db76f1311d8ee920d5a82a38b89/governance/OP-PRIVACY-20260927.md) | `dd7eca9ff36b19b07338d5ed0a6f1133d2075a81` | + +**Check the live versions too.** They are [Math- `AGENTS.md`](../../../AGENTS.md), [`docs/FORMAL_REQUIRED_CHECKS.md`](../../../docs/FORMAL_REQUIRED_CHECKS.md) and `main`'s [`governance/`](https://github.com/d6g8k5htny-coder/main/tree/main/governance). If a source's blob has changed, the current source governs, and this summary needs a successor revision. Cross-lane coordination (claims, ledgers, routing, releases) happens in [main#229](https://github.com/d6g8k5htny-coder/main/issues/229). @@ -49,7 +57,11 @@ Update it on every material change. Link evidence rather than copying it. A clos 5. **Optional and non-blocking points never start a push on their own.** - Reply once (stays as is and why, or rides a later push). - Carry the plainly correct ones into the next push that changes those files for another reason, or into a stacked successor PR. The reviewed head then stays the one the reads hashed. -6. **Changed reviewed bytes, dependencies or scope invalidate the affected review.** A base-only merge does not. It needs a bounded comparison (the packet bytes are identical to the reviewed head) plus fresh integration checks. +6. **Changed reviewed bytes, dependencies or scope invalidate the affected review.** A base-only merge carries a review forward only if a bounded comparison shows that the reviewed slice is unchanged. That slice covers: + - the packet bytes; + - every reviewed dependency (the imported or pinned sources it consumes, and its workflow). + + Fresh integration checks are also needed. If the base changed any reviewed dependency, the affected review needs a successor disposition, even when the packet directory is byte-identical. ## 4. Checks @@ -57,21 +69,31 @@ Update it on every material change. Link evidence rather than copying it. A clos **Packet checkers (Python standard library only).** - Run `python3 -B -S .py` and `python3 -B -O -S .py`. Their output must be byte-identical to each other and to the packet's `RESULTS.json`. -- Every mutant must be rejected, strictly: exit code 1 and `"passed": false`. +- Every mutant must be rejected exactly as that packet's workflow specifies. That always means exit code 1. Some packets also require a JSON `"passed": false`. Others print a plain failure message and check only the exit code, for example `frontiers/c2_exact_20261001` in `.github/workflows/c2-exact.yml`. Do not add a JSON requirement to a packet whose contract lacks one. - `SOURCE_FILES.json` records bytes, SHA-256 and git blob. Workflows check its `pins_on_main` against `main`. If `main` changes a pinned file, re-pin and refresh the record as an ordinary reviewed change. Never weaken the check. -**Lean packets** (`frontiers/cap_first_exit_lean_20261002/`, and `formal/` under its own contract): -- `python3 -B -S gate.py` in source mode; -- `python3 -B -S -m unittest test_gate` and the same with `-O`; -- `python3 gate.py --execute` with the pinned toolchain (`lake` on `PATH`). It builds fresh, replays with `leanchecker`, audits axioms (only `propext`, `Classical.choice` and `Quot.sound` are allowed) and runs three negative controls. All three must be REJECTED. +**Lean packets.** Each has its own recipe; use the one in its README and workflow. +- **The cap packet, `frontiers/cap_first_exit_lean_20261002/`**, run from that directory: + - `python3 -B -S gate.py` in source mode; + - `python3 -B -S -m unittest test_gate` and the same with `-O`; + - `python3 gate.py --execute` with the pinned toolchain (`lake` on `PATH`). It builds fresh, replays with `leanchecker`, audits axioms (only `propext`, `Classical.choice` and `Quot.sound` are allowed) and runs three negative controls. All three must be REJECTED. +- **`formal/`**, run from the repository root, as in [`formal/README.md`](../../../formal/README.md) and `.github/workflows/formal-lean.yml`: + - `python3 -m unittest discover -s formal/tests -v`, and the same with `-O`; + - its execute command, which runs **five** negative controls. After any change to a packet file, regenerate `MANIFEST.json` and run the source gate again. A kernel-checked build is engineering evidence. It is not an alignment review and not scientific acceptance. **Red CI on your PR is work now.** - Reproduce the failure, root-cause it, fix it in scope, validate locally and push. +- **If a nonauthor read is open when CI turns red**, a red head cannot merge, so the fix takes precedence over the freeze. But it is announced, not silent: + 1. post one comment on the PR naming the failing check, its root cause and the planned fix commit; + 2. push only that fix; + 3. ask the open reader to re-point to the new head, checking the `old..new` delta. + + If the failure is not this PR's (a check that is red on the base too, or an infrastructure loss before any test ran), the head stays frozen and the comment says so. - "Flake" is not a root cause. Re-run at most once, and only when the job died before any test body ran. - Never skip, disable or quarantine a test. Never push an empty commit. Never close and reopen a PR to restart CI. -- Some replays are long; the SIDE24 `d = 6` certificate replay takes about 25–45 minutes. Wait for it rather than re-running. +- Some certificate replays are long (tens of minutes). Check the job's earlier durations before treating it as stuck, and do not re-run a job that is still running. ## 5. Branches and pushes @@ -80,7 +102,7 @@ After any change to a packet file, regenerate `MANIFEST.json` and run the source - **Verify the remote head after every push** with `git ls-remote origin `. - **Stacked PRs.** When the lower PR merges: 1. merge `main` into the next branch with a merge commit; - 2. verify that the packet bytes equal the reviewed head (by diff over the packet directory and its workflow); + 2. verify by diff that the reviewed slice equals the reviewed head: the packet directory, its workflow, and every pinned or imported dependency it consumes (§3.6); 3. run the gates again and push; 4. post one comment stating the byte-identity, so the earlier review carries forward; 5. retarget the PR to `main` if GitHub has not done so already. @@ -92,7 +114,7 @@ Immediately before merging, read again: - the complete diff; - the latest reviews and unresolved threads; - ownership claims; -- the required checks at the exact head. +- the required checks for the current head/base pair. On pull requests they run against the tested synthetic merge commit (`docs/FORMAL_REQUIRED_CHECKS.md`), so a base change needs a fresh run. A result from an earlier head or base is not rebound. Merge with `expected_head_sha` and a merge commit. If the branch is behind, use a merge-commit update. Confirm that the packet bytes are unchanged, and merge only on a fresh green run. Do not bypass protection or simulate another identity's approval. Record an unexpected merge honestly. From 49ca8fb100104ea9fb0e53aaf2ed91894d5eda3e Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 4 Oct 2026 03:26:15 +0000 Subject: [PATCH 3/4] Skills: apply the A1-A9 AMEND of the #267 workflow read (5976137533) Verbatim replacement text from Grok Bot agent 14's verdict at 96b43b8: - A1: credit rule restated as the owner statement recorded in main#229 5974405061, with that comment's scope and conditions. - A2: line 8 states that lane practice is recorded, marked *(practice)*; markers added on the listed lines. - A3: review attribution per OP-WORKFLOW; "delegated AI work" marked as practice. - A4: integration-owner rule from OP-WORKFLOW; author-does-not-merge marked as practice. - A5: the head stays frozen when CI turns red during an open read; babysit lines 16-17 replaced accordingly. - A6: formal/ recipe names gate.py, --execute and its manifest. - A7: support-agent and no-restart rules cited to AGENTS.md; the 2026-09-27 stop is historical. - A8: checker, mutant and pins_on_main conventions tied to each packet's workflow, with examples. - A9: branch-update guards from OP-WORKFLOW "Integrate". Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .claude/skills/babysit/SKILL.md | 4 +-- .claude/skills/steward/SKILL.md | 52 +++++++++++++++------------------ 2 files changed, 26 insertions(+), 30 deletions(-) diff --git a/.claude/skills/babysit/SKILL.md b/.claude/skills/babysit/SKILL.md index f2c97e301..39a560122 100644 --- a/.claude/skills/babysit/SKILL.md +++ b/.claude/skills/babysit/SKILL.md @@ -13,7 +13,7 @@ Read [`../steward/SKILL.md`](../steward/SKILL.md) first. It holds this repositor - a recorded reason that nothing is yours to do, because the PR waits on a reviewer or an integrator. - **Address every unresolved thread.** Answer each one where it was raised, and resolve the threads you fixed. - **A failing test is never assumed to be an infra flake.** Reproduce it and root-cause it first (steward §4). -- **A green, mergeable head may wait on people. A red or conflicted head never waits.** -- **Keep the head frozen while a nonauthor read is open**, even when a fix seems obvious. Apply it after the verdict (steward §3). The one exception is a red head caused by this PR's own bytes. Then announce the fix on the PR, push only that fix and ask the reader to re-point to the new head (steward §4). A red check that is not this PR's leaves the head frozen. +- **A green, mergeable head may wait on people. A red or conflicted head never waits unattended:** fix it, or, while a nonauthor read is open, post its diagnosis (steward §4). +- **Keep the head frozen while a nonauthor read is open**, even when a fix seems obvious or CI is red. Apply it after the verdict, or earlier only if the reader releases the pickup or agrees to re-point (steward §3–§4). - **Update the PR body's disposition on every material change** (steward §2), and keep the lane's ledger in main#229 current. - **Stop following a PR** when it is merged or closed, or when Dylan says stop. diff --git a/.claude/skills/steward/SKILL.md b/.claude/skills/steward/SKILL.md index 9c2e65eab..353cd231d 100644 --- a/.claude/skills/steward/SKILL.md +++ b/.claude/skills/steward/SKILL.md @@ -5,7 +5,7 @@ description: Math- conventions for driving a pull request to a mergeable state. # Steward: driving a Math- pull request -This skill summarizes rules that already bind this repository. It adds none. On any conflict, the sources win. +This skill summarizes rules that bind this repository and records current lane practice from main#229 (for example main#229 5974405061: "The heads stay frozen while a read is open. I apply AMENDs only after the verdict is posted"). A statement tied to a source below restates that source. A statement marked *(practice)* records lane practice only and adds no rule. On any conflict, the sources win. It was written against these exact source identities (repository, commit, path, git blob): @@ -24,12 +24,12 @@ Cross-lane coordination (claims, ledgers, routing, releases) happens in [main#22 ## 1. Identity, roles and credit -- **One GitHub account carries every lane.** Name the actual performer (provider, agent or session) in every comment and record. The owner-facing attribution is "Dylan Roy — delegated AI work" (or "— delegated AI review"), followed immediately by the actual performer. -- **The author never approves or merges its own PR.** Integration is done by a non-author lane. The named integration owner controls branch refresh, readiness changes and the merge. +- **One GitHub account carries every lane.** Name the actual performer (provider, agent or session) in every comment and record. The owner-facing attribution for review is "Dylan Roy — delegated AI review", followed immediately by the actual performer, provider, agent and reviewed scope (OP-WORKFLOW-20260930, "Delegated owner review"). Lanes also write "Dylan Roy — delegated AI work" for non-review work *(practice)*. +- **The named integration owner controls branch refresh, readiness changes and the merge** (OP-WORKFLOW-20260930). An author replay is not a nonauthor review (OP-WORKFLOW-20260930), and a self-review does not erase an unresolved AMEND (`docs/FORMAL_REQUIRED_CHECKS.md`). *(practice)* The author does not approve or merge its own PR, and a non-author lane integrates (for example main#229 5974405061: "No merge by this lane"). - **Independence credit.** - - A same-provider read is useful technical work but earns zero organizational-independence credit. A Claude read does not count as the nonauthor read of a Claude-authored packet. - - Grok Bot agent reads count (owner ruling of 2026-10-03, main#229 comment 5974405061). The agreed performer line is "Grok Bot agent N (Grok Bot support agent; non-Claude, nonauthor lane)". -- **xAI/Grok and Cursor agents work here only as support**, at a lane's request ([`AGENTS.md`](../../../AGENTS.md)). Never restart stopped agents, timers or loops ([`OWNER_STOP.md`](../../../OWNER_STOP.md)). Cite only what such agents have published. + - A same-provider read is useful technical work but earns zero organizational-independence credit, and an author replay is not a nonauthor review ([OP-WORKFLOW-20260930](https://github.com/d6g8k5htny-coder/main/blob/9093629769f40db76f1311d8ee920d5a82a38b89/governance/OP-WORKFLOW-20260930.md), "Match verification to the change"). + - Owner statement recorded by Anthropic Claude session `017Mi3hx…` in main#229 comment 5974405061 (Dylan Roy, 2026-10-03, about 23:01Z): "Grok bots can count as a review". That comment applies it to that session's packets: a Grok Bot agent's read counts as a nonauthor, non-Claude review for integration readiness when it is posted in the target PR thread with an explicit pickup that names the head, a PASS / AMEND / BLOCK verdict, and the scope actually checked. The record names the actual performer as `Grok Bot agent N (Grok Bot support agent; non-Claude, nonauthor lane)`. Same-account organizational-independence credit stays 0. Claude reads of that session's packets still do not count. +- **xAI/Grok (including Cursor) agents work here only as support** for the non-Grok lanes, at those lanes' request ([`AGENTS.md`](../../../AGENTS.md)). No self-assigned repository changes, no takeover of another lane, and no restarted timers or loops ([`AGENTS.md`](../../../AGENTS.md); `main` [`AGENTS.md`](https://github.com/d6g8k5htny-coder/main/blob/9093629769f40db76f1311d8ee920d5a82a38b89/AGENTS.md)). The 2026-09-27 stop in [`OWNER_STOP.md`](../../../OWNER_STOP.md) is historical and lifted. Cite only what such agents have published. - **Never ask Dylan to re-approve autonomy he has already granted.** ## 2. The PR body is the disposition @@ -45,16 +45,16 @@ Update it on every material change. Link evidence rather than copying it. A clos ## 3. Reads, verdicts and AMENDs -1. **A read starts with a pickup comment** that names the PR, the slice and the exact head SHA. -2. **While a read is open, the head is frozen.** Push nothing to it, not even an optional nit, because that would stale the read. -3. **The verdict is PASS, AMEND (with the exact change) or BLOCK (with the reason)**, followed by the scope actually checked and what was not checked. -4. **Apply an AMEND only after its verdict is posted.** Then: +1. **A read starts with a pickup comment** *(practice)* that names the PR, the slice and the exact head SHA. +2. **While a read is open, the head is frozen.** *(practice)* Push nothing to it, not even an optional nit, because that would stale the read. +3. **The verdict is PASS, AMEND (with the exact change) or BLOCK (with the reason)** *(practice)*, followed by the scope actually checked and what was not checked. +4. **Apply an AMEND only after its verdict is posted.** *(practice)* Then: - push one commit that does exactly what the AMEND says; - reply on the PR, naming the commit; - request a byte-diff readback of `old-head..new-head`. A readback checks the delta, not the whole packet again. -5. **Optional and non-blocking points never start a push on their own.** +5. **Optional and non-blocking points never start a push on their own.** *(practice)* - Reply once (stays as is and why, or rides a later push). - Carry the plainly correct ones into the next push that changes those files for another reason, or into a stacked successor PR. The reviewed head then stays the one the reads hashed. 6. **Changed reviewed bytes, dependencies or scope invalidate the affected review.** A base-only merge carries a review forward only if a bounded comparison shows that the reviewed slice is unchanged. That slice covers: @@ -68,9 +68,9 @@ Update it on every material change. Link evidence rather than copying it. A clos **Required.** `math-downstream-gates` is the required aggregate. It depends on `downstream-replay` and `formal / formal-evidence` succeeding at the tested commit. Packet workflows add their own jobs, for example `certify-and-reject-mutants` for coefficient packets and `kernel-evidence` for the Lean cap packet. A missing, skipped, neutral or cancelled result is not success. Old receipts are never rebound to a new commit. **Packet checkers (Python standard library only).** -- Run `python3 -B -S .py` and `python3 -B -O -S .py`. Their output must be byte-identical to each other and to the packet's `RESULTS.json`. -- Every mutant must be rejected exactly as that packet's workflow specifies. That always means exit code 1. Some packets also require a JSON `"passed": false`. Others print a plain failure message and check only the exit code, for example `frontiers/c2_exact_20261001` in `.github/workflows/c2-exact.yml`. Do not add a JSON requirement to a packet whose contract lacks one. -- `SOURCE_FILES.json` records bytes, SHA-256 and git blob. Workflows check its `pins_on_main` against `main`. If `main` changes a pinned file, re-pin and refresh the record as an ordinary reviewed change. Never weaken the check. +- Run each checker exactly as its packet's workflow does. Many coefficient packets run `python3 -B -S .py` and `python3 -B -O -S .py` and require output byte-identical to each other and to the packet's `RESULTS.json` (for example `.github/workflows/c8-window-coefficient-planar.yml`); others use their own mode (for example `certificate.py --check` in `.github/workflows/c2-exact.yml`). +- Every mutant must be rejected exactly as that packet's workflow specifies (for example exit code 1 in `.github/workflows/c2-exact.yml` and `.github/workflows/c8-window-coefficient-planar.yml`). If a packet's workflow also requires a JSON `"passed": false`, require it there only; do not add a JSON requirement to a packet whose contract lacks one. +- Where a packet has `SOURCE_FILES.json` (bytes, SHA-256 and git blob), its workflow checks `pins_on_main` against `main` (for example `c6-tail-constant-certified.yml`, `c8-window-coefficient-planar.yml`). Other packets keep their own source records; follow the packet's workflow. If `main` changes a pinned file, re-pin and refresh the record as an ordinary reviewed change. Never weaken the check. **Lean packets.** Each has its own recipe; use the one in its README and workflow. - **The cap packet, `frontiers/cap_first_exit_lean_20261002/`**, run from that directory: @@ -79,28 +79,24 @@ Update it on every material change. Link evidence rather than copying it. A clos - `python3 gate.py --execute` with the pinned toolchain (`lake` on `PATH`). It builds fresh, replays with `leanchecker`, audits axioms (only `propext`, `Classical.choice` and `Quot.sound` are allowed) and runs three negative controls. All three must be REJECTED. - **`formal/`**, run from the repository root, as in [`formal/README.md`](../../../formal/README.md) and `.github/workflows/formal-lean.yml`: - `python3 -m unittest discover -s formal/tests -v`, and the same with `-O`; - - its execute command, which runs **five** negative controls. + - `python3 formal/gate.py` (source only, no Lean); + - `python3 formal/gate.py --execute` after `lake exe cache get` in `formal/`. It fails unless the pinned project builds, `leanchecker` rechecks the package, all 13 declarations have axiom reports restricted to `propext`, `Classical.choice` and `Quot.sound`, and five executable negative controls are rejected. -After any change to a packet file, regenerate `MANIFEST.json` and run the source gate again. A kernel-checked build is engineering evidence. It is not an alignment review and not scientific acceptance. +After any change to a packet file, update that package's manifest (`MANIFEST.json` for the cap packet, `formal/manifest.json` for `formal/`) as its gate requires and run the source gate again. A kernel-checked build is engineering evidence. It is not an alignment review and not scientific acceptance. **Red CI on your PR is work now.** - Reproduce the failure, root-cause it, fix it in scope, validate locally and push. -- **If a nonauthor read is open when CI turns red**, a red head cannot merge, so the fix takes precedence over the freeze. But it is announced, not silent: - 1. post one comment on the PR naming the failing check, its root cause and the planned fix commit; - 2. push only that fix; - 3. ask the open reader to re-point to the new head, checking the `old..new` delta. - - If the failure is not this PR's (a check that is red on the base too, or an infrastructure loss before any test ran), the head stays frozen and the comment says so. -- "Flake" is not a root cause. Re-run at most once, and only when the job died before any test body ran. -- Never skip, disable or quarantine a test. Never push an empty commit. Never close and reopen a PR to restart CI. +- **If a nonauthor read is open when CI turns red, the head stays frozen** (§3.2; main#229 5974405061: "The heads stay frozen while a read is open"). Post one comment on the PR naming the failing check, its root cause and the planned fix. Push the fix after the verdict is posted, or earlier only if the reader releases the pickup or agrees on the PR to re-point to the new head *(practice)*. A red head cannot merge in the meantime, so the freeze costs time, not correctness. +- "Flake" is not a root cause. *(practice)* Re-run at most once, and only when the job died before any test body ran. +- Never skip, disable or quarantine a test. *(practice)* Never push an empty commit. Never close and reopen a PR to restart CI. - Some certificate replays are long (tens of minutes). Check the job's earlier durations before treating it as stuck, and do not re-run a job that is still running. ## 5. Branches and pushes -- **Merge commits only.** No rebase, no amend, and no force-push on a reviewed or shared branch. +- **Merge commits only.** *(practice)* No rebase, no amend, and no force-push on a reviewed or shared branch. - **Change another owner's branch only after an explicit scoped handoff, a release, or a confirmed lease expiry**, followed by a check of its current state. -- **Verify the remote head after every push** with `git ls-remote origin `. -- **Stacked PRs.** When the lower PR merges: +- **Verify the remote head after every push** *(practice)* with `git ls-remote origin `. +- **Stacked PRs.** *(practice)* When the lower PR merges: 1. merge `main` into the next branch with a merge commit; 2. verify by diff that the reviewed slice equals the reviewed head: the packet directory, its workflow, and every pinned or imported dependency it consumes (§3.6); 3. run the gates again and push; @@ -116,7 +112,7 @@ Immediately before merging, read again: - ownership claims; - the required checks for the current head/base pair. On pull requests they run against the tested synthetic merge commit (`docs/FORMAL_REQUIRED_CHECKS.md`), so a base change needs a fresh run. A result from an earlier head or base is not rebound. -Merge with `expected_head_sha` and a merge commit. If the branch is behind, use a merge-commit update. Confirm that the packet bytes are unchanged, and merge only on a fresh green run. Do not bypass protection or simulate another identity's approval. Record an unexpected merge honestly. +Merge with `expected_head_sha` and a merge commit *(practice)*. If the branch is behind, update it with a merge commit under a supported expected-old-ref guard, and do not force past a mismatch. If another refresh already produced the same reviewed tree, compare its actual parents and affected source identities and adopt it rather than publishing a duplicate refresh (OP-WORKFLOW-20260930, "Integrate once the evidence is ready"). Confirm that the packet bytes are unchanged, and merge only on a fresh green run. Unresolved engineering AMENDs survive peer merges. Do not bypass protection or simulate another identity's approval. Record an unexpected merge honestly. ## 7. Never in a packet PR From aa67388c8a06fa5546fa27a6643b84b9f39e1059 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 4 Oct 2026 03:38:37 +0000 Subject: [PATCH 4/4] steward: apply INT-267-01 (per-packet source-record contracts) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the steward §4 bullet that generalized `pins_on_main` to every packet with SOURCE_FILES.json. The new text uses the readback's wording verbatim (OpenAI/Codex, Math-#267 comment 5976220298). Some workflows validate `pins_on_main`; others validate SOURCE_MAP.json entries marked `current_required` (c6-hard-direction-factorization.yml). Both validate on the checked-out tested tree, not against `main`. Documentation only; no other line changes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .claude/skills/steward/SKILL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.claude/skills/steward/SKILL.md b/.claude/skills/steward/SKILL.md index 353cd231d..627a4e7fd 100644 --- a/.claude/skills/steward/SKILL.md +++ b/.claude/skills/steward/SKILL.md @@ -70,7 +70,7 @@ Update it on every material change. Link evidence rather than copying it. A clos **Packet checkers (Python standard library only).** - Run each checker exactly as its packet's workflow does. Many coefficient packets run `python3 -B -S .py` and `python3 -B -O -S .py` and require output byte-identical to each other and to the packet's `RESULTS.json` (for example `.github/workflows/c8-window-coefficient-planar.yml`); others use their own mode (for example `certificate.py --check` in `.github/workflows/c2-exact.yml`). - Every mutant must be rejected exactly as that packet's workflow specifies (for example exit code 1 in `.github/workflows/c2-exact.yml` and `.github/workflows/c8-window-coefficient-planar.yml`). If a packet's workflow also requires a JSON `"passed": false`, require it there only; do not add a JSON requirement to a packet whose contract lacks one. -- Where a packet has `SOURCE_FILES.json` (bytes, SHA-256 and git blob), its workflow checks `pins_on_main` against `main` (for example `c6-tail-constant-certified.yml`, `c8-window-coefficient-planar.yml`). Other packets keep their own source records; follow the packet's workflow. If `main` changes a pinned file, re-pin and refresh the record as an ordinary reviewed change. Never weaken the check. +- Follow each packet's actual source-record contract. Some workflows validate `pins_on_main` (for example `c6-tail-constant-certified.yml` and `c8-window-coefficient-planar.yml`); others validate `SOURCE_MAP.json` entries marked `current_required` (for example `c6-hard-direction-factorization.yml`). These checks validate the pinned identities on the checked-out tested tree. If a consumed source changes, reconcile its identity and reviewed dependency scope, then refresh the record as an ordinary reviewed change. Never weaken the check. **Lean packets.** Each has its own recipe; use the one in its README and workflow. - **The cap packet, `frontiers/cap_first_exit_lean_20261002/`**, run from that directory: