Claim #12 — Verification of <i32 as integer_encoding::FixedInt>::encode_fixed_vec (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

<i32 as integer_encoding::FixedInt>::encode_fixed_vec

impl integer_encoding::FixedInt for i32
pub fn encode_fixed_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

IntegerFixedVecProofs.i32_total

for alld : integer_encoding.fixed.FixedInt Aeneas.Std.I32 (Aeneas.Std.Array Aeneas.Std.U8 4#usize)

for allx : Aeneas.Std.I32

then∃ out, integer_encoding.fixed.FixedInt.encode_fixed_vec.default (IntegerFixedVecProofs.specialize d IntegerFixedDirect.I32.Insts.Integer_encodingFixedFixedIntArrayU84.encode_fixed_light) x = Aeneas.Std.Result.ok out ∧ List.map (fun b => ↑b) ↑out = IntegerEncodingSpec.fixedBytes 4 x.bv.toNat

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

Complete Lean proposition

∀
  (d :
    integer_encoding.fixed.FixedInt.{0, 0} Aeneas.Std.I32
      (Aeneas.Std.Array.{0} Aeneas.Std.U8
        (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
          (@of_decide_eq_true
            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
            (@id.{0}
              (@Eq.{1} Bool
                (@Decidable.decide
                  (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
                    (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                  (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
                    (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                Bool.true)
              (@Eq.refl.{1} Bool Bool.true))))))
  (x : Aeneas.Std.I32),
  @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.fixed.FixedInt.encode_fixed_vec.default.{0, 0} Aeneas.Std.I32
          (Aeneas.Std.Array.{0} Aeneas.Std.U8
            (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
              (@of_decide_eq_true
                (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
                  (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
                  (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                (@id.{0}
                  (@Eq.{1} Bool
                    (@Decidable.decide
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                    Bool.true)
                  (@Eq.refl.{1} Bool Bool.true)))))
          (@IntegerFixedVecProofs.specialize Aeneas.Std.I32
            (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
              (@of_decide_eq_true
                (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
                  (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
                  (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                (@id.{0}
                  (@Eq.{1} Bool
                    (@Decidable.decide
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                    Bool.true)
                  (@Eq.refl.{1} Bool Bool.true))))
            d IntegerFixedDirect.I32.Insts.Integer_encodingFixedFixedIntArrayU84.encode_fixed_light)
          x)
        (@Aeneas.Std.Result.ok.{0} (Aeneas.Std.alloc.vec.Vec.{0} Aeneas.Std.U8) out))
      (@Eq.{1} (List.{0} Nat)
        (@List.map.{0, 0} Aeneas.Std.U8 Nat
          (fun (b : Aeneas.Std.U8) => @Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 b)
          (@Aeneas.Std.alloc.vec.Vec.val.{0} Aeneas.Std.U8 out))
        (IntegerEncodingSpec.fixedBytes (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
          (@BitVec.toNat (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32))) (Aeneas.Std.I32.bv x))))

Theorem source at recorded commit · Recorded check

Referenced definitions (up to 100 direct references)

integer_encoding.fixed.FixedInt
Aeneas.Std.I32 · Aeneas.Std.Scalar.Core
Aeneas.Std.Array · Aeneas.Std.Array.Array
Aeneas.Std.U8 · Aeneas.Std.Scalar.Core
Aeneas.Std.Usize.ofNat · Aeneas.Std.Scalar.Core
OfNat.ofNat · Init.Prelude
Nat · Init.Prelude
instOfNatNat · Init.Prelude
of_decide_eq_true · Init.Prelude
LE.le · Init.Prelude
instLENat · Init.Prelude
Aeneas.Std.UScalar.cMax · Aeneas.Std.Scalar.Core
Aeneas.Std.UScalarTy.Usize · Aeneas.Std.Scalar.Core
Nat.decLe · Init.Prelude
id · Init.Prelude
Eq · Init.Prelude
Bool · Init.Prelude
Decidable.decide · Init.Prelude
Bool.true · Init.Prelude
Eq.refl · Init.Prelude
Exists · Init.Core
Aeneas.Std.alloc.vec.Vec · Aeneas.Std.Alloc.Vec
And · Init.Prelude
Aeneas.Std.Result · Aeneas.Std.Primitives
integer_encoding.fixed.FixedInt.encode_fixed_vec.default
IntegerFixedVecProofs.specialize
IntegerFixedDirect.I32.Insts.Integer_encodingFixedFixedIntArrayU84.encode_fixed_light
Aeneas.Std.Result.ok · Aeneas.Std.Primitives
List · Init.Prelude
List.map · Init.Prelude
Aeneas.Std.UScalar.val · Aeneas.Std.Scalar.Core
Aeneas.Std.UScalarTy.U8 · Aeneas.Std.Scalar.Core
Aeneas.Std.alloc.vec.Vec.val · Aeneas.Std.Alloc.Vec
IntegerEncodingSpec.fixedBytes
BitVec.toNat · Init.Prelude
Aeneas.Std.I32.bv · Aeneas.Std.Scalar.Core

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/FixedVec.lean#L68-L72

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 →