Normalize nested DST size formulas - #3659
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. |
|
@codex review Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #3659 +/- ##
==========================================
- Coverage 91.86% 91.52% -0.34%
==========================================
Files 20 20
Lines 6097 6597 +500
==========================================
+ Hits 5601 6038 +437
- Misses 496 559 +63 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
|
Local validation on
The Kani proofs establish the layout algebra under their stated valid-layout and representability assumptions. They do not prove rustc's documented compatibility premise for compiler-accepted transitive packed/aligned nesting or exercise pointer projection end-to-end; the compiler regressions and Miri runs cover those paths. Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
![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: 2310d3b355
ℹ️ 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".
| pub fn via_unaligned(self) -> (&'a T, &'a [T::Elem]) | ||
| where | ||
| T: Unaligned, | ||
| T::Elem: Unaligned, |
There was a problem hiding this comment.
T: Unaligned caller contract
Downstream generic functions constrained by the previously documented T: SplitAt + Unaligned bound can no longer call via_unaligned, because Rust cannot infer T::Elem: Unaligned from T: Unaligned; the mirrored mutable overload has the same regression. This creates an unnecessary source-breaking API change even though via_no_dynamic_padding already provides the new bound-free path. Keep T: Unaligned on both existing via_unaligned methods and direct callers needing the broader layout-based behavior to the new method.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in d2049eb1263dc67f38d4b4d629f235ba8f9df314: restored the existing T: Unaligned bound on both public methods and the internal forwarding path, while retaining the monomorphization-time no-dynamic-padding assertion that supplies the soundness proof. via_no_dynamic_padding remains the broader API for types without that bound. I also added shared and mutable generic regression coverage using only T: SplitAt + Unaligned.
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. |
DstLayout flattened a nested slice DST's trailing-padding operation into the alignment of its packed outer container. That could understate the Rust object size, causing safe parsers and allocators to construct references and boxes whose referents extended beyond their backing storage. Represent slice-DST sizes as C + round_up(r + nE, A), encoding A and r in one nonzero word. Carry that four-word layout formula through composition, padding, metadata inference, casts, projections, allocation, and split overlap checks. This is a smaller state-model alternative to #3630. Exhaustive reduced-width model checking matches #3630's core formula transforms and representability behavior, and the checked benchmark snapshots are byte-for-byte identical. Add regression coverage for compiler-accepted generic packed/aligned nesting, parsing, allocation, zeroing, projection, metadata plateaus, and dynamic padding. Add modular Kani proofs for the normal form, transforms, inverse validator, affine cast arithmetic, alignment, containment, the conservative dynamic-padding predicate, and both modern and MSRV unchecked-arithmetic implementations. The arithmetic proofs are conditional on the documented compiler-layout premise; regression and Miri coverage exercise the actual compiler layout and pointer paths. Closes #3617 *Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: Ger2cetjqc3naucboffw4r4hal423gaa5
2310d3b to
d2049eb
Compare
|
@codex review 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. |
|
Validation on
The Kani proofs establish the layout algebra under their documented valid-layout and representability assumptions. They do not prove rustc's compatibility premise for compiler-accepted transitive packed/aligned generic nesting; regression tests and Miri exercise the compiler layout and pointer paths. Authored by an AI agent acting on Josh Liebow-Feeser's behalf. |
2 participants
DstLayout flattened a nested slice DST's trailing-padding operation into the alignment of its packed outer container. That could understate the Rust object size, causing safe parsers and allocators to construct references and boxes whose referents extended beyond their backing storage.
Represent slice-DST sizes as C + round_up(r + nE, A), encoding A and r in one nonzero word. Carry that four-word layout formula through composition, padding, metadata inference, casts, projections, allocation, and split overlap checks.
This is a smaller state-model alternative to #3630. Exhaustive reduced-width model checking matches #3630's core formula transforms and representability behavior, and the checked benchmark snapshots are byte-for-byte identical.
Add regression coverage for compiler-accepted generic packed/aligned nesting, parsing, allocation, zeroing, projection, metadata plateaus, and dynamic padding. Add modular Kani proofs for the normal form, transforms, inverse validator, affine cast arithmetic, alignment, containment, the conservative dynamic-padding predicate, and both modern and MSRV unchecked-arithmetic implementations. The arithmetic proofs are conditional on the documented compiler-layout premise; regression and Miri coverage exercise the actual compiler layout and pointer paths.
Closes #3617
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.
Latest Update: v3 — Compare vs v2
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Ger2cetjqc3naucboffw4r4hal423gaa5 && git checkout -b pr-Ger2cetjqc3naucboffw4r4hal423gaa5 FETCH_HEADCheckout
git fetch origin refs/heads/Ger2cetjqc3naucboffw4r4hal423gaa5 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Ger2cetjqc3naucboffw4r4hal423gaa5 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.