# sysp language reference (v0)

sysp is a small systems language written as typed s-expressions. Every program is type-checked,
ownership-checked and **verified**: array bounds, integer overflow, division by zero and every
contract are proven by an SMT solver at compile time, or the program is rejected. Verified programs
compile to C11 with no runtime checks.

This reference is complete: anything not described here does not exist. Every example below is
checked automatically.

## 1. Programs

A program is a sequence of `struct`, `fn` and `const` (§2) definitions. Names may contain letters, digits, `_`
and `-` (`ring-push` becomes `ring_push` in C). `;` starts a comment.

```sysp
(struct Point (x i64) (y i64))

(fn manhattan ((p (ref Point))) i64
  (effects)
  (requires (and (<= -1000000 (. p x)) (<= (. p x) 1000000)))
  (requires (and (<= -1000000 (. p y)) (<= (. p y) 1000000)))
  (ensures (>= result 0))
  (let ax (if (< (. p x) 0) (- 0 (. p x)) (. p x)))
  (let ay (if (< (. p y) 0) (- 0 (. p y)) (. p y)))
  (+ ax ay))
```

A function is `(fn name (params...) return-type clauses... body...)`:

- **Clauses**, in any order, right after the return type: `(effects e...)` is **mandatory**
  (write `(effects)` for none); any number of `(requires cond)` and `(ensures cond)`.
- **Body**: one or more expressions; the value of the last one is the result. A `unit` function's
  body must end in a `unit` expression.

## 2. Types

| Type | Meaning |
|---|---|
| `i64` | 64-bit signed integer |
| `u8` | byte, 0..255 |
| `w8` `w16` `w32` `w64` | words: bit patterns with bitwise operators and wrapping arithmetic (§20) |
| `bool` | `true` / `false` |
| `unit` | no value; written `unit` |
| `never` | return type of a function that does not return (§18) |
| `(buf T)` | owned, fixed-length, heap-allocated buffer of `i64`, `u8` or a word |
| `Name` | a struct, or an enum (§21) |

There are no implicit conversions. Integer literals take the type their context expects (`i64`
by default); a literal must fit its type, and may be written in hex (`0xff`), binary
(`0b1010`) or as a character, its byte: `#\(` is 40, `#\0` is 48; `#\space`, `#\newline`,
`#\return`, `#\tab`, `#\nul`, `#\del`, `#\backspace` and `#\escape` are named. Each is only a
spelling: `(== c #\()` and `(== c 40)` are the same program, and the formatter keeps yours. Convert with `(as T e)` between `i64`, `u8` and the words; the value must be proven
to fit `T` (V009), so `as` never changes a value.

A **constant** is a name for an integer literal, defined at top level by `(const name value)`:
every use of it is that literal, of the type its context expects. Its value is a literal,
another constant, or `(op a b ...)` with `+ - * / % & | ^ << >>`, computed exactly when
compiling. A binding may take a constant's name, and inside its scope means the binding (§15).

```sysp
(const page (* 4 kib))
(const kib 1024)

(fn page-start ((addr i64)) i64
  (effects)
  (requires (<= 0 addr))
  (ensures (and (<= 0 result) (== (% result page) 0)))
  (- addr (% addr page)))
```

## 3. Parameters and ownership

Every parameter has a mode:

| Parameter | Meaning |
|---|---|
| `(x T)` | owned: the caller gives `x` away |
| `(x (ref T))` | shared borrow: read-only for the call |
| `(x (mut T))` | mutable borrow: may be changed; the caller sees the changes |

Buffers, structs that contain buffers, and `resource` structs are **resources**. Each owned
resource must be used **exactly once** on every path: passed to an owned parameter, returned,
stored with `new`, destructured, or freed with `free`. Borrows are never stored or returned.

- A resource cannot be used after it was moved; it cannot be consumed inside a loop it was
  created outside of; both branches of an `if` must consume the same resources.
- A `ref` or `mut` argument must be a *place*: a variable or a field path like `(. r data)`.
- The same variable may not be passed twice to one call if either use is `mut`, unless the two
  are different fields of it (038): `(f (. ns a) (. ns b))` lends two places that share nothing,
  while `(. ns a)` and `ns`, or `(. ns a)` twice, overlap.
- Resources cannot be held in `var`s or overwritten with `set`.

```sysp
(fn sum-and-free ((b (buf i64))) i64
  (effects alloc)
  (requires (<= (len b) 1000))
  (requires
    (forall ((k i64))
      (=> (and (<= 0 k) (< k (len b))) (and (<= 0 (get b k)) (<= (get b k) 1000)))))
  (var s 0)
  (for (i 0 (len b))
    (invariant (and (<= 0 s) (<= s (* i 1000))))
    (set s (+ s (get b i))))
  (free b)
  s)
```

Using a buffer after freeing it is rejected:

<!-- expect: O001 -->
```sysp
(fn bad ((b (buf i64))) i64
  (effects alloc)
  (free b)
  (len b))
```

## 4. Effects

There are two effects. `alloc` is required to use `buf-new` or `free`; `io` marks access to
devices (through `extern fn`s, §12). A function may only call functions whose effects it declares.

## 5. Expressions

| Form | Meaning |
|---|---|
| `(let x e)` | immutable binding, visible until the end of the enclosing body/`do` |
| `(let (S a b ...) e)` | destructure an owned struct into one name per field, in field order |
| `(var x e)` | mutable binding (not for resources) |
| `(set x e)`, `(set (. p f) e)` | assignment to a `var`, a `mut` parameter, or a field of one |
| `(do e1 ... en)` | sequence; value of `en` |
| `(if c a b)` | both branches have the same type; `(if c a)` has type `unit` |
| `(while c (invariant i)* (decreases d)? body...)` | loop; type `unit` (`never` if `c` is `true` and nothing in it breaks) |
| `(for (i lo hi) (invariant e)* body...)` | `body` with `i` = `lo` … `hi - 1`; `lo` and `hi` are evaluated once; `i` is an `i64` constant inside the loop, whose bounds the verifier knows; type `unit` |
| `(cond (c body...) ... (else body...))` | the first clause whose `c` holds; without `else`, type `unit` |
| `(return e)`, `(return)` | leave the function |
| `(break)` | leave the innermost `while` or `for` (§24) |
| `(assert c)` | proven at compile time; no runtime cost |
| `(assume c)` | trusted without proof; reported as warning W001 in every build |
| `(+ a b)` `(- a b)` `(* a b)` `(/ a b)` `(% a b)` | integer arithmetic, both operands of the same type; `/` and `%` truncate toward zero as in C |
| `(< a b)` `(<= a b)` `(> a b)` `(>= a b)` `(== a b)` `(!= a b)` | comparisons |
| `(and a b ...)` `(or a b ...)` `(=> a b)` `(not a)` | short-circuit logic |
| `(len b)` `(get b i)` `(put b i v)` | buffer length, read, write (`put` needs a mutable place) |
| `(buf-new i64 n)` `(buf-new u8 n)` | new zero-filled buffer (needs `alloc`) |
| `(free b)` | release a buffer (needs `alloc`) |
| `(new S (f1 e1) ...)` | construct a struct; every field exactly once |
| `(. s f)` | field read |
| `(f a b ...)` | call |
| `(replace p v)` | put `v` into the mutable place `p` and return the old value (owned) |
| `"text"` | string literal: a read-only `(buf u8)`, only as an argument to a `(ref (buf u8))` parameter; escapes `\n \t \\ \" \0` |
| `?name` | a typed hole (see §8) |

Arithmetic operators take exactly two operands; nest them for more. `and` and `or` take two or
more.

## 6. Specifications

`requires`, `ensures`, `invariant`, `decreases`, `assert` and `assume` take **specification
expressions**: the expression forms above without effects (no `let`, `set`, `put`, calls, ...),
plus:

| Form | Meaning |
|---|---|
| `result` | the function's return value (in `ensures`) |
| `(old e)` | value of `e` on entry to the function (in `ensures`, invariants, assertions) |
| `(forall ((k i64) ...) c)` `(exists ((k i64) ...) c)` | quantifiers over integers |

**Predicates** name a specification so it is written once. `(pred name ((x T) ...) body)` is a
top-level item whose body is a specification of type `bool`; it may call other predicates but
not itself. Predicates can only be used in specifications and produce no code.

```sysp
(struct Counter (hits i64) (limit i64))

(pred counter-ok ((c Counter))
  (and (<= 0 (. c hits)) (<= (. c hits) (. c limit)) (<= (. c limit) 1000000)))

(fn bump ((c (mut Counter))) bool
  (effects)
  (requires (counter-ok c))
  (ensures (counter-ok c))
  (ensures (=> result (== (. c hits) (+ (. (old c) hits) 1))))
  (if (< (. c hits) (. c limit)) (do (set (. c hits) (+ (. c hits) 1)) true) false))
```

Specifications use mathematical integers, so they cannot overflow. `(get b k)` in a specification
has no bounds requirement; guard it with the range of `k`.

## 7. What the verifier proves

For every function, assuming its `requires` and the types of its parameters:

- every `get`/`put` index `i` satisfies `0 <= i < (len b)` (V003);
- every arithmetic result fits its type (V004); divisors are non-zero (V005);
- casts to `u8` are in 0..255 and `buf-new` sizes are non-negative (V009);
- each call satisfies the callee's `requires` (V001); the callee's `ensures` is then assumed;
- every exit satisfies the function's `ensures` (V002); `assert`s hold (V008);
- loop invariants hold on entry (V006) and are preserved by the body (V007); a `decreases`
  measure is non-negative and strictly decreases (V011).

**Loops**: after a loop starts, the verifier knows only the invariants about variables the loop
changes. It infers the simple ones itself: bounds on counters and accumulators (against 0, their
starting value, the loop condition and constants in the code), order between two counters,
the function's preconditions, the preconditions of functions the loop calls (at the arguments
they get), and fields the loop leaves alone. Each is kept only if it holds on
entry and survives an iteration; `--json` lists them under `inferred`. Write what it cannot
guess: facts about buffer contents, and bounds that take arithmetic to derive.

```sysp
(fn index-of ((b (ref (buf u8))) (c u8)) i64
  (effects)
  (ensures (and (<= -1 result) (< result (len b))))
  (ensures (=> (>= result 0) (== (get b result) c)))
  (ensures
    (=> (== result -1)
      (forall ((k i64)) (=> (and (<= 0 k) (< k (len b))) (!= (get b k) c)))))
  (for (i 0 (len b))
    (invariant (forall ((k i64)) (=> (and (<= 0 k) (< k i)) (!= (get b k) c))))
    (if (== (get b i) c) (return i)))
  -1)
```

A `for` states its counter's bounds itself. What the loop has seen so far it cannot know, so
without the quantified invariant the postcondition fails (V002):

<!-- expect: V002 -->
```sysp
(fn has-zero ((b (ref (buf i64)))) bool
  (effects)
  (ensures
    (=> (not result)
      (forall ((k i64)) (=> (and (<= 0 k) (< k (len b))) (!= (get b k) 0)))))
  (for (i 0 (len b))
    (if (== (get b i) 0) (return true)))
  false)
```

Overflow is caught where it happens. The midpoint `(/ (+ lo hi) 2)` overflows for large values;
`(+ lo (/ (- hi lo) 2))` does not:

<!-- expect: V004 -->
```sysp
(fn mid ((lo i64) (hi i64)) i64
  (effects)
  (requires (and (<= 0 lo) (<= lo hi)))
  (/ (+ lo hi) 2))
```

## 8. Structs and mutable borrows

```sysp
(struct Counter (hits i64) (limit i64))

(fn bump ((c (mut Counter))) bool
  (effects)
  (requires (and (<= 0 (. c hits)) (<= (. c hits) (. c limit))))
  (ensures (and (<= 0 (. c hits)) (<= (. c hits) (. c limit))))
  (ensures (=> result (== (. c hits) (+ (old (. c hits)) 1))))
  (if (< (. c hits) (. c limit)) (do (set (. c hits) (+ (. c hits) 1)) true) false))
```

A condition every function on a struct restates, like `bump`'s first two, is better said once,
as the struct's invariant (§23).

A struct with a buffer field is a resource. Build it with `new`; take it apart with a destructuring
`let` to free its buffers:

```sysp
(struct Stack (items (buf i64)) (top i64))

(fn stack-new ((cap i64)) Stack
  (effects alloc)
  (requires (and (<= 1 cap) (<= cap 1000000)))
  (ensures (and (== (len (. result items)) cap) (== (. result top) 0)))
  (new Stack (items (buf-new i64 cap)) (top 0)))

(fn stack-free ((s Stack)) unit
  (effects alloc)
  (let (Stack items top) s)
  (free items))
```

`(resource struct ...)` makes a struct a resource without a buffer: it can be neither copied nor
dropped, only moved, borrowed and taken apart where its fields are visible. With a contract on
a field, that is a protocol. Here a channel end allows exactly `left` more sends, and dropping
it early is O002, sending once too often V001:

```sysp
(resource struct Sender (left i64))

(fn send ((s (mut Sender)) (msg i64)) unit
  (effects)
  (requires (> (. s left) 0))
  (ensures (== (. s left) (- (old (. s left)) 1)))
  (set (. s left) (- (. s left) 1)))

(fn close ((s Sender)) unit
  (effects)
  (requires (== (. s left) 0))
  (let (Sender left) s))
```

## 9. Holes

`?name` stands for an expression you have not written yet. A program with holes still parses
and type-checks; the checker reports each hole's expected type and the variables in scope
(H001), and verifies every function without holes. Programs with holes do not compile.

<!-- expect: H001 -->
```sysp
(fn average ((b (ref (buf i64)))) i64
  (effects)
  (requires (> (len b) 0))
  ?body)
```

## 10. Diagnostics

`sysp check --json` reports each problem with a stable code, a span, a message, and where
relevant the expected/actual types, the failing obligation, a counterexample (concrete values of
parameters and locals), and suggested fixes. Codes: `P` syntax, `N` names, `T` types, `O`
ownership, `E` effects, `V` verification, `W` warnings, `H` holes, `I` internal errors.

## 11. C interface

`i64`, `u8`, `bool` map to `int64_t`, `uint8_t`, `bool`. `(buf i64)` is
`typedef struct { int64_t *ptr; int64_t len; } buf_i64;` (likewise `buf_u8`), passed by value in
every mode. A struct is passed by value, except `(mut S)` and mutable scalars, which become
pointers. `unit` is `void`; a `never` function is `_Noreturn void`.

For code in a lower privilege mode, `sysp build --user-entry F --gate G ...` makes the functions
`F` reaches (not through a gate) user code: there a call to a gate `G` becomes a call to
`sysp_gate_G` with the same signature, which the platform implements as a trap, and an
`(atomic ...)` block becomes `sysp_user_atomic_begin()`/`_end()`. Proofs are unchanged: a gate's
contract is the same on both sides.

A function both sides reach (a library) is compiled once when it is the same in both modes. When
it is not (it calls a gate, has an atomic block, or calls such a function), it is compiled twice:
`name` for user code, and a twin `sysp_kernel_name` that kernel code calls.

```
user code ──▶ fs_attach ──▶ fs_ask ──▶ sysp_gate_sys_serve   (a trap)
kernel    ──▶ sysp_kernel_fs_attach ──▶ sysp_kernel_fs_ask ──▶ sys_serve
```

## 12. Low-level code: externs, `replace`, several files

`(extern fn name (params) ret clauses...)` declares a function implemented outside sysp (for
example in assembly). It has no body; its contract is **trusted**, not proven, and every build
lists it as warning W002. Externs are the only way to reach hardware, so the trusted code is a
short, visible list.

`replace` moves an owned value into a slot and hands back the previous one, so a resource can
live in a struct field without ever being copied or lost:

<!-- expect: W002 -->
```sysp
(extern fn uart-write ((s (ref (buf u8)))) unit
  (effects io))

(struct Mailbox (slot (buf u8)) (full bool))

(fn take-msg ((m (mut Mailbox))) (buf u8)
  (effects alloc io)
  (requires (. m full))
  (ensures (not (. m full)))
  (uart-write "taking a message\n")
  (set (. m full) false)
  (replace (. m slot) (buf-new u8 0)))
```

`sysp check a.sysp b.sysp ...` treats several files as one program (§15 says which names each file sees). `sysp build
--freestanding` emits C without libc; the platform supplies `sysp_alloc` (zeroed memory),
`sysp_free` and `sysp_panic`.

## 13. Shared state: rely and guarantee

When interrupts can switch tasks at any instruction, state shared between tasks can change
under you. A parameter `(x (shared T R))` is such state. `R` is a predicate over two `T` values,
`(before after)`, describing every change other tasks may make.

- Shared state is read and written only inside `(atomic e ...)`, which runs with interrupts off
  (C001 otherwise). Outside atomic blocks, a shared parameter can only be passed on to another
  shared parameter with the same `R`. `atomic` needs the `io` effect, and you cannot `return` from
  inside it (C004).
- **Rely**: whenever shared state is observed outside an atomic block, the verifier assumes other
  tasks may have changed it in any way `R` allows. Facts that `R` does not preserve are lost.
- **Guarantee**: each atomic block must change shared state only in ways `R` allows (C002),
  because the other tasks rely on that.
- `R` must be reflexive and transitive (C003). The idiom is
  `(=> (inv before) (and (inv after) ...))`.

```sysp
(struct Counter (hits i64) (limit i64))

(pred counter-ok ((c Counter))
  (and (<= 0 (. c hits)) (<= (. c hits) (. c limit)) (<= (. c limit) 1000000)))

; other tasks may only count up, keep the invariant, and never change the limit
(pred counter-rely ((before Counter) (after Counter))
  (=> (counter-ok before)
    (and (counter-ok after)
      (<= (. before hits) (. after hits))
      (== (. before limit) (. after limit)))))

(fn tick ((c (shared Counter counter-rely))) bool
  (effects io)
  (requires (counter-ok c))
  (ensures (counter-ok c))
  (atomic
    (if (< (. c hits) (. c limit)) (do (set (. c hits) (+ (. c hits) 1)) true) false)))
```

Reading `hits` inside an atomic block and later asserting that it is unchanged is rejected:
another task may have counted up in between. Asserting it has not gone down is proven.
`--freestanding` builds call the platform's `sysp_irq_save()` / `sysp_irq_restore(s)`.

## 14. Arrays of owned buffers

`(cells u8)` (or `(cells i64)`) is a fixed-length array in which every cell holds an owned
buffer. `(cells-new u8 n)` makes `n` cells holding empty buffers (needs `alloc`).
`(cell-swap c i b)` puts `b` into cell `i` and returns the buffer that was there, so buffers move
in and out without being copied or lost. `(cell-len c i)` is the length of the buffer in cell
`i`. `(cells-free c)` frees the array and every buffer in it. Index bounds are proven like
`get`/`put`.

```sysp
(fn swap-in ((c (mut (cells u8))) (i i64) (b (buf u8))) (buf u8)
  (effects)
  (requires (and (<= 0 i) (< i (len c))))
  (ensures (== (cell-len c i) (len b)))
  (cell-swap c i b))
```

## 15. Files and scopes

A name means the nearest definition that can be seen: a variable bound around it, else an item
of its own file, else a public item of another file. Within one scope a name means one thing
(N002): two items of one file cannot share a name, nor two public items of the program (an
`extern fn` counts as public: its name is its C name). So a binding may take a constant's name, and
two files may each keep a private item of the same name.

Files are the privacy boundary. A `struct`, `fn`, `extern fn`, `pred` or `const` wrapped in
`(private ...)` is usable only from the file that declares it (N003 otherwise). Other files may
name a private struct as a type and move or borrow its values, but cannot construct it,
destructure it or read its fields, even in specifications.

So a private struct is an unforgeable value, and authority can be one: a struct with no fields
carries no data, only the right to call the functions that take it. Other files get it only from
the declaring file's public functions.

<!-- expect: W002 -->
```sysp
(private struct Console)

(private extern fn uart-put ((c u8)) unit
  (effects io))

(fn write-byte ((con Console) (c u8)) unit
  (effects io)
  (uart-put c))
```

An `(opaque pred ...)` may be used from other files, but there it is known by name only: their
proofs carry it from one contract to the next without seeing what it says, and its file's
functions are the only way to establish or use it. Hiding is always sound; it saves the solver
work in every file that only passes the fact along.

## 16. Contracts that cannot hold

A proof is only meaningful if the facts it starts from can all be true. When the facts on a path
contradict each other (two preconditions, an extern's trusted contract, an `assume`, a loop
invariant), every obligation on the path is "proved" for no reason. sysp checks each path where
it ends (function exits, branch and loop-body ends) and reports V012, naming the facts that
conflict. When the conflict is with a branch condition instead, the branch is dead code: W003,
naming the facts that rule it out.

<!-- expect: V012 -->
```sysp
(fn pick ((x i64)) i64
  (effects)
  (requires (> x 10))
  (requires (< x 5))
  (ensures (== result 42))
  x)
```

`sysp check --warn-unneeded` also reports W004 for a precondition no proof in its function used.
It is off by default: a precondition may state a protocol rule (take only from a full mailbox)
rather than a proof need.

## 17. Running a failed proof

A failed proof does not always mean a bug: the code may be right and a loop invariant too weak.
`sysp check --repro` tells the two apart. For each failed obligation it asks the solver for small
inputs, runs the function on them in a checked build (every obligation becomes a runtime check)
and adds a `run:` line: `fails this check ... the bug is real`, or `does not fail ... the proof
needs a stronger loop invariant or contract`. `sysp build --checked` writes that build. Programs
with externs, parameters that are not numbers, words, booleans, buffers, or structs and enums of
those, and `decreases` failures are not run; a clause C cannot express (a quantifier over two variables, `old` buffer contents)
is not checked, and a run that depends on one says so.

## 18. Functions that never return

A function whose return type is `never` does not return: every path through its body ends in
`(while true ...)` with no `break`, or a call to another `never` function (T012 otherwise), and it has no
`ensures`. A call to one ends the path. The verifier knows nothing runs after it, and the
ownership checker lets the path keep what it owns, since nothing is dropped if nothing
follows. `never` is not a value type: a call to such a function can be a statement, a branch of
an `if` or the end of a block, not an operand.

<!-- expect: W002 -->
```sysp
(extern fn halt ((code i64)) never
  (effects io))

(fn at ((b (ref (buf u8))) (i i64)) u8
  (effects io)
  (if (and (<= 0 i) (< i (len b))) (get b i) (halt 2)))
```

## 19. Keeping proofs

`sysp check --cache DIR` (and `sysp build --cache DIR`) keeps what verifying each function
reported, and reports it again, without the solver, while nothing its proof depended on has
changed: the function's own text, and the signature and contract (not the body) of every
function it calls, and every predicate and struct it names, transitively. Changing a callee's
body re-proves only the callee; changing its contract re-proves its callers. A function with an
error is never kept. Diagnostics and inferred invariants are the same as a fresh run's. A file is
known to the cache by its name, as it is to sysp (a private item's internal name is made from it),
so `kernel/x.sysp` and `/home/me/os/tests/../kernel/x.sysp` share proofs. Two files of one program
that share a name are known by as much of their paths as tells them apart (`lib/text.sysp`,
`net/text.sysp`), since each sees its own private items.

Functions are proven at once, one per processor, or N with `-j N` (`--jobs N`); the report is the
same as with `-j 1`.

## 20. Words

`i64` and `u8` are numbers: arithmetic is exact and overflow is an error. A word, `w8` `w16`
`w32` or `w64` (C `uint8_t` … `uint64_t`), is a bit pattern of that width:

| Form | Meaning |
|---|---|
| `(& a b)` `(\| a b)` `(^ a b)` `(~ a)` | and, or, xor, complement |
| `(<< a n)` `(>> a n)` | shift by the `i64` `n`, which must be proven in `[0, width)` (V013); `>>` fills with zeros |
| `(+ a b)` `(- a b)` `(* a b)` | arithmetic modulo 2^width: never an error |
| `(== a b)` `(!= a b)` | comparison; words have no order and no division: convert with `as` |

Both operands have the same word type, and a literal takes it from the other (`(<< 1 i)` next to
a `w32` is a `w32`). Numbers have no bitwise operators. A word's value, for `as`, is its
unsigned reading: `(as u8 (& w 0xff))` needs no precondition, `(as u8 w)` does.

```sysp
(fn fnv1a ((data (ref (buf u8)))) w32
  (effects)
  (var h (as w32 2166136261))
  (for (i 0 (len data))
    (set h (* (^ h (as w32 (get data i))) 16777619)))
  h)

(fn set-bit ((m w32) (i i64)) w32
  (effects)
  (requires (and (<= 0 i) (< i 32)))
  (ensures (!= (& result (<< 1 i)) 0))
  (| m (<< 1 i)))
```

## 21. Enums

An **enum** is a value that is one of several variants, each with fields of its own:
`(enum Name (variant (field type) ...) ...)`, a variant with no fields written `(variant)`. A
field's type is plain data: no buffer or resource. Variants may share a field: one name, one type,
one field of the enum (N002 if the types differ).

| Form | Meaning |
|---|---|
| `(new E variant (field e) ...)` | a value of variant `variant`: each of its fields exactly once |
| `(is e variant)` | whether `e` is that variant; also in specifications |
| `(. e field)` | the field, which `e` must be proven to be a variant with (V014) |
| `(match e ((variant x ...) body...) ... (else body...))` | the first clause for `e`'s variant, `x ...` naming its fields in order; every variant needs a clause unless there is an `else` (T013) |

A field is not set in place: set the whole value. In C an enum is a struct of its tag and its
variants' fields, and a `match` a `switch` on the tag.

```sysp
(enum Level (empty) (some (n i64)) (drained))

(fn amount ((l Level)) i64
  (effects)
  (requires (=> (is l some) (<= 0 (. l n))))
  (ensures (<= 0 result))
  (match l
    ((some n) n)
    (else 0)))
```

## 22. Views

`(view b at n)` lends `b[at, at + n)` as a buffer of length `n`, whose element `k` is `b`'s
element `at + k`. It is only an argument to a `ref` or `mut` buffer parameter (T014 elsewhere),
and must lie within `b`: `0 <= at`, `0 <= n`, `at + n <= (len b)` (V003). What the callee writes
through a `mut` view lands in `b`; the rest of `b` is unchanged. A view borrows `b` as the
parameter does, so two views of one buffer in one call conflict if either is `mut` (O005).

```sysp
(fn fill ((b (mut (buf i64))) (v i64)) unit
  (effects)
  (ensures (== (len b) (len (old b))))
  (ensures (forall ((k i64)) (=> (and (<= 0 k) (< k (len b))) (== (get b k) v))))
  (for (i 0 (len b))
    (invariant (forall ((k i64)) (=> (and (<= 0 k) (< k i)) (== (get b k) v))))
    (put b i v)))

(fn middle ((b (mut (buf i64)))) unit
  (effects)
  (requires (== (len b) 10))
  (ensures (and (== (get b 0) (get (old b) 0)) (== (get b 5) 7)))
  (fill (view b 2 6) 7))
```

## 23. Struct invariants

`(struct S (field type) ... (invariant c))` says what holds of every value of `S` that crosses
a function boundary. `c` is a specification over the field names (and constants and
predicates; a field's name hides a constant's, as a binding does, §2); there is at most one,
after the fields. A field whose struct has an invariant keeps
it inside `S` too.

| Where | The invariant is |
|---|---|
| a parameter of type `S` (owned, `ref` or `mut`), on entry | assumed |
| a call's result, a `mut` argument after the call | assumed |
| an argument at a call | proven (V015) |
| a `mut` parameter, the result, at each return | proven (V015) |

Between those points the fields may be set one at a time. The invariant is a contract the
compiler writes, so it is proven, checked in a checked build and inferred into loops as
`requires` and `ensures` are; no contract needs to say it.

```sysp
(struct Range (lo i64) (hi i64)
  (invariant (and (<= 0 lo) (<= lo hi) (<= hi 100))))

(fn width ((r (ref Range))) i64
  (effects)
  (ensures (<= 0 result))
  (- (. r hi) (. r lo)))

(fn shift ((r (mut Range))) unit
  (effects)
  (if (< (. r lo) 100) (set (. r lo) (+ (. r lo) 1)))
  (if (> (. r lo) (. r hi)) (set (. r hi) (. r lo))))
```

## 24. Break

`(break)` leaves the innermost `while` or `for`, from anywhere in its body; it has type `never`.
It is an error outside a loop (T015) and inside an `atomic` block within the loop (C004). What
the body owns must be gone first (O002). After the loop, the verifier knows what held where the
loop was left: where the condition was false, with the invariants, or at a `break`, where no
invariant is asked for. A loop is still proven one iteration at a time: a path that breaks is
not an iteration.

```sysp
(fn first-zero ((b (ref (buf u8)))) i64
  (effects)
  (ensures (and (<= 0 result) (<= result (len b))))
  (ensures (=> (< result (len b)) (== (get b result) 0)))
  (var at (len b))
  (for (i 0 (len b))
    (if (== (get b i) 0) (do (set at i) (break))))
  at)
```