Lowent — The Lowent Programming Language Standard Specification (English edition)

6.2.1 Kinds of type§

1 Types are divided into the following kinds.

6.2.2 Integer types§

1 The name of an integer type is made of a sign and a width. u means unsigned, i signed, and the number after it is the width in bits.

2 Integers are represented in two’s complement (§5.3).

3 usize and idiff are integers wide enough to count the sizes and indices of the address space. Even if they have the same width as u64 · i64, they are different types, and they do not convert into each other automatically. usize is the type for lengths and indices, idiff the type for the difference between two positions.

3-1 usize and idiff have the same width, and it is chosen by the implementation (implementation-defined). That width is 16 bits or more and does not exceed the width of the widest integer type the implementation has. The implementation documents the width. usize is unsigned and idiff a two’s-complement signed integer, so the positive numbers idiff holds are half the range usize holds.

3-2 usize · idiff do not mix with any other integer type. The widening table (§6.2.5 (4)) does not include them — there is no automatic conversion from u8 to usize, nor from usize to u64. If only one of the two operands of an arithmetic operation or comparison is usize (or idiff), translation is refused (E-TYPE-NOMINAL). The same holds between usize and idiff. Number literals follow the type of their place and so are not caught by this rule.

3-3 A conversion between usize · idiff and other integer types is written with cast (§6.2.16 (2)). cast gives the value if it fits the target type and traps if it does not. widen and narrow are refused at translation when the source or the target is usize · idiff (E-TYPE-NOMINAL) — whether that conversion widens or narrows depends on the implementation’s width, so a word that states a direction cannot write text that is true on every implementation. narrow_try · narrow_sat · narrow_wrap, whose names choose what happens when the value does not fit, accept usize · idiff as targets.

3-4 If a literal does not fit the implementation’s usize (or idiff), translation is refused (E-TYPE-WIDTH). This is the only place among integer conversions where the verdict on the same text depends on the implementation — the value has a size not in that implementation’s address space, so it is refused earlier than a trap during execution. Refusals of text that uses what a target lacks (§5.6 (4) · (4-2) — heap · floating point · 128-bit integers · atomic widths) are outside this sentence.

module ex_usize .

fn bucket input xs slice u8 . input h u64 . output u8 .
  requires gt len xs. . 0 . .
do
  let slot u64 mod h. cast u64 len xs. . . . .
  return idx xs. cast usize slot. . . .
end .

fn checked input want u64 . output usize . do
  let p option usize narrow_try usize want. . .
  guard is_some p. . else return 0 . .
  return some_value p. . .
end .

module ex_usize_mix .

fn end_of input start usize . input more u64 . output u64 . do
  return add start. more. . .
end .

module ex_usize_widen .

fn as_u64 input n usize . output u64 . do
  return widen u64 n. . .
end .

3b u128 · i128 are integers of width 128. They stand only on targets of implementations that have 128-bit integers — using these words on other targets is refused at translation (E-INT128-TARGET). The implementation documents the targets on which they stand.

3b-1 From integers of other widths to a 128-bit place there is no automatic widening — write widen u128 … · widen i128 … (E-TYPE-WIDTH). The two operands of arithmetic · comparison · bit operations are both 128 bits or neither is. Number literals follow the type of their place — a literal beyond 64 bits fits only in a 128-bit place, and in other places translation is refused (E-LIT-RANGE, §6.1).

3b-2 128-bit integers stand in scalar places (locals · inputs · results · the contents of option · result) and also in struct fields and as the elements of slices · arrays · views · stacks. Their byte layout is the same as the target’s C compiler gives 128-bit integers — size 16 bytes, alignment 16 bytes, least significant end first (a field written big reverses it). Putting them as elements of vectors (vec · matrix) or at the extern boundary is refused at translation (E-INT128-PLACE) — there is no vector unit with 128-bit integer lanes, and the ABI of the C boundary has not yet been opened.

3b-3 A 128-bit input taken from the command line is the decimal number as written. A number outside the range of the type (a negative number or 2¹²⁸ or more for u128, outside ±2¹²⁷ for i128) is refused, not truncated — the same as the type range check at the entry boundary.

module ex_u128 .

fn wide_mul input a u64 . input b u64 . output u128 . do
  let x u128 widen u128 a. . .
  let y u128 widen u128 b. . .
  return mul x. y. . .
end .

fn top_half input a u64 . input b u64 . output u64 . do
  return cast u64 shr wide_mul a. b. . 64 . . .
end .

module ex_u128_field .

struct acc do
  lo u64 .
  big u128 .
end .

fn acc_bytes output usize . do
  return size_of acc . .
end .

module ex_u128_extern .

export extern fn take input a u128 . output u64 . do
  return 0 .
end .

3a usize is not a type that holds pointers. Its width follows the address width, but a pointer value may be larger than an address (§5.3 (4a)) and cannot be brought back from an integer. Use usize for sizes · lengths · indices, and write what points as slices and references.

6.2.3 The truth-value type§

1 bool has only two values, true and false. Its representation is 1 byte, and the only valid values are 0 and 1.

2 bool and integers do not convert into each other. An integer cannot be used in a condition position, and a bool cannot be counted as a number.

module ex_cond .

proc p input n u32 . output u8 . effects none .
do
  if n. do return 1 . end .     rem `n` is not a bool
  return 0 .
end .

6.2.4 Floating-point types§

1 f32 and f64 are the IEEE 754 binary 32-bit and 64-bit formats respectively.

2 Floating-point operations happen at the width of their operands. Operations between f32s are computed as f32, and the processor does not secretly compute in wider precision.

2a One operation is one rounding. The processor does not merge two operations into one rounding — it does not turn a multiply-and-add (add mul a. b. . c.) into one fused multiply-add instruction (FMA). Rounding is the single mode «to nearest, ties to even», and a program cannot change it. Code emitted as C carries this promise in its source too — it writes directives so that the C compiler building that code does not merge them itself.

3 Integers and floating-point numbers do not convert into each other automatically. To convert, it shall be written explicitly.

4 If the result of an operation is NaN, that it is NaN is fixed. The sign bit and the remaining bits of that NaN are a free choice (FC-0004).

6.2.5 Conversions between types§

1 Lowent has no implicit conversion that loses a value. A narrowing place is always written in the source. The only conversion the processor does by itself is the widening below; the word that writes any other conversion is cast (§6.2.16).

2 A conversion that loses no value is called widening. Widening does not change the value, so the processor may do it automatically — a u8 value may be passed as it is to a place that takes u32.

2a But widening may also be written in the source. widen u64 x. . widens x to u64. Even though the result is the same, it is used when the place where the width changes should be visible.

2b Widening to 128-bit integers (u128 · i128) is not automatic — it shall always be written with widen (§6.2.2 (3b-1)).

3 A conversion that may lose a value is called narrowing and is written with narrow. Narrowing traps if the value does not fit the target type. It is not truncated silently.

4 The relations in which widening is allowed are as follows. A combination not listed here is not widening, and writing it is refused at translation (E-WIDEN-KIND · E-WIDEN-SIGN · E-WIDEN-NARROW).

 u8 ──▶ u16 ──▶ u32 ──▶ u64          f32 ──▶ f64
   ╲       ╲       ╲
    ▼       ▼       ▼
 i8 ──▶ i16 ──▶ i32 ──▶ i64
 there is no arrow down at the same width (u8 → i8), and no arrow from the i row to the u row
 usize · idiff are not in this picture — there is no arrow either way, and the word that crosses is cast

let small u8 200 .
let wide u64 widen u64 small. . .
let back u8 narrow u8 wide. . .

6.2.6 Rows — arrays and slices§

1 array n t is a row of exactly n values of type t. The length is part of the type and is fixed at translation time.

1a Write the length n first, as an integer literal, and the element type after it — the same order as vec n t · matrix k d… t. Since the element type comes at the very end, the type knows its own end. Written the other way round (array t n — a type in the length position), it is refused (E-TYPE-ORDER; lowentc --fmt moves it to the new order). If the length is not a literal, it is refused (E-TYPE-ARRAY).

1b An op input input x array n t . means that it takes a slice t of length exactly n, and that length is checked at entry, like requires eq len x. . n. . ..

1c An op can return an array — output array n t ., or with a name, output r array n t . (§6.4.1 (3e)). An array has no way of being returned as a value, so the caller provides the place:

• The caller binds the result to a name — var x array n t f a … . (let is the same). The bytes in that name’s frame are the place of the result,

and the callee builds directly there (it does not copy).

• Inside an op that returns the same kind of array, return g … . passes on its own place as it is. But if an argument given to g can see the same bytes

as that place (the named result itself, or a name derived from it — a local whose initialiser or set right side mentioned it), the processor takes it into a temporary place and copies once — while g writes, the reading side does not see new values, so the answer is the same as when they do not overlap. It passes the place on directly only when they are seen not to overlap (when the arguments mention no such name). A return outside a block (guard … else return …) has no place to insert a statement, so this rule does not stand there — the E-RESULT-PLACE below applies as it is.

• Calling an op that returns an array in any other place (the middle of an expression · an argument of another call · the source of copy) has no place, so

translation is refused (E-RESULT-PLACE). Bind it to a name first.

• A named result starts at 0 (0 in every slot). return v. . of an unnamed result copies v into the place and returns. This shall be a return

inside a block — outside a block, as in guard … else return v. . ., it is refused (E-RESULT-PLACE). Such an op names its result.

• The elements are of number types and the length is an integer literal (anything else is E-TYPE-ARRAY).

1d Arrays inside arrays — the element type may itself be an array. array n array m t is a row of n rows of length m laid out row-major without gaps (the same layout as C’s t a[n][m]). Since the element type comes at the very end, no parentheses are needed ((1a)).

• idx a. i. . is a slice t (length m, no copy) that sees the bytes of row i — it follows the same rules as the sequence of rows of (9a). If the outer

one is mut, the slots of that row can be written too, and there is no set idx a. i. . <row> . that replaces a whole row (E-TYPE-SET).

• An op input input x array n array m t . takes a slice of rows slice array m t, and that the number of rows is n is checked at entry ((1b)).

A sequence of rows, and a row view over bytes (§8.7 (7a)), can be passed as they are.

• As a struct field it holds the bytes of n × m elements inside the record (the same as the array field of §6.2.7 (1a) — copying the struct copies them too).
• A value is built with lit array n array m t <row>… [_] .. Each row is lit array m t …, and a final _ fills the remaining rows with 0 ((6a)).
• The elements are sized numbers and bool. There is no limit on the number of levels — array 2 array 3 array 4 u8 is 2 planes of 3 rows of length 4 (C’s

u8 a[2][3][4]), and idx a. i. . is a slice of rows slice array 4 u8 that sees plane i. Each idx peels off one level. The rows of a sequence of rows · of a row view can also be arrays inside arrays (slice array 3 array 4 u8 · view_array array 3 array 4 u8 b.).

• The depth of levels is part of the type — passing or binding a slice of rows of a different depth is refused (E-TYPE-ARG · E-TYPE-LET). A slice of rows

does not fit a place for a slice of elements either (idx gives a row instead of a number).

• An op can return an array inside an array too — output r array n array m t .. As in (1c), the caller provides the place (var x array n array m t f … .),

and a named result starts as rows of 0.

module ex_nested_array .

fn rowsum input g array 2 array 3 u8 . input r usize . output u64 .
  requires lt r. 2 . .
do
  var s u64 0 .
  for x idx g. r. . do
    set s. add s. widen u64 x. . . .
  end .
  return s. .
end .

export fn table output u64 . do
  var g lit array 2 array 3 u8 lit array 3 u8 1 2 3 . _ . .
  set idx idx g. 1 . 2 . 7 .
  return add mul rowsum g. 0 . 100 . rowsum g. 1 . . .
end .

module ex_nested_three .

export fn f output usize . do
  var g lit array 2 array 3 array 4 u8 _ . .
  set idx idx idx g. 1 . 2 . 3 . 9 .
  let plane slice array 4 u8 idx g. 1 . .
  return add len plane. . cast usize idx idx plane. 2 . 3 . . . .
end .

module ex_nested_depth .

fn rows input g array 3 array 4 u8 . output usize . do
  return len g. . .
end .

export fn f output usize . do
  let c lit array 2 array 3 array 4 u8 _ . .
  return rows c. . .
end .

module ex_array_result .

fn squares input n u64 . output r array 3 u64 .
  requires le n. 1000 . .
do
  repeat i usize 3 do
    let v u64 add n. cast u64 i. . . .
    set idx r. i. . mul v. v. . .
  end .
  return r. .
end .

export fn total input n u64 . output u64 .
  requires le n. 1000 . .
do
  let s array 3 u64 squares n. . .
  return add add idx s. 0 . idx s. 1 . . idx s. 2 . . .
end .

module ex_array_result_expr .

fn squares input n u64 . output r array 3 u64 .
  requires le n. 1000 . .
do
  return r. .
end .

export fn first input n u64 . output u64 .
  requires le n. 1000 . .
do
  return idx squares n. . 0 . .
end .

2 slice t points at a range of values of type t laid out contiguously, and carries a start and a length together.

3 The length of a slice is read with len. len s. . is the number of elements of s, and its type is usize (§6.2 (3a)). The numbers given by bitset_count · stack_count and capacity are usize too. len used on the capability cap args is the number of arguments received.

3′ Indices and bounds (the i of idx, the start and end of subslice, the index of atomic operations, the capacity of alloc_bytes) are usize. Putting a value of another integer type in that place is refused at translation (E-TYPE-NOMINAL). Integer literals are written as they are. Where they meet numbers that are not lengths, write the conversion — cast u64 n. . moves a usize to u64, cast usize x. . moves a u64 to usize, and either way it traps if the value does not fit (§6.2 (3-3)).

3″ A value written to an element shall be of the slice’s element type — in set idx s. i. . v ., if v does not widen to the element type, translation is refused (E-TYPE-WIDTH · E-TYPE-SIGN · E-TYPE-NOMINAL). slice usize and slice u64 are different types even on an implementation where their elements have the same width (E-TYPE-NOMINAL) — declare a table that holds only positions as slice usize, and keep a table that holds numbers of several meanings at a fixed width and write cast where it is read and written.

3‴ usize counts what belongs to one piece: its length · an index within it · the number one operation read, wrote or processed in that piece. Such numbers cannot exceed the length of that piece, so they fit usize on every implementation. Running totals accumulated over many operations, and sizes · positions outside memory (the size and position of a file · the sum of bytes passed through a stream · the bit length of a whole message), can be large regardless of the address width, so they are not usize — keep them in fixed-width integers (u64). Hash values · checksums · random numbers are not lengths: keep them at the width of the value.

4 idx s. i. . is the i-th element of s. The number of the first element is 0.

5 If i is not less than len s. ., it traps. If the processor proves that the condition is always true, the check disappears (§6.4.6).

 memory   [ 10 ][ 20 ][ 30 ][ 40 ][ 50 ]
                  ^
 s = { start ─────┘ , len 3 }
 idx s 0 = 20 · idx s 2 = 40 · idx s 3 → trap (len s = 3)

module ex_slice .

rem A slice carries a start and a length together.
export fn head input data slice u8 . output u8 .
  requires ge len data. . 1 . .
do
  return idx data. 0 . .
end .

module ex_array_order .

export fn last input xs array u64 4 . output u64 .
do
  return idx xs. 3 . .
end .

6 Element-list literals — lit array n t v₁ … vₖ . is an array n t value, and lit slice t v₁ … vₖ . a slice t value of k elements. A list is a form closed by its own full stop: at the end of a statement the list’s dot and the statement’s dot come one after another (let t lit array 4 u8 1 2 3 4 . .); in the middle it is closed with one dot and the next operand follows. Since lit shows the type of the value, the binding statement does not write the type separately.

6a The number of array elements shall equal n. If there are fewer, a _ shall be written at the end of the list to say «the remaining slots are 0»; if there are more, or _ is somewhere other than the end, or a slice list has _, it is refused (E-LIT-COUNT). Slots are not filled silently.

6b Each element shall fit t — a negative number does not fit an unsigned t either (E-TYPE-WIDTH). bool elements are only true · false.

6c Filling chosen slots — lit array n t do <index> <value> . … [_ <value> .] end . puts each value into the slot whose index is written. The indices are integer literals from 0 to n − 1, each written once. _ <value> . comes only at the end and means «every slot whose index is not written». Every slot shall be decided — if slots remain and there is no _ <value> ., or _ has no slot to fill, it is refused (E-LIT-COUNT). If an index is not a constant, is outside the length, appears twice, or _ is somewhere other than the end, it is refused (E-LIT-INDEX). Values may be expressions and are computed in the order written; the value of _ is computed once. A list written as a block is a form too and is closed by its own dot — in let t lit array 8 u8 do 2 5 . _ 0 . end . . the first dot closes the list and the second closes let. It is not mixed with the form that lays out elements in a row

6d SIMD values — lit vec n t v₁ … [_] . is a vec n t value. The element rules are the same as for array lists; in addition t is a sized number (not bool), and n is a power of 2 from 1 to 16 (E-LIT-COUNT). The type of the value shall agree with the vec type of the binding place in number of lanes, element kind and width (E-TYPE-LANES · E-TYPE-WIDTH). Since it ends with placing values into lanes, the place rules of (7) do not concern it.

7 Where a list is placed and how long it lives is decided by the processor at translation as one of three. The author does not choose. ⓐ A list bound with var, and a let list containing elements computed during execution, have one slot per declaration site in that op’s frame. That slot is filled anew each time the declaration is executed (slots not written are 0) and lives until the block that holds the declaration ends — a declaration inside a loop is filled again on every iteration, and recursive calls each have their own slot. ⓑ A list whose elements are all translation-time constants and which is bound with let, or used only for reading without a receiving place, is read-only bytes fixed in the program. It lives to the end of the program, so it may be held anywhere. Binding it to a mut name (putting it back with set is the same), or passing the name bound with let to a mut · owned · mut_ref place, is refused (E-TYPE-ARGMUT). Whether two lists with the same contents (string literals too) are the same place is a free choice (§4.3 · FC-0003) — the processor may merge them into one copy or keep them apart. So a same_slice for which it is visible at translation that both sides came from such literals is refused (E-LIT-IDENTITY — the literal itself · a name bound to it with let · its subslice). Cases not visible across calls are not refused, but a program that relies on that answer does not conform. ⓒ A list used without a receiving name that contains elements computed during execution, or is passed directly to a mut · owned · mut_ref place, is a temporary in the frame that lives until that statement ends. The receiving op may rewrite those slots.

7a If a value that sees a slot of ⓐ · ⓒ is put in a place that lasts longer than its lifetime — return, a name declared outside the declaring block (including parameters and their fields · elements), a message sent to an actor declared outside the declaring block — it is refused (E-LIT-ESCAPE). It may be handed to an actor declared in the same block or further in, and the values that actor gives afterwards receive the same lifetime. Putting a temporary of ⓒ into a name is refused too — bind the list with var and use it as ⓐ. The flow is followed across calls: the result of a call carries only what belongs to the inputs that flow into the result in that op’s body, and a call that returns a scalar carries nothing out (the same distinction as region escape in §8).

7a-1 An unnamed struct value (the result of a call · lit) ends at the end of its statement. Putting a value that sees an array field of that value into a name · return · an outer place is refused (E-VIEW-TEMP) — once the statement ends, those bytes belong to the next value made. Only reading on the spot (taking numbers out with len · idx) conforms. To see a field for long, bind the struct to a name first (let b T … . and then field b. <field> .).

7b A list bound with var is a writable slice — slots are written with set idx buf. i. . v. .. set buf …, which rebinds that name to other storage, is refused (E-ARRAY-SET). Each element follows the width rule of (6b), and elements computed during execution shall agree with the element type (E-TYPE-SET · E-TYPE-WIDTH). A slot reached through idx and subslice is the same storage too — in set idx subslice buf. a. b. . i. . v. ., if buf is not a writable name it is refused (E-TYPE-MUT). A slice that cannot be written cannot be rebound to a mut slice name — let w mut slice u32 g. . and let w mut slice u32 subslice g. a. b. . . are refused if g is not a writable name (E-TYPE-MUT) — and so is putting it back into a var of type mut slice with set w. g. .. The new name points at the same storage, so writing through it is writing to g. A view view_array <type> g. does not copy either, so it is the same — binding it to a mut name, passing it to a mut input, or doing set · copy · store through it requires g to be a writable name (E-TYPE-MUT · E-TYPE-ARGMUT). The same holds when the receiving side of copy and store is a subslice. A var of a slice (or view) type without mut can be rebound to another slice but is not a name that writes slots — writing a slot through that name is E-TYPE-MUT, and passing it to a mut · owned input is E-TYPE-ARGMUT (whatever it holds — a read input or a string literal alike).

7b-1 Copying contents — copy <receiver> <giver> . copies the contents of the giving slice into the receiver. The receiver shall be writable (E-TYPE-MUT), the two element types shall be the same (E-TYPE-SET), and the two lengths shall be the same — if they are known to differ at translation it is refused (E-COPY-LEN), and if they differ during execution it stops. Even if two pieces of the same row overlap, it copies correctly (like a move whose ends overlap). Since it writes to the receiver, an fn that copies into a parameter is not pure (E-EFFECT-PURITY).

7b-2 Swapping — swap <slice> <i> <j> . exchanges the values of two slots. Since it writes slots, that slice shall be writable (E-TYPE-MUT — a let list · a string · a parameter that is not mut · an array built at translation cannot be written).

7c The total size of all slots of ⓐ · ⓒ in one op has a limit the processor states, and exceeding it is refused (E-FRAME-SIZE — it is not silently moved to the heap). This processor’s limit is 65,536 bytes on a machine with an operating system · 4,096 bytes on a machine without one. If an op with such slots can reach itself (even through other ops), it is refused (E-FRAME-RECURSIVE) — frames multiply by the recursion depth, and that depth is not known at translation, so it cannot be shown that the stack does not run out. A list inside recursion is taken from an allocator ((7d)). If, following the call relation, the sum of ⓐ · ⓒ slots alive at the same time on the deepest path exceeds the budget below, translation is refused (E-STACK-BUDGET) — it is measured per entry (an op nobody calls). Ops that run as tasks (spawn <op> · the handler of spawn send) are measured separately against the green-thread budget. During execution, too, the sum of ⓐ · ⓒ slots and the struct slots of (7c-1) alive at the same time on one call chain has a budget the processor states, and it stops rather than enter an op that would exceed it — the stack does not overflow and break silently. This processor’s budget is 4 MiB on a machine with an operating system · 64 KiB per green thread · 16 KiB on a machine without an operating system, and every back end counts with the same numbers and stops at the same place.

7c-1 The place of a struct value is its op’s frame. For each op the processor decides at translation the number of frame slots that struct value lits and calls returning a struct will use — a value at a place for which there are not enough slots lives in the pool of §8.1 (3a). The share of the slots (8 bytes per field · the bytes of an array field) counts towards the budget of (7c). When the frame ends, the value ends too, and a returned value is copied into the caller’s place. Recursion is not refused for frame slots — frames pile up by the depth, and the budget of (7c) stops it during execution. If, on a path without recursion, struct values push the deepest path beyond the budget, translation is refused (E-STACK-BUDGET). An op that takes or makes references can write to someone else’s place, so it does not use frame slots (its values live in the pool).

7d A list taken from an allocator — var <name> use <allocator> mut slice t lit array n t … else <statement> (lit slice is the same) asks that allocator for the byte count of the list (send <allocator> reserve <bytes>); if it receives them, it fills those bytes as in (6)–(6c) and binds them to the name; if not, it goes to else (§6.5.1 (5)). To carry the failure along as an option, write the whole type — let <name> use <allocator> option mut slice t lit … .. If there is neither else nor option, or it is lit vec, it is refused (E-LIT-USING). If the element of the binding type differs from the element type of the list, it is refused (E-BIND-ELSE). The bytes belong to the allocator, so unless (7e) applies they do not receive the declaring-block lifetime of (7a) but follow the allocator’s lifetime: if the allocator received a slot of ⓐ as its backing (send <allocator> init buf), the bytes that allocator gives receive that slot’s lifetime too. A struct value is built in allocator bytes with the same spelling: var <name> use <allocator>. s lit s do … end . else <statement> . asks for size_of s . bytes; if it receives them, it fills them with 0, lays the layout of s over them (the same representation as view of §8.7.2) and writes the fields given. The binding type shall be s (E-BIND-ELSE). A slice field of numbers is placed in the allocator bytes as two words (address, length) — the same as C’s struct { const T *p; size_t n; }, aligned to 8 bytes. This layout exists only for structs built in an allocator: laying such a struct over someone else’s bytes with view, or asking its size with size_of, is still refused (bytes must not become addresses). If a value given to a slice field sees a place in a frame, the struct receives that place’s lifetime too — even if kept with keep, carrying it longer than that place is refused (E-LIT-ESCAPE). Structs with owned · actor · capability fields, slice fields whose elements are not numbers, or inner structs without a layout are not built (E-LIT-UNBUILT) — those bytes would have to end together with their fields.

7e Given back at the end of the block — if the allocator provides freeing_allocator (§8.13 (6)), bytes received through (7d) are given back to the allocator when leaving the block that declared the name (send <allocator> release <the piece received>). This holds on reaching the end of the block · on return · on break · continue inside that block. If several were received in one block, they are given back in reverse order of declaration, and what was not received (what went to else) has nothing to give back. The answer of release is not used — whether to take it back is the allocator’s policy. So these bytes receive the declaring-block lifetime of (7a): carrying them outside the block is refused (E-LIT-ESCAPE). Bytes of an allocator that is not a freeing_allocator stay with the allocator. When stopping with panic, they are not given back — stopping hands that op over to the recovery unit. The author can give them back earlier with drop <name> .. Then they are not given back again at the end of the block. drop is accepted only in the block that declared the name (in an inner block it is E-OWN-JOIN), and using the name after it is refused (E-OWN-MOVED).

7f Kept — var <name> keep <allocator> … else <statement> switches off (7e): the bytes are not given back on leaving the block, so they follow the allocator’s lifetime (§6.2.6 (7d)) and can be carried outside the block — by return too. Giving them back is the author’s job (send <allocator> release <piece>). Otherwise they all go back together when the allocator ends. keep <allocator> stands in the place of use <allocator> (directly after the name) and is used only on bindings that take a list or struct literal (E-USING-FORM).

8 An array list bound with let is a slice that sees those bytes. The list decides the length.

9 The elements of a list may be structs with a byte layout (all fields sized numbers — structs on which view of §8.7.2 can stand). An element is a copy of the value given, and the list is a slice s with a view like view_array laid over those bytes. A field of an element is written with set field <list>. <position> <field> . v. .. Place · lifetime · _ · filling chosen slots · the allocator clause are the same as for number elements. If the value in an element position is a number or a truth value it is refused with E-TYPE-FIELD; if it is another struct, with E-TYPE-STRUCT. Lists this processor has not yet built — structs without a byte layout · structs whose fields are structs · filling chosen rows (do … end) — are refused saying what is not yet built (E-LIT-UNBUILT). Array fields inside structs are specified by §6.2.7 (1a).

9-1 A struct whose fields are only sized numbers · bool and slices of numbers can also be an element of a list. Inside an element a slice field is placed as two words (the place it points at, the length) — the same layout as a struct built in allocator bytes ((7d)). The fields are written at execution, so such a list stands in a frame place of ⓐ. A slice s input taking the same elements, and an array result output r array n s ., use this layout too. A slice field only points at someone else’s bytes, so copying an element does not copy the bytes it points at.

9a A list of rows — the type of a list lit slice array m t <row>… . whose elements are fixed-length arrays (array m t) is slice array m t. Like other slice lists ((6)) the number of rows is not written and there is no _ ((6a)) — a row of 0 is written lit array m t _ .. lit array n array m t <row>… [_] ., with the number of rows written, is the value of an array inside an array ((1d)). Over existing bytes a row view of the same type is laid with view_array array m t b. (§8.7 (7a)). len is the number of rows, and idx g. r. . is a slice t (length m, no copy) that sees the bytes of row r — if the outer one is mut, the slots of that row can be written too. Row values are copied slot by slot, and if the shape of a row literal differs from array m t it is refused (E-LIT-COUNT). There is no set idx g. r. . <row> . that replaces a whole row (E-TYPE-SET) — write the slots, or copy with copy. The rows (and struct elements) of a list in a frame see that frame’s bytes, so carrying them outside the block is E-LIT-ESCAPE.

module ex_list_literal .

fn total input xs slice u32 . output u64 . do
  var s u64 0 .
  for x xs. do
    set s. add s. widen u64 x. . . .
  end .
  return s. .
end .

rem An array list is closed by its own dot — at the end of a statement there are two dots.
export fn f output u64 . do
  let t lit array 4 u32 10 20 30 _ . .
  return add total t. . total lit slice u32 1 2 . . . .
end .

module ex_frame_list .

export fn squares input n usize . output u64 . do
  var buf lit array 8 u64 _ . .
  var i usize 0 .
  while lt i. 8 . do
    set idx buf. i. . cast u64 mul i. i. . . .
    set i. add i. 1 . .
  end .
  guard lt n. 8 . else return 0 . .
  return idx buf. n. . .
end .

module ex_cell_fill .

export fn pick input a u64 . input i usize . output u64 . do
  let t lit array 6 u64 do 0 100 . 5 mul a. 2 . . _ 1 . end . .
  guard lt i. 6 . else return 0 . .
  return idx t. i. . .
end .

module ex_cell_twice .

export fn f output u64 . do
  let t lit array 4 u8 do 1 1 . 1 2 . _ 0 . end . .
  return len t. . .
end .

module ex_frame_escape .

export fn f output slice u8 . do
  var b lit array 2 u8 1 2 . .
  return b. .
end .

module ex_list_short .

export fn f output u64 . do
  let t lit array 4 u8 1 2 3 . .
  return len t. . .
end .

6.2.6.1 Rows of several dimensions — matrix§

1 matrix k d1 … dk t is a row of k dimensions holding d1 × … × dk values of type t. The number of dimensions and the sizes are part of the type and are fixed at translation. If even one of the number of dimensions or the sizes differs, it is a different type — matrix 2 3 4 u32 differs from matrix 2 4 3 u32 and from array 12 u32.

1a Write the number of dimensions first, then as many sizes as there are dimensions, and the element type at the very end (the same order as §6.2.6 (1a)). The number of dimensions is from 2 to 8 and the sizes are 1 or more, all plain decimal literals (in an op input a size may be the name of a translation-time value input — (3a)). The old order (matrix t k d… — element type first) is refused (E-TYPE-ORDER). The number of elements (the product of the sizes) cannot exceed 2^32. matrix or array cannot be written as the element type. Violations are refused (E-MATRIX-TYPE).

2 Layout. The elements are laid out contiguously in one block, row-major — the last index runs fastest. Size and alignment are the same as array n t (n is the product of the sizes), and no header is added.

3 A matrix type is written in places that make a name — the type of let · var, an op’s input and output, a struct field. It cannot be written as the element of another type, as a type argument or in the place of an alias (E-MATRIX-USE).

3a Only in an op’s input, the name of a translation-time value input of that op can be written in a size position — input comptime r u64 . input comptime c u64 . input m matrix 2 r c u32 .. The caller writes a number for that input (sum 3 4 a. .), and the shape of the argument shall be the same as the shape read with those numbers (E-MATRIX-SHAPE). The sizes of let · var · output · struct fields and of lit matrix shall be numbers (E-MATRIX-TYPE).

4 Values. lit matrix k d1 … dk t <element>… . lists the elements in row-major order. The number of elements shall equal the product of the sizes; if there are fewer, write _ at the end to fill the rest with 0. If a binding writes both a type and a literal, the two shapes shall be the same. Violations are refused (E-MATRIX-SHAPE). In a struct literal, the value of a matrix field is a lit matrix of the same shape as that field.

5 Reading and writing. idx m. i1 … ik . takes one index per dimension. If the number of indices differs from the number of dimensions, it is refused (E-MATRIX-INDEX) — an idx with fewer indices does not mean a row (a row is the row of (7a)). Each index is checked against the size of its own dimension: if any one of them is that size or more, execution stops. Index expressions are computed once each, in the order written. set idx m. i1 … ik . v. . writes that slot, and m shall be a writable name (E-TYPE-MUT).

6 dim m. j . is the size of dimension j (counting from 0). j shall be a plain decimal literal less than the number of dimensions (E-MATRIX-INDEX). Its value is a translation-time constant.

7 flat m. . is a slice t that sees the same elements as one row. It does not copy, and its length is the number of elements.

7a row m. i1 … i(k−1) . is the row that leaves one last dimension — one index for each dimension except the last, and its value is a slice t that sees the elements of that row. It does not copy, and its length is the size of the last dimension. If the number of indices differs it is refused (E-MATRIX-INDEX), and each index is checked against the size of its own dimension as in (5). If m is a writable name, that row can be bound to a mut slice t name and written; otherwise it cannot be bound that way (E-TYPE-MUT · E-IMMUTABLE if it is a field of a struct bound with let). There is no view that leaves two or more dimensions (a plane).

7b In the m position of (5) · (6) · (7) · (7a), not only a name written as matrix stands but also field x. g . that points at a matrix field — idx field b. g . r. c. ..

8 len m. . and for x m. do … end . are refused (E-MATRIX-USE). The size of one dimension is written with dim, and going over all elements with for x flat m. . do … end ..

9 The places where a matrix name can be written whole are the first argument of idx · row · dim · flat, an argument of an op with an input of the same shape, and the return of an op with a result of the same shape. Other places are refused (E-MATRIX-USE). Arguments and inputs, and the type of a binding and the result of the op called, shall agree in both number of dimensions and sizes (E-MATRIX-SHAPE).

9a A call of an op whose result is a matrix is placed in only two places — the value of a binding that makes a matrix name of the same shape, and the value of the return of an op with a result of the same shape. The return of an op whose result is a matrix gives a matrix name of that shape or a call of an op that gives that shape. Violations, including binding it to an array name or returning it from an op that gives an array, are refused (E-MATRIX-SHAPE).

10 This type specifies only places. It does not specify computations such as matrix multiplication.

module ex_matrix .

fn table output t matrix 2 3 4 u32 .
do
  repeat r usize dim t. 0 . do
    repeat c usize dim t. 1 . do
      set idx t. r. c. . cast u32 add mul r. 10 . c. . . .
    end .
  end .
  return t. .
end .

export fn row_sum input r usize . output u64 .
  requires lt r. 3 . .
do
  let t matrix 2 3 4 u32 table . .
  var s u64 0 .
  repeat c usize dim t. 1 . do
    set s. add s. widen u64 idx t. r. c. . . . .
  end .
  return s. .
end .

module ex_matrix_more .

struct board do
  id u64 .
  g matrix 2 3 4 u32 .
end .

fn sum input comptime r usize . input comptime c usize . input m matrix 2 r c u32 . output u64 .
do
  var t u64 0 .
  repeat i usize dim m. 0 . do
    for x row m. i. . do set t. add t. widen u64 x. . . . end .
  end .
  return t. .
end .

export fn total output u64 .
do
  var b lit board do id 1 . g lit matrix 2 3 4 u32 1 2 3 4 5 6 7 8 9 10 11 12 . . end . .
  set idx field b. g . 0 0 . 100 .
  let small lit matrix 2 2 2 u32 1 2 3 4 . .
  return add widen u64 idx field b. g . 0 0 . . sum 2 2 small. . . .
end .

module ex_matrix_row .

export fn f output u64 . do
  let m lit matrix 2 2 3 u32 1 2 3 4 5 6 . .
  return widen u64 idx m. 1 . . .
end .

module ex_matrix_shape .

fn first input m matrix 2 3 4 u32 . output u32 . do
  return idx m. 0 0 . .
end .

export fn f output u32 . do
  let m lit matrix 2 4 3 u32 _ . .
  return first m. . .
end .

6.2.7 Aggregates — struct and enum§

1 A struct is a collection of named fields. Each field has its own type.

1a Array fields — if the type of a field is array n t, that field holds the bytes of n elements inside the record (since the length is in the type, the place is fixed). t is a sized number or bool — fields whose elements are structs or arrays this processor has not yet built (E-LIT-UNBUILT). The sum of the bytes of the array fields of one struct has the same limit as a frame (E-FRAME-SIZE, §6.2.6 (7c)). field r. body . is a slice that sees those bytes, and set idx field r. body . i. . v. . writes an element of the record. A list literal given to the field shall have the same element type and length as the field (E-TYPE-FIELD). In a byte layout (view · encode · size_of · the C-side layout) an array field lies as it is inside the struct bytes, as in C — its size is n × |t| and its alignment that of t (len u8 . body array 4 u8 . tail u16 . is 8 bytes — len from byte 0 · body from byte 1 · tail from byte 6). The array field of a view is a slice that sees those bytes, and writing the field copies into that place.

2 An enum is one of several. Each variant has a name and may carry values.

2a Each variant is closed with .. A newline is not a closer, so variants written one per line without dots run together into one variant and are refused (E-ENUM-DOT). The values a variant carries are written as <field name> <type> pairs — if the pairs do not match, it is refused (E-ENUM-FIELD).

2b An enum value is not a number — to use a variant’s number as a number, write cast (§6.2.16 (5)).

2c Every variant has a number. The first variant is 1, and the next variant is the number of the previous variant plus 1. An integer written after a variant name (ga 11 .) becomes that variant’s number, and the next variant counts on from there. The numbers shall increase in the order declared — a number not greater than the previous variant’s number is refused (E-ENUM-NUMBER). Numbers are written only in an enum with no variant that carries values (E-ENUM-NUMBER). 0 is not the first variant’s number — in an enum whose numbers are not written, 0 is no variant.

module ex_enum_numbers .

enum hangul do
  ga 11 .
  na .
  da 101 .
  ra .
end .

fn n input h hangul . output u32 . do
  return cast u32 h. . .
end .

rem 11 + 12 + 101 + 102
fn total output u32 . do
  return add add n ga. . n na. . . add n da. . n ra. . . . .
end .

total() = 226

module ex_enum_number_falls .

enum level do
  low 5 .
  mid .
  high 6 .
end .

2d The width of an enum. An enum whose variants carry no values may have one line layout <width> . in its block. The width is one of u8 · u16 · u32 · u64, and is the number of bytes the enum occupies when it enters a byte layout (§6.2.13) — the bytes hold the variant’s number (2c). This line is not a variant. An enum without a width has no byte layout. The following are refused (E-ENUM-LAYOUT): a width outside the four, a variant number that does not fit the width, an enum with a variant that carries values, two layout lines. ☞ Why the width is not chosen automatically: adding one variant must not silently change a layout beyond a wire or a file.

module ex_enum_layout .

enum kind do
  layout u8 .
  ping .
  data 7 .
  close .
end .

struct hdr do
  layout packed .
  k kind .
  len u16 big .
end .

fn kind_of input b slice u8 . output u8 . do
  let o option view hdr try_view hdr b. . .
  guard is_some o. . else return 0 . .   rem 2 is the number of no variant
  let h view hdr some_value o. . .
  match field h. k . do
    case ping do return 1 . end .
    case data do return 2 . end .
    case close do return 3 . end .
  end .
end .

kind_of([7,0,3]) = 2 · kind_of([2,0,3]) = 0

module ex_enum_layout_fit .

enum code do
  layout u8 .
  ok .
  far 300 .
end .

3 A struct cannot have itself as a field. If it cycles, directly or through other types, translation is refused (E-STRUCT-CYCLE). Because its size would not be fixed.

3a If it points to itself through a reference, the size is fixed. But if that reference is one whose manager cannot be known, it is refused (E-STRUCT-REF-UNMANAGED) — having a size does not mean the lifetime is settled.

3b If the type of a field is exactly option (owned <that struct>), it is not regarded as the cycle of (3). That field is not a value but one address slot pointing at another node built in allocator bytes (none when empty), so the size is fixed. Such a struct is called a node that holds itself, and the rules for building and giving it back are specified by §8.5 (10)–(13). owned <itself> without option, and ownership cycles that come back through another struct, are still caught by (3).

module ex_shape .

struct point do
  x u32 .
  y u32 .
end .

enum color do
  red .
  green .
end .

4 A struct value is made with lit. When made, every field shall be filled. _ <value> . on the last line puts that value into every field not written (lit pt do y a. . _ 0 . end .) — the value is one name or literal (E-LIT-INDEX); if a field remains that the value cannot go into, it is refused naming that field (E-TYPE-FIELD); and if there is no field to fill, it is refused (E-LIT-COUNT).

4a A struct is a value. When it is made or copied (var q point p. .), the bytes of its array fields and the other struct values in its fields are copied with it — changing the copy does not change the original. Actor instances (things with an identity) and structs with owned fields are not copied but point at the same thing.

4b Writing a field is writing to that record. set field r. x . v. . and writing an element of an array field are accepted only when r is a writable place: a var or a mut parameter. Writing to a record bound with let is refused (E-IMMUTABLE) — so is taking an array field out as a writable slice (mut slice). Writing a field of a parameter received by value writes to that op’s local copy — the caller’s record does not change (§6.5.1 (2a)).

5 A field is read with field <value> <field name>. There is no form that attaches a dot and a field name after the value (E-FIELD-GLUED) — the dot is already used for module qualification and variant names.

module ex_make .

struct point do
  x u32 .
  y u32 .
end .

export fn origin output point .
do
  return lit point do x 0 . y 0 . end . .
end .

export fn get_x input p point . output u32 .
do
  return field p. x . .
end .

module ex_struct_array .

struct pkt do
  len u8 .
  body array 4 u8 .
end .

export fn copy_keeps input a u8 . output u64 . do
  var p lit pkt do len 2 . body lit array 4 u8 1 a. _ . . end . .
  var q pkt p. .
  set idx field q. body . 0 . 100 .
  return add widen u64 idx field p. body . 0 . . widen u64 idx field q. body . 0 . . . .
end .

module ex_struct_array_let .

struct pkt do
  body array 4 u8 .
end .

export fn f output u64 . do
  let p lit pkt do body lit array 4 u8 _ . . end . .
  set idx field p. body . 0 . 1 .
  return 0 .
end .

module ex_enum_dot .

enum color do
  red
  green
end .

6.2.8 Types that hold an answer — result and option§

1 result t e holds either a successful value (t) or an error (e).

2 option t holds either a value or none.

3 Values of these two types shall be checked for which side they are before being taken out.

3a Taking out is a partial operation — taking out without checking is not itself refused at translation, and taking out the absent side during execution traps. That is, the check is not done for the author by translation; the author does it.

3b The type of the contained value is part of the type. option usize and option u64, result u32 e and result u64 e are different types, and putting one in the place of the other is refused at translation (E-TYPE-NOMINAL · E-TYPE-WIDTH · E-TYPE-SIGN). The type of a value taken out (some_value · ok_value) is the type of the contained value. When some · ok wrap a literal, it follows the type of the receiving place.

3c A value of result · option is not an operand of arithmetic or comparison (eq · lt …) (E-TYPE-KIND). Write what is being asked — is_some · is_ok · value_or.

module ex_result .

enum err do
  too_small .
end .

rem If it is less than 2, report that it cannot be halved.
export fn half input n u32 . output result u32 err .
  errors too_small lt n. 2 . .
do
  guard ge n. 2 . else return error too_small . . .
  return ok div n. 2 . . .
end .

4 The making side wraps values with ok (success) error (error) some (a value is present) none (no value).

5 The receiving side first asks which side it is — is_error (is it an error) is_some (is a value present). Then it takes out — ok_value (the success value) error_value (the error) some_value (the present value).

 ok v  | error e  ──▶ is_error r ── false ──▶ ok_value r    = v
                                 └─ true ──▶ error_value r = e
 some v | none    ──▶ is_some o  ── true  ──▶ some_value o  = v
                                 └─ false ─▶ some_value o  → trap

6 value_or gives the value if there is one, otherwise the value given in its place. It reduces the two steps of asking and taking out to one.

7 try takes a result, takes out the value on success, and on failure passes that error on upward as it is (§6.5.7).

8 If a result is received and nobody looks at it, the processor reports it (W-RESULT-DISCARD). The design of returning failure as a value is kept only when the receiving side looks at that value. There are two shapes of not looking — calling the op as a statement and discarding the value without even a name, and putting it into a name and never reading it.

8a A place that deliberately lets a failure pass is written drop <name> .. Then it is not reported. There are places where there really is nothing to do with a failure — such as the place on an error path that closes resources and leaves. drop already means «I end this here», so no new word is put in that place.

module ex_partial .

fn mk input k u8 . output option u8 .
do
  guard lt k. 3 . else return none . .
  return some mul k. 10 . . .
end .

rem Take it out at once without checking — translation passes.
fn raw input k u8 . output u8 .
do
  return some_value mk k. . . .
end .

raw(2) = 20 · raw(7) → E-VM-NONE (trap)

module ex_option .

rem The making side — some if there is a value, none if not.
fn lookup input k u8 . output option u8 .
do
  guard lt k. 3 . else return none . .
  return some mul k. 10 . . .
end .

rem The receiving side ① — ask, then take out.
fn use_ask input k u8 . output u8 .
do
  let r option u8 lookup k. . .
  guard is_some r. . else return 255 . .
  return some_value r. . .
end .

rem The receiving side ② — if absent, give a value to use instead.
fn use_or input k u8 . output u8 .
do
  return value_or lookup k. . 99 . .
end .

use_ask(2) = 20 · use_ask(7) = 255 · use_or(2) = 20 · use_or(7) = 99

module ex_result_use .

enum io_error do
  too_big .
end .

rem The making side — when it fails is written in the contract.
fn halve input a u8 . output result u8 io_error .
  errors too_big gt a. 200 . .
do
  guard le a. 200 . else return error too_big . . .
  return ok div a. 2 . . .
end .

rem The receiving side ① — ask, then take out.
fn use_ask input a u8 . output u8 .
do
  let r result u8 io_error halve a. . .
  guard not is_error r. . . else return 0 . .
  return ok_value r. . .
end .

rem The receiving side ② — try passes the failure on upward as it is.
fn use_try input a u8 . output result u8 io_error .
  errors too_big gt a. 200 . .
do
  let v u8 try halve a. . . .
  return ok add v. 1 . . .
end .

use_ask(100) = 50 · use_ask(250) = 0 · use_try(100) = ok 51

6.2.9 Named types§

1 type gives an existing type another name. The two names are the same type and can be used interchangeably.

2 newtype makes a different type with the same representation as an existing type. They cannot be used interchangeably.

2a The shapes are type <name> <type> . and newtype <name> <type> .. No word is inserted between the name and the type.

module ex_newtype_mix .

newtype node_id u64 .

fn f input a node_id . input b u64 . output u64 . do
  return add a. b. . .
end .

2b The type of type and newtype cannot itself be a row type — slice · array · matrix. The same holds with mut in front. A row type is written as it is where it is used. A row type inside another type can be given a name (type found option slice u8 .). If a type with its own name is needed, put it as a struct field (§6.2.7).

module ex_rowname .

type bytes slice u8 .

fn f input b bytes . output u64 . do
  return len b. . .
end .

3 When a newtype is used as a name that separates storage (brand), one brand points at one storage. Opening storage twice with the same brand is refused (E-BRAND-REUSED) — then one name would point at two, and handles from different storage would look like the same type. That is exactly the confusion the brand was meant to prevent. If they must be separated, declare one more newtype.

6.2.10 Reading inside a value — field§

1 field is the form that reads what is inside a value. Its shape is field <value> <step> …, with one or more steps. With several steps it goes down one level at a time from left to right — field o. inner deep . means inner of o, and deep inside that.

2 A step is one of two things. A name is a field of a struct, and an integer is a position in a row (array · slice). The two may be mixed.

3 field is also a place — it can come on the left of set. The reading place and the writing place have the same spelling.

4 If a field not in the declaration is written, the processor refuses the program. Positions in rows follow the bounds rules of §6.2.6.

module ex_field .

struct inner do
  a u64 .
end .

struct outer do
  i inner .
end .

export fn read_deep input o outer . output u64 .
do
  return field o. i a . .
end .

export proc bump_deep input o mut outer .
  effects state .
do
  set field o. i a . 1 .
end .

6.2.11 Values with lanes — vec§

1 vec <lane count> <element type> holds several values of the same type as one value (the same order as §6.2.6 (1a) — the lane count comes first; the old order vec <element type> <lane count> is E-TYPE-ORDER). scalable can also stand in the lane-count position (vec scalable u8). The lane count shall be a value fixed at translation time (§6.8).

2 Two vecs with different lane counts are different types and do not mix.

3 Arithmetic on a vec happens per lane, separately. Values do not cross between lanes.

3a The per-lane arithmetic is add · sub · mul · div · mod · neg · abs · min · max. Overflow of integer lanes wraps at the lane’s width (unlike scalars — the quotient of the smallest value of a signed lane divided by −1, and its neg · abs, are that value itself). If an integer lane’s div · mod has a lane whose divisor is 0, it stops as for scalars. The quotient is truncated towards 0, mod follows the sign of the divisor (§6.3), and min · max of signed lanes compare by sign (2026-11-02). Floating-point lanes have no mod — as for scalars, translation is refused (§6.3.3 (2a) · E-TYPE-KIND).

module ex_vec_order .

export fn sum4 input xs slice u32 . output u32 .
  requires ge len xs. . 4 . .
do
  let v vec u32 4 load xs. 0 . .
  return reduce_add v. . .
end .

6.2.12 Sets made of bits — bitset§

1 bitset <bit count> holds whether each value from 0 up to, but not including, that count is present. The bit count shall be a value fixed at translation time.

2 Inserting or asking about a value outside the range does not conform.

3 A bitset is a set, not the bits of a word. Handling the bits of a word is bit operations (§6.3), and the two are different things.

4 Inserting an element is bitset_insert <set> <value> ., removing one is bitset_remove <set> <value> . — both change the set in place. add means only the addition of numbers, so using it on a set does not conform (E-BITSET-ADD).

4a The number of elements in a set is bitset_count <set>, and its type is usize. The number of elements of a stack is stack_count <stack>. Using one in place of the other, or using len (the length of a piece) on a set · stack, is refused at translation (E-TYPE-ARG).

module ex_bitset .

fn members output usize . do
  var s bitset 8 bitset_new 8 . .
  bitset_insert s. 3 .
  bitset_insert s. 5 .
  bitset_remove s. 3 .
  return bitset_count s. . .
end .

members() = 1

6.2.13 An eye laid over bytes — views§

1 A byte slice can be read, without copying, as if it were an array of another type. This is called a view.

2 When a view is obtained, the alignment and length contract is checked. If the contract is broken, the program stops.

3 A view does not copy bytes. Writing through a view changes the original bytes.

4 The opposite of a view is encode. encode <shape> <value> writes the value into bytes in the layout the shape specifies. If laying over and reading is view, writing down is encode.

5 A view laid over a struct is a window. view <struct> <bytes> gives a window that lays the layout of that struct over a byte slice. Reading a field of the window reads the bytes at that place, and writing a field writes the bytes at that place — it is not a copy. The type of a window is view T (a read window) or mut view T (a write window), different from the type T of a struct value. try_view does the same but gives none if the length · alignment do not fit or a field does not fit (9a) — its type is option view T · option mut view T, and some_value is the window. The conditions on length and alignment are specified by §8.7.2.

6 Windows and values do not mix. Putting a window in the place of a struct name T · option T — binding · returning · putting a whole struct value into a window name — is refused at translation (E-VIEW-COPY). A copy that lives apart from the bytes is made with cast T <window> . (§6.2.16 — an explicit conversion is cast). Binding a window to another window name sees the same bytes. A window can also be passed to an input that takes a value (input p T .) — the receiver only reads.

7 Whether something can be changed is written in its type (§8.8 (2)). A write window comes only from writable bytes — binding a write window from a shared input, a slice bound without mut, a string literal, a read window, or the result of an op that gives a read window is refused (E-TYPE-MUT). Writing a field through a read window or doing write_volatile is E-TYPE-MUT, passing a read window to a mut input is E-TYPE-ARGMUT, and returning a window over read-only bytes when the output is mut view T is E-TYPE-RETMUT. If an fn writes through a window over bytes it received as mut — whether laid directly or returned by another op — that is visible to the caller, so it is not pure (E-EFFECT-PURITY, §7.3 (6)).

8 A struct a view can be laid over is a struct whose byte layout is fixed. Each field shall be a number of fixed width (u8…u64 · i8…i64 · f32 · f64), a bool, an enum with a written width (§6.2.7 (2d)), a fixed array of those, or a struct made of such fields. Enums without a written width · slices · option · owned-handle fields have no fixed bytes, so neither a view nor encode can be used on such a struct (E-IR-UNDEF).

9 Every field of a struct read with view and view_array shall be plain (§8.7.1 (2)). A bool field that receives a byte other than 0 · 1 becomes a value that is neither true nor false, and an enum field that receives a number belonging to no variant becomes a value that is no variant, so if there is even one such field (including in inner structs) it is refused (E-TYPE-BITCAST) — for the same reason that bit_cast bool is refused. view_array bool is the same. encode, which writes values down into bytes, has no such restriction.

9a try_view measures such fields — if the byte of a bool field is not 0 · 1, or the number of an enum field is not the number of any variant of that enum, it gives none. It measures the fields of inner structs too. Reading an enum field of a value obtained that way gives the variant of that number, and writing an enum field puts that variant’s number into the bytes. If, after measuring, the underlying bytes change by another path so that they are no variant’s number, execution stops the moment that field is read.

module ex_struct_view .

struct pt do
  x u8 .
  y u8 .
end .

proc write_through input b mut slice u8 . output u8 . effects none . do
  let h mut view pt view pt b. . .
  set field h. y . 9 .     rem b becomes [1,9]
  return idx b. 1 . .
end .

proc copy_by_name input b mut slice u8 . output u8 . effects none . do
  let h view pt view pt b. . .
  var k pt cast pt h. . .  rem a copy that is a struct value
  set field k. y . 7 .
  return idx b. 1 . .      rem b is unchanged
end .

write_through([1,2]) = 9 · copy_by_name([1,2]) = 2

module ex_struct_view_ro .

struct pt do
  x u8 .
  y u8 .
end .

proc f input b slice u8 . output u8 . effects none . do
  let h mut view pt view pt b. . .  rem writing a field would change the caller's b
  set field h. y . 9 .
  return 0 .
end .

module ex_struct_view_copy .

struct pt do
  x u8 .
  y u8 .
end .

fn f input b slice u8 . output u8 . do
  let h pt view pt b. . .  rem a window or a copy? — `view pt` or `cast pt`
  return field h. y . .
end .

module ex_struct_view_bool .

struct flag do
  active bool .
  n u8 .
end .

fn f input b slice u8 . output u8 . do
  let h view flag view flag b. . .
  return field h. n . .
end .

6.2.14 Parameters with a narrowed range of values — range§

1 If range <low> <high> is written in the type position of a parameter, that parameter accepts only values between the two ends, both included.

2 If the caller cannot prove that the value is within that range, translation is refused. A value that came from outside the program (an argument of the entry point and the like) has no caller to prove it, so it is checked at the boundary, and the program stops if it is out of range.

2a If the caller’s type is wider than the range, that alone is refused (E-TYPE-WIDTH). A value of the same width, which is not caught by that check, has its range checked at the op’s entry and stops if it is out of range (E-VM-CONTRACT) — the same check as writing requires ge <name> <low> . and requires le <name> <high> ..

3 A declared range is used with the same standing as a contract of §6.4 — the checker may take it as a fact and remove the checks that follow.

module ex_range_wide .

fn scale input a range 0 100 . output u8 .
do
  return narrow u8 a. . .
end .

fn call_scale input x u64 . output u8 .
do
  return scale x. . .    rem `u64` is wider than 0 … 100 — it was not shown to be within the range
end .

6.2.15 Nailing down the byte layout — layout and align§

1 A layout can be written inside a struct declaration. If none is written, fields are placed in declaration order, each aligned to its type’s alignment (with as much padding between as alignment requires). The processor does not change the order.

2 layout packed . puts no padding between fields — the fields are packed together in declaration order.

2a The layout words are a closed two — packed and native. Anything else is refused (E-TYPE-LAYOUT).

3 align <n> . nails down the alignment of the place where that struct begins. n shall be a power of 2. The alignment shall be a power of 2 (E-TYPE-ALIGN) — no machine can keep any other number.

4 A marker can be attached after a field. The markers are these five and no more; writing any other word is refused at translation (E-FIELD-MARK).

4a If no byte order is written, the machine’s order is followed (§5.6).

4b The way of reaching is enforced only in structs that mirror device registers (§7.6). A violation is refused at translation, not at execution (E-MMIO-PERM).

module ex_layout .

struct wire_header do
  layout packed .
  magic u32 big .
  length u16 big .
  kind u8 .
end .

fn hdr_kind input b slice u8 . output u64 . do
  let v view wire_header view wire_header b. . .
  return widen u64 field v. kind . . .
end .

6.2.16 Explicit conversion — cast§

1 Reading a value as another type happens only where the source says so. The only conversion the processor does by itself is widening (§6.2.5 (2)); every other conversion is written by the author with a word. The centre of those words is cast <type> <value> — cast is the word that takes charge of explicit conversion in this language. widen is used only where the value does not change, and conversions that may change the value are written with cast — places that change the sign, cross kinds, or narrow.

1a There are three words that write conversions, each with its own place.

1a-1 A narrow that crosses kinds (integer ↔ floating point) is refused at translation (E-TYPE-KIND), and so is one whose target is wider than the value (E-TYPE-WIDTH — the word for that is widen).

1a-2 narrow f32 rounds an f64 value to f32 once (the same rounding as (3-1)). If a finite value rounds beyond the largest finite f32 — the value does not fit f32 — execution stops. Infinities and NaN pass as they are. To take an overflowing value as the infinity of the same sign, use cast f32.

1b A conversion that could be read either way does not happen by itself; it goes through cast. That is a conversion where the same bits could be read as two numbers, or that widens or narrows depending on the target machine, or that changes the kind of the value. This rule also applies to types and conversions that enter the language in the future — if a new conversion is ambiguous its spelling is cast, and nothing is decided in the direction of adding implicit conversions.

2 cast traps if the value does not fit the target type. It is not truncated silently. That is, cast is not a mark that says «anything may happen» but a mark that says “I know this is a place where the value may change”.

3 Converting a floating-point number to an integer truncates towards 0 — 7.9 becomes 7 and -2.9 becomes -2. Only the fractional part is discarded; if the integer part does not fit the target type, it traps as in (2).

3-1 A cast to a floating-point type — whether from an integer or from another floating-point type — gives the nearest value in the target type, and when two are equally near, the one whose last digit is even. Rounding happens once — converting an integer to f32 does not go through f64 and round twice. A value that rounds beyond the largest finite value of the target type becomes the infinity of the same sign, and NaN is NaN. This conversion does not trap as in (2) — a floating-point type has an infinity for an overflowing value to go to. From f32 to f64 the value is unchanged. cast f32 <f64 1e300> is +∞, and cast f32 <u64 16777217> is 16777216.

3a Between usize · idiff and other integer types the only crossing is cast (§6.2 (3-3)). This conversion is both a widening and a narrowing depending on the implementation’s width, so cast is its spelling — if the value fits it is given as it is; if not, it traps as in (2). On an implementation where the width is the same or grows, this cast leaves no check.

4 From a truth value to an integer goes by cast — cast <integer type> <truth value> is 1 for true and 0 for false. That value fits every integer type, so the trap of (2) does not happen. A floating-point type is not a target of this conversion (E-TYPE-KIND).

4a There is no cast from an integer to a truth value — bool cannot be the target of cast (E-TYPE-KIND). Write what is being asked: ne n. 0 . or eq n. 0 .. Which values of the number are true is decided by that question.

4b Truth values are not in the table of widen (§6.2.5 (4)) — widen <integer type> <truth value> is refused (E-WIDEN-KIND). The spelling that turns a truth value into a number is cast alone.

module ex_bool_cast .

fn big input a u64 . output u8 . do
  return cast u8 gt a. 2 . . .
end .

fn count_big input a u64 . input b u64 . output u64 . do
  return add cast u64 gt a. 2 . . cast u64 gt b. 2 . . . .
end .

big(5) = 1 · big(1) = 0 · count_big(5, 7) = 2

module ex_cast_to_bool .
fn nonzero input n u64 . output bool . do
  return cast bool n. . .     rem write what is being asked — `ne n. 0 .`
end .

5 An enum value is not a number. Putting an enum value in a place that takes a number — a name · field · argument · return declared as a number, arithmetic, comparison with numbers, indices, bit operations, widening · narrowing — is refused at translation (E-TYPE-KIND · E-TYPE-LET · E-TYPE-RETURN · E-TYPE-ARG · E-WIDEN-KIND), and putting a number in a place that takes an enum is refused too, literals included. If the variant’s number (§6.2.7 (2c)) is needed, write cast <integer type> <enum value> — if the number does not fit that type, it traps as in (2). Two values of the same enum can be compared with eq · ne, and with lt · le · gt · ge — the magnitude is the order of the numbers, and the numbers increase in declaration order, so it is the same as the order of declaration. Values of different enums are not compared (E-TYPE-KIND).

5a From a number to an enum goes by cast <enum> <integer> — it gives the variant with that number. If the number belongs to no variant, it traps (E-VM-CAST). This is the place where a number read from a file or a wire is turned back into an enum. The source shall be an integer (E-TYPE-KIND).

5b An enum with even one variant that carries values (§6.2.19) can be neither the source nor the target of cast (E-TYPE-KIND). One number cannot say everything about such a value — which variant it is is asked with isa · match, and the value is built with <enum>.<variant> ….

module ex_enum_cast .

enum color do
  red .
  green .
  blue .
end .

fn code input c color . output u8 . do
  return cast u8 c. . .
end .

fn code_of_blue output u8 . do
  return code blue. . .
end .

fn same output u8 . do
  return cast u8 eq green. green. . . .
end .

code_of_blue() = 3 · same() = 1

module ex_enum_as_number .

enum color do
  red .
  green .
end .

fn code input c color . output u8 . do
  return c. .     rem a variant's number is read with `cast u8 c. .`
end .

module ex_enum_from_number .

enum item do
  weapon_start 10 .
  sword .
  stick .
  weapon_end .
  tool_start 20 .
  hammer .
  tool_end .
end .

rem 1 = weapon · 2 = tool — values of the same enum are compared by magnitude
fn kind_of input n u8 . output u8 . do
  let it item cast item n. . .
  if and gt it. weapon_start. . lt it. weapon_end. . . do return 1 . end .
  if and gt it. tool_start. . lt it. tool_end. . . do return 2 . end .
  return 0 .
end .

enum hangul do
  ga 11 .
  na .
  da 101 .
  ra .
end .

fn round_trip input n u32 . output u32 . do
  return cast u32 cast hangul n. . . .
end .

kind_of(12) = 1 · kind_of(21) = 2 · round_trip(102) = 102

module ex_enum_cross_order .

enum color do
  red .
  green .
end .

enum size do
  small .
  large .
end .

fn f input c color . input s size . output bool . do
  return lt c. s. . .
end .

module ex_enum_arith .

enum level do
  low .
  high .
end .

fn next input l level . output u8 . do
  return add l. 1 . .
end .

6.2.17 What holds characters — a string is not a type§

1 This language has no string type. What holds characters is a piece of bytes (slice u8), and that is all.

2 So the length is the truth. A mark that signals the end of a string (a null byte) is not part of the value, and scanning the bytes to count the length does not happen.

3 The null-terminated shape is needed only where C is met (§6.9.2). It is a shape built at the boundary, not a type this language has.

4 Handling characters — cutting · searching · joining · Unicode checks — is the work of libraries (§9.5). The processor knows only pieces and bytes.

6.2.18 Type names without meaning§

1 Some names are accepted but have no meaning. If such a name is written in a signature, the processor warns (W-NOT-YET). Those names are gathered in annex A.9 (2) — names such as byte · char · str · string · bytes_view · dyn · atomic.

2 Having no meaning means that the processor does not know the shape of the values that name holds. Neither the size, the layout, nor what can be done with the value is fixed, so checks that rely on that name do not stand.

3 There are two ways to give a name meaning: write the underlying type directly, or declare that name (type str option u64 .). Once declared, it has a meaning, so there is no warning.

module ex_name_only .

rem `str` is not built in — without a meaning it gets W-NOT-YET. Here it is given a meaning by declaring it.
type str option u64 .

fn f input s str . output u8 . do return 1 . end .

f() = 1

6.2.19 Variants that carry values — building and taking apart§

1 The variants of an enum can carry values. When writing a variant, the names and types of what it carries are written with it.

2 The shape that builds such a value is <enum>.<variant>, and it gives all of what the variant was declared to carry. If something is missing it is refused (E-ENUM-ARITY) — a half-built value is not made silently.

3 There are two ways to handle an enum that carries values.

4 Naming a variant that does not exist is refused (E-ENUM-NOVARIANT), and trying to read a name that variant does not carry is refused (E-ENUM-NOFIELD). Both are decided at translation — the variant and the name are written in the source, so there is no reason to wait for execution.

5 In an enum with several variants, payload can be used only after it has been narrowed to that variant (E-ENUM-UNCHECKED). What narrows is isa, usually written as guard isa <value> <variant> else ….

5a Using payload at a place already narrowed to another variant is refused too (E-ENUM-VARIANT) — at that place it has already been proven to be another variant, so that payload reads the wrong thing.

5b The type of what a variant carries is written as one word (E-ENUM-PAYLOAD). A variant line has no mark that separates fields, so for types written as several words (slice u8 · option t · owned t · ref t) where they break would not be fixed. This is a restriction of spelling, not of size — the size of the carried value is not asked about. A multi-word type is written by naming a struct that has it as a field and using that name.

module ex_enum_named_payload .

struct bytes do
  b slice u8 .
end .

struct pt do
  x u64 .
  y u64 .
  z u64 .
end .

enum msg do
  data d bytes .
  dot p pt .
  blank .
end .

fn size_of_data input m msg . output usize . do
  guard isa m. data . else return 0 . .
  let d bytes payload m. data d . .
  return len field d. b . . .
end .

export fn f input s slice u8 . output usize . do
  let m msg msg.data lit bytes do b s. . end . . .
  return size_of_data m. . .
end .

export fn g output u64 . do
  let m msg msg.dot lit pt do x 1 . y 2 . z 7 . end . . .
  guard isa m. dot . else return 0 . .
  let p pt payload m. dot p . .
  return add add field p. x . field p. y . . field p. z . . .
end .

f([1,2,3]) = 3 · g() = 10

6 If an enum carries itself as a value, its size is not fixed, so it is refused (E-ENUM-INFINITE). A recursive structure is built by putting something in between.

6.2.20 Seeing scattered pieces as one — segments§

1 Several pieces that are not contiguous can be seen with one eye. It consists of two things: the bytes lying behind, and a descriptor that says where in them and how much.

1a An eye is an aggregate holding the fields back (the bytes behind) and descs (the descriptor). The number of pieces and the piece of a number are written by reading and cutting those fields, so they are not operations of the language but ops of the standard module segview (§9.3).

2 A descriptor is a piece holding pairs of «from where» and «how much». So these three add neither a new type nor a new machine instruction — they lower to building an aggregate, reading fields and cutting.

6.2.21 Fetching ahead — prefetch§

1 prefetch <piece> <number> tells the machine that the bytes at that place will be used soon.

2 This is only a hint. It leaves no value and does not change the meaning of the program, and if the machine ignores it, the answer is the same.

6.2.22 What it means for types to match§

1 In every place where a value is put, the type of the value shall be the same as the type that place states.

2 Aggregates and enums are declared with struct <name> do … end . · enum <name> do … end .. Trying to declare them in another shape is refused (E-TYPE-DECL).

3 Even with the same field layout, different names are different aggregates (E-TYPE-STRUCT, §8.9).

6.2.23 The shape of writing fields§

1 A field of an aggregate is a name followed by a type (x u64 .). Anything not in that shape is refused (E-FIELD-FORM).

2 A field is read with field <value> <name> …. The old spelling that reads with an attached dot does not exist in this language (E-FIELD-GLUED).

3 A vec and a mask are values themselves, and pointing or borrowing markers cannot be attached to them (E-VEC-QUAL). Their lanes are positions inside a word, not positions in memory.

module ex_field_form .

struct p do
  x .              rem there is no type
end .

fn f output u8 . do return 1 . end .

6.2.24 Integers of arbitrary width — bits§

1 type <name> bits <number> . makes an integer type with that many bits. The width is from 1 to 64.

2 The width need not be a power of 2 — bits 3 and bits 10 both stand.

6.2.25 Decided but not built: type words — c8…c64 · b8…b128 · list · an overlapping sum · a child region§

1 The words of this clause are, like the four of §6.9.4, decided in meaning but not yet built by the implementation. The three whose spelling is fixed ((2) to (4) below) are refused at translation when written in a type position (E-TYPE-UNBUILT) — they are not taken as a name without meaning or turned into another type. None of them is a reserved word: if the author declares a type of that name (type c8 u8 .), that declaration stands, and so do a local or an op of the same name.

2 c8 · c16 · c32 · c64 are code units of text — one unit of some encoding, made of that many bits. They are not numbers, so they are not computed with. They go to and from integers only through cast (§6.2.16).

3 b8 · b16 · b32 · b64 · b128 are opaque blocks of bytes — that many bytes, aligned to their size. They have no arithmetic and no comparison; they are only moved and copied. To read one as a number or a structure, go through a view (§6.2.13).

4 list is a list whose elements may differ in type. Each element carries a mark of its type and the place of its value, and the list is reached only through a handle (it is not a fixed type laid out as a value). An op that uses its elements chooses the branch by the mark.

5 An overlapping sum — a type that places one of its variants in the same place; its size is that of the largest variant. The spelling is decided when it is built: the original union collides with the rule that the language leaves short words to the author (§6.3.3 (1e) — set union too is bitset_union). So this one is not refused as a word.

6 A child region — a region carved out of another, which ends when its parent ends (not when a lexical block ends). Carving does not obtain new memory, so it is not the alloc effect (§8.13). The original spelling (child_of) has no place in the present grammar, so the spelling is decided when it is built.

7 Deferral. These words are built when a use appears. If other ways fill that use and they are shown unnecessary, they are dropped. What carries that use today: code units — integers (u8 · u16 · u32) and the utf8 · utf16 library; byte blocks — slice u8 · array N u8 and views; list — an enum whose variants carry values (§6.2.7); the overlapping sum — an enum whose variants carry values; the child region — allocators (§8.13). Whether to build or drop them is the owner’s decision. Until then this clause stays and the implementation keeps recognizing the words of (2) to (4).

module ex_unbuilt_type .

fn f input x c8 . output u64 . do
  return 0 .
end .

6.3.1 Prefix notation is the default§

1 Expressions are written in prefix notation — the name of the operation comes first and the arguments follow.

2 Prefix notation has no precedence rules. What is computed first is said entirely by the dots and the order — a form is opened by a name and closed by its own dot (§6.1.5), and the inner form closes first.

2a Nesting calls needs no parentheses — in add 1 mul a. b. . . the first dot closes mul and the second closes add. The end of a form is decided by that form’s dot. The number of arguments an operation takes does not decide the end — whether the number of arguments is right is looked at separately after the form has closed (E-IR-ARITY if not).

2b Parentheses are decoration that makes a grouping stand out — add 1 (mul a. b. .) . is the same expression as that of (2a). A form inside parentheses closes with its own dot too, and the parentheses do not change the meaning.

2c The order in which operands are computed is a free choice (§4.3). The processor may compute the operands of an operation in any order. Core ops · builtin ops and ops the author declares are the same. But the following are fixed.

• The operation is done after all its operands have been computed.
• Each operand is computed only once.
• Operands that produce effects are computed in the order written, from the left. Here an effect means an effect other than panic (§7) —

being able to stop does not by itself bind the order.

• and and or are the exception — they compute the first operand first, and if that alone decides the result, they do not compute

the second operand (§6.3.3 (4)).

let a u32 add 1 2 . .
let b u32 add 1 mul 2 3 . . .
let c bool lt a. b. . .

6.3.2 Infix notation — the expr island§

1 Long arithmetic is hard to read, so at a place that begins with expr infix notation can be used. This place is called an island.

2 The notation inside an island turns into exactly the same meaning as prefix. An island is only a projection of notation and has no execution cost.

3 Precedence exists only inside islands. The following table is all of it.

4 and binds more strongly than or. That is, expr a or b and c is the same as or a. and b. c. . ..

5 Comparisons cannot be chained. expr a lt b lt c is refused.

6 The table above is all of the island. This set is closed and does not grow. Operations not in the table — including bit operations (§6.3.5) · the remainder mod · the minimum min and maximum max — are written in prefix even inside an island.

7 There are no unary operations in an island either. To flip a sign, write expr 0 - a, or wrap a prefix form in parentheses (expr (not b. .) or c. .).

module ex_infix .

export fn score input a u32 . input b u32 . output u32 .
  requires le a. 1000 . .
  requires le b. 1000 . .
do
  return expr a. + b. * 2 . .
end .

module ex_chain .

proc p input a u32 . input b u32 . input c u32 . output bool . effects none .
do
  return expr a. lt b. lt c. . .     rem two comparisons cannot be chained
end .

6.3.3 Core ops and builtin ops§

1 The operations whose meaning the language fixes are of two kinds. A core op is called anywhere by its name alone and shares one namespace with the names the author makes. A builtin op is called only after call_builtin and has its own namespace ((1c) · (1f)). For both kinds the list of names is fixed, and the whole of it is in annex D. Annex D also states, for each operation, what it takes and what it gives, when translation is refused and when execution stops.

1a Not all the names of core ops have the same rule. Most cannot be used as local names (§6.1.3), but some are operations only within a context, and outside it they can be the author’s names. Which is which is stated by annex D.

1b What is listed below shows the basic ones by kind; it is not all of them. The full list and the meaning of each operation are in annex D.

1c A builtin op stands only after the head word call_builtin: call_builtin <name> <operand>*. Its names form a closed set, and that is the only place it is called. Which names are such is stated by annex D. Those that reach the outside world — files · the network · processes (file_* · dir_* · path_remove · path_rename · link_type · net_* · proc_*), standard input and output (write_out · read_in), arguments and the environment (arg · env_get), clocks (time_now · time_local · time_sleep), terminals (tty_raw · tty_read · tty_size), random numbers (random_bytes), the reactor (reactor_new · r_read · r_write) — take a capability as their first operand: call_builtin net_send <capability> <handle> <bytes>.

1c-1 Builtin ops that take no capability are computations — floating-point functions (§6.3.9), the sum of a piece (§6.3.7.1), and hashing · cryptography · carry-less multiplication · random sequences (hash_bytes · crc32 · sha256 · sha384 · sha512 · aes_round · aes_round_last · aes_ctr · ghash · aes_gcm · chacha20 · poly1305 · chacha_poly · clmul_lo · clmul_hi · mul_hi · rng_next).

1c-2 The standard library provides ops that wrap these builtin ops (§9.3 (1a)) — stdio · args · env · clock · tty · random · reactor · math and so on. A wrapper passes its operands on as they are, so the meaning is the same.

1f The namespace of builtin ops is separate from the author’s namespace. The word directly after call_builtin is always read as the name of a builtin op, and the same spelling in any other place is always read as the author’s name. So the author can give a spelling the same as a builtin op to their own op · parameter · local, and can use both together in one unit. Since the place where a word stands decides which it is, a spelling never has two meanings in one place.

1d If a word called by its bare name is not among the author’s names and has the spelling of a builtin op, the processor regards it as having left out call_builtin and refuses it (E-BUILTIN-BARE). Putting a word outside that closed set after call_builtin does not conform either (E-BUILTIN-NAME) — that place does not silently pass over to the author’s names.

module ex_bare .

proc p input s slice u8 . input o mut slice u8 . output u64 . effects none .
do
  return sha256 s. o. . .
end .

module ex_call .

proc p input s slice u8 . input o mut slice u8 . output usize . effects none .
do
  return call_builtin sha256 s. o. . .
end .

module ex_both .

fn sha256 input x u64 . output u64 . do
  return add x. 1 . .
end .

proc p input s slice u8 . input o mut slice u8 . output u64 . effects none .
do
  let n usize call_builtin sha256 s. o. . .
  return sha256 cast u64 n. . . .
end .

1e There are three ways of keeping names whose meaning the language fixes out of the global vocabulary.

• Head — the name position of call_builtin <name> ((1c)). Builtin ops are such.
• Prefix — a group of ops shares the same leading part: bitset_* (sets of small numbers, §6.2.12) ·

lane_* and reduce_* (lanes) · atomic_* · wrap_* · sat_* · chk_* · narrow_*. Prefixed names are global names, but since the group does not occupy short words (union · remove · select · any …), the author can use those words as their own names.

• Place — words that have meaning only inside a fixed context. The stages and terminals of pipe are such (§6.12):

the terminals any · all are words inside pipe, and the lane predicates are lane_any · lane_all. An op has one spelling. When a name is moved, the old spelling is not left behind as a synonym.

2 The arithmetic operations are add sub mul div mod. The spelling of the operation that gives a remainder is mod, and rem is the word that opens a comment (§6.1.2) — the same spelling is not used for two meanings.

2a mod is the remainder of integers. The remainder of floating-point numbers is fmod (§6.3.9), and using mod on floating-point operands is refused at translation (E-TYPE-KIND, 2026-11-02 — before that it passed the check and stopped during execution).

3 The comparison operations are eq ne lt le gt ge, and their result is bool.

3a A comparison between integers follows the same rule as arithmetic — the two operands shall be comparable by widening, and if they cannot be, translation is refused (E-TYPE-SIGN, §6.3.4 (1)). The processor does not secretly change signs for a comparison. To compare the mathematical values of two integers even when their signs or widths differ, call cmp_eq · cmp_lt · cmp_le of the standard library intops by name (§9) — intops.cmp_lt i64. u64. a. b. . is true when a is −1 and b is 0. Those ops take any pair of integer types (usize · idiff · 128 bits included).

4 The logical operations are and or not, and their operands and results are all bool. and and or short-circuit — if the first part alone decides the result, the second is not computed.

5 The slice operations are len idx (§6.2.6).

6 The conversion operations are widen narrow (§6.2.5).

7 The bit operations are in §6.3.5.

8 neg flips the sign. The operand shall be a signed integer or a floating-point number — an unsigned integer has no negative numbers, so it is refused at translation (E-TYPE-SIGN). The type of the result is the type of the operand.

8a neg is arithmetic too. If the result does not fit its width, it stops (§6.3.4 (3)) — the smallest value of a signed type is that case (−128 of i8).

6.3.4 The rules of arithmetic§

1 The two operands of binary arithmetic shall be comparable by widening (§6.2.5). If they are not comparable, translation is refused. If only their widths differ, they are computed at the wider one.

1a Even with mixed signs, it can be computed if there is a widening that keeps the value. It is enough that the unsigned side fits in the result type without losing its value — u8 and i16 can be mixed.

1b If there is no such widening, translation is refused. u32 and i32 have the same width, so the unsigned side cannot fit in the signed side, and they cannot be mixed.

2 The type of the result is the wider of the two operands. The processor does not invent a third type that is neither of the two operands.

3 Arithmetic happens at the declared width. If the result does not fit that width, it traps.

4 Dividing an integer by 0 traps. Dividing a floating-point number by 0 gives infinity, as IEEE 754 specifies.

5 div and mod are interpreted with the declared sign.

5a div truncates the quotient towards 0 — div -7 2 . is −3.

5b mod is the remainder of floored division. The sign of the remainder follows the divisor — mod -7 2 . is 1, mod 7 -2 . is −1. So when the divisor is positive the result is always 0 or more and less than the divisor: if 0 < n then 0 ≤ mod i n < n, even when i is negative.

5c So div and mod are not a pair. (div a b) × b + (mod a b) equals a only when the two numbers have the same sign or divide evenly. The remainder that pairs with the quotient truncated towards 0 is written sub a. mul div a. b. . b. . ..

5d mod of the smallest value of a signed type by −1 is 0. div stops at the same place (the quotient is not in that width), but the remainder 0 is within that width.

5e The quotient and remainder that pair up are in the standard library intops (§9) — div_floor is the floor quotient that pairs with mod ((div_floor a b) × b + (mod a b) is always a), and mod_trunc is the truncated remainder that pairs with div (its sign follows the dividend — mod_trunc -7 2 is −1). Both take the type as an argument (intops.div_floor i64. a. b. .), stop when dividing by 0, and div_floor of the smallest value of a signed type by −1 stops as div does. All are written in Lowent (§9.3 (5)).

module ex_mixsign .

rem `u8` fits in `i16` without losing its value.
fn ok_widen input a u8 . input b i16 . output i16 . do return add a. b. . . end .

rem A wider place may be chosen for the result.
fn ok_wider input a u8 . input b i16 . output i32 . do return add a. b. . . end .

ok_widen(200, -100) = 100 · ok_wider(200, -100) = 100

module ex_sign .

proc p input a i32 . input b u32 . output i32 . effects none .
do
  return add a. b. . .     rem `u32` does not fit in `i32` — the widths are the same
end .

6.3.5 Bitwise operations§

1 Bit operations treat a value as a sequence of bits. Operands and results are integers, and signed integers can be handled too.

1′ If the two operands of bit_and · bit_or · bit_xor are of the same type, the result is of that type too; if one side is a literal, it is of the other side’s type. The result of bit_not and of shifts · rotations (shl · shr · rotl · rotr) is of the type of the (left) operand. Putting usize · idiff and a fixed-width integer in one operation is refused at translation (E-TYPE-NOMINAL, §6.2 (3-2)) — the shift count is not covered by this rule.

1″ If the two operands of bit_and · bit_or · bit_xor are integers that differ only in width or sign, they follow the same rule as arithmetic (§6.3.4 (1)–(2)): if they are comparable by widening, the result is of the wider type; if not, translation is refused (E-TYPE-SIGN). The result of count_ones · leading_zeros · trailing_zeros is of the type of a.

1a The right shift shr means different things depending on the sign. For unsigned integers 0 comes into the vacated places (logical shift); for signed integers the sign bit comes in (arithmetic shift). So a negative number stays negative when shifted right.

2 The bitwise logical operations are bit_and bit_or bit_xor bit_not. The first three take two values and bit_not takes one.

3 The shifts are shl (left) and shr (right). The rotations are rotl and rotr, in which the bits pushed out come back in on the opposite side.

3a The count of a rotation may be of any integer type, and it rotates by the remainder after dividing by the width — rotating a type of width 8 by 9 is the same as rotating it by 1. Rotations do not stop.

4 The shift count shall be less than the width of the type. Otherwise it traps.

4a The count of shl · shr · wrap_shl · wrap_shr is an unsigned integer type (any width). Putting a value of a signed integer type as the count is refused at translation (E-SHIFT-SIGNED) — a negative count has no single fixed meaning. To use a signed value as the count, convert it explicitly to an unsigned type. A literal takes the type of its place, so it is used as it is (negative literals: (9)).

5 wrap_shl and wrap_shr wrap the shift count into the width before using it. On a type of width 8, 9 places are read as 1 place.

module ex_shift_signed .

fn up input a u8 . input n i8 . output u8 . do return shl a. n. . . end .

6 The counting operations are count_ones (the number of 1 bits), leading_zeros (the number of consecutive 0s from the front) and trailing_zeros (the number of consecutive 0s from the back).

7 byte_swap reverses the order of the bytes. It is used when exchanging values with a place of different endianness.

module ex_bitlogic .

rem 12 = 0000_1100 · 10 = 0000_1010
fn mask input a u8 . input b u8 . output u8 . do return bit_and a. b. . . end .
fn both input a u8 . input b u8 . output u8 . do return bit_or  a. b. . . end .
fn diff input a u8 . input b u8 . output u8 . do return bit_xor a. b. . . end .
fn flip input a u8 . output u8 . do return bit_not a. . . end .

mask(12,10) = 8 · both(12,10) = 14 · diff(12,10) = 6 · flip(12) = 243

module ex_bitshift .

fn up   input a u8 . input n u8 . output u8 . do return shl  a. n. . . end .
fn down input a u8 . input n u8 . output u8 . do return shr  a. n. . . end .
fn spin input a u8 . input n u8 . output u8 . do return rotl a. n. . . end .
fn back input a u8 . input n u8 . output u8 . do return rotr a. n. . . end .

up(3,2) = 12 · down(12,2) = 3 · spin(129,1) = 3 · back(3,1) = 129

module ex_signed_shift .

rem Signed integer — the sign bit comes into the vacated places (arithmetic shift). The count is an unsigned type ((4a)).
fn s_shr input a i32 . input n u32 . output i32 . do return shr a. n. . . end .

rem Unsigned integer — 0 comes into the vacated places (logical shift).
fn u_shr input a u32 . input n u32 . output u32 . do return shr a. n. . . end .

rem Bitwise logical operations handle signed integers too.
fn s_and input a i32 . input b i32 . output i32 . do return bit_and a. b. . . end .
fn s_not input a i32 . output i32 . do return bit_not a. . . end .

s_shr(-8, 1) = -4 · u_shr(4294967288, 1) = 2147483644 · s_and(-8, 12) = 8 · s_not(0) = -1

module ex_bitcount .

fn ones input a u8 . output u8 . do return count_ones a. . . end .
fn lead input a u8 . output u8 . do return leading_zeros a. . . end .
fn tail input a u8 . output u8 . do return trailing_zeros a. . . end .
fn endian input a u32 . output u32 . do return byte_swap a. . . end .

ones(7) = 3 · lead(1) = 7 · tail(8) = 3 · endian(1) = 16777216

8 Bit operations take only integers — bits are a property of machine words, so for values without that property they have no meaning. This mismatch is caught at the place of execution (E-BITOP-TYPE).

9 If the shift count is proven not to be less than the width of its type, it is refused (E-SHIFT-RANGE).

6.3.6 Choosing by name what to do on overflow§

1 add · sub · mul stop on overflow (§6.3.4). If another disposition is needed, use the op whose name states that disposition. That is, a disposition is not a setting but a word.

1a Arithmetic that names its overflow disposition (wrap_* · sat_* · chk_*) belongs to integers. Using it on floating-point numbers is refused at translation (E-TYPE-KIND) — floating-point arithmetic has an infinity for the overflowing value to go to.

2 Division by 0 is the same. At a place where the divisor is guaranteed by its type not to be 0, use div_nz, and no check remains at that place. A guaranteed divisor is one of three — an integer literal that is not 0 · the value of (2a) taken out with some_value · a let bound to that. The value nonzero_or of (2c) gives, and a let bound to it, are guaranteed divisors too. Giving div_nz any other divisor is refused at translation (E-TYPE-NONZERO). The division that stops at 0 is div.

2a The way to obtain that guarantee is nonzero_of. nonzero_of <value> reports as a value that the value is not 0 (⟦option⟧) — none if it is 0. Once obtained, it is not asked again at each place that divides.

2b To receive an overflowing carry · borrow as a value instead of discarding it, use the standard library intops (§9) — add_carry_<width> returns the sum and the carry (0 or 1), sub_borrow_<width> the difference and the borrow, and mul_wide_<width> the lower half lo and the upper half hi of the product, as a struct (for signed widths mul_wide_s_<width> — lo is unsigned and hi signed). The widths are unsigned u8 · u16 · u32 · u64 · usize and signed i8 · i16 · i32 · i64 · idiff. All are written in Lowent (§9.3 (5)).

2c nonzero_or <value> <fallback> gives the value when it is not 0, and the fallback when it is 0. The fallback has the value’s type and must be guaranteed not to be 0 (a nonzero integer literal · the value of nonzero_of taken out with some_value · a let bound to that · the result of another nonzero_or) — otherwise translation is refused (E-TYPE-NONZERO). So the result is guaranteed not to be 0 as well: it can be the divisor of div_nz, and so can a let bound to it: div_nz total. nonzero_or count. 1 . .. It takes integers only (E-TYPE-KIND).

3 Reducing a width also chooses its disposition by name.

6.3.7 Ops that handle lanes§

1 A vec (§6.2.11) does arithmetic per lane separately, but crossing lanes is done by separate ops.

1a splat takes the lane count from the declared type. So the only place it can be used is the value position of a binding that writes a vector type: var lim vec 4 u32 splat 5 . .. Writing it directly inside an expression does not conform (E-VEC-SPLAT) — nothing in that place says the lane count.

1b lane_avg belongs to integer lanes (the value above is an integer computation). Using it on floating-point lanes is refused at translation (E-TYPE-KIND, 2026-11-02).

1c The ops that handle lanes take vectors. Giving one a single number is refused at translation (E-TYPE-KIND).

1d The literal of splat <literal> follows §6.1.4 (8)(9), taking one lane as a place of that lane type — filling floating-point lanes with an integer literal is E-TYPE-LET, and filling f32 lanes with a floating-point literal beyond its range is E-TYPE-WIDTH. The elements of list literals (lit vec · lit array · lit slice) are the same.

2 An op that crosses lanes gathers as many as the lane count into one. The type of the result is the type of the lanes. Signed lanes are added and multiplied by sign, and if the value of reduce_add · reduce_mul does not fit that type, it stops (§6.3.4 (3)).

6.3.7.1 Adding up a piece§

1 There are two builtin ops that add up all the floating-point numbers held in a piece (⟦slice⟧), and the name says how it adds. The standard library math wraps them as ops of the same names (math.sum_neumaier · math.sum_seq).

1a sum_neumaier <piece> adds while collecting the lost digits separately and giving them back. So its error is not bound to the number of terms.

1b sum_seq <piece> adds once from front to back. It is fast, and its error is proportional to the number of terms.

module ex_slice_sum .

use math .

fn total input b slice u8 . output u64 .
do
  var xs slice f64 view_array f64 b. . .
  return math.sum_neumaier xs. . .      rem the result is a floating-point number, but the head says `u64`
end .

2 The result of both ops is a floating-point number. Returning it as it is to a place written as an integer is refused (E-TYPE-RETURN).

6.3.8 Asking the size — size_of§

1 size_of <type> gives the number of bytes one value of that type occupies, at translation time. The type of that number is usize — so are the alignment align_of gives and the number of lanes native_lanes gives.

2 It cannot be used on a type whose size cannot be known.

6.3.9 Transcendental functions§

1 The builtin ops sin · cos · exp · log · pow · sqrt · floor · ceil · round · fmod are floating-point only. The standard library math wraps them as ops of the same names (math.sqrt x.). Application programs call those ops.

1a abs takes floating-point numbers and signed integers. The type of the result is the type of the operand. At the smallest value of a signed integer it stops — its absolute value is not in that width (§6.3.4 (3)). Using it on an unsigned integer is refused at translation (E-TYPE-SIGN) — that value is already its own absolute value.

module ex_abs_unsigned .

fn f input a u32 . output u32 . do
  return abs a. . .     rem an unsigned value is already its own absolute value
end .

2 These require no capability and can be used only on machines with an operating system.

6.3.10 A truth value is not a number§

1 and · or · not take only truth values. Passing an integer is refused (E-TYPE-LOGICAL).

2 Places where a condition comes (§6.5) likewise take only truth values (E-TYPE-COND).

3 That is, there is no promise that 0 is false and everything else true. What is being asked shall be written at that place — as in gt a. 0 ..

4 A truth value cannot be an operand of arithmetic (add · sub · mul · div · mod · min · max · abs and arithmetic naming its overflow disposition) · ordering (lt · le · gt · ge) · bit operations (bit_and · bit_or · bit_xor) (E-TYPE-KIND). Two truth values are compared with eq · ne. To count a truth value as a number, write cast u8 b. . (§6.2.16 (4)).

module ex_cond .

fn f input a u8 . output u8 .
do
  if a. do return 1 . end .     rem write what is being asked — `gt a. 0 .`
  return 0 .
end .

6.3.11 Widths and lanes are part of the type§

1 Two vecs with different lane counts are different types and do not mix (E-TYPE-LANES).

2 Only a mask can come in a place that takes a mask (E-TYPE-MASK).

3 Even with the same field layout, different names are different types (E-TYPE-WRAP) — the same layout does not make the same type (§8.9).

4 Putting a value outside a narrowed range (§6.2.14) in that place is refused (E-TYPE-RANGE). So is writing a range that no value can satisfy — that is not a condition but a lie.

module ex_lanes .

fn f input a vec 4 u8 . input b vec 8 u8 . output vec 4 u8 .
do
  return add a. b. . .
end .

6.3.12 The rules inside an expr island§

1 Each piece inside an expr island (§6.3.2) is one form — a. if it is a name, a form closed by its own dot if it is a call (expr twice a. . + 1 .). Since a form has its own end, calls need not be wrapped in parentheses. The island is closed by its own dot.

2 Inside an island there are only infix operators. There is no one-place operator attached in front (E-EXPR-UNARY) — to flip a sign, call the op written as such (neg a. .).

module m .
fn flip input a i32 . output i32 . do
  return expr - a. . .
end .

6.4.1 Declaring an op§

1 An op is a unit of execution with a name and a contract. Ops are divided into two kinds.

2 The kind is always written. There is no default — whether it is fn or proc is written in front of the name.

3 The declaration of an op consists of, in order, the name, inputs, output, effects, contract and body. Inputs are written with input, the output with output. The order is laid out so that what comes first is used by what comes after:

• A named promise (satisfies) comes directly after the name — it says first what this op is.
• Translation-time inputs (comptime) come next — the types of the following inputs and output use those names.
• Capability inputs come before data inputs — who permitted it is seen before what it receives.
• The output comes after the inputs — the output type may use the inputs’ type parameters.
• Effects come after the output and before the contract — they write what is done with the capabilities received earlier.
• The contract is in the order input conditions (requires) · output promises (ensures) · failures (errors) · tests (tests).

3a The clauses of the head are written in one order only. From front to back: satisfies · lowdoc · vector · priority · comptime inputs · capability and region inputs (whose type is cap … · region …) · use · data inputs · output · effects · link · variadic · asm · absorbs · reference · why · access · inplace · invalidates · parallel · reduce · requires · ensures · errors · tests · schedule. Clauses in the same position keep the order in which they are written. The method signatures of a trait (§6.11.2) and procs inside an actor follow the same order. Violating this order is refused at translation (E-CLAUSE-ORDER). The order of inputs is also the order of the caller’s arguments — so capabilities are always passed before data.

3b The formatter (--fmt) moves clauses that are not inputs, and use clauses, into this order. It does not move inputs among themselves — moving inputs would change the meaning of calls.

3c Each clause of the head is closed by its own dot — the same as statements (§6.1.6 (2)). A clause word does not close the previous clause, and neither does a newline. Meeting the next clause word or do without a dot is refused at translation (E-DOT-MISSING). The list of clauses is the head, so clauses begin with the first word after the name — even if the name has the same spelling as a clause word (proc link …), it is read as the name.

3d The meanings of the clause words that appear in the order of (3a), and where they are defined, are as follows.

• satisfies — a named promise this op keeps (§6.4.5 · §6.11.2). lowdoc — a description for people to read (§6.4.3).
• vector · priority — make this op an interrupt handler: the number of the interrupt it receives and its urgency (§7.7).
• comptime inputs — parameters fixed at translation time (§6.8). Capability inputs — the right to produce effects (§7.2).
• use — the allocator this op uses (§8.14).
• link · variadic — the name on the C side · arguments whose number is not fixed (§7.4).
• asm — the place that writes machine instructions directly (§6.9.1).
• absorbs · reference · why — the declaration that the spread of unsafe stops here, and the pure version and assumptions that ground it (§7.2.1).
• access · inplace · invalidates — what it touches and in which mode · writing in place · what it invalidates (§6.4.3 · §8.12).
• parallel · reduce — a loop that runs divided, and the place where the steps gather (§6.5.10).
• requires · ensures · errors · tests — the clauses of the contract (§6.4.3).
• schedule — comes only in the head of a test (test). schedule explore_interleavings . runs every order in which messages are delivered

and checks that the result is the same for each order. With limit <number> it runs only up to that number. If the result differs by order, the test fails (E-SCHED-NONDET). The meaning is specified by §6.4.13 (4).

3e The output can be named — output <name> <type> .. That name is a local of the body and starts at 0: 0 · 0.0 for numbers, false for bool, none for option, and for a struct the 0 of each field. The body writes to that name and returns it with return <name> . (as with other ops that return a value, every path shall end with return — §6.5.5 (3)).

• Distinguishing: there is one namespace (§6.10), so if the first word after output is a type name, the whole output is a type;

if it is not a type name and what follows is one type, that word is the name of the result.

• A type without a fixed zero (slices · result · owned · enums · newtypes · generic parameters, and structs with such fields)

cannot be named (E-RESULT-NOZERO). Such an output is written without a name and returns a value.

• An op without a body (extern · the method signatures of a trait) cannot name its result (E-RESULT-NAMED).
• An output that returns an array (output [<name>] array <length> <type> .) has its place provided by the caller — §6.2.6 (1c).
• ensures still refers to the result as ret (§6.4.12). The name of the result is visible only inside the body.

module ex_named_result .

struct span do
  lo u64 .
  hi u64 .
  seen bool .
end .

export fn bounds input xs slice u64 . output s span .
do
  for x xs. do
    if or not field s. seen . . lt x. field s. lo . . . do set field s. lo . x. . end .
    if gt x. field s. hi . . do set field s. hi . x. . end .
    set field s. seen . true .
  end .
  return s. .
end .

module ex_named_nozero .

fn first input xs slice u8 . output r slice u8 .
do
  return xs. .
end .

module ex_op .

export fn twice input n u32 . output u32 .
  requires le n. 2147483647 . .
do
  return mul n. 2 . .
end .

module ex_clause_order .

fn twice output u32 .
  input n u32 .
  requires le n. 2147483647 . .
do
  return mul n. 2 . .
end .

module ex_clause_dot .

fn twice input n u32 output u32 .
do
  return mul n. 2 . .
end .

6.4.2 What a contract is§

1 A contract is the promise an op writes for itself about its input and output. A contract is not a comment but a statement that is checked.

2 Contracts are used in three places.

3 a) The processor uses them as facts — on the premise that the contract is true, it removes checks (§6.4.5).

4 b) They are enforced during execution — a contract the processor could not prove is confirmed during execution, and if broken it traps. But whether the remaining checks are actually kept is decided by the build mode (§6.4.8).

5 c) They speak to readers — what must be kept to call this op is visible without opening the body.

6 There are two places where a contract breaks, and the diagnostic separates whose fault it is.

6.4.3 The six clauses of a contract§

1 A contract consists of the following six clauses. Not every clause is required.

1a The clause tests <name>… writes one or more names of ops that test this op. The names written shall be ops visible at that place; if not, it is refused (E-CONTRACT-UNDEF). The name of a test block (§6.4.13) is not an op, so it cannot be written here. The tests clause neither defines nor runs tests — it only points at what already exists. If an op pointed at disappears, the head reports it.

1b The lowdoc clause writes the description of this op. One line is lowdoc "<text>" .; several lines are opened with lowdoc text <end mark>, and the text runs up to the line on which that mark stands alone. This text is read by the document output (--doc) and does not affect the meaning of the translated program.

1c The condition of the errors clause is read with the values on entry to the op.

1c1 If the body never raises that error, the processor reports it (W-ERRORS-UNRAISED). The clause is read as the promise «this op can fail this way», and the caller builds branches by looking at it; a branch that cannot be taken becomes dead code that the reader cannot tell apart from live branches. An op that passes on someone else’s result as it is is regarded as raising that error (try · return <call>).

1d So the only names that can stand in that condition are those that are the same on entry and on exit — namely inputs that do not change and module constants. Writing in the condition a name the body can change (an actor’s state field · a module var · an argument in a mut position) is refused (E-ERRORS-STATE).

2 The conditions used in a contract shall be pure expressions — something that produces effects cannot be written in a contract.

3 shared_read and write_only are disciplines of reading and writing, so the processor enforces them now. That is, writing to a place declared shared_read is refused, and reading a place declared write_only is refused (E-ACCESS-MODE). The other five are hints about usage, and the processor says that it does not use them yet (W-NOT-YET). It does not silently ignore them.

4 Not being enforced does not mean they may be written carelessly. A mode is a claim about what this op does, and the processor may someday question that claim.

6.4.4 How to write contracts§

1 Conditions are written in prefix notation. Comparison and logical operations, arithmetic, len and idx can be used.

2 If there are several requires, all shall be true.

3 A condition about every element of a slice is written with the following four. elem_lt <slice> <value> means “every element is less than that value”, and elem_le · elem_gt · elem_ge likewise.

4 These four exist because a contract cannot write going through one by one. A condition is a pure expression and a loop is a statement, so to speak about all the elements there has to be a word that says it.

module ex_contract .

rem This op reads two bytes from a slice and makes one larger number.
export fn read_pair input data slice u8 . output u32 .
  requires ge len data. . 2 . .
  ensures le ret. 65535 . .
do
  let hi u32 widen u32 idx data. 0 . . .
  let lo u32 widen u32 idx data. 1 . . .
  return add mul hi. 256 . lo. . .
end .

6.4.5 Giving a contract a name§

1 If several ops require the same condition, that condition can be given a name. It is written with contract.

2 An op writes that name with satisfies and so takes on that contract.

module ex_named .

rem If several ops require the same condition, that condition can be given a name.
contract nonneg do
  requires ge a. 1 . .
end .

fn half satisfies nonneg . input a u8 . output u8 .
do
  return div a. 2 . .
end .

6.4.6 Contracts remove checks§

1 The processor takes contracts as facts and narrows the range a value can have. If that range shows safety, it removes that check.

2 The checks that can be removed are these — overflow, division by 0, narrowing, slice bounds.

3 If a contract is not enforced, it is not used as a fact. That is, nothing is believed without confirmation. Believing without confirmation and removing checks is not being faster but being wrong.

4 The processor can report where checks it could not remove remain. A performance model that does not report is itself knowledge outside the source (§1.3).

module ex_elim .

rem Without a contract, the overflow check remains.
export fn bare input a u8 . output u8 .
do
  return add a. 1 . .
end .

rem With a contract, the processor proves it and removes the check.
export fn proven input a u8 . output u8 .
  requires le a. 200 . .
do
  return add a. 1 . .
end .

 proven 250  ──▶ requires le a 200   entry check fails → E-VM-CONTRACT (caller's fault)
 proven 150  ──▶ requires le a 200   passes → from here on a ∈ [0, 200] is a fact
                 add a 1             a + 1 ∈ [1, 201] ⊂ u8 [0, 255] → overflow check removed
 bare 255    ──▶ add a 1             no fact about a → the check stays → E-VM-OVERFLOW

6.4.7 The build mode decides the remaining checks§

1 The build mode is written in the source as build <mode> .. A proved contract leaves no check in any mode. What the mode decides is the disposition of contracts that could not be proved.

1a The modes are a closed four — debug · test · release_safe · release_fast. Any other word is refused (E-BUILD-MODE).

2 debug keeps the remaining checks and, if one breaks, stops saying what broke — the kind of check that broke (a requires, ensures or errors clause), the name of the op that has it, and the source line of that clause. test says the same.

2a test keeps checks like debug. What runs tests (§6.4.13) is not this mode but a request to run tests — that request runs tests in any mode, and even in test mode an ordinary execution does not run tests. If an expect inside a test is false, that test fails (E-TEST-FAIL) — it is not the processor’s error but the claim of the person who wrote it being wrong.

3 release_safe keeps the remaining checks and stops if one breaks. What it reports when it stops is a short fixed message naming the kind of check that broke — the contract’s text (the source expression) is not put in the executable. What differs from debug is that, as in (4), it removes contracts of debug grade.

4 release_fast removes the checks of requires that could not be proved — both those written on the op and those of named contracts taken in with satisfies. release_safe removes the requires checks of debug grade. No mode removes the exit checks of ensures.

4a A contract whose checks the mode removed is not a fact. The processor does not remove other checks on the ground of that contract — the op runs as if that contract had not been written. So if a call that broke the contract overflows or goes out of range inside that op, the check of that computation stops it. This is for the same reason that assume is not a fact (§6.4.9).

4b The checks the processor puts at each computation — overflow · division by 0 · MIN / -1 · indices · shift counts · narrowing · tags — are not removed in any mode. Those checks disappear only when they are proved.

5 That is, release_fast is the same as opening one more trust boundary (§4.4) — a person promises that the contracts are true. If the promise is wrong, the program runs the same as a program written without the contracts. It does not go into undefined behaviour.

module ex_build_mode .

build nosuchmode .

fn f output u8 . do return 1 . end .

6.4.8 Names and scopes§

1 Names nest in four layers — the module, the op, the block, and blocks inside it.

2 In one scope a name points at exactly one entity. A name already alive cannot be hidden by declaring it again. Doing so is refused at translation.

3 The things that cannot be hidden are these four — names in the module, the names of core ops (§6.1.3), the parameter names of the same op, and local names still alive in an outer block.

4 Declaring the same name twice in the same block does not conform either. The second declaration does not replace the first — the same characters would merely point at two entities.

5 On leaving a block, the names declared in that block disappear. So two side-by-side blocks each declaring the same name conforms — the two names are not alive at the same time.

5a A name written in a value position must refer to something alive at that place — a local · an input · an op · a constant · a variant of an enum. If it refers to nothing, translation is refused (E-IR-UNDEF). The implementation names that name when it says so.

5b A local lives only after it is declared — using it before its declaration is refused as in (5a). A name declared in the module (op · constant · type) lives anywhere in that module regardless of declaration order: an op declared later may be called earlier.

module ex_undeclared .

fn f input a u64 . output u64 . do
  return add a. b. . .
end .

module ex_shadow .

let g u32 7 .

proc p output u32 . effects none .
do
  let g u32 1 .     rem hides the module's `g`
  return g. .
end .

module ex_shadow_param .

proc p input n u32 . output u32 . effects none .
do
  let n u32 1 .     rem hides the parameter `n`
  return n. .
end .

module ex_shadow_twice .

proc p output u32 . effects none .
do
  let a u32 1 .
  let a u32 2 .     rem does not replace the first
  return a. .
end .