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
|
# 029 — 증명이 곧 컴파일러이고, 커밋이 곧 복제본이다
작성일: 2026-10-19. 상태: **설계 초안 2판**. 1판(기법 다섯의 나열)은 바깥 피드백 008로 반려했다. 코드는 아직 없다. 이 판은
원리 둘과 열린 질문 하나, 그리고 원리마다 그것을 깰 수 있는 실험 하나만 적는다.
## 쉬운 말로
pure link는 전송 세션이 들고 있던 것(순번, 확인, 다시 보내기)을 앱의 outbox와 heard가 이미 들고 있음을 알아보고 세션을
지웠다. 단일 싱크 트리는 WAL이 들고 있던 것(바뀐 것과 그 순서)을 트리의 새 노드가 이미 들고 있음을 알아보고 WAL을 지웠다.
같은 질문을 남은 결함에 던진다. **어느 두 계층이 같은 정보를 들고 있는가, 그리고 어느 쪽을 지울 수 있는가.**
- **원리 1.** 검증기가 증명한 것을 실행기 셋이 다시 알아내거나 버린다. 증명을 버리지 않으면 실행기 셋이 사라진다.
- **원리 2.** 복제 프로토콜이 들고 다닐 것을 저장소의 커밋과 링크가 이미 들고 있다. 복제 계층이 사라진다.
## 원리 1. 증명이 곧 컴파일러다
**사실.** 140의 느린 명세 다섯(DNS, HTTP, inflate, JSON 트리, UAX #14)은 모두 `runner 2`다. fn이 있으면 블록 전체가 실행기로
가고, 기계어는 만들어지지 않는다. 실행기에서 센 명령 하나에 3.2–3.9 ns가 든다. UAX #14는 코드 포인트당 명령 1,774개다. C는
코드 포인트 하나를 35 ns에 끝낸다.
**같은 정보를 든 두 계층.** 검증기는 모듈을 받을 때 모든 자리에서 다음을 증명한다.
- 스택의 높이와 각 칸의 타입. 높이가 정적이라 스택의 칸마다 이름 붙은 값으로 바꿀 수 있다.
- 반복마다 시작할 때의 횟수 상한.
- 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배는 시험할 주장이지 약속이 아니다.
## 원리 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`)에 있다. 원리가 서면 다시 쓴다.
|
