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.
Imports
open Copy;
Table of Contents

Types

Stack

(type) linear
linear type Stack a

StackPop

(type) linear
A pop token owns its removed element and the successor stack.
linear type StackPop 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 (1 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 (1 p : (StackPop a)) : a

pop_stack

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

peek

Peek at the top without removing it.
def peek (_inst5626 : (Copy a)) (borrow s : (Stack a) | stack_size s > 0) : a

discard

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

with_pop

Consume the token once and pass both observations to a linear continuation.
def with_pop (_inst5627 : (Copy a)) (1 token : (StackPop a)) (1 consume : (value : a) → (1 handle : (Stack a) | stack_size handle = pop_size token) → b) : b

with_pop_owned

Non-consuming observations; finish with pop/discard as appropriate. Transfer linear elements instead of copying observations.
def with_pop_owned (1 token : (StackPop a)) (1 consume : (1 value : a) → (1 handle : (Stack a) | stack_size handle = pop_size token) → b) : b

length

Non-consuming observations; finish with pop/discard as appropriate.
def length (borrow s : (Stack a)) : {n : Int | n = stack_size s && n ≥ 0}

empty

def empty (borrow s : (Stack a)) : {b : Bool | b = (stack_size s = 0)}

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