diff --git a/.github/workflows/llvm-lower.yml b/.github/workflows/llvm-lower.yml new file mode 100644 index 000000000..d42a51cc2 --- /dev/null +++ b/.github/workflows/llvm-lower.yml @@ -0,0 +1,59 @@ +name: LLVM Lowering + +on: + push: + branches: [main, "claude/**"] + pull_request: + +jobs: + llvm-lower: + runs-on: ubuntu-latest + timeout-minutes: 20 + + steps: + - uses: actions/checkout@v4 + + - name: Install Racket + uses: Bogdanp/setup-racket@v1.11 + with: + version: '9.0' + + - name: Verify clang is available + run: | + clang --version + which clang + + - name: Install Prologos package dependencies + run: cd racket/prologos && raco pkg install --auto --skip-installed + + - name: Pre-compile compiler + lowering module + run: | + cd racket/prologos + raco make driver.rkt + raco make llvm-lower.rkt + + - name: Pre-compile test runner + run: raco make tools/llvm-test.rkt tools/llvm-compile.rkt + + - name: Tier 0 unit tests (IR string assertions) + run: cd racket/prologos && raco test tests/test-llvm-lower.rkt + + - name: Tier 0 end-to-end (lower + clang + run) + env: + PROLOGOS_LLVM_TIER: "0" + run: racket tools/llvm-test.rkt --tier 0 racket/prologos/examples/llvm/tier0 + + - name: Tier 1 end-to-end (lower + clang + run) + env: + PROLOGOS_LLVM_TIER: "1" + run: racket tools/llvm-test.rkt --tier 1 racket/prologos/examples/llvm/tier1 + + - name: Tier 2 end-to-end (lower + clang + run) + env: + PROLOGOS_LLVM_TIER: "2" + run: racket tools/llvm-test.rkt --tier 2 racket/prologos/examples/llvm/tier2 + + - name: Tier 3 end-to-end (lower + clang + run) + env: + PROLOGOS_LLVM_TIER: "3" + run: racket tools/llvm-test.rkt --tier 3 racket/prologos/examples/llvm/tier3 diff --git a/.github/workflows/network-lower.yml b/.github/workflows/network-lower.yml new file mode 100644 index 000000000..e4efa067f --- /dev/null +++ b/.github/workflows/network-lower.yml @@ -0,0 +1,297 @@ +name: Network Lowering (N-series) + +on: + push: + branches: [main, "claude/**"] + pull_request: + +jobs: + network-lower: + runs-on: ubuntu-latest + timeout-minutes: 20 + + steps: + - uses: actions/checkout@v4 + + - name: Install Racket + uses: Bogdanp/setup-racket@v1.11 + with: + version: '9.0' + + - name: Install Zig + uses: mlugg/setup-zig@v1 + with: + version: 0.13.0 + + - name: Verify clang is available + run: | + clang --version + which clang + + - name: Install Prologos package dependencies + run: cd racket/prologos && raco pkg install --auto --skip-installed + + - name: Pre-compile compiler + network passes + run: | + cd racket/prologos + raco make driver.rkt + raco make network-emit.rkt + raco make network-lower.rkt + + - name: Pre-compile network tools + run: raco make tools/network-compile.rkt tools/network-test.rkt + + - name: Zig HAMT unit tests + # SH Track 6 sub-piece (Issue #42 Path A). Zig-internal `test` + # blocks in runtime/prologos-hamt.zig. Requires libc for the + # extern abort symbol (test mode does not auto-link libc). + run: zig test -lc runtime/prologos-hamt.zig + + - name: Build Zig HAMT object + run: | + zig build-obj runtime/prologos-hamt.zig \ + -OReleaseFast -fstrip -fPIC \ + -femit-bin=runtime/prologos-hamt.o + ls -la runtime/prologos-hamt.o + + - name: HAMT C-ABI smoke test + # Validates that the .o links cleanly against a non-Zig caller. + run: | + clang runtime/test-hamt.c runtime/prologos-hamt.o -o /tmp/test-hamt + /tmp/test-hamt + + - name: Build Zig kernel + run: | + zig version + # -OReleaseFast: omit bounds/overflow safety checks. Our explicit + # bounds checks already cover the boundary; without ReleaseFast, + # implicit checks emit calls into Zig's panic handler that + # zig build-obj does not include in the .o, leaving unresolved + # symbols when clang links against plain libc. + # -fstrip: drop debug info to keep the .o minimal. + # -fPIC: produce position-independent code. Modern clang on Linux + # links PIE executables by default; non-PIC objects fail with + # "relocation R_X86_64_32S against `.bss' can not be used when + # making a PIE object". -fPIC is the standard fix. + zig build-obj runtime/prologos-runtime.zig \ + -OReleaseFast -fstrip -fPIC \ + -femit-bin=runtime/prologos-runtime.o + ls -la runtime/prologos-runtime.o + file runtime/prologos-runtime.o + echo "--- exported symbols (T = strong, U = undefined) ---" + nm runtime/prologos-runtime.o || true + echo "--- undefined symbols only (should be only abort + maybe libc-internals) ---" + nm -u runtime/prologos-runtime.o || true + + - name: Smoke-test runtime linkage with a minimal IR + run: | + cat > /tmp/smoke.ll <<'EOF' + declare i32 @prologos_cell_alloc() + declare i64 @prologos_cell_read(i32) + declare void @prologos_cell_write(i32, i64) + define i64 @main() { + entry: + %c = call i32 @prologos_cell_alloc() + call void @prologos_cell_write(i32 %c, i64 99) + %v = call i64 @prologos_cell_read(i32 %c) + ret i64 %v + } + EOF + clang /tmp/smoke.ll runtime/prologos-runtime.o -o /tmp/smoke + # GitHub Actions runs `bash -eo pipefail`. /tmp/smoke is *expected* + # to return non-zero (the cell value as exit code). Without disabling + # -e around the call, set -e treats the expected return as a failure + # and the step exits with the smoke binary's exit code BEFORE the + # explicit `test` check runs. + set +e + /tmp/smoke + ec=$? + set -e + echo "smoke exit code: $ec" + test "$ec" -eq 99 + + - name: BSP scheduler + instrumentation smoke test + # Sprint B+C (2026-05-01). Validates run_to_quiescence runs proper + # BSP rounds (snapshot/diff/merge), the (3,1) select propagator + # works, and the prologos_get_stat / prologos_reset_stats / + # prologos_set_max_rounds interfaces match the kernel's exports. + run: | + clang runtime/test-bsp-stats.c runtime/prologos-runtime.o \ + -o /tmp/test-bsp-stats + /tmp/test-bsp-stats + + - name: BSP feedback smoke test (Sprint E) + # Sprint E (2026-05-01). Validates the (1,1) shape (kernel-identity) + # and that the BSP barrier keeps reads/writes consistent under + # cyclic networks. Includes iterative fib(0..20) computed by a + # gated self-feedback loop — the same algorithm a future + # source-level expr-iterate would lower to. + run: | + clang runtime/test-bsp-feedback.c runtime/prologos-runtime.o \ + -o /tmp/test-bsp-feedback + /tmp/test-bsp-feedback + + - name: N0 end-to-end (lower + clang + run) + env: + PROLOGOS_NETWORK_TIER: "0" + PROLOGOS_RUNTIME_OBJ: "runtime/prologos-runtime.o" + run: racket tools/network-test.rkt --tier 0 racket/prologos/examples/network/n0 + + - name: pnet-compile end-to-end (.prologos → .pnet → .ll → binary) + # SH milestone: full pipeline through Track 1's deployment-mode + # .pnet artifact format (instead of N0's network-skeleton). + # Validates the formal SH track structure end-to-end. + # Note on `|| ec=$?`: racket exits with the program's exit code + # (e.g. 7 for exit-7.prologos), which is the expected non-zero + # return. Without the || guard, GitHub Actions' bash -e treats + # the non-zero racket exit as step failure before our test check. + env: + PROLOGOS_RUNTIME_OBJ: "runtime/prologos-runtime.o" + run: | + raco make tools/pnet-compile.rkt + for f in 0 7 42; do + ec=0 + racket tools/pnet-compile.rkt -o /tmp/test-pnet-$f \ + racket/prologos/examples/network/n0/exit-$f.prologos > /dev/null 2>&1 || ec=$? + echo "exit-$f.prologos → racket exit=$ec (expected $f)" + test "$ec" -eq "$f" + done + + - name: pnet-compile arithmetic end-to-end (n1-arith) + # Phase 2.D: arithmetic programs compile to a propagator network + # via .pnet, with kernel-int-add/sub/mul/div fire-fns dispatched + # by the in-kernel scheduler. 6 acceptance programs covering + # add, sub, mul, div, nested, and deeply-nested arithmetic. + env: + PROLOGOS_RUNTIME_OBJ: "runtime/prologos-runtime.o" + run: | + for f in racket/prologos/examples/network/n1-arith/*.prologos; do + expected=$(grep -oE ':expect-exit -?[0-9]+' "$f" | grep -oE '\-?[0-9]+') + ec=0 + racket tools/pnet-compile.rkt -o /tmp/n1-arith-test \ + "$f" > /dev/null 2>&1 || ec=$? + echo "$(basename $f) → exit=$ec (expected $expected)" + test "$ec" -eq "$expected" + done + + - name: pnet-compile tail-recursive iteration (n2-tailrec) + # Sprint E.3 (2026-05-01). Tail-recursive defn forms are + # recognized by ast-to-low-pnet's `match-tail-rec` and lowered + # to a feedback propagator network — the same shape as + # test-bsp-feedback.c's hand-rolled iterative fib, but generated + # from regular Prologos source. Programs use 9-12 cells + 7-10 + # propagators independent of input size; networks self-terminate + # via the cond gate (no fuel needed). + env: + PROLOGOS_RUNTIME_OBJ: "runtime/prologos-runtime.o" + run: | + for f in racket/prologos/examples/network/n2-tailrec/*.prologos; do + expected=$(grep -oE ':expect-exit -?[0-9]+' "$f" | grep -oE '\-?[0-9]+') + ec=0 + racket tools/pnet-compile.rkt -o /tmp/n2-tailrec-test \ + "$f" > /dev/null 2>&1 || ec=$? + echo "$(basename $f) → exit=$ec (expected $expected)" + test "$ec" -eq "$expected" + done + + - name: pnet-compile non-recursive helpers (n3-helpers) + # Sprint F.1 (2026-05-01). Non-recursive helper functions are + # inlined at lowering time via beta-substitution: when an + # `(expr-app^k (expr-fvar f) args)` doesn't match the tail-rec + # pattern, look up f's body and substitute it for the fvar. + # Falls through to the multi-arg beta-redex handler. Self- + # recursive non-tail-rec forms error cleanly; mutual recursion + # caught by depth limit (MAX-INLINING-DEPTH=64). + env: + PROLOGOS_RUNTIME_OBJ: "runtime/prologos-runtime.o" + run: | + for f in racket/prologos/examples/network/n3-helpers/*.prologos; do + expected=$(grep -oE ':expect-exit -?[0-9]+' "$f" | grep -oE '\-?[0-9]+') + ec=0 + racket tools/pnet-compile.rkt -o /tmp/n3-helpers-test \ + "$f" > /dev/null 2>&1 || ec=$? + echo "$(basename $f) → exit=$ec (expected $expected)" + test "$ec" -eq "$expected" + done + + - name: pnet-compile non-dependent pairs (n4-pairs) + # Sprint F.2 (2026-05-01). Non-dependent pair lowering. build + # returns a value-tree (cell-id for scalars, list for pairs). + # expr-pair allocates per-component; expr-fst/expr-snd project. + # Per-component decomposition flows transparently through let- + # binding and conditional select. Helpers can take and return + # pair-typed values. Scope is simply-typed pairs only — + # dependent Sigma is intentionally excluded (per collaborator + # feedback 2026-05-01). + env: + PROLOGOS_RUNTIME_OBJ: "runtime/prologos-runtime.o" + run: | + for f in racket/prologos/examples/network/n4-pairs/*.prologos; do + expected=$(grep -oE ':expect-exit -?[0-9]+' "$f" | grep -oE '\-?[0-9]+') + ec=0 + racket tools/pnet-compile.rkt -o /tmp/n4-pairs-test \ + "$f" > /dev/null 2>&1 || ec=$? + echo "$(basename $f) → exit=$ec (expected $expected)" + test "$ec" -eq "$expected" + done + + - name: pnet-compile pair-typed iteration state (n5-pair-state) + # Sprint F.3 (2026-05-01). Extends tail-rec lowering to support + # pair-typed state slots. literal-init-value recurses through + # expr-pair (so [pair 0 1] becomes a vtree of literals). + # State allocation, cond, step-args, and feedback all walk the + # vtrees per-leaf. Bridge logic for shared state cells operates + # per-leaf as well. fib via pair state produces identical + # metrics to the 3-scalar fib-iter, confirming the per-leaf + # decomposition is equivalent. + env: + PROLOGOS_RUNTIME_OBJ: "runtime/prologos-runtime.o" + run: | + for f in racket/prologos/examples/network/n5-pair-state/*.prologos; do + expected=$(grep -oE ':expect-exit -?[0-9]+' "$f" | grep -oE '\-?[0-9]+') + ec=0 + racket tools/pnet-compile.rkt -o /tmp/n5-pair-state-test \ + "$f" > /dev/null 2>&1 || ec=$? + echo "$(basename $f) → exit=$ec (expected $expected)" + test "$ec" -eq "$expected" + done + + - name: pnet-compile Nat match (n6-nat-match) + # Sprint F.4 (2026-05-01). expr-zero / expr-suc / expr-nat-val + # lower to Int cells (Nat is i64 at runtime). Two-arm match + # `match n | zero -> z-body | suc m -> s-body` lowers to a + # cascaded select gated on (int-eq scrut 0); the suc arm's + # binder `m` becomes a cell holding (scrut - 1) pushed onto + # env. Multi-arm (>2) match for general sum types is deferred + # — needs tagged-union runtime representation. + env: + PROLOGOS_RUNTIME_OBJ: "runtime/prologos-runtime.o" + run: | + for f in racket/prologos/examples/network/n6-nat-match/*.prologos; do + expected=$(grep -oE ':expect-exit -?[0-9]+' "$f" | grep -oE '\-?[0-9]+') + ec=0 + racket tools/pnet-compile.rkt -o /tmp/n6-nat-match-test \ + "$f" > /dev/null 2>&1 || ec=$? + echo "$(basename $f) → exit=$ec (expected $expected)" + test "$ec" -eq "$expected" + done + + - name: pnet-compile combined-features showcase (n7-showcase) + # Single Prologos program exercising every Sprint A-F.4 feature + # together: int arith + comparison (A), tail-recursive defn + # (E.3), non-recursive helper inlining (F.1), pair construction + # + projection (F.2), pair-typed iteration state (F.3). + # Same fib(10)=55 result as the simpler iterative variants, + # validating that feature composition produces the expected + # minimal network (12 cells, 10 props, 32 BSP rounds). + env: + PROLOGOS_RUNTIME_OBJ: "runtime/prologos-runtime.o" + run: | + for f in racket/prologos/examples/network/n7-showcase/*.prologos; do + expected=$(grep -oE ':expect-exit -?[0-9]+' "$f" | grep -oE '\-?[0-9]+') + ec=0 + racket tools/pnet-compile.rkt -o /tmp/n7-showcase-test \ + "$f" > /dev/null 2>&1 || ec=$? + echo "$(basename $f) → exit=$ec (expected $expected)" + test "$ec" -eq "$expected" + done diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 3d54c4921..277fc58f9 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -21,6 +21,44 @@ jobs: - name: Install dependencies run: cd racket/prologos && raco pkg install --auto --skip-installed + - name: Install rackcheck (for property-based tests) + # rackcheck is declared as build-deps (not deps) in info.rkt, so + # the previous `raco pkg install --auto` step skips it. Tests + # `test-generators.rkt` and `test-properties.rkt` (require rackcheck) + # at module load time. Install explicitly so they run on CI. + run: raco pkg install --auto --skip-installed rackcheck + + - name: Install Zig (for hybrid runtime kernel) + # Zig 0.13 builds runtime/libprologos-runtime-hybrid.so used by + # tests/test-preduce-hybrid-differential.rkt. The test gracefully + # skips if the .so isn't built; this step ensures CI exercises + # the hybrid path. + uses: mlugg/setup-zig@v1 + with: + version: '0.13.0' + + - name: Build hybrid runtime kernel + run: cd runtime && zig build-lib -dynamic prologos-runtime-hybrid.zig -O ReleaseFast + + - name: Install Node.js (for OCapN interop tests) + # The OCapN tests (test-ocapn-{abort,bridge-interop,conversation, + # handshake,live-interop,pipelined,rpc}.rkt) spawn Node.js peer + # scripts under tools/interop/peer-*.mjs as subprocesses for + # bidirectional interop testing. Each test self-skips with + # (exit 0) if Node + node_modules are absent, so this step is + # what makes them actually run on CI. + uses: actions/setup-node@v4 + with: + node-version: '22' + + - name: Install OCapN interop deps + # Fetches @endo/ocapn (the JS reference implementation) into + # tools/interop/node_modules/. The test runner's + # `interop-deps-present?` check looks for + # tools/interop/node_modules/@endo/ocapn/src/syrup/js-representation.js + # to gate the OCapN-FFI test suite. + run: cd tools/interop && npm install --no-audit + - name: Pre-compile modules run: cd racket/prologos && raco make driver.rkt diff --git a/.gitignore b/.gitignore index 329e59b27..76f356d72 100644 --- a/.gitignore +++ b/.gitignore @@ -53,6 +53,24 @@ racket/prologos/data/benchmarks/failures/*.log docs/stdlib-book/racket/prologos/data/cache/ racket/prologos/data/cache/ +# Stray cache writes from misconfigured bundle paths (seen 2026-05-05 — +# the hybrid bundle binary occasionally synthesizes a relative path +# `.../prologos/data/cache/...` instead of the canonical location). +.../ + # MemPalace per-project files (issue #185) mempalace.yaml entities.json + +# Network-lowering runtime build artifacts (built by zig build-obj in CI / locally) +runtime/*.o +runtime/*.o.o +runtime/*.so +runtime/*.so.o +runtime/test-hybrid-smoke +runtime/prologos-runtime.o.dSYM/ + +# Test scratch — output binaries from network-compile.rkt / llvm-compile.rkt +/out +/out.ll +/dist/ diff --git a/.zig-version b/.zig-version new file mode 100644 index 000000000..54d1a4f2a --- /dev/null +++ b/.zig-version @@ -0,0 +1 @@ +0.13.0 diff --git a/docs/research/2026-05-03_HYBRID_RACKET_ZIG_RUNTIME.md b/docs/research/2026-05-03_HYBRID_RACKET_ZIG_RUNTIME.md new file mode 100644 index 000000000..f176bd5e3 --- /dev/null +++ b/docs/research/2026-05-03_HYBRID_RACKET_ZIG_RUNTIME.md @@ -0,0 +1,616 @@ +# Hybrid Racket-Zig Runtime — Research Sprint + +**Date**: 2026-05-03 +**Stage**: 1 — research synthesis. No design commitments; informs a future implementation track. +**Series**: SH (Self-Hosting), parallel/alternative to Track 1 LLVM lowering. +**Branch context**: `claude/prologos-layering-architecture-Pn8M9` +**Author**: Claude (research synthesis). + +**Cross-references**: +- [SH Master Tracker](2026-04-30_SH_MASTER.md) +- [Self-Hosting Path and Bootstrap Stages](../research/2026-04-30_SELF_HOSTING_PATH_AND_BOOTSTRAP.md) +- [Concurrency Primitives for the .pnet → LLVM Substrate](../research/2026-05-02_CONCURRENCY_PRIMITIVES_LLVM_SUBSTRATE.md) — Zig-side BSP design building blocks that compose with this hybrid model +- [Kernel Pocket Universes design](2026-05-02_KERNEL_POCKET_UNIVERSES.md) — the kernel PU primitive sits inside this runtime +- [PReduce-lite Design Doc](2026-05-02_PREDUCE_LITE_DESIGN.md) — Racket-side reducer that this hybrid runtime would host on the hot path +- [PReduce-lite PIR](2026-05-03_PREDUCE_LITE_PIR.md) — terminal state of Racket-side reducer +- [Low-PNet IR Design Doc](2026-05-02_LOW_PNET_IR_TRACK2.md) — alternate lowering path (LLVM IR generation for a fully-Zig binary) +- `runtime/prologos-runtime.zig` — existing 544-line single-threaded BSP kernel with per-tag profiling +- `runtime/prologos-hamt.zig` — existing 441-line CHAMP-style persistent map (Track 6 path A) + +--- + +## 1. Frame + +### 1.1 The proposal in one paragraph + +Bundle the existing Racket-implemented Prologos compiler (parser, elaborator, type-checker, PReduce-lite reducer, and standard-library `.prologos` modules) **as-is** into a distributable artifact alongside a minimal Zig runtime that owns the BSP scheduler, cell storage (HAMT), and a hardcoded set of fast fire functions. The Racket side parses Prologos programs and constructs a propagator network by **calling into the Zig runtime** (allocating cells, installing propagators). The Zig runtime executes the network on the hot path; when it needs to fire a propagator whose body lives in Racket (because we haven't migrated that fire-fn to Zig yet), it **calls back into Racket** via FFI. The runtime instruments per-tag wall-time and per-tag callback counts, producing a prioritized list of fire-fns whose Racket implementations dominate runtime — these become the next migration targets. + +### 1.2 Why this approach is interesting (vs LLVM lowering) + +**LLVM lowering** (SH Series Track 1, PR #39) compiles the elaborated AST → LLVM IR → native binary. The binary is fully self-contained: no Racket runtime, no interpreter overhead, theoretical maximum performance. But it requires every AST node + every reduction rule to be expressible at the LLVM IR level, which means re-implementing the Racket reducer in C-like terms. Today that pass handles three "tiers" (literals, arithmetic, top-level non-capturing functions); to handle the full language requires re-implementing closures, eliminators, traits, ATMS, the trait registry, etc. — essentially porting the Racket compiler. + +**The hybrid approach** (this proposal) trades binary size + interpreter overhead for **breadth-first coverage**: a binary that runs *every* Prologos program correctly today (because Racket handles it correctly), with a clear migration path to move hot-path fire functions into Zig as profiling identifies them. Time-to-first-binary is 1-2 weeks instead of months. Each subsequent migration step is independent and incremental. + +The two approaches are not exclusive — the LLVM track can continue, and the hybrid runtime can host LLVM-compiled fire functions when they exist. They share architecture (BSP scheduler, propagator network) and could converge. + +### 1.3 What this research note delivers + +A Stage 1 synthesis. Not a design commitment. The note answers: + +- **What is the seam?** (§3 — four architectural options + recommendation) +- **What's on each side?** (§4 — concrete API surface) +- **How do values cross?** (§5 — cell-value marshaling, the hardest engineering problem) +- **How does Racket call Zig and vice versa?** (§6 — FFI mechanism + Racket-CS embedding strategies) +- **How do we identify what to move next?** (§7 — profiling instrumentation, mostly already in the kernel) +- **What goes wrong?** (§8 — risk + cost analysis) +- **If we proceed, what's the sprint plan?** (§9 — 5-6 phases, ~10-15 days) +- **What's open?** (§10 — research questions for a future Stage 2/3 design doc) + +--- + +## 2. Current state (factual) + +### 2.1 Racket side + +The full Prologos toolchain in `racket/prologos/`: +- `parser.rkt` / `tree-parser.rkt` — sexp + WS-mode reader +- `elaborator.rkt` — surface-syntax → core-AST + type inference +- `typing-core.rkt` / `qtt.rkt` — type checking with QTT multiplicities +- `reduction.rkt` — 3700-LOC tree-walking reducer (the existing slow path) +- `preduce.rkt` — 1390-LOC PReduce-lite (Racket-side propagator-network reducer; just landed) +- `propagator.rkt` — propagator network primitives (cells, fire-once, BSP scheduler, register-stratum-handler, …) +- `lib/prologos/*.prologos` — standard library (Nat, Bool, List, Option, Result, traits Eq/Ord/Add/Sub/Mul, …) + +### 2.2 Zig side (existing) + +`runtime/prologos-runtime.zig` (544 LOC, single-threaded): +- Flat fixed cell array (`MAX_CELLS=1024`, `i64` cell value) +- Flat fixed propagator array (`MAX_PROPS=1024`, three shape kinds: 1-1, 2-1, 3-1) +- Per-tag dispatch in `fire_against_snapshot`: ~10 hardcoded fire-fns (identity, int-neg/abs/add/sub/mul/div/eq/lt/le, select) +- BSP scheduler (snapshot/diff/merge/dedup) — 100% functional today +- Per-tag profiling: `stat_fires_by_tag[N_TAGS]`, `stat_ns_by_tag[N_TAGS]` (opt-in via `prologos_set_profile_per_tag`) +- Subscriber lists (per-cell list of dependent prop-ids), `MAX_DEPS=16` +- Stats: rounds, fires_total, fires_by_tag, writes_committed, writes_dropped, max_worklist +- Compiles via `zig build-obj` to a single `.o` + +`runtime/prologos-hamt.zig` (441 LOC): +- CHAMP-style persistent hash array mapped trie +- Used by N1+ programs needing structural sharing +- Not yet integrated into cell storage (cells are still flat i64) + +### 2.3 What's missing + +- No Racket ↔ Zig FFI — the `.o` is currently linked into LLVM-lowered programs (Tier 0-2 of PR #39) and exercised via C test harnesses. No production path embeds Racket. +- The Zig kernel hardcodes ~10 fire-fn tags. To extend, you currently edit Zig source. There's no callback-fn-table mechanism. +- Cells are `i64`; can't hold Prologos values like AST structs, lambda closures, pairs-of-values. +- No HAMT-backed cell store yet (the HAMT library exists but isn't wired in). + +These are the deltas between today and the hybrid runtime. The research below assesses how big each delta is. + +--- + +## 3. The seam — four architectural options + +The fundamental question: where does the boundary between Racket and Zig sit? Four options, ordered by how much Zig owns. + +### 3.1 Option A — Cells in Zig only + +**Zig owns**: cell storage (HAMT-backed). Just `cell_alloc` / `cell_read` / `cell_write` / `cell_subscribe`. +**Racket owns**: everything else (network construction, scheduling, fire-fn dispatch, BSP loop). + +**Hot path**: every `(net-cell-read)` / `(net-cell-write)` is an FFI call from Racket into Zig. The BSP scheduler logic stays in Racket. + +**Cost**: ~1 week (just port the existing Racket cell store to Zig HAMT + bind FFI). + +**Verdict**: ✗ doesn't capture the hot path. The expensive work in PReduce-lite is the BSP scheduler iterating over ~1000 propagators per round. Moving cells to Zig adds FFI overhead per cell access without taking the loop into Zig. + +### 3.2 Option B — Cells + scheduler in Zig; fire-fns in Racket + +**Zig owns**: cells + propagators + BSP scheduler + per-tag dispatch. +**Racket owns**: AST → network construction. All fire functions are Racket callbacks. + +**Hot path**: BSP loop runs in Zig; every fire-fn invocation is an FFI call out to Racket. + +**Cost**: ~1.5 weeks (Racket-side network-construction shim + Racket fire-fn callback wrapper + FFI marshaling). + +**Verdict**: partial — the BSP loop is Zig-fast, but every fire is an FFI call. If 80% of fires are int-arithmetic and we have those in Zig already, this option is fine for those. If 80% of fires are Racket callbacks (PReduce-lite's case today — every preduce-merge is a Racket fn), the FFI overhead dominates and we've gained little vs running everything in Racket. + +The fix for B: include a hardcoded set of "kernel" fire-fns in Zig (which we already have for int arithmetic). Tags map to either a kernel fn or a callback. As we migrate fire-fns to Zig, the callback set shrinks. + +This is essentially **Option C** below. + +### 3.3 Option C — Cells + scheduler + dynamic fire-fn dispatch (recommended) + +**Zig owns**: cells + propagators + BSP scheduler + a dispatch table mapping `fire-fn-tag → fn ptr`. At install time, the tag is registered in the dispatch table with either: +- (a) a built-in Zig fire function (kernel set: int-add, int-mul, etc.; expand over time), OR +- (b) a Racket callback wrapper (slow path) + +**Racket owns**: AST → network construction (calls Zig install APIs); the implementation of (b) callback fire-fns; everything outside the network execution loop. + +**Hot path**: BSP loop runs in Zig; per-fire dispatch is one indirect call (kernel) or one FFI call (callback). The kernel-vs-callback decision is per-tag, set at registration. + +**Migration strategy**: profile per-tag wall time; tags whose callback time dominates get ported to Zig (the (a) path). Migration is per-tag-at-a-time; doesn't break compatibility. + +**Cost**: ~2 weeks (~1 week new Zig + ~1 week Racket FFI + integration). + +**Verdict**: ✓ this is the recommended seam. Captures the BSP hot path in Zig. Migration is incremental and observable. Existing `prologos-runtime.zig` is 80% there already (cells, scheduler, per-tag profiling all done; what's missing is the dynamic dispatch table + the Racket callback bridge). + +### 3.4 Option D — Full LLVM lowering (the alternative path; not this proposal) + +**Zig owns**: nothing — Racket stops at compile-time, the binary is a fully-LLVM-compiled standalone. +**Racket owns**: only the compiler (offline at build time). + +**Hot path**: pure native code; no FFI; theoretical max performance. + +**Cost**: per the existing PR #39, Tiers 0-2 done; full coverage of the language is months of work. + +**Verdict**: ✗ for this proposal — long-tail effort. ✓ as a parallel track that converges later. + +### 3.5 Comparison summary + +| | A (cells only) | B (sched, all callbacks) | **C (sched + dispatch table)** | D (LLVM full) | +|---|---|---|---|---| +| Hot-path BSP in native | ✗ | ✓ | **✓** | ✓ | +| Time-to-first-binary | ~1w | ~1.5w | **~2w** | months | +| Incremental fire-fn migration | n/a | n/a | **per-tag, observable** | per-feature, all-or-nothing | +| Compatibility with existing Racket Prologos | full | full | **full** | tier-limited | +| Captures FFI overhead in profile | ✓ | partial | **✓** (per-tag callback ns) | n/a | +| Composes with LLVM track | yes | yes | **yes** | self | + +**Recommendation: Option C.** Existing kernel is 80% of what's needed; the remaining 20% is dynamic dispatch + Racket FFI. Profile-driven migration gives a concrete path to close the FFI overhead over time, with measurable progress at each step. + +The rest of this document is Option C in detail. + +--- + +## 4. Concrete API surface (the seam under Option C) + +### 4.1 Zig kernel APIs (additions to existing surface) + +```zig +// === Existing (already in runtime/prologos-runtime.zig) === +prologos_cell_alloc() -> u32 +prologos_cell_write(id: u32, val: i64) -> void +prologos_cell_read(id: u32) -> i64 +prologos_propagator_install_1_1(tag, in0, out0) -> u32 +prologos_propagator_install_2_1(tag, in0, in1, out0) -> u32 +prologos_propagator_install_3_1(tag, in0, in1, in2, out0) -> u32 +prologos_run_to_quiescence() -> void +prologos_set_max_rounds(m) -> void +prologos_get_stat(key) -> u64 +prologos_print_stats() -> void +prologos_set_profile_per_tag(enabled: u32) -> void +prologos_reset_stats() -> void + +// === New for hybrid runtime === + +// Register a tag → fn-ptr binding. shape ∈ {1, 2, 3} matches the +// install_N_1 family. fn_ptr is a C ABI function with signature +// determined by shape: +// shape 1: fn(i64) i64 +// shape 2: fn(i64, i64) i64 +// shape 3: fn(i64, i64, i64) i64 +// kind ∈ {KIND_KERNEL, KIND_RACKET_CALLBACK} — distinguishes for +// profiling and for cell-value marshaling discipline. +prologos_register_fire_fn( + tag: u32, + shape: u32, + kind: u32, // 0 = kernel (Zig native), 1 = Racket callback + fn_ptr: *const fn, +) -> u32 // 0 on success, error code otherwise + +// Install a propagator with arbitrary input arity (extends 1/2/3 fixed +// shapes). For higher-arity propagators (e.g., expr-reduce dispatching +// on N constructor arms). The fire-fn has signature +// fn(num_inputs: u32, inputs: [*]const i64) i64 +prologos_propagator_install_n_1( + tag: u32, + inputs: [*]const u32, // cell ids + num_inputs: u32, + out0: u32, +) -> u32 // pid + +// Cell-value marshaling — see §5. +prologos_cell_box(racket_value_handle: u64) -> i64 // returns boxed i64 +prologos_cell_unbox(boxed: i64) -> u64 // returns Racket handle +prologos_cell_value_kind(boxed: i64) -> u32 // 0=int, 1=bool, 2=racket-handle, ... + +// Per-tag callback profiling (extends existing fires_by_tag). +prologos_get_callback_ns_by_tag(tag: u32) -> u64 +prologos_get_callback_count_by_tag(tag: u32) -> u64 +prologos_print_callback_summary() -> void // sorted by total ns + +// Generic event hook so Zig can call arbitrary Racket functions +// (used by stratum handlers to signal Racket between BSP rounds). +prologos_set_round_callback(fn_ptr: *const fn(u32) void) -> void +// fn_ptr called with (round_number) at end of each BSP round. +// #f / null → no callback. + +// Optional: HAMT-backed cell store toggle. Default: flat array. +// When enabled, cell-id 0..N have flat backing; >N have HAMT backing. +prologos_use_hamt_cells(threshold: u32) -> void +``` + +### 4.2 Racket-side wrappers + +`racket/prologos/runtime-bridge.rkt` (new): + +```racket +#lang racket/base + +(require ffi/unsafe ffi/unsafe/define) + +(define-ffi-definer define-rt + (ffi-lib "libprologos-runtime")) + +(define-rt prologos_cell_alloc (_fun -> _uint32)) +(define-rt prologos_cell_write (_fun _uint32 _int64 -> _void)) +(define-rt prologos_cell_read (_fun _uint32 -> _int64)) +(define-rt prologos_propagator_install_1_1 + (_fun _uint32 _uint32 _uint32 -> _uint32)) +(define-rt prologos_propagator_install_2_1 + (_fun _uint32 _uint32 _uint32 _uint32 -> _uint32)) +(define-rt prologos_propagator_install_3_1 + (_fun _uint32 _uint32 _uint32 _uint32 _uint32 -> _uint32)) +(define-rt prologos_propagator_install_n_1 + (_fun _uint32 (_array _uint32 0) _uint32 _uint32 -> _uint32)) +(define-rt prologos_run_to_quiescence (_fun -> _void)) +(define-rt prologos_register_fire_fn + (_fun _uint32 _uint32 _uint32 _pointer -> _uint32)) +;; ... etc +``` + +Plus a higher-level `racket/prologos/runtime/prop-network.rkt` that mirrors today's `propagator.rkt` API but routes to the Zig kernel. The existing `(net-cell-read net cid)` becomes `(prologos_cell_read cid)` (no `net` parameter — the kernel owns the singleton state). + +This is a mechanical refactor of `propagator.rkt` to be a thin shim. PReduce-lite's `compile-expr` doesn't change. + +### 4.3 Racket fire-fn callback wrapper + +Each Racket fire-fn (e.g., the closure built by PReduce-lite's `make-app-fire`) gets wrapped as a `_fun` callback the Zig kernel can invoke: + +```racket +(define (wrap-fire-fn-as-c-callback shape rkt-fire-fn) + (case shape + [(1) (function-ptr + (lambda (in0) + (rkt-fire-fn in0)) + (_fun _int64 -> _int64))] + [(2) (function-ptr + (lambda (in0 in1) + (rkt-fire-fn in0 in1)) + (_fun _int64 _int64 -> _int64))] + [(3) (function-ptr + (lambda (in0 in1 in2) + (rkt-fire-fn in0 in1 in2)) + (_fun _int64 _int64 _int64 -> _int64))])) +``` + +The `function-ptr` API in Racket FFI converts a Racket procedure into a callable C function pointer. This is the load-bearing FFI mechanism for the callback direction. + +--- + +## 5. Cell-value marshaling — the hardest engineering problem + +The existing kernel stores `i64` per cell. That's fine for `expr-int`, `expr-true/false`, `expr-nat-val`, and Bool comparison results. But PReduce-lite's value lattice includes: + +- AST nodes — `(expr-pair a b)`, `(expr-suc inner)`, `(expr-int 42)` — Racket structs +- Lambda values — `(preduce-lam mw type body env)` — Racket structs containing AST sub-trees +- Container wrappers — `(expr-champ champ-empty)`, `(expr-rrb rrb-empty)`, `(expr-hset ...)` +- Pair values — `(preduce-pair fst-cid snd-cid)` — carries cell-ids of components +- Sentinels — `'preduce-bot`, `'preduce-top` + +These are Racket-managed objects. They can't fit in i64. Three options: + +### 5.1 Option M1 — Tagged i64 with handle table + +The kernel stores `i64`. Layout: +- Bits 63..56: type tag (8 bits) +- Bits 55..0: payload +- Tag 0 = primitive int (payload is the int, sign-extended) +- Tag 1 = bool (payload 0/1) +- Tag 2 = nat-val (payload is the nat) +- Tag 3 = bot +- Tag 4 = top +- Tag 5 = Racket handle (payload is index into a Racket-managed handle table) + +For tag 5, Racket maintains a `(make-vector capacity #f)` handle table. The `cell_box` API takes a Racket value, finds a free slot, returns `(<<5 56) | slot-index`. The `cell_unbox` reverse. + +**Pros**: i64 cells stay; kernel doesn't need GC integration; Racket-side handle table lets us GC handles when their Racket counterparts are unreferenced. + +**Cons**: every non-primitive cell read/write costs a handle-table lookup in Racket. For PReduce-lite where most cells hold AST structs, this is most cells. + +### 5.2 Option M2 — Variant cell type (kernel learns about boxes) + +The kernel's cell store becomes a variant: `union { i64; *opaque; }`. The kernel stores a tag bit per cell. Reads/writes use the appropriate variant. The opaque pointer is owned by Racket. + +**Pros**: same performance as M1 for the lookup, but the tag bit is on the cell, not in the value. Doesn't waste 8 bits of i64. + +**Cons**: changes the kernel's cell layout (every cell is now ~16 bytes instead of 8); more complex. + +### 5.3 Option M3 — Push values fully into Racket; cells are pointers + +The kernel stores only pointers (or handles). All cell values are Racket-managed. + +**Pros**: simpler kernel. + +**Cons**: every cell access is FFI through a Racket lookup. Eliminates the hot-path advantage entirely. Rejected. + +### 5.4 Recommendation + +**M1 (tagged i64).** Pros: zero kernel layout change. Hot path for primitive cells (int/bool/nat) is one branch in the fire-fn (extract tag, switch). Cold path for Racket-handle cells goes through FFI but those fires are already callbacks. + +The handle table is small in practice (per-call, per-PReduce invocation, the handle count is ~100s of cells × low fraction with Racket values). GC happens at end-of-call by clearing the table. + +The 8-bit tag space (256 type tags) is more than enough; we'll use ~10. + +### 5.5 Open question: cell-id allocation across Racket-Zig + +Cell-ids live in Zig. Racket calls `prologos_cell_alloc`, gets an `u32`. That id is unique in the kernel. Racket doesn't allocate cells of its own. + +But what about Racket-side data structures referenced by handles? Their lifetime is bounded by: +1. The `(preduce e)` call — handles are valid until the call returns. +2. After return, the kernel state is reset (`prologos_reset_stats` + zero `num_cells`/`num_props`); the handle table clears. + +This works for one-shot reductions. For long-lived networks (interactive REPL, future incremental compilation), we'd need explicit handle-release / handle-GC integration. Defer to a future "long-lived hybrid runtime" design. + +--- + +## 6. FFI mechanism — Racket-CS embedding strategies + +The hybrid runtime is a **single binary** containing both Racket-CS runtime + Zig kernel + the user's Prologos program. Three packaging strategies: + +### 6.1 Strategy E1 — `raco distribute` + Zig as `.so` dependency + +Use `raco distribute` to build a self-contained Racket-CS executable. Bundle `libprologos-runtime.so` (the Zig `.o` linked as a shared library). The Racket entrypoint requires `runtime-bridge.rkt`, which `dlopen`s the `.so` via `ffi-lib`. + +**Pros**: standard Racket distribution path; documented; the `.so` is trivially included in the distribution directory. + +**Cons**: distribution is a directory, not a single file. The user runs `bin/prologos --run program.prologos`, which expects `lib/libprologos-runtime.so` alongside. + +### 6.2 Strategy E2 — `raco demod` static linking + Zig static archive + +Use `raco demod` (Racket-CS) to produce a single `.zo` containing the entire Racket runtime + the user's program. Link Zig as a static `.a`. Wrap with a shell that has Racket-CS embedded. + +**Pros**: closer to a single-file binary. + +**Cons**: more complex build; `raco demod` is for partial-evaluation, not production embedding; not the canonical path. + +### 6.3 Strategy E3 — Embed Racket-CS as a library inside Zig + +Use Chez Scheme's C embedding API (`Sscheme_init`, `Sregister_symbol`, `Scall1`, etc.) to load a Racket-CS instance into a Zig host process. The Zig binary is the entrypoint; it bootstraps Racket-CS at startup, loads the user's program, then the program calls back into Zig as expected. + +**Pros**: single-file binary; Zig owns startup; clearest separation. + +**Cons**: undocumented for Racket-CS specifically (Chez has the docs; Racket-CS is built on Chez but adds layers); risk of undefined behavior; investment cost is high. + +### 6.4 Recommendation + +**E1 for v1.** It's the well-trodden path. The distribution is a directory; the user runs a launcher script. We can ship E1 as the production mode and validate E2/E3 as future optimizations if single-file matters more than time-to-ship. + +`raco distribute` handles bundling Racket-CS itself, the user's `.zo` files, and the standard library `.prologos` modules. We add a step to copy `libprologos-runtime.so` into the distribution's `lib/` directory and ensure `ffi-lib` finds it. + +### 6.5 FFI overhead — what we should expect + +Numbers I'm extrapolating from literature (will need calibration): + +| Operation | Cost | Note | +|---|---|---| +| Racket → Zig (no marshaling, primitive args) | ~50-100 ns | One indirect call via libffi or raw | +| Racket → Zig (with marshaling, struct args) | ~200-500 ns | Allocator + boxing per arg | +| Zig → Racket callback (no marshaling) | ~100-300 ns | More expensive than the forward direction; goes through Racket's foreign-call machinery | +| Zig → Racket callback (with handle resolution) | ~500-1000 ns | + handle-table lookup | + +Compare to Zig-native fire (kernel int-add): ~1-3 ns per fire. + +**Implication**: every Racket callback fire is ~100-500x slower than a kernel fire. Workloads dominated by callbacks won't see much speedup vs pure-Racket. The migration economics: every fire-fn moved to Zig saves the callback overhead × fires-per-run. For a fire-fn that's ~30% of total fires, migration is worth it as soon as the user runs the program enough times to amortize the migration cost. + +This is exactly why per-tag profiling is load-bearing. + +--- + +## 7. Profiling instrumentation — what we measure + +The existing kernel already measures: +- `stat_rounds` — total BSP rounds +- `stat_fires_total` — total fires +- `stat_fires_by_tag[N_TAGS]` — fires per tag +- `stat_ns_by_tag[N_TAGS]` — wall time per tag (opt-in) +- `stat_writes_committed`, `stat_writes_dropped`, `stat_max_worklist` + +For the hybrid runtime we add: + +```zig +stat_callbacks_by_tag[N_TAGS] // count of Racket-callback fires per tag +stat_callback_ns_by_tag[N_TAGS] // wall time spent in Racket callbacks per tag +stat_marshal_ns_total // wall time spent in cell-value marshaling +stat_handle_table_size_max // peak handle-table occupancy +``` + +The `prologos_print_callback_summary` API sorts tags by total callback ns descending and prints a table: + +``` +=== Callback Profile === +tag fires total_ns avg_ns recommend +preduce-merge 12345 1.3M ns 105 PORT NOW (35% of run) +make-app-fire 4567 340K ns 74 consider +make-natrec-fire 1200 90K ns 75 later +kernel-int-add (native) 9876 28K ns 2.8 already native +``` + +This output is the migration triage tool. After running a representative workload, the developer reads the table and decides which Racket fire-fns to port to Zig next. + +--- + +## 8. Risk + cost analysis + +### 8.1 Costs + +| Item | Estimate | Notes | +|---|---|---| +| Zig: dynamic-dispatch table for fire-fns | 1d | extends existing `fire_against_snapshot` with fn-ptr lookup | +| Zig: `prologos_register_fire_fn` API | 0.5d | + marshaling kind tag | +| Zig: `prologos_propagator_install_n_1` (variable arity) | 1d | new arena for input-cid arrays | +| Zig: cell-value tagged-i64 marshaling | 1d | encode/decode + handle-table interop | +| Zig: callback profiling instrumentation | 0.5d | mirrors existing per-tag profiling | +| Racket: `runtime-bridge.rkt` FFI bindings | 1d | mechanical, ~150 LOC | +| Racket: `runtime/prop-network.rkt` shim mirroring existing propagator.rkt API | 2d | refactor; fold in existing fire-once / topology infrastructure | +| Racket: callback-wrapping helper (`wrap-fire-fn-as-c-callback`) | 0.5d | uses Racket's `function-ptr` | +| Racket: handle-table for Racket values crossing the seam | 1d | per-call lifetime; reset on entry | +| Integration: `raco distribute` packaging + launcher script | 1d | including `libprologos-runtime.so` copy | +| Integration: end-to-end test on a Prologos program | 1d | factorial-iter via PReduce-lite via hybrid runtime | +| Profiling validation: run on a real workload, generate the callback summary | 0.5d | | +| **Total** | **~10 days** | one-developer single-track | + +### 8.2 Risks + +**R1 — FFI overhead dominates**. If most fires are Racket callbacks (the PReduce-lite case), the per-fire 100-500ns FFI cost may exceed the saved scheduler time. Result: hybrid runtime is slower than pure Racket on PReduce-lite workloads. Mitigation: port the top-3 Racket fire-fns (preduce-merge, make-app-fire, make-natrec-fire) to Zig as Phase 1.5 if the profile shows them dominating. + +**R2 — Racket-CS embedding fragility**. `raco distribute` is the well-trodden path but specific behaviors (FFI library search, working-directory resolution, dynamic loading on Linux/macOS/Windows differences) may surface platform issues. Mitigation: target Linux only for v1; defer macOS/Windows. + +**R3 — Cell-value marshaling boundary bugs**. Tagged i64 has 8 bits of tag and 56 bits of payload; if a Prologos int exceeds 56 bits we silently corrupt. Mitigation: bound int range at the elaborator (Prologos ints are already 64-bit per `expr-int`; need a runtime check or wider tag scheme). + +**R4 — Handle-table lifetime**. If Racket GC moves objects, the kernel's stored pointers become stale. Mitigation: pin handle-table entries via Racket's `make-immobile-cell` or store integer indices into a Racket-managed vector (no movement). + +**R5 — Long-running networks** (REPL, interactive programs, future incremental compilation): handles accumulate; no GC strategy. Mitigation: defer; v1 is one-shot reductions only. Future: explicit handle-release API + per-PU lifetime scoping. + +**R6 — Multi-thread safety**. The Zig kernel is single-threaded today. The Racket-CS runtime is also single-threaded for callbacks (one place-channel per place, but cross-place callbacks are deeply problematic). If we later add Sprint D's parallel BSP, we need each worker to either own its own Racket runtime (impossible) or call back into a shared Racket runtime serially. Mitigation: defer multi-thread; v1 is single-threaded. + +**R7 — Compatibility with full Track 9**. PReduce-lite's terminal state hosts on the hybrid runtime. Full Track 9 (incremental, dependency-tracking) adds per-cell subscription that's more complex. The hybrid runtime's cell APIs need to expose subscription metadata. Mitigation: design the APIs to allow future extension; don't paint into a corner. + +### 8.3 What dominates risk + +R1 (FFI overhead dominates). All other risks are tractable engineering. R1 is fundamental: if profiling shows ~80% of fires are Racket callbacks at native speed too, the hybrid runtime is no faster than pure Racket. Mitigation requires migrating fire-fns. + +The good news: **PReduce-lite's hot fire-fns are mostly mechanical** (preduce-merge, identity, beta dispatch, eliminator dispatch). Each is a few-line Racket function that ports to Zig in under an hour. The migration economics work as long as we're willing to invest a few days porting the top-N. + +--- + +## 9. Sprint plan if proceeding + +If the user green-lights this approach, here's the phase plan: + +### Phase 0 — Calibration (0.5 day) + +Measure baseline FFI cost on the host. Microbench: +- 10M Racket → C calls (no marshaling) — measure ns/call +- 10M C → Racket callbacks — measure ns/call +- 1M tagged-i64 unbox + handle-table lookup — measure ns/op + +Anchors the cost model. If numbers are 10x worse than expected (>1us per callback), pivot to Option D (LLVM lowering). + +### Phase 1 — Zig dynamic dispatch (1.5 days) + +- Extend `fire_against_snapshot` to look up fn-ptr from a tag-keyed table +- `prologos_register_fire_fn` API +- `prologos_propagator_install_n_1` for variable arity +- Tagged-i64 cell-value marshaling helpers (`prologos_cell_box`, `prologos_cell_unbox`, `prologos_cell_value_kind`) +- Callback profiling counters + +Validate via existing C tests (`test-bsp-feedback.c`, `test-bsp-stats.c`) plus new test for dynamic dispatch. + +### Phase 2 — Racket FFI bindings + bridge (2 days) + +- `racket/prologos/runtime-bridge.rkt` — `define-rt` bindings for all kernel APIs +- `racket/prologos/runtime/prop-network.rkt` — high-level shim mirroring existing propagator.rkt API (cells, fire-once, BSP run-to-quiescence) +- Handle table: `make-vector` with index-based storage; reset per `(preduce e)` call +- `wrap-fire-fn-as-c-callback` helper + +End-to-end smoke test: `(preduce (expr-int-add (expr-int 2) (expr-int 3)))` runs through hybrid runtime, gets `(expr-int 5)`. + +### Phase 3 — PReduce-lite hosting (2 days) + +- Refactor `preduce.rkt` to call into the hybrid runtime via `runtime/prop-network.rkt` instead of Racket-side `propagator.rkt` +- Run all 90 PReduce-lite unit tests + 2000-case differential gate against the hybrid runtime +- Expected: 100% pass; some fire-fns will be slower (callbacks) but correctness identical +- Generate first callback profile for a representative workload (factorial-iter 1 100, fibonacci 20) + +### Phase 4 — `raco distribute` packaging (1 day) + +- Build script that: + 1. Compiles Racket modules (`raco make`) + 2. Builds `libprologos-runtime.so` from Zig + 3. Runs `raco distribute` to assemble the bundle + 4. Copies `.so` into bundle's `lib/` + 5. Generates launcher script +- Test on a clean machine (Docker container) — does the produced bundle run? + +### Phase 5 — First migration: top-3 Racket fire-fns to Zig (2 days) + +Based on Phase 3's profile, port the top-3 Racket fire-fns to Zig: +- Likely candidates: preduce-merge (called by every cell write), kernel-identity (β / eliminator bridges), make-app-fire wrapped (every dynamic β) +- Measure speedup; validate correctness via PReduce-lite test suite + differential gate + +### Phase 6 — PIR + handoff (0.5 day) + +PIR per `POST_IMPLEMENTATION_REVIEW.org`. Capture: +- Calibrated FFI numbers +- Validated end-to-end binary size + cold-start time +- Migration economics confirmed/refuted +- List of next-priority fire-fns to migrate (ordered by callback profile) + +**Total: ~10 days. Single-developer track.** + +--- + +## 10. Open questions + +| # | Question | Resolution path | +|---|---|---| +| Q1 | What's the actual FFI overhead on this host? | Phase 0 microbench | +| Q2 | Does Racket-CS expose `function-ptr` cleanly for arbitrary Racket procs as C function pointers? | Phase 0 — `(function-ptr proc (_fun ...))` test. Standard Racket FFI; should work. | +| Q3 | How does `raco distribute` handle a Racket binary that depends on a separate `.so`? | Phase 0 / Phase 4 — likely just `(ffi-lib "libprologos-runtime")` with `.so` in the bundle's `lib/`. | +| Q4 | Cell-id allocation: kernel grows from 1024 to 8192 to N? Or HAMT-backed dynamic? | Phase 1 — start with growable flat array (10x current), evaluate HAMT later. | +| Q5 | What about Racket's GC interacting with cells holding handles to Racket objects? | Phase 2 — use Racket-managed vector with index-based handles (no GC interaction). | +| Q6 | Multi-thread BSP integration with Racket callbacks? | Defer to Sprint D + future hybrid-multi-thread design. v1 is single-threaded. | +| Q7 | Stratum handlers (PU, NAF, retraction) — how do they cross the seam? | Phase 2/3 — `prologos_set_round_callback` API gives Zig a hook to invoke Racket between rounds. Stratum handlers stay in Racket. | +| Q8 | What about ATMS speculation / fork-on-union — those need network forking? | Defer to a kernel-PU+hybrid integration design. The kernel-PU work (separate doc) is the unifying primitive; this hybrid runtime composes with it. | +| Q9 | Long-running networks (REPL): handle GC strategy? | Defer; v1 is one-shot. Future: per-call handle-table reset, or explicit release API. | +| Q10 | Where do `.prologos` library files live in the bundle? | Standard Racket convention: `share//lib/`. Loaded via `process-file` lookup. | +| Q11 | Compatibility with the LLVM lowering track? | Compatible — the LLVM track produces standalone binaries; the hybrid track produces Racket-bundled binaries. They share the kernel ABI. Future convergence: LLVM-compiled fire-fns linked into the hybrid kernel as native fire-fns. | +| Q12 | Does this approach compose with kernel PUs? | Yes — kernel PUs add per-PU cell arenas + strata stack to the kernel. The hybrid runtime's API surface stays the same; PUs are an internal kernel concern. | + +--- + +## 11. Comparison with alternatives + recommendation + +| Path | Time-to-binary | Coverage | Runtime perf | Composes with | +|---|---|---|---|---| +| **Hybrid (Option C, this doc)** | **~10 days** | **100% (Racket fallback)** | **medium (FFI overhead, port hot tags)** | LLVM track, kernel PUs, Sprint D parallel | +| Pure-LLVM (PR #39 SH Series Track 1) | months | tier-limited | high | hybrid (eventual convergence) | +| Pure-Racket (status quo) | 0 days | 100% | low | n/a | + +**Recommendation if user proceeds**: hybrid is the right next architectural step IF the goal is "ship a working binary that runs every Prologos program in less than two weeks." It buys time for the LLVM track to mature without blocking on it. The migration economics are observable (per-tag profiling already in the kernel). The FFI risk (R1) is real but mitigable. + +If the goal is "ship a maximally fast binary," LLVM is the destination; hybrid is a stepping stone. + +--- + +## 12. References + +### Racket FFI + embedding +- [Racket FFI guide](https://docs.racket-lang.org/foreign/index.html) +- [`raco distribute`](https://docs.racket-lang.org/raco/exe-dist.html) — canonical distribution path +- [`raco demod`](https://docs.racket-lang.org/raco/demod.html) — module demodularization for static linking +- [Racket-CS embedding (Chez basis)](https://racket.discourse.group/t/embedding-racket-cs-as-a-library/) — community discussion +- [Chez Scheme C interface](https://cisco.github.io/ChezScheme/csug9.5/foreign.html) + +### Existing Prologos infrastructure +- `runtime/prologos-runtime.zig` — 544 LOC single-threaded BSP kernel +- `runtime/prologos-hamt.zig` — 441 LOC CHAMP persistent map +- `racket/prologos/preduce.rkt` — 1390 LOC Racket-side reducer (PReduce-lite, just landed) +- `racket/prologos/llvm-lower.rkt` — Tier 0-2 LLVM IR lowering (PR #39 SH Series Track 1) + +### Related design docs +- [SH Master Tracker](2026-04-30_SH_MASTER.md) — overall self-hosting roadmap +- [Concurrency Primitives](../research/2026-05-02_CONCURRENCY_PRIMITIVES_LLVM_SUBSTRATE.md) — Zig-side BSP scheduler design (Chase-Lev deque, EBR, futex-parked workers, mimalloc, per-(worker, PU) write logs) — directly composes with the hybrid runtime as the future Sprint D parallel substrate +- [Kernel Pocket Universes](2026-05-02_KERNEL_POCKET_UNIVERSES.md) — kernel-side scoped sub-networks; orthogonal to hybrid (the hybrid runtime hosts kernel PUs internally) +- [PReduce-lite Design](2026-05-02_PREDUCE_LITE_DESIGN.md) — Racket-side reducer that lives on the hybrid runtime's hot path +- [PReduce-lite PIR](2026-05-03_PREDUCE_LITE_PIR.md) — terminal state of the Racket-side reducer + +### Engineering-discipline peers +- [TigerBeetle](https://github.com/tigerbeetle/tigerbeetle) — Zig systems work; deterministic simulation testing posture +- [Riposte](https://github.com/khoek/riposte), [DrRacket](https://racket-lang.org/) — Racket binary embedding precedents + +--- + +**End of research note.** diff --git a/docs/tracking/2026-04-27_GOBLIN_PITFALLS.md b/docs/tracking/2026-04-27_GOBLIN_PITFALLS.md new file mode 100644 index 000000000..ce9ca691f --- /dev/null +++ b/docs/tracking/2026-04-27_GOBLIN_PITFALLS.md @@ -0,0 +1,1260 @@ +# Goblin Pitfalls — Implementing OCapN in Prologos + +Live log of language bugs, ergonomic friction, and pure-FP-vs-actor-system +impedance mismatches encountered while porting Spritely Goblins / OCapN to +Prologos. Each entry: what we tried, what broke, and the workaround. + +The implementation lives in `lib/prologos/ocapn/`. Tests in +`tests/test-ocapn-*.rkt`. Acceptance in +`examples/2026-04-27-ocapn-acceptance.prologos`. + +## Scope + +OCapN's reference implementation (Goblins, in Racket) leans on three things +that Prologos does not give us for free: + +1. **Mutable boxes** for actor-state. Goblins's `become` re-binds a behaviour + slot in place; the vat then routes the next message through the new closure. +2. **First-class closures stored in heterogeneous registries** — the actor + table maps an opaque `Refr` to a closure `Args -> Action` whose *capture* + shape varies per actor. +3. **Re-entrant call stacks within a turn** — `($ refr msg ...)` performs a + synchronous call that can itself send more messages. + +In Prologos we get capability types, session types, dependent types, and +QTT — but no mutation, no value-typed `Any`, and a closed-world `data` +declaration. So the impedance is real, and most pitfalls below are +load-bearing for the design. + +The goal of this doc is to make the next port easier. If a pitfall has a +trivially small repro, it is filed as a candidate language-bug for the +Prologos team to look at. + +--- + +## Pitfalls + +(populated as encountered, newest first; each entry dated) + +--- + +### #0 — [DELETED — out of scope: env limitation, not a Prologos issue] + +--- + +### #1 — Eventual-receive is a Phase 0 no-op (OCapN-side, NOT a Prologos bug) (2026-04-27) + +**Status.** This is a deferred-implementation note, not a Prologos +language bug. Number kept for catalogue continuity. + +**Where this matters.** OCapN promises require a delivery semantics +where `(<- refr msg)` enqueues a message and returns a promise that +*eventually* settles to the actor's reply. In our Phase 0: + +- *Local* promise resolution works (the FullFiller pattern emits + `eff-resolve` and the vat applies it on the next turn). +- *Cross-vat* eventual receive — i.e. the protocol-level "deliver + this message to a refr you got from a peer, and route the reply + back over CapTP" — is NOT implemented. Pipelined messages on a + promise are queued at the PromiseState level but the vat does + not flush them across resolution (see pitfall #17 for the + type-level reason: PromiseState's queue carries Syrup wire form, + vat queue carries decoded VatMsg). + +**Implication.** The `core.prologos` `ask` function returns a +promise id but the only way that promise gets settled is if some +local actor explicitly emits `eff-resolve` for it. There's no +remote-deliver path yet. + +**Open path to Phase 1.** Wire the netlayer ↔ vat bridge so that +inbound CapTP `op:deliver` messages on a connection turn into +`enqueue-msg` calls on the local vat, AND outbound `eff-resolve` +on a promise that has a remote resolver triggers an outbound +`op:listen`-reply on the originating connection. + +--- + +### #2 — [DELETED — false claim: WS-mode wildcard match works correctly with a proper spec] + +--- + +### #3 — [DELETED — false claim: function-typed `data` fields work with bracketed fn-type, e.g. `step : [Nat -> Nat]`] + +--- + +### #4 — `rec` session continuation is in the grammar but not in the elaborator (2026-04-27, real bug) + +**Symptom.** `grammar.ebnf` §6 lines 1153–1187 promise both `Mu` +(the sexp form) and `rec [label]` (the WS form) for recursive +session types. Try them: + +``` +session Loop + ! Nat + rec +``` + +Elaboration fails with: +``` +prologos-error "Unknown session type: rec" +``` + +The sexp form `(session Loop2 (Send Nat (Mu End)))` fails the same +way: +``` +prologos-error "Unknown session type: rec" +``` +(grammar admits both `Mu` and `rec`; both unimplemented.) + +**Why this matters for OCapN.** The CapTP wire protocol is a +multiplexed full-duplex stream of `op:*` messages — peers +interleave `op:deliver`, `op:listen`, `op:gc-export`, etc. until +one sends `op:abort`. The natural session is recursive: +`μX. &> {deliver:X, listen:X, abort:end}`. Without `rec`, a +single `session CapTPConn` can't capture stream-level +well-typedness; we have to settle for per-exchange sub-protocols. + +**Workaround in this port.** `captp-session.prologos` decomposes +CapTP into FIVE finite sub-protocols (Handshake, Deliver, Listen, +DeliverOnly, Gc), each its own `session` declaration. A real +driver re-instantiates the appropriate sub-protocol per +exchange. Per-exchange typing remains, but stream-level +well-typedness is unproven. + +**Filed as a Prologos bug.** The grammar documents `rec`/`Mu`; +the elaborator should accept it. Pointing at `surface-syntax.rkt` +or wherever the session-type elaborator lives would close the +gap. Until then, `MixedProto` style finite alternations are the +documented ceiling. + +--- + +### #5 — `none` and `some` need explicit type args in some contexts (2026-04-27) + +**Symptom.** Several tests need to compare against an `Option Nat` +returned by `lookup-promise`, etc. Writing the literal `none` works +in pattern position but in expression position with no surrounding +inference it can fail with an "ambiguous type variable" error. + +**Workaround.** When passed to a function that takes an +`Option Nat`, write `none` and let unification do the work. When +returning `none` from a polymorphic helper as a value, an explicit +type-arg form (`[none Nat]`) is needed in some places. We tried +both forms in `lib/prologos/ocapn/message.prologos`'s +`mk-deliver-no-resolver` (chose the no-arg form because it's +inferred from the `op-deliver` constructor's third-arg type). + +**Status.** This is a known general inference-vs-explicit-instantiation +tension in dependently-typed languages, not a goblin-specific bug. +Recorded for completeness — the OCapN port doesn't dodge it; users +will hit it any time they write predicates returning `Option α`. + +--- + +### #6 — [DELETED — out of scope: WS-mode and sexp-mode `let` are two surface forms by design] + +--- + +### #7 — [DELETED — followed from #2 which was false; wildcard fall-through obviates the noise] + +--- + +### #8 — [DELETED — false claim: `Sigma` works in `data` ctor fields, e.g. `box1 : [Sigma [_ ] Bool]`] + +--- + +### #9 — [DELETED — user error: `def` for values vs `defn` for functions is documented] + +--- + +### #10 — [DELETED — out of scope: sandbox network limitation, not a Prologos issue] + +--- + +### #11 — `thread #:pool 'own` requires Racket 9 (2026-04-27, real bug) + +**Symptom.** On Racket 8.10: +``` +application: procedure does not accept keyword arguments + procedure: thread + arguments...: + # + #:pool 'own +``` +Crashes during the very first `process-string` of any test fixture +because `driver.rkt:434` enables `(current-parallel-executor +(make-parallel-thread-fire-all))` unconditionally and that builds a +worker pool whose workers spawn via `thread #:pool 'own` — a Racket-9 +feature. + +**Workaround applied.** A try/catch fence in `driver.rkt`: + +``` +(when (with-handlers ([exn:fail? (lambda _ #f)]) + (define t (thread #:pool 'own (lambda () (void)))) + (thread-wait t) + #t) + (current-parallel-executor (make-parallel-thread-fire-all))) +``` + +If `thread #:pool 'own` raises (Racket 8.x), `current-parallel-executor` +stays `#f` and BSP falls back to `sequential-fire-all`. Tests run +single-threaded but correctly. + +**Verdict.** This is a real Prologos infrastructure bug, not specific +to OCapN. Anyone who installs Prologos on Racket 8 hits it +immediately. Should be merged upstream (or the codebase should refuse +to load on < Racket 9 with a friendlier error). + +--- + +### #12 — Test fixture loses `current-ctor-registry` and `current-type-meta` across calls (2026-04-27, real bug, **highest-impact**) + +**Symptom.** Tests of the `vat/spawn` shape produced un-evaluated +output: + +``` +"Expected '[reduce [reduce ... | vat x y z a -> ...] | allocated x y -> x] | vat x y z a -> x] : Nat' to contain '1N'" +``` + +The expression has the right TYPE (`: Nat`) but the `reduce` (i.e. +`match` on a user data constructor) was never unfolded. So `1N` never +appears in the printed value. + +**Cause.** The standard test-fixture pattern (copied from +`test-hashable-01.rkt`) captures `current-prelude-env`, +`current-trait-registry`, `current-impl-registry`, +`current-param-impl-registry`, and `current-module-registry` from the +preamble — but **not** `current-ctor-registry` or `current-type-meta`. + +For built-in types (Nat, Bool, List, Option) this is fine because their +ctor info is set in the prelude module that's always loaded. But for +*user-defined* `data` types declared inside the preamble's imports — +in our case `Vat`, `Allocated`, `Actor`, `ActorEntry`, `PromiseEntry`, +`VatMsg`, `BehaviorTag`, `Effect`, `ActStep`, `SyrupValue`, +`PromiseState`, `CapTPOp` — the ctor info goes into the registry that +the fixture *captures into a parameter at setup time but does not +restore in `run`*. When the test then calls `(eval ...)`, the reducer +sees a fresh empty `current-ctor-registry`, treats `vat`, `allocated` +et al. as opaque applications, and refuses to fire any pattern arms +that use them. + +**Why this hadn't surfaced before.** Existing tests that follow this +fixture pattern (`test-hashable-01.rkt`, `test-capability-01.rkt`, +…) only declare *traits* and *capabilities* in their preambles, not +new `data` types. The OCapN port appears to be the first stress test +of the fixture pattern with non-trivial new sums. + +**Fix in tests.** Capture and restore the two extra parameters: + +```racket +(define-values (... + shared-ctor-reg + shared-type-meta) + (parameterize ([... (current-ctor-registry) ... (current-type-meta) ...]) + (process-string shared-preamble) + (values ... + (current-ctor-registry) + (current-type-meta)))) + +(define (run s) + (parameterize ([... + [current-ctor-registry shared-ctor-reg] + [current-type-meta shared-type-meta]]) + (process-string s))) +``` + +Applied to all 8 OCapN test files via a Python sed — each gets a +`shared-ctor-reg` and `shared-type-meta` added to the `define-values` +list, captured at preamble time, restored in `run`. + +**Verdict.** This is a real Prologos test-infrastructure bug. The +canonical fixture skeleton in `test-hashable-01.rkt` needs to grow +the two extra parameters; otherwise the next person who declares a +new `data` type in their preamble hits the same wall and the +diagnostic — "match form printed without reducing" — is genuinely +mysterious to anyone who hasn't seen it before. + +Recommended fix: bake `current-ctor-registry`/`current-type-meta` +capture into `tests/test-support.rkt` so that all fixtures get it for +free (or document the requirement loudly in CLAUDE.md's testing +rules). + +--- + +### #13 — `spawn` is a reserved syntactic form (2026-04-27) + +**Symptom.** A user-defined function named `spawn` parses but fails +to elaborate calls to it: +``` +"Cannot elaborate: #(struct:surf-spawn ...)" +``` + +**Cause.** `macros.rkt` reserves `spawn` (and `spawn-with`) at the +preparse layer: +```racket +[(and (pair? datum) (eq? head 'spawn)) ...] +``` +so `(spawn ...)` is dispatched to the actor-spawn surface form, not +treated as application of a user-bound `spawn` function. Our +`vat.prologos` originally exported a `spawn` function — the test +parser silently rewrote every call site to `surf-spawn` and then +elaboration choked because the surface form expects a different +shape. + +**Fix in this port.** Rename `spawn` → `vat-spawn` and `spawn-actor` +→ `vat-spawn-actor` everywhere (library + tests + acceptance file). + +**Verdict.** This is a footgun, not a bug — the surface-syntax keyword +isn't documented as reserved in any user-facing place. A reserved- +words list in CLAUDE.md (or a clearer error message — "you cannot +declare a function with the reserved name `spawn`") would have saved +the diagnostic round. + +Other names reserved by the same mechanism in `macros.rkt`: +`spawn`, `spawn-with`. Names *not* reserved but worth being +careful with: `send`, `receive`, `become` — they're session-types +keywords (`!`, `?`) under different surface forms but the symbol- +name `send` is currently free. We use it. + +--- + +### #14 — `match | pair a b -> ...` on a `Sigma` returning a `Sigma` (2026-04-27) + +**Symptom.** With this body: + +``` +spec send Nat SyrupValue Vat -> [Sigma [_ ] Nat] +defn send [target args v] + match [fresh-promise v] + | pair v1 pid -> + pair [enqueue-msg [vmsg-deliver target args [some Nat pid]] v1] pid +``` + +elaboration emits `Type mismatch / could not infer` even though every +sub-expression has a clear type (or so it seems). Replacing the +result construction with a `the [Sigma [_ ] Nat] [pair ...]` +ascription does not fix it. Rewriting via `[fst r]` / `[snd r]` +(used twice on the same Sigma) trips QTT multiplicity. + +**Workaround.** Replace the `Sigma Vat Nat` return type with a +named struct: + +``` +data Allocated + allocated : Vat -> Nat + +spec alloc-vat Allocated -> Vat +spec alloc-id Allocated -> Nat +``` + +`spawn`, `fresh-promise`, and `send` all return `Allocated`. The +elaborator handles the named type without complaint. + +**Diagnosis.** I'm not entirely sure where the inference fails — the +elaborated body printed by the error `` shows the +right shape with `[some Nat b]` (after we provided the type arg +explicitly). My best guess is that the implicit pair-of-Sigma +introduces a meta the elaborator can't pin down because the Sigma +is non-dependent (`[_ ]`) and the constructor doesn't carry +enough info from the use-site. Stdlib `defn split-at [n xs] pair +[take n xs] [drop n xs]` works, so it's not "Sigma in result +position is broken" — something specific to the *destructure-then- +reconstruct* shape we hit here. + +**Verdict.** Probably worth a small repro for the Prologos team. Our +`Allocated` workaround is clean and what users would write anyway, +but the failure mode is silent and the error message ("could not +infer") doesn't point at the line. + +--- + +### #15 — [DELETED — false claim: tested with `[fst p]`/`[snd p]` 3× on the same Sigma, no multiplicity error; the original failure was conflated with #14's destructure issue] + +--- + +### #16 — Forward references inside a `.prologos` module (2026-04-27) + +**Symptom.** First version of `vat.prologos` had: +``` +spec apply-effect Effect Vat -> Vat +defn apply-effect [e v] + match e + | eff-resolve pid val -> resolve-promise pid val v ;; ← forward ref + | ... + +spec resolve-promise Nat SyrupValue Vat -> Vat ;; ← defined later +defn resolve-promise [pid val v] + ... +``` + +Loading the module reported `Unbound variable: resolve-promise` in +`apply-effect`'s body, then the same cascade for every later +function that references it. + +**Cause.** Module elaboration is single-pass top-to-bottom; each +`defn` requires its callees to be already in scope. (Same as Prolog, +Standard ML core, etc. Not the same as Haskell or Racket.) + +**Fix.** Reorder: `resolve-promise` and `break-promise` come before +`apply-effect` and `apply-effects`; `step-after-act` before +`deliver-msg`; `list-length-helper` before `queue-length`. + +**Verdict.** Standard FP-language convention; documented here only +because the error message doesn't suggest "did you mean to define +this lower in the file?" and a beginner can spend a few minutes +checking imports before realising the dependency order is wrong. + +--- + +### #17 — Promise-queue ↔ Vat-queue type mismatch (design pitfall, not a bug) (2026-04-27) + +**Symptom.** First version of `vat.prologos`'s `resolve-promise` +flushed pipelined messages from the promise back to the vat queue: + +``` +[vat n acts proms-after [append q [take-queue s]]] +``` + +But `take-queue : PromiseState -> List SyrupValue` and the vat +queue is `List VatMsg`. The elaborator inserts `append`'s implicit +type arg as `VatMsg`, then balks because the second argument has +type `List SyrupValue`. Reported as a `Type mismatch / could not +infer` of the whole `resolve-promise` definition. + +**Root cause.** Conceptual confusion: `pst-unresolved` carries the +*wire-level* representation of pipelined messages (Syrup values, what +a peer would send over the wire), but the local vat's queue holds +already-decoded `VatMsg` records. They are not interchangeable — +flushing requires re-encoding, which Phase 0 doesn't do. + +**Fix.** Drop the flush. `resolve-promise` and `break-promise` no +longer try to migrate queued messages; they only update the promise +state. Pipelining still works for the FullFiller pattern (where the +actor itself emits an `eff-resolve` effect that the vat applies +directly). True over-the-wire pipelining is deferred to Phase 1. + +**Verdict.** Honest scope cut. Documented in +`vat.prologos:resolve-promise` and the `core.prologos` top docstring. + +--- + +### #18 — Multi-arity `defn` with constructor patterns matches first arg only (2026-04-27) + +**Symptom.** Wrote a 2-arg structural-equality function as + +``` +spec transport-eq? Transport Transport -> Bool +defn transport-eq? + | tr-loopback tr-loopback -> true + | tr-tcp-testing-only tr-tcp-testing-only -> true + | tr-loopback tr-tcp-testing-only -> false + | tr-tcp-testing-only tr-loopback -> false +``` + +`(transport-eq? tr-loopback tr-tcp-testing-only)` returned **true**. +The dispatcher matched only the FIRST argument's pattern (`tr-loopback`) +to the FIRST arm and then returned that arm's body, ignoring the +second argument. + +**Cause.** Multi-arity `defn` (the `| pat -> body` shorthand without +explicit args) seems to dispatch on a single argument only. Stdlib +patterns reflect this — `is-zero` is the canonical 1-arg form; +nothing in stdlib's bool/etc. uses multi-pattern multi-arg `defn`. +Two-arg pattern functions are written as nested `match`: + +``` +defn transport-eq? [a b] + match a + | tr-loopback -> + match b + | tr-loopback -> true + | tr-tcp-testing-only -> false + | tr-tcp-testing-only -> + match b + | tr-loopback -> false + | tr-tcp-testing-only -> true +``` + +**Verdict.** Likely a documented-but-easy-to-miss restriction. The +ergonomics of an Erlang-style multi-arg pattern dispatch would help +when porting. Not a blocking bug; recorded so the next person +doesn't step on it. + +**Confirmed 2026-04-29.** During the syntax-idiom sweep +(commit `d65c6ac`) I converted `transport-eq?` to the multi-arity +form again (forgetting #18) and the full OCapN suite on Racket 9.1 +caught it: 158/159, with the failure exactly at +`tests/test-ocapn-locator.rkt:80` — same call site +(`transport-eq? tr-loopback tr-tcp-testing-only` returns true). +Reverting the one function to the nested-match shape restored +159/159. The hazard is specific to clauses where BOTH positional +patterns are 0-arity constructors (e.g. `tr-loopback tr-loopback`) +across multiple alternatives — patterns where the second arg has +a constructor-with-fields (`| v [pst-unresolved _]`, `| state +[syrup-tagged tag p]`, `| [vat n acts proms q] m`) work correctly +in multi-arity form. The narrowing failure appears to be about +the pattern compiler treating leading bare 0-arity constructors as +variable bindings when they shadow nothing. + +**Workaround crystallized.** Multi-arg cross-product over two +0-arity-ctor enums → write as nested `match`. Multi-arg with at +least one constructor-with-args pattern → multi-arity `defn` is +fine. + +--- + +### #19 — TCP framing for testing-only is line-oriented (design pitfall) + +**Symptom.** Endo's `tcp-test-only.js` does NOT define wire framing +itself — it streams raw bytes via `socket.write` and the higher +CapTP layer is responsible for length prefixing. + +**Our choice.** For Phase 0 we use ONE-LINE-PER-MESSAGE framing in +`tcp-ffi.rkt`: each Syrup-encoded value is followed by `\n`; on +read, the receiver consumes one line via `read-line`. This keeps +the FFI minimal (no length-prefix code, no buffering ring needed). + +**Limit.** Doesn't carry binary payloads — Syrup byte-strings could +contain `\n`. Phase 1 should swap line framing for length-prefixed +framing or for the canonical bytewise Syrup transport. Until then, +"tcp-testing-only" only carries the textual subset. + +**Verdict.** Honest scope cut, named explicitly. Keeps the path to +Phase 1 short — only `tcp-ffi.rkt`'s `tcp-send-line`/`tcp-recv-line-ret` +need to change to length-prefixed primitives. + +--- + +### #20 — `:requires (Cap)` annotation must be on same line as `foreign` (2026-04-27, ergonomics) + +**Symptom.** Multi-line foreign declaration: + +``` +foreign racket "tcp-ffi.rkt" + :requires (NetCap) + [tcp-listen :as tcp-listen-raw : Nat -> Nat] +``` + +errors with: +``` +foreign: Expected: (name [:as alias] : type), got: (:requires (NetCap)) +``` + +**Cause.** The `foreign` parser expects keyword-tag pairs and +brackets on the *same line*. WS-mode line continuation isn't +applied here. + +**Workaround.** Compress to one line per foreign: +``` +foreign racket "tcp-ffi.rkt" :requires (NetCap) [tcp-listen :as tcp-listen-raw : Nat -> Nat] +``` + +**Verdict.** Cosmetic but annoying for libraries with long +type-signatures. Worth a parser fix to allow indented continuation +of a `foreign` form. + +--- + +### #21 — Multi-line clause body silently produces `??__match-fail` holes (2026-04-29, real bug) + +**Symptom.** A `defn` whose `match` clause body spans multiple +indented lines compiles without error but evaluates to +`??__match-fail : `: + +```prologos +defn encode [v] + match v + | syrup-null -> "n" + | syrup-bool b -> + match b + | true -> "t" + | false -> "f" + | syrup-string s -> + str::append [str::from-int [str::length s]] + [str::append "\"" s] ;; 2-line body — BROKEN + ... +``` + +`(eval (encode (syrup-string "hi")))` returns +`"??__match-fail : String"` even though the pattern clearly +matched. + +**Cause.** Layout-rule interpretation of clause continuation. A +body that has its function head on one line and its argument +list on another is parsed as TWO separate forms, not one +application. The first becomes the body of the clause; the +second becomes some sort of layout-detached fragment that +elaborates to a hole. + +**Workaround.** Either (a) collapse the body to a single line, or +(b) put the entire body on the line BELOW the `->`, indented +strictly past the `->`: + +```prologos +;; (a) single line: +| syrup-string s -> str::append [str::from-int [str::length s]] [str::append "\"" s] + +;; (b) body on its own line: +| syrup-string s -> + str::append [str::from-int [str::length s]] [str::append "\"" s] +``` + +What does NOT work: head on `->` line, args on subsequent lines +at lesser indentation. + +**Verdict.** Silent failure mode — no compile error, just a hole +masquerading as a value. The same hazard appears in the +clause-continuation example in `prologos-syntax.md` § "Multi-line +clause body" (which says the body must be indented past the `|`, +but that's necessary, not sufficient — multi-line continuation +of a multi-token application is the breaking case). + +**Discovered.** Phase 1 of OCapN interop (commit `1ad3e60`) — +all encoder branches with multi-line bodies returned match-fail +sentinels. Took ~1 hour to diagnose because the symptom +(every branch falls through) hid the cause (layout +mis-parse of one specific body shape). + +**Codify-it ask.** A diagnostic that flags "this clause body +elaborated to a hole" with a layout hint would close this gap. +The hole has the right type, so type-checking passes — only the +runtime sentinel reveals the bug. + +--- + +### #22 — `Option Nat -> SyrupValue` parses as multi-arg Pi, not `(Option Nat) -> SyrupValue` (2026-04-29, real bug) + +**Symptom.** A spec like + +```prologos +spec opt-pos Option Nat -> SyrupValue +``` + +triggers `Type mismatch` at IMPORT time (not at elaboration of +the defining module), with no usable error context: + +``` +imports: Error loading module prologos::ocapn::captp-wire: Type mismatch +``` + +**Cause.** Without explicit brackets, `Option Nat -> SyrupValue` +is parsed as a 3-argument Pi `Option -> Nat -> SyrupValue`, not +as `[Option Nat] -> SyrupValue`. The mismatch surfaces only when +another module imports the function and tries to instantiate the +spec. + +**Workaround.** Bracket the parametric type in the spec: + +```prologos +spec opt-pos [Option Nat] -> SyrupValue +spec encode-safe SyrupValue -> [Option String] +spec decode-op String -> [Option CapTPOp] +``` + +This applies to ALL return / parameter positions where a type +constructor takes its own argument. `Option`, `List`, `Result` +etc. all need the brackets. + +**Verdict.** Easy to miss because (a) the function elaborates +fine in its own module, (b) the import error message gives no +location or hint about which spec is wrong. Once you know the +fix it's mechanical, but the discovery cost is high. + +**Discovered.** Phase 2 of OCapN interop (commit `50fc0c1`) — +six functions in `captp-wire.prologos` had unbracketed +`Option X` return types. The first failure narrowed the scope; +fixing them in one pass took 30 seconds. + +**Codify-it ask.** A spec-level lint or just a less generic error +message ("Type mismatch in spec for `opt-pos`: parametric type +`Option` expected an argument; did you mean `[Option Nat]`?") +would eliminate this. + +--- + +### #23 — Multi-token `defn` body on a single line needs outer `[…]` brackets (2026-04-29, real bug) + +**Symptom.** + +```prologos +defn desc-export [n] syrup-tagged "desc:export" [syrup-nat n] +``` + +triggers `Type mismatch` at import. The body `syrup-tagged "..." [syrup-nat n]` +is being parsed as something other than a 3-element application. + +**Workaround.** Either (a) wrap the body in `[…]`: + +```prologos +defn desc-export [n] [syrup-tagged "desc:export" [syrup-nat n]] +``` + +or (b) put the body on its own line, indented past the `[args]` +header: + +```prologos +defn desc-export [n] + syrup-tagged "desc:export" [syrup-nat n] +``` + +Both work. The single-line bare-juxtaposition form +`defn f [args] head a b c` does not. + +**Cause.** Same family as #21 — WS-mode application is bracket- +delimited; bare juxtaposition needs an enclosing form to anchor +the parse. + +**Verdict.** Silent error class — like #21 the failure is at +import (or evaluation), not at the `defn` itself. + +**Discovered.** Phase 2 of OCapN interop (commit `50fc0c1`) — +multiple `desc-*` helpers in captp-wire.prologos had this shape. +Fixed by moving bodies to their own line. + +--- + +### #24 — Phase-1 wire decoder asymmetry: `+` suffix produces `syrup-int`, never `syrup-nat` (2026-04-29, design choice) + +**Context.** OCapN's Syrup wire format uses `"+"` for +non-negative integers and `"-"` for negatives. There is +no separate Nat wire form — Naturals are just non-negative +integers. So `(syrup-nat 5)` and `(syrup-int 5)` BOTH serialise +to `5+`. + +**Symptom.** A round-trip `(decode (encode (syrup-nat 5)))` +returns `(syrup-int 5)`, not `(syrup-nat 5)`. Functions that +match on `syrup-nat` (via `get-nat`) fail to extract the value +from a decoded Nat-on-the-wire because the decoder always emits +`syrup-int`. + +**Workaround.** Phase 2's `wire-nat` helper (in +`captp-wire.prologos`) accepts both `syrup-nat` and `syrup-int` +(when the int is ≥ 0) and bridges back to the model's Nat type +via a structural-recursion `int-to-nat` helper. + +**Verdict.** Not a bug, but a subtle modelling tradeoff: +- pro: the wire is one-to-one with the byte sequence; encode is + total over both Int and Nat +- con: round-tripping a `syrup-nat` doesn't preserve identity +- con: any decoder that wants Nat positions has to bridge + +**Codify-it ask.** Either (a) drop `syrup-nat` from the value +type entirely (subsume into Int), or (b) make the decoder pick +syrup-nat for `+` suffix and syrup-int only for `-`. Either is +fine; the current asymmetry is just a minor wart. + +**Discovered.** Phase 2 of OCapN interop (commit `50fc0c1`). + +--- + +### #25 — Prologos `String` return values come back through the test fixture with print-escapes that need `read`-back (2026-04-29, ergonomics) + +**Symptom.** A Phase 3 test that pulls the bytes of a Prologos +`encode-op` call into Racket-side TCP code got wire bytes with +literal `\"` instead of `"`: + +```racket +(define wire-bytes (extract-value-bytes (run-last "(eval ...)"))) +;; got: "<8'op:abort13\"phase-3-works>" ;; 1 backslash + 1 quote +;; expected: "<8'op:abort13\"phase-3-works>" ;; raw quote +``` + +**Cause.** The fixture's `run-last` returns the Prologos pretty- +printer output, which uses C-style escapes (`\"`, `\\`) for +String values. Naively stripping the `"..."` wrapper preserves +those escapes in the Racket string, so subsequent uses see +phantom backslashes. + +**Workaround.** `read` the quoted form back as a Racket string +literal: + +```racket +(define m (regexp-match #px"^(\".*\") : String$" s)) +(read (open-input-string (cadr m))) ;; round-trips the escapes +``` + +**Verdict.** Test-helper-level pitfall, not a Prologos bug — +the printer is doing the right thing (round-trippable output). +Worth codifying as a reusable helper in `test-support.rkt` if +more interop tests appear. + +**Discovered.** Phase 3 of OCapN interop (commit `b4493a1`). + +--- + +### #26 — `syrup-tagged` model carries one payload, but OCapN records are arity-N (2026-04-29, real bug) + +**Symptom.** Encoding `op:start-session "0.1" "tcp-testing-only:peer-A"` +through Phase 2's `op-to-syrup` produced + +``` +<16'op:start-session[3"0.128"tcp-testing-only:peer-A]> +``` + +— a record with ONE child, a list of two strings — instead of the +canonical OCapN form + +``` +<16'op:start-session3"0.128"tcp-testing-only:peer-A> +``` + +— a record with TWO children. The Phase 4 cross-impl byte-equality +test missed it because every Phase-4 vector was a 1-arity record. +The Phase 6 handshake test caught it the moment a real `@endo/ocapn` +peer tried to extract version + locator from the record's children +and got `null` for both fields. + +**Cause.** `data SyrupValue` declares +`syrup-tagged : String -> SyrupValue`, i.e. one label and ONE +payload. The Phase-2 encoder packed multi-arg ops as +`(syrup-tagged label (syrup-list args))` which round-trips +through the Prologos decoder fine (the decoder's `decode-record-with` +explicitly wraps arity ≥ 2 records back into `(syrup-tagged label +(syrup-list rest))`) but emits the wrong wire bytes. + +**Workaround applied.** Added `encode-record : String [List +SyrupValue] -> String` to `syrup-wire.prologos`. It produces +`<` + symbol(label) + concat(encode each arg) + `>` directly, +bypassing the syrup-tagged constructor for multi-arity cases. +Phase 2's `encode-op` now uses `encode-record` for the 5 +multi-arity ops (start-session, deliver, deliver-only, listen, +gc-export) and keeps `wire::encode (syrup-tagged ...)` only for +the 1-arity ops (abort, gc-answer). + +**Verdict.** Real bug in the model abstraction. The fix is +asymmetric — encode goes through a special path; decode wraps in +syrup-list. A cleaner future fix is to extend `data SyrupValue` +with an N-arity record constructor, e.g. +`syrup-record : String -> [List SyrupValue]`, and treat the +1-arity case as a syntactic sugar. + +**Discovered.** Phase 6 of OCapN interop. + +--- + +### #27 — Prologos `decode-op` is catastrophically slow on multi-arity records (2026-04-29, perf bug) + +**Symptom.** Decoding a 60-byte op:start-session record via +`decode-op` takes **~7 minutes** of reducer wall time. The function +returns the correct value — the round-trip is sound — but takes +unbounded time per decode. + +``` +warmup encode-op... cpu time: 317 ms +decode short start-session... cpu time: 454,832 ms +``` + +**Likely cause.** The decoder's recursive structure +(`decode-many-loop` calls `decode-at` per element, which calls +`decode-many-loop` for nested records, which closes over many +SyrupValue cons cells) interacts badly with the Prologos reducer's +beta-reduction strategy. Each decode step accumulates large +substituted closures, producing exponential-ish work. + +**Workaround in this port.** Phase 6's bidirectional handshake +test asserts byte-equality directly (`their-line == +expected-prologos-bytes`) instead of decoding the received bytes +via Prologos. Byte equality is a strictly stronger correctness +signal anyway: if the bytes match, both decoders trivially recover +the same SyrupValue. + +**Verdict.** Real perf bug in the Prologos reducer (or the way +the decoder's recursion compiles to it). A proper fix needs +either a less-recursive decoder shape or compiler-level changes. +Not a blocker for interop validation — byte equality is the +preferred signal — but it would block any Prologos OCapN node +running in production. + +**Discovered.** Phase 6 of OCapN interop. +The 1-arity round-trip path used in Phase 5's +`test-ocapn-live-interop.rkt` (op:abort, op:gc-answer) doesn't +exhibit the issue — only multi-arity records do. + +**Profile data (2026-05-01).** Decode of `<3'tag5"hello>` +(1-arity record, 13 bytes): **~28s** consistently across 5 +iterations, with 538 reduce_steps × ~52 ms/step. Decode of +`<16'op:start-session3"0.110"loc-string>` (3-arity record, +~40 bytes): **~270s**, with 763 reduce_steps × ~354 ms/step. +Resetting `reset-meta-store!` and `reset-constraint-store!` +between calls did NOT change the timing (so the cost is NOT +accumulation across calls). The cost is intrinsic to each +decode and grows super-linearly with record arity. + +The likely culprit is the HOF self-reference: `decode-many-loop` +takes `decode-at` as an argument; the closure-substitution path +in the Prologos reducer compounds across recursive calls. +Combined with the 10-constructor pattern-match per +SyrupValue match, each step is doing ~52-354ms of work. + +**Three lines of attack** (option 4 SHIPPED 2026-05-01): +1. Inline `decode-many-loop` into `decode-at` (eliminate HOF + passing). Smallest scope; tests Prologos's HOF-substitution + cost specifically. +2. Move decoder to Racket FFI primitive (one big function). + Loses self-hosting purity. +3. Fix the reducer's closure-substitution hot path. + Most principled but largest scope. +4. **(SHIPPED Phase 13)** Combine two pure-Prologos rewrites + in syrup-wire.prologos: + - Tail-recursive accumulator + `reverse` for `decode-many-loop` + (was non-tail-rec head-cons recursion holding deep substitution + chains). + - Inline destructure of `Decoded` / `DecodedMany` structs at + match position (`some [decoded v end] ->`) instead of + accessor calls (`d-value` / `d-consumed`), which were each + a separate pattern match per access. + + Measured speedup vs the baseline above: + - 1-arity record: 28s → **4.5s** (6.2× faster) + - 3-arity record: 270s → **10.8s** (25× faster) + - decoder-using round-trip tests now run in <1 min instead + of timing out the runner. + +The remaining cost is still substantial (4.5s per 1-arity decode +is far slower than a function call should be) but the decoder is +now usable for bridge tests. Options 1/2/3 are still candidates +for further work if production loads emerge. + +The 1-arity round-trip Phase-5 tests already tolerated the cost +(<10s per decode); Phase 6+ tests originally sidestepped via byte +equality but could now use decode-and-compare if desired. + +--- + +### #28 — `@endo/ocapn` rejects `null` as a record child; use `false` for "absent" (2026-04-29, real interop bug) + +**Symptom.** Phase 8's RPC test sent + +``` + 4"ping" n> +``` + +— a 4-arity record where the resolver field is the Syrup `n` +(null) atom representing `none`. `@endo/ocapn`'s `decodeSyrup` +errors out at the first byte: + +``` +SyrupAnyCodec: read failed at index 0 of +``` + +When the Node side then tried to encode its own reply with +`null` in the same position, the *encoder* failed too: + +``` +SyrupAnyCodec: write failed at index 43 of +``` + +**Cause.** `@endo/ocapn`'s `AnyCodec` (in +`src/syrup/js-representation.js`) doesn't include `null` in +either its read-type-hint or write-type table. The `n` atom is +a valid wire byte but not a valid record-child *value* in +Endo's JS representation. The OCapN spec uses `false` (the +single-byte `f` atom) for "absent" sentinel positions. + +**Workaround applied.** +- `captp-wire.prologos`'s `opt-pos` now emits + `(syrup-bool false)` for `none`, not `syrup-null`. +- `unwrap-opt-desc` accepts both `syrup-bool false` and + `syrup-null` for `none` (forward compatibility — older + Prologos peers may still emit `null`). + +**Verdict.** Real interop bug. Phase 4-7 didn't surface it +because none of those vectors exercised the resolver/answer-pos +absence in a record sent TO `@endo/ocapn`. Phase 8 (RPC) +hit it on the very first deliver. + +**Discovered.** Phase 8 of OCapN interop. + +--- + +### #29 — `break` from `prologos::ocapn::promise` collides with `prologos::data::list::break-helper` in sexp-mode resolution (2026-05-01, ergonomics) + +**Symptom.** Calling `(break (syrup-string "oops") fresh)` in +sexp-mode (a test fixture context) inside a function that +expects a `PromiseState` — the resulting expression doesn't +reduce. The pretty-print shows +`[prologos::data::list::break-helper ?meta ...]` instead of +`[prologos::ocapn::promise::pst-broken ...]`. The wrong `break` +got picked up. + +**Cause.** `prologos::data::list` (transitively imported via +`prologos::ocapn::core`) provides a `break-helper` and exposes +`break` as well. The sexp-mode test imports `core :refer-all` +which surfaces both. Symbol resolution preferentially picks the +list one. + +**Workaround.** Use the constructor directly when constructing +test data: `(pst-broken reason)` instead of `(break reason fresh)`. +The constructor is unambiguous; only the convenience wrapper +`break` collides. + +**Verdict.** Real ergonomics issue. Renaming `break` in +`promise.prologos` to `mark-broken` would resolve it. Or +namespace-qualified imports. Or making sexp-mode resolution +prefer the most-recently-required module. + +**Discovered.** Phase 17 of OCapN interop — first time we +exercised broken-promise bytes encoding. + +--- + +### #30 — `match` inside a 7+ binding `let`-chain triggers elaborator inference failure (2026-05-04, real bug) + +**Symptom.** A driver expression in a test fixture that chains +~7 `let` bindings ending in a `match` expression fails to elaborate +with "Could not infer type" — every let-binding's parameter type +is held as an unsolved metavariable. Replacing the `match` with a +direct call (e.g., `unwrap-or default (nth zero list)`) makes +inference succeed; replacing with `length list` succeeds; replacing +the same shape with a top-level `defn` helper that wraps the +`match` succeeds. So the bug is specifically about an inline +`match` form sitting at the END of a deep let-chain, where the +outer binding types lack a forcing context. + +**Repro.** This shape fails: + +``` +(eval (let (op1 (unwrap-or (op-abort \"d1\") (decode-op \"<10\\\"op:abort3\\\"bye>\"))) + (let (op2 (unwrap-or (op-abort \"d2\") (decode-op \"<10\\\"op:abort3\\\"bye>\"))) + (let (sa (vat-spawn-actor beh-echo syrup-null empty-vat)) + (let (cs0 (conn-state (alloc-vat sa) bridge-state-empty nil false)) + (let (step1 (connection-step op1 cs0)) + (let (step2 (connection-step op2 (conn-step-state step1))) + (let (all (append (conn-step-outbound step1) (conn-step-outbound step2))) + (match all ;; <-- elaborator can't solve metas + | nil -> "NO-OUT" + | cons hd _ -> hd))))))))) +``` + +This same shape with `(length all)` instead of `match` succeeds. +This same shape with `(unwrap-or "NO" (nth zero all))` succeeds. + +**Hypothesis.** The match form's type-checking goes through a +different inference path than ordinary function application. When +the surrounding context is a deep nested `let` (each binding +introduces a fresh metavariable), the match's type-driven +inference can't propagate downward to the outer let-bindings. +Function applications can — perhaps because they have a clearer +arg→result type relationship — so `unwrap-or` and `nth` succeed +where match fails. + +**Workaround.** Two options: +1. Replace the `match` with a function call that has the same + semantics — e.g., `unwrap-or default (nth zero list)` for + "head with default." +2. Define a top-level `defn` that wraps the `match` and call it + instead. The function's spec gives the type-checker an anchor + it doesn't have for the inline match. + +**Discovered.** Phase 24 of OCapN interop (bridge-driven responder +interop test). The driver expression initially used `match all | +nil -> default | cons hd _ -> hd` to extract the first outbound +byte string from a list of two `connection-step` calls. Replaced +with `unwrap-or default (nth zero ...)` and elaboration succeeded. + +**Verdict.** Real Prologos elaborator bug. Workaround is cheap +(use a function instead of inline match in deep let-chains), but +the inference engine should handle this — match is supposed to be +a fundamental form. Worth filing a Prologos issue with this +specific repro. The shape generalizes beyond OCapN — any test +fixture using `process-string` to drive multi-step workflows could +hit this. + +--- + +### #31 — `decode-op` on a 50-byte op:deliver takes ~150 SECONDS in `process-string` eval (2026-05-04, perf bug, MEASURED) + +**MEASURED 2026-05-04**: `(eval (decode-op "<10'op:deliver<11'desc:export0+>5\"hello<11'desc:answer7+>f>"))` +in a `process-string` call took **150,321 ms (150 seconds)** for a +50-byte input. That's ~3ms per byte. A sane decoder for bytes-this-shaped +should complete in <10ms total. This is the underlying cause of all +"Phase 24 takes 8+ minutes" symptoms. + +The result was correct: +~[some [op-deliver 0N "hello" [some Nat 7N] [none Nat]]]~ — i.e. the +decoder produces the right answer, just 1000x to 10000x slower than +expected. Diagnostic test: `tests/test-bridge-perf.rkt`. + +**Symptom.** Phase 24's bridge-driven responder interop test +(`test-ocapn-bridge-interop.rkt`) drives the full bridge pipeline +on a Node-emitted `op:deliver` frame: + +``` +(let (op (unwrap-or (op-abort "decode-failed") (decode-op )) + sa (vat-spawn-actor beh-echo syrup-null empty-vat) + step (captp-incoming-with-state op (alloc-vat sa) bridge-state-empty) + v2 (drain (suc^8 zero) (bridge-step-vat step)) + pr (pump-outbound v2 (bridge-step-state step) nil)) + (unwrap-or "NO-OUTBOUND" (nth zero (pump-result-bytes pr)))) +``` + +This expression evaluated via `process-string` exceeds **90s** of +Racket CPU time in the full elaboration + reduction loop. Existing +unit tests in `test-ocapn-bridge.rkt` that exercise the same chain +(e.g., "bridge/pump-outbound emits bytes when a question's promise +is fulfilled") with **hand-constructed** ops (not `decode-op`- +produced) complete in ~1s. + +**Where the time goes** (now measured): the bottleneck is `decode-op` +itself, not the bridge. Confirmed by isolating each layer: +- `(eval (decode-op BYTES))` alone: ~150 seconds. +- `(eval (drive-echo-bridge-once ))` (no decode): + ~80 seconds in the first run with hand-coded ops. +- The combined chain `decode-op + bridge`: ≥ 8 minutes (killed at + that point; never observed completing). + +So decode-op contributes the lion's share of the cost. The bridge +itself (which involves comparable amounts of structural work — vat +event loop, question table, pump-outbound encoding) runs ~2× faster. + +**Hypothesis on root cause** (unverified). `decode-op` is a +recursive parser in `lib/prologos/ocapn/captp-wire.prologos` that +calls `wire::decode-value` (defined in `syrup-wire.prologos`). +The parser uses position-threading via tuples, deep `match` chains, +and each parsed sub-value allocates a fresh `SyrupValue` ctor and +a position pair. Combined with the elaborator's reduction strategy +in `process-string`, that may produce O(n²) or worse reduction +behavior on the input string. The decoder's *output* is correct +(verified — produces the expected `op-deliver` shape); only its +*throughput* is broken. + +**Investigation paths**: +1. Profile reduction inside `wire::decode-value` for inputs of + length 10, 50, 100. If timing is super-linear in length, that + confirms an algorithmic issue in the decoder's structural + recursion under Prologos reduction. +2. Compare against `(eval (encode-op ))` timing. + If encode is fast and decode is slow, the asymmetry is in how + the elaborator handles parser combinators vs constructor + applications. +3. Try a *flat* alternative decoder (e.g., a foreign Racket call + that returns a `SyrupValue` directly), keeping `syrup-to-op` + on the Prologos side. If that's fast, the problem is isolated + to the byte-level parser, not the SyrupValue→CapTPOp conversion. + +**Workaround for now.** Test stays in `.skip-tests`. Phase 24 ships +as scaffolding (Node peer + test skeleton + library helper + +diagnostic test + this pitfall). Live end-to-end gate deferred +to a Prologos decoder perf fix. + +**Discovered.** Phase 24 of OCapN interop. The perf gap between +unit tests with hand-coded ops and a real interop test that decodes +Node-emitted bytes blocks the live bridge-driven test from being +the regression gate it could be. + +**Verdict.** Real perf gap. Worth investigating because: (a) it +limits the interop test matrix; (b) once fixed, every protocol port +that uses `process-string`-driven test fixtures benefits; (c) the +gap signals something about how Prologos's reduction handles +decoder-produced expression trees that may matter for self-hosting. + +--- + +### #32 — Multi-constructor `data` types break cross-module inference for callers using bound vars (2026-05-06, real bug) + +**Symptom.** A `data` type with TWO OR MORE constructors (e.g. +`bridge-step` and `bridge-step-out`) compiles fine in its defining +module, BUT a caller in a DIFFERENT module that takes 2+ bound +arguments and passes them to a function returning that data type +fails to elaborate with "Could not infer type" — function-arg +types come back as `<_>` (uninferred metavars) even though the spec +declares them concretely. + +**Repro skeleton.** Inside module `M1`: + +``` +data Step + step : Vat -> State ;; ctor 1 + step-out : Vat -> State -> List String ;; ctor 2 + +spec do-step Op Vat State -> Step +defn do-step | ... -> step v st ;; or step-out v st bytes +``` + +Inside an importing module `M2`: + +``` +require [M1 :refer-all] + +;; FAILS — "Could not infer type" +spec wrap Op Vat State -> Vat +defn wrap [op v st] + let s := [do-step op v st] + [step-vat s] +``` + +The 2-bound-arg form `wrap` cannot elaborate. Adding a typed let +(`let s : Step := ...`) doesn't help. Inlining doesn't help. Same +function inside `M1` itself works fine. + +**Empirical evidence.** Discovered in OCapN Phase 25 (handshake +modelling, commit `4b92416`). I extended `BridgeStep` with a +second constructor `bridge-step-out` carrying immediate-outbound +bytes. The defining module `captp-bridge.prologos` continued to +compile cleanly — `connection-step` (which uses `bridge-step-vat`, +`bridge-step-state`, `bridge-step-immediate`) was fine. But the +importing module `bridge-interop-helpers.prologos` failed to define +EVERY multi-arg helper that called `captp-incoming-with-state` and +then unpacked the result — including 1-let-deep helpers, even with +explicit `: BridgeStep` annotations on the binding. + +The probe matrix isolated it precisely: + +| function shape | defines? | +|-----------------------------------------------------------|----------| +| 1-arg + let + captp-call (constants for other args) | yes | +| 1-arg + let + captp-call (constant deps) | yes | +| 2-arg + let + captp-call (1 bound + 1 constant) | NO | +| 3-arg + let + captp-call (3 bound) | NO | +| 2-arg + INLINE + captp-call (no let, all bound) | yes | +| 2-arg + let + captp-call returning a SINGLE-ctor type | yes (untested but consistent with reverting) | + +The single-ctor-type case was the workaround. Reverting the +multi-constructor extension and putting the "immediate outbound" +field on the SINGLE-CONSTRUCTOR `BridgeState` instead made every +caller compile. So the multi-constructor return type, NOT the let +or the call shape, is the trigger. + +**Hypothesis.** The elaborator's bidirectional inference for +function applications can't pin down the return type of a function +returning a multi-constructor data type when the call's arguments +include 2+ unsolved metavariables (the function-arg vars whose +types haven't been propagated from the spec yet). With a +single-constructor return type, the constructor's signature +uniquely determines the type, but with N constructors the +elaborator may delay the choice in a way that fails to back-propagate +through the let. + +**Workaround.** Avoid multi-constructor data types when the +constructor's primary use is "value with optional extra payload." +Two options: + +1. **Single constructor with all fields (some optional).** Add a + `[List X]` or `[Option X]` field that's `nil` / `none` for the + bare case. Trade-off: every caller now matches an extra field, + but it's a wildcard. This is what `BridgeState`'s `pending-out` + field does. + +2. **Wrap the optional payload in a separate function.** Instead of + "constructor with X" + "constructor without X," have a single + constructor + a separate accumulator (e.g. a list field or a + queue) that the producing function appends to. + +**Discovered.** OCapN Phase 25, commit `4b92416`. Initial design +added `bridge-step-out v st [List String]` as a second constructor +to BridgeStep so the dispatch could carry "immediate outbound bytes." +Cost about 1 hour of probing the elaborator with shrinking test +cases before realizing the multi-constructor extension was the root. + +**Verdict.** Real Prologos elaborator bug. The single-constructor +workaround (move the optional payload into the existing +single-constructor type as a list/option field) is uniformly +applicable and clean. Filed as [issue #60](https://github.com/LogosLang/prologos/issues/60) +because: (a) the catastrophic failure mode (cross-module callers +can't compile) is far enough from the surface cause (data type +definition in a DIFFERENT module) that it's hard to diagnose; +(b) multi-constructor data types are fundamental — it's a real +expressivity gap until fixed; (c) the workaround works but adds +field plumbing to every accessor and update function. + diff --git a/docs/tracking/2026-04-30_LLVM_LOWERING_TIER_0_2.md b/docs/tracking/2026-04-30_LLVM_LOWERING_TIER_0_2.md new file mode 100644 index 000000000..f20032790 --- /dev/null +++ b/docs/tracking/2026-04-30_LLVM_LOWERING_TIER_0_2.md @@ -0,0 +1,304 @@ +# LLVM Lowering — Tiers 0–2 (SH Series, Track 1) + +**Date**: 2026-04-30 +**Status**: Stage 3 design + Stage 4 implementation interleaved (per Tier-as-Phase Protocol) +**Series**: SH (Self-Hosting) — first track, scope-limited proof of concept +**Branch**: `claude/prologos-layering-architecture-Pn8M9` +**Cross-references**: +- [LANGUAGE_VISION.org § Self-Hosting → LLVM → Logos](principles/LANGUAGE_VISION.org) +- [SEXP_IR_TO_PROPAGATOR_COMPILER](../research/2026-03-30_SEXP_IR_TO_PROPAGATOR_COMPILER.md) § Phase 2 +- [MASTER_ROADMAP.org § SH Series placeholder](MASTER_ROADMAP.org) (line 258) + +--- + +## 1. Summary + +Add a Racket-hosted LLVM lowering pass that reads typed AST values produced by `elaborate-top-level` and emits LLVM IR. Three tiers, each a self-contained milestone with CI-runnable tests: + +- **Tier 0** — `Int` literal returned by `main` (exit code). +- **Tier 1** — Arithmetic, comparisons, and conversions over `Int`/`Bool` (no closures, no allocation). +- **Tier 2** — Top-level functions with non-capturing parameters, direct calls, and one-line `m0` erasure for type-level binders. + +Tier 2 is the natural break before deeper Phase-2 blockers (closure conversion, GC, layout, IO) kick in. + +## 2. Progress Tracker + +| Phase | Description | Status | Notes | +|-------|-------------|--------|-------| +| Plan | Write this document | ✅ | initial draft | +| T0.A | Driver hook: extract typed body of `def main` | ✅ | `lower-program/from-global-env` queries `global-env-lookup-{type,value}` after `process-file` populates the env | +| T0.B | LLVM emitter for `expr-int`, `expr-Int` | ✅ | `racket/prologos/llvm-lower.rkt` — closed pass; `unsupported-llvm-node` exn for everything else | +| T0.C | Tier 0 acceptance file + Racket-side test | ✅ | `examples/llvm/tier0/{exit-42,exit-0,exit-7}.prologos` + `tests/test-llvm-lower.rkt` | +| T0.D | Tier 0 CI integration | ✅ | `.github/workflows/llvm-lower.yml` runs unit + e2e | +| T0.✅ | Tier 0 commit | ✅ | `9f84490` | +| T1.A | Lowering for `expr-int-{add,sub,mul,div,mod,neg,abs}` | ✅ | scope narrowed: comparisons deferred to a later tier (no `if`/match yet means Bool is unusable) | +| T1.B | `expr-app` for primitive-rooted application | ✅ | OQ-T1-1 resolved: parser produces `surf-int-add` directly; elaborator → `expr-int-add`. No eta-expansion to handle. | +| T1.C | Tier 1 acceptance file + tests + CI | ✅ | 8 example programs + 10 rackunit tests + CI step | +| T1.✅ | Tier 1 commit | ✅ | `307e995` | +| T2.A | `expr-lam` lowering at top level (non-capturing only) | ✅ | `lower-function/tier2` walks the curried lambda chain via `collect-lambdas`, asserts it matches the type's Pi chain | +| T2.B | `expr-bvar` → SSA local; `expr-app` → `call` | ✅ | `current-bvar-env` parameter holds innermost-first env; `lower-app/tier2` uncurries the application chain | +| T2.C | `m0` binder drop (single-line erasure at top level) | ✅ | m0 binders contribute `'erased` to env (so de Bruijn distances stay correct) but emit no LLVM parameter; m0 args at call sites are dropped via `#:when` filter | +| T2.D | Free-variable detector (refuses captures with clear error) | ✅ | `lookup-bvar` raises `unsupported-llvm-node` when index ≥ env length, with a hint about closure capture | +| T2.E | Tier 2 acceptance file + tests + CI | ✅ | 4 example programs + 8 rackunit tests (positive + negative paths) + CI step | +| T2.✅ | Tier 2 commit | 🔄 | next | + +## 3. Scope + +### In scope (Tier 0–2 sum) + +- `def main : Int := ` as the entry point +- `def name : T := ` for ground `T ∈ {Int, Bool}` +- `defn name [x y ...] := ` with all parameters of type `Int` or `Bool` and no captures +- Primitive Int operators from `elaborator.rkt:795` (`int+`, `int-`, `int*`, `int/`, `int-mod`, `int-neg`, `int-abs`, `int-lt`, `int-le`, `int-eq`) +- Direct application of a known top-level definition or primitive +- `m0`-multiplicity binders dropped (degenerate case: erasure for type-only parameters) + +### Out of scope (deferred to later SH tracks) + +- Heap allocation, GC, layout for sums/products +- Closures with free variables (lifted Tier 2 detector raises a clear error) +- Polymorphism that requires monomorphization +- `Rat`, `Nat`, `String`, `List`, user data types +- Effects / IO beyond `main`'s exit code +- Pattern matching to LLVM CFG (Tier 3) +- Promotion of the lowering pass to a propagator stratum (recorded as scaffolding; see § 5) + +### Failure mode + +The lowering pass is **closed**: encountering any AST node not in the supported set raises `(unsupported-llvm-node node sub-tier)` with the struct kind, source location (when present), and a hint pointing to the next tier or to the SH-series gap. No silent fallthroughs, no no-ops, no fallbacks. Boundary failure aligns with the project's "validate at system boundaries" rule. + +## 4. WS Impact + +None. Tier 0–2 add no surface syntax. The existing reader, parser, and elaborator produce typed AST; the lowering pass is a new *output* mode invoked after `process-file`. + +## 5. Mantra Alignment — honest scaffolding statement + +> "All-at-once, all in parallel, structurally emergent information flow ON-NETWORK." + +The Tier 0–2 lowering pass is a Racket function. It is **not** a propagator stratum. It is **scaffolding** for SH Phase 2, and labelled as such. + +Where it aligns: +- **Information flow**: input is read from typed AST cells produced by the elaboration network. The pass is a *consumer* on the network's output boundary. Reading from cells is the right side of the boundary. +- **No off-network mutation of compiler state**: the pass does not write to cells, does not register propagators, does not introduce ambient parameters that hold compiler state. + +Where it does not align (and why that is acceptable here): +- **Not all-at-once / not in parallel**: the function walks the AST sequentially. There is no broadcast, no fan-in latch, no per-node propagator. Justification: the pass is at a *system boundary* (compiler emitting a textual artifact) and the items are not independent in the relevant sense — instruction emission within a basic block is sequential by SSA construction. +- **Not structurally emergent**: control flow decides which case fires (`match` on the AST struct kind). Justification: same as above; the boundary translates an in-network value to an off-network text format. + +**Retirement plan to the principled form** (deferred, named): +The mantra-aligned form is a **lowering stratum** where each LLVM-instruction-pattern is a registered propagator rule that fires when its input cell (typed AST node) is ready (per [SEXP_IR_TO_PROPAGATOR_COMPILER § 5 question 3](../research/2026-03-30_SEXP_IR_TO_PROPAGATOR_COMPILER.md)). Promotion is a later SH-series track gated on: +1. PPN Track 4D substrate so AST cells are first-class +2. Incremental compilation requirement (PPN Track 8) being in scope +3. A microbench showing per-function lowering is the bottleneck + +Until then, the function form ships and is labelled *scaffolding*. This follows the Validated-Is-Not-Deployed and "Pragmatic-Is-A-Rationalization" disciplines: the gap is named, the trigger conditions for closing it are concrete, the function form is incomplete-because-X (X = stratum form requires PPN 4D + Track 8 prerequisites). + +## 6. NTT Sketch (eventual stratum form) + +For the future stratum form. Not implemented in Tier 0–2; recorded so the function form's signatures can be designed with the eventual cell shapes in mind. + +``` +;; A typed AST node cell holds an expr-* value (lattice: discrete) +cell typed-ast-cell : Cell (Discrete Expr) :reads :writes + +;; A lowering result cell holds an LLVM-IR fragment (string-list lattice: append) +cell llvm-fragment-cell : Cell (AppendList String) :reads + +;; A lowering propagator: one instance per AST struct kind +propagator lower-int-add + :reads (typed-ast-cell input) (llvm-fragment-cell lhs) (llvm-fragment-cell rhs) + :writes (llvm-fragment-cell output) + :where Monotone + :component-paths ... +``` + +The pass emerges from the topology of typed-AST cells. Each AST shape registers a lowering rule (analogous to SRE form registry). Output fragments accumulate via an append lattice. The driver walks the output cells in topological order and serializes. + +This is the principled form. Tier 0–2 does **not** build it. The function form's API (`lower-toplevel : Symbol × Expr × Expr → String`) is shaped to be replaceable by the stratum form without touching callers. + +## 7. File layout + +| Path | Purpose | +|------|---------| +| `racket/prologos/llvm-lower.rkt` | Lowering pass module (function form) | +| `racket/prologos/tests/test-llvm-lower.rkt` | Racket-side unit tests on the IR string | +| `racket/prologos/examples/llvm/tier0/*.prologos` | Tier 0 acceptance programs | +| `racket/prologos/examples/llvm/tier1/*.prologos` | Tier 1 acceptance programs | +| `racket/prologos/examples/llvm/tier2/*.prologos` | Tier 2 acceptance programs | +| `tools/llvm-compile.rkt` | CLI driver: `.prologos` → `.ll` → `clang` → native binary | +| `.github/workflows/llvm-lower.yml` | CI: install clang, run tier acceptance tests | + +## 8. Test strategy + +### Local + +The user runs Racket v9 built from GitHub source. Tests are invoked by `racket` on the user's `PATH`. No hard-coded racket paths. Test commands: + +``` +# Racket-side unit tests (IR string assertions, no LLVM needed) +racket tools/run-affected-tests.rkt --tests tests/test-llvm-lower.rkt + +# End-to-end (requires clang on PATH) +racket tools/llvm-compile.rkt examples/llvm/tier0/exit-42.prologos +./out && echo "exit=$?" +``` + +### CI + +A new GitHub Actions workflow `.github/workflows/llvm-lower.yml`: +1. `actions/checkout@v4` +2. `Bogdanp/setup-racket@v1.11` with `version: '9.0'` (matches existing `test.yml`) +3. `apt-get install -y clang` (Ubuntu runner ships clang via base image; verify version) +4. `raco pkg install --auto --skip-installed` +5. `raco make racket/prologos/driver.rkt racket/prologos/llvm-lower.rkt` +6. **Tier 0 step**: lower + run all `examples/llvm/tier0/*.prologos`, assert exit code matches `:expect ` directive +7. **Tier 1 step**: same for tier1 +8. **Tier 2 step**: same for tier2 +9. **Unit step**: `racket tools/run-affected-tests.rkt --tests tests/test-llvm-lower.rkt` + +Each tier's step is independent so a tier-N regression does not mask tier-N+k results. CI runs are gated on this workflow at PR time. + +### Acceptance file directives + +Each `.prologos` test file ends with a comment of the form: + +``` +;; :expect-exit 42 +``` + +The test driver parses this directive, lowers the file, runs the binary, and asserts. + +## 9. Tier 0 — Literals + +### Goal + +Compile `def main : Int := 42` to a native binary that exits with code 42. + +### Supported AST set + +- `expr-int`, `expr-Int` +- The wrapping shape `(list 'def NAME TYPE BODY)` from `elaborate-top-level` +- Optional `expr-ann` around the body (if elaboration emits one for ascription) + +### Steps + +1. **T0.A — Driver hook**: Modify `process-file` (or add a sibling `process-file-for-llvm`) to return the elaborated top-level forms list. Identify the form whose name is `main`. Extract its body expression and ascribed type. +2. **T0.B — Emitter**: `racket/prologos/llvm-lower.rkt` exports `lower-program : (Listof TopForm) → String`. Tier 0 cases: + - `expr-int n` → emit `i64 n` + - body of `main` is a literal → wrap in `define i64 @main() { ret i64 }` + - All other AST nodes → `(unsupported-llvm-node ...)` +3. **T0.C — Acceptance**: `examples/llvm/tier0/exit-42.prologos` and one negative case (`exit-0.prologos`). +4. **T0.D — CI**: workflow file with the Tier 0 step. + +### Validation + +- Local: `racket tools/llvm-compile.rkt examples/llvm/tier0/exit-42.prologos --emit-only` produces deterministic IR (snapshotted in unit test). +- CI: `examples/llvm/tier0/*.prologos` exit codes match `:expect-exit` directives. + +### Commit message convention + +``` +SH Track 1 Tier 0: literal Int → main exit code + +Adds racket/prologos/llvm-lower.rkt with the closed Tier 0 AST support +(expr-int + main-as-exit-code wrapper). Adds examples/llvm/tier0/, +tests/test-llvm-lower.rkt, tools/llvm-compile.rkt, and the +llvm-lower.yml CI workflow. + +Tier 0 supports: expr-int, expr-Int, (def main Int ). +Any other AST node raises unsupported-llvm-node with source location. + +Scaffolding statement (per plan doc § 5): the lowering pass is a Racket +function, not a propagator stratum. Promotion to a stratum is gated on +PPN Track 4D + incremental compilation requirement. +``` + +## 10. Tier 1 — Arithmetic + +### Goal + +Compile programs like `def main : Int := [int+ 1 [int* 2 3]]` (exit code 7). + +### New AST set (additive) + +- `expr-int-add`, `expr-int-sub`, `expr-int-mul`, `expr-int-div`, `expr-int-mod` +- `expr-int-neg`, `expr-int-abs` + +### Scope narrowing (closed during T1.A) + +The plan originally included `expr-int-{lt,le,eq}` and `expr-Bool`/`expr-true`/`expr-false`. **Removed** because without `if` or pattern-matching control flow (Tier 3 territory), Bool values cannot be observed: a `def main : Bool` would require a Bool→exit-code coercion, and a Bool subexpression cannot drive any branch. The remaining Tier 1 surface (Int → Int → Int and Int → Int) is closed and complete. + +### OQ-T1-1 resolved + +Investigation: `racket/prologos/parser.rkt:1110` and `tree-parser.rkt:300` both produce `surf-int-add` directly for `[int+ a b]`. Elaborator (`elaborator.rkt:1233`) emits `expr-int-add` from `surf-int-add`. **No eta-expansion** survives elaboration for inline primitive applications. The eta table is only consulted when the primitive is referenced as a value (`def f := int+`); inline usage skips it. No beta-reducer needed at the lowering boundary. + +### Validation + +- Tests for each binary op with positive/negative operands +- Tests for each comparison (encoded as exit 0/1) +- Test for nested expressions (`[int+ 1 [int* 2 3]]`) +- Snapshot test of generated IR for one canonical example + +### Commit message + +`SH Track 1 Tier 1: Int arithmetic + comparisons + Bool literals` with the same scaffolding statement carried forward. + +## 11. Tier 2 — Top-level functions + +### Goal + +``` +defn add [x y : Int] := [int+ x y] +def main : Int := [add 5 7] ; exit 12 +``` + +### New AST set (additive) + +- `expr-lam` at top level only, with strict requirements: + - Multiplicity is `mw` (unrestricted) or `m1` (linear) — emitted as a parameter + - Multiplicity is `m0` (erased) — parameter dropped, body lowered without it + - Body has no free variables beyond the lambda's own bvars (i.e. no captures) +- `expr-bvar i` → look up de Bruijn index `i` in the current lowering environment, emit the SSA local name +- `expr-app` — full case: lower function (must resolve to a known top-level definition or primitive), lower args, emit `call` +- `expr-Pi` (when it appears as the type of a top-level def) — recognized but ignored at the type level + +### Constraints + +- **Closure detector** (T2.D): a free-variable scan over each `expr-lam`'s body. If any `expr-bvar` index reaches *out* of the lambda chain to an outer lambda, raise `(unsupported-llvm-node closure-capture body)` with the offending index. This is the planned failure for Tier 3 features. +- **m0 erasure** (T2.C): for a chain of lambdas, walk left-to-right; for each `expr-lam 'm0`, drop the binder and decrement bvar indices in the body. This is the *degenerate* erasure pass — full erasure (irrelevance propagation, Pi → arrow) is a future track. +- **Function name resolution**: an `expr-app` whose function is `expr-fvar name` resolves to a top-level definition by `name`. If not found and not a primitive, raise unsupported. + +### Validation + +- `[add 5 7]` exits 12 +- Recursion that the runtime can handle without stack overflow (e.g. `fact 5` exits 120) — *if* recursion fits within Tier 2 (a recursive `defn` whose body is just arithmetic + a tail call) +- Closure attempt: a `defn` whose body references a top-level `def` is allowed (resolved as `call`); a nested `fn` that captures must error cleanly. + +### Commit message + +`SH Track 1 Tier 2: top-level functions, m0 erasure, closure-rejecting` + +## 12. Open questions + +Resolved at the relevant tier's mini-design (per Per-Phase Protocol): + +- **OQ-T0-1**: How is the elaborated top-level form actually exposed by `process-file`? It currently runs but does not return the form list. *Resolution path*: add a `--emit-elaborated` mode or a new `process-file/elaborated` entry. Decide at T0.A. +- **OQ-T1-1**: Eta-expanded vs inlined primitives (see § 10). *Resolution*: investigate at T1.A by printing what `[int+ 1 2]` elaborates to. +- **OQ-T2-1**: Are de Bruijn indices preserved post-zonk for top-level `defn` bodies? *Resolution*: investigate at T2.A. +- **OQ-T2-2**: Does `defn add [x y]` produce one `expr-lam` per parameter (curried) or one with two? Affects bvar arithmetic. *Resolution*: T2.A. +- **OQ-CI-1**: Does the GHA Ubuntu runner ship a clang version compatible with our IR? Local clang is 18.1.3. *Resolution*: pin clang version in CI if the default drifts. + +## 13. Acceptance file + +Per `ACCEPTANCE_FILE_METHODOLOGY.org`, an acceptance file lives at `racket/prologos/examples/2026-04-30-llvm-tier0-2.prologos`. Sections marked Tier 0 / Tier 1 / Tier 2; commented-out target expressions get uncommented as each tier closes. The file is run via `process-file` before *and* after each tier to confirm no regressions in the elaborator. + +--- + +## Notes for the implementer + +- Use `tools/check-parens.sh` after every `.rkt` edit. Skip nothing. +- Use `tools/run-affected-tests.rkt --tests tests/test-llvm-lower.rkt` for targeted runs (per `testing.md` § Targeted tests). +- Conversational checkpoint after each Tier commit (per `workflow.md` § Conversational implementation cadence). +- All-tests-green before tier-N+1 begins. +- Each tier's commit includes the tracker update in the same commit. + diff --git a/docs/tracking/2026-04-30_SH_MASTER.md b/docs/tracking/2026-04-30_SH_MASTER.md index dd42e3a37..a36162bd0 100644 --- a/docs/tracking/2026-04-30_SH_MASTER.md +++ b/docs/tracking/2026-04-30_SH_MASTER.md @@ -26,6 +26,7 @@ | Track | Description | Status | Design | PIR | Notes | |-------|------------|--------|--------|-----|-------| | 0 | Stage 0/1 research synthesis — series founding artifacts | 🔄 | — | — | This master + path note + super-optimization research note. 2026-04-30 batch. | +| **Hybrid Runtime (alternate path)** | **Racket-Zig hybrid kernel — second Zig kernel implementation alongside the LLVM-target original; PReduce-lite hosted on it; profile-driven migration loop demonstrated** | **✅ 2026-05-04** | [Stage 1 Research](../research/2026-05-03_HYBRID_RACKET_ZIG_RUNTIME.md) + [Stage 3 Design](2026-05-03_HYBRID_RUNTIME_DESIGN.md) | [Hybrid Runtime PIR](2026-05-04_HYBRID_RUNTIME_PIR.md) | **9 commits, ~8h, +6 tests (4 C smoke + 2 Racket hybrid), three-way differential 13/13 green, Phase 10 first migration delivered 96% callback reduction. Bring-up vehicle for SH while LLVM lowering tracks (1-4) gestate. Complementary to Track 4, not competing.** | | 1 | `.pnet` network-as-value — extend serialization to round-trip propagator structure | ⬜ | — | — | Today `.pnet` serializes elaboration state and rebuilds networks fresh from sentinels. Stage A.5 needs networks themselves to round-trip as values. Foundational for the deployment-artifact format. | | 2 | Low-PNet IR design — lowering layer between propagator network and LLVM IR | ⬜ | — | — | Cells as typed memory regions; propagators as functions over those regions; scheduler as worklist data structure; lattice merges inlined or dispatched. Analog: GHC's STG/Cmm, MLIR's dialect tower. | | 3 | LLVM substrate PoC — minimal native loader for a tight Prologos slice | ⬜ | — | — | Smallest end-to-end validation of the substrate-on-LLVM path. Pick simply-typed lambda calculus slice; have Racket compiler produce `.pnet`; load and execute via LLVM-compiled substrate. ~1-2 weeks; deliberately scoped. | diff --git a/docs/tracking/2026-05-01_BSP_NATIVE_SCHEDULER.md b/docs/tracking/2026-05-01_BSP_NATIVE_SCHEDULER.md new file mode 100644 index 000000000..8ab8e86ba --- /dev/null +++ b/docs/tracking/2026-05-01_BSP_NATIVE_SCHEDULER.md @@ -0,0 +1,208 @@ +# SH/BSP-Native — BSP Scheduler in the Native Runtime + +**Status**: Sprint B+C landed (2026-05-01). Sprint D (multi-thread parallelism) deferred. +**Track**: SH-Series, sub-piece of Track 6 ("Concurrency: thread pool for BSP scheduler"). +**Predecessor**: BSP-LE Track 2B (Racket-side; commit c5e0fe2). + +## Summary + +The Zig kernel (`runtime/prologos-runtime.zig`) now runs propagators under +proper bulk-synchronous parallel (BSP) discipline: snapshot → fire all +worklist members against the snapshot → merge writes → enqueue subscribers +of changed cells → repeat. Termination is guaranteed for monotone networks +and bounded for non-monotone ones via a fuel parameter. + +A first-class instrumentation surface is exposed: per-round, per-fire, +per-tag, per-cell-write counters readable from C/LLVM via +`prologos_get_stat(key)` and printable as JSON via +`prologos_print_stats()`. + +## Why BSP, why now + +Prior to this change the kernel used a Jacobi-ish single-pass worklist: +`run_to_quiescence` iterated `worklist[0..len]` once and stopped. Reads +hit live `cells[]`; writes both committed AND scheduled subscribers +*during* the same fire. This is correct for **acyclic** networks with +exactly-once propagator firings (all SH programs through Sprint A). It is +**not** correct for cyclic networks — a self-loop would either explode +(every fire enqueues itself) or settle non-deterministically depending on +worklist ordering. + +Sprint A introduced `select` and comparison primitives, which is the +prerequisite for conditional dataflow. The next step toward +iterative-without-unrolling (Sprint D) is feedback: a cell whose +next-round value is a function of its current-round value. BSP is the +discipline that makes feedback well-defined. + +## BSP cycle structure + +Each round: + +1. **Worklist drain.** All pids enqueued during install or the prior + round's merge phase are moved into `worklist[]`. `next_worklist[]` + is cleared. +2. **Snapshot.** `cells[]` is copied verbatim into `snapshot[]`. + All reads during this round will go through `snapshot`. +3. **Fire.** For each pid in `worklist`, `fire_against_snapshot(pid)`: + - reads operands from `snapshot[]` + - computes the fire-fn's result + - appends `(out_cid, value)` to `pending_writes` + - bumps `stat_fires_total` and `stat_fires_by_tag[tag]` + - clears `in_worklist[pid]` so the same pid can be re-scheduled if + a downstream change demands it +4. **Barrier.** `merge_pending_writes()` walks `pending_writes` and calls + `prologos_cell_write(cid, value)`. That function commits the change + to `cells[]` (if different from the current value) and enqueues + `cell_subs[cid][*]` into `next_worklist`. +5. **Swap.** `worklist ← next_worklist`; if empty, terminate. + +This is the same shape as Racket's `run-to-quiescence-bsp` in +propagator.rkt (lines 2330–2450), specialized for our flat-i64-cells + +fixed-shape-propagator world. + +## CALM safety + +Read-from-snapshot decouples reads from writes. All propagators in a +round see the same state. Their writes are commutatively merged at the +barrier (in our current case, last-write-wins per cell, which is fine +because all our fire-fns are deterministic functions of their inputs: +two propagators cannot legally write different values to the same cell +in the same round — that would be a contradiction). + +This is the standard CALM-monotone story. Because cells are i64 and +merges are last-write-wins, the kernel **doesn't need a per-domain merge +function** today; one can be added later as a per-domain function pointer +in the propagator-decl table. + +## Fuel and termination + +`prologos_set_max_rounds(n)` bounds the BSP loop to `n` rounds. Default +is `DEFAULT_MAX_ROUNDS=100000`. When exhausted, the loop exits cleanly +(no abort), `stat_fuel_exhausted=1`, and the caller can still +`prologos_cell_read` whatever value has been computed. `n=0` means +unlimited. + +Fuel is the kernel's escape valve for non-monotone cycles (e.g. +`x = x+1` would never terminate naturally). It also bounds runaway in +the presence of bugs. + +## Instrumentation interface + +Six exports: + +```c +extern void prologos_set_max_rounds(uint64_t n); +extern uint64_t prologos_get_stat(uint32_t key); +extern void prologos_reset_stats(void); +extern void prologos_print_stats(void); +``` + +Stat keys (currently exposed): + +| key | meaning | +|----|----| +| 0 | `rounds` — completed BSP rounds | +| 1 | `fires_total` — propagator fires across all rounds | +| 2 | `writes_committed` — `cell_write` calls that changed cells[] | +| 3 | `writes_dropped` — `cell_write` calls that hit equal value | +| 4 | `max_worklist` — high-water mark of pending pids | +| 5 | `fuel_exhausted` — 0/1 | +| 6 | `num_cells` — allocated cells | +| 7 | `num_props` — installed propagators | +| 100..115 | `fires_by_tag[key-100]` — per-fire-fn-tag fire counts | + +`prologos_print_stats()` emits a one-line JSON object to stderr without +linking printf (writes via `extern fn write(int, *u8, usize)`): + +``` +PNET-STATS: {"rounds":2,"fires":3,"committed":5,"dropped":3,"max_worklist":2,"fuel_out":0,"cells":5,"props":2,"by_tag":[1,0,2,0,0,0,0,0,0,0,0,0,0,0,0,0]} +``` + +Future microbench harnesses (Sprint C "flamegraph-like data") can call +this between programs to attribute time / fire counts to specific +propagator tags. + +## Lightweight thread / concurrency evaluation + +The user's question: "this is where we need optimal concurrency machine +switching - lightweight threads (whats available in llvm/zig?)". + +| Option | Stack | Switch cost | Status (2026-05-01) | Verdict for BSP | +|---|---|---|---|---| +| Zig `std.Thread` (pthreads on Linux) | ~80KB default | ~5μs | Mature in 0.13.0 | **Default for Sprint D worker pool** | +| Zig stackless `async` | frame size | ~50ns | **Broken in 0.13.0**; LLVM regression; slated for return | Not viable today | +| LLVM `@llvm.coro.*` intrinsics | stackless | ~100ns | Works but requires non-trivial state-machine lowering | Too much complexity for the tiny per-fire work | +| `ucontext` / libco / Boost.Context | configurable (8KB+) | ~200ns | Mature | Helps when tasks **block**; propagators don't block | + +**Conclusion**: lightweight threads (fibers/coroutines/async) **are not +on the critical path** for our BSP scheduler. Their performance win is +on *blocking concurrency* (many tasks awaiting I/O). Propagator fires +are non-blocking, fixed-cost computations (10–100 ns each on i64 +arithmetic). The bottleneck is the BSP barrier itself; reducing +context-switch latency below the barrier latency yields zero throughput. + +For Sprint D (multi-thread BSP), the right design is a **worker pool of +OS threads via `std.Thread`** with: + +- a sharded worklist (each thread pulls from its own deque or atomic + index), with optional Chase-Lev work-stealing +- per-thread write log (each thread accumulates its `pending_writes` + locally), merged sequentially at the barrier +- per-thread cell-id namespace for any cells allocated mid-round + (analogous to BSP-LE Track 2B Phase 2b) + +Crossover threshold to expect: per BSP-LE 2B benchmark data, Racket +crosses over at N≈128 propagators per round. The native kernel will +cross over much lower because per-fire work is similar (~50 ns) but +thread-fork overhead is similar too — meaningful parallelism likely +starts at N=32–64 propagators per round. + +**For now** (Sprint B), the kernel is single-threaded. Existing programs +have ≤ 5 propagators per round; no worker pool would help. + +## Validation + +| Test | Outcome | +|---|---| +| All 13 `n1-arith/*.prologos` examples (existing acyclic + Sprint A new) | All pass with identical exit codes | +| New C smoke test (`runtime/test-bsp-stats.c`) | Validates depth-2 chain (2 rounds, 3 fires), select propagator dispatch, reset_stats, fuel-exhaust semantics | +| 18 `test-ast-to-low-pnet.rkt` cases + 22 `test-low-pnet-ir.rkt` + 12 `test-low-pnet-to-llvm.rkt` + 10 `test-network-to-low-pnet.rkt` | All pass | + +CI step `BSP scheduler + instrumentation smoke test` added to +`.github/workflows/network-lower.yml`. + +## Mantra audit + +- **All-at-once**: each round fires all enqueued propagators against + the same snapshot — no sequential dependence between fires within a + round. ✓ +- **All in parallel**: the round structure is parallelism-ready (Sprint + D will dispatch fires across worker threads). The current single-thread + loop is a degenerate-N=1 case of the parallel design. ✓ (architecturally) +- **Structurally emergent**: the round count is determined by network + depth, not by any imperative ordering. select propagators "wait" for + their cond cell to settle by virtue of the barrier, not by an explicit + `if-cond-ready` check. ✓ +- **Information flow**: every value transit is `cell_read → fire_fn → + pending_write → cell_write → enqueue_subscribers`. No threading of + values through return-types or parameters. ✓ +- **ON-NETWORK**: the snapshot, worklist, pending_writes, and stats are + all kernel-resident state addressed via i64 cell-ids and u32 prop-ids. + Stats are exposed but not first-class cells *yet* — they're + observation, not compilation input. (Future: stats could become + cells in a meta-stratum.) Mostly ✓. + +## Open follow-ups + +- **Sprint D**: multi-thread worker pool (Zig `std.Thread` × N cores + + per-thread write log + sequential merge). +- **Per-domain merge functions**: today every cell uses last-write-wins. + Lattice cells (e.g. monotone-set, interval) would need a per-domain + function pointer. +- **Topology stratum in the kernel**: the Racket scheduler has a + topology stratum for mid-quiescence cell/prop allocation. The kernel + doesn't yet — `cell_alloc` and `propagator_install_*` only run before + `run_to_quiescence`. Mid-quiescence allocation is a Track 6 concern. +- **Stats as cells**: the longest-running propagator, the deepest cell, + the per-tag fire histogram — all could be on-network meta-cells with + monotone-merge semantics. Defer until we have a use case. diff --git a/docs/tracking/2026-05-01_LLVM_LOWERING_TIER_3.md b/docs/tracking/2026-05-01_LLVM_LOWERING_TIER_3.md new file mode 100644 index 000000000..bf4a376ec --- /dev/null +++ b/docs/tracking/2026-05-01_LLVM_LOWERING_TIER_3.md @@ -0,0 +1,142 @@ +# LLVM Lowering — Tier 3 (SH Series Track 2) + +**Date**: 2026-05-01 +**Status**: Stage 4 implementation (T3.A investigation complete; design firm enough to proceed) +**Series**: SH (Self-Hosting) — second track, building on Track 1 (Tiers 0–2) +**Cross-references**: +- [Track 1 plan + tracker](2026-04-30_LLVM_LOWERING_TIER_0_2.md) +- Track 1 commits: `9f84490` (T0), `307e995` (T1), `ab5513a` (T2), `a6de14d` (post-validation fixes) + +## 1. Summary + +Add control flow + recursion to the lowering pass. The smallest meaningful program — `defn fact | 0 -> 1 | n -> [int* n [fact [int- n 1]]]` plus `def main : Int := [fact 5]` — compiles to native and exits with 120. + +## 2. T3.A — Elaborator output (resolved) + +The `defn | pat -> body | pat -> body` pattern compiler emits two AST families: + +- **`expr-reduce (list (expr-reduce-arm tag arity body) ...) `** for *constructor* patterns. For Bool: `'true` and `'false` arm tags, both with `arity = 0`. +- **`expr-boolrec `** for *Int-literal* patterns. The target is the synthesized `(expr-int-eq )` test. Motive is erased at runtime. + +Plus a third common shape: + +- **`(expr-app (expr-lam mult type body) arg)`** — a beta-redex used as an *implicit let-binding* by the pattern compiler when binding a parameter inside an arm. Tier 2 didn't hit this shape; Tier 3 must lower it. + +No additional eliminators (`expr-natrec`, `expr-J`, etc.) appear in the recursive Int test programs. Defer those to later tiers. + +## 3. Progress Tracker + +| Phase | Description | Status | Notes | +|---|---|---|---| +| T3.A | Investigate elaborator output for `defn` patterns | ✅ | findings in § 2 | +| T3.B | `expr-Bool`, `expr-true`, `expr-false` lowering | ✅ | C1 `3ac25dd` | +| T3.C | `expr-int-lt`/`expr-int-le`/`expr-int-eq` lowering | ✅ | C1 `3ac25dd` | +| T3.D | Multi-block SSA builder refactor | ✅ | C1 `3ac25dd` | +| T3.E | `(expr-app (expr-lam ...) arg)` as let-binding | ✅ | C1 `3ac25dd` | +| T3.F | `expr-boolrec` lowering | ✅ | C2 `4551684` | +| T3.G | `expr-reduce` on Bool | ✅ | C2 `4551684` | +| T3.H | Tier 3 acceptance programs + CI step | ✅ | C3 (this commit); 9 e2e tests, fact(5)=120, fib(10)=55 | + +## 4. Scope + +### In scope + +- `expr-Bool`, `expr-true`, `expr-false` +- `expr-int-lt`, `expr-int-le`, `expr-int-eq` +- `expr-boolrec` +- `expr-reduce` *only* when the scrutinee has type `Bool` and arm tags are `'true` / `'false` +- `(expr-app (expr-lam ...) arg)` — let-binding via env extension +- Recursive top-level functions whose recursion terminates within the OS stack +- `def main : Bool` (zext is a no-op since Bool is already i64) + +### Out of scope (explicit) + +- `expr-reduce` on non-Bool ADTs (List, Option, user data) → Tier 4 +- `expr-natrec`, `expr-J`, dependent eliminators → Tier 4+ +- Tail-call optimization. Stack overflow on deep recursion is **accepted**: `fact(20)` likely fine, `fact(10000)` will SO and that's documented behavior. Test programs use small inputs to stay within ~1000 recursion depth. +- Closures with free variables → Tier 4 +- Arbitrary `expr-lam` at non-top-level positions other than the let-binding shape +- Strings, chars, heap-allocated values + +### Failure mode (carried forward from Track 1) + +Closed pass. Any AST node not in the Tier-3-extended supported set raises `unsupported-llvm-node`. + +## 5. Mantra alignment (carried forward) + +The lowering pass remains a Racket function, not a propagator stratum. Same scaffolding statement as Track 1 § 5. Tier 3 introduces no new mantra decisions; it extends the existing function form. + +## 6. Design notes + +### 6.1 Multi-block builder + +State per `lower-function`: +- `instrs : Hash[Symbol → ListOf String]` — block name to reverse-instr-list +- `cur-block : Symbol | #f` — name of block currently emitting; #f after a `br` (next op must `start-block!`) +- `block-counter : Box Integer` — for `fresh-label!` +- `ssa-counter : Box Integer` — for `fresh!` + +API: +- `(emit! str)` — appends to `cur-block` +- `(start-block! name)` — sets `cur-block`, ensures `instrs` has the key +- `(branch label)` — emits `br label %label`, sets `cur-block` to #f +- `(branch-cond cond-i1 lt-label lf-label)` — emits `br i1 …`, sets `cur-block` to #f +- `(fresh-label! prefix)` — returns a fresh block name like `"true_3"` +- `(emit-fn-body)` — concatenates blocks in entry-first declaration order with their `name:\n` prefixes and instrs + +### 6.2 i64-uniform ABI + +Every Prologos value is `i64`. Bool: 0 = false, 1 = true. Comparisons: `icmp i64, i64 → i1`, then `zext i1 to i64`. Conditional branches: `icmp ne i64 %v, 0 → i1`, then `br i1`. Redundant in some cases; LLVM's `instcombine` eliminates the round trips. + +### 6.3 `expr-boolrec` lowering + +``` +(expr-boolrec motive true-case false-case target) + ↓ + ;; lower target → %t (i64) + %tc = icmp ne i64 %t, 0 + br i1 %tc, label %true_N, label %false_N + +true_N: + ;; lower true-case → %tv, last block = true_end + br label %join_N + +false_N: + ;; lower false-case → %fv, last block = false_end + br label %join_N + +join_N: + %r = phi i64 [%tv, %true_end], [%fv, %false_end] +``` + +Motive is ignored (erased). + +### 6.4 `expr-reduce` on Bool + +``` +(expr-reduce target (list (arm 'true 0 t-body) (arm 'false 0 f-body)) exh?) + ↓ (semantically same as boolrec) +``` + +Lowered identically to boolrec, dispatched by examining the arms list. Arm order may be `'true` first or `'false` first; we look up by tag, not by position. `arity = 0` is required (non-zero means a constructor with fields, which is Tier 4). + +### 6.5 Let-binding via `(expr-app (expr-lam mult type body) arg)` + +Recognized in `lower-int-expr`'s `expr-app` clause: if the head is an `expr-lam`, treat as let. Lower `arg` in current env → `%av`. Push `%av` onto bvar-env. Lower `body` in extended env. Pop. Return body's value. + +The lambda's `mult` is honored: `m0` arg means we lower the arg's body NOT (skip the arg evaluation), push `'erased` onto env, and continue. (Practically rare for top-level let, but needed for completeness when type-level binders are interleaved.) + +## 7. Commit cadence + +- **C1 (T3.B + T3.C + T3.D + T3.E)**: foundation. Bool + comparisons + multi-block builder + let-binding. No conditional acceptance program yet but Tier 0–2 acceptance still passes. New unit tests for each piece. +- **C2 (T3.F + T3.G)**: conditionals. `expr-boolrec` and `expr-reduce` on Bool. First Tier 3 acceptance program (`choose`). +- **C3 (T3.H)**: recursion. `fact` + `fib` acceptance programs, CI step for Tier 3, all tracker rows ✅. + +## 8. Risk register + +| Risk | Likelihood | Impact | Mitigation | +|---|---|---|---| +| Multi-block refactor regresses Tier 0–2 | Medium | High | Keep Tier 0–2 paths working through a thin entry-block-only shim; verify all existing acceptance tests after C1. | +| Phi source block tracking gets stale | Medium | High (silently wrong IR) | Track `cur-block` rigorously; assert `cur-block ≠ #f` before every emit. | +| Stack overflow on `fact` at unexpected n | Low | Low | Test programs use n ≤ 10. Document in plan doc. | +| Pattern compiler emits a fourth shape we haven't seen | Low | Medium | Closed-pass design catches this with a clear error pointing at the unsupported AST node. | diff --git a/docs/tracking/2026-05-01_SH_LOWERING_FEATURE_MAP.md b/docs/tracking/2026-05-01_SH_LOWERING_FEATURE_MAP.md new file mode 100644 index 000000000..43616ac2d --- /dev/null +++ b/docs/tracking/2026-05-01_SH_LOWERING_FEATURE_MAP.md @@ -0,0 +1,302 @@ +# SH Lowering — Feature Map and Dependency Graph + +**Created**: 2026-05-01 +**Status**: Stage 0/1 — research synthesis. Maps the feature surface for "AST → propagator network" lowering, classifies every AST node, and shows the dependency graph between SH lowering, the current Racket reducer, PReduce, and PPN Track 4C. +**Origin**: User question 2026-05-01 — "I want to understand all the features required to run an arbitrary Prologos program, and what the dependency graph is for those parts." + +## Thesis + +The user's two-part decomposition of SH work is **correct but incomplete**: + +- **Part 1**: AST → propagator network (lowering) +- **Part 2**: propagator network runtime (substrate) + +The two parts are real and load-bearing. **Part 1 is the long pole** — its surface area is ~200 expr-* AST nodes against the language; we currently lower ~12. **Part 2 is small in concept** (cells, propagators, BSP, fire-fn dispatch, GC, threads) but has substantial sub-projects (memory management, native concurrency, FFI inversion). + +But there is also a **hidden Part 0** that the SH master doc folds in but is worth surfacing: PReduce (Track 9). PReduce is *reduction* lifted on-network. It is **not** what our SH lowering is, despite the name overlap. It runs at a different stage of the pipeline. Conflating PReduce with SH lowering is the most common framing error. + +## Two-axis decomposition (per SH_MASTER §66-86) + +The SH series itself is structured around two axes: + +| Axis | Retires | Stage | What it produces | +|---|---|---|---| +| **Axis 1** | Racket as **runtime** dependency | A → A.5 | Native binaries; deployed Prologos programs run without Racket. Compiler still in Racket. | +| **Axis 2** | Racket as **compile-time** dependency | A.5 → B → C | Compiler-in-Prologos; bootstrap verification. | + +Our work this session — Sprints A–E.3 — is entirely **Axis 1**. The user's "Part 1 + Part 2" maps onto SH Tracks 2 + 4 (lowering + production substrate). PPN Track 4C and Track 9 are independent series that **feed into** Axis 1 but are not **OF** it. + +## Architectural pipeline (current → target) + +``` +Source (.prologos) + │ + ▼ +WS-mode reader ──► tree-parser ──► sexp form + │ + ▼ + parser ──► surface AST (surf-*) + │ + ▼ + elaborator ──► typed AST (expr-*) + │ + ┌───────────┼───────────┐ + ▼ ▼ ▼ + typing-core REDUCTION ZONK + (200 nodes) (50 cases) (~30 sites) + │ │ │ + └───────────┴───────────┘ + │ + ▼ + FULLY-ELABORATED AST ◄── starting point for lowering + │ + ▼ + ast-to-low-pnet ◄── SH Track 2 (this work; ~12/200 nodes) + │ + ▼ + Low-PNet IR + │ + ▼ + low-pnet-to-llvm ◄── SH Track 2.C + │ + ▼ + LLVM IR + │ + ▼ + clang link + │ + ▼ + runtime/prologos-runtime.{zig,o} ◄── SH Track 4 (Sprint B+C+E.1+E.2) + │ + ▼ + native binary (x86_64 ELF) +``` + +## Feature map: the 327 expr-* nodes vs what we handle + +`syntax.rkt` defines 327 `expr-*` structs. The reducer handles ~200 (some are types, not values). The SH lowering handles ~12. Here's the breakdown by family: + +### ✅ Lowered today (Sprint A–E.3) + +| Family | AST nodes | What | +|---|---|---| +| Int | `expr-int` | i64 cell with literal init | +| Bool | `expr-true`, `expr-false` | i64 0/1 cell | +| Int arith | `expr-int-add`, `-sub`, `-mul`, `-div` | (2,1) propagator with kernel-int-* tag | +| Int cmp | `expr-int-eq`, `-lt`, `-le` | (2,1) propagator → Bool cell | +| Conditional | `expr-boolrec`, `expr-reduce` (2-arm Bool) | (3,1) `kernel-select` propagator | +| Annotation | `expr-ann` | strip wrapper | +| Bound vars | `expr-bvar` | env lookup | +| Let-binding | `expr-app` of `expr-lam` | translate arg → cell, push to env | +| Tail-rec defn | recognized via pattern match in `match-tail-rec` | feedback network with select gate | + +### 🔵 Required for arbitrary Prologos but **not yet lowered** + +Listed in rough dependency / effort order: + +| Effort | Family | AST nodes | What's needed | +|---|---|---|---| +| ~0.5d | **Free vars / named call** | `expr-fvar` saturated app | Compile-time inlining via beta-reduction. Substitution already exists in `substitution.rkt`. Closes the gap from Sprint E.3 (today only tail-rec defns work; non-recursive helpers fail). | +| ~0.5d | **Negation / abs** | `expr-int-neg`, `expr-int-abs` | (1,1) propagators already exist in kernel; just need translator cases. | +| ~0.5d | **Mod / int-mod** | `expr-int-mod` | New (2,1) tag in kernel; trivial. | +| ~1d | **Nat type** | `expr-zero`, `expr-suc`, `expr-nat-val`, `expr-Nat` | Same i64 cell as Int with unsigned semantics. `expr-natrec` is the recursion eliminator — handle as compile-time unroll OR as iterate-while when target is variable. | +| ~2-3d | **Pairs / Sigma** | `expr-pair`, `expr-fst`, `expr-snd`, `expr-Sigma` | Build returns *list* of cell-ids per pair-typed expr. Generalizes `build` from `Cid` to `(Listof Cid)`. Unblocks structured iteration state. | +| ~2-3d | **General match** | `expr-reduce` with N arms of any binding-count | Multi-way select; per-constructor dispatch. Requires constructor-tag dispatch in the kernel. | +| ~1d | **Unit / Nil** | `expr-unit`, `expr-Unit`, `expr-nil`, `expr-Nil` | Trivial — cell with init=0 (or omit when erased). | +| ~3-5d | **Vectors / lists** | `expr-vnil`, `expr-vcons`, `expr-vhead`, `expr-vtail`, `expr-vindex`, `expr-Vec` | Heap-allocated runtime structure. Needs runtime alloc + GC interaction. | +| ~3-5d | **Posit family** (8/16/32/64) | `expr-posit*`, `expr-p*-add` etc. | Each shape needs full kernel arithmetic primitives. Substantial but parallel to Int. | +| ~3-5d | **Rational** | `expr-rat-*`, `expr-from-int` | Pair of i64 (num/denom). Builds on Sigma. | +| ~5d | **Strings / chars** | `expr-string-*` | Variable-length runtime data. Requires runtime alloc + UTF-8 handling. | +| ~5-10d | **Maps / Sets / PVecs** | `expr-map-*`, `expr-set-*`, `expr-pvec-*` | Persistent data structures (CHAMP/HAMT). The Zig HAMT (Track 6 stub) is the substrate; lowering needs to wire to it. | +| ~5d | **Generic arithmetic via traits** | `expr-generic-add`, `-sub`, `-mul`, etc. | Needs trait-resolution in the lowering OR a compile-time pass that resolves generic ops to monomorphic ones. Most natural: rely on elaborator's `resolve-trait-constraints!` to monomorphize before lowering. | +| ~10d | **First-class functions / closures** | `expr-lam` not at let-binding position | Heap closure cells. Needs runtime alloc + `apply` propagator that reads function cell + arg cells. Major lift — interacts with GC and possibly with runtime function-call infrastructure. | +| HARD | **Non-tail recursion** | recursive `expr-app` not in tail position | Conceptually requires runtime call stacks, fundamentally at odds with BSP-parallel model. Either (a) build classical fib via memoization (allocate one cell per `fib(k)` for k=0..n at compile time — same as our current unrolled form) or (b) introduce activation records. (a) only works for known-N. | +| ~5d | **Foreign calls** | `expr-foreign-fn` | (k,1) propagator that calls a host function. For native runtime: dlsym + symbol table. | +| HARD | **Effect / capability machinery** | `expr-effect-*`, `expr-cap-*` | Capabilities are typing-only at first; runtime depends on which effects are kept reified vs erased. Needs Track 5 (erasure boundary) decisions. | +| HARD | **Logic / solve / defr** | `expr-solve`, `expr-defr-*`, `expr-clause`, etc. | Logic-programming runtime with backtracking. Today implemented in metavar-store + relations on the elaborator network. Native version needs ATMS + scheduler ports. | +| HARD | **Session types** | `expr-session-*` | Channel runtime + protocol verification. Most of this is type-level (m0-erased). Runtime-relevant pieces: channel state, send/receive operations. | +| ~3d | **Holes / metas** | `expr-hole`, `expr-typed-hole`, `expr-meta` | At runtime: should not exist (must be solved during elaboration). Lowering should reject. Sprint E.3 already does this for `expr-fvar` unknowns. | +| HARD | **Union types / unification on values** | `expr-union`, `expr-unify-goal` | Logic-programming territory. Defer with logic. | + +### ⚪ Type-level only (no runtime presence) + +| Family | AST nodes | Note | +|---|---|---| +| Type formers | `expr-Type`, `expr-Pi`, `expr-Sigma`, `expr-Eq`, `expr-Vec`, etc. | Erased before lowering. If they appear, that's a bug. | +| Equality | `expr-refl`, `expr-J` | Erased (proofs). | +| Singletons | `expr-fzero`, `expr-fsuc`, `expr-Fin` | Erased or replaced with i64 indices. | + +## The current reducer is feature-complete; SH lowering is not + +The Racket reducer (`reduction.rkt:1340-3209`) handles **all 200 reducible AST nodes** across ~50 reduction cases. It implements: +- β-reduction (lambda app) +- ι-reduction (eliminators: natrec, boolrec, J) +- Projections (fst/snd, vhead/vtail) +- Trait dispatch (idx-nth on resolved dicts) +- Foreign function calls (with marshalling) +- Three memoization caches with cache-staleness handling +- Integer, posit, rational arithmetic + +It is **complete for arbitrary Prologos**. + +Our SH lowering handles ~12/327 nodes. Adding a node typically takes 0.5–3 days of focused work (the 8-file pipeline checklist plus the lowering case). Total estimated effort to reach feature parity with the reducer: **3–6 months** of continuous work, with the harder items (closures, effects, logic) representing genuine architectural research. + +This is **expected and not alarming**. The reducer evaluates symbolically; lowering produces an executable network. They have different shapes and different constraints. Equivalent feature parity is a long arc. The MVP path (Sprints A-E + the small follow-ups) is the **80% of the language that 80% of programs use**. + +## How SH lowering relates to PReduce, PPN 4C, and others + +### PReduce (PPN/PRN cross-series, Track 9) + +**Goal**: Make REDUCTION incremental and on-network. Each reduction result becomes a cell; a propagator recomputes when the input expression's dependency cells change. Replaces today's per-phase memo cache (which has staleness issues — see `2026-03-21_TRACK9_REDUCTION_AS_PROPAGATORS.md`). + +**Relationship to SH lowering**: +- **Different stage of pipeline**. PReduce operates on AST during the elaborator's reduce phase. SH lowering operates AFTER elaboration is complete. +- **Different output**. PReduce produces *another AST* (the reduced form). SH lowering produces a *low-pnet structure* (cells + propagators + LLVM IR). +- **Different consumer**. PReduce's output feeds back into typing-core, zonk, elaborator. SH lowering's output feeds clang. +- **Pipeline order**: PReduce runs DURING elaboration (potentially many times); SH lowering runs ONCE on the post-elaboration result. + +**Could SH lowering reuse PReduce ideas?** Partially. The cell-as-cache-of-result idea applies if we ever need *runtime* incremental recomputation (e.g. interactive REPL with dependency-tracked recomputation). Not needed for AOT compilation. + +### PPN Track 4C (compiler IS the network) + +**Goal**: Lift type checking + elaboration onto the propagator network. 5 facet lattices (`:type`, `:context`, `:usage`, `:constraints`, `:warnings`) per AST node. Inference rules become propagators. Today's CHAMP storage and zonk tree-walks dissolve into on-network equivalents. + +**Relationship to SH lowering**: +- **Different problem**. PPN 4C makes the COMPILER a network. SH lowering makes the COMPILED PROGRAM a network. +- **Sequential dependency** for self-hosting (axis 2). PPN 4C must complete before Track 9 (compiler-in-Prologos) makes sense. +- **No direct dependency** for axis 1 (which is what we're working on). The Racket-hosted compiler can produce post-elaboration ASTs whether elaboration is on-network or imperative. + +**Could SH lowering reuse PPN 4C ideas?** Yes, indirectly: +- The 5-facet attribute model could inform what *survives* elaboration into the lowering input. +- PPN 4C's stratification + dispatch infrastructure parallels what runtime BSP needs. +- But there's no shared code path today. + +### NTT (Network Type Theory / propagator-as-syntax) + +**Goal**: First-class `propagator` declarations in source syntax (NOT just for AST evaluation). Users write propagator topology directly. + +**Relationship to SH lowering**: +- **Adjacent**. NTT and SH lowering both produce networks, but from different sources (NTT from user-written `propagator` forms, SH lowering from elaborated AST). +- **Could share back-end**. Once Low-PNet IR is the common target, NTT's compiled form and SH lowering's compiled form are the same shape. +- **NTT may eventually replace some SH lowering work**. If a user writes their iterative-fib as a NTT propagator declaration directly, the recognizer in `match-tail-rec` becomes redundant for that program. + +### SRE (Structural Reasoning Engine) + +**Goal**: Lattice operations, form registry, structural unification. + +**Relationship to SH lowering**: SRE is a *runtime* concern (Part 2), not a lowering concern (Part 1). Once compiled programs use SRE primitives, the runtime substrate (Track 4) must include SRE. + +### BSP-LE Track 2B (BSP scheduler) + +**Goal**: Bulk-synchronous parallel scheduler for the propagator network. + +**Relationship to SH lowering**: BSP-LE is the spec our **runtime** (Sprint B) implements. We've already done the native port. BSP-LE the design + the Sprint B implementation = our Part 2's scheduler. + +## Dependency graph (compact) + +``` + ┌─────────────────────────┐ + │ Source .prologos │ + └────────────┬────────────┘ + │ + ▼ + ┌─────────────────────────────────────────────────┐ + │ Racket-hosted compiler (parser, elaborator, │ + │ typing-core, reducer, zonk) │ + │ │ + │ ◄── PPN 4C optional (typing-on-network) │ + │ ◄── PReduce optional (reduction-on-network) │ + └────────────┬────────────────────────────────────┘ + │ post-elaboration AST + ▼ + ┌─────────────────────────────────────────────────┐ + │ PART 1: AST → low-pnet │ + │ (this work — SH Track 2) │ + │ │ + │ Lowering surface: 12/200 today; │ + │ target: 80% of language for typical programs. │ + │ │ + │ Per-AST-node work: 0.5–3 days each. │ + │ ◄── Shares: type erasure boundary (Track 5) │ + │ ◄── Adjacent: NTT (user-written propagators) │ + └────────────┬────────────────────────────────────┘ + │ low-pnet IR + ▼ + ┌─────────────────────────────────────────────────┐ + │ low-pnet → LLVM IR (Track 2.C) │ + │ │ + │ Tag-based fire-fn dispatch. │ + │ ◄── Tags must match runtime's switch. │ + └────────────┬────────────────────────────────────┘ + │ LLVM IR + ▼ + ┌─────────────────────────────────────────────────┐ + │ PART 2: native runtime (Track 4) │ + │ │ + │ Subparts: │ + │ - Cells + propagator install (Sprint A) ✅ │ + │ - BSP scheduler (Sprint B) ✅ │ + │ - Instrumentation (Sprint C) ✅ │ + │ - Feedback / cyclic (Sprint E.1) ✅ │ + │ - GC ❌ (Track 6) │ + │ - Concurrency / threads ❌ (Track 6) │ + │ - I/O via FFI inversion ❌ (Track 7) │ + │ - HAMT/CHAMP runtime ⚠️ (Track 6) │ + │ - SRE form registry ❌ (later) │ + │ - ATMS speculation ❌ (later) │ + │ - Logic engine ❌ (Sprint F+) │ + │ │ + │ The "atomic substrate" is small. │ + │ Each persistent data structure or runtime │ + │ service is its own sub-project. │ + └─────────────────────────────────────────────────┘ +``` + +## Where most of the work is + +**By node count**: Part 1 (lowering) is the long pole. 200 expr-* nodes to handle vs maybe 10 runtime sub-systems. + +**By difficulty**: Mixed. +- *Easy lowering, easy runtime*: Int arithmetic, comparisons, conditionals. (Sprints A-E.3) +- *Easy lowering, complex runtime*: HAMT/CHAMP, GC. The structures are small; GC integration is large. +- *Complex lowering, easy runtime*: traits/dispatch (compile-time monomorphization), pair lowering. The runtime barely changes; the lowering needs Sigma-typed cells. +- *Complex lowering AND complex runtime*: closures, effects, logic. These need both new lowering AND new runtime services. + +**By calendar time**: roughly 60-70% of remaining work in Part 1 (lowering surface), 30-40% in Part 2 (runtime sub-systems). Part 2 has fewer items but each item is bigger. + +## Recommended next moves (ordered by ROI) + +1. **Sprint F.1 — non-recursive function inlining** (~0.5d). Closes the immediate `function call not supported` error for helper functions. High user-visible impact, trivial implementation. +2. **Sprint F.2 — Pair / Sigma lowering** (~2-3d). Generalizes `build` to return cell-id lists. Unblocks structured state, multi-return values, the foundation for `iterate-while` with compound state. +3. **Sprint F.3 — Nat + natrec + iterate-while** (~2d, depends on F.2). Handles Peano-style iteration cleanly. Combine with the existing tail-rec lowering for two paths into the same feedback network. +4. **Sprint F.4 — General match (multi-arm with binders)** (~2-3d). Enables pattern matching on sum types (Maybe, Either, etc). +5. **Sprint G — runtime services bootstrap**. Starts on Track 6 (GC + thread pool). Needed before any heap-allocated data (lists, maps, closures) can land in lowering. + +After F.1–F.4, lowering covers ~30 of 200 AST nodes — roughly the "first-order functional core" of Prologos. After G, the runtime is ready for heap structures. Together they cover an estimated **70%+ of typical user programs**. + +## What this design doc settles vs leaves open + +**Settles**: +- Two-part decomposition is correct for axis 1. +- Most calendar work in Part 1; Part 2 has fewer items but each one larger. +- PReduce, PPN 4C, NTT are NOT what SH lowering is. They are adjacent or upstream pieces. +- Feature parity with the reducer is a 3–6 month arc. + +**Leaves open**: +- How to handle non-tail recursion. Current options (memoization at compile time = unrolled; activation records = breaks BSP) both have drawbacks. Possibly never needs solving if user code uses tail-rec or iterate-while. +- Closure runtime. Open until we have a heap + GC. +- Logic/solve runtime. Major sub-project; defer to Sprint H+ once the functional core lands. +- When SH lowering should optionally use PReduce as a sub-pass (e.g. constant fold step expressions before lowering). Not needed yet; revisit when we have benchmarks where compile-time precomputation matters. + +## References + +- `racket/prologos/reduction.rkt:1340-3209` — current reducer feature surface +- `racket/prologos/typing-core.rkt:397-1450` — type checker surface +- `racket/prologos/syntax.rkt` — 327 expr-* node definitions +- `racket/prologos/ast-to-low-pnet.rkt:130-535` — current SH lowering (12 of 200 nodes) +- `docs/tracking/2026-04-30_SH_MASTER.md` — overall SH series + two-axis retirement +- `docs/tracking/2026-03-21_TRACK9_REDUCTION_AS_PROPAGATORS.md` — PReduce design (referenced; verify path) +- `docs/tracking/2026-04-17_PPN_TRACK4C_DESIGN.md` — typing-on-network (axis 2 prerequisite) +- `docs/tracking/2026-05-01_BSP_NATIVE_SCHEDULER.md` — Sprint B+C runtime scheduler write-up +- `runtime/prologos-runtime.zig` — Part 2 substrate (~520 lines today) +- `runtime/test-bsp-feedback.c` — kernel-level BSP feedback validation diff --git a/docs/tracking/2026-05-02_DEPTH_ALIGNMENT_RESEARCH.md b/docs/tracking/2026-05-02_DEPTH_ALIGNMENT_RESEARCH.md new file mode 100644 index 000000000..e0b2c46f1 --- /dev/null +++ b/docs/tracking/2026-05-02_DEPTH_ALIGNMENT_RESEARCH.md @@ -0,0 +1,529 @@ +# Depth Alignment in BSP Propagator Networks — Research + +**Created**: 2026-05-02 +**Status**: Stage 0/1 — research synthesis. Documents the trade-off space discovered while iterating on Sprint F.5 (lag-matching bridges) and explores in detail one rejected option (scheduler-level depth tracking) so future work can reference it without re-deriving. +**Origin**: User pushback on Sprint F.5's network-level fix — "shouldn't this be solved in the scheduler instead?" +**Cross-references**: [`SH_LOWERING_FEATURE_MAP.md`](2026-05-01_SH_LOWERING_FEATURE_MAP.md), [`BSP_NATIVE_SCHEDULER.md`](2026-05-01_BSP_NATIVE_SCHEDULER.md), [`.claude/rules/propagator-design.md`](../../.claude/rules/propagator-design.md), [`.claude/rules/structural-thinking.md`](../../.claude/rules/structural-thinking.md). + +## Problem statement + +In the Zig-runtime BSP propagator network, when a tail-recursive computation has nested arithmetic (e.g., Pell's `int-add(int-mul(2, b), a)`), the inputs to the outer `int-add` arrive at different BSP rounds. `int-mul(2, b)` takes one extra round to commit its result vs `a` which is read directly from state. The outer `int-add` reads inputs from the snapshot in its firing round; if the snapshot has stale values for some inputs and fresh values for others, the result mixes iterations of the recurrence and produces wrong values that propagate through feedback into the state cells. + +**Sprint F.5** fixed this by inserting identity-propagator "bridges" — Z⁻¹ delay elements — on shorter paths so all inputs to a multi-input propagator have equal depth (max-input-depths + 1). All paths through the network are then balanced; reads at each BSP round are coherent. + +The architectural question that prompted this research: is putting *delay elements in the network* the right design, or should the *scheduler* handle synchronization automatically? + +## Theoretical framework + +### Synchronous dataflow languages (Lustre, Esterel, Faust, SCADE) + +The canonical primitive is the **unit-delay operator**: Lustre's `pre`/`->`, Faust's `mem`, Esterel's `pause`. Compilers verify the **synchronous hypothesis** — at every logical clock tick, every signal has exactly one well-defined value — and reject programs where two paths into a combinational node have different cycle counts unless `pre` is inserted to balance them. + +So the formal answer in this lineage is: **explicit unit-delay nodes, with a typing discipline**. F.5's identity bridges are `pre` operators in disguise. + +### Kahn process networks / static dataflow + +Pure KPN doesn't have this problem because channels are unbounded FIFOs; depth differences manifest as latency, not data corruption. Static dataflow (Lee–Messerschmitt SDF) restores it: the compiler computes a balanced periodic schedule from token production/consumption rates. Path-balancing is automatic in the schedule, not in the network structure. + +### Signal flow graphs / DSP design + +Standard form is the Z-transform: `z⁻¹` denotes a unit delay. Circuits are normalized so every cycle has at least one `z⁻¹` and every fan-in node sees inputs of equal latency. Tooling (Simulink, Ptolemy) inserts delay buffers automatically. + +### BSP literature (Valiant 1990; Pregel; GraphLab; Giraph) + +BSP itself has no depth problem within a superstep — the model *is* "all messages from round k delivered before round k+1." Pregel programs use vote-to-halt + multi-superstep convergence, with no notion of intra-step combinational depth: every operation is one superstep. The implicit answer: **make every operator one superstep** — no nested combinational logic. If you have nested arithmetic, you've collapsed two BSP steps into one and the model breaks. + +### Hardware retiming (Leiserson–Saxe 1991) + +Retiming is the canonical compile-time pass: given a circuit with delays and combinational logic, move delays across gates to minimize clock period subject to functional equivalence. It's an LP / min-cost-flow problem; runs in polynomial time. The relevant sub-problem for us is **register balancing** — distribute delays so all paths into each combinational node have equal register count. + +### Software pipelining / modulo scheduling (Rau, Lam) + +Used in VLIW compilers. Builds a steady-state schedule where loop iterations overlap; resolves cross-iteration dependencies via rotating register files or explicit MOV inserts. The conceptual cousin of F.5: extra MOVs on short paths so iterations align. + +### Token-tagged dataflow (MIT Tagged-Token, Manchester Dataflow Machine, Naiad, Differential Dataflow) + +Each value carries an iteration tag (or multi-dimensional timestamp); an operator fires only when *all* inputs with matching tags have arrived. No structural alignment needed — the matching store does it dynamically at runtime cost (hash-keyed buffer per operator, frontier propagation in Naiad). + +## Survey of techniques + +| # | Technique | Description | Trade-offs | +|---|---|---|---| +| 1 | **Identity bridges (F.5)** | Insert no-op propagators on shorter paths | ✅ zero kernel change, local fix, structurally explicit. ❌ O(depth) extra cells/props per misaligned op; static depth only | +| 2 | **Retiming pass** | Compile-time min-cost-flow that places delays optimally | ✅ provably optimal in delay count; well-understood. ❌ requires building DAG and running LP — but tractable | +| 3 | **Set-latch handshake** | Each consumer waits until all producers have signaled "ready in round k" | ✅ matches `propagator-design.md`'s codified pattern. ❌ requires monotone-set cells + round-tagging — neither in i64 kernel | +| 4 | **Token-tagged dataflow** | Each value carries iteration tag; operator fires when matching tags align | ✅ most general. ❌ every cell becomes `(tag, i64)`; rearchitects kernel; per-operator matching store | +| 5 | **Speculative execution + rollback** | Fire eagerly with stale inputs; detect mismatch; rollback | ✅ keeps pipeline full. ❌ per-cell version vectors, rollback log; non-monotone, breaks CALM | +| 6 | **Manual barriers (CUDA `__syncthreads`)** | Programmer inserts sync points | ❌ BSP already has barriers per round; this is what we have, doesn't address sub-step ordering | +| 7 | **Pure FRP `Behavior`/`Signal`** | Continuous-time semantics; sample at well-defined times | ❌ implementations either compile to synchronous-dataflow (back to (1)) or pull-based lazy eval (different evaluation model entirely) | +| 8 | **Scheduler-level depth tracking** | Annotate per-cell depth/round; gate firing in scheduler | (Detailed below — rejected but documented) | +| 9 | **Software clock domains** | Insert latching cells at boundaries where rates differ | ❌ Same kernel cost as set-latch; only relevant for multi-rate, which we don't have | + +## Scheduler-level depth tracking (detailed exploration) + +The user's instinct: depth is a temporal/synchronization concern, which feels like a scheduler responsibility. This section explores what implementing it in our Zig kernel would actually require. + +### Design sketch + +Each cell gains metadata: `last_changed_round`, the BSP round when its value last actually committed (changed). When a propagator fires, the scheduler checks: are all my inputs at "matching" round numbers? If yes, fire. If no, defer to a later round. + +Concrete kernel additions: + +```zig +// New per-cell metadata (16 KB at MAX_CELLS=1024 with u64 fields) +var cell_last_round: [MAX_CELLS]u64 = [_]u64{0} ** MAX_CELLS; + +// New per-propagator metadata: compile-time-computed depth +var prop_depth: [MAX_PROPS]u32 = undefined; + +// Modified install: caller (codegen) passes precomputed depth +export fn prologos_propagator_install_2_1_with_depth( + tag: u32, in0: u32, in1: u32, out0: u32, depth: u32 +) u32 { ... prop_depth[pid] = depth; ... } + +// Modified cell_write: tag the round +fn cell_write_in_round(id: u32, value: i64, round: u64) void { + if (cells[id] != value) { + cells[id] = value; + cell_last_round[id] = round; + // schedule subscribers + } +} + +// Modified fire: gate based on input round coherence +fn fire_against_snapshot(pid: u32, current_round: u64) bool { + const r0 = cell_last_round[prop_in0[pid]]; + if (prop_shape[pid] >= SHAPE_2_1 and cell_last_round[prop_in1[pid]] != r0) { + // inputs at different rounds — defer this fire + return false; + } + if (prop_shape[pid] == SHAPE_3_1 and cell_last_round[prop_in2[pid]] != r0) { + return false; + } + // ... existing fire logic + return true; +} +``` + +### What this buys + +The Low-PNet IR no longer needs identity bridges. A program with mixed-depth step expressions emits exactly the propagators needed: + +- Pell pre-F.5: 24 cells / 21 props (with bridges) +- Pell with scheduler depth tracking: ~12 cells / 10 props (no bridges) + +That's roughly 50% reduction in cell/prop count for depth-2 programs. For depth-1 programs (fib, sum, factorial), savings are smaller (~3 cells per program from removed pre-select uniform lift bridges). + +### What it costs — the actual gory details + +#### 1. The "round number" is ambiguous in cyclic networks + +BSP rounds are linear (1, 2, 3, ...). But the FEEDBACK identity propagator (next-state → state) writes to a state cell, advancing its `last_round`. This conflates "logical iteration" with "BSP round." Concretely: + +For Pell's iteration: +- Round 5: state[a] commits new value (iteration 1's result). +- Round 6: subscribers of state[a] fire (int-mul, int-add). They WROTE on round 5's snapshot (= iteration 0 values). Their outputs commit at round 6 with `last_round = 6`. +- Round 7: int-add fires reading state[a] (last_round=5) and int-mul output (last_round=6). **Round mismatch.** + +But this mismatch is *correct* — int-mul's output reflects iteration 0's state, while state[a] now holds iteration 1. They're FROM DIFFERENT ITERATIONS, just like F.5's lag-mismatch problem. + +Fix attempt: maintain a separate **"iteration"** counter per cell. The feedback identity advances `iteration` of state cells; arithmetic propagators inherit the *minimum* iteration across their inputs. Propagators fire only when all input iterations match. + +But this requires explicit feedback-edge marking (which propagators advance iteration vs which don't), and the kernel doesn't know which is which — the install API doesn't distinguish. + +#### 2. Compile-time depth annotation API + +The kernel needs each propagator to know its depth. So `propagator_install_*` gains a `depth` parameter, computed by the lowering. This means the lowering still needs the depth tracking we have today (`cell-depth` map in the builder). The only thing that changes: instead of inserting bridges, emit propagator with depth annotation. + +So the depth-tracking infrastructure on the lowering side **does NOT go away** — it migrates from "insert bridges" to "annotate propagators." + +#### 3. Pre-fire gate adds branching to fire dispatch + +Every propagator fire now does 1-2 extra cell-array reads + comparisons before the actual fire. For tight inner loops (millions of fires), this overhead is real. Estimate: per-fire overhead increases ~2-5ns (from current ~12-20ns). + +For Pell at N=92, with 50% fewer fires (no bridges), the wall time would be: +- Current: 1868 fires × 15.3 ns = 28.6 μs +- Hypothetical: 934 fires × ~18 ns (gate overhead) = 16.8 μs + +Savings: ~12 μs. Real but small at our current scale. + +#### 4. Worklist semantics get complicated + +When a fire is *deferred* (inputs not at matching rounds), what happens? + +Option A: Re-enqueue at end of round; fire again next round. Risk: infinite re-queue if rounds never align (bug somewhere). +Option B: Delete from current worklist; re-add when ANY input changes again. Risk: missed fires if inputs settle but propagator was missed. + +Both options need careful invariants to avoid deadlock or starvation. In F.5's bridge approach, the BSP scheduler is "dumb" — it just fires what's enqueued. With scheduler-level gating, the scheduler becomes responsible for FAIRNESS and PROGRESS guarantees. + +#### 5. Multi-thread BSP (Sprint D) becomes much harder + +The round counter and per-cell `last_round` are SHARED STATE across threads. Updates need synchronization. With F.5's bridge approach, threads see the same snapshot and write to disjoint `pending_writes` regions — no shared mutable state during fires. With scheduler-level depth tracking, every fire does a synchronized read of `cell_last_round`. This is a significant scaling penalty. + +#### 6. Doesn't compose with future worldview tags + +When PPN convergence brings worldview-tagged cells to the runtime, every cell becomes `(worldview_bitmask, value)`. If we ALSO add `last_round` per cell, we have THREE pieces of metadata per cell (value, worldview, round). Token-tagged dataflow (option 4) generalizes both worldview tags AND iteration tags into one `timestamp` field. Adding scheduler-level `last_round` NOW would create a parallel metadata mechanism that gets ripped out when token-tagged lands. + +#### 7. Compile-time savings disappear + +The Low-PNet IR is "smaller" (no bridges) but the LLVM IR is "larger" (extra parameter to every install_2_1 / install_3_1 call, depth computation per call site, gate check inline). For typical programs, the IR diff is roughly a wash. + +### Estimated cost + +| Component | Effort | +|---|---| +| Kernel: per-cell + per-prop metadata fields | ~0.5 day | +| Kernel: modified install + cell_write + fire dispatch | ~1 day | +| Kernel: worklist re-enqueue / fairness guarantees | ~1-2 days | +| Lowering: emit depth annotations instead of bridges | ~1 day | +| Tests: cyclic network correctness, deferred fire, no-deadlock | ~1-2 days | +| Multi-thread compatibility audit (when Sprint D lands) | ~unknown | +| **Total** | **~5-7 days minimum** | + +### Verdict on scheduler-level depth tracking + +**Rejected.** Concrete reasons: + +1. **Off-network metadata violates the design mantra**. Per `.claude/rules/on-network.md`: "everything on the propagator network. No exceptions. Off-network state is debt against self-hosting." Per-cell round counters in scheduler memory are exactly off-network state. + +2. **Cyclic-network ambiguity is a real correctness hazard**. The "round" concept doesn't naturally extend to feedback loops. To fix it, we'd need to model "iteration" separately from "round," which is a big jump toward token-tagged dataflow without committing to the full architecture. + +3. **Worst-case savings are modest**. For typical programs, ~50% reduction in cell/prop count for depth-2 programs (Pell), ~20% for depth-1 (fib). Wall time savings ~10-20 μs at our current scale. + +4. **Multi-thread cost is significant**. Sprint D's plan for shared-nothing BSP becomes shared-something — a step backward for parallelism. + +5. **Doesn't compose with future tags**. When worldview/iteration tagging arrives, this work gets retired. + +The trade-off would be acceptable IF (a) we had no other depth-alignment options, (b) cell/prop budget were tight in our common case, or (c) we were committing to non-token-tagged for the long-term. None of these hold. + +## Mantra alignment scorecard + +| Technique | "All-at-once" | "All in parallel" | "Structurally emergent" | "On-network" | Verdict | +|---|---|---|---|---|---| +| 1. Identity bridges (F.5) | ✓ | ✓ | ✓ (depth IS topology) | ✓ (cells + props) | **Aligned** | +| 2. Retiming pass | ✓ | ✓ | ✓ | ✓ (compile-time over (1)) | **Aligned** | +| 3. Set-latch | ✓ | ✓ | ✓ | ✓ (codified in design rules) | **Aligned** | +| 4. Token-tagged | ✓ | ✓ | ✓ (tags ARE structure) | ✓ (per-cell tags) | **Aligned long-term** | +| 5. Speculation | ✗ | ✗ | ✗ | ✗ (rollback log) | **Violates CALM** | +| 6. Manual barriers | — | ✓ (BSP=barriers) | ✗ | — | **Already have it; doesn't solve** | +| 7. FRP | ✗ | depends | ✗ | ✗ (different model) | **Wrong paradigm** | +| 8. Scheduler depth | ✓ | ✗ (synchronized state) | ✗ (off-network) | ✗ (in-scheduler metadata) | **Violates mantra** | +| 9. Clock domains | ✓ | ✓ | ✓ | ✓ (cell-based) | **Aligned but unneeded** | + +## Long-term trajectory + +| Future feature | Affects depth alignment? | Best fit | +|---|---|---| +| **Sprint D — multi-thread BSP** | Yes — shared metadata is costly | Bridges (thread-local fires) > scheduler depth (shared `last_round`) | +| **PPN Track 4 — compiler on network** | Yes — compiler will need iteration semantics | Token-tagged (matches worldview tags) | +| **PReduce / Track 9** | Maybe — readiness through value lattice | Set-latch (value-domain readiness) > depth tracking | +| **Effects / capabilities runtime** | Yes — non-monotone choices | Token-tagged (handles speculation cleanly) | +| **Logic / solve runtime** | Yes — backtracking + alternatives | Token-tagged (worldview-aligned) | +| **NTT — user-written propagators** | Yes — explicit depth in source? | Retiming pass over user-declared topology | + +**Debt-free path**: bridges (F.5) today → retiming pass (F.6 candidate) → token-tagged (when worldview tags land at runtime). + +**Debt-creating paths**: scheduler-level depth tracking, speculation, manual barriers. + +## Recommendation + +**Primary**: keep F.5's identity-bridge runtime; add a compile-time **retiming pass** over Low-PNet IR before code emission. + +The retiming pass: + +1. Builds a DAG of Low-PNet propagators with edge weights = combinational depth (= 1 per binary op, 0 per identity). +2. For each multi-input propagator, computes `max_depth(inputs)` and inserts `max_depth - depth_i` identity bridges on each shorter input path. +3. **Coalesces** redundant bridges — if multiple consumers share a producer at depth d and need it at depth d', share the bridge chain. +4. Asserts post-condition: every multi-input propagator has equal depth on all input paths. + +**Cost**: ~1.5 dev-days (1 day pass + ½ day tests + property-test on bridge invariant). Zero kernel changes. + +**Wins**: +- Bridge coalescing reduces cell/prop count for programs with multiple lifts from the same source (estimated 25-30% reduction for Pell-shape programs) +- Decouples depth alignment from the tail-rec recognizer; future translators (NTT, expr-iterate) get balancing for free +- Provides a checkable post-condition; F.5's invariant becomes property-tested rather than per-pattern-trusted + +**Defer**: +- Token-tagged dataflow until worldview/iteration tags land at runtime layer (likely PPN convergence or Sprint D's multi-thread design) +- Set-latch refactor until kernel has monotone-set + threshold-gate primitives +- Scheduler-level depth tracking — never; off-network metadata, debt-creating + +**Test plan**: +1. **Depth-balance invariant**: post-pass property test that every multi-input propagator's input cells have equal max-distance from any source cell. Random-expression-tree → retime → check invariant. +2. **Iteration correctness**: every existing tail-rec acceptance file passes (regression). +3. **Coalescing**: a synthetic program where 5 consumers share a producer at depth 3 should have 3 (not 15) identity bridges. Assert via `prologos_get_stat` for prop count. +4. **No-regression on simple programs**: fib, sum, factorial cell/prop counts at most ±1 from current (allowing for coalescing wins on the pre-select uniform lift). + +## Lessons distilled (process) + +1. **The mantra catches off-network state proposals reliably.** When the user pushed back with "shouldn't this be in the scheduler?", the rule book had the answer in `on-network.md`. Took a research detour to confirm, but the rules pointed the right direction. + +2. **Naming things correctly accelerates reasoning.** Calling F.5's bridges "scaffolding" yesterday led me to think they should be replaced. Calling them "Z⁻¹ delays" or "synchronous pipelining stages" reveals they're the canonical primitive of synchronous dataflow. + +3. **Trade-off matrices need three columns: cost / benefit / mantra alignment.** Two-column comparisons (cost / benefit) miss the architectural debt creation. The mantra column is what flagged scheduler-level tracking as wrong despite its perf savings. + +4. **Token-tagged dataflow is the long-term shape**. It's currently latent in the project (worldview-bitmask tagging at the elaborator). When/if runtime cells gain tags, F.5's bridges become a special case, not technical debt — they get retired naturally. + +5. **The Leiserson-Saxe retiming algorithm is directly applicable**. We don't need to invent a new technique; the retiming pass IS the formal name for what F.5 does ad-hoc. + +## References + +### Theoretical +- Valiant, "A Bridging Model for Parallel Computation" (1990, BSP) +- Leiserson & Saxe, "Retiming Synchronous Circuitry" (1991, Algorithmica) +- Lee & Messerschmitt, "Static Scheduling of Synchronous Data Flow Programs" (1987, IEEE Trans. Computers) +- Murray et al., "Naiad: A Timely Dataflow System" (SOSP 2013) +- Halbwachs et al., "The Synchronous Data Flow Programming Language LUSTRE" (1991) + +### Project artifacts +- [`docs/tracking/2026-05-01_BSP_NATIVE_SCHEDULER.md`](2026-05-01_BSP_NATIVE_SCHEDULER.md) § BSP cycle structure +- [`docs/tracking/2026-05-01_SH_LOWERING_FEATURE_MAP.md`](2026-05-01_SH_LOWERING_FEATURE_MAP.md) § "Sprint F.5: lag-matching bridges" +- [`.claude/rules/propagator-design.md`](../../.claude/rules/propagator-design.md) § Set-Latch for Fan-In Readiness +- [`.claude/rules/on-network.md`](../../.claude/rules/on-network.md) § Migration Checklist +- [`.claude/rules/structural-thinking.md`](../../.claude/rules/structural-thinking.md) § "Direct Sum Has Two Realizations" +- `racket/prologos/ast-to-low-pnet.rkt:103-180` — F.5's `emit-aligned-propagator!` and `lift-cell-to-depth` +- `runtime/prologos-runtime.zig:1-66` — Zig kernel surface +- `runtime/test-bsp-feedback.c` — kernel-level BSP feedback validation + +## Open questions for future research + +1. **What happens when union-typed conditional has branches of different depths?** F.5 currently doesn't lower union types. When it does, the per-component select cascade may have branches with different depths. The retiming pass should handle this naturally; verifying is open work. + +2. **Can DAG depth analysis identify "always-fresh" cells?** Some cells (literals, init constants) never change — propagators reading them never have stale values from those inputs. Depth analysis could exclude them, reducing bridges. Estimated savings: 1-2 bridges per literal-input propagator. Small. + +3. **Does retiming with multi-output propagators (when we add them) compose?** Currently all our propagators are (k, 1). Future operators with (k, m) shape complicate retiming. Open. + +4. **What's the cost model for depth-balance bridges in cache terms?** Bridge cells live in the same i64 cell array as data cells. If they're heavily used in inner loops, cache pressure goes up. Empirical investigation worthwhile when scale grows. + +5. **At what scale does token-tagged dataflow become competitive?** For our current kernel (i64 cells, simple kernels), bridges win on simplicity. For ~10K-cell programs with deep nesting and multi-rate behavior, the constant overhead of `(tag, value)` cells might be amortized by removing thousands of bridges. + +This research note will be revisited if/when worldview tagging lands at the runtime layer; the conclusions above may invert at that point. + +--- + +## Revision 2 (2026-05-02) — Collaborator critique: CALM, stratification, Pocket Universes + +After F.5/F.6 shipped, a collaborator pushed back with a deeper architectural critique. Quoting: + +> "I would encourage it to think of doing this, not as 'propagator chains' to 'synchronize' — this will break under different schedulers. What it's doing is essentially non-monotonic. According to the CALM theorem, anything on a single stratum should be coordination-free. If you need coordination, ordering, retraction, topological network changes, negation, accumulation — anything non-monotonic, the answer is always: STRATIFICATION. Do this reduction as a stratification in its own PU (Pocket Universe). Review the prior art." + +Research into the codebase confirms this is the project's stated discipline, and F.5/F.6 are implementing a tactical workaround to a problem whose strategic solution is stratification. This revision documents the critique, the prior art, and what the strategic solution would actually look like. + +### What F.5/F.6 are actually doing (reframed) + +The framing in §1-§9 above ("synchronous pipelining via Z⁻¹ delay elements") is operationally accurate but architecturally misleading. The accurate framing: + +**Tail-recursive iteration is fundamentally non-monotonic.** State cells get *overwritten* each iteration with new values. That's a retraction (the previous iteration's value is gone), not a monotone refinement. Per CALM, retraction inside a stratum is an anti-pattern. + +**F.5/F.6's identity bridges are forcing ordering inside a single S0 stratum** to make the non-monotone iteration produce coherent values. That ordering is exactly what CALM forbids: BSP guarantees coordination-free monotone fixpoints, which doesn't apply to our iteration semantics. + +**What we should be doing**: stratify. Each iteration is a stratum boundary; within an iteration, all operations are monotone (read state, compute step, propose next state); between iterations, the iteration stratum non-monotonically commits next-state values to state cells. + +### The project's canonical CALM rule + +Per [`.claude/rules/stratification.md`](../../.claude/rules/stratification.md) lines 64-83 ("When to Consider a New Stratum"): + +> "Reach for a new stratum when a computation: +> - Is **non-monotone**: it can retract information (the result can decrease, not just grow). S0 is monotone by CALM; non-monotone work belongs at a higher stratum. +> - Requires **fixpoint of another stratum** before evaluating: e.g., NAF needs S0 quiescence before checking provability. +> - Is **order-sensitive**: ordering comes from the stratum stack (Sk only fires after S0...S(k-1) quiesce), not from imperative control flow." + +Tail-recursive iteration matches all three criteria. F.5/F.6 try to keep it inside S0 by inserting ordering machinery (depth bridges); the rule says: don't, escalate to a stratum. + +### Prior art: PAR Track 0 CALM audit (2026-03-27) + +The cleanest precedent is documented in `docs/tracking/2026-03-27_PAR_TRACK0_CALM_AUDIT.md`. SRE decomposition (`sre-core.rkt:456-435`) and narrowing (`narrowing.rkt:304-323`) had fire functions that performed non-monotone topology changes inside S0 — creating new propagators dynamically based on input values. + +The fix direction: **don't do topology changes inside S0; emit a topology-change request as a cell value, and let the topology stratum process the request between rounds**. Same pattern: separate the monotone observation (request emission) from the non-monotone action (topology change), with a stratum boundary between them. + +F.5/F.6 are doing the symmetric thing: rather than emitting "advance iteration" as a request handled by an iteration stratum, they're forcing the entire iteration into S0 with delay-line bridges. The right move is the same as PAR Track 0's: stratify. + +### Prior art: SRE Track 2G scatter case (2026-03-30) + +The canonical "we needed a Pocket Universe" case study. Phase 6 of SRE Track 2G originally proposed an elaborate PU with internal stratification for implication-rule scattering. The NTT model caught a non-monotone scatter operation hidden inside the design. The PIR's lesson (`SRE_TRACK2G_PIR.md` §5, Pattern 5): + +> "NTT modeling catches architectural impurities (2/2 tracks that used it)." + +The actual Phase 6 implementation was 30 lines of eager evaluation (no PU yet), with technical debt explicitly accepted: "Implication rules as eager function (not network propagators) — Elaborate Pocket Universe design is Track 3-4 scope. Scaffolding is 30 lines." + +F.5/F.6 are in the same situation: they're scaffolding (eager bridges-as-ordering) standing in for a more architecturally-correct future (PU + iteration stratum). + +### What "iteration as a Pocket Universe" would look like + +Per the codebase definitions: + +- **Pocket Universe** (`docs/research/2026-03-21_PROPAGATOR_NETWORK_TAXONOMY.md` §9.3 + `docs/research/2026-04-07_BSP_LE_TRACK2_STAGE1_AUDIT.md` §4.3a): a scoped sub-network with its own stratification + worldview, communicating with the parent network only via designated entry/exit cells. + +- **Stratum** (`.claude/rules/stratification.md`): a request-accumulator cell + handler function, registered via `register-stratum-handler!`. After S0 quiescence, the BSP outer loop invokes registered handlers. + +A PU + iteration stratum design for tail-recursion: + +``` +Parent network + │ + │ init args (cells) + ▼ +┌──────────────────────────────────────────────┐ +│ Pocket Universe: tail-rec iteration │ +│ │ +│ S0 (within PU): │ +│ state cells (a, b, n) │ +│ step body propagators (read state → │ +│ compute "next-state proposals") │ +│ cond propagator (read state → compute │ +│ "should continue" Bool) │ +│ monotone, coordination-free, BSP fixpoint │ +│ │ +│ Iteration stratum (within PU): │ +│ Handler runs after S0 quiescence. │ +│ Reads cond cell + next-state-proposal │ +│ cells. │ +│ If cond = continue: commit proposals to │ +│ state cells (non-monotone overwrite), │ +│ reset S0 worklist, reenter S0. │ +│ If cond = halt: read result cell, exit PU. │ +│ │ +└──────────────────────────────────────────────┘ + │ + │ result (cell) + ▼ +Parent network +``` + +**Properties of this design**: + +1. **CALM-compliant**: S0 within the PU is fully monotone. Each iteration's S0 fixpoint computes next-state PROPOSALS (monotone refinement), then exits to the iteration stratum which COMMITS them (non-monotone, but in its own stratum). + +2. **No identity bridges needed**: depth alignment is handled by S0 fixpoint within an iteration. All step values coherently reflect "the current iteration's state" because they all read from the same state cells which are stable during S0. + +3. **Termination is structural**: cond cell is read by the iteration handler, which decides whether to re-enter S0 or exit. No fuel needed; no cyclic feedback edges in the network. + +4. **Scheduler-independent**: works under BSP, work-stealing, topological-order, or any other scheduler that guarantees S0 fixpoint before stratum handlers run. F.5/F.6's bridges, by contrast, are tied to BSP's specific snapshot-then-merge semantics — they would break under e.g. a Datalog-style seminaive scheduler that fires propagators in topological order. + +5. **Composable**: PUs can nest. An iteration whose body itself contains an iteration becomes a PU within a PU. + +### Cost of the PU + stratification approach + +**Kernel changes required**: + +1. **Nested networks**: the kernel must support sub-networks (cells + propagators scoped to a PU; not visible from outside). Currently the Zig kernel has one flat cell array. + +2. **Stratum handler infrastructure**: between S0 rounds, run registered handlers. Currently the kernel only has S0; no handler hook. + +3. **PU lifecycle**: install PU → run to S0 quiescence → invoke iteration handler → either re-enter S0 (advance iteration) or exit (read result cell, propagate to parent). + +4. **Per-PU statistics**: rounds, fires, iteration count separate from the parent network's stats. + +**Estimated effort**: ~5-10 days for the kernel infrastructure; ~2-3 days for the lowering changes (`ast-to-low-pnet.rkt` emits PU declarations instead of feedback edges); ~2-3 days for the LLVM lowering (`low-pnet-to-llvm.rkt` emits `prologos_pu_*` calls instead of identity bridges); ~2 days for tests + acceptance file updates. + +**Total**: ~10-15 days of focused work. Substantial but well-scoped. + +### Trade-off: what F.5/F.6 actually buy us, vs the strategic cost + +This is the honest accounting: + +**F.5/F.6's wins**: +- Shipped today, no kernel changes +- 34 acceptance examples pass +- Pell works +- ~10-25% structural overhead per program (real cost) + +**F.5/F.6's hidden costs**: +- Architecturally violates CALM (non-monotone iteration enforced via ordering inside S0) +- Tied to BSP semantics; would break under other schedulers +- Doesn't match the project's stated stratification discipline +- Each future translator (NTT, expr-iterate, …) inherits the same anti-pattern +- The depth-balance invariant we added (F.6) is a SYMPTOM of the missing stratum: we're checking that bridges balance the network *because we need ordering inside what should be a monotone stratum* + +**PU + iteration stratum's wins**: +- CALM-compliant; aligns with project discipline +- Scheduler-agnostic +- No bridge cells; smaller networks +- Composable (nested PUs) +- Each future translator gets stratification-aware lowering for free + +**PU + iteration stratum's costs**: +- ~10-15 days of kernel + lowering work +- Multi-stratum runtime is genuinely new infrastructure +- Larger scope, more risk + +### Revised recommendation + +F.5 + F.6 are correctly identified as **scaffolding**, not the strategic solution. They ship today because the strategic solution (PU + iteration stratum) requires kernel infrastructure we don't have yet. + +**Position F.5/F.6 explicitly as scaffolding** in the project tracking (analogous to SRE Track 2G's "30-line eager Phase 6 scaffolding"), with the strategic followup tracked as a future track. + +**The strategic followup** ("Sprint G: tail-rec as Pocket Universe with iteration stratum") becomes the canonical tail-rec lowering once kernel multi-stratum infrastructure lands. At that point F.5/F.6's bridges + retiming + depth-balance invariant get retired. + +**Don't do retiming optimization (F.6 was the optimization layer over F.5) beyond what's already shipped** — investing more in F.6's optimization is investing in scaffolding that gets retired when stratification lands. + +**Reorder the SH track sequence** so PU + stratification is closer to the front: + +| Sprint | Was (per SH_LOWERING_FEATURE_MAP) | Revised | +|---|---|---| +| F.5 / F.6 | tactical lag-matching | tactical scaffolding (shipped) — leave as-is | +| G | Heap + GC for runtime | **PU + iteration stratum** (architectural correctness — retires F.5/F.6) | +| H | Heap + GC for runtime | (was G) | + +This reordering is justified by: F.5/F.6 are a known CALM violation. Each new translator we build on top inherits the violation. Retiring it earlier means less debt accumulation. + +### Generalization beyond tail-rec + +The same critique applies to several places in the project: + +- **PReduce / Track 9** (per agent research §4): currently designed to fire reduction propagators in S0 alongside type propagators. But reduction is incremental and CAN retract if a meta solution changes. This is the same pattern: non-monotone behavior being forced into S0. The CALM-aware design would put reduction in its own stratum or PU. + +- **SRE Track 2G Phase 6** (already known): eager evaluation as scaffolding; PU is Track 3-4 scope. + +- **Constraint retry** (metavar-store.rkt): currently uses set-latch fan-in within a single stratum. Per the rules, this is correct — readiness AGGREGATION is monotone. But the action triggered (constraint retry) is non-monotone and lives in L2 Resolution stratum. So this case is already CALM-compliant. + +- **The set-latch refactor I considered for F.5b**: would have been a wrong move. Set-latch is for monotone readiness aggregation, not for non-monotone iteration. Confirmed by the agent research: "Set-latch is the right pattern for fan-in readiness across heterogeneous sources, which we don't have yet at the runtime level." + +### What the research doc said in revision 1 vs revision 2 + +**Revision 1**: "F.5 is the right pattern for our problem; retiming optimization (F.6) is the principled improvement." + +**Revision 2**: "F.5/F.6 are tactical scaffolding for an architectural problem (non-monotone iteration in a monotone stratum). The strategic fix is PU + iteration stratum. Ship F.5/F.6, but mark them as scaffolding and prioritize the strategic followup." + +The collaborator was right. Three reasons revision 1 missed it: + +1. **Frame-confusion**: revision 1 framed the problem as "synchronous pipelining" — a hardware/circuit metaphor where Z⁻¹ delays are the primitive. That metaphor is operationally accurate but architecturally misleading; in our software substrate, the right metaphor is "non-monotone iteration in a CALM-aware stratification system." + +2. **Tactical-vs-strategic conflation**: revision 1 evaluated each option's correctness + cost but didn't distinguish "is this a tactical fix or a strategic structure." F.5/F.6 are tactical; the strategic fix is PU + stratum. + +3. **Underweighting prior art**: the project has a clear `stratification.md` rule and a documented CALM-audit precedent (PAR Track 0). Revision 1 cited propagator-design.md and on-network.md but missed stratification.md as the load-bearing rule. + +### Lessons (process, distilled) + +1. **The mantra catches structural debt; the rules catch CALM debt.** When a fix feels like it's solving a synchronization problem inside a monotone stratum, that's the smell. The answer is almost always "stratify, don't synchronize." + +2. **"Pocket Universe" is the project's idiom for stratified-sub-network**. When in doubt about how to handle non-monotone sub-computations, reach for PU before reaching for in-stratum scaffolding. + +3. **Tactical fixes aren't shameful, but mark them as such**. SRE Track 2G's 30-line eager Phase 6 was correct to ship. The mistake would have been pretending it was the architectural solution. F.5/F.6 should be marked the same way. + +4. **The depth-balance invariant in F.6 is itself a smell**. Inventing a structural invariant to enforce ordering inside a monotone stratum is the opposite of CALM. Future "we need an invariant to enforce X inside a stratum" should trigger the question: "should X be a stratum?" + +### Updated open questions + +In addition to the open questions in revision 1: + +6. **What's the minimum-viable kernel infrastructure for PU + iteration stratum?** Could it be implemented as a "scheduler outer loop with handlers", without rearchitecting cells? (Probably yes — the BSP-LE Track 2B project already has `register-stratum-handler!` as a pattern; we'd port that to the Zig kernel.) + +7. **Can the PU realization be incremental?** Could we add stratum-handler infrastructure to the kernel WITHOUT immediately migrating F.5/F.6, and then migrate program-by-program? Or does it need to be all-or-nothing? + +8. **What does this say about PReduce / Track 9?** PReduce currently designs reduction-on-S0; same critique applies. Should PReduce design be updated to use a reduction stratum or PU before implementation begins? + +9. **NTT semantics + iteration**: when NTT lands, will user-written `propagator` declarations be allowed to express "this is an iteration; it lives in its own PU"? Or do iteration boundaries have to be inferred from the AST shape (as F.5's tail-rec recognizer does)? + +These should drive the SH track resequencing if the critique is accepted. + +### References (revision 2 additions) + +- `docs/tracking/2026-03-27_PAR_TRACK0_CALM_AUDIT.md` — the canonical "non-monotone behavior in S0 → stratify" precedent +- `docs/research/2026-03-21_PROPAGATOR_NETWORK_TAXONOMY.md` §9.3 — Pocket Universe as structural decomposition +- `docs/research/2026-04-07_BSP_LE_TRACK2_STAGE1_AUDIT.md` §4.3a — Pocket Universe as worldview boundary (ATMS branches) +- `docs/tracking/2026-03-30_SRE_TRACK2G_PIR.md` §5 (Pattern 5), §8 — the "30-line eager scaffolding for what's structurally a PU" case study +- `docs/tracking/2026-03-21_TRACK9_REDUCTION_AS_PROPAGATORS.md` — PReduce design, currently with the same in-S0 anti-pattern +- `racket/prologos/propagator.rkt:2441` — `register-stratum-handler!` API (the runtime pattern to port) +- `racket/prologos/relations.rkt:115` — S1 NAF: example of a non-monotone stratum implemented via the handler API +- `racket/prologos/metavar-store.rkt:1392` — S(-1) Retraction: another non-monotone stratum precedent diff --git a/docs/tracking/2026-05-02_FIRE_FN_TAG_AUDIT_TRACK1.md b/docs/tracking/2026-05-02_FIRE_FN_TAG_AUDIT_TRACK1.md new file mode 100644 index 000000000..a6450e489 --- /dev/null +++ b/docs/tracking/2026-05-02_FIRE_FN_TAG_AUDIT_TRACK1.md @@ -0,0 +1,157 @@ +# Fire-Fn Tag Audit (SH Track 1, audit phase) + +**Date**: 2026-05-02 +**Status**: Audit — categorization, no broad tagging +**Track**: SH Track 1 (`.pnet` network-as-value), audit phase +**Branch**: `claude/prologos-layering-architecture-Pn8M9` +**Cross-references**: +- [SH Master Tracker](2026-04-30_SH_MASTER.md) — Track 1 +- [SH Series Alignment Delta](2026-05-02_SH_SERIES_ALIGNMENT.md) — §5 names this audit as the next Track 1 sub-piece +- Fire-fn-tag field commit: `b0227cb` (added `fire-fn-tag` field with default `'untagged`) +- Test fix-up: `85f5ecd` (3 direct ctor calls in test-source-loc-infrastructure.rkt) + +## 1. Purpose + +The `fire-fn-tag` field on `propagator` (commit `b0227cb`) defaults to `'untagged` for back-compat. This audit categorizes the ~200 production `net-add-propagator` / `net-add-fire-once-propagator` / `net-add-broadcast-propagator` call sites and identifies which ones will need explicit tags for `.pnet` network-topology serialization to be meaningful. + +**Key insight discovered during the audit**: the vast majority of fire-fns in the codebase are **compile-time-only** — they drive elaboration, typing, narrowing, and decomposition. They fire during `process-file`, write to typing cells, and the result is read back as typed AST. They never run in a deployed program. + +For `.pnet` deployment artifacts (mode `'program`, per the format-2 wrapper), only **runtime-relevant** fire-fns need stable tags. That set is much smaller than 200. + +## 2. Call-site distribution by file + +Total `net-add-*` invocations in production code (excluding tests): + +| File | Count | Compile-time / Runtime / Both | +|---|---|---| +| `typing-propagators.rkt` | 44 | Compile-time (typing rules) | +| `elaborator-network.rkt` | 40 | Compile-time (elaboration infra) | +| `propagator.rkt` | 22 | Substrate (the wrappers themselves) | +| `relations.rkt` | 10 | Both (compile-time tabling + runtime solve) | +| `session-propagators.rkt` | 8 | Compile-time (session typing) | +| `sre-core.rkt` | 7 | Compile-time (SRE structural reasoning) | +| `session-runtime.rkt` | 6 | **Runtime** (session protocol execution) | +| `constraint-propagators.rkt` | 6 | Compile-time (constraint solving during typing) | +| `wf-propagators.rkt` | 5 | Compile-time (well-foundedness checks) | +| `unify.rkt` | 5 | Compile-time (PUnify) | +| `elab-network-types.rkt` | 4 | Compile-time | +| `narrowing.rkt` | 2 | Compile-time | +| `merge-fn-registry.rkt` | 2 | Compile-time (registry) | +| `driver.rkt` | 2 | Compile-time | +| `sre-rewrite.rkt` | 1 | Compile-time (DPO rewriting) | +| `effect-bridge.rkt` | 1 | Both (effect ordering checks compile-time, execution runtime) | +| `effect-ordering.rkt` | 1 | Compile-time | +| `effect-executor.rkt` | 1 | **Runtime** (effect execution) | +| `cap-type-bridge.rkt` | 1 | Compile-time | +| `capability-inference.rkt` | 1 | Compile-time | +| `bilattice.rkt` | 1 | Substrate | +| `infra-cell-sre-registrations.rkt` | 1 | Substrate (domain registrations) | +| `metavar-store.rkt` | 1 | Compile-time | +| `performance-counters.rkt` | 1 | Compile-time | +| **Total** | **~170** | (some files have multiple categories) | + +(Counts via `grep -cE` per file; rough.) + +## 3. Categorization framework + +Three categories based on whether the propagator participates in deployment: + +### A. Compile-time-only propagators (the majority) + +Fire-fns that drive elaboration, typing, decomposition, constraint solving, narrowing, etc. They run inside `process-file`'s elaboration network, produce a typed AST, then stop being relevant. The compiled program (Track 4 output) does not load these propagators — they served their purpose at compile time. + +**Tag policy**: leave at `'untagged`. They never appear in a `'program` mode `.pnet` because they're not in the runtime sub-graph. + +Examples: `typing-propagators.rkt`, `elaborator-network.rkt`, `unify.rkt`, `narrowing.rkt`, `constraint-propagators.rkt`, `sre-core.rkt`, `metavar-store.rkt`. + +### B. Runtime propagators (the small but load-bearing set) + +Fire-fns that DO run at deployment. They appear in the runtime sub-graph of compiled programs. Need stable tags so the `.pnet` loader can resolve them against the runtime kernel. + +**Tag policy**: explicit, stable, kernel-resolvable. Naming convention `'rt--`, e.g., `'rt-int-add`, `'rt-merge-set-union`, `'rt-session-send`. + +Examples: `session-runtime.rkt` (session protocol execution), `effect-executor.rkt` (effect execution), `relations.rkt`'s solve-time propagators. + +### C. Substrate propagators (built into the kernel itself) + +Fire-fns that ARE the kernel. Lattice merges, structural decomposers, broadcast-fan, fire-once flags. The kernel provides them; user `.pnet` files reference them by tag. + +**Tag policy**: explicit, stable, kernel-defined. Naming convention `'kernel-`, e.g., `'kernel-merge-set-union`, `'kernel-bsp-round`, `'kernel-broadcast-fan`. + +Examples: `propagator.rkt` (the wrappers themselves), `infra-cell-sre-registrations.rkt`, `bilattice.rkt`, `merge-fn-registry.rkt`. + +## 4. Concrete runtime-relevant fire-fns identified + +The following are the call sites that MUST get stable tags for deployment: + +| Site | Category | Proposed tag | +|---|---|---| +| `session-runtime.rkt` × 6 sites | B | `'rt-session-send`, `'rt-session-recv`, `'rt-session-select-l`, `'rt-session-select-r`, `'rt-session-offer`, `'rt-session-close` | +| `effect-executor.rkt` × 1 site | B | `'rt-effect-execute` | +| `relations.rkt` solve-time propagators (subset of 10) | B | `'rt-relation-clause-N` (per-clause, generated at registration time) | + +That's roughly **10–20 distinct runtime fire-fns**. Far below 200. + +For the substrate kernel (category C), the count is similar: +| Substrate fn | Tag | +|---|---| +| Set union merge | `'kernel-merge-set-union` | +| Hash union merge | `'kernel-merge-hash-union` | +| Top-bot lattice merge | `'kernel-merge-tagged-cell-value` | +| Component-tagged compound merge | `'kernel-compound-tagged-merge` | +| Broadcast fan | `'kernel-broadcast-fan` | +| Fire-once flag-guard | `'kernel-fire-once-guard` | +| Threshold check | `'kernel-threshold-fire` | +| Cross-domain α | `'kernel-cross-domain-alpha` | +| Cross-domain γ | `'kernel-cross-domain-gamma` | + +~10 substrate primitives. Together with the runtime set, **the total fire-fn-tag namespace is ~20–30 stable tags**, not 200. + +## 5. Why not tag everything + +I considered mass-tagging all 200 call sites and rejected it for these reasons: + +1. **Compile-time fire-fns don't need tags.** They never appear in deployment artifacts. Tagging them is busywork that adds complexity without value. + +2. **Auto-generated tags are fine for unique call sites.** The `'untagged` default is acceptable as long as any future serialization (Track 1's network-topology phase) refuses to serialize `'untagged` propagators in `'program` mode. This makes the missing-tag case loud rather than silent. + +3. **Stable tags for the small runtime set is what matters.** ~20–30 named tags that the runtime kernel and per-program `.o` files agree on is a manageable convention. Naming 200 ad-hoc tags would dilute the namespace. + +4. **The audit framework + naming convention IS the deliverable.** Once we've categorized which sites are compile-time vs runtime vs substrate, future track work can apply tags incrementally and consistently. + +## 6. Naming convention (proposed) + +For tags emitted by code in this codebase: + +| Prefix | Meaning | +|---|---| +| `'kernel-*` | Built into `libprologos-runtime` (the Zig kernel). Lattice merges, scheduler primitives. | +| `'rt-*` | Runtime fire-fns shipped with the user program's `.o`. Generated by the per-program lowering pass; tag includes the user program's hash for uniqueness. | +| `'cT-*` | Compile-time fire-fns. By default, these stay `'untagged`. The prefix is reserved for cases where compile-time fire-fns need to round-trip through `.pnet` for module-cache purposes (which is the existing format-1 path; the cache today doesn't use tags). | +| `'untagged` | Default. Acceptable for compile-time fire-fns. Refused at deployment-mode serialization. | + +## 7. What this audit doesn't do + +- **Does not tag any call sites.** The fire-fn-tag field is in place; the default `'untagged` works fine. Future Track 1 phases will tag call sites *as the deployment-mode serializer requires them*. Tagging in advance commits us to a naming scheme prematurely. + +- **Does not change runtime behavior.** Pure documentation + categorization. The kernel still works as before. + +- **Does not write the deployment-mode `.pnet` serializer.** That's a future Track 1 phase that consumes this audit's output to know which call sites need attention. + +## 8. Forward path + +This audit feeds three downstream pieces of work: + +1. **Track 1 deployment-mode serialization (future phase)**: when serializing a `.pnet` in `'program` mode, refuse to serialize `'untagged` propagators. Error message: "fire-fn at has no tag; cannot serialize for deployment. See fire-fn tag audit doc § 4." + +2. **Per-program lowering pass (Track 2 / Track 4)**: when lowering a user program's runtime sub-graph, generate `'rt--` tags for each user fire-fn body. Emit them as exported symbols in the per-program `.o`. + +3. **Kernel API design (Track 4)**: the runtime kernel's API includes a tag-resolution table mapping `'kernel-*` symbols to function pointers. This audit identifies the ~10 entries that table needs. + +## 9. Cross-references + +- SH Master Tracker, Track 1 +- Fire-fn-tag struct field: commit `b0227cb` +- `.pnet` format-2 wrapper: commit `65312be` — provides the mode flag (`'module` vs `'program`) that determines whether `'untagged` is acceptable +- Low-PNet IR data model: `propagator-decl` carries `fire-fn-tag` — Track 2 implementation (commit `f4157be`) +- Issue #44 (PReductions output contract) — once PReductions registers its propagators with stable tags, those tags slot into the `'kernel-*` namespace diff --git a/docs/tracking/2026-05-02_HAMT_ZIG_TRACK6.md b/docs/tracking/2026-05-02_HAMT_ZIG_TRACK6.md new file mode 100644 index 000000000..17752c3cb --- /dev/null +++ b/docs/tracking/2026-05-02_HAMT_ZIG_TRACK6.md @@ -0,0 +1,97 @@ +# Persistent HAMT in Zig — Track 6 sub-piece + +**Date**: 2026-05-02 +**Status**: Stage 4 implementation +**Track**: SH Track 6 (Runtime services), Issue #42 Path A +**Branch**: `claude/prologos-layering-architecture-Pn8M9` + +## 1. Goal + +Implement a persistent hash-array-mapped trie in Zig as `runtime/prologos-hamt.zig`. The first non-trivial data structure in the substrate kernel — validates that Zig is the right language for substrate work and provides the persistent-map primitive every Track 4 path needs. + +Per Issue #42 Path A: re-implement CHAMP/HAMT in Zig as part of the runtime kernel. + +## 2. Scope + +### In scope + +- 32-way branching trie (Bagwell-style), 5 bits per level +- Wang's 32-bit integer hash on `u32` keys (sequential cell-ids would otherwise produce a degenerate trie) +- Path-copy on insert/remove (persistent semantics — old roots remain valid) +- C-ABI exports for `prologos_hamt_new`, `prologos_hamt_lookup`, `prologos_hamt_insert`, `prologos_hamt_remove`, `prologos_hamt_size` +- Zig unit tests covering: empty, single insert, multi-insert, overwrite, lookup-miss, remove, persistence (old root unaffected by new insert), large-N stress +- C-side smoke test linking the `.o` and exercising the C ABI + +### Out of scope (deferred) + +- Reference counting or GC — nodes leak on insert/remove. Fine for the substrate kernel where the BSP scheduler controls lifetime; revisit when Track 6 GC design lands. Documented in the Zig source. +- Hash collision handling beyond the 32-bit keyspace (impossible with `u32` keys; would matter for `u64` later) +- Generic value type — fixed `i64` for now (fits cell-ids, propagator-ids, pointer-sized payloads) +- Concurrent / lock-free operation — single-threaded; Track 6 multi-threading is N4+ +- Iterator / fold operations — only point queries needed for substrate kernel use + +## 3. Algorithm sketch + +``` +Node = Branch { bitmap: u32, children: [popcount(bitmap)]*Node } + | Leaf { key: u32, value: i64 } + +hash(k) = wang_hash_u32(k) # 32-bit pseudorandom output + +lookup(node, k, depth): + case node: + Leaf(lk, lv): if lk==k then Some(lv) else None + Branch(bm, cs): + bit = (hash(k) >> (depth*5)) & 0x1F + if bm & (1 << bit) == 0: None + else lookup(cs[popcount(bm & ((1<