From f12346827a136536c5e8e9c6af3da842bd5cc0c3 Mon Sep 17 00:00:00 2001 From: eunhhu Date: Mon, 19 Oct 2026 02:12:51 +0100 Subject: 140 after 027: the ten probes compiled again (run.sh writing to a temporary directory: 10-13's -o /dev/null made a compiled probe say Permission denied): three compile as written, the other seven's diagnostics now mostly naming the form, so the same needs written in 027's forms (probes-027/): a byte an i64, bits on i64s, a record holding itself through a list, a recursive fn in a handler with its result type, a character by for and char, a variant in a list's item all compile; three gaps left, each a change of the core: a view calling a recursive fn or a fn with a block, a record or a variant as a state by itself, a character at a cursor; the suite table's column after 027 (2 and 4 written, 6 and 7 work, the first needs of 1, 3, 5 and 9 compiling, 8's layout as a view blocked by the first gap) --- docs/research/140-spec-suite.md | 60 +++++++++++++++++----- .../044-specs/2026-10-19-probes-027.tsv | 9 ++++ .../experiments/044-specs/2026-10-19-probes.tsv | 10 ++++ .../experiments/044-specs/probes-027/p1-byte.aup | 5 ++ .../experiments/044-specs/probes-027/p2-bits.aup | 5 ++ .../experiments/044-specs/probes-027/p3-nested.aup | 5 ++ .../experiments/044-specs/probes-027/p4-rec.aup | 6 +++ .../044-specs/probes-027/p4b-rec-view.aup | 2 + .../experiments/044-specs/probes-027/p5b-chars.aup | 8 +++ .../044-specs/probes-027/p6-variant.aup | 8 +++ .../044-specs/probes-027/p6b-variant-field.aup | 11 ++++ .../044-specs/probes-027/p7-record-state.aup | 5 ++ research/experiments/044-specs/run.sh | 12 +++-- 13 files changed, 130 insertions(+), 16 deletions(-) create mode 100644 research/experiments/044-specs/2026-10-19-probes-027.tsv create mode 100644 research/experiments/044-specs/2026-10-19-probes.tsv create mode 100644 research/experiments/044-specs/probes-027/p1-byte.aup create mode 100644 research/experiments/044-specs/probes-027/p2-bits.aup create mode 100644 research/experiments/044-specs/probes-027/p3-nested.aup create mode 100644 research/experiments/044-specs/probes-027/p4-rec.aup create mode 100644 research/experiments/044-specs/probes-027/p4b-rec-view.aup create mode 100644 research/experiments/044-specs/probes-027/p5b-chars.aup create mode 100644 research/experiments/044-specs/probes-027/p6-variant.aup create mode 100644 research/experiments/044-specs/probes-027/p6b-variant-field.aup create mode 100644 research/experiments/044-specs/probes-027/p7-record-state.aup 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). 위 표의 여덟 후보 가운데 무엇을 어떤 모양으로 받을지 정한다. diff --git a/research/experiments/044-specs/2026-10-19-probes-027.tsv b/research/experiments/044-specs/2026-10-19-probes-027.tsv new file mode 100644 index 0000000..3163d34 --- /dev/null +++ b/research/experiments/044-specs/2026-10-19-probes-027.tsv @@ -0,0 +1,9 @@ +p1-byte.aup compiles +p2-bits.aup compiles +p3-nested.aup compiles +p4-rec.aup compiles +p4b-rec-view.aup p4b-rec-view.aup:2:10: a view calls no fn with a block, nor one that calls itself: handlers do ('depth') +p5b-chars.aup compiles +p6-variant.aup p6-variant.aup:8:10: state types are numbers, bools, i64, text, cursor or mark in a text, list of a record and index of a list +p6b-variant-field.aup compiles +p7-record-state.aup p7-record-state.aup:5:11: state types are numbers, bools, i64, text, cursor or mark in a text, list of a record and index of a list diff --git a/research/experiments/044-specs/2026-10-19-probes.tsv b/research/experiments/044-specs/2026-10-19-probes.tsv new file mode 100644 index 0000000..3bfd43b --- /dev/null +++ b/research/experiments/044-specs/2026-10-19-probes.tsv @@ -0,0 +1,10 @@ +p1-byte.aup p1-byte.aup:4:22: expected a number, not an i64 +p2-bits.aup p2-bits.aup:4:8: bit operations take i64s, not numbers: convert, as in i64(x) +p2b-bits.aup compiles +p3-nested.aup p3-nested.aup:2:10: expected a numeric field default +p3b-nested.aup compiles +p4-rec.aup p4-rec.aup:2:10: a view calls no fn with a block, nor one that calls itself: handlers do ('depth') +p5-chars.aup compiles +p5b-chars.aup p5b-chars.aup:4:17: a text is read by position through its bytes, as in bytes(t)[i] +p5c-cursor.aup p5c-cursor.aup:6:12: unknown library 'note'; write use note first +p6-variant.aup p6-variant.aup:2:10: state types are numbers, bools, i64, text, cursor or mark in a text, list of a record and index of a list diff --git a/research/experiments/044-specs/probes-027/p1-byte.aup b/research/experiments/044-specs/probes-027/p1-byte.aup new file mode 100644 index 0000000..678c51d --- /dev/null +++ b/research/experiments/044-specs/probes-027/p1-byte.aup @@ -0,0 +1,5 @@ +state first: i64 +input packet = message { data: bytes } +on packet { + first = packet.data[0] +} diff --git a/research/experiments/044-specs/probes-027/p2-bits.aup b/research/experiments/044-specs/probes-027/p2-bits.aup new file mode 100644 index 0000000..1e3fdca --- /dev/null +++ b/research/experiments/044-specs/probes-027/p2-bits.aup @@ -0,0 +1,5 @@ +state h: i64 +input word = message { w: i64 } +on word { + h = (h ^ word.w) << 3 +} diff --git a/research/experiments/044-specs/probes-027/p3-nested.aup b/research/experiments/044-specs/probes-027/p3-nested.aup new file mode 100644 index 0000000..0eb26eb --- /dev/null +++ b/research/experiments/044-specs/probes-027/p3-nested.aup @@ -0,0 +1,5 @@ +record Node { + name: text + children: list of Node +} +state root: list of Node diff --git a/research/experiments/044-specs/probes-027/p4-rec.aup b/research/experiments/044-specs/probes-027/p4-rec.aup new file mode 100644 index 0000000..a725d81 --- /dev/null +++ b/research/experiments/044-specs/probes-027/p4-rec.aup @@ -0,0 +1,6 @@ +fn depth(n) -> number = if n == 0 { 0 } else { 1 + depth(n - 1) } +state d = 0 +input go = key Space +on go.down { + d = depth(3) +} diff --git a/research/experiments/044-specs/probes-027/p4b-rec-view.aup b/research/experiments/044-specs/probes-027/p4b-rec-view.aup new file mode 100644 index 0000000..05dbca1 --- /dev/null +++ b/research/experiments/044-specs/probes-027/p4b-rec-view.aup @@ -0,0 +1,2 @@ +fn depth(n) -> number = if n == 0 { 0 } else { 1 + depth(n - 1) } +view d = depth(3) diff --git a/research/experiments/044-specs/probes-027/p5b-chars.aup b/research/experiments/044-specs/probes-027/p5b-chars.aup new file mode 100644 index 0000000..e81dafd --- /dev/null +++ b/research/experiments/044-specs/probes-027/p5b-chars.aup @@ -0,0 +1,8 @@ +state first: text +input line = message { t: text } +on line { + for c in line.t { + first = char(c) + break + } +} diff --git a/research/experiments/044-specs/probes-027/p6-variant.aup b/research/experiments/044-specs/probes-027/p6-variant.aup new file mode 100644 index 0000000..606b698 --- /dev/null +++ b/research/experiments/044-specs/probes-027/p6-variant.aup @@ -0,0 +1,8 @@ +record Leaf { + v = 0 +} +variant X { + leaf(Leaf) + word(text) +} +state x: X diff --git a/research/experiments/044-specs/probes-027/p6b-variant-field.aup b/research/experiments/044-specs/probes-027/p6b-variant-field.aup new file mode 100644 index 0000000..2b1504a --- /dev/null +++ b/research/experiments/044-specs/probes-027/p6b-variant-field.aup @@ -0,0 +1,11 @@ +record Leaf { + v = 0 +} +variant X { + leaf(Leaf) + word(text) +} +record Holder { + x: X +} +state xs: list of Holder diff --git a/research/experiments/044-specs/probes-027/p7-record-state.aup b/research/experiments/044-specs/probes-027/p7-record-state.aup new file mode 100644 index 0000000..ff339d2 --- /dev/null +++ b/research/experiments/044-specs/probes-027/p7-record-state.aup @@ -0,0 +1,5 @@ +record Point { + x = 0 + y = 0 +} +state at: Point diff --git a/research/experiments/044-specs/run.sh b/research/experiments/044-specs/run.sh index 670d0a7..81de578 100755 --- a/research/experiments/044-specs/run.sh +++ b/research/experiments/044-specs/run.sh @@ -3,11 +3,17 @@ # 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. +# Pure); the output is the evidence table in 140. The probes are as written on +# 2026-10-13 (probes/), or a directory given (probes-027/: the same needs in +# the forms 027 gave them, and the gaps found after it). set -u here=$(cd "$(dirname "$0")" && pwd) aup=${AUP:-$here/../../../../aup}/build/aup -for f in "$here"/probes/*.aup; do +dir=${1:-$here/probes} +dir=$(cd "$dir" && pwd) +out=$(mktemp -d) +trap 'rm -rf "$out"' EXIT +for f in "$dir"/*.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 + if said=$("$aup" build "$f" -o "$out/probe.pmod" 2>&1); then echo "compiles"; else echo "$said" | head -1 | sed "s|^$dir/||"; fi done -- cgit v1.2.3