Countable-Typed Heap Locations

CatCrypt.Core.Location requires Fintype ty, so a heap cell can only hold a value of a finite type. GLocation requires only Countable ty and Inhabited ty, which admits cells holding Nat, List α, association lists, and other unbounded values.

Both flavours read and write the same carrier, CatCrypt.Core.Heap — a partial finite map from location ids to natural numbers. Only the value codec differs: Heap.get/Heap.set code through Fintype.equivFin, while Heap.gget/Heap.gset code through gencode, a chosen injection ty ↪ Nat. Since gencode uses Fintype.equivFin whenever the value type happens to be finite, the two codecs agree on finite types, and gget/gset restrict to get/set along GLocation.ofLocation (gget_ofLocation, gset_ofLocation).

SPComp α is Heap → SDistr (α × Heap), so it needs no adjustment: rHoare, DependsOn and PreservesOutside apply directly to computations built from SPComp.gget/SPComp.gset. This file supplies the footprint lemmas for those operations.

Main definitions

• gencode, gdecode — codec for a countable inhabited type
• GLocation — heap location with a countable value type
• Heap.gget, Heap.gset — heap access at a GLocation
• SPComp.gget, SPComp.gset — the corresponding stateful operations
• CatCrypt.Relational.gLeftHas, gRightHas — one-sided pRHL assertions

Codec for a countable type

noncomputable def CatCrypt.Core.gencode (α : Type) [Countable α] : α → ℕ

Injection of a countable type into Nat. On a finite type it is Fintype.equivFin followed by Fin.val; otherwise it is a chosen injection.

Equations

• CatCrypt.Core.gencode α = if h : Nonempty (Fintype α) then fun (a : α) => ↑((Fintype.equivFin α) a) else ⋯.choose

theorem CatCrypt.Core.gencode_injective (α : Type) [Countable α] : Function.Injective (gencode α)

theorem CatCrypt.Core.gencode_eq_encode {α : Type} [inst : Fintype α] : gencode α = Heap.encode

On a finite type, gencode is Heap.encode.

noncomputable def CatCrypt.Core.gdecode (α : Type) [Countable α] [Inhabited α] (n : ℕ) : α

Partial inverse of gencode, returning default off its image.

Equations

• CatCrypt.Core.gdecode α n = if h : ∃ (a : α), CatCrypt.Core.gencode α a = n then h.choose else default

theorem CatCrypt.Core.gdecode_gencode {α : Type} [Countable α] [Inhabited α] (a : α) : gdecode α (gencode α a) = a

theorem CatCrypt.Core.gdecode_eq_decode {α : Type} [Fintype α] [Inhabited α] : gdecode α = Heap.decode α

On a finite type, gdecode is Heap.decode.

Locations with a countable value type

structure CatCrypt.Core.GLocation : Type 1

Heap location whose value type is countable and inhabited. The value type is fixed at Type (universe 0), matching Location.

• id : ℕ

  Location identifier.

• ty : Type

  Type of the value stored at this location.

• countable : Countable self.ty
• inhabited : Inhabited self.ty

@[instance_reducible]

noncomputable instance CatCrypt.Core.GLocation.instDecidableEq : DecidableEq GLocation

Equations

• CatCrypt.Core.GLocation.instDecidableEq = Classical.decEq CatCrypt.Core.GLocation

def CatCrypt.Core.GLocation.ofLocation (l : Location) : GLocation

A Location is a GLocation: a finite type is countable.

Equations

• CatCrypt.Core.GLocation.ofLocation l = { id := l.id, ty := l.ty, countable := ⋯, inhabited := l.inhabited }

@[simp]

theorem CatCrypt.Core.GLocation.ofLocation_id (l : Location) : (ofLocation l).id = l.id

@[simp]

theorem CatCrypt.Core.GLocation.ofLocation_ty (l : Location) : (ofLocation l).ty = l.ty

Heap access at a GLocation

noncomputable def CatCrypt.Core.Heap.gget (h : Heap) (l : GLocation) : l.ty

Read a countable-typed location. Returns default if never written.

Equations

• h.gget l = match Finmap.lookup l.id h.data with | some n => CatCrypt.Core.gdecode l.ty n | none => default

noncomputable def CatCrypt.Core.Heap.gset (h : Heap) (l : GLocation) (v : l.ty) : Heap

Write a countable-typed location.

Equations

• h.gset l v = { data := Finmap.insert l.id (CatCrypt.Core.gencode l.ty v) h.data }

@[simp]

theorem CatCrypt.Core.Heap.gget_gset_same (h : Heap) (l : GLocation) (v : l.ty) : (h.gset l v).gget l = v

@[simp]

theorem CatCrypt.Core.Heap.gget_gset_other (h : Heap) (l l' : GLocation) (v : l.ty) (hne : l.id ≠ l'.id) : (h.gset l v).gget l' = h.gget l'

@[simp]

theorem CatCrypt.Core.Heap.gset_gset_same (h : Heap) (l : GLocation) (v₁ v₂ : l.ty) : (h.gset l v₁).gset l v₂ = h.gset l v₂

theorem CatCrypt.Core.Heap.gset_gset_comm (h : Heap) (l₁ l₂ : GLocation) (v₁ : l₁.ty) (v₂ : l₂.ty) (hne : l₁.id ≠ l₂.id) : (h.gset l₁ v₁).gset l₂ v₂ = (h.gset l₂ v₂).gset l₁ v₁

@[simp]

theorem CatCrypt.Core.Heap.gget_empty (l : GLocation) : empty.gget l = default

@[simp]

theorem CatCrypt.Core.Heap.gset_lookup_same (h : Heap) (l : GLocation) (v : l.ty) : Finmap.lookup l.id (h.gset l v).data = some (gencode l.ty v)

theorem CatCrypt.Core.Heap.gset_lookup_of_ne (h : Heap) (l : GLocation) (v : l.ty) {i : ℕ} (hne : i ≠ l.id) : Finmap.lookup i (h.gset l v).data = Finmap.lookup i h.data

theorem CatCrypt.Core.Heap.gget_congr_of_agreeOn {h₁ h₂ : Heap} {locs : LocSet} (hag : h₁.agreeOn h₂ locs) {l : GLocation} (hmem : l.id ∈ locs) : h₁.gget l = h₂.gget l

Two heaps agreeing on a location's id agree on its contents.

Compatibility of the two flavours

The countable codec extends the finite one, so a Location read or written through the generalized interface behaves exactly as it does through Heap.get/Heap.set.

@[simp]

theorem CatCrypt.Core.Heap.gget_ofLocation (h : Heap) (l : Location) : h.gget (GLocation.ofLocation l) = h.get l

@[simp]

theorem CatCrypt.Core.Heap.gset_ofLocation (h : Heap) (l : Location) (v : l.ty) : h.gset (GLocation.ofLocation l) v = h.set l v

theorem CatCrypt.Core.Heap.gget_set_other (h : Heap) (l : Location) (l' : GLocation) (v : l.ty) (hne : l.id ≠ l'.id) : (h.set l v).gget l' = h.gget l'

A finite-typed write does not disturb a countable-typed read at a different id.

theorem CatCrypt.Core.Heap.get_gset_other (h : Heap) (l : GLocation) (l' : Location) (v : l.ty) (hne : l.id ≠ l'.id) : (h.gset l v).get l' = h.get l'

A countable-typed write does not disturb a finite-typed read at a different id.

Stateful operations

noncomputable def CatCrypt.Core.SPComp.gget (l : GLocation) : SPComp l.ty

Read a countable-typed location.

Equations

• CatCrypt.Core.SPComp.gget l h = CatCrypt.Prob.SDistr.pure (h.gget l, h)

noncomputable def CatCrypt.Core.SPComp.gset (l : GLocation) (v : l.ty) : SPComp Unit

Write a countable-typed location.

Equations

• CatCrypt.Core.SPComp.gset l v h = CatCrypt.Prob.SDistr.pure ((), h.gset l v)

theorem CatCrypt.Core.SPComp.gget_def (l : GLocation) (h : Heap) : gget l h = Prob.SDistr.pure (h.gget l, h)

theorem CatCrypt.Core.SPComp.gset_def (l : GLocation) (v : l.ty) (h : Heap) : gset l v h = Prob.SDistr.pure ((), h.gset l v)

theorem CatCrypt.Core.SPComp.gget_ofLocation (l : Location) : gget (GLocation.ofLocation l) = get l

The generalized operations restrict to the finite-typed ones.

theorem CatCrypt.Core.SPComp.gset_ofLocation (l : Location) (v : l.ty) : gset (GLocation.ofLocation l) v = set l v

Framing

def CatCrypt.Relational.gLeftHas (l : Core.GLocation) (v : l.ty) : RPre

The left heap stores v at a countable-typed location.

Equations

• CatCrypt.Relational.gLeftHas l v h₁ x✝ = (h₁.gget l = v)

def CatCrypt.Relational.gRightHas (l : Core.GLocation) (v : l.ty) : RPre

The right heap stores v at a countable-typed location.

Equations

• CatCrypt.Relational.gRightHas l v x✝ h₂ = (h₂.gget l = v)

theorem CatCrypt.Relational.dependsOn_gLeftHas (l : Core.GLocation) (v : l.ty) : DependsOn (gLeftHas l v) {l.id}

theorem CatCrypt.Relational.dependsOn_gRightHas (l : Core.GLocation) (v : l.ty) : DependsOn (gRightHas l v) {l.id}

theorem CatCrypt.Relational.preservesOutside_gget (l : Core.GLocation) : PreservesOutside (Core.SPComp.gget l) ∅

theorem CatCrypt.Relational.preservesOutside_gset (l : Core.GLocation) (v : l.ty) : PreservesOutside (Core.SPComp.gset l v) {l.id}

Non-vacuity

Nat is a legal GLocation value type and is not a legal Location value type.

@[reducible]

def CatCrypt.Core.natCounter (id : ℕ) : GLocation

An unbounded counter cell.

Equations

• CatCrypt.Core.natCounter id = { id := id, ty := ℕ, countable := instCountableNat, inhabited := instInhabitedNat }

theorem CatCrypt.Core.nat_no_fintype : ¬Nonempty (Fintype ℕ)

Nat carries no Fintype instance, so natCounter's value type is outside the range of Location.

noncomputable def CatCrypt.Core.incr (id : ℕ) : SPComp ℕ

Incrementing a counter held in the heap.

Equations

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

theorem CatCrypt.Core.incr_twice_empty (id : ℕ) : (incr id).bind (fun (x : ℕ) => incr id) Heap.empty = Prob.SDistr.pure (2, Heap.empty.gset (natCounter id) 2)

incr run twice from the empty heap yields 2 and stores 2.