38 왜 증명하는가

38.1 시험은 있음을, 증명은 없음을#

module average .
rem run: mean2 10 20
rem trap: mean2 4294967295 1
rem test

fn mean2 input a u32 . input b u32 . output u32 .
do
  return div (add a b) 2 .
end

test small_numbers
do
  expect eq (mean2 10 20) 15 .
  expect eq (mean2 0 0) 0 .
  expect eq (mean2 1000000 3000000) 2000000 .
end

$ lowentc --run mean2 average.low 10 20
mean2(10, 20) = 15
$ lowentc --run mean2 average.low 4294967295 1
== ir diagnostics (1) ==
0:0 E-VM-OVERFLOW: integer overflow at the declared width (use wrap_*/sat_*, or prove the range)
$ lowentc --test average.low
  [PASS] small_numbers
== tests: 1 run, 1 passed, 0 FAILED ==

두 수의 평균을 구하는 mean2 는 시험 세 개를 모두 통과한다. 그런데 4294967295 와 1 을 주면 add a b 가 u32 에서 넘쳐 멈춘다. 시험을 백만 개 더 써도 저자가 큰 수를 고르지 않으면 이 결함은 드러나지 않는다.

이것이 시험의 본성이다. 시험은 “이 입력에서 틀린다(∃)” 를 보일 수 있지만 “어떤 입력에서도 틀리지 않는다(∀)” 를 보일 수 없다. 자연수를 백만 개 확인해도 모든 자연수를 확인한 것이 아니다. ∃ 를 아무리 모아도 ∀ 가 되지 않는다. 이 간극이 증명이 필요한 유일한 이유다.

 mean2 의 입력: u32 두 개 = 약 1.8 × 10^19 쌍

 시험   (10,20) (0,0) (10^6,3·10^6)   세 점을 찍었다 → 셋 다 맞다
 반례   (4294967295, 1)               찍지 않은 자리 → 넘쳐 멈춘다
 증명   ─── 모든 쌍 ───────────       한 번에 모두에 대해 말한다

Lowent 에서 이 결함은 적어도 조용하지는 않다. C 였다면 넘친 합이 감겨 틀린 평균을 냈을 것이다. 여기서는 멈춘다(4장). 그리고 고친 판은 넘칠 수 없는 모양으로 적는다.

module average_fixed .
rem run: mean2 4294967295 1
rem ir

fn mean2 input a u32 . input b u32 . output u32 .
do
  let lo u32 be min a b .
  let hi u32 be max a b .
  return add lo (div (sub hi lo) 2) .
end

$ lowentc --run mean2 average_fixed.low 4294967295 1
mean2(4294967295, 1) = 2147483648
$ lowentc --ir average_fixed.low
-- runtime checks (interval analysis: overflow · division · narrowing) --
   1 / 3 removed  (33%)

작은 쪽에 두 수 차이의 절반을 더하면 넘칠 수 없다. --ir 은 세 검사 가운데 하나를 지웠다고 말한다. 남은 두 검사가 실제로 넘칠 수 없는데도 남는 것은 구간 분석이 min·max 의 관계를 모르기 때문이다. 분석은 안전한 방향으로만 틀린다 — 증명하지 못하면 검사를 남긴다.

38.2 세 층을 겹친다#

셋이 다른 종류의 실수를 잡기 때문에 겹쳐 쓴다. 누가 무엇을 맞대는지 그리면 이렇다.

 명세의 규칙 ── 옮긴다 ──▶ Coq 모델 ── 증명 ──▶ 모델 안의 모든 경우
                              ▲
                              │  전수 검사: 작은 크기에서 모델과 구현을 맞댄다
                              ▼
 컴파일러 ─┬─ VM 으로 돌린다 ──┐
           └─ C 로 내보낸다 ───┴─▶ 대조: 두 답이 다르면 컴파일러 결함

증명은 모델을, 대조는 구현을 보고, 전수 검사는 그 둘 사이를 잇는다. 이 저장소에서는 증명이 못 잡은 결함을 대조가 잡았고, 대조가 못 잡은 결함을 증명이 잡았다. 그리고 이 부는 세 낱말을 섞지 않는다. “증명됨” 은 Coq 이 모든 경우를 확인했다는 뜻이고, “전수 검사됨” 은 정해진 크기의 모든 경우를 돌렸다는 뜻이며, “스케치” 는 사람이 논증했을 뿐 기계가 확인하지 않았다는 뜻이다.

38.3 무엇이 증명되어 있나#

증명 파일은 모두 docs/proofs/coq/ 에 있다. 이 판에서 센 규모다.

Coq 에서 Admitted 는 “이건 참이라고 치고 넘어간다” 이고 Axiom 은 “이건 가정한다” 다. 그런 자리가 하나라도 있으면 그 파일의 모든 정리가 그 가정에 기댄다. 둘 다 0 이다. 무엇을 증명했고 무엇을 아직 안 했는지는 docs/proofs/LEDGER.md 에 적혀 있다.

묶음으로 보면 이렇다.

마지막 장(50장)은 이 모두가 기대는 것과 덮지 않는 것을 모은다.

38.4 증명하는 세 가지 방법#

증명 스크립트를 읽을 필요는 없다. 그러나 어떤 방식으로 증명했는지 알면 그 정리를 얼마나 믿어야 하는지 감이 온다.

불변식 보존. “프로그램이 한 걸음 갈 때마다 어떤 성질이 유지된다” 를 보인다. 시작에서 참이고(기초) 한 걸음이 참을 참으로 넘기면(보존), 몇 걸음을 가도 참이다. 수학적 귀납법의 프로그램 판이다. 차용 규칙과 반복의 정리가 이 방식이다.

순서 구조로 환원. 문제를 어떤 순서에 관한 문제로 바꾼 뒤 순서의 성질로 답한다. “u8 은 u32 에 안전하게 들어간다” 를 부분 순서로 만들면, “두 타입을 합칠 때 무엇을 골라야 하나” 가 최소 상계라는 잘 알려진 개념이 된다. 수의 넓히기와 약한 메모리 모델이 이 방식이다.

전수 검사. 아직 모든 크기에 대해 증명하지 못한 성질은 크기를 정해 그 안의 모든 경우를 돌린다. 이것은 증명이 아니고, 이 부는 그렇게 적는다.

38.5 이 부를 읽는 약속#

이 부는 세 가지를 지킨다.

• 낱말을 섞지 않는다. “증명됨”·“전수 검사됨”·“스케치” 는 서로 다른 세기다. “이 언어는 증명됐다” 가 사실은 “짧은 경우들을 돌려 봤다” 인 경우가 흔하다.
• 정리마다 막는 결함이 붙는다. 무엇을 막는지 적을 수 없는 정리는 싣지 않았다. 읽는 사람에게 값이 없는 정리는 여기서 다룰 까닭이 없다.
• 이 부는 규범이 아니다. 언어의 정의는 명세의 조항 정본이다. 이 부와 명세가 어긋나면 이 부가 틀렸다.

그리고 이 언어가 기대는 생각을 여섯 줄로 줄이면 이렇다. 여섯 모두 수학으로 뒷받침되거나, 뒷받침되지 않는다고 적혀 있다 — 그 구별이 이 부의 목적이다.

1. 틀린 프로그램은 쓸 수 없게 만든다. 틀린 것을 잡는 것보다 표현할 수 없게 하는 쪽이 싸다(42장).
2. 모르는 것은 모른다고 답한다. 실패는 option·result 라는 값이지 숨은 예외가 아니다.
3. 비용은 보여야 한다. 할당·곁효과·복사가 모두 소스에 적힌다(44장).
4. 의심스러우면 검사를 남긴다. 검사를 지우는 것은 증명이 있을 때뿐이다(41장).
5. 두 구현이 같은 답을 내야 한다. VM 과 네이티브가 다르면 컴파일러 결함이다(31장).
6. 못 한 것은 적는다. 가정·한계·미증명을 남긴다(50장).

 정리 ─────────────▶ 컴파일러가 거절할 모양을 정한다
                     예: uN ⊑ iM 의 조건은 N < M (엄격)
 구현이 겪은 결함 ─▶ 정리로 옮긴다
                     예: 차용을 함수로 세탁하기
                     그 검사를 지우면 증명이 깨진다