Locations and Heaps for Deep Embedding

This file defines locations and heaps for the deep embedding of CatCrypt computations.

Main definitions

• Location - A location pairs an atom (name) with a type
• DeepHeap - A heap mapping locations to values
• DeepHeap.empty - The empty heap
• DeepHeap.get - Get value from a location
• DeepHeap.set - Set value at a location

Nominal Structure

Locations are equipped with a nominal structure:

• Permutations act on the atom while preserving the type: π • ℓ = ⟨π • ℓ.name, ℓ.ty⟩
• The support of a location is the singleton of its atom: supp ℓ = {ℓ.name}

Design decision: Two locations with the same name but different types are considered different locations. This is the mathematically consistent approach: Location equality is structural equality of the pair (name, ty). The heap stores values indexed by the full location (including type), so there's no inconsistency.

This means you cannot have two locations with the same name but different types "collide" in a heap - they simply occupy different slots.

References

• SSProve theories/Crypt/rhl_semantics/free_prot/free_code.v
• Larsen and Schürmann, Nominal State-Separating Proofs

structure CatCrypt.Deep.Location : Type (u_1 + 1)

A location pairs an atom (name) with a type. This represents a typed memory location in the deep embedding.

Two locations are equal iff both name AND ty are equal. This is standard structural equality - no axioms needed.

• name : Nominal.Atom

  The name of the location

• ty : Type u_1

  The type of values stored at this location

def CatCrypt.Deep.Location.beqName (ℓ₁ : Location) (ℓ₂ : Location) : Bool

Decidable equality on the name component only. Note: This is weaker than structural equality since it ignores types.

Equations

• ℓ₁.beqName ℓ₂ = (ℓ₁.name == ℓ₂.name)

theorem CatCrypt.Deep.Location.ext_iff {ℓ₁ ℓ₂ : Location} : ℓ₁ = ℓ₂ ↔ ℓ₁.name = ℓ₂.name ∧ ℓ₁.ty = ℓ₂.ty

Two locations are equal iff they have the same name and type. This follows from the structure definition.

theorem CatCrypt.Deep.Location.ext {ℓ₁ ℓ₂ : Location} (hn : ℓ₁.name = ℓ₂.name) (ht : ℓ₁.ty = ℓ₂.ty) : ℓ₁ = ℓ₂

theorem CatCrypt.Deep.Location.name_eq_of_eq {ℓ₁ ℓ₂ : Location} (h : ℓ₁ = ℓ₂) : ℓ₁.name = ℓ₂.name

theorem CatCrypt.Deep.Location.ty_eq_of_eq {ℓ₁ ℓ₂ : Location} (h : ℓ₁ = ℓ₂) : ℓ₁.ty = ℓ₂.ty

def CatCrypt.Deep.Location.perm (π : Nominal.FinPerm) (ℓ : Location) : Location

Apply a permutation to a location by permuting its atom name. The type is preserved: (π • ℓ).ty = ℓ.ty.

Equations

• CatCrypt.Deep.Location.perm π ℓ = { name := π.apply ℓ.name, ty := ℓ.ty }

@[simp]

theorem CatCrypt.Deep.Location.perm_name (π : Nominal.FinPerm) (ℓ : Location) : (perm π ℓ).name = π.apply ℓ.name

@[simp]

theorem CatCrypt.Deep.Location.perm_ty (π : Nominal.FinPerm) (ℓ : Location) : (perm π ℓ).ty = ℓ.ty

@[simp]

theorem CatCrypt.Deep.Location.perm_one (ℓ : Location) : perm 1 ℓ = ℓ

theorem CatCrypt.Deep.Location.perm_mul (π₁ π₂ : Nominal.FinPerm) (ℓ : Location) : perm (π₁ * π₂) ℓ = perm π₁ (perm π₂ ℓ)

Nominal Instances for Location

Locations form a nominal set where:

• Permutations act on the atom, preserving the type
• The support is the singleton of the atom

@[implicit_reducible]

instance CatCrypt.Deep.instMulActionFinPermLocation : MulAction Nominal.FinPerm Location

Nominal action on locations: permute the atom, preserve the type

Equations

• CatCrypt.Deep.instMulActionFinPermLocation = { smul := CatCrypt.Deep.Location.perm, mul_smul := CatCrypt.Deep.Location.perm_mul, one_smul := CatCrypt.Deep.Location.perm_one }

@[implicit_reducible]

instance CatCrypt.Deep.instNomSetLocation : Nominal.NomSet Location

Locations form a nominal set with singleton support

Equations

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

@[reducible, inline]

abbrev CatCrypt.Deep.Location.atom (ℓ : Location) : Nominal.Atom

The atom of a location

Equations

• ℓ.atom = ℓ.name

@[simp]

theorem CatCrypt.Deep.Location.supp_eq (ℓ : Location) : Nominal.NomSet.supp ℓ = {ℓ.name}

The support of a location is its atom

def CatCrypt.Deep.Location.disj (ℓ₁ : Location) (ℓ₂ : Location) : Prop

Two locations are disjoint if they have different atoms

Equations

• ℓ₁.disj ℓ₂ = (ℓ₁.name ≠ ℓ₂.name)

theorem CatCrypt.Deep.Location.disj_comm (ℓ₁ : Location) (ℓ₂ : Location) : ℓ₁.disj ℓ₂ ↔ ℓ₂.disj ℓ₁

theorem CatCrypt.Deep.Location.disj_of_ne_name {ℓ₁ : Location} {ℓ₂ : Location} (h : ℓ₁.name ≠ ℓ₂.name) : ℓ₁.disj ℓ₂

@[reducible, inline]

abbrev CatCrypt.Deep.LocAtomSet : Type

A finite set of locations

Equations

• CatCrypt.Deep.LocAtomSet = Finset CatCrypt.Nominal.Atom

def CatCrypt.Deep.locsToAtoms (locs : List Location) : LocAtomSet

Get the atoms from a finite set of locations. Note: We can't use Finset Location directly since Location contains types, so we work with atoms and store locations in a separate structure.

Equations

• CatCrypt.Deep.locsToAtoms locs = List.foldl (fun (s : CatCrypt.Deep.LocAtomSet) (ℓ : CatCrypt.Deep.Location) => s ∪ {ℓ.name}) ∅ locs

structure CatCrypt.Deep.DeepHeap : Type 1

A heap is a mapping from locations to optional values. Each location can either be uninitialized (None) or contain a value of the appropriate type.

• data (ℓ : Location) : Option ℓ.ty

  The underlying data: for each location, an optional value of the right type

def CatCrypt.Deep.DeepHeap.empty : DeepHeap

The empty heap where all locations are uninitialized

Equations

• CatCrypt.Deep.DeepHeap.empty = { data := fun (x : CatCrypt.Deep.Location) => none }

def CatCrypt.Deep.DeepHeap.get (h : DeepHeap) (ℓ : Location) : Option ℓ.ty

Get the value at a location

Equations

• h.get ℓ = h.data ℓ

noncomputable def CatCrypt.Deep.DeepHeap.set (h : DeepHeap) (ℓ : Location) (v : ℓ.ty) : DeepHeap

Set the value at a location.

This updates the heap so that location ℓ contains value v. For any other location ℓ', the value is unchanged.

Two locations are considered the same iff both name AND type match. If ℓ' has the same name but different type, it is a different location and is not affected by this update.

This is noncomputable because we use classical decidability for type equality.

Equations

• h.set ℓ v = { data := fun (ℓ' : CatCrypt.Deep.Location) => if _hName : ℓ'.name = ℓ.name then if hTy : ℓ'.ty = ℓ.ty then some (cast ⋯ v) else h.data ℓ' else h.data ℓ' }

@[simp]

theorem CatCrypt.Deep.DeepHeap.get_empty (ℓ : Location) : empty.get ℓ = none

Getting from the empty heap returns None

theorem CatCrypt.Deep.DeepHeap.get_set_same (h : DeepHeap) (ℓ : Location) (v : ℓ.ty) : (h.set ℓ v).get ℓ = some v

Getting from a heap after setting the same location returns the value

theorem CatCrypt.Deep.DeepHeap.get_set_other (h : DeepHeap) (ℓ₁ ℓ₂ : Location) (v : ℓ₁.ty) (hne : ℓ₁ ≠ ℓ₂) : (h.set ℓ₁ v).get ℓ₂ = h.get ℓ₂

Getting from a heap after setting a different location returns the original value. Note: This now requires that the locations are different (either by name or by type).

theorem CatCrypt.Deep.DeepHeap.get_set_other_name (h : DeepHeap) (ℓ₁ ℓ₂ : Location) (v : ℓ₁.ty) (hne : ℓ₁.name ≠ ℓ₂.name) : (h.set ℓ₁ v).get ℓ₂ = h.get ℓ₂

Getting from a heap after setting a location with different name returns the original value. This is a convenience lemma when we know the names differ.

theorem CatCrypt.Deep.DeepHeap.ext {h₁ h₂ : DeepHeap} (hext : ∀ (ℓ : Location), h₁.get ℓ = h₂.get ℓ) : h₁ = h₂

Extensionality for heaps: heaps are equal if they agree on all locations

theorem CatCrypt.Deep.DeepHeap.ext_iff {h₁ h₂ : DeepHeap} : h₁ = h₂ ↔ ∀ (ℓ : Location), h₁.get ℓ = h₂.get ℓ

theorem CatCrypt.Deep.DeepHeap.set_set_same (h : DeepHeap) (ℓ : Location) (v₁ v₂ : ℓ.ty) : (h.set ℓ v₁).set ℓ v₂ = h.set ℓ v₂

Setting the same location twice keeps only the last value

theorem CatCrypt.Deep.DeepHeap.set_set_comm (h : DeepHeap) (ℓ₁ ℓ₂ : Location) (v₁ : ℓ₁.ty) (v₂ : ℓ₂.ty) (hne : ℓ₁ ≠ ℓ₂) : (h.set ℓ₁ v₁).set ℓ₂ v₂ = (h.set ℓ₂ v₂).set ℓ₁ v₁

Setting different locations commutes. Note: Now requires that the locations are different (either by name or type).

theorem CatCrypt.Deep.DeepHeap.set_set_comm_name (h : DeepHeap) (ℓ₁ ℓ₂ : Location) (v₁ : ℓ₁.ty) (v₂ : ℓ₂.ty) (hne : ℓ₁.name ≠ ℓ₂.name) : (h.set ℓ₁ v₁).set ℓ₂ v₂ = (h.set ℓ₂ v₂).set ℓ₁ v₁

Setting different locations (by name) commutes. This is a convenience lemma when we know the names differ.