12 Borrowing — ref and mut_ref

12.1 Two kinds of borrow#

A reference points to a value that lives elsewhere. There are only two kinds, and the name is the permission.

• ref t — a read borrow. Many can hold one at the same time. It cannot change the value.
• mut_ref t — a write borrow. There can be only one for a value at a time, and no read borrows meanwhile.

Think of a library book. Many people can read it at once, but to write corrections in it you must borrow it alone, and nobody reads it meanwhile — otherwise a reader would see half-made corrections.

module borrow .
rem run: use_sum 7
rem run: use_bump 7

struct big do
  a u64 .
  b u64 .
  c u64 .
  d u64 .
end

fn total input v ref big . output u64 .
  requires le (field v a) 1000 .
  requires le (field v b) 1000 .
  requires le (field v c) 1000 .
  requires le (field v d) 1000 .
do
  return add (add (field v a) (field v b)) (add (field v c) (field v d)) .
end

fn use_sum input x u64 . output u64 .
  requires le x 1000 .
do
  let v big be make big do a x . b 2 . c 3 . d 4 . end .
  return add (total (ref v)) (total (ref v)) .
end

proc bump input p mut_ref u64 . output u64 .
do
  set p (add (deref p) 1) .
  return deref p .
end

proc use_bump input start u64 . output u64 .
  requires lt start 1000 .
do
  var n u64 be start .
  let r u64 be bump (mut_ref n) .
  return add n r .
end

$ lowentc --run use_sum borrow.low 7
use_sum(7) = 32
$ lowentc --run use_bump borrow.low 7
use_bump(7) = 16

• total borrows the four-field big with ref big to read it without copying. field v a reads a field through the reference.
• use_sum borrows the same value twice with ref v. Read borrows may be many.
• bump takes a mut_ref u64 and changes the caller’s value with set p …. The value a reference points to is read with deref p.
• use_bump lends var n as mut_ref n. After bump returns, n is 8.

What matters is that the borrower writes ref x or mut_ref n at the call site. Someone reading the call sees from that place alone that this call can change n.

12.2 Write permission only narrows#

Writing through a read borrow is rejected.

module ref_write .
rem expect: E-TYPE-REF

proc reset input p ref u64 . output u64 .
do
  set p 0 .
  return 0 .
end

$ lowentc --check ref_write.low
ref_write.low:6:0 E-TYPE-REF: write through a shared ref (declare mut_ref)

The other direction is blocked too. Passing a value received only for reading to a position that takes mut, mut_ref or owned is rejected with E-TYPE-ARGMUT. Something writable can be passed on for reading, but something read-only cannot be passed to a writable position. Whoever received a value for reading must be able to trust that it does not change while they look at it, and that trust holds only when nobody gains write permission behind their back.

12.3 Many readers or one writer#

The trouble is overlapping borrows of the same value. Two overlapping write borrows are rejected.

module excl .
rem expect: E-EXCL

proc set_both input a mut_ref u64 . input b mut_ref u64 . output void .
do
  set a 1 .
  set b 2 .
end

proc confused output u64 .
do
  var n u64 be 0 .
  set_both (mut_ref n) (mut_ref n) .
  return n .
end

$ lowentc --check excl.low
13:0 E-EXCL: exclusivity violation: overlapping borrow/owner access (readers-XOR-writer)

The body of set_both believes a and b are different values. Lending the same n twice breaks that belief, and whether 1 or 2 remains depends on the order of writes. Overlapping read and write is rejected too.

module stale .
rem expect: E-EXCL

proc look_then_write output u64 .
do
  var n u64 be 0 .
  let r ref u64 be ref n .
  set n 5 .
  return deref r .
end

$ lowentc --check stale.low
8:0 E-EXCL: exclusivity violation: overlapping borrow/owner access (readers-XOR-writer)

Writing 5 to n while r holds a read borrow of n means whoever reads through r cannot tell when the value they saw changed. These two shapes — another flow changing a value at the same time, and a value changing while being read — are defects hard to find by reading the source, so a rule removes them.

Laying the borrows of one value n out in time makes the rule visible at a glance.

 time →          ①        ②        ③        ④        ⑤
 ref r1 n     ├─────────────────┤                          two reads may overlap
 ref r2 n              ├─────────────────┤
 mut_ref w n                                   ├────────┤  a write only when alone
 ──────────────────────────────────────────────────────────────
 ✘ ref r n    ├──────────────────────────┤
   set n 5                   ●                             the value changes while read  → refused
 ✘ mut_ref a n ├──────────────┤
   mut_ref b n        ├──────────────┤                     two writes overlap            → refused

12.4 A borrow cannot outlive what it borrows#

Returning a reference to a local from its op is rejected.

module escape .
rem expect: E-ESCAPE

fn leak output ref u32 .
do
  let here u32 be 42 .
  return ref here .
end

$ lowentc --check escape.low
7:0 E-ESCAPE: reference to a local escapes the op (dangling)

If this code were translated, the returned reference would point at a value already gone, and nobody knows what reading it would give. Lowent knows this not by running it but at translation time. A borrow cannot leave the block that opened it (E-BORROW-ESCAPE), and a borrow still alive after the lent value has moved is rejected too (E-EXCL-MOVED).

If a value must leave the op, return the value rather than a reference, or put it in storage the caller passed. If you need storage that outlives the caller, use a region (chapter 18).

12.5 There is no mut ref slice#

Slices do not take mut ref.

module mref_slice .
rem expect: E-MREF-SLICE

proc shrink input p mut ref slice u8 . output u64 .
do
  return 0 .
end

$ lowentc --check mref_slice.low
mref_slice.low:4:0 E-MREF-SLICE: `mut ref slice` gives nothing that `mut slice` does not — the elements are already writable through a plain `mut slice` (the descriptor is copied, the bytes are shared). The ONLY thing it adds is replacing the caller's descriptor, which silently changes the length behind the caller's back. Say the new slice with a RETURN VALUE instead (SPEC-004 §4.4a: the windows through which someone else can change your local are listed, and this one is closed)

Passing a mut slice already makes the elements writable. The slice value {start, length} is copied, but the bytes it points to are the same. So what mut ref slice adds is exactly one thing — secretly changing the length and start of the caller’s slice. Then the caller’s loop has its length change even though its own code contains no assignment. Return the new slice instead.

module head .
rem run: first_two [9,8,7,6]

fn take_front input p slice u8 . input n u64 . output slice u8 .
  requires le n (len p) .
do
  return subslice p 0 n .
end

fn first_two input xs slice u8 . output u64 .
  requires ge (len xs) 2 .
do
  let front slice u8 be take_front xs 2 .
  return len front .
end

$ lowentc --run first_two head.low [9,8,7,6]
first_two([9,8,7,6]) = 2
  arg0 (written) = [9,8,7,6]

take_front returns a new slice pointing at the first n elements. That the length changed shows in the return value and in let front.

12.6 Common mistakes#

module mistake_nomutref .
rem expect: E-TYPE-ARG

proc bump input p mut_ref u64 . output u64 .
do
  set p (add (deref p) 1) .
  return deref p .
end

proc use_bump input start u64 . output u64 .
  requires lt start 1000 .
do
  var n u64 be start .
  rem ✘ `mut_ref` is missing at the call --- the number 7 is passed, not a reference
  let r u64 be bump n .
  return add n r .
end

$ lowentc --check mistake_nomutref.low
mistake_nomutref.low:15:0 E-TYPE-ARG: this op takes a BORROW here (`ref` / `mut_ref`), and a plain value was passed. Take the borrow at the call — `mut_ref <name>` — so the reader sees where the callee may write. It used to pass `--check` and stop at run time with `E-VM-TYPE: deref needs a reference`

module mistake_noderef .
rem expect: E-TYPE-REFVAL

fn twice input p ref u64 . output u64 .
do
  rem ✘ `p` is not a number but a reference to one --- read it with `deref p`
  return add p p .
end

fn double input x u64 . output u64 .
  requires le x 1000 .
do
  let n u64 be x .
  return twice (ref n) .
end

$ lowentc --check mistake_noderef.low
mistake_noderef.low:7:0 E-TYPE-REFVAL: a BORROW is being used where a number is expected. `ref t` / `mut_ref t` names a place, not the value in it — read it with `deref <name>` (and write through it with `set <name> …`). It used to pass `--check` and stop at run time with `E-VM-TYPE`, which blamed the arithmetic instead of the missing read

module mistake_letmutref .
rem expect: E-TYPE-ARGMUT

proc bump input p mut_ref u64 . output void .
do
  set p (add (deref p) 1) .
end

proc use_bump input start u64 . output u64 .
  requires lt start 1000 .
do
  rem ✘ a name made with `let` is lent for writing
  let n u64 be start .
  bump (mut_ref n) .
  return n .
end

$ lowentc --check mistake_letmutref.low
mistake_letmutref.low:14:0 E-TYPE-ARGMUT: a WRITE borrow (`mut_ref`) was taken of a name that cannot be written: a `let` binding (or a shared input). `let` says the value does not change (§6.5.1) — if a borrow could change it, the reader who checked that name once would be wrong, and the borrow makes the change invisible at the call site. Bind it with `var`, or take a read borrow (`ref`)

module copyparam .
rem run: use_inc 7

proc inc input x u64 . output u64 .
  requires lt x 1000 .
do
  rem `x` is a copy of the caller's value --- nothing done here reaches the caller's variable
  var y u64 be x .
  set y (add y 1) .
  return y .
end

proc use_inc input start u64 . output u64 .
  requires lt start 1000 .
do
  var n u64 be start .
  let r u64 be inc n .
  rem `n` is still 7 --- lend it with `mut_ref n` to let it change
  return n .
end

$ lowentc --run use_inc copyparam.low 7
use_inc(7) = 7

module seqborrow .
rem run: use_twice 7

proc bump input p mut_ref u64 . output void .
  requires lt (deref p) 1000 .
do
  set p (add (deref p) 1) .
end

proc use_twice input start u64 . output u64 .
  requires lt start 900 .
do
  var n u64 be start .
  rem the first borrow comes back when this call ends --- so the next line may borrow again
  bump (mut_ref n) .
  bump (mut_ref n) .
  return n .
end

$ lowentc --run use_twice seqborrow.low 7
use_twice(7) = 9

12.7 This chapter’s syntax at a glance#