# 029 — 증명이 곧 컴파일러이고, 커밋이 곧 복제본이다

작성일: 2026-10-19. 상태: **설계 초안 2판**. 1판(기법 다섯의 나열)은 바깥 피드백 008로 반려했다. 코드는 아직 없다. 이 판은
원리 둘과 열린 질문 하나, 그리고 원리마다 그것을 깰 수 있는 실험 하나만 적는다.

**원리 1은 UAX #14에서 깨졌다(2026-10-19, 045).** 두 실험 모두 막대에 못 미쳤다. (가) 2.19배(막대 4배), (나) 1.31배(막대
3배). 아래 "깨는 실험의 결과"에 무엇을 시험했고 무엇은 시험하지 않았는지 적는다. 원리 2는 아직 시험하지 않았다.

## 쉬운 말로

pure link는 전송 세션이 들고 있던 것(순번, 확인, 다시 보내기)을 앱의 outbox와 heard가 이미 들고 있음을 알아보고 세션을
지웠다. 단일 싱크 트리는 WAL이 들고 있던 것(바뀐 것과 그 순서)을 트리의 새 노드가 이미 들고 있음을 알아보고 WAL을 지웠다.
같은 질문을 남은 결함에 던진다. **어느 두 계층이 같은 정보를 들고 있는가, 그리고 어느 쪽을 지울 수 있는가.**

- **원리 1.** 검증기가 증명한 것을 실행기 셋이 다시 알아내거나 버린다. 증명을 버리지 않으면 실행기 셋이 사라진다.
  **깨졌다(045).** 해석은 절벽의 작은 몫이었다.
- **원리 2.** 복제 프로토콜이 들고 다닐 것을 저장소의 커밋과 링크가 이미 들고 있다. 복제 계층이 사라진다.

## 원리 1. 증명이 곧 컴파일러다

**사실.** 140의 느린 명세 다섯(DNS, HTTP, inflate, JSON 트리, UAX #14)은 모두 `runner 2`다. fn이 있으면 블록 전체가 실행기로
가고, 기계어는 만들어지지 않는다. UAX #14는 코드 포인트 하나에 6,445 ns, C는 35 ns다.
- 정정(045). 이 자리에 처음 적은 "코드 포인트당 명령 1,774개, 명령 하나에 3.2–3.9 ns"는 일의 예산이 센 수였다. 예산은 블록을 쓰인
  대로 센다. 실행기가 실제로 도는 명령은 코드 포인트당 549.9개이고, 하나에 약 11.7 ns, 기계 명령 74개다.

**같은 정보를 든 두 계층.** 검증기는 모듈을 받을 때 모든 자리에서 다음을 증명한다.
- 스택의 높이와 각 칸의 타입. 높이가 정적이라 스택의 칸마다 이름 붙은 값으로 바꿀 수 있다.
- 반복마다 시작할 때의 횟수 상한.
- fn마다 그것이 바꾸는 상태의 집합. 그 밖의 읽기는 그 부름을 건너 변하지 않는다.
- 리스트는 서로 다른 상태이고 값은 바뀌지 않으므로, 두 리스트가 같은 메모리를 가리키지 않는다(별칭 없음).

그리고 그 증명을 버린다. 실행기는 명령마다 다시 풀고 다시 검사한다. 묶음 실행기는 로드 때 고리의 모양을 다시 분석한다. 기계어
계층은 몇 가지 꼴에만, 한 명령어 집합(AArch64)에서만 따로 SSA를 짓는다.

**뒤집힘.** C 컴파일러는 이 사실들을 추측해야 한다. 포인터의 별칭과 부름의 부작용을 모르므로 부름을 건너 필드 읽기를 하나로
합치지 못하고, 모르는 쓰기 너머로 경계 검사를 끌어올리지 못한다. Pure는 그것을 증명해 둔 채로 받는다. 그러니 **검증된 aup는 C보다
C의 속도로 컴파일하기 쉬운 쪽**이어야 한다. 61–183배의 절벽은 계층이 모자라서가 아니라, 증명을 버리고 해석하는 값이다.

**지우는 것과 남기는 것.**
- 지운다: 실행 길로서의 실행기 분기(명령마다의 해석), 묶음 실행기의 레인(`module-batch.c` 3,405줄), 손으로 쓴 AArch64 기계어
  계층(`module-jit.c` 5,878줄).
- 남긴다: 검증기의 사실을 그대로 내보내는 한 번의 지나감. 내보내는 조각은 실행기의 명령 몸을 시스템 C 컴파일러가 Pure를 지을 때
  컴파일한 것이고, 그것을 이어 붙인다. 그래서 명령어 집합마다의 뒤끝이 없고, 뜻은 말 그대로 같은 소스다. 실행기는 실행 길이 아니라
  참조로만 남아 검사가 견준다.
- 이것은 일반 JIT를 짓는 것이 아니다(008). 손으로 쓴 기계어 계층을 지우는 것이다(006).

**두 인자.** 격차는 (명령 수) × (명령당 시간)이다.
- 명령당 시간은 해석을 지우면 준다.
- 명령 수는 증명이 허락하는 합치기가 줄인다. 140의 "경계마다 decide 1,150개"는 규칙 마흔 개가 `t.cls[i]`, `t.eff[i]`를 저마다
  레지스터에 다시 묶고 다시 읽는 값이다. 그 읽기는 검증기가 이미 바뀌지 않음을 증명했다. 증명을 받은 컴파일러만 그것을 안전하게
  하나로 합칠 수 있다.

**깨는 실험(내보내는 코드를 쓰기 전에).** UAX #14에서 두 인자를 따로 잰다.
- (가) 증명이 허락하는 합치기를 손으로 적용하고 명령을 센다. 통과: 4배 이상 준다.
- (나) 블록 하나(`decide`)를 해석 없이 명령 몸을 이어 붙여 돌리고 잰다. 통과: 명령당 시간이 3배 이상 준다.
- 하나라도 못 미치면 이 원리는 이 일에 틀렸고, 그렇게 적는다. 둘 다 지나면 둘만으로 12배다(6,445 → 540 ns 아래, C의 약 15배).
- 그다음 남는 것(리스트의 열을 레지스터에 두기)을 잰다. C의 1–3배는 시험할 주장이지 약속이 아니다.

**깨는 실험의 결과(2026-10-19, `research/experiments/045-proof-compiler`).** 둘 다 못 미쳤다. 이 원리는 이 일에 틀렸다.
- 기준. 같은 줄 18,672개(코드 포인트 61,285개)에서 C(Vega의 `text/linebreak.c`)는 코드 포인트당 기계 명령 220개, 사이클 82다.
  Pure의 실행기는 40,703개, 15,566이다. 둘 다 줄마다의 답이 기대와 같은지 먼저 확인했다.
- **(가) 명령 수: 2.19배, 막대 4배.** 실행기가 도는 명령을 opcode마다 셌다(`ops-count.patch`). 코드 포인트당 549.9개 가운데
  레지스터가 지울 옮김(LOCAL_LOAD, LOCAL_STORE, 스택의 PICK과 SLIDE)이 205.5, 상수가 76.7, 한 사건 안에서 같은 리스트·판·필드·자리를
  다시 읽는 것이 16.4다. 셋을 모두 지워도 251.3이 남는다.
  - 전제가 틀렸다. "규칙 마흔 개가 `t.cls[i]`를 저마다 다시 읽는다"고 적었지만, 소스는 그 읽기를 이미 지역에 담는다. 증명만이
    허락하는 합치기는 16.4개(3%)다.
- **(나) 명령당 시간: 1.31배, 막대 3배.** 실행기의 `step()`을 상수 명령마다 불러 C 컴파일러가 명령마다 몸을 특수화하게 하고,
  기본 블록마다 함수 하나로 이어 붙였다(`stitch.c`, `native-hook.patch`). 기계 명령 40,703 → 28,601, 사이클
  15,566 → 11,850이다.
  - 답. 처음의 `cost.c`는 C의 답만 기대와 견주고 Pure의 답은 읽지 않았다. 고쳐서 Pure의 답을 보기 `boundaries`에서 읽고(틀린 변형은
    0줄로 거부한다), 이어 붙인 판을 다시 지어 돌렸다. 둘 다 18,672줄이 모두 맞고, 수는 40,189 → 28,089(1.43배), 사이클 1.32배로
    같다.
  - 시험한 것: 해석(가져오기, 풀기, 갈래)을 지우는 것. `Frame`과 칸은 메모리에 있고, 실행 중의 검사는 그대로다. C 컴파일러는
    증명을 받지 않았다.
  - 이 길은 위가 막혀 있다. 실행된 명령 하나의 기계 명령 74개 가운데 해석이 22개다. 이어 붙이기를 아무리 잘해도 1.42배다. 그래서
    "새 뒤끝 없이 실행기의 몸을 이어 붙인다"는 이 원리의 길은 이 일에서 죽었다.
  - 시험하지 않은 것: 증명을 받는 내보내기(칸을 레지스터에, 검사를 지움). 그것은 다른 주장이고 아직 시험하지 않았다. 008의 과제 A가
    바로 그것을 묻는다(증명을 쥐고 왜 실행 중에 분배하는가, 모든 일에 실행의 원리 하나). 008이 금한 것은 실행기의 분열과 흔한 기법의
    축소 복사이지, 증명에서의 컴파일이 아니다. 처음 이 자리에 "008이 금한 일반 JIT"라고 적은 것은 틀렸다.
- **명령이 가는 곳.** 해석이 아니라 런타임의 기계다.
  - 앱을 줄인 변형(`events.c`, `variants`)의 코드 포인트당 기계 명령: 빈 처리기 1,583, 위치마다의 리스트를 지으면 22,651이 더,
    `Text` 레코드 2,951, `decide` 12,988.
  - 연산 하나의 기계 명령(`unit.c`, `units`): 블록 fn의 부름 1,375, 저장 리스트의 자리 읽기 331, 실행기의 산술 고리 한 바퀴
    248(묶음 실행기는 35).
  - 마지막 수는 따로 적는다. 묶음 실행기가 이미 7배를 내는데, 블록 어디에든 fn이 있으면 블록 전체가 실행기로 가서 그것을 잃는다.
    이 원리는 묶음 실행기를 지우자고 했다. 다음 가설은 이 7배를 다시 셈하거나 버린다고 말해야 한다.
- **메커니즘마다(`where.c`, `where.py`).** 사용자 모드의 기계 명령 100,003개마다 주소를 표본으로 받고(표본 246,581개, 답은 먼저
  확인), 인라인된 함수의 사슬로 `step()`의 어느 명령 몸인지, 밖이면 어느 함수인지를 가렸다. 코드 포인트당 40,236개:
  | 메커니즘 | 기계 명령 | 몫 | 실행된 명령 하나에 |
  |---|---|---|---|
  | 분배(switch, `run_calls`의 고리) | 12,298 | 30.6% | 22 |
  | 리스트 짓기(append, 복사, 판, 지우기) | 6,953 | 17.3% | 13 |
  | 수(산술, 비교, `//`의 `fmod`) | 5,416 | 13.5% | 10 |
  | 리스트 읽기(트리 내려가기, 칸) | 5,238 | 13.0% | 10 |
  | 옮김(지역, 상수, 스택) | 3,601 | 9.0% | 6.5 |
  | 부름(들어가기, 나오기, 리스트 바꿔 끼우기) | 2,847 | 7.1% | 5 |
  | malloc과 free | 1,609 | 4.0% | 3 |
  | 사건, 고리, 가리지 못한 것 | 2,273 | 5.6% | 4 |
  - **어느 계층도 절벽의 대부분을 들지 않는다.** 일반적인 계층 셋(해석, 리스트의 표현, 수의 표현)이 저마다 지워져도 1.4–1.5배다.
    절벽은 그 곱이다.
  - range()의 이분 탐색 하나가 코드 포인트당 14,489개, 36%다(변형 v0r). 반복은 11.4번, 한 번에 약 1,270개다. 그 안에서 `//`가
    186(`fmod`로 정확히 내린다), 저장 리스트의 읽기가 240이다. Vega의 C는 종류를 두 단계 표에서 한 번에 읽는다. 비교는 그대로
    서지만, 저장 리스트 읽기의 몫은 앱이 고른 알고리즘 때문에 크다.
- **깨진 후보 하나(셈으로, 코드 전에).** "let 리스트는 프레임에서 나고 죽으며 별칭이 없는데, 런타임은 그것을 판이 있는 상태로
  만들어 부를 때마다 바꿔 끼운다. 프레임이 이미 든 수명을 상태 계층이 다시 든다." 지울 수 있는 몫을 모두 더해도(리스트 짓기 6,953,
  let 리스트의 읽기 약 2,500, 부름 약 2,500, 메모리 약 1,500) 약 13,000, 32%다. 값 없이 지워도 1.5배다. 절벽을 들지 못하니 깨졌다.
- **막대의 셈.** 실행된 명령은 549.9개, C는 기계 명령 220개다. 명령 하나가 기계 명령 하나여도 C의 2.5배다. (가)의 지움 뒤 251개를
  하나에 3개쯤으로 내면 약 750, C의 3.4배다. 그래서 UAX #14에서 "C의 1–3배"는 실행만으로 닿지 않는다. 명령의 수도 줄어야 하고,
  550 가운데 269.5가 Vega의 C가 하지 않는 이분 탐색이다(변형 v0r에서 셈, `2026-10-19-ops-v0r.txt`). 이분 탐색의 명령 하나는 기계
  명령 54개, 나머지 앱의 명령 하나는 92개다.

## 원리 2. 커밋이 곧 복제본이다

**같은 정보를 든 두 계층.** 복제 프로토콜은 넷을 들고 다닌다: 상태 변경의 기록을 순서대로, 그 기록의 무결성 검사, 복제본에
내구성 있게 닿았다는 확인, 잃은 것의 다시 보내기. 넷 모두 이미 있다.
- 저장 한 번이 쓰는 것은 모두 스스로 경계를 갖고 스스로 검증하는 구간이다. 트리의 커밋은 128 B 레코드(순번, 끝, 카탈로그,
  바이트의 시작과 다이제스트)와 그 뒤의 노드이고(076, 081), 리스트의 로그는 앞 항목의 다이제스트로 이어진 기록이다.
- pure link는 번호 붙은 레코드를 순서대로 한 번 옮긴다. 받는 쪽의 heard가 덮을 때까지 보내는 쪽이 내구성 있게 들고 있고, 어느
  쪽을 kill -9 해도 잃거나 겹치지 않는다.

**지우는 것.** 복제 계층이다. 로그의 형식도, 적용 고리도, 그것만의 확인도 없다. 저장 한 번이 쓴 구간을 링크의 레코드로 보내고,
따르는 노드는 각 구간을 같은 자리에 쓴다. heard가 내구성의 확인이다. 따르는 노드의 파일은 주인의 파일과 바이트까지 같다.
- 주인이 죽으면 따르는 노드가 그 파일을 주인으로 연다.
- RPO는 heard가 덮은 데까지다. 손님에게 답하기를 heard 뒤로 미루면(동기) 확인한 사건은 잃지 않는다.

**이 원리 안에서 확인할 것.** 주인의 차례 밖에서 쓰이는 것이 있다: 체크포인트 이미지(쓰는 스레드가 제때 쓴다), 새 파일을
설치하는 압축, 미리 0을 써 둔 꼬리. 이것들도 구간이거나 파일의 연산이니 레코드로 보내야 한다. 그렇지 않으면 결정적으로 만든다.
첫 실증이 그것을 드러낸다.

**깨는 실험.**
- 한 Pi 위의 두 호스트(Mac과 WSL2는 지금 닿지 않는다). 주인이 사건 10만 개를 받는 동안 따르는 노드가 보낸 구간을 쓴다.
- 저장 시점을 골라 저장소의 모든 파일을 `cmp`로 견준다.
- 주인을 kill -9하고, 따르는 노드의 저장소를 주인으로 연다.
- 통과: 고른 모든 시점에 파일이 같고, heard가 덮은 저장의 사건이 모두 있다.

**미룬 것.** 둘이 동시에 주인이 되지 않게, 어느 노드가 파일을 주인으로 열지 정하는 합의의 규칙이 필요하다. 여기서 설계하지
않는다. 실험이 지난 뒤의 다음 결정이다.

## 열린 질문: 스키마의 진화

같은 항목을 두 모양으로 든다. 지금은 레코드의 모양이 바뀌면 목록을 새 모양으로 다시 써서(100만 항목에 172 ms 막음) 그동안 옛
모양과 새 모양이 함께 있다. 지울 후보는 "트리에는 한 모양만, 투영은 읽을 때"다. 잎은 그것을 쓴 모듈의 판을 갖고, 새 모듈로 읽을
때 이관 fn을 거치며, 쓸 때 새 모양으로 쓴다.

재지 않은 것이 둘 있다. 읽을 때마다 투영하는 값이 얼마인지 모르고, 잎은 열의 꼴이라(090) 항목마다의 fn과 부딪친다. 그래서
설계가 아니라 질문으로 둔다. 재는 것: 100만 항목의 `items-wide`에서, 읽을 때 투영하며 전체를 접는 값과 옮긴 뒤 접는 값을 견준다.

## 이미 같은 경계: 효과와 화면

- **효과.** 바깥으로는 보냄이 나가고, 결과는 입력으로 들어온다. 링크가 들어오고 보기가 나가는 같은 경계다. 모자란 것은 원리가
  아니라 뒤끝(HTTP 부름, 파일)이다.
- **화면.** Vega는 보기를 읽는다. 모자란 것은 배치와 표면(네이티브 창, IME)의 뒤끝과 보기의 타입 하나다. 보기에서 fn을 부르는
  것은 원리 1의 결과다(순수함은 증명된 사실이니, 바꾸는 집합이 빈 fn의 부름을 검증기가 받는다). 원리 1이 선 뒤에 정한다.

## 하지 않는 것

- 1.0의 마감 선언.
- 기법의 나열: fn 펼치기만으로 2배, 배치 다시 쓰기의 이관, 작은 Raft, 표시 목록과 글꼴의 부름.
- 실험이 깨기 전에 내보내는 코드를 쓰는 것.
- 앱 계약의 초안 v0은 1판(커밋 `6b25d25`)에 있다. 원리가 서면 다시 쓴다.