From 543e519ac53fa3e2392230bb51ba389c664d3cf0 Mon Sep 17 00:00:00 2001
From: Bas Spitters <spitters@cs.au.dk>
Date: Mon, 20 Jul 2026 19:44:52 +0200
Subject: [PATCH] Add NominalIris: nominal separation, name-allocation ghost
 state, and the STLC [no-golf]
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

An Iris/BI layer over nominal-lean's Atom/FinPerm/NomSet framework:

- Nominal.Lambda / Nominal.LambdaAbs: the α-quotient nominal λ-term type Tm
  (a NomSet with an α-correct lam), with Tm.lam factoring through NameAbs Tm.
- NominalIris.Separation: nominal separation as a model of classical BI
  (freshName_sep_ne), over Atom (the Nat-indexed state reached via Atom.val).
- NominalIris.Camera: the DisjointLeibnizSet name camera, the Auth allocation
  view-shift name_alloc, and the iOwn/bupd ghost-state layer.
- NominalIris.Den: the den morphism proving the camera and concrete BI agree.
- NominalIris.Lambda: binding the nominal Tm with the ghost state — ownCtx,
  abs_alloc ((Abs) as name_alloc), binders_distinct, alloc_and_bind.

Adds a require on iris-lean (v4.30.0), used only by the NominalIris target; the
core Nominal library stays mathlib-only. No sorry; axioms propext/Classical.choice/
Quot.sound only.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 Nominal.lean                |   2 +
 Nominal/Lambda.lean         | 328 ++++++++++++++++++++++++++++++++++++
 Nominal/LambdaAbs.lean      |  95 +++++++++++
 NominalIris.lean            |  39 +++++
 NominalIris/Camera.lean     | 223 ++++++++++++++++++++++++
 NominalIris/Den.lean        | 102 +++++++++++
 NominalIris/Lambda.lean     | 121 +++++++++++++
 NominalIris/PR.md           |  88 ++++++++++
 NominalIris/Separation.lean | 139 +++++++++++++++
 lake-manifest.json          |  10 ++
 lakefile.lean               |  15 +-
 11 files changed, 1161 insertions(+), 1 deletion(-)
 create mode 100644 Nominal/Lambda.lean
 create mode 100644 Nominal/LambdaAbs.lean
 create mode 100644 NominalIris.lean
 create mode 100644 NominalIris/Camera.lean
 create mode 100644 NominalIris/Den.lean
 create mode 100644 NominalIris/Lambda.lean
 create mode 100644 NominalIris/PR.md
 create mode 100644 NominalIris/Separation.lean

diff --git a/Nominal.lean b/Nominal.lean
index 42f2427..5db39b8 100644
--- a/Nominal.lean
+++ b/Nominal.lean
@@ -9,6 +9,8 @@ import Nominal.Nominal
 import Nominal.Fresh
 import Nominal.Support
 import Nominal.NameAbstraction
+import Nominal.Lambda
+import Nominal.LambdaAbs
 
 /-!
 # Nominal sets
diff --git a/Nominal/Lambda.lean b/Nominal/Lambda.lean
new file mode 100644
index 0000000..a7a2d4f
--- /dev/null
+++ b/Nominal/Lambda.lean
@@ -0,0 +1,328 @@
+/-
+Copyright (c) 2026 Bas Spitters. All rights reserved.
+Released under MIT license as described in the file LICENSE.
+Authors: Bas Spitters
+-/
+import Nominal.NameAbstraction
+import Nominal.Fresh
+
+set_option autoImplicit false
+
+/-!
+# The λ-calculus as a nominal set
+
+The λ-calculus with terms defined *nominally from the start*, over the
+`Atom` / `FinPerm` / `NomSet` framework. Raw terms carry the `FinPerm` action and
+form a `NomSet`; quotienting by α-equivalence yields `Tm`, the genuine nominal
+term type. Changing the bound name of `lam` to any fresh atom leaves the term
+equal (`Tm.lam_rename`) — an equality of terms, not a separate α-relation.
+
+## Main definitions
+
+* `Raw`, `atoms`, `fv` — raw terms, their atoms, and free variables.
+* `AEq` — α-equivalence as a generated congruence (`refl`/`symm`/`trans` are
+  constructors, so it is an equivalence relation by construction).
+* `Tm := Raw / AEq` — nominal λ-terms; `Tm.var` / `Tm.app` / `Tm.lam`.
+
+## Main results
+
+* `instance : NomSet Raw` — raw terms as a nominal set (support = all atoms).
+* `instance : NomSet Tm` — nominal λ-terms as a nominal set (support = `fv`),
+  whose support-minimality is `aeq_of_fixes_fv`.
+* `Tm.lam_rename` — α-correctness of the binder.
+
+## References
+
+* A. M. Pitts, *Nominal Sets: Names and Symmetry in Computer Science*, CUP 2013.
+-/
+
+namespace CatCrypt.Nominal.Lambda
+
+open CatCrypt.Nominal
+
+/-! ## Raw λ-terms and the permutation action -/
+
+/-- Raw (pre-α) λ-terms over atoms. -/
+inductive Raw where
+  | var : Atom → Raw
+  | app : Raw → Raw → Raw
+  | lam : Atom → Raw → Raw
+  deriving DecidableEq
+
+/-- The `FinPerm` action on raw terms: rename every atom (free and bound). -/
+def rawAct (π : FinPerm) : Raw → Raw
+  | .var a   => .var (π a)
+  | .app s t => .app (rawAct π s) (rawAct π t)
+  | .lam a t => .lam (π a) (rawAct π t)
+
+theorem rawAct_one (t : Raw) : rawAct 1 t = t := by
+  induction t with
+  | var a => simp [rawAct]
+  | app s t ihs iht => simp [rawAct, ihs, iht]
+  | lam a t iht => simp [rawAct, iht]
+
+theorem rawAct_mul (π₁ π₂ : FinPerm) (t : Raw) :
+    rawAct (π₁ * π₂) t = rawAct π₁ (rawAct π₂ t) := by
+  induction t with
+  | var a => simp [rawAct]
+  | app s t ihs iht => simp [rawAct, ihs, iht]
+  | lam a t iht => simp [rawAct, iht]
+
+instance : MulAction FinPerm Raw where
+  smul := rawAct
+  one_smul := rawAct_one
+  mul_smul := rawAct_mul
+
+@[simp] theorem smul_var (π : FinPerm) (a : Atom) : π • Raw.var a = Raw.var (π a) := rfl
+@[simp] theorem smul_app (π : FinPerm) (s t : Raw) :
+    π • Raw.app s t = Raw.app (π • s) (π • t) := rfl
+@[simp] theorem smul_lam (π : FinPerm) (a : Atom) (t : Raw) :
+    π • Raw.lam a t = Raw.lam (π a) (π • t) := rfl
+
+/-! ## Atoms of a term and the `NomSet` structure -/
+
+/-- Every atom occurring in a term (free or bound) — the support of the *raw*
+term (raw terms are not yet α-quotiented, so bound names count). -/
+def atoms : Raw → Finset Atom
+  | .var a   => {a}
+  | .app s t => atoms s ∪ atoms t
+  | .lam a t => insert a (atoms t)
+
+@[simp] theorem atoms_var (a : Atom) : atoms (.var a) = {a} := rfl
+@[simp] theorem atoms_app (s t : Raw) : atoms (.app s t) = atoms s ∪ atoms t := rfl
+@[simp] theorem atoms_lam (a : Atom) (t : Raw) : atoms (.lam a t) = insert a (atoms t) := rfl
+
+theorem atoms_smul (π : FinPerm) (t : Raw) : atoms (π • t) = (atoms t).image (π ·) := by
+  induction t with
+  | var a => simp
+  | app s t ihs iht => simp [ihs, iht, Finset.image_union]
+  | lam a t iht => simp [iht, Finset.image_insert]
+
+/-- If a permutation fixes every atom of `t`, it fixes `t`. -/
+theorem smul_eq_of_atoms_fixed {π : FinPerm} {t : Raw}
+    (h : ∀ a ∈ atoms t, π a = a) : π • t = t := by
+  induction t with
+  | var a => simp only [smul_var, h a (by simp)]
+  | app s t ihs iht =>
+    simp only [smul_app]
+    rw [ihs (fun a ha => h a (by simp [ha])), iht (fun a ha => h a (by simp [ha]))]
+  | lam a t iht =>
+    simp only [smul_lam, h a (by simp)]
+    rw [iht (fun b hb => h b (by simp [hb]))]
+
+instance : NomSet Raw where
+  supp := atoms
+  supp_supports := fun _ _ h => smul_eq_of_atoms_fixed h
+  supp_equivariant := fun t π => atoms_smul π t
+
+@[simp] theorem supp_raw (t : Raw) : NomSet.supp t = atoms t := rfl
+
+/-! ## Free variables -/
+
+/-- The free variables of a term (`lam` binds). -/
+def fv : Raw → Finset Atom
+  | .var a   => {a}
+  | .app s t => fv s ∪ fv t
+  | .lam a t => fv t \ {a}
+
+@[simp] theorem fv_var (a : Atom) : fv (.var a) = {a} := rfl
+@[simp] theorem fv_app (s t : Raw) : fv (.app s t) = fv s ∪ fv t := rfl
+@[simp] theorem fv_lam (a : Atom) (t : Raw) : fv (.lam a t) = fv t \ {a} := rfl
+
+theorem fv_subset_atoms (t : Raw) : fv t ⊆ atoms t := by
+  induction t with
+  | var a => simp
+  | app s t ihs iht => exact Finset.union_subset_union ihs iht
+  | lam a t iht => exact (Finset.sdiff_subset).trans (iht.trans (Finset.subset_insert _ _))
+
+theorem fv_smul (π : FinPerm) (t : Raw) : fv (π • t) = (fv t).image (π ·) := by
+  induction t with
+  | var a => simp
+  | app s t ihs iht => simp [ihs, iht, Finset.image_union]
+  | lam a t iht =>
+    simp only [smul_lam, fv_lam, iht]
+    ext x
+    simp only [Finset.mem_sdiff, Finset.mem_image, Finset.mem_singleton]
+    constructor
+    · rintro ⟨⟨y, hy, rfl⟩, hne⟩
+      exact ⟨y, ⟨hy, fun h => hne (by rw [h])⟩, rfl⟩
+    · rintro ⟨y, ⟨hy, hya⟩, rfl⟩
+      exact ⟨⟨y, hy, rfl⟩, fun h => hya (π.val.injective h)⟩
+
+/-! ## α-equivalence (generated congruence) and the quotient
+
+`AEq` is the least congruence identifying `lam a t` with `lam b (swap a b • t)`
+for a fresh `b`. Taking `refl`/`symm`/`trans` as constructors makes it an
+equivalence relation *by construction* — no hand proof of α-transitivity. -/
+
+/-- α-equivalence of raw terms. -/
+inductive AEq : Raw → Raw → Prop
+  | rfl (t : Raw) : AEq t t
+  | symm {s t} : AEq s t → AEq t s
+  | trans {s t u} : AEq s t → AEq t u → AEq s u
+  | app {s s' t t'} : AEq s s' → AEq t t' → AEq (.app s t) (.app s' t')
+  | lam {a s t} : AEq s t → AEq (.lam a s) (.lam a t)
+  | rename (a b : Atom) (t : Raw) (h : b ∉ atoms t) :
+      AEq (.lam a t) (.lam b (FinPerm.swap a b • t))
+
+theorem AEq.equivalence : Equivalence AEq := ⟨AEq.rfl, AEq.symm, AEq.trans⟩
+
+/-- α-equivalence is equivariant. -/
+theorem aeq_smul (π : FinPerm) {s t : Raw} (h : AEq s t) : AEq (π • s) (π • t) := by
+  induction h with
+  | rfl t => exact .rfl _
+  | symm _ ih => exact ih.symm
+  | trans _ _ ih1 ih2 => exact ih1.trans ih2
+  | app _ _ ih1 ih2 => exact .app ih1 ih2
+  | lam _ ih => exact .lam ih
+  | rename a b t hb =>
+    simp only [smul_lam]
+    have hb' : π b ∉ atoms (π • t) := by
+      rw [atoms_smul]
+      intro hc
+      obtain ⟨c, hcm, hce⟩ := Finset.mem_image.mp hc
+      exact hb (π.val.injective hce ▸ hcm)
+    have hconj := swap_smul_conj π a b t
+    exact hconj ▸ AEq.rename (π a) (π b) (π • t) hb'
+
+/-- α-equivalent terms have the same free variables. -/
+theorem aeq_fv {s t : Raw} (h : AEq s t) : fv s = fv t := by
+  induction h with
+  | rfl t => rfl
+  | symm _ ih => exact ih.symm
+  | trans _ _ ih1 ih2 => exact ih1.trans ih2
+  | app _ _ ih1 ih2 => simp only [fv_app, ih1, ih2]
+  | lam _ ih => simp only [fv_lam, ih]
+  | rename a b t hb =>
+    have hbfv : b ∉ fv t := fun hc => hb (fv_subset_atoms t hc)
+    simp only [fv_lam, fv_smul]
+    ext x
+    simp only [Finset.mem_sdiff, Finset.mem_image, Finset.mem_singleton]
+    constructor
+    · rintro ⟨hx, hxa⟩
+      exact ⟨⟨x, hx, FinPerm.swap_apply_of_ne_of_ne hxa (fun h => hbfv (h ▸ hx))⟩,
+        fun hxb => hbfv (hxb ▸ hx)⟩
+    · rintro ⟨⟨y, hy, hyx⟩, hxb⟩
+      rcases eq_or_ne y a with rfl | hya
+      · exact absurd (by rw [← hyx, FinPerm.swap_apply_left]) hxb
+      · rcases eq_or_ne y b with rfl | hyb
+        · exact absurd hy hbfv
+        · rw [FinPerm.swap_apply_of_ne_of_ne hya hyb] at hyx
+          exact ⟨hyx ▸ hy, fun hxa => hya (hyx ▸ hxa)⟩
+
+/-! ## The nominal term type `Tm := Raw / α` -/
+
+/-- The α-equivalence setoid. -/
+def aeqSetoid : Setoid Raw := ⟨AEq, AEq.equivalence⟩
+
+/-- **Nominal λ-terms**: raw terms up to α-equivalence. -/
+def Tm : Type := Quotient aeqSetoid
+
+/-- The class of a raw term. -/
+def Tm.mk (t : Raw) : Tm := Quotient.mk aeqSetoid t
+
+theorem Tm.mk_eq {s t : Raw} (h : AEq s t) : Tm.mk s = Tm.mk t := Quotient.sound h
+
+@[elab_as_elim]
+theorem Tm.ind {motive : Tm → Prop} (h : ∀ t : Raw, motive (Tm.mk t)) (q : Tm) : motive q :=
+  Quotient.ind h q
+
+/-- The permutation action descends to the quotient. -/
+instance : MulAction FinPerm Tm where
+  smul π := Quotient.lift (fun t => Tm.mk (π • t)) fun _ _ h => Tm.mk_eq (aeq_smul π h)
+  one_smul := Tm.ind fun t => Tm.mk_eq (by rw [one_smul]; exact AEq.rfl t)
+  mul_smul π₁ π₂ := Tm.ind fun t => Tm.mk_eq (by rw [mul_smul]; exact AEq.rfl _)
+
+@[simp] theorem Tm.smul_mk (π : FinPerm) (t : Raw) : π • Tm.mk t = Tm.mk (π • t) := rfl
+
+/-- Free variables, descended to the quotient (α-invariant). -/
+def Tm.freeVars : Tm → Finset Atom := Quotient.lift fv fun _ _ h => aeq_fv h
+
+@[simp] theorem Tm.freeVars_mk (t : Raw) : Tm.freeVars (Tm.mk t) = fv t := rfl
+
+/-! ### Constructors on `Tm`, and α-correctness of `lam` -/
+
+/-- Variable. -/
+def Tm.var (a : Atom) : Tm := Tm.mk (.var a)
+
+/-- Application. -/
+def Tm.app : Tm → Tm → Tm :=
+  Quotient.lift₂ (fun s t => Tm.mk (.app s t))
+    fun _ _ _ _ h₁ h₂ => Tm.mk_eq (AEq.app h₁ h₂)
+
+/-- Abstraction (binding). -/
+def Tm.lam (a : Atom) : Tm → Tm :=
+  Quotient.lift (fun t => Tm.mk (.lam a t)) fun _ _ h => Tm.mk_eq (AEq.lam h)
+
+@[simp] theorem Tm.lam_mk (a : Atom) (t : Raw) : Tm.lam a (Tm.mk t) = Tm.mk (.lam a t) := rfl
+
+/-- **α-correctness of `lam`**: `lam a t = lam b (swap a b • t)` for fresh `b`,
+an equality of terms — the defining property of a nominal binder. -/
+theorem Tm.lam_rename (a b : Atom) (t : Raw) (h : b ∉ atoms t) :
+    Tm.lam a (Tm.mk t) = Tm.lam b (Tm.mk (FinPerm.swap a b • t)) :=
+  Tm.mk_eq (AEq.rename a b t h)
+
+/-! ### Support minimality: `Tm` is a nominal set with `supp = fv`
+
+The nontrivial half: a permutation fixing the *free* variables of a term acts
+α-trivially on it. -/
+
+/-- A permutation fixing every free variable of `t` fixes `t` up to α. -/
+theorem aeq_of_fixes_fv : ∀ {t : Raw} {π : FinPerm}, (∀ a ∈ fv t, π a = a) → AEq (π • t) t := by
+  intro t
+  induction t with
+  | var a =>
+    intro π h; simp only [smul_var, h a (by simp)]; exact AEq.rfl _
+  | app s t ihs iht =>
+    intro π h
+    simp only [smul_app]
+    exact AEq.app (ihs fun a ha => h a (by simp [ha])) (iht fun a ha => h a (by simp [ha]))
+  | lam a s ih =>
+    intro π h
+    simp only [smul_lam]
+    set c := Atom.fresh (insert a (insert (π a) (atoms s ∪ atoms (π • s)))) with hcdef
+    have hcmem := Atom.fresh_not_mem (insert a (insert (π a) (atoms s ∪ atoms (π • s))))
+    rw [← hcdef] at hcmem
+    have hca : c ≠ a := fun he => hcmem (by rw [he]; exact Finset.mem_insert_self _ _)
+    have hcpa : c ≠ π a := fun he =>
+      hcmem (by rw [he]; exact Finset.mem_insert_of_mem (Finset.mem_insert_self _ _))
+    have hcs : c ∉ atoms s := fun hc =>
+      hcmem (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem (Finset.mem_union_left _ hc)))
+    have hcps : c ∉ atoms (π • s) := fun hc =>
+      hcmem (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem (Finset.mem_union_right _ hc)))
+    have e1 : AEq (Raw.lam a s) (Raw.lam c (FinPerm.swap a c • s)) := AEq.rename a c s hcs
+    have e2 : AEq (Raw.lam (π a) (π • s)) (Raw.lam c (FinPerm.swap (π a) c • (π • s))) :=
+      AEq.rename (π a) c (π • s) hcps
+    refine e2.trans (AEq.trans ?_ e1.symm)
+    apply AEq.lam
+    have hρ : ∀ x ∈ fv s, (FinPerm.swap a c * (FinPerm.swap (π a) c * π)) x = x := by
+      intro x hx
+      by_cases hxa : x = a
+      · subst hxa
+        simp only [FinPerm.mul_apply, FinPerm.swap_apply_left, FinPerm.swap_apply_right]
+      · have hxfv : x ∈ fv (Raw.lam a s) := by simp [hxa, hx]
+        have hpx : π x = x := h x hxfv
+        have hxc : x ≠ c := fun he => hcs (he ▸ fv_subset_atoms s hx)
+        have hxpa : x ≠ π a := fun he => hxa (π.val.injective (hpx.trans he))
+        simp only [FinPerm.mul_apply, hpx,
+          FinPerm.swap_apply_of_ne_of_ne hxpa hxc, FinPerm.swap_apply_of_ne_of_ne hxa hxc]
+    have hfix := ih hρ
+    have key := aeq_smul (FinPerm.swap a c) hfix
+    rw [← mul_smul, ← mul_assoc, FinPerm.swap_swap, one_mul, mul_smul] at key
+    exact key
+
+/-- **`Tm` is a nominal set** over `Atom`/`FinPerm`, with support the free
+variables. -/
+noncomputable instance : NomSet Tm where
+  supp := Tm.freeVars
+  supp_supports := by
+    refine Tm.ind fun t π h => ?_
+    exact Tm.mk_eq (aeq_of_fixes_fv fun a ha => h a (by simpa using ha))
+  supp_equivariant := by
+    refine Tm.ind fun t π => ?_
+    show Tm.freeVars (Tm.mk (π • t)) = (Tm.freeVars (Tm.mk t)).image (π ·)
+    simp [fv_smul]
+
+@[simp] theorem Tm.supp_mk (t : Raw) : NomSet.supp (Tm.mk t) = fv t := rfl
+
+end CatCrypt.Nominal.Lambda
diff --git a/Nominal/LambdaAbs.lean b/Nominal/LambdaAbs.lean
new file mode 100644
index 0000000..d170d68
--- /dev/null
+++ b/Nominal/LambdaAbs.lean
@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 Bas Spitters. All rights reserved.
+Released under MIT license as described in the file LICENSE.
+Authors: Bas Spitters
+-/
+import Nominal.Lambda
+
+set_option autoImplicit false
+
+/-!
+# `Tm.lam` as name abstraction
+
+The binder `Tm.lam a` factors through name abstraction: `Tm.lam a t = tmLam (abs a t)`.
+The fv-based α-rename `Tm.lam_rename_fresh` and the some=any principle
+`Tm.lam_some_any` follow from `abs_rename`.
+
+## Main results
+
+* `avoid` — an α-equivalent representative that avoids a chosen non-free atom.
+* `Tm.lam_rename_fresh` — rename the bound name to any atom fresh for the term.
+* `tmLam` and `Tm.lam_eq_tmLam` — the binder factors through `NameAbs Tm`.
+* `Tm.lam_some_any` — the Gabbay–Pitts some=any principle for the binder.
+-/
+
+namespace CatCrypt.Nominal.Lambda
+
+open CatCrypt.Nominal
+
+/-- **Rename a bound name away.** If `c` is not free in `r`, some α-equivalent
+`r'` avoids `c` entirely (as a bound name too). -/
+theorem avoid (c : Atom) : ∀ r : Raw, c ∉ fv r → ∃ r', AEq r r' ∧ c ∉ atoms r'
+  | .var a, h => ⟨.var a, .rfl _, by simpa using (by simpa using h : c ≠ a)⟩
+  | .app s t, h => by
+    obtain ⟨s', hs, hcs⟩ := avoid c s (fun hc => h (by simp [hc]))
+    obtain ⟨t', ht, hct⟩ := avoid c t (fun hc => h (by simp [hc]))
+    exact ⟨.app s' t', .app hs ht, by simp [hcs, hct]⟩
+  | .lam a t, h => by
+    by_cases hca : c = a
+    · subst hca
+      set d := Atom.fresh (insert c (atoms t)) with hd
+      have hdmem := Atom.fresh_not_mem (insert c (atoms t))
+      rw [← hd] at hdmem
+      have hdc : d ≠ c := fun he => hdmem (by rw [he]; exact Finset.mem_insert_self _ _)
+      have hdt : d ∉ atoms t := fun hc => hdmem (Finset.mem_insert_of_mem hc)
+      refine ⟨.lam d (FinPerm.swap c d • t), AEq.rename c d t hdt, ?_⟩
+      simp only [atoms_lam, atoms_smul, Finset.mem_insert, Finset.mem_image, not_or]
+      refine ⟨fun he => hdc he.symm, ?_⟩
+      rintro ⟨x, hx, hxe⟩
+      by_cases hxd : x = d
+      · exact hdt (hxd ▸ hx)
+      · by_cases hxc : x = c
+        · rw [hxc, FinPerm.swap_apply_left] at hxe; exact hdc hxe
+        · rw [FinPerm.swap_apply_of_ne_of_ne hxc hxd] at hxe; exact hxc hxe
+    · obtain ⟨t', ht, hct⟩ := avoid c t (fun hc => h (by simp [hca, hc]))
+      exact ⟨.lam a t', AEq.lam ht, by simp [hca, hct]⟩
+
+/-- **fv-based α-rename for `Tm.lam`.** Changing the bound name to any atom fresh
+for the term (not only for a representative) gives an equal term. -/
+theorem Tm.lam_rename_fresh (a c : Atom) (t : Tm) (hc : c ∉ Tm.freeVars t) (_hca : c ≠ a) :
+    Tm.lam a t = Tm.lam c (FinPerm.swap a c • t) := by
+  induction t using Tm.ind with
+  | _ r =>
+    obtain ⟨r', har, hcr'⟩ := avoid c r (by simpa using hc)
+    have h1 : Tm.lam a (Tm.mk r) = Tm.mk (.lam a r') := by
+      rw [Tm.mk_eq har]; rfl
+    have h2 : Tm.lam c (FinPerm.swap a c • Tm.mk r) = Tm.mk (.lam c (FinPerm.swap a c • r')) := by
+      rw [Tm.smul_mk, Tm.mk_eq (aeq_smul (FinPerm.swap a c) har)]; rfl
+    rw [h1, h2]
+    exact Tm.mk_eq (AEq.rename a c r' hcr')
+
+/-- The compatibility of `Tm.lam` with α-equivalence of the abstraction. -/
+theorem Tm.lam_absRel {a a' : Atom} {t t' : Tm} (h : AbsRel (a, t) (a', t')) :
+    Tm.lam a t = Tm.lam a' t' := by
+  refine NameAbs.absRel_respect_of_swap (fun a t => Tm.lam a t) ?_ a a' t t' h
+  intro b c x hc hcb
+  exact Tm.lam_rename_fresh b c x hc hcb
+
+/-- **`Tm.lam` factors through name abstraction.** -/
+noncomputable def tmLam : NameAbs Tm → Tm :=
+  NameAbs.lift (fun a t => Tm.lam a t) (fun _ _ _ _ h => Tm.lam_absRel h)
+
+@[simp] theorem tmLam_abs (a : Atom) (t : Tm) : tmLam (abs a t) = Tm.lam a t := rfl
+
+/-- The syntactic binder **is** the nominal abstraction: `Tm.lam a t = tmLam (abs a t)`. -/
+theorem Tm.lam_eq_tmLam (a : Atom) (t : Tm) : Tm.lam a t = tmLam (abs a t) := rfl
+
+/-- **Some = any (freshness) for the binder.** Two atoms fresh for the term give
+the same abstraction after the corresponding renaming — the Gabbay–Pitts
+principle, inherited from `abs`. -/
+theorem Tm.lam_some_any (a b c : Atom) (t : Tm)
+    (hb : b ∉ Tm.freeVars t) (hc : c ∉ Tm.freeVars t) (hba : b ≠ a) (hca : c ≠ a) :
+    Tm.lam b (FinPerm.swap a b • t) = Tm.lam c (FinPerm.swap a c • t) := by
+  rw [← Tm.lam_rename_fresh a b t hb hba, ← Tm.lam_rename_fresh a c t hc hca]
+
+end CatCrypt.Nominal.Lambda
diff --git a/NominalIris.lean b/NominalIris.lean
new file mode 100644
index 0000000..90996f9
--- /dev/null
+++ b/NominalIris.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Bas Spitters. All rights reserved.
+Released under MIT license as described in the file LICENSE.
+Authors: Bas Spitters
+-/
+import NominalIris.Separation
+import NominalIris.Camera
+import NominalIris.Den
+import NominalIris.Lambda
+
+/-!
+# `NominalIris` — nominal separation and binding in Iris
+
+The Iris/BI layer of the nominal development, over nominal-lean's `Atom` (so it
+shares the `Atom` / `FinPerm` / `NomSet` framework with the nominal λ-terms in
+`Nominal.Lambda`). Depends on iris-lean; the core `Nominal` library stays
+mathlib-only.
+
+* `NominalIris.Separation` — nominal separation as a model of (classical,
+  non-affine) BI: `NomProp` (iris-lean's classical heap BI, the `ℕ`-indexed
+  state reached via `Atom.val`), `worldProp` / `freshName`, and the headline
+  `freshName_sep_ne : freshName a ∗ freshName b ⊢ ⌜a ≠ b⌝`.
+* `NominalIris.Camera` — the `DisjointLeibnizSet` name camera, the `Auth`
+  allocation view-shift `name_alloc`, and the `iOwn` / `|==>` ghost-state layer
+  (`ownAuth` / `ownFresh` / `own_name_alloc` / `ownFresh_distinct`) with a
+  points-to notation.
+* `NominalIris.Den` — the `den` monoid morphism from the camera into the concrete
+  BI, proving the two readings agree (`concrete_sep_iff_camera_valid`).
+* `NominalIris.Lambda` — binding the nominal λ-terms `Nominal.Lambda.Tm` with the
+  name-allocation ghost state: `ownCtx` (context as ghost allocator), `abs_alloc`
+  ((Abs) as a `name_alloc` view-shift), `binders_distinct` (well-formedness as
+  separation), and `alloc_and_bind` (allocate a fresh binder and form the
+  α-correct abstraction `Tm.lam`).
+
+Everything is over one framework: atoms, name-worlds, and terms live in
+nominal-lean's nominal-sets framework; the BI propositions are built over those
+atoms (`NomProp` is not itself a nominal set — not every proposition is finitely
+supported).
+-/
diff --git a/NominalIris/Camera.lean b/NominalIris/Camera.lean
new file mode 100644
index 0000000..94392f9
--- /dev/null
+++ b/NominalIris/Camera.lean
@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2026 Bas Spitters. All rights reserved.
+Released under MIT license as described in the file LICENSE.
+Authors: Bas Spitters
+-/
+import Iris.Algebra.LeibnizSet
+import Iris.Algebra.Auth
+import Iris.Instances.IProp
+import Nominal.Atom
+
+set_option autoImplicit false
+
+/-!
+# The name camera and `iOwn` ghost state, over nominal `Atom`
+
+The `DisjointLeibnizSet` name camera and its `Auth` / `iOwn` ghost-state layer,
+over nominal-lean's `Atom` (so it shares the `Atom`/`FinPerm`/`NomSet` framework
+with the nominal λ-terms). This is the atom-agnostic part of the camera
+development — no concrete `HeapProp` BI is needed for the ghost-state name
+allocator (the `den` bridge to the concrete BI lives in `NominalIris.Den`).
+
+* `NameRA` — the name camera (`DisjointLeibnizSet` over finite atom sets).
+* `name_alloc` — the `Auth` allocation view-shift `● S ~~> ● (S ∪ {a}) • ◯ {a}`.
+* `ownAuth` / `ownFresh` — `iOwn` ghost ownership; `own_name_alloc`,
+  `own_name_alloc_init`, `ownFresh_distinct`; `HasNameAlloc` + points-to notation.
+-/
+
+namespace NominalIris
+
+open CatCrypt.Nominal (Atom)
+open Iris Iris.BI CMRA
+
+/-! ## Finite atom sets as an iris-lean lawful set -/
+
+/-- Finite atom sets, the carrier of the name camera. -/
+structure NameSet where
+  ofFinset ::
+  toFinset : Finset Atom
+deriving DecidableEq
+
+namespace NameSet
+
+instance : Membership Atom NameSet := ⟨fun s a => a ∈ s.toFinset⟩
+instance : Singleton Atom NameSet := ⟨fun a => ⟨{a}⟩⟩
+instance : Union NameSet := ⟨fun s t => ⟨s.toFinset ∪ t.toFinset⟩⟩
+instance : Inter NameSet := ⟨fun s t => ⟨s.toFinset ∩ t.toFinset⟩⟩
+instance : SDiff NameSet := ⟨fun s t => ⟨s.toFinset \ t.toFinset⟩⟩
+instance : EmptyCollection NameSet := ⟨⟨∅⟩⟩
+
+@[simp] theorem mem_iff (a : Atom) (s : NameSet) : a ∈ s ↔ a ∈ s.toFinset := Iff.rfl
+@[simp] theorem toFinset_singleton (a : Atom) : ({a} : NameSet).toFinset = {a} := rfl
+@[simp] theorem toFinset_union (s t : NameSet) :
+    (s ∪ t).toFinset = s.toFinset ∪ t.toFinset := rfl
+@[simp] theorem toFinset_inter (s t : NameSet) :
+    (s ∩ t).toFinset = s.toFinset ∩ t.toFinset := rfl
+@[simp] theorem toFinset_sdiff (s t : NameSet) :
+    (s \ t).toFinset = s.toFinset \ t.toFinset := rfl
+@[simp] theorem toFinset_empty : (∅ : NameSet).toFinset = ∅ := rfl
+
+instance : Iris.Std.Set NameSet Atom where
+
+instance : Iris.Std.LawfulSet NameSet Atom where
+  ext {X Y} h := by cases X; cases Y; congr 1; exact Finset.ext h
+  mem_empty {x} := by simp
+  mem_singleton {x y} := by simp [Finset.mem_singleton]
+  mem_union {X Y x} := by simp [Finset.mem_union]
+  mem_inter {X Y x} := by simp [Finset.mem_inter]
+  mem_diff {X Y x} := by simp [Finset.mem_sdiff]
+
+/-- iris-lean `##` on `NameSet` is mathlib `Finset` disjointness of the carriers. -/
+theorem disjoint_iff (s t : NameSet) : s ## t ↔ Disjoint s.toFinset t.toFinset := by
+  rw [Finset.disjoint_left]
+  exact ⟨fun h a ha hb => h a ⟨ha, hb⟩, fun h a hab => h hab.1 hab.2⟩
+
+theorem union_comm (s t : NameSet) : s ∪ t = t ∪ s := by
+  cases s; cases t
+  show NameSet.ofFinset _ = NameSet.ofFinset _
+  rw [Finset.union_comm]
+
+end NameSet
+
+/-! ## The name camera -/
+
+open DisjointLeibnizSet
+
+/-- The **name camera**: finite atom sets under disjoint union, a `UCMRA`. -/
+abbrev NameRA : Type := DisjointLeibnizSet NameSet
+
+/-- The **fresh-name resource** as a camera fragment: the world holding exactly `a`. -/
+def freshRA (a : Atom) : NameRA := .valid {a}
+
+theorem op_valid_valid (a b : NameSet) :
+    (DisjointLeibnizSet.valid a) • (DisjointLeibnizSet.valid b)
+      = if a ## b then .valid (a ∪ b) else .error := rfl
+
+theorem op_error_left (y : NameRA) : (DisjointLeibnizSet.error) • y = .error := rfl
+
+theorem op_valid_error (a : NameSet) :
+    (DisjointLeibnizSet.valid a) • (DisjointLeibnizSet.error) = .error := rfl
+
+/-- Camera validity of the combined fragments encodes distinctness of the names. -/
+theorem freshRA_valid_op_iff (a b : Atom) : ✓ (freshRA a • freshRA b) ↔ a ≠ b := by
+  rw [freshRA, freshRA, valid_op_iff_disj, NameSet.disjoint_iff,
+    NameSet.toFinset_singleton, NameSet.toFinset_singleton, Finset.disjoint_singleton]
+
+/-! ## `Auth` allocation -/
+
+section Allocation
+
+open OFE
+
+variable {F : Type _} [UFraction F]
+
+/-- The **allocation local update**: an unused name `a` may be split off the
+empty fragment, growing the authority from `S` to `S ∪ {a}`. -/
+theorem alloc_localUpdate {S : NameSet} {a : Atom} (h : a ∉ S) :
+    ((DisjointLeibnizSet.valid S, (UCMRA.unit : NameRA)) : NameRA × NameRA) ~l~>
+      (DisjointLeibnizSet.valid (S ∪ {a}), DisjointLeibnizSet.valid {a}) := by
+  rw [local_update_unital_discrete]
+  intro z _ he
+  have hz : (DisjointLeibnizSet.valid S) = z :=
+    Leibniz.leibniz.mp (he.trans (UCMRA.unit_left_id (x := z)))
+  subst hz
+  refine ⟨trivial, ?_⟩
+  have hdisj : ({a} : NameSet) ## S := by
+    rw [NameSet.disjoint_iff, NameSet.toFinset_singleton, Finset.disjoint_singleton_left]
+    exact h
+  calc DisjointLeibnizSet.valid (S ∪ {a})
+      = DisjointLeibnizSet.valid ({a} ∪ S) := by rw [NameSet.union_comm]
+    _ ≡ (DisjointLeibnizSet.valid ({a} : NameSet)) • (DisjointLeibnizSet.valid S) :=
+        (disj_op_union hdisj).symm
+
+/-- **In-logic name allocation** — the frame-preserving update in `Auth F NameRA`. -/
+theorem name_alloc {S : NameSet} {a : Atom} (h : a ∉ S) :
+    (Auth.authFull (DisjointLeibnizSet.valid S) : Auth F NameRA) ~~>
+      (Auth.authFull (DisjointLeibnizSet.valid (S ∪ {a}))) • Auth.frag (freshRA a) :=
+  Auth.auth_update_alloc (alloc_localUpdate h)
+
+/-- Validity of two combined fresh fragments encodes distinctness. -/
+theorem frag_freshRA_valid_ne {a b : Atom}
+    (hv : ✓ ((Auth.frag (freshRA a) • Auth.frag (freshRA b)) : Auth F NameRA)) : a ≠ b := by
+  rw [← Auth.frag_op] at hv
+  refine (freshRA_valid_op_iff a b).mp ?_
+  rw [CMRA.valid_iff_validN]
+  exact fun n => Auth.frag_validN.mp (CMRA.valid_iff_validN.mp hv n)
+
+end Allocation
+
+/-! ## `iOwn` ghost ownership -/
+
+section Own
+
+open Iris.BI COFE
+
+variable {Fr : Type _} [UFraction Fr]
+variable {GF : BundledGFunctors} [E : ElemG GF (constOF (Auth Fr NameRA))]
+
+set_option synthInstance.maxHeartbeats 1000000 in
+/-- The authoritative name camera is discrete. -/
+instance nameAuth_discrete : CMRA.Discrete (Auth Fr NameRA) := inferInstance
+
+/-- Ghost ownership of the **authoritative** allocated name-set `S` at `γ`. -/
+def ownAuth (γ : GName) (S : NameSet) : IProp GF :=
+  iOwn (GF := GF) (F := constOF (Auth Fr NameRA)) (E := E) γ
+    (Auth.authFull (DisjointLeibnizSet.valid S))
+
+/-- Ghost ownership of the **fresh-name fragment** for `a` at `γ`. -/
+def ownFresh (γ : GName) (a : Atom) : IProp GF :=
+  iOwn (GF := GF) (F := constOF (Auth Fr NameRA)) (E := E) γ (Auth.frag (freshRA a))
+
+end Own
+
+/-! ### Points-to notation -/
+
+set_option synthInstance.checkSynthOrder false in
+/-- `GF` carries a name allocator, recovering `GF`/`Fr` from `γ` alone. -/
+class abbrev HasNameAlloc (γ : GName) (GF : outParam BundledGFunctors)
+    (Fr : outParam (Type _)) [UFraction Fr] :=
+  ElemG GF (constOF (Auth Fr NameRA))
+
+/-- Owned authoritative name-set, allocator recovered from `γ`. -/
+def nAuth {Fr : Type _} [UFraction Fr] {GF : BundledGFunctors} (γ : GName)
+    [HasNameAlloc γ GF Fr] (S : NameSet) : IProp GF := ownAuth (Fr := Fr) γ S
+
+/-- Owned fresh name, allocator recovered from `γ`. -/
+def nFresh {Fr : Type _} [UFraction Fr] {GF : BundledGFunctors} (γ : GName)
+    [HasNameAlloc γ GF Fr] (a : Atom) : IProp GF := ownFresh (Fr := Fr) γ a
+
+@[inherit_doc] scoped notation:55 γ:56 " ⊨auth " S:56 => nAuth γ S
+@[inherit_doc] scoped notation:55 γ:56 " ⊨fresh " a:56 => nFresh γ a
+
+section Own
+variable {Fr : Type _} [UFraction Fr]
+variable {GF : BundledGFunctors} [E : ElemG GF (constOF (Auth Fr NameRA))]
+
+/-- **`own`-level name allocation** (`iOwn_update ∘ name_alloc`). -/
+theorem own_name_alloc (γ : GName) {S : NameSet} {a : Atom} (h : a ∉ S) :
+    ownAuth (Fr := Fr) (E := E) γ S ⊢
+      |==> (ownAuth (Fr := Fr) (E := E) γ (S ∪ {a}) ∗ ownFresh (Fr := Fr) (E := E) γ a) := by
+  unfold ownAuth ownFresh
+  exact (iOwn_update (name_alloc (F := Fr) h)).trans (BIUpdate.mono iOwn_op.1)
+
+/-- **Creating a fresh name allocator** from nothing. -/
+theorem own_name_alloc_init :
+    ⊢ |==> ∃ γ, ownAuth (Fr := Fr) (E := E) γ (∅ : NameSet) := by
+  unfold ownAuth
+  refine iOwn_alloc _ ?_
+  rw [CMRA.valid_iff_validN]
+  intro n
+  rw [Auth.auth_validN]
+  exact trivial
+
+/-- **Two owned fresh names are distinct** — separation forces `a ≠ b`. -/
+theorem ownFresh_distinct (γ : GName) (a b : Atom) :
+    (ownFresh (Fr := Fr) (E := E) γ a ∗ ownFresh (Fr := Fr) (E := E) γ b : IProp GF) ⊢
+      ⌜a ≠ b⌝ := by
+  unfold ownFresh
+  exact iOwn_cmraValid_op.trans
+    (internalCmraValid_discrete.1.trans (BI.pure_mono frag_freshRA_valid_ne))
+
+end Own
+
+end NominalIris
diff --git a/NominalIris/Den.lean b/NominalIris/Den.lean
new file mode 100644
index 0000000..7c42c3b
--- /dev/null
+++ b/NominalIris/Den.lean
@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2026 Bas Spitters. All rights reserved.
+Released under MIT license as described in the file LICENSE.
+Authors: Bas Spitters
+-/
+import NominalIris.Camera
+import NominalIris.Separation
+
+set_option autoImplicit false
+
+/-!
+# The camera ↔ concrete-BI equivalence, over nominal `Atom`
+
+Bridges the `Atom` name camera (`NominalGhostAtom`) to the `Atom` nominal-
+separation BI (`NominalBIAtom`): the denotation `den` is a monoid morphism from
+the camera into the concrete BI, so the concrete headline `freshName_sep_ne` is
+the image of camera validity. This is the `ℕ`-version equivalence, rebased onto
+`Atom` so the whole stack shares one framework.
+-/
+
+namespace NominalIris
+
+open Iris Iris.BI CMRA
+open CatCrypt.Nominal (Atom)
+open DisjointLeibnizSet
+
+/-- The `False` proposition, the denotation of the invalid element. -/
+def nomFalse : NomProp := fun _ => False
+
+/-- The **denotation** of a name-camera element as a concrete nominal
+proposition. -/
+def den : NameRA → NomProp
+  | .valid w => worldProp w.toFinset
+  | .error   => nomFalse
+
+@[simp] theorem den_valid (w : NameSet) : den (.valid w) = worldProp w.toFinset := rfl
+@[simp] theorem den_error : den .error = nomFalse := rfl
+
+theorem den_freshRA (a : Atom) : den (freshRA a) = freshName a := by
+  rw [freshRA, den_valid, NameSet.toFinset_singleton, freshName_eq_worldProp]
+
+theorem den_unit : den (UCMRA.unit : NameRA) = (emp : NomProp) := by
+  show den (.valid ∅) = _
+  rw [den_valid, NameSet.toFinset_empty, worldProp_empty]
+
+private theorem nomFalse_sep (Q : NomProp) : (iprop(nomFalse ∗ Q) : NomProp) = nomFalse := by
+  funext σ; apply propext
+  exact ⟨fun ⟨_, _, _, _, h, _⟩ => h.elim, fun h => h.elim⟩
+
+private theorem sep_nomFalse (P : NomProp) : (iprop(P ∗ nomFalse) : NomProp) = nomFalse := by
+  funext σ; apply propext
+  exact ⟨fun ⟨_, _, _, _, _, h⟩ => h.elim, fun h => h.elim⟩
+
+/-- **Camera `•` ↦ separating `∗`, unconditionally.** -/
+theorem den_op (x y : NameRA) : (den (x • y) : NomProp) ⊣⊢ iprop(den x ∗ den y) := by
+  cases x with
+  | error => rw [op_error_left, den_error, nomFalse_sep]; exact .rfl
+  | valid a =>
+    cases y with
+    | error => rw [op_valid_error, den_error, sep_nomFalse]; exact .rfl
+    | valid b =>
+      rw [op_valid_valid]
+      by_cases h : a ## b
+      · rw [if_pos h, den_valid, NameSet.toFinset_union, den_valid, den_valid]
+        exact (worldProp_sep ((NameSet.disjoint_iff a b).mp h)).symm
+      · have hnd : ¬ Disjoint a.toFinset b.toFinset :=
+          fun hd => h ((NameSet.disjoint_iff a b).mpr hd)
+        rw [if_neg h, den_error, den_valid, den_valid]
+        constructor
+        · intro σ hσ; exact hσ.elim
+        · intro σ hσ; exact (hnd (worldProp_sep_disjoint a.toFinset b.toFinset σ hσ)).elim
+
+/-- **Camera validity ↦ satisfiability.** -/
+theorem den_valid_iff (x : NameRA) : (∃ σ, den x σ) ↔ ✓ x := by
+  cases x with
+  | error => exact ⟨fun ⟨_, hσ⟩ => hσ.elim, fun hv => hv.elim⟩
+  | valid w => exact ⟨fun _ => True.intro, fun _ => ⟨toNS w.toFinset, rfl⟩⟩
+
+/-- **The equivalence.** Separability of the two concrete fresh-name resources is
+camera validity of the combined fragments. -/
+theorem concrete_sep_iff_camera_valid (a b : Atom) :
+    (∃ σ, (iprop(freshName a ∗ freshName b) : NomProp) σ) ↔ ✓ (freshRA a • freshRA b) := by
+  rw [← den_valid_iff]
+  constructor
+  · rintro ⟨σ, hσ⟩
+    refine ⟨σ, ?_⟩
+    have hσ' : (iprop(den (freshRA a) ∗ den (freshRA b)) : NomProp) σ := by
+      rw [den_freshRA, den_freshRA]; exact hσ
+    exact (den_op (freshRA a) (freshRA b)).mpr σ hσ'
+  · rintro ⟨σ, hσ⟩
+    refine ⟨σ, ?_⟩
+    have hσ' := (den_op (freshRA a) (freshRA b)).mp σ hσ
+    rw [den_freshRA, den_freshRA] at hσ'
+    exact hσ'
+
+/-- **The concrete headline law, recovered from the camera.** -/
+theorem freshName_sep_ne_via_camera (a b : Atom) :
+    (iprop(freshName a ∗ freshName b) : NomProp) ⊢ iprop(⌜a ≠ b⌝) := by
+  intro σ hσ
+  exact (freshRA_valid_op_iff a b).mp ((concrete_sep_iff_camera_valid a b).mp ⟨σ, hσ⟩)
+
+end NominalIris
diff --git a/NominalIris/Lambda.lean b/NominalIris/Lambda.lean
new file mode 100644
index 0000000..fa5dd87
--- /dev/null
+++ b/NominalIris/Lambda.lean
@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2026 Bas Spitters. All rights reserved.
+Released under MIT license as described in the file LICENSE.
+Authors: Bas Spitters
+-/
+import NominalIris.Camera
+import Nominal.Lambda
+
+set_option autoImplicit false
+
+/-!
+# Binding the nominal λ-calculus with name-allocation ghost state
+
+The nominal λ-terms `Tm` (α-quotiented, `Nominal.Lambda`) and the name-allocation
+ghost state (`NominalIris.Camera`) share the one `Atom` framework, so binding can
+be expressed *in Iris*: a typing context is a ghost **name allocator**, the
+`(Abs)` rule allocates its bound variable as the `name_alloc` view-shift, and the
+allocated fresh name binds a genuine α-correct nominal abstraction `Tm.lam`.
+
+* `ownCtx` / `abs_alloc` / `binders_distinct` — the binding model over `Atom`.
+* `Tm.bound_not_free` — the bound name of a nominal abstraction is not free in it.
+* `alloc_and_bind` — allocate a fresh binder and form a well-scoped nominal
+  abstraction, under the basic update.
+-/
+
+namespace NominalIris
+
+open CatCrypt.Nominal (Atom)
+open CatCrypt.Nominal.Lambda (Tm)
+open Iris Iris.BI CMRA COFE
+
+/-! ## Nominal terms: the bound name is fresh for the abstraction -/
+
+/-- Free variables of a nominal abstraction: the body's, minus the binder. -/
+theorem Tm.freeVars_lam (a : Atom) (t : Tm) :
+    Tm.freeVars (Tm.lam a t) = Tm.freeVars t \ {a} := by
+  induction t using CatCrypt.Nominal.Lambda.Tm.ind with
+  | _ r => simp [CatCrypt.Nominal.Lambda.Tm.lam_mk]
+
+/-- **The bound name is not free in the abstraction** — well-scopedness of a
+nominal binder, holding as a property of the term. -/
+theorem Tm.bound_not_free (a : Atom) (t : Tm) : a ∉ Tm.freeVars (Tm.lam a t) := by
+  rw [Tm.freeVars_lam]; simp
+
+/-! ## Simple types and the context allocator -/
+
+/-- Simple types. -/
+inductive Ty where
+  | base : Ty
+  | arr : Ty → Ty → Ty
+  deriving DecidableEq
+
+/-- A typing context. -/
+abbrev Ctx : Type := List (Atom × Ty)
+
+/-- The atoms a context binds. -/
+def ctxDom (Γ : Ctx) : Finset Atom := (Γ.map Prod.fst).toFinset
+
+@[simp] theorem ctxDom_cons (a : Atom) (T : Ty) (Γ : Ctx) :
+    ctxDom ((a, T) :: Γ) = insert a (ctxDom Γ) := by simp [ctxDom]
+
+theorem nameSet_eq {s t : NameSet} (h : s.toFinset = t.toFinset) : s = t := by
+  cases s; cases t; exact congrArg _ h
+
+theorem ctxNS_cons (a : Atom) (T : Ty) (Γ : Ctx) :
+    NameSet.ofFinset (ctxDom ((a, T) :: Γ)) = NameSet.ofFinset (ctxDom Γ) ∪ {a} := by
+  apply nameSet_eq
+  simp only [NameSet.toFinset_union, NameSet.toFinset_singleton, ctxDom_cons]
+  ext x
+  simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton, or_comm]
+
+section Binding
+
+variable {Fr : Type _} [UFraction Fr] {GF : BundledGFunctors}
+
+/-- A typing context realised as a ghost name allocator. -/
+def ownCtx (γ : GName) [HasNameAlloc γ GF Fr] (Γ : Ctx) : IProp GF :=
+  nAuth γ (NameSet.ofFinset (ctxDom Γ))
+
+/-- **The `(Abs)` rule as fresh-name allocation.** Allocate a fresh binder for
+the context, obtaining `a # Γ`, ownership of it, and the extended context. -/
+theorem abs_alloc (γ : GName) [HasNameAlloc γ GF Fr] (Γ : Ctx) (S : Ty) :
+    ownCtx γ Γ ⊢ |==> ∃ a : Atom, ⌜a ∉ ctxDom Γ⌝ ∗ nFresh γ a ∗ ownCtx γ ((a, S) :: Γ) := by
+  obtain ⟨a, ha⟩ : ∃ a, a ∉ ctxDom Γ := ⟨Atom.fresh (ctxDom Γ), Atom.fresh_not_mem _⟩
+  unfold ownCtx nAuth nFresh
+  iintro H
+  imod own_name_alloc γ (S := NameSet.ofFinset (ctxDom Γ)) (a := a) (by simpa using ha) $$ H
+    with ⟨Hauth, Hf⟩
+  imodintro
+  iexists a
+  rw [ctxNS_cons]
+  isplit
+  · ipure_intro; exact ha
+  · isplitl [Hf]
+    · iexact Hf
+    · iexact Hauth
+
+/-- **Context well-formedness is separation**: two owned binder names are distinct. -/
+theorem binders_distinct (γ : GName) [HasNameAlloc γ GF Fr] (a b : Atom) :
+    (nFresh γ a ∗ nFresh γ b : IProp GF) ⊢ ⌜a ≠ b⌝ := by
+  unfold nFresh
+  exact ownFresh_distinct γ a b
+
+/-- **Allocate a fresh binder and bind a nominal term.** From the context
+allocator, allocate `a # Γ`, obtain ownership of it, and form the α-correct
+nominal abstraction `Tm.lam a t`, whose bound name is provably fresh for it. -/
+theorem alloc_and_bind (γ : GName) [HasNameAlloc γ GF Fr] (Γ : Ctx) (S : Ty) (t : Tm) :
+    ownCtx γ Γ ⊢
+      |==> ∃ a : Atom, nFresh γ a ∗ ⌜a ∉ Tm.freeVars (Tm.lam a t)⌝ ∗ ownCtx γ ((a, S) :: Γ) := by
+  refine (abs_alloc γ Γ S).trans (BIUpdate.mono ?_)
+  iintro ⟨%a, _, Hf, Hc⟩
+  iexists a
+  isplitl [Hf]
+  · iexact Hf
+  · isplit
+    · ipure_intro; exact Tm.bound_not_free a t
+    · iexact Hc
+
+end Binding
+
+end NominalIris
diff --git a/NominalIris/PR.md b/NominalIris/PR.md
new file mode 100644
index 0000000..cd57956
--- /dev/null
+++ b/NominalIris/PR.md
@@ -0,0 +1,88 @@
+# Nominal separation and binding in Iris
+
+## Summary
+
+This PR adds an Iris/BI layer on top of nominal-lean: nominal separation as a
+model of bunched implications, a name-allocation ghost state, and the
+simply-typed λ-calculus whose binding is expressed as that ghost state, built on
+an α-quotient nominal term type. Atoms, name-worlds, and terms live in
+nominal-lean's `Atom` / `FinPerm` / `NomSet`; the Iris layer (`NominalIris.*`) is
+built over those atoms.
+
+The headline law is the nominal analogue of `ℓ₁ ↦ ∗ ℓ₂ ↦ ⊢ ℓ₁ ≠ ℓ₂`:
+
+```lean
+theorem freshName_sep_ne (a b : Atom) :
+    (freshName a ∗ freshName b : NomProp) ⊢ iprop(⌜a ≠ b⌝)
+```
+
+and its ghost-state image is that two owned fresh names are distinct
+(`ownFresh_distinct`), which is exactly the well-formedness (distinct binders) of
+a typing context.
+
+## What it adds
+
+### `Nominal/Lambda.lean` (core, mathlib-only) — the λ-calculus as a nominal set
+
+Terms defined *nominally from the start*: raw terms carry the `FinPerm` action and
+form a `NomSet`; quotienting by α-equivalence yields `Tm`, with an α-correct
+binder.
+
+- `Raw` / `atoms` / `fv`; `instance : NomSet Raw`.
+- `AEq` — α-equivalence as a **generated congruence** (`refl`/`symm`/`trans` are
+  constructors, so it is an equivalence relation by construction).
+- `Tm := Raw / AEq`, `Tm.var` / `Tm.app` / `Tm.lam`; `instance : NomSet Tm`
+  (support = `fv`, minimality via `aeq_of_fixes_fv`).
+- `Tm.lam_rename` — **α-correctness of the binder**: `lam a t = lam b (swap a b • t)`
+  for fresh `b`, as a property of the term.
+
+`Nominal/LambdaAbs.lean` proves `Tm.lam a t = tmLam (abs a t)`: the binder factors
+through name abstraction `NameAbs Tm`, which gives the fv-based α-rename
+(`Tm.lam_rename_fresh`) and the some=any principle (`Tm.lam_some_any`).
+
+### `NominalIris/*` (iris-lean layer, over `Atom`)
+
+- **`Separation`** — nominal separation as classical BI: `NomProp = HeapProp Unit`
+  (the `ℕ`-indexed state reached via `Atom.val`), `worldProp` / `freshName`,
+  `worldProp_sep`, `freshName_sep_ne`.
+- **`Camera`** — the `DisjointLeibnizSet` name camera; `name_alloc`
+  (`● S ~~> ● (S ∪ {a}) • ◯ {a}`); the `iOwn` / `|==>` layer `ownAuth` /
+  `ownFresh` / `own_name_alloc` / `own_name_alloc_init` / `ownFresh_distinct`;
+  `HasNameAlloc` + points-to notation.
+- **`Den`** — `den`, a monoid morphism from the camera into the concrete BI,
+  proving the two readings agree (`den_op`, `den_valid_iff`,
+  `concrete_sep_iff_camera_valid`, `freshName_sep_ne_via_camera`).
+- **`Lambda`** — binding the nominal `Tm` with the ghost state: `ownCtx` (context
+  as ghost allocator), `abs_alloc` ((Abs) as a `name_alloc` view-shift),
+  `binders_distinct` (well-formedness as separation), and `alloc_and_bind` —
+  allocate a fresh binder and form the α-correct abstraction `Tm.lam a t`, bound
+  name provably fresh (`Tm.bound_not_free`).
+
+## Design notes
+
+- **One framework.** Atoms/name-worlds/terms use nominal-lean's nominal-sets
+  framework; the BI props are built over those atoms. `NomProp` is *not* itself a
+  `NomSet` — not every proposition is finitely supported — so permutation /
+  equivariance for the nominal objects comes from `NomSet` / `FinPerm`, not a
+  bespoke action on `NomProp`.
+- **Reused components.** `NomProp = HeapProp Unit` is iris-lean's classical BI,
+  so `∗` is disjoint name-support splitting. The name camera is iris-lean's
+  `DisjointLeibnizSet` (the `gset`/`copset` RA).
+- **Classical fragment.** Name resources are flat and first-order, so the
+  development uses no `▷`/OFE/step-indexing, and `name_alloc` is a discrete ghost
+  update.
+
+## Dependencies / hygiene
+
+- Adds `require iris` (iris-lean, `v4.30.0`) to the lakefile; used only by the
+  `NominalIris` target. The core `Nominal` library stays mathlib-only.
+- No `sorry`. Axioms: `propext`, `Classical.choice`, `Quot.sound` only.
+- Builds with `lake build NominalIris`.
+
+## Follow-ups
+
+- The `И`-quantifier over name-worlds, alongside the some=any principle for the
+  binder (`Tm.lam_some_any`) already in `LambdaAbs`.
+- Subject reduction and Church–Rosser on `Tm`: substitution via the nominal
+  recursor `NameAbs.lift` (α handled by construction through `tmLam`).
+- A semantic type-safety proof (logical relations) over iris-lean's WP.
diff --git a/NominalIris/Separation.lean b/NominalIris/Separation.lean
new file mode 100644
index 0000000..bce03e8
--- /dev/null
+++ b/NominalIris/Separation.lean
@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2026 Bas Spitters. All rights reserved.
+Released under MIT license as described in the file LICENSE.
+Authors: Bas Spitters
+-/
+import Iris.ProofMode
+import Iris.Instances.Classical.Instance
+import Nominal.Atom
+
+set_option autoImplicit false
+
+/-!
+# Nominal separation as a BI, over nominal `Atom`
+
+The nominal-separation BI (`freshName a ∗ freshName b ⊢ ⌜a ≠ b⌝`) over
+nominal-lean's `Atom`, so it shares the framework with the nominal λ-terms and
+the name camera. The iris-lean classical heap state is `ℕ`-indexed; an atom `a`
+occupies location `a.val` (`Atom ≅ ℕ`), so name-worlds embed faithfully.
+
+Permutation and equivariance for the nominal objects — name-worlds
+(`Finset Atom`) and terms — use nominal-lean's `NomSet` / `FinPerm` action.
+`NomProp` is not itself a nominal set: not every proposition has finite support.
+-/
+
+namespace NominalIris
+
+open Iris.BI
+open Iris.Instances.Data
+open CatCrypt.Nominal (Atom)
+
+/-- A **name-world**: a finite set of atoms. -/
+abbrev NameWorld : Type := Finset Atom
+
+/-- The nominal state model: allocated-or-not per `ℕ` location (trivial payload). -/
+abbrev NomState : Type := State Unit
+
+/-- Nominal propositions: iris-lean's classical heap BI over `NomState`. -/
+abbrev NomProp : Type := Iris.Instances.Classical.HeapProp Unit
+
+/-- Realise a name-world as a nominal state: `result ()` at location `a.val` for
+each `a` in the world, `unknown` elsewhere. -/
+def toNS (w : NameWorld) : NomState :=
+  fun i => if (⟨i⟩ : Atom) ∈ w then .result () else .unknown
+
+theorem nsUnion_apply (σ₁ σ₂ : NomState) (i : Nat) :
+    (σ₁ ∪ σ₂) i = (match σ₁ i, σ₂ i with
+      | .unknown , .unknown  => .unknown
+      | .result x, .unknown  => .result x
+      | .unknown , .result y => .result y
+      | _        , _         => .conflict) := by
+  show Union.union σ₁ σ₂ i = _
+  simp only [Union.union]
+  cases σ₁ i <;> cases σ₂ i <;> rfl
+
+theorem toNS_apply (w : NameWorld) (i : Nat) :
+    toNS w i = if (⟨i⟩ : Atom) ∈ w then .result () else .unknown := rfl
+
+theorem mem_iff_val (a : Atom) (w : NameWorld) : (⟨a.val⟩ : Atom) ∈ w ↔ a ∈ w := by
+  rw [show (⟨a.val⟩ : Atom) = a from rfl]
+
+theorem toNS_empty : toNS ∅ = (∅ : NomState) := by
+  funext i; rw [toNS_apply, if_neg (Finset.notMem_empty _)]; rfl
+
+theorem toNS_injective : Function.Injective toNS := by
+  intro w₁ w₂ h
+  ext a
+  have ha := congrFun h a.val
+  simp only [toNS_apply, show (⟨a.val⟩ : Atom) = a from rfl] at ha
+  by_cases h1 : a ∈ w₁ <;> by_cases h2 : a ∈ w₂ <;> simp_all
+
+theorem toNS_disjoint_iff (w₁ w₂ : NameWorld) :
+    (toNS w₁ || toNS w₂) ↔ Disjoint w₁ w₂ := by
+  rw [Finset.disjoint_left]
+  constructor
+  · intro h a ha1 ha2
+    rcases h a.val with h1 | h1
+    · rw [toNS_apply, if_pos (by simpa using ha1)] at h1; exact absurd h1 (by simp)
+    · rw [toNS_apply, if_pos (by simpa using ha2)] at h1; exact absurd h1 (by simp)
+  · intro h i
+    by_cases hi1 : (⟨i⟩ : Atom) ∈ w₁
+    · exact Or.inr (by rw [toNS_apply, if_neg (h hi1)])
+    · exact Or.inl (by rw [toNS_apply, if_neg hi1])
+
+theorem toNS_union {w₁ w₂ : NameWorld} (h : Disjoint w₁ w₂) :
+    toNS (w₁ ∪ w₂) = toNS w₁ ∪ toNS w₂ := by
+  funext i
+  rw [nsUnion_apply]
+  simp only [toNS_apply, Finset.mem_union]
+  rw [Finset.disjoint_left] at h
+  by_cases h1 : (⟨i⟩ : Atom) ∈ w₁ <;> by_cases h2 : (⟨i⟩ : Atom) ∈ w₂ <;> simp_all
+
+/-- The proposition "the world is exactly `w`". -/
+def worldProp (w : NameWorld) : NomProp := fun σ => σ = toNS w
+
+/-- The singleton state for atom `a`. -/
+def singletonState (a : Atom) : NomState :=
+  fun i => if i = a.val then .result () else .unknown
+
+theorem singletonState_eq (a : Atom) : singletonState a = toNS {a} := by
+  funext i
+  simp only [singletonState, toNS_apply, Finset.mem_singleton, Atom.ext_iff]
+
+/-- The **fresh-name resource**: the world holding exactly the name `a`. -/
+def freshName (a : Atom) : NomProp := fun σ => σ = singletonState a
+
+theorem freshName_eq_worldProp (a : Atom) : freshName a = worldProp {a} := by
+  unfold freshName worldProp; rw [singletonState_eq]
+
+theorem worldProp_empty : worldProp (∅ : NameWorld) = (emp : NomProp) := by
+  unfold worldProp; rw [toNS_empty]; rfl
+
+/-- **Distinct-support law.** `worldProp w₁ ∗ worldProp w₂` forces the supports
+disjoint. -/
+theorem worldProp_sep_disjoint (w₁ w₂ : NameWorld) :
+    (worldProp w₁ ∗ worldProp w₂ : NomProp) ⊢ iprop(⌜Disjoint w₁ w₂⌝) := by
+  rintro σ ⟨σ₁, σ₂, _, hd, h1, h2⟩
+  subst h1; subst h2
+  exact (toNS_disjoint_iff w₁ w₂).mp hd
+
+/-- On disjoint supports, `∗` of two worlds is the union world. -/
+theorem worldProp_sep {w₁ w₂ : NameWorld} (h : Disjoint w₁ w₂) :
+    (worldProp w₁ ∗ worldProp w₂ : NomProp) ⊣⊢ worldProp (w₁ ∪ w₂) := by
+  constructor
+  · rintro σ ⟨σ₁, σ₂, hu, _, h1, h2⟩
+    subst h1; subst h2
+    show σ = toNS (w₁ ∪ w₂); rw [hu, toNS_union h]
+  · rintro σ hσ
+    refine ⟨toNS w₁, toNS w₂, ?_, (toNS_disjoint_iff w₁ w₂).mpr h, rfl, rfl⟩
+    show σ = toNS w₁ ∪ toNS w₂; rw [hσ, toNS_union h]
+
+/-- **Headline nominal law.** Two distinct fresh names are separated. -/
+theorem freshName_sep_ne (a b : Atom) :
+    (freshName a ∗ freshName b : NomProp) ⊢ iprop(⌜a ≠ b⌝) := by
+  rintro σ ⟨σ₁, σ₂, _, hd, h1, h2⟩
+  subst h1; subst h2
+  intro hab; subst hab
+  rcases hd a.val with h | h <;> simp [singletonState] at h
+
+end NominalIris
diff --git a/lake-manifest.json b/lake-manifest.json
index e5ad73b..47f600c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -11,6 +11,16 @@
    "inputRev": "v4.30.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/iris-lean",
+   "type": "git",
+   "subDir": "Iris",
+   "scope": "",
+   "rev": "6ddf890e97c4ea058aa962fcd7a951646475e1ba",
+   "name": "iris",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
diff --git a/lakefile.lean b/lakefile.lean
index 500de79..a1ae833 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -16,6 +16,19 @@ lean_lib Nominal where
   -- so downstream `CatCryptCore` / `CatCrypt` shims re-export without churn.
   globs := #[.andSubmodules `Nominal]
 
--- mathlib only: this is an upstream leaf. No crypto / SSProve-package deps.
+-- Module root `NominalIris.*` (namespace `Nominal.Iris`). The Iris/BI reading of
+-- nominal separation: disjoint name-support as a model of bunched implications,
+-- its `DisjointLeibnizSet` camera, and the `iOwn` name-allocation view-shift.
+-- A separate library so the core `Nominal` target stays mathlib-only; only this
+-- target pulls in iris-lean.
+lean_lib NominalIris where
+  globs := #[.andSubmodules `NominalIris]
+
+-- mathlib: the core dependency.
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4" @ "v4.30.0"
+
+-- iris-lean (Lean 4 Iris port): BI + proof mode + cameras + the IProp base logic.
+-- Used only by the `NominalIris` target.
+require iris from git
+  "https://github.com/leanprover-community/iris-lean" @ "v4.30.0" / "Iris"