Stack

Linear stack with a ``size`` ghost (LiquidJava ``Stack`` exercise). ``push`` increases size; ``pop`` / ``peek`` require ``size > 0``. The stack is multiplicity-1: each op consumes the handle and returns the next state. ``discard`` frees an empty stack.
Table of Contents

Types

Stack

(type) linear
linear type Stack a

StackPop

(type)
Opaque tokens so ``pop`` / ``peek`` / ``len_of`` can return a value and the recovered stack without breaking linearity.
type StackPop a

StackPeek

(type)
type StackPeek a

StackLen

(type)
type StackLen a

Functions

new_stack

Empty stack. Use as ``Stack.new_stack{Int} unit``.
def new_stack (_ : Unit) : {s : Stack a | stack_size s = 0}

push

Push one element (size + 1).
def push (x : a) (1 s : Stack a) : {out : Stack a | stack_size out = stack_size s + 1}

pop

Pop the top; requires a non-empty stack.
def pop (1 s : Stack a | stack_size s > 0) : {p : StackPop a | pop_size p = stack_size s - 1}

pop_value

def pop_value (p : StackPop a) : a

pop_stack

def pop_stack (p : StackPop a) : {s : Stack a | stack_size s = pop_size p}

peek

Peek at the top without removing it.
def peek (1 s : Stack a | stack_size s > 0) : {p : StackPeek a | peek_size p = stack_size s}

peek_value

def peek_value (p : StackPeek a) : a

peek_stack

def peek_stack (p : StackPeek a) : {s : Stack a | stack_size s = peek_size p}

len_of

Observe length and recover the stack.
def len_of (1 s : Stack a) : {l : StackLen a | held_size l = stack_size s}

len_value

def len_value (l : StackLen a) : {n : Int | n = held_size l && n ≥ 0}

len_stack

def len_stack (l : StackLen a) : {s : Stack a | stack_size s = held_size l}

discard

Drop an empty stack.
def discard (1 s : Stack a | stack_size s = 0) : Unit

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

stack_size

uninterpreted
def stack_size : (s : Stack a) → Int

pop_size

uninterpreted
def pop_size : (p : StackPop a) → Int

peek_size

uninterpreted
def peek_size : (p : StackPeek a) → Int

held_size

uninterpreted
def held_size : (l : StackLen a) → Int