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 + m) for concatenation. ── Linear (QTT) discipline ────────────────────────────────────────────── ``Array`` is a ``linear type``: an array is a *unique* value, so every owner 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. Every owner is consumed **exactly once**. Read-only parameters use ``(borrow arr: ...)`` and return ownership to the caller after the call. Borrowing neither consumes the array nor permits aliasing it. Mutations consume the old owner and return its successor. ``set`` updates the same backing list in O(1); ``mk_concat`` and ``reversed`` allocate. Shape and numeric queries borrow. ``get`` / ``head`` also borrow, requiring Copy elements so a read cannot duplicate a nested linear handle. Use ``take`` / ``take_head`` to move an element and end ownership of its source. ``copy`` requires Copy elements and returns a linear ArrayPair, unpacked once with ``with_pair``. After a final read, call ``dispose`` explicitly, or use ``consume observer arr`` to observe and finish a pipeline.
Imports
open Copy;
Table of Contents

Types

Array

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

ArrayPair

(type) linear
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``. Wrappers own their arrays and must themselves be consumed exactly once. Use the continuation helpers to recover both fields in one consumption.
linear type ArrayPair a

ArrayGet

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

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Array (linear · opaque · mk*)

mk_empty

A Unit argument makes each empty array a fresh allocation.
def mk_empty (_ : Unit) : {xs : (Array ({_r77 : a | p _r77})) | size xs = 0}

mk_repeat

The repeated value is unrestricted: linear resources cannot be duplicated.
def mk_repeat (n : Int | n ≥ 0) (v : a) : {xs : (Array ({x : a | x = v})) | size xs = n}

mk_1

Fixed-arity constructors preserve argument order and the element predicate.
def mk_1 (1 x0 : a | p x0) : {xs : (Array ({_r79 : a | p _r79})) | size xs = 1}

mk_2

def mk_2 (1 x0 : a | p x0) (1 x1 : a | p x1) : {xs : (Array ({_r82 : a | p _r82})) | size xs = 2}

mk_4

def mk_4 (1 x0 : a | p x0) (1 x1 : a | p x1) (1 x2 : a | p x2) (1 x3 : a | p x3) : {xs : (Array ({_r87 : a | p _r87})) | size xs = 4}

mk_8

def mk_8 (1 x0 : a | p x0) (1 x1 : a | p x1) (1 x2 : a | p x2) (1 x3 : a | p x3) (1 x4 : a | p x4) (1 x5 : a | p x5) (1 x6 : a | p x6) (1 x7 : a | p x7) : {xs : (Array ({_r96 : a | p _r96})) | size xs = 8}

mk_16

def mk_16 (1 x0 : a | p x0) (1 x1 : a | p x1) (1 x2 : a | p x2) (1 x3 : a | p x3) (1 x4 : a | p x4) (1 x5 : a | p x5) (1 x6 : a | p x6) (1 x7 : a | p x7) (1 x8 : a | p x8) (1 x9 : a | p x9) (1 x10 : a | p x10) (1 x11 : a | p x11) (1 x12 : a | p x12) (1 x13 : a | p x13) (1 x14 : a | p x14) (1 x15 : a | p x15) : {xs : (Array ({_r113 : a | p _r113})) | size xs = 16}

mk_32

def mk_32 (1 x0 : a | p x0) (1 x1 : a | p x1) (1 x2 : a | p x2) (1 x3 : a | p x3) (1 x4 : a | p x4) (1 x5 : a | p x5) (1 x6 : a | p x6) (1 x7 : a | p x7) (1 x8 : a | p x8) (1 x9 : a | p x9) (1 x10 : a | p x10) (1 x11 : a | p x11) (1 x12 : a | p x12) (1 x13 : a | p x13) (1 x14 : a | p x14) (1 x15 : a | p x15) (1 x16 : a | p x16) (1 x17 : a | p x17) (1 x18 : a | p x18) (1 x19 : a | p x19) (1 x20 : a | p x20) (1 x21 : a | p x21) (1 x22 : a | p x22) (1 x23 : a | p x23) (1 x24 : a | p x24) (1 x25 : a | p x25) (1 x26 : a | p x26) (1 x27 : a | p x27) (1 x28 : a | p x28) (1 x29 : a | p x29) (1 x30 : a | p x30) (1 x31 : a | p x31) : {xs : (Array ({_r146 : a | p _r146})) | size xs = 32}

mk_concat

Consume both inputs; preserve their order, element predicate, and total size.
def mk_concat (1 xs : (Array ({_r147 : a | p _r147}))) (1 ys : (Array ({_r148 : a | p _r148}))) : {zs : (Array ({_r149 : a | p _r149})) | size zs = size xs + size ys}

Functions

functools

def functools : Unit

length

A scoped read: the caller retains ownership and may update the array later.
def length (borrow arr : (Array a)) : {n : Int | n = size arr}

dispose

End ownership when no further consuming operation is needed.
def dispose (1 arr : (Array a)) : Unit

mk_empty

A Unit argument makes each empty array a fresh allocation.
def mk_empty (_ : Unit) : {xs : (Array ({_r77 : a | p _r77})) | size xs = 0}

mk_repeat

The repeated value is unrestricted: linear resources cannot be duplicated.
def mk_repeat (n : Int | n ≥ 0) (v : a) : {xs : (Array ({x : a | x = v})) | size xs = n}

mk_1

Fixed-arity constructors preserve argument order and the element predicate.
def mk_1 (1 x0 : a | p x0) : {xs : (Array ({_r79 : a | p _r79})) | size xs = 1}

mk_2

def mk_2 (1 x0 : a | p x0) (1 x1 : a | p x1) : {xs : (Array ({_r82 : a | p _r82})) | size xs = 2}

mk_4

def mk_4 (1 x0 : a | p x0) (1 x1 : a | p x1) (1 x2 : a | p x2) (1 x3 : a | p x3) : {xs : (Array ({_r87 : a | p _r87})) | size xs = 4}

mk_8

def mk_8 (1 x0 : a | p x0) (1 x1 : a | p x1) (1 x2 : a | p x2) (1 x3 : a | p x3) (1 x4 : a | p x4) (1 x5 : a | p x5) (1 x6 : a | p x6) (1 x7 : a | p x7) : {xs : (Array ({_r96 : a | p _r96})) | size xs = 8}

mk_16

def mk_16 (1 x0 : a | p x0) (1 x1 : a | p x1) (1 x2 : a | p x2) (1 x3 : a | p x3) (1 x4 : a | p x4) (1 x5 : a | p x5) (1 x6 : a | p x6) (1 x7 : a | p x7) (1 x8 : a | p x8) (1 x9 : a | p x9) (1 x10 : a | p x10) (1 x11 : a | p x11) (1 x12 : a | p x12) (1 x13 : a | p x13) (1 x14 : a | p x14) (1 x15 : a | p x15) : {xs : (Array ({_r113 : a | p _r113})) | size xs = 16}

mk_32

def mk_32 (1 x0 : a | p x0) (1 x1 : a | p x1) (1 x2 : a | p x2) (1 x3 : a | p x3) (1 x4 : a | p x4) (1 x5 : a | p x5) (1 x6 : a | p x6) (1 x7 : a | p x7) (1 x8 : a | p x8) (1 x9 : a | p x9) (1 x10 : a | p x10) (1 x11 : a | p x11) (1 x12 : a | p x12) (1 x13 : a | p x13) (1 x14 : a | p x14) (1 x15 : a | p x15) (1 x16 : a | p x16) (1 x17 : a | p x17) (1 x18 : a | p x18) (1 x19 : a | p x19) (1 x20 : a | p x20) (1 x21 : a | p x21) (1 x22 : a | p x22) (1 x23 : a | p x23) (1 x24 : a | p x24) (1 x25 : a | p x25) (1 x26 : a | p x26) (1 x27 : a | p x27) (1 x28 : a | p x28) (1 x29 : a | p x29) (1 x30 : a | p x30) (1 x31 : a | p x31) : {xs : (Array ({_r146 : a | p _r146})) | size xs = 32}

mk_concat

Consume both inputs; preserve their order, element predicate, and total size.
def mk_concat (1 xs : (Array ({_r147 : a | p _r147}))) (1 ys : (Array ({_r148 : a | p _r148}))) : {zs : (Array ({_r149 : a | p _r149})) | size zs = size xs + size ys}

empty

True when the array is empty. Borrows it without transferring ownership.
def empty (borrow 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 (_inst150 : (Copy a)) (1 arr : (Array ({_r151 : a | p _r151}))) : {pr : (ArrayPair ({_r152 : a | p _r152})) | pair_size pr = size arr}

fst_array

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

snd_array

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

get_at

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

got_value

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

got_array

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

with_pair

Consume a copied pair once; both buffers have independent storage.
def with_pair (1 token : (ArrayPair ({_r164 : a | p _r164}))) ( 1 consume : (1 left : (Array ({_r165 : a | p _r165})) | size left = pair_size token) → (1 right : (Array ({_r166 : a | p _r166})) | size right = pair_size token) → {_r167 : b | q _r167} ) : {_r168 : b | q _r168}

with_get

Reading an element and continuing with the array uses one wrapper.
def with_get (1 token : (ArrayGet ({_r169 : a | p _r169}))) ( 1 consume : (value : a | p value) → (1 arr : (Array ({_r171 : a | p _r171})) | size arr = got_size token) → {_r172 : b | q _r172} ) : {_r173 : b | q _r173}

get

Indexed observation; the element is copyable and still satisfies ``p``.
def get (_inst174 : (Copy a)) (borrow arr : (Array ({_r175 : a | p _r175}))) (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 old owner and returns the updated owner of the same storage.
def set (1 arr : (Array ({_r176 : a | p _r176}))) (i : Int | i ≥ 0 && i < size arr) (1 x : a | p x) : {r : (Array ({_r177 : a | p _r177})) | size r = size arr}

head

First element of a non-empty array. Its predicate must come from the input; a free output predicate would let callers prove arbitrary facts. Borrows it.
def head (_inst178 : (Copy a)) (borrow arr : (Array ({_r179 : a | p _r179})) | size arr > 0) : {v : a | p v}

reversed

Reversed copy; length is preserved. Consumes the array linearly.
def reversed (1 arr : (Array ({_r180 : a | p _r180}))) : {r : (Array ({_r181 : a | p _r181})) | 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 (_inst182 : (Copy a)) (f : (x : a | p x) → {w : b | q w}) (1 arr : (Array ({_r183 : a | p _r183}))) : {r : (Array ({_r184 : b | q _r184})) | size r = size arr}

filter

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

reduce

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

sum

Sum of an Int array. Borrows the array.
def sum (borrow arr : (Array Int)) : Int

mean

Mean of a Float array. Borrows the array.
def mean (borrow arr : (Array Float)) : Float

imap

Index-aware map: ``f`` receives ``(index, element)``. Length preserved.
def imap (_inst190 : (Copy a)) (f : (i : Int) → (x : a | p x) → {w : b | q w}) (1 arr : (Array ({_r191 : a | p _r191}))) : {r : (Array ({_r192 : b | q _r192})) | size r = size arr}

zipWith

Pairwise zip-with; both arrays must share length ``size``.
def zipWith (_inst193 : (Copy a)) (_inst194 : (Copy b)) (f : (x : a | p x) → (y : b | q y) → {z : c | r z}) (1 xs : (Array ({_r195 : a | p _r195}))) (1 ys : (Array ({_r196 : b | q _r196})) | size ys = size xs) : {out : (Array ({_r197 : c | r _r197})) | size out = size xs}

count

Count copyable elements satisfying ``f``. Borrows the array.
def count (_inst198 : (Copy a)) (f : (x : a | p x) → Bool) (borrow arr : (Array ({_r199 : a | p _r199}))) : {n : Int | n ≥ 0 && n ≤ size arr}

scale

Scale every Float element by ``k``. Consumes the array.
def scale (k : Float) (1 arr : (Array Float)) : {r : (Array Float) | size r = size arr}

vadd

Elementwise add of two equal-length Float arrays.
def vadd (1 xs : (Array Float)) (1 ys : (Array Float) | size ys = size xs) : {r : (Array Float) | size r = size xs}

take

Move an element out, ending ownership of the source array.
def take (1 arr : (Array ({_r200 : a | p _r200}))) (i : Int | i ≥ 0 && i < size arr) : {v : a | p v}

take_head

def take_head (1 arr : (Array ({_r201 : a | p _r201})) | size arr > 0) : {v : a | p v}

consume

Explicitly end ownership after a borrowed observation. Useful at pipeline ends.
def consume (observe : (borrow xs : (Array ({_r202 : a | p _r202}))) → {_r203 : b | q _r203}) (1 arr : (Array ({_r204 : a | p _r204}))) : {_r205 : b | q _r205}

map_owned

Move every element into a consuming callback, including nested linear arrays.
def map_owned (f : (1 x : a | p x) → {_r207 : b | q _r207}) (1 arr : (Array ({_r208 : a | p _r208}))) : {r : (Array ({_r209 : b | q _r209})) | size r = size arr}

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`` 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

pair_size

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