Claim #4 — Verification of <endian_type::LittleEndian<T> as core::ops::BitAnd>::bitand (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
<endian_type::LittleEndian<T> as core::ops::BitAnd>::bitand
Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
Arbitrary well-typed operands and arbitrary underlying Rust operator implementation, represented by its Aeneas trait dictionary. Wrapper equivalence preserves the underlying result; no assumption of callback success is required.
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. The reflexive6 supplement uses pinned Rust nightly2026-09-17 standard From/Borrow/BorrowMut sources and typed pre/post-inline MIR to connect actual public UFCS callers to original blanket implementations. It additionally trusts official compiler Inline/RemoveStorageMarkers/ReferencePropagation/DeadStoreElimination-final/SimplifyLocals-final through optimized MIR and unchanged Charon/Aeneas. Final IR has zero residual calls; some core source spans are erased by cleanup, so no universal final-span correspondence or compiler-correctness proof is claimed. No new model, type axiom or generated/source/IR edit is introduced. Conditional6 uses original pinned std09 conversion delegation bodies and six typed before/after official Inline MIR scopes; final generated IR retains one actual trait callback per caller. Dictionary correspondence to the Rust implementation and official compiler/Charon/Aeneas/library are trusted; callback implementations are not independently proved. No custom translator, model, type axiom, source/IR/generated edit or std08/std09 equivalence is supplied.
Technical limitations
From the report
Registered Aeneas 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. Other trait/default/blanket behavior beyond the twelve supplemental reflexive/conditional caller contracts is not verified. Type-specialized Rust identities and any erased server catalogue keys must be distinguished. Reflexive6 are supplementary compiler-inlined caller contracts, not direct default-declaration/source-card bindings or new registered APIs. Borrow values and backward functions are Aeneas functional views, not physical pointer identity, arbitrary heap/provenance/alias/lifetime or caller-replacement/Drop-effect guarantees. They establish no Rust PartialEq law or conversion between the distinct BigEndian and LittleEndian nominal types. Other configurations/targets and const evaluation are not checked. Producer namespace/type coimport did not rerun all66 old theorems; the formal integrated fresh run separately rechecks all configured primary modules with the supplement. Consolidated portable regeneration/replay remains unrun; individual successful extraction, typed MIR and kernel evidence are retained. These six conditional caller contracts do not establish arbitrary callback values/correctness/termination, Drop/panic/unwinding, global/interior effects or physical heap/alias/provenance. The modeled equality is unconditional in the dictionary model, while useful normal-result facts need the corresponding callback contract. They add no direct external-body API-card binding or primary mapping. Individual frontend/proof/type-coimport checks succeeded; corrected frontend replay permits only LLBC dest_dir output metadata relocation and checks generated Lean/JSON byte equality. The consolidated whole replay script is prepared but not run.
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