Repository navigation
docs: SPEC for wide intermediates — exact pure arithmetic, narrowed only at its root - #341
Merged
Merged
Conversation
…nly at its root A draft for the user to confirm, direction included (DP-W1..W11). Measured before writing, on a local branch over today's main (helper check propagation included), four variants on the 625 rows and 48,000 random calls: - FULL (every tree): -3-though-the-answer-fits 59 -> 17, but a fast failure can become a hang and a later -2 can overtake a real overflow (measured); - PURE+CALL (leaves: variables, i32 constants, len, byte_len of a variable, and calls to loop-free infallible functions): 59 -> 20, with no hang and no overtaking — its leaves either cannot fail or fail only with -3, and always terminate; - no variant changes a correct status-0 answer, and every non--3 answer any variant gives equals the exact model. Grok plan: PURE over FULL, no reordering in PURE, narrow before `as f64` (an i64 above 2^53 would round into a new silent wrong answer). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ns the exact-value cases, scope and tasks line up Grok verify: byte_len is a loop bounded only by the host's NUL contract, so deferring the check would run it on inputs where it never ran; dropping it from the leaves changes no answer on the 626 rows (measured). A runtime zero divisor under an exact product is 0 by DP-N4 (measured: today -3, PURE+CALL 0). Acceptance I gains a scope item, §1's boundary now matches §2.1 (pure subtrees are still widened), DP-W11 is in §6, and the variant table has its "other" column. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ore" means before what is evaluated after Grok verify: a call leaf with a string argument runs `==`/`byte_len` in the callee, loops that end only by the host's NUL contract — the same reason byte_len left the leaves. Dropping them changes no answer on the 626 rows (measured). "Before anything outside the tree" was too wide: `xs[5] + a*b` is -2 today and after, because the index is evaluated first; the sentence now says "before anything evaluated after the tree", and acceptance B names the three ordering cases (measured: xs[5]+a*b -2/-2, a*b+xs[5] -3/-3, a*b/b+xs[5] -3/-2). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…n infallible body cannot do Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Owner
Author
🔵 SCAManager 분석 결과총점: 89/100 (등급 B) 점수 상세
|
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.
docs/slices/SPEC-wide-intermediates.md초안. §4의 DP-W1~W11은 방향 포함 전부 확인 대기이고 제품 코드는 없다. 관련: SPEC-checked-arithmetic §2.1·DP-O9(다시 쓴다) · DP-N4 · DP-O5 · D17 · D19.쓰기 전에 잰 것 (E2, 로컬 브랜치
exp/wide2-local— 푸시 안 함)현재 main(헬퍼 체크 전파 포함) 위에 변형 넷을 스위치로 구현해 626행과 무작위 48,000 호출로 쟀다:
-3-3이 아닌 답은 전부 정확한 정수 모델과 같다(무작위 호출).a*b + spin(n))과 앞지름(a*b + xs[5]→-2)이 측정된다. PURE+CALL은 잎이 끝나고-3으로만 실패하므로 둘 다 구조로 없다 — 측정: 즉시-3,-3.len·while없고 문자열 인자 없는 무한 함수 호출.byte_len과 문자열 인자 호출은 NUL까지 도는 반복이라 뺐다 — 빼도 626행 답이 전부 같다(측정).Grok
as f64는 먼저 좁힌다(2^53 위 반올림 = 새 조용한 오답).byte_len을 잎에서 빼고, 문자열 인자 호출을 빼고, "트리보다 뒤에 평가되는 것"으로 정밀화(세 순서 사례를 측정해 수용 B에 적음) → 재검증 CONFIRMED · 내부 일관성 DISCREPANCY → 수용 I의 범위 항목·§1/§2.1 경계·DP-W11의 §6·표의 기타 열 → CONFIRMED.doc_claims50/50.🤖 Generated with Claude Code