The FIFO meaning of a two-stack representation

The front stack lists the oldest values first; the rear stack lists the newest values first. Thus the represented FIFO sequence is front ++ rear.reverse. Enqueue pushes onto the rear. Dequeue pops the front when possible; otherwise it reverses the entire rear into the front before popping. Reversal is only a mathematical description here: the machine implementation executes a charged loop, moving one value at a time.

Main definitions

• spec: the existing FIFO specification restricted to fitting words and a fixed capacity.
• contents: the FIFO sequence represented by a pair of stacks.
• pairStep: the corresponding transition of the two stacks.

Main results

• pairStep_correct: both the returned answer and the new FIFO sequence match spec.
• pairStep_length_le: admissible calls preserve the shared capacity bound.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, Exercise 10.1-6.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.spec (w capacity : ℕ) : Stateful.Spec

A queue admits an enqueue exactly when it has spare capacity and the value fits a word.

def Cslib.WordRAM.Queue.contents (s : List ℕ × List ℕ) : List ℕ

Front is in FIFO order; rear is in reverse FIFO order.

def Cslib.WordRAM.Queue.pairStep (s : List ℕ × List ℕ) (o : Algorithms.Lean.Queue.QueueOp ℕ) : (List ℕ × List ℕ) × (Algorithms.Lean.Queue.queue ℕ).Result o

Mathematical description of the machine's two-stack transition, including an empty pop.

theorem Cslib.WordRAM.Queue.pairStep_correct (s : List ℕ × List ℕ) (o : Algorithms.Lean.Queue.QueueOp ℕ) : (contents (pairStep s o).1, (pairStep s o).2) = (Algorithms.Lean.Queue.queue ℕ).step (contents s) o

Projecting the concrete stack transition gives exactly the specified FIFO step.

theorem Cslib.WordRAM.Queue.contents_length (s : List ℕ × List ℕ) : (contents s).length = s.1.length + s.2.length

The sum of live stack lengths is the FIFO length, not the size of the reserved regions.

theorem Cslib.WordRAM.Queue.pairStep_length_le {w capacity : ℕ} {s : List ℕ × List ℕ} (hs : (contents s).length ≤ capacity) (o : Algorithms.Lean.Queue.QueueOp ℕ) (hv : (spec w capacity).valid (contents s) o) : (contents (pairStep s o).1).length ≤ capacity

Enqueues require one spare slot; dequeues cannot increase the number of live values.