diff options
| author | eunhhu <[email protected]> | 2026-10-19 12:22:24 +0100 |
|---|---|---|
| committer | eunhhu <[email protected]> | 2026-10-19 12:22:24 +0100 |
| commit | 41f66b0ea63c9a75a872727ad2a22d2f22688869 (patch) | |
| tree | cd9b78c0f66c78612f8cf15ad70ab0c66e6867a8 | |
| parent | adccf5808be0ed55bcaf7a3303dd7016044893c8 (diff) | |
| download | pure-41f66b0ea63c9a75a872727ad2a22d2f22688869.tar.gz pure-41f66b0ea63c9a75a872727ad2a22d2f22688869.zip | |
045: Pure's answers checked for real (cost.c and where.c compared only the C's with the test before; now Pure's boundaries are read from its view, and a wrong variant is refused with 0 lines right); the executor and the stitched build, rebuilt at adccf58, both answer all 18,672 lines, and the stitched build's numbers stand (40,189 to 28,089 machine instructions a point, 1.43x; cycles 1.32x); 029 says so
| -rw-r--r-- | docs/design/029-past-one-node.md | 5 | ||||
| -rw-r--r-- | research/experiments/045-proof-compiler/2026-10-19-break.jsonl | 1 | ||||
| -rw-r--r-- | research/experiments/045-proof-compiler/cost.c | 29 | ||||
| -rw-r--r-- | research/experiments/045-proof-compiler/where.c | 26 |
4 files changed, 37 insertions, 24 deletions
diff --git a/docs/design/029-past-one-node.md b/docs/design/029-past-one-node.md index b3ff26d..f36c913 100644 --- a/docs/design/029-past-one-node.md +++ b/docs/design/029-past-one-node.md @@ -65,8 +65,11 @@ C의 속도로 컴파일하기 쉬운 쪽**이어야 한다. 61–183배의 절� - 전제가 틀렸다. "규칙 마흔 개가 `t.cls[i]`를 저마다 다시 읽는다"고 적었지만, 소스는 그 읽기를 이미 지역에 담는다. 증명만이 허락하는 합치기는 16.4개(3%)다. - **(나) 명령당 시간: 1.31배, 막대 3배.** 실행기의 `step()`을 상수 명령마다 불러 C 컴파일러가 명령마다 몸을 특수화하게 하고, - 기본 블록마다 함수 하나로 이어 붙였다(`stitch.c`, `native-hook.patch`). 답은 같다. 기계 명령 40,703 → 28,601, 사이클 + 기본 블록마다 함수 하나로 이어 붙였다(`stitch.c`, `native-hook.patch`). 기계 명령 40,703 → 28,601, 사이클 15,566 → 11,850이다. + - 답. 처음의 `cost.c`는 C의 답만 기대와 견주고 Pure의 답은 읽지 않았다. 고쳐서 Pure의 답을 보기 `boundaries`에서 읽고(틀린 변형은 + 0줄로 거부한다), 이어 붙인 판을 다시 지어 돌렸다. 둘 다 18,672줄이 모두 맞고, 수는 40,189 → 28,089(1.43배), 사이클 1.32배로 + 같다. - 시험한 것: 해석(가져오기, 풀기, 갈래)을 지우는 것. `Frame`과 칸은 메모리에 있고, 실행 중의 검사는 그대로다. C 컴파일러는 증명을 받지 않았다. - 이 길은 위가 막혀 있다. 실행된 명령 하나의 기계 명령 74개 가운데 해석이 22개다. 이어 붙이기를 아무리 잘해도 1.42배다. 그래서 diff --git a/research/experiments/045-proof-compiler/2026-10-19-break.jsonl b/research/experiments/045-proof-compiler/2026-10-19-break.jsonl index f70a825..7710f47 100644 --- a/research/experiments/045-proof-compiler/2026-10-19-break.jsonl +++ b/research/experiments/045-proof-compiler/2026-10-19-break.jsonl @@ -11,3 +11,4 @@ {"what": "variant v0r: the empty handler and range(p.code) a point (events.c, PURE_JIT=0)", "empty_handler": 1562.6, "range_only": 16051.7, "lists_built": 24211.2, "range_per_point": 14489.1, "range_iterations_per_point": 11.4} {"what": "mechanisms, the app (where.c and where.py: 246,581 samples every 100,003 user instructions, 10 rounds, answers checked)", "machine_instructions_per_point": 40236, "dispatch": 12298, "list_build": 6953, "compute": 5416, "list_read": 5238, "moves": 3601, "call": 2847, "memory": 1609, "unplaced": 1213, "event": 947, "loop": 113} {"what": "mechanisms, variant v0r (range only)", "machine_instructions_per_point": 16089, "dispatch": 6038, "compute": 3697, "list_read": 2729, "moves": 1521, "unplaced": 713, "list_build": 451, "call": 360, "memory": 247, "event": 190, "loop": 144, "floor_divide_and_fmod": 2121} +{"what": "(b) checked again: cost.c now reads Pure's boundaries from its view (it compared only the C's before); the stitched build rebuilt from stitch.c and native-hook.patch at adccf58; both answer all 18,672 lines", "interpreted": {"instructions_per_point": 40189.2, "cycles_per_point": [15398.8, 15433.1]}, "stitched": {"instructions_per_point": 28088.7, "cycles_per_point": [11692.5, 11715.0]}, "instruction_factor": 1.43, "cycle_factor": 1.32, "pure_right": 18672, "lines": 18672} diff --git a/research/experiments/045-proof-compiler/cost.c b/research/experiments/045-proof-compiler/cost.c index 2b300a4..15940d6 100644 --- a/research/experiments/045-proof-compiler/cost.c +++ b/research/experiments/045-proof-compiler/cost.c @@ -13,23 +13,11 @@ #include <stdio.h> #include <stdlib.h> #include <string.h> -#include <time.h> #include <linux/perf_event.h> #include <sys/ioctl.h> #include <sys/syscall.h> #include <unistd.h> -static double now_ns(void) { - struct timespec t; - clock_gettime(CLOCK_MONOTONIC, &t); - return (double)t.tv_sec * 1e9 + (double)t.tv_nsec; -} - -static int by_value(const void *a, const void *b) { - double x = *(const double *)a, y = *(const double *)b; - return (x > y) - (x < y); -} - static unsigned char *whole(const char *path, size_t *size) { FILE *f = fopen(path, "rb"); if (!f) return NULL; @@ -44,7 +32,7 @@ static unsigned char *whole(const char *path, size_t *size) { typedef struct { uint32_t count; const uint32_t *codes; const unsigned char *want; unsigned char *payload; } Line; -/* A line's boundaries from Pure: the bytes state "breaks", compared as breaks or not with want. */ +/* A line's boundaries from Pure: the bytes view "boundaries", compared as breaks or not with want. */ typedef struct { const unsigned char *want; size_t at; bool same; } Compare; static bool compare(void *context, PureSpan span) { Compare *c = context; @@ -95,14 +83,19 @@ int main(int argc, char **argv) { int load = pure_module_input(&module, "load"), line = pure_module_input(&module, "line"); if (pure_app_message(&app, (uint32_t)load, (PureSpan){ranges, ranges_size}) != PURE_OK) return 1; static uint8_t got[4096]; - size_t right = 0; - for (size_t k = 0; k < count; ++k) { /* checked first: both give the test's boundaries */ - bool same = pure_app_message(&app, (uint32_t)line, (PureSpan){lines[k].payload, 8 * (size_t)lines[k].count}) == PURE_OK && - lines[k].count < sizeof(got) && vega_line_breaks(lines[k].codes, lines[k].count, got); + size_t right = 0, pure_right = 0; + int boundaries = pure_module_view(&module, "boundaries"); + for (size_t k = 0; k < count; ++k) { /* checked first: both give the test's boundaries, Pure's read from its view */ + bool same = lines[k].count < sizeof(got) && vega_line_breaks(lines[k].codes, lines[k].count, got); for (uint32_t i = 0; same && i <= lines[k].count; ++i) same = (got[i] != VEGA_BREAK_NONE) == lines[k].want[i]; right += same; + Compare c = {lines[k].want, 0, true}; + c.same = boundaries >= 0 && + pure_app_message(&app, (uint32_t)line, (PureSpan){lines[k].payload, 8 * (size_t)lines[k].count}) == PURE_OK && + pure_app_view_text(&app, (uint32_t)boundaries, compare, &c) == PURE_OK; + pure_right += c.same && c.at == lines[k].count + 1; } - if (right != count) { fprintf(stderr, "right %zu of %zu\n", right, count); return 1; } + if (right != count || pure_right != count) { fprintf(stderr, "right: C %zu, Pure %zu, of %zu\n", right, pure_right, count); return 1; } 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; } volatile unsigned sink = 0; diff --git a/research/experiments/045-proof-compiler/where.c b/research/experiments/045-proof-compiler/where.c index 0764443..6d3799b 100644 --- a/research/experiments/045-proof-compiler/where.c +++ b/research/experiments/045-proof-compiler/where.c @@ -34,6 +34,14 @@ static unsigned char *whole(const char *path, size_t *size) { typedef struct { uint32_t count; const uint32_t *codes; const unsigned char *want; unsigned char *payload; } Line; +/* A line's boundaries from Pure: the bytes view "boundaries", compared as breaks or not with want. */ +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; +} + /* Addresses sampled, counted in an open table. */ enum { SLOTS = 1 << 20, PAGES = 64 }; static uint64_t address[SLOTS], hits[SLOTS]; @@ -92,14 +100,22 @@ int main(int argc, char **argv) { int load = pure_module_input(&module, "load"), line = pure_module_input(&module, "line"); if (pure_app_message(&app, (uint32_t)load, (PureSpan){ranges, ranges_size}) != PURE_OK) return 1; static uint8_t got[4096]; - size_t right = 0; - for (size_t k = 0; k < count; ++k) { /* checked first: Pure gives the test's boundaries */ - bool same = pure_app_message(&app, (uint32_t)line, (PureSpan){lines[k].payload, 8 * (size_t)lines[k].count}) == PURE_OK && - lines[k].count < sizeof(got) && vega_line_breaks(lines[k].codes, lines[k].count, got); + size_t right = 0, pure_right = 0; + int boundaries = pure_module_view(&module, "boundaries"); + for (size_t k = 0; k < count; ++k) { /* checked first: both give the test's boundaries, Pure's read from its view */ + bool same = lines[k].count < sizeof(got) && vega_line_breaks(lines[k].codes, lines[k].count, got); for (uint32_t i = 0; same && i <= lines[k].count; ++i) same = (got[i] != VEGA_BREAK_NONE) == lines[k].want[i]; right += same; + Compare c = {lines[k].want, 0, true}; + c.same = boundaries >= 0 && + pure_app_message(&app, (uint32_t)line, (PureSpan){lines[k].payload, 8 * (size_t)lines[k].count}) == PURE_OK && + pure_app_view_text(&app, (uint32_t)boundaries, compare, &c) == PURE_OK; + pure_right += c.same && c.at == lines[k].count + 1; + } + if ((right != count || pure_right != count) && !getenv("WHERE_VARIANT")) { + fprintf(stderr, "right: C %zu, Pure %zu, of %zu\n", right, pure_right, count); + return 1; } - if (right != count && !getenv("WHERE_VARIANT")) { fprintf(stderr, "right %zu of %zu\n", right, count); return 1; } struct perf_event_attr a; memset(&a, 0, sizeof(a)); a.size = sizeof(a), a.type = PERF_TYPE_HARDWARE, a.config = PERF_COUNT_HW_INSTRUCTIONS, a.disabled = 1, |
