diff options
| -rw-r--r-- | docs/design/015-boundary-meaning.md | 70 | ||||
| -rw-r--r-- | docs/research/108-one-value-every-path.md | 45 |
2 files changed, 115 insertions, 0 deletions
diff --git a/docs/design/015-boundary-meaning.md b/docs/design/015-boundary-meaning.md new file mode 100644 index 0000000..bdc68df --- /dev/null +++ b/docs/design/015-boundary-meaning.md @@ -0,0 +1,70 @@ +# 015 — 경계에서의 값: 들어온 값은 모든 길에서 같게 나온다 + +작성일: 2026-09-30. 상태: 구현, 검사로 고정. [108](../research/108-one-value-every-path.md)에서 정했다. + +앱의 값은 여러 경계를 지난다. 들어올 때 HTTP의 JSON이나 쿼리에서 메시지의 필드가 되고, 저장할 때 저장 형식이 되고, +보일 때 보기의 글자가 되고, 보낼 때 링크나 HTTP의 기록이 되어 다른 노드의 입력으로 옮겨진다. 이 문서는 그 모든 경계에서 +값의 뜻이 무엇이고, 무엇을 그대로 옮기고 무엇을 거절하는지를 정한다. + +한 줄로는 이렇다. **받아들인 값은 어느 길로 나오든 같다. 수는 비트까지(0의 부호만 빼고), text는 바이트까지. +받아들일 수 없는 값은 모든 들어오는 길이 거절하고, 거절한 사건은 아무것도 남기지 않는다.** + +## 수 + +- **들어올 때.** JSON의 수와 쿼리의 값(퍼센트 인코딩을 푼 뒤)은 JSON 수의 문법으로 읽는다. 부호 `+`, 앞의 0(`01`), + 점만 있는 것(`.5`, `1.`), 16진, `NaN`, `Infinity`는 받지 않는다. 글자가 뜻하는 값에 가장 가까운 binary64로 읽는다(정확히 + 반올림하고, 가운데는 짝수로). 그 값이 유한하지 않으면(`1e999`) 거절한다. +- **0에는 부호가 없다.** aup에서 −0과 0은 같은 값이다. 비교는 같고, `distinct`는 한 번 세고, 보기와 글자는 둘 다 `0`으로 + 쓴다. 저장과 전달은 비트를 그대로 옮기므로 −0이 −0으로 남을 수 있지만, aup 코드에서는 보이지 않는다. +- **저장.** 비트 그대로 돌아온다. 크기가 2^53 미만인 정수는 zigzag varint, 그 밖은 표시와 8바이트다. +- **보일 때.** 다시 읽으면 같은 binary64가 되는 가장 짧은 글자다. 1e15 미만의 정수는 점과 지수 없이 쓰고, 그 밖은 `%g` + 모양에 지수를 줄여 쓴다. +- **보낼 때.** 기록의 비트가 그대로 간다. 받는 입력의 모양이 다르면 이름으로 옮긴다([014](014-fields-by-name.md)). u32를 + number로 넓히는 것은 정확하다. + +## u32 + +- **들어올 때.** 숫자만 받는다. 부호, 소수, 지수(`1e3`도), 앞의 0은 안 되고, 0부터 4,294,967,295까지다. 그 밖은 거절한다. + JSON과 쿼리가 같다. +- 상태에서는 수다. +- **보낼 때.** 출력의 u32 필드에 준 수는 범위 안의 정수여야 한다. 아니면 그 사건이 실패한다. 아무것도 남지 않고, 보내지도 + 않는다. + +## text + +- **들어올 때.** JSON 문자열은 이스케이프를 풀고 서로게이트 짝을 합친다. 날 본문은 바이트 그대로다. 결과는 UTF-8이어야 + 한다. 짝 없는 서로게이트, 너무 긴 인코딩, U+10FFFF 너머, 잘린 바이트는 거절한다. JSON이면 400 `json`, 날 본문이면 + 422 `encoding`이다. +- 유효한 스칼라는 무엇이든 그대로 둔다. NUL, 제어 문자, U+2028과 U+2029, BOM, 비문자가 모두 그렇다. +- **저장과 전달.** 바이트 그대로다. +- **보일 때.** JSON 문자열(따옴표, 역슬래시, 제어 문자를 이스케이프)이다. 다시 읽으면 같은 바이트다. +- **답할 때.** `reply 메시지.필드`의 답은 그 필드의 바이트다. + +## 메시지의 모양 + +- **그룹.** JSON에서는 안의 객체이고, 쿼리에서는 점으로 이은 이름(`at.x`)이다. 모듈과 전달에서는 `at.x` 같은 이름의 필드다. +- **행(`list of 레코드`).** JSON 배열의 객체 하나가 행 하나이고, 목록의 저장 형식으로 옮겨진다. 수와 text는 위와 같다. + 메시지의 행은 모두 받거나 하나도 받지 않는다. +- **사건.** 사건은 모두 되거나 아무것도 되지 않는다. 실패한 사건은 상태를 바꾸지 않고 보내지 않는다. +- **전달.** 필드를 이름으로 받는다. 같은 종류이거나 넓히는 것이어야 하고, 빠진 필드는 0이나 빈 값이며, 모르는 필드는 + 받지 않고 기다린다([014](014-fields-by-name.md)). 한 번씩, 순서대로 적용한다. + +## 저장과 다시 읽기 + +- 재시작(로그에서), 체크포인트 뒤의 재시작(이미지에서), 모듈 교체(상태를 이름으로 잇는다)가 모두 같은 값을 낸다. +- 보기와 질의는 마지막 저장의 스냅숏에서 읽는다. 그 저장의 상태와 같다. + +## 검사 + +[`tests/check.py`](../../tests/check.py)의 `server_meaning`이 한 번에 본다. + +- 값: 수 22개(0과 −0, 2^53 부근, 가장 큰 수, 정규와 비정규의 경계, 반쯤에서의 언더플로, 1e21 부근), u32 넷, text 12개(한글, + 4바이트 UTF-8, 이스케이프, NUL, U+2028, BOM, 비문자, 4 KiB). +- 들어오는 길: JSON(ASCII로 이스케이프한 것과 UTF-8), 행, 쿼리와 날 본문, 링크(다른 순서, 넓힌 필드), HTTP 전달. +- 나오는 길: 보기, 질의, 답, 재시작, 체크포인트 뒤의 재시작, 모듈 교체, 두 번 중계한 노드. +- 거절할 값 39가지(수, u32, text, 행)가 모든 들어오는 길에서 거절되고, 어디에도 남지 않는다. + +전달이 한 번씩, 순서대로 적용되는 것은 링크의 검사들(`server_links_udp_lossy`, `server_links_moved`, `server_upgrade`)과 +[012](012-link-protocol.md)이 지킨다. 필드를 이름으로 받는 규칙은 `server_fields`가 지킨다. + +화면(Vega가 보기를 그리는 것)은 이 문서 밖이다. 다음 단계다. diff --git a/docs/research/108-one-value-every-path.md b/docs/research/108-one-value-every-path.md index 4f0bb28..387ef24 100644 --- a/docs/research/108-one-value-every-path.md +++ b/docs/research/108-one-value-every-path.md @@ -35,3 +35,48 @@ - 거절할 값(넘치는 수, 음수·소수·2^32 이상의 u32, UTF-8이 아닌 text, 짝 없는 서로게이트)은 모든 들어가는 길이 거절해야 한다. 거절한 사건은 아무것도 남기지 않는다(보기에도, 보냄에도). - **범위.** Pure의 경계다. 화면(Vega가 보기를 그리는 것)은 다음 단계다. + +## 쉬운 말로 + +- **어긋난 곳은 하나였고, 고쳤다.** 입력 필드의 쿼리 값은 퍼센트 인코딩을 풀지 않았다. 같은 pure-serve가 보기의 인자는 + 풀었다. 그래서 파이썬의 `urlencode`나 브라우저처럼 지수의 `+`를 `%2B`로 보내는 클라이언트는 `?n=1e%2B21`이 거절됐다. 이제 + 입력 필드도 보기의 인자처럼 푼다. +- **0에는 부호가 없다는 것을 계약으로 적었다.** `-0`은 받아들이지만 보기에는 `0`으로 나온다. 글자로 쓰는 함수가 그렇게 + 정해져 있고, `distinct`도 둘을 한 번 센다. aup에는 둘을 가르는 연산이 없으니 −0은 aup의 별개 값이 아니다. +- **aup 문서의 예가 컴파일되지 않았다.** 문서는 `message { title: text, points: number }`처럼 선언의 필드를 쉼표로 적었는데, + 컴파일러는 줄바꿈이나 세미콜론만 받았다. 값(`Kept { id: 1 }`)은 쉼표로 나누므로, 이제 선언도 쉼표를 받는다(aup `be1122a`). +- **나머지는 모든 길에서 같았다.** + - 수는 어려운 경우까지 파이썬의 정확한 반올림과 비트가 같았다(2^53+1의 짝수 반올림, `2.2250738585072011e-308`, 비정규 수, + 반쯤에서의 언더플로). + - text는 NUL, 제어 문자, U+2028, BOM, 4 KiB까지 바이트가 같았다. + - 거절할 값은 JSON, 쿼리, 날 본문, 행이 모두 거절했다. + - 재시작, 체크포인트, 모듈 교체, 두 번의 중계를 지나도 같았다. +- **검사는 `make check`에 들어갔다.** `server_meaning`이 1.3초에 값 67개를 나가는 길 7개에서 보고, 거절할 값 39가지를 본다. + 경계마다의 계약은 [015](../design/015-boundary-meaning.md)에 적었다. + +## 한 것 + +1. **값을 하나씩 더듬었다.** 노드 하나에 경계값을 넣고 보기로 읽었다. 수 40가지(거절할 것 포함), text 25가지(서로게이트와 + UTF-8이 아닌 바이트 포함), 쿼리와 날 본문 47가지다. 수는 파이썬의 `float()`이 기대값이다. +2. **어긋난 곳을 찾아 고쳤다.** 쿼리 값의 해독이 보기와 입력에서 달랐다(pure-serve `serve.c`의 `resolve`). +3. **한 번에 보는 검사를 짰다** ([`tests/check.py`](../../tests/check.py)의 `server_meaning`). + - A가 JSON(ASCII로 이스케이프한 것과 UTF-8), 행, 쿼리와 날 본문으로 받아 쥐고, 링크로 B에 보낸다. + - B는 필드 순서를 바꾸고 u32를 number로 넓힌 입력으로 받아 HTTP로 C에 보낸다. + - 나오는 길 일곱: A의 보기, A의 질의, B와 C의 보기, 재시작한 A, 체크포인트 뒤에 재시작한 A, 모듈을 바꾼 B. 그리고 `put`의 + 답은 들어온 text의 바이트다. + - A에서만 한 행을 4 KiB로 400번 고쳐, 목록의 이미지를 새로 쓰게 했다(체크포인트 1번). +4. **검사가 헛돌지 않는지 봤다.** 고치기 전의 pure-serve로 돌리면 쿼리 경로(`1E+2`를 `1E%2B2`로 보낸 것)에서 실패한다. + B가 받은 수에 1 ulp를 곱하게 앱을 바꾸면 B에서 잡힌다. + +## 판정 + +- 통과 조건을 채웠다. 받아들인 값은 나가는 길 일곱에서 수는 비트까지(0의 부호만 빼고), text는 바이트까지 같다. 거절할 값은 + 모든 들어가는 길이 거절하고, 어디에도 남지 않는다. +- 착수 기준은 −0을 내다보지 못했다(수를 비트까지 비교한다고만 적었다). 0의 부호는 aup에서 뜻이 없으므로(가르는 연산이 + 없고, 글자와 `distinct`가 이미 같게 본다) 바꾸지 않고 계약으로 적었다(015). 검사는 0끼리를 같게 본다. + +## 다음 + +- **화면.** Vega가 보기를 그리는 경계다. 터미널과 CLI와 문장이 같은 값을 어떻게 보이는지(제어 문자, U+2028, 넓은 글자를 + 그대로 보일지, 이스케이프할지)를 정하고 같은 방식으로 고정한다. +- bytes 필드는 목록의 레코드에 담기지 않으므로 여기서 보지 않았다. 문서 모델의 검사(`server_parity`)가 본다. |