Fix M/MOD: hand-rolled 128/64 bit-serial division (FABRIC-3.md §XII.4)
mixed_math_word_m_slash_mod() had the identical bug class already fixed
in M* (commit 9a09949): it reconstructed the dividend from
`(dhigh << 32) | (dlow & 0xFFFFFFFF)`, the same wrong "32-bit halves of a
64-bit value" assumption. Latent for small inputs (fits in 32 bits, so the
reconstruction coincidentally worked), confirmed genuinely broken for a
true wide double -- feeding M*'s own correct 10^24 output into it gave a
quotient/remainder wrong by many orders of magnitude and the wrong sign.
Unlike M*, this one can't just switch to __int128 -- __int128's own `/`/`%`
need libgcc's __udivti3/__umodti3 for 128-bit division, unavailable in
this freestanding, -nostdlib build (the exact constraint
src/starkernel/arch/amd64/timer.c's own doc comment already flagged:
__int128 multiply/shift-by-constant/compare/subtract all compile clean,
only division doesn't). Fixed instead with a hand-rolled unsigned
128-by-64-bit bit-serial (restoring) long division -- 128 iterations of
shift-by-1/compare/subtract only, all in the safe set. Operates on
magnitudes via unsigned negation from 0 (well-defined even for the
extreme negative edge); signs reapplied afterward matching the same C99
truncating-toward-zero convention the previous, narrower implementation
already used, unchanged.
Verified: rebuilt all three architectures, confirmed clean link with no
__udivti3/__umodti3 undefined-symbol errors. Booted and tested all three,
identical results: 1000000000000 1000000000000 M* SWAP 1000000 M/MOD ->
1000000000000000000 remainder 0 (exact division, the case that was wrong
by orders of magnitude before); three sign-combination cases all correct
(-+, +-, --), confirming sign handling survived the magnitude-only
rewrite. T15 (original small-input case) unaffected. Full 24-case
exerciser reran clean on all three, no regressions.
All bugs found by the std79 exerciser campaign, including this one found
while fixing another, are now closed.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EXieurDfDSsDFdnSyusuWo
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
9a09949c69
commit
70db955ac9
+37
-14
@@ -2141,10 +2141,9 @@ produced one interesting, unconfirmed data point before the first panic: `-123 4
|
||||
against the other two architectures once the campaign completes; not yet root-caused or reported
|
||||
as a bug on its own.
|
||||
|
||||
### XII.4 — Campaign completed: full 27-leg run (9 identities × 3 architectures), two real
|
||||
FORTH-79 engine bugs found — BOTH root-caused and FIXED 2026-09-11 (bug 1 `M*`; bug 2 `D+`/`D-`/
|
||||
`DNEGATE`/`d_compare`); a third, `M/MOD`, found while fixing bug 1, reported not fixed
|
||||
(2026-09-10 campaign, after §XIII's WIREBIND fix)
|
||||
### XII.4 — Campaign completed: full 27-leg run (9 identities × 3 architectures) — ALL bugs
|
||||
found (`M*`, `D+`/`D-`/`DNEGATE`/`d_compare`, and `M/MOD` found along the way) root-caused and
|
||||
FIXED, 2026-09-11 (2026-09-10 campaign, after §XIII's WIREBIND fix)
|
||||
|
||||
All 27 legs run: `zuse` (auto-attached, exercised directly on Hera's own console) plus `rajames`
|
||||
(the `bob` thumbdrive's actual registered identity -- see the naming-mismatch note below) and
|
||||
@@ -2203,16 +2202,40 @@ project's standing rule (report, don't fix without being asked):**
|
||||
proof the multiply itself is now genuinely 128-bit, not just sign-extension-correct for small
|
||||
values). Full 24-case exerciser reran clean on all three, no regressions.
|
||||
|
||||
**Found while verifying, NOT fixed (report only, out of scope of what was requested):**
|
||||
`mixed_math_word_m_slash_mod()` (`M/MOD`, the very next function in the same file) has the
|
||||
*identical* bug class -- it reconstructs the dividend from `(dhigh << 32) | (dlow &
|
||||
0xFFFFFFFF)`, the same wrong "32-bit halves of a 64-bit value" assumption `M*` had. Latent for
|
||||
small inputs (`T15: 100000 S>D SWAP 7 M/MOD . .` -> `14285 5`, correct, because `100000` fits
|
||||
entirely within 32 bits so the reconstruction coincidentally works), but confirmed genuinely
|
||||
broken for a true wide double: feeding the now-fixed `M*`'s own correct large-magnitude output
|
||||
into `M/MOD` (`1000000000000 1000000000000 M* 1000000 M/MOD . .`, expected quotient
|
||||
`10^18`) produces `-6845471433603` remainder, `-99710` quotient -- wrong by many orders of
|
||||
magnitude and the wrong sign. Not touched here; flag for a future fix request.
|
||||
**`M/MOD` found broken by the same bug class, then FIXED 2026-09-11** (on explicit follow-up
|
||||
request "fix it"): `mixed_math_word_m_slash_mod()` (the very next function in the same file)
|
||||
reconstructed the dividend from `(dhigh << 32) | (dlow & 0xFFFFFFFF)`, the same wrong "32-bit
|
||||
halves of a 64-bit value" assumption `M*` had. Latent for small inputs (`T15: 100000 S>D SWAP
|
||||
7 M/MOD . .` -> `14285 5`, correct, because `100000` fits entirely within 32 bits so the
|
||||
reconstruction coincidentally worked), confirmed genuinely broken for a true wide double
|
||||
(feeding the fixed `M*`'s own `10^24` output into it gave a quotient wrong by many orders of
|
||||
magnitude and the wrong sign).
|
||||
|
||||
Fixing this one is harder than `M*`: `__int128`'s own `/`/`%` operators need libgcc's
|
||||
`__udivti3`/`__umodti3` for 128÷64 division, unavailable in this freestanding, `-nostdlib`
|
||||
build (confirmed at link time -- exactly the constraint `timer.c`'s own doc comment already
|
||||
flagged: `__int128` multiply/shift-by-constant/compare/subtract all compile clean, only
|
||||
division doesn't). Fixed instead with a hand-rolled unsigned 128-bit-by-64-bit bit-serial
|
||||
(restoring) long division -- 128 iterations of shift-by-1/compare/subtract only, all in the
|
||||
safe set. Operates on magnitudes (via unsigned negation from `0`, well-defined even for the
|
||||
extreme negative edge, unlike signed negation); signs reapplied afterward matching C99
|
||||
truncating-toward-zero division (quotient sign = XOR of operand signs, remainder sign = the
|
||||
dividend's own sign) -- the exact convention the previous, narrower implementation already
|
||||
used via plain C `/`/`%`, unchanged here.
|
||||
|
||||
**Verified:** rebuilt all three architectures -- confirmed clean link with no
|
||||
`__udivti3`/`__umodti3` undefined-symbol errors (would have failed exactly the way `timer.c`'s
|
||||
own history warned about, had `__int128` division been used instead). Booted and tested all
|
||||
three, identical results everywhere: `1000000000000 1000000000000 M* SWAP 1000000 M/MOD` ->
|
||||
quotient `1000000000000000000` (10^18), remainder `0` (exact division, the case that was
|
||||
wrong by many orders of magnitude before); three sign-combination cases
|
||||
(`-100000 S>D SWAP 7 M/MOD` -> `-14285 -5`; `100000 S>D SWAP -7 M/MOD` -> `-14285 5`;
|
||||
`-100000 S>D SWAP -7 M/MOD` -> `14285 -5`) all correct, confirming the sign-handling survived
|
||||
the magnitude-only rewrite. `T15` (the original small-input case) unaffected. Full 24-case
|
||||
exerciser reran clean on all three, no regressions.
|
||||
|
||||
**All bugs found by this campaign, including the one found while fixing another, are now
|
||||
closed.**
|
||||
|
||||
2. **`D+` on two negative doubles → `D.` reports `DOUBLE-OVERFLOW`, aarch64 only — root-caused
|
||||
2026-09-11, FIXED 2026-09-11 (`D+`/`D-`/`DNEGATE`).**
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
# Capsule Block Manifest — Auto-generated
|
||||
<!-- Generated by mkcapsule --manifest 2026-09-11T12:21:21Z -->
|
||||
<!-- Generated by mkcapsule --manifest 2026-09-11T14:26:40Z -->
|
||||
<!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. -->
|
||||
<!-- Hand-written justifications and immutability notes live -->
|
||||
<!-- in MANIFEST.md alongside this auto-generated index. -->
|
||||
|
||||
Binary file not shown.
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@@ -172,11 +172,35 @@ void mixed_math_word_m_star(VM *vm) {
|
||||
* @brief M/MOD ( d n -- rem quot )
|
||||
*
|
||||
* Divides the double-cell dividend @c d by the single-cell divisor @c n,
|
||||
* pushing the remainder deeper and the quotient on TOS. On 64-bit builds,
|
||||
* the double is reconstructed as a @c long long by shifting the high 32 bits
|
||||
* left; the UBSan-safe path uses an unsigned shift before casting to signed to
|
||||
* avoid undefined behaviour on negative values. On 32-bit builds, only handles
|
||||
* the case where the high cell is zero; sets @c vm->error = 1 otherwise.
|
||||
* pushing the remainder deeper and the quotient on TOS. A "double" here is
|
||||
* two full @c cell_t-width cells (128 bits total on a 64-bit build) -- same
|
||||
* convention as M* (see that word's own doc comment for the full story).
|
||||
* The previous implementation reconstructed the dividend as a plain 64-bit
|
||||
* @c long long from `(dhigh << 32) | (dlow & 0xFFFFFFFF)`, the same wrong
|
||||
* "32-bit halves of a 64-bit value" assumption M* had -- silently discarding
|
||||
* the upper 32 bits of @c dlow and losing @c dhigh entirely once it wasn't
|
||||
* just 0 or -1. Latent for any dividend whose true magnitude fit in 32 bits
|
||||
* (never exercised otherwise until M*'s own fix started producing genuine
|
||||
* wide doubles to feed it -- FABRIC-3.md §XII.4).
|
||||
*
|
||||
* Fixed via a hand-rolled unsigned 128-bit-by-64-bit bit-serial (restoring)
|
||||
* long division, not @c __int128's own `/`/`%` operators: those need
|
||||
* libgcc's `__udivti3`/`__umodti3`, unavailable in this freestanding,
|
||||
* `-nostdlib` build (confirmed in `src/starkernel/arch/amd64/timer.c`'s own
|
||||
* doc comment -- `__int128` multiply/shift-by-constant/compare/subtract all
|
||||
* compile cleanly with zero undefined symbols on all three toolchains, only
|
||||
* division doesn't). Shift-by-1, compare, and subtract on `unsigned
|
||||
* __int128` are all in that safe set, so the classic 128-iteration
|
||||
* shift-and-subtract algorithm works without any libgcc dependency.
|
||||
* Operates on magnitudes (converted via unsigned negation from 0, which is
|
||||
* well-defined even for the extreme negative edge, unlike signed negation);
|
||||
* signs are reapplied afterward matching C99 truncating-toward-zero
|
||||
* division (quotient sign = XOR of operand signs, remainder sign = the
|
||||
* dividend's own sign) -- the same convention the previous, narrower
|
||||
* implementation already used via plain C `/`/`%`, unchanged here.
|
||||
*
|
||||
* On 32-bit builds, only handles the case where the high cell is zero; sets
|
||||
* @c vm->error = 1 otherwise.
|
||||
*
|
||||
* Stack effect: ( d_high d_low n -- remainder quotient ) TOS = quotient
|
||||
*
|
||||
@@ -198,12 +222,28 @@ void mixed_math_word_m_slash_mod(VM *vm) {
|
||||
}
|
||||
|
||||
if (sizeof(cell_t) == 8) {
|
||||
/* UBSan fix: Perform shift on unsigned, then cast to signed (2025-12-09)
|
||||
* Left-shifting negative signed values is undefined behavior */
|
||||
long long dividend = (long long)(((unsigned long long) dhigh << 32) |
|
||||
((unsigned long long) dlow & 0xFFFFFFFFLL));
|
||||
cell_t quotient = (cell_t)(dividend / n);
|
||||
cell_t remainder = (cell_t)(dividend % n);
|
||||
int dividend_neg = (dhigh < 0);
|
||||
int divisor_neg = (n < 0);
|
||||
|
||||
unsigned __int128 udividend = ((unsigned __int128) (ucell_t) dhigh << 64) |
|
||||
(unsigned __int128) (ucell_t) dlow;
|
||||
if (dividend_neg) udividend = (unsigned __int128) 0 - udividend;
|
||||
|
||||
ucell_t udivisor = (ucell_t) n;
|
||||
if (divisor_neg) udivisor = (ucell_t) 0 - udivisor;
|
||||
|
||||
unsigned __int128 uquot = 0, urem = 0;
|
||||
for (int i = 127; i >= 0; i--) {
|
||||
urem = (urem << 1) | ((udividend >> i) & 1);
|
||||
if (urem >= (unsigned __int128) udivisor) {
|
||||
urem -= (unsigned __int128) udivisor;
|
||||
uquot |= ((unsigned __int128) 1 << i);
|
||||
}
|
||||
}
|
||||
|
||||
cell_t quotient = (dividend_neg ^ divisor_neg) ? -(cell_t) uquot : (cell_t) uquot;
|
||||
cell_t remainder = dividend_neg ? -(cell_t) urem : (cell_t) urem;
|
||||
|
||||
vm_push(vm, remainder); // remainder first (deeper)
|
||||
vm_push(vm, quotient); // quotient last (TOS)
|
||||
} else {
|
||||
|
||||
Reference in New Issue
Block a user