diff --git a/docs/v4.0.0/DECOMPOSITION.md b/docs/v4.0.0/DECOMPOSITION.md index a08fb356..d331182f 100644 --- a/docs/v4.0.0/DECOMPOSITION.md +++ b/docs/v4.0.0/DECOMPOSITION.md @@ -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 ) diff --git a/v4/include/v4/umul.h b/v4/include/v4/umul.h index 38d8f5f0..382b7640 100644 --- a/v4/include/v4/umul.h +++ b/v4/include/v4/umul.h @@ -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 diff --git a/v4/tests/test_foundation.c b/v4/tests/test_foundation.c index 6e288e09..a72654f9 100644 --- a/v4/tests/test_foundation.c +++ b/v4/tests/test_foundation.c @@ -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");