Fix CI: rackcheck dep + bench-ppn-track3 stale API by kumavis · Pull Request #3 · LogosLang/prologos

kumavis · 2026-04-23T06:41:24Z

Two CI failures in the Tests workflow's "Install dependencies" step
(raco pkg install --auto compiles all collections in the package):

tests/test-generators.rkt and tests/test-properties.rkt require
'rackcheck' (property-based testing) which was not declared in
info.rkt. Added "rackcheck" to build-deps so --auto installs it.
benchmarks/micro/bench-ppn-track3.rkt used the pre-D.5b stage-based
API of form-pipeline-value (first field = single stage symbol,
accessor = form-pipeline-value-stage). The struct was refactored to
a set-based transforms field (seteq of stage symbols) per the
dependency-set-replaces-stage-chain design, but this benchmark was
not updated. Migrated three construction sites to wrap the stage in
(seteq stage) and six V1 accessor sites to form-pipeline-value-
transforms. The V1 commutativity/associativity/idempotence tests
validate correctly against the powerset lattice's set-union merge.

https://claude.ai/code/session_01MYWyvMcQHNAdc8FqEoPHEy

Two CI failures in the Tests workflow's "Install dependencies" step (raco pkg install --auto compiles all collections in the package): 1. tests/test-generators.rkt and tests/test-properties.rkt require 'rackcheck' (property-based testing) which was not declared in info.rkt. Added "rackcheck" to build-deps so --auto installs it. 2. benchmarks/micro/bench-ppn-track3.rkt used the pre-D.5b stage-based API of form-pipeline-value (first field = single stage symbol, accessor = form-pipeline-value-stage). The struct was refactored to a set-based transforms field (seteq of stage symbols) per the dependency-set-replaces-stage-chain design, but this benchmark was not updated. Migrated three construction sites to wrap the stage in (seteq stage) and six V1 accessor sites to form-pipeline-value- transforms. The V1 commutativity/associativity/idempotence tests validate correctly against the powerset lattice's set-union merge. https://claude.ai/code/session_01MYWyvMcQHNAdc8FqEoPHEy

hierophantos

Awesome! Thank you for your PR! Approved!

Brings in: - cef5ff5 Fix CI: rackcheck dep + bench-ppn-track3 stale API - 922c38e Merge pull request #3 from LogosLang/claude/fix-github-ci-job-TcxYz PR content is our first external-contributor work from a friend of the project. It fixes two CI failures in the Tests workflow's 'Install dependencies' step: 1. Adds 'rackcheck' to info.rkt build-deps (property-based testing dependency required by test-generators.rkt and test-properties.rkt but not previously declared). 2. Migrates benchmarks/micro/bench-ppn-track3.rkt from the pre-D.5b stage-based form-pipeline-value API (single stage symbol, accessor form-pipeline-value-stage) to the set-based transforms field (seteq of stage symbols per dependency-set-replaces-stage-chain design). Three construction sites + six accessor sites updated. V1 commutativity/associativity/idempotence tests validate against the powerset lattice's set-union merge. No file overlap with local T-2 work (expr-Open AST + typing semantics + elaborator + tests + probe baseline). Merge is trivial.

The benchmark file references the pre-D.5b TMS API (`tms-write`, `tms-cell-value`, `tms-read`, `tms-commit`), which was removed when the TMS was refactored into the `tms-cell` struct + `atms-write-cell` interface. The file is a "Pre-0 micro-benchmark" (historical baseline measurements for Track 2 before it was implemented) and does not run in CI or the regression suite, but `raco pkg install --auto` compiles every .rkt in the collection, so its unbound-identifier error fails the build. Add `racket/prologos/benchmarks/micro/info.rkt` with `compile-omit-paths '("bench-bsp-le-track2.rkt")` so `raco setup` skips it. This mirrors the PR #3 fix for `bench-ppn-track3.rkt` (which migrated to the current API) but for a file whose full migration (multiple API changes) is non-trivial and out of scope for this branch. Verified locally with `raco pkg install --deps force --no-docs --link --name prologos-dev racket/prologos`: bench-bsp-le-track2 no longer appears in the summary of errors. https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp

Two coordinated changes for the trait constraint resolution path. 1. resolution.rkt — Pure trait bridge factory signature change. make-pure-trait-bridge-factory: OLD: (lambda (trait-name dict-cell-id dep-cell-ids) ...) NEW: (lambda (trait-name dict-cell-id dict-meta-id dep-pairs) ...) where dep-pairs = (listof (cons cell-id meta-id)). make-pure-trait-bridge-fire-fn body uses new helpers: meta-component-read pnet cell-id meta-id meta-component-write pnet cell-id meta-id value These dispatch on (meta-universe-cell-id? cell-id): - universe → compound-cell-component-{ref,write}/pnet - per-cell legacy → net-cell-{read,write} This handles the universe model where dict-meta + dep-metas may all share a universe-cid (e.g., all type metas under b-iii). The dict-val early-exit reads dict-meta's component (not the whole hasheq); each type-arg read reads its own meta's component; the resolved dict write goes to dict-meta's component. Order of dep-pairs preserved → impl-key-str ordering preserved per D.3 §7.5.12.9 drift risk #3. 2. metavar-store.rkt:425-459+466-481 — Install site migration. - Replaces 3-stage fan-in (Stages 1-3, ~35 LoC) with single add-readiness-set-latch! call. action-thunk produces (action-resolve-trait meta-id info) on latch non-empty. - Bridge factory call updated to pass dict-meta-id (= meta-id) + dep-pairs (built from type-arg-metas in declaration order). - elab-add-propagator now declares :component-paths for universe-cid deps (cons-pair shape per D.3 §7.5.12.5 corrected). Per-cell deps have no component-paths (per-meta cell IS the dependency unit). - Bridge propagator tagged with current-speculation-assumption for branch-isolated firing under BSP-LE 2/2B. Verification: - check-parens balanced; raco make clean - Probe (examples/2026-04-22-1A-iii-probe.prologos): 0 errors, output identical to baseline - PPN 4C acceptance file (examples/2026-04-17-ppn-track4c.prologos): 0 errors, all expected outputs correct including polymorphic Seqable + Maybe + List Int + Map Keyword Open - 189 targeted tests across 8 files: all PASS except the 4 known test-constraint-retry-propagator.rkt failures (test-rewrite targets per step 9). Trait-resolution + bundles + speculation-bridge tests all GREEN — bridge factory signature change preserves correctness. Per D.3 §7.5.12.9 step 4 (factory signature) + step 6 (install site). Next: hasmethod bridge migration (site 3/3) — analog with 4 cell-ids to dispatch (meta + trait-var + dict-meta + N type-args).

…dated Final install-site migration. Same shape as the trait bridge but with 4 cell-ids to dispatch (meta + trait-var + dict-meta + N type-args). 1. resolution.rkt — Pure hasmethod bridge factory signature change. make-pure-hasmethod-bridge-factory: OLD: (lambda (method-name meta-cell-id trait-var-cell-id dict-meta-cell-id dep-cell-ids) ...) NEW: (lambda (method-name meta-pair trait-var-pair-or-#f dict-meta-pair-or-#f dep-pairs) ...) where each *-pair = (cons cell-id meta-id). make-pure-hasmethod-bridge-fire-fn: - Destructures meta-pair, trait-var-pair, dict-meta-pair into cell-id and meta-id - All reads via meta-component-read (universe → compound-cell- component-ref/pnet, per-cell → net-cell-read) - All writes via meta-component-write (analog) - Reads: * meta-cell-id + meta-id (early exit on resolved) * each dep pair (type-arg ground check, in order) * trait-var pair (resolved-trait-name lookup) * trait-var pair re-read (write check) * dict-meta pair (write check) - Writes: * trait-var if unsolved (resolved-trait-name) * dict-meta if unsolved (dict-expr) * meta-cell (projected method) The shared meta-component-read/write helpers (added in trait migration) serve both factories. Order of dep-pairs preserved through type-arg- vals → impl-key-str (drift risk #3 cleared). 2. metavar-store.rkt:577-618 + :622-653 — Install site migration. - Replaces 3-stage fan-in (Stages 1-3, ~42 LoC) with single add-readiness-set-latch! call. action-thunk produces (action-resolve-hasmethod meta-id info) on latch non-empty. - Bridge factory call updated to pass paired tuples for meta + trait-var + dict-meta + dep-pairs. trait-var-meta-id extracted from expr-meta-id of trait-var-expr (Track 10B Phase A3 pattern extended). - elab-add-propagator declares :component-paths for universe-cid deps. Tagged with current-speculation-assumption. Verification: - check-parens balanced; raco make clean - Probe (examples/2026-04-22-1A-iii-probe.prologos): 0 errors, output identical to baseline - PPN 4C acceptance file: 0 errors, all expected outputs correct - 217 targeted tests across 11 files: all PASS except the 4 known test-constraint-retry-propagator.rkt failures. Critically, test-hasmethod-01 + test-hashable-01 + test-hashable-02 (which exercise the hasmethod bridge path) all GREEN — factory signature + paired-tuple dispatch preserves correctness. Per D.3 §7.5.12.9 step 4 (factory signature) + step 6 (install site). All 3 fan-in install sites migrated. Next: retire 4 vestigial scan functions (Option B per audit) — zero production callers; only test file invocations to update. Then test file rename + restructure.

Eigentrust pitfalls #3: in WS mode, `'[0/1 1/2 1/2]` annotated as `[List Rat]` raised `Type mismatch [List [List Rat]] ...` because `string->number "0/1"` simplified to integer 0 *before* literal-type inference, mixing Int and Rat in a list whose annotation demanded Rat. Fix shape (a — preserve at parse time): a number-token lexeme containing `/` is wrapped in a `($rat-literal val)` sentinel by the WS reader, mirroring the existing `($nat-literal val)` sentinel for `42N`. Both surface parsers (parser.rkt for the preparse path, tree-parser.rkt for the cell pipeline path) route the sentinel / slash-lexeme to `surf-rat-lit`, preserving Rat-ness even when the simplified value is an integer. Why (a) over (b — context-aware coercion): (a) is a single-source- faithful transform — a user who writes `0/1` MEANS Rat, regardless of what `string->number` simplifies to. (b) would require plumbing expected-type context into list-literal element parsing, which the parser pipeline doesn't carry. (a) keeps the bare integer literals `0` and `42` as Int (still! — the slash is the distinguisher). Trade-off: the WS reader's wire format for slash literals now wraps in `$rat-literal`. One existing round-trip assertion was updated (test-negative-literals.rkt:120) to expect the sentinel. No behavioral change for `(rat 0/1)`, `0`, `42`, true rationals (`1/2`, `-3/7`) — all keep their existing types. Files changed: - racket/prologos/parse-reader.rkt +13 emit $rat-literal sentinel - racket/prologos/parser.rkt +13 handle $rat-literal sentinel - racket/prologos/tree-parser.rkt +9 slash-lexeme → surf-rat-lit; flatten-ws-datum exemption - tests/test-rat-literal-in-list.rkt +new 17 cases: reproducer + corners - tests/test-negative-literals.rkt +6 update one round-trip expect Tests verified: test-rat (31), test-rat-literal-in-list (17), test-list-literals + test-pvec* (98), test-parse-reader + test-parser + test-sexp-reader-parity (211), test-integration + test-parse-integration + test-surface-integration (117), test-negative-literals (25), test-approx-literal (22), test-refined-rat. Total 521+ tests pass. Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>

The 2026-04-23 eigentrust pitfalls memo (forthcoming branch) enumerated 16 items hit during the EigenTrust implementation. Items #1-7 and #11-15 are language/elaboration defects with their own PRs. Items #8, #9, #10, and #16 are observations rather than Prologos defects; no compiler change is needed for them but the memo deserves a parallel disposition note so a future reader does not double-count them as open work. #8 (exact-Rat slow on deep iter): intrinsic to exact rational arithmetic; benchmark-scope guidance, not a fix. #9 (Posit32 literals work): positive observation; `~` literal prefix is unambiguous unlike `0/1`. No action. #10 (PVec preserves where List does not): subsumed by pitfall #3 fix. After #3 lands, both literal forms preserve element type uniformly. Close as duplicate. #16 (column-stochastic vs row-stochastic): algorithm/spec clarification, not a Prologos defect. The eigentrust implementation branch already takes column-stochastic M directly and validates via col-stochastic?. https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>

Eigentrust pitfalls #3: in WS mode, `'[0/1 1/2 1/2]` annotated as `[List Rat]` raised `Type mismatch [List [List Rat]] ...` because `string->number "0/1"` simplified to integer 0 *before* literal-type inference, mixing Int and Rat in a list whose annotation demanded Rat. Fix shape (a — preserve at parse time): a number-token lexeme containing `/` is wrapped in a `($rat-literal val)` sentinel by the WS reader, mirroring the existing `($nat-literal val)` sentinel for `42N`. Both surface parsers (parser.rkt for the preparse path, tree-parser.rkt for the cell pipeline path) route the sentinel / slash-lexeme to `surf-rat-lit`, preserving Rat-ness even when the simplified value is an integer. Why (a) over (b — context-aware coercion): (a) is a single-source- faithful transform — a user who writes `0/1` MEANS Rat, regardless of what `string->number` simplifies to. (b) would require plumbing expected-type context into list-literal element parsing, which the parser pipeline doesn't carry. (a) keeps the bare integer literals `0` and `42` as Int (still! — the slash is the distinguisher). Trade-off: the WS reader's wire format for slash literals now wraps in `$rat-literal`. One existing round-trip assertion was updated (test-negative-literals.rkt:120) to expect the sentinel. No behavioral change for `(rat 0/1)`, `0`, `42`, true rationals (`1/2`, `-3/7`) — all keep their existing types. Files changed: - racket/prologos/parse-reader.rkt +13 emit $rat-literal sentinel - racket/prologos/parser.rkt +13 handle $rat-literal sentinel - racket/prologos/tree-parser.rkt +9 slash-lexeme → surf-rat-lit; flatten-ws-datum exemption - tests/test-rat-literal-in-list.rkt +new 17 cases: reproducer + corners - tests/test-negative-literals.rkt +6 update one round-trip expect Tests verified: test-rat (31), test-rat-literal-in-list (17), test-list-literals + test-pvec* (98), test-parse-reader + test-parser + test-sexp-reader-parity (211), test-integration + test-parse-integration + test-surface-integration (117), test-negative-literals (25), test-approx-literal (22), test-refined-rat. Total 521+ tests pass. Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>

The 2026-04-23 eigentrust pitfalls memo (forthcoming branch) enumerated 16 items hit during the EigenTrust implementation. Items #1-7 and #11-15 are language/elaboration defects with their own PRs. Items #8, #9, #10, and #16 are observations rather than Prologos defects; no compiler change is needed for them but the memo deserves a parallel disposition note so a future reader does not double-count them as open work. #8 (exact-Rat slow on deep iter): intrinsic to exact rational arithmetic; benchmark-scope guidance, not a fix. #9 (Posit32 literals work): positive observation; `~` literal prefix is unambiguous unlike `0/1`. No action. #10 (PVec preserves where List does not): subsumed by pitfall #3 fix. After #3 lands, both literal forms preserve element type uniformly. Close as duplicate. #16 (column-stochastic vs row-stochastic): algorithm/spec clarification, not a Prologos defect. The eigentrust implementation branch already takes column-stochastic M directly and validates via col-stochastic?. https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>

…-rl3z parser: preserve Rat-ness of slash-containing number literals (eigentrust pitfall #3)

Per user review of #0-#10: many entries were either out-of-scope (env limitations, not Prologos issues) or wrong (claims I never actually tested). Re-tested every claim against a real Racket and revised the doc. Numbers are reserved per the user's instruction — entries marked DELETED keep their slot so cross-refs don't drift. Detail: #0 DELETED — out-of-scope (Racket toolchain not in sandbox). Environment limitation, not a Prologos issue. #1 REFRAMED — was "capability subtype + promise resolution composition." Re-titled to honestly reflect what this actually is: an OCapN-side Phase 0 deferred-implementation note (eventual cross-vat receive isn't wired up yet). NOT a Prologos bug. #2 DELETED — false claim. Tested with a real Racket: WS-mode wildcard match `match | _ -> body` on user data types elaborates AND evaluates correctly when the function carries a proper `spec`. The `prologos::data::datum` comment I cited applies to a narrower polymorphic-context case, not a blanket wildcard ban as I asserted. Cleanup of behavior.prologos (~250 -> ~70 LOC) follows. #3 DELETED — false claim. Tested: `data Step step : [Nat -> Nat]` (with bracketed function type per the lseq-cell convention) accepts a function value, including closures with captured state. Open-world actor behaviour storage IS supported. The closed-enum BehaviorTag in our implementation was a needless workaround driven by this incorrect pitfall. Cleanup tracked separately. #4 KEPT, REFRAMED — real, narrowed claim. grammar.ebnf §6 lines 1153/1187/1199 promise `Mu` (sexp) and `rec` (WS) for recursive sessions. Both elaborate to `Unknown session type: rec` / `Mu`. So pitfall #4 is now: "rec/Mu in grammar but not in elaborator." CapTP's stream-level well-typedness is therefore the documented ceiling; per-exchange sub-protocols remain the workaround. #5 KEPT — `none`/`some` need explicit type args in some inference contexts. Real ergonomics tension, accurately documented. #6 DELETED — out-of-scope. WS-mode `let p := body` and sexp-mode `(let (p v) body)` are TWO surface forms by design (grammar.ebnf §7 line 1236). User-error, not a Prologos bug. #7 DELETED — was a quantitative restatement of #2. With #2 recanted, #7 evaporates: behavior modules can be wildcard-collapsed, dropping ~180 LOC. #8 DELETED — false claim. Tested: `data Box1 box1 : [Sigma [_ <Nat>] Bool]` and `data Table table : Nat -> [List [Sigma [_ <Nat>] Bool]]` both elaborate cleanly. The named-struct ActorEntry/PromiseEntry workaround in vat.prologos was unnecessary; can be simplified back. #9 DELETED — user error. `def` for value bindings vs `defn` for functions is documented (grammar.ebnf §3 lines 189-190, prologos-syntax rules). Mis-using `defn` for a 0-ary constant isn't a Prologos bug. #10 DELETED — out-of-scope. Network sandbox blocking external docs is an environment limitation. #11-#20 were not in scope of this review and remain as-is for the user to review next.

The benchmark file references the pre-D.5b TMS API (`tms-write`, `tms-cell-value`, `tms-read`, `tms-commit`), which was removed when the TMS was refactored into the `tms-cell` struct + `atms-write-cell` interface. The file is a "Pre-0 micro-benchmark" (historical baseline measurements for Track 2 before it was implemented) and does not run in CI or the regression suite, but `raco pkg install --auto` compiles every .rkt in the collection, so its unbound-identifier error fails the build. Add `racket/prologos/benchmarks/micro/info.rkt` with `compile-omit-paths '("bench-bsp-le-track2.rkt")` so `raco setup` skips it. This mirrors the PR #3 fix for `bench-ppn-track3.rkt` (which migrated to the current API) but for a file whose full migration (multiple API changes) is non-trivial and out of scope for this branch. Verified locally with `raco pkg install --deps force --no-docs --link --name prologos-dev racket/prologos`: bench-bsp-le-track2 no longer appears in the summary of errors. https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp

Original PIR text claimed runtime/core/ contains the BSP scheduler. Wrong — actual runtime/core/ has only data structures (cell store + profile counters + format buffer). The BSP scheduler stayed in each kernel file (hybrid kernel's worklist + fire_against_snapshot + merge_pending_writes + swap_worklists are inlined in prologos-runtime-hybrid.zig). Stage 3 design called for core/bsp.zig (~150 LOC) + core/worklist.zig (~60 LOC) as Phase 1 deliverables. Actual Phase 1 extracted only cells.zig + profile.zig + format.zig. The factoring scope shrank silently — neither the implementing commit nor any subsequent commit acknowledged the gap. Surfaced when the user asked "what's in the hybrid core zig side?" during PIR review. Corrections: - §1 (What Was Built): explicit "data structures only" + cross-ref to wrong-assumption #9 - §2 (Stated Objectives): added "reality check on the design quote" flagging the drift - §3 delivered table: Phase 1 status changed to "✅ partial" - §4 timeline: Phase 1+3+4 line clarifies scheduler not extracted - §5 deferred: new row for BSP scheduler factoring - §8 D1 + anti-decision: caveat added; "BSP scheduler abstraction" claim corrected to "cell-store comptime-parameterization abstraction" - §9 #2: factoring narrative softened to "data structures only" - §11 #3: original kernel template + factoring made explicit at data-structure layer only - §12 #2 + #8: kernel-LOC framing corrected; "factored core LOC was bigger than expected" reframed to "smaller than expected — and the gap is the BSP scheduler" - §13 architecture: "consuming runtime/core/" framing softened to "consumes for cell store + profile + format helpers; the BSP scheduler is inlined" - §14 #3, #7, #8: "future kernels instantiate the same scheduler" claim corrected to "instantiate CellStore + reuse profile counters; each kernel still writes its own scheduler" - §15 technical debt: new row for "BSP scheduler not factored" - §17 wrong assumptions: new #9 "Phase 1 will factor the BSP scheduler into core" — Wrong; codifies the silent scope shrinkage - §18 #4: "factoring at second-instance" pattern reinforced with "complete vs minimum-viable shared surface" caveat - §21 lessons: new entry for "phase-close should compare delivered scope against design plan" - §24 open Q #4: kernel-PU consumption clarified — needs scheduler reuse in-place or triggers the extraction debt Errata block added at the top of the PIR documenting which sections were corrected and why. https://claude.ai/code/session_01Tycs6BWKG58Wo99YVPg6DF

Adds prologos::ocapn::* — a single-vat, pure-functional model of the OCapN/Goblins actor system, built entirely in Prologos with the existing capability-types and session-types primitives. Library (lib/prologos/ocapn/): - refr.prologos capability hierarchy: OCapNRefr / NearRefr FarRefr / SturdyRefr / PromiseRefr + UnresolvedPromise / ResolvedNear / Far / BrokenPromise. Subtype edges encode attenuation. - syrup.prologos abstract Syrup value model (atoms, list, tagged, refr, promise). No bytewise codec. - promise.prologos monotone promise algebra (fulfill/break + queue mechanics for pipelined messages). - message.prologos CapTP op:* values: deliver, deliver-only, listen, abort, gc-export, gc-answer, start-session. - behavior.prologos closed-enum BehaviorTag + per-tag step functions for cell, counter, greeter, echo, adder, forwarder, fulfiller. - vat.prologos local vat: spawn, send, send-only, drain + step-vat / run-vat with explicit fuel (no mutation, no threads). - captp-session.prologos five sub-protocols modelled as session types: Handshake, Deliver, Listen, DeliverOnly, Gc — with `dual` for the responder side and example defproc clients. - core.prologos public API re-exports + Goblins-flavoured aliases (spawn-actor / ask / tell / drain). Tests (tests/test-ocapn-*.rkt, 8 files): refr / syrup / promise / message / behavior / vat / pipeline / captp / e2e — exercise per-module unit semantics and the full actor-system round-trip. Acceptance file: examples/2026-04-27-ocapn-acceptance.prologos Pitfalls catalogue: docs/tracking/2026-04-27_GOBLIN_PITFALLS.md — ten language / ergonomics issues encountered during the port. Open the file for the next port to start with eyes open. Headline issues: closed-world data wildcard match (#2), no first-class actor closures (#3), no recursive session types (#4), sandbox couldn't exercise the suite (#0). Constraints followed: - No new Racket FFI introduced; everything in Prologos source - Only stdlib imports (data::list, data::option, data::nat, data::string, data::bool) - Capability types declare the refr authority lattice - Session types declare each CapTP wire sub-protocol Status: implementation is static-syntax-clean by inspection; not run on a real Racket toolchain in this environment. Pitfall #0 documents the verification gap.

Per user review of #0-#10: many entries were either out-of-scope (env limitations, not Prologos issues) or wrong (claims I never actually tested). Re-tested every claim against a real Racket and revised the doc. Numbers are reserved per the user's instruction — entries marked DELETED keep their slot so cross-refs don't drift. Detail: #0 DELETED — out-of-scope (Racket toolchain not in sandbox). Environment limitation, not a Prologos issue. #1 REFRAMED — was "capability subtype + promise resolution composition." Re-titled to honestly reflect what this actually is: an OCapN-side Phase 0 deferred-implementation note (eventual cross-vat receive isn't wired up yet). NOT a Prologos bug. #2 DELETED — false claim. Tested with a real Racket: WS-mode wildcard match `match | _ -> body` on user data types elaborates AND evaluates correctly when the function carries a proper `spec`. The `prologos::data::datum` comment I cited applies to a narrower polymorphic-context case, not a blanket wildcard ban as I asserted. Cleanup of behavior.prologos (~250 -> ~70 LOC) follows. #3 DELETED — false claim. Tested: `data Step step : [Nat -> Nat]` (with bracketed function type per the lseq-cell convention) accepts a function value, including closures with captured state. Open-world actor behaviour storage IS supported. The closed-enum BehaviorTag in our implementation was a needless workaround driven by this incorrect pitfall. Cleanup tracked separately. #4 KEPT, REFRAMED — real, narrowed claim. grammar.ebnf §6 lines 1153/1187/1199 promise `Mu` (sexp) and `rec` (WS) for recursive sessions. Both elaborate to `Unknown session type: rec` / `Mu`. So pitfall #4 is now: "rec/Mu in grammar but not in elaborator." CapTP's stream-level well-typedness is therefore the documented ceiling; per-exchange sub-protocols remain the workaround. #5 KEPT — `none`/`some` need explicit type args in some inference contexts. Real ergonomics tension, accurately documented. #6 DELETED — out-of-scope. WS-mode `let p := body` and sexp-mode `(let (p v) body)` are TWO surface forms by design (grammar.ebnf §7 line 1236). User-error, not a Prologos bug. #7 DELETED — was a quantitative restatement of #2. With #2 recanted, #7 evaporates: behavior modules can be wildcard-collapsed, dropping ~180 LOC. #8 DELETED — false claim. Tested: `data Box1 box1 : [Sigma [_ <Nat>] Bool]` and `data Table table : Nat -> [List [Sigma [_ <Nat>] Bool]]` both elaborate cleanly. The named-struct ActorEntry/PromiseEntry workaround in vat.prologos was unnecessary; can be simplified back. #9 DELETED — user error. `def` for value bindings vs `defn` for functions is documented (grammar.ebnf §3 lines 189-190, prologos-syntax rules). Mis-using `defn` for a 0-ary constant isn't a Prologos bug. #10 DELETED — out-of-scope. Network sandbox blocking external docs is an environment limitation. #11-#20 were not in scope of this review and remain as-is for the user to review next.

New file: docs/tracking/2026-05-04_PROLOGOS_LANGUAGE_PITFALLS.md Tracks bugs in the Prologos compiler stack as they surface during downstream work (running real programs through the hybrid kernel). Distinct from upstream OCapN goblin-pitfalls.md which catalogs OCapN-specific design pitfalls. Format per entry: discovered date, surfacing program, symptom, root cause hypothesis, workaround, status (🔴 open / 🟡 worked-around / 🟢 fixed), affects, path to fix. Initial entries: #1 (🟡): FQN-qualified prelude symbols (e.g. prologos::data::list::nil) not resolved by preduce.rkt's expr-fvar lookup. Affects both backends. Surfaced by ocapn-hybrid-5 + ocapn-hybrid-7. #2 (🟢): Kernel FormatBuffer 1024-byte limit silently truncated profile JSON. Fixed prior commit by bumping to 8192 bytes. #3 (🔴): Silent prelude shadowing under :refer-all produces confusing inference errors. Surfaced when ocapn-hybrid-8 called [int? a] on SyrupValue and got prologos::data::datum:: int? instead. UX issue, not correctness. #4 (🟡): Identity-bridge install sites in compile-and-bridge + dynamic-β don't pass #:native-op 'identity, missing the Phase-10-style native dispatch. Three new OCapN programs (all running on kernel): ocapn-hybrid-6: multi-arg defn (pick) matching on 2 args with one binder + one ctor pattern per arm. 16 fires, 117 µs. Result (false, true). ocapn-hybrid-7: uses prologos::ocapn::promise directly — pst-fulfilled + pst-broken predicates. 10 fires, 103 µs. (Note: works around Pitfall #1 by constructing pst-fulfilled/pst-broken directly instead of using `fresh` which depends on `nil`.) ocapn-hybrid-8: MIXED native + callback profile. int+/int* go to KERNEL-INT-ADD-TAG / KERNEL-INT-MUL-TAG (NATIVE), bool?/tagged? go through Racket callbacks. Result: **3 native fires (5.6 µs) + 6 callback fires (92 µs)** — first program where the per-tag KIND mix is visible in the kernel profile. NOTES.md test-status table extended to 8 programs (5+factorial+3 new). Average kernel time per OCapN program: 30-130 µs depending on dispatch depth. https://claude.ai/code/session_01Tycs6BWKG58Wo99YVPg6DF

Per-track LOC contribution estimates for the remaining Phase 7 migration targets, with rationale + risk weighting + prerequisite ordering. Grounded against current code-size baselines: Zig kernel: 913 LOC Racket reducer + backends + bridge: 2347 LOC Summary (track / Zig delta / Racket delta / cb-time absorbed): #5 boolrec -> kernel_select +0 +30 ~4% (free; just routing) #4 ctor-N native ABI +400 +200/-100 ~5% workload, ~50% OCapN #3 expr-reduce match dispatch +200 +200/-150 ~10% #2 expr-natrec step +150 +50/-30 ~5% effective, ~17% theoretical #1 recursive expr-fvar + expr-app +1000 +400/-200 ~60% #7 CHAMP collection ops +5000+ +500/-200 ~4% (synthetic; defer) Net if #1-#5 land: Zig +1750 LOC (~3x growth); Racket -50 LOC net. Surface complexity migrates from Racket compile-expr to Zig kernel. Three suggested orderings (A: biggest payoff first; B: incremental; C: value-engineering minimum). All start with #5 (free), all prerequisite #4 before #3. Doc identifies 5 open design questions: ctor-N ABI choice (heap-backed vs bit-packed), closure representation, tail-call semantics, eager arm compilation interaction with recursion, bot-guard convention formalization. Three things this analysis does NOT settle: - Whether #1 is feasible without losing static-beta benefits (B1/B2/H1/J1/J2 do zero runtime fires today; native apply costs more rounds). - Per-fire cost of native call apparatus (somewhere between 115ns native and 4100ns callback; not measured). - Whether #1+#2+#3 land as one track or three (architecturally coupled; landing them independently means a stub-laden middle state). https://claude.ai/code/session_01Tycs6BWKG58Wo99YVPg6DF

…ruth #3) Refactor 5 property-test functions in sre-core.rkt to take explicit join-fn parameter, mirroring Phase 3c's meet-fn discipline. Retires hardcoded 'equality lookup that was mixing lattices when meet-fn came from a non-equality relation. Functions refactored: - test-distributive (domain samples meet-fn join-fn) - test-sd-vee/detailed (domain samples meet-fn join-fn) - test-sd-wedge/detailed (domain samples meet-fn join-fn) - test-sd-vee, test-sd-wedge wrappers (thread join-fn) Callsites updated atomically across: - sre-core.rkt: infer-domain-properties + resolve-and-report-properties (look up join-fn via merge-registry per #:relation) - sre-property-sweep.rkt: run-sd-sweep (per-relation join lookup) - tests/test-sre-algebraic.rkt: 11 callsites (Phase 1+2 tests) - tests/test-sre-sd-properties.rkt: memq → check-not-false hygiene Targeted suite GREEN: 106 tests / 4.3s across test-sre-algebraic + test-sre-track2h + test-sre-sd-properties. Wider-sample sweep run (depth-1 with binders, 58 samples) produced honest data: - Both relations CONFIRM distributive at depth-0 (ground sublattice; matches Phase 3c hand-picked-6 + Track 2H decl) - Both relations REFUTE distributive at depth-1 with binders (witness: Pi-typed triple). Empirical confirmation of Track 2H F7 scope conjecture. - Both relations confirm SD-vee + SD-wedge with asymmetric non-vacuity (3.5% vs 91.4%) — type lattice is SD on full domain, distributive on ground sublattice only. Pattern: 3rd Scaffolding-Hides-Truth data point. Track 2H's quantale framing remains intact; the registration declaration at unify.rkt:96 ('distributive prop-confirmed) is over-broad relative to design body's F7 scope qualifier — Discussion-phase concern, NOT Phase 4 commit-blocker. Design doc tracker updated; dailies entry captures the arc + bonus findings + lessons distilled. Findings table commits in Phase 3 close (separate commit).

…ant rewrite (A: round-entry batch / B: local-var per-fire) User challenged my "Q-M deferred to Phase 2 PAR" framing: "Our current BSP scheduler IS the parallel BSP from PAR research (PAR essentially closed for now). Is that not so?" Audit confirmed user is right; this commit corrects the design doc. ## Audit findings (verified in code) - driver.rkt:435 sets `current-parallel-executor` globally to `(make-parallel-thread-fire-all)` — parallel BSP IS production default - PAR Track 2 R1-R2 closed with BSP-as-production-default; 4.45× speedup - Codebase has FIVE scheduler entry points, each with different loop structure + different fuel-decrement pattern: 1. run-to-quiescence-inner (sequential Gauss-Seidel; box-mutation per-fire) 2. run-to-quiescence-inner/traced (same + tracing) 3. run-to-quiescence-bsp (parallel BSP; ALREADY batch-decrement-by-N at line 2384's round-entry — production main loop) 4. run-widen-phase (sequential widening; struct-copy per-fire) 5. run-narrow-phase (sequential narrowing; struct-copy per-fire) ## The CRITICAL discovery The parallel BSP main loop (entry point #3) ALREADY does round-entry batch decrement at line 2384: ``` [fuel (- (prop-network-fuel net) n)] ``` where n = (length pids). Fuel decrements happen ON THE MAIN THREAD, sequentially, BEFORE workers spin up. Workers fire against the post-decrement snapshot but don't touch fuel. This means Phase 1C migration to D.4 + Option 13 is simpler than described: change the struct-copy field update to a cell-write at the same site. The substrate changes (struct field → cell); the concurrency pattern doesn't change. ## §10.3.A two-variant rewrite The original §10.3.A pseudocode described a single per-fire local-var pattern. The audit showed this pattern is WRONG for the parallel BSP main loop (which has no per-fire body). It's CORRECT for the sequential schedulers (#1, #2, #4, #5). Two variants: - **Variant A** (round-entry batch): parallel BSP main loop. ONE net-cell-write per BSP round, on main thread, BEFORE workers. Cost: ~6 ns/round; amortized ~0.06 ns/cycle at N=100. - **Variant B** (local-var per-fire): four sequential schedulers. Local-var box + per-fire decrement + cell-write at phase end. Cost: ~2.16 ns/cycle amortized (per §13.6.A spike). The scheduler CHOOSES the variant fitting its loop structure. Both preserve orthogonality (cell mechanism is unchanged). ## Q-M correction - Was: "DEFER-TO-PHASE-2-PAR" (incorrect framing) - Now: RESOLVED IN-SCOPE 2026-05-15 — parallel BSP main loop already serializes fuel-state updates on main thread; Phase 1C migration changes substrate but not concurrency pattern ## §9.9 open questions resolved Walkthrough of Phase 1B mini-design open questions with Option 13 + audit applied. 7 of 8 architectural questions RESOLVED: - Q-1B-8 → A2 (cell-meta on prop-cell struct; perf pressure dissolved under Option 13's boundary-only dispatch) - Q-1B-9 → F2 (predicate receives (current, new-value, net)) - Q-1B-10 → B1-prime (cell-meta + dispatch in propagator.rkt; thin specialized-cells.rkt for convenience) - Q-1B-11 → D1 (storage strategy enum: 'general + 'monotone-counter) - Q-1B-12 → E1 (fire-on enum: 'any-change + 'threshold-crossing) - Q-1B-13 → G1 (predicate runs AFTER merge) - Q-1B-14 → L1 (local-var = let-scoped ephemeral box) 3 implementation-detail questions remain deferred to code (Q-1B-1 API naming; Q-1B-2 +inf.0 vs sentinel; Q-1B-4 residuation as helper). ## Design doc updates in this commit - §10.3.A rewritten with two-variant pattern + scheduler/variant matrix; trade-offs note updated (Parallel BSP RESOLVED IN-SCOPE) - §10.4 sub-phase plan: 1C-i enumerates all 5 entry points with variant assignment; 1C-ii migrates per-variant - §10.5: D-1C-10 NEW (wrong-variant risk); D-1C-11 NEW (preserve batch semantic for parallel BSP main) - §10.7: Q-1C-M corrected from DEFER to RESOLVED IN-SCOPE; Q-1C-K/L/N added - §9.9 reorganized: 7 questions RESOLVED with specific leans; 3 deferred to code - Top-of-doc Revision Summary: audit-correction note added - DESIGN_PRINCIPLES.org § Scheduler-State Cells: deferred-write pattern rewritten with two variants + scheduler/variant assignment table ## Files in this commit - docs/tracking/2026-04-26_PPN_4C_TROPICAL_QUANTALE_ADDENDUM_DESIGN.md (§10.3.A + §10.4 + §10.5 + §10.7 + §9.9 + top-of-doc updates) - docs/tracking/principles/DESIGN_PRINCIPLES.org (§Scheduler-State Cells two-variant pattern note) - docs/tracking/standups/2026-04-26_dailies.md (walkthrough narrative + audit findings + lessons) ## Honest acknowledgment The "deferred to Phase 2 PAR" framing was lazy. PAR Track 2 R1-R2 closed; parallel BSP IS production. Phase 1B/1C must handle parallel composition NOW, not defer it. User's challenge surfaced this gap. The audit cost ~10 min of grepping + reading; it produced a substantive design correction. Pattern: external questions about production reality catch design assumptions that internal exploration misses. Phase 1B is now ready to enter Stage 4 implementation with: - All architectural decisions locked in (7 resolved questions + spike + spike-A validation) - Five-scheduler-entry-point migration plan per variant - §13.7 measurement gates at each sub-phase boundary - Codified two-variant deferred-write pattern in DESIGN_PRINCIPLES.org

…h scope 2→18) 1C-i pre-implementation audit per Per-Phase Protocol. Five findings surfaced (α/β/γ/δ/ε); user confirmed all leans; §10 doc cleanup (D-1B-iii-4 carryover) applied as 1C-i's mechanical work. Audit findings: α — Entry points #1 + #2 already have partial Variant B pattern (informational). run-to-quiescence-inner (drain at 2039) + /traced (2087) already use box-mutation + per-fire decrement + finalize flush. Migration simplifies to source/sink redirect for #1+#2; full helper introduction for #4+#5. Helpers apply uniformly. β — Tier 1 BSP fast path doesn't decrement fuel (RESOLVED β1). run-to-quiescence-bsp Tier 1 (lines 2562-2573) bypasses fuel decrement entirely (single-pass flush for deterministic cases). β1 preserves this semantic under D.4 — no net-cell-write in Tier 1; cell value unchanged after Tier 1 round. γ — run-to-quiescence-widen is a wrapper with check sites only (RESOLVED: not a 6th entry point). Line 3353 wrapper has 3 check sites (3357/3360/3367) but no decrement. Migrates under 1C-iii. δ — typing-propagators.rkt:2269 is fuel-SUBSTITUTION, not speculation rollback (RESOLVED: Q-1C-1 closes simpler). Pattern is bounded- typing-run fuel-budget-substitution. D.4 migration is 4-line cell- API substitute + restore; no helper needed. ε — Bench migration scope is 18 sites, NOT 2 (LOAD-BEARING; ε2). Q-Audit-1's "2 bench refs" only counted bench-alloc.rkt (2 sites). bench-ppn-track4c.rkt has 16 ADDITIONAL sites directly accessing prop-net-hot-fuel (Pre-0 microbench sections M7/A7). Under D.4 retirement these break at compile. Resolution ε2: 2 bench-alloc.rkt sites migrate mechanically; 16 bench-ppn-track4c.rkt sites RETIRED-PER-D.4-CANONICAL with annotations + comment-out. Historical baseline data preserved in tropical-pre0-baseline-2026-04-26.txt; new CM*+CW* benches measure the new pattern. §10 doc cleanup applied (D.4 sections only; D.3 historical RETIRED- PER-D.4-CANONICAL + §9.2.0.7 rename-history preserved): - fuel-cost-cell-id → fuel-cell-id (~10 sections) - fuel-cost-cell → fuel-cell (descriptive references) - (+ current n) → (- current n) Option A direction (§10.2 + §10.3.A Variant A/B pseudocode) - cost-framing variable names → remaining-framing (Variant B pseudo) - cost= display → remaining= display - §10.3 read-as-value, saved-fuel, pretty-print examples updated Scheduler entry point line numbers re-verified (drifted significantly since 2026-05-15 audit due to Phase 1B's prop-cell/prop-net-warm extensions + BSP scheduler refresh): - #1 run-to-quiescence-inner: 1835 → 2030 (drain at 2039) - #2 /traced: 1870 → 2087 - #3 run-to-quiescence-bsp Tier 2: 2315 → 2532; snapshot at 2606 - #4 run-widen-phase: 2989 → 3214 - #5 run-narrow-phase: 3042 → 3267 - (6) run-to-quiescence-widen (new finding): 3353 A baseline capture strategy: rely on existing Pre-0 baseline data + §13.6.A spike measurements rather than introduce new per-entry-point microbench. A = M7 24 ns/call + B.M7.2 5.7 ns/call; C = §13.6.A Variant A 0.06 ns/cycle + Variant B 2.16 ns/cycle. Design doc changes: - NEW §10.0.1 (~190 lines): 1C-i Mini-Audit Findings - §10.2 substrate plan: Option A direction + bench scope 18 sites - §10.3 per-site patterns: Option A + saved-fuel reframed - §10.3.A Variant A pseudocode: corrected direction + Tier 1 note - §10.3.A Variant B pseudocode: uses helpers + Option A direction - §10.4 1C-ii-b notes α finding; 1C-v scope expanded to 18 bench - §3 Progress Tracker: 1C-i marked ✅ Process observations (codification candidates): - Audit counts grow as implementation work proceeds (ε pattern) - Design-doc framing can be more complex than code reality (δ) - Per-phase audit discipline catches line-drift pre-implementation Suite state unchanged: 8286 tests / 127.4s / 0 failures (no code changes; pure design + doc work). Next: 1C-ii-a — Variant A migration. Replace line 2606's [fuel (- (prop-network-fuel net) n)] with net-cell-write to fuel-cell-id BEFORE workers spin up. ~5-10 LoC + 1-2 tests. Cost target ~0.06 ns/cycle amortized.

…er 2 (β1 lockstep) Production code change: propagator.rkt line 2603-2609 region. +6 LoC production + 76 LoC tests. Suite GREEN at 8289 / 126.4s / 0 failures. Implementation (Variant A; parallel BSP main loop entry point #3): After existing snapshot struct-copy (keeps [fuel (- ... n)] field update per β1 lockstep), ADD: [snapshot+fuel (net-cell-write snapshot fuel-cell-id (- (net-cell-read net fuel-cell-id) n))] Then thread snapshot+fuel through 5 downstream uses: - (executor snapshot+fuel pids) line 2612 - (bulk-merge-writes snapshot+fuel ...) lines 2624, 2626 - snapshot+fuel as if-branch return line 2625 - (net-cell-read snapshot+fuel ...) line 2682 The cell-write triggers on-write predicate (<= new 0) firing contradiction structurally if remaining-fuel hits zero. Option A semantic (cell stores REMAINING fuel; decrement by n). β1 lockstep transitional: BOTH struct field AND cell update in lockstep. Cell-value equals struct-field-value at every observation point. Acceptable transitional scaffolding ONLY because retirement obligation captured at destination sub-phase: D-1C-ii-a-1 (retirement obligation): [fuel (- ...)] struct field update at line 2606 RETIRES at 1C-iv alongside prop-net-hot-fuel field itself. Only cell-write remains as production pattern post-1C-iv. Captured in §10.4 1C-iv scope, §10.0.2 drift risk, Progress Tracker. Tests added (test-tropical-fuel.rkt, 3 new test-cases, +76 LoC): (1) cell-field-lockstep — Tier 2 BSP A→B copy; verify field = cell after round (β1 invariant) (2) Tier 1 fast path preservation — fire-once empty-inputs propagator; verify NEITHER field NOR cell changed (β1 preservation; structural) (3) exhaustion via cell-mechanism — budget=2 + 2 props; verify contradiction fires (cell on-write-check or legacy check site) Verification: - Delimiter check: balanced - raco make driver.rkt: clean - Targeted: 77 tests / 6.3s / all pass - Full suite: 8289 / 126.4s / 0 failures (+3 tests; -1.0s wall) VAG: PASS with named caveats (β1 dual update is transitional scaffolding with captured retirement; microbench verification deferred to 1C-vi A/B/C report per §13.7). Drift risks closed: - D-1C-ii-a-1: retirement obligation captured (§10.4 1C-iv + tracker) - D-1C-ii-a-2: snapshot+fuel threading verified (5 sites + suite GREEN) - D-1C-ii-a-3: (<= new 0) boundary verified by Test 3 - D-1C-ii-a-4: Tier 1 preservation verified by Test 2 Process observations: - α discussion clarified no retirement at 1C-ii-a (just diff cleanliness); user's "is this retiring something?" prevented drift in framing - β1 retirement obligation explicit capture (per user direction) prevents transitional dual-write from becoming permanent belt-and-suspenders - All 4 drift risks named at mini-design closed at implementation Next: 1C-ii-b — Variant B migration (4 sequential scheduler entry points; #1 + #2 simpler redirect per pre-existing partial Variant B; #4 + #5 full helper introduction). Cost target ~2.16 ns/cycle amortized per §13.6.A.

…context preserved Per user direction: fork back to last fork-point (75d0c47) and re-gain context from this checkpoint forward. This commit captures comprehensive session arc state in the dailies so the next session has complete re-entry pointers regardless of fork-back-and-re-execute OR fork-forward path. ## What this FORK CHECKPOINT preserves ### Session arc commits (since prior FORK CHECKPOINT 1b8e16a) 4 substantive commits: - 67448ca §10.0.7 1C-vi mini-design + mini-audit (7 resolutions; 9 audit findings; 5 drift risks; 2 NEW codification candidates) - aa0bbe4 1C-vi Commit 1 code additions (bench-tropical-fuel.rkt ~430 LoC + γ3-a/γ3-b/δ3 tests; 8299/120.9s/0 failures) - ee5010c 1C-vi Commit 2 measurement artifacts (A/B/C report ~340 lines + 3 data files + production-realistic-N + probe wall +19.2% finding + Issue #63 + multi-surface tracking; Phase 1C CLOSED) - 4061afc §7.7 1A-iii-b mini-design + mini-audit (5 resolutions + 12 audit findings incl. 2 CRITICAL inversions; 3 non-optional design doc corrections; 5 drift risks; 3 NEW codification candidates) ### Cumulative architectural state captured **Phase 1C COMPLETE**: D.4 cell-as-canonical fully realized + A/B/C report grounding production reality (Option 13 amortization is N-dependent; production median N=3 vs synthetic N=100; per-call cell-API ~450 ns dominated by 3-level nested struct-copy NOT CHAMP lookup; probe wall +19.2% at upper-ceiling of §11.3 target; GC profile intact) **Phase 1A-iii-b PRE-IMPLEMENTATION COMPLETE**: mini-design+audit done; implementation BLOCKED on 1A-iii-c (per α audit-inverted ordering); ε1 single atomic commit (~300-450 LoC pure deletion) ready **Phase 1A-iii-c**: NOT YET OPENED (next-session task) **Phase 1V**: expanded scope — item #1 (merge-fn cache) + NEW item #1-bis (fuel-cell direct-ref cache; surfaced from user question at 1C-vi Commit 1 checkpoint) + item #3 (SRE property-sweep conditional) + item #4 ✅ COMPLETED at 1C-vi **Multi-surface tracking discipline established** (per user β resolution): Issue #63 + MASTER_ROADMAP forward-refs at OE Series Track 1 + PReduce Track 4 + DEFERRED.md, all cross-referenced ### Net delta this session arc - +5 tests (8294 → 8299) - +20s wall (within S1 variance band 119.3s ± 10%) - +1 phase sub-phase complete (1C-vi closes Phase 1C) - +160 lines design doc (§7.7 + §7.8) - +5 NEW codification candidates surfaced (2 from 1C-vi + 3 from 1A-iii-b) ### Re-entry pointers (for fresh session) 5-step orientation: 1. Read this dailies in full (start from prior FORK CHECKPOINT through this) 2. Read design doc (§3 Progress Tracker + §7 + §7.7 + §7.8 + §8 + §10.0.7 + §11.3 + A/B/C report) 3. Read 1C-vi A/B/C report (docs/tracking/2026-05-16_TROPICAL_1C_VI_ABC_REPORT.md) 4. Re-execute OR fork-forward (commit replay sequence captured) 5. Verify recent commits (5 named for post-4061afcb verification) ### Pending decisions / open items - IMMEDIATE next-session task: 1A-iii-c mini-design+audit OPENING (surface ATMS AST 14-file pipeline retirement; ~600-1000 LoC; 3 open questions Q-1A-iii-c-1/2/3 from §8.6) - Audit findings inherited: test-atms.rkt OUT of 1A-iii-c scope (per F10); pretty-print.rkt:502 retires HERE; trace-serialize.rkt atms-event:* are SEPARATE struct family — preserved - Then sequence: 1A-iii-b implementation (unblocked) → Phase 1V VAG ### Suite state 8299 tests / 120.9s / 0 failures (unchanged this commit — docs-only). ## Files changed - docs/tracking/standups/2026-05-13_dailies.md: FORK CHECKPOINT entry (~170 lines) appended at end No code changes; no design doc changes (design doc + commit messages already capture state; this FORK CHECKPOINT consolidates the narrative for re-entry). No tests needed: dailies-only commit; no behavioral change.

…dit-resolved/ε1/ζ1/η1 + 8 design doc corrections Per Per-Phase Protocol steps 1+2 (co-dependent mini-design + mini-audit). 1A-iii-c is the UNBLOCKING commit for 1A-iii-b per §7.7 α1+α3 ordering. ## Five resolutions + two refinements (α/β/γ/δ/ε/ζ/η) - α1: Coordination inherited from §7.7 — 1A-iii-c lands before 1A-iii-b - β1: DELETE test-atms-integration.rkt + test-atms-types.rkt entirely (399 LoC) - γ2: Update comment text at examples/2026-03-20-punify-p3-acceptance.prologos:626 (user-confirmed lean γ2 over γ1 leave-as-is) - δ: lib/ — no action (zero callers per F15) - ε1: trace-serialize.rkt atms-event:* PRESERVE (DIFFERENT struct family per §7.7 F8 + §8.7 F12) - ζ1: Single atomic commit (~1075 LoC delta; matches §7.7 ε1 precedent; user-confirmed lean ζ1) - η1: Atomic commit contents defined (16 files; ~675 LoC mod + ~400 LoC test del); pnet-serialize/trace-serialize/typing-errors/ capability-inference/lib NO CHANGES ## 18 mini-audit findings (F1-F18; 3 notable) - F1 NEW retirement site: syntax.rkt:1135-1136 predicate composition (`(or (expr-atms-type? x) (expr-assumption-id-type? x) ...)`) — missing from original §8.2 scope - F11 NOTABLE: pnet-serialize.rkt has NO atms registrations — either intentional (atms-store wrapper is runtime-stateful, non- serializable) or original pipeline.md exhaustiveness gap. No 1A-iii-c work for pnet-serialize. - F13 CRITICAL — §8.2 scope inflation: original listed 6 dependency cleanup files (typing-errors, substitution, qtt, trait-resolution, capability-inference, union-types); audit finds only 2 have refs (union-types.rkt:67-68 + trait-resolution.rkt:93-94 = 4 lines total). typing-errors + capability-inference are FALSE POSITIVES. substitution + qtt are core pipeline (not dependency cleanup). Dependency scope corrected 6 files → 2 files. Plus F5 finding (surface forms are ALREADY thin wrappers around modern solver-state-* API — clean retirement, modern API unaffected), F12 audit-resolves Q-1A-iii-c-1 (trace-serialize preserve), F14 audit-resolves Q-1A-iii-c-2 (one comment line; γ2 cleanup), F15 audit-resolves Q-1A-iii-c-3 (zero lib/ callers), F16 zero dynamic-require/eval/macro production callers, F17 test scope smaller than §8.2 anticipated (96 + 303 = 399 LoC, not "~100 cases per file"). ## 8 design doc corrections (per §8.8; NON-OPTIONAL; audit-grounded) 1. §3 Progress Tracker: ADD row for 1A-iii-c mini-design; UPDATE 1A-iii-c row Notes 2. §8.2 Core pipeline: ADD syntax.rkt:1135-1136 (F1); refresh line numbers; note pnet-serialize NO atms (F11) 3. §8.2 Dependency cleanup: CORRECT 6 files → 2 files per F13; annotate typing-errors + capability-inference as FALSE POSITIVES 4. §8.2 Tests: APPLY §7.8 #3 correction (was declared but not applied); REMOVE test-atms.rkt from 1A-iii-c list (it's 1A-iii-b scope); update LoC counts per F17 5. §8.2 Trace/serialize: STRENGTHEN to explicit PRESERVE per ε1 6. §8.2 ADD Examples/lib subsection: γ2 + δ resolutions 7. §8.3 sub-phase plan: REPLACE 8-step plan with single atomic per ζ1+η1 8. §8.6 open questions: MARK Q-1A-iii-c-1/2/3 as ✅ RESOLVED ## 7 drift risks named (D-1A-iii-c-1 through D-1A-iii-c-7) D-1/2/3/4/5/7 RESOLVED at audit time; only D-1A-iii-c-6 (test deletion isolation issues) REMAINS AT RISK — verify shared-fixture pattern at implementation; full suite GREEN is gate. Plus 2 new drift risks surfaced: D-1A-iii-c-NEW-1 (union-types + trait-resolution silent mapping retires) and D-1A-iii-c-NEW-2 (qtt.rkt:2421-2422 subtype cases retire with structs). ## 4 NEW codification candidates (watching list) - §8.2 "dependency cleanup" scope inflation (1 data point: F13) - pnet-serialize gap intentional vs accidental (1 data point: F11) - Test-line-count overestimates in original design doc (1 data point: F17; complements 1A-iii-b F10 — potential graduation pattern) - Single-comment-mention examples don't require code migration (γ2 pattern; 1 data point: F14) ## §7.8 correction #3 verification finding Audit observation: §7.8 declared the §8.2 test-atms.rkt removal correction but the actual §8.2 text was NOT modified at commit `4061afcb`. This §8.7/§8.8 commit applies §7.8 #3 to §8.2 alongside the new corrections. Codification candidate watching: "Declaring corrections in §X.Y narrative section does not automatically apply them to the §A.B location they reference — both must be edited in the same commit." ## Pre-condition gate 1A-iii-c implementation commit unblocked at this commit. Pre-impl gate: confirm HEAD + suite GREEN; re-grep at implementation opening to verify no drift. Close gate: probe diff = 0 + full suite GREEN. ## Suite state 8299 tests / 120.9s / 0 failures (unchanged; design-doc-only commit). Next: 1A-iii-c implementation (atomic ~1075 LoC delta — the unblocking commit for 1A-iii-b atomic retirement per §7.7 ε1). Then Phase 1V atomic close (after both 1A sub-phases land).

… — 5-commit atomic close plan Per Per-Phase Protocol steps 1+2 (co-dependent mini-design + mini-audit). Phase 1V is the VISION ALIGNMENT GATE for Phase 1 — atomic closure across all 4 sub-phases (1A-iii-b + 1A-iii-c + 1B + 1C). ## Five resolutions (α/β/γ/δ/ε) - **α1**: UPDATE §11.2 VAG framing for D.4 CANONICAL BEFORE applying VAG (D.3 hybrid framing preserved at bottom as "§11.2 (D.3 historical)" for traceability). User-confirmed. - **β2**: REPLACE 3 obsolete microbenches with references to existing post-D.4 measurements (M7 struct-copy / M8 inline check / M13 prop-network-fuel macro retired under D.4). 5 NEW runs (A7.1/A7.2/ A7.3 + A9 + E8) + 6 references (M10/M11/M12 from 1B-iii; R4 + E7 from 1C-vi; §13.6 W1-W5 spike; §13.6.A Option 13 spike; 1C-vi A/B/C report). Total: 11 verifications. User-confirmed. - **γ-all3**: All 3 Items (#1 merge-fn-caching, #1-bis fuel-cell direct- ref caching, #3 SRE property-sweep) IN SCOPE for Phase 1V. User confirmed Track 2I is CLOSED AND COMPLETE (vs MASTER_ROADMAP.org's stale 🔄 marker) → Item #3 unblocked. User-confirmed. - **δ1**: Graduate 3 codifications to DEVELOPMENT_LESSONS.org at Phase 1V close: 1. Audit-driven scope refinements propagate into §10.4 estimates (5 data points; READY) 2. Transitional dual-write/substitution patterns require explicit retirement obligation (5 data points; READY) 3. Audit narrative-vs-pipeline.md function-coverage exhaustiveness gap (3 data points; PROPHYLACTIC validation strong) User-confirmed. - **ε-multi**: 5-commit Phase 1V atomic close (this Commit 1 mini- design persistence + Commits 2/3/4 sub-phase items + Commit 5 atomic VAG+close). Matches Per-Phase Protocol pattern from prior sub-phases. User-confirmed. ## 16 mini-audit findings (F1-F16; 3 notable) - **F5 ⚠️ §11.2 VAG framing OUT OF DATE**: catalogue sections reference D.3 hybrid pivot framing (struct-field, macro, M7/M8/M13). Under D.4 CANONICAL these are RETIRED. Reframed in this commit. - **F6 ⚠️ §11.3 microbench list partially obsolete**: 3 of 11 measure RETIRED patterns. Replaced with references to existing post-D.4 measurements per β2. - **F12 ✅ Track 2I USER UPDATE**: confirmed CLOSED AND COMPLETE despite MASTER_ROADMAP.org showing 🔄. Item #3 (SRE property-sweep) now unblocked for Phase 1V Commit 4. ## §11.2 reframed for D.4 CANONICAL All 4 VAG questions (a/b/c/d) reframed with: - Catalogue: D.4 CANONICAL reality (cell IS live state; modern solver- context sole substrate; ~2649 LoC removed across Phase 1A) - Challenge: post-D.4 correctness criteria (Option 13 amortization; scaffolding-hides-truth pattern absence; §7.9 prophylactic audit validation; production-realistic-N findings) D.3 hybrid framing preserved at bottom of §11.2 as "§11.2 (D.3 historical)" for traceability. ## 5-commit Phase 1V plan | Commit | Scope | |---|---| | Commit 1 (this) | §11.X mini-design + audit + §11.2 reframing + §3 tracker + dailies | | Commit 2 | Item #1 merge-fn-caching (~10-20 LoC); re-microbench CW3 | | Commit 3 | Item #1-bis fuel-cell direct-ref caching (~30-60 LoC); re-microbench amortized | | Commit 4 | Item #3 SRE property-sweep wiring + verification (mini-design at opening) | | Commit 5 | Atomic VAG + 5 NEW microbench runs + 3 codifications graduation + probe diff = 0 + suite GREEN + Phase 1V ✅ + Phase 1 close | ## 6 drift risks (5 audit-resolved + 1 deferred) - D-1V-1 (VAG framing rot) ✅ α1 - D-1V-2 (obsolete microbenches) ✅ β2 - D-1V-3 (sub-phase scope) ✅ γ-all3 (Track 2I closed per user) - D-1V-4 (codifications count) ✅ δ1 (3 graduations) - D-1V-5 (probe diff verification) ⬜ DEFERRED to Commit 5 - D-1V-6 (PIR scheduling) ⬜ DEFERRED to user (PIR likely; user will call explicitly per Q-1V-η) ## 3 NEW codification candidates surfaced - §11.X-style mini-design opening for Phase V (VAG closure follows Per-Phase Protocol like implementation sub-phases) - Multi-commit Phase V close (vs single atomic) — pattern for future Phase V closures with sub-phase items - Track 2I status update vs MASTER_ROADMAP marker staleness — user- confirmed despite stale 🔄 ## Suite state 8209 tests / 98.4s / 0 failures (unchanged; design-doc-only commit). Pre-Commit-2 gate satisfied: HEAD `53aa14ad` + this commit's mini- design persistence unblocks Item #1 implementation. Next: Phase 1V Commit 2 (Item #1 merge-fn-caching).

…7.6% cumulative) Cache fuel-cost-cell prop-cell direct-ref as 4th field on prop-net-warm, bypassing cells-map CHAMP traversal for fuel-cell-id specifically. Per §11.X.3 α1/β1/γ-combined/δ1/ε1 + §11.X.3.1 audit extension (D-1V-3-3 + D-1V-3-5 audit-resolved; WT-8 added). Precedent: 1B-ii `under-speculation?` cache. Implementation (~185 LoC across 2 files; 16-step plan + WT-8): - propagator.rkt:396 — add fuel-cell-cache 4th field - propagator.rkt:758-830 — make-prop-network: 4th constructor arg + cache lookup post fuel-cell registration - propagator.rkt:851-876 — fork-prop-network: 4th constructor arg + cache lookup post net-cell-reset - propagator.rkt:1150 — net-cell-read short-circuit (eq?+and form; falls back to champ-lookup if cache is #f or cid != fuel-cell-id) - propagator.rkt:1404 — net-cell-write short-circuit (same pattern) - propagator.rkt:1488 + 1512 — WT-1a + WT-1b: fast-path 2 struct-copies - propagator.rkt:1614 — WT-2: slow-path main struct-copy (per F14) - propagator.rkt:1371 — WT-3: net-cell-reset (WT-5 + WT-7 inherit) - propagator.rkt:3389 — WT-4: net-cell-write-widen (defensive) - propagator.rkt:1419 + 1436 — WT-6a + WT-6b: dependents updates - propagator.rkt:1650 — WT-8: net-cell-replace (defensive per §11.X.3.1 F15) - tests/test-specialized-cells.rkt — +5 cache consistency tests (10-14): cache initialized at make-prop-network; updates through net-cell-write; updates through net-cell-reset; unchanged when writes target other cells; fork-prop-network initializes fresh cache Verification: - check-parens ✓ all balanced - raco make driver.rkt ✓ PASS (3-arg → 4-arg arity transition clean) - raco test test-specialized-cells.rkt ✓ 14 tests passed (was 9; +5 new) - Targeted (specialized-cells + tropical-fuel + propagator-bsp) ✓ 67 tests / all pass - Full suite (--force-rerun) ✓ 8209 tests / 96.2s / 0 failures (notably faster than baseline 118.4s; warm-cache + optimization- compounded across elaboration; within §11.3 118-127s variance band) CW3 re-microbench REMARKABLE results: | Variant + N | Pre-Item-#1 | Post-Item-#1 | Post-#1+#1-bis | Cumulative Δ | |-----------------------|-------------|--------------|----------------|--------------| | Var-A N=100 (gate) | 7.56 | 5.78 | 3.96 | -3.60 -47.6% | | Var-A N=1000 | 1.80 | 1.64 | 1.32 | -0.48 -26.7% | | Var-B N=100 (seq) | 7.78 | 7.24 | 4.92 | -2.86 -36.8% | | Var-B N=1000 | 3.04 | 2.94 | 2.62 | -0.42 -13.8% | Item #1-bis ISOLATED contribution at Var-A N=100: **-1.82 ns (~6× projected 0.3 ns/cycle savings)**. The §11.3 projection accounted for write-side savings only; the READ-side optimization (BSP convergence check at propagator.rkt:2670 fires every iteration) was unmodeled. Auxiliary dramatic improvements: - C-M13 cell-read per-call: 74.3 → 10.9 ns/call (-85.3%) - C-M8 check-site per-call: 76.9 → 10.7 ns/call (-86.1%) - C-M7 cell-write per-call: 416.0 → 275.4 ns/call (-33.8%) - GC at 100k decrements: 0 major-GC UNCHANGED (R3 baseline preserved) §13.7 GATE DECISION: - Var-A N=100 = 3.96 ns/cycle lands in "measurement-driven discussion" range (3.5-4 ns; §13.7 codification — NOT unilateral) - §13.7 ≤ 5 ns unilateral revision target: ✓ MET - §13.7 ≤ 3 ns original target: NOT MET (close; 0.96 ns short) - Option (d) Item #1-ter trigger threshold: 5 ns - **Item #1-ter NOT TRIGGERED** (3.96 < 5) - Proceed to Commit 4 (Item #3 SRE property-sweep) per ε-multi §13.7 sub-question (user discussion deferred per measurement-driven discipline): - Option A: Accept ≤ 5 ns unilateral revision as official gate - Option B: Further optimization toward ≤ 3 ns (Item #1-ter candidates 1+2 — but partially OUT-OF-SCOPE for Phase 1V) - Option C: Re-calibrate gate to ~4 ns based on production overhead breakdown (MOCK 2.16 ns + production CHAMP dispatch 1.8 ns ≈ 4 ns structural floor) Drift risk status: - D-1V-3-1/2/3/4/5/6 ✅ RESOLVED (via WT-* enumeration + tests + full suite) - D-1V-2-3 (from Item #1) ✅ PARTIALLY RESOLVED (≤ 5 ns met; ≤ 3 ns close but not met; user discussion pending) 3 NEW codification candidates: - Item #N-bis dramatically exceeds projected savings when caching well-known hot reads (1 data point: Item #1-bis 6× exceeded — projection should model both read+write side savings) - Production-realistic-N optimization concentrates savings at low N (1 data point: 6× savings at N=100 vs ~1× at N=1000) - 3.5-4 ns measurement-driven discussion range as honest gate-decision protocol (1 data point: this 3.96 ns triggers §13.7 user discussion vs unilateral) Design doc updates: - §11.X.3.2 NEW (Implementation Results + §13.7 Gate Analysis): 4-table measurement summary; auxiliary metrics; §13.7 decision tree analysis with options A/B/C; drift risk final status; VAG TWO-COLUMN; 3 NEW codifications - §3 Progress Tracker: "1V Commit 3 — Item #1-bis" → ✅ ✓ GATE-MET; "~~1V Commit 3.5 — Item #1-ter~~" → NOT TRIGGERED - docs/tracking/standups/2026-05-13_dailies.md: NEW implementation entry Per Stage 4 Per-Phase Protocol step 5 + 7 (VAG + phase completion). Mini-design persisted at §11.X.3 (commit b138bca); pre-impl audit extension at §11.X.3.1 (commit 95ad262); implementation here per prior split pattern. Next: user discussion on §13.7 gate decision (Option A/B/C) + Commit 4 mini-design opening (Item #3 SRE property-sweep per Track 2I closure).

…codifications graduated Per user direction post Phase 1V Commit 3b: persist Option C gate re-calibration; promote 3 codifications concisely. Option C: re-calibrate §13.7 1B-ii gate to ~4 ns/cycle at Var-A N=100 based on measured production CHAMP-dispatch structural floor. Supersedes both the original ≤ 3 ns target (MOCK-based) AND the 1B-iv unilateral revision ≤ 5 ns target (had margin but only empirically grounded in merge-fn correctness discovery). Production overhead breakdown: - §13.6.A MOCK floor: 2.16 ns/cycle (CHAMP-free dispatch) - Production CHAMP cell-meta dispatch: ~0.8 ns/cycle (Item #1 cached) - Production CHAMP cells-map traversal: ~0.8 ns/cycle (Item #1-bis cached) - Tagged-cell-value + worldview-cache (under speculation): ~0.2 ns/cycle - Total structural floor: ~4.0 ns/cycle (matches measured 3.96) 3 codifications graduated: 1. DEVELOPMENT_LESSONS.org "Cache Projection Should Model Read-Side + Write-Side Independently" — methodology lesson. Origin: PPN 4C 1V-3 Item #1-bis projected ~0.3 ns/cycle savings; actual ~1.82 ns/cycle (~6×) because read-side savings (BSP convergence check every iter) were unmodeled. The discipline: enumerate read vs write access patterns separately; project savings independently per side; verify with auxiliary per-call measurements alongside amortized cycle cost. 2. DEVELOPMENT_LESSONS.org "Cache Write-Through With Persistent CHAMP: Explicit Audit List IS the Drift Mitigation" — discipline for any struct-field cache mirroring CHAMP entries. Origin: PPN 4C 1V-3 Item #1-bis WT-1..WT-8 enumeration (8 explicit + 2 inherited via delegation). The pattern: enumerate all mutation sites; classify as EXPLICIT or INHERITED; add inline conditional update at explicit sites; verify with cache consistency tests. The audit list IS the implementation checklist. 3. DESIGN_PRINCIPLES.org "Specialized Cell Type Framework as Cross-Track Template" — architectural principle. Three layers: cell-meta declarations + well-known direct-refs on prop-net-warm + write-through discipline. Cross-track applicability: PReduce (e-class cell substrate), PM 12 (parameters → cells; hot module-load cells), OE Series (cost- bounded weighted parsing), SH Series (native LLVM substrate). Honors Cell/Propagator/Scheduler Orthogonality + persistent CHAMP source-of- truth + multi-dimensional cost extension forward-compat. Codified as top-level principle (not watching list) per user-noted precedent value: "The architectural demonstration of both a scheduler/ compiler specialized cell will be good precedent not only for PReduce, but also PM 12 and others; the tropical algebraic structure serves well as a first test for us to extend towards a multi-dimensional cost optimization for future tracks." Revised Phase 1V commit plan (per user direction 2026-05-17): - Commits 1-3 (done): mini-design + Item #1 + Item #1-bis (✅) - Commit 4 (THIS): Option C + codifications - Commit 5 (a+b): Item #1-quater worldview-cache caching (NEW; user-added) - Commit 6 (a+b): F14 retirement (NEW; user-added; architectural cleanup) - Commit 7 (a+b): Item #3 SRE property-sweep (was "Commit 4") - Commit 8: Atomic VAG + close (was "Commit 5") Total: 8 substantive commits + sub-commits per Per-Phase Protocol split. Suite state unchanged (8209 / 96.2s / 0 failures; docs-only commit). Files modified: - docs/tracking/2026-04-26_PPN_4C_TROPICAL_QUANTALE_ADDENDUM_DESIGN.md - §13.7.A NEW (Option C gate re-calibration) - §3 Progress Tracker: NEW row "1V Commit 4 — Option C + codifications"; NEW rows for Items #1-quater (worldview-cache) + F14 retirement; renumbered Item #3 + atomic close to Commits 7 + 8 - docs/tracking/principles/DEVELOPMENT_LESSONS.org - +2 lessons (cache projection methodology; cache write-through discipline) - docs/tracking/principles/DESIGN_PRINCIPLES.org - +1 principle (specialized cell type framework as cross-track template) - docs/tracking/standups/2026-05-13_dailies.md - NEW entry: Option C + codifications graduation Next: Item #1-quater (worldview-cache caching) mini-design + audit; then implementation; then F14 retirement.

…WARD-INVESTMENT; pattern reuse claim validated) Cache worldview-cache-cell (cell-id 1) prop-cell direct-ref as 5th field on prop-net-warm, mirroring the fuel-cell-cache pattern from Item #1-bis. Second instance of the "well-known direct-ref cache on prop-net-warm" pattern codified at Commit 4 as the "Specialized Cell Type Framework as Cross-Track Template" principle. This is the IN-TRACK validation that the codified pattern reuses cleanly. Implementation (~150 LoC across 2 files; γ-B Approach per §11.X.4): - propagator.rkt:403 — add worldview-cache-cache 5th field - propagator.rkt:758-780 — make-prop-network: 5-arg constructor + cache lookup post worldview-cache-cell registration (unified with fuel- cell-cache lookup at end of make-prop-network) - propagator.rkt:851-866 — fork-prop-network: 5-arg constructor + cache lookup post-fork (unified; cache shared with parent via structural sharing of cells map) - propagator.rkt:1196, 1455, 1255 — short-circuits at net-cell-read + net-cell-write + net-cell-read-raw (eq?+and pattern; falls back to champ-lookup if cid is neither well-known) - propagator.rkt:1223-1226, 1607-1610, 3428-3431 — replace 3 inline champ-lookups in tagged-cell-value branches with direct cache access; defensive (if wv-cell ...) check per D-1V-4-3 mitigation - 8 WT-* sites: parallel worldview-cache-cache conditional update alongside fuel-cell-cache (16 total: 2 caches × 8 sites) - tests/test-specialized-cells.rkt — +4 tests (Test 15-18): initialized at make; updates through net-cell-write; both caches coexist independently; fork preserves cache Verification: - check-parens ✓ all balanced - raco make driver.rkt ✓ PASS (4-arg → 5-arg arity transition clean) - raco test test-specialized-cells.rkt ✓ 18 tests passed (was 14) - Targeted (5 files: specialized-cells + tropical-fuel + propagator-bsp + elaboration-parity + solver-context) ✓ 113 tests / all PASS - Full suite ✓ 8213 tests / 97.2s / all pass CW3 re-microbench at Var-A N=100: 3.96 → 3.94 ns/cycle (~flat). This is EXPECTED and honest: the current bench exercises Option 13 deferred- write on the fuel cell which holds plain numbers (not tagged-cell-value). Item #1-quater's optimization targets are the 3 inline champ-lookup sites inside tagged-cell-value branches, which fire ONLY under speculation worldviews. The bench doesn't simulate speculation. Where Item #1-quater's wins LAND (forward-investments): - Phase 3A union-type ATMS branching (speculation-heavy paths) - Phase 3C consumer paths under speculation (UC1/UC2/UC3) - Operational paths in elab-speculation-bridge + atms.rkt (non-hot) The optimization IS valuable; the measurement is silent because the current bench doesn't exercise the targeted code paths. New codification candidate: "Forward-investment optimization at speculation paths" — when an optimization targets a code path the current bench doesn't exercise, document explicitly so future maintainers don't conclude "no measured benefit = unnecessary." PATTERN REUSE CLAIM VALIDATED: The codification "Specialized Cell Type Framework as Cross-Track Template" from Commit 4 (90c271f) predicted that the well-known direct-ref cache pattern would reuse cleanly. Item #1-quater is the IN-TRACK validation: - 0 implementation surprises beyond audit (F1-F9 covered all sites) - Same struct field shape (5th field; parallel to fuel-cell-cache) - Same WT-* enumeration (8 explicit + 2 inherited) - Same eq?-short-circuit pattern - Same defensive #f-check (per D-1V-4-3) The framework genuinely generalizes — empirically grounded (1 codification claim + 1 in-track validation = strong evidence for future-track adoption: PReduce, PM 12, OE, SH Series). VAG TWO-COLUMN: (a) On-network ✓ — 5th cache on prop-net-warm; scheduler-agnostic (b) Complete ✓ — 19 steps; 4 new tests + 113 targeted + 8213 full suite (c) Vision-advancing ✓ — Codification claim validated in-track (d) Drift-risks-cleared ✓ — D-1V-4-1/2/3/4/5 all resolved 2 NEW codification candidates: - Forward-investment optimization at speculation paths (1 data point) - Codified pattern reuses cleanly in-track (1 data point; methodology validation) Design doc updates: - §11.X.4.1 NEW (Implementation Results + pattern reuse validation + measurement gap discussion) - §3 Progress Tracker: "1V Commit 5 — Item #1-quater" → ✅ ✓ FORWARD-INVESTMENT with measurement summary Suite + measurement state at this commit: - Tests: 8213 / 97.2s / 0 failures - CW3 Var-A N=100: 3.94 ns/cycle (~flat from 3.96) - GC: 0 major-GC at 100k decrements Per Stage 4 Per-Phase Protocol step 5 + 7. Mini-design persisted at §11.X.4 (commit 48b3993); implementation here per prior split pattern. Next: F14 retirement (tropical-fuel-merge-for-cell inlined-duplicate removal) per Commit 6; then Commit 7 (Item #3 SRE property-sweep); then Commit 8 atomic VAG + Phase 1 close.

…licate) Architectural cleanup: retire the inlined-duplicate `tropical-fuel-merge-for-cell` at propagator.rkt:675 by breaking the import cycle structurally. Before: propagator.rkt → (would-cycle via) tropical-fuel.rkt → sre-core.rkt → propagator.rkt After: propagator.rkt → tropical-fuel-primitives.rkt (leaf; only racket/base) tropical-fuel.rkt → tropical-fuel-primitives.rkt + sre-core.rkt (re-exports primitives for backward compat; retains SRE/merge-fn registration) Implementation (per §11.X.5 8-step plan): - NEW racket/prologos/tropical-fuel-primitives.rkt (~100 LoC): pure algebraic primitives extracted from tropical-fuel.rkt (bot/top/contradiction?/merge/meet/tensor/left-residual). Zero non-Racket deps; leaf module; cycle-safe. - racket/prologos/tropical-fuel.rkt refactor: require + re-export primitives from leaf module; retain SRE domain registration + merge-fn-registry registration. ~75 LoC net reduction (primitive defs moved out). - racket/prologos/propagator.rkt: add require for tropical-fuel-primitives.rkt; delete inline duplicate `tropical-fuel-merge-for-cell` + 9-line comment block; replace 2 use-sites with `tropical-fuel-merge` at propagator.rkt:819, 832. Two-layer separation aligns with tropical-fuel.rkt's stated design intent (preamble lines 28-31): primitives module = pure algebra; tropical-fuel.rkt = SRE-integration. The split is cleaner separation of concerns. Verification: - check-parens ✓ all 3 files balanced - raco make ✓ clean build (tropical-fuel-primitives.rkt → tropical- fuel.rkt → driver.rkt; cycle broken; module load order correct) - raco test test-specialized-cells + test-tropical-fuel ✓ 58 tests pass (backward compat preserved via re-export from tropical-fuel.rkt) - Full suite ✓ 8218 tests / 98.6s / all pass VAG TWO-COLUMN: (a) On-network ✓ — no on-network change; module structure cleanup (b) Complete ✓ — 8-step plan executed; suite GREEN; backward compat (c) Vision-advancing ✓ — architecturally cleaner two-layer separation; precedent for future tracks facing similar cycles (d) Drift-risks-cleared ✓ — D-1V-5-1/2/3 all resolved: - D-1V-5-1: re-export preserves backward compat for existing imports of `tropical-fuel-merge` from `tropical-fuel.rkt` - D-1V-5-2: new file name `tropical-fuel-primitives.rkt` unused - D-1V-5-3: raco make clean confirms module load order correct (primitives loads as leaf; tropical-fuel.rkt loads next; etc.) Codification candidate (per §11.X.5 NEW): "Two-layer module split for cycle-breaking" — when an algebraic primitive needs to be referenced from both the network layer AND from SRE-integration modules, extract to a leaf module (zero non-Racket deps). Network layer requires primitive directly; SRE-integration layer requires primitive + re-exports for backward compat. Useful pattern for future tracks (PReduce, OE, PM 12) that may face similar cycles. Suite state at this commit: - Tests: 8218 / 98.6s / 0 failures (test count varies slightly with cache state; all-pass is the load-bearing signal) - No CW3 re-microbench (no perf-affecting change) Design doc updates: - §3 Progress Tracker: "1V Commit 6 — F14 retirement" → ✅ ✓ COMPLETE with measurement summary - §11.X.5 (mini-design from prior commit 252f8c8) finalized Per Stage 4 Per-Phase Protocol step 5 + 7. Mini-design persisted at §11.X.5 (commit 252f8c8); implementation here per prior split pattern. Next: Commit 7 (Item #3 SRE property-sweep verification — Track 2I `all-sweep-properties` wiring to tropical-fuel domain); then Commit 8 atomic VAG + Phase 1 close.

…Commit-6b) Consolidating dailies entry for fork-forward continuity. Captures the cumulative state after this session arc's 10 commits + 3 codifications graduated. Captures architectural reflections that crystallized as the session progressed beyond what any individual commit message captured. Six sections: 1. State snapshot: 10 commits this session arc; HEAD `b1b5b9ce`; suite 8218/98.6s; net architectural deltas vs FORK CHECKPOINT (struct evolution; 3 well-known direct-ref caches; §13.7 ~4 ns gate; CW3 -47.9% cumulative; cell-read -85%) 2. Architectural reflections: 5 observations crystallized this session: - Well-known direct-ref cache pattern firmly established (3 instances) - Cell-read fast path is the unsung hero (auxiliary -85% measurement reveals what amortized cycle dilutes) - Full suite at 96-99s vs 119s baseline is partly the optimization compounded across thousands of cell reads per elaboration - Two-layer module-split for cycle-breaking is now precedent - Forward-investment optimization at speculation paths is a real methodology shape (Item #1-quater) 3. Codification candidate inventory: 3 GRADUATED (Commit 4); 2 STRONG watching-list (F18, 3.5-4 ns gate range); 14+ WATCHING-list (1 data point each); note that "Existing cache field as precedent" reached 3 instances but was absorbed by the umbrella DESIGN_PRINCIPLES "Specialized Cell Type Framework as Cross-Track Template" 4. Commit 7 (Item #3 SRE property-sweep) scope preview: goal = wire Track 2I `all-sweep-properties` to tropical-fuel domain; verify 11 declared quantale properties empirically against generated samples; ~50-150 LoC depending on Track 2I infrastructure shape 5. Commit 8 (atomic VAG + Phase 1 close) gate criteria preview: 4 VAG questions (already reframed for D.4 CANONICAL at Commit 1); probe diff = 0 vs Pre-0 S4 baseline (28 commands); parity tests GREEN; 3 codifications graduated (✓ Commit 4); cross-reference capture in D.3 Phase 3 Form C; 5 NEW microbench runs + 6 references to existing 6. Open considerations for next session: - Item #3 mini-audit unknowns (Track 2I infrastructure shape) - Probe baseline verification (28 commands semantic-equal) - Parity test identification + verification - Form C cross-reference capture in parent track D.3 Phase 3 - Promotion candidate "Existing cache field as precedent" (3 data points but umbrella absorbed) - PIR scope question (Phase 1 unit vs entire tropical addendum) - Post-Phase-1V trajectory (Phase 1E + Phase 2 + Phase 3A/B/C + PReduce Track 1 + OE Series Track 0) Concise wisdom for future-self captured at end: - Codification at Commit 4 PREDICTED Item #1-quater's behavior at Commit 5; prediction held; future tracks have empirical proof - Auxiliary metrics > amortized cycle for understanding optimization impact; report both - When measurement is silent (bench doesn't exercise the path), the optimization is still valuable — bench-coverage problem, not optimization-value problem - Two-layer module-split for cycle-breaking is reusable - §13.7 measurement-driven gate decision protocol is honest engineering; Option C ratification when MOCK-based target meets production CHAMP structural floor is the right answer Re-entry pointers for fork-forward session listed at bottom: 6 steps (read dailies first; design doc §3 + §11.X + §13.7.A; principles updates; verify state at b1b5b9c; Commit 7; Commit 8). This is a docs-only commit (capturing wisdom; no code changes); suite unchanged at 8218/98.6s.

…SRE property-sweep verification Per Stage 4 Per-Phase Protocol steps 1+2 (co-dependent mini-design + mini-audit) for 1V Commit 7 (Item #3 SRE property-sweep verification for the tropical-fuel domain). Persists into design doc per user direction (Stage 4 methodology mandate; matches §11.X.2/3/4/5 pattern). §11.X.6 NEW subsection (+113 lines in design doc): 5 resolutions (α1/β1/γ1/δ1/ε1): α1 — atom selection: '(1 5 10 100 1000) + bot (0) + top (+inf.0) via include-bot-top?=#t → 7 atoms at depth-0 β1 — sweep wiring: NEW entry in tools/run-phase9-sweep.rkt sweep-config for 'tropical-fuel (relations '(equality), no cross-domain ctors, include-bot-top #t) γ1 — test wiring: EXTEND tests/test-sre-sd-properties.rkt with tropical-fuel section (not new file; shared-fixture pattern preserved at depth-0 for ~5s wall budget) δ1 — assertion scope: assert ONLY on 3 DECLARED-AND-SWEPT properties (distributive + has-pseudo-complement-rel + has-pseudo-complement-abs); 14 BONUS swept properties captured as design-doc artifact (no assertions) — honest separation ε1 — atomicity: single mini-design commit (THIS); implementation in NEXT commit (Commit 7b) 14 mini-audit findings (F1-F14) at HEAD 48f52ed: F1-F4 — Track 2I infrastructure verified (sre-property-sweep.rkt 562 LoC; all-sweep-properties = 17 symbols post-Phase-15; canonical sweep-config + test patterns) F5-F8 — tropical-fuel SRE registration audit (11 declared properties at tropical-fuel.rkt:99-113; ZERO ctor-descs as atomic numeric domain; both merge + meet registries for 'equality) F9 ⭐ OVERLAP ANALYSIS: 3 DIRECT-ASSERTABLE (distributive + has-pseudo-complement-{rel,abs}) + 8 VERIFIED-AT-C-SERIES (commutative/associative/idempotent join + has-meet + quantale family + residuated — all verified at 1B-iii C1+C2+C3) + 14 BONUS sweep-only findings as captured artifact F10 — predicted findings for chain [0, +∞]: CONFIRM expected for distributive/SD/modular/pseudo-complement/whitmans/breadth/no-M3/ no-N5; REFUTE expected for relatively-/sectionally-/has-complement (chains aren't Boolean; un-declared so refutation expected) F11 ⚠️ CRITICAL halt-and-investigate: if distributive or has-pseudo-complement-{rel,abs} REFUTE — would invalidate tropical-fuel registration (chains structurally MUST be distributive); analogous to Track 2H F7 disproof F12 ⚠️ +inf.0 EDGE CASE: (- +inf.0 +inf.0) = +nan.0 may surface false REFUTE at residuation boundary; defensive guard may be needed at tropical-fuel-primitives.rkt:105-106 (impl-time verification) F13 — sample size 7 atoms × 343 triples × 17 props ≈ 5800 checks @ <5 sec wall budget (well under §11.3 118-127s variance band) F14 — Track 2I scaffolding inheritance: off-network sample-check infrastructure; labeled scaffolding (not new debt); retirement direction would be property-cells with monotone-merge (sister to PM Track 12 callback retirement scope) 5 drift risks (D-1V-6-1 through D-1V-6-5): D-1V-6-1 ✅ atomic domain ZERO ctor-descs (audit-resolved per F7) D-1V-6-2 ⬜ +inf.0/NaN edge case in residuation (needs impl verification per F12) D-1V-6-3 ⬜ CRITICAL — if distributive/has-pseudo-complement REFUTE (halt-and-investigate gate per F11) D-1V-6-4 ✅ breadth-bound #:max-width 4 ceiling for chain breadth=1 (audit-resolved per F10) D-1V-6-5 ✅ suite-wall regression (audit-resolved per F13) 3 NEW codification candidates (WATCHING list): 1. Atomic numeric domain wiring to property-sweep (first ZERO-ctor-descs domain swept; precedent for OE MemoryCostQ/MessageCountQ + PReduce e-class cost dimensions) 2. Assertion scope = declared properties only; bonus findings as captured artifact (methodology pattern) 3. +inf.0/NaN edge cases in tropical algebra surface at residuation boundary (defensive guard pattern at primitives module level) §3 Progress Tracker: - NEW row "1V Commit 7 mini-design + mini-audit" ✅ §11.X.6 - UPDATED row "1V Commit 7 — Item #3 SRE property-sweep verification" Notes reference §11.X.6 (status remains ⬜ until Commit 7b impl) Dailies opening bookmark (+97 lines): - Phase 1V state at session opening - Co-dependent mini-design + mini-audit cycle - 14 findings summary - 5 resolutions - 5 drift risks - 3 NEW codification candidates - Pre-implementation gate satisfied - Next steps (Commit 7b implementation; then Commit 8 atomic VAG + Phase 1 close) Pre-implementation gate (this commit): - HEAD 48f52ed; suite GREEN at 8218/98.6s (per Commit 6b state snapshot; unchanged this docs-only commit) - Track 2I infrastructure verified - tropical-fuel SRE registration verified - Overlap analysis complete (3 + 8 + 14) - 4 of 5 drift risks audit-resolved (D-1V-6-2 flagged for impl) No tests: docs-only persistence (consistent with prior sub-phase mini-design commits 252f8c8 / 48b3993 / b138bca / e6308cb / 2535c88). Suite GREEN gate runs at Commit 7b implementation. Files modified: - docs/tracking/2026-04-26_PPN_4C_TROPICAL_QUANTALE_ADDENDUM_DESIGN.md (+113 lines) - docs/tracking/standups/2026-05-13_dailies.md (+97 lines)

…l domain (✓ F11 GATE PASSED) Phase 1V Commit 7b implementation per §11.X.6 + §11.X.6.1. Implementation goal: wire Track 2I `all-sweep-properties` infrastructure to the tropical-fuel SRE domain. Empirically verify declared algebraic properties at the 1B-iii registration site against generated samples. Closes §11.3 item #3 obligation (Track 2I closed per user). Pre-implementation re-audit (Per-Phase Protocol step 2; 4 NEW findings): F15 ⚠️ — only test-tropical-fuel.rkt requires tropical-fuel.rkt; propagator.rkt requires only primitives per F14 cycle-break; test-sre-sd-properties.rkt MUST add explicit require F16 ⚠️ — naming-inversion concern: bot=0/top=+inf.0 vs merge=min; has-pseudo-complement-abs MAY REFUTE under standard SRE join-unit semantics (PREDICTION; refuted by measurement) F17 ⚠️ — all-sweep-properties = 20 symbols (mini-design said 17; Phases 11-15 added 5 since mini-design reference point) F18 ⚠️ — tools/run-phase9-sweep.rkt also lacks the require; sweep CLI WARN-skipped initially (F15 dual at tool path) Implementation (110 LoC + 3963-byte artifact): - tools/run-phase9-sweep.rkt (+13 LoC): - (require "../tropical-fuel.rkt") to trigger domain registration - realistic-tropical-fuel-atoms = '(1 5 10 100 1000) - 5th sweep-config entry: 'tropical-fuel '(equality) realistic-tropical-fuel-atoms (hasheq) #t - tests/test-sre-sd-properties.rkt (+97 LoC): - (require "../tropical-fuel.rkt") - tropical-fuel section with shared-fixture sweep at module load - 5 test-case blocks: 1. registration verification (F15) 2. 20 findings returned 3. shape verification 4-6. 3 ⭐ declared-and-swept assertions (distributive + has-pseudo-complement-{rel,abs}) - data/benchmarks/tropical-fuel-phase9-sweep-2026-05-17.txt (NEW): - 3963 bytes; captured artifact with variety placement + per-finding detail + 5 witness footnotes Sweep findings (depth-0; 7 atoms; 343 triples per property × 20 props): ⭐ DECLARED-AND-SWEPT (F11 gate) — ALL CONFIRMED at 100% non-vacuity: - distributive: 343/343 ✓ - has-pseudo-complement-rel: 49/49 ✓ - has-pseudo-complement-abs: 7/7 ✓ (F16 concern REFUTED) BONUS CONFIRMED (10): sd-vee, sd-wedge, modular, whitmans-condition, breadth-bound, no-m3-sublattice, no-n5-sublattice, anti-exchange-on-J, trivial-congruence-valid, total-congruence-valid BONUS REFUTED (5; structurally expected for chain): stone-identity, relatively-complemented, sectionally-complemented, has-complement, admits-day-doubling BONUS UNTESTED (2; no triples generated): mult-forgetful-congruence-valid, erasure-congruence-valid Variety placement (matches prediction for total-order chain): SD ✓ | Modular ✓ | Distributive ✓ | Heyting ✓ | Stone ✗ | Boolean ✗ | (W) ✓ F11 CRITICAL halt-and-investigate gate ✓ PASSED. F16 naming-inversion concern REFUTED by measurement: my crude pre-impl analysis didn't model the sweep's quantale-aware pseudo-complement check. Codification candidate: "trust measurement over pre-impl conjecture for declared-property verification." 3 NEW codification candidates surfaced: 1. Empirical sweep refutes pre-impl naming-inversion concern 2. Domain-registration require must land at BOTH test path and tool path (F15 + F18 dual data points; relevant for cycle-broken SRE domains per F14 pattern) 3. Atomic numeric domain wiring is FIRST instance — precedent for OE MemoryCostQ/MessageCountQ + PReduce e-class cost dimensions Drift risks (D-1V-6-1 through D-1V-6-5): D-1V-6-1 ✅ atomic ZERO ctor-descs as predicted D-1V-6-2 ✅ +inf.0/NaN DID NOT materialize D-1V-6-3 ⚠️ ✅ CRITICAL gate PASSED D-1V-6-4 ✅ breadth-bound = 1 as predicted D-1V-6-5 ✅ suite-wall within budget (108.8s; +10.2s vs baseline) VAG TWO-COLUMN (per Per-Phase Protocol step 5): (a) On-network: ✓ off-network sample-check infrastructure inherited from Track 2I (labeled scaffolding, not new debt); no new scaffolding-hides-truth patterns; require additions make registration EXPLICIT at call sites (b) Complete: ✓ 3 ⭐ assertions land + 17 BONUS findings captured; both test path + tool path wired; F11 gate PASSED at 100% non-vacuity (substantially exceeded; F16 concern dissolved) (c) Vision-advancing: ✓ empirically verifies tropical-fuel SRE registration claims; validates Track 2I cross-track methodology for atomic numeric domain wiring (FIRST instance — precedent for OE/PReduce/SH consumers) (d) Drift-risks-cleared: ✓ all 5 D-1V-6-* resolved; F18 surfaced at impl-time and resolved (codification candidate prophylactically captures the dual-path-require discipline) §3 Progress Tracker: - "1V Commit 7 — Item #3 SRE property-sweep verification" → ✅ ✓ F11-GATE-PASSED with commit hash + measurement summary - §11.X.6.1 NEW (Implementation Results + Sweep Findings) Verification: - tools/check-parens.sh — All files balanced ✓ - raco make driver.rkt — Clean compile ✓ - racket tools/run-phase9-sweep.rkt --domain tropical-fuel --depth 0 → 20 findings produced cleanly (0.0s sweep wall time) - raco test tests/test-sre-sd-properties.rkt → 38 tests / 0 failures (+5 net for tropical-fuel section vs pre-impl 33) - Full suite GREEN — 8219 tests / 108.8s / 0 failures (+1 net vs Commit 6b 8218; within §11.3 118-127s variance band) Phase 1V status: 7 of 8 commits complete. Commit 8 (atomic VAG + Phase 1 close) remaining. Files modified: - tools/run-phase9-sweep.rkt (+13 LoC) - tests/test-sre-sd-properties.rkt (+97 LoC) - data/benchmarks/tropical-fuel-phase9-sweep-2026-05-17.txt (NEW, 3963 bytes) - docs/tracking/2026-04-26_PPN_4C_TROPICAL_QUANTALE_ADDENDUM_DESIGN.md (§11.X.6.1 implementation results subsection ~210 lines; §3 tracker row updated) - docs/tracking/standups/2026-05-13_dailies.md (+~150 LoC impl bookmark)

kumavis marked this pull request as draft April 23, 2026 06:41

kumavis marked this pull request as ready for review April 23, 2026 07:51

hierophantos approved these changes Apr 23, 2026

View reviewed changes

hierophantos merged commit 922c38e into main Apr 23, 2026
1 check passed

kumavis deleted the claude/fix-github-ci-job-TcxYz branch April 23, 2026 18:05

This was referenced Apr 25, 2026

Disposition doc for eigentrust pitfalls #8/#9/#10/#16 (observations) #7

Closed

parser: preserve Rat-ness of slash-containing number literals (eigentrust pitfall #3) #13

Merged

hierophantos added a commit that referenced this pull request Apr 27, 2026

Merge pull request #13 from LogosLang/claude/fix-eigentrust-pitfall-3…

2d5a52f

…-rl3z parser: preserve Rat-ness of slash-containing number literals (eigentrust pitfall #3)

kumavis mentioned this pull request Apr 27, 2026

OCapN port: Phase 0 actor model + Phases 1–21 wire interop & vat bridge #28

Draft

kumavis mentioned this pull request May 6, 2026

Multi-constructor data types break cross-module inference for callers using bound vars #60

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix CI: rackcheck dep + bench-ppn-track3 stale API#3

Fix CI: rackcheck dep + bench-ppn-track3 stale API#3
hierophantos merged 1 commit into
mainfrom
claude/fix-github-ci-job-TcxYz

kumavis commented Apr 23, 2026

Uh oh!

hierophantos left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

kumavis commented Apr 23, 2026

Uh oh!

hierophantos left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants