Quantized Matrix Operations

This module provides the foundation for Transformer verification: Matrix-Matrix multiplication for Intervals.

Key Definitions

• IntMatrix - Flattened array of integers (row-major)
• IntervalMatrix - Structure-of-Arrays interval matrix
• matmul - Verified interval matrix multiplication

Integer Matrix (Data Layer)

structure LeanCert.ML.Optimized.IntMatrix (rows cols : ℕ) : Type

A dense integer matrix stored in row-major format.

• data : Array ℤ
• size_eq : self.data.size = rows * cols

instance LeanCert.ML.Optimized.instReprIntMatrix {rows✝ cols✝ : ℕ} : Repr (IntMatrix rows✝ cols✝)

Equations

• LeanCert.ML.Optimized.instReprIntMatrix = { reprPrec := LeanCert.ML.Optimized.instReprIntMatrix.repr }

def LeanCert.ML.Optimized.instReprIntMatrix.repr {rows✝ cols✝ : ℕ} : IntMatrix rows✝ cols✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def LeanCert.ML.Optimized.IntMatrix.get {r c : ℕ} (M : IntMatrix r c) (i j : ℕ) (hi : i < r) (hj : j < c) : ℤ

Get element at (r, c)

Equations

• M.get i j hi hj = M.data[i * c + j]

def LeanCert.ML.Optimized.IntMatrix.ofFn {r c : ℕ} (f : Fin r → Fin c → ℤ) : IntMatrix r c

Create a matrix from a function

Equations

• LeanCert.ML.Optimized.IntMatrix.ofFn f = if hc : c = 0 then { data := #[], size_eq := ⋯ } else { data := Array.ofFn (LeanCert.ML.Optimized.IntMatrix.flatToElem✝ f hc), size_eq := ⋯ }

@[simp]

theorem LeanCert.ML.Optimized.IntMatrix.ofFn_get {r c : ℕ} (f : Fin r → Fin c → ℤ) (i : Fin r) (j : Fin c) : (ofFn f).get ↑i ↑j ⋯ ⋯ = f i j

Get an element from an ofFn matrix

def LeanCert.ML.Optimized.IntMatrix.transpose {r c : ℕ} (M : IntMatrix r c) : IntMatrix c r

Matrix Transpose

Equations

• M.transpose = LeanCert.ML.Optimized.IntMatrix.ofFn fun (i : Fin c) (j : Fin r) => M.get ↑j ↑i ⋯ ⋯

def LeanCert.ML.Optimized.IntMatrix.zero (r c : ℕ) : IntMatrix r c

Zero matrix

Equations

• LeanCert.ML.Optimized.IntMatrix.zero r c = LeanCert.ML.Optimized.IntMatrix.ofFn fun (x : Fin r) (x_1 : Fin c) => 0

Interval Matrix (Verification Layer)

structure LeanCert.ML.Optimized.IntervalMatrix (rows cols : ℕ) : Type

Interval Matrix in SoA layout (separate lo/hi matrices)

• lo : IntMatrix rows cols
• hi : IntMatrix rows cols

def LeanCert.ML.Optimized.IntervalMatrix.getBounds {r c : ℕ} (M : IntervalMatrix r c) (i j : ℕ) (hi : i < r) (hj : j < c) : ℤ × ℤ

Get the interval bounds at (i, j) as a pair

Equations

• M.getBounds i j hi hj = (M.lo.get i j hi hj, M.hi.get i j hi hj)

@[inline]

def LeanCert.ML.Optimized.IntervalMatrix.intervalMul (l1 h1 l2 h2 : ℤ) : ℤ × ℤ

Interval Arithmetic Product

Computes [l1, h1] * [l2, h2]. Result lo = min(l1l2, l1h2, h1l2, h1h2) Result hi = max(l1l2, l1h2, h1l2, h1h2)

Equations

• LeanCert.ML.Optimized.IntervalMatrix.intervalMul l1 h1 l2 h2 = (min (min (l1 * l2) (l1 * h2)) (min (h1 * l2) (h1 * h2)), max (max (l1 * l2) (l1 * h2)) (max (h1 * l2) (h1 * h2)))

@[inline]

def LeanCert.ML.Optimized.IntervalMatrix.intervalAdd (l1 h1 l2 h2 : ℤ) : ℤ × ℤ

Interval addition of two pairs

Equations

• LeanCert.ML.Optimized.IntervalMatrix.intervalAdd l1 h1 l2 h2 = (l1 + l2, h1 + h2)

def LeanCert.ML.Optimized.IntervalMatrix.matmul {n m p : ℕ} (A : IntervalMatrix n m) (B : IntervalMatrix m p) : IntervalMatrix n p

Matrix-Matrix Multiplication

C = A × B where A is (n × m) and B is (m × p).

This implements the standard O(N³) loop but lifting operations to intervals. Unlike vector-matrix mul, we cannot easily decompose into Pos/Neg weights because both inputs are variable intervals.

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.ML.Optimized.IntervalMatrix.transpose {r c : ℕ} (M : IntervalMatrix r c) : IntervalMatrix c r

Transpose an interval matrix

Equations

• M.transpose = { lo := M.lo.transpose, hi := M.hi.transpose }

def LeanCert.ML.Optimized.IntervalMatrix.zero (r c : ℕ) : IntervalMatrix r c

Zero interval matrix (all zeros)

Equations

• LeanCert.ML.Optimized.IntervalMatrix.zero r c = { lo := LeanCert.ML.Optimized.IntMatrix.zero r c, hi := LeanCert.ML.Optimized.IntMatrix.zero r c }

def LeanCert.ML.Optimized.IntervalMatrix.ofFn {r c : ℕ} (f : Fin r → Fin c → ℤ × ℤ) : IntervalMatrix r c

Create from function

Equations

• One or more equations did not get rendered due to their size.

Semantics and Correctness

noncomputable def LeanCert.ML.Optimized.intVal (x exp : ℤ) : ℝ

Value of integer as real given an exponent (2^exp scaling)

Equations

• LeanCert.ML.Optimized.intVal x exp = ↑x * 2 ^ exp

theorem LeanCert.ML.Optimized.intVal_mul (x y e : ℤ) : intVal x e * intVal y e = intVal (x * y) (e + e)

Multiplication of scaled values: intVal x e * intVal y e = intVal (x*y) (e+e)

theorem LeanCert.ML.Optimized.intVal_add (x y e : ℤ) : intVal x e + intVal y e = intVal (x + y) e

intVal distributes over addition

noncomputable def LeanCert.ML.Optimized.IntMatrix.valAt {r c : ℕ} (M : IntMatrix r c) (exp : ℤ) (i : Fin r) (j : Fin c) : ℝ

Value of integer matrix entry given an exponent

Equations

• M.valAt exp i j = LeanCert.ML.Optimized.intVal (M.get ↑i ↑j ⋯ ⋯) exp

def LeanCert.ML.Optimized.IntervalMatrix.mem {r c : ℕ} (M : IntervalMatrix r c) (exp : ℤ) (A_real : Matrix (Fin r) (Fin c) ℝ) : Prop

Membership in IntervalMatrix

Equations

• M.mem exp A_real = ∀ (i : Fin r) (j : Fin c), M.lo.valAt exp i j ≤ A_real i j ∧ A_real i j ≤ M.hi.valAt exp i j

Foldl to Finset.sum conversion

theorem LeanCert.ML.Optimized.finRange_foldl_add_eq_sum {α : Type u_1} [AddCommMonoid α] {m : ℕ} (f : Fin m → α) : List.foldl (fun (acc : α) (j : Fin m) => acc + f j) 0 (List.finRange m) = Finset.univ.sum f

Key lemma: foldl with addition over List.finRange equals Finset.univ.sum. This converts the computational foldl in matmul to the mathematical Finset.sum.

Int to Real cast lemmas for foldl

theorem LeanCert.ML.Optimized.Int_cast_foldl_add {β : Type u_1} (l : List β) (f : β → ℤ) : ↑(List.foldl (fun (acc : ℤ) (b : β) => acc + f b) 0 l) = List.foldl (fun (acc : ℝ) (b : β) => acc + ↑(f b)) 0 l

Int.cast distributes over foldl with addition

Helper for sum inequalities

Interval Multiplication Soundness

theorem LeanCert.ML.Optimized.intervalMul_sound (l1 h1 l2 h2 : ℤ) (x y : ℝ) (hx_lo : ↑l1 ≤ x) (hx_hi : x ≤ ↑h1) (hy_lo : ↑l2 ≤ y) (hy_hi : y ≤ ↑h2) : match IntervalMatrix.intervalMul l1 h1 l2 h2 with | (lo, hi) => ↑lo ≤ x * y ∧ x * y ≤ ↑hi

The interval multiplication is sound: if x ∈ [l1, h1] and y ∈ [l2, h2], then x * y ∈ [intervalMul.lo, intervalMul.hi]

theorem LeanCert.ML.Optimized.intervalMul_sound_scaled (l1 h1 l2 h2 : ℤ) (x y : ℝ) (exp : ℤ) (hx_lo : intVal l1 exp ≤ x) (hx_hi : x ≤ intVal h1 exp) (hy_lo : intVal l2 exp ≤ y) (hy_hi : y ≤ intVal h2 exp) : match IntervalMatrix.intervalMul l1 h1 l2 h2 with | (lo, hi) => intVal lo (exp + exp) ≤ x * y ∧ x * y ≤ intVal hi (exp + exp)

Scaled version of intervalMul_sound using intVal with exponents. If x ∈ [intVal l1 exp, intVal h1 exp] and y ∈ [intVal l2 exp, intVal h2 exp], then x * y ∈ [intVal lo (exp+exp), intVal hi (exp+exp)] where (lo, hi) = intervalMul l1 h1 l2 h2.

theorem LeanCert.ML.Optimized.mem_transpose {r c : ℕ} (M : IntervalMatrix r c) (exp : ℤ) (A_real : Matrix (Fin r) (Fin c) ℝ) (hM : M.mem exp A_real) : M.transpose.mem exp A_real.transpose

Soundness of Matrix Transpose

If A_real ∈ A_interval, then A_realᵀ ∈ A_intervalᵀ. The exponent is preserved.

theorem LeanCert.ML.Optimized.mem_matmul {n m p : ℕ} (A : IntervalMatrix n m) (B : IntervalMatrix m p) (Ar : Matrix (Fin n) (Fin m) ℝ) (Br : Matrix (Fin m) (Fin p) ℝ) (exp : ℤ) (hA : A.mem exp Ar) (hB : B.mem exp Br) : (A.matmul B).mem (exp + exp) (Ar * Br)

Main Theorem: Soundness of Matrix Multiplication

If A_real ∈ A_interval and B_real ∈ B_interval, then (A_real * B_real) ∈ (A_interval * B_interval).

Note: Exponents add. If A has exp e and B has exp e, result has 2e.