Heap Model

This file defines the heap model for stateful computations.

Design

Following the Rocq SSProve design, values are stored using their Fintype encoding as natural numbers in a partial finite map (Finmap) from location ids to encoded values. Unaccessed locations map to none; get returns default for such locations.

This is the Lean 4 analogue of Rocq SSProve's {fmap nat → nat}.

Key Properties

• get_set_same: Getting after setting returns the stored value
• get_set_other: Setting at one location doesn't affect other locations
• set_set_same: Double write contracts to a single write
• set_set_comm: Writes to different locations commute

structure CatCrypt.Core.Heap : Type

Heap: partial finite map from location ids to encoded values. Values are encoded using their Fintype encoding as natural numbers. Unaccessed locations are absent from the map; get returns default for absent locations.

• data : Finmap fun (x : ℕ) => ℕ

  Partial map from location id to encoded value (natural number)

@[instance_reducible]

instance CatCrypt.Core.instInhabitedHeap : Inhabited Heap

Equations

• CatCrypt.Core.instInhabitedHeap = { default := CatCrypt.Core.instInhabitedHeap.default }

theorem CatCrypt.Core.Heap.ext {h₁ h₂ : Heap} (hdata : h₁.data = h₂.data) : h₁ = h₂

Extensionality for heaps

theorem CatCrypt.Core.Heap.ext_iff {h₁ h₂ : Heap} : h₁ = h₂ ↔ h₁.data = h₂.data

theorem CatCrypt.Core.Heap.ext_lookup {h₁ h₂ : Heap} (hlookup : ∀ (id : ℕ), Finmap.lookup id h₁.data = Finmap.lookup id h₂.data) : h₁ = h₂

Extensionality for heaps via lookup

def CatCrypt.Core.Heap.empty : Heap

Empty heap: no locations are initialized

Equations

• CatCrypt.Core.Heap.empty = { data := ∅ }

noncomputable def CatCrypt.Core.Heap.encode {α : Type} [Fintype α] (v : α) : ℕ

Encode a value using its Fintype equivalence

Equations

• CatCrypt.Core.Heap.encode v = ↑((Fintype.equivFin α) v)

noncomputable def CatCrypt.Core.Heap.decode (α : Type) [Fintype α] [Inhabited α] (n : ℕ) : α

Decode a natural number to a value. If the number is out of range, returns default.

Equations

• CatCrypt.Core.Heap.decode α n = if h : n < Fintype.card α then (Fintype.equivFin α).symm ⟨n, h⟩ else default

theorem CatCrypt.Core.Heap.decode_encode {α : Type} [Fintype α] [Inhabited α] (v : α) : decode α (encode v) = v

Encoding then decoding returns the original value

noncomputable def CatCrypt.Core.Heap.get (h : Heap) (l : Location) : l.ty

Get a value from the heap at a location. Returns default if the location has never been written.

Equations

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

noncomputable def CatCrypt.Core.Heap.set (h : Heap) (l : Location) (v : l.ty) : Heap

Set a value in the heap at a location

Equations

• h.set l v = { data := Finmap.insert l.id (CatCrypt.Core.Heap.encode v) h.data }

def CatCrypt.Core.Heap.agreeOn (h1 h2 : Heap) (locs : LocSet) : Prop

Two heaps agree on a set of location ids

Equations

• h1.agreeOn h2 locs = ∀ id ∈ locs, Finmap.lookup id h1.data = Finmap.lookup id h2.data

@[instance_reducible]

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

Heap equality is not decidable in general, but we can use classical logic

Equations

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

@[simp]

theorem CatCrypt.Core.Heap.get_set_same (h : Heap) (l : Location) (v : l.ty) : (h.set l v).get l = v

Getting after setting the same location returns the stored value

@[simp]

theorem CatCrypt.Core.Heap.get_set_other (h : Heap) (l l' : Location) (v : l.ty) (hne : l.id ≠ l'.id) : (h.set l v).get l' = h.get l'

Setting at one location doesn't affect getting from another location

@[simp]

theorem CatCrypt.Core.Heap.set_set_same (h : Heap) (l : Location) (v₁ v₂ : l.ty) : (h.set l v₁).set l v₂ = h.set l v₂

Setting the same location twice: the second write wins

theorem CatCrypt.Core.Heap.set_set_comm (h : Heap) (l₁ l₂ : Location) (v₁ : l₁.ty) (v₂ : l₂.ty) (hne : l₁.id ≠ l₂.id) : (h.set l₁ v₁).set l₂ v₂ = (h.set l₂ v₂).set l₁ v₁

Setting different locations commutes

@[simp]

theorem CatCrypt.Core.Heap.get_empty (l : Location) : empty.get l = default

Looking up a location in the empty heap returns none