The functions take Array UInt64. Counts and indices use UInt64, and word arithmetic wraps
modulo 2^64. Each linked family has native definitions in Program and generated execution
proofs in Compiled.
| Family | Functions and behavior |
|---|---|
| Search | count counts occurrences. firstAbove returns the first index above a limit and a Boolean indicating success. firstZero searches a specified prefix and returns the prefix length when no zero occurs. Its default read returns zero past the array's end. |
| Filter | removeAll removes matching words while preserving order. below collects at most a specified count of words below a limit. clearUntil zeros the prefix preceding the first matching word. |
| Repeat | repeated concatenates a specified number of copies. |
| Range | evens n constructs the n words 2 * i. |
| Word operations | scaled multiplies every word by a scalar. |
removeAll searches and shifts repeatedly, taking quadratic time. The compiler examples retain
their ownership and allocation tests. The search proof
proves the first-zero prefix property used by the removal example.