Design 026: the app contract written as mathematics, the part to freeze at 1.0: an event a total, atomic, deterministic function step(S, E) -> (S, Out*) or a fault (budgets in instructions and bytes), time an input, views pure functions of the committed snapshot, the history seen a prefix of commits, delivery in order and once with the transport's state in the store, values the same on every path, replacement joined by names; the layers it removes; its own suspects (input and view kinds, cursors and indexes, keyed documents, the number model, the budget's unit, fixed limits); the computation language rebuilt before 1.0, no compatibility kept before it (the user's word)

1 files changed, 185 insertions, 0 deletions

diff --git a/docs/design/026-app-contract.md b/docs/design/026-app-contract.md
new file mode 100644
index 0000000..60129ba
--- /dev/null
+++ b/docs/design/026-app-contract.md
@@ -0,0 +1,185 @@
+# 026 — 앱 계약: 1.0에서 얼릴 것
+
+작성일: 2026-10-13. 상태: 설계. 지금 있는 앱 계약을 수식으로 적고, 1.0에서 얼릴 것과 1.0 전에 다시 세울 것을 가른다. 구현은
+바꾸지 않는다. 번호에 대해: 139가 "026이 될 것"이라 부른 루프마다의 프로그램은 만들지 않았다(139의 뒷말). 이 번호는 앱 계약에 쓴다.
+
+사용자의 말(2026-10-13):
+- "세상의 그 어떤 명세와 개념이든 pure 생태계(vega, aup포함)에서 구현을 가장 유연하고 견고하게 해내야해. 추상화와 input ->
+  output으로 가는 과정은 얇고 직관적이고 빠르게."
+- 1.0 전에는 호환을 챙기지 않는다. 얼마든지 갈아엎고 깎으며, 의미론적·수학적으로 불변할 최대의 아웃풋을 목표로 한다. 호환은
+  1.0부터다.
+- 표준이란 기존 것을 이어받는 것이 아니라 Pure 생태계 안의 검증이다. 최고의 효율을 위해 바깥이 Pure에 맞춘다. JSON과 HTTP/1.1은
+  그대로 받는다(하이브리드).
+- 기존의 추상화 층이 정말 필요한지를 계속 의심한다.
+
+## 쉬운 말로
+
+- Pure에는 두 부분이 있다.
+  - **앱 계약**: 이벤트는 트랜잭션이고, 상태는 저장되고, 보기는 상태의 함수이며, 메시지는 한 번 적용된다.
+  - **계산의 언어**: 핸들러와 보기 안의 값과 연산이다.
+- **앱 계약은 이미 불변에 가깝다.** 플랫폼이 바뀌어도 이 문장들은 바뀌지 않는다. 이 문서는 그것을 수식으로 적고, 1.0에서 얼릴
+  후보로 둔다.
+- **계산의 언어는 패턴의 모음이다.** 명령 90개와 상태 종류 7개가 판마다 앱의 패턴 하나씩을 일급으로 넣으며 자랐다. 그래서 세상의
+  명세 대부분을 아직 담지 못한다. 그것은 [140](../research/140-spec-suite.md)이 재고, 다음 설계가 다시 세운다.
+- **계약 안에도 의심할 것이 있다.** 입력과 보기의 종류, 커서와 인덱스, 키별 문서, 수의 모델, 예산의 단위, 고정 한도다. 아래
+  "의심" 절에 둔다.
+- **근거.** 지금의 구현과 그 검사다([008](008-module-format.md), [011](011-pure-transport.md), [015](015-boundary-meaning.md),
+  [017](017-apps-on-one-host.md), [018](018-lifetimes-and-computation.md)). 새로 잰 것은 없다.
+- **다음 결정.** 140의 결과로 계산의 핵을 설계한다.
+
+## 계약
+
+### 앱
+
+앱 A = (Σ, I, H, V, O):
+- Σ는 상태의 선언이다. 상태마다 이름, 타입, 초기값, 수명(저장되는 것과 transient)이 있다. 상태의 값 s ∈ S는 저장되는 값과
+  transient 값의 짝이다.
+- I는 입력이고, 입력마다 이름과 페이로드의 모양이 있다.
+- H는 입력마다의 핸들러들이고, 소스 순서대로 돈다.
+- V는 보기다. 인자를 받을 수 있다.
+- O는 출력, 곧 보내는 메시지의 모양이다.
+
+### 이벤트는 전함수다
+
+이벤트 e = (입력, 페이로드, t)다. t는 호스트가 주는 시각이다. **시간은 입력이다.**
+
+    step_A : S × E → (S × Out*) ⊎ Fault
+
+- **실패의 종류.** Fault는 다음과 `require`의 거절이다: `divide`, `non_finite`, `clamp`, `limit`, `not_found`, `encoding`,
+  `exists`, `memory`, `overflow`, `work`.
+- **원자성.** step이 Fault를 내면 상태는 그대로이고 출력도 없다.
+- **끝남.** step은 언제나 끝난다. 실행량 예산 W(명령 수, 기본 2^28)를 넘으면 `work`로, 메모리 몫 M(저장 형식의 바이트, 기본
+  2^28)을 넘으면 `memory`로 끝난다. 그래서 step은 전함수다.
+- **결정성.** step은 함수다. 같은 모듈과 같은 이벤트열이면 어느 기기에서나 같은 상태, 같은 출력, 같은 실패를 낸다. 실패는 같은
+  자리에서, 같은 종류로 난다. 한도를 명령과 바이트로 세기 때문이다(017). Pi, WSL2, M3 Mac에서 `pure-run` 1,053번이 같은 출력을
+  냈다([114](../research/114-across-machines.md)).
+- **역사는 접기다.** s_n = step(s_{n−1}, e_n). 앱은 결정적인 상태 기계(밀리 기계)다.
+- **이벤트의 값**(`let`, 이벤트의 리스트, 메시지의 행)은 step 안에서만 산다.
+
+### 보기는 커밋된 상태의 순수 함수다
+
+    view_v : S_c × Args → Value ⊎ Fault
+
+- S_c는 마지막 저장의 스냅숏이다. 보기는 시각을 읽지 않고, 보내지 않고, 상태를 바꾸지 않는다. 이벤트와 같은 예산 안에서 끝난다.
+- 표 보기의 칸은 물을 때 계산된다. 10만 항목에서 20행을 그리면 20행만 계산한다. 뜻은 함수이고, 게으르게 계산하는 것은 구현이다.
+
+### 내구성: 보이는 역사는 커밋의 앞부분이다
+
+- 저장 한 번은 마지막 저장 이후의 이벤트들을 한 커밋으로 공개한다. 전부 보이거나 하나도 보이지 않는다.
+- 성공을 알린 이벤트는 저장됐고, 실패를 알린 이벤트는 흔적이 없다. 응답은 저장 뒤에 나간다. 묶어 저장할 때도 그렇다.
+- 저장이 실패하면 마지막 저장 이후의 이벤트가 모두 되돌려진다. 그래서 밖에서 보이는 역사는 언제나 커밋된 이벤트열의 앞부분이다.
+- 저장 결과를 모르면(`uncertain`) 앱은 다시 시작할 때까지 저장하지 않는다. 거짓 성공을 내지 않는다.
+
+### 전달: 순서대로, 한 번
+
+- 보냄은 이벤트의 일부다. 실패한 이벤트는 보내지 않은 것이다. 저장을 되돌리면 그 사이의 보냄과 번호도 돌아간다.
+- 출력마다 1부터 번호를 붙인다.
+- 받는 앱은 보낸 쪽마다 들은 번호를 상태와 같은 커밋에 두고, 그 이하의 번호는 다시 적용하지 않는다. 그래서 효과는 순서대로 정확히
+  한 번이다.
+- 앱이 거절한 메시지도 전달된 것이다. 그 효과가 거절이다.
+- 노드 사이에는 연결이 없다(011). 링크의 전송 상태(키 에폭, 번호, 확인, 허가)는 저장소의 행이고, 앱 상태와 같은 커밋에 든다.
+
+### 경계: 받아들인 값은 어느 길로 나와도 같다
+
+[015](015-boundary-meaning.md):
+- 수는 비트까지(0의 부호만 빼고), text는 바이트까지, bool은 `true`나 `false`로, i64는 자릿수 하나까지 같다.
+- 받아들일 수 없는 값은 들어오는 모든 길이 거절하고, 거절한 사건은 아무것도 남기지 않는다.
+
+### 교체: 이름이 상태를 잇는다
+
+- 모듈을 바꾸면 이름과 종류가 같은 상태가 남는다.
+- 레코드가 바뀌면 이름과 타입이 같은 필드를 옮기고, 새 필드는 기본값으로 채운다. 이전 스크립트는 없다.
+- 수식으로는 이름으로 정한 사상 μ : S_old → S_new 하나다.
+
+### 한 호스트의 여러 앱
+
+[017](017-apps-on-one-host.md):
+- 앱은 실행 영역이다. 상태의 소유자가 하나라서, 한 앱은 한 번에 한 스레드에서만 돈다.
+- 한도는 결정적인 단위(명령, 바이트, 요청 수)로 센다. 실패는 그 앱에서 멈춘다.
+- 앱을 가르는 것은 검증기와 예산이다. 호스트 자신의 결함은 모든 앱의 운명이다. 이것을 프로세스 격리라고 부르지 않는다.
+
+## 이 계약이 없애는 층
+
+| 보통의 층 | 계약에서 | 근거 |
+|---|---|---|
+| DB 서버, 스키마, 이전 스크립트 | 선언한 상태가 곧 영속 상태이고, 교체는 이름으로 잇는다 | 008, [092](../research/092-tpcc.md) |
+| 트랜잭션 코드와 되돌리기 처리 | 이벤트가 트랜잭션이다 | 008 |
+| ORM과 직렬화 층 | 저장 형식이 곧 상태의 값이고, 선 위의 바이트가 곧 저장한 기록이다 | 011, 015 |
+| 아웃박스, 메시지 큐, 멱등 키, 재시도 | 보냄은 이벤트의 일부이고, 받는 쪽은 들은 번호를 저장한다 | 008, [078](../research/078-app-connections.md) |
+| 연결 관리(핸드셰이크, 재연결, 풀) | 연결이 없고, 전송 상태는 저장소의 행이다 | 011 |
+| 캐시, 캐시 무효화, 읽기 복제 | 보기는 커밋된 스냅숏에서 돈다 | [080](../research/080-snapshot-reads.md) |
+| 클라이언트 상태 관리, 가상 스크롤 | 보기는 상태의 함수이고, 칸은 물을 때 계산한다 | 008 |
+| CLI·GUI·웹·API를 따로 짜기 | 같은 보기와 입력이 표면마다 쓰인다 | [010](010-surfaces.md), Vega |
+
+## 의심: 계약 안의 용의자
+
+기존의 층을 의심하듯 Pure 자신의 층도 의심한다. 아래는 지금의 계약에 들어와 있지만, 구현이나 한 앱의 패턴이 뜻이 된 것으로
+보이는 것들이다.
+
+1. **입력의 종류.**
+   - 지금: 키(누름과 뗌), text, 타이머, 메시지가 따로 있고, 초당 60번 오는 `frame` 이벤트도 있다.
+   - 의심: 기기의 패턴이 계약에 들어왔다.
+   - 후보: 입력은 모두 이름 있는 필드를 가진 메시지 하나이고, 키, 글자, 틱은 표면이나 호스트가 만드는 메시지다.
+2. **보기의 종류.**
+   - 지금: 수, text, 표, bool, i64.
+   - 의심: 표는 값이 아니라 물을 때 행을 계산하는 함수다.
+   - 후보: 보기는 일반 값(중첩 포함)을 내고, 게으르게 계산하는 것은 구현의 성질로 둔다.
+3. **커서와 인덱스.**
+   - 지금: 둘 다 상태의 종류다.
+   - 의심: 둘 다 "편집을 따라가는 위치"다. 넣기와 지우기를 따라 움직인다.
+   - 후보: 열(text, 리스트) 안의 앵커 하나.
+4. **키별 문서.**
+   - 지금: v2의 `DOC`, `REPLACE`, 기준 리비전.
+   - 의심: 키 있는 리스트와 겹친다.
+   - 후보: 없앤다.
+5. **수의 모델.**
+   - 지금: binary64가 기본이고 정수는 2^53 아래에서만 정확하며, i64와 u32(경계)가 따로 있다.
+   - 의심: f64 더하기에는 결합법칙이 없어서, 접는 순서가 답을 바꾼다.
+   - 정할 것: 정수와 실수의 관계, 그리고 접기의 순서 규칙.
+6. **예산의 단위.**
+   - 지금: 모듈 명령의 수다. 같은 모듈이면 어느 기기에서나 같다.
+   - 의심: 컴파일러가 다른 코드를 내면 같은 소스가 다른 자리에서 `work`로 실패한다.
+   - 정할 것: 결정성의 단위가 모듈인지 소스인지.
+7. **고정 한도.**
+   - 지금: 상태 32, 입력 32, 레코드 16, 레코드의 필드 16, 키별 컬렉션 1, 모듈의 코드 65,535 명령, 값을 가진 중첩 8.
+   - 의심: 구현의 숫자가 뜻이 됐다. "어떤 명세든"과 맞지 않는다(140).
+8. **교체의 세부.**
+   - 이름으로 잇는 것은 남긴다.
+   - 수와 bool을 서로 옮기는 것 같은 규칙은 수의 모델이 정해진 뒤 다시 본다.
+9. **HTTP와 JSON.**
+   - 경계의 어댑터로 남는다(하이브리드). 계약은 아니다.
+   - 보기를 GET으로, 입력을 POST로 옮기는 것은 표면의 하나다. 노드 사이의 기본은 링크다.
+
+## 얼릴 후보와 다시 세울 것
+
+**얼릴 후보(1.0):**
+- step이 전함수이고, 원자적이고, 결정적이다.
+- 시간은 입력이다.
+- 보기는 커밋된 상태의 순수 함수다.
+- 보이는 역사는 커밋의 앞부분이다.
+- 전달은 순서대로 한 번이고, 전송 상태는 저장소에 산다.
+- 한도는 결정적인 단위로 세고, 실패는 그 앱에서 멈춘다.
+- 받아들인 값은 모든 길에서 같다.
+- 교체는 이름으로 잇는다.
+
+**다시 세울 것(1.0 전):**
+- 값과 연산, 곧 계산의 언어
+- 입력과 보기의 종류
+- 커서, 인덱스, 문서
+- 수의 모델
+- 예산의 단위
+- 고정 한도
+
+원칙은 하나다. **의미는 일반적으로 두고, 특수화는 구현 아래로 내린다.** 묶음 실행기가 그 사례다. 루프의 모양을 알아보고 안에서
+특수화했는데, 다섯 단계 동안 앱은 한 줄도 바뀌지 않았다(134–138). TPC-C를 빠르게 한 것(HASHED 표현, 한 번 훑는 집계)도 이미
+구현 쪽의 결정이다.
+
+## 착수 기준 (다음 일)
+
+- **바꿀 결정.** 계산의 핵(값, 연산, 재귀, 바이트)을 어떤 모양으로 다시 세울지 정한다.
+- **남은 질문.**
+  - 세상의 명세들이 aup에서 처음 부딪치는 곳은 어디인가?
+  - 일반적인 핵이 지금의 패턴 전용 명령만큼 빠를 수 있는가?
+- **최소 확인.** [140](../research/140-spec-suite.md)의 명세 묶음과 탐침이다.
+- **중단 기준.** 일반적인 핵으로 옮긴 뒤 은행 질의의 명령 수가 1%, TPC-C가 3%를 넘게 나빠지면 멈춘다. 그때는 그 특수화를 구현
+  아래로 내리는 길을 먼저 찾는다. 찾지 못하면 그 패턴은 핵에 남긴다.