Footprints, room, and products of data structures sharing one memory

A Memory.Framed D w is a refinement of D over Memory.spec w together with a footprint, the finite set of allocated cells that holds the representation of each memory state, and a room, the number of cells the structure has reserved for its future allocations. Three obligations make them honest.

• congr: the invariant, the abstraction, the footprint and the room read only the footprint's cells, and survive a growing frontier that leaves the reserved room fitting a word.
• modifies: a method run changes no allocated cell outside the footprint, the footprint grows only into cells that the run allocated, and the frontier advances by at most the room the run gives up.
• lt_frontier: the footprint is allocated.

A structure laid out in fixed blocks has a constant footprint and no room, and Framed.ofStatic asks for less. A structure that allocates inside its operations, such as a growing array, reserves room for all of its future growth. Its invariant may then ask that the frontier plus its room fit a word, which is what Memory.valid needs of each allocation. That fact is not preserved by other structures' allocations on its own, so the product keeps it for everybody.

Products. Two framed refinements implement the product of their specifications over one shared memory (Framed.prod). The product's invariant asks that the footprints be disjoint and that the frontier plus both rooms fit a word. This is the shared room budget: a method run of one side writes only its own cells and fresh ones, and advances the frontier by at most the room it gives up, so the other side keeps its cells and its room, and the budget still fits. The product is framed again, with the union of the footprints and the sum of the rooms, so products iterate: (M₁.prod M₂).prod M₃ implements three structures in one memory. A potential that reads only the footprint (Framed.Local) is left unchanged by the other side's methods, so amortized certificates add across the product (Framed.amortized_prod), and so do worst-case Module.ChargeBounds, as the case of zero potentials.

Composition. A refinement of D over E composed with a framed refinement of E is framed by the same footprint and room (Framed.comp), since a whole linked client keeps the frame of its calls (Framed.modifies_demonic). So a structure built on others, such as a queue over two stacks, joins a product like any other.

Allocation is a memory program like any other. A run that leaves every allocated cell unchanged and leaves the room fitting, such as the allocation of a further structure, preserves a framed refinement (Framed.of_fresh), and Framed.prod_of_fresh sets up a product from structures allocated one after the other. Memory.Allocator packages this.

Main definitions

• Memory.Framed: a refinement over memory with a footprint and a room.
• Memory.Framed.ofStatic: the constructor for a constant footprint and no room.
• Memory.Framed.Local: a function of memory that reads only the footprint.
• Memory.Framed.prod: two framed refinements with disjoint footprints implement the product.
• Memory.Framed.comp: a refinement over a framed refinement is framed.

Main results

• Memory.frontier_le_of_clientRun, Memory.frontier_le_clientState: a run never lowers the frontier.
• Memory.mem_run_of_lt_frontier, Memory.mem_clientState_of_lt_frontier: a run changes an allocated cell only by writing it.
• Memory.mem_run_of_frontier_le, Memory.mem_clientState_of_frontier_le: an admissible run changes no cell at or above its final frontier.
• Memory.Framed.modifies_demonic: a linked client keeps the frame of its calls.
• Memory.Framed.frame: a method run of one structure leaves a structure with a disjoint footprint unchanged, and the shared room budget fitting.
• Memory.Framed.prod_methods: the product's methods are the two sides' methods.
• Memory.Framed.amortized_prod: potentials and charges add across the product.
• Memory.Framed.of_fresh, Memory.Framed.prod_of_fresh: allocation preserves structures and sets up products.

References

The footprint and frame discipline is the locality principle of separation logic, here with explicit finite footprints as in Cslib.WordRAM.HeapAssertion; see J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures.

Runs and allocated cells

theorem Cslib.DataStructure.Memory.frontier_le_of_clientRun {w : ℕ} {α : Type} {s s' : State} {p : Prog α} {a : α} {tr : (spec w).Transcript} (h : (spec w).ClientRun s p a s' tr) : s.frontier ≤ s'.frontier

No run of a memory program lowers the frontier.

theorem Cslib.DataStructure.Memory.frontier_le_clientState {w : ℕ} {α : Type} (s : State) (p : Prog α) : s.frontier ≤ ((spec w).clientState s p).frontier

No memory program lowers the frontier.

theorem Cslib.DataStructure.Memory.mem_run_of_lt_frontier {w : ℕ} (s : State) (os : List Op) {a : ℕ} (ha : a < s.frontier) (hw : ∀ (v : ℕ), Op.write a v ∉ os) : ((spec w).run s os).1.mem a = s.mem a

A sequence of operations changes an allocated cell only by writing it.

theorem Cslib.DataStructure.Memory.mem_clientState_of_lt_frontier {w : ℕ} {α : Type} (s : State) (p : Prog α) {a : ℕ} (ha : a < s.frontier) (hw : ∀ (v : ℕ), Op.write a v ∉ (spec w).clientHistory s p) : ((spec w).clientState s p).mem a = s.mem a

A memory program changes an allocated cell only by writing it.

theorem Cslib.DataStructure.Memory.mem_run_of_frontier_le {w : ℕ} {s : State} {os : List Op} (hv : (spec w).ValidHistory s os) {a : ℕ} (ha : ((spec w).run s os).1.frontier ≤ a) : ((spec w).run s os).1.mem a = s.mem a

An admissible sequence of operations changes no cell at or above its final frontier: writes go below the frontier, and an allocation clears only the block that it hands out.

theorem Cslib.DataStructure.Memory.mem_clientState_of_frontier_le {w : ℕ} {α : Type} (s : State) (p : Prog α) (hv : (spec w).ValidHistory s ((spec w).clientHistory s p)) {a : ℕ} (ha : ((spec w).clientState s p).frontier ≤ a) : ((spec w).clientState s p).mem a = s.mem a

An admissible memory program changes no cell at or above its final frontier.

Framed refinements

structure Cslib.DataStructure.Memory.Framed (D : StateTransitionSpec) (w : ℕ) extends Cslib.DataStructure.Refinement D (Cslib.DataStructure.Memory.spec w) : Type

A refinement of D over memory whose representation lives in a footprint of allocated cells, with room reserved for its growth. The invariant, the abstraction, the footprint and the room read only the footprint's cells; a method run changes no allocated cell outside the footprint; the footprint grows only into cells at or above the old frontier, which the run allocated; and the frontier advances by at most the room the run gives up.

• methods : Methods D (Memory.spec w)
• inv : (Memory.spec w).State → Prop
• abs : (Memory.spec w).State → D.State
• valid {e : (Memory.spec w).State} (o : D.Op) : self.inv e → D.valid (self.abs e) o → (Memory.spec w).DemonicValid e (self.methods o)
• correct {e : (Memory.spec w).State} (o : D.Op) {a : D.Result o} {e' : (Memory.spec w).State} {tr : (Memory.spec w).Transcript} : self.inv e → D.valid (self.abs e) o → (Memory.spec w).ClientRun e (self.methods o) a e' tr → D.step (self.abs e) o (self.abs e') a ∧ self.inv e'
• footprint : State → Finset ℕ

  The cells holding the representation.

• room : State → ℕ

  The cells reserved for the structure's future allocations.

• lt_frontier {s : (spec w).State} {a : ℕ} : self.inv s → a ∈ self.footprint s → a < s.frontier

  The footprint is allocated.

• congr {s s' : (spec w).State} : self.inv s → (∀ a ∈ self.footprint s, s'.mem a = s.mem a) → s.frontier ≤ s'.frontier → WordRAM.Fits w (s'.frontier + self.room s) → self.inv s' ∧ self.abs s' = self.abs s ∧ self.footprint s' = self.footprint s ∧ self.room s' = self.room s

  The invariant, the abstraction, the footprint and the room read only the footprint's cells, and survive a growing frontier that leaves the room fitting a word.

• modifies {s : (spec w).State} (o : D.Op) {a : D.Result o} {s' : (spec w).State} {tr : (spec w).Transcript} : self.inv s → D.valid (self.abs s) o → (spec w).ClientRun s (self.methods o) a s' tr → (∀ b < s.frontier, b ∉ self.footprint s → s'.mem b = s.mem b) ∧ (∀ b ∈ self.footprint s', b ∈ self.footprint s ∨ s.frontier ≤ b) ∧ s'.frontier + self.room s' ≤ s.frontier + self.room s

  A method run changes no allocated cell outside the footprint, the footprint grows only into fresh cells, and the frontier advances by at most the room given up.

def Cslib.DataStructure.Memory.Framed.ofStatic {w : ℕ} {D : StateTransitionSpec} (M : Refinement D (spec w)) (fp : Finset ℕ) (lt_frontier : ∀ {s : (spec w).State} {a : ℕ}, M.inv s → a ∈ fp → a < s.frontier) (congr : ∀ {s s' : (spec w).State}, M.inv s → (∀ a ∈ fp, s'.mem a = s.mem a) → s.frontier ≤ s'.frontier → M.inv s' ∧ M.abs s' = M.abs s) (modifies : ∀ {s : (spec w).State} (o : D.Op), M.inv s → D.valid (M.abs s) o → ∀ b < s.frontier, b ∉ fp → ((spec w).clientState s (M.methods o)).mem b = s.mem b) (frontier_eq : ∀ {s : (spec w).State} (o : D.Op), M.inv s → D.valid (M.abs s) o → ((spec w).clientState s (M.methods o)).frontier = s.frontier) : Framed D w

The constructor for a constant footprint fp and no room: the invariant and abstraction read only fp, and each method's final state agrees with its initial state on the allocated cells outside fp and has the same frontier.

def Cslib.DataStructure.Memory.Framed.Local {w : ℕ} {D : StateTransitionSpec} (M : Framed D w) {β : Type u_1} (f : State → β) : Prop

A function of memory reads only the footprint: it is unchanged when the footprint's cells are and the frontier grows, leaving the room fitting a word. The abstraction is one (Local.abs), and so is the room (Local.room); so are potentials that a product must keep apart.

theorem Cslib.DataStructure.Memory.Framed.Local.abs {w : ℕ} {D : StateTransitionSpec} (M : Framed D w) : M.Local M.abs

The abstraction reads only the footprint.

theorem Cslib.DataStructure.Memory.Framed.Local.room {w : ℕ} {D : StateTransitionSpec} (M : Framed D w) : M.Local M.room

The room reads only the footprint.

theorem Cslib.DataStructure.Memory.Framed.Local.const {w : ℕ} {D : StateTransitionSpec} (M : Framed D w) {β : Type u_1} (b : β) : M.Local fun (x : State) => b

A constant reads no cell.

theorem Cslib.DataStructure.Memory.Framed.Local.add {w : ℕ} {D : StateTransitionSpec} {M : Framed D w} {f g : State → ℕ} (hf : M.Local f) (hg : M.Local g) : M.Local fun (s : State) => f s + g s

Sums of local functions are local.

theorem Cslib.DataStructure.Memory.Framed.Local.comp_abs {w : ℕ} {D : StateTransitionSpec} (M : Framed D w) {β : Type u_1} (f : D.State → β) : M.Local fun (s : State) => f (M.abs s)

A function of the abstract state is local.

theorem Cslib.DataStructure.Memory.Framed.of_fresh {w : ℕ} {D : StateTransitionSpec} (M : Framed D w) {s s' : State} (hs : M.inv s) (hmem : ∀ a < s.frontier, s'.mem a = s.mem a) (hf : s.frontier ≤ s'.frontier) (hroom : WordRAM.Fits w (s'.frontier + M.room s)) : M.inv s' ∧ M.abs s' = M.abs s ∧ M.footprint s' = M.footprint s ∧ M.room s' = M.room s

A run that leaves every allocated cell unchanged and leaves the room fitting preserves a framed refinement. Allocating another structure is such a run.

theorem Cslib.DataStructure.Memory.Framed.modifies_demonic {w : ℕ} {D : StateTransitionSpec} (M : Framed D w) {α : Type} (p : D.Client α) {s s' : State} {a : α} {tr : (spec w).Transcript} (hs : M.inv s) (hv : D.DemonicValid (M.abs s) p) (hrun : (spec w).ClientRun s (link M.methods p) a s' tr) : (∀ b < s.frontier, b ∉ M.footprint s → s'.mem b = s.mem b) ∧ (∀ b ∈ M.footprint s', b ∈ M.footprint s ∨ s.frontier ≤ b) ∧ s'.frontier + M.room s' ≤ s.frontier + M.room s

The frame of a client. A run of a linked admissible client changes no cell outside the footprint that was allocated before it, grows the footprint only into fresh cells, and advances the frontier by at most the room it gives up, as each method run does.

Composition

def Cslib.DataStructure.Memory.Framed.comp {w : ℕ} {D E : StateTransitionSpec} (R : Refinement D E) (M : Framed E w) : Framed D w

A refinement over a framed refinement is framed, by the same footprint and room: the upper invariant and abstraction read the lower state only through its abstraction, and each upper method is a linked client of the lower methods.

theorem Cslib.DataStructure.Memory.Framed.comp_methods {w : ℕ} {D E : StateTransitionSpec} (R : Refinement D E) (M : Framed E w) : (comp R M).methods = fun (o : D.Op) => link M.methods (R.methods o)

The composite's methods link the upper methods through the lower ones.

theorem Cslib.DataStructure.Memory.Framed.comp_toRefinement {w : ℕ} {D E : StateTransitionSpec} (R : Refinement D E) (M : Framed E w) : (comp R M).toRefinement = R.comp M.toRefinement

The composite is the composition of the refinements.

theorem Cslib.DataStructure.Memory.Framed.comp_inv_iff {w : ℕ} {D E : StateTransitionSpec} (R : Refinement D E) (M : Framed E w) (s : State) : (comp R M).inv s ↔ M.inv s ∧ R.inv (M.abs s)

The composite's invariant: the lower invariant, and the upper invariant of the lower abstraction.

@[simp]

theorem Cslib.DataStructure.Memory.Framed.comp_abs {w : ℕ} {D E : StateTransitionSpec} (R : Refinement D E) (M : Framed E w) (s : State) : (comp R M).abs s = R.abs (M.abs s)

The composite represents a memory state by the upper abstraction of the lower one.

@[simp]

theorem Cslib.DataStructure.Memory.Framed.comp_footprint {w : ℕ} {D E : StateTransitionSpec} (R : Refinement D E) (M : Framed E w) (s : State) : (comp R M).footprint s = M.footprint s

The composite's footprint is the lower footprint.

@[simp]

theorem Cslib.DataStructure.Memory.Framed.comp_room {w : ℕ} {D E : StateTransitionSpec} (R : Refinement D E) (M : Framed E w) (s : State) : (comp R M).room s = M.room s

The composite's room is the lower room.

theorem Cslib.DataStructure.Memory.Framed.Local.comp {w : ℕ} {D E : StateTransitionSpec} {R : Refinement D E} {M : Framed E w} {β : Type u_1} {f : State → β} (hf : M.Local f) : (Framed.comp R M).Local f

A function local to the lower framed refinement is local to the composite.

theorem Cslib.DataStructure.Memory.Framed.amortized_comp {w : ℕ} {D E : StateTransitionSpec} {R : Refinement D E} {M : Framed E w} {lower : State → Op → ℕ} {middle : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {Φ : E.State → ℕ} {Ψ : State → ℕ} (A : R.Amortized middle upper Φ) (B : M.Amortized lower middle Ψ) : (comp R M).Amortized lower upper fun (s : (spec w).State) => Φ (M.abs s) + Ψ s

Potentials stack across composition with a framed refinement, as for refinements (Refinement.Amortized.comp).

Frames of disjoint structures

theorem Cslib.DataStructure.Memory.Framed.agree_of_run {w : ℕ} {D D₂ : StateTransitionSpec} {M : Framed D w} (N : Framed D₂ w) {s : State} (o : D.Op) {a : D.Result o} {s' : State} {tr : (spec w).Transcript} (hM : M.inv s) (hN : N.inv s) (hd : Disjoint (M.footprint s) (N.footprint s)) (hv : D.valid (M.abs s) o) (hrun : (spec w).ClientRun s (M.methods o) a s' tr) (b : ℕ) : b ∈ N.footprint s → s'.mem b = s.mem b

A method run of M keeps every cell of a disjoint, allocated footprint.

theorem Cslib.DataStructure.Memory.Framed.room_of_run {w : ℕ} {D : StateTransitionSpec} {M : Framed D w} {s : State} (o : D.Op) {a : D.Result o} {s' : State} {tr : (spec w).Transcript} (hM : M.inv s) (hv : D.valid (M.abs s) o) (hrun : (spec w).ClientRun s (M.methods o) a s' tr) {r : ℕ} (hroom : WordRAM.Fits w (s.frontier + (M.room s + r))) : WordRAM.Fits w (s'.frontier + (M.room s' + r))

A method run of M leaves room for N when both rooms fitted before.

theorem Cslib.DataStructure.Memory.Framed.frame {w : ℕ} {D D₂ : StateTransitionSpec} {M : Framed D w} (N : Framed D₂ w) {s : State} (o : D.Op) {a : D.Result o} {s' : State} {tr : (spec w).Transcript} (hM : M.inv s) (hN : N.inv s) (hd : Disjoint (M.footprint s) (N.footprint s)) (hroom : WordRAM.Fits w (s.frontier + (M.room s + N.room s))) (hv : D.valid (M.abs s) o) (hrun : (spec w).ClientRun s (M.methods o) a s' tr) : N.abs s' = N.abs s ∧ N.inv s' ∧ N.footprint s' = N.footprint s ∧ N.room s' = N.room s ∧ Disjoint (M.footprint s') (N.footprint s') ∧ WordRAM.Fits w (s'.frontier + (M.room s' + N.room s'))

The frame of a framed refinement. A method run of M leaves a framed refinement with a disjoint footprint unchanged, and the footprints disjoint and the shared room budget fitting.

theorem Cslib.DataStructure.Memory.Framed.Local.frame {w : ℕ} {D D₂ : StateTransitionSpec} {M : Framed D w} (N : Framed D₂ w) {β : Type u_1} {f : State → β} (hf : N.Local f) {s : State} (o : D.Op) {a : D.Result o} {s' : State} {tr : (spec w).Transcript} (hM : M.inv s) (hN : N.inv s) (hd : Disjoint (M.footprint s) (N.footprint s)) (hroom : WordRAM.Fits w (s.frontier + (M.room s + N.room s))) (hv : D.valid (M.abs s) o) (hrun : (spec w).ClientRun s (M.methods o) a s' tr) : f s' = f s

A method run of M leaves unchanged every function that reads only a disjoint footprint.

Products

def Cslib.DataStructure.Memory.Framed.Apart {w : ℕ} {D₁ D₂ : StateTransitionSpec} (M₁ : Framed D₁ w) (M₂ : Framed D₂ w) (s : State) : Prop

What keeps two framed refinements apart in one memory: disjoint footprints, and room for both.

theorem Cslib.DataStructure.Memory.Framed.prod_frame_left {w : ℕ} {D₁ D₂ : StateTransitionSpec} (M₁ : Framed D₁ w) (M₂ : Framed D₂ w) {s : State} (o : D₁.Op) {a : D₁.Result o} {s' : State} {tr : (spec w).Transcript} (h₁ : M₁.inv s) (h₂ : M₂.inv s) (hJ : M₁.Apart M₂ s) (hv : D₁.valid (M₁.abs s) o) (hrun : (spec w).ClientRun s (M₁.methods o) a s' tr) : M₂.abs s' = M₂.abs s ∧ M₂.inv s' ∧ M₁.Apart M₂ s'

A method run of the left side keeps the right side and keeps the two apart.

theorem Cslib.DataStructure.Memory.Framed.prod_frame_right {w : ℕ} {D₁ D₂ : StateTransitionSpec} (M₁ : Framed D₁ w) (M₂ : Framed D₂ w) {s : State} (o : D₂.Op) {a : D₂.Result o} {s' : State} {tr : (spec w).Transcript} (h₁ : M₁.inv s) (h₂ : M₂.inv s) (hJ : M₁.Apart M₂ s) (hv : D₂.valid (M₂.abs s) o) (hrun : (spec w).ClientRun s (M₂.methods o) a s' tr) : M₁.abs s' = M₁.abs s ∧ M₁.inv s' ∧ M₁.Apart M₂ s'

A method run of the right side keeps the left side and keeps the two apart.

def Cslib.DataStructure.Memory.Framed.prod {w : ℕ} {D₁ D₂ : StateTransitionSpec} (M₁ : Framed D₁ w) (M₂ : Framed D₂ w) : Framed (product D₁ D₂) w

Products over one memory. Two framed refinements implement the product of their specifications over one memory, with the union of their footprints and the sum of their rooms, while they are apart: their footprints are disjoint and the frontier plus both rooms fits a word. Being apart is part of the product's invariant.

theorem Cslib.DataStructure.Memory.Framed.prod_methods {w : ℕ} {D₁ D₂ : StateTransitionSpec} (M₁ : Framed D₁ w) (M₂ : Framed D₂ w) : (M₁.prod M₂).methods = M₁.methods.prod M₂.methods

The product's methods run each side's methods. They do not depend on the proofs.

@[simp]

theorem Cslib.DataStructure.Memory.Framed.prod_abs {w : ℕ} {D₁ D₂ : StateTransitionSpec} (M₁ : Framed D₁ w) (M₂ : Framed D₂ w) (s : State) : (M₁.prod M₂).abs s = (M₁.abs s, M₂.abs s)

The product represents each side by its own abstraction.

theorem Cslib.DataStructure.Memory.Framed.prod_inv_iff {w : ℕ} {D₁ D₂ : StateTransitionSpec} (M₁ : Framed D₁ w) (M₂ : Framed D₂ w) (s : State) : (M₁.prod M₂).inv s ↔ M₁.inv s ∧ M₂.inv s ∧ M₁.Apart M₂ s

The product's invariant: both sides' invariants, and the two sides apart.

@[simp]

theorem Cslib.DataStructure.Memory.Framed.prod_footprint {w : ℕ} {D₁ D₂ : StateTransitionSpec} (M₁ : Framed D₁ w) (M₂ : Framed D₂ w) (s : State) : (M₁.prod M₂).footprint s = M₁.footprint s ∪ M₂.footprint s

The product's footprint is the union of the footprints.

@[simp]

theorem Cslib.DataStructure.Memory.Framed.prod_room {w : ℕ} {D₁ D₂ : StateTransitionSpec} (M₁ : Framed D₁ w) (M₂ : Framed D₂ w) (s : State) : (M₁.prod M₂).room s = M₁.room s + M₂.room s

The product's room is the sum of the rooms.

theorem Cslib.DataStructure.Memory.Framed.Local.prod_left {w : ℕ} {D₁ D₂ : StateTransitionSpec} {M₁ : Framed D₁ w} {M₂ : Framed D₂ w} {β : Type u_1} {f : State → β} (hf : M₁.Local f) : (M₁.prod M₂).Local f

A function local to the left side is local to the product.

theorem Cslib.DataStructure.Memory.Framed.Local.prod_right {w : ℕ} {D₁ D₂ : StateTransitionSpec} {M₁ : Framed D₁ w} {M₂ : Framed D₂ w} {β : Type u_1} {f : State → β} (hf : M₂.Local f) : (M₁.prod M₂).Local f

A function local to the right side is local to the product.

theorem Cslib.DataStructure.Memory.Framed.amortized_prod {w : ℕ} {D₁ D₂ : StateTransitionSpec} {M₁ : Framed D₁ w} {M₂ : Framed D₂ w} {lower : State → Op → ℕ} {upper₁ : D₁.State → D₁.Op → ℕ} {upper₂ : D₂.State → D₂.Op → ℕ} {Φ₁ Φ₂ : State → ℕ} (A₁ : M₁.Amortized lower upper₁ Φ₁) (A₂ : M₂.Amortized lower upper₂ Φ₂) (hΦ₁ : M₁.Local Φ₁) (hΦ₂ : M₂.Local Φ₂) : (M₁.prod M₂).Amortized lower (productCharge upper₁ upper₂) fun (s : (spec w).State) => Φ₁ s + Φ₂ s

Potentials add across a product over one memory. Certificates of the two sides against one lower charge, with potentials that read only their own footprints, give a certificate of the product with componentwise upper charges and the sum of the potentials.

theorem Cslib.DataStructure.Memory.Framed.prod_of_fresh {w : ℕ} {D₁ D₂ : StateTransitionSpec} {M₁ : Framed D₁ w} {M₂ : Framed D₂ w} {s s' : State} (h₁ : M₁.inv s) (hmem : ∀ a < s.frontier, s'.mem a = s.mem a) (hf : s.frontier ≤ s'.frontier) (h₂ : M₂.inv s') (hd : Disjoint (M₁.footprint s) (M₂.footprint s')) (hroom : WordRAM.Fits w (s'.frontier + (M₁.room s + M₂.room s'))) : (M₁.prod M₂).inv s' ∧ (M₁.prod M₂).abs s' = (M₁.abs s, M₂.abs s') ∧ (M₁.prod M₂).footprint s' = M₁.footprint s ∪ M₂.footprint s' ∧ (M₁.prod M₂).room s' = M₁.room s + M₂.room s'

Setting up a product from structures allocated one after the other: M₁ holds at s; a run from s to s' leaves the cells below s.frontier unchanged; M₂ holds at s' on a footprint disjoint from M₁'s, such as one at or above s.frontier; and the frontier plus both rooms fits. Then the product holds at s', with M₁'s abstraction, footprint and room unchanged.