A modular queue implemented with two stacks

The behavior proof mentions no concrete stack representation or resource model. The front stack stores the next elements to dequeue; the reversed rear stack stores newly enqueued elements. When the front is empty, the implementation queries the rear size and transfers those elements. This standard construction follows Cormen et al., Exercise 10.1-6; the potential method is described in Chapter 17.

Main definitions

• stack, stackPair, and queue: total specifications with operation-dependent result types.
• implementation: semantic queue implementation over the stack-pair interface.

Main results

• transfer_run: stack operations reverse the rear contents into the front stack.
• potential_step: at most three amortized stack calls, including the size query.
• realized_client: every adaptive client has a correct backend execution with its bound.
• realized_client_bound: every supplied linked execution satisfies correctness and the bound.

For a primitive weight bound K, a client performing m queue operations satisfies weight + 2 K rearFinal.length ≤ 3 K m + 2 K rearInitial.length. This is a conditional bound on backend traces, not a machine instruction-count theorem. Pure client computation is uncharged; backend implementations must justify their primitive weights and state independence separately.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms

inductive Cslib.Algorithms.Lean.Queue.StackOp (α : Type) : Type

Stack operations with typed answers.

• push {α : Type} (value : α) : StackOp α
• pop {α : Type} : StackOp α
• size {α : Type} : StackOp α

def Cslib.Algorithms.Lean.Queue.instDecidableEqStackOp.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : StackOp α✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.Lean.Queue.instDecidableEqStackOp {α✝ : Type} [DecidableEq α✝] : DecidableEq (StackOp α✝)

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.Queue.stack (α : Type) : Stateful.Spec

A total stack specification; popping an empty stack returns none.

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.Queue.stackPair (α : Type) : Stateful.Spec

Two independently addressable stacks.

inductive Cslib.Algorithms.Lean.Queue.QueueOp (α : Type) : Type

FIFO queue operations with typed answers.

• enqueue {α : Type} (value : α) : QueueOp α
• dequeue {α : Type} : QueueOp α

@[instance_reducible]

instance Cslib.Algorithms.Lean.Queue.instDecidableEqQueueOp {α✝ : Type} [DecidableEq α✝] : DecidableEq (QueueOp α✝)

def Cslib.Algorithms.Lean.Queue.instDecidableEqQueueOp.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : QueueOp α✝) : Decidable (x✝ = x✝¹)

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.Queue.queue (α : Type) : Stateful.Spec

A total FIFO queue specification.

def Cslib.Algorithms.Lean.Queue.transfer {α : Type} : ℕ → (stackPair α).Client Unit

Move at most n items from the rear stack to the front stack. The fuel is obtained through an explicit size call, rather than inspecting hidden state.

def Cslib.Algorithms.Lean.Queue.methods {α : Type} : Stateful.Methods (queue α) (stackPair α)

The same queue methods work for every realization of the stack interface.

def Cslib.Algorithms.Lean.Queue.transferTrace {α : Type} : List α → List (stackPair α).Op

Primitive-operation trace of transferring the rear contents to the front.

theorem Cslib.Algorithms.Lean.Queue.transfer_run {α : Type} (front back : List α) : (stackPair α).runClient (front, back) (transfer back.length) = ((), (back.reverse ++ front, []), transferTrace back)

The queue's sole traversal argument: abstract stack calls reverse the rear contents.

def Cslib.Algorithms.Lean.Queue.implementation {α : Type} : Stateful.Module (queue α) (stackPair α)

Representation and behavior are proved once, before selecting a backend or cost model.

theorem Cslib.Algorithms.Lean.Queue.transferTrace_length {α : Type} (back : List α) : (transferTrace back).length = 2 * back.length

Each transferred element incurs one pop and one push.

theorem Cslib.Algorithms.Lean.Queue.potential_step {α : Type} (s : (stackPair α).State) (o : QueueOp α) : ((stackPair α).runClient s (methods o)).2.2.length + 2 * List.length ((stackPair α).runClient s (methods o)).2.1.2 ≤ 3 + 2 * List.length s.2

The queue has a three-call amortized bound; rear-stack credit remains private to the module. This counts stack calls, not execution of pure continuations or machine instructions.

theorem Cslib.Algorithms.Lean.Queue.realized_client {α C Trace β : Type} {exec : Stateful.Execution (stackPair α) C Trace} (R : Stateful.Realization (stackPair α) exec) (weight : Trace → ℕ) (K : ℕ) (B : Stateful.Bound R weight fun (x : (stackPair α).State) (x_1 : (stackPair α).Op) => K) (p : (queue α).Client β) {q : List α} {s : (stackPair α).State} {c : C} (hrep : implementation.rep q s) (hbackend : R.rep s c) : ∃ (c' : C) (traces : List Trace) (s' : (stackPair α).State), Stateful.Executes exec (Stateful.link methods p) c ((queue α).runClient q p).1 c' traces ∧ implementation.rep ((queue α).runClient q p).2.1 s' ∧ R.rep s' c' ∧ Stateful.total weight traces + K * (2 * List.length s'.2) ≤ ((queue α).runClient q p).2.2.length * (3 * K) + K * (2 * List.length s.2)

Uniform primitive bounds can be chosen after proving queue correctness. The same theorem applies to any additive measure on any backend's native traces. It also retains leftover credit.

theorem Cslib.Algorithms.Lean.Queue.realized_client_bound {α C Trace β : Type} {exec : Stateful.Execution (stackPair α) C Trace} (R : Stateful.Realization (stackPair α) exec) (weight : Trace → ℕ) (K : ℕ) (B : Stateful.Bound R weight fun (x : (stackPair α).State) (x_1 : (stackPair α).Op) => K) (p : (queue α).Client β) {q : List α} {s : (stackPair α).State} {c c' : C} {a : β} {traces : List Trace} (hrep : implementation.rep q s) (hbackend : R.rep s c) (he : Stateful.Executes exec (Stateful.link methods p) c a c' traces) : a = ((queue α).runClient q p).1 ∧ ∃ (s' : (stackPair α).State), implementation.rep ((queue α).runClient q p).2.1 s' ∧ R.rep s' c' ∧ Stateful.total weight traces + K * (2 * List.length s'.2) ≤ ((queue α).runClient q p).2.2.length * (3 * K) + K * (2 * List.length s.2)

Correctness and the same resource bound hold for every supplied flattened execution.