EconCSLib.Foundation.CostM.Cells

The "tropical-shaped" cost monoid for peak-style resource analysis.

A Cells value carries two integers, peak and delta, with invariants 0 ≤ peak and delta ≤ peak:

• peak — maximum occupancy reached during a computation, relative to the occupancy at the start of the computation.
• delta — net change in occupancy from start to end. Negative if the computation ends with fewer live cells than it started (free exceeds alloc).

Composition

(p₁, d₁) ⋆ (p₂, d₂) = (max p₁ (d₁ + p₂), d₁ + d₂)

encodes sequential semantics: the new peak is whichever was higher — the first computation's peak, or the second computation's peak shifted up by the first computation's net offset.

This is not an additive monoid in the elementwise sense — + does not just add componentwise; the peak component composes "tropically" via max. But the resulting structure still satisfies the AddMonoid laws, which is all CostM requires.

Primitives

• alloc n := ⟨n, n, _, _⟩ — claim n cells; both peak and delta rise by n.
• free n := ⟨0, -n, _, _⟩ — release n cells; peak unchanged, delta drops.

Bound shape

For an algorithm

do alloc K; ⟨body with zero ticks⟩; free K; pure result

the resulting cost has .peak = K. When K is independent of input size this gives an O(1) (constant-space) bound. The Boyer-Moore example in Examples/CostM/BoyerMoore.lean demonstrates this shape with K = 2.

structure Cells : Type

Tropical-style cost record: peak occupancy and net delta.

• peak : ℤ

  Peak occupancy reached during the computation (≥ 0).

• delta : ℤ

  Net change in occupancy from start to end (≤ peak).

• zero_le_peak : 0 ≤ self.peak

  Peak is non-negative.

• delta_le_peak : self.delta ≤ self.peak

  Delta never exceeds peak.

theorem Cells.ext_iff {x y : Cells} : x = y ↔ x.peak = y.peak ∧ x.delta = y.delta

theorem Cells.ext {x y : Cells} (peak : x.peak = y.peak) (delta : x.delta = y.delta) : x = y

@[implicit_reducible]

instance Cells.instZero : Zero Cells

Equations

• Cells.instZero = { zero := { peak := 0, delta := 0, zero_le_peak := Cells.instZero._proof_1, delta_le_peak := Cells.instZero._proof_1 } }

@[simp]

theorem Cells.peak_zero : peak 0 = 0

@[simp]

theorem Cells.delta_zero : delta 0 = 0

@[implicit_reducible]

instance Cells.instAdd : Add Cells

Equations

• Cells.instAdd = { add := fun (a b : Cells) => { peak := max a.peak (a.delta + b.peak), delta := a.delta + b.delta, zero_le_peak := ⋯, delta_le_peak := ⋯ } }

@[simp]

theorem Cells.peak_add (a b : Cells) : (a + b).peak = max a.peak (a.delta + b.peak)

@[simp]

theorem Cells.delta_add (a b : Cells) : (a + b).delta = a.delta + b.delta

@[implicit_reducible]

instance Cells.instAddMonoid : AddMonoid Cells

Equations

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

def Cells.alloc (n : ℕ) : Cells

Allocate n cells: peak and delta both rise by n.

Equations

• Cells.alloc n = { peak := ↑n, delta := ↑n, zero_le_peak := ⋯, delta_le_peak := ⋯ }

def Cells.free (n : ℕ) : Cells

Release n cells: peak unchanged, delta drops by n.

Equations

• Cells.free n = { peak := 0, delta := -↑n, zero_le_peak := Cells.instZero._proof_1, delta_le_peak := ⋯ }

@[simp]

theorem Cells.peak_alloc (n : ℕ) : (alloc n).peak = ↑n

@[simp]

theorem Cells.delta_alloc (n : ℕ) : (alloc n).delta = ↑n

@[simp]

theorem Cells.peak_free (n : ℕ) : (free n).peak = 0

@[simp]

theorem Cells.delta_free (n : ℕ) : (free n).delta = -↑n