14 계약 — 적고, 검사받고, 검사를 지운다

14.1 계약은 검사되는 약속이다#

계약은 op 이 자기 입력과 출력에 대해 스스로 적는 약속이다. 주석과 달리 검사된다.

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]

머리를 소리 내어 읽으면 이렇다. “이 op 은 길이가 2 이상인 바이트 줄을 받아야 하고(requires), 돌려주는 값은 65535 이하임을 약속하며(ensures), 순수하다(fn).” 본문을 열지 않고도 이만큼 안다. ensures 에서 ret 은 돌려주는 값을 가리킨다.

계약은 세 곳에서 쓰인다. 처리기는 계약을 사실로 삼아 검사를 지운다. 증명하지 못한 계약은 실행 중에 확인되고, 깨지면 멈춘다. 그리고 읽는 사람에게 이 op 을 부르려면 무엇을 지켜야 하는지 말한다.

14.2 누구의 잘못인가#

계약이 깨지는 자리는 둘이고, 진단이 책임을 가른다.

계약을 op 의 드나드는 문 두 개로 그리면 누구의 잘못인지가 자리로 갈린다.

        부르는 쪽                      op
                         ┌─────────────────────────────────────┐
  percent_of 250 200 ───▶│ 들어오는 문: requires               │  여기서 걸리면  → 부르는 쪽 잘못
                         │                                     │
                         │   … 본문 …                          │
                         │                                     │
            결과 ◀───────│ 나가는 문:   ensures · errors … 조건 │  여기서 걸리면  → 이 op 잘못
                         └─────────────────────────────────────┘

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 150 을 넘는 값만 자르고, 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 은 부분이 전체보다 크니 부르는 쪽의 잘못이고, VM 은 “the caller broke the contract” 라고 말한다. clamp_to_100 120 은 n 이 101 … 150 일 때 자르기를 잊은 op 의 잘못이고, VM 은 “THIS op broke its own promise” 라고 말한다. 프로그램이 멈췄을 때 “내가 잘못 불렀나, 저 op 이 잘못 만들어졌나” 를 진단이 바로 답한다.

14.3 계약이 검사를 지운다#

처리기는 계약을 사실로 삼아 값이 가질 수 있는 범위를 좁힌다. 그 범위가 안전함을 보이면 넘침·0 나누기·좁히기· 슬라이스 경계 검사를 지운다. 그래서 이 언어에서는 정직하게 적는 쪽이 빠르다.

fn bare input a u8 . output u8 .
do
  return add a 1 .          rem 넘침 검사가 남는다
end

fn proven input a u8 . output u8 .
  requires le a 200 .
do
  return add a 1 .          rem 검사가 없다 — 201 을 넘을 수 없다
end

두 op 은 본문이 같다. 다른 것은 계약 한 줄뿐이고, 그 한 줄이 실행 중 검사 하나를 없앤다. 처리기가 하는 생각은 이렇게 짧다.

 requires le a 200 .     →  a 는 0 … 200
 add a 1                 →  결과는 1 … 201
 u8 에 들어가나?          →  201 ≤ 255  ⇒ 넘칠 수 없다  ⇒ 넘침 검사를 지운다

검사가 사라진 것이 아니라 진입의 한 번으로 옮겨진 것이다. 부르는 쪽이 상수로 부르거나 자기 계약으로 범위를 증명하면 진입 검사마저 사라진다.

중요한 규칙이 하나 있다. 강제되지 않는 계약은 사실로 쓰지 않는다. 확인 없이 믿고 검사를 지우면, 그것은 빨라진 것이 아니라 틀린 것이다. 이 규칙이 뒤의 등급과 빌드 모드에서 다시 나온다.

14.4 모든 원소에 대한 조건#

계약의 조건은 순수한 식이다. 되풀이는 문장이므로 “모든 원소가 9 이하” 를 반복문으로 적을 수 없다. 그래서 그 말을 하는 낱말이 따로 있다.

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 는 모든 원소가 9 이하라는 뜻이다. elem_lt·elem_gt·elem_ge 도 있다. 이 조건은 진입에서 한 번 확인되고, 본문의 산술은 원소가 9 이하라는 사실을 쓴다.

14.5 계약에 이름을 준다#

여러 op 이 같은 조건을 요구하면 그 조건에 이름을 준다.

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 가 이름 붙은 계약이고, op 은 머리 맨 앞의 satisfies positive . 로 그것을 갖춘다. 같은 조건을 여러 곳에 손으로 되풀이하면 하나를 고치고 다른 하나를 잊는다. 이름을 주면 고칠 자리가 하나가 된다. satisfies 가 머리의 맨 앞에 오는 것은 이 op 이 무엇인지를 먼저 말하기 때문이다(3장).

14.6 지금 판정할 수 있으면 지금 판정한다#

부르는 자리가 상대의 requires 를 어기고 양쪽이 모두 상수이면, 실행을 기다리지 않고 번역에서 거절된다.

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)

진단이 적은 사연대로, 이것은 한때 초록으로 번역되어 실행 중에야 멈췄다. 맞지 않는 비트 예산을 지닌 프로그램이 실행할 수 있는 모습으로 배포되었다. 답이 지금 나는 계약은 지금 말한다.

반대쪽 실수도 거절된다. requires 가 이미 배제한 조건에 오류를 선언하면, 그 오류는 결코 나지 않는다.

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)

requires ne b 0 . 가 있으니 errors by_zero eq b 0 . 은 영영 참이 될 수 없다. 이 선언이 남아 있으면 부르는 쪽은 by_zero 를 다루는 코드를 쓰고, 그 코드는 영영 돌지 않는다. 돌지 않는 코드는 시험되지 않고, 시험되지 않는 코드는 언젠가 틀린다. 진단은 둘 중 하나를 지우라고 한다 — 부르는 쪽에 책임을 지우든(requires), op 이 스스로 처리하든(errors).

14.7 계약의 등급#

계약 절 하나에 등급을 붙여 그 조건을 언제 무엇으로 다룰지 정할 수 있다. requires <등급> <조건> . 꼴이다.

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)

같은 조건을 두 가지로 적었다. bump_checked 는 진입에서 250 을 거절하고, 그 뒤 add a 1 의 넘침 검사를 지운다. bump_assumed 는 진입에서 검사하지 않는다. 대신 조건을 사실로 쓰지도 않으므로 넘침 검사가 남는다. 그래서 255 를 주면 계약이 아니라 넘침(E-VM-OVERFLOW)으로 멈춘다.

assume 은 아직 처리기가 증명할 수 없지만 사람은 아는 것을 적어 두는 자리다. 적어 두면 읽는 사람이 알고, 나중에 처리기가 자라면 static 으로 올릴 수 있다. 지켜지지 않는 조건을 사실로 삼으면, 조건이 거짓일 때 지우지 말았어야 할 검사를 지운 채 옳다고 믿게 된다. 그래서 assume 은 사실이 아니다.

14.8 빌드 모드가 남은 검사를 정한다#

증명된 계약은 어느 모드에서도 검사가 남지 않는다. 빌드 모드가 정하는 것은 증명하지 못한 계약의 처분이다. 모드는 소스에 build <모드> . 로 적는다.

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

build release_fast . 아래에서 bump 250 은 멈추지 않고 251 을 낸다. 같은 소스가 debug 에서는 멈춘다. release_fast 는 계약이 참임을 사람이 약속하는 신뢰 경계를 하나 더 여는 것이다. 이 언어가 미정의 동작을 없앴다고 말하는 범위가 “안전한 부분집합” 으로 한정되는 이유 가운데 하나다. 속도를 위해 검사를 없애는 것은 고를 수 있는 일이지만, 고른다는 사실이 소스에 남아야 한다. 그래서 모드는 명령 줄 깃발이 아니라 build 문장이다.

14.9 흔한 실수#

module mistake_result .
rem expect: E-ENS-UNDEF

fn clamp input a u8 . output u8 .
  rem ✘ 돌려주는 값의 이름은 `result` 가 아니라 `ret` 이다
  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` 는 `i = len xs` 를 허락한다 --- 그 칸은 한 칸 밖이다
  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 ✘ 두 조건을 함께 만족하는 값이 없다 --- 어떻게 불러도 멈춘다
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 계약: 부르는 쪽이 이미 확인한 값만 받는다 --- 어기면 프로그램이 멈춘다
fn age_strict input a u8 . output u8 .
  requires le a 150 .
do
  return a .
end

rem 바깥에서 온 값은 틀릴 수 있다 --- 틀림을 값으로 돌려준다
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 이 장의 문법 한눈에#