19 Ownership — one party responsible for disposal

19.1 owned and drop#

owned t is a value that carries ownership. A value with ownership must be disposed of exactly once.

module sink .
rem run: use_once 5

type buffer u8 .

fn consume input h owned buffer . output u8 .
do
  drop h .
  return 0 .
end

fn use_once input v u8 . output u8 .
do
  var h owned buffer be v .
  return consume h .
end

$ lowentc --run use_once sink.low 5
use_once(5) = 0

consume takes an owned buffer and disposes of it with drop h .. use_once makes an owned value with var h owned buffer be v . and passes it to consume. At that moment ownership moves. Now consume is responsible for disposing of h, and use_once can no longer use h.

  use_once                              consume
  ┌──────────────────┐   pass (move)    ┌──────────────────┐
  │ h ──▶ [ buffer ] │ ───────────────▶ │ h ──▶ [ buffer ] │ ── drop h .  → gone
  └──────────────────┘                  └──────────────────┘
  h is now an empty name                 the one place responsible
  (using it again: E-OWN-MOVED)

Think of a locker with a single key. Once you hand the key over, you no longer hold it, and only the one person holding the key can empty (dispose of) the locker. So “two people empty it” (double free), “nobody empties it” (leak) and “open it again with the key you gave away” (use after move) cannot happen.

Using a moved value again is rejected.

module moved .
rem expect: E-OWN-MOVED

type buffer u8 .

fn consume input h owned buffer . output u8 .
do
  drop h .
  return 0 .
end

fn reuse input h owned buffer . output u8 .
do
  let a u8 be consume h .
  let b u8 be consume h .
  return add a b .
end

$ lowentc --check moved.low
moved.low:15:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today

Disposing twice is rejected too.

module twice_drop .
rem expect: E-OWN-MOVED

type buffer u8 .

fn twice input h owned buffer . output u8 .
do
  drop h .
  drop h .
  return 0 .
end

$ lowentc --check twice.low
twice.low:9:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today

The diagnostic notes that the specification always called this an error and that for a while nothing enforced it. Today translation stops it.

19.2 Where branches meet#

Where an if splits and rejoins, the ownership state must be the same on every path.

module join .
rem expect: E-OWN-JOIN

type buffer u8 .

fn maybe input h owned buffer . input c bool . output u8 .
do
  if c . do
    drop h .
  end
  return 0 .
end

$ lowentc --check join.low
join.low:8:0 E-OWN-JOIN: this `owned` value is CONSUMED on one path of this branch but still LIVE on another where they merge — Lowent requires the ownership state to be STATICALLY consistent at a join (RFC-0044 §9.3): no hidden drop-flag decides it at runtime. Consume it on EVERY path, or make it conditionally owned (`?owned`)

On the path where c is true, h was disposed of; on the false path it is still alive. After the paths meet, nobody can say whether h is alive. Some languages keep a hidden “already dropped” flag here, but Lowent requires the ownership state to be statically one thing. Dispose of it on both paths, or pass it on both paths.

              if c
          ┌─────┴─────┐
       drop h       (leave it)
       h: gone        h: alive
          └─────┬─────┘
       where the paths meet --- is h alive or not?  → no single answer, so it is refused

By the same principle, moving one owned field of an aggregate and then moving the whole aggregate again is rejected (E-OWN-PARTIAL). The receiver thinks it got a whole aggregate, but one field inside already belongs to someone else.

19.3 Release and completion#

Disposal comes in two kinds.

Release has no failure to swallow. Completion, done silently, has nowhere to hand its failure. The criterion is one: can finishing fail?

Which types require completion is declared by the program itself. If there is an op that takes the type as owned and returns a result, that is the declaration “finishing this can fail”. No new word is involved.

module complete .
rem run: session 3

type journal u64 .

enum flush_error do
  disk_full .
end

fn finish input j owned journal . output result u8 flush_error .
  errors disk_full eq j 0 .
do
  rem an empty journal means there was no room to write --- so this arm really does happen
  guard ne j 0 . else do
    drop j .
    return error disk_full .
  end
  drop j .
  return ok 0 .
end

fn session input n u64 . output result u8 flush_error .
  errors disk_full .
do
  var j owned journal be n .
  return finish j .
end

$ lowentc --run session complete.low 3
session(3) = ok 0

Because finish takes an owned journal and returns a result, journal becomes a type needing completion. session finishes it by calling finish j and returns that (possibly failing) result as its own. Letting it go out of scope without calling the completion is rejected.

module incomplete .
rem expect: E-OWN-INCOMPLETE

type journal u64 .

enum flush_error do
  disk_full .
end

fn finish input j owned journal . output result u8 flush_error .
  errors disk_full .
do
  drop j .
  return ok 0 .
end

fn forget input j owned journal . output u8 .
do
  return 0 .
end

$ lowentc --check incomplete.low
incomplete.low:11:0 W-ERRORS-UNRAISED: this `errors` clause names a failure the body never returns. The clause is read as a promise about what this op can do, and the callers write their handling from it — a branch that can never be taken is dead code the reader cannot tell from live code. Return it (`return error <variant>`), forward one (`try`), or remove the clause
17:0 E-OWN-INCOMPLETE: this value is dropped automatically at the end of scope — but the program itself declares an op that takes this type `owned` BY VALUE and returns a `result`: finishing it CAN FAIL. An automatic drop is a RELEASE (total, non-suspending), and it has nowhere to hand you that failure — it would SWALLOW it. A fallible finish (flush/commit/close) is a COMPLETION and must be EXPLICIT: call it and handle the `result`. If you really mean to discard the value and its failure, say so with `drop`. RFC-0058

As the diagnostic says, automatic disposal is a release, and a release has nowhere to return a failure, so it would swallow the failure. Finishing that can fail — flush, commit, close — must be written and called by the author.

19.4 Not counting on the operating system to clean up#

Many programs lean on “the operating system cleans up when the process ends anyway”. Lowent does not. Because a forgotten disposal is caught at translation, the same code holds in environments without an operating system — firmware whose process never ends.

19.5 At what strength is memory safety guaranteed?#

The words “memory safe” mean something only when they say what is safe and how. This language separates the strengths.

So calling this language “fully statically safe” would be wrong. It is a design that mixes what is stopped statically, what is stopped at run time, and what is proven. What is proven, and what gap lies between the proofs and the compiler, is covered in chapters 42 and 50.

19.6 Common mistakes#

module mistake_loopmove .
rem expect: E-OWN-MOVED

type buffer u8 .

fn consume input h owned buffer . output u8 .
do
  drop h .
  return 0 .
end

fn three_times input v u8 . output u8 .
do
  var h owned buffer be v .
  var i u64 be 0 .
  while lt i 3 . do
    rem ✘ the second round passes `h` again after the first round moved it away
    let a u8 be consume h .
    set i (add i 1) .
  end
  return 0 .
end

$ lowentc --check mistake_loopmove.low
mistake_loopmove.low:16:0 E-OWN-MOVED: this `owned` value is CONSUMED inside a LOOP and never put back — the SECOND iteration would be a use-after-move. A loop body must end the way it began: consume it and REASSIGN the place (`set <name> …`, which re-initialises it), or move the consumption out of the loop

module loopmove_fixed .
rem run: three_times 5

type buffer u8 .

fn consume input h owned buffer . output u8 .
do
  drop h .
  return 1 .
end

fn three_times input v u8 . output u8 .
do
  var h owned buffer be v .
  var n u8 be 0 .
  var i u64 be 0 .
  while lt i 3 . do
    set n (add n (consume h)) .
    rem refill the moved place with a new value --- the round ends in the same shape it began
    set h v .
    set i (add i 1) .
  end
  drop h .
  return n .
end

$ lowentc --run three_times loopmove_fixed.low 5
three_times(5) = 3

module mistake_readmove .
rem expect: E-OWN-MOVED

type buffer u8 .

fn peek input h owned buffer . output u8 .
do
  rem ✘ taking the value into a name is a move too --- the `drop h` after it destroys a moved value
  let v u8 be h .
  drop h .
  return v .
end

$ lowentc --check mistake_readmove.low
mistake_readmove.low:10:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today

module mistake_twonames .
rem expect: E-OWN-MOVED

type buffer u8 .

fn consume input h owned buffer . output u8 .
do
  drop h .
  return 0 .
end

fn both input h owned buffer . output u8 .
do
  rem ✘ believed a second name makes a copy --- ownership moved to `h2`
  var h2 owned buffer be h .
  let a u8 be consume h2 .
  let b u8 be consume h .
  return 0 .
end

$ lowentc --check mistake_twonames.low
mistake_twonames.low:17:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today

module implicit_release .
rem run: keep_or_drop 5 1
rem run: keep_or_drop 5 0

type buffer u8 .

rem the path where `c` is false leaves without `drop` --- release cannot fail, so it happens quietly where the lifetime ends
fn keep_or_drop input v u8 . input c u8 . output u8 .
do
  var h owned buffer be v .
  guard eq c 1 . else return 0 .
  drop h .
  return 1 .
end

$ lowentc --run keep_or_drop implicit_release.low 5 1
keep_or_drop(5, 1) = 1
$ lowentc --run keep_or_drop implicit_release.low 5 0
keep_or_drop(5, 0) = 0

19.7 This chapter’s syntax at a glance#