Standard library

Each library module in lean/std, lean/json and lean/data, with its purpose, main theorems and whether it has been accepted through a store.

The standard library is Lean source in lean/std/ (namespace LemaDraft.Std), with the JSON codec in lean/json/ and the byte and fixed-width integer bridges in lean/data/. Each module has a small specification that a person audits, implementations proved equal to it, and kernel-evaluated witnesses. Clients receive a module by the identities of its accepted objects. The module descriptions are in lean/std/README.md, the module .md files and lean/json/README.md.

Status words on this page:

Where the repository’s records disagree, this page gives the weaker status. Test files are under crates/lema-cli/tests/.

lean/std

Std.Text

UTF-8 text as bytes: a structure over ByteArray with Lean’s ByteArray.IsValidUTF8, not Lean’s String. The audited layer is three definitions: isAsciiUpper, specAsciiLowerByte and isAsciiByte.

Main theorems: validate_isSome, validate_bytes, isAscii_view, asciiLower_view, eqIgnoreAsciiCase_iff, ascii_valid, and the kernel-evaluated witnesses lower_header, eq_header, non_ascii.

theorem validate_isSome (b : ByteArray) : (validate b).isSome = true ↔ b.IsValidUTF8

theorem eqIgnoreAsciiCase_iff (a b : ByteArray) :
    eqIgnoreAsciiCase a b = true ↔
      a.size = b.size ∧ (Received.view a).map specAsciiLowerByte =
        (Received.view b).map specAsciiLowerByte

Validation uses Lean’s validator and Lean’s proof that it decides IsValidUTF8, which depends on Classical.choice. At run time the validator is Lean’s C function lean_string_validate_utf8, a reviewed extern assumed to match its Lean definition. The executable roots validate, isAscii, asciiLower, eqIgnoreAsciiCase and ascii? pass the executable vocabulary; validate is the one reviewed identity below which String operations are admitted. Not covered: full Unicode case mapping and case folding.

Status: accepted (std_text.rs); reverify agrees.

Std.Map

A finite-map Core v2 contract whose state is a function K → Option V, with keys ordered by a lawful total order (Order), and its first implementation, a sorted association list (impl). MapClient.lean is a client that receives the contract by identity.

Main theorems: impl_implements, put_then_get, put_then_get_runs, find_insert, find_delete, sorted_insert, sorted_delete, sorted_ext, the witness nat_example, and in MapClient.lean put_two_then_list.

theorem impl_implements {K V : Type} (o : Order K) :
    Received.Implements (contract (V := V) o) (impl o) (Rep o)

theorem put_then_get {K V : Type} (o : Order K) (k : K) (v : V)
    (s : K → Option V) :
    Received.Safe (contract o) (fun _ r => r = some v) (putThenGet k v) s

The toList promise can be kept only from a state with finitely many bindings, so a Safe claim through toList says nothing about other states. Not yet: the balanced tree, and an executable check of the map’s roots.

Status: accepted (std_map.rs); no theorem depends on Classical.choice; reverify agrees.

Std.Commute

Commutative steps of a certified actor step (received from lean/core/Actor.lean): two events commute at a state when either order gives each the same reply and ends in the same state. It licenses reordering, not running two steps on one state at once.

Main theorems: perm_run, run_front, run_inv, commute_symm, commute_fixed, commute_intro.

theorem perm_run (c : Received.CertifiedStep S E R) (k : CommutativeStep S E R c)
    {l₁ l₂ : List E} (p : l₁.Perm l₂) :
    ∀ s, Received.certInv c s → l₁.Pairwise (fun a b => k.disjoint a b = true) →
      (run (Received.certStep c) s l₁).1.Perm (run (Received.certStep c) s l₂).1 ∧
        (run (Received.certStep c) s l₁).2 = (run (Received.certStep c) s l₂).2

Status: accepted with the item store (kv.rs), whose app is retired (decision 0033); every receipt names propext and Quot.sound at most.

Std.Fixed

Fixed-point carriers Fixed16 s and Fixed64 s (a raw numerator over 2^s), checked Int64 arithmetic returning Except NumericError, explicitly named wrapping operations, and an Int16 dot product. Details are in lean/std/Fixed.md.

Main theorems: mulWide16_exact, add64_exact, sub64_exact, fromInt64_succeeds, fromInt64_overflow_iff, dotInt64_agrees.

theorem add64_exact {s : Nat} (a b r : Fixed64 s) (h : add64 a b = .ok r) :
    r.toInt = a.toInt + b.toInt

theorem dotInt64_agrees (xs ys : List Int16) (bound : xs.length < 8589934592) :
    (dotInt64 xs ys).toOption.map Int64.toInt = dotSpec xs ys

Status: accepted (std_fixed.rs); all receipts within propext and Quot.sound; the six executable roots are the accepted objects, and a client reuses dotInt64_agrees by identity.

Std.Fixed intervals

An extension of Std.Fixed, published with it: round-to-nearest-even rescaling, floor square root, and outward-rounded intervals Interval64 s. Details are in lean/std/Interval.md.

Main theorems: rescale64_exact, rescale64_nearest, roundEvenQuotient_spec, sqrt64_spec, floorSqrt_unique, add_encloses, mul_encloses, product_encloses.

theorem add_encloses {s : Nat} (a b r : Interval64 s) (x d y e : Int)
    (ha : Encloses a x d) (hb : Encloses b y e) (h : add a b = .ok r) :
    Encloses r (x*e + y*d) (d*e)

The square-root specifications depend on Classical.choice; rounding, enclosure and uniqueness need only propext and Quot.sound.

Status: checked locally (local draft measurements, not store acceptance); pending (std_interval.rs).

Std.Finite64

A finite binary64 wrapper whose arithmetic specifies Lean 4.34.1’s Float.Model. It does not enable native floating-point execution. Details are in lean/std/Finite64.md.

Main theorems: finiteBits_iff, fromBits_ok_iff, fromBits_error_iff, fromBits_toBits, add_model, sub_model, mul_model, div_model, sqrt_model, equal_iff.

theorem fromBits_toBits (x : Finite) : fromBits (toBits x) = .ok x

The executable vocabulary admits fromBits, toBits and equal, and refuses the five arithmetic roots because they reach Float.Model. The witnesses check the selected model and wrapper; they are not a proof of full IEEE 754 conformance.

Status: checked locally (local draft measurements, not store acceptance); pending (std_finite64.rs).

Std.Json

Part 1 of JSON: a proof-level codec on the integer-only JsonValue of lean/data/Json.lean. encode writes compact JSON; decode reads JSON with whitespace and refuses trailing commas, leading zeros, +, unescaped control bytes and trailing garbage.

Main theorems: decode_encode, parse_encode, and the witnesses refused and refused_valid.

theorem decode_encode (v : Received.JsonValue) (wf : WF v) : decode (encode v) = some v

The definitions are noncomputable over the received type: a checked reference, not an executable root. Fractions, exponents, \u escapes above 127, UTF-8 validity and unique member names are in the later codec, Json.

Status: accepted (std_json.rs); within propext and Quot.sound; reverify agrees.

Std.Canonical

Request canonicalisation for SigV4 and S3 over byte strings: lowercase hex, RFC 3986 percent-encoding and its S3 object-key variant, the canonical query string, canonical headers and the signed-header list, a length-prefixed tuple encoding, and a structural insertion sort. Details are in lean/std/Canonical.md.

Main theorems: hexDecode_encode, uriEncode_injective, uriEncodePath_segments, sortBy_perm, sortBy_sorted, sortBy_filter, eq_of_sorted_perm, canonicalQuery_perm, headerEntries_sorted, headerEntries_values, canonicalHeaders_injective, signedHeaders_injective, observationKey_injective.

theorem sortBy_perm {α : Type} (le : α → α → Bool) : ∀ l : List α, (sortBy le l).Perm l

theorem canonicalQuery_perm (qs qs' : List (List UInt8 × List UInt8)) (p : qs.Perm qs') :
    canonicalQuery qs = canonicalQuery qs'

The sort is structural so that the kernel can evaluate witnesses; List.mergeSort is defined by well-founded recursion and decide +kernel did not reduce it on a ten-element list. Tested locally: 248 executable vectors under lean --run, 91 of them from 18 cases of AWS’s SigV4 test suite.

Status: accepted, 16 Oct 2026 (std_canonical.rs, 7 native calls).

Std.Bytes

Byte slices (ByteSlice: len bytes of a ByteArray from off, with USize offsets and no copying), big-endian words, rotations and 64-byte blocks: the base for SHA-256. Details are in lean/std/Bytes.md.

Main theorems: loadBE32_spec, loadBE64_spec, foldBlocks_spec, sliceBoundsOK_iff, get_toList, rotl32_rotr32, toList_appendSlice, among its 130 theorems.

theorem loadBE32_spec (s : ByteSlice) (i : USize) (h : i.toNat + 4 ≤ s.len.toNat) :
    ofBytesBE32 ((s.toList.drop i.toNat).take 4) = some (s.loadBE32 i h)

theorem foldBlocks_spec {α : Type} (s : ByteSlice)
    (f : α → (b : ByteSlice) → b.len.toNat = 64 → α) (g : α → List UInt8 → α)
    (hfg : ∀ a b h, f a b h = g a b.toList) (init : α) :
    s.foldBlocks f init = (blocks64 s.toList).foldl g init

Status: accepted, 16 Oct 2026 (std_bytes.rs, 7 native calls), on a store whose policy is propext and Quot.sound, with its 29 executable roots checked by identity and a client (BytesClient.lean) that receives ByteSlice.

Std.Sha256Spec

FIPS 180-4 SHA-256 over byte lists and UInt32 words, one definition per FIPS 180-4 section. Every recursion is structural, so the kernel evaluates it. FIPS 180-4’s domain is Fits (8 * len < 2^64). Details are in lean/std/Sha256.md.

Main theorems: the known answers digest_empty, digest_abc, digest_msg448 and runs of a at the padding boundaries (55, 63, 64, 119 and 120 bytes), all by decide +kernel; K_cube_roots, H0_square_roots, padding_length, zeroCount_spec, digest_length.

theorem digest_abc : digest [0x61, 0x62, 0x63] =
    [0xba, 0x78, 0x16, 0xbf, 0x8f, 0x01, 0xcf, 0xea, 0x41, 0x41, 0x40, 0xde, 0x5d, 0xae, 0x22, 0x23,
     0xb0, 0x03, 0x61, 0xa3, 0x96, 0x17, 0x7a, 0x9c, 0xb4, 0x10, 0xff, 0x61, 0xf2, 0x00, 0x15, 0xad]

theorem digest_length (m : List UInt8) : (digest m).length = 32

Functional correctness is not collision resistance, which stays an assumption.

Status: accepted, 16 Oct 2026 (std_sha256.rs), 1,303 objects, reverify agreeing.

Std.Sha256

digestSlice, SHA-256 of a Std.Bytes slice, shaped for compiled execution and proved equal to the specification.

Main theorems: digestSlice_eq_spec, and the specification’s eight kernel-checked answers transferred through it (digestSlice_abc and the others).

theorem digestSlice_eq_spec (s : Received.Bytes.ByteSlice)
    (h : 8 * (Received.Bytes.ByteSlice.len s).toNat < 2 ^ 64) :
    digestSlice s h =
      ByteArray.mk (Received.Sha256Spec.digest (Received.Bytes.ByteSlice.toList s)).toArray

On a local IR capture, NoCopySliceCall holds and NoBigIntPrimitives and NoBoxOrCtorInCycles do not (each block allocates an array and a state). Tested, not checked: 1,030 interpreted checks against NIST’s vectors, the specification and sha256sum.

Status: accepted, 16 Oct 2026 (std_sha256_impl.rs, 8 native calls), with its 73 bindings and 79 theorem receipts.

Std.Sha256Unboxed

A second digestSlice, proved equal to the specification, whose hot path allocates nothing and does no Nat arithmetic. SigV4Payload.lean is a client that computes SigV4’s payload hash with it.

Main theorems: digestSlice_eq_spec, digest_a56, digest_a65, digest_a128; in SigV4Payload.lean, payloadHash_eq and digestSlice_eq_old.

theorem payloadHash_eq (s : Received.Bytes.ByteSlice)
    (h : 8 * (Received.Bytes.ByteSlice.len s).toNat < 2 ^ 64) :
    payloadHash s h = Received.SigV4.payloadHash (Received.Bytes.ByteSlice.toList s)

On a local IR capture all three profiles hold for the digest and its 15 helpers; they do not cover copies inside the runtime’s array operations. Tested: 827 digests of the leanc executable equal Rust’s sha2.

Status: checked locally; acceptance not confirmed. lean/std/README.md says the publication test (std_sha256_unboxed.rs) and the manifests’ test have not been run, while lean/std/Sha256.md records them as passed on 17 Oct 2026.

Std.Hmac

HMAC (FIPS 198-1, RFC 2104) specified once over byte lists for any hash (Hash: block size, output size and digest), then instantiated with Sha256Spec.digest as hmacSha256. Details are in lean/std/Hmac.md.

Main theorems: hmacSpec_congr, hmacSpec_congr_lt, hmacSha256_of_fits, hmacSha256_of_eq, sha256_lawful, and RFC 4231’s test cases case1 to case7 by decide +kernel.

theorem hmacSha256_of_fits (d : List UInt8 → List UInt8)
    (hd : ∀ m, Received.Sha256Spec.Fits m → d m = Received.Sha256Spec.digest m)
    {key msg : List UInt8} (hk : Received.Sha256Spec.Fits key)
    (hm : 8 * (64 + msg.length) < 2 ^ 64) :
    hmacSpec ⟨64, 32, d⟩ key msg = hmacSha256 key msg

Any digest function equal to Sha256Spec.digest on FIPS 180-4’s domain gives hmacSha256, without unfolding SHA-256 or HMAC. HMAC’s unforgeability is a cryptographic assumption, and pure-Lean HMAC has no constant-time guarantee.

Status: accepted, 16 Oct 2026 (std_hmac.rs, 6 native calls).

Std.SigV4

AWS Signature Version 4 for S3 PutObject (also conditional, If-None-Match: *), GetObject and HeadObject, over byte lists, composed from Std.Canonical, Std.Sha256Spec and Std.Hmac as received objects. The timestamp, region, service, access key and secret are inputs. Details are in lean/std/SigV4.md.

Main theorems: signature_eq, authorization_eq, signedHeaders_sorted, signedHeaders_names, signature_length, signature_lowerHex, signatureWith_of_fits, canonicalRequest_congr, among its 111 theorems.

theorem signature_eq (secret amzDate region service creq : List UInt8) :
    signature secret amzDate region service creq =
      Received.Canonical.hexEncode (Received.Hmac.hmacSha256
        (signingKey secret (dateStamp amzDate) region service)
        (stringToSign amzDate (credentialScope (dateStamp amzDate) region service) creq))

theorem signature_length (secret amzDate region service creq : List UInt8) :
    (signature secret amzDate region service creq).length = 64

Tested locally: 163 executable vectors, and a differential against curl’s --aws-sigv4 on 14 requests. SigV4’s security, S3’s server behaviour, the clock and constant-time execution are assumptions.

Status: accepted, 16 Oct 2026 (std_sigv4.rs, 10 native calls), 4,746 objects.

lean/json

Json

The JSON codec that compiles: decimal numbers in normal form (Number: mantissa × 10 ^ exponent), an RFC 8259 decoder with I-JSON’s UTF-8 and unique-name rules and explicit limits (nesting 64, 400 digits, exponent magnitude 400), and a compact encoder. Namespace LemaDraft.Json.

Main theorems: decode_encode, normalize_same, normalize_idem, normal_unique, distinctNames_iff, encode_normalizes, parseNumber_encode, stringBody_escape, parse_encode, and the witnesses decode_examples, decode_refusals, decode_limits.

theorem decode_encode (v : Value) (wf : WF v) : decode (encode v) = some v

theorem normal_unique (a b : Number) (na : a.Normal) (nb : b.Normal) (same : a.Same b) : a = b

decode and encode pass the executable vocabulary and are the accepted objects by identity (json_runs.rs). I-JSON’s rule against noncharacters is not applied. The accepted objects are also published as two bundles, Json and Json laws.

Status: accepted (json.rs); within propext and Quot.sound.

JsonGrammar

A declarative RFC 8259 and I-JSON grammar, Parses b v, received over the accepted Json.lean, and the proof that the decoder is exact. Namespace LemaDraft.JsonGrammar.

Main theorems: decode_iff (from decode_sound and decode_complete), parses_functional, decode_wf, parses_canonical, same_value_iff.

theorem decode_iff (b : List UInt8) (v : Received.Value) : Received.decode b = some v ↔ Parses b v

The grammar reuses byte tables, utf8Encode and the number laws from Json.lean, so decode_iff cannot catch an error in what the two share.

Status: accepted (json_grammar.rs); within propext and Quot.sound; a source-free reverify of its closure agrees.

JsonNumbers

Exact extraction from Json.Number: toIntExact and toMinorUnitsExact return Option, never round or saturate, and apply input limits before any power is computed. Namespace LemaDraft.JsonNumbers. Details are in lean/json/Numbers.md.

Main theorems: toIntExact_iff, toMinorUnitsExact_iff, integerValue_same.

theorem toIntExact_iff (n : Received.Number) (z : Int) :
    toIntExact n = some z ↔ Supported n ∧
      IntegerValue (Received.mantissa n) (Received.exponent n) z

Status: checked locally; pending. lean/json/Numbers.md describes the native acceptance test (json_numbers.rs) and records no run.

lean/json/Check.lean is a program over the Json bundles, not library code: its line_valid, line_invalid and line_encode were accepted when json_check.rs published it natively on 17 Oct 2026.

lean/data

Bytes

The specification-side view of a byte array, LemaDraft.Bytes.view, and bridge lemmas relating it to ByteArray. Executable code cannot call ByteArray.toList, which reads with get!.

Main theorems: view_getElem, view_getElem?, view_uget, view_push, view_append, view_set, view_toByteArray, toByteArray_view.

theorem view_getElem? (b : ByteArray) (i : Nat) : (view b)[i]? = b[i]?

Status: accepted (bytes.rs), part of M1, recorded done on 15 Oct 2026 in docs/roadmap.md.

Fixed-width integers

Lean’s own semantics for fixed-width integers, stated as kernel-checked theorems (division by zero, MIN / -1, shifts modulo the width, wrapping, conversions), and an Int64/Int bridge proved without Classical.choice. lean/data/lowering.md gives the safe-Rust equivalent of each operation. lean/data/Money.lean reuses the bridge by identity.

Main theorems: u64_div_zero, i64_min_div_neg_one, u8_add_wraps, u64_shift_left_mod_width, i8_shift_right_arithmetic, and the bridge i64_toInt_ge, i64_toInt_lt, i64_toInt_add_of_bounds, i64_toInt_sub_of_le.

theorem u64_div_zero (x : UInt64) : x / 0 = 0 := UInt64.div_zero
theorem i64_min_div_neg_one : Int64.minValue / -1 = Int64.minValue := Int64.minValue_div_neg_one
theorem u64_shift_left_mod_width : (1 : UInt64) <<< 65 = 2 := by decide

Status: accepted (data.rs), part of M1, recorded done on 15 Oct 2026 in docs/roadmap.md; within propext and Quot.sound.