A fixed-program bounded stack on the word RAM

A nine-register program dispatches push, pop, and size operations using an encoded operation tag. The stack occupies a fixed consecutive memory block, with its top at the highest live address. A pop from an empty stack returns none; other pops return a word and decrease the length without clearing the old cell. Push requires spare capacity and a fitting value.

The semantic certificate is independent of the separate instruction certificate. Every call includes its final halt; argument delivery and the initial reserved block are calling-convention assumptions. This realizes a bounded restriction of the mathematical stack, not its unrestricted interface. A native instruction theorem for an arbitrary free-monad client still excludes execution of the client's pure controller.

Main definitions

• spec: the mathematical stack with explicit bounded-operation admissibility.
• program: a single fixed dispatch program, independent of the requested operation.
• Rep: top-first lists represented by a bottom-first memory block.
• certificate: semantic realization over native word-RAM traces.

Main results

• execute: actual per-operation execution, representation, and frame guarantee.
• instruction_bound: at most twelve instructions per admissible operation.
• initial_rep: a concrete empty represented stack.

References

The abstract stack interface is shared with Cslib.Algorithms.Lean.Queue. Array indexing and machine execution reuse the checked WordRAM.Allocation and WordRAM.Structured substrate.

@[reducible, inline]

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

A fixed-capacity restriction of the same mathematical stack interface.

@[reducible, inline]

abbrev Cslib.WordRAM.Stack.tag : Fin 9

Encoded operation tag: push = 0, pop = 1, size = 2.

@[reducible, inline]

abbrev Cslib.WordRAM.Stack.arg : Fin 9

Caller-supplied push value.

@[reducible, inline]

abbrev Cslib.WordRAM.Stack.len : Fin 9

Persistent number of live entries.

@[reducible, inline]

abbrev Cslib.WordRAM.Stack.ptr : Fin 9

Persistent base address of the reserved region.

@[reducible, inline]

abbrev Cslib.WordRAM.Stack.addr : Fin 9

Temporary cell address.

@[reducible, inline]

abbrev Cslib.WordRAM.Stack.out : Fin 9

Returned value.

@[reducible, inline]

abbrev Cslib.WordRAM.Stack.zero : Fin 9

Constant zero.

@[reducible, inline]

abbrev Cslib.WordRAM.Stack.one : Fin 9

Constant one.

@[reducible, inline]

abbrev Cslib.WordRAM.Stack.present : Fin 9

Presence bit distinguishing none from a returned zero word.

def Cslib.WordRAM.Stack.program : Code Basis.standard 9

Fixed operation dispatch. No code is generated from an operation or its payload.

def Cslib.WordRAM.Stack.implementation (w capacity : ℕ) : DynamicProgram (spec w capacity) 9

Calling convention for the fixed dispatch program. Answers inspect only output registers.

structure Cslib.WordRAM.Stack.Rep (w base capacity : ℕ) (vs : List ℕ) (x : Data 9) : Prop

Persistent register, bounded-word, and live array invariants. Cells above the live prefix may contain old popped values; they are part of the reserved footprint.

• bounded : Data.Bounded w x
• pointer : x.regs ptr = base
• length_eq : x.regs len = vs.length
• capacity_le : vs.length ≤ capacity
• contents (i : Fin vs.length) : x.mem (base + ↑i) = vs.reverse[↑i]

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

Reserved memory footprint; it stays fixed through pushes and pops.

theorem Cslib.WordRAM.Stack.arguments_fit {w capacity : ℕ} (h2 : Fits w 2) {vs : List ℕ} (o : Algorithms.Lean.Queue.StackOp ℕ) (hv : (spec w capacity).valid vs o) (i : Fin 9) : Fits w ((implementation w capacity).encode o i)

def Cslib.WordRAM.Stack.bodyCost (vs : List ℕ) : Algorithms.Lean.Queue.StackOp ℕ → ℕ

Actual instructions excluding the final halt.

theorem Cslib.WordRAM.Stack.execute {w base capacity : ℕ} (h2 : Fits w 2) (hcap : Fits w (base + capacity)) {vs : List ℕ} {x : Data 9} (hr : Rep w base capacity vs x) (o : Algorithms.Lean.Queue.StackOp ℕ) (hv : (spec w capacity).valid vs o) : ∃ (y : Data 9), Exec w program ((implementation w capacity).prepare o x) y (bodyCost vs o) ∧ (implementation w capacity).decode o y.regs = some ((spec w capacity).step vs o).2 ∧ Rep w base capacity ((spec w capacity).step vs o).1 y ∧ Modifies (footprint base capacity) x.mem y.mem

Every admissible operation executes the fixed dispatcher with an exact instruction count, returns the specified answer, and preserves memory outside the reserved region.

def Cslib.WordRAM.Stack.certificate {w base capacity : ℕ} (h2 : Fits w 2) (hcap : Fits w (base + capacity)) : DynamicCertificate (implementation w capacity) w

Semantic realization of the bounded stack, independently of its performance theorem.

theorem Cslib.WordRAM.Stack.instructions_eq {w base capacity : ℕ} (h2 : Fits w 2) (hcap : Fits w (base + capacity)) {vs : List ℕ} {x y : Data 9} {o : Algorithms.Lean.Queue.StackOp ℕ} {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace} (hr : Rep w base capacity vs x) (hv : (spec w capacity).valid vs o) (he : (implementation w capacity).ExecOp w x o a y trace) : trace.instructions = bodyCost vs o + 1

Actual instruction count, including dispatch and the final halt, for every native call.

theorem Cslib.WordRAM.Stack.instruction_bound {w base capacity : ℕ} (h2 : Fits w 2) (hcap : Fits w (base + capacity)) : Stateful.Bound (certificate h2 hcap).realization DynamicProgram.OperationTrace.instructions fun (x : (spec w capacity).State) (x_1 : (spec w capacity).Op) => 12

Every admissible call has a separate worst-case bound of twelve native instructions.

theorem Cslib.WordRAM.Stack.modifies {w base capacity : ℕ} (h2 : Fits w 2) (hcap : Fits w (base + capacity)) {vs : List ℕ} {x y : Data 9} {o : Algorithms.Lean.Queue.StackOp ℕ} {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace} (hr : Rep w base capacity vs x) (hv : (spec w capacity).valid vs o) (he : (implementation w capacity).ExecOp w x o a y trace) : Modifies (footprint base capacity) x.mem y.mem

Every concrete call preserves all memory outside the same reserved stack block.

theorem Cslib.WordRAM.Stack.frame {w base capacity : ℕ} (h2 : Fits w 2) (hcap : Fits w (base + capacity)) {vs : List ℕ} {x y : Data 9} {o : Algorithms.Lean.Queue.StackOp ℕ} {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace} (hr : Rep w base capacity vs x) (hv : (spec w capacity).valid vs 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

The machine stack preserves any disjoint heap representation.

def Cslib.WordRAM.Stack.initial (base : ℕ) : Data 9

An empty reserved block, with all memory zero and the persistent pointer installed. This is a calling-convention initial state, not an uncharged allocation instruction.

theorem Cslib.WordRAM.Stack.initial_rep {w base capacity : ℕ} (hcap : Fits w (base + capacity)) : Rep w base capacity [] (initial base)

The initial representation is inhabited for every fitting reserved block.

theorem Cslib.WordRAM.Stack.run_client {w base capacity : ℕ} (h2 : Fits w 2) (hcap : Fits w (base + capacity)) {α : Type} (p : (spec w capacity).Client α) {vs : List ℕ} {x : Data 9} (hr : Rep w base capacity vs x) (hv : (spec w capacity).ValidHistory vs ((spec w capacity).runClient vs p).2.2) : ∃ (y : Data 9) (traces : List DynamicProgram.OperationTrace), Stateful.Executes ((implementation w capacity).ExecOp w) p x ((spec w capacity).runClient vs p).1 y traces ∧ Rep w base capacity ((spec w capacity).runClient vs p).2.1 y ∧ Stateful.total DynamicProgram.OperationTrace.instructions traces ≤ ((spec w capacity).runClient vs p).2.2.length * 12

One-operation realization and an independent resource certificate compose across arbitrary admissible adaptive clients. The client controller itself is external to the machine code.