diff options
| -rw-r--r-- | docs/design/008-module-format.md | 72 | ||||
| -rw-r--r-- | prototypes/connections/Makefile | 12 | ||||
| -rw-r--r-- | prototypes/connections/module.c | 294 | ||||
| -rw-r--r-- | prototypes/connections/module.h | 72 | ||||
| -rw-r--r-- | prototypes/connections/pure-run.c | 77 | ||||
| -rw-r--r-- | prototypes/connections/test-module.c | 294 |
6 files changed, 820 insertions, 1 deletions
diff --git a/docs/design/008-module-format.md b/docs/design/008-module-format.md new file mode 100644 index 0000000..616125c --- /dev/null +++ b/docs/design/008-module-format.md @@ -0,0 +1,72 @@ +# Pure 모듈 형식 v1 + +2026-09-25. 상태: scalar 모듈 확정, 구현 `prototypes/connections/module.{h,c}`. + +Pure가 실행하는 앱 정의의 형식이다. JVM이 class 파일 형식을 소유하듯 Pure가 이 형식과 +검증 규칙을 소유한다. 생산자는 [aup](/srv/git/aup.git) 같은 툴체인이다. Pure는 소스·문법을 모르며, +로드할 때 모든 규칙을 확인한 모듈만 실행한다. + +v1은 워크벤치 scalar 앱과 같은 의미를 담는다. f64 상태, 키 입력, 원자적 이벤트 핸들러, +순수한 보기다. 바이트 값과 영속 문서는 v2에서 추가한다. + +## 바이트 배치 + +모든 정수는 little-endian이고, 실수는 IEEE binary64 비트 그대로다. + +| 위치 | 내용 | +|---|---| +| 0 | `PUREMOD1` (8 B) | +| 8 | u16 상태 수, u16 입력 수, u16 보기 수, u16 핸들러 수 | +| 16 | u32 명령 수, u32 문자열 바이트 수 | +| 24 | u32 0, u32 0 (예약) | +| 32 | 상태 × 16 B: u32 이름, u32 0, f64 초기값 | +| | 입력 × 12 B: u32 이름, u32 종류(1 = 키), u32 키 이름 | +| | 보기 × 12 B: u32 이름, u32 시작 명령, u32 명령 수 | +| | 핸들러 × 12 B: u32 이벤트, u32 시작 명령, u32 명령 수 | +| | 명령 × 16 B: u8 opcode, 0 3바이트, u32 인자, f64 값 | +| | 문자열: `[u8 길이][바이트]`의 연속. 이름은 이 영역의 오프셋이다 | + +파일 크기는 위 합과 정확히 같아야 한다. 이벤트 번호는 `frame`이 0, 입력 `i`의 누름이 `1 + 2i`, +뗌이 `2 + 2i`다. 핸들러는 파일 순서대로 실행한다. + +## 명령 + +| opcode | 이름 | 스택 | 의미 | +|---:|---|---|---| +| 0 | CONST | → v | 값(유한)을 넣는다 | +| 1 | LOAD | → v | 상태 `인자`를 읽는다 | +| 2 | DT | → v | 이벤트 시간(frame 1/60, 입력 0). 핸들러 전용 | +| 3–6 | ADD SUB MUL DIV | a b → v | DIV에서 b = 0이면 실패 | +| 7 | NEG | a → v | | +| 8–13 | LT LE GT GE EQ NE | a b → 0/1 | | +| 14–16 | AND OR NOT | | 0이 아니면 참, 양쪽 모두 계산 | +| 17–18 | MIN MAX | a b → v | IEEE 754-2019: −0 < +0 | +| 19 | CLAMP | x lo hi → v | lo > hi이면 실패 | +| 20 | STORE | v → | 상태 `인자`에 쓴다. 핸들러 전용 | +| 21 | JZ | c → | c = 0이면 `인자`로. 핸들러 전용 | +| 22 | JMP | | `인자`로. 핸들러 전용 | + +연산 결과가 유한하지 않으면 실패한다. 실패하면 그 이벤트의 모든 핸들러가 한 일이 취소된다. + +## 로드할 때 검증하는 것 + +- 머리말, 예약 바이트, 명령 패딩이 0인지. 한도(상태 32, 입력 8, 보기 24, 핸들러 64, 명령 512, + 문자열 32 KiB)와 정확한 파일 크기. +- 이름은 ASCII 식별자 1–31바이트. 상태·입력·보기 이름은 한 이름공간에서 겹치지 않는다. + 키는 `Space Enter ArrowLeft ArrowRight ArrowUp ArrowDown KeyA–KeyZ Digit0–Digit9` 중 하나이고 겹치지 않는다. +- 초기값과 CONST 값은 유한하다. 인자·값을 쓰지 않는 명령은 둘 다 0이다(표현이 하나뿐). +- 보기·핸들러의 명령 범위가 모듈 안에 있고, 핸들러 이벤트가 존재한다. +- 각 블록에서: 모든 명령이 도달 가능하고, 분기는 블록 안에서 앞으로만 간다. + 모든 경로가 합류점에서 같은 스택 높이를 갖고, 높이는 0–64다. 핸들러는 0개, 보기는 1개의 값을 남긴다. + 보기에는 DT, STORE, 분기가 없다. + +분기가 앞으로만 가므로 한 번의 순차 검사로 모든 들어오는 경로를 본다. 검증된 모듈을 실행할 때는 +스택 검사가 필요 없고, 이벤트 하나의 실행량은 핸들러 명령 수 이하다. + +## 실행 인스턴스 + +`PureApp`은 모듈 참조와 상태 값(최대 32 × f64)만 가진다(288 B). 이벤트는 상태 사본에서 실행하고 +모두 성공했을 때만 반영한다. `pure_app_replace`는 같은 이름의 상태 값을 유지하고 새 상태에 초기값을 준다. +불러오기·실행·교체 모두 할당하지 않는다. `PureModule`은 고정 용량 11,728 B이다. + +아직 런타임 코어(`runtime.c`)의 작업·예산 모델과 연결하지 않았다. 호스트가 직접 호출한다. diff --git a/prototypes/connections/Makefile b/prototypes/connections/Makefile index a416bee..cce12d3 100644 --- a/prototypes/connections/Makefile +++ b/prototypes/connections/Makefile @@ -3,7 +3,7 @@ CFLAGS ?= -O2 -g CFLAGS += -std=c17 -Wall -Wextra -Wpedantic -Werror BUILD ?= build -.PHONY: all core async-core editor fixed-editor fixed-server fixed-tui source-tui compiler mirror window server async-server document-peer document-server check check-policy check-policy-peer check-portable check-portable-tui check-paged-portable check-tree check-portable-peer check-native-checkpoint check-mirror check-core check-async check-async-server check-async-service-scale check-profile check-fixed-profile check-fixed-server check-service-scale check-tui-profile check-source-tui-profile check-tui check-source-tui check-release check-micro-memory check-hybrid check-flat-export check-copy-range check-peer-profile check-document-server-profile check-window-profile check-document-peer check-document-server FORCE +.PHONY: all core async-core editor fixed-editor fixed-server fixed-tui source-tui compiler mirror window server async-server document-peer document-server check check-policy check-policy-peer check-portable check-portable-tui check-paged-portable check-tree check-module check-portable-peer check-native-checkpoint check-mirror check-core check-async check-async-server check-async-service-scale check-profile check-fixed-profile check-fixed-server check-service-scale check-tui-profile check-source-tui-profile check-tui check-source-tui check-release check-micro-memory check-hybrid check-flat-export check-copy-range check-peer-profile check-document-server-profile check-window-profile check-document-peer check-document-server FORCE CORE = runtime.c STORE ?= store.c FIXED_PROGRAM ?= examples/editor.pure @@ -115,6 +115,16 @@ $(BUILD)/test-async: test-async.c program.c $(CORE) $(HOST) $(HEADERS) | $(BUILD $(BUILD)/test-splice: test-splice.c program.c $(CORE) $(HOST) $(HEADERS) | $(BUILD) $(CC) $(CPPFLAGS) $(CFLAGS) -DPURE_RUNTIME_METRICS -DPURE_STORE_TEST test-splice.c program.c $(CORE) $(HOST) $(LDFLAGS) $(LDLIBS) -o $@ +# Pure module format v1: loader/verifier/executor, its tests and a test host. +$(BUILD)/test-module: test-module.c module.c module.h result.h | $(BUILD) + $(CC) $(CPPFLAGS) $(CFLAGS) test-module.c module.c $(LDFLAGS) -lm $(LDLIBS) -o $@ + +$(BUILD)/pure-run: pure-run.c module.c module.h result.h | $(BUILD) + $(CC) $(CPPFLAGS) $(CFLAGS) pure-run.c module.c $(LDFLAGS) -lm $(LDLIBS) -o $@ + +check-module: $(BUILD)/test-module $(BUILD)/pure-run + $(BUILD)/test-module + $(BUILD)/test-tree-store: test-tree-store.c store-tree.c $(HEADERS) | $(BUILD) $(CC) $(CPPFLAGS) $(CFLAGS) -DPURE_STORE_TEST test-tree-store.c store-tree.c $(LDFLAGS) $(LDLIBS) -o $@ diff --git a/prototypes/connections/module.c b/prototypes/connections/module.c new file mode 100644 index 0000000..1d4d8a7 --- /dev/null +++ b/prototypes/connections/module.c @@ -0,0 +1,294 @@ +#include "module.h" +#include <math.h> +#include <stdio.h> +#include <string.h> + +enum { STATE_BYTES = 16, TABLE_BYTES = 12, OP_BYTES = 16, KEY_INPUT = 1 }; +static const unsigned char magic[8] = {'P','U','R','E','M','O','D','1'}; +/* Operand stack effect per opcode, in PureOpcode order. */ +static const unsigned char pops[PURE_OP_COUNT] = + {0,0,0,2,2,2,2,1,2,2,2,2,2,2,2,2,1,2,2,3,1,1,0}; +static const unsigned char pushes[PURE_OP_COUNT] = + {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,0}; + +static uint32_t read32(const unsigned char *p) { + return (uint32_t)p[0] | (uint32_t)p[1] << 8 | (uint32_t)p[2] << 16 | (uint32_t)p[3] << 24; +} + +static double read_double(const unsigned char *p) { + uint64_t bits = read32(p) | (uint64_t)read32(p + 4) << 32; + double value; + memcpy(&value, &bits, sizeof(value)); + return value; +} + +static bool reject(char *error, size_t size, const char *message, unsigned index) { + if (size) snprintf(error, size, "%s (%u)", message, index); + return false; +} + +static bool key_name(const char *key) { + static const char *const named[] = {"Space", "Enter", "ArrowLeft", "ArrowRight", "ArrowUp", "ArrowDown"}; + for (size_t i = 0; i < sizeof(named) / sizeof(*named); ++i) + if (!strcmp(key, named[i])) return true; + if (!strncmp(key, "Key", 3)) return key[3] >= 'A' && key[3] <= 'Z' && !key[4]; + if (!strncmp(key, "Digit", 5)) return key[5] >= '0' && key[5] <= '9' && !key[6]; + return false; +} + +/* Strings are [u8 length][bytes]; a name is an ASCII identifier of 1..31 bytes. */ +static bool name_at(const unsigned char *strings, uint32_t size, uint32_t offset, + bool identifier, char out[PURE_MODULE_NAME]) { + if (offset >= size) return false; + uint32_t length = strings[offset]; + if (!length || length >= PURE_MODULE_NAME || length > size - offset - 1) return false; + for (uint32_t i = 0; i < length; ++i) { + unsigned char c = strings[offset + 1 + i]; + bool letter = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') || c == '_'; + if (!letter && !(i && c >= '0' && c <= '9') && (identifier || c < 32 || c > 126)) return false; + } + memcpy(out, strings + offset + 1, length); + out[length] = 0; + return true; +} + +static bool merge(int16_t *height, uint32_t at, int value) { + if (height[at] < 0) height[at] = (int16_t)value; + return height[at] == value; +} + +/* Every instruction is reachable, every path meets the same stack height at a + * join, and the block ends with 0 (handler) or 1 (view) values. Branches only + * move forward, so one pass in order sees all incoming edges first. */ +static bool verify_block(const PureModule *m, PureBlock block, bool view, + char *error, size_t size, unsigned index) { + if (block.start > m->code_count || block.length > m->code_count - block.start) + return reject(error, size, "code range outside module", index); + if (view && !block.length) return reject(error, size, "empty view", index); + int16_t height[PURE_MODULE_CODE + 1]; + for (uint32_t i = 0; i <= block.length; ++i) height[i] = -1; + height[0] = 0; + for (uint32_t i = 0; i < block.length; ++i) { + const PureOp *op = &m->code[block.start + i]; + int h = height[i]; + if (h < 0) return reject(error, size, "unreachable instruction", block.start + i); + if (op->op >= PURE_OP_COUNT) return reject(error, size, "unknown opcode", block.start + i); + if (view && (op->op == PURE_OP_DT || op->op >= PURE_OP_STORE)) + return reject(error, size, "view with an effect or branch", block.start + i); + if (h < pops[op->op]) return reject(error, size, "stack underflow", block.start + i); + int next = h - pops[op->op] + pushes[op->op]; + if (next > PURE_MODULE_STACK) return reject(error, size, "stack overflow", block.start + i); + bool uses_arg = op->op == PURE_OP_LOAD || op->op == PURE_OP_STORE || + op->op == PURE_OP_JZ || op->op == PURE_OP_JMP; + if ((!uses_arg && op->arg) || (op->op != PURE_OP_CONST && op->value != 0) || + (op->op == PURE_OP_CONST && !isfinite(op->value))) + return reject(error, size, "non-canonical operand", block.start + i); + if ((op->op == PURE_OP_LOAD || op->op == PURE_OP_STORE) && op->arg >= m->states) + return reject(error, size, "unknown state", block.start + i); + if (op->op == PURE_OP_JZ || op->op == PURE_OP_JMP) { + if (op->arg <= block.start + i || op->arg > block.start + block.length) + return reject(error, size, "branch not forward within its block", block.start + i); + if (!merge(height, op->arg - block.start, next)) + return reject(error, size, "stack height differs at branch target", block.start + i); + } + if (op->op != PURE_OP_JMP && !merge(height, i + 1, next)) + return reject(error, size, "stack height differs at join", block.start + i); + } + if (height[block.length] != (view ? 1 : 0)) + return reject(error, size, view ? "view must leave one value" : "handler must leave no value", index); + return true; +} + +PureResult pure_module_load(const void *bytes, size_t size, PureModule *out, + char *error, size_t error_size) { + const unsigned char *p = bytes; + if (error_size) error[0] = 0; + memset(out, 0, sizeof(*out)); + if (!p || size < PURE_MODULE_HEADER || memcmp(p, magic, sizeof(magic))) + return reject(error, error_size, "not a Pure module v1", 0), PURE_INVALID; + out->states = (uint16_t)(p[8] | p[9] << 8); + out->inputs = (uint16_t)(p[10] | p[11] << 8); + out->views = (uint16_t)(p[12] | p[13] << 8); + out->handlers = (uint16_t)(p[14] | p[15] << 8); + out->code_count = read32(p + 16); + uint32_t strings = read32(p + 20); + if (read32(p + 24) || read32(p + 28)) + return reject(error, error_size, "reserved header bytes", 24), PURE_INVALID; + if (out->states > PURE_MODULE_STATES || out->inputs > PURE_MODULE_INPUTS || + out->views > PURE_MODULE_VIEWS || out->handlers > PURE_MODULE_HANDLERS || + out->code_count > PURE_MODULE_CODE || strings > PURE_MODULE_STRINGS) + return reject(error, error_size, "module exceeds a limit", 8), PURE_LIMIT; + size_t expected = PURE_MODULE_HEADER + (size_t)out->states * STATE_BYTES + + ((size_t)out->inputs + out->views + out->handlers) * TABLE_BYTES + + (size_t)out->code_count * OP_BYTES + strings; + if (size != expected) return reject(error, error_size, "module size", (unsigned)expected), PURE_INVALID; + const unsigned char *at = p + PURE_MODULE_HEADER; + const unsigned char *table = at + (size_t)out->states * STATE_BYTES + + ((size_t)out->inputs + out->views + out->handlers) * TABLE_BYTES; + const unsigned char *text = table + (size_t)out->code_count * OP_BYTES; + for (uint32_t i = 0; i < out->code_count; ++i, table += OP_BYTES) { + if (table[1] || table[2] || table[3]) + return reject(error, error_size, "instruction padding", i), PURE_INVALID; + out->code[i] = (PureOp){.op = table[0], .arg = read32(table + 4), .value = read_double(table + 8)}; + } + for (uint32_t i = 0; i < out->states; ++i, at += STATE_BYTES) { + out->initial[i] = read_double(at + 8); + if (!name_at(text, strings, read32(at), true, out->state_names[i]) || read32(at + 4)) + return reject(error, error_size, "state name", i), PURE_INVALID; + if (!isfinite(out->initial[i])) return reject(error, error_size, "non-finite initial value", i), PURE_INVALID; + } + for (uint32_t i = 0; i < out->inputs; ++i, at += TABLE_BYTES) { + if (!name_at(text, strings, read32(at), true, out->input_names[i])) + return reject(error, error_size, "input name", i), PURE_INVALID; + if (read32(at + 4) != KEY_INPUT || !name_at(text, strings, read32(at + 8), false, out->input_keys[i]) || + !key_name(out->input_keys[i])) return reject(error, error_size, "input key", i), PURE_INVALID; + for (uint32_t k = 0; k < i; ++k) + if (!strcmp(out->input_keys[k], out->input_keys[i])) + return reject(error, error_size, "duplicate key", i), PURE_INVALID; + } + for (uint32_t i = 0; i < out->views; ++i, at += TABLE_BYTES) { + if (!name_at(text, strings, read32(at), true, out->view_names[i])) + return reject(error, error_size, "view name", i), PURE_INVALID; + out->view_code[i] = (PureBlock){read32(at + 4), read32(at + 8)}; + } + for (uint32_t i = 0; i < out->handlers; ++i, at += TABLE_BYTES) { + out->handler[i] = (PureHandler){read32(at), {read32(at + 4), read32(at + 8)}}; + if (out->handler[i].event > 2u * out->inputs) + return reject(error, error_size, "handler event", i), PURE_INVALID; + } + /* States, inputs and views share one namespace. */ + const char *names[PURE_MODULE_STATES + PURE_MODULE_INPUTS + PURE_MODULE_VIEWS]; + size_t count = 0; + for (uint32_t i = 0; i < out->states; ++i) names[count++] = out->state_names[i]; + for (uint32_t i = 0; i < out->inputs; ++i) names[count++] = out->input_names[i]; + for (uint32_t i = 0; i < out->views; ++i) names[count++] = out->view_names[i]; + for (size_t i = 0; i < count; ++i) + for (size_t k = 0; k < i; ++k) + if (!strcmp(names[i], names[k])) return reject(error, error_size, "duplicate name", (unsigned)i), PURE_INVALID; + for (uint32_t i = 0; i < out->views; ++i) + if (!verify_block(out, out->view_code[i], true, error, error_size, i)) return PURE_INVALID; + for (uint32_t i = 0; i < out->handlers; ++i) + if (!verify_block(out, out->handler[i].code, false, error, error_size, i)) return PURE_INVALID; + return PURE_OK; +} + +static int find(const char (*names)[PURE_MODULE_NAME], unsigned count, const char *name) { + for (unsigned i = 0; i < count; ++i) + if (!strcmp(names[i], name)) return (int)i; + return -1; +} + +int pure_module_state(const PureModule *m, const char *name) { return find(m->state_names, m->states, name); } +int pure_module_input(const PureModule *m, const char *name) { return find(m->input_names, m->inputs, name); } +int pure_module_view(const PureModule *m, const char *name) { return find(m->view_names, m->views, name); } + +/* IEEE 754-2019 minimum/maximum on finite values: -0 orders below +0. */ +static double minimum(double a, double b) { return a < b || (a == b && signbit(a)) ? a : b; } +static double maximum(double a, double b) { return a > b || (a == b && !signbit(a)) ? a : b; } + +/* Run a verified block. Stack bounds were proven at load. */ +static PureFault run(const PureModule *m, double *values, PureBlock block, double dt, + double *result, uint32_t *fault_pc) { + double stack[PURE_MODULE_STACK]; + size_t sp = 0; + uint32_t pc = block.start, end = block.start + block.length; + while (pc < end) { + const PureOp *op = &m->code[pc]; + double a, b, value; + switch (op->op) { + case PURE_OP_CONST: stack[sp++] = op->value; ++pc; continue; + case PURE_OP_LOAD: stack[sp++] = values[op->arg]; ++pc; continue; + case PURE_OP_DT: stack[sp++] = dt; ++pc; continue; + case PURE_OP_STORE: values[op->arg] = stack[--sp]; ++pc; continue; + case PURE_OP_JZ: pc = stack[--sp] == 0 ? op->arg : pc + 1; continue; + case PURE_OP_JMP: pc = op->arg; continue; + case PURE_OP_NEG: stack[sp - 1] = -stack[sp - 1]; ++pc; continue; + case PURE_OP_NOT: stack[sp - 1] = stack[sp - 1] == 0; ++pc; continue; + case PURE_OP_CLAMP: { + double high = stack[--sp], low = stack[--sp]; + if (low > high) { *fault_pc = pc; return PURE_FAULT_CLAMP; } + stack[sp - 1] = maximum(low, minimum(stack[sp - 1], high)); + ++pc; + continue; + } + default: break; + } + b = stack[--sp]; + a = stack[sp - 1]; + switch (op->op) { + case PURE_OP_ADD: value = a + b; break; + case PURE_OP_SUB: value = a - b; break; + case PURE_OP_MUL: value = a * b; break; + case PURE_OP_DIV: + if (b == 0) { *fault_pc = pc; return PURE_FAULT_DIVIDE; } + value = a / b; + break; + case PURE_OP_LT: value = a < b; break; + case PURE_OP_LE: value = a <= b; break; + case PURE_OP_GT: value = a > b; break; + case PURE_OP_GE: value = a >= b; break; + case PURE_OP_EQ: value = a == b; break; + case PURE_OP_NE: value = a != b; break; + case PURE_OP_AND: value = a != 0 && b != 0; break; + case PURE_OP_OR: value = a != 0 || b != 0; break; + case PURE_OP_MIN: value = minimum(a, b); break; + default: value = maximum(a, b); break; + } + if (!isfinite(value)) { *fault_pc = pc; return PURE_FAULT_NON_FINITE; } + stack[sp - 1] = value; + ++pc; + } + if (result) *result = stack[0]; + return PURE_FAULT_NONE; +} + +void pure_app_start(PureApp *app, const PureModule *module) { + *app = (PureApp){.module = module, .fault_pc = UINT32_MAX}; + memcpy(app->values, module->initial, sizeof(double) * module->states); +} + +/* All handlers of one event run in module order against a pending copy. */ +static PureResult dispatch(PureApp *app, uint32_t event, double dt) { + const PureModule *m = app->module; + double pending[PURE_MODULE_STATES]; + memcpy(pending, app->values, sizeof(pending)); + app->fault = PURE_FAULT_NONE; + app->fault_pc = UINT32_MAX; + for (uint32_t i = 0; i < m->handlers; ++i) { + if (m->handler[i].event != event) continue; + app->fault = run(m, pending, m->handler[i].code, dt, NULL, &app->fault_pc); + if (app->fault) return PURE_INVALID; + } + memcpy(app->values, pending, sizeof(pending)); + ++app->events; + return PURE_OK; +} + +PureResult pure_app_frame(PureApp *app) { + PureResult result = dispatch(app, 0, 1.0 / 60.0); + if (result == PURE_OK) ++app->ticks; + return result; +} + +PureResult pure_app_input(PureApp *app, uint32_t input, PureEdge edge) { + if (input >= app->module->inputs || (edge != PURE_EDGE_DOWN && edge != PURE_EDGE_UP)) return PURE_INVALID; + return dispatch(app, 1 + 2 * input + (edge == PURE_EDGE_UP), 0); +} + +bool pure_app_view(const PureApp *app, uint32_t view, double *out) { + if (view >= app->module->views) return false; + double values[PURE_MODULE_STATES]; + uint32_t pc; + memcpy(values, app->values, sizeof(values)); + return run(app->module, values, app->module->view_code[view], 0, out, &pc) == PURE_FAULT_NONE; +} + +void pure_app_replace(PureApp *app, const PureModule *module) { + double values[PURE_MODULE_STATES]; + for (uint32_t i = 0; i < module->states; ++i) { + int old = pure_module_state(app->module, module->state_names[i]); + values[i] = old >= 0 ? app->values[old] : module->initial[i]; + } + memcpy(app->values, values, sizeof(double) * module->states); + app->module = module; +} diff --git a/prototypes/connections/module.h b/prototypes/connections/module.h new file mode 100644 index 0000000..ab2d6fc --- /dev/null +++ b/prototypes/connections/module.h @@ -0,0 +1,72 @@ +#ifndef PURE_MODULE_H +#define PURE_MODULE_H +#include "result.h" +#include <stdbool.h> +#include <stddef.h> +#include <stdint.h> + +/* Pure module format v1 (docs/design/008-module-format.md). A toolchain such + * as aup produces it; Pure verifies it completely before anything executes, so + * a loaded module cannot overflow the stack, branch backwards or name a + * missing state. Fixed capacity: no allocation in load, run or replace. */ +enum { + PURE_MODULE_STATES = 32, PURE_MODULE_INPUTS = 8, PURE_MODULE_VIEWS = 24, + PURE_MODULE_HANDLERS = 64, PURE_MODULE_CODE = 512, PURE_MODULE_STACK = 64, + PURE_MODULE_NAME = 32, PURE_MODULE_STRINGS = 32768, PURE_MODULE_HEADER = 32 +}; + +typedef enum { + PURE_OP_CONST, PURE_OP_LOAD, PURE_OP_DT, PURE_OP_ADD, PURE_OP_SUB, PURE_OP_MUL, + PURE_OP_DIV, PURE_OP_NEG, PURE_OP_LT, PURE_OP_LE, PURE_OP_GT, PURE_OP_GE, + PURE_OP_EQ, PURE_OP_NE, PURE_OP_AND, PURE_OP_OR, PURE_OP_NOT, PURE_OP_MIN, + PURE_OP_MAX, PURE_OP_CLAMP, PURE_OP_STORE, PURE_OP_JZ, PURE_OP_JMP, PURE_OP_COUNT +} PureOpcode; + +typedef enum { PURE_EDGE_DOWN, PURE_EDGE_UP } PureEdge; +typedef enum { + PURE_FAULT_NONE, PURE_FAULT_DIVIDE, PURE_FAULT_NON_FINITE, PURE_FAULT_CLAMP +} PureFault; + +typedef struct { double value; uint32_t arg; uint8_t op; } PureOp; +typedef struct { uint32_t start, length; } PureBlock; +typedef struct { uint32_t event; PureBlock code; } PureHandler; + +typedef struct { + uint16_t states, inputs, views, handlers; + uint32_t code_count; + char state_names[PURE_MODULE_STATES][PURE_MODULE_NAME]; + char input_names[PURE_MODULE_INPUTS][PURE_MODULE_NAME]; + char view_names[PURE_MODULE_VIEWS][PURE_MODULE_NAME]; + char input_keys[PURE_MODULE_INPUTS][PURE_MODULE_NAME]; + double initial[PURE_MODULE_STATES]; + PureBlock view_code[PURE_MODULE_VIEWS]; + PureHandler handler[PURE_MODULE_HANDLERS]; + PureOp code[PURE_MODULE_CODE]; +} PureModule; + +/* Decode and verify. On failure out is unspecified and error names the rule. */ +PureResult pure_module_load(const void *bytes, size_t size, PureModule *out, + char *error, size_t error_size); +/* Index of a name, or -1. */ +int pure_module_state(const PureModule *, const char *name); +int pure_module_input(const PureModule *, const char *name); +int pure_module_view(const PureModule *, const char *name); + +/* One app instance: state values of a module. Every event is atomic: on a + * fault the values are exactly those before the event. */ +typedef struct { + const PureModule *module; + double values[PURE_MODULE_STATES]; + PureFault fault; + uint32_t fault_pc; + uint64_t ticks, events; +} PureApp; + +void pure_app_start(PureApp *, const PureModule *); +PureResult pure_app_frame(PureApp *); +PureResult pure_app_input(PureApp *, uint32_t input, PureEdge); +bool pure_app_view(const PureApp *, uint32_t view, double *out); +/* Switch to another verified module. States keep their value by name; new + * states start at their initial value. The module must outlive the app. */ +void pure_app_replace(PureApp *, const PureModule *); +#endif diff --git a/prototypes/connections/pure-run.c b/prototypes/connections/pure-run.c new file mode 100644 index 0000000..9059a1e --- /dev/null +++ b/prototypes/connections/pure-run.c @@ -0,0 +1,77 @@ +#define _POSIX_C_SOURCE 200809L +#include "module.h" +#include <stdio.h> +#include <stdlib.h> +#include <string.h> + +/* Test host for a verified module: reads commands from stdin and prints one + * JSON snapshot per command. Not a product interface. + * down NAME | up NAME | frame [N] | replace PATH | show */ +static const char *const fault_names[] = {"none", "divide", "non_finite", "clamp"}; + +static bool load(const char *path, PureModule *module) { + FILE *file = fopen(path, "rb"); + static unsigned char bytes[1 << 17]; + size_t size = file ? fread(bytes, 1, sizeof(bytes), file) : 0; + bool ok = file && !ferror(file) && size < sizeof(bytes); + if (file) fclose(file); + char error[128]; + if (!ok) { fprintf(stderr, "cannot read %s\n", path); return false; } + if (pure_module_load(bytes, size, module, error, sizeof(error)) != PURE_OK) { + fprintf(stderr, "%s: %s\n", path, error); + return false; + } + return true; +} + +static void show(const PureApp *app, const char *failure) { + const PureModule *m = app->module; + printf("{\"states\":{"); + for (uint32_t i = 0; i < m->states; ++i) + printf("%s\"%s\":%.17g", i ? "," : "", m->state_names[i], app->values[i]); + printf("},\"views\":{"); + for (uint32_t i = 0; i < m->views; ++i) { + double value; + if (pure_app_view(app, i, &value)) printf("%s\"%s\":%.17g", i ? "," : "", m->view_names[i], value); + else printf("%s\"%s\":null", i ? "," : "", m->view_names[i]); + } + printf("},\"tick\":%llu,\"successfulEvents\":%llu,\"fault\":\"%s\",\"error\":%s%s%s}\n", + (unsigned long long)app->ticks, (unsigned long long)app->events, fault_names[app->fault], + failure ? "\"" : "", failure ? failure : "null", failure ? "\"" : ""); +} + +int main(int argc, char **argv) { + static PureModule modules[2]; + if (argc != 2 || !load(argv[1], &modules[0])) { + if (argc != 2) fputs("pure-run MODULE < commands\n", stderr); + return 2; + } + unsigned active = 0; + PureApp app; + pure_app_start(&app, &modules[active]); + char line[4096]; + int status = 0; + while (fgets(line, sizeof(line), stdin)) { + char command[16] = "", argument[4000] = ""; + const char *failure = NULL; + line[strcspn(line, "\r\n")] = 0; + if (sscanf(line, "%15s %3999s", command, argument) < 1) continue; + if (!strcmp(command, "down") || !strcmp(command, "up")) { + int input = pure_module_input(app.module, argument); + if (input < 0) failure = "unknown input"; + else if (pure_app_input(&app, (uint32_t)input, command[0] == 'd' ? PURE_EDGE_DOWN : PURE_EDGE_UP) != PURE_OK) + failure = "event failed"; + } else if (!strcmp(command, "frame")) { + long count = *argument ? strtol(argument, NULL, 10) : 1; + if (count < 1 || count > 600) failure = "frame count"; + for (long i = 0; !failure && i < count; ++i) + if (pure_app_frame(&app) != PURE_OK) failure = "event failed"; + } else if (!strcmp(command, "replace")) { + if (!load(argument, &modules[!active])) failure = "invalid module"; + else { active = !active; pure_app_replace(&app, &modules[active]); } + } else if (strcmp(command, "show")) failure = "unknown command"; + if (failure) status = 1; + show(&app, failure); + } + return status; +} diff --git a/prototypes/connections/test-module.c b/prototypes/connections/test-module.c new file mode 100644 index 0000000..fc0d1d4 --- /dev/null +++ b/prototypes/connections/test-module.c @@ -0,0 +1,294 @@ +#include "module.h" +#include <math.h> +#include <stdio.h> +#include <stdlib.h> +#include <string.h> + +#define CHECK(x) do { if (!(x)) { fprintf(stderr, "%s:%d: %s\n", __FILE__, __LINE__, #x); abort(); } } while (0) + +typedef struct { const char *name; double initial; } S; +typedef struct { const char *name, *key; } I; +typedef struct { const char *name; uint32_t start, length; } V; +typedef struct { uint32_t event, start, length; } H; +typedef struct { uint8_t op; uint32_t arg; double value; } O; +typedef struct { + const S *s; size_t ns; const I *in; size_t ni; const V *v; size_t nv; + const H *h; size_t nh; const O *o; size_t no; +} Spec; + +static unsigned char *put32(unsigned char *p, uint32_t v) { + for (unsigned i = 0; i < 4; ++i) p[i] = (unsigned char)(v >> (8 * i)); + return p + 4; +} + +static unsigned char *put_double(unsigned char *p, double value) { + uint64_t bits; + memcpy(&bits, &value, sizeof(bits)); + put32(p, (uint32_t)bits); + return put32(p + 4, (uint32_t)(bits >> 32)); +} + +/* Test-side encoder for format v1; the toolchain has its own. */ +static size_t build(unsigned char *out, Spec spec) { + unsigned char strings[4096]; + size_t used = 0; + uint32_t offset[256]; + size_t names = 0; + const char *text[256]; + for (size_t i = 0; i < spec.ns; ++i) text[names++] = spec.s[i].name; + for (size_t i = 0; i < spec.ni; ++i) { text[names++] = spec.in[i].name; text[names++] = spec.in[i].key; } + for (size_t i = 0; i < spec.nv; ++i) text[names++] = spec.v[i].name; + for (size_t i = 0; i < names; ++i) { + size_t length = strlen(text[i]); + offset[i] = (uint32_t)used; + strings[used++] = (unsigned char)length; + memcpy(strings + used, text[i], length); + used += length; + } + unsigned char *p = out; + memcpy(p, "PUREMOD1", 8); + p[8] = (unsigned char)spec.ns; p[9] = (unsigned char)(spec.ns >> 8); + p[10] = (unsigned char)spec.ni; p[11] = 0; + p[12] = (unsigned char)spec.nv; p[13] = 0; + p[14] = (unsigned char)spec.nh; p[15] = 0; + put32(p + 16, (uint32_t)spec.no); + put32(p + 20, (uint32_t)used); + memset(p + 24, 0, 8); + p += 32; + size_t n = 0; + for (size_t i = 0; i < spec.ns; ++i) { p = put32(p, offset[n++]); p = put32(p, 0); p = put_double(p, spec.s[i].initial); } + for (size_t i = 0; i < spec.ni; ++i) { p = put32(p, offset[n++]); p = put32(p, 1); p = put32(p, offset[n++]); } + for (size_t i = 0; i < spec.nv; ++i) { p = put32(p, offset[n++]); p = put32(p, spec.v[i].start); p = put32(p, spec.v[i].length); } + for (size_t i = 0; i < spec.nh; ++i) { p = put32(p, spec.h[i].event); p = put32(p, spec.h[i].start); p = put32(p, spec.h[i].length); } + for (size_t i = 0; i < spec.no; ++i) { + *p++ = spec.o[i].op; *p++ = 0; *p++ = 0; *p++ = 0; + p = put32(p, spec.o[i].arg); + p = put_double(p, spec.o[i].value); + } + memcpy(p, strings, used); + return (size_t)(p + used - out); +} + +static PureModule module_a, module_b; +static char error[128]; + +static PureResult load(Spec spec, PureModule *out) { + static unsigned char bytes[65536]; + size_t size = build(bytes, spec); + return pure_module_load(bytes, size, out, error, sizeof(error)); +} + +#define LEN(a) (sizeof(a) / sizeof(*(a))) +#define SPEC(s, in, v, h, o) ((Spec){s, LEN(s), in, LEN(in), v, LEN(v), h, LEN(h), o, LEN(o)}) + +enum { C = PURE_OP_CONST, L = PURE_OP_LOAD, DT = PURE_OP_DT, ADD = PURE_OP_ADD, + MUL = PURE_OP_MUL, DIV = PURE_OP_DIV, GT = PURE_OP_GT, MIN = PURE_OP_MIN, + MAX = PURE_OP_MAX, CL = PURE_OP_CLAMP, ST = PURE_OP_STORE, JZ = PURE_OP_JZ, + JMP = PURE_OP_JMP, NEG = PURE_OP_NEG }; + +static const S counter_states[] = {{"count", 0}, {"x", 3}}; +static const I counter_inputs[] = {{"tap", "Space"}, {"move", "ArrowRight"}}; +static const V counter_views[] = {{"label", 0, 1}, {"width", 1, 6}}; +static const O counter_code[] = { + {L, 0, 0}, /* 0 view label */ + {C, 0, 40}, {L, 0, 0}, {C, 0, 20}, {MIN, 0, 0}, {C, 0, 8}, /* 1 view width */ + {MUL, 0, 0}, + /* 7: fixed-up below: 40 + min(count, 20) * 8 needs an ADD; see width2 */ + {L, 0, 0}, {C, 0, 1}, {ADD, 0, 0}, {ST, 0, 0}, /* 7 tap.down */ + /* 11 move.down: if x > 5 { x = 0 } else { x = x + 1 } */ + {L, 1, 0}, {C, 0, 5}, {GT, 0, 0}, {JZ, 18, 0}, {C, 0, 0}, {ST, 1, 0}, {JMP, 22, 0}, + {L, 1, 0}, {C, 0, 1}, {ADD, 0, 0}, {ST, 1, 0}, + /* 22 frame: x = x + dt */ + {L, 1, 0}, {DT, 0, 0}, {ADD, 0, 0}, {ST, 1, 0}, + /* 26 view width2 = 40 + min(count, 20) * 8 */ + {C, 0, 40}, {L, 0, 0}, {C, 0, 20}, {MIN, 0, 0}, {C, 0, 8}, {MUL, 0, 0}, {ADD, 0, 0}, +}; +static const H counter_handlers[] = {{1, 7, 4}, {3, 11, 11}, {0, 22, 4}}; + +static void behaviour(void) { + /* width at 1..7 leaves two values: rejected at load. */ + CHECK(load(SPEC(counter_states, counter_inputs, counter_views, counter_handlers, counter_code), &module_a) == PURE_INVALID); + CHECK(strstr(error, "view must leave one value")); + static const V views[] = {{"label", 0, 1}, {"width", 26, 7}}; + CHECK(load(SPEC(counter_states, counter_inputs, views, counter_handlers, counter_code), &module_a) == PURE_OK); + PureApp app; + pure_app_start(&app, &module_a); + double value; + CHECK(pure_app_view(&app, 1, &value) && value == 40); + for (int i = 0; i < 25; ++i) CHECK(pure_app_input(&app, 0, PURE_EDGE_DOWN) == PURE_OK); + CHECK(app.values[0] == 25 && pure_app_view(&app, 1, &value) && value == 200); + CHECK(pure_app_input(&app, 0, PURE_EDGE_UP) == PURE_OK && app.events == 26); + /* if / else with forward JZ and JMP */ + CHECK(pure_app_input(&app, 1, PURE_EDGE_DOWN) == PURE_OK && app.values[1] == 4); + CHECK(pure_app_input(&app, 1, PURE_EDGE_DOWN) == PURE_OK && app.values[1] == 5); + CHECK(pure_app_input(&app, 1, PURE_EDGE_DOWN) == PURE_OK && app.values[1] == 6); + CHECK(pure_app_input(&app, 1, PURE_EDGE_DOWN) == PURE_OK && app.values[1] == 0); + CHECK(pure_app_frame(&app) == PURE_OK && app.values[1] == 1.0 / 60.0 && app.ticks == 1); + CHECK(pure_app_input(&app, 2, PURE_EDGE_DOWN) == PURE_INVALID); + CHECK(pure_module_input(&module_a, "move") == 1 && pure_module_view(&module_a, "width") == 1 && + pure_module_state(&module_a, "missing") == -1); + + /* Replacement keeps values by name. */ + static const S next_states[] = {{"fresh", 7}, {"count", 99}}; + static const I no_inputs[1]; + static const V no_views[1]; + static const H no_handlers[1]; + static const O no_code[1]; + CHECK(load((Spec){next_states, 2, no_inputs, 0, no_views, 0, no_handlers, 0, no_code, 0}, &module_b) == PURE_OK); + pure_app_replace(&app, &module_b); + CHECK(app.module == &module_b && app.values[0] == 7 && app.values[1] == 25); + pure_app_replace(&app, &module_a); + CHECK(app.values[0] == 25 && app.values[1] == 3); +} + +/* A fault leaves every state exactly as before the event. */ +static void faults(void) { + static const S states[] = {{"a", 1}, {"b", 2}}; + static const I inputs[] = {{"one", "KeyA"}, {"two", "KeyB"}, {"three", "Digit3"}}; + static const O code[] = { + {C, 0, 9}, {ST, 0, 0}, {C, 0, 1}, {C, 0, 0}, {DIV, 0, 0}, {ST, 1, 0}, /* 0 divide */ + {C, 0, 9}, {ST, 0, 0}, {C, 0, 1e308}, {C, 0, 10}, {MUL, 0, 0}, {ST, 1, 0}, /* 6 overflow */ + {C, 0, 9}, {ST, 0, 0}, {C, 0, 1}, {C, 0, 3}, {C, 0, 2}, {CL, 0, 0}, {ST, 1, 0}, /* 12 clamp */ + {C, 0, 5}, {ST, 0, 0}, /* 19 ok */ + {C, 0, 0}, {NEG, 0, 0}, {C, 0, 0}, {MIN, 0, 0}, /* 21 view -0 */ + {C, 0, 0}, {C, 0, 0}, {NEG, 0, 0}, {MAX, 0, 0}, /* 25 view +0 */ + }; + static const H handlers[] = {{1, 0, 6}, {3, 6, 6}, {5, 12, 7}, {5, 19, 2}}; + static const V views[] = {{"low", 21, 4}, {"high", 25, 4}}; + CHECK(load(SPEC(states, inputs, views, handlers, code), &module_a) == PURE_OK); + PureApp app; + pure_app_start(&app, &module_a); + const PureFault expected[] = {PURE_FAULT_DIVIDE, PURE_FAULT_NON_FINITE, PURE_FAULT_CLAMP}; + for (uint32_t i = 0; i < 3; ++i) { + CHECK(pure_app_input(&app, i, PURE_EDGE_DOWN) == PURE_INVALID && app.fault == expected[i]); + CHECK(app.values[0] == 1 && app.values[1] == 2 && app.events == 0); + } + /* A later handler of the same event does not run after a fault. */ + CHECK(app.fault_pc == 17); + double value; + CHECK(pure_app_view(&app, 0, &value) && value == 0 && signbit(value)); + CHECK(pure_app_view(&app, 1, &value) && value == 0 && !signbit(value)); +} + +typedef struct { const char *reason; Spec spec; PureResult result; } Rejection; + +static void rejections(void) { + static const S s1[] = {{"a", 0}}; + static const S dup[] = {{"a", 0}, {"a", 1}}; + static const S bad_name[] = {{"1a", 0}}; + static const S long_name[] = {{"abcdefghijklmnopqrstuvwxyz012345", 0}}; + static const S non_finite[] = {{"a", INFINITY}}; + static const I i1[] = {{"k", "Space"}}; + static const I bad_key[] = {{"k", "KeyAA"}}; + static const I dup_key[] = {{"k", "Space"}, {"j", "Space"}}; + static const V clash[] = {{"a", 0, 1}}; + static const V v_store[] = {{"v", 0, 2}}; + static const V v_dt[] = {{"v", 2, 1}}; + static const V v_empty[] = {{"v", 0, 0}}; + static const H none[1]; + static const O load_a[] = {{L, 0, 0}}; + static const O store[] = {{C, 0, 1}, {ST, 0, 0}, {DT, 0, 0}}; + static const H h0[] = {{0, 0, 2}}; + static const H h_bad_event[] = {{3, 0, 2}}; + static const O back[] = {{C, 0, 1}, {JZ, 0, 0}}; + static const O beyond[] = {{C, 0, 1}, {JZ, 3, 0}}; + static const O under[] = {{ADD, 0, 0}}; + static const O join[] = {{C, 0, 1}, {JZ, 4, 0}, {C, 0, 1}, {C, 0, 1}, {ST, 0, 0}}; + static const O leftover[] = {{C, 0, 1}, {C, 0, 2}}; + static const O unknown_state[] = {{L, 1, 0}, {ST, 0, 0}}; + static const O nan_const[] = {{C, 0, NAN}, {ST, 0, 0}}; + static const O noncanon[] = {{C, 0, 1}, {NEG, 1, 0}, {ST, 0, 0}}; + static const O unreachable[] = {{JMP, 2, 0}, {C, 0, 1}, {C, 0, 1}, {ST, 0, 0}}; + static const O bad_op[] = {{99, 0, 0}, {ST, 0, 0}}; + static const H h_all[] = {{0, 0, 1}}; + static const H h_two[] = {{0, 0, 2}}; + static const H h_five[] = {{0, 0, 5}}; + static const H h_four[] = {{0, 0, 4}}; + O overflow[66]; + for (int i = 0; i < 65; ++i) overflow[i] = (O){C, 0, 1}; + overflow[65] = (O){ST, 0, 0}; + const Rejection cases[] = { + {"duplicate name", {dup, 2, i1, 0, clash, 0, none, 0, load_a, 0}, PURE_INVALID}, + {"state name", {bad_name, 1, i1, 0, clash, 0, none, 0, load_a, 0}, PURE_INVALID}, + {"state name", {long_name, 1, i1, 0, clash, 0, none, 0, load_a, 0}, PURE_INVALID}, + {"non-finite initial value", {non_finite, 1, i1, 0, clash, 0, none, 0, load_a, 0}, PURE_INVALID}, + {"input key", {s1, 1, bad_key, 1, clash, 0, none, 0, load_a, 0}, PURE_INVALID}, + {"duplicate key", {s1, 1, dup_key, 2, clash, 0, none, 0, load_a, 0}, PURE_INVALID}, + {"duplicate name", {s1, 1, i1, 0, clash, 1, none, 0, load_a, 1}, PURE_INVALID}, + {"view with an effect", {s1, 1, i1, 0, v_store, 1, none, 0, store, 3}, PURE_INVALID}, + {"view with an effect", {s1, 1, i1, 0, v_dt, 1, none, 0, store, 3}, PURE_INVALID}, + {"empty view", {s1, 1, i1, 0, v_empty, 1, none, 0, store, 3}, PURE_INVALID}, + {"handler event", {s1, 1, i1, 1, clash, 0, h_bad_event, 1, store, 3}, PURE_INVALID}, + {"branch not forward", {s1, 1, i1, 0, clash, 0, h_two, 1, back, 2}, PURE_INVALID}, + {"branch not forward", {s1, 1, i1, 0, clash, 0, h_two, 1, beyond, 2}, PURE_INVALID}, + {"stack underflow", {s1, 1, i1, 0, clash, 0, h_all, 1, under, 1}, PURE_INVALID}, + {"stack height differs", {s1, 1, i1, 0, clash, 0, h_five, 1, join, 5}, PURE_INVALID}, + {"handler must leave no value", {s1, 1, i1, 0, clash, 0, h_two, 1, leftover, 2}, PURE_INVALID}, + {"unknown state", {s1, 1, i1, 0, clash, 0, h_two, 1, unknown_state, 2}, PURE_INVALID}, + {"non-canonical operand", {s1, 1, i1, 0, clash, 0, h_two, 1, nan_const, 2}, PURE_INVALID}, + {"non-canonical operand", {s1, 1, i1, 0, clash, 0, h0, 1, noncanon, 3}, PURE_INVALID}, + {"unreachable instruction", {s1, 1, i1, 0, clash, 0, h_four, 1, unreachable, 4}, PURE_INVALID}, + {"unknown opcode", {s1, 1, i1, 0, clash, 0, h_two, 1, bad_op, 2}, PURE_INVALID}, + {"stack overflow", {s1, 1, i1, 0, clash, 0, (H[]){{0, 0, 66}}, 1, overflow, 66}, PURE_INVALID}, + }; + for (size_t i = 0; i < LEN(cases); ++i) { + PureResult result = load(cases[i].spec, &module_a); + if (result != cases[i].result || !strstr(error, cases[i].reason)) { + fprintf(stderr, "case %zu: expected '%s', got %d '%s'\n", i, cases[i].reason, (int)result, error); + abort(); + } + } + static S many[33]; + static char many_names[33][8]; + for (unsigned i = 0; i < 33; ++i) { snprintf(many_names[i], 8, "s%u", i % 100u); many[i] = (S){many_names[i], 0}; } + CHECK(load((Spec){many, 33, i1, 0, clash, 0, none, 0, load_a, 0}, &module_a) == PURE_LIMIT); + static unsigned char bytes[65536]; + size_t size = build(bytes, (Spec){s1, 1, i1, 0, clash, 0, none, 0, load_a, 0}); + CHECK(pure_module_load(bytes, size - 1, &module_a, error, sizeof(error)) == PURE_INVALID); + CHECK(pure_module_load(bytes, size + 1, &module_a, error, sizeof(error)) == PURE_INVALID); + bytes[0] = 'X'; + CHECK(pure_module_load(bytes, size, &module_a, error, sizeof(error)) == PURE_INVALID); +} + +static uint32_t next_random(uint32_t *state) { + *state ^= *state << 13; + *state ^= *state >> 17; + *state ^= *state << 5; + return *state; +} + +/* Arbitrary damage is either rejected or yields a module that runs safely. */ +static void mutations(void) { + static const V views[] = {{"label", 0, 1}, {"width", 26, 7}}; + static unsigned char valid[65536], bytes[65536]; + size_t size = build(valid, SPEC(counter_states, counter_inputs, views, counter_handlers, counter_code)); + uint32_t state = 0x2545f491u; + unsigned accepted = 0; + for (unsigned round = 0; round < 20000; ++round) { + memcpy(bytes, valid, size); + unsigned flips = 1 + next_random(&state) % 4; + for (unsigned f = 0; f < flips; ++f) + bytes[next_random(&state) % size] ^= (unsigned char)(1u << (next_random(&state) % 8)); + if (pure_module_load(bytes, size, &module_a, error, sizeof(error)) != PURE_OK) continue; + ++accepted; + PureApp app; + pure_app_start(&app, &module_a); + for (unsigned e = 0; e < 16; ++e) { + if (e % 3 == 0) pure_app_frame(&app); + else pure_app_input(&app, e % 4, e & 1 ? PURE_EDGE_UP : PURE_EDGE_DOWN); + for (uint32_t v = 0; v < module_a.views; ++v) { double value; pure_app_view(&app, v, &value); } + for (uint32_t s = 0; s < module_a.states; ++s) CHECK(isfinite(app.values[s])); + } + } + printf("{\"module_mutations\":20000,\"accepted_after_damage\":%u}\n", accepted); +} + +int main(void) { + behaviour(); + faults(); + rejections(); + mutations(); + printf("{\"sizeof_module\":%zu,\"sizeof_app\":%zu}\n", sizeof(PureModule), sizeof(PureApp)); + puts("{\"module_tests\":\"verified-load-atomic-events-faults-signed-zero-if-else-replace-by-name-rejections-mutations\"}"); + return 0; +} |