You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Part 7 of 9 of a Claude Opus 5 review of MULTI/DEX. This part is a correction to issue #12, plus the supporting scan findings that produce it.
Full write-ups live in REVIEW-FINDINGS.md under the matching ## N. headings — ## 6, ## 30, ## 12, ## 5, ## 10, ## 41, ## 40. Every line number below was re-checked against the current source; where the write-up had drifted, the numbers here are the corrected ones.
The correction
Issue #12 section 1 argues that runLiquidationBatch is "the only uncapped sweep on a fund-safety path", and supports that with an enumeration of the other sweeps as bounded:
That framing is a genuine contribution — it is the right question to ask, and asking it is what made the rest of this issue findable. Three of the five rows do not hold:
tickTier is not bounded. The Shard.step cursor covers exactly one of its four walks — the join-badge backfill at main.mo:6039-6042. The uptime sampler six lines above it (:6010) walks openOrdersByUser in full, and the volume-badge sweep two lines below it (:6044-6045) walks lifetimeVol in full. Both walked maps are monotonic: neither has a production delete path. Findings 6 and 30 below.
tickLeaderboardShard's cursor bounds only one dimension.Shard.step bounds the user dimension to LEADER_SHARD_SIZE = 500 (:9995). Each of those 500 users runs leaderRowFor → accountCrossSection (:10022), which full-scans marginPools. Per-tick cost is O(500 × total pools), and the pool count grows underneath a cursor that never sees it. Finding 12 below.
sweepStaleUserOrders has no per-call cap at all.MAX_PER_CALL does not exist. The constant is EVICT_MAX_PER_CALL = 5 (:1491), and it belongs to evictOverCap (:1541), a different function on a different path. sweepStaleUserOrders (:1495-1520) iterates all of openOrdersByUser and then cancels every stale order it found, with no cap on either loop. This is the same map that finding 6 shows is never pruned.
reapClosedOrders (REAP_SWEEP_CAP = 20_000, :6551/:6564) and the processDeferred / tickHeatmaps rows are correct as stated in #12.
The conclusion that changes is #12's "everything else is bounded", not #12's finding about runLiquidationBatch, which stands.
Severity framing — read this before triaging
None of these is a correctness or value defect, and none is demonstrated to trap today. They are scalability and cycle-burn defects. No user loses funds, no accounting is wrong, no invariant is violated. What they establish is that the per-message cost of several heartbeat subtasks is proportional to a lifetime-cumulative quantity rather than to a live one, so today's comfortable margin is not evidence about next season's.
The value of this issue is the correction itself. If tickTier is on the "already bounded" list, nobody re-measures it.
Growth terms, since that is the whole argument:
finding
walked structure
grows in
6
openOrdersByUser
all-time principals that ever rested an order
30
lifetimeVol
all-time scorecard keys that ever settled a fill
12
marginPools
total margin pools across all owners (64/principal, no delete)
5
deferredExecs + deferredSwaps
global staged-queue depth
10
state.balances
registered users × registry tokens
41
poolPositions
all-time (pool, market) pairs ever traded
40
counterpartyStats
lifetime distinct counterparty principals
1. Finding 6 — openOrdersByUser is never pruned, so tickTier walks every principal that ever traded
The asymmetry
removeFromOpenIndexes (src/backend/lib/OrderBook.mo:205-248) maintains two indexes in one function. It prunes one and not the other.
The price-level index, :213-233:
// Price-level index — remove the id and prune the level if now empty// (so minEntry/maxEntry never land on an empty price)....ignoreMap.delete(lvl, Nat.compare, order.id);
if (Map.size(lvl) ==0) {
ignoreMap.delete(lvls, Nat.compare, order.price);
} else {
Map.add(lvls, Nat.compare, order.price, lvl);
};
No if (Map.size(s) == 0). The now-empty set is written back under userKey, and the key survives.
The in-function asymmetry is the strongest evidence this is unintended. The author knew empty containers had to be pruned — they wrote the prune, with a comment explaining why — and did not carry the same treatment across to the sibling index in the same function.
Consumers
Two heartbeat subtasks iterate this map in full:
main.mo:6010, inside tickTier: for ((k, _) in Map.entries(orderStore.openOrdersByUser)) { List.add(quoters, k) }, then sampleUptime on every collected key. tickTier runs every 60 s, synchronously, inside the heartbeat at :6174.
For each dead key, sampleUptime (:6053) runs Principal.fromText, isInternalPrincipal, scorecardKeyOf (another Principal.toText plus map reads), finds zero resting orders, and records a FAIL uptime sample. That creates a fresh uptimeStats entry for a principal with no orders, accumulates fails, gets pruned at the 20-sample floor, and is recreated on the next tick — churn, not just cost, and it contradicts the map's stated invariant that it tracks live or recent quoters.
Reclamation
There is none on any automatic path. The only removal of a user key anywhere is Map.clear(store.openOrdersByUser) inside OrderBook.rebuildIndexes (OrderBook.mo:257), reachable only from adminRebuildIndexes (main.mo:6729-6738), which is controller-gated and deliberately not wired into upgrade — the comment immediately above it (:6720-6728) explains that choice, noting the rebuild can itself exceed the instruction limit on large state and that this is survivable precisely because an operator invokes it rather than every user's first post-upgrade call. That reasoning is sound. The consequence is that nothing reclaims these keys in normal operation.
Proof
Run from the repository root:
MOC=$(mops toolchain bin moc | tail -1)
$MOC $(mops sources) --implicit-package=core -r proofs/h6-openordersbyuser-never-pruned.mo
This drives the real OrderBook.createOrder / OrderBook.cancelOrder — no mock, no reimplementation of the index logic. Verbatim output:
orders placed and then cancelled : 5
open orders remaining : 0
--- price-level index (pruned at OrderBook.mo:225-226) ---
levels retained OBSERVED 0 CORRECT 0
--- per-user index (NOT pruned, OrderBook.mo:236-244) ---
user keys retained OBSERVED 5 CORRECT 0
of which hold an EMPTY id-set: 5
every heartbeat sweep (main.mo:1498, main.mo:6010) walks all 5 of these dead keys; CORRECT walk length is 0
BUG REPRODUCED: price level pruned to 0, but 5 empty openOrdersByUser entries survive forever (asymmetric prune)
Both indexes see identical traffic — five principals, one order each, same market-side, same price, all cancelled. The price level goes to zero. The user index keeps all five keys, each holding an empty set. The proof's inline references to OrderBook.mo:225-226 and :236-244 are one line off the current source; the correct lines are :224-225 and :235-243.
Source, for the record:
// H6: removeFromOpenIndexes prunes the emptied PRICE LEVEL (OrderBook.mo:225-226)// but never prunes the emptied PER-USER entry (OrderBook.mo:236-244).// Every principal that ever rested an order stays a key in openOrdersByUser// forever -> main.mo:1498 and main.mo:6010 walk it on every heartbeat.importMap"mo:core/Map";
importNat"mo:core/Nat";
importNat8"mo:core/Nat8";
importText"mo:core/Text";
importBlob"mo:core/Blob";
importDebug"mo:core/Debug";
importPrincipal"mo:core/Principal";
importRuntime"mo:core/Runtime";
importOrderBook"../src/backend/lib/OrderBook";
let store =OrderBook.emptyStore();
letMKT="ICP/USD";
letPRICE : Nat=1_000_000;
letN : Nat=5;
// N distinct principals each rest one buy order at the SAME price, then cancel it.var i : Nat=0;
while (i <N) {
let p =Principal.fromBlob(Blob.fromArray([1, 2, 3, Nat8.fromNat(i)]));
let o =OrderBook.createOrder(store, MKT, p, #buy, #limit, PRICE, 1000, 1000+ i);
ignoreOrderBook.cancelOrder(store, o.id);
i +=1;
};
// Price-level index for that market-side after all cancels.let msKey =OrderBook.marketSideKey(MKT, #buy);
let levelCount =switch (Map.get(store.levelsByMarketSide, Text.compare, msKey)) {
casenull { 0 };
case (?lvls) { Map.size(lvls) };
};
// Per-user index after all cancels: keys retained, and how many are empty.let userKeys =Map.size(store.openOrdersByUser);
var emptyUserKeys : Nat=0;
for ((_, idSet) inMap.entries(store.openOrdersByUser)) {
if (Map.size(idSet) ==0) { emptyUserKeys +=1 };
};
(The remainder is the Debug.print reporting and the pass/fail assertion shown above.)
Growth term
All-time principals that ever rested an order. Not active quoters, not registered users — every principal that ever placed and closed a single order, forever, plus every simulation bot.
Suggested direction
Mirror the level index: after the delete, if (Map.size(s) == 0) { ignore Map.delete(store.openOrdersByUser, Text.compare, userKey) } else { Map.add(...) }. That is the whole fix for new state. Pre-existing dead keys will persist until an operator runs adminRebuildIndexes, so it is also worth skipping empty id-sets in the tickTier quoter loop so those keys stop generating spurious fail samples in the interim.
2. Finding 30 — the volume-badge sweep is the second unsharded walk in the same message
Findings 6 and 30 are two legs of one argument: tickTier is not bounded. Presenting them separately would understate it, because they are additive within a single heartbeat message.
The contrast
tickTier ends with these four lines (main.mo:6039-6045):
let br =Shard.step<Bool>(registeredUsers, _tierBadgeCursor, TIER_BADGE_SHARD_SIZE, func(k) {
if (not hasBadge(k, BADGE_JOIN)) { awardBadge(k, BADGE_JOIN, now) };
});
_tierBadgeCursor :=if (br.completed) { null } else { br.nextCursor };
let volKeys =List.empty<Text>();
for ((k, _) inMap.entries(lifetimeVol)) { List.add(volKeys, k) };
for (k inList.values(volKeys)) { checkVolumeBadges(k, now) };
The first walk is sharded at TIER_BADGE_SHARD_SIZE = 2_000 (:5989), under a header comment (:5984-5988) that states the reason explicitly:
// The join-badge backfill inside walks ALL registered users, so it is SHARDED
// (Shard.step, like the leaderboard) to keep the per-tick cost bounded as the
// registry grows.
The second walk, on the immediately following line, materialises the entire key set of lifetimeVol into a list and calls checkVolumeBadges on every one. Same message, same tick, no cursor.
Why the map only grows
lifetimeVol (:678) is written by mapBump at :790, inside bumpPartyVolume — the production fill path. There is no decrement and no delete. The only Map.clear(lifetimeVol) is at :14035, inside the admin reset. Its sibling declaration comment describes the class as lifetime and monotonic, which is what the design intends; the problem is only that a monotonic map is being walked at a fixed cadence.
Per key, checkVolumeBadges (:915-924) does two lifetime-map reads plus up to six hasBadge lookups, each an outer and inner map get — roughly eight ordered-map operations, times every all-time trader, every 60 s.
One correction to how this is often framed
It is tempting to say the sweep is redundant because badges are awarded inline on fills. They are not.checkVolumeBadges has exactly three call sites: this sweep (:6045), and setTestScorecard at :5032 — which is a controller-gated, IS_DEV-gated test hook (:5019-5021) that also feeds lifetimeVol at :5029 and is unreachable in play or production posture. The production fill path never calls it. So the sweep cannot simply be deleted; it is the only thing that awards volume badges at all.
The redundancy is real but narrower: a key whose lifetime volume has not changed since the previous tick cannot newly cross a threshold, so the overwhelming majority of the eight-operation check is wasted on unchanged keys. The natural fix is to award at bump time — bumpPartyVolume already has the exact key in hand and the per-batch key set is tiny — and keep a sharded sweep only as an idempotent backfill. Failing that, shard this walk with the Shard.step machinery sitting on the line above; badge awarding is idempotent, so no staging is needed.
Growth term
All-time scorecard keys that ever settled a fill.
Cross-reference
Findings 6 and 30 both land inside the subtask set issue #5 item 7 already flags: tickTier and sweepStaleUserOrders as unisolated synchronous heartbeat subtasks with no summed budget. #5 item 7 identified the structural exposure — a trap in any one subtask takes the whole heartbeat down, and nothing sums their costs. These two findings supply the specific unbounded terms that make that exposure quantitative rather than theoretical. They should be triaged together.
3. Finding 12 — no owner index on marginPools; the leaderboard shard bounds only the user dimension
The scan
accountCrossSection (:9840) walks every margin pool in existence to find the ones belonging to one user (:9853-9867):
for ((id, pool) inMap.entries(marginPools)) {
if (Principal.equal(pool.owner, user)) {
nPools +=1;
let poolP = poolPrincipalOf(id);
BorrowEngine.accrueAll(loans, poolP, now);
...
selfAndOwnedPools (:11497-11504) does the same:
// Bounded by the per-owner pool cap.func selfAndOwnedPools(user : Principal) : [Principal] {
let out =List.empty<Principal>();
List.add(out, user);
for ((id, pool) inMap.entries(marginPools)) {
if (Principal.equal(pool.owner, user)) { List.add(out, poolPrincipalOf(id)) };
};
The comment at :11496 — "Bounded by the per-owner pool cap" — describes the result size. The iteration is over every owner's pools. That distinction is the whole finding.
Why the shard does not save it
tickLeaderboardShard (:10062) calls Shard.step over registeredUsers with LEADER_SHARD_SIZE = 500 (:9995), and for each of those 500 keys runs leaderRowFor (:10001), which calls accountCrossSection at :10022. So per tick:
The cursor bounds the user dimension. The pool dimension is inside the loop body and grows independently. This is the precise sense in which #12's "tickLeaderboardShard → lib/Shard.mo cursor" row is incomplete: the cursor is real and it does bound something, just not the term that grows.
The header comment at :9986-9989 shows the reasoning that produced the current design — "valuation (accountCrossSection) is O(tokens + pools), so the full walk is …" — and sharding the outer walk follows correctly from it. The premise is what drifted: accountCrossSection is O(tokens + all pools), not O(tokens + this user's pools).
This is an update-path heartbeat, so the instructions are replicated. That is what separates it from the getMy* query call sites of the same scan, where a full walk is query-node CPU and comfortably within query limits.
Growth term and its driver
Total margin pools across all owners. Issue #5 item 3 supplies the driver: marginPools has no delete path and each principal may hold 64 pools, so the map is monotonic in cumulative participation. Finding 12 is what that growth costs once it is multiplied by 500 per tick. The two should be read together — #5 item 3 explains why |marginPools| never comes down; this explains why that matters on a replicated path.
Suggested direction
The reverse index already exists in the other direction — poolByPrincipal (:3535), maintained at both pool-creation sites — and ownerPoolCount (:3543) already counts pools per owner but is not enumerable. Adding poolIdsByOwner : Map<Text, Map<Nat, Bool>> at the same two choke points that maintain ownerPoolCount makes accountCrossSection and selfAndOwnedPools O(pools owned by this user), and the leaderboard tick genuinely bounded.
4. Finding 5 — softLockedReserved is an unindexed scan inside every health computation
The scan
main.mo:1100-1109:
func softLockedReserved(user : Principal, token : Types.TokenId) : Nat {
var sum : Nat=0;
for ((_, d) inMap.entries(deferredExecs)) {
if (Principal.equal(d.owner, user) and d.reservedTok == token) { sum += d.reservedAmt };
};
for ((_, s) inMap.entries(deferredSwaps)) {
if (Principal.equal(s.owner, user) and s.sellToken == token) { sum += s.amount };
};
sum;
};
Two full scans of the global staged maps, to answer a question about one user and one token.
The comment
:1099, the last line of the header block: O(staged entries) — small.
That is true only while the global staged count stays small. STAGED_CAP_PER_OWNER = 32 (:728) bounds one owner's contribution and does nothing to the scan length, which is over the whole map. The shed thresholds in the two lines below it — SHED_SOFT_STAGED = 2_000 (:729) and SHED_HARD_STAGED = 5_000 (:730) — are the design's own statement of how large that map is expected to get. The comment predates them.
The fan-out
softLockedReserved is not called directly by callers; it is baked into the ReservedLookup closure at :1120-1121:
transientlet reservedBalance : (Principal, Types.TokenId) ->Nat=func(p, t) { let g = getReserved(p, t); let s = softLockedReserved(p, t); if (g > s) { g - s } else { 0 } };
That closure is handed to MarginEngine.valuations, which invokes it once per entry in MARGIN_COLLATERAL_TOKENS (MarginEngine.mo:62-63):
for (token inTypes.MARGIN_COLLATERAL_TOKENS.vals()) {
let bal =Accounts.getBalance(accounts, user, token) + reserved(user, token);
BorrowEngine.getHealth calls valuations, and reservedBalance is threaded into every getHealth, liquidation, and margin-gate call site in the file. So a single health check costs one full pair of staged-map scans per collateral token, and health checks are on the placement path, the release path, the liquidation path, and the query path alike.
Premise
The staged-depth numbers come from issue #6 item 6 — 2,080 entries per owner reachable, against SHED_HARD_STAGED = 5000. This issue does not re-derive them and does not need to; it takes them as given and observes that the per-owner cap #6 discusses does not bound this scan, because this scan is global.
Growth term
Global staged-queue depth, at the moment the venue is busiest — which is exactly when health checks are most frequent.
The trap outcome on the liquidation batch is already #12's finding, and #12's sharding fix would bound per-message work without removing this helper's cost. The two fixes are complementary. What is new here is the cost model: per-health-check cost is proportional to global staged-queue depth, a dimension #12's measurements do not contain, and it degrades single-user paths (openPosition, borrow, health queries) that the batch fix never touches.
Suggested direction
An incremental per-(owner, token) aggregate, mirroring the stagedCountByOwner pattern already in the file at :814-825 and the reservedBalances ledger (map at :224, addReserved / subReserved at :1052-1067). Bump on stage, decrement at every removal site that already calls subReserved, and the helper becomes an O(log n) read.
5. Finding 10 — getUserBalances walks the entire global balance ledger
The scan
src/backend/lib/Accounts.mo:63-75:
publicfunc getUserBalances(state : AccountState, user : Principal) : [(Types.TokenId, Nat)] {
let prefix =Principal.toText(user) # "#";
let results =Map.empty<Text, Nat>();
for ((key, bal) inMap.entries(state.balances)) {
if (Text.startsWith(key, #text prefix)) {
let token = textAfter(key, Text.size(prefix));
if (bal >0) {
Map.add(results, Text.compare, token, bal);
};
};
};
Iter.toArray(Map.entries(results));
};
Every "principal#token" key in the exchange, for all users, with a Text.startsWith per entry, to return the handful of pairs belonging to one caller. AccountState carries no per-user index.
Being precise about the hot caller
The caller worth naming is main.mo:8262, inside getMarketChanges — the frontend's delta-poll endpoint. It is important not to overstate this. The call sits inside a version gate at :8259:
So it fires when the caller's own state changed — after a fill, an order event, a deposit — not on every 2 s tick. An idle poller never reaches the line. Any characterisation of this as "a full ledger scan every two seconds per client" is wrong.
It is also not attacker-controlled. N is bounded by (registered users × registry tokens), and the open faucet is disabled outside dev (:8170, not IS_DEV, // faucetDisabled — the open faucet is dev-only), so an attacker cannot cheaply inflate the ledger's row count. Both call sites are non-replicated queries.
This is a scalability defect, not an availability threat. It should be triaged as latency and query-node CPU that degrade linearly with the exchange's lifetime user count, including for a wallet holding a single token. It should not be triaged as a denial-of-service vector.
One further note worth checking against the docs: docs/security-review.md:137 lists getUserBalances among the O(total) scans under L3 and marks the class fixed on the strength of the per-user secondary indexes that landed with the order-book scaling work. Those indexes went into OrderBook. Accounts did not get any.
Optional proof
bash proofs/h10-getuserbalances-full-scan.sh measures the scan across three ledger sizes and reports a clean linear scaling ratio. If you run it: it executes under the moc interpreter, so only the ratio is meaningful — the absolute timings are interpreter timings and bear no relation to replica instruction counts.
Growth term
Registered users × registry tokens. setBalance also stores zero balances and rows are never deleted, so the map retains every (user, token) pair ever touched.
Suggested direction
state.balances is an orderedText map, so one user's keys are already contiguous under the "principal#" prefix. Seeking to the first key ≥ prefix and iterating until the prefix stops matching is O(log n + k) and needs no new state.
Novelty
No existing issue touches Accounts.getUserBalances. This one is not a correction to anything.
6. Findings 41 and 40 — two more unindexed maps, briefly
Finding 41 — poolPositions has no per-pool index. Four sites full-scan it, and two are on the update path. reconcilePoolPositions (:4488) walks every position record of every pool after each liquidation, filtering on pos.poolId == poolId. openPosition's isolated-pool guard (:9348) does the same global walk to answer a question about one pool. The rest are queries: previewOpenPosition (:9512, which the UI can hit on every ticket edit) and getMyPositions (:10108). The keys already cluster — posKey is "poolId#marketId" (:3666) — so a pool holds at most |markets| entries, and every lookup pays for all pools'. Unlike the heatmap scans, which are capped by HEAT_MAX_POOLS, these have no cap. Growth term: all-time (pool, market) pairs ever traded — worse than open positions, because the normal close path re-adds the record even when the fill flattens the position, so size-zero tombstones persist.
Finding 40 — aggregateHostilityBps walks the lifetime counterparty map on every requote of every market.main.mo:1010-1026 iterates all of counterpartyStats filtering on a one-hour window, with no cache. It is called at :1980, inside ammRequote (:1935), which fires per pool from the 2 s AMM tick and from event-driven price refreshes. The result is market-independent — a single global Float — yet it is recomputed once per market per tick. counterpartyStats (:646) is keyed by counterparty principal (:985, Principal.toText(counterparty)), not by pair, so it gains an entry per principal that ever fills and is never pruned; the only clear is resetExchange (:13940). Stale entries cost one comparison each rather than full arithmetic, which caps the per-entry constant but not the linear term. Growth term: lifetime distinct counterparty principals (per season, since the reset clears it). The cheapest partial fix is to compute it once per tickAmm and reuse it across markets, which removes the per-market multiplier for free.
Finding 6 is the cheapest fix in this issue — a size check and a delete, mirroring code twenty lines up in the same function — and it removes both a growth term and a source of spurious FAIL uptime samples. It has a reproducing proof against the real OrderBook.
Nothing here is urgent in the sense of "today". Everything here is urgent in the sense of "the cost model does not have a ceiling, and the current numbers are not evidence that it does".
Found and verified with Claude Opus 5. Line numbers re-checked against the current source; where REVIEW-FINDINGS.md or the proof comments had drifted, the corrected numbers are used above and the drift is called out inline.
Getting the proof scripts. The proofs/ paths referenced above are not in this repository — they ship separately, so nothing is added to your tree. All of them are here:
Verified end to end from a clean checkout. The scripts are read-only: they compile and read the product source, modify nothing, and contain no fixes. Each prints the observed value alongside the correct one, exits 0 with BUG REPRODUCED: while the defect is present, and flips to exit 1 once it is fixed. The gist README maps every proof to its issue and also includes the proofs for candidates that were investigated and not filed.
Part 7 of 9 of a Claude Opus 5 review of MULTI/DEX. This part is a correction to issue #12, plus the supporting scan findings that produce it.
Full write-ups live in
REVIEW-FINDINGS.mdunder the matching## N.headings —## 6,## 30,## 12,## 5,## 10,## 41,## 40. Every line number below was re-checked against the current source; where the write-up had drifted, the numbers here are the corrected ones.The correction
Issue #12 section 1 argues that
runLiquidationBatchis "the only uncapped sweep on a fund-safety path", and supports that with an enumeration of the other sweeps as bounded:reapClosedOrdersREAP_SWEEP_CAPsweepStaleUserOrdersMAX_PER_CALLtickTier/tickLeaderboardShardlib/Shard.mocursorprocessDeferredlimittickHeatmapsMAX_POOLSThat framing is a genuine contribution — it is the right question to ask, and asking it is what made the rest of this issue findable. Three of the five rows do not hold:
tickTieris not bounded. TheShard.stepcursor covers exactly one of its four walks — the join-badge backfill atmain.mo:6039-6042. The uptime sampler six lines above it (:6010) walksopenOrdersByUserin full, and the volume-badge sweep two lines below it (:6044-6045) walkslifetimeVolin full. Both walked maps are monotonic: neither has a production delete path. Findings 6 and 30 below.tickLeaderboardShard's cursor bounds only one dimension.Shard.stepbounds the user dimension toLEADER_SHARD_SIZE = 500(:9995). Each of those 500 users runsleaderRowFor → accountCrossSection(:10022), which full-scansmarginPools. Per-tick cost is O(500 × total pools), and the pool count grows underneath a cursor that never sees it. Finding 12 below.sweepStaleUserOrdershas no per-call cap at all.MAX_PER_CALLdoes not exist. The constant isEVICT_MAX_PER_CALL = 5(:1491), and it belongs toevictOverCap(:1541), a different function on a different path.sweepStaleUserOrders(:1495-1520) iterates all ofopenOrdersByUserand then cancels every stale order it found, with no cap on either loop. This is the same map that finding 6 shows is never pruned.reapClosedOrders(REAP_SWEEP_CAP = 20_000,:6551/:6564) and theprocessDeferred/tickHeatmapsrows are correct as stated in #12.The conclusion that changes is #12's "everything else is bounded", not #12's finding about
runLiquidationBatch, which stands.Severity framing — read this before triaging
None of these is a correctness or value defect, and none is demonstrated to trap today. They are scalability and cycle-burn defects. No user loses funds, no accounting is wrong, no invariant is violated. What they establish is that the per-message cost of several heartbeat subtasks is proportional to a lifetime-cumulative quantity rather than to a live one, so today's comfortable margin is not evidence about next season's.
The value of this issue is the correction itself. If
tickTieris on the "already bounded" list, nobody re-measures it.Growth terms, since that is the whole argument:
openOrdersByUserlifetimeVolmarginPoolsdeferredExecs+deferredSwapsstate.balancespoolPositions(pool, market)pairs ever tradedcounterpartyStats1. Finding 6 —
openOrdersByUseris never pruned, sotickTierwalks every principal that ever tradedThe asymmetry
removeFromOpenIndexes(src/backend/lib/OrderBook.mo:205-248) maintains two indexes in one function. It prunes one and not the other.The price-level index,
:213-233:The user index, twenty lines later at
:235-243:No
if (Map.size(s) == 0). The now-empty set is written back underuserKey, and the key survives.The in-function asymmetry is the strongest evidence this is unintended. The author knew empty containers had to be pruned — they wrote the prune, with a comment explaining why — and did not carry the same treatment across to the sibling index in the same function.
Consumers
Two heartbeat subtasks iterate this map in full:
main.mo:6010, insidetickTier:for ((k, _) in Map.entries(orderStore.openOrdersByUser)) { List.add(quoters, k) }, thensampleUptimeon every collected key.tickTierruns every 60 s, synchronously, inside the heartbeat at:6174.main.mo:1498, insidesweepStaleUserOrders— the sweep Menese DeFi Team evaluation, Part 3: the liquidation path — one new reproduced finding, and a cross-report synthesis with OhShii Labs (#4–#11) #12 lists as capped, which as noted above is not capped.For each dead key,
sampleUptime(:6053) runsPrincipal.fromText,isInternalPrincipal,scorecardKeyOf(anotherPrincipal.toTextplus map reads), finds zero resting orders, and records a FAIL uptime sample. That creates a freshuptimeStatsentry for a principal with no orders, accumulates fails, gets pruned at the 20-sample floor, and is recreated on the next tick — churn, not just cost, and it contradicts the map's stated invariant that it tracks live or recent quoters.Reclamation
There is none on any automatic path. The only removal of a user key anywhere is
Map.clear(store.openOrdersByUser)insideOrderBook.rebuildIndexes(OrderBook.mo:257), reachable only fromadminRebuildIndexes(main.mo:6729-6738), which is controller-gated and deliberately not wired into upgrade — the comment immediately above it (:6720-6728) explains that choice, noting the rebuild can itself exceed the instruction limit on large state and that this is survivable precisely because an operator invokes it rather than every user's first post-upgrade call. That reasoning is sound. The consequence is that nothing reclaims these keys in normal operation.Proof
Run from the repository root:
This drives the real
OrderBook.createOrder/OrderBook.cancelOrder— no mock, no reimplementation of the index logic. Verbatim output:Both indexes see identical traffic — five principals, one order each, same market-side, same price, all cancelled. The price level goes to zero. The user index keeps all five keys, each holding an empty set. The proof's inline references to
OrderBook.mo:225-226and:236-244are one line off the current source; the correct lines are:224-225and:235-243.Source, for the record:
(The remainder is the
Debug.printreporting and the pass/fail assertion shown above.)Growth term
All-time principals that ever rested an order. Not active quoters, not registered users — every principal that ever placed and closed a single order, forever, plus every simulation bot.
Suggested direction
Mirror the level index: after the delete,
if (Map.size(s) == 0) { ignore Map.delete(store.openOrdersByUser, Text.compare, userKey) } else { Map.add(...) }. That is the whole fix for new state. Pre-existing dead keys will persist until an operator runsadminRebuildIndexes, so it is also worth skipping empty id-sets in thetickTierquoter loop so those keys stop generating spurious fail samples in the interim.2. Finding 30 — the volume-badge sweep is the second unsharded walk in the same message
Findings 6 and 30 are two legs of one argument:
tickTieris not bounded. Presenting them separately would understate it, because they are additive within a single heartbeat message.The contrast
tickTierends with these four lines (main.mo:6039-6045):The first walk is sharded at
TIER_BADGE_SHARD_SIZE = 2_000(:5989), under a header comment (:5984-5988) that states the reason explicitly:The second walk, on the immediately following line, materialises the entire key set of
lifetimeVolinto a list and callscheckVolumeBadgeson every one. Same message, same tick, no cursor.Why the map only grows
lifetimeVol(:678) is written bymapBumpat:790, insidebumpPartyVolume— the production fill path. There is no decrement and no delete. The onlyMap.clear(lifetimeVol)is at:14035, inside the admin reset. Its sibling declaration comment describes the class as lifetime and monotonic, which is what the design intends; the problem is only that a monotonic map is being walked at a fixed cadence.Per key,
checkVolumeBadges(:915-924) does two lifetime-map reads plus up to sixhasBadgelookups, each an outer and inner map get — roughly eight ordered-map operations, times every all-time trader, every 60 s.One correction to how this is often framed
It is tempting to say the sweep is redundant because badges are awarded inline on fills. They are not.
checkVolumeBadgeshas exactly three call sites: this sweep (:6045), andsetTestScorecardat:5032— which is a controller-gated,IS_DEV-gated test hook (:5019-5021) that also feedslifetimeVolat:5029and is unreachable in play or production posture. The production fill path never calls it. So the sweep cannot simply be deleted; it is the only thing that awards volume badges at all.The redundancy is real but narrower: a key whose lifetime volume has not changed since the previous tick cannot newly cross a threshold, so the overwhelming majority of the eight-operation check is wasted on unchanged keys. The natural fix is to award at bump time —
bumpPartyVolumealready has the exact key in hand and the per-batch key set is tiny — and keep a sharded sweep only as an idempotent backfill. Failing that, shard this walk with theShard.stepmachinery sitting on the line above; badge awarding is idempotent, so no staging is needed.Growth term
All-time scorecard keys that ever settled a fill.
Cross-reference
Findings 6 and 30 both land inside the subtask set issue #5 item 7 already flags:
tickTierandsweepStaleUserOrdersas unisolated synchronous heartbeat subtasks with no summed budget. #5 item 7 identified the structural exposure — a trap in any one subtask takes the whole heartbeat down, and nothing sums their costs. These two findings supply the specific unbounded terms that make that exposure quantitative rather than theoretical. They should be triaged together.3. Finding 12 — no owner index on
marginPools; the leaderboard shard bounds only the user dimensionThe scan
accountCrossSection(:9840) walks every margin pool in existence to find the ones belonging to one user (:9853-9867):selfAndOwnedPools(:11497-11504) does the same:The comment at
:11496— "Bounded by the per-owner pool cap" — describes the result size. The iteration is over every owner's pools. That distinction is the whole finding.Why the shard does not save it
tickLeaderboardShard(:10062) callsShard.stepoverregisteredUserswithLEADER_SHARD_SIZE = 500(:9995), and for each of those 500 keys runsleaderRowFor(:10001), which callsaccountCrossSectionat:10022. So per tick:The cursor bounds the user dimension. The pool dimension is inside the loop body and grows independently. This is the precise sense in which #12's "
tickLeaderboardShard→lib/Shard.mocursor" row is incomplete: the cursor is real and it does bound something, just not the term that grows.The header comment at
:9986-9989shows the reasoning that produced the current design — "valuation (accountCrossSection) is O(tokens + pools), so the full walk is …" — and sharding the outer walk follows correctly from it. The premise is what drifted:accountCrossSectionis O(tokens + all pools), not O(tokens + this user's pools).This is an update-path heartbeat, so the instructions are replicated. That is what separates it from the
getMy*query call sites of the same scan, where a full walk is query-node CPU and comfortably within query limits.Growth term and its driver
Total margin pools across all owners. Issue #5 item 3 supplies the driver:
marginPoolshas no delete path and each principal may hold 64 pools, so the map is monotonic in cumulative participation. Finding 12 is what that growth costs once it is multiplied by 500 per tick. The two should be read together — #5 item 3 explains why|marginPools|never comes down; this explains why that matters on a replicated path.Suggested direction
The reverse index already exists in the other direction —
poolByPrincipal(:3535), maintained at both pool-creation sites — andownerPoolCount(:3543) already counts pools per owner but is not enumerable. AddingpoolIdsByOwner : Map<Text, Map<Nat, Bool>>at the same two choke points that maintainownerPoolCountmakesaccountCrossSectionandselfAndOwnedPoolsO(pools owned by this user), and the leaderboard tick genuinely bounded.4. Finding 5 —
softLockedReservedis an unindexed scan inside every health computationThe scan
main.mo:1100-1109:Two full scans of the global staged maps, to answer a question about one user and one token.
The comment
:1099, the last line of the header block:O(staged entries) — small.That is true only while the global staged count stays small.
STAGED_CAP_PER_OWNER = 32(:728) bounds one owner's contribution and does nothing to the scan length, which is over the whole map. The shed thresholds in the two lines below it —SHED_SOFT_STAGED = 2_000(:729) andSHED_HARD_STAGED = 5_000(:730) — are the design's own statement of how large that map is expected to get. The comment predates them.The fan-out
softLockedReservedis not called directly by callers; it is baked into theReservedLookupclosure at:1120-1121:That closure is handed to
MarginEngine.valuations, which invokes it once per entry inMARGIN_COLLATERAL_TOKENS(MarginEngine.mo:62-63):BorrowEngine.getHealthcallsvaluations, andreservedBalanceis threaded into everygetHealth, liquidation, and margin-gate call site in the file. So a single health check costs one full pair of staged-map scans per collateral token, and health checks are on the placement path, the release path, the liquidation path, and the query path alike.Premise
The staged-depth numbers come from issue #6 item 6 — 2,080 entries per owner reachable, against
SHED_HARD_STAGED = 5000. This issue does not re-derive them and does not need to; it takes them as given and observes that the per-owner cap #6 discusses does not bound this scan, because this scan is global.Growth term
Global staged-queue depth, at the moment the venue is busiest — which is exactly when health checks are most frequent.
Relation to #12
The trap outcome on the liquidation batch is already #12's finding, and #12's sharding fix would bound per-message work without removing this helper's cost. The two fixes are complementary. What is new here is the cost model: per-health-check cost is proportional to global staged-queue depth, a dimension #12's measurements do not contain, and it degrades single-user paths (
openPosition,borrow, health queries) that the batch fix never touches.Suggested direction
An incremental per-
(owner, token)aggregate, mirroring thestagedCountByOwnerpattern already in the file at:814-825and thereservedBalancesledger (map at:224,addReserved/subReservedat:1052-1067). Bump on stage, decrement at every removal site that already callssubReserved, and the helper becomes an O(log n) read.5. Finding 10 —
getUserBalanceswalks the entire global balance ledgerThe scan
src/backend/lib/Accounts.mo:63-75:Every
"principal#token"key in the exchange, for all users, with aText.startsWithper entry, to return the handful of pairs belonging to one caller.AccountStatecarries no per-user index.Being precise about the hot caller
The caller worth naming is
main.mo:8262, insidegetMarketChanges— the frontend's delta-poll endpoint. It is important not to overstate this. The call sits inside a version gate at:8259:So it fires when the caller's own state changed — after a fill, an order event, a deposit — not on every 2 s tick. An idle poller never reaches the line. Any characterisation of this as "a full ledger scan every two seconds per client" is wrong.
It is also not attacker-controlled. N is bounded by (registered users × registry tokens), and the open faucet is disabled outside dev (
:8170,not IS_DEV, // faucetDisabled — the open faucet is dev-only), so an attacker cannot cheaply inflate the ledger's row count. Both call sites are non-replicated queries.This is a scalability defect, not an availability threat. It should be triaged as latency and query-node CPU that degrade linearly with the exchange's lifetime user count, including for a wallet holding a single token. It should not be triaged as a denial-of-service vector.
One further note worth checking against the docs:
docs/security-review.md:137listsgetUserBalancesamong the O(total) scans under L3 and marks the class fixed on the strength of the per-user secondary indexes that landed with the order-book scaling work. Those indexes went intoOrderBook.Accountsdid not get any.Optional proof
bash proofs/h10-getuserbalances-full-scan.shmeasures the scan across three ledger sizes and reports a clean linear scaling ratio. If you run it: it executes under themocinterpreter, so only the ratio is meaningful — the absolute timings are interpreter timings and bear no relation to replica instruction counts.Growth term
Registered users × registry tokens.
setBalancealso stores zero balances and rows are never deleted, so the map retains every(user, token)pair ever touched.Suggested direction
state.balancesis an orderedTextmap, so one user's keys are already contiguous under the"principal#"prefix. Seeking to the first key ≥ prefix and iterating until the prefix stops matching is O(log n + k) and needs no new state.Novelty
No existing issue touches
Accounts.getUserBalances. This one is not a correction to anything.6. Findings 41 and 40 — two more unindexed maps, briefly
Finding 41 —
poolPositionshas no per-pool index. Four sites full-scan it, and two are on the update path.reconcilePoolPositions(:4488) walks every position record of every pool after each liquidation, filtering onpos.poolId == poolId.openPosition's isolated-pool guard (:9348) does the same global walk to answer a question about one pool. The rest are queries:previewOpenPosition(:9512, which the UI can hit on every ticket edit) andgetMyPositions(:10108). The keys already cluster —posKeyis"poolId#marketId"(:3666) — so a pool holds at most|markets|entries, and every lookup pays for all pools'. Unlike the heatmap scans, which are capped byHEAT_MAX_POOLS, these have no cap. Growth term: all-time(pool, market)pairs ever traded — worse than open positions, because the normal close path re-adds the record even when the fill flattens the position, so size-zero tombstones persist.Finding 40 —
aggregateHostilityBpswalks the lifetime counterparty map on every requote of every market.main.mo:1010-1026iterates all ofcounterpartyStatsfiltering on a one-hour window, with no cache. It is called at:1980, insideammRequote(:1935), which fires per pool from the 2 s AMM tick and from event-driven price refreshes. The result is market-independent — a single global Float — yet it is recomputed once per market per tick.counterpartyStats(:646) is keyed by counterparty principal (:985,Principal.toText(counterparty)), not by pair, so it gains an entry per principal that ever fills and is never pruned; the only clear isresetExchange(:13940). Stale entries cost one comparison each rather than full arithmetic, which caps the per-entry constant but not the linear term. Growth term: lifetime distinct counterparty principals (per season, since the reset clears it). The cheapest partial fix is to compute it once pertickAmmand reuse it across markets, which removes the per-market multiplier for free.Summary for triage
tickTierstays on the "already measured" list and never gets re-measured.OrderBook.Found and verified with Claude Opus 5. Line numbers re-checked against the current source; where
REVIEW-FINDINGS.mdor the proof comments had drifted, the corrected numbers are used above and the drift is called out inline.Getting the proof scripts. The
proofs/paths referenced above are not in this repository — they ship separately, so nothing is added to your tree. All of them are here:https://gist.github.com/andreij6/ed9f244e47a71a786405bc7959550d4b
To run them, clone the gist into a
proofs/directory at the root of apublic-multidexcheckout:Verified end to end from a clean checkout. The scripts are read-only: they compile and read the product source, modify nothing, and contain no fixes. Each prints the observed value alongside the correct one, exits 0 with
BUG REPRODUCED:while the defect is present, and flips to exit 1 once it is fixed. The gist README maps every proof to its issue and also includes the proofs for candidates that were investigated and not filed.