Enhanced Location Tracking

This file defines a structured collection of memory locations for package validity tracking. Locations are tracked as a finite set with type information.

Main definitions

• Locations - A finite collection of typed memory locations
• Locations.empty - Empty location set
• Locations.Separate - Two location sets with disjoint ids
• Locations.mem - Location membership

References

• Larsen and Schürmann, Nominal State-Separating Proofs

structure CatCrypt.Package.Locations : Type 1

Locations: a finite set of location ids with their type information. We track locations by their ids since type information is bundled in Location.

• ids : Finset ℕ

  The set of location identifiers

• toLocation (id : ℕ) : id ∈ self.ids → Core.Location

  Function mapping ids to their locations (partial)

• id_consistent (id : ℕ) (h : id ∈ self.ids) : (self.toLocation id h).id = id

  Locations have consistent ids

def CatCrypt.Package.Locations.empty : Locations

Empty location set

Equations

• CatCrypt.Package.Locations.empty = { ids := ∅, toLocation := fun (x : ℕ) (h : x ∈ ∅) => ⋯.elim, id_consistent := CatCrypt.Package.Locations.empty._proof_1 }

@[implicit_reducible]

instance CatCrypt.Package.Locations.instEmptyCollection : EmptyCollection Locations

Equations

• CatCrypt.Package.Locations.instEmptyCollection = { emptyCollection := CatCrypt.Package.Locations.empty }

@[implicit_reducible]

instance CatCrypt.Package.Locations.instMembershipLocation : Membership Core.Location Locations

A location is in the set if its id is in the id set

Equations

• CatCrypt.Package.Locations.instMembershipLocation = { mem := fun (L : CatCrypt.Package.Locations) (l : CatCrypt.Core.Location) => l.id ∈ L.ids }

theorem CatCrypt.Package.Locations.mem_iff (L : Locations) (l : Core.Location) : l ∈ L ↔ l.id ∈ L.ids

def CatCrypt.Package.Locations.singleton (l : Core.Location) : Locations

Singleton location set

Equations

• CatCrypt.Package.Locations.singleton l = { ids := {l.id}, toLocation := fun (id : ℕ) (x : id ∈ {l.id}) => l, id_consistent := ⋯ }

@[implicit_reducible]

instance CatCrypt.Package.Locations.instSingletonLocation : Singleton Core.Location Locations

Equations

• CatCrypt.Package.Locations.instSingletonLocation = { singleton := CatCrypt.Package.Locations.singleton }

theorem CatCrypt.Package.Locations.mem_singleton (l l' : Core.Location) : l' ∈ {l} ↔ l'.id = l.id

def CatCrypt.Package.Locations.Separate (L₁ L₂ : Locations) : Prop

Two location sets are separate (disjoint ids)

Equations

• L₁.Separate L₂ = Disjoint L₁.ids L₂.ids

theorem CatCrypt.Package.Locations.separate_symm {L₁ L₂ : Locations} (h : L₁.Separate L₂) : L₂.Separate L₁

theorem CatCrypt.Package.Locations.separate_empty_left (L : Locations) : empty.Separate L

theorem CatCrypt.Package.Locations.separate_empty_right (L : Locations) : L.Separate empty

noncomputable def CatCrypt.Package.Locations.union (L₁ L₂ : Locations) (h : L₁.Separate L₂) : Locations

Union of location sets (partial - should only be used with disjoint locations for well-definedness of the location mapping)

Equations

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

theorem CatCrypt.Package.Locations.union_ids {L₁ L₂ : Locations} (h : L₁.Separate L₂) : (L₁.union L₂ h).ids = L₁.ids ∪ L₂.ids

theorem CatCrypt.Package.Locations.mem_union_left {L₁ L₂ : Locations} (h : L₁.Separate L₂) (l : Core.Location) : l ∈ L₁ → l ∈ L₁.union L₂ h

theorem CatCrypt.Package.Locations.mem_union_right {L₁ L₂ : Locations} (h : L₁.Separate L₂) (l : Core.Location) : l ∈ L₂ → l ∈ L₁.union L₂ h

def CatCrypt.Package.Locations.Subset (L₁ L₂ : Locations) : Prop

Subset relation on locations

Equations

• L₁.Subset L₂ = (L₁.ids ⊆ L₂.ids)

@[implicit_reducible]

instance CatCrypt.Package.Locations.instHasSubset : HasSubset Locations

Equations

• CatCrypt.Package.Locations.instHasSubset = { Subset := CatCrypt.Package.Locations.Subset }

theorem CatCrypt.Package.Locations.empty_subset (L : Locations) : ∅ ⊆ L

def CatCrypt.Package.Locations.diff (L₁ L₂ : Locations) : Locations

Difference of location sets

Equations

• L₁.diff L₂ = { ids := L₁.ids \ L₂.ids, toLocation := fun (id : ℕ) (hid : id ∈ L₁.ids \ L₂.ids) => have h := ⋯; L₁.toLocation id h, id_consistent := ⋯ }

theorem CatCrypt.Package.Locations.diff_ids (L₁ L₂ : Locations) : (L₁.diff L₂).ids = L₁.ids \ L₂.ids

def CatCrypt.Package.Locations.card (L : Locations) : ℕ

Card of a location set

Equations

• L.card = L.ids.card

theorem CatCrypt.Package.Locations.empty_card : ∅.card = 0

theorem CatCrypt.Package.Locations.singleton_card (l : Core.Location) : {l}.card = 1