Codebase correctness review @ b467f1e (executed): `[head '[…]]` reports "Multiplicity violation", 28/44 examples broken, QTT off for pattern matching, CI compiles interpreted (4,713×)

[kumavis]

Correctness review of the codebase, executed against a live build.

Revision 4. r1 was static-only. Racket 9.0 + deps were then installed, the tree rebuilt with PLT_CS_COMPILE_LIMIT=1000000, and every finding probed against the running system. Tags:

✅ VALIDATED (reproduced) · ❌ RETRACTED (r1 was wrong) · ⚠️ AMENDED · 🆕 NEW (only found by running it)

Base: b467f1e. origin/main re-fetched at validation time — identical, so nothing here was resolved or introduced by intervening work.

Suite status: GREEN. 471 files. A first run reported 3 failures (test-rel-t1-pol, -typed-rows, -typed-vars) but all three were TIMEOUT: file exceeded 120s caused by contention from my own concurrent example sweep — not real. Re-run on an idle machine all three pass (106 / 24 / 24 tests). Reported here for completeness, and because it is itself the point: the suite is green while [head '[1N 2N 3N]] is broken.

Headline: the worst findings were invisible to static review — ordinary stdlib calls fail with a diagnostic naming the wrong subsystem, 28 of 44 example files don't run, and the one test covering the head case is a hollow no-op that reports PASS.

---

🆕 N4. [head '[1N 2N 3N]] reports "Multiplicity violation" — core stdlib broken at the def seam

Found by sweeping the example files. Ordinary code, no exotic nesting:

ns demo
def a := [head '[1N 2N 3N]]         ;; => ERROR: Multiplicity violation
def b := [length '[1N 2N]]          ;; => ERROR: Multiplicity violation
def c := [map [int* _ 2] '[1 2 3]]  ;; => ERROR: Expression is not a valid type

Discriminating cases — exactly the pattern pipeline.md documents:

expression	position	result
def a := [head '[1N 2N 3N]]	infer (def RHS)	❌ Multiplicity violation
defn f [xs] [head xs]	check (defn body)	✅ ok
def c := [fn [xs : <List Nat>] [head xs]]	infer at seam	❌ Multiplicity violation
[tail '[1N 2N 3N]], [foldr int+ 0 '[1 2 3]], [eq? 1N 1N]	—	✅ ok

head fails, tail succeeds — that asymmetry rules out a missing import, and both are :refer'd from prologos::data::list.

Per pipeline.md's own debug rule — "a 'Multiplicity violation' on a def whose body is not a lambda is an un-arm'd node until proven otherwise — check inferQ before believing QTT" — this is almost certainly a missing inferQ arm, not a real QTT violation. It is the live instance of #3, reachable from the most basic list code in the language.

And the test that would catch it is disabled. tests/test-elaboration-parity.rkt:114-118 covers exactly "[head '[1N 2N 3N]]" with #:expected '(Just 1N) — via parity-test-skip, which expands to:

(define-syntax-rule (parity-test-skip tag phase input body ...)
  (test-case (format "[~a] ~a (pending ~a)" tag input phase)
    (void)))          ;; <-- body discarded

That is not a skip — it emits a passing test-case with no assertions. See N5.

---

S1 — Correctness defects

1. ✅ VALIDATED — four AST nodes crash the compiler, from one line of documented syntax

Defined (syntax.rkt:1032-1035), parseable (parser.rkt:3113-3156), elaborated (elaborator.rkt:3234-3269), unhandled downstream:

(process-string "(ns p)\n(solve (all-different ?x ?y ?z))")
;; => match: no matching clause for (expr-all-different '(x y z))
(process-string "(ns p)\n(solve (element ?i (cons 1 nil) ?v))")
;; => match: no matching clause for (expr-element 'i (expr-goal-app 'cons ...) 'v)
(process-string "(ns p)\n(solve (minimize ?c))")
;; => match: no matching clause for (expr-minimize 'c)

Raw Racket exceptions, not language errors. Confirmed at unit level too: subst, shift, zonk each raise on all four.

Stage	Arm?	Fallback	Consequence
substitution.rkt shift/subst	✗	none	crash ✅ reproduced
zonk.rkt zonk	✗	none	crash ✅ reproduced
reduction.rkt nf	✓ wrong	leaf identity	sub-exprs never normalized
typing-core.rkt infer	✗	[_ (expr-error)]	silent type error
qtt.rkt inferQ	✗	[_ (tu-error)]	"Multiplicity violation"
pretty-print.rkt pp-expr	✗	[_ (format "~a" e)]	leaks #(struct:expr-…)
pnet-serialize.rkt	✗	unregistered	vector-impostor ✅ (see #6)

expr-element carries list-val; expr-cumulative carries tasks/capacity. driver.rkt calls freeze (zonk + default-metas, zonk.rkt:1046) on every def body.

Invisible because test-global-constraints-01.rkt tests the solver-side narrow-constraint struct, not the AST nodes; and the two examples using the syntax have it commented out and are never run (#9).

2. ✅ VALIDATED — QTT silently disabled for every pattern-matching definition

contains-unsupported-qtt? (driver.rkt:295-322) returns #t for expr-reduce; both call sites (:1848, :2061) then skip checkQ-top.

Same erasure violation, with and without a match:

;; A. no match -> correctly REJECTED
(def useE <(Pi [x :0 <Nat>] Nat)> (fn [x :0 <Nat>] x))
;; => ERROR: Multiplicity violation

;; B. identical violation, body is a match -> SILENTLY ACCEPTED
(def useM <(Pi [x :0 <Nat>] Nat)>
  (fn [x :0 <Nat>] (match x (zero -> x) (suc n -> x))))
;; => ACCEPTED: "useM : [Pi [x :0 <Nat>] Nat] defined."

An erased variable is used at runtime and accepted. Soundness hole, not a missing feature.

expr-reduce is the target for all match and multi-arity defn dispatch (macros.rkt:9920/:9876 → elaborator.rkt:3346) — per prologos-syntax.md, "the primary dispatch mechanism." Stdlib exposure: 1116 pattern-arm lines across 38 of 157 files, plus 13 using (match.

Root cause: qtt.rkt has zero references to expr-reduce. No arms — so the skip predicate is load-bearing.

3. ✅ RESTORED (via N4) — the skip predicate is non-exhaustive and the lying diagnostic is live

r2 downgraded this for lack of a repro. N4 is the repro. contains-unsupported-qtt? has a [_ #f] catch-all and recurses into only ~15 node kinds, never containers, while inferQ does (qtt.rkt:1479-1488).

Missing inferQ arms for nodes typing-core infers (11, verified): expr-reduce, expr-vcons, expr-vhead, expr-vtail, expr-vnil, expr-vindex, expr-fzero, expr-fsuc, expr-narrow, expr-foreign-fn, expr-Fin.

4. ❌ RETRACTED (smaller real finding inside)

r1 claimed expr-net-new-cell was unregistered. Wrong. It is registered by reg3! at pnet-serialize.rkt:266 and round-trips fine — my static scan matched only reg0!/reg1!/regN!/auto-cache! and missed reg2!/reg3!.

What survives, verified at runtime:

• auto-cache! swallows all exceptions (:358-359), so arity-mismatched calls silently no-op. Dead calls: expr-net-new-cell (:438), expr-net-type (:437), expr-cell-id-type (:442), expr-from-int/from-nat (:430), expr-net-new-cell-widen (:439). All harmless duplicates. Dead code that obscures real gaps.
• Two dead guards — a when whose predicate builds the struct at a stale arity, so the guarded regN! never runs:
  • spec-entry (:327-328): guard uses 6 args, arity is 8 → dead. Harmless; :274 covers it.
  • ctor-meta (:352-353): guard uses 6 args, arity is 5 → dead. Verified absent from the static tag table; survives only via the dynamic cache at :434.

5. ✅ VALIDATED — narrow-subst-bvars silently drops bindings in record field types

narrowing.rkt:952-969 is the SUB.3b fix whose comment claims "the walker cannot silently skip a node kind again." Its walk-list descends only when (struct? (car l)). expr-Record's fields is a list of (cons key record-field) (syntax.rkt:694-697) — pairs, not structs.

(narrow-subst-bvars
  (expr-Record 'keyword (list (cons 'a (record-field (expr-bvar 0) 'present))) 'closed)
  (list (expr-int 99)) 0)
;; field type stays  #(struct:expr-bvar 0)   <-- binding silently dropped
;; control expr-app: #(struct:expr-app #(struct:expr-int 99) #(struct:expr-unit))  <-- ok

Vector- and hash-valued fields are likewise not traversed.

🆕 N1. match inside a container literal leaks an unexpanded surface node at the user

def a := [id (match 0N (zero -> 1N) (suc n -> n))]   ;; control (app arg): ok
def b := '[(match 0N (zero -> 1N) (suc n -> n))]     ;; list literal
def c := {:k (match 0N (zero -> 1N) (suc n -> n))}   ;; map literal
def d := '['[(match 0N (zero -> 1N) (suc n -> n))]]  ;; nested
;; b, c, d => Cannot elaborate: #(struct:surf-match-patterns #(struct:surf-zero
;;            #(struct:srcloc <ws-string> 1 0 12)) (#(struct:match-pattern-arm ...

Root cause: expand-expression (macros.rkt:9392) has 58 surf-* arms, terminates in [_ surf] (:9518), and has zero arms for surf-list-literal, surf-map-literal, surf-pvec-literal, surf-set-literal.

Same [_ e] failure mode as #1 and #5, one stage earlier — and the only one that dumps an internal Racket struct as the user-facing error.

---

S2 — Systemic: the walker problem is structural

6. ✅ VALIDATED (number revised) — 139 of 344 AST nodes fail the .pnet round-trip

Measured by constructing every expr-* node and running deep-struct->serializable → deep-serializable->struct:

expr-* nodes instantiable      : 344
absent from STATIC tag-table   : 274
fail round-trip outright       : 139     <-- returns a RAW VECTOR

(r1's static estimate was 136; live count 139. The dynamic cache rescues 135 of the 274 static misses.)

Writer serializes any struct generically (:126-127); reader rebuilds known tags and otherwise returns the raw vector (:483, [else v]). Confirmed-broken families: the entire relational subsystem (expr-rel, expr-defr, expr-clause, expr-fact-row, expr-guard, expr-not-goal, expr-is-goal, expr-unify-goal, expr-cut, expr-solve/-one/-with), all 14 remaining expr-generic-* nodes, length-indexed vectors, Fin, all quire ops, transients, union-find, tables.

The comment at :354-356 claims the block "populate[s] dynamic-ctor-cache with ALL constructors from syntax.rkt." It doesn't — it's a hand-written list. With auto-cache!'s swallowed failures, coverage is unverifiable at load time.

7. The prescribed structural fix exists in-tree but wasn't applied to the core walkers

pipeline.md § "Exhaustive Walkers" prescribes a generic transparent-struct rebuild as the fallback. Implemented twice — zonk.rkt:1514-1531, narrowing.rkt:952 — but not in shift, subst, zonk, default-metas, pp-expr, infer, inferQ, or expand-expression, which is where #1, #5, and N1 all live.

Highest-leverage fix: every expr-* struct is already #:transparent. Export a constructor registry from syntax.rkt so pnet-serialize enumerates instead of hand-listing (kills #4/#6 permanently), and add a reflective fallback to the core walkers (makes #1/#5/N1 structurally impossible).

---

S3 — CI and test coverage

8. ✅ VALIDATED — both CI workflows compile the compiler interpreted; measured 4,713×

PLT_CS_COMPILE_LIMIT is set only inside run-affected-tests.rkt:49 and bench-ab.rkt:34, via runtime putenv. Both workflows run a separate, earlier raco make driver.rkt in a bare shell (test.yml:25, benchmark.yml:24) without it.

A/B on shift, 2000 iterations over a 200-node term:

build	time
raco make, no limit (what CI does)	344,048 ms
raco make with PLT_CS_COMPILE_LIMIT=1000000	73 ms

4,713× — far worse than the ~830× in testing.md.

The runner cannot rescue it. Simulating CI exactly — bare raco make, then the runner's putenv:

1) bare 'raco make' (no limit)             -> shift x100: 16,500 ms
2) PLT_CS_COMPILE_LIMIT=1000000 raco make  (no rebuild — SHA short-circuit)
                                           -> shift x100: 16,633 ms

No improvement. test.yml runs the whole suite interpreted against a 30-min timeout; benchmark.yml → ci-regression-check.rkt (never sets the variable) measures interpreted timings, so the perf regression gate measures the wrong artifact.

Fix: env: PLT_CS_COMPILE_LIMIT: 1000000 at job level in both workflows.

9. ✅ VALIDATED — only 16 of 44 example/acceptance files run clean

All 44 through process-file, 90s timeout each:

OK 16   |   ERR 21   |   TIMEOUT 4   |   CRASH 3

Unambiguous breakage (caveat: some acceptance files deliberately contain negative cases, so part of the 21 ERRs may be intentional — the crashes, timeouts, and tutorials are not):

file	outcome
map-tutorial-demo.prologos	CRASH — Cannot find module: prologos::core::map-ops
numerics-tutorial-demo.prologos	CRASH — if requires: (if cond then else)…
2026-03-20-first-class-paths.prologos	CRASH — .{ … } not supported, "under redesign"
strings-tutorial-demo.prologos	ERR — Unbound variable
2026-03-28-sudoku-demo.prologos	ERR — solve expects 1 argument, got 16
2026-03-16-track4/5/6-acceptance, 2026-03-18-track7-acceptance	TIMEOUT >90s
2026-04-17-ppn-track4c-adversarial.prologos	ERR — Multiplicity violation → led to N4
2026-07-06-ciu-t6-f1-records, 2026-07-17-…-f1b3/f1b4	ERR (current active track)

All three tutorial demos — the user-facing onboarding material — are broken.

workflow.md mandates "The track isn't done until the acceptance file runs with 0 errors"; testing.md calls Level-3 WS-file validation "the gap that most commonly produces 'works in tests, broken for users'." Only 6 of 44 are referenced by any test, and nothing in CI runs them — which is why #1 and N4 stayed invisible.

10. No round-trip contract test for pnet-serialize

No test-pnet-serialize.rkt. The ~25-line probe that produced #6's numbers is the missing test: for every expr-* constructor, build an instance, round-trip it, assert struct-not-vector.

11. ✅ VALIDATED — the documented pre-push gate doesn't exist in the repo

testing.md:47 documents a .git/hooks/pre-push full-suite gate. tools/git-hooks/ holds only pre-commit and post-commit, and install-git-hooks.sh:53 symlinks only what's there. Absent on a fresh clone.

🆕 N2. The project's own lint gates are RED on main and unwired from CI

Both ship as tooling, both fail now, neither runs in CI (no reference to lint-parameters, lint-cells, or check-parens in .github/workflows/):

$ racket tools/lint-parameters.rkt --strict ; echo $?
  unclassified: 182 (baselined: 180, NEW: 2)
⚠ NEW: current-check-fire-invariants? (propagator.rkt:2229)
       current-residuation-enabled?   (global-env.rkt:67)
1                                     <-- non-zero exit

$ racket tools/lint-cells.rkt
  unregistered: 16 sites, 10 unique merge fns
    NEW (not in baseline): 11 sites, 6 unique
⚠ level-merge, mult-merge, session-merge, type-merge  (meta-universe.rkt:187-193)
  type-unify-or-top  (cap-type-bridge.rkt:197, elaborator-network.rkt:374/377/380,
                      session-type-bridge.rkt:121/131)

Nine are production modules.

🆕 N5. 13 hollow "tests" report PASS while asserting nothing

parity-test-skip (tests/test-elaboration-parity.rkt:101-103) expands to (test-case … (void)) — a passing test case with the body discarded. 13 of the 31 parity tests in that file are hollow, including the one covering N4's [head '[1N 2N 3N]] with the correct #:expected '(Just 1N).

A skipped test that reports green is worse than a missing one: it makes the suite claim coverage it doesn't have.

🆕 N6. PRELUDE manifest and the shipped prelude are out of sync — and CI only warns

tools/run-affected-tests.rkt:519 prints ⚠ PRELUDE DRIFT DETECTED on every run. gen-prelude.rkt --validate shows why:

Generated: 38 import entries from PRELUDE manifest
Current:   40 import entries in namespace.rkt

  DIFF at entry 4:
    generated: (imports [prologos::data::nat :refer [add mult double pred zero? sub pow
                                                     le? lt? gt? ge? nat-eq? min max
                                                     bool-to-nat clamp]])
    current:   (imports [prologos::data::nat :as nat :refer [zero?]])

namespace.rkt additionally ships prologos::core::io and prologos::data::datum, which the manifest does not declare — and all subsequent entries are shifted.

This is semantic, not cosmetic: the manifest (documented as "the single source of truth for the prelude auto-imports") claims 16 Nat functions are in scope unqualified, while what actually ships refers only zero? and puts the rest behind the nat:: alias. Any doc or tutorial written against the manifest is wrong about what's in scope.

The check exists and fires, but run-affected-tests.rkt only printfs — CI passes with the drift in place.

🆕 N7. Three test files exceed the project's own size guideline and time out under any load

testing.md guideline: "Keep test files under ~20 test-cases / ~30s wall time." Measured on an idle machine:

file	test cases	wall
test-rel-t1-pol.rkt	106	>120s under load, passes idle
test-rel-t1-typed-vars.rkt	24	53s
test-rel-t1-typed-rows.rkt	24	~50s

All three pass on an idle machine but exceed the 120s per-file batch limit under moderate parallel load — they are the suite's flake surface. (This is how my first run produced 3 spurious failures.)

🆕 N3. No root README, LICENSE, or CONTRIBUTING

git ls-files finds READMEs only under docs/spec/, docs/tracking/principles/, and tools/git-hooks/ — none at the repo root, and no LICENSE or CONTRIBUTING anywhere. The GitHub landing page is empty; CLAUDE.md is agent-facing, not a human entry point. The repo already takes external contributor PRs (workflow.md § external critique), so the missing license is a real ambiguity.

---

S4 — Documentation defects

12. ✅ CLAUDE.md quick-start commands fail as written. Verified from repo root: tools/run-affected-tests.rkt, tools/bench-ab.rkt, tools/update-deps.rkt do not exist there (they're under racket/prologos/tools/), while tools/install-git-hooks.sh and tools/check-parens.sh do. Two different tools/ directories documented as one.

13. CLAUDE.md hardcodes "/Applications/Racket v9.0/bin/racket" as "the Racket binary on this machine." Wrong on CI, containers, and Linux.

14. ✅ Stale line references. All ten file.rkt:NNN citations in .claude/rules/ re-checked; four materially wrong:

cited	claims	actually at
driver.rkt:2658	current-structural-mult-bridge	3584
propagator.rkt:3153	register-stratum-handler! topology tier	3198 (#:tier at 3242)
propagator.rkt:3213	handler append-order note	an error string
effect-executor.rkt:53	Stratum 3 reference	54

15. stratification.md registration count is stale. Claims "8 production registration sites across [6 files]"; actual is 10 across 7 — sre-core.rkt:2853 is missing.

Verified accurate: the run-stratified-resolution! / run-retraction-stratum! retirement claims hold, and the fire-function-captures-stale-net class is clean in production.

---

Standing hygiene notes

• 2 TODO/FIXME markers in 105K LOC. Genuinely excellent.
• parameter-lint-baseline.txt is 193 lines of accepted debt, plus the live regression in N2.
• 21 production with-handlers sites discard all exn? — the direct cause of the dead registrations in parse-reader: splice multi-line spec continuations so -> stays top-level #4. workflow.md asks "is the guarded condition STRUCTURALLY POSSIBLE?" Here it is, and the guard turns a load-time arity error into corruption arbitrarily far away.

---

Suggested order

1. Fix [head …] / [length …] / [map …] (N4) — core stdlib, wrong diagnostic, one-line repro. Check inferQ before believing QTT, per the project's own rule.
2. Un-skip the 13 parity-test-skip cases (N5) — or make the macro emit a real pending marker instead of a green no-op. This is what let N4 hide.
3. env: PLT_CS_COMPILE_LIMIT: 1000000 in both workflows — one line each; 4,713× on the hot path.
4. Wire lint-parameters --strict + lint-cells into CI (N2), and make the PRELUDE drift check fail rather than warn (N6). All three gates exist and are already red.
5. Run all 44 examples in CI (Add [force e] strict-normalization combinator (eigentrust pitfall #11) #9) and repair the 28 — starting with the three tutorial demos.
6. pnet-serialize round-trip test + make auto-cache! fail loudly (parse-reader: splice multi-line spec continuations so -> stays top-level #4/pretty-print: emit type-applied forms with [T A] syntax (eigentrust pitfall #14) #6).
7. Container arms / reflective fallback in expand-expression (N1) — the only user-visible leak.
8. Reflective fallback in shift/subst/zonk/pp-expr (multi-line spec with comments between tokens confused the preparser #1, Add pvec-zip-with library function (eigentrust pitfalls #13) #5).
9. inferQ arms for the 11 nodes, then delete contains-unsupported-qtt? (Add EigenTrust reputation algorithm: implementation, tests, benchmark #2, Fix CI: rackcheck dep + bench-ppn-track3 stale API #3).
10. Split the three oversized Rel T1 test files (N7); add root README + LICENSE (N3); doc fixes (parse-reader: splice multi-line def := continuations (eigentrust pitfall #15) #12–pvec: add Int-indexed helpers (eigentrust pitfall #12) #15).

---

Validation environment: Racket 9.0 CS on Ubuntu 24.04, raco pkg install --auto, full rebuild with PLT_CS_COMPILE_LIMIT=1000000. Suite: 471 files, green (the 3 apparent failures were self-inflicted contention timeouts — verified by clean re-runs).