14 Contracts — write them, have them checked, lose the checks

14.1 A contract is a checked promise#

A contract is the promise an op makes about its own inputs and outputs. Unlike a comment, it is checked.

module pair .
rem run: read_pair [1,2,3]

fn read_pair input data slice u8 . output u32 .
  requires ge (len data) 2 .
  ensures le ret 65535 .
do
  let hi u32 be widen u32 (index data 0) .
  let lo u32 be widen u32 (index data 1) .
  return add (mul hi 256) lo .
end

$ lowentc --run read_pair pair.low [1,2,3]
read_pair([1,2,3]) = 258
  arg0 (written) = [1,2,3]

Read aloud, the head says: “this op must be given a byte sequence of length at least 2 (requires), promises that the value it returns is at most 65535 (ensures), and is pure (fn).” You know that much without opening the body. In ensures, ret stands for the returned value.

A contract is used in three places. The processor uses it as a fact to remove checks. A contract the processor could not prove is checked at run time and stops when broken. And it tells the reader what must be kept to call this op.

14.2 Whose fault is it?#

There are two places a contract breaks, and the diagnostic assigns blame.

Draw a contract as an op’s two doors and the blame is decided by which door caught it.

        caller                         op
                         ┌─────────────────────────────────────┐
  percent_of 250 200 ───▶│ way in:  requires                   │  caught here  → the caller's fault
                         │                                     │
                         │   … body …                          │
                         │                                     │
            result ◀─────│ way out: ensures · errors … cond    │  caught here  → this op's fault
                         └─────────────────────────────────────┘

module blame .
rem run: percent_of 50 200
rem trap: percent_of 250 200
rem run: clamp_to_100 400
rem trap: clamp_to_100 120

fn percent_of input part u64 . input whole u64 . output u64 .
  requires le part whole .
  requires gt whole 0 .
  requires le whole 1000000 .
  ensures le ret 100 .
do
  return div (mul part 100) whole .
end

rem clamps only values above 150 and forgets 101 … 150
fn clamp_to_100 input n u64 . output u64 .
  requires le n 1000 .
  ensures le ret 100 .
do
  if gt n 150 . do
    return 100 .
  end
  return n .
end

$ lowentc --run percent_of blame.low 50 200
percent_of(50, 200) = 25
$ lowentc --run clamp_to_100 blame.low 400
clamp_to_100(400) = 100
$ lowentc --run percent_of blame.low 250 200
== ir diagnostics (1) ==
0:0 E-VM-CONTRACT: `requires` violated at entry — the caller broke the contract
$ lowentc --run clamp_to_100 blame.low 120
== ir diagnostics (1) ==
0:0 E-VM-CONTRACT: `ensures` violated at exit — THIS op broke its own promise (the caller was told a lie)

percent_of 250 200 has a part larger than the whole, so it is the caller’s fault, and the VM says “the caller broke the contract”. clamp_to_100 120 is the fault of an op that forgot to clamp values from 101 to 150, and the VM says “THIS op broke its own promise”. When a program stops, the diagnostic answers at once “did I call it wrong, or is that op built wrong?”.

14.3 Contracts remove checks#

The processor uses contracts as facts to narrow the ranges values can take. When those ranges show safety, it removes overflow, division by zero, narrowing and slice bounds checks. So in this language writing honestly makes code faster.

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

fn proven input a u8 . output u8 .
  requires le a 200 .
do
  return add a 1 .          rem no check --- it cannot exceed 201
end

The two ops have the same body. The only difference is one line of contract, and that line removes a run-time check. What the processor thinks is this short:

 requires le a 200 .     →  a is 0 … 200
 add a 1                 →  the result is 1 … 201
 does it fit u8?         →  201 ≤ 255  ⇒ cannot overflow  ⇒ drop the overflow check

The check did not vanish but was moved to one check on entry. If the caller calls with a constant, or proves the range with its own contract, even the entry check disappears.

There is one important rule. A contract that is not enforced is not used as a fact. Trusting without checking and removing checks is not being faster but being wrong. This rule returns below with grades and build modes.

14.4 Conditions over every element#

A contract’s condition is a pure expression. Loops are statements, so “every element is at most 9” cannot be written as a loop. There are words that say it instead.

module elems .
rem run: digit_sum [1,2,3,9]
rem trap: digit_sum [1,20]

fn digit_sum input ds slice u8 . output u64 .
  requires elem_le ds 9 .
do
  var s u64 be 0 .
  for d ds do
    set s (add s (widen u64 d)) .
  end
  return s .
end

$ lowentc --run digit_sum elems.low [1,2,3,9]
digit_sum([1,2,3,9]) = 15
  arg0 (written) = [1,2,3,9]
$ lowentc --run digit_sum elems.low [1,20]
== ir diagnostics (1) ==
0:0 E-VM-CONTRACT: `requires` violated at entry — the caller broke the contract

elem_le ds 9 means every element is at most 9. There are also elem_lt, elem_gt and elem_ge. The condition is checked once on entry, and the arithmetic in the body uses the fact that the elements are at most 9.

14.5 Naming a contract#

When several ops require the same condition, give the condition a name.

module named .
rem run: half 10
rem run: third 10

contract positive do
  requires ge a 1 .
end

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

fn third satisfies positive . input a u8 . output u8 .
do
  return div a 3 .
end

$ lowentc --run half named.low 10
half(10) = 5
$ lowentc --run third named.low 10
third(10) = 3

contract positive do … end is a named contract, and an op adopts it with satisfies positive . at the very front of its head. Repeating the same condition by hand in several places means fixing one and forgetting another; a name leaves one place to fix. satisfies comes first in the head because it says what the op is first (chapter 3).

14.6 Decide now what can be decided now#

When a call breaks the callee’s requires and both sides are constants, translation rejects it without waiting to run.

module impossible .
rem expect: E-CONTRACT-IMPOSSIBLE

fn small input a u8 . output u8 .
  requires lt a 10 .
do
  return a .
end

fn caller output u8 .
do
  return small 200 .
end

$ lowentc --check impossible.low
impossible.low:12:0 E-CONTRACT-IMPOSSIBLE: this call breaks the callee's `requires`, and BOTH SIDES ARE CONSTANTS — so it can be decided here, now. It used to compile green and trap at run time (E-VM-CONTRACT): a bit budget that does not fit (`slot + shard + generation > word`) shipped as a runnable program. A contract that can be decided at compile time IS decided at compile time (RFC-0104 §8-3)

As the diagnostic’s story says, this once translated green and only stopped at run time. A program carrying a bit budget that did not fit shipped in runnable form. A contract whose answer is available now is decided now.

The mistake in the other direction is rejected too. Declaring an error for a condition that requires already excludes means that error can never happen.

module dead .
rem expect: E-CONTRACT-DEAD

enum div_error do
  by_zero .
end

fn safe_div input a u32 . input b u32 . output result u32 div_error .
  requires ne b 0 .
  errors by_zero eq b 0 .
do
  guard ne b 0 . else return error by_zero .
  return ok (div a b) .
end

$ lowentc --check dead.low
dead.low:10:0 E-CONTRACT-DEAD: this declared error can never occur: `requires` already excludes the condition, and the condition's inputs cannot change during the op (remove the `requires`, or remove the error — not both)

With requires ne b 0 ., errors by_zero eq b 0 . can never be true. If the declaration stays, callers write code to handle by_zero, and that code never runs. Code that never runs is never tested, and untested code is wrong someday. The diagnostic says to remove one of the two — either make it the caller’s responsibility (requires) or have the op handle it itself (errors).

14.7 Contract grades#

A grade on a single contract clause decides when and how its condition is treated. The shape is requires <grade> <condition> ..

module grades .
rem run: bump_checked 10
rem trap: bump_checked 250
rem run: bump_assumed 10
rem trap: bump_assumed 255

fn bump_checked input a u8 . output u8 .
  requires le a 200 .
do
  return add a 1 .
end

fn bump_assumed input a u8 . output u8 .
  requires assume le a 200 .
do
  return add a 1 .
end

$ lowentc --run bump_checked grades.low 10
bump_checked(10) = 11
$ lowentc --run bump_assumed grades.low 10
bump_assumed(10) = 11
$ lowentc --run bump_checked grades.low 250
== ir diagnostics (1) ==
0:0 E-VM-CONTRACT: `requires` violated at entry — the caller broke the contract
$ lowentc --run bump_assumed grades.low 255
== ir diagnostics (1) ==
0:0 E-VM-OVERFLOW: integer overflow at the declared width (use wrap_*/sat_*, or prove the range)

The same condition is written two ways. bump_checked rejects 250 on entry and then removes the overflow check in add a 1. bump_assumed does not check on entry. In exchange it does not use the condition as a fact either, so the overflow check remains. That is why giving it 255 stops with overflow (E-VM-OVERFLOW), not with a contract violation.

assume is a place to write down what the processor cannot yet prove but a person knows. Written down, readers know it, and when the processor grows it can be raised to static. Treating an unenforced condition as a fact would mean removing checks that should not have been removed, and believing that was right when the condition turns out false. So assume is not a fact.

14.8 Build modes decide the remaining checks#

Proven contracts leave no check in any mode. What a build mode decides is the treatment of contracts that could not be proven. The mode is written in the source as build <mode> ..

module fast .
rem run: bump 10
rem run: bump 250

build release_fast .

fn bump input a u8 . output u8 .
  requires le a 200 .
do
  return add a 1 .
end

$ lowentc --run bump fast.low 10
bump(10) = 11
$ lowentc --run bump fast.low 250
bump(250) = 251

Under build release_fast ., bump 250 does not stop and gives 251. The same source stops under debug. release_fast opens one more trust boundary, where a person promises the contracts are true. It is one reason the claim that this language has no undefined behaviour is limited to “the safe subset”. Removing checks for speed is a choice you may make, but the fact of choosing must stay in the source. That is why the mode is a build statement and not a command-line flag.

14.9 Common mistakes#

module mistake_result .
rem expect: E-ENS-UNDEF

fn clamp input a u8 . output u8 .
  rem ✘ the returned value is named `ret`, not `result`
  ensures le result 100 .
do
  guard le a 100 . else return 100 .
  return a .
end

$ lowentc --check mistake_result.low
mistake_result.low:6:0 E-ENS-UNDEF: ensures references an undefined name — an ensures that names nothing checks nothing, and the interval analysis DERIVES the result range from it (`ret` is the result)

module mistake_leindex .
rem run: at [1,2,3] 2
rem trap: at [1,2,3] 3

fn at input xs slice u8 . input i u64 . output u8 .
  rem ✘ `le` allows `i = len xs` --- that slot is one past the end
  requires le i (len xs) .
do
  return index xs i .
end

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

module mistake_contradict .
rem expect: E-CONTRACT-UNSAT

rem ✘ no value satisfies both conditions --- every call stops
fn pick input a u8 . output u8 .
  requires le a 100 .
  requires ge a 200 .
do
  return a .
end

$ lowentc --check mistake_contradict.low
mistake_contradict.low:7:0 E-CONTRACT-UNSAT: two preconditions on the same input cannot both hold, so EVERY call stops at the door and the body never runs. A contract that no argument satisfies is not a strong contract, it is a dead op — usually one line left behind when the other was edited. Keep the one you meant

module contract_input .
rem run: check_age 30
rem trap: age_strict 200
rem run: age_checked 200

enum age_error do
  too_old .
end

rem contract: accept only values the caller has already checked --- breaking it stops the program
fn age_strict input a u8 . output u8 .
  requires le a 150 .
do
  return a .
end

rem values from outside may be wrong --- report it as a value
fn age_checked input a u8 . output result u8 age_error .
  errors too_old gt a 150 .
do
  guard le a 150 . else return error too_old .
  return ok a .
end

fn check_age input a u8 . output u8 .
do
  match age_checked a do
    case ok v . return age_strict v .
    case error e . return 0 .
  end
end

$ lowentc --run check_age contract_input.low 30
check_age(30) = 30
$ lowentc --run age_checked contract_input.low 200
age_checked(200) = err too_old
$ lowentc --run age_strict contract_input.low 200
== ir diagnostics (1) ==
0:0 E-VM-CONTRACT: `requires` violated at entry — the caller broke the contract

14.10 This chapter’s syntax at a glance#