Repository navigation
proofs: ledger repairs, PWG census, T-1 recheck legs (PWG-2ii), T-2/T-3 split - #171
Conversation
…cone The grade records were written against the mathesis brief on 2026-11-01, before the owner ruling of 2026-11-04 made PROOF-POLICY §8 normative: - The five theory rows (G-1, T-1, T-2, T-3, E-1m) are PWG-3, written with the prefix. The brief's "2ii needs Isabelle/HOL" is replaced by §8.3's +foundation-diverse tag. - The receipt is the current green agda-proofs run 42076969251 at 23bc8c3, covering all three modules under the §2.1 canonical invocation, with library pin, flags, import cone and axioms recorded. Runs 41687715055 and 40867211509 are kept as state: superseded. The page had still cited the pre-flag receipt it said it would replace. - The duplicated row counts, which had drifted (23 against 27 TESTED), are removed from PROOF-GRADES; PROOF-NEEDS stays the only count. - Rust's verifiers read Creusot/Pearlite and Verus (§1.2, 2026-11-07). §8.4 asks for a comment-aware postulate scan of the import cone beside --safe. scripts/scan-postulates.sh does that, and check-agda.sh runs it on the proofs and the pinned resource-algebra sibling with a negative and a positive control written at run time. Verified locally: cone 10 files, 0 postulates; a mutant scan that reports nothing fails the gate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 14 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
…comments Stacked on #170, which records the theory grades as PROOF-POLICY §8 PWG-3 and adds the postulate scan. This adds what #170 does not cover. The ledger lost #168's T-8 and T-9 rows: main still showed T-8 OPEN ("not yet built") although its five tests are green in CI and locally, and T-9 existed only in prose. T-8 now has one TESTED row per test, T-9 is an OPEN row in both tables, and E-1m gains its missing status-table row so the two tables agree. A PWG census with its denominator (§8.4.7): PWG-3 5 of 6 theory theorems, G-3 ungraded. The Rocq and Lean legs are recorded as not attempted (OPEN) rather than `unavailable`: under §2 that route means a leg that cannot be built, and a hand re-proof is always the fallback. Two proof files had misleading comments, though no statement or proof changed. TransactionAtomicity's "What is NOT claimed" block described non-atomic saves and a non-resumable rollback, both since fixed (T-4, T-5, T-8). Reversibility implied that the 𝟙 grade of a wrap/unwrap pair derives from its cancellation law; the grade is assigned. The G-1 and E-1m wording now says so, and the receipt notes the re-earn. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
b905794 to
a71dc76
Compare
hyperpolymath
changed the title
…e-run Review on #170 (Codex, CodeRabbit), each finding checked: - The cone is now the module set `agda --dependency-graph` reports for the three roots, resolved to files on the include path and in Agda's own library; an unresolved module fails the gate. The directory scan both missed the 8 prover-supplied modules and swept in unimported ones. - First-party modules (6) must have no postulate. Agda.Primitive's universe-level primitives (Level, lzero, lsuc, _⊔_, bound by BUILTIN) are reported as the prover's trusted base; a postulate in any other prover-supplied module fails. - The scanner takes explicit files, refuses unreadable ones, and lexes `--` comments with no space, and string and character literals. - Controls must exit exactly 0 and 1, and the planted one must be named. - Run 42076969251 predates the changed gate, so it is recorded as the last receipt for the modules; the first green run of this gate on main replaces it. - The stale "23 TESTED" is gone; Rust guidance names Creusot/Pearlite and Verus throughout. Verified locally: gate OK (6 first-party, 0 postulates; 2 BUILTIN blocks in Agda.Primitive); a never-reporting scanner, a comment-blind scanner and a planted postulate in Epistemic.agda each fail the gate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg
agda-proofs.yml run 42623188471 at a71dc76 checked the edited Reversibility and TransactionAtomicity bytes under the same gate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5f123b947e
ℹ️ 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".
…y name The scanner treated only space and tab as keyword boundaries, so a postulate next to NO-BREAK SPACE, a Unicode space separator, CR, FF or VT went unreported. Agda reads every isSpace character other than tab and newline as a space (Agda.Syntax.Parser.Alex, toASCII); the scanner now does the same, byte-wise in the C locale so mawk and gawk agree. The planted control gains a NO-BREAK SPACE case, and the comments-only control `--postulate postulate`. The prover-supplied allowance was the path Agda/Primitive.agda. The gate now requires those blocks to declare exactly Level, lzero, lsuc and _⊔_, each with its BUILTIN binding, so a prover pin that adds a postulate fails. PROOF-NEEDS states the PWG-3 grade as pending its re-run receipt, and PROOF-GRADES cites the green branch run of the changed gate as evidence. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg
- E-1m: state rotation's premise old ≠ new (rotate-forgets-old needs it; with old = new the key stays usable). - TransactionAtomicity comment: a failed metadata append keeps its record, and no failure after the temporary file exists is injected, so the failed-save summary no longer overgeneralises. - T-9's artefact is operations.rs, where execute appends after the file change and undo marks after the inverse. - G-3 names this repository's FFI bridge, so PROOF-POLICY §1 makes it engineering: the PWG census is 5 of 5, with no ungraded theory row. T-2 and T-3 are flagged as the same open classification question. - Per-leg records (§8.5) for the Agda, Rocq and Lean legs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: dcaac10613
ℹ️ 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".
…gda does
A block comment was removed without leaving a token boundary, so
`postulate{- c -}X : Set`, which Agda reads as a postulate, became
`postulateX` and was not reported; in Agda.Primitive it would also have slipped
past the name check. A comment now leaves a space behind.
A pragma was scanned as code, so a FOREIGN payload using `postulate` as a
Haskell name failed the gate, and a payload holding `{- {-` opened a comment
Agda never sees, hiding a postulate after the pragma. Agda does not nest
comments inside a pragma and closes it at a `#-}` token (Lexer.x); the scan
now skips to the first `#-}`, which can end a pragma early but never late.
Controls: the comments-only file gains a FOREIGN payload; the planted file
gains the comment-separated and after-pragma cases, and must name lines 2-5.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg
…to claude/vibrant-cori-lirqrr
#170 now records its gate change as "PWG-3, receipt pending re-run". The comment edits here are covered by the same first green run on main. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9eb9f5f0d7
ℹ️ 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".
The PROOF-POLICY §2 pilot. Transport is not available: Agda2Dedukti was
last changed in January 2022, builds against a forked Agda branch of
that period, and cannot read modules checked by the pinned Agda 2.6.4.3.
So both legs are re-proved by hand, in core Rocq 8.18 and core Lean
4.35.0 (no Mathlib, no imports).
- verification/proofs/{rocq,lean}/Rollback: rollback_restores, with
Print Assumptions / #print axioms showing no axioms.
- tests/reject-{rocq,lean}/ForwardRollback: twins of the Agda fixture.
Undoing real double and increment operations in execution order is
refused, each with the message the fixture names.
- scripts/check-recheck.sh (just test-recheck): fails on a leg that does
not check, on any axiom, on an accepted fixture, and on a fixture
refused for another reason. Mutants with Admitted and sorry are caught.
- agda-proofs.yml gains a recheck job on ubuntu-24.04 with
coq=8.18.0+dfsg-1build2 and the Lean 4.35.0 tarball checked by
SHA-256. It sits in the same workflow so actions.lock is unchanged.
- PROOF-GRADES records the §2.2 statement comparison and the residual
logic differences. The census is now PWG-3 4, PWG-2ii 1 (T-1).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
PROOF-POLICY §1 puts a statement that names one repository's types in engineering. T-2 and T-3 were stated over a model of januskey's TransactionManager, so, per the owner's ruling, they are split: - SingleActiveLog.agda (new, builtins only) proves the invariant for any record type with a decidable key and an active or settled phase, under three transitions: open a fresh active record, a key- and phase-preserving edit, and a settling transition. finish-good needs only the settling law, not key preservation. These are T-2 and T-3, now theory. - TransactionAtomicity Part B is januskey's instance. Tx is keyed by id, its phase comes from its state, and begin, add_operation, commit and mark_rolled_back are the abstract transitions. Every theorem name the ledger, fixtures and docs cite is kept as a corollary. - T-10 (new, OPEN, engineering): the Rust TransactionManager refines the abstract log, for Creusot or Verus. - tests/reject-agda/SettleWithoutSettling.agda pins finish-good's settling premise. With an identity "finish", one record stays active with no pointer, and the claim that the count is 0 is refused with 1 != 0. Its true counterpart checks. - check-agda.sh gains the fourth root, and its warning counts are updated. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
hyperpolymath
changed the title
…irqrr # Conflicts: # PROOF-NEEDS.adoc # docs/theory/PROOF-GRADES.adoc # scripts/check-agda.sh
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
…r download check-recheck.sh compiled each Rocq rejection fixture in place, so coqc's .glob and .aux files were committed next to the fixture. They are removed and ignored, and fixtures are now compiled from a copy in the gate's temporary directory. The Lean download is restricted to HTTPS with TLS 1.2 or later, so a redirect cannot downgrade it. The SHA-256 check still runs before unpacking. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
…sync None of the named tests observes sync_all: removing it would leave every failed-save, hard-link, temporary-file and retry assertion green. Both rows now claim what the tests show, which is that the log is replaced by rename and never overwritten in place. They say the sync before the rename is there by construction only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f73046b649
ℹ️ 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".
- STATE: claimed-higher now records T-1 at PWG-2ii; it still said none. - PROOF-GRADES: T-1's Agda module imports the sibling's prelude. The comparison now accounts for the three things Rollback uses from it (builtin _≡_, trans, cong) instead of calling T-1 sibling-free. - PROOF-GRADES: full input digests, with check-recheck.sh's current 5171d9d2… replacing the stale be20e857…. - wiki rmr-primitive: T-8 is TESTED (the log itself) and T-9 is OPEN (a file change and its record are not written together). T-2/T-3 are abstract, T-10 is added, and T-5's fsync is noted as by construction. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 99770a3d30
ℹ️ 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".
…o stale PWG text - T-9 was two failure modes. The forward window (execute changes the filesystem, then appends) can leave a change with no record, which needs write-ahead intent. Undo is different: every helper records the inverse as its own operation via execute before mark_undone, so a failed mark leaves the original unmarked and a retry re-applies the inverse. That is T-11 (OPEN), and its fix is an idempotent undo. The ledger, PROOF-GRADES and the RMR wiki are updated. - Axiom-free Rocq has neither K nor UIP. Only Lean's proof-irrelevant Prop adds UIP, so the residual-differences note now says so. - Two passages still said no row is above PWG-3. They now name T-1 at PWG-2ii. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3716998f70
ℹ️ 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".
READINESS still said all five were PWG-3, contradicting the census in PROOF-NEEDS and PROOF-GRADES. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX
|
…rry forward only what is new #170 and #171 landed the PWG records, the import-cone postulate scan, the restored T-8/T-9 rows and the T-1 recheck legs while #172 was in review. In every overlapping file this merge takes main's version, and it removes #172's scripts/agda-cone.sh, which duplicated scripts/scan-postulates.sh. What #172 still adds on top of main: - T-12 (TESTED): TransactionManager::new refuses a log read from disk that breaks Good, and the unused active_mut is removed. T-10 (the refinement itself) stays OPEN; T-12 is evidence for it at the load boundary. - Dashboard: Agda 2.6.4.3 from agda-proofs.yml's pinned image. #171 listed this as left undone. The "two pins" obligation is marked resolved. - Owner decisions of 2026-11-09, recorded on T-5 (the directory fsync stays best-effort) and T-9 (to be closed with a write-ahead intent log). - E-1m: a note that adversary-ignorant and obliterate-ignorance are proved for two particular worlds. - Test count 143. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
…pin across CI (#172) ## Scope after merging `main` While this PR was in review, #170 and #171 landed most of its original content, more thoroughly in places: - the PWG records and per-leg records; - the import-cone postulate scan (`scripts/scan-postulates.sh`); - the restored T-8 and T-9 rows; - the T-1 Rocq and Lean legs (`PWG-2ii`); - the T-2/T-3 split into `SingleActiveLog`. The merge commit takes `main`'s version of every overlapping file and removes this PR's duplicate `scripts/agda-cone.sh`. Four things remain, on top of `main`. ### 1. T-12 (TESTED): a loaded log satisfies the invariant `Good` T-2 and T-3 take `Good` as a premise. Before this change, `TransactionManager::new` loaded any log that parsed, so a hand-edited or foreign log could start the Rust outside the invariant. A public, unused `active_mut` could also change a transaction outside the four transitions. - **Change:** a log that breaks `Good` is now refused with `MetadataCorrupted`, and `active_mut` is removed. - **Tests:** - `a_loaded_log_that_breaks_the_invariant_is_refused` covers five ways of breaking `Good`: a pointer to a missing transaction, a pointer to a settled one, an Active transaction with no pointer, two Active transactions, and a settled first transaction with the active id. - `a_log_the_manager_wrote_loads_back` covers idle and busy logs as the positive control. - Three mutants each fail the first test: no check at load, last-with-id instead of first, and no stray-Active scan. Each mutant was confirmed applied with `cmp`. - **Ledger:** this is evidence for T-10 at the load boundary. The refinement itself, T-10, stays OPEN for Creusot or Verus. ### 2. One Agda version across CI (owner decision 2026-11-09) #170 and #171 both listed this as not done. `dashboard-check.yml` used to install Ubuntu's Agda 2.6.3. The job now runs on the host, and `agda` and `idris2` on PATH are wrappers around the images the proof jobs already pin: - `debian:trixie-slim@sha256:a29215f6…` with `agda-bin=2.6.4.3-1+b2`; - `idris2-pack@sha256:f0758996…`. It asserts `Agda version 2.6.4.3` exactly as `agda-proofs.yml` does. Agda runs as the runner user. idris2 runs as root, because its toolchain is under `/root`, and the wrapper hands back any root-owned file it leaves, so `check-idris-reject.sh` can still delete its scratch copy. The "two pins" obligation in `PROOF-GRADES.adoc` and `STATE.a2ml` is marked resolved. On the pre-merge head 59f1d15 this job ran green, with every Idris2 and Agda row proven through the wrappers. ### 3. Owner decisions recorded (2026-11-09) - **T-5:** the directory fsync after the rename stays best-effort. - **T-9:** to be closed with a write-ahead intent log. Not built yet; still OPEN. ### 4. Design-review note E-1m's `adversary-ignorant` and `obliterate-ignorance` are proved for two particular worlds. The general form is `different-store-unknown`. The other two findings from the review were already on `main`: `wrap-unwrap-𝟙` and `rotate-forgets-old` hold by definition. The test count is now 143. ## Verification (local, on the merged tree) - `cargo fmt --check` and `clippy -D warnings`: clean. - `cargo test --workspace --locked`: 143 pass. - Aspect tests: 32 pass. - `scripts/check-agda.sh`: OK. - `dashboard-check`: the only divergences are the 10 Idris2 rows, because `idris2` isn't installed in this sandbox. CI runs them. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
What
This was stacked on #170, which is now merged; it now targets
main. No previously proved statement is weakened. One statement is generalised: T-2 and T-3 move from the transaction model to an abstract log.1. Ledger repairs.
main; they are restored. T-9's artefact isoperations.rs.TransactionAtomicity.agdaandReversibility.agdano longer describe since-fixed bugs or imply a derived grade.old ≠ newpremise.2. PWG census and leg records (PROOF-POLICY §8.4.7, §8.5).
unavailable.3. T-1 recheck legs:
PWG-2ii(PROOF-POLICY §2).docs/theory/PROOF-GRADES.adoc.ForwardRollbackpin non-vacuity.scripts/check-recheck.shfails on any axiom, on an accepted fixture, and on a fixture refused for another reason. Mutants withAdmittedandsorryare caught.agda-proofs.yml→ "Rocq and Lean recheck legs".coq=8.18.0+dfsg-1build2onubuntu-24.04.actions.lockis unchanged.4. T-2/T-3 split (owner ruling).
SingleActiveLog.agda(new, builtins only) proves the invariant for any record type with a decidable key and an active or settled phase. This is theory.finish-goodneeds only the settling law.TransactionAtomicityPart B is now januskey's instance. Every cited theorem name is kept.tests/reject-agda/SettleWithoutSettling.agdapins the settling premise: it is refused with1 != 0, and its true counterpart checks.Census after this PR:
PWG-34 (G-1, T-2, T-3, E-1m) ·PWG-2ii1 (T-1) ·PWG-2i0 ·PWG-10 ·ungraded0.Verification (local)
dashboard-check: OK.Not in this PR
🤖 Generated with Claude Code
https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX