Reorganize source tree: kernel/, v3/, v4/ split and board infrastructure

Source tree reorganization: - Move StarForth v3 engine to v3/ (src/, include/, Makefile) - Move kernel to kernel/ (src/, include/, linker/, Makefile) - Create v4/ skeleton for F18-ISA golden model (DECOMPOSITION.md, JUSTIFICATION.md) - Move FABRIC-0..4.md to docs/fabric/ - Move ONTOLOGY.md and ROADMAP.md to docs/ Board infrastructure: - Add boards/ser5/, boards/raspi/, boards/milkv/, boards/zynq7020/ - Each board has board.mk (ISA, CPU flags, boot recipe) and README.md - Root Makefile becomes thin dispatcher: boot_image, all, clean, docs take TARGET - make boot_image TARGET=SER5|RASPI|MILKV builds one GPT/MBR image per board - ZYNQ7020 target exists but stops with clear error (ARMv7 port not built yet) - scripts/mkdiskimage.sh builds disk images for all boards Docs pipeline: - docs/book/ with LaTeX master (main.tex) and Makefile - pandoc converts Markdown to LaTeX at build time - Two Lua filters: table-widths.lua (wide tables wrap), code-breaks.lua (inline code breaks) - make docs builds single PDF (754 pages, 0 missing characters) - make docs TARGET=<board> adds board appendix - build/docs/<book|board>/meta.tex stamps git commit into PDF Bug fixes: - 42 include paths that only worked by accident now use correct relative paths - clang-18 hardcode replaced with configurable CC variable (fixed aarch64 build) - Pi 5: kernel_2712.img linked at 0x80000, .bss zeroed, memory reserved - Doxyfile, .clang-tidy, README.md, Kconfig paths updated Verified: - Hosted v3 build passes 1012 tests, 0 failures - SER5 image boots in QEMU (OVMF), POST passes, K exact (65536 = Q48_ONE) - Milk-V image boots in QEMU (OpenSBI + U-Boot + bootefi), POST passes - make clean TARGET=<board> removes only that board and its ISA objects - make all builds all boards, hosted v3, and docs in one run Co-authored-by: Junie <junie@jetbrains.com>
2026-10-01 15:40:09 -04:00
parent 3c709c115b
commit a8b70e88d3
630 changed files with 2646 additions and 2036 deletions
@@ -0,0 +1,356 @@
+/*
+  StarForth — Steady-State Virtual Machine Runtime
+  Copyright (c) 2023–2025 Robert A. James
+  Licensed under the Starship License 1.0 (SL-1.0)
+*/
+
+/*
+ * test_contracts.c — Runtime witnesses for Isabelle/HOL axioms A1 and A4'.
+ *
+ * All contract checks are compiled away when CONTRACTS_ENABLED != 1 so that
+ * normal `make test` builds carry zero overhead.
+ */
+
+#include "test_contracts.h"
+#include "log.h"     /* log_message, LOG_ERROR, LOG_TEST */
+#include "vm.h"      /* VM, vm_interpret, vm_tick, ROLLING_WINDOW_SIZE */
+#include <string.h>  /* memcpy, memset, memcmp */
+
+/* Global violation counter (defined here; declared extern in test_contracts.h) */
+int global_contract_violations = 0;
+
+/*
+ * Accessor functions — same-TU direct access avoids R_X86_64_REX_GOTPCRELX
+ * double-dereference in -fPIC PE builds where GOTPCRELX is not relaxed to LEA.
+ */
+/**
+ * @brief Return the current count of accumulated contract violations.
+ *
+ * Reads @c global_contract_violations directly; same-TU access avoids
+ * GOT double-dereference in @c -fPIC PE32+ builds where
+ * @c R_X86_64_REX_GOTPCRELX is not relaxed to a LEA instruction.
+ *
+ * @return Number of contract violations recorded since last reset.
+ */
+int  contract_get_violation_count(void)  { return global_contract_violations; }
+
+/**
+ * @brief Reset the contract violation counter to zero.
+ *
+ * Call before a fresh round of contract checks so that counts from
+ * earlier test phases do not accumulate across module boundaries.
+ */
+void contract_reset_violation_count(void) { global_contract_violations = 0; }
+
+/* ============================================================================
+ * xorshift64 RNG — deterministic, seeded per-round so each perturbation
+ * produces a distinct physics state.
+ * ============================================================================ */
+
+static uint64_t rng_state = 0xDEADBEEFCAFEBABEULL;
+
+/**
+ * @brief Generate the next pseudo-random 64-bit value via xorshift64.
+ *
+ * Uses the global @c rng_state. The xorshift64 parameters (13, 7, 17)
+ * produce a full-period sequence over all non-zero 64-bit states.
+ * Caller must seed via @c rng_seed() before starting a new fuzz round
+ * to ensure different perturbation sequences across rounds.
+ *
+ * @return Next pseudo-random 64-bit integer.
+ */
+static uint64_t contract_rand(void) {
+    uint64_t x = rng_state;
+    x ^= x << 13;
+    x ^= x >> 7;
+    x ^= x << 17;
+    rng_state = x;
+    return x;
+}
+
+/**
+ * @brief Seed the RNG for a given fuzz round.
+ *
+ * Derives a deterministic seed from the round index mixed with a
+ * Fibonacci multiplier (@c 0x9E3779B97F4A7C15) so each round produces
+ * a distinct, reproducible perturbation sequence regardless of how many
+ * rounds have previously run.
+ *
+ * @param round  Zero-based fuzz round index.
+ */
+static void rng_seed(int round) {
+    rng_state = 0xDEADBEEFCAFEBABEULL ^ ((uint64_t)(unsigned)round * 0x9E3779B97F4A7C15ULL);
+}
+
+/* ============================================================================
+ * Exec-domain capture and comparison
+ * ============================================================================ */
+
+/**
+ * @brief Snapshot the execution-domain fields of a VM into an @c ExecResult.
+ *
+ * Captures @c dsp, @c rsp, @c error, and the live portion of the data
+ * stack (indices 0 … dsp−1). The remainder of @c r->stack is zeroed for
+ * deterministic @c memcmp() comparisons in @c exec_results_equal().
+ *
+ * Only execution-domain fields are captured — physics scalars, heartbeat
+ * state, and rolling-window counters are deliberately excluded.
+ *
+ * @param vm  VM instance to snapshot.
+ * @param r   Output @c ExecResult struct to populate.
+ */
+void capture_exec_result(VM *vm, ExecResult *r) {
+    r->dsp   = vm->dsp;
+    r->rsp   = vm->rsp;
+    r->error = vm->error;
+    /* copy only the live portion; zero the rest for deterministic memcmp */
+    int depth = (vm->dsp > 0) ? vm->dsp : 0;
+    memcpy(r->stack, vm->data_stack, (size_t)depth * sizeof(cell_t));
+    if (depth < STACK_SIZE)
+        memset(&r->stack[depth], 0, (size_t)(STACK_SIZE - depth) * sizeof(cell_t));
+}
+
+/**
+ * @brief Compare two @c ExecResult snapshots for execution-domain equality.
+ *
+ * Returns 1 only if @c dsp, @c rsp, @c error, and the live stack contents
+ * are all identical. Stack comparison uses @c memcmp() over the live
+ * portion (0 … dsp−1 cells); the zeroed tail guarantees no false
+ * positives from uninitialised padding.
+ *
+ * @param a  First snapshot.
+ * @param b  Second snapshot.
+ * @return   1 if execution-domain is identical, 0 if any field differs.
+ */
+int exec_results_equal(const ExecResult *a, const ExecResult *b) {
+    if (a->dsp   != b->dsp)   return 0;
+    if (a->rsp   != b->rsp)   return 0;
+    if (a->error != b->error) return 0;
+    int depth = (a->dsp > 0) ? a->dsp : 0;
+    return memcmp(a->stack, b->stack, (size_t)depth * sizeof(cell_t)) == 0;
+}
+
+/* ============================================================================
+ * Physics snapshot / restore / perturb
+ *
+ * These cover the key scalars touched by the seven feedback loops.  A word
+ * that reads any of these will produce a different ExecResult after perturb,
+ * exposing a violation of A4'.
+ * ============================================================================ */
+
+/**
+ * @brief Save the key physics scalars touched by the seven feedback loops.
+ *
+ * Captures the eight fields that @c perturb_physics() will randomise:
+ * @c decay_slope_q48, @c effective_window_size, @c tick_target_ns,
+ * the three heat percentile thresholds, @c prefetch_attempts, and
+ * @c total_executions. Used as a bracket pair with @c restore_physics()
+ * around each fuzz round so the VM returns to a known state.
+ *
+ * @param vm  VM instance to snapshot.
+ * @param s   Output @c PhysicsSnapshot to populate.
+ */
+void save_physics(VM *vm, PhysicsSnapshot *s) {
+    s->decay_slope_q48  = vm->decay_slope_q48;
+    s->eff_window_size  = vm->rolling_window.effective_window_size;
+    s->tick_target_ns   = vm->heartbeat.tick_target_ns;
+    s->heat_25th        = vm->heat_threshold_25th;
+    s->heat_50th        = vm->heat_threshold_50th;
+    s->heat_75th        = vm->heat_threshold_75th;
+    s->prefetch_attempts = vm->pipeline_metrics.prefetch_attempts;
+    s->total_executions = vm->rolling_window.total_executions;
+}
+
+/**
+ * @brief Restore the physics scalars from a previously saved snapshot.
+ *
+ * Writes back the eight fields saved by @c save_physics(), undoing any
+ * perturbations made by @c perturb_physics(). Called at the end of each
+ * fuzz round and after the full @c check_physics_transparent() loop so
+ * the VM state is clean for the next contract check.
+ *
+ * @param vm  VM instance to restore.
+ * @param s   Source @c PhysicsSnapshot to restore from.
+ */
+void restore_physics(VM *vm, const PhysicsSnapshot *s) {
+    vm->decay_slope_q48                      = s->decay_slope_q48;
+    vm->rolling_window.effective_window_size = s->eff_window_size;
+    vm->heartbeat.tick_target_ns             = s->tick_target_ns;
+    vm->heat_threshold_25th                  = s->heat_25th;
+    vm->heat_threshold_50th                  = s->heat_50th;
+    vm->heat_threshold_75th                  = s->heat_75th;
+    vm->pipeline_metrics.prefetch_attempts   = s->prefetch_attempts;
+    vm->rolling_window.total_executions      = s->total_executions;
+}
+
+/**
+ * @brief Randomly perturb key physics scalars to expose A4' violations.
+ *
+ * Seeds the RNG via @c rng_seed(@p round) for deterministic but distinct
+ * perturbations per round, then overwrites the eight tracked physics
+ * fields with random values that still satisfy their well-formedness
+ * invariants:
+ *
+ *  - @c decay_slope_q48: LSB forced to 1 (must be > 0 per @c slope_wf)
+ *  - @c effective_window_size: [1, ROLLING_WINDOW_SIZE] (never 0)
+ *  - @c tick_target_ns: LSB forced to 1 (must be > 0 per @c hb_state_wf)
+ *  - Heat thresholds: arbitrary positive values (no strict invariant)
+ *  - @c prefetch_attempts / @c total_executions: arbitrary counts
+ *
+ * After perturbation, running the same FORTH input must produce an
+ * identical @c ExecResult; divergence is an A4' violation.
+ *
+ * @param vm     VM instance to perturb.
+ * @param round  Fuzz round index (used to seed the RNG).
+ */
+void perturb_physics(VM *vm, int round) {
+    rng_seed(round);
+
+    /* decay_slope_q48: must be > 0 per slope_wf */
+    vm->decay_slope_q48 = contract_rand() | 1ULL;
+
+    /* effective_window_size: must be in [1, ROLLING_WINDOW_SIZE] */
+    uint64_t w = contract_rand() % (uint64_t)ROLLING_WINDOW_SIZE;
+    vm->rolling_window.effective_window_size = (uint32_t)(w == 0 ? 1 : w);
+
+    /* tick_target_ns: must be > 0 per hb_state_wf */
+    vm->heartbeat.tick_target_ns = contract_rand() | 1ULL;
+
+    /* heat thresholds: arbitrary signed values */
+    vm->heat_threshold_25th = (cell_t)(contract_rand() & 0x7FFF);
+    vm->heat_threshold_50th = (cell_t)(contract_rand() & 0xFFFF);
+    vm->heat_threshold_75th = (cell_t)(contract_rand() & 0x1FFFF);
+
+    /* pipeline and window counters */
+    vm->pipeline_metrics.prefetch_attempts    = contract_rand();
+    vm->rolling_window.total_executions       = contract_rand();
+}
+
+/* ============================================================================
+ * A4' contract check
+ * ============================================================================ */
+
+/**
+ * @brief A4' contract check — verify a word is transparent to physics state.
+ *
+ * Axiom A4' (physics transparency): a FORTH word's execution-domain
+ * result (@c ExecResult) must be identical regardless of the values of
+ * the seven physics feedback-loop scalars.
+ *
+ * Protocol:
+ *  1. Run @p input with current (unperturbed) physics; capture baseline.
+ *  2. For each of @p fuzz_rounds rounds: seed RNG, perturb physics,
+ *     re-run @p input, capture result, compare to baseline.
+ *  3. On divergence, log the violation and increment
+ *     @c global_contract_violations.
+ *  4. Always restore original physics state before returning.
+ *
+ * Error-expected tests (@p should_error) and unimplemented words
+ * (@p implemented == 0) are skipped: exec-equivalent divergence is
+ * legitimate for error paths.
+ *
+ * @param vm          VM instance.
+ * @param word_name   Human-readable word name for diagnostic messages.
+ * @param input       FORTH source string to execute (same each round).
+ * @param should_error  Non-zero if the test is expected to raise an error.
+ * @param implemented   Non-zero if the word is implemented and should be checked.
+ * @param fuzz_rounds   Number of perturbation rounds; 0 → CONTRACT_DEFAULT_FUZZ_ROUNDS.
+ * @return            1 if all rounds passed (or test skipped), 0 on any violation.
+ */
+int check_physics_transparent(VM *vm, const char *word_name,
+                               const char *input,
+                               int should_error, int implemented,
+                               int fuzz_rounds) {
+    /* Skip error-expected tests: exec-equiv may legitimately differ */
+    if (!implemented || should_error) return 1;
+
+    int rounds = (fuzz_rounds > 0) ? fuzz_rounds : CONTRACT_DEFAULT_FUZZ_ROUNDS;
+
+    /* --- Baseline run with current (unperturbed) physics --- */
+    vm->error = 0;
+    vm->dsp   = -1;
+    vm->rsp   = -1;
+    vm->exit_colon      = 0;
+    vm->abort_requested = 0;
+    vm_interpret(vm, input);
+
+    ExecResult baseline;
+    capture_exec_result(vm, &baseline);
+
+    PhysicsSnapshot saved;
+    save_physics(vm, &saved);
+
+    int ok = 1;
+    for (int r = 0; r < rounds && ok; r++) {
+        perturb_physics(vm, r);
+
+        vm->error = 0;
+        vm->dsp   = -1;
+        vm->rsp   = -1;
+        vm->exit_colon      = 0;
+        vm->abort_requested = 0;
+        vm_interpret(vm, input);
+
+        ExecResult fuzzed;
+        capture_exec_result(vm, &fuzzed);
+
+        if (!exec_results_equal(&baseline, &fuzzed)) {
+            log_message(LOG_ERROR,
+                "[A4' CONTRACT] VIOLATION: %s '%s' result changed under physics perturbation (round %d)",
+                word_name, input, r);
+            log_message(LOG_ERROR,
+                "  baseline dsp=%d  fuzzed dsp=%d", baseline.dsp, fuzzed.dsp);
+            ok = 0;
+            global_contract_violations++;
+        }
+
+        vm->dsp   = -1;
+        vm->rsp   = -1;
+        vm->error = 0;
+    }
+
+    restore_physics(vm, &saved);
+    vm->dsp   = -1;
+    vm->rsp   = -1;
+    vm->error = 0;
+    return ok;
+}
+
+/* ============================================================================
+ * A1 contract check
+ * ============================================================================ */
+
+/**
+ * @brief A1 contract check — verify @c vm_tick() does not modify the execution domain.
+ *
+ * Axiom A1 (heartbeat isolation): the background heartbeat tick must never
+ * alter stacks, error state, or any other execution-domain field observable
+ * by FORTH words. This function captures an @c ExecResult before and after
+ * one @c vm_tick() call and compares them with @c exec_results_equal().
+ *
+ * On violation, logs @c [A1 CONTRACT] VIOLATION with before/after dsp and
+ * rsp values, and increments @c global_contract_violations.
+ *
+ * @param vm  VM instance; stacks and error state must already be in a known
+ *            reference state before calling.
+ * @return    1 if the heartbeat left the execution domain unchanged, 0 on violation.
+ */
+int assert_heartbeat_safe(VM *vm) {
+    ExecResult before, after;
+    capture_exec_result(vm, &before);
+
+    vm_tick(vm);
+
+    capture_exec_result(vm, &after);
+
+    if (!exec_results_equal(&before, &after)) {
+        log_message(LOG_ERROR,
+            "[A1 CONTRACT] VIOLATION: vm_tick() modified exec-equiv fields");
+        log_message(LOG_ERROR,
+            "  dsp before=%d after=%d  rsp before=%d after=%d",
+            before.dsp, after.dsp, before.rsp, after.rsp);
+        global_contract_violations++;
+        return 0;
+    }
+    return 1;
+}