Optimized Interval Arrays (Structure-of-Arrays Layout)

This module implements a cache-friendly interval vector representation using Structure-of-Arrays (SoA) layout instead of Array-of-Structures (AoS).

Key Optimization: SoA Layout

Instead of:

Array IntervalDyadic = [⟨lo₁, hi₁⟩, ⟨lo₂, hi₂⟩, ...]

We store:

IntervalArray = { lo: Array Dyadic, hi: Array Dyadic }
            = { lo: [lo₁, lo₂, ...], hi: [hi₁, hi₂, ...] }

Why SoA? When computing lower bounds of a layer output, we mostly access lo values. Keeping them contiguous in memory improves cache hit rates by ~5x.

Main Definitions

• IntervalArray n - A fixed-size array of n intervals in SoA layout
• mem - Membership predicate for real vectors
• add, sub - Interval operations on arrays

structure LeanCert.ML.Optimized.IntervalArray (n : ℕ) : Type

Structure-of-Arrays interval representation. Stores lower and upper bounds in separate contiguous arrays for cache efficiency.

• lo : Array Core.Dyadic

  Lower bounds array

• hi : Array Core.Dyadic

  Upper bounds array

• lo_size : self.lo.size = n

  Size invariant for lower bounds

• hi_size : self.hi.size = n

  Size invariant for upper bounds

def LeanCert.ML.Optimized.instReprIntervalArray.repr {n✝ : ℕ} : IntervalArray n✝ → ℕ → Std.Format

Equations

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

instance LeanCert.ML.Optimized.instReprIntervalArray {n✝ : ℕ} : Repr (IntervalArray n✝)

Equations

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

@[inline]

def LeanCert.ML.Optimized.IntervalArray.getLo {n : ℕ} (v : IntervalArray n) (i : Fin n) : Core.Dyadic

Access lower bound at index i

Equations

• v.getLo i = v.lo[↑i]

@[inline]

def LeanCert.ML.Optimized.IntervalArray.getHi {n : ℕ} (v : IntervalArray n) (i : Fin n) : Core.Dyadic

Access upper bound at index i

Equations

• v.getHi i = v.hi[↑i]

def LeanCert.ML.Optimized.IntervalArray.get {n : ℕ} (v : IntervalArray n) (i : Fin n) (hle : (v.getLo i).toRat ≤ (v.getHi i).toRat) : Core.IntervalDyadic

Get the i-th interval as an IntervalDyadic

Equations

• v.get i hle = { lo := v.getLo i, hi := v.getHi i, le := hle }

def LeanCert.ML.Optimized.IntervalArray.mem {n : ℕ} (v : IntervalArray n) (x : Fin n → ℝ) : Prop

A real vector is a member of an interval array if each component is in bounds

Equations

• v.mem x = ∀ (i : Fin n), ↑(v.getLo i).toRat ≤ x i ∧ x i ≤ ↑(v.getHi i).toRat

instance LeanCert.ML.Optimized.IntervalArray.instMembershipForallFinReal {n : ℕ} : Membership (Fin n → ℝ) (IntervalArray n)

Equations

• LeanCert.ML.Optimized.IntervalArray.instMembershipForallFinReal = { mem := LeanCert.ML.Optimized.IntervalArray.mem }

def LeanCert.ML.Optimized.IntervalArray.ofFn {n : ℕ} (f : Fin n → Core.IntervalDyadic) : IntervalArray n

Create an interval array from a function

Equations

• LeanCert.ML.Optimized.IntervalArray.ofFn f = { lo := Array.ofFn fun (i : Fin n) => (f i).lo, hi := Array.ofFn fun (i : Fin n) => (f i).hi, lo_size := ⋯, hi_size := ⋯ }

def LeanCert.ML.Optimized.IntervalArray.mk' {n : ℕ} (lo hi : Array Core.Dyadic) (hlo : lo.size = n) (hhi : hi.size = n) : IntervalArray n

Create from separate lo/hi arrays (with proof of validity)

Equations

• LeanCert.ML.Optimized.IntervalArray.mk' lo hi hlo hhi = { lo := lo, hi := hi, lo_size := hlo, hi_size := hhi }

def LeanCert.ML.Optimized.IntervalArray.empty : IntervalArray 0

Empty interval array (for n = 0)

Equations

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

def LeanCert.ML.Optimized.IntervalArray.singleton (I : Core.IntervalDyadic) : IntervalArray 1

Singleton interval array

Equations

• LeanCert.ML.Optimized.IntervalArray.singleton I = { lo := #[I.lo], hi := #[I.hi], lo_size := ⋯, hi_size := ⋯ }

def LeanCert.ML.Optimized.IntervalArray.add {n : ℕ} (a b : IntervalArray n) : IntervalArray n

Point-wise addition of interval arrays (exact, no rounding)

Equations

• a.add b = { lo := Array.ofFn fun (i : Fin n) => (a.getLo i).add (b.getLo i), hi := Array.ofFn fun (i : Fin n) => (a.getHi i).add (b.getHi i), lo_size := ⋯, hi_size := ⋯ }

def LeanCert.ML.Optimized.IntervalArray.neg {n : ℕ} (a : IntervalArray n) : IntervalArray n

Point-wise negation of interval array

Equations

• a.neg = { lo := Array.ofFn fun (i : Fin n) => (a.getHi i).neg, hi := Array.ofFn fun (i : Fin n) => (a.getLo i).neg, lo_size := ⋯, hi_size := ⋯ }

def LeanCert.ML.Optimized.IntervalArray.sub {n : ℕ} (a b : IntervalArray n) : IntervalArray n

Point-wise subtraction of interval arrays

Equations

• a.sub b = a.add b.neg

def LeanCert.ML.Optimized.IntervalArray.relu {n : ℕ} (a : IntervalArray n) : IntervalArray n

Apply ReLU (max(0, x)) to each interval component

Equations

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

Soundness Theorems

theorem LeanCert.ML.Optimized.IntervalArray.mem_add {n : ℕ} {x y : Fin n → ℝ} {a b : IntervalArray n} (hx : x ∈ a) (hy : y ∈ b) : (fun (i : Fin n) => x i + y i) ∈ a.add b

Addition is sound: if x ∈ a and y ∈ b, then x + y ∈ add a b

theorem LeanCert.ML.Optimized.IntervalArray.mem_neg {n : ℕ} {x : Fin n → ℝ} {a : IntervalArray n} (hx : x ∈ a) : (fun (i : Fin n) => -x i) ∈ a.neg

Negation is sound: if x ∈ a, then -x ∈ neg a

theorem LeanCert.ML.Optimized.IntervalArray.mem_sub {n : ℕ} {x y : Fin n → ℝ} {a b : IntervalArray n} (hx : x ∈ a) (hy : y ∈ b) : (fun (i : Fin n) => x i - y i) ∈ a.sub b

Subtraction is sound

theorem LeanCert.ML.Optimized.IntervalArray.mem_relu {n : ℕ} {x : Fin n → ℝ} {a : IntervalArray n} (hx : x ∈ a) : (fun (i : Fin n) => max 0 (x i)) ∈ a.relu

ReLU is sound: if x ∈ a, then max(0, x) ∈ relu a

Conversion

def LeanCert.ML.Optimized.IntervalArray.ofList (v : List Core.IntervalDyadic) : IntervalArray v.length

Convert from list-based IntervalVector

Equations

• LeanCert.ML.Optimized.IntervalArray.ofList v = { lo := Array.ofFn fun (i : Fin v.length) => v[↑i].lo, hi := Array.ofFn fun (i : Fin v.length) => v[↑i].hi, lo_size := ⋯, hi_size := ⋯ }

def LeanCert.ML.Optimized.IntervalArray.toList {n : ℕ} (v : IntervalArray n) (hle : ∀ (i : Fin n), (v.getLo i).toRat ≤ (v.getHi i).toRat) : List Core.IntervalDyadic

Convert to list-based IntervalVector

Equations

• v.toList hle = List.ofFn fun (i : Fin n) => v.get i ⋯