Correctness and amortized instruction cost of a RAM queue

The mathematical client sees only a FIFO list. The realization hides how that list is split between the two arrays. A dequeue can move every rear element, but each enqueue deposits eight credits: six instructions move an element and two instructions control that loop iteration. Consequently every admissible history costs at most fourteen instructions per operation, plus the initial rear credit. The final unused credit is retained in the inequality.

These are actual RAM operation instructions, including each call's halt. The operation interface still uses externally delivered argument registers; arbitrary pure computation in a client's Lean continuation is not included in this bound. Initialization is a separate six-instruction program. The arrays reserve twice the queue capacity, while at most one capacity's worth of values are live. No allocator or dynamically growing capacity is assumed.

Main definitions

• QueueRep: the FIFO representation hiding the split into two stacks.
• certificate: a semantic realization of the bounded queue interface.
• amortized: the separate instruction-cost certificate with rear-stack potential.

Main results

• run_client: correct adaptive execution and the amortized native instruction bound.
• frame: every operation preserves any disjoint heap assertion.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, Chapters 10 and 17.

theorem Cslib.WordRAM.Queue.footprint_card (base capacity : ℕ) : (footprint base capacity).card = 2 * capacity

The two reserved blocks contain exactly twice the queue capacity in word cells.

def Cslib.WordRAM.Queue.QueueRep (w base capacity : ℕ) (q : List ℕ) (x : Data 11) : Prop

A client observes a FIFO list, while the machine retains a hidden split between two stacks.

def Cslib.WordRAM.Queue.certificate {w base capacity : ℕ} (h1 : Fits w 1) (hc : Fits w (base + 2 * capacity)) : DynamicCertificate (implementation w capacity) w

The fixed dispatcher implements the bounded FIFO specification.

theorem Cslib.WordRAM.Queue.bodyCost_potential (front back : List ℕ) (o : Algorithms.Lean.Queue.QueueOp ℕ) : bodyCost front back o + 1 + 8 * (pairStep (front, back) o).1.2.length ≤ 14 + 8 * back.length

The expensive transfer consumes eight credits per rear element, including loop control. The final halt contributes the extra one in the left side.

theorem Cslib.WordRAM.Queue.instructions_eq {w base capacity : ℕ} (hc : Fits w (base + 2 * capacity)) {front back : List ℕ} {x y : Data 11} {o : Algorithms.Lean.Queue.QueueOp ℕ} {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace} (hr : Rep w base capacity front back x) (hv : (spec w capacity).valid (contents (front, back)) o) (he : (implementation w capacity).ExecOp w x o a y trace) : trace.instructions = bodyCost front back o + 1

Every native operation has the exact charged body cost plus its final halt.

def Cslib.WordRAM.Queue.potential (x : Data 11) : ℕ

Rear-stack credit is read from the concrete persistent length register.

theorem Cslib.WordRAM.Queue.amortized {w base capacity : ℕ} (h1 : Fits w 1) (hc : Fits w (base + 2 * capacity)) : Stateful.Amortized (certificate h1 hc).realization DynamicProgram.OperationTrace.instructions (fun (x : (spec w capacity).State) (x_1 : Data 11) => potential x_1) fun (x : (spec w capacity).State) (x_1 : (spec w capacity).Op) => 14

Amortized constant instruction cost is certified separately from FIFO correctness.

theorem Cslib.WordRAM.Queue.run_client {w base capacity : ℕ} (h1 : Fits w 1) (hc : Fits w (base + 2 * capacity)) {α : Type} (p : (spec w capacity).Client α) {q : List ℕ} {x : Data 11} (hr : QueueRep w base capacity q x) (hv : (spec w capacity).ValidHistory q ((spec w capacity).runClient q p).2.2) : ∃ (y : Data 11) (traces : List DynamicProgram.OperationTrace), Stateful.Executes ((implementation w capacity).ExecOp w) p x ((spec w capacity).runClient q p).1 y traces ∧ QueueRep w base capacity ((spec w capacity).runClient q p).2.1 y ∧ Stateful.total DynamicProgram.OperationTrace.instructions traces + potential y ≤ ((spec w capacity).runClient q p).2.2.length * 14 + potential x

Every admissible adaptive client has a correct native execution with a telescoping bound. This sums operation calls; the externally supplied client controller is not machine code.

theorem Cslib.WordRAM.Queue.run_initialized {w base capacity : ℕ} (h1 : Fits w 1) (hc : Fits w (base + 2 * capacity)) {α : Type} (p : (spec w capacity).Client α) {x : Data 11} (hx : Data.Bounded w x) (hv : (spec w capacity).ValidHistory [] ((spec w capacity).runClient [] p).2.2) : ∃ (ready : Data 11) (y : Data 11) (traces : List DynamicProgram.OperationTrace), Exec w (initializeCode base capacity) x ready 6 ∧ Stateful.Executes ((implementation w capacity).ExecOp w) p ready ((spec w capacity).runClient [] p).1 y traces ∧ QueueRep w base capacity ((spec w capacity).runClient [] p).2.1 y ∧ 6 + Stateful.total DynamicProgram.OperationTrace.instructions traces + potential y ≤ 6 + ((spec w capacity).runClient [] p).2.2.length * 14

Starting with arbitrary bounded data, charge the six initialization instructions before summing the actual queue calls. Empty regions need no zeroing; controller computation and external argument delivery retain the boundary stated in run_client.

theorem Cslib.WordRAM.Queue.modifies {w base capacity : ℕ} (hc : Fits w (base + 2 * capacity)) {q : List ℕ} {x y : Data 11} {o : Algorithms.Lean.Queue.QueueOp ℕ} {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace} (hr : QueueRep w base capacity q x) (hv : (spec w capacity).valid q o) (he : (implementation w capacity).ExecOp w x o a y trace) : Modifies (footprint base capacity) x.mem y.mem

Actual queue calls modify only the two reserved array regions.

theorem Cslib.WordRAM.Queue.frame {w base capacity : ℕ} (hc : Fits w (base + 2 * capacity)) {q : List ℕ} {x y : Data 11} {o : Algorithms.Lean.Queue.QueueOp ℕ} {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace} (hr : QueueRep w base capacity q x) (hv : (spec w capacity).valid q o) (he : (implementation w capacity).ExecOp w x o a y trace) {Q : HeapAssertion} (hQ : Q.holds x.mem) (hd : Disjoint Q.footprint (footprint base capacity)) : Q.holds y.mem

Disjoint heap representations survive every queue call, including a full rear transfer.