Optimize validate_cast_and_convert_metadata

[jswrenn]

This routine begins by rounding bytes_len down to the nearest multiple of
align (thus computing the intermediary max_total_bytes), subtracting the
offset of the trailing slice, and calculating how many elements (elems) fit in
that space. Then, in an expensive computation involving elems, the element
size, the trailing slice offset, align, the total self_bytes is computed.

This commit observes that when the element size is no larger than the align,
self_bytes is simply equal to max_total_bytes. For example, if
max_total_bytes is 16 bytes, the header occupies 9 bytes and two 3-byte
elements fit, they would occupy 15 bytes altogether, leaving 1 byte in excess.

This excess must be smaller than one element, otherwise another element would
fit. When elem_size <= align, the gap is smaller than align and trailing
padding fills it exactly.

---

• 　  Prove record construction against independent Rust references #3744
• 　  Prove cast metadata composition against reference sizes #3777
• 　  Prove numerical cast plan selection and metadata conversion #3776
• 　  Prove cast validation and exact metadata inference #3755
• 　  Prove allocation size preparation and tail containment #3790
• 　  Prove the concrete CastUnsized layout gate #3789
• 　  Prove split lengths and non-overlapping numerical regions #3788
• 　  Prove byte advancement and padding sequence queries #3754
• 　  Prove normalized layout padding and field extension #3753
• 　  Prove concrete pointer metadata operations #3787
• 　  Prove exact trailing sizes, padding and capacity #3752
• 　  Prove primitive layout constructors with recursive mathematical models #3751
• 　  Compare nested DST sizes with a recursive Rust oracle #3749
• 　  Model alignment and phase encoding as a bounded mathematical pair #3747
• 　  Refine recursive record semantics into normalized layouts #3743
• 　  Prove trailing-layout normalization and capacity arithmetic #3742
• 　  Reuse Aeneas specifications for views and indexed loops #3745
• 　  Strengthen arithmetic specifications and prove arithmetic corollaries #3746
• 　  Check native total and partial Aeneas specifications #3739
• 　  Verify doc-owned specifications over recursive mathematical models #3738
• 　  Separate numerical cast planning from typed pointer projection #3774
• 　  Move pointer cast implementation into its own source file #3773
• 👉 Optimize validate_cast_and_convert_metadata #3716

Latest Update: v4 — Compare vs v3

📚 Full Patch History

Links show the diff between the row version and the column version.

Version	v3	v2	v1	Base
v4	vs v3	vs v2	vs v1	vs Base
v3		vs v2	vs v1	vs Base
v2			vs v1	vs Base
v1				vs Base

⬇️ Download this PR

Branch

git fetch origin refs/heads/G463fe47353c89d061e6458fa9c4bd19328a954a8 && git checkout -b pr-G463fe47353c89d061e6458fa9c4bd19328a954a8 FETCH_HEAD

Checkout

git fetch origin refs/heads/G463fe47353c89d061e6458fa9c4bd19328a954a8 && git checkout FETCH_HEAD

Cherry Pick

git fetch origin refs/heads/G463fe47353c89d061e6458fa9c4bd19328a954a8 && git cherry-pick FETCH_HEAD

Pull

git pull origin refs/heads/G463fe47353c89d061e6458fa9c4bd19328a954a8

Stacked PRs enabled by GHerrit.

[codecov-commenter]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 92.94%. Comparing base (3e328bc) to head (6f00605).

Additional details and impacted files

@@           Coverage Diff           @@
##             main    #3716   +/-   ##
=======================================
  Coverage   92.94%   92.94%           
=======================================
  Files          16       16           
  Lines        2466     2466           
=======================================
  Hits         2292     2292           
  Misses        174      174           

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[joshlf]

Would it be possible to use Kani to completely prove the correctness of this fast path for usize? IIRC we were unable to do that for the full version of the algorithm.

[jswrenn]

@joshlf Unfortunately, not really. For this particular case, we can prove panic freedom (i.e., that we can merely call the method) and that split_at <= bytes_len, but seemingly nothing else. Given our hefty test suite for validate_cast_and_convert_metadata and our upcoming changes to this DstLayout and this method, I don't think this very limited proof is worth adding.

[jswrenn]

Obsoleted (for now) by #3659.