Finite-footprint memory assertions

Assertions record a finite footprint and depend only on its cells. Separating conjunction requires disjoint footprints. This is an assertion and frame calculus over the RAM's total memory, not a new allocator or a claim that inaccessible cells cease to exist.

Main definitions

• HeapAssertion: a memory predicate supported on a finite footprint.
• HeapAssertion.sep, HeapAssertion.pointsto, HeapAssertion.array: representation primitives.
• Modifies: equality outside a permitted set of writes.

Main results

• HeapAssertion.frame: writes to a disjoint region preserve an assertion.
• HeapAssertion.sep_comm: separating conjunction is commutative at the predicate level.

References

The footprint/frame principle is the standard locality principle of separation logic; this file uses explicit finite supports rather than partial-heap semantics. See J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures.

def Cslib.WordRAM.Block.footprint (b : Block) : Finset ℕ

The finite set of memory cells owned by the block.

@[simp]

theorem Cslib.WordRAM.Block.mem_footprint {b : Block} {a : ℕ} : a ∈ b.footprint ↔ b.Owns a

@[simp]

theorem Cslib.WordRAM.Block.card_footprint (b : Block) : b.footprint.card = b.length

structure Cslib.WordRAM.HeapAssertion : Type

A predicate depending only on a finite set of memory cells.

• footprint : Finset ℕ

  Cells on which the predicate may depend.

• holds : (ℕ → ℕ) → Prop

  The asserted property of total RAM memory.

• supported {m m' : ℕ → ℕ} : (∀ a ∈ self.footprint, m a = m' a) → self.holds m → self.holds m'

  Agreement on owned cells transports the assertion.

def Cslib.WordRAM.Modifies (writes : Finset ℕ) (m m' : ℕ → ℕ) : Prop

The two memories agree outside the permitted write footprint.

theorem Cslib.WordRAM.Modifies.refl (F : Finset ℕ) (m : ℕ → ℕ) : Modifies F m m

An unchanged memory modifies no cells.

theorem Cslib.WordRAM.Modifies.trans {F G : Finset ℕ} {m m' m'' : ℕ → ℕ} (h : Modifies F m m') (h' : Modifies G m' m'') : Modifies (F ∪ G) m m''

Sequential writes use the union of the permitted regions.

theorem Cslib.WordRAM.Modifies.update (m : ℕ → ℕ) (a v : ℕ) : Modifies {a} m (Function.update m a v)

A single write modifies at most its destination.

theorem Cslib.WordRAM.Modifies.write_of_owns {base n a : ℕ} {m : ℕ → ℕ} (ha : base ≤ a ∧ a < base + n) (v : ℕ) : Modifies { base := base, length := n }.footprint m (Function.update m a v)

Writing a cell owned by a block modifies at most the block's footprint.

theorem Cslib.WordRAM.Modifies.block_iff {b : Block} {m m' : ℕ → ℕ} : Modifies b.footprint m m' ↔ ∀ (a : ℕ), a < b.base ∨ b.base + b.length ≤ a → m' a = m a

Modifying at most a block's footprint is equivalent to preserving all cells outside its address interval.

def Cslib.WordRAM.HeapAssertion.pure (P : Prop) : HeapAssertion

A memory-free assertion.

def Cslib.WordRAM.HeapAssertion.pointsto (a v : ℕ) : HeapAssertion

A single owned cell with specified contents.

def Cslib.WordRAM.HeapAssertion.array (base n : ℕ) (values : Fin n → ℕ) : HeapAssertion

A record, or array, of consecutive owned cells.

def Cslib.WordRAM.HeapAssertion.sep (P Q : HeapAssertion) : HeapAssertion

Conjunction of assertions with disjoint ownership.

theorem Cslib.WordRAM.HeapAssertion.sep_comm (P Q : HeapAssertion) (m : ℕ → ℕ) : (P.sep Q).holds m ↔ (Q.sep P).holds m

Separating conjunction can be reordered.

theorem Cslib.WordRAM.HeapAssertion.frame {P : HeapAssertion} {F : Finset ℕ} {m m' : ℕ → ℕ} (hP : P.holds m) (hF : Disjoint P.footprint F) (hm : Modifies F m m') : P.holds m'

A disjoint write preserves every assertion supported on the framed region.

theorem Cslib.WordRAM.HeapAssertion.frame_update {P : HeapAssertion} {m : ℕ → ℕ} (hP : P.holds m) {a : ℕ} (ha : a ∉ P.footprint) (v : ℕ) : P.holds (Function.update m a v)

Updating an unowned cell preserves an assertion.

theorem Cslib.WordRAM.HeapAssertion.pointsto_update (m : ℕ → ℕ) (a v : ℕ) : (pointsto a v).holds (Function.update m a v)

A point assertion is updated by the corresponding store.