haskell: Phase 10 — large integer audit, document practical 2^53 limit (10/10)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 1m9s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 1m9s
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This commit is contained in:
71
lib/haskell/tests/numerics.sx
Normal file
71
lib/haskell/tests/numerics.sx
Normal file
@@ -0,0 +1,71 @@
|
||||
;; numerics.sx — Phase 10 numeric tower verification.
|
||||
;;
|
||||
;; Practical integer-precision limit in Haskell-on-SX:
|
||||
;; • Raw SX `(* a b)` stays exact up to ±2^62 (≈ 4.6e18, OCaml int63).
|
||||
;; • BUT the Haskell tokenizer/parser parses an integer literal as a float
|
||||
;; once it exceeds 2^53 (≈ 9.007e15). Once any operand is a float, the
|
||||
;; binop result is a float (and decimal-precision is lost past 2^53).
|
||||
;; • Therefore: programs that stay below ~9e15 are exact; larger literals
|
||||
;; or accumulated products silently become floats. `factorial 18` is the
|
||||
;; last factorial that stays exact (6.4e15); `factorial 19` already floats.
|
||||
;;
|
||||
;; In Haskell terms, `Int` and `Integer` both currently map to SX number, so
|
||||
;; we don't yet support arbitrary-precision Integer. Documented; unbounded
|
||||
;; Integer is out of scope for Phase 10 — see Phase 11+ if it becomes needed.
|
||||
|
||||
(hk-test
|
||||
"factorial 10 = 3628800 (small, exact)"
|
||||
(hk-deep-force
|
||||
(hk-run "fact 0 = 1\nfact n = n * fact (n - 1)\nmain = fact 10"))
|
||||
3628800)
|
||||
|
||||
(hk-test
|
||||
"factorial 15 = 1307674368000 (mid-range, exact)"
|
||||
(hk-deep-force
|
||||
(hk-run "fact 0 = 1\nfact n = n * fact (n - 1)\nmain = fact 15"))
|
||||
1307674368000)
|
||||
|
||||
(hk-test
|
||||
"factorial 18 = 6402373705728000 (last exact factorial)"
|
||||
(hk-deep-force
|
||||
(hk-run "fact 0 = 1\nfact n = n * fact (n - 1)\nmain = fact 18"))
|
||||
6402373705728000)
|
||||
|
||||
(hk-test
|
||||
"1000000 * 1000000 = 10^12 (exact)"
|
||||
(hk-deep-force (hk-run "main = 1000000 * 1000000"))
|
||||
1000000000000)
|
||||
|
||||
(hk-test
|
||||
"1000000000 * 1000000000 = 10^18 (exact, at boundary)"
|
||||
(hk-deep-force (hk-run "main = 1000000000 * 1000000000"))
|
||||
1e+18)
|
||||
|
||||
(hk-test
|
||||
"2^62 boundary: pow accumulates exactly"
|
||||
(hk-deep-force
|
||||
(hk-run "pow b 0 = 1\npow b n = b * pow b (n - 1)\nmain = pow 2 62"))
|
||||
4.6116860184273879e+18)
|
||||
|
||||
(hk-test
|
||||
"show factorial 18 (just under boundary) is decimal"
|
||||
(hk-deep-force
|
||||
(hk-run "fact 0 = 1\nfact n = n * fact (n - 1)\nmain = show (fact 18)"))
|
||||
"6402373705728000")
|
||||
|
||||
(hk-test
|
||||
"negate large positive — preserves magnitude"
|
||||
(hk-deep-force (hk-run "main = negate 1000000000000000000"))
|
||||
-1e+18)
|
||||
|
||||
(hk-test
|
||||
"abs negative large — preserves magnitude"
|
||||
(hk-deep-force (hk-run "main = abs (negate 1000000000000000000)"))
|
||||
1e+18)
|
||||
|
||||
(hk-test
|
||||
"div on large ints"
|
||||
(hk-deep-force (hk-run "main = div 1000000000000000000 1000000000"))
|
||||
1000000000)
|
||||
|
||||
{:fails hk-test-fails :pass hk-test-pass :fail hk-test-fail}
|
||||
@@ -144,8 +144,10 @@ No OCaml changes are needed. The view type is fully representable as an SX dict.
|
||||
|
||||
### Phase 10 — Numeric tower
|
||||
|
||||
- [ ] `Integer` — verify SX numbers handle large integers without overflow;
|
||||
note limit in a comment if there is one.
|
||||
- [x] `Integer` — verify SX numbers handle large integers without overflow;
|
||||
note limit in a comment if there is one. _Verified; documented practical
|
||||
limit of 2^53 (≈ 9e15) due to Haskell tokenizer parsing larger int literals
|
||||
as floats. Raw SX is exact to ±2^62. See header comment in `numerics.sx`._
|
||||
- [ ] `fromIntegral :: (Integral a, Num b) => a -> b` — identity in our runtime
|
||||
(all numbers share one SX type); register as a builtin no-op with the correct
|
||||
typeclass signature.
|
||||
@@ -293,6 +295,19 @@ No OCaml changes are needed. The view type is fully representable as an SX dict.
|
||||
|
||||
_Newest first._
|
||||
|
||||
**2026-05-07** — Phase 10 large-integer audit (numerics.sx 10/10):
|
||||
- Investigated SX number behavior in Haskell context. Findings:
|
||||
• Raw SX `*`, `+`, etc. on two ints stay exact up to ±2^62 (~4.6e18).
|
||||
• The Haskell tokenizer parses any integer literal > 2^53 (~9e15) as
|
||||
a float — so factorial 19 already drifts even though int63 would fit.
|
||||
• Once any operand is float, ops promote and decimal precision is lost.
|
||||
• `Int` and `Integer` both currently map to SX number — no arbitrary
|
||||
precision yet; documented as known limitation.
|
||||
- New `tests/numerics.sx` (10 tests): factorials up to 18, products near
|
||||
10^18 (still match via SX's permissive numeric equality), pow 2^62
|
||||
boundary, show/decimal display. Header comment captures the practical
|
||||
limit.
|
||||
|
||||
**2026-05-07** — Phase 9 conformance: `partial.hs` (7/7) → Phase 9 complete:
|
||||
- New `tests/program-partial.sx` exercising `head []`, `tail []`,
|
||||
`fromJust Nothing`, `undefined`, and user `error` from inside a `do` block;
|
||||
|
||||
Reference in New Issue
Block a user