Migrate bench-bsp-le-track2.rkt to current ATMS API (CI unblock) by kumavis · Pull Request #10 · LogosLang/prologos

kumavis · 2026-04-25T09:03:33Z

Summary

raco pkg install --auto (the CI install step) was failing with:

benchmarks/micro/bench-bsp-le-track2.rkt:47:3: tms-write: unbound identifier

The file targeted 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.

This PR migrates the benchmark to the current API rather than skipping it (the originally-considered approach in PR #2's commit f3a3ca3). The benchmark stays in the suite and continues to provide pre-Track-2 baseline data on the now-current ATMS API.

Migration shape

Old (deleted)	New
`tms-read tcv stack` (depth-N walk over per-cell stack)	`atms-read-cell a key` (walk values list until support ⊆ believed); depth N modeled by atms with N supported values + believed worldview = N-element assumption set
`tms-write tcv stack value` (push depth-N frame)	`atms-write-cell a key value support` (O(1) struct-copy); cost dominated by support-set construction (hoisted out of the timed loop, mirroring the old benchmark's structure)
`tms-commit tcv aid` (promote contingent value to permanent)	No direct analog. Replaced with `atms-with-worldview` benchmarks (alone, and switch + read) — the closest behavioural shape: changing the believed set so subsequent reads re-resolve

Other helpers (atms-empty, atms-assume, atms-amb, atms-add-nogood, atms-consistent?, set operations, make-prop-network, net-new-cell, net-add-propagator, run-to-quiescence) are unchanged — those names still exist on the post-refactor API.

Verification

raco make racket/prologos/benchmarks/micro/bench-bsp-le-track2.rkt succeeds on Racket 8.10 (CI uses 8.14)
Full bench runs end-to-end: 19 timed benchmarks reporting stable results
Sample from end-to-end run:
- atms-read-cell depth=1 x100000 median 7.40 ms
- atms-read-cell depth=10 x100000 median 57.34 ms — confirms the design intuition that read cost scales with depth
- atms-write-cell depth=10 x50000 median 4.00 ms — write cost is roughly depth-independent, dominated by struct-copy

Why this approach instead of the skip

The earlier-considered fix on PR #2's commit f3a3ca3 adds compile-omit-paths to skip the file. That unblocks CI but loses a useful pre-track baseline. Migrating preserves the data the benchmark was intended to gather, on the API the system actually uses now.

Cross-PR impact

PRs #4, #5, #6, #7, #8, #9, #11, #12 all currently carry the compile-omit-paths skip as a CI-unblock commit. Once this PR lands, those PRs can drop their skip commit (it becomes redundant: the bench works on its own). Strictly merge this first, then rebase the others to drop the duplicate.

Commits

3e03516 — migrate bench file (97 insertions, 33 deletions)

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

The file targeted 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. `raco pkg install --auto` was failing on `unbound identifier: tms-write`. Migration shape: * TMS read at depth N → atms-read-cell against an atms whose target cell carries N supported values, with the believed worldview = N-element assumption set. Read cost is O(values-length) walking the values list + a hash-subset? against an N-element support, mirroring the old O(stack-depth) walk. * TMS write at depth N → atms-write-cell with a pre-built N-element support hasheq. The atms-write-cell call itself is O(1); the meaningful cost is constructing the support set, which the benchmark does once outside the timed loop (matching the old benchmark's structure where the stack was hoisted). * TMS commit → no direct analog post-refactor. Replaced with worldview switching benchmarks (atms-with-worldview alone, and switch + read) which are the closest behavioural shape: changing the believed set so subsequent reads re-resolve. Other helpers (atms-empty / atms-assume / atms-amb / atms-add-nogood / atms-consistent? / set operations / make-prop-network / net-new-cell / net-add-propagator / run-to-quiescence) are unchanged — those names still exist on the post-refactor API. Verified locally on Racket 8.10 (CI uses 8.14): the file now compiles via `raco make` and the full bench runs end-to-end with 19 timed benchmarks reporting stable results. This replaces the earlier-considered `compile-omit-paths` skip (pre-existing on PR #2's branch f3a3ca3) with a real fix, so the benchmark stays in the suite and continues to provide pre-Track-2 baseline data on the (now current) ATMS API. https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>

hierophantos

Thanks for the careful migration. Three things I appreciated: the honest "no direct analog" note for tms-commit (forcing an analog would have produced misleading numbers), the string->symbol correctness fix that the old benchmark was getting away with by accident, and the merge-this-first sequencing call in the PR body — saved us a rebase round. Approving and merging.

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>

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.

@Endo

…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

…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

@bcast

… files + the two strategy-independent repairs The Exhaustive Walkers rule applied BEFORE the new step kind lands rather than after a silent miss. Q_U7's (@bcast step) arrives at P4c and would have met every one of these. THE COUNT WENT 4 -> 8 -> 13, AND THE METHOD WAS THE DEFECT EACH TIME. The design's audit said four silent catch-alls. My census said eight. The adversarial verify (4 skeptics, distinct lenses) found THIRTEEN across five files. My method was syntax-directed: grep the exported helper names, look for `cond` arms, in three files. That structurally cannot see dispatchers that OPEN-CODE the shape tests (pretty-print's step->string has no exported identifier to grep) or that are shaped as `and`/`if` rather than `cond` (the leaf classifiers; parser.rkt, a fourth file the census never opened). The five it missed, and why two of them are the serious ones: 9 syntax.rkt select-branch-collapse [leaf] UPSTREAM of the guards 10 syntax.rkt select-branch-keyless? [leaf] UPSTREAM of the guards 11 parser.rkt dissolve-step? [leaf] gates the ^.. desugar 12 parser.rkt branch-problem positional ^ legality 13 pretty-print.rkt step->string leaked the raw datum to users #9 and #10 classify a branch's LAST step and run BEFORE the guard in all three branch walks. A silent #f there DEFEATS the guards rather than reaching them: the branch is mis-SORTED (keyed vs keyless) with no raise anywhere, and select-branch-top-keys' `key` arm returns without touching `rest`, so the wrong key set flows into the parser's L4 and duplicate-output-key checks. Traced: [server (@bcast (@key name dissolve))] yields '(server) where '(#f) is correct. Owner ruling: extend the routing; deliver the totality. All thirteen now route through select-step-kind. Twelve RAISE. #13 renders a loud marker instead -- pp-expr is on the error-message path, so raising there converts a real diagnostic into an internal crash, and typing-errors' catch-all could swallow it, achieving LESS than a visible marker. It uses select-step-kind/display, a non-raising variant defined by DELEGATION to the classifier (never a second copy of the kind list -- that is the drift this phase exists to kill). Written scope decision, not an omission. The ADDING A KIND recipe in syntax.rkt was corrected to name all thirteen sites and all five files: that comment, not the design doc, is what a future implementer follows at P4c, and its first version would have left five sites wrong. SELF-REVIEW CAUGHT ONE BEFORE THE VERIFY (twin-drift): the memq guards must list EXACTLY what the old else caught, and the four do NOT have the same right answer. Sites 5 and 8 -- the "below a kept head" twins -- sit under arms taking TERMINAL sub and ord-step, so their else also caught ord-branch; I omitted it at both, turning a delegation into a raise. Validated by re-introducing the defect: fails with "select-below-value: no arm for select step kind 'ord-branch". THE VERIFY REFUTED MY OWN REASONING, TWICE: - I cited reduce_steps flatness as proving "pure per-step cost reduction". perf-inc-reduce! fires at :2054, BEFORE the whnf-trivial? branch at :2062, so reduce_steps CANNOT move for that leg. A tautology dressed as a control. - n=3 sequential wall is not an A/B by our own rules. Measured spread on an unchanged tree is ~20%, so my 6 ms delta sat ~1.2x the noise band. What actually carries the claim is a control I never considered: expr-tchamp/trrb/thset are structurally identical transients that are NOT whnf-trivial and have no match arm. Interleaved, 200k iters x 5 rounds: 211 ns vs 2019 ns = 1822 ns/call, 9.5x. Honest magnitude is ~= -0.1% of WALL (reduce_ms is 0.3% of end-to-end), not the "-25%" headline I wrote. TWO FALSE CLAIMS OF MINE, CORRECTED: "commit the corpus A/B harness, still uncommitted" -- it landed at 3005170 and this document's OWN P2 close notes record it, four hundred lines above where I asserted it open. And the [_ e] catch-all cited at :3936 when it is :3957. Plus an off-by-one repeated ten times: the classifier has FIVE kinds, so (@bcast ...) is the SIXTH -- in the phase whose subject is counting correctly. THE REPAIRS. The re-whnf hoist moved NOTHING and lands as a CONTRACT fix: the header comment has claimed since P3a that the subject is "evaluated ONCE ... reused across every branch" while (whnf subj-expr) sat INSIDE the append-map lambda; on a def-bound subject the repeat calls are cache hits. The whnf-trivial? container arms carry the win. Their safety proof holds structurally (546 arms, only [_ e] non-anchored, zero match-expanders in the tree) but "identical semantics" was too strong: the fast path returns before the fuel decrement, so containers now consume zero reduction fuel. One-way, cannot produce a wrong answer, matches the ~70 pre-existing trivial kinds -- now qualified in place rather than smuggled under the match-arm proof. TESTS +20 (204 -> 224). The pins were weaker than claimed: check-exn exn:fail? demonstrably passes on an ARITY error or a malformed fixture, so a change to make-record/champ-insert could have turned all eight green with the arms fully reverted. Narrowed to a message-matching predicate; fixtures hoisted out of the guarded lambdas. select-step-kind-unhandled had ZERO coverage (all 8 pins raise from the CLASSIFIER, never a consumer's else) and now has a direct pin. One whole-node fixture was a message pin sold as a discriminator (expr-champ is transparent, so a buried panic prints the same strings) -- the expr-panic? assertion was added. KNOWN LIMIT, STATED: the whole-node fixtures discriminate at BRANCH granularity inside one select-reduce call. If P4c implements omega by mapping a sub-walk over N elements, each gets its own let/ec and burial returns with all three still green. P4c owes the element-level fixture. This IS the P2-baseline establishment: sections 5.P4/5.X price X.close against a "P2 baseline" that was never recorded. Suite 9614/476/0 (full, complete run). Battery measured 224 (grep and runner agree). Acceptance 52/52. The suite total is +15 not +20 because test-properties.rkt is property-based and reported 13 -> 8 between runs; it reports 13 in three consecutive standalone runs and is untouched by this change. The gate is 0 failures across 476 files, never the count.

kumavis force-pushed the claude/ci-fix-skip-bench-bsp-le-track2 branch from 5cdcee3 to 3e03516 Compare April 25, 2026 09:13

kumavis changed the title ~~Skip stale bench-bsp-le-track2.rkt during raco setup (CI unblock)~~ Migrate bench-bsp-le-track2.rkt to current ATMS API (CI unblock) Apr 25, 2026

hierophantos approved these changes Apr 25, 2026

View reviewed changes

hierophantos merged commit bd3f8f8 into main Apr 25, 2026
1 check passed

hierophantos deleted the claude/ci-fix-skip-bench-bsp-le-track2 branch April 25, 2026 23:25

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

Merge origin/main: PR #10 (bench-bsp-le-track2 ATMS API migration)

3bff5a7

kumavis mentioned this pull request Apr 26, 2026

Tracking issue for "eigentrust pitfall doc" PRs #19

Open

13 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Migrate bench-bsp-le-track2.rkt to current ATMS API (CI unblock) - #10

Migrate bench-bsp-le-track2.rkt to current ATMS API (CI unblock)#10
hierophantos merged 1 commit into
mainfrom
claude/ci-fix-skip-bench-bsp-le-track2

kumavis commented Apr 25, 2026 •

edited

Loading

Uh oh!

hierophantos left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

kumavis commented Apr 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Migration shape

Verification

Why this approach instead of the skip

Cross-PR impact

Commits

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

kumavis commented Apr 25, 2026 •

edited

Loading