Array

Flat, contiguous, native-backed sequence with random access. ``Array`` is an opaque type parameterised by: * its element type ``a``; * an abstract refinement ``p`` (Liquid Haskell-style ``data Array a <p>``) that every element of the array satisfies. The underlying storage is a Python list, so operations are O(1) for indexed access and O(n) for prepend. ── Linear (QTT) discipline ────────────────────────────────────────────── ``Array`` is a ``linear type``: an array is a *unique* value, so every binder that holds one must be declared at multiplicity 1 — ``let 1 a := ...`` for a local, ``(1 arr: ...)`` for a parameter. Omitting the ``1`` is an error, not a silent escape hatch. Consequently every array is consumed **exactly once**: using it twice (which would alias the buffer) or dropping it without consuming it are both rejected. Because uniqueness is statically guaranteed, the native bodies are free to mutate the backing list in place — there is no other observer that a mutation could surprise. (The bodies below stay purely functional, so the runtime behaviour is unchanged.) Operations come in two flavours: * **Transformers** (``append``, ``cons``, ``set``, ``reversed``, ``map``, ``filter``) consume the array and return a fresh one — bind the result to the next ``let 1`` and keep going. * **Readers** (``length``, ``get``, ``head``, ``sum``, ``reduce``, ``empty``) also consume the array, because reading it uses up the one reference. Terminal reads therefore need nothing special: ``length #[5, 6, 7]`` is fine. To read a value *and carry on* with the array, use ``get_at`` / ``len_of``: they hand back an opaque result carrying both the value read and the array itself, which ``got_value`` / ``got_array`` (resp. ``len_value`` / ``len_array``) project. Both wrappers are refinement-parametric and thread the ``size`` measure, so nothing is lost by the round trip. When you need two genuinely independent arrays — to branch a computation in two — call ``copy``: it consumes the array once and hands back two arrays packaged in an ``ArrayPair`` (projected with ``fst_array`` / ``snd_array``), each with the element refinement and length preserved.
Table of Contents

Types

Array

(type) linear
linear type Array a forall <p:(_ : a) → Bool → Bool>

ArrayPair

(type)
Opaque pair of arrays, returned by ``copy``. Backed by a Python 2-tuple; kept self-contained (rather than reusing the ``Pair`` library) so that ``Array`` has no further imports to drag through every ``open Array``. The wrappers below are deliberately *not* linear: they are inert values whose only purpose is to be projected. The arrays they carry re-enter the linear discipline as soon as a projection is bound to a ``let 1``.
type ArrayPair a

ArrayGet

(type)
Result of ``get_at``: the element read, plus the array it was read from.
type ArrayGet a

ArrayLen

(type)
Result of ``len_of``: the length, plus the array it was measured from.
type ArrayLen a

Functions

functools

def functools : Unit

length

Length of the array. Consumes it; use ``len_of`` to keep the array.
def length (1 arr : Array a) : {n : Int | n = size arr}

new

Empty array — a fresh, uniquely-owned buffer.
def new (_ : Unit) : {arr : Array a | size arr = 0}

empty

True when the array is empty. Consumes it.
def empty (1 arr : Array a) : {b : Bool | b = size arr = 0}

copy

Explicit copy: consume the single linear reference and return two independent arrays — the original buffer plus a fresh physical duplicate. At run time both halves hold the same elements as the input; this is the only way to turn one unique reference into two, to branch a linear computation. The element refinement ``<p>`` rides on the element type of the pair and the length is threaded by the ``pair_size`` measure, so both projections come back fully specified.
def copy (1 arr : Array ({_r77 : a | p _r77})) : {pr : ArrayPair ({_r78 : a | p _r78}) | pair_size pr = size arr}

fst_array

Left projection of a ``copy`` — the original buffer.
def fst_array (pr : ArrayPair ({_r79 : a | p _r79})) : {r : Array ({_r80 : a | p _r80}) | size r = pair_size pr}

snd_array

Right projection of a ``copy`` — the fresh duplicate.
def snd_array (pr : ArrayPair ({_r81 : a | p _r81})) : {r : Array ({_r82 : a | p _r82}) | size r = pair_size pr}

get_at

def get_at (1 arr : Array ({_r83 : a | p _r83})) (i : Int | i ≥ 0 && i < size arr) : {g : ArrayGet ({_r84 : a | p _r84}) | got_size g = size arr}

got_value

The element read by ``get_at``; still known to satisfy ``p``.
def got_value (g : ArrayGet ({_r85 : a | p _r85})) : {_r86 : a | p _r86}

got_array

The array ``get_at`` read from, with its length intact.
def got_array (g : ArrayGet ({_r87 : a | p _r87})) : {r : Array ({_r88 : a | p _r88}) | size r = got_size g}

len_of

def len_of (1 arr : Array ({_r89 : a | p _r89})) : {l : ArrayLen ({_r90 : a | p _r90}) | held_size l = size arr}

len_value

The length measured by ``len_of``.
def len_value (l : ArrayLen ({_r91 : a | p _r91})) : {n : Int | n = held_size l}

len_array

The array ``len_of`` measured, with its length intact.
def len_array (l : ArrayLen ({_r92 : a | p _r92})) : {r : Array ({_r93 : a | p _r93}) | size r = held_size l}

append

Append an element to the back.
def append (1 arr : Array a) (1 x : a | p x) : {r : Array a | size r = size arr + 1}

cons

Prepend an element to the front; the value must satisfy the refinement ``p``. Consumes the array linearly and returns a fresh one, one element longer.
def cons (1 arr : Array a) (1 x : a | p x) : {r : Array a | size r = size arr + 1}

get

Indexed read; the result is known to satisfy ``p``. Consumes the array — use ``get_at`` to read and keep it.
def get (1 arr : Array a) (i : Int | i ≥ 0 && i < size arr) : {v : a | p v}

set

Indexed write; preserves length, and the written value must satisfy ``p``. Consumes the array linearly and returns the fresh, updated array.
def set (1 arr : Array a) (i : Int | i ≥ 0 && i < size arr) (1 x : a | p x) : {r : Array a | size r = size arr}

head

First element of a non-empty array. Consumes the array.
def head (1 arr : Array a | size arr > 0) : {v : a | p v}

reversed

Reversed copy; length is preserved. Consumes the array linearly.
def reversed (1 arr : Array a) : {r : Array a | size r = size arr}

map

Map a function across the array; length is preserved and the result refinement ``q`` is pushed through ``f``. Consumes the array linearly.
def map (f : (x : a | p x) → {w : b | q w}) (1 arr : Array a) : {r : Array b | size r = size arr}

filter

Filter an array by ``f``; the length never grows. Consumes the array linearly.
def filter (f : (x : a | p x) → Bool) (1 arr : Array a) : {r : Array a | size r ≤ size arr}

reduce

Right fold: ``reduce f z [x1, ..., xn] == f x1 (f x2 (... (f xn z)))``. Consumes the array.
def reduce (f : (x : a | p x) → (acc : b) → b) (z : b) (1 arr : Array a) : b

sum

Sum of an Int array. Consumes the array.
def sum (1 arr : Array Int) : Int

Uninterpreted

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

size

uninterpreted
Abstract length measure.
def size : (arr : Array a) → Int

got_size

uninterpreted
Length carried by an ``ArrayGet`` / ``ArrayLen`` wrapper — the ``size`` of the array inside it. Lets the projections restate the length they were built with, so threading an array through a read loses nothing.
def got_size : (g : ArrayGet a) → Int

held_size

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

pair_size

uninterpreted
Common length of the two arrays inside an ``ArrayPair``.
def pair_size : (pr : ArrayPair a) → Int