Skip to content

Add pvec-zip-with library function (eigentrust pitfalls #13) - #5

Merged
hierophantos merged 1 commit into
mainfrom
claude/fix-eigentrust-pitfall-13-pv13
Apr 27, 2026
Merged

Add pvec-zip-with library function (eigentrust pitfalls #13)#5
hierophantos merged 1 commit into
mainfrom
claude/fix-eigentrust-pitfall-13-pv13

Conversation

@kumavis

@kumavis kumavis commented Apr 25, 2026

Copy link
Copy Markdown
Contributor

Fixes pitfall #13 from docs/tracking/2026-04-23_eigentrust_pitfalls.md.

Summary

Adds pvec-zip-with : (A → B → C) → PVec A → PVec B → PVec C to lib/prologos/core/pvec.prologos, mirroring data::list zip-with. Truncates to the shorter PVec, same as the List version.

Why

Without pvec-zip-with, elementwise binary operations on two PVecs (e.g. pvec-zip-with int+ a b in eigentrust) had to be written as explicit index-threaded-accumulator recursion — acc grown via pvec-push, inputs read via pvec-nth. The pitfalls memo measures this at "+1 *-go helper per primitive" doubling the file size of PVec-based algorithms.

The deeper closure-multiplicity issue (pitfall #2) is not fixed here — it gets its own PR. This change just removes one of the most painful workarounds.

Implementation

Routes through pvec-to-list / list zip-with / pvec-from-list rather than threading an index accumulator. Same O(n) cost; sidesteps pitfall #2 entirely because the wrapped f parameter is itself a function value (naturally mw), not a closure capturing a scalar.

pvec-fold-zip skipped — the user-facing case (Σ aᵢ·bᵢ) decomposes cleanly as pvec-fold add zero (pvec-zip-with mult a b) at one extra allocation. Defer until a measured use case justifies a direct primitive.

Test plan

  • New tests/test-pvec-zip-with.rkt (11 cases): equal-length elementwise add, truncation when xs/ys is shorter, both-empty / xs-empty edge cases, heterogeneous result types (Nat → Nat → Bool), eigentrust mirror case (elementwise add of two equal-length Nat vectors)
  • raco make racket/prologos/tests/test-pvec-zip-with.rkt succeeds; spec/defn forms parse cleanly through prologos-sexp-read
  • Tests do not run end-to-end on Racket 8.10 because test-support.rkt module-load hits (thread #:pool 'own ...) (a pre-existing Racket-9-only requirement). Re-run on Racket 9.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x


Generated by Claude Code

@kumavis
kumavis force-pushed the claude/fix-eigentrust-pitfall-13-pv13 branch from 7381009 to 0aad507 Compare April 26, 2026 01:03
kumavis added a commit that referenced this pull request Apr 26, 2026
…rks in WS (eigentrust pitfalls #5)

EigenTrust pitfall #5 (2026-04-23) reported that

    (let [tnew := [eigentrust-step c p alpha t]]
      match [rat-lt [linf-norm [sub-vec tnew t]] eps]
        | true  -> tnew
        | false -> [eigentrust-iterate c p alpha eps [int- budget 1] tnew])

failed with `let: let with bracket bindings requires: (let [bindings...]
body)`. Working `let` examples either kept the body on the same line as
`let ...]` or used a bracket-grouped expression body — nested `match`
inside the body did not parse.

Root cause: the whole let form is wrapped in `(...)`. parse-reader's
`group-items` applies its "brackets win" rule and DROPS the
indent-open/indent-close markers around the body line. The body's
continuation tokens (`match x | _ -> x`) end up spliced flat into the
let's argument list, so `expand-let` saw `((x := 1) match x ...)`
instead of the expected `((x := 1) <body>)` shape. Branch 1 of
`expand-let` rejected anything other than `(length rest) = 2`, hence
the error.

Fix: in `expand-let`'s bracket-bindings branch, when `rest` has more
than 2 elements, treat all post-bindings tokens as the body and wrap
them as a single application list. This matches the usual
"continuation lines are indented further than `let`" convention that
`defn` and `match` already honour at the top level. Bare let and
empty-body let still raise as before.

Test coverage in `tests/test-let-multiline-ws.rkt`:
- Read-level shape checks (single-line, single-token continuation,
  bracket-grouped body, multi-token continuation) document the parser
  behavior the fix relies on
- End-to-end `run-ns-ws-last` checks for: single-line, simple body,
  bracket-grouped body, multi-token application body, the eigentrust
  reproducer (multi-line match inside let body), and two-binding let
  with multi-token body
- Empty-body let still raises

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>

@kumavis kumavis left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

hiero approved

kumavis added a commit that referenced this pull request Apr 26, 2026
…rks in WS (eigentrust pitfalls #5)

EigenTrust pitfall #5 (2026-04-23) reported that

    (let [tnew := [eigentrust-step c p alpha t]]
      match [rat-lt [linf-norm [sub-vec tnew t]] eps]
        | true  -> tnew
        | false -> [eigentrust-iterate c p alpha eps [int- budget 1] tnew])

failed with `let: let with bracket bindings requires: (let [bindings...]
body)`. Working `let` examples either kept the body on the same line as
`let ...]` or used a bracket-grouped expression body — nested `match`
inside the body did not parse.

Root cause: the whole let form is wrapped in `(...)`. parse-reader's
`group-items` applies its "brackets win" rule and DROPS the
indent-open/indent-close markers around the body line. The body's
continuation tokens (`match x | _ -> x`) end up spliced flat into the
let's argument list, so `expand-let` saw `((x := 1) match x ...)`
instead of the expected `((x := 1) <body>)` shape. Branch 1 of
`expand-let` rejected anything other than `(length rest) = 2`, hence
the error.

Fix: in `expand-let`'s bracket-bindings branch, when `rest` has more
than 2 elements, treat all post-bindings tokens as the body and wrap
them as a single application list. This matches the usual
"continuation lines are indented further than `let`" convention that
`defn` and `match` already honour at the top level. Bare let and
empty-body let still raise as before.

Test coverage in `tests/test-let-multiline-ws.rkt`:
- Read-level shape checks (single-line, single-token continuation,
  bracket-grouped body, multi-token continuation) document the parser
  behavior the fix relies on
- End-to-end `run-ns-ws-last` checks for: single-line, simple body,
  bracket-grouped body, multi-token application body, the eigentrust
  reproducer (multi-line match inside let body), and two-binding let
  with multi-token body
- Empty-body let still raises

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
Adds pvec-zip-with: (A -> B -> C) -> PVec A -> PVec B -> PVec C as a
library function in lib/prologos/core/pvec.prologos. Truncates to the
shorter PVec's length, mirroring List zip-with's semantics. The
signature also mirrors List zip-with: spec pvec-zip-with {A B C : Type}
[A -> B -> C] [PVec A] [PVec B] -> [PVec C].

Implementation routes through pvec-to-list / zip-with / pvec-from-list
rather than threading an index accumulator via pvec-fold + pvec-nth.
The list-conversion path is O(n) (same asymptotic cost as a direct
index walk) and avoids the closure-multiplicity issues that pitfall #2
identifies for pvec-fold callbacks that capture scalars. The wrapping
zip-with's f parameter is itself a function (naturally mw), so it does
not trip the QTT path that scalar capture in a pvec-fold closure would.

Without this primitive, callers writing elementwise binary operations
on two PVecs (e.g. pvec-zip-with int+ a b in eigentrust) had to write
explicit index-threaded-accumulator recursion. This restores parity
with the List API.

Adds tests/test-pvec-zip-with.rkt covering: equal-length elementwise
add (length / nth values), truncation when xs is shorter, truncation
when ys is shorter, both-empty / xs-empty edge cases, heterogeneous
result types (Nat -> Nat -> Bool), and the eigentrust mirror case
(elementwise add of two equal-length Nat vectors). Tests do not run
under Racket 8.10 due to the pre-existing BSP scheduler issue
((thread #:pool 'own ...) keyword arg unsupported); both this new
file and the pre-existing test-pvec-fold.rkt fail with the same
test-support.rkt module-load error on 8.10. Test file compiles cleanly
via raco make and parses cleanly through prologos-sexp-read.

pvec-fold-zip skipped: the user-facing case (Σ aᵢ·bᵢ) decomposes
cleanly as pvec-fold add zero (pvec-zip-with mult a b) at one extra
allocation. A direct pvec-fold-zip primitive would either add a
second native AST node or require building an intermediate Sigma-pair
list which itself risks tripping multiplicity inference. Defer until
a measured use case justifies the extra surface.

https: //claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x
Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
@kumavis
kumavis force-pushed the claude/fix-eigentrust-pitfall-13-pv13 branch from 0aad507 to b8dcf8b Compare April 26, 2026 03:05
kumavis added a commit that referenced this pull request Apr 26, 2026
…rks in WS (eigentrust pitfalls #5)

EigenTrust pitfall #5 (2026-04-23) reported that

    (let [tnew := [eigentrust-step c p alpha t]]
      match [rat-lt [linf-norm [sub-vec tnew t]] eps]
        | true  -> tnew
        | false -> [eigentrust-iterate c p alpha eps [int- budget 1] tnew])

failed with `let: let with bracket bindings requires: (let [bindings...]
body)`. Working `let` examples either kept the body on the same line as
`let ...]` or used a bracket-grouped expression body — nested `match`
inside the body did not parse.

Root cause: the whole let form is wrapped in `(...)`. parse-reader's
`group-items` applies its "brackets win" rule and DROPS the
indent-open/indent-close markers around the body line. The body's
continuation tokens (`match x | _ -> x`) end up spliced flat into the
let's argument list, so `expand-let` saw `((x := 1) match x ...)`
instead of the expected `((x := 1) <body>)` shape. Branch 1 of
`expand-let` rejected anything other than `(length rest) = 2`, hence
the error.

Fix: in `expand-let`'s bracket-bindings branch, when `rest` has more
than 2 elements, treat all post-bindings tokens as the body and wrap
them as a single application list. This matches the usual
"continuation lines are indented further than `let`" convention that
`defn` and `match` already honour at the top level. Bare let and
empty-body let still raise as before.

Test coverage in `tests/test-let-multiline-ws.rkt`:
- Read-level shape checks (single-line, single-token continuation,
  bracket-grouped body, multi-token continuation) document the parser
  behavior the fix relies on
- End-to-end `run-ns-ws-last` checks for: single-line, simple body,
  bracket-grouped body, multi-token application body, the eigentrust
  reproducer (multi-line match inside let body), and two-binding let
  with multi-token body
- Empty-body let still raises

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>

@hierophantos hierophantos left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Small surgical addition to lib/prologos/core/pvec.prologos: routes through pvec-to-list / list zip-with / pvec-from-list (same O(n) asymptotic, sidesteps pitfall #2 by making f a value rather than a scalar-capturing closure). 11 cases cover equal/truncated/empty inputs, heterogeneous result types, and the eigentrust elementwise-add mirror.

No conflicts with #4 / #16.

Two non-blocking observations:

  1. PR #15 makes its new pvec helpers prelude-available via book/PRELUDE + namespace.rkt. This PR doesn't — pvec-zip-with reachable only via explicit require [prologos::core::pvec :refer [pvec-zip-with]]. Was that intentional? Other pvec functions are in the prelude (push, nth, length, ...).

  2. Style observation, not a request: we have an unsettled convention in core/ (curried [A -> B -> C] vs uncurried [A B -> C] — currently 2:2 split) and a planned-but-unimplemented "improved implicit inference" cleanup that would let us drop {A B C : Type} for simple kind-Type variables. Both are our work to settle, not yours; just flagging that the canonical form will likely be spec pvec-zip-with [A B -> C] [PVec A] [PVec B] -> [PVec C] once we land that work.

Approving.

@hierophantos
hierophantos merged commit becda91 into main Apr 27, 2026
1 check passed
@hierophantos
hierophantos deleted the claude/fix-eigentrust-pitfall-13-pv13 branch April 27, 2026 04:55
hierophantos added a commit that referenced this pull request Apr 27, 2026
…-letm

Multi-line let body wrapping in expand-let (eigentrust pitfall #5)
kumavis pushed a commit that referenced this pull request Apr 27, 2026
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.
kumavis pushed a commit that referenced this pull request Apr 27, 2026
Per user direction:
- Replace the body of every DELETED entry with a single-sentence
  explanation. Numbers reserved per prior instruction.
- Delete #15 (QTT multiplicity on fst/snd thrice). I re-tested
  with a real Racket — `pair [snd p] [fst p]` then a third use of
  `fst p` works fine; no multiplicity error. The failure I had
  conflated this with was actually #14's "match-and-reconstruct
  Sigma" issue.

Result: pitfalls doc shrinks from 765 to 534 lines. Remaining
real claims: #1, #4, #5, #11, #12, #13, #14, #16, #17, #18, #19,
#20 (the user has reviewed only #0-10 so far; #11-20 still
pending their review).
kumavis pushed a commit that referenced this pull request May 4, 2026
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.
kumavis pushed a commit that referenced this pull request May 4, 2026
Per user direction:
- Replace the body of every DELETED entry with a single-sentence
  explanation. Numbers reserved per prior instruction.
- Delete #15 (QTT multiplicity on fst/snd thrice). I re-tested
  with a real Racket — `pair [snd p] [fst p]` then a third use of
  `fst p` works fine; no multiplicity error. The failure I had
  conflated this with was actually #14's "match-and-reconstruct
  Sigma" issue.

Result: pitfalls doc shrinks from 765 to 534 lines. Remaining
real claims: #1, #4, #5, #11, #12, #13, #14, #16, #17, #18, #19,
#20 (the user has reviewed only #0-10 so far; #11-20 still
pending their review).
kumavis pushed a commit that referenced this pull request May 6, 2026
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
hierophantos added a commit that referenced this pull request May 17, 2026
…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
hierophantos added a commit that referenced this pull request May 17, 2026
…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.
hierophantos added a commit that referenced this pull request May 17, 2026
…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.
hierophantos added a commit that referenced this pull request May 17, 2026
…n) + FORK CHECKPOINT

1C-ii-b mini-design conversation 2026-05-16. Four questions (α/β/γ/δ);
one (α) architecturally load-bearing. All resolved with user.

Resolutions:

α2 — Box pattern at #4 + #5 (matches §10.3.A Variant B canonical design).
  The 1C-i α finding revealed #1 + #2 already have partial Variant B
  (box-mutation pattern); #4 + #5 use recursive function with per-fire
  struct-copy decrement. α1 (per-fire lockstep keeping recursive structure)
  would deviate from Variant B design + miss §13.6.A perf target. α2
  refactors recursive → box pattern, matching design intent.
  Trade-off: preempts 1C-iii migration for check sites at lines 3217 +
  3270 (those check sites migrate to per-iteration box checks under α2).
  D-1C-ii-b-2: 1C-iii scope reduces from 11 to 9 check sites; captured
  explicitly so 1C-iii doesn't double-migrate.

β1 — Helper signature: set-box! mutation style (matches §10.3.A
  pseudocode + #1 + #2 idiom + §13.6.A spike measurement pattern):
    (init-fuel-local-var! net) -> box
    (flush-fuel-local-var! net box) -> net

γ1 — Helpers inline in propagator.rkt (tightly coupled to BSP scheduler
  code; ~15-25 LoC doesn't justify separate module).

δ-3-tests — Mirror 1C-ii-a pattern: cell-field-lockstep at sequential
  phase exit + helper correctness + sequential exhaustion via
  cell-mechanism. Per-entry-point coverage via full suite GREEN.

Drift risks named:
- D-1C-ii-b-1 (LOAD-BEARING; retirement obligation): β1 lockstep at
  1C-iv. flush-fuel-local-var! writes BOTH cell + struct field during
  1C-ii-b through 1C-iii. At 1C-iv, struct-field write retires
  alongside prop-net-hot-fuel field; only cell-write remains. Affects
  all 4 sequential schedulers (share the helper). Captured in §10.4
  1C-iv scope.
- D-1C-ii-b-2 (LOAD-BEARING; scope reduction): α2 preempts 1C-iii
  migration for lines 3217 + 3270. 1C-iii scope 11 → 9 captured in
  §10.4 1C-iii scope.
- D-1C-ii-b-3: widen/narrow used by abstract interpretation; full
  suite catches semantic regressions.
- D-1C-ii-b-4: #1 + #2 redirect preserves inner-loop set-box! pattern.
- D-1C-ii-b-5: recursive→box refactor mechanical mistake risk.

Implementation sketch (confirmed; pending impl):
- Helpers in propagator.rkt (~15-25 LoC; init returns box; flush writes
  both cell + field; D-1C-ii-b-1 retirement at 1C-iv)
- #1 + #2 redirect (~10-20 LoC): preserve existing box pattern; init
  source + finalize sink use helpers
- #4 + #5 refactor (~40-60 LoC): recursive define → let loop; per-fire
  box decrement replaces struct-copy [fuel (sub1 ...)]; check sites
  3217 + 3270 migrate to (<= (unbox local-fuel) 0)

Revised total scope: ~115-205 LoC (larger than §10.4 original ~40-60
LoC estimate due to recursive→box refactor at #4 + #5).

Design doc changes:
- NEW §10.0.3: 1C-ii-b Mini-Design Resolutions (4 questions + retirement
  obligation + 1C-iii scope reduction + drift risks + impl sketch)
- §10.4 1C-ii-b: refined with α2 box pattern + helper details + scope
  estimate ~115-205 LoC; 1C-ii-b row notes #1+#2 simple redirect vs
  #4+#5 refactor distinction
- §10.4 1C-iii: scope REDUCED to 9 check sites (was 11) per D-1C-ii-b-2;
  lines 3217 + 3270 marked PREEMPTED by 1C-ii-b
- §10.4 1C-iv: scope expanded with explicit "retire 1C-ii-b β1 lockstep
  sync" task (D-1C-ii-b-1 retirement obligation)
- §3 Progress Tracker: 1C-ii-b mini-design ✅; 1C-ii-b impl ⬜ pending;
  1C-iii scope reduced annotation; 1C-ii-b row notes revised scope

🍴 FORK CHECKPOINT 2026-05-16:

User plans to fork back to `75d0c47e` (Phase 1B SUBSTRATE END-OF-PHASE
summary commit). Future session re-enters at that commit; design doc +
dailies file carry forward ALL 1C work (4 commits this fork).

Commits accomplished this fork (since 75d0c47):
- 97163e1 whole-phase 1C mini-design + Phase 1V scope (§10.0)
- cd770a0 1C-i mini-audit + §10 doc cleanup (§10.0.1; 5 findings)
- c7cbffc 1C-ii-a mini-design (§10.0.2)
- e94b0b8 1C-ii-a impl (Variant A; 8289/126.4s/0 fails)
- THIS commit: 1C-ii-b mini-design (§10.0.3) + fork checkpoint

Dailies entry includes comprehensive re-entry pointers:
- Cumulative architectural state at fork checkpoint
- 4-step re-orientation guide for fresh session
- Watching list of codification candidates accumulated across 1C arc

Process observation: Q-1C-ii-b-α surfaced a genuine architectural choice
(not just diff cleanliness like 1C-ii-a's α). The recursive-vs-box
pattern decision at #4 + #5 has real perf implications AND triggers a
sub-phase boundary blur (preempts 1C-iii for 2 sites). Explicit capture
of LOAD-BEARING + scope reduction prevents drift.

Codification candidate: "Audit-driven scope refinements should
propagate from §10.0.x mini-audit findings into §10.4 sub-phase plan
estimates BEFORE next sub-phase opens." 2 data points (1C-i ε bench
2→18; 1C-ii-b α scope 40-60→115-205). Watching list.

No code changes; pure design clarification + fork checkpoint. Suite
state unchanged: 8289 tests / 126.4s / 0 failures.

Next (per re-entry plan): 1C-ii-b implementation per §10.0.3 sketch.
~45-90 min estimated.
hierophantos added a commit that referenced this pull request May 17, 2026
…e drift caught

Per Stage 4 Per-Phase Protocol step 2: audit codebase BEFORE 1C-ii-b
implementation, even though mini-design landed (§10.0.3). Mini-design ↔
mini-audit are co-dependent; audit refines design before code lands.

Five findings (F1-F5) + 3 structural confirmations (F6-F8) + 2 new drift
risks (D-1C-ii-b-6/7).

**Key finding F1 — Line drift confirmed (D-1C-i-1 materialized)**:
+11 line shift at #4 (run-widen-phase 3214→3225; check 3217→3228) +
#5 (run-narrow-phase 3267→3278; check 3270→3281) + wrapper
(run-to-quiescence-widen 3353→3364) since 1C-i audit (2026-05-16
earlier). §10.0.3's preempted-check-site references at 3217+3270
updated to 3228+3281 in §10.4 1C-ii-b + 1C-iii rows + §3 Progress
Tracker.

**Key finding F3 — DESIGN REFINEMENT to §10.0.3 at #1+#2 finalize**:
Audit reality: the existing finalize at #1 (lines 2050-2058) + #2
(lines 2092-2095) writes BOTH worklist AND fuel-field via a single
struct-copy. Replacing with `flush-fuel-local-var!` (cell + field for
fuel; not worklist) would lose worklist update.

Resolution Option A (cleanest):
- #1 + #2 init: use `init-fuel-local-var!` ✓ matches §10.0.3
- #1 + #2 finalize: keep existing struct-copy verbatim; ADD
  `(net-cell-write n* fuel-cell-id (unbox remaining-fuel))` after it
- #4 + #5: use BOTH helpers per §10.0.3 sketch (no worklist
  interleaving; helper fits cleanly)

Helper signature stays generic; application mechanism varies per-site
based on existing code structure. D-1C-ii-b-6 names the asymmetry for
future maintainers.

**Other findings**:
- F2: #1 split between `run-to-quiescence-inner` (outer guard at 2030;
  check at 2034 stays 1C-iii scope) + `run-to-quiescence-drain` (box
  pattern at 2039+)
- F4: widen wrapper check sites (3368/3371/3378) stay 1C-iii scope
- F5: `net-fuel-remaining` accessor (line 3110) is 1C-iv scope
- F6: helper placement at line ~2027-2029 (before
  run-to-quiescence-inner; first user of helpers)
- F7: helpers don't exist yet (clean introduction)
- F8: 1C-ii-a tests (test-tropical-fuel.rkt:404-475) are mirror
  template

**Revised scope (audit-driven; tighter than §10.0.3)**:
~106-167 LoC (down from ~115-205) due to F3 refinement saving
~10-40 LoC of unnecessary refactoring.

**Persisted**:
- §10.0.4 NEW: full audit findings + F3 refinement + drift risks
- §10.0.3 amended with forward-pointer to §10.0.4
- §3 Progress Tracker: new "1C-ii-b mini-audit ✅" row
- §10.4 1C-ii-b + 1C-iii line numbers refreshed
- Dailies entry capturing audit findings + process observation

**Codification candidate**: 3rd data point on "Mini-audit step is
materially load-bearing for scope precision" (1C-i ε bench 2→18; 1C-ii-b
α scope 40-60→115-205; this audit 115-205→106-167). Strong watching-list
status; codify after 1 more.

No code changes; design doc + dailies only. Suite state unchanged at
8289 tests / 126.4s / 0 failures.
hierophantos added a commit that referenced this pull request May 17, 2026
…rn + convergence-check filter

Implementation per §10.0.3 mini-design + §10.0.4 audit refinement (F3 Option A).
Migrates 4 sequential scheduler entry points (#1/#2/#4/#5) from per-fire
struct-copy to box-pattern fuel tracking with β1 lockstep flush at observation
points.

**Helpers** (~30 LoC at line ~2030, before run-to-quiescence-inner):
- init-fuel-local-var! — reads cell into mutable box (Option A: REMAINING)
- flush-fuel-local-var! — writes box to BOTH cell + struct-field (β1 lockstep
  transitional; struct-field write retires at 1C-iv per D-1C-ii-b-1)

**#1 + #2 redirect** (per F3 Option A — helper init only):
- run-to-quiescence-drain (#1): init source migrated; existing finalize
  struct-copy preserved (handles fuel-field alongside worklist); cell-write
  ADDED after struct-copy for β1 lockstep
- run-to-quiescence-inner/traced (#2): mirrors #1
- Helper NOT used at #1+#2 finalize (would lose worklist flush); F3 audit
  refinement saved ~10-40 LoC over §10.0.3's symmetric design

**#4 + #5 recursive→box refactor** (~80 LoC mirrored):
- run-widen-phase (#4) + run-narrow-phase (#5): converted from recursive
  define with per-fire [fuel (sub1 ...)] struct-copy to (let loop ...) with
  box init at entry, box decrement per fire, flush at all 3 exits
  (contradiction / fuel-exhausted / null-worklist)
- 2 preempted check sites (refreshed line numbers per §10.0.4 F1) migrate to
  (<= (unbox local-fuel) 0) box check; 1C-iii scope reduces from 11 to 9

**Convergence-check filter** (D-1C-ii-b-8 NEW load-bearing invariant):
- run-to-quiescence-widen's narrow-loop convergence check compared full
  (prop-network-cells narrowed) vs (prop-network-cells net) via equal?
- My flush updates fuel-cell-id every narrow round → cell 11 differs per
  round → equal? always #f → narrow loop never converges → fuel exhausts
- Fix: filter scheduler-state cells (fuel-cell-id + fuel-budget-cell-id)
  from BOTH sides of the equal? via champ-delete before comparison
- **Principled per Cell/Propagator/Scheduler Orthogonality**: scheduler-state
  cells should not participate in propagator-driven convergence checks.
  Codification candidate captured.

**Tests added** (test-tropical-fuel.rkt; +118 LoC):
1. cell-field-lockstep at sequential phase exit (via run-to-quiescence-widen)
2. helper correctness (init returns box from cell; flush writes BOTH cell + field)
3. exhaustion via cell-mechanism at sequential scheduler

**Verification**:
- Delimiter check: GREEN both files
- raco make: clean
- Targeted (5 files; 105 tests): all PASS in 6.6s
- Full suite: **8292 tests / 113.7s / 0 failures** (-12.7s vs 1C-ii-a baseline
  126.4s; +3 tests). Wall-time improvement likely from box pattern eliminating
  per-fire struct-copy alloc for widen+narrow paths.

**Drift risks**:
- D-1C-ii-b-1 (retirement obligation): cell+field dual write retires at 1C-iv
  alongside prop-net-hot-fuel field
- D-1C-ii-b-2 (1C-iii scope reduction 11→9): captured in §10.4 + §3 Progress
  Tracker with refreshed line numbers
- D-1C-ii-b-6 (helper asymmetry at #1+#2): documented inline + §10.0.4 F3
- D-1C-ii-b-7 (1C-iii scope boundaries): line 2034 + 3477/3480/3487 NOT
  touched (1C-iii scope respected)
- **D-1C-ii-b-8 NEW** (convergence-check filter as load-bearing invariant):
  future modifications to prop-network-cells semantics OR new scheduler-state
  cells must update the filter

**Process observation**: the F3 audit refinement (helper init-only at #1+#2)
saved ~10-40 LoC of unnecessary refactoring AND preserved the worklist flush
semantic that would have been lost under §10.0.3's symmetric design.
Audit-precedes-implementation paid off again (3rd data point on this watching
pattern).

**Codification candidate (NEW)**: "Cells-map convergence checks must filter
scheduler-state cells per Cell/Propagator/Scheduler Orthogonality." Watching
list; 1 data point.

**Watching list update**: "Audit-driven scope refinements propagate into §10.4
estimates pre-next-sub-phase" now has 3 data points (1C-i ε; 1C-ii-b α; 1C-ii-b
F3) — strong codification candidate; codify after 1 more.

Tracker + dailies updated. β1 lockstep retirement obligation at 1C-iv captured
in §10.4 scope so transitional dual-writes can't drift into permanent
belt-and-suspenders.

Next: 1C-iii (9 check sites; line numbers re-audited at 1C-iii mini-audit).
hierophantos added a commit that referenced this pull request May 24, 2026
…entation pending next session

Strong checkpoint entry for 2026-05-20 session close:
- Current HEAD: df9dacc (PM 13 + 2A.b mini-design captured)
- Suite: 8228 / 109.1s / 0 failures (last measured 2A.a close)
- Phase 2A.b: 🔄 mini-design + audit complete; implementation PENDING

Includes:
- Status matrix across all addendum phases
- 3 NEW architectural deliverables summary (PM 13, Parent Design Doc Phase 4 update, §8.7.b)
- Operational principle codified: "off-network ≡ scaffolding"
- 8-step implementation plan from §8.7.b.9 with file:line references
- 8 drift risks from §8.7.b.8 to scrutinize
- Tasks status carried forward (#4 ✅ / #5 🔄 / #6 ⬜)
- Key reference docs ordered for next-session hot-load
- 4 critical context items NOT to lose (handler-as-scaffolding is PM 13 scope;
  box-bridge is structural scaffolding; adversarial 3-column framing discipline;
  operational principle for decision-making)
- 6 codification candidates watching list

Rationale for checkpoint: context budget pressure after substantial design
work (mini-design + audit + PM 13 capture + Parent Design Doc update +
§8.7.b persistence). Implementation requires another ~95-110 LoC + test
rewrite + validation cycles. Cleaner to land in fresh session per Stage 4
"conversational implementation cadence" — checkpoint surfaces what was built,
what's next.

Next session: hot-load HANDOFF_PROTOCOL → read §8.7.b → execute 8-step
implementation list → validate → close 2A.b.
kumavis pushed a commit that referenced this pull request Jul 29, 2026
…its value

Two more entries from the gaps document. 9604 unit tests, conformance 24/24.

SETS AND FLOATS (§1.1 #5, §1.10 #3, §1.10 #11)

The reference emits both -- `b'#' + sorted(items) + b'$'` and
`b'D' + struct.pack('>d', obj)` -- and the model had no constructor for
either, so a peer that sent one got a decode failure and no diagnostic. The
gap was open because adding a constructor means following it through every
exhaustive match over SyrupValue: 100 arms across five files.

A set canonicalises by SORTED ENCODED ITEM, exactly as a dict does by key, so
`encode` sorts and `re-encode` preserves what the peer sent -- the same split,
for the same reason.

A float is carried as its RAW WIRE PAYLOAD INCLUDING THE MARKER BYTE, not as a
number. Nothing in this stack does float arithmetic, and the one thing the
codec owes a peer is byte-exactness. Decoding an `F` to a number and
re-encoding it as the `D` the reference prefers would preserve the value and
change the bytes -- precisely the class of defect `re-encode` exists to
prevent. It also costs one constructor instead of two.

The cross-impl fixture grew both, and its harness moved from UTF-8 to Latin-1:
it hex-encoded through `string->bytes/utf-8` while the codec's byte model is
one byte per code point, so no vector carrying a byte >= 0x80 could ride it at
all -- which is exactly the bug class the fixture exists to catch.

The set vector is inserted in sorted order deliberately. @Endo's encoder emits
insertion order where `contrib/syrup.py` sorts; an unsorted literal would pin
that disagreement into a cross-impl vector instead of testing anything. Our
sorting is pinned separately, against the reference's rule.

THE PLAIN-VALUE ERROR (§1.10 #10)

`plain-value-error-reason` ignored its argument and returned a constant, so
the peer could not tell which of its pipelined sends went to a plain value.
It now names the offending value after the condition. It stays a single
string rather than a record: the reason travels inside our own `<Error …>`
wrapper, which upstream has no type for, so a peer can only treat it as a
diagnostic -- and the condition stays the prefix so it still discriminates
"rejected" from "forwarded".

A NOTE ON HOW THE ARM INSERTION WENT WRONG

The mechanical pass copied each `syrup-bytes` arm's right-hand side for the
new float arm, and one of those right-hand sides referenced its own binder --
so `syrup-bytes-of` got `| syrup-float _ -> some b` with `b` unbound. That
presents as "Unbound variable" when a CONSUMER imports captp-core, while
captp-core itself processes with zero errors: the exact signature of a stale
`.pnet` cache. I cleared the cache, saw it again, and only then went looking
for the real cause. Clearing twice is what separated the two.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YM6gc3cMNH2Ymor4jdZY8u
kumavis pushed a commit that referenced this pull request Jul 29, 2026
…wn premises

9616 unit tests, conformance 24/24. Seven entries were open; five are closed
and two turned out to rest on premises that no longer hold.

§1.9 #4 IS A LANGUAGE GAP, NOT AN OCapN ONE

Annotating an FFI binding `:requires (CryptoCap)` makes the whole module
unimportable from a `.prologos` file: the requirement propagates to the caller
and nothing can introduce a root capability. I tried wrapping the bindings in
same-module functions the way `tcp-testing` does, and importing the capability
type alongside. Neither helps.

Then the actual discovery: `prologos::ocapn::tcp-testing`, which this document
cites as proof the convention is live, CANNOT BE IMPORTED EITHER. Nothing in
the tree imports it, and its test loads it through the sexp `imports` path,
which does not hit the check — so a module that no consumer can use has been
sitting there with a green test asserting "just load the module".

It now carries a characterization test that pins the WS-mode failure. That
test asserts behaviour that is WRONG on purpose: when the language grows a
root capability form it fails, and that is the signal to thread the capability
for real. A gap with a witness beats a gap with a comment.

§1.8 M2 HAS LOST ITS CONSEQUENCE

The stated failure was that a process-wide keypair collapses session-ids and
the handoff replay guard, keyed on session, then refuses a peer's legitimate
second handoff. That guard became per-connection when the gift namespace was
split, so two connections no longer share a replay set. What is left is a
conformance deviation with no failing input — which by this document's own
standard is not a finding. Minting per connection also costs a
`process-string` per accept, which the suite's wall-clock budget would notice.

CLOSED

  - §1.1 #5 / §1.10 #3 / §1.10 #11 — sets and floats (previous commit)
  - §1.4 #6 — op:listen carries wants-partial (previous commit)
  - §1.6 M8 — undecodable frames abort (previous commit)
  - §1.10 #10 — the plain-value reason names its value (previous commit)
  - §1.10 #12 — locator hints are a map (previous commit)

WHAT IS ACTUALLY LEFT

Five entries, and four of them are one problem: the gifter and receiver roles
live in Racket because a Prologos behaviour cannot open a socket. §1.7 M8
(double processing), §1.7 M7 (unregistered enliven slots) and §1.10 #8
(unsigned Node peers) are all downstream of that. Both of §1.7 M7's live
consequences are gone; what remains is that the slot reservation is by
convention rather than construction.

The fifth, §1.2 M3, is independent and has a known shape: allocate our own
answer position for a forwarded send and resolve the queued deliver's from it.
The pieces exist — `bs-add-question` already maps a peer answer position to a
local promise and the pump answers from it — but wiring them means threading
BridgeState through a loop that returns bytes only.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YM6gc3cMNH2Ymor4jdZY8u
hierophantos added a commit that referenced this pull request Aug 14, 2026
…ercised" fix had a pin all along — and it was green through a message that asserted a falsehood

F5 — reduction's `below-value` `@sub` arm still panicked with "the parser
grammar forbids this shape". The parser never forbade it; the depth-≥2 SHIELD
did, and C2 removed the shield. Round 1 found the identical false assertion in
the sibling `below-components` twelve lines above and fixed it there. This is the
sibling-function shape a third time in one slice.

⭐ THE SIBLING'S FIX IS THE WRONG FIX HERE, and that is why this is a message
change and not a delegation. `below-components` could go terminal-only-else-
delegate because its fallthrough IS the branch walk. `below-value`'s fallthrough
is the `memq` arm, which LISTS `sub` — an entry its own P4a site-8 comment
records as DEAD *only while this arm guards on `@sub` alone*. Delegating would
revive it and run `branch-entries` on a `(@sub …)` head, projecting a RAW STEP
LIST as a nominal key: the class D4.P4a removed. So the guard stays; the wording
is corrected to state the true invariant.

⭐⭐ AND I RECORDED IT AS "LATENT AND UNEXERCISED, NO PIN CAN REACH IT" — FALSE,
caught by sweeping for echoes of the string I was renaming. `(sub ★)` genuinely
cannot reach the arm (the star-TAIL arm above catches it, a sub-step not being a
star), so no SURFACE spelling was demonstrated — but the P3a-verify pin
constructs the residue directly as IR, `'((a (@sub (b)) c))`, and reaches this
exact panic. It stayed green across a message asserting a prohibition that never
existed, because it asserted only `expr-panic?`. That is Watching #5 — "pins that
assert KINDS never assert MESSAGES" — verbatim, and it is the second time this
slice has paid for it. The message is pinned now: it must say "not terminal" and
"compiler-invariant violation", and must NOT say "grammar forbids".

Mutation-tested by inverting the message IN PLACE: exactly one pin reddens, and
its failure output is the proof the arm is reached. ⚠ The mutant run exited 0.

F7 — `select-steps-star-tail?`'s PRECONDITION header (the "⚠ EXACTLY TWO, and
that is the subtle half" note, which is what stops the tail arm firing on
`(b c ★)` and re-nesting into the branch-root reading Q_U46 rejected) was
separated from the function it guards by ~40 lines and two unrelated
definitions — round 1 spliced `select-step-makes-no-layer?` and
`select-branch-has-star?/deep` in between. Definition moved up under its header;
the two round-1 predicates follow it. Verified pure motion: the added and removed
blocks are byte-identical.

Also swept: the arm-order note above F5's arm quoted the old message text.

Gate: battery 517, 0 FAILURE / 0 ERROR by direct require (the runner aborts this
file; run via direct require) · mutation-tested in place · neighbourhood 4/4, 122
tests · acceptance 89 markers, 0 errors · compile clean with
PLT_CS_COMPILE_LIMIT=1000000.

Owed next: the three diagnostic majors (using the VERIFIED remedies, not the
recorded one), DEFERRED 122's rename, then the full suite — unrun since 5e4a333
and still the biggest untested claim.
hierophantos added a commit that referenced this pull request Aug 14, 2026
…peated the class it was fixing — derived from ONE example, backwards about its own rule, and pinned by a test that was vacuous from birth

Round 3 (`wf_1bb04012-af2`, 4 lenses + adjudicator): 14 raw → 9 survivors, 5
killed or merged by the adjudicator's own re-runs. Every finding below was
re-measured on the main thread before acting. Nothing in rounds 1–2 produced a
wrong answer; all survivors are diagnostic, instrument or record defects.

⭐⭐ #1 (MAJOR) — THE ROUND-2 REWRITE OF `star-l4-mixed` WAS ITSELF DERIVED FROM
ONE POPULATION. In its driving example the STAR branch happened to be the
keyless one, so both remedies were written as things to do to a SIBLING. Outside
that example they are non-actions, measured:
  pc{db.hosts* ports*}   → the error BYTE-IDENTICAL (starring a sibling that
                           keeps no key changes nothing)
  pc{db.hosts* ports^^}  → parse error, "one `^` per segment"
  d3{a* x^.y.z*}         → byte-identical to d3{a* x.y.z*} — one caret is not
                           enough at depth 3
and the action that DOES work was never named, because it is on the star branch:
  pc{db^.hosts* ports^}  → @[@[1 2] @[80]]           ✓
  d3{a* x^.y^.z*}        → @[@[1 2] @[5 6]]          ✓
The message now states Q_U47's REMAINDER rule and lets the action follow from it
— dissolve the surviving key on WHICHEVER branch keeps one, including the star
branch itself, one per surviving level — instead of enumerating spellings that
hold for one shape. "Select the flatten in its own block" was the only clause
that was an action in every population measured; it stays, marked as such.

⭐⭐ #5 (MINOR, but it is why #1 was invisible) — THE RULE WAS STATED BACKWARDS.
It said a star lands keyless "when no step survives AFTER it". `*` is
branch-FINAL (`e3{a*.p}` → "`*` is only supported at the END of a branch"), so
that condition is VACUOUSLY TRUE and the sentence asserts every star lands
keyless — while `e3{a.b.c*}` → `{:a {:b @[1 2]}}` lands KEYED. The sibling
message written in the SAME commit had it right ("the steps BEFORE the star").
Two messages, one rule, opposite directions, and the battery pinned the wrong
one.

⭐⭐ #2 (MAJOR) — AND THE PIN THAT SHOULD HAVE CAUGHT #1 WAS VACUOUS FROM BIRTH
(`d8776b66`). `C2V`'s `cfg` is `{:db {:hosts … :ports …}}`, so `:ports` lives
UNDER `:db` and `cfg{db.hosts* ports^}` died at field resolution ("field :ports
is not present … available fields: :db"), never reaching the L4 seat. Its
`c2-refused?` half is #t for that unrelated error and its `check-false` matched
nothing — both halves green on a failure that was not the one under test. That
is precisely why the round-2 rewrite could specialise to the wrong population
with nothing to contradict it. Fixed with a subject whose keyless sibling is
genuinely top-level, plus the POSITIVE half the file's own `c2-refused?` header
already demands: assert WHICH gate refused.

#8 (MINOR) — "sub-block grouping does NOT survive a star" was an overclaim.
Measured, it survives when EVERY grouped branch is starred
(`cfg{db.{hosts* ports*}}` → `{:db @[@[1 2] @[80]]}`, 0 errors); what breaks it
is starring some but not all — Q_U47 again. Claim narrowed and BOTH spellings
pinned, so a future session trying the natural all-starred form finds the record
already knows about it instead of concluding the comment is wrong.

#7 (MINOR) — the round-2 pins under-discriminated: bare `c2-refused?` negatives
that pass on any error (the #2 class), and a `^k'` regex already green before
"EITHER branch" was added. Each refusal now asserts which gate produced it.

#3 + #9 — DEFERRED 123 corrected on two points, both mine. It is LIVE, not a
latent quality risk: `rec3{a.b a^r.b.zzz}` reports ``(branch `a.b`)`` while
`rec3{a.b}` alone SUCCEEDS, so the message names a valid sibling that did not
fail. And there is a SECOND collapse channel the diagnosis never named — the ω
marker (`rowz{k:s.zzz}` → ``(branch `k.s`)``, and `k.s` fails one step earlier,
so it is not merely a different spelling). The repair scope also charged for a
"reduction twin" that DOES NOT EXIST: reduction has 0 `append path` and 0
`select-fail` sites and threads no path at all. That stale clause read as an
ATOMIC co-migration obligation and would have sent the next session hunting for
a seat that isn't there — it survived a whole verify round because pins assert
kinds and code, never prose.

NOT charged to this commit, reported by round 3 and left where they belong:
· DEFERRED 117 reproduces at HEAD and its exposure is understated — `mx{z a^.{c*}}`
  is a WHOLE-FILE ABORT (`symbol<?: contract violation`, no output at all) and
  the branch-swapped order silently drops a key at 0 errors, while the un-nested
  spelling refuses correctly in both orders. Pre-existing; the deliberate
  "widen both gates in one edit" deferral still stands.
· LATENT: typing's `select-step-name` `[else s]` renders a raw IR step list into
  a user-facing message for a `(@sub …)` head, and syntax.rkt's comment above it
  asserts that cannot happen. Reachable only as constructed IR — the parser
  seals all four follower bands.

Gate: battery 520 → 521, 0 FAILURE / 0 ERROR, exit 0, full output size ·
mutation-tested in place (round-2 wording restored → exactly the two new R3 pins
redden) · acceptance 89 markers, 0 errors · neighbourhood 4/4, 122 tests.
⚠ The first cut of two pins compared FULL rendered lines, which end with the
source expression — so byte-identical messages could never compare equal and the
pin went red for its own construction, not for behaviour. They compare the
message body now.
hierophantos added a commit that referenced this pull request Aug 14, 2026
…ted its own class, the pin that was vacuous from birth, and two corrections to a one-day-old DEFERRED

D4 §5.P4e-1b-iii-C2-R3 (new anchor #p4e-1b-iii-c2-r3), tracker row, dailies LOG
(viii) + STATE head. Suite 10188/488/0 at 428e0c8.

The record's centre of gravity is that #1, #5 and #2 are ONE story: round 2 fixed
two messages whose remedies did not work, and derived the replacement from the
single example in front of it — where the star branch happened to be the keyless
one — so every new remedy was scoped to a sibling and was a non-action elsewhere.
The rule it stated was vacuous for a branch-final operator, which is why it read
as fine. And the only pin over that population had been vacuous since d8776b6,
which is why nothing contradicted it.

⭐ A vacuous pin does not merely fail to catch a defect — it LICENSES a rewrite
to specialise to the wrong population. Recorded as the lesson to carry into
1b-iv, alongside 'derive from the ruling, not the example' and 'pins assert kinds
and code, never prose'.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants