Rewrite CLAUDE.md and README.md for post-split single-repo scope
LithosAnanke is now its own repository rather than a branch inside the combined StarForth/LithosAnanke monorepo, so this drops the old master(StarForth)/lithosananke(kernel) branch-topology framing in favor of the current reality: this repo's master is the sole LithosAnanke production line. Ground-truths numbers that had drifted (kernel tree file count, word_source file count, capsule count), reframes the vendored VM source as the embedded engine it actually is rather than a second production target, and independently verifies the ACL kernel-parity and DoE-campaign claims against the actual current code. Fixes README's self-referential "see master branch" link to point at the separate StarForth repo instead. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
co-authored by
Claude Sonnet 5
Claude Sonnet 5
parent
db8a3e0fd9
commit
8ab51d9f07
+260
-353
@@ -2,45 +2,82 @@
|
||||
|
||||
This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
|
||||
|
||||
> **Note:** There is also a `docs/CLAUDE.md` (older, hosted-only snapshot). This file at `.claude/CLAUDE.md` is the authoritative reference.
|
||||
> **Note:** There is also a `docs/CLAUDE.md` and `docs/formal/CLAUDE.md` — these govern the
|
||||
> two-tier documentation-authoring system (`docs/formal/` = press-ready LaTeX for
|
||||
> patent/SSRN/licensees, `docs/working/` = living drafts) and are still accurate; read them
|
||||
> if you're touching documentation build tooling. This file at `.claude/CLAUDE.md` is the
|
||||
> authoritative reference for everything else.
|
||||
|
||||
> **Tripod:** `.claude/TRIPOD.md` is authoritative for all Tripod VM (Hera/Hermes/Artemis) work. Read it completely before touching any Tripod code.
|
||||
> **Hermes:** `.claude/HERMES.md` is authoritative for all Hermes VM work. Read before touching Hermes.
|
||||
> **Artemis:** `.claude/ARTEMIS.md` is authoritative for all Artemis VM work. Read before touching Artemis.
|
||||
> **Artemis:** `.claude/ARTEMIS.md` is authoritative for all Artemis VM work. Read before touching Artemis. Note: Artemis is design-confirmed but **build-authorization deferred** as of this writing — see the "Build Status" section of that file before assuming it's live.
|
||||
|
||||
> **Scope:** This repo is LithosAnanke — the bare-metal UEFI kernel that boots StarForth
|
||||
> directly on hardware. StarForth (the hosted FORTH-79 VM) has its own separate repository
|
||||
> now. This repo vendors a full copy of the shared VM source (`src/vm.c`, `src/word_source/`,
|
||||
> `capsules/`, `proof/`) because LithosAnanke embeds it as its execution engine — that vendored
|
||||
> code is not a leftover or a second production target, it's load-bearing here. Kernel-specific
|
||||
> code lives in `src/starkernel/`.
|
||||
|
||||
---
|
||||
|
||||
## Hard Rules — Captain Bob's Law
|
||||
|
||||
- **NEVER CREATE A BRANCH WITHOUT EXPLICIT PERMISSION FROM THE USER.** Work on the branch you are given or already on. Do not create feature branches, session branches, or any other branch unless the user explicitly asks. This applies every time, not just once per session — re-confirm before creating a branch even if one was created earlier in the same conversation.
|
||||
- **NEVER WORK ON MASTER.** `master` is a production branch. All development happens on feature or integration branches. If you find yourself on master, stop and ask.
|
||||
- **BRANCH TOPOLOGY — know which production line you're on.** `master` (origin) is **StarForth** production (the hosted VM). `lithosananke` is **LithosAnanke** production (the bare-metal kernel), branched off `master` and diverging intentionally from it — see "On Tags" below. A task about StarKernel, capsules, Tripod/Hermes/Artemis, or anything bare-metal belongs on `lithosananke`, not on a branch cut from `master`. If a session's assigned branch doesn't have `.claude/ARTEMIS.md`, `.claude/HERMES.md`, `.claude/TRIPOD.md`, that is a signal you're on the wrong line — stop and confirm with the user before doing any further work, rather than proceeding against a stale/wrong-branch view of these instructions.
|
||||
- **NEVER STASH WITHOUT EXPLICIT PERMISSION.** `git stash` hides work and creates debt. If the working tree is dirty, report it and wait for instructions. Do not stash to work around a problem.
|
||||
- **NEVER APPLY A FIX NOT EXPLICITLY REQUESTED.** If you identify a bug, report it. Do not fix it unless the user says to. Initiative on code changes causes damage.
|
||||
- **USE A SUBVERSION-LIKE WORKFLOW.** Commit and push directly to the working branch. No detours, no side branches, no pull requests unless explicitly requested.
|
||||
- **USE A SUBVERSION-LIKE WORKFLOW.** Commit and push directly to the working branch (including `master` — this repo works directly on `master`; see below). No detours, no side branches, no pull requests unless explicitly requested.
|
||||
- **AFTER ANY OUT-OF-BRANCH WORK** (switching branches, resetting, fetching, etc.) always return to the correct working branch and do a full `git fetch` + `git pull` to ensure the working tree is clean and current before continuing.
|
||||
- **ALWAYS START CLEAN.** Before doing any work, verify `git status` is clean and the branch is the correct one. No surprises.
|
||||
- **ANNOUNCE THE BRANCH** at the start of every session resumption. First line of output after context load: state the current branch and last commit.
|
||||
|
||||
### On the branch topology (post-split)
|
||||
|
||||
This repo used to be a `lithosananke` branch inside the combined StarForth/LithosAnanke
|
||||
monorepo, diverging from a `master` that carried StarForth's hosted-VM production line.
|
||||
That monorepo has been split into two separate repositories. **In this repo, `master` is now
|
||||
the sole LithosAnanke production line — there is no `lithosananke` branch here, and none is
|
||||
needed.** Don't look for one, and don't recreate the old two-branch framing when reasoning
|
||||
about "which line am I on."
|
||||
|
||||
---
|
||||
|
||||
## Lessons Learned — Hard-Won in the Field
|
||||
|
||||
### On Tags
|
||||
- **Tags are sacred ground.** Each tag has logs attached proving its state. When in doubt about the correct state of any file or branch, look at the tag first. `git show <tag>` and `git log <tag>` are your oracle.
|
||||
- **Two same-day tags = two production targets.** `v3.1.0` = StarForth hosted (master). `v1.5.3` = LithosAnanke bare metal (lithosananke). They diverge intentionally.
|
||||
|
||||
### On the FORTH Dictionary
|
||||
- **BIRTH, RUN, USE are primitives** — registered in C exactly like DUP, BYE, EXEC. Use `' BIRTH` directly. Never reach for FIND, never add conditionals, never rename them to `CAPSULE-BIRTH` or anything else.
|
||||
- **FIND is a proven, tested, registered word. Never modify it.** The implementation is intentionally non-standard (parses from input stream). It is tested. Leave it alone.
|
||||
- **Never modify a registered, tested word to "fix" it.** If something seems wrong with a word, the problem is almost certainly in the caller, not the word.
|
||||
- **ACL policy belongs in `ACL.4th`, never in C.** No policy logic in `kernel_main.c`, no `vm_find_word` + field assignment for pinning. Use `' WORD ACL-PIN` in FORTH exactly as IMMEDIATE works.
|
||||
- **`' BIRTH` in shared capsules breaks the hosted build** — BIRTH is kernel-only. Pin it in a kernel-specific capsule, not in `ACL.4th` which is shared.
|
||||
- **`' BIRTH` in shared capsules breaks the hosted build** — BIRTH is kernel-only. Pin it in a kernel-specific capsule, not in `ACL.4th` which is shared. `capsules/ACL.4th` itself documents this exclusion in a comment (line ~64) — it deliberately omits `BIRTH`/`CAPSULE-BIRTH` even though this IS the kernel repo, because `ACL.4th` is meant to stay portable/shared.
|
||||
|
||||
### On the Two Production Targets
|
||||
- **Every change to shared VM code must compile and behave on both targets.** `src/vm.c`, `include/vm.h`, `capsules/`, `src/word_source/` are shared. Gate with `#ifdef __STARKERNEL__` or `#ifdef STARFORTH_ENABLE_VM`.
|
||||
- **The only valid acceptance test is the three-arch QEMU boot** (see QEMU section below). Tests run automatically at binary startup — no separate test target exists.
|
||||
- **`INPUT_BUFFER_SIZE` must be 1025.** `vm_interpret()` is the shared dispatch path for BOTH interactive REPL lines AND block content from LOAD. LOAD copies up to 1024 bytes from block RAM and calls `vm_interpret()` directly; with a 256-byte cap, everything past byte 255 is silently dropped. 1025 = 1024 content bytes + 1 NUL terminator.
|
||||
### On the Embedded VM vs. the Kernel
|
||||
- **`src/vm.c`, `include/vm.h`, `capsules/`, `src/word_source/` are the shared/vendored VM
|
||||
source.** They must compile and behave correctly both standalone (bare `make` here still
|
||||
produces a plain hosted `starforth` binary for quick local sanity checks) and embedded in
|
||||
the kernel build. Gate kernel-only code with `#ifdef __STARKERNEL__` or
|
||||
`#ifdef STARFORTH_ENABLE_VM`.
|
||||
- **The vendored VM source has diverged from the standalone StarForth repo's copy** — it is
|
||||
not a byte-identical mirror. This repo's `src/word_source/` has 31 files (StarForth's has
|
||||
26); the extras (`defer_words.c`, `inference_words.c`, `lifecycle_words_hosted.c`,
|
||||
`log_words.c`, `q48_words.c`) are kernel-side-only additions. Don't assume a fix made in
|
||||
the StarForth repo needs to be, or even can be cleanly, ported here — check first.
|
||||
Similarly `src/starkernel/` here is real and load-bearing (~74 files across arch/boot/
|
||||
capsule/hal/memory/math/hash/pci/virtio/vm subtrees) — much larger than older docs claimed.
|
||||
- **`src/*.c.bak` files (`vm.c.bak`, `doe_metrics.c.bak`, `inference_engine.c.bak`) are
|
||||
tracked in git at the `src/` top level.** This looks like repo hygiene debt, not
|
||||
intentional. Report it if it comes up; don't delete unprompted.
|
||||
- **There is no `make test` target in this repo's hosted `Makefile`** (unlike the standalone
|
||||
StarForth repo, which has one). Don't invent one. The only acceptance authority for kernel
|
||||
changes is the three-arch QEMU boot (see below); bare `make` here is for quick compile
|
||||
sanity on the vendored source only, not test execution.
|
||||
- **`INPUT_BUFFER_SIZE` must be 1025.** `vm_interpret()` is the shared dispatch path for BOTH
|
||||
interactive REPL lines AND block content from LOAD. LOAD copies up to 1024 bytes from block
|
||||
RAM and calls `vm_interpret()` directly; with a 256-byte cap, everything past byte 255 is
|
||||
silently dropped. 1025 = 1024 content bytes + 1 NUL terminator.
|
||||
|
||||
### On Working Style
|
||||
- **When told to stop, stop immediately.** Do not make one more change. Do not commit "just to clean up". Stop.
|
||||
@@ -51,12 +88,13 @@ This file provides guidance to Claude Code (claude.ai/code) when working with co
|
||||
|
||||
---
|
||||
|
||||
## Word-Level ACL System — Complete through Phase 7
|
||||
## Word-Level ACL System — Complete through Phase 7 (independently verified)
|
||||
|
||||
**Design doc:** `docs/03-architecture/word-acl/DESIGN.md`
|
||||
**Design doc:** `docs/03-architecture/word-acl/DESIGN.md` (this repo kept the old-style
|
||||
`docs/03-architecture/` tree alongside the newer `docs/formal/`/`docs/working/` restructure —
|
||||
both exist here; this path is still current for ACL specifically).
|
||||
|
||||
The word-level ACL system is fully implemented and validated. Read the design
|
||||
doc before touching any ACL-related code. Key constraints:
|
||||
The word-level ACL system is fully implemented, including kernel parity. Key constraints:
|
||||
|
||||
- All policy logic in `ACL.4th` — no new C primitives for policy
|
||||
- Four C fields: `acl_ttl` + `acl_allow` + `acl_mode` + `acl_pinned` in `DictEntry`
|
||||
@@ -72,127 +110,126 @@ doc before touching any ACL-related code. Key constraints:
|
||||
2. ✅ `ACL.4th` — FORTH policy words + `ACL-INIT-PRIMITIVES` + self-activation
|
||||
3. ✅ `capsules/zuse.4th` — bootstrap superuser skeleton; CA root placeholder in `ACL.4th`
|
||||
4. ✅ `init.4th` opt-in toggle — `\ S" ACL.4th" EXEC` (comment out = no security)
|
||||
5. ✅ POST tests (800/800) + Isabelle/HOL proofs (5 theory files)
|
||||
5. ✅ POST tests + Isabelle/HOL proofs (5 `ACL_*.thy` theory files)
|
||||
6. ✅ `EMERGENCY_CONSOLE_ENABLED` build flag + `vm_fault_handler` extension point
|
||||
7. ✅ LithosAnanke parity — kernel ACL hook wired; all three ISAs boot to `zuse)ok>` (confirmed in log)
|
||||
8. ⬜ PKI / thumbdrive — Ed25519 challenge-response; user minting by zuse
|
||||
7. ✅ LithosAnanke kernel parity — **independently verified present in current `master`**:
|
||||
`acl_recheck()`/`zuse_session`/`emergency_console` wiring confirmed in
|
||||
`src/starkernel/vm/vm_core.c` (~lines 549, 608–633, 747–749, 906–908); the
|
||||
per-iteration `emergency_console = zuse_session ? 0 : 1` assignment confirmed in
|
||||
`src/starkernel/repl.c` (~lines 174, 219); the old `!vm->zuse_session` ACL-check bypass
|
||||
confirmed **absent** from `src/vm.c`. (The `feature/acl-rwt` branch this work was
|
||||
apparently done on is not traceable in `git log --all` — likely squash-merged without
|
||||
preserving the ref. The code is real and verified; the branch name is not.)
|
||||
8. ⬜ PKI / thumbdrive — Ed25519 challenge-response; user minting by zuse. **This is the open
|
||||
item — pick up here next.**
|
||||
|
||||
**Bug resolutions (all fixed, branch `feature/acl-rwt`):**
|
||||
- Bug 1 ✅: Kernel ACL interpreter hook ported to `src/starkernel/vm/vm_core.c`
|
||||
- Bug 2 ✅: `emergency_console` set per-iteration in `src/starkernel/repl.c` (`zuse_session ? 0 : 1`)
|
||||
- Bug 3 ✅: `!vm->zuse_session` bypass removed from `src/vm.c` ACL checks
|
||||
**ACL-RWT DoE campaign (June 15–16 2026):**
|
||||
- 3×3 Latin square: 3 seeds × amd64/aarch64/riscv64, 30 reps each
|
||||
- Measured overhead: +0.0054%–+0.0088% across all 9 cells; CV = 0.000%
|
||||
- Report confirmed to exist: `experiments/bare_metal/analysis/report/bare_metal_doe_report.pdf`
|
||||
(~2MB, with LaTeX source and figures) — patent support material
|
||||
|
||||
**ACL-RWT DoE campaign (branch `feature/acl-rwt`, June 15–16 2026):**
|
||||
- 3×3 Latin square: seeds 12345/67890/13579 × amd64/aarch64/riscv64, 30 reps each
|
||||
- This IS the first true ACL-active campaign (Bug 1 fixed before runs)
|
||||
- Results: +0.0054%–+0.0088% overhead across all 9 cells; CV = 0.000%
|
||||
- ISA gap closed: ACL-RWT vs Floor=16 is three orders of magnitude improvement
|
||||
- Baseline (no ACL): amd64=261,098 ticks; aarch64/riscv64=261,095 ticks
|
||||
- Report: `experiments/bare_metal/analysis/report/bare_metal_doe_report.pdf` (19 pages)
|
||||
- 5 R-generated vector figure pairs (10 SVGs via ggplot2/svglite)
|
||||
- All data from confirmed measured tick counts — patent support material
|
||||
|
||||
**Pick up here next session:**
|
||||
1. Phase 8 — PKI / Ed25519 thumbdrive (challenge-response; user minting by zuse)
|
||||
**Before writing or modifying any `.4th` capsule file**, read `experiments/bare_metal/README.md`
|
||||
in full. The block namespace is shared across all loaded capsules; violations cause silent
|
||||
word-definition collisions and corrupt the DoE. Block ranges (spot-checked against real
|
||||
capsule files — accurate):
|
||||
- `2048–2099` — `init.4th` only
|
||||
- `2100–2199` — `doe.4th` only
|
||||
- `3000–3999` — workload capsules
|
||||
- `4000+` — user-defined capsules (`ACL.4th` uses 4000–4015, `zuse.4th` uses 4016–4018)
|
||||
Each block header line counts against the 1024-byte limit. Any block exceeding 1024 bytes
|
||||
is truncated silently at load time — verify with `wc -c` before committing.
|
||||
|
||||
---
|
||||
|
||||
## Project Overview
|
||||
|
||||
StarForth is a FORTH-79 compliant virtual machine written in strict ANSI C99,
|
||||
featuring a physics-driven adaptive runtime. It is the primary execution engine
|
||||
for **StarshipOS** and runs standalone on Linux and bare metal via
|
||||
**LithosAnanke** (StarKernel). (HISTORICAL: L4Re/Fiasco.OC was a supported
|
||||
platform target through mid-2026; removed as an active target.)
|
||||
LithosAnanke ("stone" + "necessity") is a UEFI-bootable bare-metal microkernel that boots
|
||||
directly from firmware, initializes memory and interrupts, then runs StarForth — a FORTH-79
|
||||
virtual machine with a physics-driven adaptive runtime (Compudynamics) — as its sole
|
||||
userspace runtime. No libc, no traditional OS underneath. It is the bare-metal target under
|
||||
**StarshipOS**. (HISTORICAL: L4Re/Fiasco.OC was a supported platform target through mid-2026;
|
||||
removed as an active target.)
|
||||
|
||||
**Current status: M7.1** — capsule birth protocol, Mama FORTH vocabulary, Tripod multi-VM
|
||||
fleet (Hera/Hermes/Artemis), and word-level ACL (Phases 1–7) are live; POST at boot verifies
|
||||
parity hash across amd64/aarch64/riscv64 with a 453-word Mama capsule dictionary.
|
||||
|
||||
**Key distinguishing features:**
|
||||
|
||||
- Physics-grounded self-adaptive runtime with formally proven deterministic behavior
|
||||
(0% algorithmic variance across 90 experimental runs)
|
||||
- 7 feedback loops driving runtime optimization while preserving determinism
|
||||
- Formally verified with 19 Isabelle/HOL theory files covering all loops and word categories
|
||||
- Bare-metal UEFI kernel (LithosAnanke v1.5.3) enabling native execution without Linux
|
||||
- Patent pending on adaptive runtime mechanisms
|
||||
- Published SSRN paper: `papers/James_Steady-State_Convergence_Adaptive_Runtime.pdf`
|
||||
|
||||
**Technology stack:**
|
||||
|
||||
```
|
||||
┌─────────────────────────────────────────────────────────────────┐
|
||||
│ StarshipOS (future — self-hosting OS) │
|
||||
├─────────────────────────────────────────────────────────────────┤
|
||||
│ LithosAnanke v1.5.3) │
|
||||
│ ← Milestones M0–M6 complete; M7 VM integration in progress → │
|
||||
├─────────────────────────────────────────────────────────────────┤
|
||||
│ StarForth v3.1.0 (FORTH-79 VM + physics-driven adaptive RT) │
|
||||
├───────────────────────────┬─────────────────────────────────────┤
|
||||
│ Linux │ Bare metal (amd64, aarch64, riscv) │
|
||||
└───────────────────────────┴─────────────────────────────────────┘
|
||||
```
|
||||
- Embeds StarForth's physics-grounded self-adaptive runtime — 7 feedback loops + L8 Jacquard
|
||||
mode selector, formally proven deterministic (0.000% CV across 90 experimental runs)
|
||||
- Content-addressed, immutable **capsules** as the primary organizational unit — no dynamic
|
||||
allocator in the traditional sense; identity is a content hash (XXHash64), mutation
|
||||
produces a new capsule
|
||||
- **Tripod** — a named multi-VM fleet (Hera the Mama VM, two Hermes instances, Artemis)
|
||||
that births, runs, and re-births independently; verified booting live pre-REPL on all
|
||||
three architectures. See `.claude/TRIPOD.md`, `.claude/HERMES.md`, `.claude/ARTEMIS.md`.
|
||||
- Word-level ACL security system with kernel parity (see above) — measured overhead three
|
||||
orders of magnitude below the measurement floor
|
||||
- Kconfig-based build configuration (~40 discoverable symbols spanning physics/heartbeat/
|
||||
pipelining/kernel-only knobs), shared between the hosted and kernel build
|
||||
- Patent pending (USPTO provisional, December 2025)
|
||||
|
||||
---
|
||||
|
||||
## Build Commands
|
||||
|
||||
### StarForth VM (hosted)
|
||||
### Kernel (primary)
|
||||
|
||||
```bash
|
||||
# Standard optimized build (auto-detects architecture)
|
||||
make
|
||||
|
||||
# Maximum performance build (ASM + LTO + direct threading)
|
||||
make fastest
|
||||
|
||||
# Profile-guided optimization build
|
||||
make pgo
|
||||
|
||||
# Debug build with symbols
|
||||
make debug
|
||||
|
||||
# Quick benchmark
|
||||
make bench
|
||||
|
||||
# Clean build artifacts
|
||||
make clean
|
||||
```
|
||||
|
||||
### StarKernel / LithosAnanke (bare metal)
|
||||
|
||||
```bash
|
||||
# Build UEFI kernel (amd64, requires cross toolchain or native gcc)
|
||||
make -f Makefile.starkernel
|
||||
|
||||
# Build for aarch64
|
||||
# Build kernel for a given architecture (amd64 default)
|
||||
make -f Makefile.starkernel ARCH=amd64
|
||||
make -f Makefile.starkernel ARCH=aarch64
|
||||
|
||||
# Build for riscv64
|
||||
make -f Makefile.starkernel ARCH=riscv64
|
||||
|
||||
# Run in QEMU with OVMF
|
||||
make -f Makefile.starkernel qemu
|
||||
make -f Makefile.starkernel ARCH=aarch64 qemu
|
||||
make -f Makefile.starkernel ARCH=riscv64 qemu
|
||||
|
||||
# Enable VM integration (M7)
|
||||
make -f Makefile.starkernel STARFORTH_ENABLE_VM=1
|
||||
# Clean
|
||||
make -f Makefile.starkernel clean
|
||||
```
|
||||
|
||||
Output: `build/amd64/kernel/starkernel_loader.efi` (UEFI PE32+ executable)
|
||||
Output: `build/<arch>/kernel/starkernel_loader.efi` + `build/<arch>/kernel/starkernel_kernel.elf`.
|
||||
|
||||
### Build Targets and Architectures
|
||||
Two independently tracked version strings flow into the generated `include/version.h`:
|
||||
`VERSION` (`Makefile.starkernel` — the embedded StarForth engine version, currently `3.1.0`;
|
||||
note this does **not** auto-sync with the standalone StarForth repo's own version) and
|
||||
`LITHOS_VERSION` (`Makefile.starkernel` — the kernel version, currently `1.5.3`).
|
||||
|
||||
- `TARGET=standard|fast|fastest|turbo|pgo` - VM build profiles
|
||||
- `ARCH=x86_64|amd64|aarch64|arm64|raspi|riscv64` - Target architecture
|
||||
- Cross-compile for Raspberry Pi: `make rpi4-cross`
|
||||
### Build configuration (Kconfig — real, wired, not vestigial)
|
||||
|
||||
### Key Build Flags
|
||||
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`,
|
||||
`Kconfig.heartbeat`, `Kconfig.kernel`, `Kconfig.physics`, `Kconfig.variant` (~40 symbols
|
||||
total). `Makefile.starkernel` pulls its defaults from this system via a `kconfig_bool(...)`
|
||||
mechanism — e.g. `STARFORTH_ENABLE_VM` defaults to **1** (confirmed at
|
||||
`Makefile.starkernel:61`), meaning a plain `make -f Makefile.starkernel` already builds with
|
||||
VM + capsule-birth + ACL active. A bare invocation uses the defaults it always has:
|
||||
|
||||
- `STRICT_PTR=1` - Enforce pointer safety checks (default on)
|
||||
- `USE_ASM_OPT=1` - Enable architecture-specific assembler optimizations
|
||||
- `ENABLE_HOTWORDS_CACHE=1` - Physics-driven hot-words cache (default on)
|
||||
- `ENABLE_PIPELINING=1` - Speculative execution via word transition prediction (default on)
|
||||
- `HEARTBEAT_THREAD_ENABLED=1` - Background heartbeat thread for adaptive tuning (default on)
|
||||
- `STARFORTH_ENABLE_VM=1` - Enable VM integration in StarKernel (M7)
|
||||
- `PARITY_MODE=1` - Deterministic parity harness mode
|
||||
- `EMERGENCY_CONSOLE_ENABLED=1` - Interactive fault handler / error recovery REPL (default on; set 0 for production or embedded builds to strip interactive fallthrough surface)
|
||||
```bash
|
||||
make -f Makefile.starkernel ARCH=amd64 menuconfig
|
||||
make -f Makefile.starkernel ARCH=amd64 kernel_amd64_defconfig
|
||||
```
|
||||
|
||||
### Hosted VM (vendored, for local sanity only)
|
||||
|
||||
```bash
|
||||
make # builds a standalone hosted `starforth` binary from the vendored source
|
||||
make clean
|
||||
```
|
||||
|
||||
There is **no `make test` here** — this is a compile-sanity convenience only, not a test
|
||||
runner. Don't advertise it as one. `bump-z`/`bump-y` targets exist in this Makefile
|
||||
(mirroring the standalone StarForth repo) but are **broken the same way**: they reference
|
||||
`STARFORTH_VERSION_MAJOR`/`MINOR`/`PATCH`/`STARFORTH_VERSION_STRING` fields that don't exist
|
||||
in the actual generated `include/version.h` (which only has `STARFORTH_VERSION`,
|
||||
`STARFORTH_ARCH`, `STARFORTH_TARGET`, `STARFORTH_TIMESTAMP`, `STARFORTH_VERSION_FULL`,
|
||||
`LITHOS_VERSION`, `LITHOS_VERSION_STR`). Bump versions by hand-editing the `VERSION`/
|
||||
`LITHOS_VERSION` variables in `Makefile.starkernel` instead. Report the broken targets if
|
||||
asked, don't silently fix them.
|
||||
|
||||
### Important: Linker Configuration
|
||||
|
||||
@@ -201,30 +238,14 @@ The `fastest` target uses `-flto=auto -fuse-linker-plugin` instead of plain `-fl
|
||||
|
||||
---
|
||||
|
||||
## Running
|
||||
|
||||
```bash
|
||||
./build/amd64/standard/starforth # Interactive REPL
|
||||
./build/amd64/standard/starforth --run-tests # Run tests then REPL
|
||||
./build/amd64/standard/starforth -c "1 2 + . BYE" # Execute inline code
|
||||
```
|
||||
|
||||
### DoE (Design of Experiments) Mode
|
||||
|
||||
```bash
|
||||
./build/amd64/fastest/starforth --doe
|
||||
```
|
||||
|
||||
The `--doe` flag runs the full test harness. The CSV metrics row has been **suppressed**
|
||||
as of 2025-12-08 (redundant with internal VM metrics). See `src/main.c:390-396`.
|
||||
To re-enable, add a `--csv-export` flag or write to a file.
|
||||
## Running / Acceptance
|
||||
|
||||
### Kernel via QEMU
|
||||
|
||||
**ACCEPTANCE CRITERIA — non-negotiable:**
|
||||
The ONLY valid acceptance test for any kernel change is booting all three
|
||||
architectures in QEMU and capturing the serial log. There is no other test.
|
||||
`make test` (hosted VM) is NEVER used to validate kernel changes.
|
||||
The vendored hosted `make` build (above) is NEVER used to validate kernel changes.
|
||||
|
||||
```bash
|
||||
# Run in this exact order for every kernel change:
|
||||
@@ -244,16 +265,25 @@ TCG and is the most likely to outlast a silent interval. Captain Bob must stay e
|
||||
during long runs (30-rep DoE ≈ 25–30 min per ISA).
|
||||
|
||||
Always pass `clean` before `qemu` — never build-only without clean.
|
||||
Serial output is automatically captured to:
|
||||
```
|
||||
logs/YYYYMMDD-HHMMSS/amd64/qemu-amd64-YYYYMMDD-HHMMSS.log
|
||||
logs/YYYYMMDD-HHMMSS/aarch64/qemu-aarch64-YYYYMMDD-HHMMSS.log
|
||||
logs/YYYYMMDD-HHMMSS/riscv64/qemu-riscv64-YYYYMMDD-HHMMSS.log
|
||||
```
|
||||
These logs are audit artifacts — they are committed to the repo. Do not delete them.
|
||||
Serial output is automatically captured to
|
||||
`logs/YYYYMMDD-HHMMSS/<arch>/qemu-<arch>-YYYYMMDD-HHMMSS.log` — confirmed to be the real,
|
||||
current convention (real timestamped log directories exist under `logs/`). These logs are
|
||||
audit artifacts — they are committed to the repo. Do not delete them. There is also a
|
||||
`logs2/` directory — a flatter, older archive predating or running parallel to the
|
||||
timestamped convention (self-documented via its own README); not a contradiction, just a
|
||||
second, less-structured log location.
|
||||
|
||||
Do not claim a change is accepted until all three architectures have booted
|
||||
to `zuse)ok>` and their logs are present in `logs/`.
|
||||
|
||||
### CI
|
||||
|
||||
`.gitea/workflows/build.yml` runs three parallel jobs, each building a real bootable
|
||||
artifact (not just compiling): `build-amd64-iso` (kernel build + El Torito ISO),
|
||||
`build-aarch64-iso` (same, ARM boot file naming), `build-riscv64-img` (kernel build + raw
|
||||
GPT/FAT32 disk image — riscv64 virt doesn't support El Torito ISO or `-bios` QEMU mode, so
|
||||
it ships a raw disk image instead). No QEMU boot step in CI — artifact packaging only.
|
||||
|
||||
---
|
||||
|
||||
## Architecture
|
||||
@@ -262,130 +292,87 @@ to `zuse)ok>` and their logs are present in `logs/`.
|
||||
|
||||
```
|
||||
src/
|
||||
├── main.c # Entry point, CLI, VM init, DoE mode
|
||||
├── vm.c # Interpreter loop, stacks, dictionary state
|
||||
├── vm_api.c # External VM API
|
||||
├── vm_bootstrap.c # VM bootstrap initialization
|
||||
├── vm_debug.c # Debugging utilities
|
||||
├── vm_time.c # Time-related VM operations
|
||||
├── repl.c # REPL read-eval-print loop
|
||||
├── cli.c # CLI parsing
|
||||
├── io.c # I/O operations
|
||||
├── log.c # Logging infrastructure
|
||||
├── memory_management.c # Dictionary allocator
|
||||
├── dictionary_management.c # Dictionary allocation & search
|
||||
├── dictionary_heat_optimization.c # Heat tracking (Loop #1)
|
||||
├── word_registry.c # Word registration system
|
||||
├── block_subsystem.c # Logical→physical block mapper
|
||||
├── blkio_*.c # Block I/O backends (file, RAM, factory)
|
||||
├── stack_management.c # Stack operations
|
||||
├── math_portable.c # Portable math functions
|
||||
├── profiler.c # Performance profiling
|
||||
├── heartbeat_export.c # Heartbeat metrics export
|
||||
├── ssm_jacquard.c # L8 Jacquard steady-state machine
|
||||
├── doe_metrics.c # Design of Experiments metrics (2^7 factorial)
|
||||
├── main.c, vm.c, vm_api.c, vm_bootstrap.c, vm_debug.c, vm_time.c # Vendored VM core (see below)
|
||||
├── repl.c, cli.c, io.c, log.c # Vendored VM core
|
||||
├── memory_management.c, dictionary_management.c, block_subsystem.c, blkio_*.c
|
||||
├── stack_management.c, math_portable.c, profiler.c, compudynamics.c
|
||||
├── heartbeat_export.c, ssm_jacquard.c, doe_metrics.c
|
||||
├── physics_runtime.c, physics_hotwords_cache.c, physics_metadata.c,
|
||||
│ physics_pipelining_metrics.c, physics_execution_hooks.c,
|
||||
│ rolling_window_of_truth.c, inference_engine.c # 7 feedback loops
|
||||
├── vm.c.bak, doe_metrics.c.bak, inference_engine.c.bak # tracked but stale — flag, don't delete unprompted
|
||||
│
|
||||
├── Physics Engine (7 Feedback Loops):
|
||||
├── physics_runtime.c # Main physics coordinator
|
||||
├── physics_hotwords_cache.c # Loop #1: Hot-words caching
|
||||
├── physics_metadata.c # Metadata tracking
|
||||
├── physics_pipelining_metrics.c # Loop #4: Word transition prediction
|
||||
├── physics_execution_hooks.c # Execution instrumentation
|
||||
├── rolling_window_of_truth.c # Loop #2: Circular execution history
|
||||
├── inference_engine.c # Loops #5/#6: ANOVA + statistical inference
|
||||
├── word_source/ # 31 files (vendored StarForth word_source PLUS
|
||||
│ │ # kernel-side-only additions)
|
||||
│ ├── (all of StarForth's 26: arithmetic, stack, control, defining, memory,
|
||||
│ │ return_stack, double, logical, io, string, block, editor, format, system,
|
||||
│ │ dictionary, dictionary_manipulation, dictionary_heat_diagnostic, vocabulary,
|
||||
│ │ q48_16, starforth, acl, physics_benchmark, physics_diagnostic,
|
||||
│ │ physics_freeze, physics_pipelining_diagnostic, mixed_arithmetic)
|
||||
│ └── kernel-only additions: defer_words.c, inference_words.c,
|
||||
│ lifecycle_words_hosted.c, log_words.c, q48_words.c
|
||||
│
|
||||
├── word_source/ # 25 FORTH-79 word implementation files
|
||||
│ ├── arithmetic_words.c # + - * / MOD ABS MIN MAX
|
||||
│ ├── stack_words.c # DUP DROP SWAP ROT OVER NIP TUCK
|
||||
│ ├── control_words.c # IF ELSE THEN DO LOOP BEGIN UNTIL WHILE
|
||||
│ ├── defining_words.c # : ; CREATE DOES> VARIABLE CONSTANT
|
||||
│ ├── memory_words.c # @ ! C@ C! MOVE FILL
|
||||
│ ├── return_stack_words.c # >R R> R@ RDROP 2>R 2R@ 2R>
|
||||
│ ├── double_words.c # 2DUP 2DROP 2SWAP 2@ 2! D+ D-
|
||||
│ ├── logical_words.c # AND OR XOR NOT INVERT LSHIFT RSHIFT
|
||||
│ ├── io_words.c # EMIT KEY TYPE CR TAB SPACE ACCEPT
|
||||
│ ├── string_words.c # S" SLITERAL string operations
|
||||
│ ├── block_words.c # BLOCK BUFFER LOAD THRU FLUSH
|
||||
│ ├── format_words.c # .( .R .S HEX DECIMAL BASE
|
||||
│ ├── system_words.c # BYE ABORT INCLUDE STATE
|
||||
│ ├── dictionary_words.c # FIND SEARCH-WORDLIST WORDS
|
||||
│ ├── vocabulary_words.c # VOCABULARY DEFINITIONS FORTH-WORDLIST
|
||||
│ ├── q48_16_words.c # Q48.16 fixed-point word definitions
|
||||
│ ├── starforth_words.c # StarForth-specific extensions
|
||||
│ ├── physics_benchmark_words.c # Benchmark harness (L1-L7)
|
||||
│ ├── physics_diagnostic_words.c # Physics diagnostics (WORD-ENTROPY)
|
||||
│ ├── physics_freeze_words.c # PHYSICS-FREEZE / PHYSICS-THAW
|
||||
│ └── physics_pipelining_diagnostic_words.c
|
||||
├── test_runner/ # 23 test module files (matches StarForth's count)
|
||||
│
|
||||
├── test_runner/ # 936+ test cases
|
||||
│ ├── test_runner.c # Test harness orchestration
|
||||
│ ├── test_common.c # Shared test utilities
|
||||
│ ├── test_contracts.c # Contract-based testing
|
||||
│ └── modules/ # 22 per-category test files
|
||||
│ ├── arithmetic_words_test.c
|
||||
│ ├── stack_words_test.c ... (22 files, incl. integration & stress)
|
||||
├── platform/ # Platform abstraction (hosted build)
|
||||
│
|
||||
├── platform/ # Platform abstraction (hosted)
|
||||
│ ├── linux/time.c # POSIX timing
|
||||
│ └── l4re/time.c # HISTORICAL: L4Re timing, no longer wired into any build
|
||||
│
|
||||
└── starkernel/ # LithosAnanke bare-metal kernel (37 files)
|
||||
├── kernel_main.c # Kernel entry point (M0–M7 milestones)
|
||||
└── starkernel/ # ~74 files — the real, load-bearing kernel tree
|
||||
├── kernel_main.c # Kernel entry point (M0–M9 milestones)
|
||||
│ # NOTE: this file's own header comment claims
|
||||
│ # "M7: Not started" — that comment is STALE;
|
||||
│ # M7/M7.1/M7.pre logic is present and functional
|
||||
│ # (kernel_main.c ~lines 481–517). Don't propagate
|
||||
│ # the stale comment.
|
||||
├── repl.c # Kernel REPL
|
||||
├── arch/amd64/ # AMD64: arch.c apic.c timer.c interrupts.c boot.S isr.S
|
||||
├── arch/{amd64,aarch64,riscv64}/ # Per-arch: arch.c apic.c timer.c interrupts.c boot.S isr.S
|
||||
├── boot/ # uefi_loader.c elf_loader.c reloc_stub.c reloc.S
|
||||
├── capsule/ # capsule_birth.c capsule_run.c capsule_loader.c
|
||||
│ # capsule_find.c capsule_validate.c capsule_vm_hooks.c
|
||||
│ # mama_forth_words.c
|
||||
│ # capsule_vm_physics.c mama_forth_words.c
|
||||
├── hal/ # hal.c console.c memory.c host_services.c
|
||||
│ # framebuffer.c vt100.c font_8x16.c (VT100 console — live)
|
||||
├── pci/pci.c # PCI enumeration
|
||||
├── virtio/virtio_blk.c # virtio block device (relates to roadmap's "M9 block
|
||||
│ # storage" item — implemented via virtio, not AHCI as
|
||||
│ # older docs describe; don't assume milestone-complete
|
||||
│ # from source presence alone, that hasn't been verified)
|
||||
├── memory/ # kmalloc.c pmm.c vmm.c
|
||||
├── math/q48_16.c # Q48.16 fixed-point (kernel build)
|
||||
├── hash/xxhash64.c # XXHash64 (content addressing)
|
||||
├── doe_log.c
|
||||
└── vm/ # Kernel VM subsystem
|
||||
├── bootstrap/sk_vm_bootstrap.c
|
||||
├── host/shim.c
|
||||
├── vm_core.c vm_runtime.c vm_bootstrap.c
|
||||
├── vm_core.c vm_runtime.c vm_bootstrap.c q48_stubs.c
|
||||
├── parity.c # Birth/execution parity logging
|
||||
├── arena.c # Capsule arena allocator
|
||||
└── alloc_kernel.c
|
||||
```
|
||||
|
||||
### LithosAnanke / StarKernel
|
||||
### Boot sequence
|
||||
|
||||
LithosAnanke ("stone inevitability") is the bare-metal UEFI kernel that boots
|
||||
StarForth directly on hardware. Version **1.5.3**, monolithic UEFI PE32+ executable.
|
||||
|
||||
**Boot sequence:**
|
||||
```
|
||||
UEFI Firmware → uefi_loader.c (BOOTX64.EFI)
|
||||
UEFI Firmware → uefi_loader.c (BOOTX64.EFI / BOOTAA64.EFI / BOOTRISCV64.EFI)
|
||||
ExitBootServices() → owns hardware
|
||||
BootInfo{memory map, ACPI, framebuffer}
|
||||
→ kernel_main()
|
||||
M1: Console init (UART 16550 + framebuffer)
|
||||
M2: PMM (physical memory manager, bitmap)
|
||||
M3: VMM (4-level x86_64 paging)
|
||||
M4: IDT + APIC interrupts
|
||||
M5: TSC + HPET + APIC timer (100 Hz heartbeat)
|
||||
M3: VMM (4-level paging)
|
||||
M4: IDT + APIC/interrupt controller
|
||||
M5: Timer + heartbeat
|
||||
M6: kmalloc heap
|
||||
M7: StarForth VM bootstrap + capsule loading → "ok" REPL
|
||||
M7/M7.1: StarForth VM bootstrap + capsule birth (Tripod fleet) + word-level ACL
|
||||
→ "ok>" / "zuse)ok>" REPL
|
||||
```
|
||||
|
||||
**Milestone status (as of v1.5.3):**
|
||||
- ✅ M0–M5: complete (verified with QEMU/OVMF, three-arch tested)
|
||||
- ✅ M6: kmalloc infrastructure present (full validation deferred)
|
||||
- 🔄 M7: VM integration in progress (capsule execution pipeline partially wired)
|
||||
|
||||
**Kernel memory layout:**
|
||||
- Kernel heap: 16 MB (`kmalloc`)
|
||||
- Block RAM (LBN 0–991): 1 MB dedicated RAM blocks
|
||||
- Kernel ramdrive (LBN 2048–3071): 1 MB for capsule loading
|
||||
- LBN 2048 = entry point for `init.4th`
|
||||
|
||||
**LinkerScripts in `linker/`:**
|
||||
- `starkernel-loader-amd64.ld` — UEFI loader
|
||||
- `starkernel-loader-amd64-pe.ld` — PE32+ format
|
||||
- `starkernel-kernel-amd64.ld` — ELF kernel (split build)
|
||||
- `starkernel-amd64.ld` — monolithic build
|
||||
**Milestone status:**
|
||||
- ✅ M0–M6: complete, v1.5.1-FINAL
|
||||
- ✅ M7: StarForth VM integration + parity validation, complete
|
||||
- 🔄 M7.1: capsule birth protocol · Mama FORTH vocabulary · Tripod fleet · word-level ACL —
|
||||
in progress (Phase 8 PKI is the open item, see ACL section above)
|
||||
- Planned: M8 (REPL keyboard input), M9 (block storage — see the virtio note above; source
|
||||
exists but milestone-complete status not independently verified here)
|
||||
|
||||
### Capsule System
|
||||
|
||||
@@ -401,28 +388,17 @@ ID is its XXHash64 content hash — any mutation is detectable.
|
||||
execute IDENTITY (capsule code) → execute PERSONALITY (block 1 from ramdrive)
|
||||
→ log parity record (VM ID + capsule hash + dict hash).
|
||||
|
||||
**Capsule files in `capsules/` (17 `.4th` files):**
|
||||
- `init.4th` — default Mama VM personality
|
||||
- `init-0.4th` through `init-9.4th` — numbered variants
|
||||
- `init-l8-{stable,volatile,diverse,temporal,transition,omni}.4th` — L8 Jacquard variants
|
||||
**Capsule files:** `capsules/` has 23 `.4th` files (the `mkcapsule` build tool reports "26
|
||||
capsule(s)" registered — some files apparently register more than one capsule entry; not
|
||||
further investigated). Includes `init.4th`, `init-0.4th`–`init-9.4th`,
|
||||
`init-l8-{stable,volatile,diverse,temporal,transition,omni}.4th`, plus `doe.4th`,
|
||||
`doe-campaign.4th`, `lib.4th`, `process.4th`, `ACL.4th`, `zuse.4th` — more than the 17 older
|
||||
docs claimed.
|
||||
|
||||
Tool `tools/mkcapsule.c` assembles `.4th` files into the binary capsule directory
|
||||
format (`capsule_generated.c`) baked into the kernel image.
|
||||
|
||||
**ACL capsules (implemented):**
|
||||
- `capsules/ACL.4th` — word-level ACL system; self-activating; contains CA root placeholder
|
||||
- `capsules/zuse.4th` — bootstrap superuser; loaded by `ACL.4th` at boot
|
||||
|
||||
**MANDATORY: Read before writing capsules.**
|
||||
Before writing or modifying any `.4th` capsule file, read `experiments/bare_metal/README.md`
|
||||
in full. The block namespace is shared across all loaded capsules; violations cause silent
|
||||
word-definition collisions and corrupt the DoE. Block ranges are:
|
||||
- `2048–2099` — `init.4th` only
|
||||
- `2100–2199` — `doe.4th` only
|
||||
- `3000–3999` — workload capsules
|
||||
- `4000+` — user-defined capsules (ACL.4th, zuse.4th, etc.)
|
||||
Each block header line counts against the 1024-byte limit. Any block exceeding 1024 bytes
|
||||
is truncated silently at load time — verify with `wc -c` before committing.
|
||||
format (`capsule_generated.c`) baked into the kernel image; it also regenerates
|
||||
`capsules/BLOCK_MAP.md` as a manifest (expect that file to show as modified after any
|
||||
kernel build — it's a generated artifact, not hand content).
|
||||
|
||||
### Physics-Driven Adaptive Runtime
|
||||
|
||||
@@ -436,109 +412,39 @@ Uses thermodynamic metaphors as modeling language (see `ONTOLOGY.md`):
|
||||
6. **Loop #6 — Decay Slope Inference** (`inference_engine.c`) — exponential regression
|
||||
7. **Loop #7 — Adaptive Heartrate** (`HeartbeatState`) — background tick coordinator
|
||||
|
||||
**L8 Jacquard Mode Selector** (`ssm_jacquard.c`) — additional steady-state machine layer
|
||||
that switches between mode configurations based on attractor bucket statistics. Modes:
|
||||
stable, volatile, diverse, temporal, transition, omni. Controlled by `vm->ssm_l8_state`.
|
||||
|
||||
All loops are independently togglable via Makefile build flags.
|
||||
|
||||
### Key Data Structures (`include/vm.h`)
|
||||
|
||||
- **`VM` struct** — entire VM state: stacks, dictionary, memory, physics, heartbeat, SSM
|
||||
- **`DictEntry`** — `execution_heat`, `physics` (DictPhysics), `transition_metrics`, `word_id`, `acl_default`
|
||||
- **`DictPhysics`** — `temperature_q8`, `last_active_ns`, `mass_bytes`, `avg_latency_ns`, `acl_hint`
|
||||
- **`RollingWindowOfTruth`** — circular buffer, double-buffered snapshots, adaptive sizing
|
||||
- **`HeartbeatState`** — tick coordinator, DoE observation counters, L8 bucket stats, M5 time trust
|
||||
- **`HeartbeatTickSnapshot`** — per-tick: cache hits, heat, window width, jitter, L8 mode
|
||||
- **`PipelineGlobalMetrics`** — prefetch accuracy, binary-chop window tuning state
|
||||
- **`CapsuleDesc`** — 64-byte cache-aligned capsule descriptor with content hash
|
||||
|
||||
### Memory Model
|
||||
|
||||
- `vaddr_t` — VM addresses are byte offsets, not C pointers
|
||||
- `vm_load_cell()` / `vm_store_cell()` — canonical memory accessors
|
||||
- `VM_ADDR(cell)` / `CELL(vaddr)` — explicit stack↔offset conversions
|
||||
- Dictionary occupies first 2MB (`DICTIONARY_BLOCKS=2048`), user blocks start at 2048
|
||||
- Total VM memory: 5MB (`VM_MEMORY_SIZE`)
|
||||
- Log blocks: 3072–5120 (2MB for persistent log, 32768 max lines at 64 bytes/line)
|
||||
|
||||
---
|
||||
|
||||
## Testing
|
||||
|
||||
Tests are organized in POST (Power-On Self Test) order:
|
||||
|
||||
1. **Unit tests:** Q48.16 fixed-point, inference statistics, decay slope inference
|
||||
2. **Dictionary tests:** FORTH-79 word validation across 22 categories (not 18)
|
||||
3. **Integration tests, stress tests, adversarial/fuzzing tests** (break_me_tests.c)
|
||||
|
||||
Test files: `src/test_runner/modules/` — 22 `*_test.c` files (including
|
||||
`mama_forth_words_test.c`, `integration_tests.c`, `stress_tests.c`, `break_me_tests.c`).
|
||||
|
||||
Kernel baseline: `QEMU_BASELINE.log` captures reference QEMU/OVMF output for regression detection.
|
||||
**L8 Jacquard Mode Selector** (`ssm_jacquard.c`) — a 128-state, 7-bit loop-gate selector.
|
||||
In this repo it now has a real per-VM heat channel into fleet-wide tuning (VM Fleet
|
||||
Attractor physics — see `docs/working/architecture/VM-FLEET-ATTRACTOR-DESIGN-20260705.md`),
|
||||
replacing hardcoded compudynamics constants with a dynamically-inferred rate.
|
||||
|
||||
---
|
||||
|
||||
## Formal Verification
|
||||
|
||||
The `proof/` directory contains 19 Isabelle/HOL theory files providing
|
||||
machine-checkable proofs of determinism and correctness:
|
||||
|
||||
```
|
||||
proof/
|
||||
├── ROOT # Isabelle project manifest
|
||||
├── StarForth_Base.thy # Base definitions and type system
|
||||
├── StarForth_Loop1_Heat.thy # Execution heat tracking
|
||||
├── StarForth_Loop2_Window.thy # Rolling window
|
||||
├── StarForth_Loop3_Decay.thy # Linear decay
|
||||
├── StarForth_Loop4_Pipeline.thy # Pipelining metrics
|
||||
├── StarForth_Loop5_WinInf.thy # Window width inference
|
||||
├── StarForth_Loop6_DecayInf.thy # Decay slope inference
|
||||
├── StarForth_Loop7_Heartrate.thy # Adaptive heartrate
|
||||
├── StarForth_Arithmetic_Words.thy
|
||||
├── StarForth_Stack_Words.thy
|
||||
├── StarForth_Logical_Words.thy
|
||||
├── StarForth_Memory_Words.thy
|
||||
├── StarForth_Return_Stack_Words.thy
|
||||
├── StarForth_Q48_16.thy # Q48.16 fixed-point
|
||||
├── StarForth_Correctness.thy # Overall correctness
|
||||
├── StarForth_Concurrent.thy # Concurrency properties
|
||||
├── StarForth_Transition.thy # State transitions
|
||||
└── StarForth_Mutex.thy # Mutual exclusion
|
||||
```
|
||||
|
||||
To check proofs: `isabelle build -D proof/` (requires Isabelle installation,
|
||||
see `docs/01-getting-started/DEVELOPER.md`).
|
||||
|
||||
ACL proofs complete (Phase 6): `ACL_Pin_Monotone.thy`, `ACL_Inherit_Clears_Pin.thy`,
|
||||
`ACL_TTL_Bounded.thy`, `ACL_Emergency_Bypass.thy`, `ACL_No_Escalation.thy`. Total: 24 theory files.
|
||||
`proof/` contains 23 Isabelle/HOL theory files (same composition as the standalone StarForth
|
||||
repo — 18 core VM/word-category theories + 5 ACL theories). Run `isabelle build -D proof/`
|
||||
directly; neither `Makefile` nor `Makefile.starkernel` in this repo defines an
|
||||
`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
|
||||
mistakenly invoke).
|
||||
|
||||
---
|
||||
|
||||
## Roadmap
|
||||
|
||||
Full roadmap: `ROADMAP.md`. Summary:
|
||||
|
||||
```
|
||||
2025 (done) 2026 2027 2028
|
||||
StarForth → StarKernel → StarshipOS → FPGA Hardware
|
||||
VM (bare metal) (self-hosting) (custom silicon)
|
||||
DONE M0-M6 done storage,net, feasibility
|
||||
M7 in progress multitask, study
|
||||
self-compile
|
||||
```
|
||||
|
||||
**LithosAnanke roadmap:**
|
||||
- `v1.0.x` — serial-only production (current)
|
||||
- `v1.5.0` — framebuffer VT100 terminal milestone
|
||||
- `v2.0.0` — StarForth SDK release
|
||||
`ROADMAP.md` and `docs/lithosananke/ROADMAP.md` contain real, LithosAnanke-specific phase
|
||||
content (e.g. "PHASE 2: STARKERNEL (Months 3-5)", "StarKernel boots to 'ok' on QEMU ✅") —
|
||||
not a copy of the standalone StarForth repo's roadmap. Prefer these when citing roadmap
|
||||
status for kernel work.
|
||||
|
||||
---
|
||||
|
||||
## Code Standards
|
||||
|
||||
- **Strict ANSI C99** — No GNU extensions, no C++ features
|
||||
- **Zero warnings** — Build with `-Wall -Werror`
|
||||
- **Zero warnings target** — Build with `-Wall -Werror`; note `-Wmissing-field-initializers`
|
||||
warnings have been observed in `src/test_runner/modules/vocabulary_words_test.c` during a
|
||||
full kernel build — worth reporting if it recurs, not silently patched
|
||||
- **No hidden state** — All VM state is explicit in the `VM` struct
|
||||
- **Platform-agnostic** — Kernel code gated by `__STARKERNEL__` and `STARFORTH_ENABLE_VM`
|
||||
- **Content-addressed immutability** — Capsule ID = content hash; any mutation is detectable
|
||||
@@ -553,7 +459,7 @@ StarForth → StarKernel → StarshipOS → FPGA Hardware
|
||||
- `WORD_FROZEN` = execution heat does not decay at all
|
||||
- `STRICT_PTR=1` enforces bounds checking (disable only for benchmarking)
|
||||
- Kernel code uses `#ifdef __STARKERNEL__`; VM-enabled path uses `#ifdef STARFORTH_ENABLE_VM`
|
||||
- Never add `acl_*` fields to `DictEntry` beyond the four already planned (see ACL design doc)
|
||||
- Never add `acl_*` fields to `DictEntry` beyond the four already present
|
||||
|
||||
---
|
||||
|
||||
@@ -564,13 +470,12 @@ StarForth → StarKernel → StarshipOS → FPGA Hardware
|
||||
Intentionally suppressed as of 2025-12-08. See `src/main.c:390-396`:
|
||||
- Metrics still collected via `metrics_from_vm()`
|
||||
- CSV row was redundant with internal VM metrics
|
||||
- To re-enable: add `--csv-export` flag or write to file
|
||||
- To re-enable: add a `--csv-export` flag or write to a file
|
||||
|
||||
### Heartbeat Instrumentation (Planned)
|
||||
|
||||
`HeartbeatTickSnapshot` and `tick_buffer` are declared in `include/vm.h`,
|
||||
but `heartbeat_export_csv()` is **not yet implemented**.
|
||||
See `docs/03-architecture/heartbeat-system/instrumentation-plan.md`.
|
||||
|
||||
### Word Statistics Output
|
||||
|
||||
@@ -587,28 +492,30 @@ capsule and compare dict hashes. Zero-deviation means 0% algorithmic variance.
|
||||
|
||||
## Documentation
|
||||
|
||||
```bash
|
||||
make book # LaTeX → PDF (gold standard)
|
||||
make book-html # HTML single-page + multi-page with dark.css
|
||||
```
|
||||
Key files (this repo has both the older `docs/03-architecture/` tree — still current for
|
||||
ACL/Tripod specifically — and the newer restructured `docs/formal/`/`docs/working/`/
|
||||
`docs/patent/` trees, plus a repo-specific `docs/lithosananke/` tree):
|
||||
|
||||
Key files:
|
||||
- `README.md` — project overview and quick start
|
||||
- `ROADMAP.md` — full VM→Kernel→OS→FPGA roadmap
|
||||
- `ONTOLOGY.md` — formal taxonomy: thermodynamic metaphors, literal implementations, lexicon
|
||||
- `docs/01-getting-started/DEVELOPER.md` — dev environment, Isabelle setup, CI/CD
|
||||
- `docs/03-architecture/OVERVIEW.md` — complete architecture overview
|
||||
- `docs/03-architecture/physics-engine/feedback-loops.md` — all 7 loops detailed
|
||||
- `docs/03-architecture/hal/` — HAL architecture docs (6 files)
|
||||
- `docs/03-architecture/heartbeat-system/` — heartbeat architecture, planned instrumentation
|
||||
- `docs/03-architecture/word-acl/DESIGN.md` — ACL system design + implementation punch list
|
||||
- `docs/02-experiments/` — DoE guides (factorial, heartbeat, physics-optimization)
|
||||
- `papers/James_Steady-State_Convergence_Adaptive_Runtime.pdf` — published SSRN paper
|
||||
- `sbom.spdx` / `sbom.spdx.json` — Software Bill of Materials
|
||||
- `QEMU_BASELINE.log` — QEMU/OVMF reference output for kernel regression testing
|
||||
- `docs/lithosananke/SYSTEM_ARCHITECTURE.md` — full kernel + VM design
|
||||
- `docs/lithosananke/hal/` — HAL reference
|
||||
- `docs/lithosananke/M7.1.md` — capsule birth protocol design
|
||||
- `docs/lithosananke/ROADMAP.md` — milestone plan through self-hosting
|
||||
- `docs/lithosananke/hosted-acceptance-test/README.md` — the hosted-VM acceptance test
|
||||
writeup referenced from the standalone StarForth repo's own docs
|
||||
- `docs/03-architecture/tripod/`, `docs/03-architecture/word-acl/DESIGN.md`
|
||||
- `docs/working/architecture/VM-FLEET-ATTRACTOR-DESIGN-20260705.md` — Tripod/Hermes/Artemis
|
||||
physics + build-system history
|
||||
- `docs/working/architecture/getting-started/DEVELOPER.md` — dev setup, Kconfig reference
|
||||
- `ROADMAP.md`, `CHANGELOG.md`
|
||||
- `experiments/bare_metal/README.md` — **mandatory read before touching capsules** (block
|
||||
namespace rules, see ACL section above)
|
||||
- `experiments/bare_metal/analysis/report/bare_metal_doe_report.pdf` — DoE campaign report
|
||||
- `sbom.spdx` / `sbom.spdx.json`
|
||||
|
||||
---
|
||||
|
||||
## License
|
||||
|
||||
See `./LICENSE` (Starship License 1.0). Commercial license available.
|
||||
See `./LICENSE` (Starship License 1.0, SPDX: `LicenseRef-Starship-1.0`). Commercial
|
||||
license available.
|
||||
@@ -61,7 +61,9 @@ make -f Makefile.starkernel ARCH=riscv64 qemu
|
||||
|
||||
Artifacts: `build/amd64/kernel/starkernel_loader.efi` · `build/amd64/kernel/starkernel_kernel.elf`
|
||||
|
||||
For the hosted VM (Linux, no cross-compiler needed): see [`master` branch](../../tree/master).
|
||||
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,
|
||||
now it's its own project with its own `master`.
|
||||
|
||||
### Build configuration (optional)
|
||||
|
||||
|
||||
Reference in New Issue
Block a user