# 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`, a word, or a struct's rows (§25); `retype` reads its bytes as another `T` (§26) |
| `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)` | binding that is never reassigned, visible until the end of the enclosing body/`do`; a buffer or struct it owns can still be written (a mutable place, §5) |
| `(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.

A **mutable place**, which `put` and `replace` write, is a variable the function owns, whether
bound by `let`, `var` or a parameter, a variable lent to it as `mut`, or a field of either:
`(let b (buf-new u8 n))` then `(put b 0 1)` is fine. A `ref` borrow is not one (O008).

## 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, and
itself if it says how that ends (below), but not itself through another (T011). 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))
```

**Spec functions** (sysp 071) are predicates of any scalar type: `(spec name ((x T) ...) R body)`,
R an `i64`, `u8`, word or `bool`. One that calls itself says `(decreases m)` before its body, m an
`i64` of its parameters; at each call of itself, under the conditions that lead there, m must be
smaller and not below 0 (V011), or a definition such as `f(x) = f(x) + 1` would let the verifier
prove anything. The verifier knows such a function by its definition, unfolded once where it is
used (to the end where its arguments are constants), so a loop states what it has computed so far
as an invariant, and one step is one unfolding. It does so only in a function whose own text names
it, or names a predicate that does (sysp 075): to any other, a value of it is one it does not know,
the same where the arguments are, so a caller of a function whose contract uses one pays nothing
for it, and a caller that needs it names it, in an `assert` if nowhere else. Even there, only the
applications its own text makes are unfolded: one in a callee's postcondition is passed along as
it is (sysp 078), unless its arguments are constants or the function's own text makes the same
one. An application to a quantifier's variable is never unfolded. A buffer argument may be a view, and is passed as
that part of the buffer alone: a value over `t[a, b)` is unchanged by a write outside it, with no
lemma. A checked build leaves a contract that uses one to the proof.

```sysp
(spec pow10 ((k i64)) i64
  (decreases k)
  (if (<= k 0) 1 (* 10 (pow10 (- k 1)))))

; the value of the decimal digits d, the first the most significant
(spec dec-value ((d (buf u8))) i64
  (decreases (len d))
  (if (== (len d) 0)
    0
    (+ (* (- (as i64 (get d 0)) 48) (pow10 (- (len d) 1)))
      (dec-value (view d 1 (- (len d) 1))))))

; a digit written before t[p + 1, p + 1 + n): the value gains it, at its place
(fn put-digit ((t (mut (buf u8))) (p i64) (n i64) (c i64)) unit
  (effects)
  (requires (and (<= 0 p) (<= 0 n) (< (+ p n) (len t)) (<= 0 c) (<= c 9)))
  (ensures
    (== (dec-value (view t p (+ n 1)))
      (+ (* c (pow10 n)) (dec-value (view (old t) (+ p 1) n)))))
  (put t p (as u8 (+ 48 c))))
```

**Lemmas** (sysp 090) are proofs a function calls for their conclusion:
`(lemma name ((x T) ...) (requires c) (ensures c) [(decreases m)] body)`, proven as a function is,
and no code: neither the lemma nor a call of it is in the C. A call brings the lemma's `ensures`
in where it is made, at its arguments, as the function's own facts (so a spec function in them
unfolds there). A lemma that calls itself, as a proof by induction does, says `(decreases m)`,
smaller at each call and not below 0 (V011), or its proof would rest on itself; not through
another lemma (T011). A lemma is no code (T017): its parameters are values or `ref`, it owns no
resource, calls only lemmas, loops only with `for`, and a call of one runs no code in its
arguments.

```sysp
(spec pow10 ((k i64)) i64
  (decreases k)
  (if (<= k 0) 1 (* 10 (pow10 (- k 1)))))

(spec dec-value ((d (buf u8))) i64
  (decreases (len d))
  (if (== (len d) 0)
    0
    (+ (* (- (as i64 (get d 0)) 48) (pow10 (- (len d) 1)))
      (dec-value (view d 1 (- (len d) 1))))))

(pred digits ((d (buf u8)))
  (forall ((j i64))
    (=> (and (<= 0 j) (< j (len d))) (and (<= 48 (get d j)) (<= (get d j) 57)))))

; n digits have a value below 10^n: by induction on n, the rest of the digits first
(lemma dec-bound ((d (ref (buf u8))))
  (requires (digits d))
  (ensures (and (<= 0 (dec-value d)) (< (dec-value d) (pow10 (len d)))))
  (decreases (len d))
  (if (> (len d) 0) (dec-bound (view d 1 (- (len d) 1))) unit))

(fn fits ((t (ref (buf u8)))) bool
  (effects)
  (requires (and (digits t) (== (len t) 3)))
  (ensures (< (dec-value t) 1000))
  (dec-bound t)
  (assert (== (pow10 3) 1000))
  true)
```

Specifications use mathematical integers, so they cannot overflow (a checked build evaluates
their arithmetic in 128 bits, which is exact for a product of two `i64` and sums of such). `(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, `buf-new` sizes are non-negative, and a `retype`'s bytes are
  whole rows (V009, §26);
- each call satisfies the callee's `requires` (V001); the callee's `ensures` is then assumed;
  of a `mut` argument, only what the callee may write changes (its write set, below);
- 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).

**Write sets** (sysp 097): what a function may write of each `mut` parameter is read from its
body: the places it sets, `put`s into or `replace`s, and what its callees may write of what it
passes them. A call changes only those places of its argument; the rest keeps its value with no
frame in the callee's contract, as Dafny's `modifies` and Viper's permissions frame a call, but
found, not written. An extern may write all of a `mut` parameter, as may a function through a
parameter it passes as a view, a row or `shared`, or through a call that reaches itself again.
A caller's kept proof counts its callees' write sets, so a callee that writes more proves its
callers again.

**Loops**: after a loop starts, the verifier knows only the invariants about the places the loop
changes. A field the loop never sets, and never passes `mut` to a function that may write it,
keeps its value; a buffer it only
`put`s into, or a table whose rows' fields it sets (§25), keeps its length. 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; one
that names a view argument is left out, the call's others kept, such as a struct's invariant on
another argument; a call whose argument is another call's result gives none), and fields a call
in 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` (or `--report FILE`, which writes the JSON there and prints the text, for
`check` and `build`) 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, `S` secrets (§27), `V` verification, `W` warnings, `H` holes, `I` internal errors. Its
`stats` count obligations, those proven, milliseconds, and `work`: z3's own count of what the
proofs took (kept proofs included), which load does not change, so two versions of a program are
compared by it. `functions` gives each function's obligations, work, `unknowns` (the checks z3
could not decide, each counted with its retry) and `peak` (the most one check took), and the text
names the five costliest, so a run says where the work went; a function's work is the same at any
load and any `-j`. To see where one function's work went, `SYSP_CHECK_LOG=FILE` adds a line per check
to FILE, tab-separated: its work as the function counts it, its own work, its answer, the
function, and what the check was: an obligation's code, place and message, `inference FILE:LINE`
for the loop whose invariants are inferred, or `path` for whether a path's facts can hold (sysp
112). A kept answer carries its work, so a run from the store gives this without asking z3. `sources` gives each file and the SHA-256 of its bytes as sysp read them (sysp
103), so a build record can name what was compiled and proven as bytes (sysk's `/sys/build`).

Each check is bounded by work, not time: `--check-work N`, 30 million by default, above every
check that answers in sysk's whole system (the most, 18 million). A check that reaches it is
undecided, as one z3 cannot decide (V010), the same on a busy machine as on an idle one.
A check of a path alone, whether its facts can hold (§16), has 3 million (sysp 099).
`--timeout-ms` (120 s by default) only stops a z3 that hangs. z3 looks at its own limits only now
and then, so an answer that has not come 30 s past it ends the function's session (sysp 069): z3 is
stopped, that check and every later one in the function are undecided, and the check counts as
its whole work bound. A z3 that ends (its process, or the link to it; sysp 089) is started again,
once a function, and sent the facts the session holds (sysp 098, with `--cache`); a second end, or
one without `--cache`, ends the session as a silent one does. sysp never waits on a write to z3:
commands go through a thread of the session's own (sysp 105), so a z3 that stops reading costs only
the deadline of the answer it owes.

A function's checks together have a budget: 50 million by default, the suite's (sysp 061), or
`--work-max N` (`0` for none). A function over it is an error (V016), which says, with
`--cache`, what it took before, so a change elsewhere that made it dearer (a widely used invariant)
shows. A long proof is a design problem, solved by splitting the function (lookups apart from
changes) or stating its loops' invariants; and a fact is not free: one more implication in a
callee's `ensures` is something every caller's proof works with (sysc's `sha-byte` gained one, and
its caller `sha-pad` went from 5 to 65 million). `--work-allow FILE` lists the functions allowed
over the budget, a line each, `name` or `file:name` (`;` starts a comment): each is reported as a
warning (W005), and so is one listed that no longer needs it.

## 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`, and `buf_S` for a
table, §25), passed by value in every mode. A struct is passed by value when owned; `(mut S)` and
mutable scalars become pointers, and `(ref S)` a `const` pointer, so a call does not copy a struct
it only reads (sysp 082). `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,
16-byte aligned), `sysp_free` and `sysp_panic`. An extern that returns a buffer returns memory
aligned to 8 bytes at least, as allocators do: `retype` (§26) counts on it. `--no-verify` (for `check`, and `build` since sysp 062) checks names,
types, ownership, effects and contracts but proves nothing: the report says `not verified
(--no-verify): nothing is proven` (`"verified": false` in its JSON), and `build` writes C from a
program no proof has looked at, for running something before its proofs are made, never as a
build that is trusted.

## 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)`.

Outside an atomic block, wherever another task may run (a call included), a shared value is a
fresh one, related to the last only by its rely. An opaque predicate (§6) is known by the terms it
is applied to, not their values, so a fact `(p k ...)` or `(p (. k n) ...)` over the shared `k` is a
new, unknown fact there, though the rely says `n` is unchanged. A fact meant to last is kept over
what no task changes: read `n` once, in an atomic block, into a local or a field of a value the
function owns, keep the opaque fact over that, and state where it is used that `n` is still
`(. k n)`, which the rely gives as a plain fact. sysk 101 kept its mount table's facts so
(`mounts-over`), where a quantified predicate over every row in a widely used one had made 13
functions 20 to 500 times dearer: 821 million units of work became 3.3.

## 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. It is one function of its arguments' values,
in a quantifier and out (sysp 080, 095): a fact kept for every block under a `forall` gives the one
at block d. A spec function may be opaque too,
`(opaque spec ...)` (sysp 093): to other files a value equal where its arguments are, so a byte
format's get and put state their laws with it in their own file, and a caller elsewhere has get
after put without paying for the arithmetic under it.

## 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.

These checks of a path alone are bounded lower than an obligation: 3 million units of z3's work
(sysp 099), or `--check-work` when that is lower. They only ever add a warning or an error, and
one z3 cannot decide within the bound reports nothing, as it did at 30 million. A contradiction
is found in far less (on sysf, every one under a million), while a path whose facts quantify over
a recursive spec could take the whole 30 million to answer unknown, and most of a function's work
was that.

<!-- 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 proving it, while nothing its proof depended on has
changed: the z3 that proved it (its version, the one thing z3 is asked) and the bound on a check
(§10), the function's own text, and the signature and contract (not the body) of every
function it calls, every predicate it uses, every struct and enum that is the type of a value in it
(with the struct's invariant), every constant it uses (with its value) and the rely of every shared
parameter, transitively; an opaque predicate of another file (§15) by its signature only, as its
proofs know it by name. These are the items sysp resolved its names to, so a field, a comment or
another file's private item that happens to share a name is not one of them (sysp 057), and a
file added to the program leaves the other files' proofs kept. 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.

A kept proof also depends on sysp itself, so a new sysp proves every function again; but beneath
the proofs the same directory keeps z3's answers (`DIR/queries`, sysp 060), each by what its check
says (sysp 094): the declarations, the facts of the scopes open at it, and the check itself. A
function whose queries a new sysp leaves as they were is proven from these answers without
starting z3; one whose queries changed asks z3 only the checks whose text changed. z3 is started
at the first of them and sent the facts the session holds, none of the checks before, and asked
only what the store does not answer. Answers kept before 094, by everything z3 was sent before
them (060), are still read, and kept again by their check.

A z3 started part way answers from the facts alone, not from what it learned on the checks
before, so such a run (warm) can differ from one with an empty store (cold): a check proved in
one and unknown in the other, at a limit, and the inferred invariants and work that follow. Each
answer is sound. A function's work is z3's count across its checks and what came between them,
kept with each answer, so a run from kept answers reports what made them; costs compare between
runs of one path, and the work budget holds on the cold path. `--cold` (or `SYSP_COLD=1`) reads
no kept proof or answer and asks z3 every check in one session, keeping what it makes: what an
empty `--cache` reports.

An answer given at the time limit (`--timeout-ms`), or never given (sysp 069), is not kept, nor
anything after it in its session.
A function's answers are also kept together, in order, in one file for it (`DIR/answers`, sysp
067), read once when its proof starts: the file per answer is for runs proving the same change at
once. Runs that share the directory and miss the same answer at once wait for the first to get it, but
no longer than a check may take; then each asks z3 itself (sysp 091).
Each z3 is started with the function it proves in `SYSP_FN`, so `ps eww` shows what each one
works on (sysp 092).

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 |
| `(rotl a n)` `(rotr a n)` | rotate left or right by the `i64` `n`, any `n`, taken modulo the width (sysp 070) |
| `(+ 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 mix ((a w32) (b w32)) w32
  (effects)
  (ensures (== result (^ a (rotl b 7))))
  (rotl (^ (rotr a 7) b) 7))

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

## 25. Tables

`(buf S)`, for a struct `S` of plain data (integers, words, `bool`, enums without fields, and
structs of these; T016 otherwise), is a table: one buffer of rows. `(get b i)` is row `i`, a
copy, and `(put b i r)` writes a whole row. A row's field is read as `(. (get b i) f)` and set in
place with `(set (. (get b i) f) v)`, which changes that field of that row and nothing else.
Every index is bounded (V003). A row's field may also be lent to a `ref` or `mut` parameter, or
swapped with `replace`, which changes that row's field alone (sysp 081), and a row may be lent
whole, `(get b i)` (sysp 083). `(buf-new S n)` makes `n` rows of zeros (`false`, an enum's first variant). If `S` has an
invariant (§23), every row keeps it wherever the table crosses a function boundary, and
`buf-new` proves that a row of zeros does (V015). A table can also be made from bytes, such as
an allocator's, with `retype` (§26). In C a table is an array of `S`:
`buf_S { S *ptr; int64_t len; }`.

**Tables of resources** (sysp 081): the rows of `(buf S)` may be a resource struct of such fields,
a channel's end, say. They are never copied or moved out by value (O006): a row's fields are
lent, or swapped with `replace`. `buf-new` cannot make one, as a row of zeros is no resource
(T016), and a plain `retype` cannot make one from bytes or bytes from one (O006, sysp 086). One
is made with its rows given, in order, and known to be them: `(buf-of S e ...)` allocates their
memory (the `alloc` effect), and `(retype (buf S) b e ...)` puts them in an owned buffer `b` the
caller already has, exactly their size (V009, sysp 085), as a task does from its own heap. `free`
cannot end one (O006); `(buf-end t f a ...)` does: `t` is moved, and `(f a ... row)` is called
for each row in order, `f` taking the row, owned, last; the other arguments may be lent anew to
each call, and what `f` ensures of them carries to the next, as a loop's inferred invariant. It
gives the table's memory back as a `(buf u8)` of its length, for the caller to free or return to
the heap it came from (085).

```sysp
(struct Chan (queued i64) (ended bool))

(fn drain ((chans (mut (buf Chan))) (c i64)) unit
  (effects)
  (requires (and (<= 0 c) (< c (len chans))))
  (ensures (== (. (get chans c) queued) 0))
  (ensures (== (. (get chans c) ended) (. (get (old chans) c) ended)))
  (set (. (get chans c) queued) 0))
```

## 26. Retype

`(retype (buf U) b)` takes an owned buffer `b` of any element `T` a buffer may have and gives
back the same memory as a `(buf U)`: nothing is copied, and `b` is moved (§3). An allocator can
hand out bytes and its callers can have words or a table's rows (§25) from them, and give them
back as bytes. `(size-of T)` is the size of an element in bytes, an `i64`: C's `sizeof`, padding
included (a struct's fields in order, each at a multiple of its alignment, the whole rounded up
to the largest).

- The length is `(len b)` × `(size-of T)` / `(size-of U)`, and the bytes must be a whole number
  of rows (V009).
- **Bits**: `i64`, `u8`, the words, and structs of these without an invariant (§23), are types
  every bit pattern of which is a value, so any bytes are rows of them. Nothing is known of the
  new rows but zero: when every row of `b` was zero and `T` has no padding, every row of the
  result is zero; when every row of the result is zero and `U` has no padding, every row of `b`
  was. So an allocator's zeroed bytes become zeroed words, and wiped words become wiped bytes.
- Rows that are not bits (a `bool`, an enum's tag, a struct with an invariant) come only from
  bytes of zeros: the verifier proves every row of `b` zero, and `T` without padding (V009), and
  the rows are rows of zeros, as `buf-new`'s are, which an invariant must allow (V015).

```sysp
(pred zeroed ((b (buf u8)))
  (forall ((k i64)) (=> (and (<= 0 k) (< k (len b))) (== (get b k) 0))))

(struct Task (done bool) (alarms i64))

(fn tasks ((b (buf u8)) (n i64)) (buf Task)
  (effects)
  (requires (and (zeroed b) (<= 0 n) (<= n 100) (== (len b) (* n (size-of Task)))))
  (ensures (and (== (len result) n) (=> (< 0 n) (not (. (get result 0) done)))))
  (retype (buf Task) b))
```

In C, `retype` is a function that returns `{ (U *)b.ptr, b.len * sizeof(T) / sizeof(U) }`, and
nothing is checked at run time but in a checked build. An owned buffer always starts where any
row may: `buf-new`'s memory is the allocator's, and an extern's is aligned to 8 bytes (§12). A
view (§22) is never owned, so it is never retyped. `size-of` is not yet allowed in a `const`.

## 27. Secrets

A function says which of its arguments it keeps secret and what it makes public on return
(sysp 102), as contract clauses beside `requires` and `ensures`:

```
(fn sip-hash ((key (ref (buf u8))) (msg (ref (buf u8))) (at i64) (n i64)) w64
  (effects)
  (secret key)
  (declassify result)
  ...)
```

`(secret NAME ...)` names arguments, or fields of one at any depth, `(field s sha w)`, when only
that field is secret; a buffer's name is its contents, and **a buffer's length is public**, so a
loop to `(len key)` has a public bound. `(declassify NAME ...)` names `result` or arguments whose
contents may hold what was derived from a secret and are public on return: a hash, whether a tag
was right, the box a cipher writes.

The checker, before any proof and with no query to z3, follows each secret through the body:
through arithmetic, bitwise operations, shifts and rotations, multiplication, comparisons as
values, `as`, `let`, `var`, `set`, fields and buffers' contents. A secret may not reach a branch
(an `if` or `cond`'s test, a loop's condition or bound, `and` and `or`'s left side), an index or a
view's offset or length, a division or remainder, an allocation's size, or an extern (S001), and
may end only in the arguments named secret, or in what is declassified (S002): a function with
secrets returns a public result unless it declassifies it, and code that hands a secret back (a
field element's arithmetic) has no clauses and is followed through its summary. A clause naming
no argument is S003. Only data flows count: a branch on a public condition makes nothing it
assigns secret. Precision is by value, by field of a struct, and by a buffer's whole contents.

Every function has a summary of where its arguments go: which reach its result and each `mut`
argument's contents, and which reach a place a secret may not go. A caller's secrets flow through
a callee as its body allows, so a function with no clauses (sysl's `bytes-copy`) is used with
secrets as its body permits, a call is refused when it would carry a secret to a branch or an
index inside, and a public caller writes nothing: `sha-add` is constant-time in its words for
HMAC, and sysf's checksums through it stay public. Only functions with a `secret` clause, and
what they call, are followed, so a program with none pays nothing.

Which machine instructions are constant time is sysi's to check, in the code it makes (sysi 020,
023), from the same clauses (`fn-def-secrets`, `fn-def-declassify`).

## 28. Layouts

A record of bytes another program, a disk or a wire defines is declared once (sysp 104):

```
(layout ptr-bytes 128
  (dev u8 0)
  (block le63 4)
  (skip sha 44 32)
  (size le16 76)
  (alg u8 82 (= 1)))
```

A field is `(name kind offset)`, or `(name kind offset (= value))` for a value every writing has.
Kinds: `u8`; `le16`, `le32`, `le64`, little-endian; `be16`, `be32`, big-endian; `le63`, a `le64`
whose top bit is clear in a writing, so the reader refuses one that has it and a field read can be
`as i64`. `(skip name offset n)` is a place the record leaves to its owner (a hash written and
compared in place): in neither the struct nor the writer nor the reader, its offset and size
constants `NAME-SKIP-at` and `NAME-SKIP-size`. **Every byte no field or skip names is zero in a
writing.** Fields may not overlap or leave the record (P003).

From it sysp makes, as ordinary code proven like any other:

| Name | What it is |
|---|---|
| `(struct Ptr-Bytes (dev u8) (block w64) ...)` | the fields that are not fixed |
| `(const ptr-bytes-size 128)` | the record's bytes |
| `(ptr-bytes-block b at)` | an opaque spec per field: its value in the bytes at `b[at, ...)` |
| `(ptr-bytes-ok b at)` | an opaque predicate: the fixed and zero bytes as a writing has them |
| `(ptr-bytes-put b at v)` | writes `v`: ensures `ok` and each field's spec equal to `v`'s, changes no byte outside `b[at, at + 128)`, and keeps every other record of the layout in `b` |
| `(ptr-bytes-get b at v)` | whether the bytes are a writing (`ok`), and when they are, `v`'s fields set to their specs |

So a get after a put gives the record back, and what a get accepts is exactly what some put
writes: every byte is said by a field, a fixed value or zero, so no record has two writings. A
caller sees only the specs, so it pays for these laws by matching terms: a put then a get costs
it some ten thousand units of z3's work. The layout's own proofs, a put per field in a file of the
layout's own (`FILE#name`) where the specs are plain, the record's put and get in another
(`FILE#name.record`, sysp 106), cost more (sysf's 128-byte pointer, nine
fields, about 160 million in all, none over 25), and are kept like any proof, so they are paid
again only when the declaration changes. What a field means beyond its bytes (a range, a sum of
two fields, a size that must match a level) is the caller's to check, on the struct.

`sysp layout [--json] FILE ...` prints each layout's table from its declaration, as its code is
made (sysp 109): every byte in order, a field (its kind and fixed value), a skip, or zero, each with
the comment written just before it in the declaration. `--json` gives
`{"layouts": [{name, file, line, size, doc, fields: [{name, kind, at, width, value?, doc?}], skips:
[{name, at, width, doc?}], zeros: [{at, width}]}]}`, for docs pages, sysk's views and sysq's
schema, which then cannot disagree with what is read and written. These pages draw each example's
layouts so.