Repository navigation
feat(codegen): a helper under a fallible caller is checked too — the call path decides - #339
Merged
Merged
Conversation
…call path decides SPEC-helper-check-propagation §6 task 1 (DP-P1..P11, user-confirmed 2026-09-26). Arithmetic a fallible body executes is checked wherever it is written. ir::checked_helpers is the one set: infallible functions (exported included, DP-P2) reached from a fallible body through infallible calls whose body or callees can overflow. Codegen gives each member a checked copy `ml_ck_<name>` (DP-P7) and a fallible body calls it, propagating -3 where the call stands (DP-P4); a copy calls its callees' copies, so any depth is covered. The plain body is dropped only when nothing but fallible bodies and copies call it (DP-P8), so a module this slice does not reach emits byte-identical Rust — the generated-Rust golden is unchanged. The same set decides ML_ST_OVERFLOW in both bindings (DP-P6): the prototype returned -3 through a helper while neither binding named it. The Cx context carries the set alongside the return shape instead of global state. DP-O7 is reversed (DP-P10): the checked_arithmetic.rs line that pinned it now asserts -3. Fingerprint and ABI version unchanged (DP-P9); header/unit goldens change only in the comment wording. Docs: LANGUAGE.md, HOST_ABI.md, SPEC status, slice index, STATUS; the reserved.rs header no longer says internal function names are emitted raw (#101). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…iding scheme can fail it Planting copy names inside the user namespace (ml_fn_ck_<name>) passed the value test: every function there was called only from a fallible body, so no plain body was emitted to collide with. An infallible caller keeps them. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…where HOST_ABI says it Grok verify: the host-call saturation sentence had no helper-side assertion. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Owner
Author
🔵 SCAManager 분석 결과총점: 89/100 (등급 B) 점수 상세
|
xzawed
added a commit
that referenced
this pull request
Sep 26, 2026
…heck-propagation slice closes (§9-72) (#340) * test(c-host): the helper path reaches a real C host, and the helper-check-propagation slice closes (§9-72) - examples/basket.mls: the line total moves into an internal helper `line_total` with no `!`. The C host's existing overflow check now measures the helper path (acceptance F): the compiler before #339 answers status 0 with -2 for that input, today -3. Internal, so no IFACE_HASH line moves; only basket's generated Rust changes in the golden. - 626 rows re-measured with the implementation: identical to the prototype on every row (acceptance I) — §9-71.3's table holds. - SPEC closed banner and status; index row ✅; candidates: the slice leaves, `wrapping_*` builtins enter (DP-P10). - Session wrap: 9-72.md, HISTORY stub, ▶ entry (6), entry (5) byte-identical to start-block-053.md. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * docs: §9-72.5 records this PR's four Grok rounds Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
SPEC-helper-check-propagation§6 작업 1. DP-P1~P11 사용자 확인(2026-09-26, 권고안 그대로). 관련: DP-O7(뒤집는다) · DP-O4/O6/O8 · D17 · #238.무엇이 바뀌나
!함수가 실행하는 산술은 어디에 쓰여 있든 검사된다 — 자기 본문이든, (여러 단계로) 부른 무한 함수 안이든(export된 함수 포함). 같은 함수를 무한 본문·호스트가 부르면 오늘처럼 wrap·포화한다.ir::checked_helpers, DP-P6):!본문에서 무한 호출로 닿고 자기 본문이나 그 아래가 넘칠 수 있는 무한 함수. codegen과.h·.pas가 이 집합 하나를 읽는다 — 시험 구현은 헬퍼 경로로-3을 내면서 바인딩이 선언하지 않았다.ml_ck_<name>(DP-P7):!본문과 다른 사본이 부르고,-3은 호출 자리에서try처럼 전파된다(DP-P4). 사본이 사본을 불러 깊이에 제한이 없다.!본문과 사본만 부를 때에만 빠진다 — 이 슬라이스가 닿지 않는 모듈의 생성 Rust는 글자 그대로 같다(생성 Rust 골든 불변).Cx { abi, checked }— 모듈 수준 집합을 반환 모양과 함께 넘긴다(전역 상태 없음). 이 기계적 변경이 방출 텍스트를 바꾸지 않음을 Grok이 확인했다.IFACE_HASH0줄).LANGUAGE.md·HOST_ABI.md· SPEC 상태 · 색인 · STATUS ·reserved.rs머리 주석(feat(codegen): one name, one body — split every export into a body and an adapter #101 이후 낡음 — Grok UNASKED).근거 (E2)
-D warnings·doc_claims50/50 ·language_gaps9/9.bool/f64· export 호출 대상 · 단락과 순서 · 이름 무충돌 · 무한 호출자의 wrap·포화), 컴파일러 3(바인딩 술어 · 방출 범위 · 지문),-D warnings빌드 1, 바인딩 행렬 1행.--no-fail-fast): 사본으로 안 부름 · 자기 본문만 보는 술어 · export 제외 · 평범한 본문 모두 유지 · 사용자 이름공간 안의 사본 이름 · 사본이 사슬을 안 탐 · 직접 호출만 도달. 이름 충돌 심기는 처음에 값 테스트를 통과했다 — 평범한 본문이 전부 빠져 충돌할 것이 없었다 → 무한 호출자를 더해 테스트를 강화했고 E0428로 떨어지는 것을 확인했다(624f7b6).Grok (한 번에 주장 하나)
ir.rs집합·술어·걷기 — CONFIRMEDCx리팩터가 호출 자리의abi를 하나도 바꾸지 않음 — CONFIRMEDIFACE_HASH불변 — CONFIRMED남은 것 (작업 2)
예제에 헬퍼를 넣어 실제 C 호스트가
-3을 받는 수용 F · §9-71의 626행 재측정 · 슬라이스 닫기.🤖 Generated with Claude Code