28 Commits
Author SHA1 Message Date
rajamesandClaude Opus 5.5 13ec4b1b6c test(v4.0.0): execute the in-line constants Q.1, Q.0 and Q.SCALE
DECOMPOSITION.md 5.26 gives them fate IN: the compiler places two
literals, low cell first. Q.1 and Q.SCALE are `65536 0`, Q.0 is `0 0`;
v3's are 65536, 0 and 65536.

Each expansion is assembled and run, and checked against v3's value;
then in use: Q.1 Q.TO-INT is 1, 1 Q.FROM-INT is Q.1, and q Q.1 Q.* and
q Q.0 Q.+ return q for 2000 pseudo-random q plus 0, Q max and Q min.
At 32- and 64-bit cells, optimised and ASan+UBSan (`make test`,
`make sanitize`). A wrong value in any of the three fails.

Test results on the amd64 host only. This is a development check, not
acceptance (JUSTIFICATION.md section 16).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-03 11:03:57 -04:00
rajamesandClaude Opus 5.5 8235078b3b feat(v4.0.0): Q.COS, bit for bit with v3
Q.COS is v3's q48_cos_approx: on |(Q.REDUCE) x|, the even Taylor series
to n = 10. It sets term and sum to 1.0, n to 2 and the sign cell to 0,
then jumps into Q.SIN's loop, so it adds no call level.

Checked bit for bit against v3's q48_cos_approx (ported into the test)
on the same 33 edge angles and 3000 pseudo-random angles as Q.SIN, at
32- and 64-bit cells, optimised and ASan+UBSan (`make test`,
`make sanitize`). Mutating the start index, the start sum, the
alternation or the sign cell each fails 2500+ cosine checks and no sine
checks.

Headroom (data under arg / return): Q.COS 3/2.

Test results on the amd64 host only. This is a development check, not
acceptance (JUSTIFICATION.md section 16).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-03 10:53:52 -04:00
rajamesandClaude Opus 5.5 1ce705783c feat(v4.0.0): Q.SIN and (Q.REDUCE), bit for bit with v3
(Q.REDUCE) is v3's q48_reduce_angle: the angle as one cell in [-pi, pi].
x / 2pi does not fit a cell, but only the remainder is needed, and
|x| mod 2pi is two UM/MOD steps (high cell first, its remainder leading
the low cell); then the sign of x and one step of 2pi back into range.

Q.SIN is v3's q48_sin_approx on the reduced angle: the odd Taylor series
to n = 11, each term the last times x^2 over n(n-1), stopping below 10
ulp. After the reduction every value fits one cell, so the 6-cell
variable (QT) holds single cells. The loop is laid out for Q.COS to jump
into, so the pair share it without an extra call level.

Checked bit for bit against v3 (both functions ported into the test) on
33 edge angles -- around +-pi/2, +-pi, +-2pi, the 32-bit seam and both
64-bit extremes -- and 3000 pseudo-random angles of every size and sign,
at 32- and 64-bit cells, optimised and ASan+UBSan (`make test`,
`make sanitize`). Mutating either range boundary, the series length or
the sign alternation fails. Moving the 10-ulp stop to 11 fails nothing,
and a scan of all 205888 reduced angles in C shows why: no input's
result depends on it, for sine or cosine.

Headroom (data under arg / return): (Q.REDUCE) 5/5, Q.SIN 3/2.

Test results on the amd64 host only. This is a development check, not
acceptance (JUSTIFICATION.md section 16).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-03 10:44:42 -04:00
rajamesandClaude Opus 5.5 e117333a87 feat(v4.0.0): Q.LOG, flattened, bit for bit with v3
Q.LOG is v3's q48_log_approx: x = 2^k * m with 1.0 <= m < 2.0, ln m by
up to 6 Newton rounds on e^y = m, result y + k * ln 2. As ruled, e^y is
Q.EXP's Taylor loop written in line rather than a call to Q.EXP, so
Q.LOG calls only Q.*, Q./ and UM*. After the reduction m, y, the Taylor
term and its sum each fit one cell, so the 7-cell variable (QL) holds
single cells. x <= 0 returns 0 and sets NODE-ERROR (D-12).

Checked bit for bit against v3's q48_log_approx (ported into the test)
on 22 positive edge values, 2000 pseudo-random x of every magnitude and
a sweep of every 17th reduced m, at 32- and 64-bit cells, optimised and
ASan+UBSan (`make test`, `make sanitize`). Mutating the round count, the
100-ulp stop, ln 2 or the Taylor length all fail.

v3's clamp y = max(y - corr, 0) is kept but cannot fire: a scan of all
65536 values of m in C never reaches it, and never needs more than 4
rounds. So no test covers it.

The test harness's per-call step limit is raised from 100000 to 4000000
instruction words: a 64-bit Q./ takes about 6500, and a mutant forcing
extra Newton rounds ran past the old limit and looked like a width
difference.

Headroom (data under arg / return): Q.LOG 3/2.

Test results on the amd64 host only. This is a development check, not
acceptance (JUSTIFICATION.md section 16).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-03 10:29:59 -04:00
rajamesandClaude Opus 5.5 a2a4a85d38 docs(v4.0.0): record the three products and v4's acceptance criteria
Both ruled by Captain Bob, 2026-10-03.

Products (README.md, JUSTIFICATION.md section 15): Hosted StarForth F18
(native Linux, amd64/arm64/riscv64, on hardware); FPGA StarForth F18 (a
32-bit build loaded into the FPGA, the gateway and foundation); and
StarshipOS (bare metal, LithosAnanke on the v4 F18 engine). FORTH-79
recomposed on the F18 engine is stored as a capsule, as are the
StarshipOS portions; the tree will be reorganised around this.

Acceptance (JUSTIFICATION.md section 16, v4/README.md): v4 is equivalent
to v3 at any point in time -- same vocabularies, same behaviour, on the
F18-derived engine -- and every ISA, hosted and bare metal, must still
reach its ok prompt. `make -C v4 test` is a development check, not
acceptance. v4 had no acceptance criteria before this.

Documentation only; no code changed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-03 10:13:58 -04:00
rajamesandClaude Opus 5.5 f4bfe7de02 logs: three-architecture kernel acceptance baseline at a2d21d5c
Baseline run for StarForth-v4.0.0 as it stands, before any further work.
`make -f kernel/Makefile ARCH=<arch> clean qemu` for amd64, aarch64 and
riscv64, one at a time, disk/artemis.img and
disk/thumbdrives/zuse-thumb-ident.img restored to their committed state
before each.

All three reach `[zuse@Hera] ok>`, with zero UNKNOWN WORD, PARITY:OK,
1050 POST tests run and ALL IMPLEMENTED TESTS PASSED,
stadium_conserved(Artemis)=true.

dict_hash is identical across the three:
  Hera (PARITY:M7.1a, word_count=530)  0x08873e0f44b7cb2a
  dict_hash                            0xe11082140cf86b05
  dict_hash                            0xb1256603f848e2b9
  dict_hash                            0xc791409ac1715690

QEMU was asked to quit over QMP once the prompt had appeared and the
serial log had been quiet for 10 seconds.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-03 10:11:25 -04:00
rajamesandClaude Opus 5.5 a2d21d5cda feat(v4.0.0): Q.SQRT bit for bit with v3; D-12 domain errors
D-12 (ruled 2026-10-02): Q.SQRT of a negative value and Q.LOG of zero or
a negative value return 0 and set NODE-ERROR, as Q./ does on division by
zero.

Q.SQRT is v3's q48_sqrt_approx: Newton from x0 = q/2 + 0.25, up to 8
rounds of x' = (x + q/x) / 2, returning x once |x' - x| < 10 ulp;
sqrt(0) = 0 and sqrt(1.0) = 1.0. q, x and the rounds left live in a
5-cell variable (QR). Checked bit for bit against v3's q48_sqrt_approx
(ported into the test) on 19 edge values and 3000 pseudo-random q below
2^48, at both cell widths, optimised and ASan+UBSan. Above 2^48 v3's
q48_div saturates and v4 divides correctly, so there is no parity there.

Bug found and fixed on the way: the "< 10 ulp" test subtracted 10 from
the step's low cell as a signed number, so at 32-bit cells a step of
2^31 or more read as small and the iteration stopped early. It now
tests the low cell's top bit first, as Q.EXP does. The first test run
missed it because `make build/32-test_foundation.c` rebuilds nothing
(the Makefile's rules use absolute paths); the mutation runs, compiled
from source, exposed it. Only `make test` is used from here.

Headroom (data under arg / return): Q.SQRT 3/2.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-03 09:07:30 -04:00
rajamesandClaude Opus 5.5 29cf2688d2 feat(v4.0.0): Q.EXP bit for bit with v3; lighter D2*C and (UQ/)
Q.EXP is v3's q48_exp_approx: the Taylor series to 10 terms on |q|,
stopping below 50 ulp, 1.0 Q./ e^|q| for q < 0, e^0 = 1.0, and for
|q| >= 16.0 either 0 or Q max (v3 returned all ones, which is -ulp read
signed under D-8). x, term, sum, sign and term index live in a new
8-cell variable (QE). Checked bit for bit against v3's q48_exp_approx
(ported into the test) on 23 edge values and 3000 pseudo-random q in
(-16.0, 16.0), at both cell widths, optimised and ASan+UBSan; dropping a
term, moving the 50-ulp stop or skipping the reciprocal all fail.

Q.EXP calls Q./, which calls (UQ/), which calls D2*C, and at first it
left its caller no return entries. Lightened along the chain:
- D2*C takes cin in A and builds 2hi+m with `over + +`: no ROT, no SWAP.
- (UQ/) parks the quotient bit instead of using ROT, stores q without
  SWAP, and does its full trial subtraction (with borrow) in line
  instead of calling DNEGATE D+.
- Q.EXP keeps its term index in (QE) instead of a FOR count.

Headroom (data under args / return): (UQ/) 4/3 -> 4/4, Q./ 3/2 -> 3/3,
Q.EXP 3/2.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-03 00:26:36 -04:00
rajamesandClaude Opus 5.5 9e03bdab19 feat(v4.0.0): Q./ under D-11, with (UQ/), D2*C and the (Q/) variable
D-11 (ruled 2026-10-02): Q./ rounds toward zero, saturates to Q max /
Q min on overflow, and on division by zero returns Q max / Q min by the
dividend's sign (0 for 0/0) and sets the new NODE-ERROR register (7),
which VM-ERROR? reads.

- (UQ/): unsigned floor(a * 2^16 / b) for b != 0 and no overflow.
  Restoring division, 2N+16 steps, on one shifting register (quotient
  above remainder). Quotient register and divisor live in a 5-cell
  variable (Q/), like BASE and the hold buffer, so the stacks carry only
  the remainder, the quotient bit and the loop count. A first version
  kept the divisor on the return stack and overflowed it when called
  from Q./ (it never returned).
- D2*C: double shift left with carry in and out.
- Q./: zero-divisor handling, signs (kept in (Q/)), an overflow test
  that needs no division (|a| * 2^16 >= |b| * 2^(2N-1), possible only
  for |b| < 2^17), then (UQ/) and the sign.

Checked at 32- and 64-bit cells, optimised and ASan+UBSan, against an
independent limb-by-limb long division (including NODE-ERROR): every
pair of 18 edge Q values, 13 width-native edge values (true Q max/min at
either width), the overflow boundary, divisors in [2^(2N-2), 2^(2N-1)),
and pseudo-random cases; and against v3's q48_div for non-negative
a < 2^48. Q.* now also runs on the width-native edge values.
Mutations of the compare paths, the take path, the error flag and the
overflow mask are all caught (the mask matters only for Q min / -1.0).

Headroom (data under args / return): Q./ 3/2.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-03 00:17:11 -04:00
rajamesandClaude Opus 5.5 8f37e15f8a feat(v4.0.0): repack Q.* so no UM* call holds all four inputs
Q.* now forms its products in the order a1*b1 (low cell), a0*b1, a1*b0,
a0*b0, dropping each input after its last use, with b0 waiting on the
return stack. Each sign correction, (b1<0 ? a0 : 0) and (a1<0 ? b0 : 0),
is folded into cell 2 as soon as its operands are adjacent, using -if
rather than 0< calls. At most four live values sit under any UM* call.

Headroom (data cells under args / return entries): 2/2 -> 3/3.

Same checks as before at 32- and 64-bit cells, optimised and ASan+UBSan;
dropping either sign correction fails about 9900 checks.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 23:33:57 -04:00
rajamesandClaude Opus 5.5 54e1cdafb1 feat(v4.0.0): UM* corrections after the loop; return headroom 4 -> 6
UM* parked its three corrections (c_hi, c_lo, t0) on the return stack
before the +* loop, leaving its caller 4 return entries. Now u1 and u2
wait on the data stack under the loop -- +* touches only T, S and A --
and the corrections are made after it, with -if in place of 0< calls.
The return stack holds the loop count, then at most two temporaries.
The loop count is pushed before s is made, so the data stack never holds
more than four cells: data headroom is unchanged at 6.

Headroom (data cells under args / return entries): 6/4 -> 6/6.
Q.*, which calls UM* four times, goes from 2/1 to 2/2.

Same checks as before at 32- and 64-bit cells, optimised and
ASan+UBSan; breaking any of the four corrections fails 4900+ checks.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 23:31:52 -04:00
rajamesandClaude Opus 5.5 ab3b708540 feat(v4.0.0): Q.* from four UM* cell products
Q.* is floor(a*b / 2^16), signed (D-8), cut to two cells. Cells 0..2 of
the product come from the unsigned cell products a0*b0, a0*b1, a1*b0 and
the low cell of a1*b1; reading a1 and b1 as signed takes
(a1<0 ? b0 : 0) + (b1<0 ? a0 : 0) off cell 2. The result is cells 0..2
shifted right 16 with Q.TO-INT twice. Clobbers A.

Checked at 32- and 64-bit cells, optimised and ASan+UBSan, on every pair
of 17 edge Q values plus 20000 pseudo-random pairs:
- against an independent reference (16-bit limbs, magnitudes multiplied
  schoolbook, negated, shifted), and
- against v3's q48_mul for non-negative operands.

The first draft applied only a1's sign correction; the reference caught
the missing b1 term (9860 failures at 32-bit cells).

v3 bug found, not fixed: q48_mul's portable branch (used where there is
no __int128) returns (result_hi << 16) | (result_lo >> 16); the high
part must move up 48, so it is wrong whenever the product passes bit
64, e.g. 0.5 * Q max gives 0000ffffffffffff instead of 3fffffffffffffff.
The parity reference here is that branch with the shift corrected,
which matches v3's __int128 branch.

Stack use is tight: Q.* leaves its caller 2 data cells and 1 return
entry, because UM* parks three values on the return stack. Recorded in
5.26; to be improved next.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 23:27:57 -04:00
rajamesandClaude Opus 5.5 d0accdbb88 feat(v4.0.0): D< and Q comparisons; call-free (D<), DMAX, DMIN, 2SWAP
Executed on the golden model as written, and correct: <, =, D<, 2OVER,
and Q.=, Q.<, Q.0= (the D=, D<, D0= words).

Fixed, because they could not work under D-2 or were wrong:
- DMAX, DMIN: 2OVER 2OVER D< needs 8 data cells plus D<'s 2, the whole
  10-deep data stack, so both failed on every case once the caller held
  anything. Rewritten on a new call-free helper
    (D<) ( d1 d2 -- d1 d2 flag )
  which compares copies of the high cells, then the low cells unsigned
  on a tie, with in-line sign tests; DMAX and DMIN then drop the loser.
- 2SWAP: ROT and SWAP written in line. Return headroom 2 -> 4, which
  also lifts 2OVER 1 -> 3 and Q.> 1 -> 2.
- Q.>: section 5.26 gave SWAP D<, which swaps single cells; it was wrong
  in 11702 of 20169 cases. Now 2SWAP D<.

Checked at 32- and 64-bit cells, optimised and ASan+UBSan: every
edge-vector quadruple (50625) for D<, (D<), 2SWAP, 2OVER, DMAX and DMIN;
Q comparisons on every pair of 13 edge Q values plus 20000 pseudo-random
pairs weighted to ties and one-bit differences, signed (D-8) and against
v3's unsigned comparisons where both values have the same sign.
Mutating any (D<) branch or subtraction fails 700+ checks.

The new fatal-UBSan setting caught a test-side array overflow in the
headroom probe (results buffer sized 4, six needed); fixed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 23:06:25 -04:00
rajamesandClaude Opus 5.5 167fdc3973 build(v4): make UBSan reports fatal in make sanitize
Without -fno-sanitize-recover=all, UBSan prints a report and the run
carries on to "all v4 tests passed". The sanitize build now aborts on
the first report. Verified by rebuilding the test-side shift bug found
in 981f4180 with these flags: the run exits 1 at the report.

Both test binaries now also depend on v4/Makefile, so a flag change
rebuilds them instead of leaving stale binaries in place.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 22:59:50 -04:00
rajamesandClaude Opus 5.5 981f4180ce feat(v4.0.0): Q.FROM-INT and Q.TO-INT as +* double shifts
DECOMPOSITION.md 5.26 described both words in prose only. They are now
written out, call-free, on one observation: +* with S = 0 never adds, so
each step is an exact arithmetic right shift of the double T:A.

  : Q.FROM-INT ( n -- q )  push 0 a! 0 pop  15 FOR +* UNEXT  push drop a pop ;
      T:A = n:0 is n * 2^N; N-16 shifts leave n * 2^16 (count 15 at
      32-bit cells, 47 at 64).
  : Q.TO-INT ( q -- n )    push a! 0 pop  15 FOR +* UNEXT  drop drop a ;
      16 shifts at every width; the low cell is left in A. Rounds toward
      minus infinity, as v3's arithmetic shift does.

Both clobber A; added to the section 2 list.

Checked at 32- and 64-bit cells, optimised and ASan+UBSan:
- Q.FROM-INT against n * 2^16 for edge values and 20000 pseudo-random n,
  and against v3's q48_from_u64 for n >= 0 (low cell at 64-bit, D-10).
- Q.TO-INT against v3's (int64_t)q >> 16 on the edge Q values and 20000
  pseudo-random Q values, and against a C double shift on 20000
  arbitrary doubles.
- Round trip Q.TO-INT(Q.FROM-INT(n)) = n.
Mutating either shift count or the S = 0 setup fails 40000+ checks.

Note: make sanitize prints UBSan reports but does not fail on them. One
was found here, in the test's own random shift amount (fixed); a grep of
the full sanitize output now shows no runtime errors.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 22:58:04 -04:00
rajamesandClaude Opus 5.5 d948e0c1a3 test(v4.0.0): D-10 two-cell Q48.16; execute Q.ABS and Q.NEG against v3
D-10 (ruled 2026-10-02): a Q48.16 value is two cells at every cell
width, so every Q word is the same double word on 32- and 64-bit nodes.
Recorded in DECOMPOSITION.md section 3 and 5.26; the open note on the
Q.+/Q.- row is resolved by it.

Q.ABS and Q.NEG are the DABS and DNEGATE words. Checked against v3's
q48_abs and 0 - q on the 15 edge Q values and 20000 pseudo-random
values, at 32- and 64-bit cells, optimised and ASan+UBSan:
- 32-bit cells: bit-for-bit v3, including v3's wrap of Q min to itself.
- 64-bit cells: the low cell is v3's; the high cell is the true sign
  (so ABS and NEG of Q min give +2^63 rather than wrapping), per D-10.
Breaking DNEGATE's carry fails Q.NEG, Q.ABS and Q.- checks.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 22:54:40 -04:00
rajamesandClaude Opus 5.5 4f493fa317 test(v4.0.0): note Q.+/Q.- coverage in test_foundation.c header
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 22:52:54 -04:00
rajamesandClaude Opus 5.5 5ac52f19d6 test(v4.0.0): execute Q.+ and Q.- against v3 Q48.16
DECOMPOSITION.md 5.26 makes Q.+ and Q.- the D+ and D- words. They are
checked against v3's q48_add/q48_sub (uint64_t a + b, a - b, wrapping)
on every pair of 15 edge Q values (0, ulp, 0.5, 1.0, 1.5, -1.0, -ulp,
values across the 32-bit seam, Q max and min, +-12345.0) and 20000
pseudo-random pairs, 2682 of which overflow Q48.16.

- 32-bit cells: bit-for-bit v3's result, overflow wrap included.
- 64-bit cells, with a Q value as a sign-extended double: the low cell is
  v3's result; on overflow the high cell holds the true carry where v3
  wraps. Whether a Q value is one cell or two on a 64-bit node is not
  ruled; recorded as open in 5.26.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 22:52:27 -04:00
rajamesandClaude Opus 5.5 6a371b850e test(v4.0.0): execute M+, D-, D0= and D= on the golden model
All four run exactly as written in DECOMPOSITION.md 5.6/5.7 and need no
change now that D+ and DNEGATE are call-free.

Checked against C at 32- and 64-bit cells, optimised and ASan+UBSan:
every edge-vector combination (M+ over all triples, D- and D= over all
50625 quadruples, D0= over all pairs) plus 20000 pseudo-random cases
weighted to equal low or high cells and low sums that wrap to 0.
Mutations of D0= and M+ are caught.

Headroom (data cells under args / return entries under return address):
  M+ 6/4, D- 5/4, D0= 7/7, D= 5/3.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 22:50:30 -04:00
rajamesandClaude Opus 5.5 092036c97a feat(v4.0.0): call-free D+ (D-2 stack headroom)
D+ as written in 5.7 was exact but kept two cells on the return stack
while calling U> -> SWAP/U<, leaving its caller one return entry: any
word calling a word that calls D+ (M+, D-, D=, Q.+, Q.-) would have a
return address silently overwritten.

The new D+ makes no calls. Both high cells wait on the return stack; the
carry out of the low-cell add comes from sign tests -- if the low cells'
top bits differ, there is a carry exactly when the sum's top bit is
clear; if they match, exactly when both are set.

Headroom (data cells under args / return entries): 4/1 -> 6/5.
Checked against C over all 50625 edge-vector quadruples and 20000
pseudo-random pairs (weighted to top-bit cases and low sums wrapping to
0), at 32- and 64-bit cells, optimised and ASan+UBSan. Retargeting each
of the four carry branches fails more than 13000 checks.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 22:46:11 -04:00
rajamesandClaude Opus 5.5 93d09840da feat(v4.0.0): SM/REM and DNEGATE call-free; execute /MOD and its section 5 words
SM/REM as written in section 4 never returned correctly for a negative
dividend. It holds three entries on the return stack and then calls
DABS -> DNEGATE -> D+ -> U> -> SWAP/U<, which overflows the 9-deep
circular return stack (D-2). DABS itself could not run: DNEGATE as
written (inv SWAP inv SWAP 1 0 D+) left its caller no return entries.

- DNEGATE: inv over if L1 drop push inv 1 + pop ; L1: drop 1 + ;
  i.e. ~d + 1, carrying into the high cell exactly when lo = 0.
- SM/REM: sign tests are native -if (as in 0<) and NEGATE is in line;
  the only calls are DNEGATE and UM/MOD, both call-free inside.

Executed on the golden model at 32- and 64-bit cells, optimised and
under ASan+UBSan:
- SM/REM on dividends built as q*n + r with |r| < |n| and r signed as
  d: every edge-vector q, n with r = 0 and r = +-(|n|-1), plus 20000
  pseudo-random cases.
- /MOD, U>, ABS, S>D, D+ and DABS as written in section 5, against C
  (D+ over all 50625 edge-vector quadruples).
Mutations of DNEGATE's carry and of each SM/REM sign branch are caught.

Headroom (data cells under args / return entries under return address):
  SM/REM 5/3, /MOD 5/2, DNEGATE 7/7, DABS 7/6, ABS 8/7, U> 6/5.
D+ as written is exact but leaves only 1 return entry; recorded in
DECOMPOSITION.md 5.7 as not yet revised.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 22:44:04 -04:00
rajamesandClaude Opus 5.5 3b9d1e4337 feat(v4.0.0): call-free UM/MOD loop for D-2 stack headroom
The first UM/MOD was exact but called 0<, U<, SWAP and OR inside its
loop, so it left its caller only 3 return-stack entries. SM/REM pushes
two signs before calling it, so under /MOD, M/MOD or */MOD the caller's
return address would be silently overwritten (D-2 circular stacks).

The loop now makes no calls. It branches on hi's top bit with -if, does
the unsigned hi' >= d test as U< does but with in-line sign tests,
subtracts with `inv a + inv`, and sets the quotient bit with `1 +` on an
even lo'. The final SWAP is in line.

Measured on the golden model at 32- and 64-bit cells:
  headroom   data 3 -> 6 cells under args, return 3 -> 6 entries
  speed      ~1355-1605 -> ~227-313 instruction words per call
Still exact for every uhi < ud (edge-vector triples and 20000 random
cases, optimised and ASan+UBSan). Retargeting each of the four in-loop
branches to the wrong label fails more than 12000 checks each.

DECOMPOSITION.md: section 4 UM/MOD replaced, with its derivation and
stack limits.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 22:35:49 -04:00
rajamesandClaude Opus 5.5 41f59afeb3 test(v4.0.0): execute UM/MOD on the golden model; measure stack headroom
UM/MOD is assembled exactly as DECOMPOSITION.md section 4 gives it and
needs no change: it is exact for every uhi < ud at 32- and 64-bit cells.
It is checked against q*d + r = uhi:ulo with r < d through v4_umul, so
no second C divider has to be trusted. Coverage: all edge-vector triples
with uhi < ud plus 20000 pseudo-random cases (top-bit, small and
near-maximum divisors), optimised and under ASan+UBSan. Two hand
mutations each fail more than 15000 checks.

New headroom probe: runs a word with marked cells under the canary and
under its return address and reports how many survive, since the D-2
circular stacks overwrite silently instead of faulting. Measured:
  UM*     6 data cells under its args, 4 return entries under its return
  UM/MOD  3 data cells under its args, 3 return entries under its return

DECOMPOSITION.md: UM/MOD marked executed, with its defined range and
stack limits.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 19:48:04 -04:00
rajamesandClaude Opus 5.5 9a391eb0ad 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>
2026-10-02 19:21:17 -04:00
rajamesandClaude Opus 5.5 067f317c47 feat(v4.0.0): hosted golden model, single node
First code for StarForth v4 (JUSTIFICATION.md section 10, step 1): one node
of the 32-instruction core as a C99 model, with cell width as a build
parameter.

- Node: P, A, B, F18 circular stacks (10 and 9 deep, D-2), word-addressed
  memory (D-1), 5% guard bands on every bounded list.
- Instruction word: six 5-bit slots in 32 bits at every cell width.
- Executor: all 32 opcodes of DECOMPOSITION.md 1.3. Cell arithmetic wraps
  explicitly; no signed overflow or implementation-defined shift.
- Heat: per-opcode and per-call-target counters and the anti-clock, driven
  by instruction retirement (1.4, D-6 interim).
- Slot packer and runner for tests, and a reference unsigned multiply in
  plain C99 with no 128-bit type.

Tests run at 32- and 64-bit cells, and under ASan and UBSan. They cover
every opcode and execute the first section 4 definitions (NIP SWAP OR
NEGATE ROT 0< 0= 2DUP - U<) against the C operation each stands for.

UM* as written in section 4 is exact only while u1 <= 2^(n-2). Two known
failing cases are pinned in test_foundation.c until it is rewritten.

DECOMPOSITION.md: record D-9, the instruction word is 32 bits at every
cell width (ruled 2026-10-02).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2026-10-02 14:38:27 -04:00
rajames 1f98034311 Merge remote-tracking branch 'origin/StarForth-v4.0.0' into StarForth-v4.0.0 2026-10-01 15:55:37 -04:00
rajamesandJunie a8b70e88d3 Reorganize source tree: kernel/, v3/, v4/ split and board infrastructure
Source tree reorganization:
- Move StarForth v3 engine to v3/ (src/, include/, Makefile)
- Move kernel to kernel/ (src/, include/, linker/, Makefile)
- Create v4/ skeleton for F18-ISA golden model (DECOMPOSITION.md, JUSTIFICATION.md)
- Move FABRIC-0..4.md to docs/fabric/
- Move ONTOLOGY.md and ROADMAP.md to docs/

Board infrastructure:
- Add boards/ser5/, boards/raspi/, boards/milkv/, boards/zynq7020/
- Each board has board.mk (ISA, CPU flags, boot recipe) and README.md
- Root Makefile becomes thin dispatcher: boot_image, all, clean, docs take TARGET
- make boot_image TARGET=SER5|RASPI|MILKV builds one GPT/MBR image per board
- ZYNQ7020 target exists but stops with clear error (ARMv7 port not built yet)
- scripts/mkdiskimage.sh builds disk images for all boards

Docs pipeline:
- docs/book/ with LaTeX master (main.tex) and Makefile
- pandoc converts Markdown to LaTeX at build time
- Two Lua filters: table-widths.lua (wide tables wrap), code-breaks.lua (inline code breaks)
- make docs builds single PDF (754 pages, 0 missing characters)
- make docs TARGET=<board> adds board appendix
- build/docs/<book|board>/meta.tex stamps git commit into PDF

Bug fixes:
- 42 include paths that only worked by accident now use correct relative paths
- clang-18 hardcode replaced with configurable CC variable (fixed aarch64 build)
- Pi 5: kernel_2712.img linked at 0x80000, .bss zeroed, memory reserved
- Doxyfile, .clang-tidy, README.md, Kconfig paths updated

Verified:
- Hosted v3 build passes 1012 tests, 0 failures
- SER5 image boots in QEMU (OVMF), POST passes, K exact (65536 = Q48_ONE)
- Milk-V image boots in QEMU (OpenSBI + U-Boot + bootefi), POST passes
- make clean TARGET=<board> removes only that board and its ISA objects
- make all builds all boards, hosted v3, and docs in one run

Co-authored-by: Junie <junie@jetbrains.com>
2026-10-01 15:40:09 -04:00
Claude f238f02afa docs(v4.0.0): record D-1..D-8 rulings in DECOMPOSITION.md
D-1 word addressing; D-2 F18 circular stacks (10/9 deep), hidden, so
DEPTH/PICK/ROLL/.S/SP@/SP! are retired everywhere and the DSP register is
dropped; D-3 plain F18 +* (UM* flagged for revision); D-5 host width
matches the host CPU; D-7 moot; D-8 signed Q48.16; D-4 and D-6 deferred
to the hosted-mesh step. Adds a note that every CAP definition must be
re-checked against the 10/9 stack depths.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BY9HMwK5Cetz3caBgHGyds
2026-10-01 00:55:20 +00:00
666 changed files with 36455 additions and 2103 deletions
+1 -1
View File
@@ -14,7 +14,7 @@ Checks: >
WarningsAsErrors: [ ] WarningsAsErrors: [ ]
HeaderFilterRegex: '^src/.*|^include/.*' HeaderFilterRegex: '^v3/(src|include)/.*|^kernel/(src|include)/.*'
AnalyzeTemporaryDtors: false AnalyzeTemporaryDtors: false
FormatStyle: none FormatStyle: none
+28 -28
View File
@@ -6,8 +6,8 @@
# clang-tidy will ALWAYS false-positive them. Always. # clang-tidy will ALWAYS false-positive them. Always.
# --------------------------------------------------------- # ---------------------------------------------------------
src/platform/** v3/src/platform/**
src/platform/* v3/src/platform/*
# --------------------------------------------------------- # ---------------------------------------------------------
# Skip test infrastructure # Skip test infrastructure
@@ -15,8 +15,8 @@ src/platform/*
# and stress edge conditions clang-tidy will never grok. # and stress edge conditions clang-tidy will never grok.
# --------------------------------------------------------- # ---------------------------------------------------------
src/test_runner/** v3/src/test_runner/**
src/test_runner/* v3/src/test_runner/*
# --------------------------------------------------------- # ---------------------------------------------------------
# Skip word definitions generated or "mechanically patterned" # Skip word definitions generated or "mechanically patterned"
@@ -24,30 +24,30 @@ src/test_runner/*
# clang-tidy gives ZERO useful feedback on them. # clang-tidy gives ZERO useful feedback on them.
# --------------------------------------------------------- # ---------------------------------------------------------
src/word_source/string_words.c v3/src/word_source/string_words.c
src/word_source/block_words.c v3/src/word_source/block_words.c
src/word_source/arithmetic_words.c v3/src/word_source/arithmetic_words.c
src/word_source/mixed_arithmetic_words.c v3/src/word_source/mixed_arithmetic_words.c
src/word_source/return_stack_words.c v3/src/word_source/return_stack_words.c
src/word_source/defining_words.c v3/src/word_source/defining_words.c
src/word_source/stack_words.c v3/src/word_source/stack_words.c
src/word_source/logical_words.c v3/src/word_source/logical_words.c
src/word_source/memory_words.c v3/src/word_source/memory_words.c
src/word_source/io_words.c v3/src/word_source/io_words.c
src/word_source/dictionary_words.c v3/src/word_source/dictionary_words.c
src/word_source/dictionary_manipulation_words.c v3/src/word_source/dictionary_manipulation_words.c
src/word_source/vocabulary_words.c v3/src/word_source/vocabulary_words.c
src/word_source/system_words.c v3/src/word_source/system_words.c
src/word_source/starforth_words.c v3/src/word_source/starforth_words.c
src/word_source/editor_words.c v3/src/word_source/editor_words.c
src/word_source/format_words.c v3/src/word_source/format_words.c
# --------------------------------------------------------- # ---------------------------------------------------------
# Skip headers belonging to the word system # Skip headers belonging to the word system
# Same reason: no signal, infinite false positives. # Same reason: no signal, infinite false positives.
# --------------------------------------------------------- # ---------------------------------------------------------
src/word_source/include/* v3/src/word_source/include/*
# --------------------------------------------------------- # ---------------------------------------------------------
# Skip anything that implements performance knobs, # Skip anything that implements performance knobs,
@@ -55,15 +55,15 @@ src/word_source/include/*
# These are meant to be weird, and tidy can't reason about them. # These are meant to be weird, and tidy can't reason about them.
# --------------------------------------------------------- # ---------------------------------------------------------
src/stack_management.c v3/src/stack_management.c
src/profiler.c v3/src/profiler.c
src/vm_debug.c v3/src/vm_debug.c
src/physics_runtime.c v3/src/physics_runtime.c
# --------------------------------------------------------- # ---------------------------------------------------------
# Skip integration + stress torture-tests. # Skip integration + stress torture-tests.
# These *intentionally* do UB-like bullshit. # These *intentionally* do UB-like bullshit.
# --------------------------------------------------------- # ---------------------------------------------------------
src/test_runner/modules/*stress* v3/src/test_runner/modules/*stress*
src/test_runner/modules/*integration* v3/src/test_runner/modules/*integration*
+20 -20
View File
@@ -224,43 +224,43 @@ changes with any new C word registration).
```bash ```bash
# Build kernel for a given architecture (amd64 default) # Build kernel for a given architecture (amd64 default)
make -f Makefile.starkernel ARCH=amd64 make -f kernel/Makefile ARCH=amd64
make -f Makefile.starkernel ARCH=aarch64 make -f kernel/Makefile ARCH=aarch64
make -f Makefile.starkernel ARCH=riscv64 make -f kernel/Makefile ARCH=riscv64
# Run in QEMU with OVMF # Run in QEMU with OVMF
make -f Makefile.starkernel qemu make -f kernel/Makefile qemu
make -f Makefile.starkernel ARCH=aarch64 qemu make -f kernel/Makefile ARCH=aarch64 qemu
make -f Makefile.starkernel ARCH=riscv64 qemu make -f kernel/Makefile ARCH=riscv64 qemu
# Clean # Clean
make -f Makefile.starkernel clean make -f kernel/Makefile clean
``` ```
Output: `build/<arch>/kernel/starkernel_loader.efi` + `build/<arch>/kernel/starkernel_kernel.elf`. Output: `build/<arch>/kernel/starkernel_loader.efi` + `build/<arch>/kernel/starkernel_kernel.elf`.
Two independently tracked version strings flow into the generated `include/version.h`: Two independently tracked version strings flow into the generated `include/version.h`:
`VERSION` (`Makefile.starkernel` — the embedded StarForth engine version, currently `3.1.0`; `VERSION` (`kernel/Makefile` — the embedded StarForth engine version, currently `3.1.0`;
note this does **not** auto-sync with the standalone StarForth repo's own version) and note this does **not** auto-sync with the standalone StarForth repo's own version) and
`LITHOS_VERSION` (`Makefile.starkernel` — the kernel version, currently **`2.0.0`**; `LITHOS_VERSION` (`kernel/Makefile` — the kernel version, currently **`2.0.0`**;
corrected 2026-09-19 — this file said `2.0.1`, but `FABRIC-3.md` §I.2 rolled it back to corrected 2026-09-19 — this file said `2.0.1`, but `FABRIC-3.md` §I.2 rolled it back to
`2.0.0` on 2026-09-04 because `2.0.1` names the SER5 hardware-track line and claims hardware `2.0.0` on 2026-09-04 because `2.0.1` names the SER5 hardware-track line and claims hardware
progress not yet verified. The versioning policy is **semantic, not sequential** — see the progress not yet verified. The versioning policy is **semantic, not sequential** — see the
roadmap table in `Makefile.starkernel` before choosing any version). roadmap table in `kernel/Makefile` before choosing any version).
### Build configuration (Kconfig — real, wired, not vestigial) ### Build configuration (Kconfig — real, wired, not vestigial)
Every kernel-only knob (`STARFORTH_ENABLE_VM`, `PARITY_MODE`, the shared physics/heartbeat Every kernel-only knob (`STARFORTH_ENABLE_VM`, `PARITY_MODE`, the shared physics/heartbeat
family, etc.) is an optional Kconfig symbol defined across `Kconfig`, `Kconfig.arch`, family, etc.) is an optional Kconfig symbol defined across `Kconfig`, `Kconfig.arch`,
`Kconfig.heartbeat`, `Kconfig.kernel`, `Kconfig.physics`, `Kconfig.variant` (~40 symbols `Kconfig.heartbeat`, `Kconfig.kernel`, `Kconfig.physics`, `Kconfig.variant` (~40 symbols
total). `Makefile.starkernel` pulls its defaults from this system via a `kconfig_bool(...)` total). `kernel/Makefile` pulls its defaults from this system via a `kconfig_bool(...)`
mechanism — e.g. `STARFORTH_ENABLE_VM` defaults to **1** (confirmed at mechanism — e.g. `STARFORTH_ENABLE_VM` defaults to **1** (confirmed at
`Makefile.starkernel:61`), meaning a plain `make -f Makefile.starkernel` already builds with `kernel/Makefile:61`), meaning a plain `make -f kernel/Makefile` already builds with
VM + capsule-birth + ACL active. A bare invocation uses the defaults it always has: VM + capsule-birth + ACL active. A bare invocation uses the defaults it always has:
```bash ```bash
make -f Makefile.starkernel ARCH=amd64 menuconfig make -f kernel/Makefile ARCH=amd64 menuconfig
make -f Makefile.starkernel ARCH=amd64 kernel_amd64_defconfig make -f kernel/Makefile ARCH=amd64 kernel_amd64_defconfig
``` ```
### Hosted VM (vendored, for local sanity only) ### Hosted VM (vendored, for local sanity only)
@@ -277,7 +277,7 @@ StarForth repo) were removed 2026-08-15 — they referenced
in the actual generated `include/version.h` (which only has `STARFORTH_VERSION`, in the actual generated `include/version.h` (which only has `STARFORTH_VERSION`,
`STARFORTH_ARCH`, `STARFORTH_TARGET`, `STARFORTH_TIMESTAMP`, `STARFORTH_VERSION_FULL`, `STARFORTH_ARCH`, `STARFORTH_TARGET`, `STARFORTH_TIMESTAMP`, `STARFORTH_VERSION_FULL`,
`LITHOS_VERSION`, `LITHOS_VERSION_STR`), so they could never have worked. Bump versions by hand-editing the `VERSION`/ `LITHOS_VERSION`, `LITHOS_VERSION_STR`), so they could never have worked. Bump versions by hand-editing the `VERSION`/
`LITHOS_VERSION` variables in `Makefile.starkernel` instead. Report the broken targets if `LITHOS_VERSION` variables in `kernel/Makefile` instead. Report the broken targets if
asked, don't silently fix them. asked, don't silently fix them.
### Important: Linker Configuration ### Important: Linker Configuration
@@ -298,9 +298,9 @@ The vendored hosted `make` build (above) is NEVER used to validate kernel change
```bash ```bash
# Run in this exact order for every kernel change: # Run in this exact order for every kernel change:
make -f Makefile.starkernel ARCH=amd64 clean qemu make -f kernel/Makefile ARCH=amd64 clean qemu
make -f Makefile.starkernel ARCH=aarch64 clean qemu make -f kernel/Makefile ARCH=aarch64 clean qemu
make -f Makefile.starkernel ARCH=riscv64 clean qemu make -f kernel/Makefile ARCH=riscv64 clean qemu
``` ```
**QEMU rule — non-negotiable:** Only ONE QEMU instance may run at a time, always in the **QEMU rule — non-negotiable:** Only ONE QEMU instance may run at a time, always in the
@@ -475,7 +475,7 @@ listed in `proof/ROOT` (corrected 2026-09-19; this file said 23, and `proof/COVE
said 52 all along). **Read `proof/COVERAGE.md` first**: its stated goal is not a green build but said 52 all along). **Read `proof/COVERAGE.md` first**: its stated goal is not a green build but
"identify precisely what cannot be proven and why — the boundary between 'formally verified' "identify precisely what cannot be proven and why — the boundary between 'formally verified'
and 'not, for this specific reason'." Run `isabelle build -D proof/` and 'not, for this specific reason'." Run `isabelle build -D proof/`
directly; neither `Makefile` nor `Makefile.starkernel` in this repo defines an directly; neither `Makefile` nor `kernel/Makefile` in this repo defines an
`isabelle-build`/`isabelle-check` target (unlike the standalone StarForth repo, which has a `isabelle-build`/`isabelle-check` target (unlike the standalone StarForth repo, which has a
broken one — this repo simply doesn't have the target at all, so there's nothing to broken one — this repo simply doesn't have the target at all, so there's nothing to
mistakenly invoke). mistakenly invoke).
@@ -495,7 +495,7 @@ status for kernel work.
- **Strict ANSI C99** — No GNU extensions, no C++ features - **Strict ANSI C99** — No GNU extensions, no C++ features
- **Zero warnings target, with four explicit exceptions — corrected 2026-08-18, previous - **Zero warnings target, with four explicit exceptions — corrected 2026-08-18, previous
claim was wrong.** Build with `-Wall -Wextra -Werror`, but `Makefile.starkernel` carries claim was wrong.** Build with `-Wall -Wextra -Werror`, but `kernel/Makefile` carries
`-Wno-error=unused-parameter -Wno-error=shift-negative-value -Wno-error=sign-compare `-Wno-error=unused-parameter -Wno-error=shift-negative-value -Wno-error=sign-compare
-Wno-error=missing-field-initializers` — those four classes are enabled (still visible as -Wno-error=missing-field-initializers` — those four classes are enabled (still visible as
warnings) but deliberately downgraded from fatal, everything else is. The previous version warnings) but deliberately downgraded from fatal, everything else is. The previous version
+10 -7
View File
@@ -933,10 +933,12 @@ WARN_LOGFILE = docs/api/doxygen_warnings.log
# spaces. See also FILE_PATTERNS and EXTENSION_MAPPING # spaces. See also FILE_PATTERNS and EXTENSION_MAPPING
# Note: If this tag is empty the current directory is searched. # Note: If this tag is empty the current directory is searched.
INPUT = include \ INPUT = v3/include \
src \ v3/src \
src/word_source \ v3/src/word_source \
src/test_runner \ v3/src/test_runner \
kernel/include \
kernel/src \
README.md README.md
# This tag can be used to specify the character encoding of the source files # This tag can be used to specify the character encoding of the source files
@@ -2366,9 +2368,10 @@ SEARCH_INCLUDES = YES
# RECURSIVE has no effect here. # RECURSIVE has no effect here.
# This tag requires that the tag SEARCH_INCLUDES is set to YES. # This tag requires that the tag SEARCH_INCLUDES is set to YES.
INCLUDE_PATH = include \ INCLUDE_PATH = v3/include \
src/word_source/include \ kernel/include \
src/test_runner/include v3/src/word_source/include \
v3/src/test_runner/include
# You can use the INCLUDE_FILE_PATTERNS tag to specify one or more wildcard # You can use the INCLUDE_FILE_PATTERNS tag to specify one or more wildcard
# patterns (like *.h and *.hpp) to filter out the header-files in the # patterns (like *.h and *.hpp) to filter out the header-files in the
+1 -1
View File
@@ -5,7 +5,7 @@ choice
default ARCH_AMD64 default ARCH_AMD64
help help
Selects the value passed as ARCH= to whichever Makefile Selects the value passed as ARCH= to whichever Makefile
(Makefile or Makefile.starkernel) is driven from this config. (Makefile or kernel/Makefile) is driven from this config.
Both Makefiles already accept "amd64"/"aarch64"/"riscv64" as Both Makefiles already accept "amd64"/"aarch64"/"riscv64" as
canonical spellings (each has its own alias-normalizing logic canonical spellings (each has its own alias-normalizing logic
for other spellings like x86_64/arm64/riscv), so this choice for other spellings like x86_64/arm64/riscv), so this choice
+1 -1
View File
@@ -17,7 +17,7 @@ config HEARTBEAT_THREAD_ENABLED
builds without needing a special case. This is UI/model builds without needing a special case. This is UI/model
correctness (menuconfig can't offer a choice LithosAnanke has no correctness (menuconfig can't offer a choice LithosAnanke has no
way to honor -- there are no pthreads in a freestanding kernel), way to honor -- there are no pthreads in a freestanding kernel),
not the sole enforcement mechanism: Makefile.starkernel additionally not the sole enforcement mechanism: kernel/Makefile additionally
keeps its own unconditional `VM_FEATURE_OVERRIDES += keeps its own unconditional `VM_FEATURE_OVERRIDES +=
-DHEARTBEAT_THREAD_ENABLED=0` post-override exactly as it was -DHEARTBEAT_THREAD_ENABLED=0` post-override exactly as it was
before this migration. Deliberately redundant with the `depends before this migration. Deliberately redundant with the `depends
+1 -1
View File
@@ -11,7 +11,7 @@ config STARFORTH_ENABLE_VM
kernel that only reaches the M0-M6 hardware milestones (console, kernel that only reaches the M0-M6 hardware milestones (console,
PMM, VMM, interrupts, timers, kmalloc) with no FORTH interpreter, PMM, VMM, interrupts, timers, kmalloc) with no FORTH interpreter,
no capsules, no "ok" REPL. Gates a large source-file selection no capsules, no "ok" REPL. Gates a large source-file selection
block in Makefile.starkernel, not just a handful of -D flags. block in kernel/Makefile, not just a handful of -D flags.
config PARITY_MODE config PARITY_MODE
bool "Deterministic parity harness mode (PARITY_MODE)" bool "Deterministic parity harness mode (PARITY_MODE)"
+133 -1314
View File
File diff suppressed because it is too large Load Diff
+46 -7
View File
@@ -6,6 +6,25 @@
--- ---
## Products
StarForth v4 moves the engine onto a 32-instruction core derived from Chuck Moore's F18
(`docs/v4.0.0/`). With it, this repository carries three products, not one:
| Product | What it is |
|---|---|
| **Hosted StarForth F18** | The v4 engine as a native Linux build, for amd64, arm64 and riscv64, on real hardware. |
| **FPGA StarForth F18** | A 32-bit build of the same engine loaded into the FPGA. It is the gateway to the rest: the foundation everything else is built up from. |
| **StarshipOS** | The bare-metal product: LithosAnanke running the v4 F18 engine. |
FORTH-79 is recomposed on the F18 engine and stored as a capsule; the StarshipOS-specific
vocabulary gets the same treatment. The source tree will be reorganised around this split.
v3 remains the reference system until v4 meets its acceptance criteria
(`docs/v4.0.0/JUSTIFICATION.md` §16). Everything below describes v3 as it stands today.
---
## Status — M7.1 (Capsule System · Multi-VM Fleet) ## Status — M7.1 (Capsule System · Multi-VM Fleet)
| Milestone | | Status | | Milestone | | Status |
@@ -48,19 +67,39 @@ POST at boot: **parity hash verified across amd64/aarch64/riscv64 · Mama capsul
## Quick Start ## Quick Start
```bash ```bash
# One boot image per physical target (output: build/boards/<board>/)
make boot_image TARGET=SER5 # Beelink SER5 -- GPT/ESP, BOOTX64.EFI
make boot_image TARGET=RASPI # Raspberry Pi 5 -- FAT, config.txt + kernel_2712.img + DTB
make boot_image TARGET=MILKV # Milk-V Mars -- GPT/ESP, BOOTRISCV64.EFI (U-Boot bootefi)
make boot_image TARGET=ZYNQ7020 # Zynq-7020 -- ARMv7 port in progress
make boards # list boards
# The same TARGET drives all, docs and clean (make help)
make # every board with a kernel port + hosted v3 + the book
make TARGET=RASPI # one board's image + build/docs/LithosAnanke-raspi.pdf
make docs # build/docs/LithosAnanke.pdf (LaTeX master: docs/book/main.tex)
make clean TARGET=RASPI # that board's outputs and build/aarch64/kernel
make clean # all of build/ except build/cache/
# Build kernel (requires cross-compilation toolchain, or native gcc) # Build kernel (requires cross-compilation toolchain, or native gcc)
make -f Makefile.starkernel ARCH=amd64 make -f kernel/Makefile ARCH=amd64
# Run in QEMU with OVMF # Run in QEMU with OVMF
make -f Makefile.starkernel qemu make -f kernel/Makefile qemu
# Other architectures # Other architectures
make -f Makefile.starkernel ARCH=aarch64 qemu make -f kernel/Makefile ARCH=aarch64 qemu
make -f Makefile.starkernel ARCH=riscv64 qemu make -f kernel/Makefile ARCH=riscv64 qemu
``` ```
Artifacts: `build/amd64/kernel/starkernel_loader.efi` · `build/amd64/kernel/starkernel_kernel.elf` Artifacts: `build/amd64/kernel/starkernel_loader.efi` · `build/amd64/kernel/starkernel_kernel.elf`
Tree: `kernel/` (LithosAnanke: `Makefile`, `src/`, `include/starkernel/`, `linker/`),
`v3/` (StarForth v3 engine and hosted build: `Makefile`, `src/`, `include/`),
`v4/` (StarForth v4, see `docs/v4.0.0/`), `boards/<board>/` (`board.mk` + boot files).
Every makefile runs from the repo root; the root `Makefile` forwards any other goal to
`v3/Makefile` (hosted build).
For the hosted VM by itself (Linux, no cross-compiler needed, no bare-metal tooling): see For the hosted VM by itself (Linux, no cross-compiler needed, no bare-metal tooling): see
the separate **StarForth** repository — LithosAnanke used to be a branch inside that repo, the separate **StarForth** repository — LithosAnanke used to be a branch inside that repo,
now it's its own project with its own `master`. now it's its own project with its own `master`.
@@ -69,12 +108,12 @@ now it's its own project with its own `master`.
Every kernel-only knob (`STARFORTH_ENABLE_VM`, `PARITY_MODE`, the shared Every kernel-only knob (`STARFORTH_ENABLE_VM`, `PARITY_MODE`, the shared
physics/heartbeat family, etc.) is an optional Kconfig symbol — a plain physics/heartbeat family, etc.) is an optional Kconfig symbol — a plain
`make -f Makefile.starkernel` uses the same defaults it always has unless `make -f kernel/Makefile` uses the same defaults it always has unless
you opt in: you opt in:
```bash ```bash
make -f Makefile.starkernel ARCH=amd64 menuconfig make -f kernel/Makefile ARCH=amd64 menuconfig
make -f Makefile.starkernel ARCH=amd64 kernel_amd64_defconfig make -f kernel/Makefile ARCH=amd64 kernel_amd64_defconfig
``` ```
--- ---
+29
View File
@@ -0,0 +1,29 @@
# boards/
One directory per physical target. `make boot_image TARGET=<NAME>` (repo root) maps the
name to a directory here, reads its `board.mk`, and builds the single file that goes on
that board's boot medium into `build/boards/<board>/`.
| TARGET | Directory | ISA | Boot path | Image |
|---|---|---|---|---|
| `SER5` | `ser5/` | amd64 | UEFI firmware, removable-media path | GPT + FAT32 ESP: `EFI/BOOT/BOOTX64.EFI` |
| `RASPI` | `raspi/` | aarch64 | Pi 5 EEPROM firmware, native | MBR + FAT32: `config.txt`, `kernel_2712.img`, `bcm2712-rpi-5-b.dtb` |
| `MILKV` | `milkv/` | riscv64 | SPI-flash U-Boot + OpenSBI, `bootefi` | GPT + FAT32 ESP: `EFI/BOOT/BOOTRISCV64.EFI` |
| `ZYNQ7020` | `zynq7020/` | armv7 | BootROM, `BOOT.BIN`, U-Boot | not yet: needs `kernel/src/arch/armv7` |
`board.mk` sets:
- `BOARD_DESC`: one-line description (`make boards`)
- `BOARD_ARCH`: kernel ISA (`kernel/src/arch/<arch>`)
- `BOARD_BOOT`: image recipe in `kernel/Makefile` (`uefi-esp`, `rpi-native`, ...)
- `BOARD_IMAGE`: output file name
Disk images are assembled by `scripts/mkdiskimage.sh`, which needs no root access and no loop
devices. `KERNEL_ARGS="..."` is written as `starforth.cfg` (UEFI boards) or `cmdline.txt`
(Pi 5, where the firmware copies it into `/chosen/bootargs`). `BOOT_IMAGE_SIZE_MIB` sets the
image size; the default is 128.
Hardware status: none of these images has been booted on real silicon from this build. The
SER5 image has been booted in QEMU (q35 + OVMF, from its own disk) through POST. The Pi 5
native path (`raspi/README.md`) and the JH7110 peripherals have still only been checked by
compiling.
+30
View File
@@ -0,0 +1,30 @@
# Milk-V Mars boot media
`make boot_image TARGET=MILKV` builds `build/boards/milkv/lithos-milkv.img`: a GPT disk with one
FAT32 EFI System Partition. Write it to an SD card with `dd`. The partition holds:
- `EFI/BOOT/BOOTRISCV64.EFI`: the riscv64 monolithic loader, the same one QEMU boots.
- `startup.nsh`: for a UEFI shell, if one is used.
- `starforth.cfg`: only present when `KERNEL_ARGS="..."` is given.
The board's own SPI-flash U-Boot, with OpenSBI underneath, finds the loader through its standard
`bootefi` scan of the removable-media path. U-Boot passes its devicetree to the loader through the
EFI configuration table.
Status: booted in QEMU through the same chain the board uses: OpenSBI, then U-Boot
`qemu-riscv64_smode`, then `bootefi` from this image's ESP, then the loader and the kernel. POST
passed, Stadium conservation was exact (resident 43691 + reservoir 21845 = 65536 = `Q48_ONE`), and
Hestia and Artemis came up. Not yet booted on the Mars itself. The JH7110 peripherals
(framebuffer, RNG) have only been checked by compiling.
To repeat the QEMU boot (`qemu-system-riscv64` is in Ubuntu 26.04's `qemu-system-riscv` package;
OpenSBI and U-Boot come from `opensbi` and `u-boot-qemu`). Use a copy, because the kernel writes
to its disk:
```
cp build/boards/milkv/lithos-milkv.img /tmp/mv.img
qemu-system-riscv64 -machine virt -cpu rv64 -m 2048 -nographic \
-bios /usr/lib/riscv64-linux-gnu/opensbi/generic/fw_dynamic.bin \
-kernel /usr/lib/u-boot/qemu-riscv64_smode/u-boot.bin \
-drive if=none,format=raw,file=/tmp/mv.img,id=d0 -device virtio-blk-device,drive=d0
```
+11
View File
@@ -0,0 +1,11 @@
# boards/milkv/board.mk -- Milk-V Mars (StarFive JH7110, SiFive U74, RV64GC).
#
# The board's own SPI-flash U-Boot (OpenSBI underneath) runs the EFI
# application through its standard distro/bootefi scan: the SD card is a GPT
# disk with one FAT32 EFI System Partition holding EFI/BOOT/BOOTRISCV64.EFI,
# the same riscv64 monolithic loader QEMU boots. U-Boot passes its own
# devicetree through the EFI configuration table.
BOARD_DESC := Milk-V Mars (StarFive JH7110, RV64GC, U-Boot bootefi)
BOARD_ARCH := riscv64
BOARD_BOOT := uefi-esp
BOARD_IMAGE := lithos-milkv.img
+20
View File
@@ -0,0 +1,20 @@
# Raspberry Pi 5 native boot media
`make boot_image TARGET=RASPI` builds `build/boards/raspi/lithos-raspi.img`: an MBR disk
with one FAT32 (LBA) partition. Write it to an SD card with `dd`. The partition holds:
- `config.txt`: checked in here (FABRIC-3.md §IV.3 item 6). It pins `kernel_address=0x80000`
because Pi 5 firmware loads `kernel_2712.img` at 0x200000 by default.
- `kernel_2712.img`: the aarch64 kernel objects relinked at 0x80000 by
`kernel/linker/starkernel-native-rpi5.ld`, entered at `rpi5_native_start`
(`kernel/src/arch/aarch64/native_rpi5_entry.S`, which zeroes `.bss` first), and flattened
with `objcopy -O binary`.
- `bcm2712-rpi-5-b.dtb`: the Raspberry Pi firmware's own stock DTB. It is not built by this
project; it is fetched once from the firmware release pinned in `board.mk`
(`RPI_FIRMWARE_TAG`) into `build/cache/`. To use a local copy, pass `RPI5_DTB=/path/to/dtb`.
- `cmdline.txt`: only present when `KERNEL_ARGS="..."` is given. The firmware copies it into
`/chosen/bootargs`, which `rpi5_native_boot()` parses.
Not yet verified on hardware. The native path still assumes everything `kernel_main()`
needs after a UEFI handoff. The firmware enters at EL2 with the MMU off, which is not what
UEFI hands over, and that difference has not been exercised.
+18
View File
@@ -0,0 +1,18 @@
# boards/raspi/board.mk -- Raspberry Pi 5 (BCM2712, Cortex-A76, aarch64).
#
# Native firmware boot, no UEFI (FABRIC-3.md §IV): the Pi 5 bootloader
# lives in EEPROM and reads config.txt, kernel_2712.img and the board DTB
# from the first FAT partition of the SD card. kernel_2712.img is the
# aarch64 kernel relinked at 0x80000 (kernel/linker/starkernel-native-rpi5.ld)
# and flattened to a raw binary.
#
# The DTB is the Raspberry Pi firmware's own stock file, not built here. It
# is fetched once from the pinned firmware release below into build/cache/
# unless RPI5_DTB points at a local copy.
BOARD_DESC := Raspberry Pi 5 (BCM2712, Cortex-A76, native firmware boot)
BOARD_ARCH := aarch64
BOARD_BOOT := rpi-native
BOARD_IMAGE := lithos-raspi.img
RPI_FIRMWARE_TAG ?= 1.20260915
RPI5_DTB_URL ?= https://raw.githubusercontent.com/raspberrypi/firmware/$(RPI_FIRMWARE_TAG)/boot/bcm2712-rpi-5-b.dtb
RPI5_DTB ?= build/cache/raspi-$(RPI_FIRMWARE_TAG)/bcm2712-rpi-5-b.dtb
@@ -12,6 +12,13 @@
# firmware picks up. # firmware picks up.
kernel=kernel_2712.img kernel=kernel_2712.img
# Pin the load address to the one the image is linked at
# (kernel/linker/starkernel-native-rpi5.ld). Pi 5 firmware's own default
# for kernel_2712.img is 0x200000, not the classic 0x80000 -- leaving it
# implicit would load a 0x80000-linked flat image 1.5 MiB away from where
# every absolute address in it points.
kernel_address=0x80000
# Disable the firmware's Linux-compatible-image sanity check. Without # Disable the firmware's Linux-compatible-image sanity check. Without
# this, official docs describe it as checking for "a compatible Device # this, official docs describe it as checking for "a compatible Device
# Tree file before attempting to boot" and warn that "older non-compatible # Tree file before attempting to boot" and warn that "older non-compatible
+14
View File
@@ -0,0 +1,14 @@
# Beelink SER5 boot media
`make boot_image TARGET=SER5` builds `build/boards/ser5/lithos-ser5.img`: a GPT disk with one
FAT32 EFI System Partition. Write it to a USB stick with `dd`. The partition holds:
- `EFI/BOOT/BOOTX64.EFI`: the amd64 monolithic loader, with the whole kernel embedded. Firmware
finds it through the UEFI removable-media path, so no boot entry has to be created.
- `startup.nsh`: runs the loader if the firmware drops into the UEFI shell.
- `starforth.cfg`: only present when `KERNEL_ARGS="..."` is given.
Nothing in the image is SER5-specific. It follows the generic UEFI/ACPI path in FABRIC-3.md §III.
Status: booted in QEMU (q35 + OVMF, from this image as its own disk) through POST, with Stadium
conservation exact (sum 65536 = `Q48_ONE`). Not yet booted on the SER5 itself.
+10
View File
@@ -0,0 +1,10 @@
# boards/ser5/board.mk -- Beelink SER5 (AMD Ryzen, x86-64, UEFI/ACPI).
#
# Generic standards-compliant UEFI path (FABRIC-3.md §III): nothing in the
# image is SER5-specific. The monolithic loader embeds the whole kernel, so
# the image is a GPT disk with one FAT32 EFI System Partition holding
# EFI/BOOT/BOOTX64.EFI. Write it to a USB stick with dd.
BOARD_DESC := Beelink SER5 (AMD Ryzen, x86-64, UEFI)
BOARD_ARCH := amd64
BOARD_BOOT := uefi-esp
BOARD_IMAGE := lithos-ser5.img
+17
View File
@@ -0,0 +1,17 @@
# Xilinx Zynq-7020 boot media
The Zynq-7020's processing system is a dual Cortex-A9: ARMv7-A, 32-bit. It is the host for the
StarForth v4 mesh (`docs/v4.0.0/JUSTIFICATION.md` §5, §8).
Boot chain: BootROM, then `BOOT.BIN` (U-Boot SPL with the board's `ps7_init` DDR and clock setup),
then U-Boot, then LithosAnanke. Everything is read from the SD card's FAT partition.
Status: no image yet. `make boot_image TARGET=ZYNQ7020` stops with an error, because there is no
ARMv7 kernel port (`kernel/src/arch/armv7`: entry code, MMU, GIC, private timer). A trial
compile for Cortex-A9 built 147 of the 151 kernel and engine sources. The four that failed use
`__int128` or have no ARMv7 branch: `kernel/src/crypto/fe25519.c`,
`kernel/src/crypto/scalar25519.c`, `kernel/src/hal/hal.c` and
`v3/src/word_source/mixed_arithmetic_words.c`.
`BOOT.BIN` depends on the exact board (Zybo Z7-20, PYNQ-Z2, Arty Z7-20, ZedBoard, ...), because
`ps7_init` holds that board's DDR timing. The board has not been chosen yet.
+11
View File
@@ -0,0 +1,11 @@
# boards/zynq7020/board.mk -- Xilinx Zynq-7020 (dual Cortex-A9, ARMv7-A, 32-bit).
#
# Boot chain: BootROM -> BOOT.BIN (U-Boot SPL with the board's ps7_init DDR/
# clock setup) -> U-Boot -> LithosAnanke, all from the SD card's FAT
# partition. Needs the ARMv7 kernel port (kernel/src/arch/armv7), which is
# in progress: until it exists, boot_image stops with an explicit error
# rather than producing an image that cannot run.
BOARD_DESC := Xilinx Zynq-7020 (Cortex-A9, ARMv7-A, BOOT.BIN) -- ARMv7 port in progress
BOARD_ARCH := armv7
BOARD_BOOT := zynq-bootbin
BOARD_IMAGE := lithos-zynq7020.img
-12
View File
@@ -1,12 +0,0 @@
# Raspberry Pi 5 native boot media
What goes on the SD card for the native (non-UEFI) boot path (FABRIC-3.md §IV):
- `config.txt` — checked in here, done (§IV.3 item 6).
- `bcm2712-rpi-5-b.dtb` — Raspberry Pi firmware's own stock DTB; not built by this
project, copied from the firmware release the card is otherwise built from.
- `kernel_2712.img` — **does not exist yet.** `config.txt` names it, but no build target
in `Makefile.starkernel` currently emits a raw image by this name at load address
0x80000 — item 1 (entry stub) explicitly scoped a separate-image build target as future
work, not part of that item. Building this file is the remaining prerequisite before
item 7 (assembling the card) is possible.
+42 -40
View File
@@ -1,5 +1,5 @@
# Capsule Block Manifest — Auto-generated # Capsule Block Manifest — Auto-generated
<!-- Generated by mkcapsule --manifest 2026-09-22T22:29:26Z --> <!-- Generated by mkcapsule --manifest 2026-10-01T19:21:21Z -->
<!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. --> <!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. -->
<!-- Hand-written justifications and immutability notes live --> <!-- Hand-written justifications and immutability notes live -->
<!-- in MANIFEST.md alongside this auto-generated index. --> <!-- in MANIFEST.md alongside this auto-generated index. -->
@@ -8,42 +8,44 @@
| Capsule | Blocks claimed | xxHash64 | Signed | | Capsule | Blocks claimed | xxHash64 | Signed |
|---------|----------------|----------|--------| |---------|----------------|----------|--------|
| `ACL.4th` | 4000, 4001, 4002, 4003, 4004, 4005, 4006, 4007, 4008, 4015 | `0xf8890c05c0d8f921` | yes | | `ACL.4th` | 4000, 4001, 4002, 4003, 4004, 4005, 4006, 4007, 4008, 4015 | `0xf8890c05c0d8f921` | n/a |
| `acl-std79.4th` | 4023, 4024, 4025, 4026, 4027, 4028, 4029, 4030, 4031, 4032, 4033, 4034, 4035, 4036, 4037, 4038, 4039, 4040, 4041, 4042, 4043, 4044, 4045, 4046, 4047, 4048 | `0x773bf9209df191d1` | yes | | `acl-std79.4th` | 4023, 4024, 4025, 4026, 4027, 4028, 4029, 4030, 4031, 4032, 4033, 4034, 4035, 4036, 4037, 4038, 4039, 4040, 4041, 4042, 4043, 4044, 4045, 4046, 4047, 4048 | `0x773bf9209df191d1` | n/a |
| `artemis:init.4th` | 4110, 4111, 4112, 4113, 4122, 4123, 4124, 4125, 4126, 4127, 4128, 4129, 4130, 4131, 4132, 4133, 4134, 4135, 4136, 4137, 4138, 4139, 4140, 4141, 4160, 4161, 4162, 4163, 4164, 4165, 4166, 4167, 4168, 4169, 4170, 4171, 4172, 4173, 4174, 4177, 4178, 4179, 4180, 4181, 4182, 4851, 4852, 4853, 4854, 4856, 4857, 4858, 4860 | `0xe6fba9ae56e1c916` | yes | | `artemis:init.4th` | 4110, 4111, 4112, 4113, 4122, 4123, 4124, 4125, 4126, 4127, 4128, 4129, 4130, 4131, 4132, 4133, 4134, 4135, 4136, 4137, 4138, 4139, 4140, 4141, 4160, 4161, 4162, 4163, 4164, 4165, 4166, 4167, 4168, 4169, 4170, 4171, 4172, 4173, 4174, 4177, 4178, 4179, 4180, 4181, 4182, 4851, 4852, 4853, 4854, 4856, 4857, 4858, 4860 | `0xe6fba9ae56e1c916` | n/a |
| `block-acl.4th` | 4019, 4020 | `0xf6cc2a59e3a6734e` | yes | | `block-acl.4th` | 4019, 4020 | `0xf6cc2a59e3a6734e` | n/a |
| `doe-campaign.4th` | 4060, 4061, 4062, 4063, 4064, 4065 | `0x26fb485e5c9dc6ff` | yes | | `doe-campaign.4th` | 4060, 4061, 4062, 4063, 4064, 4065 | `0x26fb485e5c9dc6ff` | n/a |
| `doe.4th` | 2100, 2101, 2102, 2103, 2104, 2105, 2106, 2107 | `0xf154616d248e861f` | yes | | `doe.4th` | 2100, 2101, 2102, 2103, 2104, 2105, 2106, 2107 | `0xf154616d248e861f` | n/a |
| `fabric.4th` | 4900, 4901, 4902, 4903, 4904, 4905, 4906, 4907, 4908, 4909, 4910, 4911, 4912, 4913, 4914, 4915, 4916, 4917, 4918, 4919, 4920, 4921, 4922, 4923, 4924, 5000, 5001, 5002 | `0x9d9489cbeca4099b` | yes | | `fabric.4th` | 4900, 4901, 4902, 4903, 4904, 4905, 4906, 4907, 4908, 4909, 4910, 4911, 4912, 4913, 4914, 4915, 4916, 4917, 4918, 4919, 4920, 4921, 4922, 4923, 4924, 5000, 5001, 5002 | `0x9d9489cbeca4099b` | n/a |
| `font.4th` | 4925, 4926, 4927, 4928, 4929, 4930, 4931, 4932, 4933, 4934, 4935, 4936, 4937, 4938, 4939, 4940, 4941, 4942, 4943, 4944, 4945, 4946, 4947, 4948, 4949, 4950, 4951, 4952, 4953, 4954, 4955, 4956, 4957, 4958, 4959, 4960, 4961, 4962, 4963, 4964, 4965, 4966, 4967, 4968, 4969, 4970, 4971, 4972, 4973, 4974, 4975, 4976, 4977, 4978, 4979, 4980, 4981, 4982, 4983, 4984, 4985 | `0x3f305911500c78f6` | yes | | `font.4th` | 4925, 4926, 4927, 4928, 4929, 4930, 4931, 4932, 4933, 4934, 4935, 4936, 4937, 4938, 4939, 4940, 4941, 4942, 4943, 4944, 4945, 4946, 4947, 4948, 4949, 4950, 4951, 4952, 4953, 4954, 4955, 4956, 4957, 4958, 4959, 4960, 4961, 4962, 4963, 4964, 4965, 4966, 4967, 4968, 4969, 4970, 4971, 4972, 4973, 4974, 4975, 4976, 4977, 4978, 4979, 4980, 4981, 4982, 4983, 4984, 4985 | `0x3f305911500c78f6` | n/a |
| `hestia:init.4th` | 4986, 4987, 4988 | `0x64e111990fbc45ff` | yes | | `hestia:init.4th` | 4986, 4987, 4988 | `0x64e111990fbc45ff` | n/a |
| `init-l8-diverse.4th` | 4820, 4821, 4822 | `0xaa293201a6c91838` | yes | | `init-l8-diverse.4th` | 4820, 4821, 4822 | `0xaa293201a6c91838` | n/a |
| `init-l8-omni.4th` | 2064, 2065, 2066, 2067, 2068, 2069, 2070, 2071, 2072, 2073, 2074, 2075, 2076, 2077, 2078, 2079 | `0x5979e314d6452045` | yes | | `init-l8-omni.4th` | 2064, 2065, 2066, 2067, 2068, 2069, 2070, 2071, 2072, 2073, 2074, 2075, 2076, 2077, 2078, 2079 | `0x5979e314d6452045` | n/a |
| `init-l8-stable.4th` | 4806 | `0xdc3830f189063a9a` | yes | | `init-l8-stable.4th` | 4806 | `0xdc3830f189063a9a` | n/a |
| `init-l8-temporal.4th` | 4830, 4831 | `0x51abd4c138246651` | yes | | `init-l8-temporal.4th` | 4830, 4831 | `0x51abd4c138246651` | n/a |
| `init-l8-transition.4th` | 4840, 4841, 4842 | `0xbcc1a81976f0a4c9` | yes | | `init-l8-transition.4th` | 4840, 4841, 4842 | `0xbcc1a81976f0a4c9` | n/a |
| `init-l8-volatile.4th` | 4810, 4811, 4812, 4813 | `0x98caabbbd92abac4` | yes | | `init-l8-volatile.4th` | 4810, 4811, 4812, 4813 | `0x98caabbbd92abac4` | n/a |
| `init.4th` | 2049, 2050, 2057 | `0xea038ba684c53443` | yes | | `init.4th` | 2049, 2050, 2057 | `0xea038ba684c53443` | n/a |
| `lib.4th` | 4050 | `0x4b216635c359ef73` | yes | | `lib.4th` | 4050 | `0x4b216635c359ef73` | n/a |
| `multiuser-doe.4th` | 5044, 5045, 5046, 5047, 5048, 5049, 5050, 5051, 5052, 5053, 5054, 5055 | `0x22140588ee7c39e6` | yes | | `multiuser-doe.4th` | 5044, 5045, 5046, 5047, 5048, 5049, 5050, 5051, 5052, 5053, 5054, 5055 | `0x22140588ee7c39e6` | n/a |
| `sdk.4th` | 5109, 5110, 5111, 5112, 5113, 5114, 5115 | `0x008fdbbb62c94a3a` | yes | | `sdk.4th` | 5109, 5110, 5111, 5112, 5113, 5114, 5115 | `0x008fdbbb62c94a3a` | n/a |
| `turtle.4th` | 5100, 5101, 5102, 5103, 5104, 5105, 5106, 5107, 5108 | `0x4d470418ca543365` | yes | | `turtle.4th` | 5100, 5101, 5102, 5103, 5104, 5105, 5106, 5107, 5108 | `0x4d470418ca543365` | n/a |
| `user-font-demo.4th` | 4200, 4201, 4202 | `0xce1fd7d1b581a56d` | yes | | `user-font-demo.4th` | 4200, 4201, 4202 | `0xce1fd7d1b581a56d` | n/a |
| `workload-0.4th` | 2200, 2201 | `0x93f86f60aeba8feb` | yes | | `workload-0.4th` | 2200, 2201 | `0x93f86f60aeba8feb` | n/a |
| `workload-1-lite.4th` | 5058, 5059 | `0x44a7a7e3176dcc8d` | yes | | `workload-1-lite.4th` | 5058, 5059 | `0x44a7a7e3176dcc8d` | n/a |
| `workload-1.4th` | 4406, 4415, 4425, 4435 | `0x63e251adb0a03613` | yes | | `workload-1.4th` | 4406, 4415, 4425, 4435 | `0x63e251adb0a03613` | n/a |
| `workload-2.4th` | 4506, 4515, 4525, 4535, 4545 | `0xf113b3d0bcccae47` | yes | | `workload-2.4th` | 4506, 4515, 4525, 4535, 4545 | `0xf113b3d0bcccae47` | n/a |
| `workload-3.4th` | 4606, 4615, 4625, 4635, 4645, 4655, 4665 | `0x62b7a71576ad1041` | yes | | `workload-3.4th` | 4606, 4615, 4625, 4635, 4645, 4655, 4665 | `0x62b7a71576ad1041` | n/a |
| `workload-4.4th` | 2130, 2131, 2132 | `0x099619264e650b1c` | yes | | `workload-4.4th` | 2130, 2131, 2132 | `0x099619264e650b1c` | n/a |
| `workload-5-lite.4th` | 5056, 5057 | `0xea0303f38824f254` | yes | | `workload-5-lite.4th` | 5056, 5057 | `0xea0303f38824f254` | n/a |
| `workload-5.4th` | *(none — raw code capsule)* | `0x526964c7c9506a11` | yes | | `workload-5.4th` | *(none — raw code capsule)* | `0x526964c7c9506a11` | n/a |
| `workload-6.4th` | 2080, 2081, 2082, 2083, 2084, 2085, 2086, 2087, 2088, 2089, 2090, 2091, 2092, 2093, 2094, 2095 | `0x06fc0ce1e369ef5a` | yes | | `workload-6.4th` | 2080, 2081, 2082, 2083, 2084, 2085, 2086, 2087, 2088, 2089, 2090, 2091, 2092, 2093, 2094, 2095 | `0x06fc0ce1e369ef5a` | n/a |
| `workload-7.4th` | 2150 | `0x02862291387eb7ac` | yes | | `workload-7.4th` | 2150 | `0x02862291387eb7ac` | n/a |
| `workload-8.4th` | 2160 | `0x56b7f2f0efa000df` | yes | | `workload-8.4th` | 2160 | `0x56b7f2f0efa000df` | n/a |
| `workload-9.4th` | 4706, 4715, 4725, 4735, 4745 | `0x3f2bec73142aa424` | yes | | `workload-9.4th` | 4706, 4715, 4725, 4735, 4745 | `0x3f2bec73142aa424` | n/a |
| `workload-calib1.4th` | 5043 | `0x3b9f2d17b554fabc` | yes | | `workload-calib1.4th` | 5043 | `0x3b9f2d17b554fabc` | n/a |
| `zuse-eligibility.4th` | 4021, 4022 | `0x7b28f4776a32e0b7` | yes | | `zuse-eligibility.4th` | 4021, 4022 | `0x7b28f4776a32e0b7` | n/a |
| `zuse.4th` | 4016, 4017, 4018 | `0x490ded9be257a90b` | yes | | `zuse.4th` | 4016, 4017, 4018 | `0xa14d5a7a88791cf6` | n/a |
*Signed column is `n/a`: this manifest run had no `--sign-key`. Re-run with `--sign-key <path>` to check signing status (does not modify or require rebuilding capsule_generated.c).*
## Block Map (sorted by LBN) ## Block Map (sorted by LBN)
@@ -109,9 +111,9 @@
| 4007 | `ACL.4th` | `0xf8890c05c0d8f921` | ok | | 4007 | `ACL.4th` | `0xf8890c05c0d8f921` | ok |
| 4008 | `ACL.4th` | `0xf8890c05c0d8f921` | ok | | 4008 | `ACL.4th` | `0xf8890c05c0d8f921` | ok |
| 4015 | `ACL.4th` | `0xf8890c05c0d8f921` | ok | | 4015 | `ACL.4th` | `0xf8890c05c0d8f921` | ok |
| 4016 | `zuse.4th` | `0x490ded9be257a90b` | ok | | 4016 | `zuse.4th` | `0xa14d5a7a88791cf6` | ok |
| 4017 | `zuse.4th` | `0x490ded9be257a90b` | ok | | 4017 | `zuse.4th` | `0xa14d5a7a88791cf6` | ok |
| 4018 | `zuse.4th` | `0x490ded9be257a90b` | ok | | 4018 | `zuse.4th` | `0xa14d5a7a88791cf6` | ok |
| 4019 | `block-acl.4th` | `0xf6cc2a59e3a6734e` | ok | | 4019 | `block-acl.4th` | `0xf6cc2a59e3a6734e` | ok |
| 4020 | `block-acl.4th` | `0xf6cc2a59e3a6734e` | ok | | 4020 | `block-acl.4th` | `0xf6cc2a59e3a6734e` | ok |
| 4021 | `zuse-eligibility.4th` | `0x7b28f4776a32e0b7` | ok | | 4021 | `zuse-eligibility.4th` | `0x7b28f4776a32e0b7` | ok |
+1 -1
View File
@@ -1,7 +1,7 @@
# configs/ # configs/
Example Kconfig `defconfig` files — starting points for `make -f Example Kconfig `defconfig` files — starting points for `make -f
Makefile.starkernel ARCH=<arch> defconfig` (kernel) or the equivalent kernel/Makefile ARCH=<arch> defconfig` (kernel) or the equivalent
hosted target, matching the current committed default build behavior for hosted target, matching the current committed default build behavior for
each profile. Loaded via `tools/kconfig/conf`. each profile. Loaded via `tools/kconfig/conf`.
View File
View File
+112
View File
@@ -0,0 +1,112 @@
# docs/book/Makefile -- the single LithosAnanke book, built from LaTeX.
#
# Run from the repo root (the root Makefile does this):
# make docs -> build/docs/LithosAnanke.pdf
# make docs TARGET=<board> -> build/docs/LithosAnanke-<board>.pdf
# (same book + that board's appendix)
#
# docs/book/main.tex is the master. Markdown sources are converted by pandoc
# into LaTeX fragments under build/docs/gen/ and \input from main.tex; the
# Markdown stays the source of truth until a chapter is rewritten in LaTeX.
# Figures and tables that present data read the CSV directly at LaTeX time
# (pgfplots / pgfplotstable) and cite it with \datasource{path}; see
# docs/book/README.md.
BOOK_DIR := docs/book
OUT := build/docs
GEN := $(OUT)/gen
BOARD ?=
BOARD_NAME ?=
VARIANT := $(if $(BOARD),$(BOARD),book)
VAR_DIR := $(OUT)/$(VARIANT)
PDF := $(OUT)/LithosAnanke$(if $(BOARD),-$(BOARD)).pdf
PANDOC ?= pandoc
LATEXMK ?= latexmk
PANDOC_FILTERS := $(BOOK_DIR)/pandoc/table-widths.lua $(BOOK_DIR)/pandoc/code-breaks.lua
PANDOC_FLAGS := -f gfm -t latex --top-level-division=chapter --wrap=preserve \
$(foreach f,$(PANDOC_FILTERS),--lua-filter=$(f))
# fragment name : Markdown source. The order of \input lines is main.tex's.
CHAPTERS := \
ontology:docs/ONTOLOGY.md \
roadmap:docs/ROADMAP.md \
boards:boards/README.md \
justification:docs/v4.0.0/JUSTIFICATION.md \
decomposition:docs/v4.0.0/DECOMPOSITION.md \
fabric-0:docs/fabric/FABRIC-0.md \
fabric-1:docs/fabric/FABRIC-1.md \
fabric-2:docs/fabric/FABRIC-2.md \
fabric-3:docs/fabric/FABRIC-3.md \
fabric-3-5:docs/fabric/FABRIC-3.5.md \
fabric-3-6:docs/fabric/FABRIC-3.6.md \
fabric-3-7:docs/fabric/FABRIC-3.7.md \
fabric-4:docs/fabric/FABRIC-4.md
ifneq ($(BOARD),)
ifeq ($(wildcard boards/$(BOARD)/README.md),)
$(error boards/$(BOARD)/README.md is missing: it is the board's appendix)
endif
CHAPTERS += board-$(BOARD):boards/$(BOARD)/README.md
endif
chapter_name = $(word 1,$(subst :, ,$(1)))
chapter_src = $(word 2,$(subst :, ,$(1)))
FRAGMENTS := $(foreach c,$(CHAPTERS),$(GEN)/$(call chapter_name,$(c)).tex)
.PHONY: all tools FORCE
all: $(PDF)
tools:
@missing=""; \
for t in $(PANDOC) $(LATEXMK) xelatex; do command -v $$t >/dev/null 2>&1 || missing="$$missing $$t"; done; \
if [ -n "$$missing" ]; then \
echo "Error: make docs needs:$$missing"; \
echo " sudo apt-get install -y pandoc latexmk texlive-xetex texlive-latex-extra texlive-pictures texlive-fonts-recommended fonts-dejavu fonts-dejavu-extra"; \
echo " (or a user-local TinyTeX + pandoc in ~/.local; see docs/book/README.md)"; \
exit 1; \
fi
# --id-prefix keeps heading labels unique across documents that reuse
# section names ("Summary", "Open questions", ...).
define chapter_rule
$(GEN)/$(call chapter_name,$(1)).tex: $(call chapter_src,$(1)) $(PANDOC_FILTERS) | tools
@mkdir -p $(GEN)
@echo " PANDOC $$< -> $$@"
@$(PANDOC) $(PANDOC_FLAGS) --id-prefix=$(call chapter_name,$(1))- $$< -o $$@
endef
$(foreach c,$(CHAPTERS),$(eval $(call chapter_rule,$(c))))
# Pandoc's syntax-highlighting macros, taken from the installed pandoc so the
# fragments and their macros always come from the same version.
$(GEN)/pandoc-highlighting.tex: $(BOOK_DIR)/pandoc/highlighting.latex | tools
@mkdir -p $(GEN)
@printf '```c\nx\n```\n' | $(PANDOC) -f gfm -t latex -s --template=$< -o $@
# Per-build facts the book prints: the commit every \datasource refers to,
# and which board appendix (if any) is included.
$(VAR_DIR)/meta.tex: FORCE
@mkdir -p $(VAR_DIR)
@{ \
c=$$(git rev-parse --short=12 HEAD 2>/dev/null || echo unknown); \
git diff --quiet HEAD -- 2>/dev/null || c="$$c (+ uncommitted changes)"; \
printf '\\newcommand{\\bookcommit}{%s}\n' "$$c"; \
printf '\\newcommand{\\bookdate}{%s}\n' "$$(date -u +%Y-%m-%d)"; \
printf '\\def\\bookboard{%s}\n' "$(BOARD_NAME)"; \
$(if $(BOARD),printf '\\newcommand{\\bookboardappendix}{board-%s}\n' "$(BOARD)";) \
} > $@.tmp
@cmp -s $@.tmp $@ && rm -f $@.tmp || mv $@.tmp $@
FORCE:
TEXINPUTS_BOOK := $(abspath $(VAR_DIR)):$(abspath $(GEN)):$(abspath $(BOOK_DIR)):
$(PDF): $(BOOK_DIR)/main.tex $(FRAGMENTS) $(GEN)/pandoc-highlighting.tex $(VAR_DIR)/meta.tex | tools
@echo " LATEXMK $(BOOK_DIR)/main.tex -> $@"
@TEXINPUTS=$(TEXINPUTS_BOOK) $(LATEXMK) -xelatex -interaction=nonstopmode -halt-on-error \
-file-line-error -outdir=$(VAR_DIR) $(BOOK_DIR)/main.tex > $(VAR_DIR)/latexmk.log 2>&1 || { \
grep -A4 -E '^(.*:[0-9]+:|!)' $(VAR_DIR)/main.log | head -40; \
echo "Error: LaTeX failed; full log: $(VAR_DIR)/main.log"; exit 1; }
@cp $(VAR_DIR)/main.pdf $@
@echo " PDF $@"
+66
View File
@@ -0,0 +1,66 @@
# docs/book/
`make docs` builds one PDF, `build/docs/LithosAnanke.pdf`, from `main.tex` with xelatex.
`make docs TARGET=<board>` builds `build/docs/LithosAnanke-<board>.pdf`: the same book with
`boards/<board>/README.md` added as an appendix.
Tools: `sudo apt-get install -y pandoc latexmk texlive-xetex texlive-latex-extra texlive-pictures texlive-fonts-recommended fonts-dejavu fonts-dejavu-extra`
Without root, a user-local TeX Live works too (this is how the book was first built):
TinyTeX (`curl -sL https://yihui.org/tinytex/install-bin-unix.sh | sh`) plus
`tlmgr install latexmk xetex fontspec pgf pgfplots booktabs multirow fancyvrb fvextra lineno upquote ulem enumitem newunicodechar bookmark hyperref geometry xcolor graphics tools etoolbox fancyhdr truncate amsfonts`,
and the pandoc release tarball unpacked into `~/.local`.
The installed DejaVu decides italics: `fonts-dejavu-core` alone has no serif italic, so
`main.tex` falls back to a slanted upright face; `fonts-dejavu-extra` gives real italics.
## How it fits together
- `main.tex` is the master file. It sets the parts and the chapter order.
- Chapters that are still Markdown are listed in `Makefile` (`CHAPTERS`, as `name:source.md`).
At build time pandoc converts each one into `build/docs/gen/<name>.tex`, and `main.tex`
includes it with `\input{<name>}`. The Markdown stays the source until the chapter is
rewritten in LaTeX. At that point the `.tex` moves into this directory and the `CHAPTERS`
entry is removed.
- `pandoc/highlighting.latex` extracts the code-highlighting macros from the installed pandoc,
so the macros and the fragments always come from the same pandoc version.
- Two Lua filters run on every chapter. `pandoc/table-widths.lua` gives wide tables
proportional wrapping columns, because pandoc's gfm reader leaves column widths unset.
`pandoc/code-breaks.lua` lets long inline identifiers and paths break after `_ / . - :`.
Code blocks wrap through fvextra (`breaklines`).
- `build/docs/<book|board>/meta.tex` is written on every build. It records the commit (and
whether there were uncommitted changes), the date, and the board.
## Rule for data
Any figure or table that shows measured numbers is generated from the CSV when the book is
built. Numbers are never typed in by hand:
```latex
\begin{tikzpicture}
\begin{axis}[xlabel=run, ylabel=K]
\addplot table[col sep=comma, x=run, y=K]{experiments/<campaign>/results.csv};
\end{axis}
\end{tikzpicture}
\datasource{experiments/<campaign>/results.csv}
```
Use `\pgfplotstabletypeset[col sep=comma]{...}` for tables. `\datasource` prints the CSV path
and the commit, so a reader can find the exact file the figure was drawn from. CSV paths are
repo-relative, because xelatex runs from the repo root.
## Older pipelines to fold in or retire
These still exist and still have their own targets. Each one needs a decision during the
curation pass: move it into this book, or retire it.
| Source | Current target | Produces |
|---|---|---|
| `docs/formal/vol1-vm-physics`, `vol2-kernel`, `vol3-research` | `make -C docs/formal vols` | three volume PDFs |
| `docs/formal/dev-guide`, `user-guide`, `cookbook` | `make -C docs/formal books` | three practitioner PDFs |
| `docs/formal/experiments`, `proofs`, `ssrn`, `patent` | `make -C docs/formal standalone` | four standalone PDFs |
| Doxygen (`Doxyfile`) | `make -C docs/formal doxygen` | API reference PDF |
| `scripts/generate-doxygen-appendix.sh` | `make -f v3/Makefile api-docs` | AsciiDoc API appendix |
| `docs/src/internal/formal/*.thy` | `make -f v3/Makefile docs-isabelle` | Isabelle report |
| `scripts/asciidoc-to-latex.sh` | `make -f v3/Makefile docs-latex` | `docs/latex/` |
| `docs/SSRN_companion/Math_Companion_SSRN.tex` | `make -f v3/Makefile math-companion` | SSRN math companion |
+161
View File
@@ -0,0 +1,161 @@
% docs/book/main.tex -- master file of the single LithosAnanke book.
%
% Built by `make docs [TARGET=<board>]` (docs/book/Makefile) with xelatex.
% Fragments named below (ontology, fabric-0, ...) are generated by pandoc
% from the Markdown listed in docs/book/Makefile's CHAPTERS into
% build/docs/gen/; meta.tex is generated per build. Neither is committed.
\documentclass[11pt,openany]{book}
\usepackage{amsmath,amssymb}
\usepackage{fontspec}
% fonts-dejavu-core has no serif/sans italics (fonts-dejavu-extra does); when a
% shape is missing, slant the upright one rather than silently drop emphasis.
\setmainfont{DejaVu Serif}[AutoFakeSlant=0.2]
\setsansfont{DejaVu Sans}[AutoFakeSlant=0.2]
\setmonofont{DejaVu Sans Mono}[Scale=0.85]
\newfontfamily\symbolfont{DejaVu Sans}
\usepackage[letterpaper,margin=1in]{geometry}
\usepackage{xcolor}
\usepackage{graphicx}
\usepackage{longtable,booktabs,array,calc,multirow}
\usepackage{fancyvrb}
\usepackage[normalem]{ulem}
\usepackage{enumitem}
\usepackage{newunicodechar}
\usepackage{pgfplots}
\usepackage{pgfplotstable}
\pgfplotsset{compat=1.18}
\usepackage[hidelinks]{hyperref}
\usepackage{bookmark}
% --- what pandoc's LaTeX fragments expect (normally from its own template)
\providecommand{\tightlist}{\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\providecommand{\pandocbounded}[1]{#1}
\providecommand{\st}[1]{\sout{#1}}
\newcounter{none} % pandoc: {\def\LTcaptype{none} ...} marks unnumbered tables
\usepackage{etoolbox}
\makeatletter
\def\fnum@table{\tablename~\thetable}
\patchcmd\longtable{\par}{\if@noskipsec\mbox{}\fi\par}{}{}
\makeatother
\usepackage{fvextra}
\input{pandoc-highlighting}
% Code and diagrams are wider than the page in places: wrap, never overflow.
\RecustomVerbatimEnvironment{Highlighting}{Verbatim}{commandchars=\\\{\},breaklines,breakanywhere,fontsize=\small}
\RecustomVerbatimEnvironment{verbatim}{Verbatim}{breaklines,breakanywhere,fontsize=\small}
\setlistdepth{9}
\renewlist{itemize}{itemize}{9}
\setlist[itemize]{label=\textbullet}
\renewlist{enumerate}{enumerate}{9}
\setlist[enumerate]{label=\arabic*.}
% Running heads: chapter on the left page, section on the right, both cut to
% the page width (several design-record titles are a full sentence long).
\usepackage{fancyhdr}
\usepackage[fit]{truncate}
\pagestyle{fancy}
\fancyhf{}
\renewcommand{\chaptermark}[1]{\markboth{#1}{}}
\renewcommand{\sectionmark}[1]{\markright{#1}}
\fancyhead[LE]{\small\truncate{\dimexpr\headwidth-3em}{\leftmark}}
\fancyhead[RO]{\small\truncate{\dimexpr\headwidth-3em}{\rightmark}}
\fancyhead[RE,LO]{\small\thepage}
\renewcommand{\headrulewidth}{0.4pt}
\setlength{\headheight}{14pt}
\fancypagestyle{plain}{\fancyhf{}\fancyfoot[C]{\small\thepage}\renewcommand{\headrulewidth}{0pt}}
\setlength{\emergencystretch}{3em}
\setlength{\parindent}{0pt}
\setlength{\parskip}{0.5em}
% --- glyphs DejaVu Serif lacks: the status marks used across the docs
\newunicodechar{✅}{{\symbolfont ✔}}
\newunicodechar{✓}{{\symbolfont ✓}}
\newunicodechar{❌}{{\symbolfont ✘}}
\newunicodechar{✗}{{\symbolfont ✗}}
\newunicodechar{⬜}{{\symbolfont ☐}}
\newunicodechar{⭐}{{\symbolfont ★}}
\newunicodechar{🔶}{{\symbolfont ◆}}
\newunicodechar{⚠}{{\symbolfont ⚠}}
\newunicodechar{📋}{}
\newunicodechar{🐛}{[bug]}
\newunicodechar{🎯}{[goal]}
\newunicodechar{🟡}{{\symbolfont ●}}
\newunicodechar{📍}{{\symbolfont ▸}}
\newunicodechar{🔓}{[unlocked]}
\newunicodechar{❓}{?}
\newunicodechar{⟺}{\ensuremath{\Longleftrightarrow}}
\newunicodechar{⋯}{\ensuremath{\cdots}}
\newunicodechar{^^^^fe0f}{}
% --- the documents number their own sections (§III.1, D-3, ...)
\setcounter{secnumdepth}{0}
\setcounter{tocdepth}{1}
\input{meta}
% \datasource{path/to/data.csv}: cite the data behind a figure or table.
% Every figure or table of measured numbers reads its CSV at build time
% (\addplot table / \pgfplotstabletypeset) and is followed by this line, so
% the reader can find the exact file at the exact commit.
\newcommand{\datasource}[1]{%
\par{\small Data: \texttt{\detokenize{#1}} at commit \texttt{\bookcommit}.}\par}
\title{LithosAnanke and StarForth}
\author{}
\date{Built \bookdate{} from commit \texttt{\bookcommit}%
\ifx\bookboard\empty\else\\Board appendix: \bookboard\fi}
\begin{document}
\frontmatter
\maketitle
\tableofcontents
\chapter{About this book}
This book is generated from the repository by \texttt{make docs}. Each
chapter below is still maintained as the Markdown file named in the table and
converted at build time; a chapter moves into LaTeX source when it is
rewritten. Part~III is the design record: those documents are archival and
are reproduced as written, including their struck-through corrections.
\begin{longtable}{@{}ll@{}}
\toprule
Chapter & Source \\
\midrule
\endhead
Ontology & \texttt{docs/ONTOLOGY.md} \\
Roadmap & \texttt{docs/ROADMAP.md} \\
Boot targets & \texttt{boards/README.md} \\
v4 justification & \texttt{docs/v4.0.0/JUSTIFICATION.md} \\
v4 decomposition & \texttt{docs/v4.0.0/DECOMPOSITION.md} \\
FABRIC-0 \dots{} FABRIC-4 & \texttt{docs/fabric/FABRIC-*.md} \\
Board appendix (\texttt{TARGET=}) & \texttt{boards/<board>/README.md} \\
\bottomrule
\end{longtable}
\mainmatter
\part{The system}
\input{ontology}
\input{roadmap}
\input{boards}
\part{StarForth v4}
\input{justification}
\input{decomposition}
\part{Design record (FABRIC series)}
\input{fabric-0}
\input{fabric-1}
\input{fabric-2}
\input{fabric-3}
\input{fabric-3-5}
\input{fabric-3-6}
\input{fabric-3-7}
\input{fabric-4}
\ifdefined\bookboardappendix
\appendix
\input{\bookboardappendix}
\fi
\end{document}
+29
View File
@@ -0,0 +1,29 @@
-- docs/book/pandoc/code-breaks.lua
--
-- Inline code in the design record is full of long identifiers and paths
-- (g_wirebind_attached_username, kernel/src/arch/riscv64/...), which LaTeX
-- cannot break, so they run into the margin. Emit inline code as \texttt
-- ourselves, escaped the same way pandoc does, with a break opportunity
-- after each separator character.
local BREAK_AFTER = { ["_"] = true, ["/"] = true, ["."] = true, ["-"] = true,
[":"] = true, [","] = true, ["("] = true, ["="] = true }
local ESCAPE = {
["\\"] = "\\textbackslash{}", ["{"] = "\\{", ["}"] = "\\}",
["$"] = "\\$", ["&"] = "\\&", ["#"] = "\\#", ["%"] = "\\%", ["_"] = "\\_",
["^"] = "\\textasciicircum{}", ["~"] = "\\textasciitilde{}",
["'"] = "\\textquotesingle{}", ["`"] = "\\textasciigrave{}",
[" "] = "\\ ",
}
function Code(el)
if not FORMAT:match("latex") then return nil end
local out = {}
for _, cp in utf8.codes(el.text) do
local ch = utf8.char(cp)
out[#out + 1] = ESCAPE[ch] or ch
if BREAK_AFTER[ch] then out[#out + 1] = "\\allowbreak{}" end
end
return pandoc.RawInline("latex", "\\texttt{" .. table.concat(out) .. "}")
end
+3
View File
@@ -0,0 +1,3 @@
$if(highlighting-macros)$
$highlighting-macros$
$endif$
+55
View File
@@ -0,0 +1,55 @@
-- docs/book/pandoc/table-widths.lua
--
-- pandoc's gfm reader leaves every column width unset, so the LaTeX writer
-- emits `l` columns and a table with long cells runs off the page. For any
-- table wider than WIDE characters, give each column a width proportional
-- to its longest cell (clamped to [MIN_COL, MAX_COL] characters); the
-- writer then emits wrapping p{} columns that together fill \linewidth.
local WIDE = 72
local MIN_COL = 6
local MAX_COL = 60
local stringify = pandoc.utils.stringify
local function measure(rows, widths)
for _, row in ipairs(rows) do
local col = 1
for _, cell in ipairs(row.cells) do
local span = cell.col_span or 1
local len = utf8.len(stringify(cell.contents)) or #stringify(cell.contents)
local per = len / span
for c = col, col + span - 1 do
if per > (widths[c] or 0) then widths[c] = per end
end
col = col + span
end
end
end
function Table(tbl)
local n = #tbl.colspecs
local widths = {}
for i = 1, n do widths[i] = 0 end
measure(tbl.head.rows, widths)
for _, body in ipairs(tbl.bodies) do
measure(body.head, widths)
measure(body.body, widths)
end
measure(tbl.foot.rows, widths)
local total = 0
for i = 1, n do total = total + widths[i] end
if total <= WIDE then return nil end
local sum = 0
for i = 1, n do
widths[i] = math.max(MIN_COL, math.min(MAX_COL, widths[i]))
sum = sum + widths[i]
end
for i = 1, n do
tbl.colspecs[i] = { tbl.colspecs[i][1], widths[i] / sum }
end
return tbl
end
+151 -67
View File
@@ -18,7 +18,7 @@ model produces the same results as the v3 C primitive it replaces.
0. [Fates](#0-fates) 0. [Fates](#0-fates)
1. [The v4 core ISA](#1-the-v4-core-isa) 1. [The v4 core ISA](#1-the-v4-core-isa)
2. [Compiler conventions](#2-compiler-conventions) 2. [Compiler conventions](#2-compiler-conventions)
3. [Open decisions](#3-open-decisions) 3. [Decisions](#3-decisions)
4. [Foundation layer (new words)](#4-foundation-layer-new-words) 4. [Foundation layer (new words)](#4-foundation-layer-new-words)
5. [Fate of every v3 primitive](#5-fate-of-every-v3-primitive) 5. [Fate of every v3 primitive](#5-fate-of-every-v3-primitive)
6. [Messaging between nodes](#6-messaging-between-nodes) 6. [Messaging between nodes](#6-messaging-between-nodes)
@@ -48,9 +48,9 @@ model produces the same results as the v3 C primitive it replaces.
| Item | v4 node | | Item | v4 node |
| --- | --- | | --- | --- |
| Cell | 32 bits (mesh node). The host node's width is a build parameter; see D-5. | | Cell | 32 bits (mesh node). The host node's width is a build parameter; see D-5. |
| Addressing | Word-addressed (pending D-1). | | Addressing | Word-addressed (D-1). |
| Registers | `T` (top of data stack), `S` (second), `R` (top of return stack), `P` (program counter), `A` and `B` (address registers). | | Registers | `T` (top of data stack), `S` (second), `R` (top of return stack), `P` (program counter), `A` and `B` (address registers). |
| Stacks | Hardware stacks below `S` and `R`. Depth and visibility are D-2. | | Stacks | F18 circular hardware stacks, not visible to code (D-2): data stack `T`, `S` + 8 circular (10 deep), return stack `R` + 8 circular (9 deep). No overflow or underflow; pushing past the bottom silently overwrites the oldest entry. |
| Instruction word | Six 5-bit slots, plus 2 spare bits. | | Instruction word | Six 5-bit slots, plus 2 spare bits. |
### 1.2 Instruction word layout ### 1.2 Instruction word layout
@@ -147,28 +147,39 @@ IF body1 ELSE body2 THEN → if L1 drop body1 jump L2
times, as on the F18. `FOR ... UNEXT` is the same but the body must fit in one instruction word. times, as on the F18. `FOR ... UNEXT` is the same but the body must fit in one instruction word.
**Register conventions.** `A` and `B` are caller-saved. A word that uses them says so. Words in this **Register conventions.** `A` and `B` are caller-saved. A word that uses them says so. Words in this
document that clobber `A`: `@ ! +! -! 2@ 2! C@ C! UM* * UM/MOD SEND RECV`. Words that clobber `B`: document that clobber `A`: `@ ! +! -! 2@ 2! C@ C! UM* * UM/MOD Q.FROM-INT Q.TO-INT Q.* Q./ Q.EXP Q.SQRT Q.LOG Q.SIN Q.COS SEND RECV`. Words that clobber `B`:
`SEND RECV`. `Q./ Q.EXP Q.SQRT Q.LOG Q.SIN Q.COS SEND RECV`.
**Return-stack words** (`>R R> R@ 2>R 2R> 2R@ I J UNLOOP` and the loop runtimes) are always IN. **Return-stack words** (`>R R> R@ 2>R 2R> 2R@ I J UNLOOP` and the loop runtimes) are always IN.
--- ---
## 3. Open decisions ## 3. Decisions
These must be settled before the golden model is built. Where a definition below depends on one, it Ruled by Captain Bob, 2026-10-01, except D-4 and D-6, which are deferred to development step 2 (the
says so. hosted mesh, `JUSTIFICATION.md` §10) because only the mesh and the RTL depend on them. Where a
definition below depends on one, it says so.
| ID | Decision | Default in this document | | ID | Decision | Ruling |
| --- | --- | --- | | --- | --- | --- |
| **D-1** | Word addressing (pure Moore) or byte addressing. | Word addressing. `C@`/`C!` are CAP; `CELLS` is a no-op. | | **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 (needed by `DEPTH`, `PICK`, `ROLL`, `SP@`, `SP!`). | Stacks backed by node RAM, with the data stack pointer exposed as MM register `DSP`. | | **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. | Carry is kept (extended multiply step), so `UM*` returns a full 64-bit product. | | **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. | Symbolic names only (§6, §7). | | **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. | 32 on a Zynq-7000 (Cortex-A9); 64 on an aarch64 host. The compiler capsule is written width-independent. | | **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. | Per-opcode and per-call-target. Transition counters deferred. | | **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. |
| **D-7** | `ROLL` semantics. | Fix to ANS (count from the top). v3's bottom-counting `ROLL` is retired. | | **D-7** | `ROLL` semantics. | **Moot.** `ROLL` is retired under D-2. |
| **D-8** | Q48.16 signedness. | Signed. v3's unsigned comparisons and `Q.FROM-INT` clamping are retired. | | **D-8** | Q48.16 signedness. | **Signed.** v3's unsigned comparisons and `Q.FROM-INT` clamping are retired. |
| **D-9** | Instruction word width on a 64-bit-cell host (ruled 2026-10-02). | **32 bits at every cell width.** Six 5-bit slots plus 2 spare bits, as in §1.2. On a 64-bit host the instruction word is the low 32 bits of the cell and the high half is ignored, so compiled code is identical at both widths. Only data and `@p` literals are a full cell wide. |
| **D-10** | Q48.16 width on a 64-bit-cell node (ruled 2026-10-02). | **Two cells at every cell width.** A Q value is a signed double on 32- and 64-bit nodes alike, so every Q word is the same double word at both widths. At 32-bit cells this is bit-for-bit v3's 64-bit Q. At 64-bit cells the low cell is v3's value, and where v3 wraps on Q48.16 overflow (a sum past Q max, `ABS` or `NEG` of Q min) the high cell carries the true result instead. |
| **D-11** | `Q./` semantics: division by zero, rounding, overflow (ruled 2026-10-02). | **Saturate and flag; round toward zero; saturate on overflow.** The quotient of `a * 2^16 / b` is rounded toward zero, like `SM/REM`. When it does not fit a Q value it is clamped to Q max or Q min by its sign. Division by zero returns Q max or Q min by the sign of the dividend (`0 / 0` gives 0) and sets the node's `NODE-ERROR` register (§7), which `VM-ERROR?` reads. v3 returned 0 on division by zero and saturated whenever the dividend was 2^48 or more, even when the quotient would have fit. |
| **D-12** | Q approximations outside their domain (ruled 2026-10-02). | **Return 0 and set `NODE-ERROR`.** `Q.SQRT` of a negative value and `Q.LOG` of zero or a negative value return 0 and set `NODE-ERROR` (§7), as `Q./` does on division by zero (D-11). v3 returned 0 for `ln(0)` without a flag and read negative arguments as large unsigned values. |
**Consequences of D-2 that every definition must respect.** The data stack holds 10 items and the
return stack 9, and every `call`, `FOR`, `DO` loop frame and `push` uses return-stack slots. Nesting
is therefore shallow, and exceeding either depth corrupts silently rather than faulting. Every CAP
definition in §4 and §5 must be re-checked against these limits before it is accepted as a POST
target; the hand traces so far assumed unbounded stacks.
--- ---
@@ -193,31 +204,91 @@ dependency order.
: U< ( u1 u2 -- flag ) 2DUP xor 0< IF NIP 0< ELSE - 0< THEN ; : U< ( u1 u2 -- flag ) 2DUP xor 0< IF NIP 0< ELSE - 0< THEN ;
\ ---- multiply (D-3) ----------------------------------------------------- \ ---- multiply (D-3) -----------------------------------------------------
: 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 1 and inv 1 + over 2/ and \ u1 u2 t0 t0 = u2 2/ if u1 odd
over a! 31 push \ A: u2 R: loop count (FOR's push, early)
push over 2/ pop \ u1 u2 s t0 s = u1 2/
L: +* unext \ u1 u2 s hi A: lo
push drop pop \ u1 u2 hi
2* a -if L0 drop 1 + jump L1 L0: drop L1: push \ R: 2hi + top bit of lo
over -if L2 drop dup jump L3 L2: drop 0 L3: push \ R: + (u1<0 ? u2 : 0)
dup -if L4 drop over 1 and jump L5 L4: drop 0 L5: \ u2<0 ? u1&1 : 0
pop + pop + push \ u1 u2 R: hi'
and 1 and a 2* + pop ; \ lo' hi'
\ u1 and u2 wait on the data stack under the loop (+* touches only T, S and
\ A), so the corrections are made after it, with -if in place of 0< calls,
\ and the return stack holds at most two temporaries. The loop count is
\ pushed before s is made, so the data stack never holds more than four.
\ Leaves its caller 6 data cells under its arguments and 6 return entries
\ (revised 2026-10-02; the first full-range version parked its three
\ corrections on the return stack and left 4).
\ ---- divide: 32-step restoring division, divisor held in A -------------- \ ---- divide: 32-step restoring division, divisor held in A --------------
\ Each step shifts hi:lo left one bit and, when the shifted-out bit of hi was
\ set or hi' >= d, subtracts d from hi' and sets the new low bit of lo. The
\ unsigned compare is done by sign tests in line (as U< does), and x - d is
\ `inv a + inv`, so the loop body makes no calls: it needs one return-stack
\ entry beyond its own count.
: UM/MOD ( ulo uhi ud -- urem uquot ) : UM/MOD ( ulo uhi ud -- urem uquot )
a! a! 31 FOR
31 FOR -if L0 \ hi's top bit set:
over 0< NEGATE push \ R: lo's top bit (1/0) 2* over -if L1 drop 1 + jump L2 \ hi' = 2hi + top bit of lo
dup 0< push \ R: hi's top bit (-1/0) L1: drop L2: push 2* pop \ lo' = 2lo
2* pop pop SWAP push OR pop \ lo hi' t hi shifted, lo bit brought in jump SUB \ true hi' >= 2^n > d
push SWAP 2* SWAP pop \ lo' hi' t L0:
over a U< 0= OR \ lo' hi' flag t OR hi' >= d 2* over -if L3 drop 1 + jump L4
IF a - SWAP 1 OR SWAP THEN L3: drop L4: push 2* pop
dup a xor -if L5 \ top bits of hi' and d differ:
drop -if NOSUB jump SUB \ hi' >= d iff hi' has it
L5: drop dup inv a + inv -if L6 \ same: hi' >= d iff hi'-d >= 0
drop jump NOSUB
L6: push drop pop jump SETBIT
SUB: inv a + inv \ hi' - d
SETBIT: push 1 + pop \ lo' is even: + 1 sets bit 0
NOSUB:
NEXT NEXT
SWAP ; over push push drop pop pop ; \ SWAP in line
\ Executed on the golden model (2026-10-02): exact, q*d + r = uhi:ulo with
\ r < d, for every uhi < ud at 32- and 64-bit cells. Outside that range
\ (uhi >= ud, including ud = 0) the result is unspecified, as in FORTH-79; it
\ always terminates after 32 steps. Stack use (D-2): up to 6 data cells may
\ lie under the three arguments and up to 6 return-stack entries under its
\ return address. For UM* the same limits are 6 and 6. This replaces a
\ first version built on U<, 0<, SWAP and OR calls, which was also exact but
\ left only 3 and 3 (too few for SM/REM inside /MOD) and stepped about five
\ times as many instruction words.
\ ---- signed division, truncating toward zero (v3 semantics) ------------- \ ---- signed division, truncating toward zero (v3 semantics) -------------
\ The quotient takes the sign of d xor n, the remainder the sign of d. Sign
\ tests are native -if (as in 0<) and NEGATE is in line, so the only calls
\ are DNEGATE and UM/MOD, both call-free inside.
: SM/REM ( d n -- rem quot ) : SM/REM ( d n -- rem quot )
2DUP xor push \ R: quotient sign over over xor push \ R: quotient sign (top bit)
over push \ R: remainder sign (sign of dividend) over push \ R: + remainder sign (top bit of d)
ABS push DABS pop UM/MOD -if L0 inv 1 + L0: push \ R: + |n|
pop 0< IF push NEGATE pop THEN -if L1 DNEGATE L1: \ |d|
pop 0< IF NEGATE THEN ; pop UM/MOD \ urem uquot
pop -if L2 drop push inv 1 + pop jump L3 L2: drop L3:
pop -if L4 drop inv 1 + ; L4: drop ;
\ Executed on the golden model (2026-10-02): exact whenever the truncated
\ quotient fits a signed cell, at 32- and 64-bit cells. Stack use (D-2): up
\ to 5 data cells under the three arguments and 3 return-stack entries under
\ its return address; /MOD, one call further out, leaves 2. The first
\ version, built on ABS, DABS, 0< and NEGATE calls, overflowed the return
\ stack inside DABS -> DNEGATE -> D+ -> U> and never returned correctly for
\ a negative dividend.
``` ```
`2DUP`, `-`, `ABS`, and `DABS` are defined in §5; the compiler resolves forward references within the `2DUP`, `-`, and `DNEGATE` are defined in §5; the compiler resolves forward references within the
core capsule. core capsule.
--- ---
@@ -237,9 +308,9 @@ Section numbers match the v3 primitive reference.
| `?DUP` | CAP | `dup IF dup THEN` | | `?DUP` | CAP | `dup IF dup THEN` |
| `ROT` | CAP | §4 | | `ROT` | CAP | §4 |
| `-ROT` | CAP | `ROT ROT` | | `-ROT` | CAP | `ROT ROT` |
| `DEPTH` | MM | Read `DSP` (D-2). | | `DEPTH` | RET | No visible stack pointer (D-2). |
| `PICK` | MM + CAP | Read stack RAM at `DSP − n` (D-2). 0-based, as in v3. | | `PICK` | RET | No visible stack pointer (D-2). |
| `ROLL` | CAP | Rewritten with ANS semantics (D-7), using `PICK` and a copy loop. | | `ROLL` | RET | No visible stack pointer (D-2); D-7 is moot. |
### 5.2 Return stack ### 5.2 Return stack
@@ -294,7 +365,7 @@ Section numbers match the v3 primitive reference.
| `1+` `1-` `2+` `2-` | IN | `1 +`, `-1 +`, `2 +`, `-2 +` | | `1+` `1-` `2+` `2-` | IN | `1 +`, `-1 +`, `2 +`, `-2 +` |
| `2*` | OP | `2*` | | `2*` | OP | `2*` |
| `2/` | OP | `2/` | | `2/` | OP | `2/` |
| `ABS` | CAP | `dup 0< IF NEGATE THEN` | | `ABS` | CAP | `dup 0< IF NEGATE THEN` — executed on the golden model (2026-10-02). |
| `NEGATE` | CAP | §4 | | `NEGATE` | CAP | §4 |
| `MIN` | CAP | `2DUP > IF SWAP THEN drop` | | `MIN` | CAP | `2DUP > IF SWAP THEN drop` |
| `MAX` | CAP | `2DUP < IF SWAP THEN drop` | | `MAX` | CAP | `2DUP < IF SWAP THEN drop` |
@@ -313,14 +384,14 @@ Section numbers match the v3 primitive reference.
| `0=` `0<` | CAP | §4 | | `0=` `0<` | CAP | §4 |
| `0<>` | CAP | `0= 0=` | | `0<>` | CAP | `0= 0=` |
| `0>` | CAP | `dup 0< SWAP 0= OR 0=` (correct for the most negative number) | | `0>` | CAP | `dup 0< SWAP 0= OR 0=` (correct for the most negative number) |
| `=` | CAP | `xor 0=` | | `=` | CAP | `xor 0=` — executed on the golden model (2026-10-02). |
| `<>` | CAP | `xor 0<>` | | `<>` | CAP | `xor 0<>` |
| `<` | CAP | `2DUP xor 0< IF drop 0< ELSE - 0< THEN` (overflow-safe) | | `<` | CAP | `2DUP xor 0< IF drop 0< ELSE - 0< THEN` (overflow-safe) — executed on the golden model (2026-10-02). |
| `>` | CAP | `SWAP <` | | `>` | CAP | `SWAP <` |
| `<=` | CAP | `> 0=` | | `<=` | CAP | `> 0=` |
| `>=` | CAP | `< 0=` | | `>=` | CAP | `< 0=` |
| `U<` | CAP | §4 | | `U<` | CAP | §4 |
| `U>` | CAP | `SWAP U<` | | `U>` | CAP | `SWAP U<` — executed on the golden model (2026-10-02). |
| `WITHIN` | CAP | `over - push - pop U<` | | `WITHIN` | CAP | `over - push - pop U<` |
| `TRUE` | IN | `-1` | | `TRUE` | IN | `-1` |
| `FALSE` | IN | `0` | | `FALSE` | IN | `0` |
@@ -331,12 +402,12 @@ A double is two 32-bit cells on a mesh node.
| Word | Fate | v4 definition | | Word | Fate | v4 definition |
| --- | --- | --- | | --- | --- | --- |
| `M+` | CAP | `S>D D+` | | `M+` | CAP | `S>D D+` — executed on the golden model (2026-10-02). |
| `M-` | CAP | `NEGATE M+` | | `M-` | CAP | `NEGATE M+` |
| `M*` | CAP | `2DUP xor push ABS SWAP ABS UM* pop 0< IF DNEGATE THEN` | | `M*` | CAP | `2DUP xor push ABS SWAP ABS UM* pop 0< IF DNEGATE THEN` |
| `M/MOD` | CAP | `SM/REM` | | `M/MOD` | CAP | `SM/REM` |
| `MOD` | CAP | `/MOD drop` | | `MOD` | CAP | `/MOD drop` |
| `/MOD` | CAP | `push S>D pop SM/REM` | | `/MOD` | CAP | `push S>D pop SM/REM` — executed on the golden model (2026-10-02). |
| `*/` | CAP | `*/MOD NIP` | | `*/` | CAP | `*/MOD NIP` |
| `*/MOD` | CAP | `push M* pop SM/REM` | | `*/MOD` | CAP | `push M* pop SM/REM` |
@@ -344,23 +415,24 @@ A double is two 32-bit cells on a mesh node.
| Word | Fate | v4 definition | | Word | Fate | v4 definition |
| --- | --- | --- | | --- | --- | --- |
| `S>D` | CAP | `dup 0<` | | `S>D` | CAP | `dup 0<` — executed on the golden model (2026-10-02). |
| `D+` | CAP | `push SWAP push over + 2DUP U> ROT drop NEGATE pop pop + +` | | `D+` | CAP | `push over push push drop pop over over xor -if L1 drop + -if C1 jump C0 L1: drop over -if L2 drop + jump C1 L2: drop + C0: pop pop + ; C1: pop pop + 1 + ;` — call-free. The carry out of the low cells is found by sign tests: if their top bits differ, there is a carry exactly when the sum's top bit is clear; if they match, exactly when both are set. Executed on the golden model (2026-10-02); leaves its caller 6 data cells under its arguments and 5 return entries. Replaces `push SWAP push over + 2DUP U> ROT drop NEGATE pop pop + +`, which was exact but left 1 return entry. |
| `DNEGATE` | CAP | `inv SWAP inv SWAP 1 0 D+` | | `DNEGATE` | CAP | `inv over if L1 drop push inv 1 + pop ; L1: drop 1 + ;` — call-free: `~d + 1`, carrying into the high cell exactly when the low cell is 0. Executed on the golden model (2026-10-02). Replaces `inv SWAP inv SWAP 1 0 D+`, which left a caller no return-stack room, so `DABS` could not run at all. |
| `D-` | CAP | `DNEGATE D+` | | `D-` | CAP | `DNEGATE D+` — executed on the golden model (2026-10-02). |
| `DABS` | CAP | `dup 0< IF DNEGATE THEN` | | `DABS` | CAP | `dup 0< IF DNEGATE THEN` — executed on the golden model (2026-10-02). |
| `D0=` | CAP | `OR 0=` | | `D0=` | CAP | `OR 0=` — executed on the golden model (2026-10-02). |
| `D0<` | CAP | `NIP 0<` | | `D0<` | CAP | `NIP 0<` |
| `D=` | CAP | `D- D0=` | | `D=` | CAP | `D- D0=` — executed on the golden model (2026-10-02). |
| `D<` | CAP | `ROT 2DUP = IF 2DROP U< ELSE SWAP < NIP NIP THEN` | | `D<` | CAP | `ROT 2DUP = IF 2DROP U< ELSE SWAP < NIP NIP THEN` — executed on the golden model (2026-10-02). |
| `DMAX` | CAP | `2OVER 2OVER D< IF 2SWAP THEN 2DROP` | | `(D<)` | CAP | `( d1 d2 -- d1 d2 flag )`, call-free; internal to `DMAX` and `DMIN`. Copies of the high cells go on top; if they differ the flag comes from them, else from the low cells unsigned. The value tested always has its top bit set exactly when `d1 < d2`: `ah` (high signs differ), `ah - bh` (agree), `bl` (low top bits differ), `al - bl` (agree); `x - y` with `y` on top is `push inv pop + inv`. `dup push push over pop over over xor if TIE drop over over xor -if HS drop drop jump S1 HS: drop push inv pop + inv S1: -if N1 drop -1 jump D1 N1: drop 0 D1: pop SWAP ; TIE: drop drop drop dup push push over pop over over xor -if LS drop NIP jump S2 LS: drop push inv pop + inv S2: -if N2 drop -1 jump D2 N2: drop 0 D2: pop pop ROT ;` with `SWAP`, `NIP` and `ROT` in line. Executed on the golden model (2026-10-02). |
| `DMIN` | CAP | `2OVER 2OVER D< 0= IF 2SWAP THEN 2DROP` | | `DMAX` | CAP | `(D<) if L drop push push drop drop pop pop ; L: drop drop drop ;` Executed on the golden model (2026-10-02). Replaces `2OVER 2OVER D< IF 2SWAP THEN 2DROP`, which needs 8 data cells plus `D<`'s 2: the whole 10-deep data stack, so it failed whenever the caller held anything at all (D-2). |
| `DMIN` | CAP | `(D<) if L drop drop drop ; L: drop push push drop drop pop pop ;` Executed on the golden model (2026-10-02); replaces `2OVER 2OVER D< 0= IF 2SWAP THEN 2DROP` for the same reason as `DMAX`. |
| `D2*` | CAP | `2* over 0< NEGATE OR SWAP 2* SWAP` | | `D2*` | CAP | `2* over 0< NEGATE OR SWAP 2* SWAP` |
| `D2/` | CAP | `dup 1 and push 2/ SWAP 1 RSHIFT pop IF MSB OR THEN SWAP` | | `D2/` | CAP | `dup 1 and push 2/ SWAP 1 RSHIFT pop IF MSB OR THEN SWAP` |
| `2DROP` | IN | `drop drop` | | `2DROP` | IN | `drop drop` |
| `2DUP` | IN | `over over` | | `2DUP` | IN | `over over` |
| `2SWAP` | CAP | `ROT push ROT pop` | | `2SWAP` | CAP | `ROT push ROT pop`, with `ROT` and `SWAP` in line so it makes no calls. Executed on the golden model (2026-10-02). Called, `ROT` and `SWAP` left its caller 2 return entries; in line, 4. |
| `2OVER` | CAP | `push push 2DUP pop pop 2SWAP` | | `2OVER` | CAP | `push push 2DUP pop pop 2SWAP` — executed on the golden model (2026-10-02). |
| `2ROT` | CAP | `2>R 2SWAP 2R> 2SWAP` | | `2ROT` | CAP | `2>R 2SWAP 2R> 2SWAP` |
| `2>R` | IN | `SWAP push push` | | `2>R` | IN | `SWAP push push` |
| `2R>` | IN | `pop pop SWAP` | | `2R>` | IN | `pop pop SWAP` |
@@ -374,7 +446,7 @@ All output reaches the console through `EMIT` (DEV).
| --- | --- | --- | | --- | --- | --- |
| `<#` `#` `#S` `HOLD` `SIGN` `#>` | CAP | Standard pictured-output definitions over `UM/MOD` and a hold buffer. v3's tolerant `#>` (pops `ud` only if present) is not kept; v4 follows the standard stack effect. | | `<#` `#` `#S` `HOLD` `SIGN` `#>` | CAP | Standard pictured-output definitions over `UM/MOD` and a hold buffer. v3's tolerant `#>` (pops `ud` only if present) is not kept; v4 follows the standard stack effect. |
| `.` `.R` `U.` `U.R` `D.` `D.R` | CAP | Built on pictured output and `TYPE`. | | `.` `.R` `U.` `U.R` `D.` `D.R` | CAP | Built on pictured output and `TYPE`. |
| `.S` | CAP | Walks the stack via `DSP` (D-2). | | `.S` | RET | No visible stack pointer (D-2). |
| `?` | CAP | `@ .` | | `?` | CAP | `@ .` |
| `DUMP` | CAP | Loop over `@`/`C@` with pictured output. | | `DUMP` | CAP | Loop over `@`/`C@` with pictured output. |
| `BASE` | CAP | Variable. | | `BASE` | CAP | Variable. |
@@ -441,7 +513,7 @@ The storage service belongs to the Artemis role, now a device node.
| Word | Fate | Notes | | Word | Fate | Notes |
| --- | --- | --- | | --- | --- | --- |
| `HERE` `ALIGN` `ALLOT` `,` `C,` `2,` `PAD` `LATEST` | CC | The dictionary lives on the host node. | | `HERE` `ALIGN` `ALLOT` `,` `C,` `2,` `PAD` `LATEST` | CC | The dictionary lives on the host node. |
| `SP@` `SP!` | MM | `DSP` register (D-2). | | `SP@` `SP!` | RET | No visible stack pointer (D-2). |
### 5.13 Dictionary manipulation ### 5.13 Dictionary manipulation
@@ -581,19 +653,31 @@ index should use them; they cost one instruction per iteration.
### 5.26 Q48.16 fixed-point math ### 5.26 Q48.16 fixed-point math
A Q48.16 value is 64 bits, so on a 32-bit node it occupies **two cells** and every Q word is a double A Q48.16 value is 64 bits, so on a 32-bit node it occupies **two cells** and every Q word is a double
word. Per D-8, v4 Q values are signed. word. Per D-10 it occupies two cells on a 64-bit node too. Per D-8, v4 Q values are signed.
| Word | Fate | Notes | | Word | Fate | Notes |
| --- | --- | --- | | --- | --- | --- |
| `Q.+` `Q.-` | CAP | `D+`, `D-` | | `Q.+` `Q.-` | CAP | `D+`, `D-` — executed on the golden model (2026-10-02) against v3's `q48_add`/`q48_sub` (`uint64_t` wrapping): bit-for-bit at 32-bit cells; at 64-bit cells the low cell is v3's, per D-10. |
| `Q.*` | CAP | 64×64 product from four `UM*` partial products, shifted right 16. | | `Q.*` | CAP | `SWAP push over over UM* drop push push over pop -if L1 SWAP jump L2 L1: SWAP drop 0 L2: pop SWAP - push push over pop UM* pop + ROT pop dup push over -if L3 drop dup jump L4 L3: drop 0 L4: push UM* pop - D+ ROT pop UM* SWAP push 0 D+ pop push over pop SWAP Q.TO-INT push Q.TO-INT pop SWAP` (`SWAP` and `ROT` in line) — `floor(a*b / 2^16)`, signed (D-8), cut to two cells. Cells 0–2 of the product come from the unsigned cell products `a1*b1` (low cell), `a0*b1`, `a1*b0`, `a0*b0`, in that order, each input dropped after its last use and `b0` waiting on the return stack. Reading `a1` and `b1` as signed takes `(b1<0 ? a0 : 0)` and `(a1<0 ? b0 : 0)` off cell 2; each is folded in as soon as its operands are adjacent. The result is cells 0–2 shifted right 16 with `Q.TO-INT` twice. Executed on the golden model (2026-10-02) against an independent limb-by-limb reference, and against v3's `q48_mul` for non-negative operands. Leaves its caller 3 data cells under its arguments and 3 return entries. Clobbers `A`. |
| `Q./` | CAP | Shifted long division. **Division by zero sets an error** (v3 returned 0 silently). | | `Q./` | CAP | `over over OR if ZERO drop push over pop SWAP over xor (Q/) 4 + b! !b -if L1 DNEGATE L1: push push -if L2 DNEGATE L2: pop pop dup if CHK drop jump DIV CHK: drop over -131072 and if CHK2 drop jump DIV CHK2: drop push push dup pop dup push N-18 FOR 2* UNEXT over over xor -if SAME drop drop -if NOOV jump OV SAME: drop push inv pop + inv -if OV NOOV: drop pop pop jump DIV OV: drop drop drop pop pop drop drop (Q/) 4 + b! @b -if OVP drop 0 MSB ; OVP: drop -1 MAXHI ; DIV: (UQ/) (Q/) 4 + b! @b -if L3 drop DNEGATE ; L3: drop ; ZERO: drop drop drop NODE-ERROR b! -1 !b over over OR if Z0 drop -if ZP drop drop 0 MSB ; ZP: drop drop -1 MAXHI ; Z0: drop ;` — D-11: `a * 2^16 / b`, rounded toward zero; saturated to Q max / Q min on overflow; on division by zero, Q max / Q min by the dividend's sign (0 for `0 / 0`) and `NODE-ERROR` set. The sign of the result waits in `(Q/)`. Overflow needs no division: the quotient reaches `2^(2N-1)` exactly when `|a| * 2^16 >= |b| * 2^(2N-1)`, possible only for `|b| < 2^17`, where it is `a1 >= b0 << (N-17)` unsigned. `MSB` and `MAXHI` are the high cells of Q min and Q max. Executed on the golden model (2026-10-02) against an independent limb-by-limb reference (including `NODE-ERROR`), on width-native edge values, and against v3's `q48_div` for non-negative `a < 2^48`. Leaves its caller 3 data cells under its arguments and 3 return entries. Clobbers `A` and `B`. |
| `Q.ABS` `Q.NEG` | CAP | `DABS`, `DNEGATE` | | `(UQ/)` | CAP | Internal to `Q./`: unsigned `floor(a * 2^16 / b)` for `b != 0` and no overflow. Restoring division, `2N+16` steps, on one shifting register — quotient (starting as `a`) above remainder — with the quotient and divisor in `(Q/)` so the stacks carry only the remainder, the quotient bit and the loop count. Each step's quotient bit enters at the next step's shift; with no overflow the bits leaving the quotient in the last 16 steps are zeros. Trial subtraction by in-line sign tests (`x - y` with `y` on top is `push inv pop + inv`), including the full double subtraction with its borrow, so the loop calls nothing but `D2*C`. Executed on the golden model (2026-10-02). Clobbers `A` and `B`. |
| `Q.LOG` `Q.EXP` `Q.SQRT` `Q.SIN` `Q.COS` | CAP | Algorithms ported from `q48_words.c`; the hosted C versions are the golden model. | | `D2*C` | CAP | `( lo hi cin -- lo' hi' cout )`: the double shifted left one bit, `cin` entering at the bottom and `cout` the bit leaving the top (both 0 or 1). `a! dup -if L1 drop 1 jump L2 L1: drop 0 L2: push over -if L3 drop 1 jump L4 L3: drop 0 L4: over + + push 2* a + pop pop` — `cin` waits in `A`, and `2hi + m` is `over + +`, so it needs one return entry. Executed on the golden model (2026-10-02). Clobbers `A`. |
| `Q.FROM-INT` | CAP | `S>D` shifted left 16. Negative values are no longer clamped to 0. | | `(Q/)` | CAP | Variable, 5 cells: `Q./`'s quotient register, divisor and result sign. Like `BASE` and the hold buffer, it lives in node memory. |
| `Q.TO-INT` | CAP | Shift right 16, take the low cell. | | `Q.ABS` `Q.NEG` | CAP | `DABS`, `DNEGATE` — executed on the golden model (2026-10-02) against v3's `q48_abs` and `0 - q`: bit-for-bit at 32-bit cells, including v3's wrap of Q min to itself; at 64-bit cells the low cell is v3's and the high cell is the true sign, per D-10. |
| `Q.1` `Q.0` `Q.SCALE` | IN | Double-cell constants. | | `Q.COS` | CAP | v3's `q48_cos_approx`: on `xu = |(Q.REDUCE) x|`, `1 - xu^2/2! + xu^4/4! - …` to `n = 10`, run by `Q.SIN`'s loop: `(Q.REDUCE) -if A1 inv 1 + A1: 0 (QT) b! !b 0 over 0 Q.* drop (QT) 1 + b! !b 65536 (QT) 2 + b! !b 65536 (QT) 3 + b! !b 2 (QT) 4 + b! !b -1 (QT) 5 + b! !b jump TRIG` — term and sum start at 1.0, `n` at 2, and the sign cell is 0 so nothing is negated at the end. It jumps into the loop rather than calling it, so it costs no extra return entry. Executed on the golden model (2026-10-03): bit for bit v3's result on angles of every size and sign. Leaves its caller 3 data cells under its argument and 2 return entries. Clobbers `A` and `B`. |
| `Q.=` `Q.<` `Q.>` `Q.0=` `Q.MAX` `Q.MIN` | CAP | `D=`, `D<`, `SWAP D<` (for `Q.>`), `D0=`, `DMAX`, `DMIN`. Signed. | | `Q.SIN` | CAP | v3's `q48_sin_approx`: on `r = (Q.REDUCE) x` and `xu = |r|`, `xu - xu^3/3! + xu^5/5! - …` to `n = 11`, each term the last times `xu^2` over `n(n-1)`, stopping once a term is below 10 ulp; negated if `r < 0`. After the reduction every value fits one cell, so the variable `(QT)` holds single cells and the only calls are `(Q.REDUCE)`, `Q.*`, `Q./` and `UM*`. The Taylor loop is written so that `Q.COS` can jump into it. Executed on the golden model (2026-10-03): bit for bit v3's result on angles of every size and sign. Leaves its caller 3 data cells under its argument and 2 return entries. Clobbers `A` and `B`. |
| `(Q.REDUCE)` | CAP | `( x -- r )`, v3's `q48_reduce_angle`: the angle reduced to one cell, `-pi <= r <= pi` with `pi = 205887`, `2pi = 411774` — the remainder of `x / 2pi` with the sign of `x`, then one step of `2pi` back into range. `x / 2pi` does not fit a cell, but only the remainder is wanted: `|x| mod 2pi` is two `UM/MOD` steps, the high cell first and its remainder then leading the low cell. `dup (QT) b! !b -if L1 DNEGATE L1: 0 411774 UM/MOD drop 411774 UM/MOD drop (QT) b! @b -if P1 drop inv 1 + jump J1 P1: drop J1: dup -205888 + -if BIG drop dup 205887 + -if OK drop 411774 + ; OK: drop ; BIG: drop -411774 + ;` Executed on the golden model (2026-10-03), bit for bit v3's. Clobbers `A` and `B`. |
| `(QT)` | CAP | Variable, 6 cells: `Q.SIN` / `Q.COS`'s sign, `x^2`, term, sum, `n` and subtract flag. |
| `Q.LOG` | CAP | v3's `q48_log_approx`: `x = 2^k * m` with `1.0 <= m < 2.0`; `ln m` by up to 6 Newton rounds on `e^y = m` from `y = m - 1.0`, stopping once `|m - e^y| < 100` ulp; result `y + k * ln 2` with `ln 2 = 45426`. `e^y` is `Q.EXP`'s Taylor loop **written in line** (flattened, ruled 2026-10-02), so `Q.LOG` calls only `Q.*`, `Q./` and `UM*` and the call chain is one level shorter than through `Q.EXP`. After the reduction `m`, `y`, the Taylor term and its sum each fit one cell at either width, so the variable `(QL)` holds single cells. `x <= 0` returns 0 and sets `NODE-ERROR` (D-12). Executed on the golden model (2026-10-03): bit for bit v3's result for every `x > 0` tested, including a sweep of the reduced `m`. v3's clamp `y = max(y - corr, 0)` is kept for fidelity but cannot fire: over all 65536 values of `m` it is never reached, and the iteration never needs more than 4 rounds. Leaves its caller 3 data cells under its argument and 2 return entries. Clobbers `A` and `B`. |
| `(QL)` | CAP | Variable, 7 cells: `Q.LOG`'s `m`, `y`, `k`, rounds left, Taylor term (then `delta`), sum, and `n * 1.0`. |
| `Q.SQRT` | CAP | v3's `q48_sqrt_approx`: Newton from `x0 = q/2 + 0.25`, up to 8 rounds of `x' = (x + q/x) / 2`, returning `x` as soon as `|x' - x| < 10` ulp; `sqrt(0) = 0`, `sqrt(1.0) = 1.0`. `q < 0` returns 0 and sets `NODE-ERROR` (D-12). `q`, `x` and the rounds left live in the variable `(QR)`. The halving is a logical double shift, `push a! 0 pop +* MAXHI and push drop a pop`. Executed on the golden model (2026-10-02): bit for bit v3's result for `0 <= q < 2^48`; above that v3's `q48_div` saturates and v4 divides correctly, so they part. Leaves its caller 3 data cells under its argument and 2 return entries. Clobbers `A` and `B`. |
| `(QR)` | CAP | Variable, 5 cells: `Q.SQRT`'s `q`, `x` and rounds left. |
| `Q.EXP` | CAP | v3's `q48_exp_approx`: `1 + x + x^2/2! + …` to 10 terms on `x = |q|`, stopping once a term is below 50 ulp; `1.0 Q./ e^|q|` for `q < 0`; `e^0 = 1.0`; `|q| >= 16.0` gives 0 (`q < 0`) or **Q max** (v3 returned all ones, which reads as −ulp under D-8). `x`, the term, the sum, the sign and the term index live in the variable `(QE)`, so only `Q.*` and `Q./` arguments sit on the stacks. Executed on the golden model (2026-10-02): bit for bit v3's result for `|q| < 16.0` (at 64-bit cells as the same value, high cell 0). Leaves its caller 3 data cells under its argument and 2 return entries. Clobbers `A` and `B`. |
| `(QE)` | CAP | Variable, 8 cells: `Q.EXP`'s `x`, term, sum, sign and term index. |
| `Q.FROM-INT` | CAP | `push 0 a! 0 pop 15 FOR +* UNEXT push drop a pop` — `n * 2^16` as a signed double. `+*` with `S = 0` never adds, so each step is an exact arithmetic right shift of `T:A`; starting from `T:A = n:0` (that is, `n * 2^N`) and shifting `N-16` bits leaves `n * 2^16`. The count is `N-17`: 15 at 32-bit cells, 47 at 64. Negative values are no longer clamped to 0. Executed on the golden model (2026-10-02): matches v3's `q48_from_u64` for `n >= 0` (at 64-bit cells in the low cell, where v3 wraps for `n >= 2^47`, per D-10). Clobbers `A`. |
| `Q.TO-INT` | CAP | `push a! 0 pop 15 FOR +* UNEXT drop drop a` — the same `+*` shift, 16 bits at every cell width, leaving the low cell in `A`. Rounds toward minus infinity, as v3's arithmetic shift does (−1.5 gives −2). Executed on the golden model (2026-10-02): v3's `q48_to_u64` exactly at 64-bit cells, its low cell at 32. Clobbers `A`. |
| `Q.1` `Q.0` `Q.SCALE` | IN | Double-cell constants, placed in line as two literals, low cell first: `Q.1` and `Q.SCALE` are `65536 0` (1.0), `Q.0` is `0 0`. v3's are 65536, 0 and 65536. Executed on the golden model (2026-10-03): the values match v3's, `Q.1 Q.TO-INT` is 1, `1 Q.FROM-INT` is `Q.1`, and `q Q.1 Q.*` and `q Q.0 Q.+` return `q`. |
| `Q.=` `Q.<` `Q.>` `Q.0=` `Q.MAX` `Q.MIN` | CAP | `D=`, `D<`, `2SWAP D<` (for `Q.>`), `D0=`, `DMAX`, `DMIN`. Signed (D-8); v3 compared unsigned, so v3 agrees only when both values have the same sign. Executed on the golden model (2026-10-02). `Q.>` was given here as `SWAP D<`, which swaps single cells, not Q values, and gave a wrong answer in 11702 of 20169 test cases. |
| `Q.PRINT` | CAP | Pictured output, five fractional digits. | | `Q.PRINT` | CAP | Pictured output, five fractional digits. |
### 5.27 Inference engine ### 5.27 Inference engine
@@ -688,7 +772,6 @@ Addresses are assigned in the node memory map (D-4). Names only here.
| Register | Access | Contents | | Register | Access | Contents |
| --- | --- | --- | | --- | --- | --- |
| `DSP` | R/W | Data stack pointer (D-2). |
| `HEAT-OP[0..31]` | R | Per-opcode retirement heat. | | `HEAT-OP[0..31]` | R | Per-opcode retirement heat. |
| `HEAT-CALL[...]` | R/W | Per-call-target heat, with freeze bit (D-6). | | `HEAT-CALL[...]` | R/W | Per-call-target heat, with freeze bit (D-6). |
| `ANTICLOCK` | R | Virtual tick: a pure function of the execution stream. | | `ANTICLOCK` | R | Virtual tick: a pure function of the execution stream. |
@@ -696,3 +779,4 @@ Addresses are assigned in the node memory map (D-4). Names only here.
| `GOV-*` | R/W | Governor parameters and Jacquard selector state (`L8-*`, decay rate). | | `GOV-*` | R/W | Governor parameters and Jacquard selector state (`L8-*`, decay rate). |
| `REC-ENABLE` | R/W | DoE recorder on/off (`HB-ON` / `HB-OFF`). | | `REC-ENABLE` | R/W | DoE recorder on/off (`HB-ON` / `HB-OFF`). |
| `PORT-STATUS` | R | Per-port ready flags, for non-blocking polls. | | `PORT-STATUS` | R | Per-port ready flags, for non-blocking polls. |
| `NODE-ERROR` | R/W | Arithmetic error flag: set to −1 by `Q./` on division by zero (D-11) and by `Q.SQRT` / `Q.LOG` outside their domain (D-12), cleared by writing 0. `VM-ERROR?` reads it. |
+31
View File
@@ -224,3 +224,34 @@ LithosAnanke filing is a question for counsel.
- K≡1.0 holds on the golden model at both widths, on all three host ISAs. - K≡1.0 holds on the golden model at both widths, on all three host ISAs.
- A hosted mesh runs the Tripod roles as nodes, with Hermes as the network. - A hosted mesh runs the Tripod roles as nodes, with Hermes as the network.
- Verilator co-simulation of one node matches the golden model instruction for instruction. - Verilator co-simulation of one node matches the golden model instruction for instruction.
## 15. Products
Ruled by Captain Bob, 2026-10-03. v4 turns one project into three products built on the same engine:
1. **Hosted StarForth F18.** The v4 engine as a native Linux build for amd64, arm64 and riscv64, on
real hardware.
2. **FPGA StarForth F18.** A 32-bit build of the engine loaded into the FPGA. This is the gateway into
building the whole system, and its foundation.
3. **StarshipOS.** The bare-metal product: LithosAnanke running the v4 F18 engine.
The FORTH-79 vocabulary, recomposed on the F18 engine (`DECOMPOSITION.md`), is stored as a capsule. The
StarshipOS-specific portions are recomposed and stored as capsules in the same way. The source tree
will be reorganised around this split.
## 16. Acceptance criteria
Ruled by Captain Bob, 2026-10-03. Until then v4 had none: this document and `v4/README.md` named a
POST suite and K≡1.0 on three host ISAs, neither of which exists yet, so nothing could be called
accepted.
- **v4 is equivalent to v3 at any point in time.** It must provide the same vocabularies and behave
the same way. The only difference is the machine underneath: the F18-derived engine instead of the
original StarForth VM.
- **Every ISA, hosted and bare metal, must still reach its `ok` prompt.** That is amd64, aarch64 and
riscv64, as a hosted build and as a bare-metal boot.
The existing acceptance tests keep their force and their rules: the three-architecture QEMU boot for
anything bare metal (`.claude/CLAUDE.md`), and the hosted three-architecture test
(`docs/lithosananke/hosted-acceptance-test/README.md`). Passing `make -C v4 test` is a development
check on the golden model, not acceptance.
+183 -99
View File
@@ -1,13 +1,13 @@
# ============================================================================== # ==============================================================================
# Makefile.starkernel — StarKernel UEFI Build System # kernel/Makefile — StarKernel UEFI Build System
# Multi-architecture: amd64 (x86_64), aarch64 (ARM64), riscv64 (RISC-V 64) # Multi-architecture: amd64 (x86_64), aarch64 (ARM64), riscv64 (RISC-V 64)
# #
# Quick start: # Quick start:
# make -f Makefile.starkernel — build for host arch # make -f kernel/Makefile — build for host arch
# make -f Makefile.starkernel ARCH=amd64 qemu — build + boot (x86_64) # make -f kernel/Makefile ARCH=amd64 qemu — build + boot (x86_64)
# make -f Makefile.starkernel ARCH=aarch64 qemu — build + boot (aarch64) # make -f kernel/Makefile ARCH=aarch64 qemu — build + boot (aarch64)
# make -f Makefile.starkernel ARCH=riscv64 qemu — build + boot (riscv64) # make -f kernel/Makefile ARCH=riscv64 qemu — build + boot (riscv64)
# make -f Makefile.starkernel help — show all targets # make -f kernel/Makefile help — show all targets
# ============================================================================== # ==============================================================================
# ============================================================================== # ==============================================================================
@@ -64,7 +64,7 @@ $(eval $(call kconfig_bool,STARFORTH_ENABLE_VM,1))
MONOLITHIC ?= 1 MONOLITHIC ?= 1
# Parallel build — use all available cores when not cleaning # Parallel build — use all available cores when not cleaning
# (adding -j when 'clean' is also a goal causes a race on include/version.h) # (adding -j when 'clean' is also a goal causes a race on v3/include/version.h)
NPROC := $(shell nproc 2>/dev/null || echo 4) NPROC := $(shell nproc 2>/dev/null || echo 4)
ifeq ($(filter clean,$(MAKECMDGOALS)),) ifeq ($(filter clean,$(MAKECMDGOALS)),)
MAKEFLAGS += -j$(NPROC) MAKEFLAGS += -j$(NPROC)
@@ -106,9 +106,9 @@ KERNEL_OBJ_DIR := $(OBJ_DIR)/kernel
LOADER_EFI := $(BUILD_DIR)/starkernel_loader.efi LOADER_EFI := $(BUILD_DIR)/starkernel_loader.efi
KERNEL_ELF := $(BUILD_DIR)/starkernel_kernel.elf KERNEL_ELF := $(BUILD_DIR)/starkernel_kernel.elf
KERNEL_SRC := src/starkernel KERNEL_SRC := kernel/src
KERNEL_INC := include/starkernel KERNEL_INC := kernel/include/starkernel
STARFORTH_CONFIG_HEADER := include/starforth_config.h STARFORTH_CONFIG_HEADER := v3/include/starforth_config.h
QEMU_LOG_DIR := logs QEMU_LOG_DIR := logs
QEMU_ISO := $(BUILD_DIR)/starkernel.iso QEMU_ISO := $(BUILD_DIR)/starkernel.iso
@@ -129,17 +129,17 @@ ARTDISK ?= disk/artemis.img
# headroom above the current 9-device identity roster (Zuse + 8 minted identities) # headroom above the current 9-device identity roster (Zuse + 8 minted identities)
# rather than matching it exactly, per Bob's standing ruling against hardcoding a bound # rather than matching it exactly, per Bob's standing ruling against hardcoding a bound
# to today's scale (FABRIC-3.md §VII.4). Override if a future test needs more, e.g. # to today's scale (FABRIC-3.md §VII.4). Override if a future test needs more, e.g.
# `make -f Makefile.starkernel qemu XHCI_PORTS=32`. # `make -f kernel/Makefile qemu XHCI_PORTS=32`.
XHCI_PORTS ?= 16 XHCI_PORTS ?= 16
# ZUSEDISK -- Zuse's own minted USB thumbdrive, attached by default so a # ZUSEDISK -- Zuse's own minted USB thumbdrive, attached by default so a
# plain `make qemu` lands already authenticated into the Zuse identity # plain `make qemu` lands already authenticated into the Zuse identity
# (Captain Bob, 2026-08-28). Attached at QEMU launch time via -drive/ # (Captain Bob, 2026-08-28). Attached at QEMU launch time via -drive/
# -device on the qemu-xhci controller each arch's qemu target already # -device on the qemu-xhci controller each arch's qemu target already
# creates; xhci_bringup()'s initial port scan (src/starkernel/usb/xhci.c) # creates; xhci_bringup()'s initial port scan (kernel/src/usb/xhci.c)
# is what makes an already-connected-at-launch device visible at all -- # is what makes an already-connected-at-launch device visible at all --
# xhci_poll_events() alone is purely hotplug-event-driven and would never # xhci_poll_events() alone is purely hotplug-event-driven and would never
# see a device present before controller reset. Override to "" (empty) to # see a device present before controller reset. Override to "" (empty) to
# boot without Zuse attached, e.g. `make -f Makefile.starkernel qemu ZUSEDISK=`. # boot without Zuse attached, e.g. `make -f kernel/Makefile qemu ZUSEDISK=`.
ZUSEDISK ?= disk/thumbdrives/zuse-thumb-ident.img ZUSEDISK ?= disk/thumbdrives/zuse-thumb-ident.img
# Precomputed (not inlined as $(if ...,...)) because the drive/device specs # Precomputed (not inlined as $(if ...,...)) because the drive/device specs
# below are comma-heavy and GNU make's $(if) function splits its own # below are comma-heavy and GNU make's $(if) function splits its own
@@ -153,10 +153,10 @@ else
ZUSEDISK_QEMU_ARGS := ZUSEDISK_QEMU_ARGS :=
endif endif
MKCAPSULE_SRC = tools/mkcapsule.c tools/pkcs8_ed25519.c \ MKCAPSULE_SRC = tools/mkcapsule.c tools/pkcs8_ed25519.c \
src/starkernel/crypto/ed25519.c \ kernel/src/crypto/ed25519.c \
src/starkernel/crypto/fe25519.c \ kernel/src/crypto/fe25519.c \
src/starkernel/crypto/scalar25519.c \ kernel/src/crypto/scalar25519.c \
src/starkernel/crypto/sha512.c kernel/src/crypto/sha512.c
MKCAPSULE_BIN = $(BUILD_DIR)/tools/mkcapsule MKCAPSULE_BIN = $(BUILD_DIR)/tools/mkcapsule
# Milestone 6 (Phase 8): the snakeoil intermediate's private key, generated # Milestone 6 (Phase 8): the snakeoil intermediate's private key, generated
# offline outside this repo entirely (see FABRIC-2.md's Phase 8 §Milestone 6 # offline outside this repo entirely (see FABRIC-2.md's Phase 8 §Milestone 6
@@ -169,6 +169,28 @@ CAPSULE_GENERATED = $(BUILD_DIR)/capsule_generated.c
CAPSULE_GENERATED_OBJ = $(BUILD_DIR)/capsule_generated.o CAPSULE_GENERATED_OBJ = $(BUILD_DIR)/capsule_generated.o
CAPSULE_GENERATED_KOBJ = $(KERNEL_OBJ_DIR)/capsule_generated.o CAPSULE_GENERATED_KOBJ = $(KERNEL_OBJ_DIR)/capsule_generated.o
# ==============================================================================
# BOARD (boot_image)
# ==============================================================================
# BOARD names a directory under boards/ (ser5, raspi, milkv, ...). Its
# board.mk sets BOARD_ARCH, BOARD_BOOT (how the firmware finds us) and
# BOARD_IMAGE (the single file written to the boot medium). The root
# Makefile's `make boot_image TARGET=<NAME>` maps NAME to BOARD and passes
# ARCH=$(BOARD_ARCH); the kernel objects themselves are the ordinary
# build/$(ARCH)/kernel ones, shared with `make qemu`.
BOARD ?=
ifneq ($(strip $(BOARD)),)
ifeq ($(wildcard boards/$(BOARD)/board.mk),)
$(error Unknown BOARD='$(BOARD)': no boards/$(BOARD)/board.mk)
endif
include boards/$(BOARD)/board.mk
ifneq ($(BOARD_ARCH),$(ARCH))
$(error BOARD=$(BOARD) is ARCH=$(BOARD_ARCH), but ARCH=$(ARCH) was requested)
endif
BOARD_OUT := build/boards/$(BOARD)
endif
BOOT_IMAGE_SIZE_MIB ?= 128
# ============================================================================== # ==============================================================================
# TOOLCHAIN # TOOLCHAIN
# ============================================================================== # ==============================================================================
@@ -195,8 +217,8 @@ ifeq ($(ARCH),amd64)
# correctly. These flags come after COMMON_CFLAGS on the command line so # correctly. These flags come after COMMON_CFLAGS on the command line so
# they win for amd64 only; riscv64/aarch64 keep -fPIC. # they win for amd64 only; riscv64/aarch64 keep -fPIC.
ARCH_CFLAGS := -m64 -march=x86-64 -mno-red-zone -DARCH_AMD64 -fno-pic -fno-pie ARCH_CFLAGS := -m64 -march=x86-64 -mno-red-zone -DARCH_AMD64 -fno-pic -fno-pie
LOADER_LINKER_SCRIPT := linker/starkernel-loader-amd64.ld LOADER_LINKER_SCRIPT := kernel/linker/starkernel-loader-amd64.ld
KERNEL_LINKER_SCRIPT := linker/starkernel-kernel-amd64.ld KERNEL_LINKER_SCRIPT := kernel/linker/starkernel-kernel-amd64.ld
else ifeq ($(ARCH),aarch64) else ifeq ($(ARCH),aarch64)
ifneq ($(shell which aarch64-linux-gnu-gcc 2>/dev/null),) ifneq ($(shell which aarch64-linux-gnu-gcc 2>/dev/null),)
@@ -211,14 +233,16 @@ else ifeq ($(ARCH),aarch64)
$(error No ARM64 toolchain found. Install aarch64-linux-gnu-gcc or aarch64-none-elf-gcc) $(error No ARM64 toolchain found. Install aarch64-linux-gnu-gcc or aarch64-none-elf-gcc)
endif endif
# aarch64 loader uses clang + lld-link (COFF target — GCC cannot produce aarch64 PE) # aarch64 loader uses clang + lld-link (COFF target — GCC cannot produce aarch64 PE)
LOADER_CC := clang-18 # Any clang with the aarch64 COFF backend works; the version is not
# Debian/Ubuntu package only installs the versioned lld-link-18 on PATH by # pinned (Ubuntu 26.04 ships clang-21, older hosts clang-18).
# default (unversioned lld-link lives under /usr/lib/llvm-18/bin, which LOADER_CC := $(shell which clang 2>/dev/null || ls /usr/bin/clang-[0-9]* 2>/dev/null | sort -V | tail -1 || echo clang)
# Debian/Ubuntu package only installs the versioned lld-link-NN on PATH by
# default (unversioned lld-link lives under /usr/lib/llvm-NN/bin, which
# isn't on PATH unless explicitly prepended) — detect whichever resolves. # isn't on PATH unless explicitly prepended) — detect whichever resolves.
LOADER_LD := $(shell which lld-link 2>/dev/null || which lld-link-18 2>/dev/null || echo lld-link) LOADER_LD := $(shell which lld-link 2>/dev/null || ls /usr/bin/lld-link-[0-9]* /usr/lib/llvm-*/bin/lld-link 2>/dev/null | sort -V | tail -1 || echo lld-link)
ARCH_CFLAGS := -march=armv8-a -mcpu=cortex-a72 -DARCH_AARCH64 -mno-outline-atomics ARCH_CFLAGS := -march=armv8-a -mcpu=cortex-a72 -DARCH_AARCH64 -mno-outline-atomics
LOADER_LINKER_SCRIPT := linker/starkernel-loader-aarch64.ld LOADER_LINKER_SCRIPT := kernel/linker/starkernel-loader-aarch64.ld
KERNEL_LINKER_SCRIPT := linker/starkernel-kernel-aarch64.ld KERNEL_LINKER_SCRIPT := kernel/linker/starkernel-kernel-aarch64.ld
else ifeq ($(ARCH),riscv64) else ifeq ($(ARCH),riscv64)
ifneq ($(shell which riscv64-unknown-elf-gcc 2>/dev/null),) ifneq ($(shell which riscv64-unknown-elf-gcc 2>/dev/null),)
@@ -233,8 +257,8 @@ else ifeq ($(ARCH),riscv64)
$(error No RISC-V toolchain found. Install riscv64-unknown-elf-gcc or riscv64-linux-gnu-gcc) $(error No RISC-V toolchain found. Install riscv64-unknown-elf-gcc or riscv64-linux-gnu-gcc)
endif endif
ARCH_CFLAGS := -march=rv64gc -mabi=lp64d -DARCH_RISCV64 ARCH_CFLAGS := -march=rv64gc -mabi=lp64d -DARCH_RISCV64
LOADER_LINKER_SCRIPT := linker/starkernel-loader-riscv64.ld LOADER_LINKER_SCRIPT := kernel/linker/starkernel-loader-riscv64.ld
KERNEL_LINKER_SCRIPT := linker/starkernel-kernel-riscv64.ld KERNEL_LINKER_SCRIPT := kernel/linker/starkernel-kernel-riscv64.ld
endif endif
# Default loader toolchain = kernel toolchain (overridden for aarch64 above) # Default loader toolchain = kernel toolchain (overridden for aarch64 above)
@@ -260,13 +284,13 @@ COMMON_CFLAGS := \
-ffreestanding -nostdlib -fno-builtin \ -ffreestanding -nostdlib -fno-builtin \
-fPIC -fvisibility=hidden -fno-stack-protector -fshort-wchar \ -fPIC -fvisibility=hidden -fno-stack-protector -fshort-wchar \
$(ARCH_CFLAGS) \ $(ARCH_CFLAGS) \
-I$(KERNEL_INC) -Iinclude -Isrc \ -I$(KERNEL_INC) -Iv3/include -Ikernel/include -Iv3/src \
-include $(STARFORTH_CONFIG_HEADER) \ -include $(STARFORTH_CONFIG_HEADER) \
-DPARITY_MODE=$(PARITY_MODE) -DPARITY_MODE=$(PARITY_MODE)
VMCORE_CFLAGS_COMMON := \ VMCORE_CFLAGS_COMMON := \
$(filter-out -I$(KERNEL_INC),$(COMMON_CFLAGS)) \ $(filter-out -I$(KERNEL_INC),$(COMMON_CFLAGS)) \
-Iinclude -I. -Isrc/word_source -Isrc/test_runner/include \ -Iv3/include -Ikernel/include -I. -Iv3/src/word_source -Iv3/src/test_runner/include \
-Wno-error=unused-parameter -Wno-error=shift-negative-value \ -Wno-error=unused-parameter -Wno-error=shift-negative-value \
-Wno-error=sign-compare -Wno-error=missing-field-initializers -Wno-error=sign-compare -Wno-error=missing-field-initializers
@@ -281,8 +305,8 @@ LOADER_BASE_CFLAGS := \
-mno-stack-arg-probe \ -mno-stack-arg-probe \
-march=armv8-a \ -march=armv8-a \
-DARCH_AARCH64 \ -DARCH_AARCH64 \
-I$(KERNEL_INC) -Iinclude -Isrc \ -I$(KERNEL_INC) -Iv3/include -Ikernel/include -Iv3/src \
-Iinclude/starkernel/freestanding \ -Ikernel/include/starkernel/freestanding \
-include $(STARFORTH_CONFIG_HEADER) \ -include $(STARFORTH_CONFIG_HEADER) \
-DPARITY_MODE=$(PARITY_MODE) \ -DPARITY_MODE=$(PARITY_MODE) \
-DPLATFORM_TIME_NO_INLINE -DPLATFORM_TIME_NO_INLINE
@@ -308,7 +332,7 @@ ifeq ($(ARCH),aarch64)
else ifeq ($(ARCH),riscv64) else ifeq ($(ARCH),riscv64)
LOADER_LDFLAGS_PE := # ELF→objcopy pipeline in link rule LOADER_LDFLAGS_PE := # ELF→objcopy pipeline in link rule
else else
LOADER_LINKER_SCRIPT_PE := linker/starkernel-loader-amd64-pe.ld LOADER_LINKER_SCRIPT_PE := kernel/linker/starkernel-loader-amd64-pe.ld
LOADER_LDFLAGS_PE := \ LOADER_LDFLAGS_PE := \
-T $(LOADER_LINKER_SCRIPT_PE) -m i386pep -nostdlib \ -T $(LOADER_LINKER_SCRIPT_PE) -m i386pep -nostdlib \
--enable-reloc-section --image-base 0 --subsystem 10 -e efi_main --enable-reloc-section --image-base 0 --subsystem 10 -e efi_main
@@ -429,7 +453,7 @@ LOADER_CFLAGS += $(VM_FEATURE_OVERRIDES)
endif endif
# SK_CMD — optional startup FORTH script injected before the interactive REPL. # SK_CMD — optional startup FORTH script injected before the interactive REPL.
# Usage: make -f Makefile.starkernel qemu SK_CMD="TIME-TICKS . BYE" # Usage: make -f kernel/Makefile qemu SK_CMD="TIME-TICKS . BYE"
ifdef SK_CMD ifdef SK_CMD
KERNEL_CFLAGS += -DSK_STARTUP_FORTH='"$(SK_CMD)"' KERNEL_CFLAGS += -DSK_STARTUP_FORTH='"$(SK_CMD)"'
LOADER_CFLAGS += -DSK_STARTUP_FORTH='"$(SK_CMD)"' LOADER_CFLAGS += -DSK_STARTUP_FORTH='"$(SK_CMD)"'
@@ -439,7 +463,7 @@ endif
# The loader reads this file from the EFI partition and parses it at boot. # The loader reads this file from the EFI partition and parses it at boot.
# Supported flags: --doe --log-level=<debug|info|warn|error> # Supported flags: --doe --log-level=<debug|info|warn|error>
# --stack=<N>[MG] --heap=<N>[MG] # --stack=<N>[MG] --heap=<N>[MG]
# Usage: make -f Makefile.starkernel qemu KERNEL_ARGS="--doe --log-level=info" # Usage: make -f kernel/Makefile qemu KERNEL_ARGS="--doe --log-level=info"
KERNEL_ARGS ?= KERNEL_ARGS ?=
# ============================================================================== # ==============================================================================
@@ -534,19 +558,19 @@ KERNEL_ASM := $(wildcard $(KERNEL_SRC)/arch/$(ARCH)/*.S)
ifeq ($(STARFORTH_ENABLE_VM),1) ifeq ($(STARFORTH_ENABLE_VM),1)
VM_ALL_SRCS := \ VM_ALL_SRCS := \
$(wildcard src/*.c) \ $(wildcard v3/src/*.c) \
$(wildcard src/word_source/*.c) \ $(wildcard v3/src/word_source/*.c) \
$(wildcard src/test_runner/*.c) \ $(wildcard v3/src/test_runner/*.c) \
$(wildcard src/test_runner/modules/*.c) $(wildcard v3/src/test_runner/modules/*.c)
VM_EXCLUDE := \ VM_EXCLUDE := \
src/main.c src/cli.c src/repl.c \ v3/src/main.c v3/src/cli.c v3/src/repl.c \
src/platform/% \ v3/src/platform/% \
src/blkio_factory.c src/blkio_file.c \ v3/src/blkio_factory.c v3/src/blkio_file.c \
src/log.c src/doe_metrics.c \ v3/src/log.c v3/src/doe_metrics.c \
src/vm.c src/vm_core.c src/vm_bootstrap.c src/vm_runtime.c src/vm_time.c \ v3/src/vm.c v3/src/vm_core.c v3/src/vm_bootstrap.c v3/src/vm_runtime.c v3/src/vm_time.c \
src/word_source/q48_16_words.c \ v3/src/word_source/q48_16_words.c \
src/test_runner/modules/break_me_tests.c v3/src/test_runner/modules/break_me_tests.c
VM_CORE_SRCS := $(filter-out $(VM_EXCLUDE),$(VM_ALL_SRCS)) VM_CORE_SRCS := $(filter-out $(VM_EXCLUDE),$(VM_ALL_SRCS))
@@ -569,8 +593,8 @@ LOADER_EXTRA_SRCS := \
KERNEL_EXTRA_SRCS := $(LOADER_EXTRA_SRCS) KERNEL_EXTRA_SRCS := $(LOADER_EXTRA_SRCS)
LOADER_VM_OBJS := $(patsubst src/%.c,$(LOADER_OBJ_DIR)/vmcore/%.o,$(VM_CORE_SRCS)) LOADER_VM_OBJS := $(patsubst v3/src/%.c,$(LOADER_OBJ_DIR)/vmcore/%.o,$(VM_CORE_SRCS))
KERNEL_VM_OBJS := $(patsubst src/%.c,$(KERNEL_OBJ_DIR)/vmcore/%.o,$(VM_CORE_SRCS)) KERNEL_VM_OBJS := $(patsubst v3/src/%.c,$(KERNEL_OBJ_DIR)/vmcore/%.o,$(VM_CORE_SRCS))
endif endif
LOADER_SRCS := $(LOADER_SRCS_BASE) $(LOADER_EXTRA_SRCS) LOADER_SRCS := $(LOADER_SRCS_BASE) $(LOADER_EXTRA_SRCS)
@@ -603,7 +627,7 @@ KERNEL_OBJS := \
# MAIN TARGETS # MAIN TARGETS
# ============================================================================== # ==============================================================================
all: include/version.h $(CAPSULE_GENERATED_OBJ) $(CAPSULE_GENERATED_KOBJ) $(LOADER_EFI) $(KERNEL_ELF) all: v3/include/version.h $(CAPSULE_GENERATED_OBJ) $(CAPSULE_GENERATED_KOBJ) $(LOADER_EFI) $(KERNEL_ELF)
@echo "StarKernel built successfully for $(ARCH)" @echo "StarKernel built successfully for $(ARCH)"
@echo " Loader: $(LOADER_EFI)" @echo " Loader: $(LOADER_EFI)"
@echo " Kernel: $(KERNEL_ELF)" @echo " Kernel: $(KERNEL_ELF)"
@@ -611,13 +635,13 @@ all: include/version.h $(CAPSULE_GENERATED_OBJ) $(CAPSULE_GENERATED_KOBJ) $(LOAD
kernel: all kernel: all
kernel-all: kernel-all:
@$(MAKE) -f Makefile.starkernel ARCH=amd64 TARGET=$(TARGET) @$(MAKE) -f kernel/Makefile ARCH=amd64 TARGET=$(TARGET)
@$(MAKE) -f Makefile.starkernel ARCH=aarch64 TARGET=$(TARGET) @$(MAKE) -f kernel/Makefile ARCH=aarch64 TARGET=$(TARGET)
@$(MAKE) -f Makefile.starkernel ARCH=riscv64 TARGET=$(TARGET) @$(MAKE) -f kernel/Makefile ARCH=riscv64 TARGET=$(TARGET)
clean: clean:
rm -rf build/$(ARCH)/$(TARGET) rm -rf build/$(ARCH)/$(TARGET)
rm -f include/version.h rm -f v3/include/version.h
clean-kernel: clean-kernel:
@echo "Cleaning all StarKernel build artifacts..." @echo "Cleaning all StarKernel build artifacts..."
@@ -636,8 +660,8 @@ FORCE:
# here after a hosted `make` run silently reuses that stale/wrong-flavored file # here after a hosted `make` run silently reuses that stale/wrong-flavored file
# and fails with "LITHOS_VERSION_STR undeclared" deep in kernel_main.c, instead # and fails with "LITHOS_VERSION_STR undeclared" deep in kernel_main.c, instead
# of regenerating its own correct version. # of regenerating its own correct version.
include/version.h: FORCE v3/include/version.h: FORCE
@mkdir -p include @mkdir -p v3/include
@BUILD_TS=$$(date -Iseconds 2>/dev/null || echo "unknown"); \ @BUILD_TS=$$(date -Iseconds 2>/dev/null || echo "unknown"); \
printf '#ifndef STARFORTH_VERSION_H\n#define STARFORTH_VERSION_H\n\n' > $@; \ printf '#ifndef STARFORTH_VERSION_H\n#define STARFORTH_VERSION_H\n\n' > $@; \
printf '#define STARFORTH_VERSION "%s"\n' "$(VERSION)" >> $@; \ printf '#define STARFORTH_VERSION "%s"\n' "$(VERSION)" >> $@; \
@@ -653,7 +677,7 @@ include/version.h: FORCE
$(MKCAPSULE_BIN): $(MKCAPSULE_SRC) $(MKCAPSULE_BIN): $(MKCAPSULE_SRC)
@mkdir -p $(dir $@) @mkdir -p $(dir $@)
@echo "HOSTCC $(MKCAPSULE_SRC)" @echo "HOSTCC $(MKCAPSULE_SRC)"
@cc -std=c99 -Wall -Wextra -O2 -Iinclude -Itools -o $@ $(MKCAPSULE_SRC) @cc -std=c99 -Wall -Wextra -O2 -Iv3/include -Ikernel/include -Itools -o $@ $(MKCAPSULE_SRC)
# Generate capsule_generated.c from capsules/ # Generate capsule_generated.c from capsules/
CAPSULE_SRCS := $(shell find $(CAPSULES_DIR) -type f ! -name '.*' 2>/dev/null) CAPSULE_SRCS := $(shell find $(CAPSULES_DIR) -type f ! -name '.*' 2>/dev/null)
@@ -695,12 +719,12 @@ $(LOADER_OBJ_DIR)/%.o: $(KERNEL_SRC)/%.c | $(LOADER_OBJ_DIR)
@$(LOADER_CC) $(LOADER_CFLAGS) -c $< -o $@ @$(LOADER_CC) $(LOADER_CFLAGS) -c $< -o $@
# Compile loader VM core sources # Compile loader VM core sources
$(LOADER_OBJ_DIR)/vmcore/%.o: src/%.c include/version.h | $(LOADER_OBJ_DIR) $(LOADER_OBJ_DIR)/vmcore/%.o: v3/src/%.c v3/include/version.h | $(LOADER_OBJ_DIR)
@mkdir -p $(dir $@) @mkdir -p $(dir $@)
@echo "CC (loader) $<" @echo "CC (loader) $<"
ifeq ($(ARCH),aarch64) ifeq ($(ARCH),aarch64)
@$(LOADER_CC) $(LOADER_CFLAGS) \ @$(LOADER_CC) $(LOADER_CFLAGS) \
-Iinclude -I. -Isrc/test_runner/include \ -Iv3/include -Ikernel/include -I. -Iv3/src/test_runner/include \
-Wno-error=unused-parameter -Wno-error=shift-negative-value \ -Wno-error=unused-parameter -Wno-error=shift-negative-value \
-Wno-error=sign-compare -Wno-error=missing-field-initializers \ -Wno-error=sign-compare -Wno-error=missing-field-initializers \
-Wno-unused-function \ -Wno-unused-function \
@@ -722,10 +746,10 @@ $(KERNEL_OBJ_DIR)/%.o: $(KERNEL_SRC)/%.c | $(KERNEL_OBJ_DIR)
@$(CC) $(KERNEL_CFLAGS) -c $< -o $@ @$(CC) $(KERNEL_CFLAGS) -c $< -o $@
# Compile kernel VM core sources # Compile kernel VM core sources
$(KERNEL_OBJ_DIR)/vmcore/%.o: src/%.c include/version.h | $(KERNEL_OBJ_DIR) $(KERNEL_OBJ_DIR)/vmcore/%.o: v3/src/%.c v3/include/version.h | $(KERNEL_OBJ_DIR)
@mkdir -p $(dir $@) @mkdir -p $(dir $@)
@echo "CC (kernel) $<" @echo "CC (kernel) $<"
@$(CC) $(VMCORE_CFLAGS_COMMON) $(filter-out -I$(KERNEL_INC),$(KERNEL_CFLAGS)) -Isrc/starkernel/vm -c $< -o $@ @$(CC) $(VMCORE_CFLAGS_COMMON) $(filter-out -I$(KERNEL_INC),$(KERNEL_CFLAGS)) -Ikernel/src/vm -c $< -o $@
# Compile kernel assembly sources # Compile kernel assembly sources
$(KERNEL_OBJ_DIR)/%.o: $(KERNEL_SRC)/%.S | $(KERNEL_OBJ_DIR) $(KERNEL_OBJ_DIR)/%.o: $(KERNEL_SRC)/%.S | $(KERNEL_OBJ_DIR)
@@ -802,7 +826,7 @@ OVMF_CODE := /usr/share/OVMF/OVMF_CODE_4M.fd
OVMF_VARS_RO := /usr/share/OVMF/OVMF_VARS_4M.fd OVMF_VARS_RO := /usr/share/OVMF/OVMF_VARS_4M.fd
# QEMU_DISPLAY — window backend for the framebuffer console (gtk/sdl/none/...). # QEMU_DISPLAY — window backend for the framebuffer console (gtk/sdl/none/...).
# Usage: make -f Makefile.starkernel qemu QEMU_DISPLAY=none # headless/CI # Usage: make -f kernel/Makefile qemu QEMU_DISPLAY=none # headless/CI
QEMU_DISPLAY ?= gtk QEMU_DISPLAY ?= gtk
# QEMU_EXTRA — extra raw qemu-system-* args appended verbatim to every arch's # QEMU_EXTRA — extra raw qemu-system-* args appended verbatim to every arch's
@@ -1072,38 +1096,98 @@ else ifeq ($(ARCH),riscv64)
# fallback boot path EFI/BOOT/BOOT<ARCH>.EFI. Storage on real hardware is the # fallback boot path EFI/BOOT/BOOT<ARCH>.EFI. Storage on real hardware is the
# USB BOT/xHCI path (already live), not virtio. # USB BOT/xHCI path (already live), not virtio.
thumbdrive: all thumbdrive: all
@mkdir -p $(BUILD_DIR) @printf 'FS0:\\EFI\\BOOT\\%s\r\n' "$(EFI_BOOTNAME)" > $(BUILD_DIR)/thumbdrive-startup.nsh
@if ! which sgdisk >/dev/null 2>&1; then echo "Error: sgdisk not found. Install gdisk (apt-get install gdisk)."; exit 1; fi @bash scripts/mkdiskimage.sh --out $(BUILD_DIR)/starkernel-thumbdrive.img --table gpt \
@if ! which mkfs.fat >/dev/null 2>&1; then echo "Error: mkfs.fat not found. Install dosfstools (apt-get install dosfstools)."; exit 1; fi --size-mib 128 --label STARKERNEL \
@case "$(ARCH)" in \ $(LOADER_EFI):/EFI/BOOT/$(EFI_BOOTNAME) \
amd64) BOOTNAME="BOOTX64.EFI" ;; \ $(BUILD_DIR)/thumbdrive-startup.nsh:/startup.nsh
aarch64) BOOTNAME="BOOTAA64.EFI" ;; \ @rm -f $(BUILD_DIR)/thumbdrive-startup.nsh
riscv64) BOOTNAME="BOOTRISCV64.EFI" ;; \ @echo "Write to a USB stick with: dd if=$(BUILD_DIR)/starkernel-thumbdrive.img of=/dev/sdX bs=4M status=progress"
*) echo "Error: no thumbdrive EFI boot name for ARCH=$(ARCH)"; exit 1 ;; \
esac; \
# Geometry: 128 MiB disk (262144 sectors), GPT partition 1 spans sectors \
# 2048..262110 (the GPT last-usable sector for this disk size), i.e. \
# 260063 sectors. The FAT32 ESP image MUST match the partition size \
# exactly; a larger ESP overruns the disk (GPT grows corrupt) or \
# spills past the partition end, both of which made earlier builds \
# unbootable on hardware. \
DISK=$(BUILD_DIR)/starkernel-thumbdrive.img; \
ESP_SECTORS=260063; \
rm -f $$DISK $(BUILD_DIR)/thumbdrive-esp.img; \
dd if=/dev/zero of=$(BUILD_DIR)/thumbdrive-esp.img bs=512 count=$$ESP_SECTORS 2>/dev/null; \
mkfs.fat -F 32 -n "STARKERNEL" $(BUILD_DIR)/thumbdrive-esp.img >/dev/null 2>&1; \
mmd -i $(BUILD_DIR)/thumbdrive-esp.img ::/EFI; \
mmd -i $(BUILD_DIR)/thumbdrive-esp.img ::/EFI/BOOT; \
mcopy -i $(BUILD_DIR)/thumbdrive-esp.img $(LOADER_EFI) ::/EFI/BOOT/$$BOOTNAME; \
printf 'FS0:\\EFI\\BOOT\\%s\r\n' "$$BOOTNAME" > $(BUILD_DIR)/thumbdrive-startup.nsh; \
mcopy -i $(BUILD_DIR)/thumbdrive-esp.img $(BUILD_DIR)/thumbdrive-startup.nsh ::/startup.nsh; \
dd if=/dev/zero of=$$DISK bs=1M count=128 2>/dev/null; \
sgdisk -n 1:2048:0 -t 1:ef00 -c 1:"EFI System" $$DISK >/dev/null 2>&1; \
dd if=$(BUILD_DIR)/thumbdrive-esp.img of=$$DISK bs=512 seek=2048 conv=notrunc 2>/dev/null; \
rm -f $(BUILD_DIR)/thumbdrive-esp.img $(BUILD_DIR)/thumbdrive-startup.nsh; \
echo "Thumbdrive image: $$DISK"; \
echo "Write to a USB stick with: dd if=$$DISK of=/dev/sdX bs=4M status=progress"
# ==============================================================================
# BOOT IMAGES (one per board)
# ==============================================================================
# boot_image -- the single file written to a board's boot medium. Driven by
# BOARD (boards/<board>/board.mk); normally invoked from the repo root as
# make boot_image TARGET=SER5|RASPI|MILKV|ZYNQ7020
# Output: build/boards/<board>/$(BOARD_IMAGE).
#
# BOARD_BOOT selects the recipe:
# uefi-esp -- GPT disk, one FAT32 EFI System Partition holding the
# monolithic loader as EFI/BOOT/BOOT<ARCH>.EFI (+ startup.nsh
# for the UEFI shell, + starforth.cfg when KERNEL_ARGS is set).
# Real UEFI firmware (SER5) and U-Boot's bootefi (Milk-V) both
# boot it through the removable-media fallback path.
# rpi-native -- MBR disk, one FAT32 (LBA) partition holding config.txt,
# kernel_2712.img (kernel relinked at 0x80000 and flattened)
# and the stock BCM2712 DTB (+ cmdline.txt, which firmware
# copies into /chosen/bootargs, when KERNEL_ARGS is set).
ifeq ($(ARCH),amd64)
EFI_BOOTNAME := BOOTX64.EFI
else ifeq ($(ARCH),aarch64)
EFI_BOOTNAME := BOOTAA64.EFI
else ifeq ($(ARCH),riscv64)
EFI_BOOTNAME := BOOTRISCV64.EFI
endif
RPI5_NATIVE_LINKER_SCRIPT := kernel/linker/starkernel-native-rpi5.ld
RPI5_NATIVE_ELF := $(BUILD_DIR)/starkernel_rpi5.elf
RPI5_NATIVE_IMG := $(BUILD_DIR)/kernel_2712.img
$(RPI5_NATIVE_ELF): $(KERNEL_OBJS) $(RPI5_NATIVE_LINKER_SCRIPT) | $(BUILD_DIR)
@echo "LD (rpi5 native) $@"
@$(LD) -T $(RPI5_NATIVE_LINKER_SCRIPT) -nostdlib --build-id=none \
-e rpi5_native_start $(KERNEL_OBJS) -o $@
$(RPI5_NATIVE_IMG): $(RPI5_NATIVE_ELF)
@echo "OBJCOPY (raw) $@"
@$(OBJCOPY) -O binary $< $@
.PHONY: boot_image
ifeq ($(strip $(BOARD)),)
boot_image:
@echo "boot_image needs a board. From the repo root:"
@echo " make boot_image TARGET=SER5|RASPI|MILKV|ZYNQ7020"
@exit 1
else ifeq ($(BOARD_BOOT),uefi-esp)
boot_image: all
@mkdir -p $(BOARD_OUT)
@printf 'FS0:\\EFI\\BOOT\\%s\r\n' "$(EFI_BOOTNAME)" > $(BOARD_OUT)/startup.nsh
@rm -f $(BOARD_OUT)/starforth.cfg
$(if $(KERNEL_ARGS),@printf '%s\n' '$(KERNEL_ARGS)' > $(BOARD_OUT)/starforth.cfg)
@bash scripts/mkdiskimage.sh --out $(BOARD_OUT)/$(BOARD_IMAGE) --table gpt \
--size-mib $(BOOT_IMAGE_SIZE_MIB) --label LITHOS \
$(LOADER_EFI):/EFI/BOOT/$(EFI_BOOTNAME) \
$(BOARD_OUT)/startup.nsh:/startup.nsh \
$(if $(KERNEL_ARGS),$(BOARD_OUT)/starforth.cfg:/starforth.cfg)
@echo "$(BOARD_DESC)"
@echo "Write with: dd if=$(BOARD_OUT)/$(BOARD_IMAGE) of=/dev/sdX bs=4M conv=fsync status=progress"
else ifeq ($(BOARD_BOOT),rpi-native)
$(RPI5_DTB):
@mkdir -p $(dir $@)
@echo " FETCH $(RPI5_DTB_URL)"
@curl -fsSL -o $@.tmp $(RPI5_DTB_URL) || { rm -f $@.tmp; \
echo "Error: could not fetch the Pi 5 DTB. Copy bcm2712-rpi-5-b.dtb from a Raspberry Pi"; \
echo "firmware release and pass RPI5_DTB=/path/to/bcm2712-rpi-5-b.dtb"; exit 1; }
@mv $@.tmp $@
boot_image: v3/include/version.h $(RPI5_NATIVE_IMG) $(RPI5_DTB)
@mkdir -p $(BOARD_OUT)
@rm -f $(BOARD_OUT)/cmdline.txt
$(if $(KERNEL_ARGS),@printf '%s\n' '$(KERNEL_ARGS)' > $(BOARD_OUT)/cmdline.txt)
@bash scripts/mkdiskimage.sh --out $(BOARD_OUT)/$(BOARD_IMAGE) --table mbr \
--size-mib $(BOOT_IMAGE_SIZE_MIB) --label LITHOS \
boards/$(BOARD)/config.txt:/config.txt \
$(RPI5_NATIVE_IMG):/kernel_2712.img \
$(RPI5_DTB):/bcm2712-rpi-5-b.dtb \
$(if $(KERNEL_ARGS),$(BOARD_OUT)/cmdline.txt:/cmdline.txt)
@echo "$(BOARD_DESC)"
@echo "Write with: dd if=$(BOARD_OUT)/$(BOARD_IMAGE) of=/dev/mmcblkX bs=4M conv=fsync status=progress"
else
boot_image:
@echo "Error: BOARD=$(BOARD) has BOARD_BOOT='$(BOARD_BOOT)', which has no boot_image recipe"
@exit 1
endif
# iso-usb — build a PURE UEFI isohybrid ISO for the Iso Image Writer workflow # iso-usb — build a PURE UEFI isohybrid ISO for the Iso Image Writer workflow
# (GNOME Disks "Restore Disk Image...", or dd). Writes a single .iso to a USB # (GNOME Disks "Restore Disk Image...", or dd). Writes a single .iso to a USB
@@ -1150,7 +1234,7 @@ iso-usb: all
# yourself with Ctrl-A X or by closing the window). # yourself with Ctrl-A X or by closing the window).
# amd64/aarch64: serial → stdio (bidirectional, you can type into the REPL); # amd64/aarch64: serial → stdio (bidirectional, you can type into the REPL);
# riscv64: uses proper GPT (esp dir not supported) # riscv64: uses proper GPT (esp dir not supported)
qemu-esp: include/version.h $(LOADER_EFI) $(KERNEL_ELF) qemu-esp: v3/include/version.h $(LOADER_EFI) $(KERNEL_ELF)
ifeq ($(ARCH),amd64) ifeq ($(ARCH),amd64)
@rm -rf $(BUILD_DIR)/esp @rm -rf $(BUILD_DIR)/esp
@mkdir -p $(BUILD_DIR)/esp/EFI/BOOT @mkdir -p $(BUILD_DIR)/esp/EFI/BOOT
@@ -1206,7 +1290,7 @@ else ifeq ($(ARCH),riscv64)
endif endif
# qemu-gdb — launch QEMU with GDB stub on port 1234 # qemu-gdb — launch QEMU with GDB stub on port 1234
qemu-gdb: include/version.h $(LOADER_EFI) $(KERNEL_ELF) qemu-gdb: v3/include/version.h $(LOADER_EFI) $(KERNEL_ELF)
ifeq ($(ARCH),amd64) ifeq ($(ARCH),amd64)
@mkdir -p $(BUILD_DIR)/esp/EFI/BOOT @mkdir -p $(BUILD_DIR)/esp/EFI/BOOT
@cp $(LOADER_EFI) $(BUILD_DIR)/esp/EFI/BOOT/BOOTX64.EFI @cp $(LOADER_EFI) $(BUILD_DIR)/esp/EFI/BOOT/BOOTX64.EFI
@@ -1259,7 +1343,7 @@ help:
@echo "StarKernel Build System" @echo "StarKernel Build System"
@echo "=======================" @echo "======================="
@echo "" @echo ""
@echo "Usage: make -f Makefile.starkernel [ARCH=<arch>] [TARGET=<target>] <goal>" @echo "Usage: make -f kernel/Makefile [ARCH=<arch>] [TARGET=<target>] <goal>"
@echo "" @echo ""
@echo "Architectures (aliases accepted):" @echo "Architectures (aliases accepted):"
@echo " ARCH=amd64 / x86_64 — x86-64 (default on x86 host)" @echo " ARCH=amd64 / x86_64 — x86-64 (default on x86 host)"
@@ -1289,8 +1373,8 @@ help:
@echo " help — show this message" @echo " help — show this message"
@echo "" @echo ""
@echo "Examples:" @echo "Examples:"
@echo " make -f Makefile.starkernel ARCH=amd64 qemu" @echo " make -f kernel/Makefile ARCH=amd64 qemu"
@echo " make -f Makefile.starkernel ARCH=aarch64 clean qemu" @echo " make -f kernel/Makefile ARCH=aarch64 clean qemu"
@echo " make -f Makefile.starkernel ARCH=riscv64 clean qemu" @echo " make -f kernel/Makefile ARCH=riscv64 clean qemu"
@echo " make -f Makefile.starkernel ARCH=x86_64 qemu # alias works" @echo " make -f kernel/Makefile ARCH=x86_64 qemu # alias works"
@echo " make -f Makefile.starkernel kernel-all" @echo " make -f kernel/Makefile kernel-all"

Some files were not shown because too many files have changed in this diff Show More