Provedaithercounterexamplenative-stateb846d70

Aither: native pool fallback can exceed capacity and nested calls can lose the outer cursor

\begin{aligned} & \left(\right. \htmlData{mx=2}{524032 + 256} \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{\operatorname{poolSize}} \\ & \htmlData{mx=1}{\land} \htmlData{mx=7}{\htmlData{mx=6}{\htmlData{mx=5}{\operatorname{claimBase}}(524032, 256)} + 256} \mathrel{\htmlData{mx=9}{>}} \htmlData{mx=8}{\operatorname{poolSize}} \left.\right) \\ & \htmlData{mx=0}{\land} (\htmlData{mx=11}{\htmlData{mx=10}{\operatorname{nestedOuterBase}}(1, 1, 1)} \mathrel{\htmlData{mx=12}{=}} 2 \mathbin{\htmlData{mx=16}{\land}} \htmlData{mx=14}{\htmlData{mx=13}{\operatorname{nestedOuterBase}}(1, 1, 1)} \mathrel{\htmlData{mx=15}{\neq}} 0) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=17}{\forall} \mathit{idx}, n \in \htmlData{mx=18}{\mathbb{N}}, \\ & \quad \htmlData{mx=22}{\htmlData{mx=20}{\mathit{idx}} + \htmlData{mx=21}{n}} \mathrel{\htmlData{mx=24}{\leq}} \htmlData{mx=23}{\operatorname{overflowSlot}} \\ & \quad \htmlData{mx=19}{\implies} \htmlData{mx=28}{\htmlData{mx=25}{\operatorname{claimBase}}(\htmlData{mx=26}{\mathit{idx}}, \htmlData{mx=27}{n})} \mathrel{\htmlData{mx=30}{=}} \htmlData{mx=29}{\mathit{idx}} \mathbin{\htmlData{mx=39}{\land}} \htmlData{mx=34}{\htmlData{mx=31}{\operatorname{nextCursor}}(\htmlData{mx=32}{\mathit{idx}}, \htmlData{mx=33}{n})} \mathrel{\htmlData{mx=38}{=}} \htmlData{mx=37}{\htmlData{mx=35}{\mathit{idx}} + \htmlData{mx=36}{n}} \left.\right) \end{aligned}

What the notation means · or point at any symbol

+Addition: 524032 plus 256. (524032 + 256)
≤At most: 524032 + 256 is less than or equal to poolSize. (524032 + 256 ≤ poolSize)
∧And: Both hold: 524032 + 256 ≤ poolSize, and claimBase(524032, 256) + 256 > poolSize. (524032 + 256 ≤ poolSize ∧ claimBase 524…)
poolSize: poolSize: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (poolSize)
claimBase: claimBase: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (claimBase)
f(x)Function application: claimBase applied to 524032, 256. Lean writes f x; papers write f(x). (claimBase 524032 256)
>Greater than: claimBase(524032, 256) + 256 is strictly larger than poolSize. (claimBase 524032 256 + 256 > poolSize)
nestedOuterBase: nestedOuterBase: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (nestedOuterBase)
=Equality: nestedOuterBase(1, 1, 1) and 2 are the same. (nestedOuterBase 1 1 1 = 2)
≠Not equal: nestedOuterBase(1, 1, 1) and 0 are different. (nestedOuterBase 1 1 1 ≠ 0)
∀For all: The statement after the comma holds for every idx, n. (∀ (idx n : Nat), idx + n ≤ overflowSlot…)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
⟹Implies: If idx + n ≤ overflowSlot, then claimBase(idx, n) = idx ∧ nextCursor(idx, n) = idx + n. (Between types, A → B is the type of functions from A to B.) (idx + n ≤ overflowSlot → claimBase idx …)
overflowSlot: overflowSlot: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (overflowSlot)
nextCursor: nextCursor: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (nextCursor)

theorem aither-b846-native-cursor-counterexamples :
    (524032 + 256 ≤ poolSize ∧ claimBase 524032 256 + 256 > poolSize) ∧ (nestedOuterBase 1 1 1 = 2 ∧ nestedOuterBase 1 1 1 ≠ 0) ∧ (∀ (idx n : Nat), idx + n ≤ overflowSlot → claimBase idx n = idx ∧ nextCursor idx n = idx + n)

Source-mapped natural arithmetic counterexamples: idx524032,size256 fits compiler pool524288 but fallback base524160 makes end524416; inner base1,size1 leaves outer claim at2 rather than0. Also proves correct nonfallback branch under idx+n<=OverflowSlot. Independent C witnesses reproduced both patterns at -O0/-O2. Not an end-to-end Aither binary test or proof of arbitrary memory safety.

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: Quot.sound, propext
Proof: 18 lines of Lean

Aither: native pool fallback can exceed capacity and nested calls can lose the outer cursor

How it was proved

More proved statements