40 수의 증명 — 넓히기, 좁히기, 나눗셈

먼저 알아야 할 것

4장 수 · 넓히기는 저절로, 좁히기는 적는다

13장 이름 붙인 타입 · range lo hi 는 매개변수의 생김새가 된 계약이다

39장 수학 도구상자 · 부분 순서의 세 조건과 join

돌아보기

4장에서 u8 과 i16 은 섞을 수 있지만 u32 와 i32 는 섞을 수 없었다. 무엇이 둘을 갈랐는가?

답. 값을 지키는 넓히기가 있느냐였다. u8 의 모든 값(0 … 255)은 i16 에 들어가지만, u32 의 큰 값은 폭이 같은 i32 에 들어가지 않는다. 이 장은 그 “값을 지키는 넓히기” 를 39장의 부분 순서로 정의하고, 그것이 정말 안전하다는 기계 증명을 읽는다.

이 장의 필요성과 맥락

C 에서 unsigned char small = 300; 은 경고 없이 44 가 되고, -1 을 unsigned int 에 넣으면 4294967295 가 된다. Lowent 는 값이 보존되는 넓히기만 저절로 허락하고, 잃어도 괜찮으면 어떻게 잃을지 골라 적게 한다(narrow_wrap·narrow_sat·narrow_try). 그 규칙이 옳다는 말은 표 몇 줄이 틀리지 않았다는 뜻인데, 사람은 그런 표를 틀린다. 그래서 정의를 수학으로 세우고 경우를 하나도 빠뜨리지 않았음을 기계에 맡겼다. 코드와 가장 직접 닿는 증명이라 제10부의 도구 다음에 둔다.

이 장이 끝나면

넓히기 관계 ⊑ 의 네 줄 정의와 그것이 값을 보존하는 부분 순서라는 정리, join 과 좁히기의 성질을 알게 된다. 나눗셈이 실패하는 경우가 정확히 무엇인지, mod 와 부호의 약속, range 가 검사를 지우는 근거가 되는 정리들을 익힌다. 타입 규칙의 세 정리(progress·preservation· values_fit)가 멈춤을 어떻게 정직하게 모델에 넣었는지도 보게 된다.

이 장에서 답할 질문

넓히기가 실패할 수 없다는 것은 따로 증명할 만한가?

40.1 넓히기는 부분 순서다#

t ⊑ u 는 “타입 t 의 어떤 값이든 타입 u 에 값이 변하지 않고 들어간다” 로 읽는다. 정의는 네 줄이다.

왼쪽 → 오른쪽	조건	왜
`uN` → `uM`	N ≤ M	부호 없음끼리는 폭만 넓으면 된다
`iN` → `iM`	N ≤ M	부호 있음끼리도 같다
`uN` → `iM`	N < M	`u8`(255)은 `i8`(127)에 안 들어간다. 폭이 더 커야 한다
`iN` → `uM`	없음	음수를 담을 곳이 없다

표 40.1 — 넓히기 관계 ⊑

셋째 줄의 < 가 요점이다. ≤ 로 적었다면 u8 ⊑ i8 이 허용되고 255 가 −1 로 바뀐다. 이 한 글자가 값의 안전을 가르고, 사람이 이런 것을 틀린다.

 u8 ──▶ u16 ──▶ u32 ──▶ u64
   ╲       ╲       ╲
    ▼       ▼       ▼
 i8 ──▶ i16 ──▶ i32 ──▶ i64

 → 는 ⊑ (값이 안 바뀌고 들어간다). 화살을 이어 가면 그것도 ⊑ 다(추이성).
 u8 → i8 · u16 → i16 … 처럼 같은 폭으로 내려가는 화살은 없다 (N < M).
 i 줄에서 u 줄로 올라가는 화살도 없다 (음수를 담을 곳이 없다).

examples/ch40/order_strict.low

module order_strict .
rem expect: E-TYPE-SIGN

fn same_width input a u8 . output i8 .
do
  return a .
end

실행 결과

$ lowentc --check order_strict.low
order_strict.low:6:0 E-TYPE-SIGN: sign mismatch: no value-preserving widening exists (widen both to a strictly wider signed type, or bitcast_sign)

examples/ch40/order_ok.low

module order_ok .
rem run: wider 200

fn wider input a u8 . output i16 .
do
  return a .
end

실행 결과

$ lowentc --run wider order_ok.low 200
wider(200) = 200

NumericLattice.v 가 이 관계에 대해 증명한 것들이다.

값을 보존한다(sub_preserves). t ⊑ u 이고 v 가 t 의 범위에 있으면 u 의 범위에도 있다. 넓히기에 실행 중 검사가 없는 근거다.
부분 순서다(sub_refl·sub_trans·sub_antisym). 추이성이 깨지면 u8 → u16 과 u16 → u32 는 되는데 u8 → u32 는 안 되는 언어가 된다. 표를 손으로 관리하면 실제로 그런 구멍이 생긴다.
join 은 둘 다를 담고, 둘 가운데 하나다(join_sound·join_is_an_operand). 두 값을 한 연산에 넣을 때 고르는 타입은 두 값을 모두 담고, 소스에 없는 제3의 타입을 지어내지 않는다(39장의 u8 ⊔ u16 = u16).
좁히기의 조건은 정확히 하나다(narrow_ok_iff). narrow_try u8 300 이 조용히 성공해 44 를 주는 일이 없다.

수학. 넓히기가 값을 보존한다는 증명의 뼈대

경우를 넷으로 나눈다. uN ⊑ uM(N ≤ M)이면 두 아래 끝이 모두 0 이고, 위 끝은 2^N − 1 ≤ 2^M − 1 이다 — 2 의 거듭제곱이 단조라는 사실만 쓴다. uN ⊑ iM(N < M)이면 N ≤ M − 1 이므로 2^N − 1 ≤ 2^M−1 − 1 이다. 부호 있음끼리도 같고, iN ⊑ uM 은 정의상 거짓이라 할 일이 없다. 핵심 보조정리는 “a ≤ b 이면 2^a ≤ 2^b” 하나다. 증명 전체가 고등학교 지수법칙 위에 서 있다. 어려운 것은 논증이 아니라 경우를 하나도 빠뜨리지 않는 것이고, 그것이 기계에게 맡기는 이유다.

40.2 나눗셈과 나머지#

나눗셈은 이 언어가 유별나게 조심하는 자리다.

examples/ch40/division.low

module division .
rem run: quot -7 2
rem trap: quot -128 -1
rem run: rest -7 3
rem run: rest 7 -3

fn quot input a i8 . input b i8 . output i8 . do
  return div a b .
end

rem mod 의 부호는 나누는 수를 따른다
fn rest input a i8 . input b i8 . output i8 . do
  return mod a b .
end

실행 결과

$ lowentc --run quot division.low -7 2
quot(-7, 2) = -3
$ lowentc --run rest division.low -7 3
rest(-7, 3) = 2
$ lowentc --run rest division.low 7 -3
rest(7, -3) = -2
$ lowentc --run quot division.low -128 -1
== ir diagnostics (1) ==
0:0 E-VM-OVERFLOW: division overflow (MIN / -1) at the declared width

부호 있는 나눗셈 -7 / 2 는 0 쪽으로 잘라 −3 이다. -128 / -1 은 i8 에 128 이 없으므로 멈춘다. C 에서는 이 한 경우가 정의되지 않은 동작이다. mod 의 부호는 나누는 수를 따른다 — mod -7 3 은 2, mod 7 -3 은 −2 다.

정리	뜻
`div_unsigned_total`	부호 없는 나눗셈은 0 으로 나누지 않으면 언제나 성공한다
`div_signed_failure_is_only_min_neg1`	부호 있는 나눗셈이 실패하는 경우는 `MIN / −1` 하나뿐이다
`mod_sign_follows_divisor`	`mod` 의 부호는 나누는 수를 따른다
`mod_is_a_safe_index`	`mod h (len s)` 는 언제나 0 이상 `len s` 미만이다

표 40.2 — 나눗셈과 나머지에 대해 증명된 것

 부호 없는 div a b    b = 0                 → 멈춘다
                      그 밖                 → 언제나 값
 부호 있는 div a b    b = 0                 → 멈춘다
                      a = MIN 이고 b = −1   → 멈춘다 (C 에서는 미정의 동작)
                      그 밖                 → 언제나 값 (0 쪽으로 자른다)
 mod h n              n > 0 이면            → 0 ≤ 결과 < n  (안전한 색인)

마지막 정리가 실전에서 값이 크다.

examples/ch40/modslot.low

module modslot .
rem run: pick [5,6,7,8] 1000003
rem ir

fn pick input table slice u8 . input h u64 . output u8 .
  requires gt (len table) 0 .
do
  return index table (mod h (len table)) .
end

실행 결과

$ lowentc --run pick modslot.low [5,6,7,8] 1000003
pick([5,6,7,8], 1000003) = 8
  arg0 (written) = [5,6,7,8]
$ lowentc --ir modslot.low
-- runtime checks (interval analysis: overflow · division · narrowing) --
   2 / 2 removed  (100%)

해시 테이블은 늘 mod 로 칸을 고르는데, 그 결과가 범위 안임이 증명되므로 색인 검사가 사라진다. len s 가 0 이면? 0 으로 나누므로 먼저 멈춘다. 그래서 값이 나온 경로에서는 len s > 0 이 보장된다. 논증에 빈틈이 없다.

40.3 `range` 가 주는 정리#

매개변수의 타입 자리에 적은 range lo hi(13장)는 넓히기 이야기를 한 겹 더 정밀하게 만든다.

정리	뜻
`rsub_preserves`	범위끼리의 넓히기도 값을 보존한다
`radd_sound`	두 범위를 더한 결과는 계산된 범위 안에 있다
`radd_no_check`	결과 범위가 타입 안에 들어가면 넘침 검사가 필요 없다
`idx_no_check`	색인 범위가 길이 안이면 경계 검사가 필요 없다
`rdisj_no_value`	서로소인 두 범위에는 공통 값이 없다(그래서 갈래 하나가 죽는다)
`derive_minimal`	도출된 범위는 가장 작은 것이다(필요 이상으로 넓지 않다)

표 40.3 — 범위에 대해 증명된 것

radd_no_check 와 idx_no_check 가 검사를 지우는 최적화의 정당성이다. 그 두 정리를 실제 코드에 적용하는 분석은 41장에서 본다.

40.4 멈춤을 정직하게 모델에 넣는다#

타입 규칙은 한 층 더 깊이 증명되어 있다(LowentType.v). 폭과 부호가 붙은 수치 식에 묶기·갈래·비교·좁히기·검사되는 산술·감싸는 산술을 얹고 세 정리를 증명했다.

progress — 타입이 붙은 닫힌 식은 값이거나, 멈추거나, 한 걸음 간다. 막히지 않는다.
preservation — 한 걸음 가도 타입이 바뀌지 않는다.
values_fit — 실행이 값에 닿으면 그 값은 언제나 그 타입의 폭 안에 있다.

세 번째가 이 언어에서 특별하다. u8 자리에 8 비트를 넘는 값이 들어오면 방출된 C 가 조용히 다른 일을 한다. 그래서 범위를 타입 규칙 안에 넣고 (값에 타입을 붙이려면 범위 증거가 있어야 한다) 실행 내내 보존됨을 증명했다.

그리고 결론이 셋인 것이 요점이다. 검사되는 산술은 넘치면 값을 내지 않고 멈춘다. 멈춤을 값에 넣으면 정리가 거짓말이 되고, 멈춤을 빼면 정리가 거짓이 된다. 그래서 “값이거나 · 멈추거나 · 한 걸음” 이다. 멈춤을 번역 시각에 막는 것은 정상 경로의 일이고, 계약과 증명서가 그 일을 한다 (41장).

 타입이 붙은 닫힌 식 e
    ├─▶ 값 v          values_fit: v 는 언제나 그 타입의 폭 안
    ├─▶ 멈춘다        검사되는 산술이 넘쳤다 · 0 으로 나눴다
    └─▶ 한 걸음 → e'  preservation: e' 도 같은 타입이다 (그리고 다시 셋 가운데 하나)

문. 넓히기가 실패할 수 없다는 것은 따로 증명할 만한가?

답. 그렇다(widen_never_fails). “실패할 수 없음” 이 증명되어야 넓히기 자리에 실행 중 검사를 두지 않아도 된다. 그것이 넓히기가 공짜인 이유다. 반대로 좁히기는 narrow_ok_iff 가 성공 조건을 “정확히 범위 안” 으로 못 박으므로, narrow_try u8 300 은 조용히 44 를 주지 않고 none 이다. 실패가 값이다.

흔한 오해. values_fit 가 증명되었으니 이 판의 컴파일러에서 u8 자리에 넘치는 값이 들어올 일은 없다

정리는 타입 규칙에 대한 것이다. 컴파일러가 모든 자리에서 그 규칙을 따르는지는 따로다. 이 매뉴얼을 쓰며 찾은 예로, pipe 의 map 이 u64 를 내는데 collect into 가 u8 버퍼에 담는 자리를 이 판의 도구가 오래도록 조용히 감았다(지금은 E-TYPE-COLLECT 로 거절한다, 24장). 규칙이 옳다는 증명과 구현이 규칙을 빠짐없이 적용한다는 사실 사이의 틈이 이런 자리에서 드러나고, 그 틈은 시험과 두 백엔드 대조가 메운다. 증명은 “무엇을 막아야 하는가” 를 정하고, 막았는지는 재서 확인한다.

40.5 증명하지 않은 것#

부동소수는 이 격자에 없다. 정수만 다뤘다. f32 → f64 는 값을 보존하지만, 반대 방향과 섞인 연산은 별도 규칙이며 여기서 증명되지 않았다. 반올림·NaN·−0 도 다루지 않았다.
폭은 8·16·32·64 넷으로 고정했다. 임의 폭 정수(bits 7 같은 것)는 구현에는 있지만(13장) 이 모델 밖이고, u128 은 모델에도 구현에도 없다.
정리는 타입 규칙에 대한 것이다. 컴파일러가 그 규칙을 정확히 구현했는지는 시험과 두 백엔드 대조가 확인한다(31장).

복습 정리

넓히기 ⊑ 는 네 줄로 정의된 부분 순서이고, uN ⊑ iM 의 조건은 엄격한 N < M 이다. 넓히기는 값을 보존하고 실패할 수 없으며, join 은 두 피연산자 가운데 하나이고, 좁히기의 성공 조건은 정확히 범위 안이다. 부호 있는 나눗셈의 실패는 MIN / −1 하나뿐이고 mod 는 나누는 수의 부호를 따르며 언제나 안전한 색인이다. range 의 정리들이 검사를 지우는 근거가 되고, 타입 규칙은 “값·멈춤·한 걸음” 셋으로 멈춤을 정직하게 모델에 넣었다. 부동소수는 증명 밖이다.

← 이전목차로다음 →