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
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
|
# 029 — 증명이 곧 컴파일러이고, 커밋이 곧 복제본이다
작성일: 2026-10-19. 상태: **설계 초안 2판**. 1판(기법 다섯의 나열)은 바깥 피드백 008로 반려했다. 코드는 아직 없다. 이 판은
원리 둘과 열린 질문 하나, 그리고 원리마다 그것을 깰 수 있는 실험 하나만 적는다.
**원리 1은 UAX #14에서 깨졌다(2026-10-19, 045).** 두 실험 모두 막대에 못 미쳤다. (가) 2.19배(막대 4배), (나) 1.31배(막대
3배). 아래 "깨는 실험의 결과"에 무엇을 시험했고 무엇은 시험하지 않았는지 적는다. 깨진 것은 "실행기의 몸을 이어 붙인다"는
길이다. 표현까지 증명에서 내보내는 것은 손으로 쓴 점에서 range() 하나가 C의 1.75배, UAX #14의 처리기 전체가 C의 2.5배였다
(사건 자체의 1,566은 따로 남는다). 원리 2는 아직 시험하지 않았다.
## 쉬운 말로
pure link는 전송 세션이 들고 있던 것(순번, 확인, 다시 보내기)을 앱의 outbox와 heard가 이미 들고 있음을 알아보고 세션을
지웠다. 단일 싱크 트리는 WAL이 들고 있던 것(바뀐 것과 그 순서)을 트리의 새 노드가 이미 들고 있음을 알아보고 WAL을 지웠다.
같은 질문을 남은 결함에 던진다. **어느 두 계층이 같은 정보를 들고 있는가, 그리고 어느 쪽을 지울 수 있는가.**
- **원리 1.** 검증기가 증명한 것을 실행기 셋이 다시 알아내거나 버린다. 증명을 버리지 않으면 실행기 셋이 사라진다.
**이어 붙이는 길은 깨졌다(045).** range()에서 절벽은 수와 리스트의 표현(10.9배), 메모리의 칸과 부름(3.29배), 분배(1.78배)의
곱이었다.
- **원리 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()의 사슬이 보이듯 계층은 곱해지고, 한 계층의
인자는 다른 계층이 지워진 뒤에야 드러난다.
- range()의 이분 탐색 하나가 코드 포인트당 14,489개, 36%다(변형 v0r). 실행된 명령으로는 549.9 가운데 269.5다
(`2026-10-19-ops-v0r.txt`). 반복은 11.4번이다. Vega의 C는 종류를 두 단계 표에서 한 번에 읽는다. 그래서 저장 리스트 읽기의
몫은 앱이 고른 알고리즘 때문에 크다.
- **range()를 손으로 내보낸 사슬(`range.c`, 2026-10-19).** 내보내기가 쓸 코드를 손으로 쓰고, 증명이 허락할 수 있는 것을 하나씩
지웠다. 모든 방식의 답이 61,285개 코드 포인트 모두에서 실행기와 이어 붙인 판의 답과 같다.
| 방식 | 남은 것 | 기계 명령/점 | 사이클/점 | 반복 한 번 |
|---|---|---|---|---|
| 실행기 | 분배, 메모리의 칸, 부름의 기계, 아래 전부 | 14,488 | 5,508 | |
| 이어 붙임 | 메모리의 칸, 부름의 기계, 아래 전부 | 8,144 | 3,209 | |
| exact | 레지스터와 맨 부름. double, `fmod`의 `//`, 유한·정수 검사, 트리 읽기, 예산 | 2,474 | 1,315 | 217 |
| integer | exact에서 수를 정수로 | 1,587 | 875 | 139 |
| flat | exact에서 `start`를 평평한 열에서 | 1,083 | 633 | 95 |
| both | 정수와 평평한 열. 경계 검사와 예산은 남는다 | 226 | 125 | 19.8 |
| C | 같은 이분 탐색, 검사도 예산도 없이 | 129 | 93 | 11.3 |
- 인자(기계 명령): 분배 1.78배, 메모리의 칸과 부름의 기계 3.29배, 수와 리스트의 표현 10.9배, 남은 경계 검사와 예산이 C의 1.75배.
사이클로는 1.72, 2.44, 10.5배, C의 1.36배다.
- **미리 정한 막대(C 반복의 3배, 34)로: exact 217은 못 미치고, both 19.8은 지난다.** 판정은 미리 적은 대로다. range()에서 절벽은
분배가 아니라 수와 리스트의 표현, 그리고 메모리의 칸과 부름에 있다.
- 확인한 전제 셋.
- "리스트가 바뀌지 않음": 증명되어 있다. 검증기는 fn마다 그것이 바꾸는 리스트의 집합(`function_changes`)을 증명하고, range()는
아무것도 바꾸지 않는다.
- "정수 인덱스임": **증명되어 있지 않다.** low와 high는 `number`이고, INDEX_AT이 정수인지를 실행 중에 검사한다. aup는 그것을 알
수 있다(0, `.count`, 정수끼리의 `//`). 하지만 지금은 aup도 검증기도 그 사실을 적지 않는다. 증명에 새로 넣어야 할 사실이고, 그것
하나로 1.56배다.
- "함수 지역 수명": range()는 제 리스트가 없어서 이 실험이 시험하지 않는다.
- 묶인 것과 단서.
- 이어 붙임 → exact의 3.29배는 메모리의 칸과 부름의 기계를 함께 지운다. 둘을 가르지 않았다. 부름 하나의 값(단위 1,375)으로 어림하면
5,670 가운데 약 1,400이 부름이다. 어림이다.
- 평평한 열은 잰 구간 밖에서 지었다. 증명이 허락하는 것은 "부름 안에서 바뀌지 않음"이다. 돌아가는 시스템에서는 그 값이 바뀔 때로
옮겨 간다. `ranges`(한 번 싣는다)에는 거의 없지만, 사건마다 바뀌는 리스트에는 재지 않았다. 트리의 잎은 이미 열이다(090).
반복당 122개가 내려가기인지 칸의 일반 경로인지는 가르지 않았다.
- 앱의 36%만이다. decide, let 리스트, `Text`의 복사는 이 사슬로 보이지 않았다.
- **앱 전체의 사슬(`app.c`, `app-way.h`, 2026-10-19).** `on line`, decide와 그 fn들을 한 번 쓰고, 단마다 매크로를 달리해 펼쳤다.
모든 단의 답이 18,672줄 모두에서 시험의 답과 같고 exact의 출력과 정확히 같다. 규칙 하나(LB18)를 틀리게 지은 판은 일곱 단 모두
6,233줄이 틀려 거부된다. 두 번 돌려 수가 같다.
| 단 | 남은 것 / 지운 것 | 기계 명령/점 | 사이클/점 | 인자 | 허락하는 사실 |
|---|---|---|---|---|---|
| 실행기(사건 1,566 빼고) | | 38,623 | 14,791 | | |
| 이어 붙임(사건 빼고) | 분배를 지움 | 26,523 | 11,079 | 1.46 | |
| exact | 메모리의 칸과 부름의 기계를 지움. double과 검사, FLAT `PureList`(append마다 `list_held`와 `grows`), `Text`의 복사, 트리의 `ranges`, 예산은 남김 | 8,785 | 4,002 | 3.02 | 오늘 증명됨: 스택의 모양과 타입, fn마다의 등록기·리스트·바꾸는 집합 |
| integer | 정수를 정수로 | 7,979 | 3,547 | 1.10 | **N1** 정수임(새로) |
| stored_flat | `ranges`의 열을 평평하게 | 6,561 | 2,800 | 1.22 | **N2** 처리기의 바꾸는 집합(있는 분석을 처리기로 넓힘) |
| local_flat | 사건의 리스트, 점, `out`을 타입 있는 버퍼로(append마다 메모리 셈은 남김) | 696 | 364 | 9.43 | **N3** let 리스트가 받는 연산(덧붙이기, 자리 읽기, 세기뿐: 키 없음, 인덱스 상태 없음)(새). 원소 타입은 정적이고, 정수 열은 N1 |
| shared | `Text`가 버퍼를 함께 씀(복사 없음) | 564 | 317 | 1.23 | **N4** 담은 뒤 바뀌지 않음: `LIST_VALUE` 뒤에 그 리스트도 레코드의 리스트도 바뀌지 않는다(새) |
| unbounded | 경계 검사를 지움 | 502 | 298 | 1.12 | (N5 경계 안임: 막대에 필요 없어 넣지 않음) |
| plain | 예산과 메모리 셈까지 지움: 같은 알고리즘의 C | 362 | 258 | 1.39 | 셈은 계약이라 증명으로 지우지 않는다 |
| Vega의 C | 두 단계 표, 이분 탐색 없음 | 225 | 88 | 1.61 | |
- 인자의 곱 1.46 × 3.02 × 1.10 × 1.22 × 9.43 × 1.23 × 1.12 × 1.39 × 1.61 = 172 = 38,623 / 225.
- **처리기는 38,623 → 564, 68배다. Vega의 C(225)의 2.5배이고, 사이클로는 3.6배다.** 남은 것은 Pure의 계약(경계 검사 1.12배, 예산과
메모리 셈 1.39배)과 알고리즘(이분 탐색과 위치마다의 리스트, 1.61배)이다. 미리 정한 막대(shared ≤ plain의 2배)를 지난다(1.56배).
- **사건 자체가 이제 가장 큰 계층이다.** 빈 처리기가 코드 포인트당 1,566이다. 줄 하나에 약 5,140이고, 내보낸 처리기(564)의 2.8배다.
표본으로는 리스트의 일(점을 사건의 리스트로 풀기, 사건의 리스트를 비우고 놓기) 674, malloc과 free 389, 사건의 기계 386, 상태
`breaks`를 저장 트리로 쓰기 113이다. 이 사슬은 그것을 지우지 않았다. 지금의 사건을 그대로 두면 메시지 하나의 값은 564 + 1,566 =
2,130, Vega의 9.5배다. 메시지의 점은 이미 평평한 수의 열인데, 사건이 그것을 리스트로 다시 푼다. 이것이 다음에 볼 겹친 계층이다.
- **전제 하나를 고친다.** let 리스트는 영속 트리가 아니다. 실행기는 사건의 리스트를 처음부터 FLAT 배열로 둔다(021, `pure_list_arrays`:
담은 것에 맞춰 폭을 고르는 열). 9.43배는 트리가 아니라 범용 리스트의 길에서 온다. append마다 `pure_list_insert`의 폭 고르기와
넓히기, `list_held`가 앞뒤로 부르는 함수 여덟, 읽기마다 꼴과 폭의 갈래와 double로의 바꿈이 든다. 트리는 저장 리스트 `ranges`뿐이다.
- **새로 증명할 사실은 셋, 넓힐 분석은 하나다(N1–N4).** 오늘의 증명(스택의 모양과 타입, fn마다의 등록기·리스트·바꾸는 집합)이 exact를
허락한다. 이 앱의 fn 여섯은 제 사건 리스트가 없고 아무것도 바꾸지 않으며, 등록기는 부름마다 제 것이라 C의 지역이 된다. 그 위에
N1 정수임, N3 let 리스트의 연산, N4 담은 뒤 바뀌지 않음은 새로 증명해야 하고, N2는 fn에 하는 분석을 처리기로 넓히면 된다. 확인한 것:
입력 리스트는 aup가 바꾸지 못하게 한다(언어의 뜻이라 증명이 필요 없다). 담은 뒤 바꾸는 것은 aup가 허락하므로 N4는 지점마다
증명해야 한다.
- 단서.
- exact는 소스에서 썼다. C의 `&&`와 `||`는 필요한 데까지만 가고, 읽기마다의 `LIST_BIND`는 없으며, cc가 fn을 인라인할 수 있다. 그래서
exact는 충실한 내보내기보다 싸다. 이어 붙임 → exact의 인자는 크게, exact 뒤의 인자들은 작게 나왔을 수 있다.
- 단의 차례가 인자를 정한다(곱은 같다).
- 사건의 리스트에 대한 메모리 셈을 append마다 8바이트로 바꾸었다. 지금의 셈은 폭으로 압축한 저장 꼴의 바이트이고, 구현에 따라
정해진다. 셈의 정의를 꼴과 무관하게 정하는 것은 계약의 결정이다.
- 평평한 `ranges`의 값은 바뀔 때로 옮겨 간다(재지 않음).
- UAX #14 하나다. DNS, HTTP, inflate, JSON은 바이트와 텍스트와 재귀의 섞임이 달라, 인자를 옮겨 말하지 않는다.
- **고친 것: let 리스트 후보.** 처음 이 자리에 "셈으로 깨졌다(13,000, 32%, 1.5배)"라고 적었다. 그것은 실행기 안의 몫이었다. 위의 사슬에서
인자로 재니 9.43배이고, 사슬에서 가장 큰 인자다.
- **고친 것: 막대의 셈.** "명령 하나가 기계 명령 하나여도 C의 2.5배"라고 적었다. 명령의 수가 바닥이라고 본 것인데, range()의 both는
실행된 명령 269.5개를 기계 명령 226개로 한다(하나에 0.84). 레지스터 아래에서 옮김과 상수가 사라진다. 그 셈은 틀렸다.
- **원리 1이 지금 말하는 것.** 시험한 길(실행기의 몸을 이어 붙이기)은 죽었다(앱 1.43배, range() 1.78배). 표현까지 포함해 증명에서
내보내는 것은 UAX #14의 처리기에서 C의 2.5배(사이클 3.6배)다. 새 사실 셋과 넓힌 분석 하나가 필요하고, 계약(검사와 셈)과 알고리즘이
남는다. 사건 자체(1,566)는 이 길 밖이다. 손으로 쓴 점 하나이지, 지은 내보내기가 아니다.
## 원리 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`)에 있다. 원리가 서면 다시 쓴다.
|
