[kani] Prove sized Ref construction and restoration - #3657
Conversation
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. |
93cdb98 to
efa1180
Compare
a5d27ff to
f131f42
Compare
efa1180 to
d41363c
Compare
f131f42 to
d474119
Compare
d41363c to
9742a70
Compare
d474119 to
6cc76b9
Compare
9742a70 to
3f9d1cf
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G3ehtgm3rda6i5wi6h6gwkvlmzeh4sn46 #3657 +/- ##
==================================================================
Coverage 91.89% 91.89%
==================================================================
Files 20 20
Lines 6118 6118
==================================================================
Hits 5622 5622
Misses 496 496 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
|
@codex review Please review current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
Codex Review: Didn't find any major issues. Breezy! 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". |
|
Security review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
6cc76b9 to
e0bc7fa
Compare
|
@codex review Please review current head Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
|
Security review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
![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: 510e818403
ℹ️ 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".
|
|
||
| match (result, expected_success) { | ||
| (Ok(typed), true) => { | ||
| kani::cover!(view.start == 0 && source_len == SIZE); |
There was a problem hiding this comment.
Every claimed reachability witness depends on kani::cover! creating a cover property whose satisfaction means this condition is reachable, but the supposedly exact pinned premise list documents kani::any, kani::assume, assertions, and failures without documenting the cover! contract. Add the Kani 0.67 cover semantics to the premise list and map them to these non-vacuity sites so the proof account establishes what the CI-checked cover summaries actually witness.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The pinned premise list now records that kani::cover! asks whether an execution reaches the observer with its condition true and that SATISFIED means such an execution was found. Every cover is mapped to that premise and to the fail-closed result checker; the proof account explicitly limits each result to an existential reachability witness rather than an assertion or universal target theorem.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| mem::forget(typed); | ||
| } | ||
| (Err(err), false) => { | ||
| kani::cover!(view.start == 0 && source_len == SIZE - 1); |
There was a problem hiding this comment.
The earlier manual View::len subtraction was removed, but the current revision still introduces fresh usize subtraction in these error-partition covers through SIZE - 1. Premises [12], [24], and [25] establish size observation, equality, and ordering, not subtraction or its overflow behavior, so the supposedly exact audit basis does not establish that these covers denote the intended one-byte-short partition; cite the pinned Rust subtraction semantics and map them to both remaining uses.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. Both one-byte-short covers now call a shared one_byte_short_of_u32 oracle implemented with SIZE.checked_sub(1).expect(...). The proof account cites usize::checked_sub, maps both uses to it, and explains that expect makes a hypothetical zero-sized premise fail closed under Kani. No unchecked SIZE - 1 reconstruction remains.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
|
|
||
| kani::cover!(view.start == 0 && source_len == SIZE); | ||
| kani::cover!(view.start == SIZE && source_len == SIZE); | ||
| kani::cover!(original_value != replacement); |
There was a problem hiding this comment.
These original_value != replacement witnesses depend on u32::PartialEq::ne and the != operator, while premise [21] records only PartialEq::eq and its use by ==. Consequently, the exact premise map does not ground the classification used to prove that non-idempotent DerefMut and into_mut cases are reachable; add the versioned inequality contract and map it to both covers.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in the current revision. The premise list now records Rust’s mapping of != to PartialEq::ne and the applicable primitive u32 operation, and maps it to both non-idempotent mutation covers. The analogous u8 error-replacement cover is documented separately under the same language operation.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
|
@codex review 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. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 7fec9e49a2
ℹ️ 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".
| // theorem: `Ref::from_bytes` documents rejection for either invalid size | ||
| // or alignment, while this proof also asserts the intended converse. | ||
| fn construction_oracle(source: &[u8]) -> bool { | ||
| source.len() == SIZE && source.as_ptr().cast::<u32>().is_aligned() |
There was a problem hiding this comment.
The supposedly exact assertion map grounds the two operands of construction_oracle in length, alignment, and equality premises, but never grounds the && operation that combines them into the success predicate used by all four harnesses. Without the pinned Rust Boolean conjunction contract, the proof account does not establish its central “success iff both checks pass” policy or the mutation-domain assumptions; cite that contract and map it to this oracle.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed. The construction-oracle proof map now cites Rust 1.93's lazy Boolean && contract and explicitly derives that the oracle succeeds exactly when both the independently grounded length and alignment predicates hold.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| if selected.len() != SIZE { | ||
| return None; |
There was a problem hiding this comment.
All three mutation-frame expectations depend on this if selected.len() != SIZE { return None; } guard selecting the copy path, but the supposedly complete post-mutation frame basis at lines 1291–1293 omits both the [24] usize::ne comparison premise and the conditional/return control-flow premise. The constructor assumption supplies an exact-size input but does not itself establish how this separate oracle guard evaluates, so add those pinned Rust contracts to the frame assertion map.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed. The frame-oracle account now maps selected.len() != SIZE through the pinned usize inequality contract and the Rust 1.93 conditional-expression and return-expression rules before the copy path is used.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
| // or any generic `Ref` or `B` drop behavior. | ||
| #[kani::proof] | ||
| #[kani::unwind(9)] | ||
| fn prove_sized_u32_from_bytes_deref_and_error_restoration() { |
There was a problem hiding this comment.
This single harness targets Ref::from_bytes classification, immutable Deref, and CastError::into_src restoration/write-through, even though agent_docs/validation.md requires distinct harnesses for different entry points or contracts. Consequently, a dereference or error-accessor regression fails the constructor harness and obscures which contract broke; keep the shared generator and oracles, but move the target-specific assertions into separate constructor, dereference, and restoration harnesses.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed. The combined harness was split into separate classification, immutable dereference, error-source restoration, mutable dereference, write, and into_mut harnesses. They retain shared input/oracle helpers while each target entry point and contract now fails independently.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
|
@codex review Please review 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: 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". |
|
@codex review 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. More of your lovely PRs please. 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". |
|
@codex review Please review exact 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. Keep them coming! 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". |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
|
Codex Review: Didn't find any major issues. More of your lovely PRs please. 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". |
|
You have reached your Codex usage limits for security reviews. Please try again later. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 78d9d75b21
ℹ️ 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".
| *typed = replacement; | ||
| assert_eq!(*typed, replacement); | ||
| } |
There was a problem hiding this comment.
In both prove_sized_u32_into_mut and prove_sized_u32_error_into_src, the returned &mut reference falls out of scope before the backing-buffer frame is checked, so each harness observes the target operation plus destruction of that reference value. Unlike the other frame harnesses, the exact premise/assertion map neither isolates this step nor cites Rust's guarantee that destroying a reference has no storage effect; explicitly document and map that premise, or retain the returned reference in a ManuallyDrop until after the frame observation.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
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 408601076d97cd22429eef20009b719e325d773a. The three returned mutable-reference values in the error-restoration, DerefMut, and into_mut harnesses are now placed in ManuallyDrop after their final observation/write and before the outer backing-frame assertion. Premise [42] records this explicit automatic-drop isolation; the comments no longer rely on an unstated general reference-destruction theorem. The wrapper-forgetting boundaries remain in place. This change is also preserved in the downstream direct-construction variant in #3663.
| if selected.len() != SIZE { | ||
| return None; | ||
| } | ||
| selected.copy_from_slice(&replacement.to_ne_bytes()); |
There was a problem hiding this comment.
Every mutation-frame expectation passes &replacement.to_ne_bytes(), whose type is &[u8; 4], to copy_from_slice, whose parameter is &[u8]; the expected frame therefore depends on Rust's array-to-slice unsizing coercion (and the borrowed temporary surviving the call). Premises [3] and [4] establish the produced array and equal-length slice copy but not this bridge, so cite the pinned coercion contract and include it in the post-mutation frame map.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
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 408601076d97cd22429eef20009b719e325d773a. The replacement array is now a named replacement_bytes binding before copy_from_slice. The proof explicitly connects the binding scope [32], function-argument coercion site, and array-to-slice unsizing through the shared reference [41]. It no longer needs a borrowed-temporary lifetime argument. The same repair is preserved in #3663.
|
You have reached your Codex usage limits for security reviews. Please try again later. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 65cfd710a5
ℹ️ 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".
| // in the immutable `Deref`, `DerefMut`, and `into_mut` harnesses consume | ||
| // [1], [2], [6], [11], [12], [21], and the applicable immutable or mutable | ||
| // `Deref` placement policy above. Direct post-target typed comparisons |
There was a problem hiding this comment.
The typed-value assertions in all three named harnesses obtain the observed u32 by applying unary * to the returned reference (for example, lines 1631, 1721, and 1804), but this supposedly exact basis omits premise [8], which is the documented language rule connecting that dereference to the referenced location. The direct post-target comparison map below has the same omission. Add [8] to both mappings so the value observations are fully grounded rather than relying only on the zerocopy placement policy and primitive equality.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
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 408601076d97cd22429eef20009b719e325d773a. The consumer map now explicitly includes dereference premise [8] for both the source-derived initial typed-value assertions and the direct post-target typed comparisons. This documentation change is preserved in #3663 as well.
| // importing another as a lemma. The immutable-`Deref` frame additionally | ||
| // consumes its placement/value policy above. The separate error-restoration |
There was a problem hiding this comment.
The immutable-Deref harness checks the entire backing frame after calling Deref::deref, so it will fail if the target returns the correct address and value but also mutates any backing byte as a side effect. The mapped placement/value policy establishes only which referent is returned, not that invoking deref leaves all storage unchanged; explicitly adopt and map immutable-Deref non-mutation as a zerocopy regression policy, or remove this frame assertion from the target-specific harness.
AGENTS.md reference: zerocopy/AGENTS.md:L67-L73
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 408601076d97cd22429eef20009b719e325d773a. The immutable Deref policy and harness scope now expressly require the entire backing byte slice to remain unchanged, and the frame consumer cites that policy. The text identifies this as an adopted zerocopy regression policy, not a guarantee inferred from Rust or the Deref trait. The same qualification is preserved in #3663.
*Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: Glkshhyn2hsme53vnmamjpny6o3s637ys
|
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
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Latest Update: v52 — Compare vs v51
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Glkshhyn2hsme53vnmamjpny6o3s637ys && git checkout -b pr-Glkshhyn2hsme53vnmamjpny6o3s637ys FETCH_HEADCheckout
git fetch origin refs/heads/Glkshhyn2hsme53vnmamjpny6o3s637ys && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Glkshhyn2hsme53vnmamjpny6o3s637ys && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.