proofs.rs

Claim #1 — Verification of <block_padding::ZeroPadding as block_padding::Padding>::raw_pad (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

<block_padding::ZeroPadding as block_padding::Padding>::raw_pad

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

pos ≤ block.len()

Formal statement

BlockPadding.Proof.zero_pad_total

for allb : Aeneas.Std.Slice Aeneas.Std.U8
for allp : Aeneas.Std.Usize
assumeh : ↑p ≤ b.length
then∃ out, block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_pad b p = Aeneas.Std.Result.ok out ∧ BlockPadding.Proof.bytes out = BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.zero (BlockPadding.Proof.bytes b) ↑p

In Lean notation, ↑ denotes an implicit type conversion (coercion).

Complete Lean proposition
∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8) (p : Aeneas.Std.Usize)
  (h :
    @LE.le.{0} Nat instLENat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)
      (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b)),
  @Exists.{1} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>
    And
      (@Eq.{1} (Aeneas.Std.Result.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8))
        (block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_pad b p)
        (@Aeneas.Std.Result.ok.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) out))
      (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)
        (BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.zero (BlockPadding.Proof.bytes b)
          (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)))

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/MasWag/crate-proofs/blob/8ffde6cb60a5f280528cc3759b03663db8e0b7d6/block-padding/0.4.2/aeneas/profiles/default/proofs/Proofs.lean#L108-L111

What is trusted

From the report

The claims rely on the pinned Charon and Aeneas translation, their Rust slice and integer models, and the Lean kernel. Source correspondence is based on review rather than a formal equivalence proof. The two decoder iterator checks were rewritten as explicit loops in the verification harness: each scans the same suffix and rejects upon the first byte that differs from the required value. This source reasoning has been independently reviewed, but equivalence of the adapted bodies to the published release has not been formally proved.

Technical limitations

From the report

These are selected raw-method contracts, not verification of the entire crate. They do not establish behavior outside the stated domains or prove the panic boundaries. Typed array methods, detached padding, block-list unpadding, and the hybrid-array representation bridge remain unproved. Generic extraction attempts encountered translation or model boundaries; these attempts do not establish that verification is impossible. Native tests are separate from the formal claims. In particular, empty input causes three raw decoders to panic despite the trait documentation's malformed-padding error statement, as described in the finding.

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 →