1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
# 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`)에 있다. 원리가 서면 다시 쓴다.
|
