[kani] Ground validator proofs in Rust oracles - #3664
Conversation
|
You have reached your Codex usage limits for security reviews. Please try again later. |
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. |
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
Reviewer guide: exact scopeThis follow-up replaces hand-reconstructed expectations with pre-call safe Rust/std observations across validator, transmute-macro, and UTF-8 scope: For byte sequences of lengths 0–4 at fixed modeled stack placements, the proofs show that zerocopy’s Other non-goals: Macro proofs remain limited to the documented Evidence: the full pinned run verified 332/332 harnesses and all 896 covers; repository pre-push validation passes. Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
@codex review Please review exact current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. Delightful! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
222841b to
e750fbc
Compare
47c3086 to
f837dcf
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G31fb58e3f6c48d287ce6208bb1b061e4 #3664 +/- ##
====================================================================
Coverage ? 91.85%
====================================================================
Files ? 20
Lines ? 6093
Branches ? 0
====================================================================
Hits ? 5597
Misses ? 496
Partials ? 0 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
f837dcf to
73ef3b5
Compare
e750fbc to
6f016f6
Compare
|
@codex review Please review exact current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
![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: 73ef3b54e8
ℹ️ 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".
| // `Unaligned` and `Aligned` zerocopy validator path returns with candidate | ||
| // bytes equal to the pre-call snapshot and reports the same classification | ||
| // as the standard-library operation it wraps. |
There was a problem hiding this comment.
The direct-validator harnesses do not establish that the candidate still refers to the original bytes: both new preservation checks compare bytes with snapshot, while neither observes candidate's address or referent. If the transmute_with/validator plumbing redirects the candidate to another same-valued buffer—the newly allocated snapshot provides such a buffer—the classifications and source-preservation assertions can all pass, so the stated conclusion that the candidate bytes equal the snapshot overstates what is proved. Snapshot bytes.as_ptr() before constructing the candidate and compare it with the candidate pointer, or explicitly exclude candidate address/referent preservation from the theorem.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Addressed on exact head dbb798e6a8ab8081d548dfc5c0d9f9ddc59e7976. The direct validator harness now snapshots the address from the original byte slice before candidate construction. It binds each actual unaligned/aligned candidate, compares the exposed address of that candidate with the snapshot, and then passes that same candidate to the validator. The original source-byte frame remains checked afterward. The documentation limits this to an address observation, explicitly excluding metadata/provenance claims and any assumption that distinct zero-sized storage must have distinct addresses. All five focused direct-validator harnesses passed, including every cover.
Replace hand-reconstructed expectations with safe Rust and standard-library observations, take independent pre-call snapshots, and make closure captures explicit. Document normal-return frame, padding-validity, and transient-write limits next to the affected harness families. The UTF-8 family now proves validator and public-borrow plumbing against core::str::from_utf8; it intentionally no longer claims an independent proof of the standard library’s UTF-8 classifier. *Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: G9a640f60dbaf8b9e24379dca9ac30494
73ef3b5 to
dbb798e
Compare
6f016f6 to
92d5e03
Compare
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Something went wrong. Try again later by commenting “@codex review”. ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
2 participants
Replace hand-reconstructed expectations with safe Rust and standard-library observations, take independent pre-call snapshots, and make closure captures explicit. Document normal-return frame, padding-validity, and transient-write limits next to the affected harness families.
The UTF-8 family now proves validator and public-borrow plumbing against core::str::from_utf8; it intentionally no longer claims an independent proof of the standard library’s UTF-8 classifier.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Latest Update: v4 — Compare vs v3
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/G9a640f60dbaf8b9e24379dca9ac30494 && git checkout -b pr-G9a640f60dbaf8b9e24379dca9ac30494 FETCH_HEADCheckout
git fetch origin refs/heads/G9a640f60dbaf8b9e24379dca9ac30494 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G9a640f60dbaf8b9e24379dca9ac30494 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.