From 7ffb1145aa11b8c3a691695b3103ee8ae209adc7 Mon Sep 17 00:00:00 2001 From: eunhhu Date: Mon, 19 Oct 2026 13:06:52 +0100 Subject: 029: UAX #14's whole chain and the facts it needs: the handler 38,623 machine instructions a point (event aside) to 564 emitted by hand, 2.5x Vega's C (225; cycles 3.6x), factors 1.46 (dispatch), 3.02 (memory slots and calls), 1.10 (whole numbers), 1.22 (ranges flat), 9.43 (the event's lists typed buffers), 1.23 (Text sharing), the contract left (bounds 1.12, budget and memory 1.39) and the algorithm (1.61); the facts: today's proof licenses exact (each fn's registers, lists and changes: none of the six has lists or changes), then three new (N1 whole numbers, N3 a let list's operations, N4 unchanged after LIST_VALUE) and one analysis widened (N2 the handler's changes); the event itself now the largest layer (1,566 a point: the points decoded into a list, lists cleared and freed, malloc, breaks through the store tree), outside this chain; a premise corrected (the event's lists are FLAT arrays since 021, not trees: the 9.43x is the generic list path); the let lists' factor, broken by a share before, measured as the chain's largest --- docs/design/029-past-one-node.md | 52 ++++++++++++++++++++++++++++++++++------ 1 file changed, 45 insertions(+), 7 deletions(-) (limited to 'docs') diff --git a/docs/design/029-past-one-node.md b/docs/design/029-past-one-node.md index cef1a7b..a7f4966 100644 --- a/docs/design/029-past-one-node.md +++ b/docs/design/029-past-one-node.md @@ -5,8 +5,8 @@ **원리 1은 UAX #14에서 깨졌다(2026-10-19, 045).** 두 실험 모두 막대에 못 미쳤다. (가) 2.19배(막대 4배), (나) 1.31배(막대 3배). 아래 "깨는 실험의 결과"에 무엇을 시험했고 무엇은 시험하지 않았는지 적는다. 깨진 것은 "실행기의 몸을 이어 붙인다"는 -길이다. 표현까지 증명에서 내보내는 것은 range() 하나에서 C의 1.75배였다(잰 점 하나, 앱 전체가 아니다). 원리 2는 아직 시험하지 -않았다. +길이다. 표현까지 증명에서 내보내는 것은 손으로 쓴 점에서 range() 하나가 C의 1.75배, UAX #14의 처리기 전체가 C의 2.5배였다 +(사건 자체의 1,566은 따로 남는다). 원리 2는 아직 시험하지 않았다. ## 쉬운 말로 @@ -134,13 +134,51 @@ C의 속도로 컴파일하기 쉬운 쪽**이어야 한다. 61–183배의 절 옮겨 간다. `ranges`(한 번 싣는다)에는 거의 없지만, 사건마다 바뀌는 리스트에는 재지 않았다. 트리의 잎은 이미 열이다(090). 반복당 122개가 내려가기인지 칸의 일반 경로인지는 가르지 않았다. - 앱의 36%만이다. decide, let 리스트, `Text`의 복사는 이 사슬로 보이지 않았다. -- **고친 것: let 리스트 후보.** 처음 이 자리에 "셈으로 깨졌다(13,000, 32%, 1.5배)"라고 적었다. 그것도 실행기 안의 몫이었다. 그래서 - 인자로서는 재지 않은 채로 남는다. 시험은 몫이 아니라 사슬이다. +- **앱 전체의 사슬(`app.c`, `app-way.h`, 2026-10-19).** `on line`, decide와 그 fn들을 한 번 쓰고, 단마다 매크로를 달리해 펼쳤다. + 모든 단의 답이 18,672줄 모두에서 시험의 답과 같고 exact의 출력과 정확히 같다. 규칙 하나(LB18)를 틀리게 지은 판은 일곱 단 모두 + 6,233줄이 틀려 거부된다. 두 번 돌려 수가 같다. + | 단 | 남은 것 / 지운 것 | 기계 명령/점 | 사이클/점 | 인자 | 허락하는 사실 | + |---|---|---|---|---|---| + | 실행기(사건 1,566 빼고) | | 38,623 | 14,791 | | | + | 이어 붙임(사건 빼고) | 분배를 지움 | 26,523 | 11,079 | 1.46 | | + | exact | 메모리의 칸과 부름의 기계를 지움. double과 검사, FLAT `PureList`(append마다 `list_held`와 `grows`), `Text`의 복사, 트리의 `ranges`, 예산은 남김 | 8,785 | 4,002 | 3.02 | 오늘 증명됨: 스택의 모양과 타입, fn마다의 등록기·리스트·바꾸는 집합 | + | integer | 정수를 정수로 | 7,979 | 3,547 | 1.10 | **N1** 정수임(새로) | + | stored_flat | `ranges`의 열을 평평하게 | 6,561 | 2,800 | 1.22 | **N2** 처리기의 바꾸는 집합(있는 분석을 처리기로 넓힘) | + | local_flat | 사건의 리스트, 점, `out`을 타입 있는 버퍼로(append마다 메모리 셈은 남김) | 696 | 364 | 9.43 | **N3** let 리스트가 받는 연산(덧붙이기, 자리 읽기, 세기뿐: 키 없음, 인덱스 상태 없음)(새). 원소 타입은 정적이고, 정수 열은 N1 | + | shared | `Text`가 버퍼를 함께 씀(복사 없음) | 564 | 317 | 1.23 | **N4** 담은 뒤 바뀌지 않음: `LIST_VALUE` 뒤에 그 리스트도 레코드의 리스트도 바뀌지 않는다(새) | + | unbounded | 경계 검사를 지움 | 502 | 298 | 1.12 | (N5 경계 안임: 막대에 필요 없어 넣지 않음) | + | plain | 예산과 메모리 셈까지 지움: 같은 알고리즘의 C | 362 | 258 | 1.39 | 셈은 계약이라 증명으로 지우지 않는다 | + | Vega의 C | 두 단계 표, 이분 탐색 없음 | 225 | 88 | 1.61 | | + - 인자의 곱 1.46 × 3.02 × 1.10 × 1.22 × 9.43 × 1.23 × 1.12 × 1.39 × 1.61 = 172 = 38,623 / 225. + - **처리기는 38,623 → 564, 68배다. Vega의 C(225)의 2.5배이고, 사이클로는 3.6배다.** 남은 것은 Pure의 계약(경계 검사 1.12배, 예산과 + 메모리 셈 1.39배)과 알고리즘(이분 탐색과 위치마다의 리스트, 1.61배)이다. 미리 정한 막대(shared ≤ plain의 2배)를 지난다(1.56배). + - **사건 자체가 이제 가장 큰 계층이다.** 빈 처리기가 코드 포인트당 1,566이다. 줄 하나에 약 5,140이고, 내보낸 처리기(564)의 2.8배다. + 표본으로는 리스트의 일(점을 사건의 리스트로 풀기, 사건의 리스트를 비우고 놓기) 674, malloc과 free 389, 사건의 기계 386, 상태 + `breaks`를 저장 트리로 쓰기 113이다. 이 사슬은 그것을 지우지 않았다. 지금의 사건을 그대로 두면 메시지 하나의 값은 564 + 1,566 = + 2,130, Vega의 9.5배다. 메시지의 점은 이미 평평한 수의 열인데, 사건이 그것을 리스트로 다시 푼다. 이것이 다음에 볼 겹친 계층이다. + - **전제 하나를 고친다.** let 리스트는 영속 트리가 아니다. 실행기는 사건의 리스트를 처음부터 FLAT 배열로 둔다(021, `pure_list_arrays`: + 담은 것에 맞춰 폭을 고르는 열). 9.43배는 트리가 아니라 범용 리스트의 길에서 온다. append마다 `pure_list_insert`의 폭 고르기와 + 넓히기, `list_held`가 앞뒤로 부르는 함수 여덟, 읽기마다 꼴과 폭의 갈래와 double로의 바꿈이 든다. 트리는 저장 리스트 `ranges`뿐이다. + - **새로 증명할 사실은 셋, 넓힐 분석은 하나다(N1–N4).** 오늘의 증명(스택의 모양과 타입, fn마다의 등록기·리스트·바꾸는 집합)이 exact를 + 허락한다. 이 앱의 fn 여섯은 제 사건 리스트가 없고 아무것도 바꾸지 않으며, 등록기는 부름마다 제 것이라 C의 지역이 된다. 그 위에 + N1 정수임, N3 let 리스트의 연산, N4 담은 뒤 바뀌지 않음은 새로 증명해야 하고, N2는 fn에 하는 분석을 처리기로 넓히면 된다. 확인한 것: + 입력 리스트는 aup가 바꾸지 못하게 한다(언어의 뜻이라 증명이 필요 없다). 담은 뒤 바꾸는 것은 aup가 허락하므로 N4는 지점마다 + 증명해야 한다. + - 단서. + - exact는 소스에서 썼다. C의 `&&`와 `||`는 필요한 데까지만 가고, 읽기마다의 `LIST_BIND`는 없으며, cc가 fn을 인라인할 수 있다. 그래서 + exact는 충실한 내보내기보다 싸다. 이어 붙임 → exact의 인자는 크게, exact 뒤의 인자들은 작게 나왔을 수 있다. + - 단의 차례가 인자를 정한다(곱은 같다). + - 사건의 리스트에 대한 메모리 셈을 append마다 8바이트로 바꾸었다. 지금의 셈은 폭으로 압축한 저장 꼴의 바이트이고, 구현에 따라 + 정해진다. 셈의 정의를 꼴과 무관하게 정하는 것은 계약의 결정이다. + - 평평한 `ranges`의 값은 바뀔 때로 옮겨 간다(재지 않음). + - UAX #14 하나다. DNS, HTTP, inflate, JSON은 바이트와 텍스트와 재귀의 섞임이 달라, 인자를 옮겨 말하지 않는다. +- **고친 것: let 리스트 후보.** 처음 이 자리에 "셈으로 깨졌다(13,000, 32%, 1.5배)"라고 적었다. 그것은 실행기 안의 몫이었다. 위의 사슬에서 + 인자로 재니 9.43배이고, 사슬에서 가장 큰 인자다. - **고친 것: 막대의 셈.** "명령 하나가 기계 명령 하나여도 C의 2.5배"라고 적었다. 명령의 수가 바닥이라고 본 것인데, range()의 both는 실행된 명령 269.5개를 기계 명령 226개로 한다(하나에 0.84). 레지스터 아래에서 옮김과 상수가 사라진다. 그 셈은 틀렸다. -- **원리 1이 지금 말하는 것.** 시험한 길(실행기의 몸을 이어 붙이기)은 죽었다(앱 1.43배, range() 1.78배). 시험하지 않았던 주장(표현까지 - 포함해 증명에서 내보내기)에 잰 점이 하나 생겼다. range()에서 C의 1.75배다. 정수임은 증명에 새로 넣어야 하고, 경계 검사와 예산이 - 남는다. 새 원리가 아니라, 미리 정한 막대 아래의 점 하나다. +- **원리 1이 지금 말하는 것.** 시험한 길(실행기의 몸을 이어 붙이기)은 죽었다(앱 1.43배, range() 1.78배). 표현까지 포함해 증명에서 + 내보내는 것은 UAX #14의 처리기에서 C의 2.5배(사이클 3.6배)다. 새 사실 셋과 넓힌 분석 하나가 필요하고, 계약(검사와 셈)과 알고리즘이 + 남는다. 사건 자체(1,566)는 이 길 밖이다. 손으로 쓴 점 하나이지, 지은 내보내기가 아니다. ## 원리 2. 커밋이 곧 복제본이다 -- cgit v1.2.3