Prove production byte writes and preserved destination regions

[joshlf]

Route IntoBytes exact, prefix and suffix writes through the extracted byte
selection helpers. Prove acceptance, complete updated bytes, unchanged rejection
and untouched regions; compose the public big-endian word constructor/accessor
with the production prefix writer. Keep the typed-to-byte pointer bridge an
explicit Rust safety premise.

Register a self-contained, source-bound offset-copy interpretation with complete
guard checks and negative controls. Avoid the pinned backend's unsupported
suffix reconstruction rather than admitting its incorrect prefix behavior.

Validation: pinned extraction, independent golden/live proofs and axiom audits;
public write regression tests; compiler compatibility, Clippy and pre-push checks.

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

---

• 　  Prove record construction against independent Rust references #3846
• 　  Prove cast metadata composition against reference sizes #3845
• 　  Prove numerical cast plan selection and metadata conversion #3844
• 　  Prove cast validation and exact metadata inference #3843
• 　  Prove allocation size preparation and tail containment #3842
• 　  Prove the concrete CastUnsized layout gate #3841
• 　  Prove split lengths and non-overlapping numerical regions #3840
• 　  Prove byte advancement and padding sequence queries #3839
• 　  Prove normalized layout padding and field extension #3838
• 　  Prove concrete pointer metadata operations #3837
• 　  Prove exact trailing sizes, padding and capacity #3836
• 　  Prove primitive layout constructors with recursive mathematical models #3835
• 　  Compare nested DST sizes with a recursive Rust oracle #3834
• 　  Model alignment and phase encoding as a bounded mathematical pair #3833
• 　  Refine recursive record semantics into normalized layouts #3832
• 　  Prove trailing-layout normalization and capacity arithmetic #3831
• 　  Reuse Aeneas specifications for views and indexed loops #3830
• 　  Strengthen arithmetic specifications and prove arithmetic corollaries #3829
• 　  Check native total and partial Aeneas specifications #3828
• 　  Prove scalar bit-validity predicates and checked byte candidates #3852
• 👉 Prove production byte writes and preserved destination regions #3851
• 　  Prove unsigned byte-order reads, writes and updates #3827
• 　  Prove checked Boolean decoding and byte-prefix copying #3849
• 　  Inspect Rust execution before Aeneas lowering #3848
• 　  Verify doc-owned specifications over recursive mathematical models #3826
• 　  Separate numerical cast planning from typed pointer projection #3825
• 　  Move pointer cast implementation into its own source file #3824
• 　  Share Rust mathematical models across Anneal frontends #3823
• 　  Align Anneal V1 with the current Aeneas and Lean toolchain #3822

⬇️ Download this PR

Branch

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

Checkout

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

Cherry Pick

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

Pull

git pull origin refs/heads/Gkipiolhcatlfs5igrsox32w4yivfp7k3

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-09T02:24:54.655814Z	c2aa05d	PR opened
🔒 Security Review	✅ Completed 2026-10-09T02:25:14.540012Z	c2aa05d	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.