Deque

Linear double-ended queue with a ``size`` ghost (LiquidJava ``ArrayDeque``). Ends support push/pop/peek; pop and peek require ``size > 0``. The deque is multiplicity-1. ``discard`` frees an empty deque.
Imports
open Copy;
Table of Contents

Types

Deque

(type) linear
linear type Deque a

DequePop

(type) linear
linear type DequePop a

Functions

new_deque

Empty deque. Use as ``Deque.new_deque{Int} unit``.
def new_deque (_ : Unit) : {d : (Deque a) | deque_size d = 0}

push_back

def push_back (1 x : a) (1 d : (Deque a)) : {out : (Deque a) | deque_size out = deque_size d + 1}

push_front

def push_front (1 x : a) (1 d : (Deque a)) : {out : (Deque a) | deque_size out = deque_size d + 1}

pop_back

def pop_back (1 d : (Deque a) | deque_size d > 0) : {p : (DequePop a) | pop_size p = deque_size d - 1}

pop_front

def pop_front (1 d : (Deque a) | deque_size d > 0) : {p : (DequePop a) | pop_size p = deque_size d - 1}

pop_value

def pop_value (1 p : (DequePop a)) : a

pop_deque

def pop_deque (1 p : (DequePop a)) : {d : (Deque a) | deque_size d = pop_size p}

peek_back

def peek_back (_inst2062 : (Copy a)) (borrow d : (Deque a) | deque_size d > 0) : a

peek_front

def peek_front (_inst2063 : (Copy a)) (borrow d : (Deque a) | deque_size d > 0) : a

discard

def discard (1 d : (Deque a) | deque_size d = 0) : Unit

with_pop

Consume the token once and pass both observations to a linear continuation.
def with_pop (_inst2064 : (Copy a)) (1 token : (DequePop a)) (1 consume : (value : a) → (1 handle : (Deque a) | deque_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 : (DequePop a)) (1 consume : (1 value : a) → (1 handle : (Deque a) | deque_size handle = pop_size token) → b) : b

length

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

empty

def empty (borrow d : (Deque a)) : {b : Bool | b = (deque_size d = 0)}

Uninterpreted

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

deque_size

uninterpreted
def deque_size : (d : (Deque a)) → Int

pop_size

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