proofs.rs

Claim #79 — Verification of <usize as integer_encoding::VarInt>::encode_var_vec (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

<usize as integer_encoding::VarInt>::encode_var_vec

impl integer_encoding::VarInt for usize
pub fn encode_var_vec(self: Self) -> Vec<u8>

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

IntegerEncodingVec.usize_total

for allvalue : Aeneas.Std.Usize
for alldecode : Aeneas.Std.Slice Aeneas.Std.U8 → Aeneas.Std.Result (Option (Aeneas.Std.Usize × Aeneas.Std.Usize))
for allencodeVec : Aeneas.Std.Usize → Aeneas.Std.Result (Aeneas.Std.alloc.vec.Vec Aeneas.Std.U8)
then∃ out, integer_encoding.varint.VarInt.encode_var_vec.default (IntegerEncodingVec.sourceDictionary Aeneas.Std.core.marker.CopyUsize integer_encoding.Usize.Insts.Integer_encodingVarintVarInt.required_space integer_encoding.Usize.Insts.Integer_encodingVarintVarInt.encode_var decode encodeVec) value = Aeneas.Std.Result.ok out ∧ IntegerEncodingVec.EncodedVec (↑value) out

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

Complete Lean proposition
∀ (value : Aeneas.Std.Usize)
  (decode :
    Aeneas.Std.Slice.{0} Aeneas.Std.U8 →
      Aeneas.Std.Result.{0} (Option.{0} (Prod.{0, 0} Aeneas.Std.Usize Aeneas.Std.Usize)))
  (encodeVec : Aeneas.Std.Usize → Aeneas.Std.Result.{0} (Aeneas.Std.alloc.vec.Vec.{0} Aeneas.Std.U8)),
  @Exists.{1} (Aeneas.Std.alloc.vec.Vec.{0} Aeneas.Std.U8) fun (out : Aeneas.Std.alloc.vec.Vec.{0} Aeneas.Std.U8) =>
    And
      (@Eq.{1} (Aeneas.Std.Result.{0} (Aeneas.Std.alloc.vec.Vec.{0} Aeneas.Std.U8))
        (@integer_encoding.varint.VarInt.encode_var_vec.default.{0} Aeneas.Std.Usize
          (@IntegerEncodingVec.sourceDictionary Aeneas.Std.Usize Aeneas.Std.core.marker.CopyUsize
            integer_encoding.Usize.Insts.Integer_encodingVarintVarInt.required_space
            integer_encoding.Usize.Insts.Integer_encodingVarintVarInt.encode_var decode encodeVec)
          value)
        (@Aeneas.Std.Result.ok.{0} (Aeneas.Std.alloc.vec.Vec.{0} Aeneas.Std.U8) out))
      (IntegerEncodingVec.EncodedVec (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize value) out)

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/ed016e12463fdae695da11060d7e0d41b8b672b0/integer-encoding/4.1.0/aeneas/aeneas/profiles/default/proofs/VarintVec.lean#L99-L109

What is trusted

From the report

The result relies on Rust-to-Charon/Aeneas translation, Lean and the standard scalar and library models. The fixed-width supplement models size_of by scalar cardinality only for the ten selected primitive types, where the resulting 1, 2, 4 or 8 bytes agree with Rust's primitive sizes. Its clone_from_slice model copies bytes on equal lengths and panics otherwise; the extracted calls use the standard u8 clone implementation, not arbitrary user-defined cloning. Pointer-sized endian conversions use 64-bit primitives and preserve all bits under the stated 64-bit premise.

For fixed decoding, the model erases the formatting dictionary for the standard TryFromSliceError: the modeled unwrap still returns the Ok payload or panics on Err, but does not represent panic formatting or its effects. Source inspection supports these restricted model choices; it is not a proof of the Rust compiler or standard library. Allocation failures, panic text, hooks and unwinding effects are not established. The theorem audit allowed Lean's propext, Classical.choice and Quot.sound, with no application axioms.

Technical limitations

From the report

The checked executable bodies come from the locked crates.io 4.1.0 source, with generated bodies checked against fresh extraction. This is not a proof of compiler or translation correctness. The ten decode_var instances are blocked by the pinned translator and are not proved. Generic and asynchronous I/O, custom trait implementations and other unselected APIs are outside the formal scope. A destination shorter than the canonical varint is outside the successful encoding contract and may panic. The short-buffer theorem's modeled debug assertion does not describe release behavior or unwind state.

The accepted run is for macOS arm64; the separately maintained Linux models have not been accepted in this configuration. Native examples are finite observations, not proofs of the excluded I/O behavior or of big-endian execution.

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 →