Fix repository-wide autoreview findings - #19
Conversation
![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: dc57d089c5
ℹ️ 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".
| if (file.name !== validatedEntryNames[streamedEntries]) { | ||
| failure = new Error("The ZIP archive could not be safely extracted."); |
There was a problem hiding this comment.
When a valid ZIP's central directory is not in the same order as the local file headers, validatedEntryNames is in central-directory order while Unzip emits entries as it streams the local headers. This check then rejects the upload as unsafe even though each central record points at a valid local entry; reconcile the validated entries by localOffset (or by offset) instead of assuming both orders are identical.
Useful? React with 👍 / 👎.
| setSelectionError("That passage could not be matched to the indexed paper text. Try a smaller selection.") | ||
| return |
There was a problem hiding this comment.
When a user already has a selection menu open and then highlights a passage that resolvePageBlockIds cannot match, this early return only sets the status text; the parent selection is never cleared because onSelection is not called. The old menu stays active and its buttons submit the previous passage, so the explanation can be for text the user no longer selected; notify the parent to dismiss/clear the selection before returning.
Useful? React with 👍 / 👎.
| const mapping = | ||
| loaded.manifest.mappings.find((item) => item.paper.sourceId === sourceId) ?? | ||
| loaded.manifest.mappings.find((item) => item.paper.pages.includes(page.number)); | ||
| const mapping = loaded.manifest.mappings.find((item) => item.paper.sourceId === sourceId); |
There was a problem hiding this comment.
For paper selections that start in an unmapped block but include a mapped block—e.g. selecting a heading together with the theorem paragraph—blocks[0] becomes the heading, so this lookup drops the mapping and sends no Lean counterpart even though one of the selected block IDs is mapped. Resolve the mapping from any selected block, or from the block containing the matched text, rather than only the first block.
Useful? React with 👍 / 👎.
1 participant
Summary
Root causes and impact
The repository-wide autoreview found trust-boundary, mapping, archive, subprocess, and CLI validation gaps. These changes prevent client-spoofed rate-limit identities, wrong paper-to-Lean grounding, malformed or oversized archive processing, orphaned verification subprocess trees, silently skipped proof packages, and accidental paid evaluation runs.
One infrastructure follow-up remains explicit: the in-process limiter is not globally shared across Cloudflare isolates. A provider-backed rate-limit binding or shared durable store should replace it before relying on it as the only production quota.
Review disposition
Validation