diff options
Diffstat (limited to 'docs/research/140-spec-suite.md')
| -rw-r--r-- | docs/research/140-spec-suite.md | 72 |
1 files changed, 70 insertions, 2 deletions
diff --git a/docs/research/140-spec-suite.md b/docs/research/140-spec-suite.md index 6bb2138..4dfffdb 100644 --- a/docs/research/140-spec-suite.md +++ b/docs/research/140-spec-suite.md @@ -28,9 +28,12 @@ - **직접 확인할 것.** `research/experiments/044-specs/run.sh`가 탐침을 컴파일하고 진단을 낸다. - **다음 결정.** 계산의 핵을 설계한다. 여섯 가지와 고정 한도, 상수 시간 암호가 핵이 받아야 할 최소의 후보다. - **027 뒤(2026-10-19).** 핵을 다섯 단계로 다시 세웠다. 탐침의 필요는 셋을 빼고 모두 컴파일된다: 보기에서 재귀 fn을 - 부르기, 레코드나 갈래 하나인 상태, 커서 자리의 글자(아래 "027 뒤의 탐침"). 묶음에서 쓴 것은 2(SHA-256), 4(JSON), 3(inflate)이다. + 부르기, 레코드나 갈래 하나인 상태, 커서 자리의 글자(아래 "027 뒤의 탐침"). 묶음에서 쓴 것은 2(SHA-256), 4(JSON), 3(inflate), + 1(DNS)이다. inflate는 새 명령 없이 써졌고 zlib의 스트림을 모두 맞게 푼다. 다만 우회가 셋(리스트를 받는 fn, 바이트 하나인 상태, 블록 안의 리스트)이고, 줄은 파이썬의 1.6배, 시간은 같은 알고리즘의 C의 108배다. + DNS도 새 명령 없이 써졌고 dnspython의 메시지를 모두 맞게 읽고 다시 쓴다. 우회는 둘(바이트의 `==`, 보기에서의 블록 fn)이고, + 보기에서 블록 fn을 부르지 못하는 틈에 써서 닿은 것은 DNS가 처음이다(배치는 탐침뿐). 줄은 파이썬의 1.6배, 시간은 C의 67배다. ## 묶음 @@ -42,7 +45,7 @@ | # | 명세 | 분야 | 처음 필요한 것 | Pure 안의 검증 | 10-13 | 027 뒤(10-19) | |---|---|---|---|---|---|---| -| 1 | DNS 메시지(RFC 1035) | 와이어 프로토콜 | 바이트 읽고 쓰기, 빅엔디언, 비트 필드, 이름 압축(바이트 안의 참조) | 알려진 구현이 만든 질의·응답 바이트와 대조 | 못 쓴다(바이트, 비트) | 처음 필요한 것(바이트, 비트)이 컴파일된다. 쓰지 않음 | +| 1 | DNS 메시지(RFC 1035) | 와이어 프로토콜 | 바이트 읽고 쓰기, 빅엔디언, 비트 필드, 이름 압축(바이트 안의 참조) | 알려진 구현이 만든 질의·응답 바이트와 대조 | 못 쓴다(바이트, 비트) | 썼다: dnspython의 메시지 400개를 읽고 다시 써 같다. 우회 둘, 줄 수 못 미침, C의 67배(아래) | | 2 | SHA-256(FIPS 180-4) | 해시 | 32비트 낱말, 회전, xor | NIST CAVP의 SHA 벡터 | 우회로만 될 것으로 보인다(써 보지 않음) | 썼다: NIST 벡터를 세 실행 길에서 지난다(1단계) | | 3 | inflate(RFC 1951) | 압축 | 비트 읽기, 허프만 표, 뒤 참조 | zlib로 압축한 말뭉치를 풀어 원본과 비교 | 못 쓴다(바이트, 비트) | 썼다: zlib 스트림 640개, 손상 240개가 파이썬 참조와 같다. 우회 셋, 줄 수 못 미침, C의 108배(아래) | | 4 | JSON(RFC 8259) → 트리와 질의 | 깊이를 모르는 데이터 | 글자 읽기, 중첩, 재귀, 갈래 | JSONTestSuite | 못 쓴다(글자, 중첩, 재귀, 갈래) | 썼다: JSONTestSuite와 무작위 문서가 파이썬과 같다(2a–2c) | @@ -526,6 +529,71 @@ - 그 사이 Pure의 API가 바뀌어(4b, 메시지의 키가 빠졌다) 컴파일되지 않던 시간 도구 넷(`time.c`, `json_time.c`, `json_tree_time.c`, `json_rec_time.c`)의 메시지 부름을 고쳤다. +## 묶음의 1: DNS 메시지 (2026-10-19) + +027 뒤에 둘째로 쓴 명세다. 새 명령도 코어의 C도 없이 aup와 Pure만으로 썼다(aup의 `examples/dns.aup`). +- **읽기는 핸들러다.** 메시지의 바이트를 머리(id, 플래그)와 레코드의 리스트로 읽는다. 이름은 압축을 푼 와이어 꼴(길이를 앞에 둔 + 라벨들과 뿌리)로 둔다. 소유자의 이름과, NS·CNAME·PTR·MX·SOA·SRV 데이터 안의 이름이 그렇다. 다른 데이터는 그대로다. +- **포인터.** 압축 포인터는 앞의 것보다 앞을 가리켜야 한다(dnspython과 같다). 그래서 고리가 생기지 않고 끝난다. +- **쓰기는 보기 `wire`다.** 그 상태에서 메시지의 바이트를 쓰고, 소유자의 이름을 압축한다. 메시지는 상태이고, 와이어는 그 상태의 + 순수 함수다. 그래서 바이트 하나인 상태(inflate의 둘째 우회)에 닿지 않았다. +- **SRV.** dnspython은 RFC 2782와 달리 SRV의 이름도 압축해 쓴다. 알려진 구현이 그렇게 쓰므로, 읽는 쪽이 SRV의 이름도 푼다. + +**맞음.** +- `dns_check.py`: dnspython 2.7.0이 만든 메시지 400개(148,582바이트, 레코드 3,466개)를 세 실행 길에서 읽는다. + - 메시지는 질의와 응답이다. 레코드는 A, AAAA, NS, CNAME, PTR, MX, SOA, TXT, SRV이고, EDNS가 있다. + - 이름은 접미를 나눠 가져 압축이 앞을 가리킨다. 63바이트 라벨, 0x7f 위의 바이트, 245바이트 이름도 있다. + - 머리와 레코드가 dnspython이 읽은 것과 같다. 섹션마다 레코드의 모음으로 견준다. dnspython은 한 이름과 종류의 레코드를 집합 + 하나로 모으므로, 그 차례가 메시지의 차례가 아니다. + - 보기가 다시 쓴 바이트를 dnspython이 같은 메시지로 읽는다. 세 길의 출력은 바이트까지 같다. +- 손상된 메시지 300개(자른 것, 비트 하나를 뒤집은 것)를 같은 길로 읽는 파이썬 참조(`dns_message.py`)와 견준다. 185개는 둘 다 + 거절하고, 115개는 같은 레코드와 같은 다시 쓴 바이트를 낸다. +- Pure의 `make check`(`module_specs`)에 들어갔다. dnspython에 기대지 않도록, 그것이 만든 메시지 200개를 `tests/specs/dns`에 두었다. + - 그 메시지들(레코드 1,780개)을 세 길에서 읽는다. + - 다시 쓴 것을 다시 읽으면 같은 상태와 같은 바이트다. + - 반으로 자른 23개는 이벤트가 실패한다. +- 말뭉치를 만들며 dnspython에 대해 알게 된 것이 둘이다. + - `to_wire`는 RRset 안의 레코드를 시드 없이 섞는다(`want_shuffle`). 끄지 않으면 말뭉치가 실행마다 다르다. + - TTL이 다른 같은 RRset을 합치며 작은 TTL을 고른다(RFC 2181 §5.2). 그래서 생성기는 한 이름과 종류에 TTL 하나를 준다. + +**막대.** + +| 막대 | 잰 것 | | +|---|---|---| +| 쓸 수 있다 | aup와 Pure만. 새 명령 없음 | 지남 | +| 우회가 없다 | 둘(아래): 바이트에 `==`가 없어 한 바이트씩 견준다, 보기가 블록 fn을 부르지 못해 압축을 보기 안에 풀어 쓴다 | **못 미침** | +| 줄 수 ≤ 파이썬 참조 | aup 115줄(닫는 괄호만인 줄 21) 대 파이썬 72줄 | **못 미침** | +| C 대비 시간 | 메시지 400개를 읽고 다시 쓰기, 메시지 바이트당 244 ns. 같은 알고리즘의 C(3.65 ns)의 **67배**. glibc의 해석기는 읽기만 4.4 ns(쓰는 쪽이 없다). 순수 파이썬 131 ns(Pure가 **1.9배 느림**). 기계어 계층(`PURE_JIT=all`)에서 218 ns | 기록(막대 없음) | +| 견고하다 | 위의 맞음, 세 길이 같음, 예산 안에서 끝남. 세 기계는 아직 돌리지 않았다 | 일부 | + +**우회 둘(언어의 틈).** +1. **바이트에 `==`가 없다.** 압축은 앞서 쓴 이름의 접미와 견준다. aup는 바이트의 `==`를 거절하고, Pure의 TEXT_COMPARE는 text만 + 받는다(CONCAT은 인자로 바이트도 받는다). 그래서 보기 안에서 한 바이트씩 견주는 고리를 쓴다. + - 이것은 핵의 일이다. TEXT_COMPARE가 바이트를 받거나(CONCAT처럼 인자로), 같은 뜻의 명령이 있어야 한다. + - 둘 이상의 명세가 필요로 하는가? HTTP/1.1(9)의 머리 이름과 메서드도 바이트를 견줄 것이다. 아직 쓰지 않았다. +2. **보기가 블록 fn을 부르지 못한다**(027 뒤의 탐침의 첫째 틈). 그래서 압축을 fn으로 빼지 못하고 보기 안에 풀어 썼다. + - Pure의 CALL은 핸들러와 함수의 코드에만 있다(008). 그래서 핵의 일이다. + - 써서 이 틈에 닿은 명세는 DNS가 처음이다. 묶음 8(배치)은 탐침에서만 보였다(쓰지 않음). + +**줄을 길게 한 것.** 115 대 72다. 닫는 괄호의 줄을 빼면 94다. +- 닫는 괄호의 줄이 21줄이다. +- 한 바이트씩 견주는 고리가 `==` 하나로 쓸 때보다 9줄 길다. 파이썬은 사전에서 찾는다(`owner[k:] not in seen`). +- 레코드 둘(`Record`, `Seen`)의 선언이 12줄이다. 파이썬은 튜플과 사전이다. +- 상태와 입력의 선언이 4줄이다. + +**시간이 가는 곳.** 메시지 바이트당 Pure 명령이 63.6개이고, 명령 하나에 약 3.8 ns가 든다. +- 읽기(핸들러)가 42%, 쓰기(보기)가 58%다. +- 쓰기의 압축은 앞서 쓴 이름을 차례로 훑으며 바이트마다 견준다. 같은 알고리즘의 C도 차례로 훑지만 `memcmp`로 견준다. 파이썬은 + 사전으로 찾는다. +- 기계어 계층은 시간을 11% 줄인다. 보기의 고리 일부를 컴파일한다(inflate에서는 0%였다). + +**원본.** `research/experiments/044-specs/` +- `dns_message.py`: 파이썬 참조 +- `dns_check.py`: 맞음과 줄 수. 경로를 주면 `dns_time.c`가 읽을 메시지도 쓴다. +- `dns_time.c`: 같은 메시지로 같은 알고리즘의 C, glibc의 해석기, Pure의 시간. Pure와 C가 쓴 바이트가 같아야 잰다. +- `2026-10-19-dns.jsonl`: 잰 수 +- `tests/specs/dns/`: Pure의 검사가 읽는 메시지 200개 + ## 착수 기준 (다음 일) - **바꿀 결정.** 계산의 핵을 설계한다(027). 위 표의 여덟 후보 가운데 무엇을 어떤 모양으로 받을지 정한다. |