Record the FPGA three-product split: Hosted StarForth / full StarshipOS / HOL-proven sealed-execution hardware
The Zynq FPGA is not a fourth platform to port to — it is the pivot that
forces the project into three distinct products, each with its own host,
delivery, and proof character (decided 2026-08-29):
1. Hosted StarForth - the existing hosted/interpreted StarForth runtime
(3-arch acceptance-tested), delivered as a portable embedded runtime.
2. A full StarshipOS - the standalone OS built on LithosAnanke
(LithosAnanke -> StarshipOS), a self-booting OS on general silicon
(SER5/RasPi/Milk-V line).
3. Hardware steady-state machinery with sealed executions, HOL-proven -
the FPGA-native product: hardware-enforced sealed executions and
steady-state machinery machine-checked in a proof assistant (HOL);
delivery is the bitstream + HOL proof artifacts, not just an OS port.
The coupling is the point: product 3 is born on the FPGA, and its existence
is what cleanly separates 1 from 2 from 3. Product 1 ships hosted on an OS,
product 2 as an OS on general silicon, product 3 as proven hardware. Per-
product gates and the even-major line carrying the three as separate tracks
are scoped at v2.5.0 close / during the coloring-in phase. Complements, and
does not retract, the existing hardware bare-metal release policy.
Authoritative form in ROADMAP.md; FABRIC-3.md tracks the same horizon.
This commit is contained in:
+11
-2
@@ -3501,5 +3501,14 @@ a genuinely larger step than any prior board, expected on a new even-major line.
|
|||||||
v2.5.0 and starting the Zynq sits a **"coloring in"** hardening phase: making v2.5.0's
|
v2.5.0 and starting the Zynq sits a **"coloring in"** hardening phase: making v2.5.0's
|
||||||
real-hardware story production-honest (USB BOT/xHCI + block robustness; live-entropy and
|
real-hardware story production-honest (USB BOT/xHCI + block robustness; live-entropy and
|
||||||
Zuse-cert hardening on real ASICs; SMP/multi-core + IRQ routing from the HAL notes; driver
|
Zuse-cert hardening on real ASICs; SMP/multi-core + IRQ routing from the HAL notes; driver
|
||||||
breadth) so the FPGA carries a thickened, not thin, shape forward. Full form in
|
breadth) so the FPGA carries a thickened, not thin, shape forward.
|
||||||
`ROADMAP.md` "Beyond v2.5.0 — Zynq FPGA is the next big milestone".
|
|
||||||
|
**The FPGA creates a three-product split, decided 2026-08-29.** The Zynq is the pivot that
|
||||||
|
forces the project into three distinct products, each with its own host, delivery, and proof
|
||||||
|
character: (1) **Hosted StarForth** — the existing hosted/interpreted StarForth runtime;
|
||||||
|
(2) **A full StarshipOS** — the standalone OS on general silicon (LithosAnanke → StarshipOS);
|
||||||
|
(3) **Hardware steady-state machinery with sealed executions, HOL-proven** — the FPGA-native
|
||||||
|
product: hardware-enforced sealed executions and steady-state machinery machine-checked in a
|
||||||
|
proof assistant (HOL); delivery is the bitstream + HOL proof artifacts. Product 3 is born on
|
||||||
|
the FPGA and its existence is what cleanly separates 1 from 2 from 3. Full form in
|
||||||
|
`ROADMAP.md` "Release Versioning Policy → The FPGA creates a three-product split".
|
||||||
|
|||||||
@@ -56,6 +56,33 @@ architecture-delta work, and it reshapes the hardware story (soft/hard CPU cores
|
|||||||
non-standard memory map, custom peripherals). Expect a new even-major line for it once the
|
non-standard memory map, custom peripherals). Expect a new even-major line for it once the
|
||||||
coloring-in period below lands.
|
coloring-in period below lands.
|
||||||
|
|
||||||
|
**The FPGA creates a three-product split, decided 2026-08-29.** The Zynq is not just a fourth
|
||||||
|
platform to port to — it is the pivot that forces the project to separate into three
|
||||||
|
distinct products, each with its own host, delivery, and proof character. This is the neat
|
||||||
|
partition the FPGA's configurable-silicon nature makes possible and demands:
|
||||||
|
|
||||||
|
1. **Hosted StarForth** — the hosted/interpreted StarForth product that already exists
|
||||||
|
(3-arch acceptance-tested; runs StarForth hosted on an OS). Its delivery is the Forth
|
||||||
|
+ VM + capsule semantics as a portable, embeddable interpreted runtime.
|
||||||
|
2. **A full StarshipOS** — the standalone operating system built on LithosAnanke
|
||||||
|
(LithosAnanke → StarshipOS). Its delivery is a self-booting OS on general-purpose
|
||||||
|
silicon (the SER5/RasPi/Milk-V line already covers this).
|
||||||
|
3. **Hardware steady-state machinery with sealed executions, HOL-proven** — the
|
||||||
|
FPGA-native product: hardware-enforced sealed executions and steady-state machinery
|
||||||
|
whose guarantees are machine-checked in a proof assistant (HOL). This is the product only
|
||||||
|
configurable silicon can honor — secret/hardware-boundary enforcement and formally
|
||||||
|
verified behavior carried in silicon rather than software. Its delivery is the bitstream +
|
||||||
|
the HOL proof artifacts (not just a port of the OS).
|
||||||
|
|
||||||
|
The coupling is the point: the FPGA is where product 3 is born, and product 3's existence is
|
||||||
|
what cleanly separates 1 from 2 from 3. Product 1 ships hosted on an OS; product 2 ships as
|
||||||
|
an OS on general silicon; product 3 ships as proven hardware. Anything that straddles those
|
||||||
|
boundaries after this decision is a conscious product-line choice, not an accident of history.
|
||||||
|
Scoping of each product's concrete gates, and the new even-major line that carries products 1
|
||||||
|
through 3 as separate tracks, is defined at v2.5.0 close / during the coloring-in phase.
|
||||||
|
(This complements, and does not retract, the existing "hardware bare-metal release" policy
|
||||||
|
above.)
|
||||||
|
|
||||||
**Before the FPGA — "coloring in", decided 2026-08-29.** The period between the all-three
|
**Before the FPGA — "coloring in", decided 2026-08-29.** The period between the all-three
|
||||||
bare-metal cut (v2.5.0) and starting the Zynq is finishing/hardening work that thickens the
|
bare-metal cut (v2.5.0) and starting the Zynq is finishing/hardening work that thickens the
|
||||||
shape of what already exists rather than adding new silicon. This is not idle time; it is
|
shape of what already exists rather than adding new silicon. This is not idle time; it is
|
||||||
|
|||||||
Reference in New Issue
Block a user