Share Rust mathematical models across Anneal frontends

[joshlf]

Move common layout and numerical memory geometry into an independent Lean
package under anneal/lean. Add reusable integer byte-order models and prove
length, bound, truncation and round-trip laws without frontend assumptions.

Package sources and compiled artifacts in the existing omnibus dependency
archive; import the installed package from Anneal V1 and test relocation
from V2. Include these sources in archive cache inputs. Keep frontend
axioms and annotation machinery in their existing consumers.

Validation: independent Lean builds on 4.30.0-rc2 and 4.31.0; V1 Rust unit
tests; native relocation check; formatting and workflow/script checks.
Nix archive construction remains covered by the existing CI builder.

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/Gluzscumtqii4zeryhevzpymev2ojqng && git checkout -b pr-Gluzscumtqii4zeryhevzpymev2ojqng FETCH_HEAD

Checkout

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

Cherry Pick

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

Pull

git pull origin refs/heads/Gluzscumtqii4zeryhevzpymev2ojqng

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:21.286706Z	ae3acb5	PR opened
🔒 Security Review	✅ Completed 2026-10-07T11:14:25.335289Z	ae3acb5	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

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 92.94%. Comparing base (7bbce8d) to head (ae3acb5).

Additional details and impacted files

@@           Coverage Diff           @@
##             main    #3799   +/-   ##
=======================================
  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.