49 해시의 증명 — 이름이 아니라 내용으로 부르기

49.1 해시 함수와 Merkle DAG#

해시 함수 BLAKE3-256 은 임의 길이의 바이트를 32 바이트로 줄인다. 필요한 성질은 하나다 — 다른 입력이 같은 출력을 내는 짝을 찾을 수 없다(충돌 저항). 그래서 “해시가 같다” 를 “내용이 같다” 로 써도 된다. 이것은 수학적으로 증명된 것이 아니라 가정이고 신뢰 기반에 들어간다(50장). 그래도 실용적으로는 다른 어떤 가정보다 튼튼하다.

49.2 이름이 아니라 내용으로 부른다#

보통의 빌드 시스템은 파일 이름과 수정 시각으로 캐시를 판단한다. 그래서 파일을 만졌지만 내용이 같으면 쓸데없이 다시 짓고(손해), 내용이 바뀌었는데 시각이 같으면 낡은 결과를 쓴다(위험). 내용 주소화는 이름을 버리고 내용의 해시로 부른다. lowentc --emit-db 가 op 마다 해시 둘을 낸다 — iface 는 밖에서 관찰 가능한 표면(서명과 계약), def 는 정의 전체다. 해시 함수는 BLAKE3-256 이다.

해시는 의존을 그들의 해시로 품는다. 그러면 어떤 정의의 해시는 그것이 의존하는 모든 것의 내용을 반영하고, 깊은 곳의 op 하나가 바뀌면 위쪽 해시가 따라 바뀐다. 해시 자체가 의존 추적이다. 이것이 Merkle DAG 다.

서로를 부르는 op 은 순환을 만든다. hash(A) 가 hash(B) 를 담고 hash(B) 가 hash(A) 를 담으면 정의가 돈다. 그래서 순환하는 것들을 한 덩어리 (강결합 요소, SCC)로 묶는다. 이름 없는 예비 해시로 덩어리 안의 정규 차례를 정하고, 덩어리 안의 호출은 이름 대신 그 차례의 번호를 담고, 덩어리를 한 번 해싱한 뒤, 구성원마다 (덩어리 해시, 자기 번호)를 해시로 준다. 강결합 요소로 줄이면 남는 것은 순환 없는 그래프다 — 39장의 고정점과 같은 발상이 또 나왔다.

 A ⇄ B (서로 부른다)      C ──▶ A

 1  {A, B} 를 한 덩어리(SCC)로 묶는다
 2  이름 없는 예비 해시로 덩어리 안의 차례를 정한다      A = 0 · B = 1
 3  덩어리 안의 호출은 이름 대신 번호를 담는다           A 가 B 를 부름 → «1 번»
 4  덩어리를 한 번 해싱한다                              → H
 5  구성원마다 (H, 번호) 를 해싱한다                     hash(A) = h(H, 0) · hash(B) = h(H, 1)
    C 는 hash(A) 를 담는다 — 남은 그래프에는 순환이 없다

49.3 무엇이 해시를 바꾸고 무엇이 안 바꾸나#

module hashed .
rem db

export fn twice input a u64 . output u64 .
do
  return add a a .
end

$ lowentc --emit-db h1_plain.low
fn twice/1 iface:6630705cb68be394 def:73e3a88345444202

module hashed .
rem db

rem 주석을 넣어도 해시는 그대로다
export fn twice input a u64 . output u64 .
do
  rem 여기도 주석
  return add a a .
end

$ lowentc --emit-db h1_comment.low
fn twice/1 iface:6630705cb68be394 def:73e3a88345444202

H1 — 주석은 아무것도 바꾸지 않는다. 두 해시가 모두 같다. 주석을 고쳤다고 프로젝트 전체가 다시 지어지지 않는다. 그리고 “같은 프로그램” 의 정의가 바이트가 아니라 뜻이라는 것을 기계가 지킨다.

module hashed .
rem db

export fn twice input a u64 . output u64 .
do
  return mul a 2 .
end

$ lowentc --emit-db h2_body.low
fn twice/1 iface:6630705cb68be394 def:64a7865b02486293

H2 — 본문만 바뀌면 def 만 바뀐다. add a a 를 mul a 2 로 바꾸자 iface 는 그대로이고 def 만 바뀌었다. 이것이 증분 빌드의 심장이다. 어떤 op 의 본문만 바뀌면 그 op 을 쓰는 쪽은 다시 컴파일하되 그 쪽의 iface 도 그대로이므로, 그다음 의존자는 캐시에 적중한다. 서명이 바뀌면 사슬을 따라 번지고, 본문만 바뀌면 한 단계에서 멈춘다.

 main ──부른다──▶ util ──부른다──▶ leaf        leaf 의 본문만 바꿨다

 leaf   def 바뀜 · iface 그대로
 util   다시 컴파일한다 · 그 iface 도 그대로
 main   캐시 적중 — 여기서 멈춘다

module hashed .
rem db

proc greet input out cap io . input al cap allocator . output u64 . effects io alloc .
do
  let g option mut slice u8 be alloc_bytes al capacity 4 .
  return write_out out 1 "hi" .
end

$ lowentc --emit-db h3_effects_a.low
proc greet/2 iface:d864e930303f7437 def:bebc1fcf6231d282

module hashed .
rem db

proc greet input out cap io . input al cap allocator . output u64 . effects alloc io .
do
  let g option mut slice u8 be alloc_bytes al capacity 4 .
  return write_out out 1 "hi" .
end

$ lowentc --emit-db h3_effects_b.low
proc greet/2 iface:d864e930303f7437 def:bebc1fcf6231d282

H3 — 효과는 집합이다. effects io alloc 과 effects alloc io 가 같은 해시를 낸다. 한때는 달랐다. 절의 원문을 해싱했기 때문이다. 그러면 내용 주소화가 뜻이 아니라 철자를 주소화한 것이 된다. 효과는 문법이 집합이라고 말하므로 정규화된 차례로 해싱한다.

module hashed .
rem db

export fn twice input a u64 . output u64 .
  requires le a 100 .
do
  return add a a .
end

$ lowentc --emit-db h4_contract.low
fn twice/1 iface:31247d9015a6c804 def:a088ec347ad280ef

계약도 표면이다. requires le a 100 . 을 붙이자 iface 가 바뀌었다. 부르는 쪽은 부르는 op 의 계약을 믿고 검사하며, 41장에서 보았듯 경계 검사를 지우는 근거가 계약이다. 계약이 바뀌었는데 해시가 같으면 캐시가 옛 계약을 믿은 결과를 그대로 쓰게 된다 — 전제가 바뀌었는데 증명을 재사용하는 셈이다. 한때 구현이 서명만 해싱해서 이 구멍이 있었고, 고쳤다.

49.4 증명할 수 있는 것과 없는 것#

LowentHash.v 는 둘을 정확히 가른다. BLAKE3 의 충돌 저항성은 암호 가정이라 증명 대상이 아니다. 증명할 수 있는 것은 그 앞, 곧 정규 인코딩이 무엇을 지우고 무엇을 남기느냐다.

계약 절은 효과와 달리 정규화하지 않고 적힌 차례로 해싱한다. 그래서 requires A . requires B . 와 requires B . requires A . 는 뜻이 같은데 해시가 다르다. 부정확하다. 그런데 안전한 방향이다. 같은 뜻이 다른 해시를 내면 재빌드가 한 번 더 돌 뿐이지만, 다른 뜻이 같은 해시를 내면 캐시가 거짓말을 한다. 이 방향이 안전하다는 것도 증명되어 있다. 구간 분석(41장)과 차용 검사(42장)에서 본 비대칭 — 모르면 넓게 잡는다 — 이 여기서도 판단을 정했다.

49.5 해시가 막는 것#

뒤의 두 줄이 재현 가능한 빌드의 근거다. “같은 소스가 같은 결과를 낸다” 를 비교할 수 있는 형태로 만든 것이 내용 주소화의 값이다 — 믿는 것이 아니라 비교하는 것이 된다.

49.6 증명하지 않은 것#

• 정리는 모델 위의 것이다. LowentHash.v 는 정규 인코딩에 대해 H1·H2·H3 을 증명했다. 실제 구현이 그 인코딩을 쓰는지는 시험이 몇 개의 예에서 확인한다.
• 정규화가 완전하지 않다. 계약 절의 차례에 민감하고, 지역 변수 이름이나 수 리터럴의 표기(0x10 대 16)가 어디까지 정규화되는지 전수 확인하지 않았다.
• BLAKE3 의 충돌 저항성은 가정이다. 틀리면 캐시가 다른 내용을 같다고 본다.
• 덩어리(SCC) 해시가 여러 구현에서 같게 나온다는 것은 명세 수준의 약속이고 확정되지 않았다. 순환을 다루는 방법은 여럿이다.
• 시험이 지키는 것은 해시의 값이 아니라 같다·다르다의 관계다. 인코딩이 바뀌면 값은 바뀌지만 관계는 그대로여야 한다.