Nominal Packages

This file defines nominal packages - packages equipped with nominal structure (atom support) enabling separated composition.

Main definitions

• NomPackage - A package wrapped with support information
• NomPackage.sep - Separated composition (packages with disjoint supports)

Overview

In nominal CatCrypt, packages are given a nominal structure where atoms represent abstract memory locations. The key insight is that:

1. Each package has a finite support (the atoms/locations it uses)
2. Packages with disjoint supports can be composed without interference
3. The "move" operation can rename atoms to achieve disjoint supports

References

• Larsen and Schürmann, Nominal State-Separating Proofs
• [Pitts, Nominal Sets], Chapter 6

structure CatCrypt.Nominal.NomPackage : Type 1

A nominal package: a raw package together with its atom support. The support represents the abstract locations/names the package uses.

• raw : Package.RawPackage

  The underlying raw package

• support : Finset Atom

  The support: atoms that matter for this package

theorem CatCrypt.Nominal.NomPackage.ext {P₁ P₂ : NomPackage} (hRaw : P₁.raw = P₂.raw) (hSupp : P₁.support = P₂.support) : P₁ = P₂

theorem CatCrypt.Nominal.NomPackage.ext_iff {P₁ P₂ : NomPackage} : P₁ = P₂ ↔ P₁.raw = P₂.raw ∧ P₁.support = P₂.support

def CatCrypt.Nominal.NomPackage.empty : NomPackage

Empty nominal package with empty support

Equations

• CatCrypt.Nominal.NomPackage.empty = { raw := CatCrypt.Package.RawPackage.empty, support := ∅ }

@[implicit_reducible]

instance CatCrypt.Nominal.NomPackage.instEmptyCollection : EmptyCollection NomPackage

Equations

• CatCrypt.Nominal.NomPackage.instEmptyCollection = { emptyCollection := CatCrypt.Nominal.NomPackage.empty }

@[implicit_reducible]

instance CatCrypt.Nominal.NomPackage.instInhabited : Inhabited NomPackage

Equations

• CatCrypt.Nominal.NomPackage.instInhabited = { default := CatCrypt.Nominal.NomPackage.empty }

def CatCrypt.Nominal.NomPackage.getSupport (P : NomPackage) : Finset Atom

Get the support of a nominal package

Equations

• P.getSupport = P.support

@[simp]

theorem CatCrypt.Nominal.NomPackage.getSupport_eq (P : NomPackage) : P.getSupport = P.support

def CatCrypt.Nominal.NomPackage.Fresh (a : Atom) (P : NomPackage) : Prop

An atom is fresh for a package if it's not in the support

Equations

• CatCrypt.Nominal.NomPackage.Fresh a P = (a ∉ P.support)

def CatCrypt.Nominal.NomPackage.Disjoint (P₁ P₂ : NomPackage) : Prop

Two nominal packages are disjoint if their supports are disjoint

Equations

• P₁.Disjoint P₂ = Disjoint P₁.support P₂.support

theorem CatCrypt.Nominal.NomPackage.disjoint_comm (P₁ P₂ : NomPackage) : P₁.Disjoint P₂ ↔ P₂.Disjoint P₁

noncomputable def CatCrypt.Nominal.NomPackage.sep (P₁ P₂ : NomPackage) (_hDisj : P₁.Disjoint P₂) (hIds : P₁.raw.Disjoint P₂.raw) : NomPackage

Separated composition: compose two packages with disjoint supports. This is the key operation for nominal reasoning - packages that use different atoms can be composed without interference.

Equations

• P₁.sep P₂ _hDisj hIds = { raw := P₁.raw.par P₂.raw hIds, support := P₁.support ∪ P₂.support }

theorem CatCrypt.Nominal.NomPackage.sep_support (P₁ P₂ : NomPackage) (hDisj : P₁.Disjoint P₂) (hIds : P₁.raw.Disjoint P₂.raw) : (P₁.sep P₂ hDisj hIds).support = P₁.support ∪ P₂.support

noncomputable def CatCrypt.Nominal.NomPackage.par (P₁ P₂ : NomPackage) (hIds : P₁.raw.Disjoint P₂.raw) : NomPackage

Parallel composition without disjointness proof (using trivially empty supports). This is a fallback when support information isn't needed.

Equations

• P₁.par P₂ hIds = { raw := P₁.raw.par P₂.raw hIds, support := P₁.support ∪ P₂.support }

noncomputable def CatCrypt.Nominal.NomPackage.link (P₁ P₂ : NomPackage) : NomPackage

Sequential composition (linking) of nominal packages

Equations

• P₁.link P₂ = { raw := P₁.raw.link P₂.raw, support := P₁.support ∪ P₂.support }

noncomputable def CatCrypt.Nominal.NomPackage.singleton (id : ℕ) (S T : Type) (f : S → Core.SPComp T) (support : Finset Atom := ∅) : NomPackage

Create a singleton nominal package with given support. S and T are restricted to Type (not Type*) to match the underlying RawPackage.singleton constraint.

Equations

• CatCrypt.Nominal.NomPackage.singleton id S T f support = { raw := CatCrypt.Package.RawPackage.singleton id S T f, support := support }

noncomputable def CatCrypt.Nominal.NomPackage.rename (P : NomPackage) (π : FinPerm) : NomPackage

Rename atoms in a package using a finite permutation. This changes the support according to the permutation.

WARNING: This only renames the support, NOT the underlying code. The RawPackage stores S → SPComp T functions that have no notion of atom/location identity, so there is nothing to rename inside the code.

For actual code renaming, use the deep embedding layer where RawCode has explicit location references that can be permuted via RawCode.renameLocations.

Equations

• P.rename π = { raw := P.raw, support := Finset.image (fun (x : CatCrypt.Nominal.Atom) => π.apply x) P.support }

theorem CatCrypt.Nominal.NomPackage.rename_support (P : NomPackage) (π : FinPerm) : (P.rename π).support = Finset.image (fun (x : Atom) => π.apply x) P.support

Separated composition properties

theorem CatCrypt.Nominal.NomPackage.sep_comm (P₁ P₂ : NomPackage) (hDisj : P₁.Disjoint P₂) (hIds : P₁.raw.Disjoint P₂.raw) (hIds' : P₂.raw.Disjoint P₁.raw) : (P₁.sep P₂ hDisj hIds).support = (P₂.sep P₁ ⋯ hIds').support

Separated composition is commutative (up to raw package commutativity)

theorem CatCrypt.Nominal.NomPackage.rename_fresh (P : NomPackage) (a b : Atom) (ha : Fresh a P) (hb : Fresh b P) : P.rename (FinPerm.swap a b) = P

Fresh atoms don't affect packages under renaming

NominalAction and NomSet instances

@[implicit_reducible]

noncomputable instance CatCrypt.Nominal.NomPackage.instMulActionFinPerm : MulAction FinPerm NomPackage

NomPackage has a nominal action: permutations act on the support

Equations

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

@[implicit_reducible]

noncomputable instance CatCrypt.Nominal.NomPackage.instNomSet : NomSet NomPackage

NomPackage is a nominal set

Equations

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

Alpha-equivalence for packages

def CatCrypt.Nominal.NomPackage.AlphaEquiv (P₁ P₂ : NomPackage) : Prop

Alpha-equivalence for NomPackage: two packages are equivalent if they differ only by a permutation

Equations

• (P₁ ≡αP P₂) = (P₁ ≡α P₂)

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

Equations

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

theorem CatCrypt.Nominal.NomPackage.AlphaEquiv.refl (P : NomPackage) : P ≡αP P

Alpha-equivalence is reflexive

theorem CatCrypt.Nominal.NomPackage.AlphaEquiv.symm {P₁ P₂ : NomPackage} (h : P₁ ≡αP P₂) : P₂ ≡αP P₁

Alpha-equivalence is symmetric

theorem CatCrypt.Nominal.NomPackage.AlphaEquiv.trans {P₁ P₂ P₃ : NomPackage} (h₁₂ : P₁ ≡αP P₂) (h₂₃ : P₂ ≡αP P₃) : P₁ ≡αP P₃

Alpha-equivalence is transitive

Package algebra laws

theorem CatCrypt.Nominal.NomPackage.RawPackage.par_comm (P₁ P₂ : Package.RawPackage) (hIds : P₁.Disjoint P₂) (hIds' : P₂.Disjoint P₁) : (P₁.par P₂ hIds).entries = (P₂.par P₁ hIds').entries

Raw package parallel composition is commutative up to alpha-equivalence.

This theorem states that the underlying raw packages have the same entries (though possibly in different order in the union).

theorem CatCrypt.Nominal.NomPackage.sep_comm_eq (P₁ P₂ : NomPackage) (hDisj : P₁.Disjoint P₂) (hIds : P₁.raw.Disjoint P₂.raw) (hIds' : P₂.raw.Disjoint P₁.raw) : P₁.sep P₂ hDisj hIds = P₂.sep P₁ ⋯ hIds'

Commutativity of separated composition for NomPackage.

When two packages have disjoint supports, their separated composition is equal (not just alpha-equivalent) because:

• The raw packages combine with union (which is commutative)
• The supports combine with union (which is commutative)

theorem CatCrypt.Nominal.NomPackage.sep_comm_alpha (P₁ P₂ : NomPackage) (hDisj : P₁.Disjoint P₂) (hIds : P₁.raw.Disjoint P₂.raw) (hIds' : P₂.raw.Disjoint P₁.raw) : P₁.sep P₂ hDisj hIds ≡αP P₂.sep P₁ ⋯ hIds'

Commutativity of separated composition up to alpha-equivalence

theorem CatCrypt.Nominal.NomPackage.sep_assoc_eq (P₁ P₂ P₃ : NomPackage) (hDisj₁₂ : P₁.Disjoint P₂) (hDisj₂₃ : P₂.Disjoint P₃) (hDisj₁₃ : P₁.Disjoint P₃) (hIds₁₂ : P₁.raw.Disjoint P₂.raw) (hIds₂₃ : P₂.raw.Disjoint P₃.raw) (hIds₁₃ : P₁.raw.Disjoint P₃.raw) (hIds₁₂₃_left : (P₁.raw.par P₂.raw hIds₁₂).Disjoint P₃.raw) (hIds₁₂₃_right : P₁.raw.Disjoint (P₂.raw.par P₃.raw hIds₂₃)) (hDisj₁₂_₃ : (P₁.sep P₂ hDisj₁₂ hIds₁₂).Disjoint P₃) (hDisj₁_₂₃ : P₁.Disjoint (P₂.sep P₃ hDisj₂₃ hIds₂₃)) : (P₁.sep P₂ hDisj₁₂ hIds₁₂).sep P₃ hDisj₁₂_₃ hIds₁₂₃_left = P₁.sep (P₂.sep P₃ hDisj₂₃ hIds₂₃) hDisj₁_₂₃ hIds₁₂₃_right

Associativity of separated composition (equality version).

For three packages with mutually disjoint supports, separated composition is associative.

theorem CatCrypt.Nominal.NomPackage.sep_assoc_alpha (P₁ P₂ P₃ : NomPackage) (hDisj₁₂ : P₁.Disjoint P₂) (hDisj₂₃ : P₂.Disjoint P₃) (hDisj₁₃ : P₁.Disjoint P₃) (hIds₁₂ : P₁.raw.Disjoint P₂.raw) (hIds₂₃ : P₂.raw.Disjoint P₃.raw) (hIds₁₃ : P₁.raw.Disjoint P₃.raw) (hIds₁₂₃_left : (P₁.raw.par P₂.raw hIds₁₂).Disjoint P₃.raw) (hIds₁₂₃_right : P₁.raw.Disjoint (P₂.raw.par P₃.raw hIds₂₃)) (hDisj₁₂_₃ : (P₁.sep P₂ hDisj₁₂ hIds₁₂).Disjoint P₃) (hDisj₁_₂₃ : P₁.Disjoint (P₂.sep P₃ hDisj₂₃ hIds₂₃)) : (P₁.sep P₂ hDisj₁₂ hIds₁₂).sep P₃ hDisj₁₂_₃ hIds₁₂₃_left ≡αP P₁.sep (P₂.sep P₃ hDisj₂₃ hIds₂₃) hDisj₁_₂₃ hIds₁₂₃_right

Associativity of separated composition up to alpha-equivalence

Simplified versions with automatic disjointness

theorem CatCrypt.Nominal.NomPackage.sep_disjoint_right (P₁ P₂ P₃ : NomPackage) (hDisj₁₂ : P₁.Disjoint P₂) (hIds₁₂ : P₁.raw.Disjoint P₂.raw) (hDisj₁₃ : P₁.Disjoint P₃) (hDisj₂₃ : P₂.Disjoint P₃) : (P₁.sep P₂ hDisj₁₂ hIds₁₂).Disjoint P₃

Disjointness of sep's support with a third package

theorem CatCrypt.Nominal.NomPackage.disjoint_sep_left (P₁ P₂ P₃ : NomPackage) (hDisj₂₃ : P₂.Disjoint P₃) (hIds₂₃ : P₂.raw.Disjoint P₃.raw) (hDisj₁₂ : P₁.Disjoint P₂) (hDisj₁₃ : P₁.Disjoint P₃) : P₁.Disjoint (P₂.sep P₃ hDisj₂₃ hIds₂₃)

Disjointness of a package with sep's support