You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
proofs: a token may start after a skipped literal in the postulate scan - #174
This follows #170 (merged as 05ade78) and answers the Codex finding on it that arrived after the merge: "Recognize line comments after character literals".
The scanner decided whether -- (or ') starts a token from the raw character before it. In c = 'x'-- postulate X : Set the closing quote of the character literal therefore counted as a name character, so the line comment was not recognised, and a postulate Agda never sees failed the gate. That is a false failure, so it fails safe, but it is still wrong lexing. The scanner now uses the last character it emitted as code. A skipped literal, comment or pragma leaves a space, just as it leaves a token boundary in Agda.
Changes
scripts/scan-postulates.sh: prev is the last character of code, not substr(line, i-1, 1).
scripts/check-agda.sh: the comments-only control gains c = 'x'-- postulate after a character literal, which must exit 0.
The branch merges main into #170's head rather than rewriting it, so its diff against main is exactly these two files (+4/−2).
Testing
Check
Result
Scanner cases (32), under mawk and gawk
all pass. The scanner at 9ff3043 (merged) fails exactly the reported case; string literals, block comments and primed names (x'--y stays one name) are unchanged
bash scripts/check-agda.sh (local Agda 2.6.3)
[check-agda] OK: cone 6 + 8, 0 postulates, Primitive names and bindings checked, controls behave, 6 rejections refused as named
shellcheck on both scripts
clean
After merge
The first green agda-proofs.yml run on main at this PR's merge commit becomes the gate's receipt. #170's merge run 42633520061 at 05ade78 was green too, but this PR changes the checker again. A doc-only PR then records that run in PROOF-GRADES.adoc and PROOF-NEEDS.adoc, marks 42076969251 superseded, and drops "pending re-run". A doc-only commit changes neither the modules nor the checker, so it leaves that receipt current.
…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
…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
…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
…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
The scanner decided whether `--` or `'` starts a token from the raw
character before it, so in `c = 'x'-- postulate …` the closing quote of
the character literal counted as a name character, the line comment was
not recognised, and a postulate that Agda never sees failed the gate.
It now uses the last character emitted as code: a skipped literal,
comment or pragma leaves a space, as it leaves a token boundary in Agda.
The comments-only control carries the case.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg
No actionable comments were generated in the recent review.
Summary
Summary by CodeRabbit
Bug Fixes
Improved postulate scanning so skipped literals, comments and pragmas are handled correctly when identifying token boundaries. This helps prevent text following these elements from being misread during scanning.
Tests
Expanded scanner checks to cover a character literal followed by a line comment, alongside the existing foreign pragma case.
The scanner now checks the last character emitted into code when it determines whether a token can begin. The comments-only fixture adds a character literal followed by a line comment.
Changes: Scanner token-boundary handling
Layer / File(s)
Summary
Token-boundary check and fixture scripts/scan-postulates.sh, scripts/check-agda.sh
The scanner checks the last emitted character in code instead of the preceding raw input character. The comments-only fixture adds a character literal followed by a line comment.
No actionable merge-blocking risk was identified. Run the normal checks before merging.
Pre-merge checks: 5
Check name
Status
Explanation
Title check
The title clearly describes the scanner change: recognising a token after a skipped literal.
Description check
The description explains the scanner change, its test case and reported test results. It is relevant to the changeset.
Docstring Coverage
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentat…
Linked Issues check
Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check
Check skipped because no linked issues were found for this pull request.
Full details: Docstring Coverage
Explanation
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 0 functions across 2 files.
Finishing Touches
Generate docstrings
Commit to this branch
Create a new PR
Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
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.
File: No configuration file from this repository applied
Commit: Unavailable
Layers: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: 54e116f8-3c60-47af-9782-83d6e4d54a2d
Commits
Reviewing files that changed from the base of the PR and between e0bee35 and 224324f.
Files selected for processing: 1
scripts/check-agda.sh
Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.
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.
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
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.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Summary
This follows #170 (merged as
05ade78) and answers the Codex finding on it that arrived after the merge: "Recognize line comments after character literals".The scanner decided whether
--(or') starts a token from the raw character before it. Inc = 'x'-- postulate X : Setthe closing quote of the character literal therefore counted as a name character, so the line comment was not recognised, and a postulate Agda never sees failed the gate. That is a false failure, so it fails safe, but it is still wrong lexing. The scanner now uses the last character it emitted as code. A skipped literal, comment or pragma leaves a space, just as it leaves a token boundary in Agda.Changes
scripts/scan-postulates.sh:previs the last character ofcode, notsubstr(line, i-1, 1).scripts/check-agda.sh: the comments-only control gainsc = 'x'-- postulate after a character literal, which must exit 0.The branch merges
maininto #170's head rather than rewriting it, so its diff againstmainis exactly these two files (+4/−2).Testing
9ff3043(merged) fails exactly the reported case; string literals, block comments and primed names (x'--ystays one name) are unchangedbash scripts/check-agda.sh(local Agda 2.6.3)[check-agda] OK: cone 6 + 8, 0 postulates, Primitive names and bindings checked, controls behave, 6 rejections refused as namedshellcheckon both scriptsAfter merge
The first green
agda-proofs.ymlrun onmainat this PR's merge commit becomes the gate's receipt. #170's merge run 42633520061 at05ade78was green too, but this PR changes the checker again. A doc-only PR then records that run inPROOF-GRADES.adocandPROOF-NEEDS.adoc, marks 42076969251superseded, and drops "pending re-run". A doc-only commit changes neither the modules nor the checker, so it leaves that receipt current.Generated by Claude Code