Provedaitherhot-reloadmigrationb846d70

Aither: relocation and unrelated regions do not interfere with migration

For all $\htmlData{mx=1}{A \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=3}{\mathit{healthy} : \htmlData{mx=0}{A} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\operatorname{Bool}}}$ :

\begin{aligned} & \left(\right. \htmlData{mx=1}{\forall} \mathit{old} : \htmlData{mx=6}{\htmlData{mx=2}{\operatorname{List}}\,\htmlData{mx=5}{\htmlData{mx=3}{\operatorname{Region}}\,\htmlData{mx=4}{A}}},\ \mathit{fresh} : \htmlData{mx=9}{\htmlData{mx=7}{\operatorname{Region}}\,\htmlData{mx=8}{A}},\ \mathit{delta} \in \htmlData{mx=10}{\mathbb{N}}, \\ & \quad \htmlData{mx=25}{\htmlData{mx=12}{\operatorname{migrate}}(\htmlData{mx=13}{\mathit{healthy}}, \htmlData{mx=20}{\htmlData{mx=16}{\operatorname{map}\left(\htmlData{mx=15}{\mathit{old}}\right)}(\htmlData{mx=19}{\htmlData{mx=17}{\operatorname{relocate}}(\htmlData{mx=18}{\mathit{delta}})})}, \htmlData{mx=24}{\htmlData{mx=21}{\operatorname{relocate}}(\htmlData{mx=22}{\mathit{delta}}, \htmlData{mx=23}{\mathit{fresh}})})} \\ & \quad \quad \htmlData{mx=11}{=} \htmlData{mx=30}{\htmlData{mx=26}{\operatorname{migrate}}(\htmlData{mx=27}{\mathit{healthy}}, \htmlData{mx=28}{\mathit{old}}, \htmlData{mx=29}{\mathit{fresh}})} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=31}{\forall} \mathit{before}, \mathit{old} : \htmlData{mx=36}{\htmlData{mx=32}{\operatorname{List}}\,\htmlData{mx=35}{\htmlData{mx=33}{\operatorname{Region}}\,\htmlData{mx=34}{A}}},\ \mathit{fresh} : \htmlData{mx=39}{\htmlData{mx=37}{\operatorname{Region}}\,\htmlData{mx=38}{A}}, \\ & \quad (\htmlData{mx=49}{\forall r \in \htmlData{mx=48}{\mathit{before}},\ \htmlData{mx=43}{\htmlData{mx=41}{\operatorname{signature}}(\htmlData{mx=42}{r})} \mathrel{\htmlData{mx=47}{\neq}} \htmlData{mx=46}{\htmlData{mx=44}{\operatorname{signature}}(\htmlData{mx=45}{\mathit{fresh}})}}) \\ & \quad \htmlData{mx=40}{\implies} \htmlData{mx=58}{\htmlData{mx=51}{\operatorname{migrate}}(\htmlData{mx=52}{\mathit{healthy}}, \htmlData{mx=56}{\htmlData{mx=53}{\mathit{before}} + \htmlData{mx=55}{\mathtt{+}(\htmlData{mx=54}{\mathit{old}})}}, \htmlData{mx=57}{\mathit{fresh}})} \\ & \quad \quad \htmlData{mx=50}{=} \htmlData{mx=63}{\htmlData{mx=59}{\operatorname{migrate}}(\htmlData{mx=60}{\mathit{healthy}}, \htmlData{mx=61}{\mathit{old}}, \htmlData{mx=62}{\mathit{fresh}})} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=64}{\forall} \mathit{old} : \htmlData{mx=69}{\htmlData{mx=65}{\operatorname{List}}\,\htmlData{mx=68}{\htmlData{mx=66}{\operatorname{Region}}\,\htmlData{mx=67}{A}}},\ \mathit{fresh} : \htmlData{mx=72}{\htmlData{mx=70}{\operatorname{Region}}\,\htmlData{mx=71}{A}}, \\ & \quad (\htmlData{mx=82}{\forall r \in \htmlData{mx=81}{\mathit{old}},\ \htmlData{mx=76}{\htmlData{mx=74}{\operatorname{signature}}(\htmlData{mx=75}{r})} \mathrel{\htmlData{mx=80}{\neq}} \htmlData{mx=79}{\htmlData{mx=77}{\operatorname{signature}}(\htmlData{mx=78}{\mathit{fresh}})}}) \\ & \quad \htmlData{mx=73}{\implies} \htmlData{mx=87}{\htmlData{mx=83}{\operatorname{migrate}}(\htmlData{mx=84}{\mathit{healthy}}, \htmlData{mx=85}{\mathit{old}}, \htmlData{mx=86}{\mathit{fresh}})} \mathrel{\htmlData{mx=91}{=}} \htmlData{mx=90}{\operatorname{payload}\left(\htmlData{mx=89}{\mathit{fresh}}\right)} \left.\right) \end{aligned}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
⟹Implies: If A, then Bool. (Between types, A → B is the type of functions from A to B.) (A → Bool)
∀For all: The statement after the comma holds for every old, fresh, delta. (∀ (old : List (Region A)) (fresh : Regi…)
Bool: Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Bool)
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)
Region: Region: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Region)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
migrate: migrate: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (migrate)
=Equality: migrate(healthy, map(relocate(delta)), relocate(delta, fre… and migrate(healthy, old, fresh) are the same. (migrate healthy (old.map (relocate delt…)
e.fmap: map of old: Lean's dot notation e.map means map applied to e. (old.map)
relocate: relocate: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (relocate)
f(x)Function application: relocate applied to delta. Lean writes f x; papers write f(x). (relocate delta)
∧And: Both hold: ∀ before, old, fresh, (∀ r, signature(r) ≠ signature(fresh…, and ∀ old, fresh, (∀ r, signature(r) ≠ signature(fresh)) → mig…. ((∀ (before old : List (Region A)) (fres…)
signature: signature: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (signature)
≠Not equal: signature(r) and signature(fresh) are different. (signature r ≠ signature fresh)
+Addition: before plus +(old). (before ++ old)
e.fpayload: payload of fresh: Lean's dot notation e.payload means payload applied to e. (fresh.payload)

theorem aither-b846-migration-noninterference (A : Type) (healthy : A → Bool) :
    (∀ (old : List (Region A)) (fresh : Region A) (delta : Nat), migrate healthy (old.map (relocate delta)) (relocate delta fresh) = migrate healthy old fresh) ∧ (∀ (before old : List (Region A)) (fresh : Region A), (∀ r ∈ before, signature r ≠ signature fresh) → migrate healthy (before ++ old) fresh = migrate healthy old fresh) ∧ (∀ (old : List (Region A)) (fresh : Region A), (∀ r ∈ old, signature r ≠ signature fresh) → migrate healthy old fresh = fresh.payload)

Payload model of signature-based migration. Relocating addresses leaves selection unchanged; adding a nonmatching prefix does not interfere; a layout with no matching signatures retains prepared payload. First-match semantics and health policy are unchanged. Not a pointer validity theorem.

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: propext
Proof: 49 lines of Lean

Aither: relocation and unrelated regions do not interfere with migration

How it was proved

More proved statements