# 030 — 한 실행 경로: 증명이 표현을 고르고, 같은 데이터는 한 모양으로

작성일: 2026-10-19. 상태: **설계 확정, 단 하나는 사용자의 결정**(아래 "정할 것"). 코드는 아직 없다. 근거는 029의 원리 1 결과, 045,
046, 047이다. 바깥 피드백 008(실행기 분열 금지)과 009(같은 데이터는 한 바이트 모양)를 따른다.

## 쉬운 말로

UAX #14의 메시지 하나는 오늘 런타임에서 코드 포인트당 기계 명령 40,847개(사이클 15,735)가 든다. 같은 앱을 손으로 바꿔 써서 잰 경로는
813개(사이클 348)다. 둘 다 같은 빌드에서 쟀다. 리스트의 코드를 하네스 안에 함께 지은 빌드라, 다른 빌드의 40,365와 1–2% 다르다. 그 경로에서는
트리 밖 복사도 역직렬화도 하지 않고, 앱은 aup가 오늘 받는 그대로(키 있는 리스트와 seek)다. 그래서 같은 빌드의 Vega의 C(같은 페이로드에
251, 사이클 93)의 3.2배이고, 사이클로는 3.7배다. 앞서 보고한 602(사이클 373)는 앱이 쓰지 않은 알고리즘으로 바꾼 수였다. 키로 하는
seek는 기계 명령이 더 많지만, 안쪽 노드의 키를 쓰고 자식 포인터를 따라가지 않아 사이클은 더 적다. 이 문서는 그 경로를 런타임의 단 하나의
실행 경로로 만드는 설계다.

## 경로

메시지 → 테두리 → 내보낸 처리기 → 커밋 → 복제, 보기. 단계마다 무엇을 하고, 무엇이 그것을 허락하고, 무엇으로 쟀는지 적는다.

| 단계 | 하는 일 | 허락하는 것 | 잰 것 |
|---|---|---|---|
| 테두리 | 행을 페이로드가 둔 자리에서 읽는다. 검사만 한다(행이 온전한지, 수가 유한한지, 불이 0이나 1인지). 처리기가 바꾸는 상태 하나만 따로 쓰고, 오류 없이 끝나면 그것으로 바꾼다 | 언어의 뜻(입력은 바뀌지 않는다), N2 | 1,595 → 22/점(045). 여러 필드 행은 32행 열 덩어리로 오면 1,318 → 44/행(047) |
| 처리기 | 지역과 스택은 레지스터에 둔다. 부름은 맨 부름이다. 사건의 리스트는 타입 있는 버퍼다(내보낸 사슬에서 9.43배). 레코드에 담은 리스트는 복사하지 않고 함께 쓴다. 정수는 정수로 다룬다 | 오늘의 증명(스택 모양, fn마다의 집합), N1, N4, 표현의 결정 | 38,623 → 564–788/점(045) |
| 저장 리스트 읽기 | 메모리의 리프(binary64 열)를 그 자리에서 읽는다. 키로 찾을 때는 안쪽 노드의 키로 내려가 리프의 키 열에서 찾는다. 사건 안에서는 리프를 쥐고 있는다 | N2(사건 안에서 바뀌지 않음), 키 있는 리스트의 선언 | keyed_shared 788, 끝에서 끝 813, 사이클 348(045) |
| 커밋 | 덧붙이기는 마지막 리프의 빈칸에 셀만 그 자리에서 쓰고, 개수는 커밋 레코드에 둔다. 흩어진 갱신은 오늘의 로그 레코드로 쓴다 | 쥔 스냅숏은 제 개수 너머를 읽지 않는다 | 덧붙이기 리스트 바이트 25.9 / 10.9 / 10.0(오늘 65.5 / 15.7 / 12.4), 갱신은 로그 그대로(047) |
| 복제 | 저장소가 제 sync에서 끊은 제 파일 연산을 pure link로 보낸다. 확인은 heard다 | 원리 2 | 바이트 같음, kill -9 90번, 접두 867곳(046) |
| 보기 | 리프를 그 자리에서 읽는다(오늘의 스냅숏이 하는 대로) | 090의 O(1) 스냅숏 | — |

지우는 것.
- 실행 경로로서의 실행기, 묶음 실행기의 레인(`module-batch.c`), AArch64 기계어 계층(`module-jit.c`). 실행기는 참조로만 남아, 검사가 두
  경로의 답을 견준다.
- 메시지마다 행을 트리로 다시 짓는 `pure_list_read`.
- 사건마다 상태 54개를 다섯 번 훑기. N2가 바뀌는 것만 알려 준다.
- 뜨거운 길의 범용 리스트 API(폭 고르기, `list_held`, PureCell 바꿈). 참조 경로에는 남는다.
- 통째로만 바뀌는 bytes 상태의 조각 트리.

## 검증기가 더할 사실

오늘 증명하는 것은 스택의 높이와 타입, 반복의 상한, fn마다의 등록기·리스트·바꾸는 집합, 리스트 사이에 별칭이 없음이다. 여기에 더할
것은 셋이다. 검증기가 스스로 알아낸다. aup가 말한 것을 믿지 않는다.
- **N1 정수임.** `number` 자리(지역, 매개변수, 결과, 리스트의 열)가 정수만 갖는지, 0 이상인지. 0, `.count`, 정수끼리의 `+ - *`, 0 이상
  정수끼리의 `//`와 `%`, 정수 열에서 읽은 값에서 퍼진다. 처리기에서 1.10배, 정수 버퍼의 전제다.
- **N4 담은 뒤 바뀌지 않음.** `LIST_VALUE` 뒤에 그 리스트도 레코드의 리스트도 바뀌지 않는다. 1.23배다. aup는 담은 뒤 바꾸는 것을
  허락하므로 지점마다 증명해야 한다.
- **N2 처리기의 변경 집합.** fn에 하는 분석을 처리기로 넓힌다. 테두리의 상태 하나와, 사건 안에서 리프를 쥐는 것을 허락한다.

경계 안임(N5)은 더하지 않는다. 경계 검사는 남기고, 그 값은 1.12배다.

## 표현의 결정(증명이 필요 없는 것)

- 사건의 리스트: 타입 있는 버퍼다(수는 binary64, 정수 열은 N1이면 i64, 불은 u8). 키 없고 인덱스 없는 리스트가 받는 연산을 모두 한다.
  9.43배는 내보낸 사슬 안의 인자다(분배와 메모리 칸이 지워진 뒤). 실행기 안에서는 몫이 훨씬 작을 것이다. 인자는 몫이 아니다. 차례 1에서
  처음 잴 것이지 예측이 아니다.
- 입력의 행: 페이로드 그 자리에서 읽는다. 필드가 하나인 레코드는 행이 곧 열이다. 필드가 여럿인 메시지는 32행의 열 덩어리(메모리 리프의
  열)로 바꾼다. 메시지 형식을 바꾸는 일이고, 1.0 전이라 깰 수 있다.
- 통째로 바뀌는 bytes 상태: 버퍼 둘을 번갈아 쓴다.
- 메모리 셈: 꼴과 상관없이 정의한다(셀 8바이트, 텍스트는 그 바이트). 지금은 폭으로 압축한 꼴에 따라 정해진다. 계약의 결정이다.
- 앱의 관용구: 정렬된 데이터를 찾는 일은 키 있는 리스트와 seek(`first(x in L where x.key >= v)`)로 쓴다. 손으로 쓴 이분 탐색은 트리가
  이미 가진 색인을 다시 짓는다. aup의 걸림이 하나 있다. fn 안의 접기가 fn의 매개변수를 읽지 못해서, seek를 처리기에 써야 했다.
  매개변수는 접기 동안 정해진 값이니 받아들이는 것이 맞다(aup의 일).

## 009와의 긴장(한 번 적는다)

항목의 셀은 덧붙이기에서 한 모양을 지킨다. 패킷, 리프, 리프의 꼬리, 복제 모두 binary64다. 흩어진 갱신에서는 델타라는 그릇이 어떤
리프 모양보다 싸다(047: 3–5배 이상). 오늘의 로그는 거기에 더해 정수를 zigzag varint로 줄인다. 정수에 대해서는 둘째 바이트 모양이고,
그것이 이기는 모양이다. 이 설계는 흩어진 갱신을 로그에 둔다. 그래서 정수의 델타에서는 009의 철칙을 지키지 않는다. 지키려면 델타의
값을 binary64로 두면 된다(바뀜 하나에 약 7 B 더). 그 값을 치를지는 재고 나서 정한다.

## 단서

- 047은 바이트를 세는 모형이지 저장소가 아니다. 델타 방을 읽는 값은 세지 않았고, 리프는 가득 찼다고 보았으며, 커밋 레코드의 크기는 가정했다.
- 기준선의 은행 실행에는 트리 커밋이 없다(리스트만 바뀐다). 기준선은 실행마다 메시지 2만 개라, 그 안에 이미지 체크포인트가 없다.
- 패킷을 리프로 받는 것은 메시지 형식을 바꾸는 일이고, 텍스트 열을 설계하기 전까지는 수에만 해당한다.
- 손으로 쓴 경로의 수는 하네스 빌드마다 1–2% 움직인다.

## 정할 것(사용자의 결정)

내보낸 처리기를 제품에서 무엇이 기계어로 바꾸는가.
- **(가) 설치할 때 시스템 C 컴파일러.** 호스트가 검증한 모듈을 C로 옮기고, `cc`로 지어 모듈의 다이제스트로 캐시한다. 잰 것은 이것이다
  (손으로 쓴 C, gcc -O2). `cc`가 런타임의 의존이 된다. 재지 않은 것: 모듈 하나를 짓는 시간(140의 앱 200–2,000줄; Pi에서 몇 초로 본다),
  `cc`가 없는 호스트(그때는 실행기, 참조 경로).
- **(나) Pure 자신의 내보내기, 명령어 집합마다.** AArch64부터 시작한다. 의존이 없고 짓는 시간이 짧다. 029는 명령어 집합마다의 뒤끝을 두지
  않으려 했고, 그것을 피하던 길(이어 붙이기)은 죽었다. 재지 않은 것: 전부다.
- aup가 미리 기계어를 내보내는 길은 없다. 검증기는 바이트코드를 증명하고, 실행되는 코드는 그 증명에서 나와야 한다.

## 짓는 차례와 차례마다의 깨는 확인

1. **표현 먼저, 실행기 안에서.** 입력 행을 그 자리에서 읽기, 사건 리스트를 타입 있는 버퍼로, 리프를 쥐고 읽기, 상태 훑기를 N2로 줄이기.
   내보내기 없이도 140의 모든 명세가 빨라져야 한다. 확인: 140의 검사가 모두 지나고(답이 같다), 041의 셈, 은행 1%, TPC-C 3%를 지킨다.
   이 단계로 얼마나 주는지는 재지 않았다. 먼저 잴 것이다.
2. **검증기의 N1, N2, N4.** 확인: 140의 모듈에서 각 사실이 몇 자리에 서는지 센다. 변이 시험으로, 사실을 거짓으로 세우는 모듈을
   검증기가 거부하는지 본다.
3. **내보내기((가) 또는 (나)).** 확인: 140의 모든 명세를 두 경로로 돌려 답을 견준다. 041과 은행, TPC-C의 관문을 지킨다.
4. **저장소의 리프 꼬리.** 덧붙이기는 리프에, 흩어진 갱신은 로그에 쓴다(047). 확인: 046의 같음, 이어받기, 찢긴 꼬리를 그대로 다시 돌리고,
   047의 바이트를 실제 저장소에서 다시 잰다.
5. **메시지 형식.** 필드 여럿인 행을 32행 열 덩어리로 보낸다. 확인: 047의 `packet.c`를 실제 테두리에서 다시 잰다.

## 하지 않는 것

- 흩어진 갱신을 리프로 쓰는 것. 047에서 16–55배였다.
- 트리 밖에 열을 복사해 두는 것(009). 045의 stored_flat은 비교로만 남는다.
- 1.0의 마감 선언.