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
|
# 140 — 명세 묶음: 세상의 명세가 aup에서 처음 부딪치는 곳
2026-10-13. [026](../design/026-app-contract.md)은 1.0에서 얼릴 앱 계약을 적었다. 이 연구는 다시 세울 쪽인 계산의 언어를 잴 도구를
세운다. 분야마다 명세 하나를 골라 묶음을 만들고, 오늘의 aup가 각 명세의 첫 줄에서 무엇에 막히는지를 작은 프로그램으로 확인했다.
사용자의 말: "세상의 그 어떤 명세와 개념이든 pure 생태계(vega, aup포함)에서 구현을 가장 유연하고 견고하게 해내야해. 추상화와 input
-> output으로 가는 과정은 얇고 직관적이고 빠르게." (2026-10-13)
## 쉬운 말로
- **알아낸 것.** 지금의 aup로는 묶음의 명세 대부분을 첫 줄에서 쓸 수 없다. 탐침 열 개로 확인했다. 막는 것은 여섯 가지다.
- 바이트의 i번째를 읽지 못한다.
- 비트 연산(xor, and, shift)이 없다.
- 레코드 안에 레코드나 리스트를 둘 수 없다.
- 재귀가 컴파일 오류다.
- 갈래 타입(이것 아니면 저것)이 없다.
- text의 글자를 하나씩 읽지 못한다.
- **우회는 있지만 얇지 않다.** 모두 "얇고 직관적"에 어긋나고, 명세의 개념이 언어의 개념에 바로 놓이지 않는다.
- 바이트는 메시지의 행(수의 리스트)으로 받는다.
- 비트 연산은 `floor`와 `%`의 반복으로 한다.
- 트리는 부모 키를 가진 평평한 리스트로 둔다.
- 재귀는 이벤트의 리스트로 짠 스택으로 한다.
- 한 번의 타이머는 주기 틱과 `now`로 흉내 낸다.
- **되는 것.** 관계 질의(TPC-C, 은행 질의), 그래프(BFS), 텍스트 편집과 커서, 주기 타이머다. 지금의 패턴이 덮는 곳이다.
- **아직 모르는 것.** 핵을 다시 세운 뒤 명세마다의 줄 수와 시간이다. 수치 막대는 첫 구현을 잰 뒤에 정한다. 막대가 설 수 있는지
셈부터 하고, 막대를 먼저 세우지 않는다.
- **근거.** aup 컴파일러의 실제 진단(아래 표)과 aup·Pure 설계 문서의 연산 목록이다. 시간은 재지 않았다.
- **직접 확인할 것.** `research/experiments/044-specs/run.sh`가 탐침을 컴파일하고 진단을 낸다.
- **다음 결정.** 계산의 핵을 설계한다. 여섯 가지와 고정 한도, 상수 시간 암호가 핵이 받아야 할 최소의 후보다.
## 묶음
명세를 구현하는 것과 Pure가 그것을 내부에 받아들이는 것은 다르다.
- DNS, JSON, HTTP는 경계의 명세이고, 하이브리드로 남는다.
- SHA-256과 Unicode는 수학이거나 세상의 자료다.
- 배치는 Vega의 일이다.
- 묶음이 재는 것은 "세상의 명세를 Pure 생태계에서 얇게 쓸 수 있는가"이다.
| # | 명세 | 분야 | 처음 필요한 것 | Pure 안의 검증 | 오늘 |
|---|---|---|---|---|---|
| 1 | DNS 메시지(RFC 1035) | 와이어 프로토콜 | 바이트 읽고 쓰기, 빅엔디언, 비트 필드, 이름 압축(바이트 안의 참조) | 알려진 구현이 만든 질의·응답 바이트와 대조 | 못 쓴다(바이트, 비트) |
| 2 | SHA-256(FIPS 180-4) | 해시 | 32비트 낱말, 회전, xor | NIST CAVP의 SHA 벡터 | 우회로만 될 것으로 보인다(써 보지 않음) |
| 3 | inflate(RFC 1951) | 압축 | 비트 읽기, 허프만 표, 뒤 참조 | zlib로 압축한 말뭉치를 풀어 원본과 비교 | 못 쓴다(바이트, 비트) |
| 4 | JSON(RFC 8259) → 트리와 질의 | 깊이를 모르는 데이터 | 글자 읽기, 중첩, 재귀, 갈래 | JSONTestSuite | 못 쓴다(글자, 중첩, 재귀, 갈래) |
| 5 | UTF-8과 줄 나누기(UAX #14) | 텍스트 | 바이트, 코드 포인트, 속성 표 | Unicode의 `LineBreakTest.txt` | 못 쓴다(글자) |
| 6 | 관계 질의, 그래프 탐색 | 데이터 모델 | 리스트, 키, 접기, 이벤트의 리스트 | TPC-C, 은행 질의, 파이썬 모델 | 된다(기준선: [092](092-tpcc.md), 040의 은행 질의, aup `routes.aup`) |
| 7 | 텍스트 편집 | UI 개념 | text, 커서 | 편집기의 참조 모델 대조(aup `make check`) | 된다 |
| 8 | 상자 배치(flex 같은) | UI 개념 | 중첩, 재귀 | 기존 배치 구현(Yoga, Taffy)의 결과와 대조 | 못 쓴다(중첩, 재귀) |
| 9 | HTTP/1.1 요청을 패킷마다(RFC 9112) | 스트림의 상태 기계 | 바이트, 이벤트를 넘는 상태 | 경계를 아무 데서나 자른 요청 모음 | 못 쓴다(바이트). 지금은 `serve/`의 C다 |
| 10 | 재시도, 물러서기, 시간 제한 | 시간 | 시각, 한 번의 타이머 | 시각을 준 시뮬레이션 | 우회(주기 틱 `every`와 `now`) |
| 11 | X25519, ChaCha20-Poly1305 | 상수 시간 암호 | 데이터에 따라 달라지지 않는 시간 | RFC 7748, RFC 8439의 벡터 | aup 밖(설계상, 아래) |
**11은 핵의 원시 연산으로 둔다(가설).** 실행기의 시간은 데이터에 따라 달라진다. 묶음 실행기도 결함이 나면 묶음을 처음부터 실행기로
다시 돈다. 그래서 상수 시간을 언어로 약속하기 어렵다. 지금도 암호는 `link/`의 C와 OpenSSL에 있다.
## 기준 (명세마다)
1. **쓸 수 있다.** aup와 Pure만으로 쓴다. 코어에 C를 더하지 않는다.
2. **우회가 없다.** 명세의 개념이 언어의 개념에 바로 놓인다. 바이트는 바이트이고 트리는 트리다.
3. **얇다.** 줄 수를 깔끔한 참조 구현(파이썬)과 견준다.
4. **빠르다.** 시간을 C의 참조 구현과 견준다. 막대는 첫 구현을 잰 뒤 정한다.
5. **견고하다.** 위 표의 검증을 모두 지나고, 예산 안에서 끝나고, 세 기계(Pi, WSL2, Mac)에서 같은 답을 낸다. 검증은 Pure의
검사(`make check`) 안에서 돈다. 이것이 Pure 생태계 안의 표준이다.
**쌓임을 막는 규칙.** 핵에는 묶음의 명세 둘 이상이 필요로 하는 것만 넣는다. 하나만 필요로 하는 것은 라이브러리다. 지금의 명령
90개가 판마다 패턴 하나씩 쌓인 길(026)을 다시 걷지 않기 위해서다.
## 탐침
명세가 처음 필요로 하는 것을 가장 작은 aup 프로그램으로 써서 컴파일했다(aup `build/aup`, 2026-10-13). 원본은
`research/experiments/044-specs/probes/`, 출력은 `2026-10-13-probes.tsv`다.
| 탐침 | 쓴 것 | aup의 진단 |
|---|---|---|
| `p1-byte` | `packet.data[0]`(bytes 필드의 첫 바이트) | `expected newline or semicolon` |
| `p2-bits` | `(h ^ word.w) << 3` | `unexpected character '^'` |
| `p2b-bits` | i64의 `h & word.w` | `unexpected character '&'` |
| `p3-nested` | 레코드 안의 `children: list of Node` | `expected a numeric field default` |
| `p3b-nested` | 레코드 안의 `at: Point` | `a field is a number …, a bool …, text … or an i64` |
| `p4-rec` | 자신을 부르는 `fn depth(n)` | `fn 'depth' calls itself` |
| `p5-chars` | `for c in line.t` | `unknown list 'line.t'` |
| `p5b-chars` | `line.t[0]` | `expected newline or semicolon` |
| `p5c-cursor` | 커서 자리의 글자 `note.char(at)` | `unknown library 'note'` |
| `p6-variant` | `state x: Leaf \| text` | `unexpected character '\|'` |
진단이 아니라 연산 목록에서 확인한 것도 있다.
- Pure의 명령에 바이트를 자리로 읽거나 쓰는 것이 없다. 바이트 값에는 `LEN`과 text 변환(`TEXT_FROM`, `BYTES_FROM`)뿐이다(008).
- text에는 길이(`.chars`, `.lines`, `.bytes`), 커서가 있는 줄(`TEXT_LINE`), 넣기와 지우기, 비교, 잇기가 있고, 글자 하나를 읽는 것은
없다(aup 002).
- 고정 한도가 형식에 있다: 상태 32, 입력 32, 레코드 16, 레코드의 필드 16, 키별 컬렉션 1, 모듈의 코드 65,535 명령(`core/module.h`).
fn은 부르는 곳마다 인라인되므로, 큰 명세의 구현은 코드 한도에 먼저 닿을 수 있다.
## 핵이 받아야 할 최소 (가설)
| 후보 | 그것을 필요로 하는 명세 |
|---|---|
| 바이트를 자리로 읽고 쓰고 자르기 | 1, 2, 3, 5, 9 |
| 정수의 비트 연산(and, or, xor, shift, rotate) | 1, 2, 3 |
| 중첩(레코드 안의 레코드와 리스트) | 4, 8 |
| 갈래(합 타입) | 4, 8, 9(파서의 상태) |
| 재귀(깊이를 실행량과 메모리 예산에 센다) | 4, 8 |
| text를 글자의 열로 읽기 | 4, 5 |
| 뜻에서 구현의 숫자 빼기(고정 한도) | 3, 4, 5(표의 크기) |
| 상수 시간 암호의 원시 연산 | 11과 링크 |
**재귀는 끝남과 결정성을 깨지 않는다.** 이벤트가 끝나는 것을 실제로 보증하는 것은 문법(상한 있는 반복, 재귀 금지)이 아니라
예산이다. `for i in 0 .. 1e15`가 어느 기기에서나 같은 자리에서 `work`로 멈추는 것도 예산 덕이다. 재귀도 그 깊이를 실행량과
메모리에 세면 같은 보증 아래 둘 수 있다. 끝이 없는 일(스트림, 긴 계산)은 이벤트마다 상한 있는 걸음 하나를 하고, 이어갈 자리를
상태에 둔다(9가 그 꼴이다). 이 가설이 맞다면 aup의 제한 일부는 불변의 핵이 아니라, 패턴을 모으던 때의 안전장치다. 핵 설계에서
확인한다.
## 의심
- **text와 바이트를 따로 둘 것인가?** text는 "UTF-8로 검사한 바이트"의 한 견해일 수 있다. 4와 5가 같은 열을 다른 단위(바이트,
글자)로 읽는다.
- **리스트, 키 있는 리스트, 인덱스, 커서를 하나로 모을 수 있는가?** 026의 3번 의심과 같다. 중첩이 들어오면 리스트는 값이 되고, 키와
앵커는 그 위의 견해가 될 수 있다.
- **메시지의 행은 중첩의 땜질인가?** 레코드의 리스트를 메시지에만 허락한 것은 중첩이 없어서 낸 길로 보인다. 중첩이 들어오면 따로 둘
까닭이 없다.
## 착수 기준 (다음 일)
- **바꿀 결정.** 계산의 핵을 설계한다(027). 위 표의 여덟 후보 가운데 무엇을 어떤 모양으로 받을지 정한다.
- **남은 질문.**
- 핵을 일반화해도 은행 질의와 TPC-C가 그대로인가?
- 바이트와 비트 일의 시간이 C와 얼마나 떨어지는가? 지금 그런 일은 실행기로 돈다.
- **최소 확인.** 핵의 첫 꼴로 2(SHA-256)와 4(JSON)를 먼저 쓴다. 둘이 탐침 여섯을 모두 덮는다: 2는 바이트와 비트, 4는 글자, 중첩,
재귀, 갈래다. 공식 벡터를 지나는지, 줄 수, C 대비 시간을 잰다.
- **중단 기준.** 한 명세만 필요로 하는 원시 연산이 핵에 들어가야 하면 멈추고 라이브러리 길을 찾는다. 일반화한 핵에서 은행 질의의
명령 수가 1%, TPC-C가 3%를 넘게 나빠지면 026의 중단 기준을 따른다.
|
