feat(v4.0.0): full-range UM* under plain F18 +* (D-3)
UM* as first written in DECOMPOSITION.md section 4 was exact only while u1 <= 2^(n-2): plain +* loses the carry out of T and its shift keeps T's sign bit, so the loop is exact only while S and T stay in [-2^(n-2), 2^(n-2)). The rewrite multiplies by s = u1 2/, which always lies in that range, starting T at t0 = u2 2/ when u1 is odd, so the loop yields hi:lo = t0 + s*u2 exactly. Then u1*u2 = 2*(hi:lo) + c_lo + c_hi*2^n c_lo = u1 & u2 & 1 c_hi = (u1<0 ? u2 : 0) + (u1 odd and u2<0 ? 1 : 0) restores the halved-away bits and the unsigned reading of both top bits. test_foundation.c runs the new definition against v4_umul over every pair of the edge vectors plus 20000 pseudo-random pairs, at 32- and 64-bit cells, optimised and under ASan+UBSan. The two pinned failing cases are now ordinary exactness checks. Two hand mutations of the correction step each fail more than 10000 checks at both widths. DECOMPOSITION.md: section 4 UM* replaced, D-3 ruling text updated. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
rajames
co-authored by
Claude Opus 5.5
Claude Opus 5.5
parent
067f317c47
commit
9a391eb0ad
@@ -164,7 +164,7 @@ definition below depends on one, it says so.
|
||||
| --- | --- | --- |
|
||||
| **D-1** | Word addressing (pure Moore) or byte addressing. | **Word addressing.** `C@`/`C!` are CAP; `CELLS` is a no-op. |
|
||||
| **D-2** | Stack depth, and whether the stacks are visible. | **F18 circular stacks, hidden.** Data stack 10 deep (`T`, `S` + 8 circular), return stack 9 deep (`R` + 8 circular), exactly as the F18. No stack pointer is visible to code, so `DEPTH`, `PICK`, `ROLL`, `.S`, `SP@` and `SP!` are **retired everywhere**, host node included. |
|
||||
| **D-3** | Exact `+*` semantics at 32 bits: whether the add carries out of `T` into the shift. | **Plain F18 semantics.** The carry out of `T` is not kept. `UM*` in §4 must be revised accordingly (see the note there). |
|
||||
| **D-3** | Exact `+*` semantics at 32 bits: whether the add carries out of `T` into the shift. | **Plain F18 semantics.** The carry out of `T` is not kept. `UM*` in §4 is written for this and is exact over the full range (revised and proven on the golden model, 2026-10-02). |
|
||||
| **D-4** | Node memory map, including port and register addresses. | **Deferred** to step 2. Symbolic names only for now (§6, §7). |
|
||||
| **D-5** | Host node cell width. | **Match the host CPU:** 32 on a Zynq-7000 (Cortex-A9), 64 on an aarch64 host. The compiler capsule is written width-independent. |
|
||||
| **D-6** | Which heat structures exist in hardware: per-opcode counters only, or also per-call-target and word-to-word transition counters. | **Deferred** to step 2. The golden model implements per-opcode and per-call-target heat in the meantime. |
|
||||
@@ -201,11 +201,24 @@ dependency order.
|
||||
: U< ( u1 u2 -- flag ) 2DUP xor 0< IF NIP 0< ELSE - 0< THEN ;
|
||||
|
||||
\ ---- multiply (D-3) -----------------------------------------------------
|
||||
\ NEEDS REVISION: written for the carry-keeping +* that D-3 rejected. With
|
||||
\ plain F18 +* the carry out of T is lost, so this is only correct when the
|
||||
\ partial sums never overflow T (operands below 2^31). A full-range UM*
|
||||
\ needs a correction step; to be rewritten and proven on the golden model.
|
||||
: UM* ( u1 u2 -- ulo uhi ) a! 0 31 FOR +* UNEXT push drop a pop ;
|
||||
\ Plain F18 +* loses the carry out of T, and its shift keeps T's sign bit, so
|
||||
\ the loop is exact only while the multiplicand in S and the running T both
|
||||
\ lie in [-2^(n-2), 2^(n-2)). UM* therefore multiplies by s = u1 2/, which
|
||||
\ always does, starting T at t0 = u2 2/ when u1 is odd, and gets
|
||||
\ hi:lo = t0 + s*u2. Then u1*u2 = 2*(hi:lo) + c_lo + c_hi*2^n, where
|
||||
\ c_lo = u1 & u2 & 1
|
||||
\ c_hi = (u1<0 ? u2 : 0) + (u1 odd and u2<0 ? 1 : 0)
|
||||
\ restore the bits the two halvings dropped and the unsigned reading of
|
||||
\ both top bits. Exact over the full range; proven on the golden model.
|
||||
: UM* ( u1 u2 -- ulo uhi )
|
||||
over 0< over and push \ R: u1<0 ? u2 : 0
|
||||
over over 0< and 1 and pop + push \ R: c_hi
|
||||
over over and 1 and push \ R: c_hi c_lo
|
||||
over 1 and NEGATE over 2/ and push \ R: c_hi c_lo t0
|
||||
a! 2/ pop \ s t0 A: u2
|
||||
31 FOR +* UNEXT \ s hi A: lo
|
||||
NIP a 2* pop + SWAP \ lo' hi
|
||||
2* a 0< NEGATE + pop + ; \ lo' hi'
|
||||
|
||||
\ ---- divide: 32-step restoring division, divisor held in A --------------
|
||||
: UM/MOD ( ulo uhi ud -- urem uquot )
|
||||
|
||||
@@ -1,6 +1,7 @@
|
||||
/* umul.h -- unsigned multiply fixing UM* under D-3 constraints.
|
||||
*
|
||||
* DECOMPOSITION.md line 205-207: "NEEDS REVISION: written for the carry-keeping
|
||||
* DECOMPOSITION.md section 4 first said of UM* (since rewritten to be exact over
|
||||
* the full range; see test_foundation.c): "NEEDS REVISION: written for the carry-keeping
|
||||
* +* that D-3 rejected. With plain F18 +* the carry out of T is lost, so this
|
||||
* is only correct when the partial sums never overflow T (operands below 2^31).
|
||||
* A full-range UM* needs a correction step; to be rewritten and proven on the
|
||||
|
||||
+53
-20
@@ -6,6 +6,10 @@
|
||||
* section 5, which U< needs) and runs them on the golden model against the C
|
||||
* operation each one stands for.
|
||||
*
|
||||
* UM* is the full-range version that section 4 gives under D-3, and is checked
|
||||
* against the reference v4_umul over every pair of the edge vectors and 20000
|
||||
* pseudo-random pairs at each cell width.
|
||||
*
|
||||
* Every call is made with a canary under the arguments, and the canary must
|
||||
* still be directly under the results afterwards: a definition that leaves
|
||||
* the right answer but an unbalanced stack is wrong.
|
||||
@@ -92,14 +96,32 @@ static void build(void)
|
||||
v4_asm_resolve(&as, ref, v4_asm_label(&as));
|
||||
O(DROP); CALL(w_minus); CALL(w_zless); O(SEMI);
|
||||
|
||||
/* : UM* a! 0 31 FOR +* UNEXT push drop a pop ;
|
||||
* 31 is the cell width less one; written for a 32-bit cell in section 4.
|
||||
* The loop body is the start of its own word so that unext restarts it. */
|
||||
/* : UM* ( u1 u2 -- ulo uhi ) section 4, D-3
|
||||
* over 0< over and push R: m1 ? u2 : 0
|
||||
* over over 0< and 1 and pop + push R: c_hi
|
||||
* over over and 1 and push R: c_hi c_lo
|
||||
* over 1 and NEGATE over 2/ and push R: c_hi c_lo t0
|
||||
* a! 2/ pop s t0 A: u2
|
||||
* 31 FOR +* UNEXT s hi A: lo
|
||||
* NIP a 2* pop + SWAP lo' hi
|
||||
* 2* a 0< NEGATE + pop + ; lo' hi'
|
||||
* NEGATE is placed in line. 31 is the cell width less one; the loop body
|
||||
* is the start of its own word so that unext restarts it. */
|
||||
w_umstar = v4_asm_label(&as);
|
||||
O(BANG_A); LIT(0); LIT(V4_CELL_BITS - 1); O(PUSH);
|
||||
O(OVER); CALL(w_zless); O(OVER); O(AND); O(PUSH);
|
||||
O(OVER); O(OVER); CALL(w_zless); O(AND); LIT(1); O(AND);
|
||||
O(RPOP); O(ADD); O(PUSH);
|
||||
O(OVER); O(OVER); O(AND); LIT(1); O(AND); O(PUSH);
|
||||
O(OVER); LIT(1); O(AND); O(INV); LIT(1); O(ADD);
|
||||
O(OVER); O(TWO_SLASH); O(AND); O(PUSH);
|
||||
O(BANG_A); O(TWO_SLASH); O(RPOP);
|
||||
LIT(V4_CELL_BITS - 1); O(PUSH);
|
||||
(void)v4_asm_label(&as);
|
||||
O(MUL_STEP); O(UNEXT); O(PUSH); O(DROP); O(PUSH_A); O(RPOP);
|
||||
O(SEMI);
|
||||
O(MUL_STEP); O(UNEXT);
|
||||
CALL(w_nip);
|
||||
O(PUSH_A); O(TWO_STAR); O(RPOP); O(ADD); CALL(w_swap);
|
||||
O(TWO_STAR); O(PUSH_A); CALL(w_zless); O(INV); LIT(1); O(ADD); O(ADD);
|
||||
O(RPOP); O(ADD); O(SEMI);
|
||||
|
||||
CHECK(v4_asm_ok(&as), "foundation words assemble");
|
||||
}
|
||||
@@ -184,23 +206,34 @@ int main(void)
|
||||
CHECK(call(w_rot, 3, a, b, c) && left3(b, c, a), "ROT [%u,%u,%u]", i, j, k);
|
||||
}
|
||||
|
||||
/* UM* as written is exact whenever the multiplicand (u1, which
|
||||
* stays in S) is at most 2^(n-2): T is then always below S, so
|
||||
* T+S stays below 2^(n-1) and neither the lost carry nor +*'s
|
||||
* sign-keeping shift can touch the result. u2 is unrestricted. */
|
||||
if (ua <= (V4_MSB >> 1))
|
||||
CHECK(umstar_exact(ua, ub), "UM* [%u,%u]", i, j);
|
||||
CHECK(umstar_exact(ua, ub), "UM* [%u,%u]", i, j);
|
||||
}
|
||||
}
|
||||
|
||||
/* KNOWN LIMITS of UM* as written, recorded so they cannot be forgotten.
|
||||
* Section 4 marks UM* "NEEDS REVISION" and gives the limit as "operands
|
||||
* below 2^31". The measured limit is tighter and is on u1 only. These
|
||||
* two checks assert that the definition is still wrong where it is known
|
||||
* to be wrong; when UM* is rewritten they must be turned into ordinary
|
||||
* exactness checks. */
|
||||
CHECK(!umstar_exact(MAXU, MAXU), "UM* limit: carry out of T is lost (D-3)");
|
||||
CHECK(!umstar_exact(V4_MSB - 1u, 3u), "UM* limit: u1 below 2^(n-1) still fails");
|
||||
/* UM* over the full range: products of pseudo-random operands, and of
|
||||
* operands chosen near the edges D-3 makes dangerous (top bit set, all
|
||||
* ones, just under a power of two). */
|
||||
{
|
||||
v4_ucell x = (v4_ucell)0x9E3779B9u;
|
||||
for (unsigned i = 0; i < 20000; i++) {
|
||||
v4_ucell u1, u2;
|
||||
x ^= x << 13; x ^= x >> 7; x ^= x << 17;
|
||||
u1 = x;
|
||||
x ^= x << 13; x ^= x >> 7; x ^= x << 17;
|
||||
u2 = x;
|
||||
switch (i & 3u) {
|
||||
case 1: u1 |= V4_MSB; break;
|
||||
case 2: u1 |= V4_MSB; u2 |= V4_MSB; break;
|
||||
case 3: u1 = MAXU - (u1 & 7u); break;
|
||||
default: break;
|
||||
}
|
||||
CHECK(umstar_exact(u1, u2), "UM* random [%u]", i);
|
||||
}
|
||||
}
|
||||
|
||||
/* The two cases that broke UM* as first written in section 4. */
|
||||
CHECK(umstar_exact(MAXU, MAXU), "UM* MAX*MAX: carry out of T (D-3)");
|
||||
CHECK(umstar_exact(V4_MSB - 1u, 3u), "UM* (2^(n-1)-1)*3");
|
||||
|
||||
CHECK(v4_node_guards_intact(&n), "guards intact");
|
||||
|
||||
|
||||
Reference in New Issue
Block a user