Prove unsigned byte-order reads, writes and updates

[joshlf]

Exercise the production U16/U32 read, write and set paths for both byte
orders with twelve total inline contracts over every typed input. Connect
Aeneas bit-vector codecs to the shared radix-256 mathematics and separately
check complete positional sums, output digits and setter/getter equality.

Model the extracted zero-field PhantomData carrier explicitly. Admit only
the exact opaque Formatter Type required by unused formatting dictionaries;
no formatting behavior or proposition is assumed. Both signatures and raw
model ownership remain audited.

Validation: fresh pinned extraction, complete golden comparison, independent
golden/live proof builds and required-contract/axiom audits; pinned-nightly
Rust byte examples and repository pre-push checks.

Agent-authored-by: AI agent acting on joshlf's behalf

---

• 　  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
• 👉 Prove unsigned byte-order reads, writes and updates #3800
• 　  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
• 　  Share Rust mathematical models across Anneal frontends #3799

⬇️ Download this PR

Branch

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

Checkout

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

Cherry Pick

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

Pull

git pull origin refs/heads/G3uqhjrihjne4qee2q6qpmhde46wlhdy

Stacked PRs enabled by GHerrit.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-07T11:13:09.643761Z	ac33eeb	PR opened
🔒 Security Review	✅ Completed 2026-10-07T11:13:02.836169Z	ac33eeb	PR opened

ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[codecov-commenter]

Codecov Report

❌ Patch coverage is 0% with 44 lines in your changes missing coverage. Please review.
⚠️ Please upload report for BASE (Gf75ukj4vvtufg6dwjpfa3bx5a457sw74@70fe293). Learn more about missing BASE report.

Files with missing lines	Patch %	Lines
zerocopy/src/byteorder.rs	0.00%	44 Missing ⚠️

Additional details and impacted files

@@                         Coverage Diff                          @@
##             Gf75ukj4vvtufg6dwjpfa3bx5a457sw74    #3800   +/-   ##
====================================================================
  Coverage                                     ?   60.60%           
====================================================================
  Files                                        ?       20           
  Lines                                        ?     3757           
  Branches                                     ?        0           
====================================================================
  Hits                                         ?     2277           
  Misses                                       ?     1480           
  Partials                                     ?        0           

☔ 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.