diff --git a/docs/HISTORY.md b/docs/HISTORY.md index 711858c..0814511 100644 --- a/docs/HISTORY.md +++ b/docs/HISTORY.md @@ -40,6 +40,7 @@ --- +### 9-71. 체크드 산술 다음을 쟀다 (2026-09-26, E2) — **헬퍼 체크 전파가 조용한 오답을 가장 많이 줄인다** → [본문](history/9-71.md) ### 9-70. 체크드 정수 산술 슬라이스 (2026-09-26, E2) — **`!` 본문의 오버플로가 `-3`이 됐다** → [본문](history/9-70.md) ### 9-69. §7을 열두 도메인으로 돌렸다 (2026-09-26, E2) — **가장 강한 근거는 체크드 산술이고, 그것은 설계 결정 하나에 걸려 있다** → [본문](history/9-69.md) ### 9-68. 상수 선언 슬라이스 (2026-09-26, E2) — **조용한 오독이 거부가 됐다** → [본문](history/9-68.md) diff --git a/docs/STATUS.md b/docs/STATUS.md index 73f6435..2338d90 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -227,26 +227,24 @@ > ## ▶ 여기서 시작한다 > -> ### 2026-09-26 기준 (4) — **체크드 정수 산술 슬라이스가 닫혔다: `!` 본문의 오버플로가 `-3`이 됐다 (§9-70)** +> ### 2026-09-26 기준 (5) — **체크드 산술 다음을 쟀다: 헬퍼 체크 전파가 조용한 오답을 가장 많이 줄인다 (§9-71)** > -> §9-69가 잰 1위 후보를 슬라이스로 닫았다(#333 SPEC · #334 구현). `!` 본문의 i32 `+ - *`·단항 `-`·`MIN / -1`과 -> NaN·범위 밖 `f64 as i32`가 `ML_ST_OVERFLOW`(`-3`)를 내고, 실제 C 호스트가 그것을 받는다. 구현으로 다시 잰 -> 626행은 실험의 표와 같다(조용한 오답 161행 중 101이 status). 같은 날 Q17은 (A)로 열어 두고 위험을 -> `HOST_ABI.md`에 적었다(#335). +> 남은 103행을 기능에 귀속하고(귀속 대조 포함), 상위 두 설계를 로컬 브랜치에서 구현해 626행 전부로 다시 쟀다. +> 어느 모드도 맞던 status 0 답을 바꾸지 않았다. 조용한 오답은 **헬퍼 체크 전파(F2)** 가 60 → 44로 줄이고, +> **넓은 중간값(WIDE)** 은 참값이 드는데 `-3`인 행을 52 → 17로 줄이지만 멈춤·추출 위험을 갖고 있다(§9-71.4). > > **▶ 다음 세션 — 여기서 시작한다.** 순서대로: > -> 1. **다음 슬라이스 — 사용자 결정.** 후보의 정본은 `docs/slices/README.md`의 "다음 슬라이스" 절이다. 체크드 산술 뒤에 -> 남은 근거는 §9-70.2가 센다 — 여전히 조용한 60행(무한 헬퍼 16 · f64 절삭·NaN 14 · 산술이 아닌 것 25 …)과, -> `-3`이 됐지만 참값이 i32에 드는 43행(정답을 주는 것은 **i64**뿐이다). +> 1. **다음 슬라이스 — 사용자 결정.** 결정표는 §9-71.6이다(권고: F2 — DP-O7을 뒤집는다, Grok 동의). 고르면 +> 그 안의 SPEC을 먼저 쓴다. 시험 구현은 로컬 브랜치 `exp/wide-local`에 있다(푸시 안 함). > 2. **작은 항목**: C# 호스트(Phase 4) · LSP(Phase 3, 큰 일). > 3. **외부**: `X1`·`X2` — Delphi가 있는 CI 러너. 이 저장소 안에서는 닫히지 않는다. > > ⚠ **이 머신의 전체 게이트는 6회 중 2회 실패한다**(§9-63.5) — 실패를 보면 먼저 원인을 읽는다. > 강한 신호는 CI 두 잡이다. > -> 📌 **본문은 §9-70이다**(`docs/history/9-70.md`). 그 앞의 2026-09-26 (3) 항목(§7 열두 도메인)은 -> 바이트 그대로 옮겼다 — 지금은 `docs/history/start-block-051.md`다. +> 📌 **본문은 §9-71이다**(`docs/history/9-71.md`). 그 앞의 2026-09-26 (4) 항목(체크드 산술 닫힘)은 +> 바이트 그대로 옮겼다 — 지금은 `docs/history/start-block-052.md`다. > > > ### 그 앞의 항목들 — **본문은 `docs/history/start-block-NNN.md`로 옮긴다 (2026-09-23부터)** diff --git a/docs/history/9-71.md b/docs/history/9-71.md new file mode 100644 index 0000000..2308218 --- /dev/null +++ b/docs/history/9-71.md @@ -0,0 +1,117 @@ +### 9-71. 체크드 산술 다음을 쟀다 (2026-09-26, E2) — **헬퍼 체크 전파가 조용한 오답을 가장 많이 줄이고, 넓은 중간값은 SPEC이 정할 위험을 갖고 있다** + +사용자가 §9-70의 보고를 수용하고 *"후속작업을 Grok과 함께"* 를 요청했다(관계 없는 MCP 인증은 보류). 다음 +슬라이스는 고르지 않았다 — 사용자 결정이다. 이 기록은 그 결정의 근거를 잰 것이다. + +#### 9-71.1. 정리한 것 + +- **Delphi 로컬 게이트**: `MATHLESS_GATE_DELPHI=require` → `GATE_DELPHI_OK`(검사 42줄 `ok`). 호스트가 쓰는 + `shapes`·`basket`·`allocate` 유닛이 #334 뒤로 `ML_ST_OVERFLOW`를 선언하는데, dcc64(IDE 빌드)가 그 유닛을 + 컴파일하고 호스트가 돈다. CI에서는 여전히 돌지 않는다(X2). +- 실험 브랜치 `exp/checked-arith-local`은 번들로 백업한 뒤 지웠다(사용자 확인). + +#### 9-71.2. 방법 — 남은 행을 기능에 귀속하고, 상위 설계를 시험 구현했다 + +§9-70.2 뒤에 남은 **103행**(여전히 조용한 60 + `-3`이 됐지만 참값이 i32에 드는 43)을 워크플로 둘로 쟀다. + +- **귀속**(에이전트 10): 도메인 묶음 분석가 여섯이 행마다 원인과, 후보 기능마다 *"가장 직접적인 형태가 맞는 답이나 + status가 되는가, 그 기능이 있어도 같은 실수가 똑같이 쉬운가"*(귀속 대조, STATUS §7)를 판정했다. 기능을 오늘의 + 언어로 흉내 낼 수 있으면 `mlprobe`로 쟀다. 상위 셋에는 회의론자, 끝에는 완결성 비평. +- **보완**(에이전트 2): 회의론을 받지 못한 텍스트 후보(F6)의 회의론, 그리고 넓은 중간값의 표본 밖 위험 검토. + +원인: 참값이 드는 중간값 오버플로 40 · 무한 헬퍼의 wrap 16 · 산술이 아닌 것 23 · f64 정밀도 14 · 무한 export의 +wrap 4 · 기타 6. 귀속에서 나온 것: + +- **목록에 없던 기능이 가장 많이 귀속됐다 — 넓은 중간값**(아래 WIDE): 29행, 전부 흉내로 쟀고 회의론에서 28이 남았다. +- **i64 타입**은 51행에서 *"옵트인이라 저자가 똑같이 i32로 쓴다"* 로 대조를 통과하지 못했다. +- **헬퍼 체크 전파**(아래 F2): 13행 → 회의론 11 생존(둘은 비현실 입력). +- **텍스트**(F6 — 문자 길이 · 비ASCII 비교 · 입력 인코딩 계약): 11행 중 **규칙 넷**만 남았다(인코딩 계약 NA-R1·R5, + 문자 길이 NA-R2, 비ASCII 비교 NA-R4). 넷 다 Q17(A)를 다시 열어야 하고, UTF-8 전용(B)은 SMS 규칙(NA-R3)을 + CP949 호스트에서 틀리게 만든다(측정 — 그 호스트에서 오늘은 맞다). + +비평이 짚은 대로 103행은 체크드 산술이 만든 **오탐 9행**(맞던 답이 `-3`)을 빼고 있었다. 그래서 시험 구현은 +**626행 전부**로 쟀다. + +#### 9-71.3. 시험 구현 — 네 모드, 626행 (로컬 브랜치 `exp/wide-local`, 푸시 안 함) + +스위치 `MLC_EXP_WIDE` 하나: + +- **twin (F2)**: `!` 본문이 부르는 무한 내부 헬퍼는 체크된 쌍둥이를 부르고 실패를 전파한다 — DP-O7을 뒤집는다. +- **bang (WIDE)**: `!` 본문의 i32 산술 트리를 i64로 재고(체크드 i64, 0 제수 가드, `wrapping_rem`), 산술이 아닌 + 소비자(`let`·대입·`return`·인자·인덱스·`result`·`as`)가 값을 받는 자리에서만 좁히며 검사한다. 비교는 넓은 값끼리. +- **prop**: 둘 다. **all**: WIDE를 무한 본문까지(좁힐 때 wrap). + +625행(메모 행 1 제외)의 최종 상태 — 바뀐 행은 하나하나 기록된 기댓값, 분석가가 정확한 정수로 계산한 값, 또는 +체크드 산술 이전의 답과 대조했다: + +| 모드 | 맞음 | **조용한 오답** | 참값이 드는데 `-3` | 기타 | +|---|---|---|---|---| +| 오늘 | 496 | 60 | 52 | 17 | +| twin (F2) | 505 | **44** | 59 | 17 | +| bang (WIDE) | 530 | 60 | 17 | 18 | +| prop (둘 다) | **546** | **44** | **17** | 18 | +| all | 537 | 53 | 17 | 18 | + +- **어느 모드에서도 오늘 맞던 status 0 답은 바뀌지 않았다.** +- **bang** — 바뀐 38행이 전부 오늘 `-3`이던 행이다: 30 → 참값(14행은 기록된 기댓값, 16행은 계산한 값과 같다), + 4 → 체크드 산술 이전의 맞던 답 복구(records R4d · R6m, coupon R4w-7, stateful R4-oob3), 3 → 기대한 도메인 + 에러(hostdata R6 → `E_STALE = 2`), 1 → 규칙 불변식 밖 입력의 거절(stateful R1-oob, `-3` → `3`; 표의 "기타" +1). +- **twin** — 바뀐 16행이 전부 오늘 조용한 오답이다: 9 → 참값이 i32 밖이라 실패가 맞는 행(billing R4 넷 · R6 셋, + hostdata R2 둘), 7 → 참값이 드는데 `-3`(records R2 넷, stateful R1 셋). 검사 자리는 오늘과 같은 연산자다. +- **prop** — 같은 16행이 전부 맞는 답이 된다: 실패 9, records R2 넷과 stateful R1-fits는 기댓값, R1-fail · + R1-thr-hi는 도메인 에러 `3`. +- **all** — 무한 헬퍼 7행이 맞게 되지만 billing R4 같은 행은 좁힐 때 wrap해 조용히 남는다(53). 그리고 **무한 본문의 + status 0 값이 바뀐다**: `(2147483647 + 1) / 2`가 `-1073741824`에서 `1073741824`로(측정). + +전체 스위트(게이트 셋 require)에서 바뀐 테스트: + +| 모드 | 동작 | 텍스트 고정 | +|---|---|---| +| bang | `an_intermediate_overflow_fails_even_when_the_answer_fits`(WIDE가 없애는 바로 그 한계) | 골든 | +| twin | `infallible_bodies_still_wrap_and_literals_are_checked`의 DP-O7 줄 | 골든 · `every_concat_piece_is_evaluated_once`(호출은 한 번 — 쌍둥이 이름이라 문자열 개수가 줄었다) | + +#### 9-71.4. 넓은 중간값의 위험 — 표본 밖에서 잰 것 (위험 검토 에이전트, E2) + +- **무작위 48,000 호출**(함수 200개 × 입력 80 × 시드 3, 정확한 정수 모델과 대조): 병합된 규칙이 `-3`이 아닌 + 26,476 호출에서 bang과 차이 0. `-3`이던 21,524 호출에서 bang은 값 6,337 · 도메인 에러 1,770 · `-2` 3,130 · + 여전히 `-3` 10,287. 검토 에이전트의 요약은 `-3` 호출을 17,524로 적었는데 네 칸의 합과 맞지 않아, 같은 스크립트를 + 다시 돌려 21,524를 확인했다. +- **빨리 실패하던 입력이 멈출 수 있다**: `return a*b + spin(n)`(`spin`은 끝나지 않는 `while`) — 오늘은 즉시 + `-3`, bang은 15초 타임아웃까지 돌아오지 않았다. 검사가 연산자에서 좁히는 자리로 늦춰졌기 때문이다. +- **추출이 답을 바꾼다**: `return a*b/b`는 값인데 `let t = a*b return t/b`는 `-3`이다. 헬퍼 인자도 좁힌다. + 코퍼스의 산술 뿌리 588 중 158이 누적 대입이라 가장 큰 부류는 얻는 것이 없다. +- **실패 코드가 바뀐다**: `if a*b > xs[5]`가 `-3`에서 `-2`로. +- **i64도 넘친다**: `(a*a + b*b)/(a*a)`는 `a = b = i32::MIN`에서 참값 2인데 `-3`. 무작위 호출 중 정확한 모델에는 + 답이 있는데 bang이 `-3`을 낸 것이 1,687이다. +- **C 백엔드(D19)**: MSVC 19.44는 ``·`__builtin_mul_overflow`·`__int128`을 모두 거부했다(clang + 21은 앞의 둘을 받는다). C에서 부호 있는 int64 오버플로는 미정의 동작이다. +- 크기: 예제 26개 `.text` 합 95,348 → 95,440바이트. 호스트는 어느 규칙으로 빌드됐는지 알 수 없다(헤더·지문 같음). + +SPEC으로 가면 정할 것: 좁히는 자리의 전체 목록(`as f64`·`as string`·인덱스·헬퍼 인자), 지역 변수, 실패 순서와 +멈춤, i64 한계, DP-O9 재서술, 바인딩 문구, C 백엔드의 구현. + +#### 9-71.5. Grok + +- **plan**(WIDE 착수 전): Q1 — `!` 본문에서 status 0 답을 보존하는가 **YES**. Q2 — 무한 본문도 보존하는가 + **NO**(`(2147483647 + 1) / 2`). Q3 — 소비자 목록에 빠진 것(`i32 as i32`, 비교). 함정: 늦춘 실패가 다른 실패 + 코드에 먼저 닿는다. +- **verify**: 실험 코드(네 주장) CONFIRMED · 626행 비교(status 0 385행 중 변화 0, 차이 38 전부 `-3`) CONFIRMED. + 이 기록에는 넷 — 표의 수치 · 옮긴 블록의 바이트 · 바뀐 행의 이름은 CONFIRMED, 9-71.4의 수치는 DISCREPANCY였다: + 네 칸의 합이 적힌 `-3` 호출 수와 맞지 않았고(위 21,524), clang이 `__int128`을 받는다는 말은 근거에 없었다. +- **plan**(권고 순서): **(a) F2 먼저**(조용한 오답을 줄이고 가장 작은 슬라이스) · DP-O7 뒤집기 **수용 가능**(고정 + 테스트만 기댄다) · WIDE는 멈춤 위험을 SPEC이 정하기 전까지 **보류**. UNASKED: WIDE의 "기타" +1 행을 이름으로 적어라 + → stateful R1-oob(9-71.3). +- 타임아웃 0회. + +#### 9-71.6. 남은 것 — 사용자 결정 + +| 안 | 조용한 오답 | 참값이 드는데 `-3` | 뒤집는 것 | 새 위험 | +|---|---|---|---|---| +| **F2 — 헬퍼 체크 전파 (권고)** | 60 → **44** | 52 → 59 | DP-O7(무한 헬퍼 = 탈출구) | 같은 헬퍼가 호출자에 따라 다르게 동작한다(`!`와 무한 본문 사이의 차이가 이미 그렇다) · 쌍둥이만큼 코드가 는다 | +| WIDE — 넓은 중간값 | 60 | 52 → **17** | SPEC-checked-arithmetic §2.1의 검사 자리 | 9-71.4 전부 — 멈춤 · 추출 · C 백엔드 · i64 | +| F2 + WIDE | **44** | **17** | 둘 다 | 둘 다 | +| 텍스트(F6) | 규칙 넷 | — | Q17 (A) · DP-S2 | 인코딩을 정하면 반대 규칙(EUC-KR)이 틀린다 | + +권고는 **F2 먼저**다 — 이 저장소의 논지(*"그럴듯한 오답보다 실패"*)를 체크드 산술이 닿지 못한 16행으로 넓히고, +검사 규칙은 그대로 둔다. WIDE는 조용한 오답을 하나도 줄이지 않고 시끄러운 거절을 맞는 답으로 바꾸며, 그 대가가 +9-71.4다 — 따로 SPEC이 정할 일이다. diff --git a/docs/history/start-block-052.md b/docs/history/start-block-052.md new file mode 100644 index 0000000..d2696ca --- /dev/null +++ b/docs/history/start-block-052.md @@ -0,0 +1,21 @@ +> ### 2026-09-26 기준 (4) — **체크드 정수 산술 슬라이스가 닫혔다: `!` 본문의 오버플로가 `-3`이 됐다 (§9-70)** +> +> §9-69가 잰 1위 후보를 슬라이스로 닫았다(#333 SPEC · #334 구현). `!` 본문의 i32 `+ - *`·단항 `-`·`MIN / -1`과 +> NaN·범위 밖 `f64 as i32`가 `ML_ST_OVERFLOW`(`-3`)를 내고, 실제 C 호스트가 그것을 받는다. 구현으로 다시 잰 +> 626행은 실험의 표와 같다(조용한 오답 161행 중 101이 status). 같은 날 Q17은 (A)로 열어 두고 위험을 +> `HOST_ABI.md`에 적었다(#335). +> +> **▶ 다음 세션 — 여기서 시작한다.** 순서대로: +> +> 1. **다음 슬라이스 — 사용자 결정.** 후보의 정본은 `docs/slices/README.md`의 "다음 슬라이스" 절이다. 체크드 산술 뒤에 +> 남은 근거는 §9-70.2가 센다 — 여전히 조용한 60행(무한 헬퍼 16 · f64 절삭·NaN 14 · 산술이 아닌 것 25 …)과, +> `-3`이 됐지만 참값이 i32에 드는 43행(정답을 주는 것은 **i64**뿐이다). +> 2. **작은 항목**: C# 호스트(Phase 4) · LSP(Phase 3, 큰 일). +> 3. **외부**: `X1`·`X2` — Delphi가 있는 CI 러너. 이 저장소 안에서는 닫히지 않는다. +> +> ⚠ **이 머신의 전체 게이트는 6회 중 2회 실패한다**(§9-63.5) — 실패를 보면 먼저 원인을 읽는다. +> 강한 신호는 CI 두 잡이다. +> +> 📌 **본문은 §9-70이다**(`docs/history/9-70.md`). 그 앞의 2026-09-26 (3) 항목(§7 열두 도메인)은 +> 바이트 그대로 옮겼다 — 지금은 `docs/history/start-block-051.md`다. +> diff --git a/docs/history/start-block-index.md b/docs/history/start-block-index.md index a6f3816..51552b6 100644 --- a/docs/history/start-block-index.md +++ b/docs/history/start-block-index.md @@ -9,6 +9,7 @@ > | 날짜 | 무엇을 했나 | 본문 | > |---|---|---| +> | 2026-09-26 (4) | **체크드 정수 산술 슬라이스가 닫혔다: `!` 본문의 오버플로가 `-3`이 됐다** — 같은 날 다음 후보를 쟀다(§9-71) | §9-70 | > | 2026-09-26 (3) | **§7을 열두 도메인으로 돌렸다: 가장 강한 근거는 체크드 산술이고, 설계 결정 하나에 걸려 있다** — 같은 날 슬라이스로 닫혔다(§9-70) | §9-69 | > | 2026-09-26 (2) | **상수 선언 슬라이스가 닫혔다: 조용한 오독이 로드 거부가 됐다** — 다음 선택은 §7부터(§9-69) | §9-68 | > | 2026-09-26 | **상태 머신 예제가 경계의 공백을 쟀다: 상태 번호는 헤더와 지문 밖에 있다** — 같은 날 상수 선언 슬라이스로 닫혔다(§9-68) | §9-67 | diff --git a/docs/slices/README.md b/docs/slices/README.md index e46b068..f688b23 100644 --- a/docs/slices/README.md +++ b/docs/slices/README.md @@ -125,7 +125,7 @@ TDD 구현 → Grok 검증 → PR** 순서를 따른다(`CLAUDE.md` "개발 방 두 번째 호스트(C#, ROADMAP Phase 4), 그리고 ROADMAP Phase 2가 이름만 두고 설계가 없던 둘 — **인터페이스 정의 파일**(설계부터)과 **개발/배포 빌드 분리**(D13, `SECURITY.md` P1). *(2026-09-25 로드맵 검토에서 더했다 — Phase 2의 다섯 항목 중 이 둘이 이 목록에 없었다.)* -§7(§9-69, 12개 도메인 72규칙과 귀속 대조)이 더한 후보: **i64**(체크드 산술 뒤에도 43행은 `-3`일 뿐 정답이 아니다 — §9-70.2), **입력 문자열의 인코딩 계약**(닫힌 DP-S2의 재개 — `OPEN_QUESTIONS.md` Q17이 (A)로 열어 두었고 재검토 조건은 거기 있다), 비트 연산자, +§7(§9-69, 12개 도메인 72규칙과 귀속 대조)이 더한 후보: **헬퍼 체크 전파**와 **넓은 중간값**(둘 다 626행으로 시험 구현했다 — 결정표는 §9-71.6), **i64**(§9-71: 옵트인이라 귀속 대조에서 51행이 빠졌다), **입력 문자열의 인코딩 계약**(닫힌 DP-S2의 재개 — `OPEN_QUESTIONS.md` Q17이 (A)로 열어 두었고 재검토 조건은 거기 있다), 비트 연산자, 지역 작업 배열, 수학 내장 함수, 문자 단위 길이. **struct는 §9-1이 강제되지 않는다고 결론냈다** — 고르려면 그 절을 먼저 읽는다(§9-69도 귀속 0으로 다시 확인했다). 배열도 같은 결론이었고(§9-9가 다섯 번째로), **입력은 그 사실을 SPEC 첫 절에 적은 채로 열렸다**.