diff --git a/compiler/tests/golden/generated.rs.txt b/compiler/tests/golden/generated.rs.txt index be5045f..e7d4a5f 100644 --- a/compiler/tests/golden/generated.rs.txt +++ b/compiler/tests/golden/generated.rs.txt @@ -353,6 +353,10 @@ pub extern "C" fn ml_module_abi_version() -> u32 { 1 } #[no_mangle] pub extern "C" fn ml_iface_hash_basket() -> u64 { 0x5D04BA666CC0CBC6 } +fn ml_ck_line_total(q: i32, p: i32) -> Result { + return Ok((match (q).checked_mul(p) { Some(__o) => __o, None => { return Err(-3); } })); +} + fn ml_fn_basket_total(qty: *const i32, qty_len: i32, price: *const i32, price_len: i32, cap: i32) -> Result { if (qty_len != price_len) { return Err(1); @@ -360,7 +364,7 @@ fn ml_fn_basket_total(qty: *const i32, qty_len: i32, price: *const i32, price_le let mut total = 0i32; let mut i = 0i32; while (i < qty_len) { - let line = (match ({ let __i = i; if __i < 0 || __i >= qty_len { return Err(-2); } unsafe { *qty.add(__i as usize) } }).checked_mul({ let __i = i; if __i < 0 || __i >= price_len { return Err(-2); } unsafe { *price.add(__i as usize) } }) { Some(__o) => __o, None => { return Err(-3); } }); + let line = (match ml_ck_line_total({ let __i = i; if __i < 0 || __i >= qty_len { return Err(-2); } unsafe { *qty.add(__i as usize) } }, { let __i = i; if __i < 0 || __i >= price_len { return Err(-2); } unsafe { *price.add(__i as usize) } }) { Ok(__v) => __v, Err(__e) => { return Err(__e); } }); if (line > cap) { total = (match (total).checked_add(cap) { Some(__o) => __o, None => { return Err(-3); } }); } diff --git a/docs/HISTORY.md b/docs/HISTORY.md index 0814511..9a93e40 100644 --- a/docs/HISTORY.md +++ b/docs/HISTORY.md @@ -40,6 +40,7 @@ --- +### 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) ### 9-69. §7을 열두 도메인으로 돌렸다 (2026-09-26, E2) — **가장 강한 근거는 체크드 산술이고, 그것은 설계 결정 하나에 걸려 있다** → [본문](history/9-69.md) diff --git a/docs/STATUS.md b/docs/STATUS.md index e71e7cf..0acb53f 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -227,25 +227,25 @@ > ## ▶ 여기서 시작한다 > -> ### 2026-09-26 기준 (5) — **체크드 산술 다음을 쟀다: 헬퍼 체크 전파가 조용한 오답을 가장 많이 줄인다 (§9-71)** +> ### 2026-09-26 기준 (6) — **헬퍼 체크 전파 슬라이스가 닫혔다: `!`를 위해 실행되는 산술은 어디서든 검사된다 (§9-72)** > -> 남은 103행을 기능에 귀속하고(귀속 대조 포함), 상위 두 설계를 로컬 브랜치에서 구현해 626행 전부로 다시 쟀다. -> 어느 모드도 맞던 status 0 답을 바꾸지 않았다. 조용한 오답은 **헬퍼 체크 전파(F2)** 가 60 → 44로 줄이고, -> **넓은 중간값(WIDE)** 은 참값이 드는데 `-3`인 행을 52 → 17로 줄이지만 멈춤·추출 위험을 갖고 있다(§9-71.4). +> §9-71의 권고안을 슬라이스로 닫았다(#338 SPEC · #339 구현). `!` 함수가 부른 무한 함수(export 포함) 안의 산술도 넘치면 +> `-3`이 전파되고, 같은 함수를 무한 본문·호스트가 부르면 wrap한다. 바인딩은 한 집합으로 선언하고, 닿지 않는 모듈의 +> 생성 Rust는 글자 그대로 같다. 조용한 오답 60 → 44(626행, 시험 구현과 같다). DP-O7(무한 헬퍼 = 탈출구)은 뒤집혔다. > > **▶ 다음 세션 — 여기서 시작한다.** 순서대로: > -> 1. **헬퍼 체크 전파 — 구현 중.** DP-P1~P11 전부 사용자 확인(2026-09-26). `docs/slices/SPEC-helper-check-propagation.md` -> §6의 작업 1(검사 집합 · 사본 · 바인딩 술어 · 테스트 · 문서)이 들어갔고, **작업 2가 남았다** — 예제에 헬퍼를 넣어 -> 실제 C 호스트가 `-3`을 받는 수용 F, §9-71의 626행 재측정, 슬라이스 닫기. +> 1. **다음 슬라이스 — 사용자 결정.** 후보의 정본은 `docs/slices/README.md`의 "다음 슬라이스" 절이다. 가장 가까운 것은 +> **넓은 중간값(WIDE)** 이다 — 참값이 드는데 `-3`인 행을 줄이지만 §9-71.4의 위험을 SPEC이 정해야 하고, 헬퍼 체크 전파 +> 뒤로 그 표를 다시 재야 한다(§9-72.7). 시험 구현은 로컬 브랜치 `exp/wide-local`에 있다(푸시 안 함). > 2. **작은 항목**: C# 호스트(Phase 4) · LSP(Phase 3, 큰 일). > 3. **외부**: `X1`·`X2` — Delphi가 있는 CI 러너. 이 저장소 안에서는 닫히지 않는다. > > ⚠ **이 머신의 전체 게이트는 6회 중 2회 실패한다**(§9-63.5) — 실패를 보면 먼저 원인을 읽는다. > 강한 신호는 CI 두 잡이다. > -> 📌 **본문은 §9-71이다**(`docs/history/9-71.md`). 그 앞의 2026-09-26 (4) 항목(체크드 산술 닫힘)은 -> 바이트 그대로 옮겼다 — 지금은 `docs/history/start-block-052.md`다. +> 📌 **본문은 §9-72다**(`docs/history/9-72.md`). 그 앞의 2026-09-26 (5) 항목(체크드 산술 다음 측정)은 +> 바이트 그대로 옮겼다 — 지금은 `docs/history/start-block-053.md`다. > > > ### 그 앞의 항목들 — **본문은 `docs/history/start-block-NNN.md`로 옮긴다 (2026-09-23부터)** diff --git a/docs/history/9-72.md b/docs/history/9-72.md new file mode 100644 index 0000000..679ee24 --- /dev/null +++ b/docs/history/9-72.md @@ -0,0 +1,68 @@ +### 9-72. 헬퍼 체크 전파 슬라이스 (2026-09-26, E2) — **`!`를 위해 실행되는 산술은 어디에 쓰여 있든 검사된다** + +사용자가 §9-71의 권고안 F2를 골랐고(*"권고안으로 진행"*), SPEC 초안의 DP-P2~P11을 권고안 그대로 확인했다. +Grok 호출은 사용자의 앞선 요청대로 한 번에 주장 하나로 보냈다. + +#### 9-72.1. 들어간 것 — PR 셋 + +| PR | 내용 | +|---|---| +| #338 | `SPEC-helper-check-propagation.md` 초안 — 쓰기 전에 잰 것(9-72.2)과 DP-P1~P11 | +| #339 | `ir::checked_helpers`(한 집합) · 사본 `ml_ck_` · 참조되는 본문만 방출 · 바인딩 술어 · `Cx` 문맥 · 테스트 · 문서. DP-O7을 고정하던 줄은 새 규칙으로 뒤집었다 | +| 이 기록의 PR | 예제에 헬퍼를 넣어 실제 C 호스트가 헬퍼 경로의 `-3`을 받는다(수용 F) · 626행 재측정(수용 I) · 슬라이스 닫기 | + +#### 9-72.2. SPEC 전에 잰 것 + +워크플로(에이전트 셋 — 코퍼스 조사 · 설계 반론 · 크기)로 시험 구현(`exp/wide-local`의 `twin` 모드)을 쟀다. + +- **의도한 wrap에 기대는 헬퍼는 어느 코퍼스에도 없다** — 컴파일러 IR로 센 것. §7 83파일의 헬퍼 50개가 전부 `!`에서 닿고 + 17개가 검사할 연산을 가진다. 의도한 wrap은 합성 해시·LCG로만 보였다. +- **시험 구현의 결함 다섯**이 SPEC의 결정이 됐다: 바인딩이 헬퍼 경로의 `-3`을 선언하지 않음(DP-P6) · 쌍둥이 이름 충돌 + E0428(DP-P7) · 주변 `-D warnings`에서 빌드 실패와 쓸모없는 사본(DP-P8) · `export`가 검사를 멈춤(DP-P2). +- 그중 충돌 · `-D warnings`(`examples/discount4.mls`) · export 경계, 그리고 지문 불변과 `grow(1, n)`의 멈춤(오늘 30초 + 타임아웃, 사본으로 즉시 `-3`)은 **손으로 다시 쟀다** — 처음 두 시도는 탐침을 잘못 세워(`grep`이 주석 줄을 잡음, + `grow(MAX, MAX)`가 즉시 돌아옴) 다시 했다. + +#### 9-72.3. 수용 F와 I + +- **F — 실제 C 호스트**: `examples/basket.mls`의 줄 합을 `!` 없는 내부 헬퍼 `line_total`로 옮겼다(내부라 지문 불변 — + 골든의 `IFACE_HASH` 0줄). 같은 예제를 헬퍼 전파 전 컴파일러(#334 빌드의 `mlprobe`)로 부르면 `basket_total(INT32_MAX, 2)`가 + **status 0에 `-2`**(조용한 오답으로 되돌아감), 지금은 `-3`이다. `host.c`의 기존 검사가 그대로 이 경로를 잰다. +- **I — 626행**: 구현본 `mlprobe`의 출력이 시험 구현(`twin`)과 **626행 전부 같다**. §9-71.3의 표(맞음 505 · 조용한 오답 44 · + 참값이 드는데 `-3` 59)가 구현에도 그대로다. 시험 구현은 export를 빼먹었지만(DP-P2) 코퍼스에 `!`에서 부르는 export 무한 + 함수가 0개라 표에는 차이가 없다. + +#### 9-72.4. 결함 심기 — 하나는 테스트를 고쳤다 + +커밋된 트리에서 일곱을 심었고(`--no-fail-fast`) 전부 적발됐다: 사본으로 안 부름 · 자기 본문만 보는 술어 · export 제외 · +평범한 본문 모두 유지 · 사용자 이름공간 안의 사본 이름 · 사본이 사슬을 안 탐 · 직접 호출만 도달. + +**이름 충돌 심기(`ml_fn_ck_`)는 처음에 값 테스트를 통과했다.** 그 모듈의 함수가 전부 `!`에서만 불려 평범한 본문이 +하나도 방출되지 않았고, 사본 이름이 부딪칠 상대가 없었다. 무한 호출자를 더해 평범한 본문을 살리자 E0428로 떨어졌다. +*"심은 결함이 떨어지는가"* 가 아니라 *"그 테스트가 그 결함을 볼 수 있는 모양인가"* 를 물은 것이 이 경우다. + +#### 9-72.5. Grok + +- **plan**(설계 착수): export 호출 대상 포함 YES · 한 집합으로 바인딩 술어 충분 · **`allow(dead_code)` 대신 참조되는 본문만 + 방출** — 덮으면 과다 방출이 숨는다. 이 답이 설계를 바꿨다. +- **SPEC verify** 다섯: §0.1 수치 CONFIRMED · `-2`의 범위(*무한* 헬퍼만, `fixed`의 이유) DISCREPANCY · `ml_ck_` 무충돌 + CONFIRMED · 내부 일관성 DISCREPANCY(수용 I의 범위 항목 없음, `allow(non_snake_case)`가 모든 모듈을 바꿔 수용 H와 충돌 → + 이미 있던 문제라 §5로) → 재검증 CONFIRMED. +- **구현 verify** 다섯: `ir.rs` · codegen · `Cx` 리팩터가 호출 자리의 `abi`를 바꾸지 않음 · 바인딩 한 술어 CONFIRMED · + 문서 ↔ 테스트 DISCREPANCY(무한 호출자의 *포화*를 헬퍼 쪽에서 재지 않음 → 단언 추가). +- **이 기록의 PR** 넷: 예제·골든·`host.c` · 옮긴 블록의 바이트(blob 동일) · 이 기록의 수치 · 슬라이스 닫기의 일관성 — + 전부 CONFIRMED. +- 타임아웃 0회. + +#### 9-72.6. 그 밖에 기록할 것 + +- PR 본문에 확인하지 않은 커밋 해시(`fb3a…`)를 적었다가 실제 해시(`624f7b6`)로 고쳤다 — 공개 저장소의 본문은 쓰는 즉시 + 보인다(STATUS §6). +- 로컬 실험 브랜치 `exp/wide-local`은 남아 있다(푸시 안 함) — 넓은 중간값(WIDE)의 출발점이다. + +#### 9-72.7. 남은 것 + +- **넓은 중간값(WIDE)** — 참값이 드는데 `-3`인 행을 52 → 17로 줄이지만 §9-71.4의 위험(멈춤 · 추출 · C 백엔드 · i64)을 + SPEC이 정해야 한다. 헬퍼 체크 전파 뒤로는 그 표가 59 → ?로 바뀌므로 다시 잰다. +- **`wrapping_*` 내장 함수** — DP-O7의 탈출구가 사라졌다. 의도한 wrap이 필요한 규칙이 측정되면 가산적으로. +- **주변 `RUSTFLAGS=-D warnings`의 기존 실패** — snake_case가 아닌 사용자 이름, 아무도 부르지 않는 함수(SPEC §5). diff --git a/docs/history/start-block-053.md b/docs/history/start-block-053.md new file mode 100644 index 0000000..b20fddf --- /dev/null +++ b/docs/history/start-block-053.md @@ -0,0 +1,20 @@ +> ### 2026-09-26 기준 (5) — **체크드 산술 다음을 쟀다: 헬퍼 체크 전파가 조용한 오답을 가장 많이 줄인다 (§9-71)** +> +> 남은 103행을 기능에 귀속하고(귀속 대조 포함), 상위 두 설계를 로컬 브랜치에서 구현해 626행 전부로 다시 쟀다. +> 어느 모드도 맞던 status 0 답을 바꾸지 않았다. 조용한 오답은 **헬퍼 체크 전파(F2)** 가 60 → 44로 줄이고, +> **넓은 중간값(WIDE)** 은 참값이 드는데 `-3`인 행을 52 → 17로 줄이지만 멈춤·추출 위험을 갖고 있다(§9-71.4). +> +> **▶ 다음 세션 — 여기서 시작한다.** 순서대로: +> +> 1. **헬퍼 체크 전파 — 구현 중.** DP-P1~P11 전부 사용자 확인(2026-09-26). `docs/slices/SPEC-helper-check-propagation.md` +> §6의 작업 1(검사 집합 · 사본 · 바인딩 술어 · 테스트 · 문서)이 들어갔고, **작업 2가 남았다** — 예제에 헬퍼를 넣어 +> 실제 C 호스트가 `-3`을 받는 수용 F, §9-71의 626행 재측정, 슬라이스 닫기. +> 2. **작은 항목**: C# 호스트(Phase 4) · LSP(Phase 3, 큰 일). +> 3. **외부**: `X1`·`X2` — Delphi가 있는 CI 러너. 이 저장소 안에서는 닫히지 않는다. +> +> ⚠ **이 머신의 전체 게이트는 6회 중 2회 실패한다**(§9-63.5) — 실패를 보면 먼저 원인을 읽는다. +> 강한 신호는 CI 두 잡이다. +> +> 📌 **본문은 §9-71이다**(`docs/history/9-71.md`). 그 앞의 2026-09-26 (4) 항목(체크드 산술 닫힘)은 +> 바이트 그대로 옮겼다 — 지금은 `docs/history/start-block-052.md`다. +> diff --git a/docs/history/start-block-index.md b/docs/history/start-block-index.md index 51552b6..0ae61ee 100644 --- a/docs/history/start-block-index.md +++ b/docs/history/start-block-index.md @@ -9,6 +9,7 @@ > | 날짜 | 무엇을 했나 | 본문 | > |---|---|---| +> | 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 | > | 2026-09-26 (2) | **상수 선언 슬라이스가 닫혔다: 조용한 오독이 로드 거부가 됐다** — 다음 선택은 §7부터(§9-69) | §9-68 | diff --git a/docs/slices/README.md b/docs/slices/README.md index de787d5..24e46db 100644 --- a/docs/slices/README.md +++ b/docs/slices/README.md @@ -63,7 +63,7 @@ TDD 구현 → Grok 검증 → PR** 순서를 따른다(`CLAUDE.md` "개발 방 | [나눗셈 가드가 왼쪽 피연산자를 건너뛴다](SPEC-division-guard-operands.md) | ✅ **구현 완료** (2026-09-23) | 제수가 0이면 `/`·`%`의 왼쪽 피연산자(배열 경계 검사)가 실행되지 않던 결함 — 왼쪽을 먼저 묶어 평가한다 | #287 / #291 | | [상수 선언 `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) | `!` 본문이 부른 무한 헬퍼의 산술도 검사하고 `-3`을 전파한다 — DP-P1~P11 사용자 확인, §6 작업 1이 들어갔고 작업 2(C 호스트 수용 · 재측정)가 남았다 | §9-71 / — | +| [헬퍼 체크 전파](SPEC-helper-check-propagation.md) | ✅ **구현 완료** (2026-09-26) | `!` 함수가 부른 무한 함수(export 포함)의 산술도 검사하고 `-3`을 전파한다 — 조용한 오답 60 → 44 | §9-71 / #339 · §9-72 | > **2026-09-25에 행을 한 줄로 접었다.** 접기 전의 서술은 [`../history/slices-index.md`](../history/slices-index.md)에 > 바이트 그대로 있다. **새 행도 한 줄로 쓴다** — 행당 400 B(`every_slice_index_row_is_one_line`)이고, 경위는 그 @@ -126,7 +126,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규칙과 귀속 대조)이 더한 후보: **헬퍼 체크 전파**(확정되어 구현 중이다, 위 색인)와 **넓은 중간값**(둘 다 626행으로 시험 구현했다 — 결정표는 §9-71.6), **i64**(§9-71: 옵트인이라 귀속 대조에서 51행이 빠졌다), **입력 문자열의 인코딩 계약**(닫힌 DP-S2의 재개 — `OPEN_QUESTIONS.md` Q17이 (A)로 열어 두었고 재검토 조건은 거기 있다), 비트 연산자, +§7(§9-69, 12개 도메인 72규칙과 귀속 대조)이 더한 후보: **넓은 중간값**(626행으로 시험 구현했다 — 결정표는 §9-71.6, 위험은 §9-71.4), **`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-helper-check-propagation.md b/docs/slices/SPEC-helper-check-propagation.md index a7188b9..983be3f 100644 --- a/docs/slices/SPEC-helper-check-propagation.md +++ b/docs/slices/SPEC-helper-check-propagation.md @@ -1,8 +1,13 @@ # SPEC — 헬퍼 체크 전파 (`!` 본문이 부른 헬퍼도 검사한다) -- **상태: 확정 · 구현 중.** §4의 DP-P1~P11 전부 **사용자 확인**(2026-09-26, 권고안 그대로). §6의 작업 1이 - 들어갔고 작업 2가 남았다. - - 방향은 먼저 확인받았다: §9-71.6의 권고안 F2 — `!` 함수가 부른 무한 헬퍼 안의 산술도 검사한다. +> **기록 문서다.** 이 SPEC은 닫힌 슬라이스의 설계 기록이다 — 본문은 닫힌 날의 사실이고 다시 고치지 않는다. +> 현재 상태는 [`docs/STATUS.md`](../STATUS.md)가 말한다. + +> **상태: 확정 · 구현 완료** — DP-P1~P11 사용자 확인(권고안 그대로) 2026-09-26 / SPEC #338 · 구현 #339 · 호스트와 +> 재측정은 `HISTORY.md` §9-72. 수용 A~J 전부 닫혔다. **근거 수준:** E2 — 로드한 모듈의 반환값, 실제 C 호스트, 구현으로 +> 다시 잰 626행(시험 구현과 같다, §9-72.3). + +- 방향은 먼저 확인받았다: §9-71.6의 권고안 F2 — `!` 함수가 부른 무한 헬퍼 안의 산술도 검사한다. - 선행: `SPEC-checked-arithmetic.md`(DP-O1 — `!` 본문만 · **DP-O7 — 무한 헬퍼가 탈출구**, 이 슬라이스가 뒤집는다 · DP-O4 — 지문·ABI 불변 · DP-O6 — `result` 뒤) · `SPEC-calls.md`(재귀 금지 — 호출 그래프는 DAG) - 관련 결정: **D17**(음수 status 예약) · #238(바인딩은 모듈이 낼 수 있는 status를 빠짐없이, 그리고 그것만 선언한다) @@ -213,3 +218,5 @@ DP-P1은 방향 확인 때, DP-P2~P11은 이 표 그대로 **사용자 확인** |---|---|---| | 1. `ir.rs` 검사 집합 · codegen 사본(`ml_ck_`, 참조만 방출) · `.h`/`.pas` 술어 · 경고 · 골든 · 컴파일러 테스트 · 오라클 값 · 문서 | A · B · C · D · E · G · H · J | 한 PR | | 2. 예제에 헬퍼를 넣고 실제 C 호스트가 `-3`을 받는다 · §9-71의 626행 재측정 · 슬라이스 닫기 | F · I | 한 PR | + +두 작업 다 들어갔다(#339 · §9-72). diff --git a/examples/basket.mls b/examples/basket.mls index c8a496b..ab6d507 100644 --- a/examples/basket.mls +++ b/examples/basket.mls @@ -11,6 +11,14 @@ error E_LENGTH_MISMATCH = 1 +// One line's total. It has no `!` and needs none: a helper a `!` body calls is checked too +// (SPEC-helper-check-propagation), so a product with no i32 value fails basket_total with +// ML_ST_OVERFLOW from here — the C host's acceptance for the helper path. Internal, so the +// module's fingerprint does not change. +fn line_total(q: i32, p: i32) -> i32 { + return q * p +} + // Line totals with a per-line cap. Two arrays that must agree in length, which the module // checks itself: the host passes two independent pointers and nothing else can. export fn basket_total(qty: [i32], price: [i32], cap: i32) -> i32! { @@ -18,7 +26,7 @@ export fn basket_total(qty: [i32], price: [i32], cap: i32) -> i32! { let mut total = 0 let mut i = 0 while i < len(qty) { - let line = qty[i] * price[i] + let line = line_total(qty[i], price[i]) if line > cap { total = total + cap } diff --git a/hosts/c-host/host.c b/hosts/c-host/host.c index bfab59d..1bcd891 100644 --- a/hosts/c-host/host.c +++ b/hosts/c-host/host.c @@ -1377,7 +1377,10 @@ int main(int argc, char **argv) { check(pick(qty, 3, 2, &last) == 0 && last == 4, "the last element is in range"); /* A line total with no i32 value. Before SPEC-checked-arithmetic this product wrapped - to -2, which is <= cap, so the basket answered -2 with status 0. */ + to -2, which is <= cap, so the basket answered -2 with status 0. The product now + lives in basket.mls's helper `line_total`, which has no `!`: this is also the C host's + evidence that a helper under a `!` caller is checked (SPEC-helper-check-propagation + acceptance F) -- before that slice the helper would have wrapped silently again. */ const int32_t big_qty[1] = {INT32_MAX}; const int32_t two[1] = {2}; int32_t total = 0x5A5A5A5A;