Claim #2 — Verification of base16ct::decoded_len (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
Every well-typed input slice, regardless of byte contents; default features, x86_64, debug assertions enabled.
Evidence
What is trusted
From the report
The Rust compiler, official Charon/Aeneas translation, standard-library slice/scalar models and Lean kernel are trusted. The proofs add no local axioms or custom standard-library models. Transitive theorem dependencies use only propext, Classical.choice and Quot.sound.
Technical limitations
From the report
Only decoded_len, encoded_len and From<Error> for core::fmt::Error are covered; general Display formatting is not proved. General-length hexadecimal encoding, decoding, character validation, destination writes, allocation and encode_str's unchecked UTF-8 conversion are not verified. encoded_len behavior above usize::MAX / 2 is outside the proved precondition. Other targets, feature configurations and release overflow behavior were not checked. The separate Display supplement covers only default formatting and this fixed writer, not arbitrary format flags/writers, partial-prefix error policies, other targets or feature configurations. It adds no Aeneas mapping. Encoded-length overflow remains outside the existing precondition. These five codec checks cover only source/destination lengths2/3 for decode and1/4 for encode, with independent1-byte roundtrip decode destinations. They do not prove arbitrary lengths/capacities, general failure-side prefix contents, encode_str UTF8 conversion, allocation or encoded_len overflow. Ordinary Kani supplements add no Aeneas mappings.
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