[xzawed]

This PR is a draft SPEC plus an open question. There is no product code. The user confirmed the direction on 2026-09-26: design A+as from §9-69.2, and put the encoding question in OPEN_QUESTIONS.

docs/slices/SPEC-checked-arithmetic.md

Inside fallible bodies (-> T!, -> string!, -> [T]!), these operations fail with a new reserved status ML_ST_OVERFLOW = -3 instead of wrapping or saturating:

• i32 + - * and unary -;
• i32::MIN / -1;
• f64 as i32 when the value is NaN or out of range.

Infallible functions keep today's semantics. That means the wrap decisions (DP-I4, DP-U4, the D2 row) and the saturation rule (§2.3) still hold for them.

Evidence (§0). This comes from the §7 measurements and the local design-A prototype (E2, 626 rows):

• A+as turns 101 of 161 silent wrong answers into a status.
• It falsely refuses 9 rows; only 1 of those is a realistic input.
• It changes the behaviour of 0 existing oracle tests.

DPs. DP-O1 and DP-O2 are confirmed by the user. DP-O3 through DP-O9 await confirmation:

DP	Question	Proposal
DP-O3	Status value	A new -3, not a reused -2
DP-O4	Fingerprint and ABI version	Both unchanged
DP-O5	%	MIN % -1 stays 0, the true remainder
DP-O6	Failure after result	Same as -2: buffer undefined
DP-O7	Escape hatch	No new one; infallible helpers already wrap
DP-O8	Migration	No marker in the fingerprint or manifest
DP-O9	Overflowing literal or constant expressions	Fail at run time, no constant folding

docs/OPEN_QUESTIONS.md Q17

Reopen DP-S2 (input string encoding)? It covers:

• the CP949 measurement;
• the EUC-KR counterexample (SMS/LMS limits are defined in EUC-KR bytes);
• the fact that the recorded reopen condition was case-insensitivity or normalization, not this evidence.

It lists three options. The recommendation is (A) keep it open and document the hazard, awaiting confirmation.

Grok

Following the user's instruction, every call carried one claim and ran in parallel. All of them finished in 2 to 4 turns.

Plan gate, one call per DP:

• %: keep wrapping_rem.
• Fingerprint and ABI version: unchanged.
• Status: Grok first chose -2, citing the cost fix(bindings): -2를 낼 수 있는 모듈이 헤더에서 그것을 말한다 #238 measured. A follow-up verify then CONFIRMED that reusing -2 also requires widening the -2 declaration predicate. That leaves one constant as the only difference, so the SPEC proposes -3 and records the dissent.

Verify, 5 single-claim calls, all CONFIRMED:

• checked_rem on MIN % -1;
• the HOST_ABI status row covering failures after result;
• the 312,949,672 arithmetic;
• which DPs are confirmed versus proposed;
• the Q17 text.

One unasked line found a gap: an overflowing literal-only expression was unspecified. It is now DP-O9.

Evidence: cargo test -p ml_oracle --test doc_claims --locked gives 50 passed.

Related: D17, D18, SPEC-i32 DP-I4, SPEC-unary DP-U4, SPEC-i32-division D2, SPEC-numeric-conversion §2.3, SPEC-array-return DP-R9, SPEC-fixed-decimals DP-M4, SPEC-string-input DP-S2, §9-69.

🤖 Generated with Claude Code

[xzawed]

⚠️ AI 리뷰가 완전 검증되지 않음 — 기본값이 적용됐습니다(비활성/API 키 없음/빈 diff). AI 배점은 측정값이 아니므로 총점을 부분 점수로 보세요.

🔵 SCAManager 분석 결과

총점: 89/100 (등급 B)

점수 상세

항목	점수	만점
커밋 메시지	13	15
코드 품질	25	25
보안	20	20
구현 방향성 (AI)	21	25
테스트	10	15