diff options
Diffstat (limited to 'docs/research/140-spec-suite.md')
| -rw-r--r-- | docs/research/140-spec-suite.md | 60 |
1 files changed, 47 insertions, 13 deletions
diff --git a/docs/research/140-spec-suite.md b/docs/research/140-spec-suite.md index 44f4e9f..e0e1b13 100644 --- a/docs/research/140-spec-suite.md +++ b/docs/research/140-spec-suite.md @@ -27,6 +27,8 @@ - **근거.** aup 컴파일러의 실제 진단(아래 표)과 aup·Pure 설계 문서의 연산 목록이다. 시간은 재지 않았다. - **직접 확인할 것.** `research/experiments/044-specs/run.sh`가 탐침을 컴파일하고 진단을 낸다. - **다음 결정.** 계산의 핵을 설계한다. 여섯 가지와 고정 한도, 상수 시간 암호가 핵이 받아야 할 최소의 후보다. +- **027 뒤(2026-10-19).** 핵을 다섯 단계로 다시 세웠다. 탐침의 필요는 셋을 빼고 모두 컴파일된다: 보기에서 재귀 fn을 + 부르기, 레코드나 갈래 하나인 상태, 커서 자리의 글자(아래 "027 뒤의 탐침"). 묶음에서 쓴 것은 2(SHA-256)와 4(JSON)다. ## 묶음 @@ -36,19 +38,19 @@ - 배치는 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 밖(설계상, 아래) | +| # | 명세 | 분야 | 처음 필요한 것 | Pure 안의 검증 | 10-13 | 027 뒤(10-19) | +|---|---|---|---|---|---|---| +| 1 | DNS 메시지(RFC 1035) | 와이어 프로토콜 | 바이트 읽고 쓰기, 빅엔디언, 비트 필드, 이름 압축(바이트 안의 참조) | 알려진 구현이 만든 질의·응답 바이트와 대조 | 못 쓴다(바이트, 비트) | 처음 필요한 것(바이트, 비트)이 컴파일된다. 쓰지 않음 | +| 2 | SHA-256(FIPS 180-4) | 해시 | 32비트 낱말, 회전, xor | NIST CAVP의 SHA 벡터 | 우회로만 될 것으로 보인다(써 보지 않음) | 썼다: NIST 벡터를 세 실행 길에서 지난다(1단계) | +| 3 | inflate(RFC 1951) | 압축 | 비트 읽기, 허프만 표, 뒤 참조 | zlib로 압축한 말뭉치를 풀어 원본과 비교 | 못 쓴다(바이트, 비트) | 처음 필요한 것(바이트, 비트)이 컴파일된다. 쓰지 않음 | +| 4 | JSON(RFC 8259) → 트리와 질의 | 깊이를 모르는 데이터 | 글자 읽기, 중첩, 재귀, 갈래 | JSONTestSuite | 못 쓴다(글자, 중첩, 재귀, 갈래) | 썼다: JSONTestSuite와 무작위 문서가 파이썬과 같다(2a–2c) | +| 5 | UTF-8과 줄 나누기(UAX #14) | 텍스트 | 바이트, 코드 포인트, 속성 표 | Unicode의 `LineBreakTest.txt` | 못 쓴다(글자) | 글자 읽기가 컴파일된다(2c). 쓰지 않음 | +| 6 | 관계 질의, 그래프 탐색 | 데이터 모델 | 리스트, 키, 접기, 이벤트의 리스트 | TPC-C, 은행 질의, 파이썬 모델 | 된다(기준선: [092](092-tpcc.md), 040의 은행 질의, aup `routes.aup`) | 된다. TPC-C가 SQLite와 오차 없이 같다(5단계) | +| 7 | 텍스트 편집 | UI 개념 | text, 커서 | 편집기의 참조 모델 대조(aup `make check`) | 된다 | 된다 | +| 8 | 상자 배치(flex 같은) | UI 개념 | 중첩, 재귀 | 기존 배치 구현(Yoga, Taffy)의 결과와 대조 | 못 쓴다(중첩, 재귀) | 중첩과 재귀는 핸들러에서 된다. 보기에서 재귀 fn을 부르지 못한다(탐침). 쓰지 않음 | +| 9 | HTTP/1.1 요청을 패킷마다(RFC 9112) | 스트림의 상태 기계 | 바이트, 이벤트를 넘는 상태 | 경계를 아무 데서나 자른 요청 모음 | 못 쓴다(바이트). 지금은 `serve/`의 C다 | 처음 필요한 것(바이트)이 컴파일된다. 쓰지 않음 | +| 10 | 재시도, 물러서기, 시간 제한 | 시간 | 시각, 한 번의 타이머 | 시각을 준 시뮬레이션 | 우회(주기 틱 `every`와 `now`) | 다시 보지 않음 | +| 11 | X25519, ChaCha20-Poly1305 | 상수 시간 암호 | 데이터에 따라 달라지지 않는 시간 | RFC 7748, RFC 8439의 벡터 | aup 밖(설계상, 아래) | 그대로(설계상 aup 밖) | **11은 핵의 원시 연산으로 둔다(가설).** 실행기의 시간은 데이터에 따라 달라진다. 묶음 실행기도 결함이 나면 묶음을 처음부터 실행기로 다시 돈다. 그래서 상수 시간을 언어로 약속하기 어렵다. 지금도 암호는 `link/`의 C와 OpenSSL에 있다. @@ -424,6 +426,38 @@ - 접기 안에서 리스트 필드의 `.count`를 읽는 것(`sum(c.cards.count for c in cols)`)은 거절된다. 접기는 레지스터를 묶지 않기 때문이다. - `for c in columns[i].cards`는 구문이 받지 않는다. `let col = columns[i]`로 한 번 거친다. +## 027 뒤의 탐침 (2026-10-19) + +027의 다섯 단계 뒤에 같은 탐침을 다시 컴파일했다(`run.sh`, `2026-10-19-probes.tsv`). 10-13의 열 개 가운데 셋(`p2b-bits`, +`p3b-nested`, `p5-chars`)이 그대로 컴파일된다. 나머지 일곱의 진단은 이제 대부분 쓰는 꼴을 가리킨다. 그래서 같은 필요를 027이 +준 꼴로 다시 썼다(`probes-027/`, `run.sh probes-027`, `2026-10-19-probes-027.tsv`). 그 사이에 드러난 틈도 탐침으로 더했다. +(10-13의 `run.sh`는 `-o /dev/null`로 써서, 컴파일된 모듈을 옆에 쓰려다 `Permission denied`를 냈다. 이제 임시 디렉터리에 쓴다.) + +| 필요 | 10-13 | 10-19, 그때의 꼴 그대로 | 027이 준 꼴 | 그 꼴의 결과 | +|---|---|---|---|---| +| 바이트의 자리 | 구문 오류 | 바이트는 i64다(수의 상태에 넣지 못한다) | `state first: i64`, `packet.data[0]` | 컴파일된다 | +| 비트 연산 | `^` 모름 | 비트 연산은 i64만 받는다 | i64의 `(h ^ w) << 3` | 컴파일된다 | +| i64의 `&` | `&` 모름 | 컴파일된다 | 그대로 | 컴파일된다 | +| 자신을 담는 레코드 | 기본값 진단 | 같다: `name = ""`는 text 필드가 아니다 | `name: text`, `children: list of Node` | 컴파일된다 | +| 레코드 안의 레코드 | 필드 종류 진단 | 컴파일된다 | 그대로 | 컴파일된다 | +| 자신을 부르는 fn | 부를 수 없음 | 보기는 그런 fn을 부르지 못한다 | 핸들러에서, 결과 타입을 적어(`-> number`) | 컴파일된다 | +| 보기에서 자신을 부르는 fn | (위와 같은 탐침) | (위) | `view d = depth(3)` | **거절**: 보기는 블록 있는 fn도 자신을 부르는 fn도 부르지 않는다 | +| text를 글자로 돌기 | 모르는 리스트 | 컴파일된다 | 그대로 | 컴파일된다 | +| 글자 하나 | 구문 오류 | 자리로는 바이트로 읽는다(`bytes(t)[i]`) | `for c in t`의 첫 `char(c)` | 컴파일된다 | +| 커서 자리의 글자 | 모르는 라이브러리 | 같다 | (027이 준 꼴 없음) | **거절** | +| 갈래 하나인 상태 | `\|` 모름 | 상태의 타입이 아니다 | `variant X { … }`, `state x: X` | **거절**: 상태의 타입이 아니다 | +| 리스트 항목 안의 갈래 | — | — | 레코드의 `x: X`, `state xs: list of Holder` | 컴파일된다 | +| 레코드 하나인 상태 | — | — | `state at: Point` | **거절**: 상태의 타입이 아니다 | + +**가름.** +- 꼴이 바뀐 것(틈이 아니다): 바이트와 비트는 i64(5단계의 수의 모델), 자신을 담는 레코드는 리스트를 거쳐, 글자는 돌기와 `char`, + 재귀는 결과 타입을 적은 핸들러의 fn이다. +- 남은 틈 셋. 027의 핵이 말한 것("상태는 타입 있는 값 하나다", 2c의 남은 것 "보기에서의 부름")과 다르다. + - 보기에서 재귀 fn이나 블록 있는 fn을 부르지 못한다. 트리를 보기로 접는 일(묶음 8의 배치, JSON 트리의 질의)이 핸들러에 가야 한다. + - 레코드나 갈래 하나를 상태로 두지 못한다. 항목 하나의 리스트로 우회한다. + - 커서 자리의 글자를 읽지 못한다. +- 셋 다 핵의 변경이다. 묶음의 명세를 더 쓰며 둘 이상이 필요로 하는지 본 뒤에 정한다(쌓임을 막는 규칙). + ## 착수 기준 (다음 일) - **바꿀 결정.** 계산의 핵을 설계한다(027). 위 표의 여덟 후보 가운데 무엇을 어떤 모양으로 받을지 정한다. |