LithosAnanake/docs/v4.0.0/JUSTIFICATION.md

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.

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.