Repository navigation
Verifier README: state what the executable-operation check is independent of - #849
Conversation
…dent of The README said the verifier reconstructs the expected package without importing or calling the lowerer. That is true, but on 2026-10-14 91% of the lowerer's distinct code lines in executable_operation.rs appeared verbatim in the verifier's copy, so one mistake is usually made twice. The new paragraph states the property the byte comparison does provide: it rejects tampering and a defect in the lowerer alone, as the rebound-coordinate and tamper tests show, and it accepts a mistake present in both copies, as d121758 showed. Fixes #809. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
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 36 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. Comment |
Codex Review SummaryThis 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. |
![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: dca2ff03de
ℹ️ 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".
…dent The caveat now names the packages rebuilt in the copied file (mutation, compare-and-set, bounded pure) and says the bounded-read route rebuilds Core from the Target IR instead. The architecture document called the mutation/CAS verifier independent twice; it now says structurally separate. Found by review of #849. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 518325a05a
ℹ️ 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 bounded-pure, mutation and compare-and-set verifier routes rebuild the package with code that largely repeats the lowerer's. Four more places called that reconstruction independent: the provider schema README, the verifier README's bounded-pure paragraph, the architecture document, and the Jedit fixture README. They now say structurally separate or name the shared code. Found by review of #849. Statements of the requirement, and the first native verifier, are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2a046bdcf9
ℹ️ 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".
Three Unreleased entries (projected CAS, transformed effect arguments, the bounded-pure package) called the same verifier independent. They now say structurally separate. Source-function checks, where the verifier shares about 29% of the lowerer's code, keep their wording. Found by review of #849. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5e5facacb7
ℹ️ 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 create mutation profile's Core-relation evidence, the result-ceiling entry and the obstruction-alias entry still called the copied verification independent. Remaining uses describe the requirement, the bounded-read route, or how release digests are verified. Found by review of #849. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 participant
What
Takes the documentation option in #809: the verifier README now states the independence the executable-operation route actually has.
Measured 2026-10-14: 924 of the lowerer's 1,011 distinct non-comment code lines in
executable_operation.rs(91%) appear verbatim in the verifier's file of the same name.The new paragraph says:
tests/executable_operation_package.rsshow this:verifier_rejects_a_canonical_package_with_a_rebound_operation_coordinate, its obstruction twin, andverifier_independently_accepts_and_tamper_rejects_generic_pure_packagestake a real lowered package, change one binding, keep it canonical, and get a rejected report. That covers the issue's seeded-defect criterion.d121758bis the example.Not changed: the bounded-read route, which rebuilds Core from Target IR by reverse mapping rather than by a copy, and
docs/topics/GeneratedRules.md, which already says the separation is not an independently implemented verifier.Left open: writing a verifier that derives its expectation independently is not done. It is the larger option in #809 and can be a follow-up issue if wanted.
Checks
Prettier,
test_knowledge_model,test_documentation_model.Fixes #809.
🤖 Generated with Claude Code