Claim #34 — Verification of <usize as From<endian_type::LittleEndian<usize>>>::from (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
<usize as From<endian_type::LittleEndian<usize>>>::from
Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
x86_64 little-endian; all primitive input bit patterns; System.Platform.numBits=64 explicitly required in Lean. Exact specialization: <usize as core::convert::From<endian_type::LittleEndian<usize>>>::from. Uses explicit native-endian scalar models; the Rust-byte-formula/Lean-primitive correspondence is reviewed with separate all-input Kani evidence.
Evidence
What is trusted
From the report
The Rust compiler, Charon/Aeneas, official scalar/byte primitives, Lean kernel, Kani and CBMC are trusted. Fifty native-endian std-operation models are explicitly supplied. Their Rust byte formulas and official Lean byte primitives are connected by review, not a mechanically checked cross-language theorem; std operator bodies are not independently proved in Lean. Kani and extraction use different Rust nightlies. The six bitwise results quantify arbitrary underlying operator dictionaries without proving user callback bodies. All 66 API contracts and 50 model specifications use only propext, Classical.choice and Quot.sound as transitive axioms.
Technical limitations
From the report
Coverage is limited to six bitwise methods and sixty concrete integer From implementations on the stated target/model domain. The forty-six byte/slice APIs and their unsafe layout/validity/aliasing obligations are not covered by these Aeneas claims. No generic arbitrary-T memory-safety, other target, endian, or pointer-width claim is established. Derived standard-trait methods are excluded. Remaining trait/default/blanket behavior is not verified. Type-specialized Rust identities and any erased server catalogue keys must be distinguished.
Tool limitations
Lean backend only, requiring cargo-proofs 0.4.0 or later. The version identifies the official Aeneas Git revision pinned in lake-manifest.json (backends/lean); this revision uses Lean 4.35.0. The recorder checks committed Lean theorem declarations and permits only propext, Classical.choice, and Quot.sound as transitive axioms. It rejects sorryAx and custom axioms, including axiomatized external models. Charon/Aeneas extraction is not rerun. The author must review that the committed functional model matches the recorded Rust source, that the named theorem corresponds to the public API, and that the reported precondition matches the theorem. A checked theorem alone does not establish those links or the adequacy of the specification. The current adapter records the default Cargo configuration, with ordinary Lean module paths and a pinned official Git dependency. Other backends, custom Lake source directories, and local-path Aeneas dependencies are unsupported. See https://proofs.rs/book/aeneas.html and https://github.com/AeneasVerif/aeneas/tree/be86ab0f1989d04944292b345b24c435be3ad10a.
Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details