From 49978a22102d748468d3203a1ce0becf27404511 Mon Sep 17 00:00:00 2001 From: eunhhu Date: Wed, 30 Sep 2026 13:06:41 +0100 Subject: Say what a value means at each boundary, and what checking it found (015, 108) --- docs/research/108-one-value-every-path.md | 45 +++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) (limited to 'docs/research') 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`)가 본다. -- cgit v1.2.3