diff options
| -rw-r--r-- | CHECKPOINT.md | 1 | ||||
| -rw-r--r-- | docs/research/140-spec-suite.md | 130 | ||||
| -rw-r--r-- | research/experiments/044-specs/2026-10-13-probes.tsv | 10 | ||||
| -rw-r--r-- | research/experiments/044-specs/probes/p1-byte.aup | 5 | ||||
| -rw-r--r-- | research/experiments/044-specs/probes/p2-bits.aup | 5 | ||||
| -rw-r--r-- | research/experiments/044-specs/probes/p2b-bits.aup | 5 | ||||
| -rw-r--r-- | research/experiments/044-specs/probes/p3-nested.aup | 5 | ||||
| -rw-r--r-- | research/experiments/044-specs/probes/p3b-nested.aup | 8 | ||||
| -rw-r--r-- | research/experiments/044-specs/probes/p4-rec.aup | 2 | ||||
| -rw-r--r-- | research/experiments/044-specs/probes/p5-chars.aup | 7 | ||||
| -rw-r--r-- | research/experiments/044-specs/probes/p5b-chars.aup | 5 | ||||
| -rw-r--r-- | research/experiments/044-specs/probes/p5c-cursor.aup | 7 | ||||
| -rw-r--r-- | research/experiments/044-specs/probes/p6-variant.aup | 2 | ||||
| -rwxr-xr-x | research/experiments/044-specs/run.sh | 13 |
14 files changed, 205 insertions, 0 deletions
diff --git a/CHECKPOINT.md b/CHECKPOINT.md index a3bbca4..71c693f 100644 --- a/CHECKPOINT.md +++ b/CHECKPOINT.md @@ -26,6 +26,7 @@ | 표 크기의 상태 | 목록이 영속 B+트리다(변경·키 탐색·저장본 위치 O(log n), 스냅숏 O(1), 1,600만 항목, 런타임 상태 1 GiB). pgbench의 TPC-B 같은 이체(세 표의 행과 이력, 한 트랜잭션)가 10만 계좌에서 RAM 24.5k/s(전: 3만 계좌 3.2k/s), SD 카드 내구 1,339/s(SQLite WAL FULL 84–153/s) | [090](docs/research/090-tables.md) | | 일반 트랜잭션 | TPC-C의 다섯 트랜잭션을 aup 앱 하나로 쓴다(여러 표 읽기·쓰기, 조각 훑기, 중복 없는 셈, 실패하면 통째 되돌림). 같은 입력에서 SQLite와 아홉 표의 모든 행이 같다(창고 하나와 넷). RAM 초당 40,976건(W=4 35,838; 조율한 SQLite 10,164, 트랜잭션당 CPU 43–50 µs, HTTP·JSON 포함), SD 카드 내구 4,980건(W=4 4,590). SQLite도 카드에 맞게 조율하고 묶어 커밋하면 739건(W=4 426)이다. 남은 차이는 거래당 쓰는 바이트다(SQLite는 페이지째 써서 8–18배) | [092](docs/research/092-tpcc.md), [106](docs/research/106-tpcc-conditions-first.md), [107](docs/research/107-snapshot-nodes-reused.md) | | 질의 | 질의는 앱의 상태 위에 보기를 더한 모듈이다(`aup query`, `PUT·GET /queries/이름`). 검증한 뒤 스냅숏에서 돌고, 열 안의 fold가 그 행을 읽는다(상관 부질의). 잎이 항목을 필드별로 들고, fold와 필터는 잎 하나씩 돌며(결함이 날 잎만 항목별로), 열 안의 그룹·순위 fold는 목록을 한 번 지나 모든 행에 답한다. 10만 계좌에서 지점별 합계 4.9 ms(SQLite 45, 인덱스를 주면 14.3), 조인 0.48 ms(1.47), 자기 조인 순위 6.8 ms(2,840, 인덱스를 주면 7.6). Pure에는 인덱스 선언이 없다 | [091](docs/research/091-queries.md) | +| 방향(1.0 전) | 앱 계약을 1.0에서 얼릴 후보로 적었다: 이벤트는 전함수이고 원자적이며 결정적이다, 시간은 입력이다, 보기는 커밋된 상태의 순수 함수다, 보이는 역사는 커밋의 앞부분이다, 전달은 순서대로 한 번이다. 계산의 언어(명령 90개, 상태 종류 7개)는 패턴의 모음이라 다시 세운다. 분야마다 고른 명세 열한 개의 묶음에서 오늘의 aup는 바이트, 비트 연산, 중첩, 재귀, 갈래, 글자 읽기에 막힌다(탐침 열 개). 1.0 전에는 호환을 챙기지 않고, JSON과 HTTP는 경계에 남는다 | [026](docs/design/026-app-contract.md), [140](docs/research/140-spec-suite.md) | 키로 나눈 소유자와 저장을 넘길 스레드는 하지 않기로 했다. 이 장치는 동기화를 한 줄로 세워, 나누면 쓰기가 23% 줄고 넘겨도 기기의 일은 줄지 않는다([084](docs/research/084-parallel-syncs.md)). 다만 동기화가 공짜인 RAM에서 TPC-C는 소유자 하나가 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의 중단 기준을 따른다. diff --git a/research/experiments/044-specs/2026-10-13-probes.tsv b/research/experiments/044-specs/2026-10-13-probes.tsv new file mode 100644 index 0000000..71b6de0 --- /dev/null +++ b/research/experiments/044-specs/2026-10-13-probes.tsv @@ -0,0 +1,10 @@ +p1-byte.aup p1-byte.aup:4:22: expected newline or semicolon +p2-bits.aup p2-bits.aup:4:10: unexpected character '^' +p2b-bits.aup p2b-bits.aup:4:9: unexpected character '&' +p3-nested.aup p3-nested.aup:2:10: expected a numeric field default +p3b-nested.aup p3b-nested.aup:6:7: a field is a number (field = 0), a bool (field = false), text (field: text) or an i64 (field: i64) +p4-rec.aup p4-rec.aup:1:42: fn 'depth' calls itself (in fn 'depth' called at 2:10) +p5-chars.aup p5-chars.aup:4:12: unknown list 'line.t' +p5b-chars.aup p5b-chars.aup:4:17: expected newline or semicolon +p5c-cursor.aup p5c-cursor.aup:6:12: unknown library 'note'; write use note first +p6-variant.aup p6-variant.aup:2:15: unexpected character '|' diff --git a/research/experiments/044-specs/probes/p1-byte.aup b/research/experiments/044-specs/probes/p1-byte.aup new file mode 100644 index 0000000..0a5ad6e --- /dev/null +++ b/research/experiments/044-specs/probes/p1-byte.aup @@ -0,0 +1,5 @@ +state first = 0 +input packet = message { data: bytes } +on packet { + first = packet.data[0] +} diff --git a/research/experiments/044-specs/probes/p2-bits.aup b/research/experiments/044-specs/probes/p2-bits.aup new file mode 100644 index 0000000..569825f --- /dev/null +++ b/research/experiments/044-specs/probes/p2-bits.aup @@ -0,0 +1,5 @@ +state h = 0 +input word = message { w: u32 } +on word { + h = (h ^ word.w) << 3 +} diff --git a/research/experiments/044-specs/probes/p2b-bits.aup b/research/experiments/044-specs/probes/p2b-bits.aup new file mode 100644 index 0000000..e432668 --- /dev/null +++ b/research/experiments/044-specs/probes/p2b-bits.aup @@ -0,0 +1,5 @@ +state h: i64 = 0 +input word = message { w: i64 } +on word { + h = h & word.w +} diff --git a/research/experiments/044-specs/probes/p3-nested.aup b/research/experiments/044-specs/probes/p3-nested.aup new file mode 100644 index 0000000..c80a343 --- /dev/null +++ b/research/experiments/044-specs/probes/p3-nested.aup @@ -0,0 +1,5 @@ +record Node { + name = "" + children: list of Node +} +state root: list of Node diff --git a/research/experiments/044-specs/probes/p3b-nested.aup b/research/experiments/044-specs/probes/p3b-nested.aup new file mode 100644 index 0000000..105da0a --- /dev/null +++ b/research/experiments/044-specs/probes/p3b-nested.aup @@ -0,0 +1,8 @@ +record Point { + x = 0 + y = 0 +} +record Box { + at: Point +} +state boxes: list of Box diff --git a/research/experiments/044-specs/probes/p4-rec.aup b/research/experiments/044-specs/probes/p4-rec.aup new file mode 100644 index 0000000..753eaff --- /dev/null +++ b/research/experiments/044-specs/probes/p4-rec.aup @@ -0,0 +1,2 @@ +fn depth(n) = if n == 0 { 0 } else { 1 + depth(n - 1) } +view d = depth(3) diff --git a/research/experiments/044-specs/probes/p5-chars.aup b/research/experiments/044-specs/probes/p5-chars.aup new file mode 100644 index 0000000..95f5c6b --- /dev/null +++ b/research/experiments/044-specs/probes/p5-chars.aup @@ -0,0 +1,7 @@ +state count = 0 +input line = message { t: text } +on line { + for c in line.t { + count = count + 1 + } +} diff --git a/research/experiments/044-specs/probes/p5b-chars.aup b/research/experiments/044-specs/probes/p5b-chars.aup new file mode 100644 index 0000000..c5bc23b --- /dev/null +++ b/research/experiments/044-specs/probes/p5b-chars.aup @@ -0,0 +1,5 @@ +state first: text +input line = message { t: text } +on line { + first = line.t[0] +} diff --git a/research/experiments/044-specs/probes/p5c-cursor.aup b/research/experiments/044-specs/probes/p5c-cursor.aup new file mode 100644 index 0000000..97a73f9 --- /dev/null +++ b/research/experiments/044-specs/probes/p5c-cursor.aup @@ -0,0 +1,7 @@ +state note: text +state at: cursor in note +state c: text +input next = key ArrowRight +on next.down { + c = note.char(at) +} diff --git a/research/experiments/044-specs/probes/p6-variant.aup b/research/experiments/044-specs/probes/p6-variant.aup new file mode 100644 index 0000000..35f12fc --- /dev/null +++ b/research/experiments/044-specs/probes/p6-variant.aup @@ -0,0 +1,2 @@ +record Leaf { v = 0 } +state x: Leaf | text = "" diff --git a/research/experiments/044-specs/run.sh b/research/experiments/044-specs/run.sh new file mode 100755 index 0000000..670d0a7 --- /dev/null +++ b/research/experiments/044-specs/run.sh @@ -0,0 +1,13 @@ +#!/bin/sh +# Research 140: compile each probe with aup and print what it says. A probe is +# the first thing a spec in the suite needs (a byte at a position, a bit +# operation, a record inside a record, a call to itself, a variant, a +# character at a position). AUP is the aup checkout (default ../aup beside +# Pure); the output is the evidence table in 140. +set -u +here=$(cd "$(dirname "$0")" && pwd) +aup=${AUP:-$here/../../../../aup}/build/aup +for f in "$here"/probes/*.aup; do + printf '%s\t' "$(basename "$f")" + if out=$("$aup" build "$f" -o /dev/null 2>&1); then echo "compiles"; else echo "$out" | head -1 | sed "s|^$here/probes/||"; fi +done |