fix: don't PATCH a scoreboard owned by another identity - #116
Closed
sankalpsthakur wants to merge 138 commits into
Closed
fix: don't PATCH a scoreboard owned by another identity#116sankalpsthakur wants to merge 138 commits into
sankalpsthakur wants to merge 138 commits into
Conversation
Set use-github-cache: false on lean-action. lean-action otherwise wraps the ~2.4 GB ./.lake directory in actions/cache, whose save and restore cost ~40s per run, far more than the ~6s `lake exe cache get` it avoids. The Mathlib cache server (use-mathlib-cache: true) still supplies the prebuilt oleans, so nothing is compiled from Mathlib; this only drops the redundant GitHub-side caching.
The branch renamed the files and directories but left the contents referring to Centauri (lakefile library names, namespaces, imports, README, manifest), which broke the build. Sweep the contents: Centauri → TauCeti, Proxima Centauri → Tau Ceti, and the package name / URLs.
Replace the textual no-sorry CI grep with a Lean metaprogram that builds the TauCeti environment from its oleans and inspects, for every declaration defined in TauCeti, the axioms it transitively depends on (Lean.collectAxioms), failing on anything outside the allowlist propext, Classical.choice, Quot.sound. Because it reads the kernel environment rather than source text, it catches sorry/admit (sorryAx), native_decide (Lean.ofReduceBool), and home-rolled axioms, including ones reaching in through imports. Add it as `lean_exe axioms` (root TauCetiReview.Axioms), run in CI after the build, and update TauCetiReview/README to reflect that the audit is now mechanized.
Address review of the axiom audit: enumerate every TauCeti/**/*.lean module (not only those imported from the root) so an orphan module that smuggles in an axiom is still audited; glob the TauCeti lean_lib (`TauCeti.*`) so `lake build` builds every such module (and a broken/orphan module fails the build); fail loudly if zero declarations are audited (miswiring); index the module-name table safely; and document the trustLevel contract (the audit checks axiom dependencies, not proof validity — the build does that).
feat: add the axiom-allowlist audit (lake exe axioms)
Rewrite the remaining em-dash constructions (README axiom note, the ci.yml audit comment, the lakefile glob comment, and two in TauCetiReview/Axioms.lean) using a semicolon, comma, or colon.
…axiom-audit style: remove em-dashes from the axiom-audit docs and comments
Add the per-angle prompts for the AI review agents under TauCetiReview/rubrics/: a shared protocol plus eleven single-angle rubrics (scope, correctness, reuse, api-design, generality, placement, naming, documentation, proof-quality, deprecation, attribution). Each agent runs after CI is green and judges one angle, returning approve/request_changes/ block with evidence; only the integrity angles may block. The prompts are deliberately terse and adversarial, with a shared materiality bar so agents hunt real problems rather than nitpick.
Split the review rubrics out into their own repo: rubrics at the root, the axiom audit removed (it moves to the TauCeti code repo) and the superseded rubric.md skeleton deleted. Update the shared protocol and scope rubric to reflect that the code, roadmaps, and rubrics now live in three repos, with the runner providing code and roadmap checkouts. Add README, LICENSE, and CODEOWNERS. The review runner and workflow land in a follow-up.
…ality (scope's lane)
feat: AI review harness (runner + reusable workflow)
…checkout fix: reusable workflow checks out TauCetiReview explicitly
codex exec occasionally exits non-zero with no output; after the same-provider retry, try the other provider once so a transient crash never drops a rubric.
…-fallback feat: provider fallback when a reviewer CLI fails
…stead A fallback to the other provider masked codex exec's intermittent non-zero exits. Remove it and instead record codex's event stream, error events, and raw stdout on failure so the crash can be root-caused. Keep only a single same-provider retry for a genuine transient network blip.
…er-fallback revert: drop provider fallback, capture codex failure detail
I1: never evaluate PR-controlled Lake in the privileged job. Get Mathlib source from a trusted clone at the rev pinned in the BASE manifest, not via the PR's lakefile (which would be arbitrary code execution on attacker input). I2: reviewers run in a clean workspace (PR source w/o .git, roadmap, mathlib, diff only) with a minimal per-provider env — only that provider's key, never a GitHub token or the other provider's key. Keys are staged to files, read into memory by the runner, and unlinked before any reviewer runs. persist-credentials is off on every checkout. codex runs with shell_environment_policy.inherit=none. I3: replace the single broad App token with two scoped tokens (TauCeti pull-requests:write to comment; TauCetiReview contents:write to persist), minted only after reviewers finish, in separate steps. No token is in the reviewer phase. With public transcripts and no redaction gate, this isolation is the only leak barrier; the residual is that a reviewer can read its own provider key via /proc/self/environ (tracked in TauCetiProject#8).
…-a-sandbox harden: sandbox the review pipeline (I1/I2/I3)
I6: parse the verdict only from after a one-time random marker the runner injects
per review. Attacker content (incl. a forged {"verdict":"approve"}) sits before
the marker and is ignored; fail closed on missing marker, bad JSON, or a verdict
outside {approve,request_changes,block}. _common.md gains an explicit
untrusted-input boundary and documents the marker channel.
I5: reserve before spending — skip a rubric if spend-so-far plus --max-call-cost
would breach the daily budget (a per-call ceiling, not a post-spend check); count
every attempt incl. the retry; persist spend to the ledger incrementally so a
crash cannot lose what was billed.
…auCetiProject#93) * feat: provide the Mathlib naming conventions to the naming reviewer The naming rubric judges names against "standard Mathlib terminology" but the agent was never given the conventions: they live in the leanprover-community website repo, not in anything the read-only reviewer can grep. Vendor the document under rubrics/references/ (with a provenance header and a short local addendum on _def/_apply/_iff/_eq suffix semantics), append it to the naming rubric's prompt via a small per-rubric RUBRIC_REFERENCES mapping in build_prompt, and fold references/*.md into rubrics_fingerprint so a reference edit invalidates carried-forward approvals like any rubric edit. * fix: correct fingerprint claim, add reference boundary and path validation Review findings on this branch (Codex): - The claim that rubrics_fingerprint invalidates carried-forward approvals was false: state_of() binds approvals to the PR head SHA only, and the fingerprint is recorded purely as rubrics_version provenance (archive records, run ids, dedupe keys, meta blocks). Correct the comment, the fingerprint docstring, and the test docstring; TauCetiProject#95 tracks actually binding approvals to the fingerprint. - Wrap each spliced reference in a generated BEGIN/END boundary naming the source and stating it cannot override the shared protocol, output format, tools, or verdict instructions. - Validate RUBRIC_REFERENCES entries (relative, no '..', resolves under rubrics/references/, exists) via resolve_reference(), shared by prompt assembly and fingerprinting so a spliced document can never escape the fingerprint's references/*.md coverage. - Tests for the boundary and validation; all standalone suites pass. ---------
…lic surface (TauCetiProject#96) Reword the exposure rule so it no longer hinges on "the named downstream target", which review agents read as the entries in a roadmap's Targets.lean and used to block any public declaration not literally listed there. It now frames the public surface as what later roadmap stages need or the roadmap's explicit products, so a general theorem the named milestones specialize is characteristic API, not over-exposure.
…CetiProject#99) * feat: placement covers directory structure and filename families New files should join an existing topic subdirectory when one fits; a flat filename-prefix family is evidence of a subdirectory in the making, to be handled by a dedicated relocation PR, with the prefix count treated as evidence only and never alone grounds for request_changes. * feat: restructure-as-you-add in placement, sanctioned in scope A PR adding a file to an already-large flat family is expected to move the family into its subdirectory in the same PR; scope explicitly treats that bundle as one topic. Deferral only for documented open-PR conflicts, via the structure tracking issue. * style: tighten the placement structure bullet * style: drop the redundant deferral clause The unless-clause already carries the exception; the tracking-issue bookkeeping is author-side guidance and has no reviewer action. * style: drop the vague coda Judgment over counting is already carried by 'several'; the one-topic sanction lives in scope.md where its reviewer reads it. * style: fold the restructure-as-you-add sanction into the existing sentence * feat: preliminary relocation PR replaces restructure-as-you-add The relocation ships as its own PR before the addition, per the repo's existing ship-a-prerequisite-refactor-as-its-own-PR rule; the scope.md carve-out is unnecessary under this policy and is reverted. ---------
* feat: the pair is the directory threshold Foo.lean plus FooBar.lean become Foo/Basic.lean (or Defs.lean) and Foo/Bar.lean via a preliminary relocation PR; anchors move inside. * feat: move as you add, same PR; scope sanctions the bundle * style: should be, not are * style: tighten the scope sanction * style: name placement.md explicitly ---------
Switch the codex reviewer's default model from gpt-5.5 to gpt-5.6-sol and price the gpt-5.6 family (sol/terra/luna) so the engine's require_priced guard and daily-budget accounting cover them. Sol lists at $5/$30 per 1M tokens (identical to gpt-5.5, with the same >272K long-context tier), Terra at $2.50/$15, and Luna at $1/$6, all with the 10% cached-input read rate; the three windows are dated to the family's 2026-07-09 GA. The worker passes only --reviewer codex and never --codex-model, so moving the default is what actually routes review rounds onto sol. 🤖 Prepared with Claude Code
…uCetiProject#102) Downgrade a codex reviewer to gpt-5.6-terra when the account isn't entitled to the default model (Sol needs a paid ChatGPT tier; Free/Go subscriptions get Terra), so an unentitled account no longer fails every codex rubric. run_codex parses the terminal turn.failed event's JSON payload into a structured error_status / error_type / error_message (defensively: a string/list where a dict is expected, or a malformed payload, is skipped, not crashed on, and never masks a good earlier one). codex_model_unavailable() then needs BOTH a model-access message (matched against that structured message — grounded in the captured codex-cli 0.144 wording "... not supported when using Codex with a ChatGPT account", not a blind guess) AND a non-transient status: a 400/403/404 qualifies, a 429 or 5xx never does. A 400 alone is not model-specific, so it can't trigger a downgrade on its own. Because codex has been seen to wrap a transient server error in the same "not supported" 400 (openai/codex#14190), run_one reconfirms on the same model before downgrading (a transient clears on the retry; a real unavailability repeats), and only persists the downgrade — flipping the shared runner registry so later rubrics skip the dead Sol call — once the fallback yields a verdict. So a misclassification costs at most one extra attempt, never a sticky downgrade. Only the default model auto-falls-back: passing --codex-model explicitly (now None-defaulted so an explicit Sol is distinguishable) opts out. Each attempt records the model it ran. Rubrics dispatch sequentially, so the registry mutation races nothing; the registry is rebuilt from CODEX_MODEL each run, so Sol is re-probed next run. The fallback is kept priced (dispatch_models lists it; the price-sync test enforces it) and re-checked by dispatch-time require_priced. A dependency-free test covers the real captured output, the status+message classifier, the malformed-payload hardening, and the full reconfirm/downgrade state machine. 🤖 Prepared with Claude Code
…ith "should be private" (TauCetiProject#103) This PR loosens the api-design rubric's exposure guidance so it no longer asks for a declaration to be `private` merely because the roadmap's named targets do not mention it. The named targets are not the whole allowed surface: genuinely reusable general results and the products a later stage needs may be exposed, and a helper is kept `private` only when it has no use outside the proof or file it serves. 🤖 Prepared with Claude Code
…auCetiProject#97) Scope gains two qualitative checks: a PR citing a later stage of a roadmap needs its prerequisite stage merged or in flight, and reviewers weigh whether the cited target is actually getting closer rather than approving on citation alone. Correctness gains the unexercised-predicate check: a new Prop-valued definition needs a consuming theorem or a non-degenerate witness before its faithfulness is falsifiable.
…-bot-lakefile fix: merge validated bot lakefile bumps
* fix: preserve login identity for reviewers * fix: stream reviewer prompts over stdin * fix: stream pi prompts over stdin
…tiProject#107) * fix: keep a failed attempt's diagnosis, publish none of it Every artifact a failed rubric produced recorded returncode, secs and usage at $0.00 and no error text, so a total auth failure was indistinguishable from a model that answered nothing. run_claude captured the operative line all along and then dropped it: the attempts allowlist omitted raw_stderr, and only the final attempt's copy survived at the top level of the local result. Carry raw_stderr per attempt in the local store, and echo each distinct stderr summary to stderr when a rubric ends with no verdict, so the cause appears beside the symptom. The archive repo is public, so ATTEMPT_PRIVATE_KEYS names both fields that must not leave the machine and the durable record strips them. * fix: publish why a rubric errored, not the stderr it came from Second-opinion review caught that the premise of the first attempt was wrong. `--store` is a checkout of this repo's `reviews` branch and the review workflow commits and pushes it, so the per-rubric record is as public as the archive. It has been publishing top-level `raw_stderr` and `session_id` all along: 57 records on origin/reviews carry both. Adding per-attempt stderr to that file would have widened an existing leak rather than staying local. Publish a classified `error_kind` instead: a closed vocabulary derived from stderr that carries the diagnosis without the payload, which is what the scoreboard's bare "error" at $0.00 was missing. Route both persisted sinks through one recursive `public_record`, so `raw_stderr` and `session_id` are stripped at any depth and a field added to an attempt cannot start publishing either by accident. That also closes the pre-existing top-level leak. The unsanitised line still prints for a local operator, which is the case that had nothing to go on, but never under GITHUB_ACTIONS, whose logs are as public as the repo. ---------
* fix: support older gh when resolving PR refs * test: guard old-gh compatibility path
A stored scoreboard id whose user.login is not the current gh actor 404s on edit; post a fresh kind:scoreboard instead, matching the review-thread guard from TauCetiProject#110.
sankalpsthakur
force-pushed
the
fix/98-scoreboard-cross-identity
branch
from
August 17, 2026 12:15
5ce553f to
9923c0a
Compare
Contributor
Author
|
Superseded by #121 (same patch, agent trailer removed from the commit). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Review-thread roots already refuse to PATCH a comment whose
user.loginis not the currentghidentity (PR #110). The scoreboard issue-comment path did not: a storedscoreboard_comment_idwas PATCHed unconditionally, which 404s when that comment was authored by a different worker and strands the merge-sweep.If the known scoreboard's
user.login≠ currentghidentity, post a freshkind:scoreboardinstead of PATCHing. Newest-wins on the consumer side picks it up.Closes #98
Regression coverage
plan_sb_idexecute_postlayer: stored id 500 owned byother-botis not PATCHedVerification
python3 -m py_compile runner/*.pypython3 tests/test_cli.pypython3 tests/test_prices.pypython3 tests/test_post.py(20 checks, including the new ones)python3 tests/test_billing.pypython3 tests/test_thread_states.pypython3 tests/test_sweep.pypython3 tests/test_codex_fallback.pypython3 tests/test_kiro.pypython3 tests/test_attempt_diagnostics.pypython3 tests/test_prompt_refs.py,python3 tests/test_coordinate.pytests/test_reviewer_env.pyfails on this Darwin host withKeyError: XDG_DATA_HOMEalready onmain(the following test asserts that key is absent on macOS). CI runs Ubuntu, where that file is expected to pass. Untouched by this PR.Made with Cursor