diff options
| -rw-r--r-- | docs/design/029-past-one-node.md | 33 | ||||
| -rw-r--r-- | docs/research/140-spec-suite.md | 3 | ||||
| -rw-r--r-- | research/experiments/045-proof-compiler/2026-10-19-ops.txt | 35 |
3 files changed, 69 insertions, 2 deletions
diff --git a/docs/design/029-past-one-node.md b/docs/design/029-past-one-node.md index 88fedf8..7d2f737 100644 --- a/docs/design/029-past-one-node.md +++ b/docs/design/029-past-one-node.md @@ -3,6 +3,9 @@ 작성일: 2026-10-19. 상태: **설계 초안 2판**. 1판(기법 다섯의 나열)은 바깥 피드백 008로 반려했다. 코드는 아직 없다. 이 판은 원리 둘과 열린 질문 하나, 그리고 원리마다 그것을 깰 수 있는 실험 하나만 적는다. +**원리 1은 UAX #14에서 깨졌다(2026-10-19, 045).** 두 실험 모두 막대에 못 미쳤다. (가) 2.19배(막대 4배), (나) 1.31배(막대 +3배). 아래 "깨는 실험의 결과"에 무엇을 시험했고 무엇은 시험하지 않았는지 적는다. 원리 2는 아직 시험하지 않았다. + ## 쉬운 말로 pure link는 전송 세션이 들고 있던 것(순번, 확인, 다시 보내기)을 앱의 outbox와 heard가 이미 들고 있음을 알아보고 세션을 @@ -10,13 +13,15 @@ pure link는 전송 세션이 들고 있던 것(순번, 확인, 다시 보내기 같은 질문을 남은 결함에 던진다. **어느 두 계층이 같은 정보를 들고 있는가, 그리고 어느 쪽을 지울 수 있는가.** - **원리 1.** 검증기가 증명한 것을 실행기 셋이 다시 알아내거나 버린다. 증명을 버리지 않으면 실행기 셋이 사라진다. + **깨졌다(045).** 해석은 절벽의 작은 몫이었다. - **원리 2.** 복제 프로토콜이 들고 다닐 것을 저장소의 커밋과 링크가 이미 들고 있다. 복제 계층이 사라진다. ## 원리 1. 증명이 곧 컴파일러다 **사실.** 140의 느린 명세 다섯(DNS, HTTP, inflate, JSON 트리, UAX #14)은 모두 `runner 2`다. fn이 있으면 블록 전체가 실행기로 -가고, 기계어는 만들어지지 않는다. 실행기에서 센 명령 하나에 3.2–3.9 ns가 든다. UAX #14는 코드 포인트당 명령 1,774개다. C는 -코드 포인트 하나를 35 ns에 끝낸다. +가고, 기계어는 만들어지지 않는다. UAX #14는 코드 포인트 하나에 6,445 ns, C는 35 ns다. +- 정정(045). 이 자리에 처음 적은 "코드 포인트당 명령 1,774개, 명령 하나에 3.2–3.9 ns"는 일의 예산이 센 수였다. 예산은 블록을 쓰인 + 대로 센다. 실행기가 실제로 도는 명령은 코드 포인트당 549.9개이고, 하나에 약 11.7 ns, 기계 명령 74개다. **같은 정보를 든 두 계층.** 검증기는 모듈을 받을 때 모든 자리에서 다음을 증명한다. - 스택의 높이와 각 칸의 타입. 높이가 정적이라 스택의 칸마다 이름 붙은 값으로 바꿀 수 있다. @@ -51,6 +56,30 @@ C의 속도로 컴파일하기 쉬운 쪽**이어야 한다. 61–183배의 절� - 하나라도 못 미치면 이 원리는 이 일에 틀렸고, 그렇게 적는다. 둘 다 지나면 둘만으로 12배다(6,445 → 540 ns 아래, C의 약 15배). - 그다음 남는 것(리스트의 열을 레지스터에 두기)을 잰다. C의 1–3배는 시험할 주장이지 약속이 아니다. +**깨는 실험의 결과(2026-10-19, `research/experiments/045-proof-compiler`).** 둘 다 못 미쳤다. 이 원리는 이 일에 틀렸다. +- 기준. 같은 줄 18,672개(코드 포인트 61,285개)에서 C(Vega의 `text/linebreak.c`)는 코드 포인트당 기계 명령 220개, 사이클 82다. + Pure의 실행기는 40,703개, 15,566이다. 둘 다 줄마다의 답이 기대와 같은지 먼저 확인했다. +- **(가) 명령 수: 2.19배, 막대 4배.** 실행기가 도는 명령을 opcode마다 셌다(`ops-count.patch`). 코드 포인트당 549.9개 가운데 + 레지스터가 지울 옮김(LOCAL_LOAD, LOCAL_STORE, 스택의 PICK과 SLIDE)이 205.5, 상수가 76.7, 한 사건 안에서 같은 리스트·판·필드·자리를 + 다시 읽는 것이 16.4다. 셋을 모두 지워도 251.3이 남는다. + - 전제가 틀렸다. "규칙 마흔 개가 `t.cls[i]`를 저마다 다시 읽는다"고 적었지만, 소스는 그 읽기를 이미 지역에 담는다. 증명만이 + 허락하는 합치기는 16.4개(3%)다. +- **(나) 명령당 시간: 1.31배, 막대 3배.** 실행기의 `step()`을 상수 명령마다 불러 C 컴파일러가 명령마다 몸을 특수화하게 하고, + 기본 블록마다 함수 하나로 이어 붙였다(`stitch.c`, `native-hook.patch`). 답은 같다. 기계 명령 40,703 → 28,601, 사이클 + 15,566 → 11,850이다. + - 시험한 것: 해석(가져오기, 풀기, 갈래)을 지우는 것. `Frame`과 칸은 메모리에 있고, 실행 중의 검사는 그대로다. C 컴파일러는 + 증명을 받지 않았다. + - 이 길은 위가 막혀 있다. 실행된 명령 하나의 기계 명령 74개 가운데 해석이 22개다. 이어 붙이기를 아무리 잘해도 1.42배다. 그래서 + "새 뒤끝 없이 실행기의 몸을 이어 붙인다"는 이 원리의 길은 이 일에서 죽었다. + - 시험하지 않은 것: 증명을 받는 내보내기(칸을 레지스터에, 검사를 지움). 그것은 다른 주장이고, 008이 금한 일반 JIT다. +- **명령이 가는 곳.** 해석이 아니라 런타임의 기계다. + - 앱을 줄인 변형(`events.c`, `variants`)의 코드 포인트당 기계 명령: 빈 처리기 1,583, 위치마다의 리스트를 지으면 22,651이 더, + `Text` 레코드 2,951, `decide` 12,988. + - 연산 하나의 기계 명령(`unit.c`, `units`): 블록 fn의 부름 1,375, 저장 리스트의 자리 읽기 331, 실행기의 산술 고리 한 바퀴 + 248(묶음 실행기는 35). + - 마지막 수는 따로 적는다. 묶음 실행기가 이미 7배를 내는데, 블록 어디에든 fn이 있으면 블록 전체가 실행기로 가서 그것을 잃는다. + 이 원리는 묶음 실행기를 지우자고 했다. 다음 가설은 이 7배를 다시 셈하거나 버린다고 말해야 한다. + ## 원리 2. 커밋이 곧 복제본이다 **같은 정보를 든 두 계층.** 복제 프로토콜은 넷을 들고 다닌다: 상태 변경의 기록을 순서대로, 그 기록의 무결성 검사, 복제본에 diff --git a/docs/research/140-spec-suite.md b/docs/research/140-spec-suite.md index ca5cf83..6ca0c78 100644 --- a/docs/research/140-spec-suite.md +++ b/docs/research/140-spec-suite.md @@ -765,6 +765,9 @@ - `if … { return … }`의 규칙 줄은 파이썬과 거의 한 줄씩 맞는다. **시간이 가는 곳.** 코드 포인트당 Pure 명령이 1,774개이고, 명령 하나에 약 3.9 ns가 든다. +- 정정(045). 1,774는 일의 예산이 센 수다(블록을 쓰인 대로 센다). 실행기가 실제로 도는 명령은 549.9개이고, 하나에 약 11.7 ns, + 기계 명령 74개다. 아래의 나눔도 예산의 수다. 실제로 도는 명령과 기계 명령의 나눔은 [029](../design/029-past-one-node.md)의 + "깨는 실험의 결과"에 있다. - 위치마다의 리스트 아홉 개를 짓고 레코드로 묶는 데 260개다. 레코드를 지을 때 let의 리스트마다 항목을 복사한다(LIST_VALUE). - 범위의 이분 탐색이 360개다(열두 번 남짓 저장 리스트의 항목을 읽는다). C는 종류를 두 단계 표에서 한 번에 읽는다(다른 성질은 이분 탐색). diff --git a/research/experiments/045-proof-compiler/2026-10-19-ops.txt b/research/experiments/045-proof-compiler/2026-10-19-ops.txt new file mode 100644 index 0000000..fd18476 --- /dev/null +++ b/research/experiments/045-proof-compiler/2026-10-19-ops.txt @@ -0,0 +1,35 @@ +CONST 4703032 0 +ADD 700234 0 +SUB 1014832 0 +LT 1104 0 +LE 698524 0 +GT 976466 0 +GE 98373 0 +EQ 1602826 0 +NE 79705 0 +AND 170898 0 +OR 39511 0 +NOT 772197 0 +JZ 4105359 0 +JMP 567474 0 +TEXT_SET 18672 0 +LIST_COUNT 203422 85565 +LIST_APPEND 634309 0 +ITEM_GET 1454991 332863 +ROW 122570 0 +PICK 198855 0 +SLIDE 50563 0 +MOD 18 0 +EACH 18673 0 +LOCAL_LOAD 9230328 0 +LOCAL_STORE 3113793 0 +I64_FROM 42613 0 +LOOP 80835 0 +BREAK 62163 0 +BYTES_OF 18672 0 +LIST_VALUE 168048 0 +LIST_BIND 482333 250353 +CALL 119917 0 +RETURN 119917 0 +FLOORDIV 698524 0 +INDEX_AT 1332421 333613 |