Skip to content

Add EigenTrust reputation algorithm: implementation, tests, benchmark#2

Draft
kumavis wants to merge 20 commits into
mainfrom
claude/eigentrust-prologos-implementation-JGszt
Draft

Add EigenTrust reputation algorithm: implementation, tests, benchmark#2
kumavis wants to merge 20 commits into
mainfrom
claude/eigentrust-prologos-implementation-JGszt

Conversation

@kumavis
Copy link
Copy Markdown
Contributor

@kumavis kumavis commented Apr 23, 2026

Implements the Kamvar-Schlosser-Garcia-Molina (2003) EigenTrust
algorithm in Prologos, with exact-Rat power iteration on the
row-stochastic local-trust matrix. The update rule is the standard
damped form

t_{k+1} = (1 - alpha) * (C^T * t_k) + alpha * p

expressed entirely through structural recursion over [List [List Rat]].

Deliverables:

  • examples/eigentrust.prologos: canonical demo with worked examples
    (uniform fixed point, symmetric uniform-on-others matrix, the step
    operator in isolation, and helper primitives). Runs in ~50s via
    racket driver.rkt and outputs the expected stationary distributions.

  • tests/test-eigentrust.rkt: 17 rackunit assertions covering vector
    primitives, matrix operations, convergence on the uniform and
    symmetric matrices, edge cases (empty vectors), and a hand-computed
    single-step check from a perturbed starting vector. Uses the shared
    prelude-cache from test-support.rkt and runs the entire algorithm
    through the WS reader in a single process-string-ws call to amortise
    the ~50s elaboration cost across all 17 test-cases. Runs in ~50s.

  • benchmarks/comparative/eigentrust.prologos: four workloads exercising
    full convergence, iter-capped power iteration from a perturbed start
    (with epsilon=0 to force deterministic iteration counts), and the
    isolated step operator. Integrates with tools/bench-ab.rkt; median
    wall time ~36s with <1% coefficient of variation across runs.

  • docs/tracking/2026-04-23_eigentrust_pitfalls.md: eight elaboration /
    surface-syntax gotchas surfaced by this implementation (primitives
    not first-class in map/zip-with but accepted by foldr, QTT
    multiplicity violations on map-with-closure, nested list literals
    coercing 0/1 to Int 0, missing mutual recursion, WS let with
    multi-line body, multi-line spec with comments, multi-arg multi-
    clause defn failures, and exact-Rat denominator blow-up). Each is
    documented with expected behaviour, actual behaviour, workaround,
    and a suggested fix.

All implementation choices (explicit structural recursion instead of
map/zip-with, single-function iterator with (t, tnew) pair to avoid
mutual recursion, top-level rz : Rat := 0/1 as a splice target for
nested list literals) are driven by the pitfalls above and documented
in the source.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp

@kumavis kumavis marked this pull request as draft April 23, 2026 03:54
@kumavis kumavis force-pushed the claude/eigentrust-prologos-implementation-JGszt branch from 1f2cce5 to 45681c4 Compare April 23, 2026 19:04
kumavis added a commit that referenced this pull request Apr 25, 2026
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 added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
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>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 25, 2026
Cherry-picked from PR #2 (commit f3a3ca3). 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
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
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 is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 26, 2026
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 added a commit that referenced this pull request Apr 26, 2026
…uctor args

Eigentrust pitfall memo (2026-04-23) #2 reports that

    spec scale-vec Rat [List Rat] -> [List Rat]
    defn scale-vec [s xs] [map (fn [x : Rat] [rat* s x]) xs]

fails QTT with "Multiplicity violation," even though no parameter is
annotated linear. The user's workaround was to inline the recursion.

ROOT CAUSE (diagnosed via tracing checkQ-fb / inferQ-app): a kind-level
Pi multiplicity mismatch. Type constructors like List are registered
with kind `Pi(m0, Type, Type)` (the type arg is erased — `data List {A}`
uses `:0` mult on its implicit binder). Generic combinators' specs like
`(spec map {A B : Type} {C : Type -> Type} ...)` elaborate the inner
`Type -> Type` via surf-arrow, which defaults `->` to `mw`. So map's `C`
parameter expects `Pi(mw, Type, Type)`. When List flows into that slot
via implicit insertion, QTT's `unify` rejects the mult mismatch even
though typing-core succeeds (typing-core's check uses Pi-domain only,
not mult). The user-visible error wrongly accuses the closure body of
the violation; the actual conflict is the kind unification.

FIX (approach (a) — targeted lattice lenience): in
`classify-mult-problem` (unify.rkt), treat the {m0, mw} pair as
compatible. Rationale: m0 = "zero runtime uses" trivially satisfies
mw = "any number of uses (including zero)." {m1, m0} and {m1, mw} stay
incompatible — linear (m1) IS a real value-level usage constraint.

SIDE EFFECT FOLLOW-UP: making more unify paths succeed exposed a
pre-existing latent bug in typing-core.rkt's check/Pi case
(lines 2143, 2151, 2503): three `solve-mult-meta!` calls were
unguarded, so re-entry on already-solved metas crashed with
`solve-mult-meta!: mult-meta already solved`. Guarded each call with
`mult-meta-solved?` (matches the existing QTT-side guards in
qtt.rkt:2106-2108). This bug existed before but was masked because the
m0/mw mismatch caused unification to fail earlier and short-circuit.

APPROACH SELECTION:
  (a) chosen — targeted unify-mult lenience for {m0, mw}. Surgical,
      covers the kind-level case, doesn't change the rest of QTT.
  (b) rejected — defaulting all closure captures to mw would break
      linearity guarantees in code that relies on the inference.
  (c) deferred — type-driven inference of closure captures from the
      callee's spec is the principled fix but requires touching
      elaborator.rkt + typing-core.rkt + qtt.rkt across multiple
      argument-position detection sites. Approach (c) remains the
      future ideal once the spec-position information flows
      consistently into the closure elaboration site.
  (d) not needed — (a) handles the actual eigentrust case cleanly.

Tests:
- Updated test-unify.rkt: replaced the {m0, mw} reject test with two
  new tests: (i) {m0, m1} still rejects, (ii) {m0, mw} now succeeds.
- Added test-closure-mult.rkt with 10 tests covering: unit tests for
  unify-mult lenience, eigentrust scale-vec reproducer (full
  invocation), foldr/scale-and-shift defns capturing scalars,
  explicit -1> linear annotation still rejected on multi-use, and
  the dict-param mw heuristic regression check.
- Full suite: 7818 tests in 545s, 9 failures all pre-existing
  environmental (collection not found for prologos/propagator +
  rackcheck — same modules unavailable in this Racket install).
- All 105 mult/qtt-related tests pass; all 51 unify tests pass; all
  141 capability + qtt-pipeline tests pass.

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 26, 2026
…uctor args

Eigentrust pitfall memo (2026-04-23) #2 reports that

    spec scale-vec Rat [List Rat] -> [List Rat]
    defn scale-vec [s xs] [map (fn [x : Rat] [rat* s x]) xs]

fails QTT with "Multiplicity violation," even though no parameter is
annotated linear. The user's workaround was to inline the recursion.

ROOT CAUSE (diagnosed via tracing checkQ-fb / inferQ-app): a kind-level
Pi multiplicity mismatch. Type constructors like List are registered
with kind `Pi(m0, Type, Type)` (the type arg is erased — `data List {A}`
uses `:0` mult on its implicit binder). Generic combinators' specs like
`(spec map {A B : Type} {C : Type -> Type} ...)` elaborate the inner
`Type -> Type` via surf-arrow, which defaults `->` to `mw`. So map's `C`
parameter expects `Pi(mw, Type, Type)`. When List flows into that slot
via implicit insertion, QTT's `unify` rejects the mult mismatch even
though typing-core succeeds (typing-core's check uses Pi-domain only,
not mult). The user-visible error wrongly accuses the closure body of
the violation; the actual conflict is the kind unification.

FIX (approach (a) — targeted lattice lenience): in
`classify-mult-problem` (unify.rkt), treat the {m0, mw} pair as
compatible. Rationale: m0 = "zero runtime uses" trivially satisfies
mw = "any number of uses (including zero)." {m1, m0} and {m1, mw} stay
incompatible — linear (m1) IS a real value-level usage constraint.

SIDE EFFECT FOLLOW-UP: making more unify paths succeed exposed a
pre-existing latent bug in typing-core.rkt's check/Pi case
(lines 2143, 2151, 2503): three `solve-mult-meta!` calls were
unguarded, so re-entry on already-solved metas crashed with
`solve-mult-meta!: mult-meta already solved`. Guarded each call with
`mult-meta-solved?` (matches the existing QTT-side guards in
qtt.rkt:2106-2108). This bug existed before but was masked because the
m0/mw mismatch caused unification to fail earlier and short-circuit.

APPROACH SELECTION:
  (a) chosen — targeted unify-mult lenience for {m0, mw}. Surgical,
      covers the kind-level case, doesn't change the rest of QTT.
  (b) rejected — defaulting all closure captures to mw would break
      linearity guarantees in code that relies on the inference.
  (c) deferred — type-driven inference of closure captures from the
      callee's spec is the principled fix but requires touching
      elaborator.rkt + typing-core.rkt + qtt.rkt across multiple
      argument-position detection sites. Approach (c) remains the
      future ideal once the spec-position information flows
      consistently into the closure elaboration site.
  (d) not needed — (a) handles the actual eigentrust case cleanly.

Tests:
- Updated test-unify.rkt: replaced the {m0, mw} reject test with two
  new tests: (i) {m0, m1} still rejects, (ii) {m0, mw} now succeeds.
- Added test-closure-mult.rkt with 10 tests covering: unit tests for
  unify-mult lenience, eigentrust scale-vec reproducer (full
  invocation), foldr/scale-and-shift defns capturing scalars,
  explicit -1> linear annotation still rejected on multi-use, and
  the dict-param mw heuristic regression check.
- Full suite: 7818 tests in 545s, 9 failures all pre-existing
  environmental (collection not found for prologos/propagator +
  rackcheck — same modules unavailable in this Racket install).
- All 105 mult/qtt-related tests pass; all 51 unify tests pass; all
  141 capability + qtt-pipeline tests pass.

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 26, 2026
…uctor args

Eigentrust pitfall memo (2026-04-23) #2 reports that

    spec scale-vec Rat [List Rat] -> [List Rat]
    defn scale-vec [s xs] [map (fn [x : Rat] [rat* s x]) xs]

fails QTT with "Multiplicity violation," even though no parameter is
annotated linear. The user's workaround was to inline the recursion.

ROOT CAUSE (diagnosed via tracing checkQ-fb / inferQ-app): a kind-level
Pi multiplicity mismatch. Type constructors like List are registered
with kind `Pi(m0, Type, Type)` (the type arg is erased — `data List {A}`
uses `:0` mult on its implicit binder). Generic combinators' specs like
`(spec map {A B : Type} {C : Type -> Type} ...)` elaborate the inner
`Type -> Type` via surf-arrow, which defaults `->` to `mw`. So map's `C`
parameter expects `Pi(mw, Type, Type)`. When List flows into that slot
via implicit insertion, QTT's `unify` rejects the mult mismatch even
though typing-core succeeds (typing-core's check uses Pi-domain only,
not mult). The user-visible error wrongly accuses the closure body of
the violation; the actual conflict is the kind unification.

FIX (approach (a) — targeted lattice lenience): in
`classify-mult-problem` (unify.rkt), treat the {m0, mw} pair as
compatible. Rationale: m0 = "zero runtime uses" trivially satisfies
mw = "any number of uses (including zero)." {m1, m0} and {m1, mw} stay
incompatible — linear (m1) IS a real value-level usage constraint.

SIDE EFFECT FOLLOW-UP: making more unify paths succeed exposed a
pre-existing latent bug in typing-core.rkt's check/Pi case
(lines 2143, 2151, 2503): three `solve-mult-meta!` calls were
unguarded, so re-entry on already-solved metas crashed with
`solve-mult-meta!: mult-meta already solved`. Guarded each call with
`mult-meta-solved?` (matches the existing QTT-side guards in
qtt.rkt:2106-2108). This bug existed before but was masked because the
m0/mw mismatch caused unification to fail earlier and short-circuit.

APPROACH SELECTION:
  (a) chosen — targeted unify-mult lenience for {m0, mw}. Surgical,
      covers the kind-level case, doesn't change the rest of QTT.
  (b) rejected — defaulting all closure captures to mw would break
      linearity guarantees in code that relies on the inference.
  (c) deferred — type-driven inference of closure captures from the
      callee's spec is the principled fix but requires touching
      elaborator.rkt + typing-core.rkt + qtt.rkt across multiple
      argument-position detection sites. Approach (c) remains the
      future ideal once the spec-position information flows
      consistently into the closure elaboration site.
  (d) not needed — (a) handles the actual eigentrust case cleanly.

Tests:
- Updated test-unify.rkt: replaced the {m0, mw} reject test with two
  new tests: (i) {m0, m1} still rejects, (ii) {m0, mw} now succeeds.
- Added test-closure-mult.rkt with 10 tests covering: unit tests for
  unify-mult lenience, eigentrust scale-vec reproducer (full
  invocation), foldr/scale-and-shift defns capturing scalars,
  explicit -1> linear annotation still rejected on multi-use, and
  the dict-param mw heuristic regression check.
- Full suite: 7818 tests in 545s, 9 failures all pre-existing
  environmental (collection not found for prologos/propagator +
  rackcheck — same modules unavailable in this Racket install).
- All 105 mult/qtt-related tests pass; all 51 unify tests pass; all
  141 capability + qtt-pipeline tests pass.

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 26, 2026
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 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.
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
@kumavis kumavis force-pushed the claude/eigentrust-prologos-implementation-JGszt branch from f3a3ca3 to 04219ac Compare April 29, 2026 06:49
claude added 9 commits April 29, 2026 07:01
Adds a Racket-direct EigenTrust implementation that uses Prologos's
underlying propagator network (make-prop-network, net-new-cell,
net-add-propagator, run-to-quiescence-bsp) but bypasses the Prologos
surface language entirely. The point is to isolate "how fast is the
propagator infrastructure on this workload" from "how fast is the
Prologos elaboration + reduction on this workload" — the first four
variants pay both.

Architecture: chain-of-cells. One cell per iteration holds the
entire trust vector at step k; one plain propagator per step reads
t_{k-1} and writes t_k. Constants (M, p, alpha) live in cells with
last-write-wins merge. After K BSP rounds the chain has settled;
the final answer is read from t_K's cell.

Plain propagators (NOT fire-once) are required: the chain depends
on cell writes propagating across BSP rounds, which is what plain
propagators do. With fire-once, all K propagators fire in round 1
on the initial snapshot before any of them can chain — only step-1
sees the right input, and the result is alpha*p.

Files:
  benchmarks/comparative/eigentrust-propagators.rkt       — implementation
  benchmarks/comparative/eigentrust-propagators-bench.rkt — timing harness
  tests/test-eigentrust-propagators.rkt                   — 13 rackunit
  docs/tracking/2026-04-29_0650_eigentrust-on-propagators.md — design + tracker

Results (5-run median):
  variant            wall_ms  reduce_ms
  list + rat (P)     62 475   18 372
  list + posit32 (P) 61 683   17 990
  pvec + rat (P)     76 884   33 006
  pvec + posit32 (P) 77 039   33 198
  propagators           600   0.16

The propagator-direct variant is ~115_000x faster on the W3 ring
workload. Both versions perform identical Racket-level exact-rational
arithmetic; the 5-orders-of-magnitude gap measures the cost of the
Prologos elaborator + reducer on this hot path. The propagator
chain handles k=10 in 0.56 ms; the surface variants exhibit O(k^2)
reducer blowup beyond k≈3 (unreduced tnew term tree).

Network Reality Check (per .claude/rules/workflow.md):
  1. net-add-propagator calls? K (=4 for W3) plain propagators.
  2. net-cell-write calls produce the result? K writes to t_1..t_K.
  3. Trace cell-creation → prop-install → write → read = result? Yes.

The matrix-vector multiply inside each fire function is off-network
Racket compute. The on-network flow is the trust-vector cell
sequence. A fine-grained per-peer variant is documented in the
design doc as out-of-scope.

Updates the comparison doc to 5-way; expands "How to reproduce"
with the new bench + test commands.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
…omparison

Two new variants on top of the rat-coarse propagator implementation:

  * float: same chain-of-cells topology, hardware flonums (flvector)
    instead of exact rationals. Lets us measure the cost of exact-Rat
    vs hardware float on the same propagator network. Result matches
    the rational version within 1e-9.

  * rat-fine: per-peer cells (K*n cells, K*n propagators) instead
    of one cell per iteration. Each peer-step propagator reads all
    n cells of the previous iteration row + 3 constants and writes
    one scalar trust value. Architecturally more on-network at the
    cost of higher constant overhead per cell.

Results on the W3 reference workload (ring-4, k=4, alpha=3/10):

  variant            reduce_ms
  list+rat (P)       18 372
  list+posit32 (P)   17 990
  pvec+rat (P)       33 006
  pvec+posit32 (P)   33 198
  rat-coarse           0.12
  rat-fine             0.23
  float                0.10

All three propagator variants are 5+ orders of magnitude faster than
any surface variant. Among the propagator variants:
  - float beats rat-coarse by ~17% (hardware double vs exact rat)
  - rat-fine loses to coarse by ~2x at n=4 (per-cell overhead exceeds
    per-fire-work savings; the crossover happens at larger n or under
    parallel BSP)
  - All scale linearly with K; surface variants O(k^2) blow up
    beyond k=3

New files:
  benchmarks/comparative/eigentrust-propagators-float.rkt — flonum impl
  benchmarks/comparative/eigentrust-propagators-fine.rkt  — per-peer impl
  tests/test-eigentrust-propagators-float.rkt             — 9 tests
  tests/test-eigentrust-propagators-fine.rkt              — 6 tests
  docs/tracking/2026-04-29_eigentrust_propagators_pitfalls.md
                                                          — 5 hiccups

Updates:
  benchmarks/comparative/eigentrust-propagators-bench.rkt
                          — refactored to time all 3 variants
                            (was: just rat-coarse)
  docs/tracking/2026-04-23_eigentrust_comparison.md
                          — 5-way -> 7-way; added W3-deep table;
                            cross-references both pitfalls docs

Pitfalls doc seeded with 5 entries (most important first):

  1. Fire-once + initial scheduling breaks chained propagators. All K
     fire-once props get scheduled at install time (their inputs are
     pre-loaded), then BSP fires them ALL in round 1 on the same
     snapshot. Only step-1 sees its right input; step-2..K read zeros
     and write alpha*p. Use plain (non-fire-once) props for chains.

  2. Cell merge function is invoked only on writes, not on initial-value
     reads. For value-typed cells, last-write-wins (lambda (old new)
     new) is the correct merge.

  3. Vector equality of inexact floats fails `equal?` after arithmetic.
     Use approximate comparison in tests.

  4. (for/sum (...)) returns exact 0 on empty input, not 0.0. Use
     for/fold seeded at 0.0 for flonum accumulators.

  5. Fine-grained variant: store cell-ids in vectors-of-vectors for
     O(1) access in fire functions; list-ref would be O(n).

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
Generates random column-stochastic matrices at n = 8..512 and times
all three propagator variants at fixed K=4 to characterize how the
implementations scale with matrix size. Looking for:

- Whether coarse-vs-fine flips at larger n (per-cell overhead
  amortizes when per-fire work grows)
- How float vs rat-coarse scales as denominators grow
- At what n the per-cell construction cost (build_ms) becomes
  significant

Random seed fixed for reproducibility. Results to be added to
docs/tracking/2026-04-23_eigentrust_comparison.md once the run
completes.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
…8..128 results

The initial scaling sweep ran rat-coarse, rat-fine, and float at the
same sizes. Exact-rat denominators compound across iterations, making
each doubling of n cost ~10-15x more time. n=128 already takes ~140s
per run; n=256 hung past 25min. Capped the rat sweep at n=128 and
added a float-only sweep at n=256..4096 (rat is intractable there).

Documented results for n=8..128 in the comparison doc:

  n      rat-coarse   rat-fine   float    rat/float
  8         5.3 ms     6.9 ms    0.14 ms     38x
  16       56.7 ms    75.8 ms    0.14 ms    392x
  32      669.5 ms   687.8 ms    0.19 ms  3 496x
  64       10.0 s     10.2 s     0.42 ms 23 647x
  128     138.2 s    138.7 s     1.11 ms 124 088x

Key findings:
- Exact-rat is exponential in n (denominators grow as O(n^k))
- Float scales sub-n^2 (memory-bandwidth bound at small/medium sizes)
- rat-fine vs rat-coarse converges to 1.0x by n>=32 — per-cell
  overhead amortizes when per-fire work grows
- rat/float ratio explodes from 38x to 124,088x over n=8..128

Float-only data (n=256..4096) to follow once the running bench
completes.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
Adds per-sample timeout via thread + sync/timeout: each (variant, n)
run is killed after 30 s and reported as TIMEOUT. Once a variant
times out at some n, larger n are skipped (TIMEOUT propagates
monotonically in n for these algorithms — exact-rat denominator
growth is monotone in matrix size).

Replaces the earlier "split rat sweep at n<=128, float-only above"
hack: we now attempt every variant at every size in one sweep and
honestly report which (variant, n) cells are intractable rather
than hard-coding a cutoff. This lets the float scaling go as far
as the timeout allows and lets the rat variants self-document
their viable range.

Bench is currently running in the background (n = 8..4096); the
comparison doc will be updated with the new table when it
completes.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
…at n>=128

Final scaling table from eigentrust-propagators-scaling.rkt with the
30s per-sample timeout in place. Float runs the full sweep; rat
variants time out at n=128 and the larger sizes are skipped.

  n      rat-coarse   rat-fine   float
  8        5.72 ms    7.01 ms    0.20 ms
  16      59.80 ms   69.05 ms    0.20 ms
  32     704.99 ms  736.14 ms    0.27 ms
  64       9.37 s     9.60 s     0.43 ms
  128    TIMEOUT    TIMEOUT      1.19 ms
  256    (skip)     (skip)       4.25 ms
  512    (skip)     (skip)      18.79 ms
  1024   (skip)     (skip)      66.61 ms
  2048   (skip)     (skip)     301.24 ms
  4096   (skip)     (skip)    1455.50 ms

Headlines:
- Float computes a 4 096-peer K=4 EigenTrust step in 1.46 s.
  Sub-cubic scaling (~3.5-5x per doubling at n>=128, near the n^2
  theoretical lower bound).
- Exact-rat denominators grow as O(n^k) -- intractable past n~64.
- rat-fine/rat-coarse stays ~1.0x at all measured n; per-cell
  overhead amortizes as per-fire work grows.
- rat/float gap is exponential in n (28x at n=8, ~125 000x at n=128).

The implementations look good. Float is genuinely viable for
real-world trust graphs (thousands of peers). The rat variants are
correctness-verification tools at small n only.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
The plain implementation iterates the same off-network kernel
(eigentrust-step / eigentrust-step-fl) K times in a tail loop, with
parameter-passing instead of cells. Both rat and float variants.
Same kernel as the propagator versions; only the orchestration
differs. Lets us measure:

  propagator overhead = (propagator time) - (plain time)

for the same workload.

Files:
  benchmarks/comparative/eigentrust-plain.rkt  - run-eigentrust-plain
                                                  + run-eigentrust-plain-fl
  tests/test-eigentrust-plain.rkt              - 9 tests:
    * golden-equality with propagator variants on rat
    * within-tol equality on float
    * panics on non-column-stochastic
    * agreement with propagator variants across k=1..6
  benchmarks/comparative/eigentrust-propagators-scaling.rkt
                                                - extended with
                                                  plain-rat + plain-fl
                                                  columns alongside the
                                                  3 propagator variants

Numbers + observations follow in a separate commit once the bench
finishes.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
Adds plain-rat + plain-fl columns to the scaling table so we can
read off the propagator infrastructure overhead directly. Updates
title from "5-way" to "9-way" comparison (4 surface + 3 propagator
+ 2 plain).

Scaling table (K=4, 30s per-sample timeout, median of 3 runs):

  n      plain-rat   rat-coarse  rat-fine   plain-fl   float
  8        2.74 ms    3.36 ms    4.43 ms    0.03 ms    0.12 ms
  16      33.97 ms   37.05 ms   41.01 ms    0.03 ms    0.14 ms
  32     413.42 ms  455.36 ms  474.43 ms    0.05 ms    0.16 ms
  64       6.10 s     6.37 s     6.41 s     0.09 ms    0.28 ms
  128    TIMEOUT    TIMEOUT    TIMEOUT      0.27 ms    0.57 ms
  256    (skip)     (skip)     (skip)       0.99 ms    2.10 ms
  512    (skip)     (skip)     (skip)       4.59 ms    9.00 ms
  1024   (skip)     (skip)     (skip)      19.40 ms   33.86 ms
  2048   (skip)     (skip)     (skip)      88.37 ms  151.62 ms
  4096   (skip)     (skip)     (skip)     442.14 ms  619.37 ms

Propagator infrastructure overhead = (propagator - plain) / plain:

  n      rat overhead  float overhead
  8        +23%         +300%
  16        +9%         +367%
  32       +10%         +220%
  64        +4%         +211%
  128        -          +111%
  256        -          +112%
  512        -           +96%
  1024       -           +75%
  2048       -           +72%
  4096       -           +40%

Two distinct stories:
- For rat: overhead is 4-23% and shrinks fast as n grows. By n=64
  the propagator version is within 4% of plain — the bigint
  arithmetic dwarfs CHAMP cell ops.
- For float: 4x slower at n=8 (300% overhead, 0.12ms vs 0.03ms),
  converging to +40% at n=4096. The per-iteration constant cost
  (cell allocation, BSP round dispatch) is many multiples of an
  8x8 mat-vec but amortizes as per-fire work climbs.

Absolute terms: ~177ms of propagator overhead per call at n=4096
(619 - 442 ms), most of it the BSP scheduler doing K=4 rounds of
fire/snapshot/merge on cells holding large flvectors. CHAMP
path-copy on each write is the likely dominant term.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
… future Prologos network)

User feedback: drop Nat/Rat from comparison analysis (we want
floats and similar types). Reorganize around the actual axes that
matter:

  - math          : algorithm in plain Racket
  - network       : Racket on Prologos's propagator network
  - Prologos math : surface language through reducer
  - (Prologos network: future, doesn't exist yet)

Replace the 9-way comparison with a 4-axis frame using only float-
typed representatives (Racket flonums + Prologos Posit32). The
rat-flavored variants are now an appendix as correctness-
verification tools at small n.

Headline numbers (W3, n=4):

  Axis             reduce_ms      vs math
  math (plain-fl)    ~0.03 ms        1x
  network (float)     0.10 ms       ~3x  (~70 µs of network ceremony)
  Prologos math    17 990 ms   ~600 000x  (reducer overhead + O(k^2))

Scaling (math vs network at large n, only float-typed):

  n        math      network   network overhead
  8        0.03 ms   0.12 ms   +300 %
  64       0.09 ms   0.28 ms   +211 %
  256      0.99 ms   2.10 ms   +112 %
  1024    19.40 ms  33.86 ms    +75 %
  4096   442.14 ms 619.37 ms    +40 %

Net: the propagator network adds a roughly constant ~177 ms of
absolute overhead per call at n=4096, asymptoting to ~40 % of the
math cost as n grows. The 6-order gap between math and Prologos
math is the reducer, not the network -- which is the most
important data point for the future "Prologos network" axis: a
surface Prologos that compiles to a propagator network would
inherit the network's +40-75 % profile, not the reducer's 6-order
multiplier.

The rat exploration is preserved in code/tests but moved to an
appendix in the doc; the variants stay useful for golden-equality
testing at small n.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
claude added 3 commits May 1, 2026 03:09
Add eigentrust-list-posit-w3only.prologos containing the same defns +
fixtures as eigentrust-list-posit.prologos but with only the W3
workload as a top-level expression. This removes the W1/W2 reduce
contributions from the surface-variant headline number.

Pure W3 reduce_ms (List + Posit32, k=4, n=4): 15 047 ms
(was 17 990 ms when W1+W2+W3 reduce times were summed). The
math-vs-Prologos-math gap drops from ~600 000× to ~500 000×.

Note that reduce_ms already excluded elaboration / type-check / qtt /
zonk / trait-resolve before this change — those phases are reported
separately by tools/bench-phases.rkt. The previous number was
inflated by W1+W2 *reduce* time, not by pre-reduce phases.

Update the comparison doc with the cleaner W3-only number, a note on
exactly what reduce_ms measures, and reproduction instructions.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
Regenerated module cache from running bench-phases against the
W3-only fixture. Content-equivalent to the previous cache; diff is
embedded source-mtime + serialized timestamp.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
Add eigentrust-scaling-large.rkt running math + network at n past
the original 4096 cap. Fast O(n²) flvector-only fixture generator
(replacing the list-of-lists scatter pattern that pinned previous
attempts to multi-minute fixture-gen on n>=8192).

New empirical points:
  n= 4096 (extended run):  math   584 ms, network   958 ms,  +64%
  n= 8192:                 math  3016 ms, network  4440 ms,  +47%
  n=16384:                 math 15989 ms, network 20674 ms,  +29%

n=32768 attempted but OOMs the 16 GB host during fixture allocation
(8 GB matrix + still-rooted previous 2 GB + working set drives GC
into thrashing). Documented in-script with instructions to extend
SIZES on a 32+ GB box.

Comparison doc updated with:
- Combined n=8..16384 table (10 prior + 3 extended rows)
- Math doubling-factor analysis (4.64×→5.30× past n=512, cache effects)
- Two-term shared-n² fit:
    math    ≈ 6.18e-5 · n²
    network ≈ 6.18e-5 · n² + 0.230·n − 526
- Breakeven argument: network does math + strictly-positive
  bookkeeping (CHAMP path-copy, BSP dispatch); overhead
  asymptotically → 0 from above as n→∞ but never crosses.
  Predicted overhead at n=32768 is ~11%, n=262144 ~1.4%.
- Three scenarios where network could win (multi-thread BSP,
  incremental, working-set effects) — none apply to the
  measured one-shot single-thread dense workload.

Run-to-run variance at n=4096 (32% on math between two separate
runs) is honestly larger than the model accounts for; both rows
are kept in the table rather than averaged.

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
hierophantos added a commit that referenced this pull request May 1, 2026
…tors

Stage 0/1 research note in the PTF (Propagator Theory Foundations) series.
The hierarchy from free at the top to Boolean at the bottom (plus orthogonal
quantale + residuated enrichments) catalogued per algebraic level — for each
level, what equations hold, what canonical-form algorithms apply, what
propagator-kind capabilities and optimizations become available.

Anchored on the SRE Track 2I Phase 3c (commit d4e8c81, 2026-04-30) bonus
discovery: the type lattice's distributivity status flipped from "refuted"
(Track 2G) to "confirmed" (Phase 3c) under principled per-relation dispatch
because the always-installed `current-lattice-subtype-fn` callback had been
mixing equality+subtype semantics. The note uses this as a worked example
of why the hierarchy posture matters: defensive scaffolding can hide the
true algebraic posture, and the propagator capabilities that follow from
each level depend on getting the posture correct.

Sections:
- The hierarchy (free → SD → modular → distributive → Heyting → Boolean)
- Per-level operational catalog (what each unlocks)
- Orthogonal enrichments (quantale, residuated)
- The distributivity-status flip as worked example
- Connection to UCS dispatch by algebraic class
- Connection to NTT type-level encoding
- Cross-domain bridge composition by level
- Open questions including "track-changes-merge implies re-validate" discipline candidate

Refines and extends Algebraic Embeddings (PTF, 2026-03-28). Companion to
the SRE-side and UCS-side variety/canonical-form notes (2026-04-30).

PTF Master research table updated (entry #2).
Adds eigentrust-propagators-fine-float.rkt — fine-grained per-peer
EigenTrust on flonums (K·n cells, K·n propagators, n independent
per-peer propagators per BSP round). Mirrors the existing fine
rat variant but in flonum so it can compose with the parallel
executors.

Adds eigentrust-parallel-bench.rkt — runs 5 variants across
n=16..1024 to test whether BSP parallelism can close the math →
network gap:
  - math (plain Racket flvector, 1 core)
  - coarse net, sequential (chain, 1 prop/round, 1 core)
  - fine net, sequential (n props/round, 1 core)
  - fine net, parallel-thread (4 cores via Racket-9 threads)
  - fine net, worker-pool (4 cores via persistent pool)

Findings on a 4-core host (median of 3 runs, K=4):

1. BSP parallelism IS working — fine-seq → fine-thread shows
   up to 2.16× speedup at n=256. Worker-pool ≈ parallel-thread.

2. But fine-grained topology's overhead swamps the speedup —
   fine-thread is 290-400× slower than math at every n. Per-peer
   decomposition pays K·n² CHAMP cell reads + K·n cell writes;
   at n=1024 that's ~4M cell ops vs math's 4M flonum ops, so
   cell access dominates per-fire cost.

The architectural bind: coarse topology has no parallel work to
dispatch (strict chain); fine topology has parallel work but the
work-per-fire (~n flonum ops) is too small to amortize per-fire
BSP overhead. Mat-vec-mul is BLAS-2; the regime where
coordination overhead vs flop count is unfavorable.

Comparison doc updated with the full parallel data table, an
analysis of why each variant doesn't win, and a sketch of what
WOULD let BSP-parallelism beat math on this kind of kernel
(coarse topology + parallelism inside the fire function, or much
higher arithmetic intensity per fire than mat-vec gives).

https://claude.ai/code/session_01UrB1yXsd8hzjyXwj8PFiVp
kumavis pushed a commit that referenced this pull request May 4, 2026
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
kumavis pushed a commit that referenced this pull request May 4, 2026
…throughout)

User challenged: "which threading model is appropriate to use both in
and out of native?" The answer is functional — preserve preduce.rkt's
(values cid net) discipline, have the hybrid backend wrap with a unit
sentinel.

Why functional, in-and-out-of-native:
- SH Track 1 deliverable is ".pnet network-as-value" — networks become
  first-class cell values that round-trip
- SH Track 9 (compiler-in-Prologos): compile-expr itself runs natively
  on propagators, with AST-cell input + network-cell output
- Native fire-fns can't side-effect networks they don't hold; they
  must take net as input and produce net' as output
- Side-effecting via current-prop-net is a bring-up convenience that
  becomes a dead-end at the SH endpoint
- The current-bsp-fire-round? #f hack retires when the parameter
  becomes the threaded net itself (in native)

Cost trade-off favors functional too:
- Functional: preduce.rkt unchanged; backend-hybrid wraps with sentinel
- Side-effecting: ~80-call-site flip in preduce.rkt
- Both backends pass through fire-fn closures unchanged (still
  net-threaded)

Plan revisions:
- §2.3 reconciliation: flipped from "side-effecting under the hood"
  to "functional throughout"; added comparison table showing why
  functional fits native + cost is lower today
- §3.1 interface: every primitive accepts and returns net; fire-fns
  unchanged from today (still net → net')
- §3.2 backends: backend-racket uses prop-network struct; backend-
  hybrid uses 'hybrid sentinel; future backend-native uses cell-id
  as net (native dataflow)
- §3.3 compile-expr sketch: structurally identical to today's
  preduce.rkt; only primitive-rename to b-alloc / b-install-fire-once
- §4 rollout: simplified — Phase 2 (interface inversion) eliminated;
  total dropped from 9-11h to 8-10h
- §5 risks: dropped #1 (threading-flip), refined #2 (bot-handling
  via b-read normalization), added #7 (current-bsp-fire-round?
  through FFI verification)
- §9 tracker: 8 phases, this design doc done

Critical implication for the hybrid backend: fire-fns stay net-
threaded, which means make-reduce-fire's compile-and-bridge recursive
compilation (which itself installs more propagators) just works
through the abstract backend without modification.

https://claude.ai/code/session_01Tycs6BWKG58Wo99YVPg6DF
kumavis pushed a commit that referenced this pull request May 4, 2026
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.
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
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
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).
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.

2 participants