Repository navigation
Conversation
noahgift
enabled auto-merge
September 27, 2026 10:51
|
§13.11 rung 1 — quorum shadow verdict Shadow mode: this records a verdict and merges nothing. A refusal |
…denied credit to sorry-free theorems (#4351) insert_domain_theorems skipped any file whose text contained "sorry", including prose ("compiles sorry-free"), and never registered the dotted Theorems.<Domain>.<File> name that equations cite. Both failed closed: real proofs were denied, no false credit granted. lean_has_sorry now matches `sorry` as an identifier outside -- and nested /- -/ comments and strings, and fails closed on an unterminated one. pv proof-status contracts/: 70 -> 77 of 181 lean claims grounded; self-declared stays 27 (equation-only L4 rule, see #3141 audit §3). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit 7c128ef)
…eal sorry (#4351 quorum) Both quorum lanes (sonnet, haiku) found it; sonnet showed the false-credit case '"' sorry '"'. A prime now skips a well-formed char literal (one char, or an escape whose digits are hex only, so no body can spell sorry). Any other prime is term syntax (xs[i]'h, used in the tree) and is skipped alone. A first try that treated every token-start prime as a literal and failed closed took pv from 77 to 73 grounded on real files. pv proof-status contracts/: 77 of 181 grounded, 27 self-declared. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit 9115804)
Closes #4351 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…agy withheld, not tier-1) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
noahgift
force-pushed
the
91/4351-on-main
branch
from
September 27, 2026 13:19
61cd689 to
773e9e8
Compare
…merge (guard-tree DRIFT) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
Author
|
Moved into #4608 (PRCAP fold, cop order 14:02Z). Fold = MOVE: head |
auto-merge was automatically disabled
September 28, 2026 14:24
Pull request was closed
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
1 participant
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.
Closes #4351
pv's proof_status Lean scan used a plain substring match forsorry. It refused credit to sorry-free theorems when a doc comment or string said "sorry", or when the theorem was cited in theTheorems.<Domain>.<File>form.What changes (
crates/aprender-contracts/src/proof_status.rs)lean_has_sorryreads Lean tokens:sorry_freeas names, not thesorryterm;Theorems.<Domain>.<File>citation now resolves to its file.'"'no longer opens a phantom string that hid a realsorry.The two fix commits come from
origin/GH-4351-lean-scan-false-negatives, cherry-picked onto main unchanged.Measured (main 761d624 + this branch)
cargo test -p aprender-contracts --lib proof_statusclippy -D warnings/fmt --checklean_has_sorry→src.contains("sorry")lean_has_sorry_case_table,lean_scan_grounds_comment_sorry_file_and_dotted_form); restored, tree cleanQuorum: 3/3 PASS on eaa2d3b (
docs/audits/quorum-GH-4351.json). Degraded same-family: sonnet-5 ×2 + haiku-4-5. agy was withheld by policy because this diff is not tier-1. The author (opus-5-5) sat on no lane.🤖 Generated with Claude Code