docs(v4.0.0): add StarForth v4 justification and primitive decomposition
JUSTIFICATION.md records why v4 exists and the reasoning behind each major design decision. DECOMPOSITION.md assigns every v3 C primitive a fate on the 32-instruction F18-derived core. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BY9HMwK5Cetz3caBgHGyds
This commit is contained in:
@@ -0,0 +1,698 @@
|
||||
# StarForth v4.0.0 — Primitive Decomposition
|
||||
|
||||
This document assigns every C primitive in StarForth v3 (`admin/LithosAnanake` at `6302dcb`) a fate in
|
||||
StarForth v4.0.0. v4 is built on a 32-instruction core derived from Chuck Moore's F18 (the GA144 node).
|
||||
Everything that is not one of those 32 instructions becomes capsule code, a service message to another
|
||||
node, a memory-mapped register, or is retired.
|
||||
|
||||
The rationale is in `JUSTIFICATION.md`. This document is the specification.
|
||||
|
||||
**Status.** Every colon definition below is written against the ISA in §1 and has been traced by hand,
|
||||
but none has been executed. Each one becomes a POST test target: it is correct when the hosted v4 golden
|
||||
model produces the same results as the v3 C primitive it replaces.
|
||||
|
||||
---
|
||||
|
||||
## Contents
|
||||
|
||||
0. [Fates](#0-fates)
|
||||
1. [The v4 core ISA](#1-the-v4-core-isa)
|
||||
2. [Compiler conventions](#2-compiler-conventions)
|
||||
3. [Open decisions](#3-open-decisions)
|
||||
4. [Foundation layer (new words)](#4-foundation-layer-new-words)
|
||||
5. [Fate of every v3 primitive](#5-fate-of-every-v3-primitive)
|
||||
6. [Messaging between nodes](#6-messaging-between-nodes)
|
||||
7. [Memory-mapped registers](#7-memory-mapped-registers)
|
||||
|
||||
---
|
||||
|
||||
## 0. Fates
|
||||
|
||||
| Code | Fate | Meaning |
|
||||
| --- | --- | --- |
|
||||
| **OP** | Instruction | One of the 32 core opcodes. |
|
||||
| **IN** | Inline macro | A short opcode sequence the compiler places in-line. Never called. Required for anything that touches the return stack, since a call would bury the return address. |
|
||||
| **CAP** | Core capsule | A colon definition in the core capsule, built only from OP, IN, and earlier CAP words. |
|
||||
| **CC** | Compiler capsule | Part of the compiler/interpreter capsule, which runs on the host node only. Mesh nodes receive compiled code. |
|
||||
| **DEV** | Device service | A message to a device node that owns real hardware (console, storage, display, keyboard, log). |
|
||||
| **HERA** | Hera service | A message to the Hera node, which owns lifecycle, identity, capsules, ACLs, and Stadium admission. |
|
||||
| **MM** | Memory-mapped | An `@` or `!` against a hardware register (heat counters, anti-clock, governor, stack pointer). |
|
||||
| **RET** | Retired | A diagnostic of v3's software machine that has no equivalent in v4. |
|
||||
|
||||
---
|
||||
|
||||
## 1. The v4 core ISA
|
||||
|
||||
### 1.1 Machine model
|
||||
|
||||
| Item | v4 node |
|
||||
| --- | --- |
|
||||
| Cell | 32 bits (mesh node). The host node's width is a build parameter; see D-5. |
|
||||
| Addressing | Word-addressed (pending D-1). |
|
||||
| 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. |
|
||||
| Instruction word | Six 5-bit slots, plus 2 spare bits. |
|
||||
|
||||
### 1.2 Instruction word layout
|
||||
|
||||
```
|
||||
31 27 26 22 21 17 16 12 11 7 6 2 1 0
|
||||
+--------+--------+--------+--------+--------+--------+----+
|
||||
| slot 0 | slot 1 | slot 2 | slot 3 | slot 4 | slot 5 | xx |
|
||||
+--------+--------+--------+--------+--------+--------+----+
|
||||
```
|
||||
|
||||
Slots execute left to right. A branch (`jump`, `call`, `next`, `if`, `-if`) takes its target from all
|
||||
bits to the right of its slot, and that target replaces the same low bits of `P` (page-relative, as in
|
||||
the F18). Branches are therefore legal in slots 0–3 only:
|
||||
|
||||
| Branch in slot | Address bits | Reach |
|
||||
| --- | --- | --- |
|
||||
| 0 | 27 | whole address space |
|
||||
| 1 | 22 | 4M words |
|
||||
| 2 | 17 | 128K words |
|
||||
| 3 | 12 | 4K words (node-local) |
|
||||
|
||||
### 1.3 The 32 opcodes
|
||||
|
||||
Opcode numbering follows the F18. Two names differ from Moore's: F18 `-` is renamed `inv` and F18 `or`
|
||||
(which is exclusive-or) is renamed `xor`, so instruction names never collide with FORTH-79 word names.
|
||||
|
||||
| Op | Name | Effect |
|
||||
| --- | --- | --- |
|
||||
| 00 | `;` | Return: `P ← R`, pop `R`. |
|
||||
| 01 | `ex` | Swap `P` and `R` (co-routine / execute). |
|
||||
| 02 | `jump a` | `P ← a`. |
|
||||
| 03 | `call a` | Push `P` to `R`, `P ← a`. |
|
||||
| 04 | `unext` | If `R ≠ 0`: decrement `R`, restart the current instruction word at slot 0. Else pop `R`. |
|
||||
| 05 | `next a` | If `R ≠ 0`: decrement `R`, `P ← a`. Else pop `R`. |
|
||||
| 06 | `if a` | If `T = 0`: `P ← a`. **Does not pop `T`.** |
|
||||
| 07 | `-if a` | If `T ≥ 0` (sign bit clear): `P ← a`. **Does not pop `T`.** |
|
||||
| 08 | `@p` | Push the word at `P`, `P ← P+1` (literal). |
|
||||
| 09 | `@+` | Push the word at `A`, `A ← A+1`. |
|
||||
| 0A | `@b` | Push the word at `B`. |
|
||||
| 0B | `@` | Push the word at `A`. |
|
||||
| 0C | `!p` | Store `T` at `P`, pop, `P ← P+1`. |
|
||||
| 0D | `!+` | Store `T` at `A`, pop, `A ← A+1`. |
|
||||
| 0E | `!b` | Store `T` at `B`, pop. |
|
||||
| 0F | `!` | Store `T` at `A`, pop. |
|
||||
| 10 | `+*` | Multiply step: if bit 0 of `A` is set, `T ← T+S`; then shift `T:A` right one bit. See D-3. |
|
||||
| 11 | `2*` | `T ← T << 1`. |
|
||||
| 12 | `2/` | `T ← T >> 1`, arithmetic. |
|
||||
| 13 | `inv` | `T ← ~T`. |
|
||||
| 14 | `+` | `T ← S + T`, pop. |
|
||||
| 15 | `and` | `T ← S & T`, pop. |
|
||||
| 16 | `xor` | `T ← S ^ T`, pop. |
|
||||
| 17 | `drop` | Pop `T`. |
|
||||
| 18 | `dup` | Push a copy of `T`. |
|
||||
| 19 | `pop` | Pop `R` onto the data stack. |
|
||||
| 1A | `over` | Push a copy of `S`. |
|
||||
| 1B | `a` | Push `A`. |
|
||||
| 1C | `nop` | Nothing. |
|
||||
| 1D | `push` | Pop `T` onto the return stack. |
|
||||
| 1E | `b!` | `B ← T`, pop. |
|
||||
| 1F | `a!` | `A ← T`, pop. |
|
||||
|
||||
Note that `@` and `!` address through `A`, not through `T`. The FORTH words `@` and `!` therefore become
|
||||
`a! @` and `a! !`.
|
||||
|
||||
### 1.4 Side effects that are not instructions
|
||||
|
||||
Execution itself drives the physics. Every retired instruction increments that opcode's heat counter and
|
||||
advances the anti-clock; every `call` increments the heat counter of its target. None of this costs an
|
||||
instruction. Capsule code reads it through the memory-mapped registers in §7.
|
||||
|
||||
---
|
||||
|
||||
## 2. Compiler conventions
|
||||
|
||||
**Literals.** A number in source compiles to `@p` followed by the value in the next word.
|
||||
|
||||
**Capsule `IF`.** Native `if` and `-if` leave the flag on the stack. The capsule-level `IF` consumes it,
|
||||
so the compiler drops it on both paths:
|
||||
|
||||
```
|
||||
IF body THEN → if L1 drop body jump L2
|
||||
L1: drop
|
||||
L2:
|
||||
|
||||
IF body1 ELSE body2 THEN → if L1 drop body1 jump L2
|
||||
L1: drop body2
|
||||
L2:
|
||||
```
|
||||
|
||||
`BEGIN ... WHILE ... REPEAT` and `BEGIN ... UNTIL` expand the same way.
|
||||
|
||||
**`FOR ... NEXT`.** `n FOR ... NEXT` compiles `push` then the body then `next`. The body runs `n+1`
|
||||
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
|
||||
document that clobber `A`: `@ ! +! -! 2@ 2! C@ C! UM* * UM/MOD SEND RECV`. Words that clobber `B`:
|
||||
`SEND RECV`.
|
||||
|
||||
**Return-stack words** (`>R R> R@ 2>R 2R> 2R@ I J UNLOOP` and the loop runtimes) are always IN.
|
||||
|
||||
---
|
||||
|
||||
## 3. Open decisions
|
||||
|
||||
These must be settled before the golden model is built. Where a definition below depends on one, it
|
||||
says so.
|
||||
|
||||
| ID | Decision | Default in this document |
|
||||
| --- | --- | --- |
|
||||
| **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-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-4** | Node memory map, including port and register addresses. | Symbolic names only (§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-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-7** | `ROLL` semantics. | Fix to ANS (count from the top). v3's bottom-counting `ROLL` is retired. |
|
||||
| **D-8** | Q48.16 signedness. | Signed. v3's unsigned comparisons and `Q.FROM-INT` clamping are retired. |
|
||||
|
||||
---
|
||||
|
||||
## 4. Foundation layer (new words)
|
||||
|
||||
These words do not exist as primitives in v3 but everything else is built on them. They are listed in
|
||||
dependency order.
|
||||
|
||||
```forth
|
||||
\ ---- helpers ------------------------------------------------------------
|
||||
: NIP ( a b -- b ) push drop pop ;
|
||||
: SWAP ( a b -- b a ) over push push drop pop pop ;
|
||||
: OR ( a b -- a|b ) over inv and xor ;
|
||||
: NEGATE ( n -- -n ) inv 1 + ;
|
||||
: ROT ( a b c -- b c a ) push SWAP pop SWAP ;
|
||||
|
||||
\ ---- sign and zero tests (raw branches, labels shown) ------------------
|
||||
: 0< ( n -- flag ) -if L1 drop -1 ; L1: drop 0 ;
|
||||
: 0= ( n -- flag ) if L1 drop 0 ; L1: drop -1 ;
|
||||
|
||||
\ ---- unsigned compare ---------------------------------------------------
|
||||
: U< ( u1 u2 -- flag ) 2DUP xor 0< IF NIP 0< ELSE - 0< THEN ;
|
||||
|
||||
\ ---- multiply (D-3) -----------------------------------------------------
|
||||
: UM* ( u1 u2 -- ulo uhi ) a! 0 31 FOR +* UNEXT push drop a pop ;
|
||||
|
||||
\ ---- divide: 32-step restoring division, divisor held in A --------------
|
||||
: UM/MOD ( ulo uhi ud -- urem uquot )
|
||||
a!
|
||||
31 FOR
|
||||
over 0< NEGATE push \ R: lo's top bit (1/0)
|
||||
dup 0< push \ R: hi's top bit (-1/0)
|
||||
2* pop pop SWAP push OR pop \ lo hi' t hi shifted, lo bit brought in
|
||||
push SWAP 2* SWAP pop \ lo' hi' t
|
||||
over a U< 0= OR \ lo' hi' flag t OR hi' >= d
|
||||
IF a - SWAP 1 OR SWAP THEN
|
||||
NEXT
|
||||
SWAP ;
|
||||
|
||||
\ ---- signed division, truncating toward zero (v3 semantics) -------------
|
||||
: SM/REM ( d n -- rem quot )
|
||||
2DUP xor push \ R: quotient sign
|
||||
over push \ R: remainder sign (sign of dividend)
|
||||
ABS push DABS pop UM/MOD
|
||||
pop 0< IF push NEGATE pop THEN
|
||||
pop 0< IF NEGATE THEN ;
|
||||
```
|
||||
|
||||
`2DUP`, `-`, `ABS`, and `DABS` are defined in §5; the compiler resolves forward references within the
|
||||
core capsule.
|
||||
|
||||
---
|
||||
|
||||
## 5. Fate of every v3 primitive
|
||||
|
||||
Section numbers match the v3 primitive reference.
|
||||
|
||||
### 5.1 Stack
|
||||
|
||||
| Word | Fate | v4 definition / notes |
|
||||
| --- | --- | --- |
|
||||
| `DROP` | OP | `drop` |
|
||||
| `DUP` | OP | `dup` |
|
||||
| `OVER` | OP | `over` |
|
||||
| `SWAP` | CAP | §4 |
|
||||
| `?DUP` | CAP | `dup IF dup THEN` |
|
||||
| `ROT` | CAP | §4 |
|
||||
| `-ROT` | CAP | `ROT ROT` |
|
||||
| `DEPTH` | MM | Read `DSP` (D-2). |
|
||||
| `PICK` | MM + CAP | Read stack RAM at `DSP − n` (D-2). 0-based, as in v3. |
|
||||
| `ROLL` | CAP | Rewritten with ANS semantics (D-7), using `PICK` and a copy loop. |
|
||||
|
||||
### 5.2 Return stack
|
||||
|
||||
| Word | Fate | v4 definition |
|
||||
| --- | --- | --- |
|
||||
| `>R` | IN | `push` |
|
||||
| `R>` | IN | `pop` |
|
||||
| `R@` | IN | `pop dup push` |
|
||||
|
||||
### 5.3 Memory
|
||||
|
||||
| Word | Fate | v4 definition / notes |
|
||||
| --- | --- | --- |
|
||||
| `@` | IN | `a! @` |
|
||||
| `!` | IN | `a! !` |
|
||||
| `+!` | CAP | `a! @ + !` |
|
||||
| `-!` | CAP | `a! NEGATE @ + !` |
|
||||
| `2@` | CAP | `a! @+ @` (low cell at `addr`, high at `addr+1`, as in v3) |
|
||||
| `2!` | CAP | `a! SWAP !+ !` |
|
||||
| `C@` | CAP | See below (D-1). |
|
||||
| `C!` | CAP | See below (D-1). |
|
||||
| `FILL` | CAP | See below. |
|
||||
| `MOVE` | CAP | `push 2DUP U< IF pop CMOVE> ELSE pop CMOVE THEN` |
|
||||
| `ERASE` | CAP | `0 FILL` |
|
||||
| `CELLS` | IN | Empty (word-addressed). Becomes `2* 2*` if D-1 chooses bytes. |
|
||||
|
||||
```forth
|
||||
\ byte access on a word-addressed node, little-endian
|
||||
: C@ ( baddr -- c )
|
||||
dup 3 and 3 LSHIFT SWAP 2 RSHIFT a! @ SWAP RSHIFT 255 and ;
|
||||
|
||||
: C! ( c baddr -- )
|
||||
dup 2 RSHIFT a! \ A = word address
|
||||
3 and 3 LSHIFT \ c bits
|
||||
SWAP 255 and over LSHIFT \ bits c'
|
||||
SWAP 255 SWAP LSHIFT inv \ c' ~mask
|
||||
@ and OR ! ;
|
||||
|
||||
: FILL ( baddr u c -- )
|
||||
SWAP BEGIN dup WHILE 1- push 2DUP SWAP C! SWAP 1+ SWAP pop REPEAT 2DROP drop ;
|
||||
```
|
||||
|
||||
### 5.4 Arithmetic
|
||||
|
||||
| Word | Fate | v4 definition / notes |
|
||||
| --- | --- | --- |
|
||||
| `+` | OP | `+` |
|
||||
| `-` | CAP | `NEGATE +` |
|
||||
| `*` | CAP | `UM* drop` |
|
||||
| `/` | CAP | `/MOD NIP` |
|
||||
| `MOD` `/MOD` `*/` `*/MOD` (§4 versions) | RET | Shadowed duplicates. Only the §6 versions survive. |
|
||||
| `1+` `1-` `2+` `2-` | IN | `1 +`, `-1 +`, `2 +`, `-2 +` |
|
||||
| `2*` | OP | `2*` |
|
||||
| `2/` | OP | `2/` |
|
||||
| `ABS` | CAP | `dup 0< IF NEGATE THEN` |
|
||||
| `NEGATE` | CAP | §4 |
|
||||
| `MIN` | CAP | `2DUP > IF SWAP THEN drop` |
|
||||
| `MAX` | CAP | `2DUP < IF SWAP THEN drop` |
|
||||
|
||||
### 5.5 Logic and comparison
|
||||
|
||||
| Word | Fate | v4 definition / notes |
|
||||
| --- | --- | --- |
|
||||
| `AND` | OP | `and` |
|
||||
| `XOR` | OP | `xor` |
|
||||
| `OR` | CAP | §4 |
|
||||
| `INVERT` | OP | `inv` |
|
||||
| `NOT` | CAP | `0=` (FORTH-79 logical not, as in v3) |
|
||||
| `LSHIFT` | CAP | `BEGIN dup WHILE 1- SWAP 2* SWAP REPEAT drop` |
|
||||
| `RSHIFT` | CAP | `BEGIN dup WHILE 1- SWAP 2/ MSB inv and SWAP REPEAT drop` (clears the sign bit each step; `MSB` is the cell-width top-bit constant) |
|
||||
| `0=` `0<` | CAP | §4 |
|
||||
| `0<>` | CAP | `0= 0=` |
|
||||
| `0>` | CAP | `dup 0< SWAP 0= OR 0=` (correct for the most negative number) |
|
||||
| `=` | CAP | `xor 0=` |
|
||||
| `<>` | CAP | `xor 0<>` |
|
||||
| `<` | CAP | `2DUP xor 0< IF drop 0< ELSE - 0< THEN` (overflow-safe) |
|
||||
| `>` | CAP | `SWAP <` |
|
||||
| `<=` | CAP | `> 0=` |
|
||||
| `>=` | CAP | `< 0=` |
|
||||
| `U<` | CAP | §4 |
|
||||
| `U>` | CAP | `SWAP U<` |
|
||||
| `WITHIN` | CAP | `over - push - pop U<` |
|
||||
| `TRUE` | IN | `-1` |
|
||||
| `FALSE` | IN | `0` |
|
||||
|
||||
### 5.6 Mixed-precision arithmetic
|
||||
|
||||
A double is two 32-bit cells on a mesh node.
|
||||
|
||||
| Word | Fate | v4 definition |
|
||||
| --- | --- | --- |
|
||||
| `M+` | CAP | `S>D D+` |
|
||||
| `M-` | CAP | `NEGATE M+` |
|
||||
| `M*` | CAP | `2DUP xor push ABS SWAP ABS UM* pop 0< IF DNEGATE THEN` |
|
||||
| `M/MOD` | CAP | `SM/REM` |
|
||||
| `MOD` | CAP | `/MOD drop` |
|
||||
| `/MOD` | CAP | `push S>D pop SM/REM` |
|
||||
| `*/` | CAP | `*/MOD NIP` |
|
||||
| `*/MOD` | CAP | `push M* pop SM/REM` |
|
||||
|
||||
### 5.7 Double-cell numbers
|
||||
|
||||
| Word | Fate | v4 definition |
|
||||
| --- | --- | --- |
|
||||
| `S>D` | CAP | `dup 0<` |
|
||||
| `D+` | CAP | `push SWAP push over + 2DUP U> ROT drop NEGATE pop pop + +` |
|
||||
| `DNEGATE` | CAP | `inv SWAP inv SWAP 1 0 D+` |
|
||||
| `D-` | CAP | `DNEGATE D+` |
|
||||
| `DABS` | CAP | `dup 0< IF DNEGATE THEN` |
|
||||
| `D0=` | CAP | `OR 0=` |
|
||||
| `D0<` | CAP | `NIP 0<` |
|
||||
| `D=` | CAP | `D- D0=` |
|
||||
| `D<` | CAP | `ROT 2DUP = IF 2DROP U< ELSE SWAP < NIP NIP THEN` |
|
||||
| `DMAX` | CAP | `2OVER 2OVER D< IF 2SWAP THEN 2DROP` |
|
||||
| `DMIN` | CAP | `2OVER 2OVER D< 0= IF 2SWAP THEN 2DROP` |
|
||||
| `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` |
|
||||
| `2DROP` | IN | `drop drop` |
|
||||
| `2DUP` | IN | `over over` |
|
||||
| `2SWAP` | CAP | `ROT push ROT pop` |
|
||||
| `2OVER` | CAP | `push push 2DUP pop pop 2SWAP` |
|
||||
| `2ROT` | CAP | `2>R 2SWAP 2R> 2SWAP` |
|
||||
| `2>R` | IN | `SWAP push push` |
|
||||
| `2R>` | IN | `pop pop SWAP` |
|
||||
| `2R@` | IN | `pop pop 2DUP push push SWAP` |
|
||||
|
||||
### 5.8 Number formatting and output
|
||||
|
||||
All output reaches the console through `EMIT` (DEV).
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `<#` `#` `#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`. |
|
||||
| `.S` | CAP | Walks the stack via `DSP` (D-2). |
|
||||
| `?` | CAP | `@ .` |
|
||||
| `DUMP` | CAP | Loop over `@`/`C@` with pictured output. |
|
||||
| `BASE` | CAP | Variable. |
|
||||
| `DECIMAL` `HEX` `OCTAL` | CAP | `10 BASE !` and so on. |
|
||||
|
||||
### 5.9 Strings, parsing, and input
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `COUNT` | CAP | `dup 1+ SWAP C@` |
|
||||
| `CMOVE` | CAP | See below. |
|
||||
| `CMOVE>` | CAP | See below. |
|
||||
| `BLANK` | CAP | `32 FILL` |
|
||||
| `-TRAILING` | CAP | Loop from the end while the character is a space. |
|
||||
| `COMPARE` | CAP | Byte loop returning `-1`, `0`, or `1`. v3's counted-string auto-detection is not kept. |
|
||||
| `SEARCH` | CAP | Nested loop over `COMPARE`. Same note. |
|
||||
| `SCAN` `SKIP` | CAP | Byte loops. |
|
||||
| `BL` | IN | `32` |
|
||||
| `EXPECT` `QUERY` | CC | Built on `KEY` (DEV). |
|
||||
| `SPAN` `TIB` `>IN` `SOURCE` | CC | Interpreter state on the host node. |
|
||||
| `WORD` `ENCLOSE` | CC | Parser. |
|
||||
| `NUMBER` `CONVERT` | CC | Rewritten to honour `BASE` (v3's `NUMBER` is base 10 only). |
|
||||
| `S"` `(s")` `[']` | CC | Compiler words. |
|
||||
| `LITERAL` `[LITERAL]` (placeholders) | RET | The working `LITERAL` is in §5.17. |
|
||||
|
||||
```forth
|
||||
: CMOVE ( src dst u -- )
|
||||
BEGIN dup WHILE 1- push over C@ over C! 1+ SWAP 1+ SWAP pop REPEAT drop 2DROP ;
|
||||
|
||||
: CMOVE> ( src dst u -- )
|
||||
BEGIN dup WHILE 1- push over R@ + C@ over R@ + C! pop REPEAT drop 2DROP ;
|
||||
```
|
||||
|
||||
### 5.10 Terminal I/O
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `EMIT` | DEV | Console service: one-character message. |
|
||||
| `KEY` | DEV | Console service: blocking receive. |
|
||||
| `?TERMINAL` | DEV | Console service: non-blocking status. |
|
||||
| `TYPE` | CAP | Loop of `C@ EMIT`, or one string message to the console node. |
|
||||
| `CR` | CAP | `10 EMIT` |
|
||||
| `SPACE` | CAP | `BL EMIT` |
|
||||
| `SPACES` | CAP | `BEGIN dup 0> WHILE SPACE 1- REPEAT drop` |
|
||||
| `."` `(do-string)` | CC | Compiler words. |
|
||||
|
||||
### 5.11 Blocks and mass storage
|
||||
|
||||
The storage service belongs to the Artemis role, now a device node.
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `BLOCK` `BUFFER` `UPDATE` `SAVE-BUFFERS` `EMPTY-BUFFERS` `FLUSH` | DEV | Block-service messages. Buffers live in the requesting node's RAM or in DDR. |
|
||||
| `LOAD` `THRU` `-->` | CC | The interpreter reads blocks through the service. |
|
||||
| `LIST` | CAP | `BLOCK` plus `TYPE`. |
|
||||
| `SCR` | CAP | Variable. |
|
||||
| `BLK-CONFIRM-FORMAT` `RELOCATE-BLOCK` | DEV | Owner-only storage messages. |
|
||||
| `BLK-ACL-ALLOW@` `BLK-ACL-ALLOW!` `BLK-ACL-TTL@` `BLK-ACL-TTL!` | HERA | ACL state is held by Hera. |
|
||||
| `BLK-OWNER@` | HERA | Read-only, as in v3. |
|
||||
| `BLK-ATTACH` | RET | Took a raw host pointer. Replaced by an attach message from the device node. |
|
||||
|
||||
### 5.12 Dictionary space
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `HERE` `ALIGN` `ALLOT` `,` `C,` `2,` `PAD` `LATEST` | CC | The dictionary lives on the host node. |
|
||||
| `SP@` `SP!` | MM | `DSP` register (D-2). |
|
||||
|
||||
### 5.13 Dictionary manipulation
|
||||
|
||||
| Word | Fate |
|
||||
| --- | --- |
|
||||
| `'` `FIND` `SMUDGE` `HIDDEN` `>BODY` `>NAME` `NAME>` `>LINK` `LINK>` `CFA` `LFA` `NFA` `PFA` `TRAVERSE` `INTERPRET` | CC |
|
||||
|
||||
### 5.14 Vocabularies
|
||||
|
||||
| Word | Fate |
|
||||
| --- | --- |
|
||||
| `VOCABULARY` `DEFINITIONS` `CONTEXT` `CURRENT` `FORTH` `ORDER` `(FIND)` | CC |
|
||||
|
||||
### 5.15 System
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `(` `\` | CC | |
|
||||
| `EXECUTE` | CAP | `push ;` (tail-jumps to the xt; the xt returns to `EXECUTE`'s caller) |
|
||||
| `NOP` | OP | `nop` |
|
||||
| `QUIT` `ABORT` `ABORT"` `(ABORT")` `COLD` `WARM` | CC | |
|
||||
| `BYE` `REBOOT` | HERA | |
|
||||
| `SAVE-SYSTEM` | HERA | Snapshot becomes a capsule-image request. |
|
||||
| `WORDS` `VLIST` `SEE` | CC | |
|
||||
| `PAGE` | DEV | |
|
||||
| `79-STANDARD` | CC | |
|
||||
|
||||
### 5.16 Line editor
|
||||
|
||||
| Word | Fate |
|
||||
| --- | --- |
|
||||
| `L` `S` `SHOW` `EDIT` | CC |
|
||||
|
||||
### 5.17 Defining words and the compiler
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `:` `;` `CREATE` `VARIABLE` `CONSTANT` `DOES>` `IMMEDIATE` `STATE` `[` `]` `LITERAL` `COMPILE` `[COMPILE]` `FORGET` `FENCE` | CC | |
|
||||
| `LIT` | OP | `@p` |
|
||||
| `does_rt` | RET | Internal helper; `DOES>` is implemented by the compiler capsule. |
|
||||
|
||||
### 5.18 Control flow
|
||||
|
||||
| Word | Fate | v4 definition / notes |
|
||||
| --- | --- | --- |
|
||||
| `IF` `ELSE` `THEN` `BEGIN` `UNTIL` `AGAIN` `WHILE` `REPEAT` `DO` `?DO` `LOOP` `+LOOP` `LEAVE` `CASE` `OF` `ENDOF` `ENDCASE` | CC | Compile-time structure words. Expansions per §2 and below. |
|
||||
| `EXIT` | OP | `;` |
|
||||
| `(BRANCH)` | OP | `jump` |
|
||||
| `(0BRANCH)` | IN | `if L … drop` (§2) |
|
||||
| `(DO)` | IN | `SWAP push push` (R: limit index) |
|
||||
| `(?DO)` | IN | `2DUP = IF 2DROP jump past-loop THEN SWAP push push` |
|
||||
| `(LOOP)` | IN | See below. |
|
||||
| `(+LOOP)` | IN | Sign-aware boundary-crossing test; specified in the compiler capsule. |
|
||||
| `(LEAVE)` | IN | `pop drop pop dup push push jump loop-test` (sets index to limit) |
|
||||
| `I` | IN | `pop dup push` |
|
||||
| `J` | IN | `pop pop pop dup push SWAP push SWAP push` |
|
||||
| `UNLOOP` | IN | `pop pop drop drop` |
|
||||
|
||||
```
|
||||
(LOOP) expansion:
|
||||
pop 1 + pop \ index' limit
|
||||
2DUP xor \ index' limit flag (0 when equal)
|
||||
if Lexit
|
||||
drop push push \ R: limit index'
|
||||
jump Lbody
|
||||
Lexit: drop drop drop
|
||||
```
|
||||
|
||||
`(LOOP)` terminates when the index reaches the limit, which matches v3 for every loop where
|
||||
`start < limit`.
|
||||
|
||||
**New in v4:** `FOR`, `NEXT`, and `UNEXT` are native (§2). Counted loops that don't need an ascending
|
||||
index should use them; they cost one instruction per iteration.
|
||||
|
||||
### 5.19 StarForth extensions
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `ENTROPY@` `ENTROPY!` | MM | Per-call-target heat table (D-6). |
|
||||
| `WORD-ENTROPY` `RESET-ENTROPY` `TOP-WORDS` | CC | Reports over the heat registers. |
|
||||
| `(-` `INIT` | CC | |
|
||||
| `VERSION` | CC | |
|
||||
| `SEED` `RANDOM` | CAP | Deterministic PRNG (xorshift) in capsule code, reproducible from the seed. |
|
||||
| `WAIT` | CAP | Loop until the `ANTICLOCK` register has advanced `n`. |
|
||||
| `HEARTBEAT-TICKS@` | MM | `HEARTBEAT` register. |
|
||||
| `ZUSE-AUTHENTICATE` `ZUSE-SESSION?` `ZUSE-PUBKEY@` `ZUSE-CERT-INSTALLED?` | HERA | |
|
||||
|
||||
### 5.20 Word-level ACL
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `ACL-MODE@` `ACL-MODE!` `ACL-TTL@` `ACL-TTL!` `ACL-ALLOW@` `ACL-ALLOW!` `ACL-PINNED?` `ACL-PIN` `ACL-INHERIT` `ACL-INIT-PRIMITIVES` | HERA | Hera holds the ACL table. In the fabric, per-message ACL checks happen in the router (§6). |
|
||||
| `ACL-HEAT@` | MM | |
|
||||
| `ACL-WORD-ID` | CC | |
|
||||
|
||||
### 5.21 Physics: benchmark and diagnostics
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `BENCH-DICT-LOOKUP` `PHYSICS-CACHE-STATS` `PHYSICS-TOGGLE-CACHE` `PHYSICS-RESET-STATS` `PHYSICS-BUILD-INFO` | RET | Measure v3's software dictionary and hot-words cache, which do not exist on a node. |
|
||||
| `PHYSICS-BAYESIAN-REPORT` | CAP | Host node only; kept as an analysis tool. |
|
||||
| `PHYSICS-WORD-METRICS` `PHYSICS-CALC-KNOBS` `PHYSICS-BURN` `PHYSICS-SHOW-FEEDBACK` | RET | Never registered in v3. |
|
||||
|
||||
### 5.22 Physics: pipelining diagnostics
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `PIPELINING-*` (all six) | RET | Return as MM reports if D-6 adds transition counters. |
|
||||
|
||||
### 5.23 Physics: freeze, heat, and decay
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `FREEZE-WORD` `UNFREEZE-WORD` `FROZEN?` | MM | Freeze bit in the heat table. |
|
||||
| `HEAT@` `HEAT!` | MM | Test-only write retained. |
|
||||
| `SHOW-HEAT` `ALL-HEATS` | CC | |
|
||||
| `DECAY-RATE@` | MM | Governor parameter register. |
|
||||
| `FREEZE-CRITICAL` | CAP | Freezes the core set; the list is rewritten for v4 names. |
|
||||
|
||||
### 5.24 Dictionary heat optimisation
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `HEAT-PERCENTILES` `LOOKUP-STRATEGY@` `LOOKUP-STRATEGY!` `REORG-BUCKETS` `SHOW-HEAT-OPTIMIZATION` `COMPARE-LOOKUPS` | RET | Lookup strategy is a software-dictionary concern. The host compiler may keep a heat-ordered dictionary internally, but these words are not carried forward. |
|
||||
|
||||
### 5.25 Logging
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `LOG-ERROR` … `LOG-DEBUG` (levels) | IN | Constants. |
|
||||
| `LOG-LEVEL!` `LOG-LEVEL@` | CAP | Variable. |
|
||||
| `LOG-ERROR"` … `LOG-DEBUG"` | CC | |
|
||||
| `LOG-*-STR` | DEV | Log-ring service on the recorder (the ARM). |
|
||||
| `(do-log-*)` | CC | |
|
||||
| `(LOG-APPEND-RAW)` | DEV | |
|
||||
|
||||
### 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
|
||||
word. Per D-8, v4 Q values are signed.
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `Q.+` `Q.-` | CAP | `D+`, `D-` |
|
||||
| `Q.*` | CAP | 64×64 product from four `UM*` partial products, shifted right 16. |
|
||||
| `Q./` | CAP | Shifted long division. **Division by zero sets an error** (v3 returned 0 silently). |
|
||||
| `Q.ABS` `Q.NEG` | CAP | `DABS`, `DNEGATE` |
|
||||
| `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. |
|
||||
| `Q.FROM-INT` | CAP | `S>D` shifted left 16. Negative values are no longer clamped to 0. |
|
||||
| `Q.TO-INT` | CAP | Shift right 16, take the low cell. |
|
||||
| `Q.1` `Q.0` `Q.SCALE` | IN | Double-cell constants. |
|
||||
| `Q.=` `Q.<` `Q.>` `Q.0=` `Q.MAX` `Q.MIN` | CAP | `D=`, `D<`, `SWAP D<` (for `Q.>`), `D0=`, `DMAX`, `DMIN`. Signed. |
|
||||
| `Q.PRINT` | CAP | Pictured output, five fractional digits. |
|
||||
|
||||
### 5.27 Inference engine
|
||||
|
||||
The runtime governor moves into hardware as the multi-level Rolling Window of Truth (see
|
||||
`JUSTIFICATION.md`). These words survive on the host node as analysis tools.
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `INFER-RUN` `INFER-WINDOW@` `INFER-DECAY@` `INFER-VARIANCE@` `INFER-FIT@` `INFER-EARLY-EXIT@` | CAP | Host node only. Ported from `inference_words.c`. |
|
||||
| `Q.VARIANCE` `INFER-DECAY-SLOPE` `INFER-WINDOW-WIDTH` `WINDOW-DIVERSITY` | CAP | Host node only. |
|
||||
| `L8-MODE` `L8-UPDATE` `L8-APPLY` `L8-TABLE-FORCE` | MM | Jacquard selector state becomes governor registers. `L8-TABLE-FORCE` remains the DoE override. |
|
||||
| `BAYES-*` (all six) | RET | Model the v3 hot-words cache and bucket search. |
|
||||
|
||||
### 5.28 DEFER and IS
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `DEFER` `IS` `DEFER@` | CC | A deferred word's runtime is `@p push ;` followed by the stored xt. |
|
||||
|
||||
### 5.29 – 5.32 Framebuffer, keyboard, TrueType, scrollback
|
||||
|
||||
| Word | Fate |
|
||||
| --- | --- |
|
||||
| `PLOT` `FB-WIDTH` `FB-HEIGHT` | DEV |
|
||||
| `KBD-SCAN` `KBD-DEBUG` `VKBD-EVENT` `VKBD-DEBUG` `KEY-EVENT` `ALT+TAB` | DEV |
|
||||
| `TTF-TEXT` | DEV |
|
||||
| `SCROLL-BACK` `SCROLL-FWD` | DEV |
|
||||
|
||||
### 5.33 Kernel REPL and DoE hooks
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `HB-ON` `HB-OFF` | MM | Recorder-enable register. The fabric pushes DoE rows into a FIFO; the ARM drains it to storage. |
|
||||
| `BLK-ATTACH-ACK` `KH-BLK-ATTACH-SEND` `KH-ELEVATE-SEND` | RET | Kernel-Hermes calls. Hermes is now the fabric; these become ordinary packets (§6). |
|
||||
|
||||
### 5.34 Hera and child-VM words
|
||||
|
||||
| Word | Fate | Notes |
|
||||
| --- | --- | --- |
|
||||
| `BIRTH` `KILL` `START` `STOP` `USE` `EXEC` `EJECT` `CONNECT-HERMES` `CONNECT-ARTEMIS` `BYE` | HERA | A VM becomes a node (or a group of nodes). `BIRTH` loads a capsule into a node and releases it. |
|
||||
| `VM-EXEC` `VM-CALL` `VM-STEP` | CAP | Built on `SEND` and `RECV` (§6). |
|
||||
| `VM-HEAT` `VM-ERROR?` `VM-COUNT` `VM-CONSERVED?` `VM-PHYSICS-STATUS` | MM + HERA | Per-node heat is a register; fleet totals are Hera's. |
|
||||
| `SWITCH-MARK-WORK` | RET | Nodes run concurrently; there is no context switch to mark. |
|
||||
| `MAMA-VM-ID` `NAME>XT` | HERA, CC | |
|
||||
| `CAPSULE-*` `WORKER-BIRTH` `UNATTENDED-BIRTH` `CONSOLE-ATTACH` | HERA | |
|
||||
| `MINT` `MINT-SCRATCH` `MINT-SCRATCH-EMIT` `ZUSE-ELIGIBILITY-ADD` `ZUSE-ELIGIBLE?` `ELEVATE-PUBKEY-UNPACK` | HERA | |
|
||||
| `RUNCAP-TEST` `PAIR-TEST` | HERA | Diagnostics, kept. |
|
||||
| `STADIUM-ADMIT` `STADIUM-EVICT` `STADIUM-RES-PULL` `STADIUM-RES-PUSH` | HERA | Admission and reservoir are Hera's. |
|
||||
| `STADIUM-HEAT@` `STADIUM-HEAT!` `STADIUM-RES@` `STADIUM-WORD-HEAT` | MM | |
|
||||
|
||||
### 5.35 Hosted lifecycle stubs
|
||||
|
||||
| Word | Fate |
|
||||
| --- | --- |
|
||||
| `BIRTH` `KILL` `PAUSE` `RESUME` `USE` (hosted) | RET — the hosted v4 golden model implements the real HERA messages. |
|
||||
|
||||
---
|
||||
|
||||
## 6. Messaging between nodes
|
||||
|
||||
Each node has four neighbour ports (`PORT-UP`, `PORT-DOWN`, `PORT-LEFT`, `PORT-RIGHT`) mapped into its
|
||||
address space. A read from a port blocks until the neighbour writes; a write blocks until the neighbour
|
||||
reads. This is the GA144 model. No instruction is added: a port is an address.
|
||||
|
||||
### 6.1 Packet format (proposal)
|
||||
|
||||
| Word | Contents |
|
||||
| --- | --- |
|
||||
| 0 | Header: destination node (8 bits), type (8), TTL/heat (8), payload length in words (8). |
|
||||
| 1 | ACL tag: sender identity fingerprint, checked by the router on every packet. |
|
||||
| 2 … | Payload. |
|
||||
|
||||
The router in each node forwards packets not addressed to it, decrements TTL, and drops a packet whose
|
||||
TTL reaches zero or whose ACL tag fails. This is v3 Hermes's per-message ACL check and unconditional TTL
|
||||
expiry, moved into logic. A packet type `SOS` is reserved for any node to emit.
|
||||
|
||||
### 6.2 Send and receive
|
||||
|
||||
```forth
|
||||
: SEND ( addr u port -- ) b! SWAP a! BEGIN dup WHILE 1- @+ !b REPEAT drop ;
|
||||
: RECV ( addr u port -- ) b! SWAP a! BEGIN dup WHILE 1- @b !+ REPEAT drop ;
|
||||
```
|
||||
|
||||
`A` walks the buffer and `B` holds the port, so each word moved costs one fetch and one store.
|
||||
|
||||
---
|
||||
|
||||
## 7. Memory-mapped registers
|
||||
|
||||
Addresses are assigned in the node memory map (D-4). Names only here.
|
||||
|
||||
| Register | Access | Contents |
|
||||
| --- | --- | --- |
|
||||
| `DSP` | R/W | Data stack pointer (D-2). |
|
||||
| `HEAT-OP[0..31]` | R | Per-opcode retirement heat. |
|
||||
| `HEAT-CALL[...]` | R/W | Per-call-target heat, with freeze bit (D-6). |
|
||||
| `ANTICLOCK` | R | Virtual tick: a pure function of the execution stream. |
|
||||
| `HEARTBEAT` | R | Adaptive heartbeat count. |
|
||||
| `GOV-*` | R/W | Governor parameters and Jacquard selector state (`L8-*`, decay rate). |
|
||||
| `REC-ENABLE` | R/W | DoE recorder on/off (`HB-ON` / `HB-OFF`). |
|
||||
| `PORT-STATUS` | R | Per-port ready flags, for non-blocking polls. |
|
||||
@@ -0,0 +1,226 @@
|
||||
# StarForth v4.0.0 — Justification
|
||||
|
||||
This document records why StarForth v4.0.0 exists, what it changes, and why each major decision was
|
||||
made. The specification is `DECOMPOSITION.md`. Per project practice, this document is written before
|
||||
any v4 code.
|
||||
|
||||
---
|
||||
|
||||
## 1. The problem with v3
|
||||
|
||||
StarForth v3 is a successful software machine. It boots on amd64, aarch64, and riscv64, runs the
|
||||
Tripod fleet on LithosAnanke, and has held K≡1.0 across 38,400+ experimental runs. But it was designed
|
||||
for a large host, and it shows:
|
||||
|
||||
- **More than 300 C primitives.** Most are not primitive in any hardware sense. Double-cell arithmetic,
|
||||
string handling, comparisons, pictured output, and Q48.16 transcendentals are all expressible in a
|
||||
handful of machine operations.
|
||||
- **64-bit cells and 5 MB of linear memory per VM.** Reasonable on a PC; far too large for a node in a
|
||||
fabric.
|
||||
- **Diagnostics of its own implementation.** A significant block of words (hot-words cache statistics,
|
||||
lookup strategies, pipelining metrics, Bayesian cache models) measures v3's software dictionary, not
|
||||
the computation the dictionary performs.
|
||||
- **Hermes in software.** Message routing, per-message ACL checks, and TTL expiry are C code executed by
|
||||
a CPU that is also doing everything else.
|
||||
|
||||
None of this is wrong for a hosted or bare-metal OS. It is wrong for silicon. The project's direction
|
||||
is now an FPGA embodiment, and eventually an ASIC, and v3 cannot be carried there by porting.
|
||||
|
||||
## 2. What v4 is
|
||||
|
||||
StarForth v4 is a Forth machine designed to be the same thing in software and in hardware:
|
||||
|
||||
1. **A 32-instruction core ISA** derived from Chuck Moore's F18, the node of the GA144. Every core word
|
||||
is a mnemonic; every mnemonic is one 5-bit opcode.
|
||||
2. **Everything else is capsule code**, compiled from those 32 instructions, or a message to a node that
|
||||
owns a service, or a memory-mapped register, or retired.
|
||||
3. **A mesh of small nodes** that talk to their four neighbours through blocking ports. Hermes becomes
|
||||
the network itself: routing, ACL checks, and TTL expiry move into logic in every node's router.
|
||||
4. **Compudynamics as a side effect of execution.** Heat counters, the anti-clock, and the heartbeat are
|
||||
driven by instruction retirement in hardware. They cost no instructions.
|
||||
5. **A power-aware governor** built from a multi-level Rolling Window of Truth, controlling timing only.
|
||||
|
||||
v4 is a new implementation, not a refactor. v3 remains the reference system for LithosAnanke until v4
|
||||
reaches parity.
|
||||
|
||||
## 3. Why Moore's F18 instruction set
|
||||
|
||||
**It is proven minimal.** Moore spent decades removing instructions from his stack machines. The F18's
|
||||
32 opcodes are the result: enough to build a complete Forth, nothing that can be composed from the
|
||||
rest. There is no multiply, no divide, no compare, and no `SWAP`; each is a short sequence (for example
|
||||
`SWAP` is `over push push drop pop pop`).
|
||||
|
||||
**It fits a 32-bit word exactly.** 32 opcodes need 5 bits. Six slots fill 30 bits of a 32-bit
|
||||
instruction word, with 2 spare. One fetch feeds six instructions.
|
||||
|
||||
**It matches the project's formal-verification plan.** Proving 32 instruction semantics in Isabelle/HOL
|
||||
is a bounded task. Proving 300 C primitives is not. Every higher word then inherits correctness from its
|
||||
definition, which is itself a checkable object.
|
||||
|
||||
**It matches the dictionary-shrink plan that was already underway.** The existing POST suite, which
|
||||
exercises every dictionary word, was to be used as a regression gate while C primitives were replaced by
|
||||
colon definitions. v4 carries that plan to its end point: the surviving primitives are the ISA.
|
||||
|
||||
**It comes with a mesh precedent.** The GA144 places 144 F18 nodes on one die, each talking to its
|
||||
neighbours through blocking ports. v4 adopts that topology directly.
|
||||
|
||||
## 4. Why a mesh, and why Hermes goes into the fabric
|
||||
|
||||
v3's Tripod is several VMs sharing one CPU, with Hermes arbitrating messages between them in software.
|
||||
The mesh replaces time-sharing with space: each VM role runs on its own node or group of nodes,
|
||||
concurrently.
|
||||
|
||||
Moving Hermes into the fabric has three consequences:
|
||||
|
||||
- **The message semantics become hardware.** Per-message ACL checks and unconditional TTL expiry, which
|
||||
v3 already treats as rules rather than options, become router logic that cannot be bypassed.
|
||||
- **Contention disappears as a scheduling problem.** A blocking port is flow control. There is no
|
||||
scheduler to write, which honours the existing design goal of avoiding one.
|
||||
- **The SOS mechanism generalises.** Any node can emit an `SOS` packet. A node whose router fails can
|
||||
only stop forwarding, which its neighbours detect as blocked ports; this is the hardware form of v3's
|
||||
"Hermes raises a semaphore while sinking" rule.
|
||||
|
||||
## 5. Why cell width becomes a parameter
|
||||
|
||||
The Zynq-7000's processing system is a Cortex-A9, a 32-bit ARMv7-A core. Rather than maintain a separate
|
||||
32-bit fork, v4 makes cell width a build parameter of one VM (32 or 64). This has three benefits:
|
||||
|
||||
1. **The ARM becomes a real StarForth host**, not just a bootloader, at 32 bits.
|
||||
2. **Mesh nodes use 32-bit cells**, roughly halving stack and ALU cost in the fabric.
|
||||
3. **It opens a second invariance axis.** K≡1.0 has been shown invariant across amd64, aarch64, and
|
||||
riscv64. If it also holds across cell widths, the conservation law is shown not to depend on word
|
||||
size either. That is a stronger claim than ISA invariance alone.
|
||||
|
||||
The physics does not shrink with the cell. Heat and K arithmetic remain 64-bit (`int64_t` in C99 on
|
||||
every host; double cells on a 32-bit node). Changing only the payload width keeps the experiment clean:
|
||||
any difference in K can be attributed to cell width and not to lost precision.
|
||||
|
||||
## 6. Why the physics splits into "what" and "when"
|
||||
|
||||
The fabric can measure real power: the Zynq's XADC reads on-die temperature and supply voltages, and a
|
||||
current sensor on the core rail gives true power draw. This makes "heat" a physical quantity rather than
|
||||
a metaphor.
|
||||
|
||||
Physical measurements are noisy and never reproducible run to run. If they controlled which code
|
||||
executes, parity hashes would break and formal proofs of behaviour would become impossible. v4
|
||||
therefore splits the physics:
|
||||
|
||||
| Layer | Driven by | Controls | Property |
|
||||
| --- | --- | --- | --- |
|
||||
| **Virtual heat** | Instruction retirement and call counts | What executes (selection, promotion, eviction) | Deterministic and provable |
|
||||
| **Physical power** | XADC and rail current | When things happen (clock gating, node sleep, message pacing) | Adaptive, never affects results |
|
||||
|
||||
This settles a question left open in the original FPGA concept: whether compudynamic feedback into the
|
||||
control unit should affect only timing or also the execution path. The answer is both, through separate
|
||||
channels: logic chooses *what*, physics chooses *when*.
|
||||
|
||||
## 7. Why the governor is a multi-level Rolling Window of Truth
|
||||
|
||||
The timing governor uses the project's own Rolling Window of Truth mechanism at three timescales:
|
||||
|
||||
| Window | Timescale | Governs |
|
||||
| --- | --- | --- |
|
||||
| Short | microseconds | Clock gating on one node |
|
||||
| Medium | milliseconds | Node sleep and wake |
|
||||
| Long | seconds | Thermal trend and mesh-wide message pacing |
|
||||
|
||||
Positive feedback (rising message load) wakes neighbouring nodes and raises the clock. Negative feedback
|
||||
(rising temperature or power) throttles pacing and puts cool nodes to sleep. Each level reacts much more
|
||||
slowly than the one below it, so the loops do not fight; hysteresis at each level prevents flapping at
|
||||
thresholds. Hard limits (thermal ceiling, minimum clock) sit outside the adaptive layer as fixed logic.
|
||||
|
||||
A small neural network is a later candidate. Because the governor only controls timing, a poor governor
|
||||
costs power or speed and never correctness, so it is a safe place to experiment. The DoE recorder
|
||||
(below) produces exactly the training data such a network would need, so the two approaches can be
|
||||
compared on identical workloads.
|
||||
|
||||
## 8. Division of labour on the Zynq
|
||||
|
||||
| Component | Runs on | Role |
|
||||
| --- | --- | --- |
|
||||
| Mesh nodes | Fabric | All StarForth execution, the anti-clock, heat counters, routers |
|
||||
| Governor | Fabric | Multi-level RWT, single clock domain, cycle-exact |
|
||||
| Host node | ARM (32-bit) | Boot and bitstream load, compiler capsule, console bridge, DoE recorder |
|
||||
|
||||
The anti-clock stays in the fabric because it is defined as a pure function of the execution stream and
|
||||
must live where execution happens. The heartbeat's adaptive loop stays in the fabric because a loop
|
||||
crossing the PS–PL boundary would inherit ARM-side jitter (caches, interrupts, bus latency).
|
||||
|
||||
The ARM's recorder role keeps measurement separate from the thing being measured: the fabric pushes
|
||||
DoE rows into a FIFO, the ARM drains them to storage, and if the ARM falls behind rows are dropped
|
||||
rather than execution stalled. This is the fabric form of the planned `HB-ON`/`HB-OFF` disk recording.
|
||||
|
||||
## 9. Why the compiler lives on the host node
|
||||
|
||||
GA144 nodes have 64 words of RAM and 64 of ROM, and arrayForth compiles on a host. v4 follows the same
|
||||
split. The outer interpreter, dictionary, vocabularies, and defining words form the compiler capsule,
|
||||
which runs on the host node. Mesh nodes receive compiled code. Large capsules stay in DDR and are
|
||||
streamed to nodes as needed, so capsule size is not limited by node memory.
|
||||
|
||||
This is also why so many v3 words become CC rather than CAP in `DECOMPOSITION.md`: they are compiler
|
||||
machinery, not computation.
|
||||
|
||||
## 10. Development path
|
||||
|
||||
Each stage is checked against the one before it. Nothing proceeds on trust.
|
||||
|
||||
1. **Hosted golden model.** A C99 implementation of the v4 ISA and node model, with cell width, node
|
||||
count, and node memory as parameters. The POST suite, rewritten against v4 capsules, must pass at
|
||||
both 32 and 64 bits, and K≡1.0 must hold.
|
||||
2. **Hosted mesh.** Several golden-model nodes wired through simulated ports, running the Tripod roles
|
||||
as nodes. The 144-node configuration is exercised here, since the host is not limited by fabric size.
|
||||
3. **Co-simulation.** The node RTL is compiled with Verilator and run in lockstep with the golden model.
|
||||
After every instruction, stacks, registers, and heat counters are compared. The first mismatch
|
||||
identifies the faulty mnemonic exactly.
|
||||
4. **FPGA.** A 2×2 mesh on the PZ7020, then the largest grid that fits. The bitstream only has to match
|
||||
the co-simulation.
|
||||
5. **ASIC.** A single v4 node, not the mesh, as a proof of silicon through an open-source shuttle
|
||||
(currently Tiny Tapeout on IHP's SG13G2 130 nm open PDK). The same RTL is reused; block RAM is
|
||||
replaced by the process's SRAM macros.
|
||||
|
||||
## 11. Scaling beyond the PZ7020
|
||||
|
||||
Node count, node memory, and cell width are parameters, and the mesh is generated by a loop over rows
|
||||
and columns, so a larger board changes numbers, not design.
|
||||
|
||||
| Part | Approximate resources | Estimated nodes |
|
||||
| --- | --- | --- |
|
||||
| Zynq-7020 | ~53K LUTs, 140 BRAM36 | ~8–16 |
|
||||
| Zynq-7045 | ~218K LUTs, 545 BRAM36 | ~50–70 |
|
||||
| Zynq UltraScale+ (e.g. Kria K26) | ~117K LUTs, 144 BRAM36, 64 UltraRAM | ~30–40, with much larger node memory |
|
||||
| Larger UltraScale+ / Versal | Several hundred K LUTs and up | A full 144 |
|
||||
|
||||
Node counts are estimates. The first hardware measurement to take is the LUT cost of one node plus its
|
||||
router on the 7020; every other board's capacity follows from that number.
|
||||
|
||||
UltraScale+ parts also change the host: their Cortex-A53 cores are aarch64, so the host node can run
|
||||
64-bit StarForth while the mesh runs 32-bit cells, which the cell-width parameter already supports.
|
||||
Larger meshes will need registered router-to-router links to close timing, and the free edition of
|
||||
Vivado supports only smaller devices, so tool licensing must be checked before choosing a board.
|
||||
|
||||
## 12. Risks
|
||||
|
||||
| Risk | Mitigation |
|
||||
| --- | --- |
|
||||
| Capsule-level arithmetic is much slower than v3's C primitives on a hosted build. | Accepted. v4's measure of performance is the fabric, where each instruction is one cycle. The hosted build is a correctness oracle. |
|
||||
| Word addressing makes byte and string operations expensive. | D-1 in `DECOMPOSITION.md` keeps the choice open; colorForth's packed, pre-parsed source is a proven alternative for text. |
|
||||
| K≡1.0 may behave differently at 32-bit cell width. | That is an experimental result either way, and the hosted golden model finds it before any hardware exists. |
|
||||
| Hand-traced definitions contain errors. | Every CAP definition is a POST target against the v3 C primitive it replaces. |
|
||||
| The mesh does not fit the 7020 at a useful size. | Measure one node first; the design scales to larger parts unchanged. |
|
||||
|
||||
## 13. Relationship to intellectual property
|
||||
|
||||
v4 strengthens rather than replaces the existing claims. The Jacquard Selector, the Rolling Window of
|
||||
Truth, and the Steady State Machine all survive, now as hardware structures. The new elements a filing
|
||||
could draw on are: compudynamic heat as a zero-cost side effect of instruction retirement; the split of
|
||||
deterministic virtual heat (selection) from physical power (timing); per-packet ACL and TTL enforcement
|
||||
in a mesh router; and conservation invariance across cell width. Whether any of these belong in the
|
||||
LithosAnanke filing is a question for counsel.
|
||||
|
||||
## 14. Definition of done for v4.0.0
|
||||
|
||||
- The 32-instruction ISA is specified, with every open decision in `DECOMPOSITION.md` §3 settled.
|
||||
- The hosted golden model passes the rewritten POST suite at 32-bit and 64-bit cell widths.
|
||||
- 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.
|
||||
- Verilator co-simulation of one node matches the golden model instruction for instruction.
|
||||
Reference in New Issue
Block a user