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.

1 files changed, 72 insertions, 0 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`)의 작업·예산 모델과 연결하지 않았다. 호스트가 직접 호출한다.