41 경계의 증명 — 구간, 관계, 행우선 주소

41.1 구간으로 계산한다#

컴파일러는 값 하나 대신 구간 [lo, hi] 로 계산해 넘침과 경계를 판정한다.

a ∈ [0, 100],  b ∈ [0, 100]
a + b ∈ [0, 200]        lo+lo, hi+hi
a − b ∈ [−100, 100]     lo−hi, hi−lo   뺄셈은 뒤집힌다 --- 흔한 실수 자리
a × b ∈ [0, 10000]      부호가 섞이면 네 곱의 최소·최대

module sum_contract .
rem run: small_sum 100 100
rem ir

fn small_sum input a u8 . input b u8 . output u16 .
  requires le a 100 .
  requires le b 100 .
do
  return add (widen u16 a) (widen u16 b) .
end

$ lowentc --run small_sum sum_contract.low 100 100
small_sum(100, 100) = 200
$ lowentc --ir sum_contract.low
-- runtime checks (interval analysis: overflow · division · narrowing) --
   2 / 2 removed  (100%)

계약이 두 입력을 100 이하로 묶었으므로 합은 200 을 넘지 않고 u16 에서 넘치지 않는다. 검사가 모두 사라진다. 같은 모양이라도 입력이 묶이지 않으면 검사가 남는다.

module product_bare .
rem run: product 1000 1000
rem ir

fn product input a u64 . input b u64 . output u64 .
do
  return mul a b .
end

$ lowentc --run product product_bare.low 1000 1000
product(1000, 1000) = 1000000
$ lowentc --ir product_bare.low
-- runtime checks (interval analysis: overflow · division · narrowing) --
   0 / 1 removed  (0%)

1000 × 1000 은 넘치지 않지만 분석은 a·b 가 어디까지 커질지 모른다. 그래서 검사를 남기고, 실제 값이 들어와서야 넘치지 않음을 확인한다.

정리들은 모두 한 방향이다. “안전하다고 말한 자리는 정말 안전하다.” 그 반대 — 안전한데 안전하다고 말하지 못함 — 는 정리가 보장하지 않는다. 그것은 성능 손해일 뿐이다.

분석이 넓게 잡음  →  검사가 남는다     →  느리다(안전)
분석이 좁게 잡음  →  검사가 사라진다   →  틀린 메모리 접근(위험)

그래서 규칙을 하나 더할 때마다 묻는 것은 늘 같다 — “이 규칙이 실제보다 좁게 잡을 수 있는가?”

41.2 관계 — 구간이 못 하는 것#

구간은 변수를 따로따로 본다. i ∈ [0, 100], n ∈ [0, 100] 을 알아도 i < n 인지는 모른다. 그런데 배열 안전에 필요한 사실이 바로 그것이다. 그래서 구간 옆에 한 칸짜리 관계를 둔다.

lenlt[i] = s     지역 i 는 len(지역 s) 보다 작다
lerel[i] = n     지역 i 는 지역 n 보다 작다

이 사실은 분기 조건에서 온다. while lt i n 의 몸 안에서는 i < n 이 참이고, 조건이 거짓인 갈래에서는 i ≥ n 이 참이다. 무거운 관계 영역 (팔각형·다면체) 대신 한 칸을 두는 까닭은 실제 코드의 모양 때문이다. 배열을 훑는 코드는 거의 언제나 while lt i (len s) 모양이고, 정교한 이론보다 실제 코드의 모양을 정확히 담는 쪽이 값이 크다.

사실을 다루는 규칙은 세 조각이다.

1. 얻기. 분기 조건이 참인 갈래에 그 조건을 사실로 기록해 둔다.
2. 나르기. 대입을 따라간다 — var x be j 에서 j < cap 이면 x < cap 이다. 합류에서는 두 경로가 같을 때만 살린다. 한쪽에서만 참인 것은 사실이 아니다.
3. 죽이기. 관련 변수가 바뀌면 그 사실을 양방향으로 죽인다. 슬라이스가 다시 묶이면 그 길이에 대한 사실이 전부 죽는다.

셋째가 안전의 핵이다. 사실을 오래 살려 두는 것이 곧 잘못된 검사 제거이므로, 죽이는 쪽이 늘 더 공격적이다.

41.3 네 단계#

경계 검사가 사라지는 모양을 세지는 순서로 늘어놓는다. --emit-proof 는 증명으로 지운 검사를 한 줄씩 적는다 — op 이름, 명령 위치, 연산, 쓴 규칙, 그리고 그 규칙이 쓴 범위다.

module bound_stages .
rem run: direct [1,2,3]
rem run: stored [1,2,3]
rem run: capacity [1,2,3,4] 3
rem run: grid [1,2,3,4] 2
rem proof

rem 1 --- 반복 조건이 len 을 직접 본다
fn direct input s slice u8 . output u64 . do
  var t u64 be 0 .
  var i u64 be 0 .
  while lt i (len s) . do
    set t (wrap_add t (widen u64 (index s i))) .
    set i (add i 1) .
  end
  return t .
end

rem 2 --- 길이를 지역에 담았다
fn stored input s slice u8 . output u64 . do
  let n u64 be len s .
  var t u64 be 0 .
  var i u64 be 0 .
  while lt i n . do
    set t (wrap_add t (widen u64 (index s i))) .
    set i (add i 1) .
  end
  return t .
end

rem 3 --- 계약이 용량을 말한다
fn capacity input s slice u8 . input cap u64 . output u64 .
  requires ge (len s) cap .
do
  var t u64 be 0 .
  var j u64 be 0 .
  while lt j cap . do
    set t (wrap_add t (widen u64 (index s j))) .
    set j (add j 1) .
  end
  return t .
end

rem 4 --- 행우선 주소 i·n + k
fn grid input a slice u8 . input n u64 . output u64 .
  requires le n 1000 .
  requires ge (len a) (mul n n) .
do
  var t u64 be 0 .
  var i u64 be 0 .
  while lt i n . do
    var k u64 be 0 .
    while lt k n . do
      set t (wrap_add t (widen u64 (index a (add (mul i n) k)))) .
      set k (add k 1) .
    end
    set i (add i 1) .
  end
  return t .
end

$ lowentc --run direct bound_stages.low [1,2,3]
direct([1,2,3]) = 6
  arg0 (written) = [1,2,3]
$ lowentc --run stored bound_stages.low [1,2,3]
stored([1,2,3]) = 6
  arg0 (written) = [1,2,3]
$ lowentc --run capacity bound_stages.low [1,2,3,4] 3
capacity([1,2,3,4], 3) = 6
  arg0 (written) = [1,2,3,4]
$ lowentc --run grid bound_stages.low [1,2,3,4] 2
grid([1,2,3,4], 2) = 10
  arg0 (written) = [1,2,3,4]
$ lowentc --emit-proof bound_stages.low
# proven 12 certified 12
direct 12 index R-IDX-LENLT 0 281474976710655
direct 18 add.i64 R-ADD-LENLT 0 281474976710655 1 1 64 0
stored 14 index R-IDX-LENLT 0 281474976710655
stored 20 add.i64 R-ADD-LEREL 0 281474976710655 1 1 64 0
capacity 16 index R-IDX-LENLT 0 281474976710655
capacity 22 add.i64 R-ADD-LEREL 0 281474976710655 1 1 64 0
grid 8 mul.i64 R-MUL-CAP 0 1000 0 1000 64 0
grid 29 mul.i64 R-MUL-CAP 0 999 0 1000 64 0
grid 31 add.i64 R-ROW-CAP 0 999000 0 999 64 0
grid 32 index R-IDX-ROWMAJOR 0 999999
grid 38 add.i64 R-ADD-LEREL 0 999 1 1 64 0
grid 43 add.i64 R-ADD-LEREL 0 999 1 1 64 0

• 1 · 직접. direct 는 반복 조건이 len s 를 직접 본다. index 가 R-IDX-LENLT 로 지워졌다.
• 2 · 지역에 담은 길이. stored 는 let n be len s 로 길이를 지역에 담았다. 아주 흔한 관용구다. 한때는 “이 값은 len s 다” 라는 사실이 스택 값의 속성이라 지역에 담는 순간 사라졌고, 이 루프의 검사가 남았다. 지역에도 그 사실을 싣도록 고친 뒤로 1 과 같이 지워진다. 이것은 안전성이 아니라 성능 수정이다 — 검사가 있었으므로 처음부터 안전했다.
• 3 · 계약의 용량. capacity 는 배열 크기와 반복 상한이 다른 변수다. j < cap(반복 조건)이고 len s ≥ cap(계약)이므로 j < len s 다.
• 4 · 행우선 주소. grid 는 index a (add (mul i n) k) 처럼 계산된 색인을 쓴다. 구간도 한 칸 관계도 곱을 다루지 못하지만 R-IDX-ROWMAJOR 로 지워졌다. 주소의 곱과 합도 R-MUL-CAP·R-ROW-CAP 으로 함께 증명되었다.

i 와 j 를 하나 올리는 덧셈이 R-ADD-LENLT·R-ADD-LEREL 로 함께 사라진 것도 같은 관계 덕분이다. i < n 이면 i + 1 ≤ n 이라 넘치지 않는다.

41.4 행우선 증명#

고등학교 수학이지만, 전제가 하나라도 빠지면 무너진다.

마지막 줄이 가장 미묘하다.

module grid_wrap .
rem run: grid [1,2,3,4] 2
rem proof

rem 같은 주소를 감기는 곱으로 계산했다
fn grid input a slice u8 . input n u64 . output u64 .
  requires le n 1000 .
  requires ge (len a) (mul n n) .
do
  var t u64 be 0 .
  var i u64 be 0 .
  while lt i n . do
    var k u64 be 0 .
    while lt k n . do
      set t (wrap_add t (widen u64 (index a (wrap_add (wrap_mul i n) k)))) .
      set k (add k 1) .
    end
    set i (add i 1) .
  end
  return t .
end

$ lowentc --run grid grid_wrap.low [1,2,3,4] 2
grid([1,2,3,4], 2) = 10
  arg0 (written) = [1,2,3,4]
$ lowentc --emit-proof grid_wrap.low
# proven 5 certified 5
grid 8 mul.i64 R-MUL-CAP 0 1000 0 1000 64 0
grid 29 mul.i64 R-ARITH-RANGE 0 999 0 1000 64 0
grid 31 add.i64 R-ARITH-RANGE 0 999000 0 999 64 0
grid 38 add.i64 R-ADD-LEREL 0 999 1 1 64 0
grid 43 add.i64 R-ADD-LEREL 0 999 1 1 64 0

같은 수식인데 index 줄이 없다. wrap_mul 은 넘칠 때 조용히 감긴다. 감긴 값은 작아질 수 있어서 i·q ≤ (p − 1)·q 라는 단계가 깨진다. 이 예제에서는 n ≤ 1000 이라 실제로 감기지 않지만, 규칙은 “멈추는 곱일 때” 에만 선다. 멈추는 연산이 아니면 사실이 아니다.

그러면 계약의 곱 p·q 자체가 넘치면? 계약의 곱은 멈추는 곱이고 계약 검사는 절대 지워지지 않으므로, 본문에 닿았다면 넘치지 않았다. 경계 검사를 없앤 자리의 유일한 방벽이 계약 검사다. 그래서 계약 검사는 모드로도 최적화로도 지워지지 않는다.

개발 저장소의 측정에서 이 규칙은 행렬 곱셈 벤치마크의 경계 검사를 6 개에서 1 개로 줄였고(남은 하나는 n ≥ 1 이 계약에 없는 index c 0 자리다), 계약이 용량을 말하는 LRU 벤치마크는 10 개에서 4 개로 줄였다.

41.5 증명을 신뢰하되, 신뢰를 검사로 받친다#

정리는 규칙이 옳다고 말하지만, 컴파일러가 그 규칙을 정확히 적용했는지는 따로 확인해야 한다. 장치가 둘이다.

분석 자기 고발. VM 은 검사를 지우지 않는다. 컴파일러가 “지워도 된다” 고 표시한 자리를 실행해 보고, 실제로 범위를 벗어나면 그 자리에서 E-VM-ANALYSIS: … the interval/relational analysis is UNSOUND (this is a compiler bug) 로 컴파일러를 고발한다. 네이티브 빌드에는 검사가 없어 빠르고, VM 에는 검사가 있어 표시가 거짓이면 알려 주며, 두 백엔드 대조가 둘을 같은 입력으로 돌린다. 이 장치가 실제로 일한 적이 있다. 행우선 규칙을 넣으면서 requires ge (len a) (mul n n) 을 검사되는 계약으로 믿었는데, 처리기가 그 모양의 계약을 읽지 못해 실제로는 검사가 없었고, 바로 이 진단이 떴다. 믿을 것은 검사되는 것뿐이다.

증명서 검산. --emit-proof 의 줄 끝 숫자가 그 근거다. 컴파일러는 검사를 지운 자리마다 산술 근거(Farkas 증명서)를 남기고, 컴파일러와 따로 짠 검산기가 그 산술을 다시 계산한다. 첫 줄의 certified 수가 검산을 통과한 수다. 검산기 가운데 하나는 규칙의 건전성을 증명한 Coq 코드에서 OCaml 로 추출한 것이다(LowentCert.v·LowentCertExtract.v). 사람이 옮긴 검산기는 “이 산술을 옳게 옮겼나” 를 아무도 확인하지 않지만, 추출본은 정리가 말하는 함수 그 자체다. 다만 이것은 규칙의 산술을 믿을 만하게 할 뿐, “그 자리에 그 사실이 정말 성립하는가” 는 검산기의 관할 밖이다.

41.6 증명하지 않은 것#

계약을 붙여도 빠지지 않는 검사가 남는다. 측정한 자리들이다.

• 위드닝은 정보를 버린다. 고정점에 빨리 닿으려고 넓게 잡으므로 안전한 자리에서도 검사가 남는다(39장의 count_up). 손해이지 위험이 아니다.
• 배열 내용에 대한 사실은 이 영역에 자리가 없다. “모든 원소가 10 보다 작다” 는 어떤 requires 로도 닫히지 않는다. 도구의 한계이지 프로그램의 결함이 아니고, 검사가 남으므로 답은 여전히 옳다.
• 부동소수 구간은 다루지 않는다.
• 분석 규칙과 정리 사이의 대응은 경험적이다. 자기 고발·증명서 검산·두 백엔드 대조가 받친다(50장).