Porting s2n-bignum to Lean 4

Alexandre Rademaker

FGV/EMAp | CSLib at Renaissance Philanthropy

INRIA Paris 2026

Part 1: The s2n-bignum Library

What is s2n-bignum?

s2n-bignum is a collection of integer arithmetic routines designed for cryptographic applications. All routines are written in pure machine code, designed to be callable from C and other high-level languages, with separate but API-compatible versions of each function for 64-bit x86 (x86_64) and ARM (aarch64).

https://github.com/awslabs/s2n-bignum

Primary goals: performance and assurance

What Does It Provide?

• Elementary 64-bit word operations

• Generic bignum arithmetic: addition, subtraction, multiplication, comparison

• Constant-time data manipulation

• Montgomery operations for modular arithmetic

• Optimized operations for elliptic curves:

  • Curve25519, NIST P-256/384/521, secp256k1, SM2

Constant-Time Design

The actual sequence of machine instructions executed, including the specific addresses and sequencing of memory loads and stores, is independent of the numbers themselves, depending only on their nominal sizes.

Consequences:

• No stripping of leading zeros, no dynamic memory allocation

• Results that do not fit are truncated modulo the output size

• Sizes are explicit parameters — fixed at call time

void bignum_mul(uint64_t p, uint64_t *z,
                uint64_t m, uint64_t *x,
                uint64_t n, uint64_t *y);

x is an m-digit bignum, y is n-digit; result written to p-word buffer z.

Formal Verification in HOL Light

Each function ships with a machine-checked proof in HOL Light:

• Proves the mathematical result is correct

• Based on a formal model of the underlying processor (ARM or x86)

• The model specifies exactly how each instruction modifies registers, flags, and memory

Two logics, both mechanized in HOL Light:

• L1 (unary): functional correctness via Hoare triples — eventually operator, ~860K lines of proofs covering 600+ routines. It is implemented in 10k lines of HOL Light.

• L2 (relational): extends L1 with step-counting eventually to prove constant-time behavior and equivalence between optimized and reference implementations. The core of the relational verification amounts to 1704 lines of code.

Why is this relevant?

• Relational Hoare Logic for Realistically Modelled Machine Code.

• Formal verification makes RSA faster — and faster to deploy

• Better-performing “25519” elliptic-curve cryptography

• Dan J. Bernstein (creator of elliptic curve Curve25519) "OpenSSL/BoringSSL must use s2n-bignum!"

Library Structure (HOL Light)

s2n-bignum/
├── arm/
│   ├── proofs/          # ~351 HOL Light files
│   │   ├── bignum_add.ml
│   │   ├── bignum_mul.ml
│   │   └── ...
│   └── tutorial/        # introductory examples
│       ├── simple.ml
│       └── sequence.ml
├── x86/
│   └── proofs/          # x86-64 proofs (similar structure)
└── common/
    └── bignum.ml        # core definitions

Why HOL Light?

• Because John Harrison is the creator of HOL Light!

• HOL Light is an interactive theorem prover, like Lean

Verifying Assembly in s2n-bignum

Why Port to Lean 4?

• Lean 4 advantages:

  • Same language for code and proofs — no translation layer

  • Mathlib: 2M+ lines of mathematics, growing fast

  • Active community, modern tooling (Lake, LSP, VS Code)

  • Lean is implemented in Lean — highly extensible

  • Performance

• Goal: make this verification infrastructure accessible to the broader Lean community

Part 3: General Model

Hoare-Style Specifications

We use ensures triples — Hoare logic adapted to machine code:

• pre: precondition on initial state

• post: relates initial and final state (allows frame reasoning)

• frame: memory and registers not mentioned are unchanged

Compositionality

Programs compose sequentially:

theorem ensures_sequence
    (pre mid post : ArmState → Prop)
    (prog₁ prog₂  : List UInt8) :
    ensures pre prog₁ mid →
    ensures mid prog₂ post →
    ensures pre (prog₁ ++ prog₂) post

This enables modular proofs — verify each chunk independently.

Part 4: Lean vs HOL Light

Key Differences: Proofs

HOL Light (OCaml meta-language):

let HIGH_LOW_DIGITS = prove
 (`(!n i. 2 EXP (64 * i) * highdigits n i + lowdigits n i = n) /\
   (!n i. lowdigits n i + 2 EXP (64 * i) * highdigits n i = n) /\
   (!n i. highdigits n i * 2 EXP (64 * i) + lowdigits n i = n) /\
   (!n i. lowdigits n i + highdigits n i * 2 EXP (64 * i) = n)`,
  REWRITE_TAC[lowdigits; highdigits] THEN
  MESON_TAC[DIVISION_SIMP; ADD_SYM; MULT_SYM]);;

Lean 4 (same language as definitions):

Every Lean definition maps back to its HOL Light source equivalence.

Lean Project Structure

bignum-lean/
├── Bignum/
│   ├── Common/
│   │   ├── Basic/
│   │   │   ├── Defs.lean       # bigdigit, highdigits, lowdigits
│   │   │   └── Lemmas.lean     # core theorems (complete)
│   │   ├── Word.lean           # BitVec 64 arithmetic
│   │   └── Memory.lean         # memory model
│   └── Arm/
│       ├── Machine/            # State, Instruction, Decode, Loader
│       ├── Spec.lean           # ensures + operational semantics
│       ├── Tactic.lean         # proof automation
│       └── Tutorial/           # Simple.lean, Sequence.lean
└── s2n-bignum/                 # original HOL Light (git submodule)

Part 5: Two Tutorials

Tutorial 1: Simple

Port of s2n-bignum/arm/tutorial/simple.ml

0:   8b000022        add     x2, x1, x0
4:   cb010042        sub     x2, x2, x1

Tutorial 1: The Claim

Starting with X0 = a, X1 = b, after both instructions: X2 = a. Only PC and X2 change.

theorem SIMPLE_SPEC (pc a b : ℕ) :
    ensures arm
      (fun s => aligned_bytes_loaded s.mem (BitVec.ofNat 64 pc) simple_mc ∧
                s.read_reg Reg.PC = BitVec.ofNat 64 pc ∧
                s.read_reg Reg.X0 = BitVec.ofNat 64 a ∧
                s.read_reg Reg.X1 = BitVec.ofNat 64 b)
      (fun s => s.read_reg Reg.PC = BitVec.ofNat 64 (pc + 8) ∧
                s.read_reg Reg.X2 = BitVec.ofNat 64 a)
      (maychange_regs [Reg.PC, Reg.X2]) := by

Tutorial 1: Proof Strategy

• 1. Decode: bytes → Instruction list (2 lines)

• 2. Post: postcondition holds after exec (10 lines)

• 3. Frame: other registers unchanged (5 lines)

Tutorial 2: Sequence

Port of s2n-bignum/arm/tutorial/sequence.ml

0:   8b000021        add     x1, x1, x0
4:   8b000042        add     x2, x2, x0
8:   d2800043        mov     x3, #0x2
c:   9b037c21        mul     x1, x1, x3

Tutorial 2: The Approach

1. Split at pc+8 into two chunks:

   • First chunk (pc to pc+8): two add instructions

   • Second chunk (pc+8 to pc+16): mov and mul

2. Intermediate assertion at pc+8: X1 = a + b

3. Prove each chunk with ensures_of_exec, compose with ensures_sequence.

Tutorial 2: Proof by Composition

theorem sequence_correct (pc a b c : ℕ) :
    ensures arm
      (sequence_pre pc a b c)
      (sequence_post pc a b)
      (maychange_regs [Reg.PC, Reg.X1, Reg.X2, Reg.X3]) :=
  ensures_sequence _ _ _
    (maychange_regs [Reg.PC, Reg.X1, Reg.X2, Reg.X3])
    (sequence_chunk1_correct pc a b c)
    (sequence_chunk2_correct pc a b)
    (maychange_regs_trans _)

Original HOL Light: ~185 lines. Lean port: ~100 lines.

Part 6: Next Steps

Conclusion

• First version of ARM architecture

• First two tutorials completed

• Building the Lean project is faster than load HOL Light

High-level integration

• Connect to CSLib

• Connect to Mathlib

• End-to-end proofs from algorithm to assembly

Next Steps

1. Port ARM arithmetic algorithm proofs

   • bignum_add, bignum_mul, bignum_sub, modular reduction...

   • Revise infrastructure (Spec, Tactic, Decode) in place

2. x86-64 support

   • Adapt the ARM machine model for x86-64

   • Port the x86 proofs from s2n-bignum

3. Relational verification (see the paper)

   • Constant-time proofs

   • Functional equivalence between optimized and verification-friendly routines

Thank You

Alexandre Rademaker

FGV/EMAp | CSLib

github.com/atlas-computing-org/bignum

arademaker@gmail.com