proofs.rs

Claim #3 — Verification of adler2::Adler32::new (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

adler2::Adler32::new

impl Adler32
pub fn new() -> Self

Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

This claim has no explanation of its own. Read the report Overview, and treat the formal statement below as authoritative. See Concepts and terminology.

Preconditions

true

Formal statement

adler2.new_spec

thenadler2.Adler32.new = Aeneas.Std.Result.ok { a := 1#u16, b := 0#u16 }
Complete Lean proposition
@Eq.{1} (Aeneas.Std.Result.{0} adler2.Adler32) adler2.Adler32.new
  (@Aeneas.Std.Result.ok.{0} adler2.Adler32
    (adler2.Adler32.mk
      (Aeneas.Std.U16.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) adler2.new_spec._proof_1)
      (Aeneas.Std.U16.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) adler2.new_spec._proof_2)))

Theorem source at recorded commit · Recorded check

Referenced definitions (up to 100 direct references)
  • Eq · Init.Prelude
  • Aeneas.Std.Result · Aeneas.Std.Primitives
  • adler2.Adler32
  • adler2.Adler32.new
  • Aeneas.Std.Result.ok · Aeneas.Std.Primitives
  • adler2.Adler32.mk
  • Aeneas.Std.U16.ofNat · Aeneas.Std.Scalar.Core
  • OfNat.ofNat · Init.Prelude
  • Nat · Init.Prelude
  • instOfNatNat · Init.Prelude
  • adler2.new_spec._proof_1 · Proofs.Smoke
  • adler2.new_spec._proof_2 · Proofs.Smoke

Mapping: manual. Translation was not rerun by this recording.

Evidence

https://github.com/keiichiw/crate-proofs/blob/5c4e0f729b5bd557451157346250211069968474/adler2/2.0.1/proofs/Proofs/Smoke.lean#L10-L13

What is trusted

From the report

Trusted boundaries

  • Translation: the pinned Charon/Aeneas Rust-to-LLBC-to-Lean translation.
  • Library models: the correspondence between Aeneas standard-library models
    and Rust, including slice and iterator semantics.
  • Proof checking: the Lean kernel. The transitive theorem audit permits only
    propext, Classical.choice, and Quot.sound.

The audit rejects sorryAx, custom axioms, and native-decision axioms. The
algorithm contracts do not assume correctness of the optimized compute body.

Technical limitations

From the report

Scope exclusions

This report concerns the computation core under default Cargo features for the
macOS arm64 extraction target. It does not establish whole-crate correctness.
The following remain outside the formal scope:

  • Generic BufRead I/O and its error behavior.
  • Derived traits and Hasher laws.
  • no_std configurations and alternative targets.

Native no_std tests are separate finite observations, not formal proofs for
that configuration.

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

Read and join the discussion on the report →