Two stacks implementing a queue in shared RAM

Two disjoint reserved blocks hold bottom-first stack arrays. Enqueue pushes onto the rear; dequeue transfers the rear into an empty front before popping. All address arithmetic, memory accesses, loop tests and operation dispatch are machine instructions. Empty live prefixes do not require clearing the reserved memory.

Main definitions

• Rep: the bounded shared-memory representation of the two top-first lists.
• program: one fixed operation dispatcher.
• implementation: its argument and result conventions.
• initializeCode: six charged writes installing an empty representation.

Main results

• execute: exact instruction execution, observations, representation and memory frame.
• initialize_exec: initialization from arbitrary bounded machine data without clearing memory.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.tag : Fin 11

Operation tag: enqueue zero, dequeue one.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.arg : Fin 11

Enqueued word.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.frontLen : Fin 11

Front stack length.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.frontBase : Fin 11

Front block base.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.backLen : Fin 11

Rear stack length.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.backBase : Fin 11

Rear block base.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.addr : Fin 11

Temporary address.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.out : Fin 11

Returned word.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.present : Fin 11

Returned presence flag.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.zero : Fin 11

Constant zero.

@[reducible, inline]

abbrev Cslib.WordRAM.Queue.one : Fin 11

Constant one.

structure Cslib.WordRAM.Queue.Rep (w base capacity : ℕ) (front back : List ℕ) (x : Data 11) : Prop

Both stack arrays live in one bounded memory, with one common capacity bound.

• bounded : Data.Bounded w x
• frontBase_eq : x.regs frontBase = base
• backBase_eq : x.regs backBase = base + capacity
• frontLen_eq : x.regs frontLen = front.length
• backLen_eq : x.regs backLen = back.length
• zero_eq : x.regs zero = 0
• one_eq : x.regs one = 1
• size_le : front.length + back.length ≤ capacity
• front_contents (i : Fin front.length) : x.mem (base + ↑i) = front.reverse[↑i]
• back_contents (i : Fin back.length) : x.mem (base + capacity + ↑i) = back.reverse[↑i]

def Cslib.WordRAM.Queue.footprint (base capacity : ℕ) : Finset ℕ

The fixed reserved region, including currently unused cells.

def Cslib.WordRAM.Queue.enqueue : Code Basis.standard 11

Enqueue writes the next rear cell and advances the rear length.

def Cslib.WordRAM.Queue.move : Code Basis.standard 11

Move the top rear word onto the front stack.

def Cslib.WordRAM.Queue.transfer : Code Basis.standard 11

Reverse the rear stack onto the front, testing each iteration on machine registers.

def Cslib.WordRAM.Queue.pop : Code Basis.standard 11

Pop the front, distinguishing the empty queue from a returned zero.

def Cslib.WordRAM.Queue.dequeue : Code Basis.standard 11

Transfer only when the front is empty.

def Cslib.WordRAM.Queue.program : Code Basis.standard 11

One fixed dispatcher, independent of queue contents, capacity, and operation arguments.

def Cslib.WordRAM.Queue.implementation (w capacity : ℕ) : DynamicProgram (spec w capacity) 11

Register calling convention for the fixed queue dispatcher.

theorem Cslib.WordRAM.Queue.enqueue_exec {w base capacity v : ℕ} {front back : List ℕ} {x : Data 11} (hc : Fits w (base + 2 * capacity)) (hr : Rep w base capacity front back x) (hs : front.length + back.length < capacity) (hv : x.regs arg = v) : ∃ (y : Data 11), Exec w enqueue x y 4 ∧ Rep w base capacity front (v :: back) y ∧ Modifies (footprint base capacity) x.mem y.mem

Enqueue body correctness with an exact four-instruction execution.

theorem Cslib.WordRAM.Queue.move_exec {w base capacity v : ℕ} {front back : List ℕ} {x : Data 11} (hc : Fits w (base + 2 * capacity)) (hr : Rep w base capacity front (v :: back) x) : ∃ (y : Data 11), Exec w move x y 6 ∧ Rep w base capacity (v :: front) back y ∧ Modifies (footprint base capacity) x.mem y.mem

A rear-to-front move performs six instructions and preserves the reserved-region frame.

theorem Cslib.WordRAM.Queue.transfer_exec {w base capacity : ℕ} {front back : List ℕ} {x : Data 11} (hc : Fits w (base + 2 * capacity)) (hr : Rep w base capacity front back x) : ∃ (y : Data 11), Exec w transfer x y (8 * back.length + 2) ∧ Rep w base capacity (back.reverse ++ front) [] y ∧ Modifies (footprint base capacity) x.mem y.mem

Transfer costs eight instructions per moved word and two instructions to exit the loop.

theorem Cslib.WordRAM.Queue.pop_exec {w base capacity : ℕ} {front back : List ℕ} {x : Data 11} (hc : Fits w (base + 2 * capacity)) (hr : Rep w base capacity front back x) : ∃ (y : Data 11), Exec w pop x y (if front = [] then 3 else 6) ∧ Rep w base capacity front.tail back y ∧ (if y.regs present = 0 then none else some (y.regs out)) = front.head? ∧ y.mem = x.mem

Front-pop execution counts include the empty/nonempty branch and distinguish returned zero.

def Cslib.WordRAM.Queue.bodyCost (front back : List ℕ) : Algorithms.Lean.Queue.QueueOp ℕ → ℕ

Exact instruction count of a dispatched operation, excluding the final halt.

theorem Cslib.WordRAM.Queue.arguments_fit {w capacity : ℕ} (h1 : Fits w 1) {q : List ℕ} (o : Algorithms.Lean.Queue.QueueOp ℕ) (hv : (spec w capacity).valid q o) (i : Fin 11) : Fits w ((implementation w capacity).encode o i)

theorem Cslib.WordRAM.Queue.execute {w base capacity : ℕ} {front back : List ℕ} {x : Data 11} (hc : Fits w (base + 2 * capacity)) (hr : Rep w base capacity front back x) (o : Algorithms.Lean.Queue.QueueOp ℕ) (hv : (spec w capacity).valid (contents (front, back)) o) : ∃ (y : Data 11), Exec w program ((implementation w capacity).prepare o x) y (bodyCost front back o) ∧ (implementation w capacity).decode o y.regs = some (pairStep (front, back) o).2 ∧ Rep w base capacity (pairStep (front, back) o).1.1 (pairStep (front, back) o).1.2 y ∧ Modifies (footprint base capacity) x.mem y.mem

Every valid operation executes the fixed dispatcher with its exact instruction count, implements the two-stack transition, and preserves every cell outside the reserved region.

def Cslib.WordRAM.Queue.initializeCode (base capacity : ℕ) : Code Basis.standard 11

Install an empty queue using six register instructions, with no writes to reserved memory.

theorem Cslib.WordRAM.Queue.initialize_exec {w base capacity : ℕ} {x : Data 11} (hx : Data.Bounded w x) (h1 : Fits w 1) (hc : Fits w (base + 2 * capacity)) : ∃ (y : Data 11), Exec w (initializeCode base capacity) x y 6 ∧ Rep w base capacity [] [] y ∧ y.mem = x.mem

Initialization accepts arbitrary bounded registers and memory. Only the six representation registers change; both reserved live prefixes are empty, so memory remains untouched.