[kani] Tighten slice and Ref proof scopes - #3663
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 factors and documents three bounded proof families around safe Rust/std observations:
Sized Direct-setup premises: The versioned source-body/Rust-move payload lemma applies to both direct paths. For the four constructible-range operation harnesses, the direct path rechecks size and alignment with safe Rust observations, uses the exact Non-goals: These are not generic theorems over other types/backings, nonzero-start destinations, invalid or uninitialized values, the unsafe byte-slice trait contracts themselves, provenance, aliasing, reference identity/lifetimes, or drop behavior. Frames observe normal-return final state and cannot exclude transient writes restored before observation. Custom/nested DST layout, including the known issue in #3630, is excluded. Kani input generation and translation remain documented TOOL/TCB premises. Evidence: the full pinned run verified 332/332 harnesses and all 896 covers; the five operation harnesses have ten setup-mode reachability 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. |
![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: 222841b361
ℹ️ 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 constructor harness quantifies over a superset of each operation | ||
| // harness's original-buffer and view domain under the same configuration. | ||
| // Its unchanged final frame can therefore be instantiated for each setup | ||
| // case and composed with the operation harness's sequence frame. This | ||
| // composition separates the setup's final-state contribution from the | ||
| // subsequent operation's stated final-state result; it still neither rules |
There was a problem hiding this comment.
When Ref::from_bytes and a later operation have compensating defects, the constructor harness only proves result classification and unchanged backing bytes after forgetting the payload; it does not establish the returned Ref or error payload's internal source/address state. Consequently, combining that result with a proof of the sequence operation(from_bytes(input)) cannot isolate the operation's final-state behavior as claimed here. Construct an independently known-good wrapper for the operation harnesses, or first prove the exact returned payload invariant needed by the operation.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in exact current head 6f016f6ad382118998ef6479b706003679661bfb. Each of the five Ref operation harnesses now checks a fresh symbolic public-constructor mode and a direct mode, with two covers requiring both modes to reach normal return. The direct mode bypasses Ref::from_bytes. For the four constructible-range operations, it rechecks size/alignment with safe Rust observations and uses new_unchecked under the source-payload lemma plus the concrete &mut [u8] unsafe-trait stability premise. For into_src, it instead uses the independently classified exact error constructor and payload lemma, with no byte-slice-stability premise. The constructor frame is no longer composed into the named-operation theorem. The full run verifies 332/332 harnesses and all 896 covers.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
222841b to
e750fbc
Compare
7509f06 to
4d90a86
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G868f72aa79c4e2c0240a06b3f1151fc9 #3663 +/- ##
==================================================================
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:
|
e750fbc to
6f016f6
Compare
4d90a86 to
16c135c
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. |
|
Codex Review: Didn't find any major issues. Hooray! 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". |
Factor the bounded slice and sized Ref proof accounts around safe Rust observations, including first_chunk and checked_sub oracles. State the universal input domains, final-state frames, transient-write exclusions, and Kani input-model premises next to the harness families. Pin the remaining layout citations to Rust 1.93. This follow-up deliberately excludes the separately tracked custom-DST layout bug in #3630. *Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: G31fb58e3f6c48d287ce6208bb1b061e4
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
Factor the bounded slice and sized Ref proof accounts around safe Rust observations, including first_chunk and checked_sub oracles. State the universal input domains, final-state frames, transient-write exclusions, and Kani input-model premises next to the harness families.
Pin the remaining layout citations to Rust 1.93. This follow-up deliberately excludes the separately tracked custom-DST layout bug in #3630.
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/G31fb58e3f6c48d287ce6208bb1b061e4 && git checkout -b pr-G31fb58e3f6c48d287ce6208bb1b061e4 FETCH_HEADCheckout
git fetch origin refs/heads/G31fb58e3f6c48d287ce6208bb1b061e4 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G31fb58e3f6c48d287ce6208bb1b061e4 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.