proofs.rs

Claim #9 — Verification of crc::Crc<u32, Table<1>>::table (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

crc::Crc<u32, Table<1>>::table

Recorded callable · signature and safety not independently recorded.

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

CrcProofs.table_u32_l1_spec

for allc : crc_mono_anchors.crc.CrcU32Table1
then∃ out, crc_mono_anchors.crc.crc32.CrcU32Table1.table1 c = Aeneas.Std.Result.ok out ∧ out = c.data
Complete Lean proposition
∀ (c : crc_mono_anchors.crc.CrcU32Table1),
  @Exists.{1}
    (Aeneas.Std.Array.{0}
      (Aeneas.Std.Array.{0} Aeneas.Std.U32
        (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
          crc_mono_anchors.crc.CrcU128Table0._proof_1))
      (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
        crc_mono_anchors.crc.CrcU128Table1._proof_1))
    fun
      (out :
        Aeneas.Std.Array.{0}
          (Aeneas.Std.Array.{0} Aeneas.Std.U32
            (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
              crc_mono_anchors.crc.CrcU128Table0._proof_1))
          (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
            crc_mono_anchors.crc.CrcU128Table1._proof_1)) =>
    And
      (@Eq.{1}
        (Aeneas.Std.Result.{0}
          (Aeneas.Std.Array.{0}
            (Aeneas.Std.Array.{0} Aeneas.Std.U32
              (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                crc_mono_anchors.crc.CrcU128Table0._proof_1))
            (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
              crc_mono_anchors.crc.CrcU128Table1._proof_1)))
        (crc_mono_anchors.crc.crc32.CrcU32Table1.table1 c)
        (@Aeneas.Std.Result.ok.{0}
          (Aeneas.Std.Array.{0}
            (Aeneas.Std.Array.{0} Aeneas.Std.U32
              (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                crc_mono_anchors.crc.CrcU128Table0._proof_1))
            (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
              crc_mono_anchors.crc.CrcU128Table1._proof_1))
          out))
      (@Eq.{1}
        (Aeneas.Std.Array.{0}
          (Aeneas.Std.Array.{0} Aeneas.Std.U32
            (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
              crc_mono_anchors.crc.CrcU128Table0._proof_1))
          (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
            crc_mono_anchors.crc.CrcU128Table1._proof_1))
        out (crc_mono_anchors.crc.CrcU32Table1.data c))

Theorem source at recorded commit · Recorded check

Referenced definitions (up to 100 direct references)

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

Evidence

https://github.com/keiichiw/crate-proofs/blob/d0358890f8bdc8e72a376d225667ac162f89e3b8/crc/3.4.0/aeneas/profiles/default/proofs/CrcProofs/Table.lean#L41-L44

What is trusted

From the report

The proofs check a translated model of the Rust code and depend on Rust-to-LLBC translation (LLBC is the intermediate representation consumed by Aeneas), Aeneas translation, their primitive models, and the Lean kernel. These are not compiler-correctness proofs. The accepted audit permits only Lean's propext, Classical.choice, and Quot.sound as transitive axioms.

Technical limitations

From the report
  • Not established: These contracts do not establish that stored tables contain correct CRC transitions, that constructors produce them, or that checksums or digest updates are correct.
  • Outside scope: Custom implementations, other lanes and re-exported dependency APIs are outside the selected scope.
  • Supporting proofs: This profile also includes supporting polynomial-kernel proofs; they do not prove end-to-end checksums.

The verified source is taken from the locked crates.io 3.4.0 archive; the selected executable crate bodies are unchanged from that archive. The existing Rust-to-Lean translation (not rerun in this recording) and model correspondence checks support the correspondence between the proved Lean model and the release source; see Trusted assumptions for the translation boundary.

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 →