Fresh Atoms and the Move Operation

This file defines freshness and the "move" operation that is central to nominal CatCrypt's state separation.

Main definitions

• Fresh - Freshness relation (an atom is fresh for x if it's not in supp x)
• Disj - Disjointness of supports
• move - Generate a permutation that makes one element's support disjoint from another

References

• Pitts, Nominal Sets: Names and Symmetry in Computer Science, Cambridge University Press, 2013, Chapter 3.
• Larsen and Schürmann, Nominal State-Separating Proofs, IACR ePrint 2025/598 — the SSProve Nominal/ layer this development ports.

def CatCrypt.Nominal.Fresh {α : Type u_1} [NomSet α] (a : Atom) (x : α) : Prop

An atom is fresh for an element if it's not in the element's support.

Equations

• CatCrypt.Nominal.Fresh a x = (a ∉ CatCrypt.Nominal.NomSet.supp x)

def CatCrypt.Nominal.Disj {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (x : α) (y : β) : Prop

Two elements are disjoint if their supports are disjoint.

Equations

• CatCrypt.Nominal.Disj x y = Disjoint (CatCrypt.Nominal.NomSet.supp x) (CatCrypt.Nominal.NomSet.supp y)

theorem CatCrypt.Nominal.Fresh.act_swap_fresh {α : Type u_1} [NomSet α] (a b : Atom) (x : α) (ha : Fresh a x) (hb : Fresh b x) : FinPerm.swap a b • x = x

Fresh atoms don't affect elements under permutation

noncomputable def CatCrypt.Nominal.freshFor {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (x : α) (y : β) : Atom

Generate a fresh atom not in the union of two supports

Equations

• CatCrypt.Nominal.freshFor x y = CatCrypt.Nominal.Atom.fresh (CatCrypt.Nominal.NomSet.supp x ∪ CatCrypt.Nominal.NomSet.supp y)

theorem CatCrypt.Nominal.freshFor_not_in_supp_left {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (x : α) (y : β) : Fresh (freshFor x y) x

freshFor x y is fresh for x.

theorem CatCrypt.Nominal.freshFor_not_in_supp_right {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (x : α) (y : β) : Fresh (freshFor x y) y

freshFor x y is fresh for y.

noncomputable def CatCrypt.Nominal.offset (s : Finset Atom) : ℕ

The offset of a finset: one plus the maximum value. This is used to generate fresh atoms.

Equations

• CatCrypt.Nominal.offset s = CatCrypt.Nominal.Atom.offset s

def CatCrypt.Nominal.atomShift (base : ℕ) (a : Atom) : Atom

Map an atom a to a fresh atom above the offset of some set. This is used to construct the fresh permutation.

Equations

• CatCrypt.Nominal.atomShift base a = { val := base + a.val }

theorem CatCrypt.Nominal.atomShift_injective (base : ℕ) : Function.Injective (atomShift base)

Shifting by a fixed base is injective.

theorem CatCrypt.Nominal.atomShift_image_disjoint {s : Finset Atom} {a : Atom} (_ha : a ∈ s) (base : ℕ) (hbase : Atom.offset s ≤ base) : atomShift base a ∉ s

Once base clears the offset of s, shifting any atom lands outside s.

theorem CatCrypt.Nominal.atomShift_val_ge (base : ℕ) (a : Atom) : base ≤ (atomShift base a).val

Shifted atoms are above the offset

theorem CatCrypt.Nominal.atom_val_lt_offset {s : Finset Atom} {a : Atom} (ha : a ∈ s) : a.val < Atom.offset s

Atoms in s are below the offset

theorem CatCrypt.Nominal.atomShift_not_in_set {s : Finset Atom} {a : Atom} (base : ℕ) (hbase : Atom.offset s ≤ base) : atomShift base a ∉ s

Shifted atoms are not in the original set when base ≥ offset

theorem CatCrypt.Nominal.atom_lt_shifted {s : Finset Atom} {base : ℕ} {a b : Atom} (hbase : Atom.offset s ≤ base) (ha : a ∈ s) : a.val < (atomShift base b).val

Atoms in s have values strictly less than shifted atoms when base ≥ offset s

theorem CatCrypt.Nominal.shifted_ne_mem {s : Finset Atom} {base : ℕ} {a b : Atom} (hbase : Atom.offset s ≤ base) (hb : b ∈ s) : atomShift base a ≠ b

Shifted atoms are different from atoms in s

noncomputable def CatCrypt.Nominal.freshPerm (s : Finset Atom) (base : ℕ) : FinPerm

The fresh permutation construction.

freshPerm s base creates a permutation that:

• For each a in s, swaps a with atomShift base a
• Acts as identity outside s ∪ (atomShift base '' s)

The key property is that when base ≥ offset s, the images are above the offset, hence disjoint from any set with offset ≤ base.

Following Rocq SSProve's fperm (λ a, atomize (offset (supp x) + natize a)) (supp y).

Equations

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

theorem CatCrypt.Nominal.foldl_mul_swap_fix {a : Atom} {init : FinPerm} (l : List Atom) (base : ℕ) (hinit : init.apply a = a) (hswaps : ∀ x ∈ l, a ≠ x ∧ a ≠ atomShift base x) : (List.foldl (fun (π : FinPerm) (b : Atom) => π * FinPerm.swap b (atomShift base b)) init l).apply a = a

Helper: if each swap in a fold fixes a point, the fold result fixes that point. This is a general induction principle for foldl with permutation multiplication.

theorem CatCrypt.Nominal.freshPerm_fix_outside {s : Finset Atom} {base : ℕ} {a : Atom} (_hbase : Atom.offset s ≤ base) (ha : a ∉ s) (hshift : ∀ b ∈ s, atomShift base b ≠ a) : (freshPerm s base).apply a = a

freshPerm fixes atoms outside s when base ≥ offset s

theorem CatCrypt.Nominal.foldl_mul_swap_transparent {x : Atom} {init : FinPerm} (l : List Atom) (base : ℕ) (hswaps : ∀ y ∈ l, x ≠ y ∧ x ≠ atomShift base y) : (List.foldl (fun (π : FinPerm) (b : Atom) => π * FinPerm.swap b (atomShift base b)) init l).apply x = init.apply x

If all swaps in the list fix a point, the fold is transparent at that point: the fold result applied to x equals the initial permutation applied to x.

theorem CatCrypt.Nominal.foldl_mul_swap_apply_mem {a : Atom} {init : FinPerm} (l : List Atom) (base : ℕ) (hnodup : l.Nodup) (ha : a ∈ l) (hinit : init.apply a = a) (hinit_shift : init.apply (atomShift base a) = atomShift base a) (hbefore : ∀ x ∈ l, x ≠ a → a.val < (atomShift base x).val) (hafter : ∀ x ∈ l, x ≠ a → (atomShift base a).val ≠ x.val ∧ atomShift base a ≠ atomShift base x) : (List.foldl (fun (π : FinPerm) (b : Atom) => π * FinPerm.swap b (atomShift base b)) init l).apply a = atomShift base a

Helper for freshPerm_apply_mem': when a is in the list, the fold maps a to its shift. Key invariants: init fixes a, and init fixes atomShift base a.

theorem CatCrypt.Nominal.freshPerm_apply_mem' {s : Finset Atom} {base : ℕ} {a : Atom} (hbase : Atom.offset s ≤ base) (ha : a ∈ s) : (freshPerm s base).apply a = atomShift base a

freshPerm maps atoms in s to their shifts when base ≥ offset

theorem CatCrypt.Nominal.supp_act_freshPerm_disjoint {α : Type u_1} [NomSet α] (y : α) (base : ℕ) (hbase : Atom.offset (NomSet.supp y) ≤ base) (sups : Finset Atom) (hsups : Atom.offset sups ≤ base) : Disjoint sups (NomSet.supp (freshPerm (NomSet.supp y) base • y))

Support of an element under freshPerm shifts appropriately. The support of π ∙ y is π '' (supp y), so it consists of shifted atoms which have values ≥ base, while atoms in sups have values < offset sups ≤ base.

noncomputable def CatCrypt.Nominal.freshMove {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (x : α) (y : β) : FinPerm

The fresh permutation for move: maps supp y to atoms above offset(supp x ∪ supp y)

Equations

• CatCrypt.Nominal.freshMove x y = CatCrypt.Nominal.freshPerm (CatCrypt.Nominal.NomSet.supp y) (CatCrypt.Nominal.Atom.offset (CatCrypt.Nominal.NomSet.supp x ∪ CatCrypt.Nominal.NomSet.supp y))

noncomputable def CatCrypt.Nominal.move {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (x : α) (y : β) : β

The move permutation: applies freshMove to relocate y's support away from x's support.

This follows the Rocq definition: move x y := fresh x y ∙ y where fresh x y is the permutation mapping supp y to fresh atoms.

Equations

• CatCrypt.Nominal.move x y = CatCrypt.Nominal.freshMove x y • y

noncomputable def CatCrypt.Nominal.movePerm {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (x : α) (y : β) : FinPerm

The permutation used by move

Equations

• CatCrypt.Nominal.movePerm x y = CatCrypt.Nominal.freshMove x y

theorem CatCrypt.Nominal.move_disj {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (x : α) (y : β) : Disj x (move x y)

After applying move, the supports become disjoint.

This is the key property from nominal set theory (Rocq: fresh_disjoint).

Proof sketch:

• freshMove x y maps atoms in supp y to atoms above offset(supp x ∪ supp y)
• All atoms in supp x are below this offset
• Therefore, supp(move x y) ∩ supp x = ∅

theorem CatCrypt.Nominal.movePerm_act_left {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (x : α) (y : β) (hdisj : Disjoint (NomSet.supp x) (NomSet.supp y)) : movePerm x y • x = x

movePerm doesn't move the first argument when supports are disjoint.

Note: This requires the disjointness hypothesis because freshPerm moves all atoms in supp y. If a ∈ supp x ∩ supp y, then a would be moved.

def CatCrypt.Nominal.AlphaEquiv {α : Type u_1} [NomSet α] (x y : α) : Prop

Alpha-equivalence: two elements are equivalent if they differ only by a permutation

Equations

• (x ≡α y) = ∃ (π : CatCrypt.Nominal.FinPerm), π • x = y

def CatCrypt.Nominal.«term_≡α_» : Lean.TrailingParserDescr

Equations

• CatCrypt.Nominal.«term_≡α_» = Lean.ParserDescr.trailingNode `CatCrypt.Nominal.«term_≡α_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡α ") (Lean.ParserDescr.cat `term 0))

theorem CatCrypt.Nominal.AlphaEquiv.refl {α : Type u_1} [NomSet α] (x : α) : x ≡α x

Alpha-equivalence is reflexive.

theorem CatCrypt.Nominal.AlphaEquiv.symm {α : Type u_1} [NomSet α] {x y : α} (h : x ≡α y) : y ≡α x

Alpha-equivalence is symmetric.

theorem CatCrypt.Nominal.AlphaEquiv.trans {α : Type u_1} [NomSet α] {x y z : α} (hxy : x ≡α y) (hyz : y ≡α z) : x ≡α z

Alpha-equivalence is transitive.