aboutsummaryrefslogtreecommitdiffstats
path: root/docs
diff options
context:
space:
mode:
authoreunhhu <[email protected]>2026-10-13 04:29:52 +0100
committereunhhu <[email protected]>2026-10-13 04:29:52 +0100
commit6d677df51faa120a91c44d5f069a0e51f4212727 (patch)
tree8997e9fb92ed563d3e17f8d2d022f17f645877a7 /docs
parent6238169f9adec8bc83337ffe0f54f4be756fa558 (diff)
downloadpure-6d677df51faa120a91c44d5f069a0e51f4212727.tar.gz
pure-6d677df51faa120a91c44d5f069a0e51f4212727.zip
Research 140: a suite of eleven specs from different fields (DNS, SHA-256, inflate, JSON, UTF-8 and line breaking, relational queries and graphs, text editing, box layout, HTTP/1.1 by packets, retries and timeouts, constant-time crypto) with five criteria (written in aup and Pure alone, no workaround, lines against a Python reference, time against C, the spec's own vectors passing in Pure's checks on three machines); ten probes (044) show today's aup stops at a byte by position, bit operations, nesting, recursion, variants and reading a character; the core's minimal candidates and the rule against piling up (only what two specs need); SHA-256 and JSON first
Diffstat (limited to 'docs')
-rw-r--r--docs/research/140-spec-suite.md130
1 files changed, 130 insertions, 0 deletions
diff --git a/docs/research/140-spec-suite.md b/docs/research/140-spec-suite.md
new file mode 100644
index 0000000..24d488a
--- /dev/null
+++ b/docs/research/140-spec-suite.md
@@ -0,0 +1,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의 중단 기준을 따른다.