Provedaitherallocationmemory-modelb846d70

Aither: packed state intervals are ordered, disjoint and bounded

For all $\htmlData{mx=1}{\mathit{base} \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=3}{\mathit{sizes} \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{List}}\,\htmlData{mx=1}{\mathbb{N}}}}$ :

\begin{aligned} & \left(\right. \htmlData{mx=1}{\forall} \mathit{off}, \mathit{size} \in \htmlData{mx=2}{\mathbb{N}}, \\ & \quad \htmlData{mx=6}{\left( \htmlData{mx=4}{\mathit{off}}, \htmlData{mx=5}{\mathit{size}} \right)} \mathrel{\htmlData{mx=11}{\in}} \htmlData{mx=10}{\htmlData{mx=7}{\operatorname{packed}}(\htmlData{mx=8}{\mathit{base}}, \htmlData{mx=9}{\mathit{sizes}})} \\ & \quad \htmlData{mx=3}{\implies} \htmlData{mx=12}{\mathit{base}} \mathrel{\htmlData{mx=14}{\leq}} \htmlData{mx=13}{\mathit{off}} \mathbin{\htmlData{mx=24}{\land}} \htmlData{mx=17}{\htmlData{mx=15}{\mathit{off}} + \htmlData{mx=16}{\mathit{size}}} \mathrel{\htmlData{mx=23}{\leq}} \htmlData{mx=22}{\htmlData{mx=18}{\mathit{base}} + \htmlData{mx=21}{\operatorname{sum}\left(\htmlData{mx=20}{\mathit{sizes}}\right)}} \left.\right) \\ & \htmlData{mx=0}{\land} \htmlData{mx=40}{\htmlData{mx=33}{\operatorname{Pairwise}\left(\htmlData{mx=32}{\htmlData{mx=29}{\operatorname{packed}}(\htmlData{mx=30}{\mathit{base}}, \htmlData{mx=31}{\mathit{sizes}})}\right)}(\htmlData{mx=39}{a, b \mapsto \htmlData{mx=36}{\htmlData{mx=34}{a_{1}} + \htmlData{mx=35}{a_{2}}} \mathrel{\htmlData{mx=38}{\leq}} \htmlData{mx=37}{b_{1}}})} \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=41}{\forall} \mathit{capacity}, \mathit{off}, \mathit{size} \in \htmlData{mx=42}{\mathbb{N}}, \\ & \quad \htmlData{mx=48}{\htmlData{mx=44}{\mathit{base}} + \htmlData{mx=47}{\operatorname{sum}\left(\htmlData{mx=46}{\mathit{sizes}}\right)}} \mathrel{\htmlData{mx=50}{\leq}} \htmlData{mx=49}{\mathit{capacity}} \\ & \quad \htmlData{mx=43}{\implies} \htmlData{mx=53}{\left( \htmlData{mx=51}{\mathit{off}}, \htmlData{mx=52}{\mathit{size}} \right)} \mathrel{\htmlData{mx=58}{\in}} \htmlData{mx=57}{\htmlData{mx=54}{\operatorname{packed}}(\htmlData{mx=55}{\mathit{base}}, \htmlData{mx=56}{\mathit{sizes}})} \\ & \quad \htmlData{mx=43}{\implies} \htmlData{mx=61}{\htmlData{mx=59}{\mathit{off}} + \htmlData{mx=60}{\mathit{size}}} \mathrel{\htmlData{mx=63}{\leq}} \htmlData{mx=62}{\mathit{capacity}} \left.\right) \end{aligned}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
List: List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
f(x)Function application: List applied to Nat. Lean writes f x; papers write f(x). (List Nat)
∀For all: The statement after the comma holds for every off, size. (∀ (off size : Nat), (off, size) ∈ packe…)
(a, b)Tuple: The ordered pair (or tuple) of off, size. ((off, size))
∈Element of: (off, size) is a member of packed(base, sizes). ((off, size) ∈ packed base sizes)
⟹Implies: If (off, size) ∈ packed(base, sizes), then base ≤ off ∧ off + size ≤ base + sizes.sum. (Between types, A → B is the type of functions from A to B.) ((off, size) ∈ packed base sizes → base …)
packed: packed: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (packed)
≤At most: base is less than or equal to off. (base ≤ off)
∧And: Both hold: base ≤ off, and off + size ≤ base + sizes.sum. (base ≤ off ∧ off + size ≤ base + sizes.…)
+Addition: off plus size. (off + size)
e.fsum: sum of sizes: Lean's dot notation e.sum means sum applied to e. (sizes.sum)
e.fPairwise: Pairwise of packed(base, sizes): Lean's dot notation e.Pairwise means Pairwise applied to e. ((packed base sizes).Pairwise)
x ↦ f(x)Function (λ-abstraction): The function sending a, b to a.1 + a.2 ≤ b.1. Lean writes fun x => …; papers write x ↦ …. (fun a b => a.1 + a.2 ≤ b.1)
p₁Component: The first component of the pair a. (a.1)

theorem aither-b846-packed-layout (base : Nat) (sizes : List Nat) :
    (∀ (off size : Nat), (off, size) ∈ packed base sizes → base ≤ off ∧ off + size ≤ base + sizes.sum) ∧ (packed base sizes).Pairwise (fun a b => a.1 + a.2 ≤ b.1) ∧ (∀ (capacity off size : Nat), base + sizes.sum ≤ capacity → (off, size) ∈ packed base sizes → off + size ≤ capacity)

Abstract nonnegative prefix-sum layout underlying type bases and intra-type offsets. All intervals lie within the summed allocation; list order implies nonoverlap; a capacity bound implies each interval fits. Excludes machine integer overflow and native claim behavior, whose mismatch is proved separately.

How it was proved

Proved: 1 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 40 lines of Lean

Aither: packed state intervals are ordered, disjoint and bounded

How it was proved

More proved statements