Verify Boolean and NonZeroUsize candidate predicates

[joshlf]

Use extracted value predicates in the production TryFromBytes validators
for bool and NonZeroUsize. Keep Boolean candidates as bytes until validation,
so invalid encodings remain expressible in the model.

Prove scalar and pair conversions and a terminating Boolean-slice
validator, including rejected inputs. Reuse the production predicates and
compare the concrete candidates with public conversions, exhaustively for
Boolean bytes and pairs.

Register a narrow, source-bound byte read that preserves bounds failure.
Check its complete interpretation and reject an out-of-range-read mutant.
Reading through the generic Maybe pointer abstraction remains a separate
Rust safety premise.

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

---

• 　  Prove record construction against independent Rust references #3846
• 　  Prove selected cast plans preserve size without metadata overflow #3845
• 　  Prove CastPlan selection and unchecked metadata arithmetic #3844
• 　  Prove cast validation and exact-size metadata inference #3843
• 　  Prove allocation-size preparation and tail containment #3842
• 　  Prove CastUnsized's production layout acceptance gate #3841
• 　  Prove the numerical bounds used by split operations #3840
• 　  Prove advancement and padding-sequence decisions #3839
• 　  Prove DstLayout padding and field extension #3838
• 　  Prove unit and usize PointerMetadata operations #3837
• 　  Prove trailing sizes, padding and capacity including overflow #3836
• 　  Prove primitive DstLayout constructors #3835
• 　  Add an independent Rust reference for nested DST sizes #3834
• 　  Specify rounding encodings as alignment and phase #3833
• 　  Relate recursive record layout to normalized size formulas #3832
• 　  Prove normalized trailing-size and capacity formulas #3831
• 　  Reuse Aeneas rules for views and indexed loops #3830
• 　  Prove least padding and greatest aligned predecessors #3829
• 　  Test total and partial Aeneas contract semantics #3828
• 👉 Verify Boolean and NonZeroUsize candidate predicates #3852
• 　  Verify the byte writers used by IntoBytes #3851
• 　  Prove U16 and U32 byte-order reads, writes and updates #3827
• 　  Prove guarded Boolean conversion and byte copying #3849
• 　  Reject unsupported execution effects before Aeneas lowering #3848
• 　  Check Rust specs against golden and live Aeneas models #3826
• 　  Separate cast plans from pointer reconstruction #3825
• 　  Move cast_from into layout/cast_from.rs #3824
• 　  Share Rust layout and byte models in anneal/lean #3823
• 　  Update Anneal to Aeneas ca282ec and Lean 4.31 #3822

Latest Update: v2 — Compare vs v1

📚 Full Patch History

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

Version	v1	Base
v2	vs v1	vs Base
v1		vs Base

⬇️ Download this PR

Branch

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

Checkout

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

Cherry Pick

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

Pull

git pull origin refs/heads/G7q2xz2bs5ln4dfgckfspk2us4dhjperw

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:47.234919Z	e631dcb	PR opened
🔒 Security Review	✅ Completed 2026-10-09T02:26:22.992668Z	e631dcb	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.