diff options
| author | eunhhu <[email protected]> | 2026-10-13 04:29:52 +0100 |
|---|---|---|
| committer | eunhhu <[email protected]> | 2026-10-13 04:29:52 +0100 |
| commit | 6d677df51faa120a91c44d5f069a0e51f4212727 (patch) | |
| tree | 8997e9fb92ed563d3e17f8d2d022f17f645877a7 /docs/research | |
| parent | 6238169f9adec8bc83337ffe0f54f4be756fa558 (diff) | |
| download | pure-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/research')
| -rw-r--r-- | docs/research/140-spec-suite.md | 130 |
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의 중단 기준을 따른다. |
