Repository navigation
Fix TrailingSliceLayout and remove Split::via_unaligned - #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 92.64% 92.66% +0.01%
==========================================
Files 20 20
Lines 6429 7412 +983
==========================================
+ Hits 5956 6868 +912
- Misses 473 544 +71 ☔ 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".
|
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. |
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. |
5dd7cb5 to
001893b
Compare
001893b to
3eb98c0
Compare
joshlf
left a comment
joshlf
left a comment
There was a problem hiding this comment.
Let's add inline Kani specs and proofs (like we do in util) in as many places as possible.
6787c8a to
1e5246b
Compare
jswrenn
changed the title
TrailingSliceLayout and remove Split::via_unaligned
46f2459 to
056079c
Compare
Carry the normalized trailing-size formula through composition, padding, metadata inference, casts, projections, allocation, and split overlap checks. Preserve complete inner sizes under packing: the packed regression has size 10 where flattening produces 8. This incorporates the fix from #3659 as a new stack commit. Prove all DstLayout methods and their representation helpers with 27 inline total contracts. Connect the machine operations to independent recursive semantics, including arbitrary field-list construction, exact overflow, physical padding, conservative size-sequence equivalence, largest fitting metadata, and error priority. Use reusable view contracts and the indexed-prefix loop adapter, and obtain checked-arithmetic facts from upstream step registrations. Record an explicit premise connecting those semantics and external size/alignment inputs to Rust; numerical proofs do not certify rustc or pointer safety. Check independent required propositions, closed method coverage, golden/live proof builds, declared theorem dependencies, and a data-only external-input axiom audit, including the named required-contract conversion witnesses. Add failure controls for dropped inner rounding and confusion between physical offsets and size bases. Validation: fresh extraction and both Lean builds; all 27 required types and dependency checks; 1,446 declaration axiom audit; failure controls in both workspaces; 26 Python and 3 annotation-tool tests; nightly Rust workspace tests and Clippy; MSRV/stable compilation and UI tests; repository pre-push checks. Closes #3617 gherrit-pr-id: Gnng6cftnqanivvm3mjiwcif6hovmkymt Agent-authored-by: AI agent acting on joshlf's behalf
Carry the normalized trailing-size formula through composition, padding, metadata inference, casts, projections, allocation, and split overlap checks. Preserve complete inner sizes under packing: the packed regression has size 10 where flattening produces 8. This incorporates the fix from #3659 as a new stack commit. Prove all DstLayout methods and their representation helpers with 27 inline total contracts. Connect the machine operations to independent recursive semantics, including arbitrary field-list construction, exact overflow, physical padding, conservative size-sequence equivalence, largest fitting metadata, and error priority. Use reusable view contracts and the indexed-prefix loop adapter, and obtain checked-arithmetic facts from upstream step registrations. Record an explicit premise connecting those semantics and external size/alignment inputs to Rust; numerical proofs do not certify rustc or pointer safety. Check independent required propositions, closed method coverage, golden/live proof builds, declared theorem dependencies, and a data-only external-input axiom audit, including the named required-contract conversion witnesses. Add failure controls for dropped inner rounding and confusion between physical offsets and size bases. Validation: fresh extraction and both Lean builds; all 27 required types and dependency checks; 1,446 declaration axiom audit; failure controls in both workspaces; 26 Python and 3 annotation-tool tests; nightly Rust workspace tests and Clippy; MSRV/stable compilation and UI tests; repository pre-push checks. Closes #3617 gherrit-pr-id: Gnng6cftnqanivvm3mjiwcif6hovmkymt Agent-authored-by: AI agent acting on joshlf's behalf
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. 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. Refresh dynamic-size and dynamic-padding codegen expectations for the pinned nightly. Report both expected and actual assembly on failure, and join every benchmark worker so all mismatches are reported. Closes #3617 *Authored by an AI agent acting on Josh Liebow-Feeser's and Jack Wrenn's behalf.* gherrit-pr-id: Ger2cetjqc3naucboffw4r4hal423gaa5 Agent-authored-by: AI agent acting on joshlf's behalf
056079c to
bbde23b
Compare
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.
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.
Refresh dynamic-size and dynamic-padding codegen expectations for the
pinned nightly. Report both expected and actual assembly on failure,
and join every benchmark worker so all mismatches are reported.
Closes #3617
Authored by an AI agent acting on Josh Liebow-Feeser's and Jack Wrenn's behalf.
Agent-authored-by: AI agent acting on joshlf's behalf
TrailingSliceLayoutand removeSplit::via_unaligned#3659Latest Update: v15 — Compare vs v14
📚 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.