9 Sequences — arrays and slices

9.1 Start and length together#

slice t is a contiguous run of values of type t. A slice value carries its start address and its length together, so nobody has to remember separately “how many are here”.

module basics .
rem run: head [9,8,7]
rem run: last4 [1,2,3,4]
rem run: total [10,20,30]
rem trap: at [1,2,3] 5

fn head input data slice u8 .
  output u8 .
  requires ge (len data) 1 .
do
  return index data 0 .
end

fn last4 input xs array 4 u8 . output u8 .
do
  return index xs 3 .
end

fn total input xs slice u8 . output u64 .
do
  var acc u64 be 0 .
  for x xs do
    set acc (add acc (widen u64 x)) .
  end
  return acc .
end

fn at input xs slice u8 . input i u64 . output u8 .
do
  return index xs i .
end

$ lowentc --run head basics.low [9,8,7]
head([9,8,7]) = 9
  arg0 (written) = [9,8,7]
$ lowentc --run last4 basics.low [1,2,3,4]
last4([1,2,3,4]) = 4
  arg0 (written) = [1,2,3,4]
$ lowentc --run total basics.low [10,20,30]
total([10,20,30]) = 60
  arg0 (written) = [10,20,30]
$ lowentc --run at basics.low [1,2,3] 5
== ir diagnostics (1) ==
0:0 E-VM-BOUNDS: slice index out of bounds (panic)

• len data is the number of elements, and index data 0 is the first element. Numbering starts at 0.
• array 4 u8 in last4 is a sequence of exactly 4. An array in an input position means it receives a slice of length 4, and that length is checked on entry, like requires eq (len xs) 4 ..
• for x xs do … end walks the elements in order.
• Passing a slice of length 3 and 5 to at stops with E-VM-BOUNDS. It does not read someone else’s memory.

An array writes its length first. The reverse order is rejected.

module array_order .
rem expect: E-TYPE-ARRAY

fn last input xs array u8 4 . output u8 .
do
  return index xs 3 .
end

$ lowentc --check array_order.low
array_order.low:4:0 E-TYPE-ARRAY: `array` is written `array <count> <type>` — the length first, as a literal (`array 4 u64`). The other order used to be read as a plain slice and the length was dropped silently

According to the diagnostic, the old tool read array u8 4 as a plain slice and silently dropped the length — a place where a written promise vanished. Today array is used only in op input positions; in outputs, locals and struct fields, write slice with a contract.

9.2 Writing needs mut slice#

To write the elements of a slice, the slice must be mut. And changing bytes the caller passed is visible to the caller, so it must be a proc (chapter 5).

module fill .
rem run: fill_two [0,0,5]

proc fill_two input xs mut slice u8 . output u64 . effects state .
  requires ge (len xs) 2 .
do
  set (index xs 0) 10 .
  set (index xs 1) 20 .
  var s u64 be 0 .
  for x xs do
    set s (add s (widen u64 x)) .
  end
  return s .
end

$ lowentc --run fill_two fill.low [0,0,5]
fill_two([10,20,5]) = 35
  arg0 (written) = [10,20,5]

The fill_two([10,20,5]) the VM shows is the argument’s state after the op ended; the caller’s bytes changed. Writing without mut is rejected.

module readonly .
rem expect: E-TYPE-MUT

fn poke input xs slice u8 . output u64 .
do
  set (index xs 0) 1 .
  return 0 .
end

$ lowentc --check readonly.low
readonly.low:6:0 E-TYPE-MUT: writing an element of a slice that is not declared `mut` (a shared slice is read-only)

mut is a permission on the slice’s elements. It is a different question from whether the name holding the slice was made with let (chapter 6). It is followed by the rule that a slice whose elements can be written may be borrowed in only one place at a time (chapter 12).

9.3 Narrowing the window#

subslice s from to makes a new slice pointing from position from of s up to, but not including, to. It copies no bytes; it just places another, narrower window over the same bytes.

module windows .
rem run: middle_sum [1,2,3,4,5]
rem run: prefix_char 4

fn middle_sum input xs slice u8 . output u64 .
  requires ge (len xs) 3 .
do
  let mid slice u8 be subslice xs 1 (sub (len xs) 1) .
  var s u64 be 0 .
  for x mid do
    set s (add s (widen u64 x)) .
  end
  return s .
end

fn prefix_char input k u64 . output u8 .
  requires lt k 11 .
do
  return index "/api/users/" k .
end

$ lowentc --run middle_sum windows.low [1,2,3,4,5]
middle_sum([1,2,3,4,5]) = 9
  arg0 (written) = [1,2,3,4,5]
$ lowentc --run prefix_char windows.low 4
prefix_char(4) = 47

middle_sum sums the middle elements, leaving out both ends. prefix_char indexes a string literal directly, because a literal is a slice u8.

module table .
rem run: prefix_char 4
rem run: prefix_chain 4

rem a string literal is a slice u8 and can be indexed as it is
fn prefix_char input k u64 . output u8 .
  requires lt k 11 .
do
  return index "/api/users/" k .
end

rem the same job as an if chain costs one comparison and one branch per character
fn prefix_chain input k u64 . output u8 . do
  if eq k 0 . do return 47 . end
  if eq k 1 . do return 97 . end
  if eq k 2 . do return 112 . end
  if eq k 3 . do return 105 . end
  if eq k 4 . do return 47 . end
  return 0 .
end

$ lowentc --run prefix_char table.low 4
prefix_char(4) = 47
$ lowentc --run prefix_chain table.low 4
prefix_chain(4) = 47

The two ops give the same answer. Looking with --emit-c, prefix_char is one string table and one index, while prefix_chain is a chain of comparisons and gotos. In this edition, though, the index check in prefix_char remains — the analysis does not connect the literal’s length 11 with the contract lt k 11.

9.4 Contracts remove bounds checks#

An index bounds check remains only where it is not proven. Write the length condition as requires, and the check happens once on entry to the op while the index checks in the body disappear.

module bounds .
rem run: sum_first [3,4,5,6] 3

fn sum_first input a slice u8 . input n u64 . output u64 .
  requires le n (len a) .
do
  var s u64 be 0 .
  var i u64 be 0 .
  while lt i n . do
    set s (add s (widen u64 (index a i))) .
    set i (add i 1) .
  end
  return s .
end

$ lowentc --run sum_first bounds.low [3,4,5,6] 3
sum_first([3,4,5,6], 3) = 12
  arg0 (written) = [3,4,5,6]

With requires le n (len a) ., i inside while lt i n . is always less than len a. The compiler’s interval analysis works that out and removes the check in index a i. The rules behind this reasoning are proven in Coq, and an independent checker re-verifies the arithmetic evidence the compiler leaves at every removed check (chapter 41).

One thing to watch: a count n uses le, but an index itself uses lt. requires le i (len a) . allows i = len a, which is one past the end.

module stale_len .
rem run: fresh [1,2,3,4]
rem trap: stale [1,2,3,4]

rem len stays in the condition --- each round reads the current length
fn fresh input xs slice u8 . output u64 . do
  var s slice u8 be xs .
  var t u64 be 0 .
  var i u64 be 0 .
  while lt i (len s) . do
    set t (wrap_add t (widen u64 (index s i))) .
    set s (subslice s 0 2) .
    set i (add i 1) .
  end
  return t .
end

rem the length was stored ahead --- m stays even when s gets shorter
fn stale input xs slice u8 . output u64 . do
  var s slice u8 be xs .
  let m u64 be len s .
  var t u64 be 0 .
  var i u64 be 0 .
  while lt i m . do
    set t (wrap_add t (widen u64 (index s i))) .
    set s (subslice s 0 2) .
    set i (add i 1) .
  end
  return t .
end

$ lowentc --run fresh stale_len.low [1,2,3,4]
fresh([1,2,3,4]) = 3
  arg0 (written) = [1,2,3,4]
$ lowentc --run stale stale_len.low [1,2,3,4]
== ir diagnostics (1) ==
0:0 E-VM-BOUNDS: slice index out of bounds (panic)

fresh reads the current length each time round, so when s shrinks to two elements the loop stops there too. stale stored the first length 4 in m, so on the third round it tries to read element 2 of the two-element s and stops. len reads the current value every time, and that is what keeps it safe.

9.5 Common mistakes#

Almost every slice mistake comes down to being off by one. Where C would read someone else’s memory and carry on, Lowent stops.

module mistake_offbyone .
rem trap: total [1,2,3]

fn total input xs slice u8 . output u64 .
do
  var t u64 be 0 .
  var i u64 be 0 .
  rem ✘ with `le` it also runs when i is 3 --- a slice of length 3 has indexes 0, 1, 2 only
  while le i (len xs) . do
    set t (add t (widen u64 (index xs i))) .
    set i (add i 1) .
  end
  return t .
end

$ lowentc --run total mistake_offbyone.low [1,2,3]
== ir diagnostics (1) ==
0:0 E-VM-BOUNDS: slice index out of bounds (panic)

module mistake_cindex .
rem expect: E-CHAR

fn first input xs slice u8 . output u8 .
do
  rem ✘ there is no bracket indexing --- read with `index xs 0`
  return xs[0] .
end

$ lowentc --check mistake_cindex.low
7:12 E-CHAR: unexpected character
7:14 E-CHAR: unexpected character
7:12 E-FORM-UNEXPECTED: unexpected token in form

module mistake_empty .
rem trap: first []

fn first input xs slice u8 . output u8 .
do
  rem ✘ an empty slice has no element 0
  return index xs 0 .
end

$ lowentc --run first mistake_empty.low []
== ir diagnostics (1) ==
0:0 E-VM-BOUNDS: slice index out of bounds (panic)

module empty_fixed .
rem run: first_or [] 0
rem run: first_or [7,8] 0

fn first_or input xs slice u8 . input fallback u8 . output u8 .
do
  rem leave here if empty --- below this line, having at least one element is a fact
  guard gt (len xs) 0 . else return fallback .
  return index xs 0 .
end

$ lowentc --run first_or empty_fixed.low [] 0
first_or([], 0) = 0
  arg0 (written) = []
$ lowentc --run first_or empty_fixed.low [7,8] 0
first_or([7,8], 0) = 7
  arg0 (written) = [7,8]

module mistake_subrev .
rem trap: tail_len [1,2,3,4]

fn tail_len input xs slice u8 . output u64 .
do
  rem ✘ the start (3) is after the end (1) --- `subslice s from to` needs from ≤ to ≤ len
  return len (subslice xs 3 1) .
end

$ lowentc --run tail_len mistake_subrev.low [1,2,3,4]
== ir diagnostics (1) ==
0:0 E-VM-BOUNDS: subslice out of bounds (panic)

module subslice_end .
rem run: middle [10,20,30,40,50]

fn middle input xs slice u8 . output u64 .
do
  rem from index 1 up to (not including) 3 --- indexes 1 and 2, two elements
  return len (subslice xs 1 3) .
end

$ lowentc --run middle subslice_end.low [10,20,30,40,50]
middle([10,20,30,40,50]) = 2
  arg0 (written) = [10,20,30,40,50]

module mistake_litwrite .
rem expect: E-TYPE-ARGMUT

rem ✘ taking a string literal as mut slice and changing it; a literal is read-only bytes baked into the program
fn poke output u8 . do
  let buf mut slice u8 . be "abc" .
  set (index buf 0) 65 .
  return index buf 0 .
end

$ lowentc --check mistake_litwrite.low
mistake_litwrite.low:6:0 E-TYPE-ARGMUT: a string LITERAL was bound to a name declared `mut`. A literal is bytes baked into the program, not a place that can be written: the VM used to change them while the native build did not, so the same program gave two answers, and a library op writing there killed the native build. Take bytes you will change from `alloc_bytes` or from the caller's buffer, and copy the literal into them

9.6 This chapter’s syntax at a glance#