From de1d30da1203cae9cd857052c339ac026f18cffa Mon Sep 17 00:00:00 2001 From: eunhhu Date: Mon, 19 Oct 2026 13:41:28 +0100 Subject: 045, 029: a message end to end, the event's border written by hand too (app.c's BORDER: rows whole and finite, the budget and memory begun again, the one state the handler changes written apart and made the state's at a faultless end into a buffer no reader holds, events and changes counted; every end answers all 18,672 lines, the broken-rule build refused at both hand ends): machine instructions a code point, the runtime 40,365, its empty handler 1,595, the hand border with shared 592 and with plain 379, Vega's C given the same payload 240: 68x, 2.5x C (cycles 3.2x), the border 1,595 to about 22; what went: the rows rebuilt into a tree each message (pure_list_read's make_tree), 54 states walked five times an event (40 of them t.X's registers), the last event's nested lists, a bytes state set whole through a text's piece tree; no new fact (N2, today's proof, the language, forms chosen) --- docs/design/029-past-one-node.md | 26 +++- .../045-proof-compiler/2026-10-19-message.jsonl | 14 +++ research/experiments/045-proof-compiler/app.c | 137 ++++++++++++++++++++- 3 files changed, 174 insertions(+), 3 deletions(-) create mode 100644 research/experiments/045-proof-compiler/2026-10-19-message.jsonl diff --git a/docs/design/029-past-one-node.md b/docs/design/029-past-one-node.md index 5f2c7bb..93c2752 100644 --- a/docs/design/029-past-one-node.md +++ b/docs/design/029-past-one-node.md @@ -176,13 +176,37 @@ C의 속도로 컴파일하기 쉬운 쪽**이어야 한다. 61–183배의 절 정해진다. 셈의 정의를 꼴과 무관하게 정하는 것은 계약의 결정이다. - 평평한 `ranges`의 값은 바뀔 때로 옮겨 간다(재지 않음). - UAX #14 하나다. DNS, HTTP, inflate, JSON은 바이트와 텍스트와 재귀의 섞임이 달라, 인자를 옮겨 말하지 않는다. +- **메시지 끝에서 끝(`app.c`의 BORDER, 2026-10-19).** 사건의 테두리도 손으로 썼다. 런타임의 `pure_app_message`와 같은 페이로드를 + 받고, 상태 `breaks`에 답을 남긴다. 모든 끝이 18,672줄 모두에서 시험의 답과 같다. 틀린 규칙 판은 손으로 쓴 끝 둘도 거부된다. + | 끝 | 기계 명령/점 | 사이클/점 | 줄 하나에 | + |---|---|---|---| + | 런타임(실행기) | 40,365 | 15,525 | 132,262 | + | 런타임, 빈 처리기(사건만) | 1,595 | 664 | 5,268 | + | 손으로 쓴 테두리 + shared | 592 | 292 | 1,944 | + | 손으로 쓴 테두리 + plain | 379 | 238 | 1,245 | + | 같은 페이로드를 받는 Vega의 C | 240 | 91 | 787 | + - **끝에서 끝 40,365 → 592, 68배다. 같은 페이로드를 받는 C(240)의 2.5배이고, 사이클로는 3.2배다.** 테두리는 1,595에서 약 22(줄 하나에 + 약 72)로 준다. + - 테두리가 남기는 뜻은 이것뿐이다. 행이 온전하고 수마다 유한한지 본다(`place_fields`, `decode_cell`). 일의 예산과 메모리 셈을 다시 + 시작한다. 처리기가 바꾸는 단 하나의 상태(`breaks`, N2)를 따로 쓰고, 오류 없이 끝날 때만 상태의 것으로 만든다(그 상태 하나에 대한 + pending과 되돌리기). 읽는 이가 쥐지 않은 버퍼에 쓰고, 쥐고 있으면 새 버퍼를 잡는다. 사건과 바뀜을 센다. 저장소가 없는 앱이다(여기 + 런타임과 같다). 저장은 원리 2의 일이다. + - 지운 것. 메시지의 행을 메시지마다 트리로 다시 짓기(`pure_list_read`의 `make_tree`와 행마다의 `pure_list_insert`). 상태 54개를 사건마다 + 다섯 번 훑기(pending 복사, 되복사, 버스트 열기와 닫기, settle). 그 가운데 40개는 `t.X` 읽기의 등록기다. 지난 사건의 중첩 리스트 놓기. + 통째로만 바뀌는 bytes 상태를 텍스트 편집의 조각 트리(`pure_draft_splice`)로 쓰기. + - 새 사실은 없다. 테두리가 지운 것은 N2(처리기가 바꾸는 것은 `breaks`뿐)와 오늘의 증명(등록기는 부름마다 제 것), 언어의 뜻(입력은 + 바뀌지 않는다), 표현의 결정(행은 페이로드에서 읽고, bytes 상태는 버퍼)이 허락한다. 그래서 끝에서 끝까지 새로 증명할 사실은 + 여전히 N1과 N4, 넓힐 분석은 N2다. + - 단서. 손으로 쓴 판의 수는 하네스를 다시 지을 때마다 1% 안에서 움직인다(인라인의 결정). shared는 이번 빌드에서 570이었다. 런타임의 + 수도 돌릴 때마다 0.2% 안에서 움직인다. 저장소가 붙은 앱은 재지 않았다. - **고친 것: let 리스트 후보.** 처음 이 자리에 "셈으로 깨졌다(13,000, 32%, 1.5배)"라고 적었다. 그것은 실행기 안의 몫이었다. 위의 사슬에서 인자로 재니 9.43배이고, 사슬에서 가장 큰 인자다. - **고친 것: 막대의 셈.** "명령 하나가 기계 명령 하나여도 C의 2.5배"라고 적었다. 명령의 수가 바닥이라고 본 것인데, range()의 both는 실행된 명령 269.5개를 기계 명령 226개로 한다(하나에 0.84). 레지스터 아래에서 옮김과 상수가 사라진다. 그 셈은 틀렸다. - **원리 1이 지금 말하는 것.** 시험한 길(실행기의 몸을 이어 붙이기)은 죽었다(앱 1.43배, range() 1.78배). 표현까지 포함해 증명에서 내보내는 것은 UAX #14의 처리기에서 C의 2.5배(사이클 3.6배)다. 새 사실 둘과 넓힌 분석 하나가 필요하고, 계약(검사와 셈)과 알고리즘이 - 남는다. 사건 자체(1,566)는 이 길 밖이다. 손으로 쓴 점 하나이지, 지은 내보내기가 아니다. + 남는다. 사건의 테두리도 손으로 쓰면 메시지 끝에서 끝이 40,365 → 592, 같은 페이로드를 받는 C의 2.5배다(새 사실 없이). 손으로 쓴 +점 하나이지, 지은 내보내기가 아니다. ## 원리 2. 커밋이 곧 복제본이다 diff --git a/research/experiments/045-proof-compiler/2026-10-19-message.jsonl b/research/experiments/045-proof-compiler/2026-10-19-message.jsonl new file mode 100644 index 0000000..0f8ebe2 --- /dev/null +++ b/research/experiments/045-proof-compiler/2026-10-19-message.jsonl @@ -0,0 +1,14 @@ +{"rung": "exact", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 8784.0, "cycles_per_point": 3989.2, "answers": "the test's, and exact's", "run": 2} +{"rung": "integer", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 7979.0, "cycles_per_point": 3547.1, "answers": "the test's, and exact's", "run": 2} +{"rung": "stored_flat", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 6559.9, "cycles_per_point": 2788.4, "answers": "the test's, and exact's", "run": 2} +{"rung": "local_flat", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 698.1, "cycles_per_point": 364.5, "answers": "the test's, and exact's", "run": 2} +{"rung": "shared", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 570.5, "cycles_per_point": 313.2, "answers": "the test's, and exact's", "run": 2} +{"rung": "unbounded", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 499.8, "cycles_per_point": 296.5, "answers": "the test's, and exact's", "run": 2} +{"rung": "plain", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 365.9, "cycles_per_point": 257.8, "answers": "the test's, and exact's", "run": 2} +{"rung": "vega", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 224.7, "cycles_per_point": 87.9, "answers": "the test's, and exact's", "run": 2} +{"end": "runtime", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 40364.6, "cycles_per_point": 15524.6, "instructions_per_line": 132484.1, "answers": "the test's", "run": 2} +{"end": "runtime_empty_handler", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 1595.2, "cycles_per_point": 664.4, "instructions_per_line": 5235.8, "answers": "the test's", "run": 2} +{"end": "end_to_end_shared", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 592.2, "cycles_per_point": 292.3, "instructions_per_line": 1943.6, "answers": "the test's", "run": 2} +{"end": "end_to_end_plain", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 379.3, "cycles_per_point": 237.6, "instructions_per_line": 1245.1, "answers": "the test's", "run": 2} +{"end": "end_to_end_vega", "lines": 18672, "code_points": 61285, "rounds": 5, "instructions_per_point": 239.9, "cycles_per_point": 90.9, "instructions_per_line": 787.5, "answers": "the test's", "run": 2} +{"what": "built with -DBREAK_ONE_RULE: every hand rung and both hand-written ends refused, 6,233 of 18,672 lines wrong each"} diff --git a/research/experiments/045-proof-compiler/app.c b/research/experiments/045-proof-compiler/app.c index 2c54a8e..7ff4610 100644 --- a/research/experiments/045-proof-compiler/app.c +++ b/research/experiments/045-proof-compiler/app.c @@ -22,7 +22,10 @@ * * cc -O2 -std=gnu17 -I../../../core -I../../../../vega/text app.c ../../../../vega/text/linebreak.c \ * ../../../../vega/text/unicode-data.c ../../../build/libpure.a -lm -pthread -o app - * ./app linebreak.pmod RANGES LINES ROUNDS one JSON line a rung */ + * Then a message end to end (BORDER below): the runtime's pure_app_message (the executor; an empty handler, the event + * alone), the border written by hand around shared and plain, and Vega's C given the same payload. + * + * ./app linebreak.pmod RANGES LINES ROUNDS v0-empty.pmod one JSON line a rung, then one an end */ #define _GNU_SOURCE #include "module.h" #include "module-list.h" @@ -275,6 +278,69 @@ static bool on_line_vega(Context *x, const Points *p, const uint32_t *codes, uin return vega_line_breaks(codes, p->count, got); } +/* ---- A message end to end: the event's border written by hand around a rung's handler. What it keeps of the + * runtime's meaning: the payload's rows whole and each number finite (place_fields, decode_cell); the work budget + * begun again and charged the handler's length (dispatch); the memory counts begun again; the one state the handler + * changes (breaks, its change set: N2) written apart and made the state's only when the handler ends without a fault + * (the pending copy and undo, for that state alone), into the buffer readers do not hold (a snapshot holding it: a new + * one); the events and changes counted. The rows are read where the payload has them (the message cannot change them), + * and breaks is a buffer (the module only ever sets it whole). Without a store (as the runtime here): no save. */ +typedef struct { uint8_t *buffer[2]; size_t room[2], size; unsigned now; bool held[2]; uint64_t events, changes; } BytesState; +enum { HANDLER_LENGTH = 180 }; /* what the handler charges as it begins (its instructions as written: a constant) */ + +#define BORDER(WAYNAME, CHECKED) \ + static bool message_##WAYNAME(Context *x, BytesState *breaks, const unsigned char *payload, size_t size) { \ + if (CHECKED && size % 8) return false; /* rows not whole: LIMIT */ \ + size_t n = size / 8; \ + const double *codes = (const double *)payload; \ + if (CHECKED) \ + for (size_t i = 0; i < n; ++i) \ + if (!isfinite(codes[i])) return false; /* a number that does not fit */ \ + x->fault = false, x->work = 0, x->spent = x->grown = 0; \ + if (CHECKED && HANDLER_LENGTH > x->budget) return false; \ + x->work = HANDLER_LENGTH; \ + unsigned next = breaks->now ^ 1; \ + if (breaks->held[next] || breaks->room[next] < n + 1) { /* a snapshot reads it, or it is too small: another */ \ + size_t room = n + 1 > 2 * breaks->room[next] ? n + 1 : 2 * breaks->room[next]; \ + uint8_t *b = malloc(room); \ + if (!b) return false; \ + if (!breaks->held[next]) free(breaks->buffer[next]); \ + breaks->buffer[next] = b, breaks->room[next] = room, breaks->held[next] = false; \ + } \ + Points p = {NULL, codes, n}; \ + if (!on_line_##WAYNAME(x, &p, breaks->buffer[next]) || x->fault) return false; /* nothing changed */ \ + breaks->now = next, breaks->size = n + 1; \ + ++breaks->events, ++breaks->changes; \ + return true; \ + } +BORDER(shared, true) +BORDER(plain, false) + +/* The same message to Vega's C: its numbers as code points, the boundaries into the state's buffer. */ +static bool message_vega(BytesState *breaks, const unsigned char *payload, size_t size, uint32_t *scratch) { + size_t n = size / 8; + const double *codes = (const double *)payload; + for (size_t i = 0; i < n; ++i) scratch[i] = (uint32_t)codes[i]; + unsigned next = breaks->now ^ 1; + if (breaks->room[next] < n + 1) { + free(breaks->buffer[next]); + if (!(breaks->buffer[next] = malloc(n + 1))) return false; + breaks->room[next] = n + 1; + } + if (!vega_line_breaks(scratch, n, breaks->buffer[next])) return false; + breaks->now = next, breaks->size = n + 1; + ++breaks->events, ++breaks->changes; + return true; +} + +/* Pure's own boundaries, from its view: compared with the test's. */ +typedef struct { const unsigned char *want; size_t at; bool same; } Compare; +static bool compare(void *context, PureSpan span) { + Compare *c = context; + for (size_t i = 0; i < span.size; ++i, ++c->at) c->same = c->same && (span.data[i] != 0) == c->want[c->at]; + return true; +} + /* ---- the harness ---- */ static unsigned char *whole(const char *path, size_t *size) { FILE *f = fopen(path, "rb"); @@ -319,7 +385,7 @@ static bool run(int rung, Context *x, const Line *l, uint8_t *got) { } int main(int argc, char **argv) { - if (argc != 5) { fprintf(stderr, "usage: %s linebreak.pmod RANGES LINES ROUNDS\n", argv[0]); return 2; } + if (argc != 6) { fprintf(stderr, "usage: %s linebreak.pmod RANGES LINES ROUNDS v0-empty.pmod\n", argv[0]); return 2; } size_t ranges_size, lines_size; unsigned char *ranges = whole(argv[2], &ranges_size), *bytes = whole(argv[3], &lines_size); int rounds = atoi(argv[4]); @@ -393,7 +459,9 @@ int main(int argc, char **argv) { bool refused = false; for (int r = 0; r < RUNGS; ++r) if (wrong[r]) fprintf(stderr, "%s: %zu of %zu lines wrong\n", names[r], wrong[r], count), refused = true; +#ifndef BREAK_ONE_RULE /* broken, on to the ends: they must be refused too */ if (refused) return 1; +#endif int ins = counter(PERF_COUNT_HW_INSTRUCTIONS), cyc = counter(PERF_COUNT_HW_CPU_CYCLES); if (ins < 0 || cyc < 0) { perror("perf_event_open"); return 1; } uint64_t total_ins[RUNGS] = {0}, total_cyc[RUNGS] = {0}; @@ -412,6 +480,71 @@ int main(int argc, char **argv) { printf("{\"rung\":\"%s\",\"lines\":%zu,\"code_points\":%zu,\"rounds\":%d,\"instructions_per_point\":%.1f," "\"cycles_per_point\":%.1f,\"answers\":\"the test's, and exact's\"}\n", names[r], count, points, rounds, total_ins[r] / n, total_cyc[r] / n); + /* A message end to end: the runtime (the executor, and an empty handler: the event alone), the border written by + * hand around shared and plain, and Vega's C on the same payload. */ + PureModule empty_module = {0}; + PureApp empty; + if (pure_module_read(argv[5], &empty_module, error, sizeof(error)) != PURE_OK) { fprintf(stderr, "%s\n", error); return 1; } + if (pure_app_start(&empty, &empty_module, (PureData){0}) != PURE_OK || + pure_app_message(&empty, (uint32_t)pure_module_input(&empty_module, "load"), (PureSpan){ranges, ranges_size}) != PURE_OK) + return 1; + int line = pure_module_input(&module, "line"), empty_line = pure_module_input(&empty_module, "line"); + int boundaries = pure_module_view(&module, "boundaries"); + if (line < 0 || empty_line < 0 || boundaries < 0) return 1; + unsigned char **payloads = malloc(count * sizeof(*payloads)); + for (size_t k = 0; k < count; ++k) { + size_t n = lines[k].points.count; + payloads[k] = malloc(8 * n + 8); + memcpy(payloads[k], lines[k].points.codes, 8 * n); /* the message: each point's code, a number (8 bytes) */ + } + static BytesState breaks[3]; + static uint32_t scratch[4096]; + enum { ENDS = 5 }; + const char *ends[ENDS] = {"runtime", "runtime_empty_handler", "end_to_end_shared", "end_to_end_plain", "end_to_end_vega"}; + size_t wrong_ends[ENDS] = {0}; + for (size_t k = 0; k < count; ++k) { /* checked first: each end's boundaries the test's */ + const Line *l = &lines[k]; + size_t size = 8 * l->points.count; + Compare c = {l->want, 0, true}; + c.same = pure_app_message(&app, (uint32_t)line, (PureSpan){payloads[k], size}) == PURE_OK && + pure_app_view_text(&app, (uint32_t)boundaries, compare, &c) == PURE_OK && c.at == l->points.count + 1; + wrong_ends[0] += !c.same; + wrong_ends[1] += pure_app_message(&empty, (uint32_t)empty_line, (PureSpan){payloads[k], size}) != PURE_OK; + for (int e = 2; e < ENDS; ++e) { + BytesState *b = &breaks[e - 2]; + bool done = e == 2 ? message_shared(&x, b, payloads[k], size) : e == 3 ? message_plain(&x, b, payloads[k], size) + : message_vega(b, payloads[k], size, scratch); + bool same = done && b->size == l->points.count + 1; + for (size_t i = 0; same && i < b->size; ++i) same = (b->buffer[b->now][i] != NONE) == l->want[i]; + wrong_ends[e] += !same; + } + } + for (int e = 0; e < ENDS; ++e) + if (wrong_ends[e]) fprintf(stderr, "%s: %zu of %zu lines wrong\n", ends[e], wrong_ends[e], count), refused = true; + if (refused) return 1; + uint64_t end_ins[ENDS] = {0}, end_cyc[ENDS] = {0}; + for (int round = 0; round < rounds; ++round) + for (int e = 0; e < ENDS; ++e) { + ioctl(ins, PERF_EVENT_IOC_RESET, 0), ioctl(cyc, PERF_EVENT_IOC_RESET, 0); + ioctl(ins, PERF_EVENT_IOC_ENABLE, 0), ioctl(cyc, PERF_EVENT_IOC_ENABLE, 0); + for (size_t k = 0; k < count; ++k) { + size_t size = 8 * lines[k].points.count; + switch (e) { + case 0: pure_app_message(&app, (uint32_t)line, (PureSpan){payloads[k], size}); break; + case 1: pure_app_message(&empty, (uint32_t)empty_line, (PureSpan){payloads[k], size}); break; + case 2: message_shared(&x, &breaks[0], payloads[k], size); break; + case 3: message_plain(&x, &breaks[1], payloads[k], size); break; + default: message_vega(&breaks[2], payloads[k], size, scratch); + } + } + ioctl(ins, PERF_EVENT_IOC_DISABLE, 0), ioctl(cyc, PERF_EVENT_IOC_DISABLE, 0); + end_ins[e] += read_counter(ins), end_cyc[e] += read_counter(cyc); + } + for (int e = 0; e < ENDS; ++e) + printf("{\"end\":\"%s\",\"lines\":%zu,\"code_points\":%zu,\"rounds\":%d,\"instructions_per_point\":%.1f," + "\"cycles_per_point\":%.1f,\"instructions_per_line\":%.1f,\"answers\":\"the test's\"}\n", + ends[e], count, points, rounds, end_ins[e] / n, end_cyc[e] / n, end_ins[e] / ((double)count * rounds)); + pure_app_stop(&empty); pure_app_stop(&app); return 0; } -- cgit v1.2.3