Define Pure module format v1 with a static verifier

Pure now owns the format its toolchains target, as the JVM owns class files.
A v1 module carries f64 states, key inputs, atomic event handlers and pure
views. pure_module_load checks sizes, names, keys, operands, forward-only
branches, reachability and stack heights at every join before anything runs,
so execution needs no stack checks and each event is bounded by its handler
length. PureApp runs events on a pending copy and replaces modules keeping
states by name, without allocation. Semantics match the workbench engine,
including IEEE minimum/maximum on signed zeros.

test-module covers behaviour, atomic faults, 26 rejection checks and 20,000
damaged modules under ASan/UBSan; pure-run is a JSON test host.

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;
+}