Report #31 — Base16 length calculations and formatting-error conversion

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

3 verified claims · 0 findings

Recorded by the author; proofs.rs has not re-run it. How to read a report

nyuichi · 2026-11-05 05:01 UTC

Revision v3 · v2 · v1

Overview

For base16ct 1.0.0, decoded_len terminates normally for every input slice. It returns Ok of exactly half the input length when that length is even, and Err(InvalidLength) exactly when it is odd. It examines length only, so this result does not validate hexadecimal characters. encoded_len returns exactly twice the input length without a panic when the length is at most usize::MAX / 2. The handwritten From<Error> conversion into core::fmt::Error always returns the formatting error value normally for either source error, intentionally discarding which error occurred. These are body proofs of the unchanged published APIs; the length proofs quantify arbitrary slice lengths representable in the model. Separately, original Error Display formatting under default {} flags and a fixed initialized64-byte writer returns exactly invalid Base16 encoding (23bytes) or invalid Base16 length (21bytes) for the corresponding variant. A writer that rejects the first literal before storing bytes instead propagates fmt::Error and retains its original length and bytes. Both variants and writer modes are symbolic; one Kani harness completes1910checks with no failures. Additional original-code Kani checks cover lower/upper/mixed decode for every2-byte input and every initial3-byte destination: success occurs exactly for the accepted alphabet, returns exactly1decoded byte, and preserves destination bytes1and2; invalid input returns InvalidEncoding while byte0 is not specified. Lower/upper encode checks cover every1-byte input and initial4-byte destination, return its exact canonical2ASCII bytes, preserve bytes2and3 and roundtrip through the actual decoder.

Findings (0)

No findings reported.

APIs (3)

Recorded callables

<core::fmt::Error as From<base16ct::Error>>::from recorded callable · signature and safety not recorded

Claim #3

decoded_len recorded callable · signature and safety not recorded

Claim #2

encoded_len recorded callable · signature and safety not recorded

Claim #1

Evidence

https://github.com/nyuichi/rust-crate-proofs/tree/9e4aa31960ae3b6b129ba88dd8aaa368df4111c3

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-31-source-1
git -C report-31-source-1 checkout --detach 9e4aa31960ae3b6b129ba88dd8aaa368df4111c3
git -C report-31-source-1 submodule update --init --recursive --checkout
cd report-31-source-1/base16ct/1.0.0/aeneas/2026-11-05/proofs

lake build +Proofs

printf '%s' 'import Lean
import Proofs
open Lean Elab Command

run_cmd do
  let theorem_name := `Proofs.encoded_len_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.encoded_len_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.encoded_len_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.encoded_len_spec"

run_cmd do
  let theorem_name := `Proofs.decoded_len_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.decoded_len_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.decoded_len_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.decoded_len_spec"

run_cmd do
  let theorem_name := `Proofs.error_to_fmt_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.error_to_fmt_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.error_to_fmt_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.error_to_fmt_spec"
' | lake env lean --stdin

Checks out the recorded source commit from GitHub. Install the report’s tool version before running.

Source on GitHub · SARIF with logs (.json)

Recorded run

Completed · 3 checks passed · 0 failed

2026-11-05T08:43:12.957712660+00:00 · 91.4 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem Proofs.encoded_len_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.encoded_len_spec`	Passed	Claim #1
Lean checked theorem Proofs.decoded_len_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.decoded_len_spec`	Passed	Claim #2
Lean checked theorem Proofs.error_to_fmt_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.error_to_fmt_spec`	Passed	Claim #3

Execution details

Started: 2026-11-05T08:43:12.957712660+00:00
Finished: 2026-11-05T08:44:44.374851094+00:00
Platform: linux x86_64
Rust compiler: rustc 1.100.0-nightly (923c95cdf 2026-09-16) binary: rustc commit-hash: 923c95cdf5ba65cea505aa2ea829f578e1506ed8 commit-date: 2026-09-16 host: x86_64-unknown-linux-gnu release: 1.100.0-nightly LLVM version: 23.1.1
Working directory: base16ct/1.0.0/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: 9e4aa31960ae3b6b129ba88dd8aaa368df4111c3

Diagnostics & logs

=== stdout ===
⚠ [2/11] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [3/530] Built Aeneas.Std.Global (40s)
✔ [4/530] Built AeneasMeta.UtilsCore (40s)
✔ [1797/1798] Built Generated.Base16ct (1.7s)
ℹ [1798/1798] Built Proofs (2.3s)
info: Proofs.lean:26:0: 'Proofs.encoded_len_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:27:0: 'Proofs.decoded_len_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:29:0: 'Proofs.error_to_fmt_spec' depends on axioms: [propext, Quot.sound]
Build completed successfully (1798 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.encoded_len_spec
proofs.rs:checked:Proofs.decoded_len_spec
proofs.rs:checked:Proofs.error_to_fmt_spec

=== stderr ===
info: aeneas: materializing new dependency
info: aeneas: fetching revision 'be86ab0f1989d04944292b345b24c435be3ad10a' from https://github.com/AeneasVerif/aeneas
info: aeneas: checking out revision 'be86ab0f1989d04944292b345b24c435be3ad10a'
info: mathlib: materializing new dependency
info: mathlib: fetching revision '56a005855ea17e0b0958f73ec801ae140b0a1679' from https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '56a005855ea17e0b0958f73ec801ae140b0a1679'
info: plausible: materializing new dependency
info: plausible: fetching revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24' from https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24'
info: LeanSearchClient: materializing new dependency
info: LeanSearchClient: fetching revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372' from https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372'
info: importGraph: materializing new dependency
info: importGraph: fetching revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93' from https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93'
info: proofwidgets: materializing new dependency
info: proofwidgets: fetching revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04' from https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04'
info: aesop: materializing new dependency
info: aesop: fetching revision '4a174c490d8707121c4a9290800489f105d85e07' from https://github.com/leanprover-community/aesop
info: aesop: checking out revision '4a174c490d8707121c4a9290800489f105d85e07'
info: Qq: materializing new dependency
info: Qq: fetching revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8' from https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8'
info: batteries: materializing new dependency
info: batteries: fetching revision '66e469188fe07963e5cf666c7d4433f45b8131c5' from https://github.com/leanprover-community/batteries
info: batteries: checking out revision '66e469188fe07963e5cf666c7d4433f45b8131c5'
info: Cli: materializing new dependency
info: Cli: fetching revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8' from https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8'

Environment

Original crates.io base16ct 1.0.0 source files and Cargo.toml, byte-compared against the archived release; default features, debug assertions enabled, x86_64-unknown-linux-gnu. Rust nightly-2026-09-17, Charon 08d7c9d50144bd84848212c24701253585e90d1f, Aeneas be86ab0f1989d04944292b345b24c435be3ad10a, Lean 4.35.0. Official targeted extraction; no Rust or generated Lean changes. A local cargo-proofs API-discovery patch recognizes the crate-owned Error argument in From<Error> for foreign core::fmt::Error; exact-one API resolution and axiom policy are unchanged. Display supplement: Kani0.68.0/CBMC6.11.0/Rust nightly2026-08-21,1910checks/0fail/125internalunreachable,11harnessproperties/3unsupportedguards,unwind80, archived completed original run independently audited. Metadata erratum corrects prior22/20 literal lengths to actual23/21; source/harness/log unchanged. evidence/kani-display. Additional bounded byte codec evidence:5Kani harnesses/1484checks/0fail, unwind8 assertions enabled, original archive-identical source, nightly2026-08-21/default/x86_64; evidence/kani-byte-codec.

What is trusted

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

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.

Updated 2026-10-16 00:00 UTC

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details

Dependencies (0)

No direct dependencies.

Comments (0)

No comments.