diff --git a/compiler/tests/golden/generated.rs.txt b/compiler/tests/golden/generated.rs.txt index 406f4a6..4a9d31a 100644 --- a/compiler/tests/golden/generated.rs.txt +++ b/compiler/tests/golden/generated.rs.txt @@ -1806,11 +1806,7 @@ fn ml_fn_one_payment(principal: i32, months: i32, month: i32) -> Result= months) { return Err(1); } - let base = (match i32::try_from({ let __wl: i64 = ((principal) as i64); let __wr: i64 = ((months) as i64); if __wr == 0 { 0i64 } else { match __wl.checked_div(__wr) { Some(__o) => __o, None => { return Err(-3); } } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } }); - if (month == 0i32) { - return Ok((match i32::try_from({ let __wl: i64 = ((base) as i64); let __wr: i64 = { let __wl: i64 = ((principal) as i64); let __wr: i64 = ((months) as i64); if __wr == 0 { 0i64 } else { __wl.wrapping_rem(__wr) } }; match __wl.checked_add(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } })); - } - return Ok(base); + return Ok((match i32::try_from({ let __wl: i64 = { let __wl: i64 = { let __wl: i64 = ((principal) as i64); let __wr: i64 = { let __wl: i64 = ((month) as i64); let __wr: i64 = ((1i32) as i64); match __wl.checked_add(__wr) { Some(__o) => __o, None => { return Err(-3); } } }; match __wl.checked_mul(__wr) { Some(__o) => __o, None => { return Err(-3); } } }; let __wr: i64 = ((months) as i64); if __wr == 0 { 0i64 } else { match __wl.checked_div(__wr) { Some(__o) => __o, None => { return Err(-3); } } } }; let __wr: i64 = { let __wl: i64 = { let __wl: i64 = ((principal) as i64); let __wr: i64 = ((month) as i64); match __wl.checked_mul(__wr) { Some(__o) => __o, None => { return Err(-3); } } }; let __wr: i64 = ((months) as i64); if __wr == 0 { 0i64 } else { match __wl.checked_div(__wr) { Some(__o) => __o, None => { return Err(-3); } } } }; match __wl.checked_sub(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } })); } #[no_mangle] pub extern "C" fn mlx_one_payment(principal: i32, months: i32, month: i32, out_value: *mut i32) -> i32 { diff --git a/docs/HISTORY.md b/docs/HISTORY.md index 9a93e40..ba82e2a 100644 --- a/docs/HISTORY.md +++ b/docs/HISTORY.md @@ -40,6 +40,7 @@ --- +### 9-73. 넓은 중간값 슬라이스 (2026-09-27, E2) — **`!` 문맥의 순수 산술 식은 정확히 계산되고, 뿌리에서 한 번 좁혀진다** → [본문](history/9-73.md) ### 9-72. 헬퍼 체크 전파 슬라이스 (2026-09-26, E2) — **`!`를 위해 실행되는 산술은 어디에 쓰여 있든 검사된다** → [본문](history/9-72.md) ### 9-71. 체크드 산술 다음을 쟀다 (2026-09-26, E2) — **헬퍼 체크 전파가 조용한 오답을 가장 많이 줄인다** → [본문](history/9-71.md) ### 9-70. 체크드 정수 산술 슬라이스 (2026-09-26, E2) — **`!` 본문의 오버플로가 `-3`이 됐다** → [본문](history/9-70.md) diff --git a/docs/STATUS.md b/docs/STATUS.md index c23ddb5..e898bf6 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -227,26 +227,25 @@ > ## ▶ 여기서 시작한다 > -> ### 2026-09-26 기준 (6) — **헬퍼 체크 전파 슬라이스가 닫혔다: `!`를 위해 실행되는 산술은 어디서든 검사된다 (§9-72)** +> ### 2026-09-27 기준 — **넓은 중간값 슬라이스가 닫혔다: `!` 문맥의 순수 산술 식은 정확히 계산된다 (§9-73)** > -> §9-71의 권고안을 슬라이스로 닫았다(#338 SPEC · #339 구현). `!` 함수가 부른 무한 함수(export 포함) 안의 산술도 넘치면 -> `-3`이 전파되고, 같은 함수를 무한 본문·호스트가 부르면 wrap한다. 바인딩은 한 집합으로 선언하고, 닿지 않는 모듈의 -> 생성 Rust는 글자 그대로 같다. 조용한 오답 60 → 44(626행, 시험 구현과 같다). DP-O7(무한 헬퍼 = 탈출구)은 뒤집혔다. +> SPEC을 권고안대로 확인받아 슬라이스로 닫았다(#341 SPEC · #342 구현). `!` 문맥의 순수 산술 식은 i64로 계산해 값이 +> i32가 되어야 하는 자리에서 한 번 좁힌다. 참값이 드는데 `-3`인 행 59 → 20(626행, 시험 구현과 행마다 같다). 실제 C 호스트가 +> 바꾼 `one_payment`로 곱이 i32 밖인 입력의 정답을 받는다. 지문·ABI·바인딩은 그대로다. > > **▶ 다음 세션 — 여기서 시작한다.** 순서대로: > -> 1. **넓은 중간값 — 확정(2026-09-27), 구현 중.** `docs/slices/SPEC-wide-intermediates.md`의 DP-W1~W11을 권고안대로 -> 확인받았다(**순수 트리만** — 멈춤·앞지름 없이 참값이 드는데 `-3`인 행 59 → 20). §6 작업 1(codegen)이 들어가면 남는 것은 -> 작업 2 — 기존 예제의 한 식을 실제 C 호스트로 재고, 626행을 구현본으로 다시 잰다. 시험 구현은 로컬 브랜치 -> `exp/wide2-local`에 있다(푸시 안 함). +> 1. **강제되는 슬라이스가 없다 — 다음은 측정이다.** 참값이 드는데 `-3`으로 남은 20행 중 17행(FULL로도 남는 행)이 +> 무엇인지 귀속하지 않았다(§9-73.7). 귀속이 `i64` 타입이나 다른 후보(`docs/slices/README.md`의 "다음 슬라이스" 절)를 +> 가리키면 그때 SPEC을 쓴다. > 2. **작은 항목**: C# 호스트(Phase 4) · LSP(Phase 3, 큰 일). > 3. **외부**: `X1`·`X2` — Delphi가 있는 CI 러너. 이 저장소 안에서는 닫히지 않는다. > > ⚠ **이 머신의 전체 게이트는 6회 중 2회 실패한다**(§9-63.5) — 실패를 보면 먼저 원인을 읽는다. > 강한 신호는 CI 두 잡이다. > -> 📌 **본문은 §9-72다**(`docs/history/9-72.md`). 그 앞의 2026-09-26 (5) 항목(체크드 산술 다음 측정)은 -> 바이트 그대로 옮겼다 — 지금은 `docs/history/start-block-053.md`다. +> 📌 **본문은 §9-73이다**(`docs/history/9-73.md`). 그 앞의 2026-09-26 (6) 항목(헬퍼 체크 전파 닫힘)은 +> 바이트 그대로 옮겼다 — 지금은 `docs/history/start-block-054.md`다. > > > ### 그 앞의 항목들 — **본문은 `docs/history/start-block-NNN.md`로 옮긴다 (2026-09-23부터)** diff --git a/docs/history/9-73.md b/docs/history/9-73.md new file mode 100644 index 0000000..8d03219 --- /dev/null +++ b/docs/history/9-73.md @@ -0,0 +1,74 @@ +### 9-73. 넓은 중간값 슬라이스 (2026-09-27, E2) — **`!` 문맥의 순수 산술 식은 정확히 계산되고, 뿌리에서 한 번 좁혀진다** + +사용자가 SPEC 초안의 DP-W1~W11을 권고안 그대로 확인했다(*"권고안 기준으로"*, 2026-09-27). Grok 호출은 사용자의 앞선 +요청대로 한 번에 주장 하나로 보냈다. + +#### 9-73.1. 들어간 것 — PR 셋 + +| PR | 내용 | +|---|---| +| #341 | `SPEC-wide-intermediates.md` 초안 — 헬퍼 체크 전파 뒤로 네 변형을 다시 잰 표(§0.2)와 DP-W1~W11 | +| #342 | `ir::loop_free_functions` · 순수 트리 판정(`is_pure` · `is_leaf_argument`) · i64 계산(`emit_exact`) · 뿌리 좁힘과 비교(`emit_wide`) · 오라클 · 골든 · 문서. 이 규칙이 옮긴 기존 고정 둘(`checked_arithmetic`의 `mid`, `helper_check_propagation`의 `big`) | +| 이 기록의 PR | 기존 예제의 한 식을 바꿔 실제 C 호스트가 정답을 받는다(수용 F) · 626행 재측정(수용 I) · 크기 재측정 · 슬라이스 닫기 | + +#### 9-73.2. 구현 중에 잰 대가 — 헬퍼의 `return`도 좁힌다 + +SPEC §2.6은 `let` 추출만 적었다. 구현 중 같은 산술을 세 가지로 쟀다(46341, 제곱이 i32 밖): 인라인 `x * x / x`는 `46341`, +`let t = x * x return t / x`와 `sq(x) / x`는 `-3`. 호출 잎은 헬퍼가 **돌려준 i32**를 잎으로 받을 뿐 그 안의 식을 넓히지 +않는다 — 헬퍼의 `return`이 좁히는 자리다. §2.6과 `LANGUAGE.md`에 한 줄씩 더했고 `wide_intermediates.rs`가 세 값을 고정한다. + +#### 9-73.3. 수용 F와 I, 그리고 크기 + +- **F — 실제 C 호스트**: 여섯 예제 어디에도 중간값만 넘치는 식이 없었다(본문을 전부 읽음). 그래서 DP-W11대로 한 식을 + 바꿨다: `examples/schedule.mls`의 `one_payment`를 **두 누적 몫의 차** `principal * (month + 1) / months - + principal * month / months`로(본문만 — 골든의 헤더·유닛 0줄, 지문 불변). 1,000,000,000을 12개월로 나누면 `month` 2부터 + `principal * (month + 1)`이 i32 밖이고 답은 든다. `host.c`가 `one_payment(1e9, 12, 2) = 83333334`와 열두 달 합 = + 원금을 받는다. **슬라이스 전 코드젠(8438cf9)으로 같은 `host.c`를 돌리면 새 검사 둘만 FAIL**(`GATE_D_FAILED (2)`), + 도메인 에러 검사는 통과한다. + - **대가:** 나머지가 첫 달에 몰리지 않고 한 단위씩 퍼진다(100000/7이면 `month` 1·2·4·5·6). 합이 원금이라는 성질은 그대로이고 + 어떤 입력에서도 답이 i32에 든다. `array_return.rs`가 새 값을 고정한다. +- **I — 626행**: 머지된 `main`(b077cb9)으로 빌드한 `mlprobe`의 출력이 시험 구현(PURE+CALL 최종)과 **626행 전부 같다**. + 표는 맞음 543 · 조용한 오답 44 · 참값이 드는데 `-3` 20 · 기타 18(판정 불명 0). `main` 대비 **출력**이 바뀐 행은 42이고, 범주 표의 순이동은 39다. §0.3의 무작위 + 48,000호출은 시험 구현의 환경 스위치에 기대는 비교라 구현본으로 다시 돌리지 않았다 — **이 수용의 표본은 626행이다.** +- **크기**: 예제 26개 `.text` 합 95,334 → 95,472(+138), 모듈별 −123~+192, 여섯 모듈 — PURE로 잰 §0.4와 **같다**. + `.text` virtual size를 PE 헤더에서 직접 읽었다. 바꾼 `one_payment`로는 `schedule`이 3640 → 3656. + +#### 9-73.4. 결함 심기 + +커밋된 트리에서 열을 심었고(`--no-fail-fast`) 전부 제 테스트에서 떨어졌다: 배열 읽기를 잎으로(B, `-2`가 `-3`을 앞지름) · +`while` 호출 허용(B와 C의 10초 기한) · 문자열 인자 검사 제거 · `byte_len`을 잎으로(B — 이 심기 전에는 잡는 단언이 없어 +`direct_blen`을 더했다) · `try_from` 대신 `as i32`(다섯 테스트) · 0 제수 보호 제거(`checked_arithmetic`도) · 정확한 비교 +제거 · `as f64`를 넓힌 채 변환 · 무한 본문도 넓힘 · `len`을 잎에서 뺌. + +- **무한 본문 심기는 처음에 빌드가 깨져 떨어졌다** — `emit_exact`가 자기 bail을 따로 구했기 때문에 한쪽만 바꾼 심기가 + 생성 Rust를 컴파일되지 않게 했다. 값이 아니라 빌드로 떨어진 빨강이라 두 곳을 같이 바꿔 다시 심었다(`plain` 100000 ≠ 14100). +- **대입 · 인자 · 인덱스에서 좁히는 단언은 첫 실행부터 초록이었다.** 그 셋만 담은 탐침을 슬라이스 전 코드젠으로 돌려 + `-3`, 지금 코드젠으로 정확한 값을 받아 단언이 둘을 가른다는 것을 보였다. + +#### 9-73.5. Grok + +- **plan**(SPEC 착수): PURE 대 FULL에 PURE · PURE 안의 재배열 없음 · `as f64`는 먼저 좁힌다(2^53 위의 i64가 반올림돼 + 새 조용한 오답이 된다). +- **SPEC verify**: 규칙 서술 CONFIRMED · 건전성 논증 DISCREPANCY 둘(→ `byte_len`과 문자열 인자 호출을 잎에서 뺐고, *"트리 + 밖의 무엇보다 먼저"* 를 *"트리보다 뒤에 평가되는 무엇보다 먼저"* 로 좁혔다) · 내부 일관성 DISCREPANCY(수용 I의 범위, + §1/§2.1 경계, DP-W11의 §6, 표의 기타 열) → 재검증 CONFIRMED. +- **구현 verify** 여덟: 잎 집합 · 문자열 규칙 · `emit_exact`의 순서·0 제수·나머지 · `emit_wide`의 무한 본문 무변경과 비교 + 관문 · bail 전달 · 문서 값 ↔ 단언 CONFIRMED. `loop_free_functions`의 DISCREPANCY는 **내 질문의 오류**였다(`If`만 + 문장을 품는다고 썼는데 `While`도 품는다 — 코드는 그것을 이미 참으로 센다). 묻지 않은 지적 다섯은 코드로 다시 확인했다: + `len` 잎과 대입·인자·인덱스 좁힘이 고정되지 않음 → **단언 추가** · `emit_exact`의 `unwrap_or_default` bail → **인자로 + 받게 바꿈** · 비교 관문이 `rhs.ty`를 안 봄 → typeck가 양쪽을 한 타입으로 준다(주석) · `Len`이 피연산자를 무시 → `Len`에는 + 피연산자가 없다 · 문자열이 아닌 `ConstStr` → 생길 수 없다. +- 타임아웃 1회 — 주장 둘을 한 호출에 묶은 것. 하나씩 다시 보내 닫았다. + +#### 9-73.6. 그 밖에 기록할 것 + +- 거부 단언의 메시지에 심볼 이름의 NUL 바이트가 섞여 `grep`이 출력을 이진으로 읽었다 — 이름에서 NUL을 떼어 고쳤다. +- 로컬 실험 브랜치 `exp/wide-local` · `exp/wide2-local`은 남아 있다(푸시 안 함). 이 슬라이스로 둘 다 할 일을 마쳤다. + +#### 9-73.7. 남은 것 + +- **참값이 드는데 `-3`인 20행** — 그중 3행은 배열 읽기가 든 식이다(PURE+INDEX가 되찾지만 앞지름 위험 때문에 뺐다). + 나머지 17행은 FULL로도 남는 행이고, **무엇인지는 아직 귀속하지 않았다** — 다음 측정의 가장 가까운 입력이다. + 중간값을 담는 자리까지 정답을 주는 후보는 **`i64` 타입**이다. +- **`wrapping_*` 내장 함수** — 의도한 wrap이 필요한 규칙이 측정되면. +- **C 백엔드의 실제 구현**(§2.8) — 요구는 `LANGUAGE.md`에 있다. diff --git a/docs/history/start-block-054.md b/docs/history/start-block-054.md new file mode 100644 index 0000000..f1024a5 --- /dev/null +++ b/docs/history/start-block-054.md @@ -0,0 +1,21 @@ +> ### 2026-09-26 기준 (6) — **헬퍼 체크 전파 슬라이스가 닫혔다: `!`를 위해 실행되는 산술은 어디서든 검사된다 (§9-72)** +> +> §9-71의 권고안을 슬라이스로 닫았다(#338 SPEC · #339 구현). `!` 함수가 부른 무한 함수(export 포함) 안의 산술도 넘치면 +> `-3`이 전파되고, 같은 함수를 무한 본문·호스트가 부르면 wrap한다. 바인딩은 한 집합으로 선언하고, 닿지 않는 모듈의 +> 생성 Rust는 글자 그대로 같다. 조용한 오답 60 → 44(626행, 시험 구현과 같다). DP-O7(무한 헬퍼 = 탈출구)은 뒤집혔다. +> +> **▶ 다음 세션 — 여기서 시작한다.** 순서대로: +> +> 1. **넓은 중간값 — 확정(2026-09-27), 구현 중.** `docs/slices/SPEC-wide-intermediates.md`의 DP-W1~W11을 권고안대로 +> 확인받았다(**순수 트리만** — 멈춤·앞지름 없이 참값이 드는데 `-3`인 행 59 → 20). §6 작업 1(codegen)이 들어가면 남는 것은 +> 작업 2 — 기존 예제의 한 식을 실제 C 호스트로 재고, 626행을 구현본으로 다시 잰다. 시험 구현은 로컬 브랜치 +> `exp/wide2-local`에 있다(푸시 안 함). +> 2. **작은 항목**: C# 호스트(Phase 4) · LSP(Phase 3, 큰 일). +> 3. **외부**: `X1`·`X2` — Delphi가 있는 CI 러너. 이 저장소 안에서는 닫히지 않는다. +> +> ⚠ **이 머신의 전체 게이트는 6회 중 2회 실패한다**(§9-63.5) — 실패를 보면 먼저 원인을 읽는다. +> 강한 신호는 CI 두 잡이다. +> +> 📌 **본문은 §9-72다**(`docs/history/9-72.md`). 그 앞의 2026-09-26 (5) 항목(체크드 산술 다음 측정)은 +> 바이트 그대로 옮겼다 — 지금은 `docs/history/start-block-053.md`다. +> diff --git a/docs/history/start-block-index.md b/docs/history/start-block-index.md index 0ae61ee..bc810a4 100644 --- a/docs/history/start-block-index.md +++ b/docs/history/start-block-index.md @@ -9,6 +9,7 @@ > | 날짜 | 무엇을 했나 | 본문 | > |---|---|---| +> | 2026-09-26 (6) | **헬퍼 체크 전파 슬라이스가 닫혔다: `!`를 위해 실행되는 산술은 어디서든 검사된다** — 다음 날 넓은 중간값 슬라이스로 닫혔다(§9-73) | §9-72 | > | 2026-09-26 (5) | **체크드 산술 다음을 쟀다: 헬퍼 체크 전파가 조용한 오답을 가장 많이 줄인다** — 같은 날 슬라이스로 닫혔다(§9-72) | §9-71 | > | 2026-09-26 (4) | **체크드 정수 산술 슬라이스가 닫혔다: `!` 본문의 오버플로가 `-3`이 됐다** — 같은 날 다음 후보를 쟀다(§9-71) | §9-70 | > | 2026-09-26 (3) | **§7을 열두 도메인으로 돌렸다: 가장 강한 근거는 체크드 산술이고, 설계 결정 하나에 걸려 있다** — 같은 날 슬라이스로 닫혔다(§9-70) | §9-69 | diff --git a/docs/slices/README.md b/docs/slices/README.md index a1245f0..04947a5 100644 --- a/docs/slices/README.md +++ b/docs/slices/README.md @@ -64,7 +64,7 @@ TDD 구현 → Grok 검증 → PR** 순서를 따른다(`CLAUDE.md` "개발 방 | [상수 선언 `const` · `export const`](SPEC-constants.md) | ✅ **구현 완료** (2026-09-26) | 이름 붙은 리터럴 — `export const`만 헤더(`ML__CONST_`)와 지문에 나가, 번호를 바꾼 모듈을 게이트가 거부한다 | #325 / #326·#327 | | [체크드 정수 산술](SPEC-checked-arithmetic.md) | ✅ **구현 완료** (2026-09-26) | `!` 본문의 i32 오버플로와 `f64 as i32`가 `ML_ST_OVERFLOW`(`-3`)로 실패한다 — 조용한 오답 161행 중 101이 status가 된다 | §9-69 / #334 · §9-70 | | [헬퍼 체크 전파](SPEC-helper-check-propagation.md) | ✅ **구현 완료** (2026-09-26) | `!` 함수가 부른 무한 함수(export 포함)의 산술도 검사하고 `-3`을 전파한다 — 조용한 오답 60 → 44 | §9-71 / #339 · §9-72 | -| [넓은 중간값](SPEC-wide-intermediates.md) | 🔨 **확정 · 구현 중** (2026-09-27) | `!` 문맥의 순수 산술 식을 정확히 계산하고 뿌리에서만 좁힌다 — 참값이 드는데 `-3`인 행 59 → 20(시험 구현) | §9-71 · §9-72 / #341 | +| [넓은 중간값](SPEC-wide-intermediates.md) | ✅ **구현 완료** (2026-09-27) | `!` 문맥의 순수 산술 식을 정확히 계산하고 뿌리에서만 좁힌다 — 참값이 드는데 `-3`인 행 59 → 20 | §9-72 / #342 · §9-73 | > **2026-09-25에 행을 한 줄로 접었다.** 접기 전의 서술은 [`../history/slices-index.md`](../history/slices-index.md)에 > 바이트 그대로 있다. **새 행도 한 줄로 쓴다** — 행당 400 B(`every_slice_index_row_is_one_line`)이고, 경위는 그 @@ -127,7 +127,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규칙과 귀속 대조)이 더한 후보: **넓은 중간값**(SPEC 확정 · 구현 중, 위 색인), **`wrapping_*` 내장 함수**(무한 헬퍼라는 탈출구(DP-O7)가 §9-72로 사라졌다 — 필요가 측정되면), **i64**(§9-71: 옵트인이라 귀속 대조에서 51행이 빠졌다), **입력 문자열의 인코딩 계약**(닫힌 DP-S2의 재개 — `OPEN_QUESTIONS.md` Q17이 (A)로 열어 두었고 재검토 조건은 거기 있다), 비트 연산자, +§7(§9-69, 12개 도메인 72규칙과 귀속 대조)이 더한 후보: **`wrapping_*` 내장 함수**(무한 헬퍼라는 탈출구(DP-O7)가 §9-72로 사라졌다 — 필요가 측정되면), **i64**(§9-71: 옵트인이라 귀속 대조에서 51행이 빠졌다), **입력 문자열의 인코딩 계약**(닫힌 DP-S2의 재개 — `OPEN_QUESTIONS.md` Q17이 (A)로 열어 두었고 재검토 조건은 거기 있다), 비트 연산자, 지역 작업 배열, 수학 내장 함수, 문자 단위 길이. **struct는 §9-1이 강제되지 않는다고 결론냈다** — 고르려면 그 절을 먼저 읽는다(§9-69도 귀속 0으로 다시 확인했다). 배열도 같은 결론이었고(§9-9가 다섯 번째로), **입력은 그 사실을 SPEC 첫 절에 적은 채로 열렸다**. diff --git a/docs/slices/SPEC-wide-intermediates.md b/docs/slices/SPEC-wide-intermediates.md index 06af8ca..612f1b7 100644 --- a/docs/slices/SPEC-wide-intermediates.md +++ b/docs/slices/SPEC-wide-intermediates.md @@ -1,7 +1,12 @@ # SPEC — 넓은 중간값 (순수 산술 식은 정확히 계산하고, 뿌리에서만 좁힌다) -- **상태: 확정 · 구현 중.** §4의 DP-W1~W11을 사용자가 권고안대로 확인했다(2026-09-27). §6의 작업 1이 codegen이고, - 작업 2(실제 C 호스트 · 626행 재측정)가 슬라이스를 닫는다. +> **기록 문서다.** 이 SPEC은 닫힌 슬라이스의 설계 기록이다 — 본문은 닫힌 날의 사실이고 다시 고치지 않는다. +> 현재 상태는 [`docs/STATUS.md`](../STATUS.md)가 말한다. + +> **상태: 확정 · 구현 완료** — DP-W1~W11 사용자 확인(권고안 그대로) 2026-09-27 / SPEC #341 · 구현 #342 · 호스트와 +> 재측정은 `HISTORY.md` §9-73. 수용 A~I 전부 닫혔다. **근거 수준:** E2 — 로드한 모듈의 반환값, 실제 C 호스트, 구현으로 +> 다시 잰 626행(시험 구현과 행마다 같다, §9-73). + - 선행: `SPEC-checked-arithmetic.md`(§2.1 — 검사 자리는 **연산자** · DP-O9 — 리터럴만의 오버플로는 실행 시 `-3`) · `SPEC-helper-check-propagation.md`(검사된 사본도 fallible 문맥이다) - 관련 결정: **D17**(음수 status 예약) · **D19**(C-emit 백엔드의 여지) @@ -70,8 +75,8 @@ ### 0.4 크기 (E2) -PURE로 잰 값: 예제 26개 `.text` 합 95,334 → 95,472바이트(+138), 모듈별 −123~+192, 6개 모듈만 바뀐다. PURE+CALL은 잎만 -늘어나므로 같은 방식으로 다시 잰다(§6 작업 1). +PURE로 잰 값: 예제 26개 `.text` 합 95,334 → 95,472바이트(+138), 모듈별 −123~+192, 6개 모듈만 바뀐다. 구현(PURE+CALL)으로 +다시 쟀더니 **같은 값**이다(§9-73). --- diff --git a/examples/schedule.mls b/examples/schedule.mls index 165ccac..5688e23 100644 --- a/examples/schedule.mls +++ b/examples/schedule.mls @@ -1,8 +1,8 @@ // SPEC-array-return, acceptance A. One of the two rules that opened the slice (§0.1). // -// Instalments: the principal split over `months`, with the remainder folded into the first -// payment so the parts sum to exactly the principal. Before array return the host called this -// once per month and assembled the schedule itself. +// Instalments: the principal split over `months`. `schedule` returns the equal parts; +// `one_payment` spreads the remainder so its parts sum to exactly the principal. Before array +// return the host called `one_payment` once per month and assembled the schedule itself. // // The length is declared FIRST. That is where the host's capacity is checked, before a single // element is written, which is how a truncated call still writes nothing (SPEC §2.4). @@ -21,11 +21,15 @@ export fn schedule(principal: i32, months: i32) -> [i32]! { // The same split, as a single payment, so a host that wants one month need not take the // whole schedule. It also keeps a NON-array export in this module, which is what pins that // the buffer triple is added per function rather than per module. +// +// Month `m` is the difference of two cumulative shares, so the remainder is spread one unit at +// a time and the parts telescope to exactly the principal. Each product can leave i32 while +// the payment fits — 1,000,000,000 over 12 months — and SPEC-wide-intermediates computes the +// expression exactly and narrows it once, so the host gets the payment instead of +// ML_ST_OVERFLOW (acceptance F, asserted in hosts/c-host/host.c). export fn one_payment(principal: i32, months: i32, month: i32) -> i32! { if months <= 0 { fail E_BAD_TERM } if month < 0 { fail E_BAD_TERM } if month >= months { fail E_BAD_TERM } - let base = principal / months - if month == 0 { return base + principal % months } - return base + return principal * (month + 1) / months - principal * month / months } diff --git a/hosts/c-host/host.c b/hosts/c-host/host.c index 1bcd891..8129887 100644 --- a/hosts/c-host/host.c +++ b/hosts/c-host/host.c @@ -99,6 +99,9 @@ _Static_assert(_Generic(&mlx_next_state, next_state_fn: 1, default: 0), * and here ml_cap and ml_needed count ELEMENTS -- the header says so, and this host allocates * with the multiplication on purpose so the trap is written in code and not only in prose. */ typedef int32_t (*schedule_fn)(int32_t, int32_t, int32_t *, int32_t, int32_t *); +typedef int32_t (*one_payment_fn)(int32_t, int32_t, int32_t, int32_t *); +_Static_assert(_Generic(&mlx_one_payment, one_payment_fn: 1, default: 0), + "generated mlx_one_payment signature changed"); typedef int32_t (*allocate_fn)(const int32_t *, int32_t, int32_t, int32_t *, int32_t, int32_t *); typedef int32_t (*in_stock_fn)(const int32_t *, int32_t, bool *, int32_t, int32_t *); @@ -1465,6 +1468,34 @@ int main(int argc, char **argv) { "a negative capacity is zero, not an enormous unsigned one"); } + /* SPEC-wide-intermediates acceptance F. one_payment is + principal * (month + 1) / months - principal * month / months: at 1,000,000,000 over + 12 months, principal * (month + 1) leaves int32_t from month 2 on while every payment + fits. Checked at each operator that was ML_ST_OVERFLOW; the expression is pure, so the + module now computes it exactly and narrows once -- the host gets the payment. */ + one_payment_fn one_payment = (one_payment_fn)sym(sc, "mlx_one_payment"); + if (one_payment) { + int32_t pay = -999; + check(one_payment(1000000000, 12, 2, &pay) == 0 && pay == 83333334, + "one_payment(1e9, 12, 2) is 250000000 - 166666666 although 3e9 has no int32_t"); + int32_t total = 0; + int answered = 1; + for (int32_t m = 0; m < 12; m++) { + pay = -999; + if (one_payment(1000000000, 12, m, &pay) != 0) { + answered = 0; + } else { + total += pay; + } + } + check(answered && total == 1000000000, + "every month answers and the twelve payments sum to the principal exactly"); + /* The domain check comes first and still owns its status. */ + pay = -999; + check(one_payment(1000000000, 12, 12, &pay) == ML_SCHEDULE_ERR_E_BAD_TERM && pay == -999, + "month 12 of 12 is the domain error and leaves the out-param untouched"); + } + HMODULE al = load(dir, "allocate.dll", expected_abi, ML_ALLOCATE_IFACE_HASH); if (al == NULL) { return 1; diff --git a/hosts/rust-oracle/tests/array_return.rs b/hosts/rust-oracle/tests/array_return.rs index 8beda3c..f64d687 100644 --- a/hosts/rust-oracle/tests/array_return.rs +++ b/hosts/rust-oracle/tests/array_return.rs @@ -296,32 +296,39 @@ fn a_bool_result_is_one_byte_per_element() { /// pass every other test in this file and break every scalar export beside it -- and the /// generated header would agree with the mistake, because both come from the same place. /// -/// `one_payment` is also the workaround the slice replaced: one call per month, with the -/// remainder folded into the first. Keeping it callable is deliberate; a host that wants a -/// single month should not have to take the whole schedule. +/// `one_payment` is also the workaround the slice replaced: one call per month. Keeping it +/// callable is deliberate; a host that wants a single month should not have to take the whole +/// schedule. Since SPEC-wide-intermediates it spreads the remainder (the difference of two +/// cumulative shares) instead of folding it into the first month. #[test] fn a_scalar_export_beside_an_array_one_keeps_the_plain_d17_shape() { let (_d, m) = build("schedule", "scalar"); let one: OnePayment = unsafe { std::mem::transmute(m.symbol(b"mlx_one_payment\0").unwrap()) }; - let mut got = -999i32; - let st = unsafe { one(100_000, 7, 0, &mut got) }; - assert_eq!(st, 0); - assert_eq!(got, 14_290, "the first payment carries the remainder"); - - let mut rest = -999i32; - assert_eq!(unsafe { one(100_000, 7, 3, &mut rest) }, 0); - assert_eq!(rest, 14_285); + // floor(100000·(m+1)/7) − floor(100000·m/7): the five left over land one each on months + // 1, 2, 4, 5 and 6. + let mut months = [0i32; 7]; + for (month, v) in months.iter_mut().enumerate() { + assert_eq!(unsafe { one(100_000, 7, month as i32, v) }, 0); + } + assert_eq!( + months, + [14_285, 14_286, 14_286, 14_285, 14_286, 14_286, 14_286] + ); // And the whole schedule still sums to the principal, which the array return alone cannot - // show: its elements are equal, so an off-by-one in the fold would be invisible there. - let mut total = 0i32; - for month in 0..7 { - let mut v = 0i32; - assert_eq!(unsafe { one(100_000, 7, month, &mut v) }, 0); - total += v; - } - assert_eq!(total, 100_000, "the parts sum to the principal exactly"); + // show: its elements are equal, so an off-by-one in the spread would be invisible there. + assert_eq!( + months.iter().sum::(), + 100_000, + "the parts sum to the principal exactly" + ); + + // The input of acceptance F, which the C host asserts too: 1e9 · 3 has no i32 value, the + // payment does (SPEC-wide-intermediates). + let mut big = -999i32; + assert_eq!(unsafe { one(1_000_000_000, 12, 2, &mut big) }, 0); + assert_eq!(big, 83_333_334); // The domain error is untouched by this slice, and a failed call writes no out-param. let mut canary = 0x5A5A_5A5Ai32;