An adaptive stack client executed entirely on the word RAM

The client pushes its input, pops it, and replaces a returned zero by another push and pop of one. Its fixed controller explicitly executes initialization, argument preparation and branch instructions. Input placement follows WordRAM.Data.init; no additional heap initialization is needed because the reserved stack starts empty.

Main definitions

• roundTrip: push the argument register and pop its value back.
• code: initialize one reserved cell and execute the adaptive controller.
• client: the same adaptive computation over the abstract stack interface.

Main results

• execute: the whole controller returns max n 1, leaving its stack empty.
• refines: the fixed machine controller implements the abstract adaptive client.
• executes: a halting flat program, with all controller costs and its final halt charged.
• positive_polytime: a reusable polynomial RAM-time certificate for the complete client.

References

The stack implementation and specification are those of WordRAM.Stack and Algorithms.Lean.Queue. This example is a certificate-composition test, not a new stack algorithm.

def Cslib.WordRAM.Stack.Controller.roundTrip : Code Basis.standard 9

Push the argument register, then pop it; argument tags and clearing are real instructions.

def Cslib.WordRAM.Stack.Controller.setup : Code Basis.standard 9

One reserved stack cell at address two, outside the singleton input at address one.

def Cslib.WordRAM.Stack.Controller.code : Code Basis.standard 9

Fixed adaptive code: replace a popped zero using another pair of stack operations.

def Cslib.WordRAM.Stack.Controller.client (w n : ℕ) : (spec w 1).Client ℕ

The abstract controller observes its first pop before deciding whether to call again.

theorem Cslib.WordRAM.Stack.Controller.roundTrip_exec {w n : ℕ} {x : Data 9} (h3 : Fits w 3) (hr : Rep w 2 1 [] x) (hn : x.regs arg = n) : ∃ (y : Data 9), Exec w roundTrip x y 21 ∧ Rep w 2 1 [] y ∧ y.regs out = n

A full push/pop round trip costs twenty-one instructions, including argument delivery.

theorem Cslib.WordRAM.Stack.Controller.setup_exec {w n : ℕ} (h3 : Fits w 3) (hn : InputFits w [n]) : ∃ (x : Data 9), Exec w setup (Data.init [n]) x 4 ∧ Rep w 2 1 [] x ∧ x.regs arg = n

Initialize the empty representation and load the input in four actual instructions.

theorem Cslib.WordRAM.Stack.Controller.execute {w n : ℕ} (h3 : Fits w 3) (hn : InputFits w [n]) : ∃ (y : Data 9), Exec w code (Data.init [n]) y (if n = 0 then 48 else 28) ∧ Rep w 2 1 [] y ∧ y.regs out = max n 1

The exact controller time includes setup, adaptive control and argument preparation. The final halt is added separately by Exec.executes.

theorem Cslib.WordRAM.Stack.Controller.runClient_client (w n : ℕ) : ((spec w 1).runClient [] (client w n)).1 = max n 1 ∧ ((spec w 1).runClient [] (client w n)).2.1 = []

The abstract client returns the same positive value and restores the empty stack.

theorem Cslib.WordRAM.Stack.Controller.client_valid {w n : ℕ} (h3 : Fits w 3) (hn : InputFits w [n]) : (spec w 1).ValidHistory [] ((spec w 1).runClient [] (client w n)).2.2

Both adaptive histories respect the one-cell capacity and word bounds.

theorem Cslib.WordRAM.Stack.Controller.refines {w n : ℕ} (h3 : Fits w 3) (hn : InputFits w [n]) : Refines w (fun (s : (spec w 1).State) (x : Data 9) => s = [] ∧ x = Data.init [n]) (client w n) (fun (a : ℕ) (s : (spec w 1).State) (y : Data 9) => Rep w 2 1 s y ∧ y.regs out = a) (fun (x : (spec w 1).State) (x_1 : Data 9) => if n = 0 then 48 else 28) code

The full fixed controller refines the adaptive client, including setup and argument work.

theorem Cslib.WordRAM.Stack.Controller.executes {w n : ℕ} (h3 : Fits w 3) (hn : InputFits w [n]) : Executes w (code.program out) (State.init [n]) (max n 1) ((if n = 0 then 48 else 28) + 1)

A single flat program computes the positive replacement, including its final halt.

theorem Cslib.WordRAM.Stack.Controller.executes_le {w n : ℕ} (h3 : Fits w 3) (hn : InputFits w [n]) : ∃ t ≤ 49, Executes w (code.program out) (State.init [n]) (max n 1) t

The shared refinement API produces a uniform forty-nine-instruction certificate.

def Cslib.WordRAM.Stack.Controller.positive (n : ℕ) : ℕ

The word-valued function computed by the adaptive stack controller.

theorem Cslib.WordRAM.Stack.Controller.computesInTime : (code.program out).ComputesInTime (fun (x n : ℕ) => [n]) (fun (x x_1 : ℕ) => 49) (fun (x w : ℕ) => 2 ≤ w) positive

Uniform computation at every fitting word size of at least two bits.

theorem Cslib.WordRAM.Stack.Controller.positive_polytime : UniformComputableInPolyTime Basis.standard positive (fun (x n : ℕ) => [n]) id

The same fixed controller has a constant, hence polynomial, RAM instruction bound. The size parameter is the numerical magnitude n; the admissible width is logarithmic in it.

theorem Cslib.WordRAM.Stack.Controller.input_fits (n : ℕ) : InputFits (logWidth 2 n) [n]

The logarithmic threshold used by the function certificate fits every input, so the uniform computation theorem has a successful execution for every natural input.