Claim #23 — Verification of <byteorder::BigEndian as byteorder::ByteOrder>::read_uint (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
<byteorder::BigEndian as byteorder::ByteOrder>::read_uint
Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
Arbitrary byte slice and byte count on x86_64 with default features. Normal return exactly when 1 <= nbytes <= 8 and nbytes <= input length; return is the unsigned selected-endian decoding of the first nbytes bytes, zero-padded to 8 bytes. Otherwise assertionFailure.
Evidence
What is trusted
From the report
F32/F64 are explicit 32/64-bit logical patterns; two executable std to_bits models preserve those patterns as unsigned words, with checked Lean value-preservation lemmas. Guards require original writer bodies and allow no other float operation. Kani checks std bit identity for every pattern and actual released writers with 6/10-byte buffers. Connecting these Rust checks to the Lean representation is reviewed, not mechanized; Rust nightlies differ. Official translation/standard integer and slice models, Lean, and Kani/CBMC are trusted. The four original native conversion bodies make no external calls after official target-branch translation. Five unused declarations remain in the unchanged, unimported template; the provider supplies zero definitions. Guards require exact identity bodies and zero external use. Mapped audits permit only propext, Classical.choice and Quot.sound.
Technical limitations
From the report
This covers 20 selected writer methods, eight unsigned and eight signed readers, four native-target unsigned identity conversions, and two handwritten Default methods, not all public APIs. Fixed 16/32/64/128-bit reads, variable-width writers, other bulk and in-place conversions, I/O extensions, other targets and release extraction remain unproved. The float result establishes bit serialization only: floating arithmetic, comparisons, rounding, numeric accuracy, NaN arithmetic and signaling behavior are not modeled. Kani public-writer buffer lengths are fixed at 6 and 10; arbitrary valid slice lengths are quantified separately by the Lean theorems. The signed from_slice defaults contain unsafe slice reinterpretation and are not covered; the floating conversions and opposite-endian/other-target paths are also unproved. The byteorder-lite eight-method result is not assumed transferable across versions. Panic messages and unwinding side effects are not specified. The separate variable-width writer comparison is limited to normal-success inputs and the 32-byte allocation shape. It does not establish failing inputs, arbitrary lengths/allocations, or independent memory safety. It adds no Aeneas API claims.
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