LithosAnanake/docs/working/architecture/getting-started/DEVELOPER.md

StarForth Developer Guide

Development Environment Setup

Required Tools

Core Build Tools

sudo apt-get update
sudo apt-get install build-essential gcc make git

Optional Tools

• Doxygen - For API documentation generation
• syft - For SBOM generation
• fpm - For package building (DEB/RPM)

# Doxygen
sudo apt-get install doxygen

# syft
wget https://github.com/anchore/syft/releases/latest/download/syft_linux_amd64.tar.gz
tar -xzf syft_linux_amd64.tar.gz
sudo mv syft /usr/local/bin/

# fpm (for packaging)
sudo apt-get install ruby-dev build-essential
sudo gem install fpm

Isabelle/HOL Installation

Isabelle is required for formal verification documentation generation.

Download & Install

1. Download Isabelle2025 from https://isabelle.in.tum.de/

# Example installation to ~/bin/
cd ~/bin
wget https://isabelle.in.tum.de/dist/Isabelle2025_linux.tar.gz
tar -xzf Isabelle2025_linux.tar.gz

2. Add Isabelle to your PATH in ~/.bashrc:

# Add Isabelle2025 binaries to PATH
export PATH="$PATH:$HOME/bin/Isabelle2025/bin"

3. Reload your shell:

source ~/.bashrc

4. Verify installation:

isabelle version
# Should output: Isabelle2025

Project Integration

The StarForth build system expects isabelle to be available on the PATH. The Makefile will automatically detect it:

# From Makefile line 24:
ISABELLE ?= isabelle

Do NOT commit Isabelle to the repository. It's excluded via .gitignore:

/tools/Isabelle2025/

Isabelle Make Targets

Once Isabelle is installed, you can use these targets:

# Verify all formal theories
make isabelle-build

# Quick syntax check (faster)
make isabelle-check

# Generate audit-ready documentation
make docs-isabelle

Build Configuration (Kconfig)

StarForth has a Linux-kernel-style Kconfig system for its ~40 build-time tuning knobs (physics/SSM engine, adaptive heartbeat, pipelining speculation, architecture, build profile, platform mode, kernel-only flags). It is entirely optional. Nothing changes about a plain make or make -f Makefile.starkernel until you explicitly generate a .config — until then, every knob uses the same bare defaults it always has, and the two Makefiles behave exactly as if Kconfig didn't exist.

Configuring

Config lives per architecture, under build/$(ARCH)/.config — not one root .config — because building all three kernel architectures back-to-back in one script is this project's normal QEMU acceptance workflow, and a single shared config would desync from whichever arch is actually being built.

# Interactive, curses-based menu (recommended)
make menuconfig            # hosted build, current ARCH
make -f Makefile.starkernel ARCH=amd64 menuconfig

# Interactive, Qt-based GUI menu
make xconfig

# Line-by-line interactive prompts (every symbol, in order)
make config

# Re-prompt only for symbols that are new or changed since last time
make oldconfig

# Apply one of the example configs below non-interactively
make hosted_standard_defconfig
make -f Makefile.starkernel ARCH=amd64 kernel_amd64_defconfig

Four example configs ship in configs/: hosted_standard_defconfig, kernel_amd64_defconfig, kernel_aarch64_defconfig, kernel_riscv64_defconfig. Each just selects the architecture/variant choice; every other symbol takes its Kconfig default.

Once a .config exists for an architecture, a plain make (or make -f Makefile.starkernel ARCH=...) picks it up automatically — no extra flag needed. Editing the .config by hand or re-running menuconfig and rebuilding does not force recompilation of unrelated object files (the same is true of today's bare ?= knobs); run make clean first if you want a config change to take full effect.

Command-line always wins. make ROLLING_WINDOW_SIZE=8192 (or any knob, or MINIMAL=1 for platform mode) overrides whatever the active .config says, whether or not Kconfig is in use at all. This is true for every symbol below without exception.

Symbol reference

Architecture & build variant (Kconfig.arch, Kconfig.variant)

Symbol	Type	Default	Effect
ARCH (choice: AMD64/AARCH64/RISCV64)	choice	AMD64	Selects the ARCH= value passed to whichever Makefile is driven from this config.
STARFORTH_VARIANT (choice: HOSTED/KERNEL)	choice	HOSTED	Which Makefile this config targets. Gates the choices below — a kernel-variant config never offers TARGET/PLATFORM, and Kconfig.kernel's symbols only exist for a kernel-variant config.
TARGET (choice: standard/fast/fastest/turbo/pgo/asan) — hosted only	choice	standard	Hosted TARGET= build profile: optimization level, LTO, direct threading, ASan/UBSan instrumentation. pgo only selects which multi-stage make recipe runs, not a flag set.
PLATFORM (choice: default/minimal) — hosted only	choice	default	minimal swaps in freestanding platform sources (-nostdlib -ffreestanding, no libc dependency surface). HISTORICAL: a third mode, l4re (L4Re/Fiasco.OC, -D__l4__=1, forced HEARTBEAT_THREAD_ENABLED off), existed here through mid-2026; removed as an active target.

Physics / SSM engine tuning (Kconfig.physics)

Symbol	Type	Default	Effect
STRICT_PTR	bool	y	VM memory bounds checking on every pointer access. Disable only for raw benchmarking comparisons.
ENABLE_HOTWORDS_CACHE	bool	n	Physics-driven hot-words cache — 1.78× speedup on dictionary lookups when on. Also gates L8 Jacquard's L1_heat_tracking bit.
ENABLE_PIPELINING	bool	n	Speculative execution via word-transition prediction. Also gates L8 Jacquard's L4_pipelining bit, and gates every symbol below down to MINIMUM_PREFETCH_ROI.
TRANSITION_WINDOW_SIZE	int	8	Word-transition lookahead depth for pipelining prediction. Range 1–8.
SPECULATION_THRESHOLD_Q48	hex (Q48.16)	0x8000 (0.50)	Minimum transition probability before pipelining will speculate on a word. Range 0.10 (aggressive) to 0.95 (conservative).
SPECULATION_DEPTH	int	1	How many words ahead to prefetch speculatively. Range 1–4.
MIN_SAMPLES_FOR_SPECULATION	int	10	Transitions observed before pipelining makes a speculation decision for a word.
MISPREDICTION_COST_Q48	hex (Q48.16)	0x190000 (25 ns)	Estimated cost of recovering from a wrong speculation.
MINIMUM_PREFETCH_ROI	hex (Q48.16)	0x1199A (1.10)	Minimum expected return-on-investment ratio for speculation to be worthwhile. (Corrected 2026-07-08 from a long-shipped 0x11999A, which was ~17.6 in Q48.16 — an order of magnitude off from the documented 1.10 intent and effectively disabling speculation whenever pipelining was on.)
ROLLING_WINDOW_SIZE	int	4096	Initial execution-history capture size (rolling window of truth). Automatically shrinks at runtime if pattern diversity plateaus.
ADAPTIVE_SHRINK_RATE	int	50	Percentage of the rolling window retained when an adaptive shrink fires. Range 50–95; lower = more aggressive.
ADAPTIVE_MIN_WINDOW_SIZE	int	256	Floor — the rolling window never shrinks below this many word IDs.
ADAPTIVE_CHECK_FREQUENCY	int	512	How often (in executions) to measure pattern diversity for the shrink decision.
ADAPTIVE_GROWTH_THRESHOLD	int	5	Growth-rate percentage below which the window is considered saturated and a shrink is considered.
INITIAL_DECAY_SLOPE_Q48	int (Q48.16)	21845 (≈0.333)	Cold-start seed for the adaptively-inferred heat-decay slope (Loop #6 retunes it at runtime; this only matters at boot).
DECAY_MIN_INTERVAL	int	500	Historical minimum-interval knob. No longer load-bearing since decay went tick-based (2026-07); kept only because doe_metrics.c still reports it.
DECAY_RATE_PER_US_Q16	int (Q16)	1	Heat decay rate. Half-life ≈6.5s at the default; 0 disables decay entirely.
HEARTBEAT_INFERENCE_FREQUENCY	int	1000	Heartbeat ticks between inference-engine runs (window-width + decay-slope re-inference). Set very high (e.g. 999999) to effectively disable inference for a static-configuration run.
SSM_ENTROPY_HIGH_THRESHOLD	string (float)	"0.75"	Rolling-window entropy above this votes to enable L8 Jacquard's Loop #2 (diversity).
SSM_CV_HIGH_THRESHOLD	string (float)	"0.15"	Short-term volatility above this votes to enable Loops #5/#6 (inference).
SSM_TEMPORAL_DECAY_THRESHOLD	string (float)	"0.5"	Temporal-locality strength above this votes to enable Loop #3 (decay).
SSM_TEMPORAL_DECAY_LOW_THRESHOLD	string (float)	"0.3"	Lower temporal-locality bound that, combined with a high-CV vote, also enables Loop #6.
SSM_HYSTERESIS_TICKS	int	5	Consecutive ticks required before an L8 mode change actually commits (prevents thrashing).

Heartbeat / adaptive tick coordinator (Kconfig.heartbeat)

Symbol	Type	Default	Effect
HEARTBEAT_THREAD_ENABLED — hosted only	bool	y	vm_tick() runs in a dedicated background thread (optimal) vs. inline from the interpreter loop (legacy). Invisible/off for a kernel-variant config — LithosAnanke has no pthreads — and the kernel Makefile keeps an unconditional -D...=0 override regardless, as a second, independent guarantee of the same fact.
HEARTBEAT_TICK_NS	int	10000	Background heartbeat thread wake period, nanoseconds. Only meaningful when HEARTBEAT_THREAD_ENABLED is on.
HEARTBEAT_CHECK_FREQUENCY	int	256	Word executions between heartbeat checks — the counter that makes vm->heartbeat.tick_count a purely execution-driven virtual clock, which is also what Loop #3 heat decay reads (kept architecture-invariant on purpose).
HEARTBEAT_WINDOW_TUNING_FREQUENCY	int	1000	Heartbeat ticks between Loop #5 (window-width inference) runs.
HEARTBEAT_SLOPE_VALIDATION_FREQUENCY	int	5000	Heartbeat ticks between Loop #6 (decay-slope inference) revalidation runs.
EMERGENCY_CONSOLE_ENABLED	bool	y	REPL recovers from errors and continues (interactive fallthrough), vs. exiting to vm_fault_handler(). Set n for production/embedded/high-security builds with no interactive fallthrough surface. Applies to both builds; on the kernel side this only bypasses the bare ok> REPL — zuse sessions are always subject to ACL regardless.

Kernel-only options (Kconfig.kernel) — kernel variant only

Symbol	Type	Default	Effect
STARFORTH_ENABLE_VM	bool	y	Compiles the full StarForth VM source tree into the kernel image and enables capsule birth/execution (M7 milestone). Off builds a kernel that only reaches M0–M6 (console, PMM, VMM, interrupts, timers, kmalloc) — no interpreter, no capsules, no ok> REPL.
PARITY_MODE	bool	n	Enables the parity/determinism verification harness used to compare dict_hash/capsule state across independent runs.
SK_PARITY_DEBUG	bool	n	Extra diagnostic logging in the parity/vocabulary code paths.
HEARTBEAT_DOE_LOG	bool	y	Per-heartbeat-tick DoE observation logging. The bare-metal DoE tooling (experiments/bare_metal/) expects this on.

Out of scope for Kconfig, by design: compudynamics.h's CDTuning values (C function return values, not macros); runtime-only parameters like PROFILE, DOE_INJECT/DOE_REPS/DOE_SEED, KERNEL_ARGS (these govern a specific run, not a compiled configuration).

CI/CD Considerations

GitHub Actions / GitLab CI

For CI/CD pipelines, you'll need to install Isabelle as part of the build process:

GitHub Actions Example

name: Build & Verify

on: [push, pull_request]

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3

      - name: Install build dependencies
        run: |
          sudo apt-get update
          sudo apt-get install -y build-essential gcc make

      - name: Install Isabelle
        run: |
          wget -q https://isabelle.in.tum.de/dist/Isabelle2025_linux.tar.gz
          tar -xzf Isabelle2025_linux.tar.gz
          echo "$GITHUB_WORKSPACE/Isabelle2025/bin" >> $GITHUB_PATH

      - name: Verify Isabelle installation
        run: isabelle version

      - name: Build StarForth
        run: make fastest

      - name: Run tests
        run: make test

      - name: Build formal verification docs
        run: make docs-isabelle

      - name: Upload documentation artifacts
        uses: actions/upload-artifact@v3
        with:
          name: isabelle-docs
          path: docs/src/isabelle/

GitLab CI Example

variables:
  ISABELLE_VERSION: "2025"
  ISABELLE_URL: "https://isabelle.in.tum.de/dist/Isabelle2025_linux.tar.gz"

before_script:
  - apt-get update -qq
  - apt-get install -y -qq build-essential gcc make wget
  - wget -q $ISABELLE_URL
  - tar -xzf Isabelle2025_linux.tar.gz
  - export PATH="$PATH:$PWD/Isabelle2025/bin"
  - isabelle version

build:
  stage: build
  script:
    - make fastest
    - make test

docs:
  stage: deploy
  script:
    - make docs-isabelle
  artifacts:
    paths:
      - docs/src/isabelle/

Docker Considerations

If building in Docker, Isabelle requires Java (JDK 17+):

FROM ubuntu:22.04

# Install build tools
RUN apt-get update && apt-get install -y \
    build-essential \
    gcc \
    make \
    wget \
    openjdk-17-jdk \
    && rm -rf /var/lib/apt/lists/*

# Install Isabelle
RUN wget -q https://isabelle.in.tum.de/dist/Isabelle2025_linux.tar.gz && \
    tar -xzf Isabelle2025_linux.tar.gz && \
    rm Isabelle2025_linux.tar.gz

ENV PATH="/Isabelle2025/bin:${PATH}"

# Verify
RUN isabelle version

CI/CD Performance Notes

• Isabelle build takes 5-10 minutes for all theory verification
• Consider caching Isabelle installation between builds
• Use isabelle-check for quick syntax checking in pre-commit hooks
• Only run full isabelle-build on main branch or release tags

GitHub Actions Caching Example

- name: Cache Isabelle
  uses: actions/cache@v3
  with:
    path: Isabelle2025
    key: isabelle-2025-${{ runner.os }}

- name: Install Isabelle (if not cached)
  if: steps.cache-isabelle.outputs.cache-hit != 'true'
  run: |
    wget -q https://isabelle.in.tum.de/dist/Isabelle2025_linux.tar.gz
    tar -xzf Isabelle2025_linux.tar.gz

Quick Start

# Clone the repository
git clone <repo-url>
cd StarForth

# Install dependencies (including Isabelle - see above)
# ...

# Build the fastest version
make fastest

# Run tests
make test

# Generate documentation (requires Isabelle)
make docs-isabelle

# View generated docs
ls -la docs/src/isabelle/

Project Structure

StarForth/
├── src/                          # C source code
├── include/                      # Header files
├── docs/
│   ├── src/
│   │   ├── internal/formal/     # Isabelle theory files
│   │   └── isabelle/            # Generated Isabelle docs (gitignored)
│   └── DEVELOPER.md             # This file
├── scripts/
│   └── isabelle-to-adoc.sh      # Isabelle doc generator
├── build/                        # Build artifacts (gitignored)
├── tools/
│   └── Isabelle2025/            # Local Isabelle (gitignored)
└── Makefile                      # Build system

Formal Verification

StarForth includes machine-checked correctness proofs using Isabelle/HOL:

• Location: docs/src/internal/formal/*.thy
• Sessions: VM_Formal, Physics_Formal
• Generated docs: docs/src/isabelle/ (after make docs-isabelle)

Theory Files

• VM_Core.thy - Core VM semantics
• VM_Stacks.thy - Stack operations
• VM_StackRuntime.thy - Runtime stack management
• VM_Words.thy - Word definitions
• VM_DataStack_Words.thy - Data stack operations
• VM_ReturnStack_Words.thy - Return stack operations
• VM_Register.thy - Register operations
• Physics_StateMachine.thy - Physics state machine
• Physics_Observation.thy - Observation model

All theories are fully verified with machine-checked proofs.

Contributing

When contributing code that affects the VM semantics:

1. Update relevant Isabelle theories if needed
2. Run make isabelle-build to verify proofs
3. Run make docs-isabelle to regenerate documentation
4. Include Isabelle docs in your pull request

Support

• Issues: GitHub Issues
• Discussions: GitHub Discussions
• Isabelle Help: https://isabelle.in.tum.de/
• Formal Verification: See docs/src/isabelle/VERIFICATION_REPORT.adoc

---

Last Updated: 2025-10-30 Isabelle Version: 2025 Build System: GNU Make