smalloc-verify

Formal verification of pure-arithmetic functions from zooko/smalloc, using the Rust → Aeneas → Lean 4 pipeline.

Status

First target in scope: reqali_to_sc — the size-class mapping function the maintainer identified as the highest-leverage verification point (one-line function with a history of bugs).

What is verified

Function	Upstream location	Theorems
reqali_to_sc(siz, ali)	smalloc/src/lib.rs	reqali_to_sc_size_fits, reqali_to_sc_alignment_fits

Theorems proved:

1. reqali_to_sc_size_fits. Under safe preconditions on the inputs, the slot size 2 ^ reqali_to_sc(siz, ali) is at least max(siz, ali, SMALLEST_SLOT_SIZE).
2. reqali_to_sc_alignment_fits. Under safe preconditions, the alignment of the returned slot is at least ali (i.e. ali divides 2 ^ result).

Safe preconditions (matching upstream's debug_assert!s):

• siz ≥ 1
• ali ≥ 1
• ali is a power of two
• ali < 2³²

Pipeline

smalloc-arith/src/lib.rs           (standalone Rust crate)
        │
        ▼ Charon
smalloc_arith.llbc                 (typed intermediate representation)
        │
        ▼ Aeneas
lean/SmallocArith/{Types,Funs}.lean  (pure-functional Lean 4)
lean/SmallocArith/FunsExternal.lean  (hand-written model of usize::ilog2)
        │
        ▼ specifications + proofs
lean/SmallocArithVerif/BasicProofs.lean
        │
        ▼ Lean 4 kernel
Machine-checked theorems

Repository layout

smalloc-verify/
├── README.md
├── .gitignore
├── .github/workflows/ci.yml
├── smalloc-arith/                   # standalone Rust crate
│   ├── Cargo.toml
│   └── src/lib.rs                   # reqali_to_sc + supporting consts
├── smalloc_arith.llbc               # generated by Charon
└── lean/
    ├── lakefile.lean
    ├── lean-toolchain               # leanprover/lean4:v4.30.0-rc2 (matches Aeneas)
    ├── lake-manifest.json           # pins dependency revisions
    ├── SmallocArith.lean
    ├── SmallocArith/
    │   ├── Types.lean               # generated by Aeneas
    │   ├── Funs.lean                # generated by Aeneas
    │   ├── FunsExternal_Template.lean  # generated by Aeneas (template, not imported)
    │   └── FunsExternal.lean        # hand-written: model of usize::ilog2
    ├── SmallocArithVerif.lean
    └── SmallocArithVerif/
        └── BasicProofs.lean         # the proofs

Re-extracting Lean from Rust

cd smalloc-arith
nix run github:aeneasverif/aeneas#charon -L -- cargo --preset=aeneas
nix run github:aeneasverif/aeneas -L -- -backend lean -split-files *.llbc
# Move the generated Types.lean and Funs.lean into lean/SmallocArith/
# and the .llbc file into the repo root.

Aeneas also emits FunsExternal_Template.lean. Do not let it clobber the hand-written FunsExternal.lean (see "Notes on extraction" below): the template is regenerated each run, but FunsExternal.lean is maintained by hand. If a re-extraction introduces a new external function, the template will gain a new hole — diff it against FunsExternal.lean and port any additions over.

Building the proofs

cd lean
lake build

A clean build with no sorry and no unproved axioms is the deliverable.

Notes on extraction

Two things about the current Aeneas (Lean toolchain v4.30.0-rc2) are worth recording, since they differ from older walkthroughs:

• External functions are split into a separate, hand-completed file. Aeneas cannot translate usize::ilog2 (a std intrinsic), so it emits the function as a hole in FunsExternal_Template.lean. Funs.lean imports SmallocArith.FunsExternal (no _Template), so the build fails until the template is copied to FunsExternal.lean and the hole filled. This file is user-authored and committed.

• ilog2 is modelled, not rewritten. Rather than rewriting the Rust with leading_zeros, FunsExternal.lean gives ilog2 a computable model, ilog2 x = Nat.log 2 x.val (floor-log2), with a @[step] spec lemma. This keeps the Rust source byte-for-byte identical to upstream and replaces the template's opaque axiom with an honest definition, so the proofs rest on no unproved axiom beyond Lean/Mathlib's standard propext, Classical.choice, and Quot.sound.

Acknowledgements

Zooko (smalloc maintainer) identified reqali_to_sc as the highest-leverage verification target. Despite being one line of code, the function has had multiple bugs historically — exactly the shape where machine-checked proofs pay off.

This work uses the Aeneas / Charon / Lean 4 stack, building on patterns established in Verified-zkEVM/rust-lean.