Seize-loop exhaustion misclassifies collateralized users as insolvent, writing off recoverable debt

[andreij6]

Third of nine. Theme: the liquidation and netting path — specifically the two places where the
accounting stops matching the value movement. One finding forgives recoverable debt and socialises
it; one moves value with nothing booked against it; two are narrower (efficiency, and a published
number).

All four were found and verified with Claude Opus 5 against the published tip
(0241cba). Every line number below was re-checked against source before filing; where our working
notes had drifted, the citations here are the corrected ones.

Two of these bear directly on conclusions already recorded in this tracker, so we lead with the
overlap rather than bury it:

• Item 1 shares a line with OhShii Labs review, 3/8 · 6 findings (#6.1–#6.6): liquidation evasion, a de-lever trap, and release priority that is purchasable #6 item 1 (the ICPUSD-dust liquidation block) but is a different
  branch of the same switch. See the explicit divergence note in that section.
• Item 2 is a correction to OhShii Labs review, 4/8 · 4 findings (#7.1–#7.4): vault and insurance — mint/redemption asymmetries and a guard evaluated on the wrong quantity #7's closing paragraph, which listed settleNettedPair's
  conservation among the things checked and found clean. We think that clearance was one clamp short.
• Items 3 and 4 sit in code Menese DeFi Team evaluation, Part 3: the liquidation path — one new reproduced finding, and a cross-report synthesis with OhShii Labs (#4–#11) #12 section 1 and OhShii Labs review, 3/8 · 6 findings (#6.1–#6.6): liquidation evasion, a de-lever trap, and release priority that is purchasable #6 items 1–2 already measured, for different
  reasons.

---

1. Seize-loop exhaustion is classified as insolvency, so recoverable debt is written off while the user keeps their collateral

Where: src/backend/lib/Liquidator.mo:497 (the loop bound), :521-526 (the mid-loop #err
break), :576-580 (the classifier); consumed at src/backend/main.mo:8084-8089, which calls
absorbBadDebt (:5804-5821).

What is wrong

tryLiquidate's multi-token close is bounded at eight iterations, and it breaks out of the loop on
any seizeOnce error once at least one leg has succeeded:

    label L while (iter < 8) {
      iter += 1;
      let h = BorrowEngine.getHealth(loans, margin, accounts, reserved, user, priceLookup);
      if (h.debtUsd == 0) { break L };
      if (h.healthRatio >= Types.TARGET_HEALTH_RATIO) { break L };

        case (#err(e)) {
          // seizeOnce rolled back its own work. Stop here; if we'd
          // already made progress, finalise with what we got.
          if (not madeProgress) { stopErr := ?e };
          break L;
        };

Both of those exits — the iteration bound, and the post-progress error — fall through to a
classifier that tests only the resulting health, never why the loop stopped:

    if (healthAfter.isLiquidatable) {
      #insolvent(event)
    } else {
      #liquidated(event)
    };

#insolvent is the correct classification for exactly one of the loop's exits: pickCollateral
returning null at :507, i.e. there is nothing seizable. The other exits mean "we ran out of budget"
or "one leg failed", not "there is no collateral". The caller does not distinguish either:

      case (#insolvent(e)) {
        recordLiquidation(e);
        // Couldn't fully cover — close the position and absorb the residual
        // bad debt from the insurance buffer (any shortfall is an LP loss).
        ignore absorbBadDebt(user, now);

and absorbBadDebt charges the insurance pool for the whole residual and then writes off every
remaining loan, with no reference to what the user still holds:

    // Write off every remaining loan token to close the position.
    for (d in BorrowEngine.getDebt(loans, user, marginPriceLookup).vals()) {
      ignore BorrowEngine.writeOffLoan(loans, user, d.token, d.principal, now);
    };

writeOffLoan deletes the token entry, and the user's loans entry once the last token clears
(src/backend/lib/BorrowEngine.mo:286-288), so no later sweep revisits the account. The collateral is
untouched and stays spendable.

The iteration bound is genuinely reachable: each productive iteration drains one collateral token,
retires one debt token, or hits target. With five collateral tokens and five borrowable tokens
(src/backend/lib/Types.mo:300-302), the worst case exceeds eight.

A concrete trigger for the error branch, which needs no exotic position shape. pickCollateral
prefers an exact-token match unconditionally, on balance > 0 alone with no value floor:

    // First pass: exact-token match (direct repay path).
    var sameTokenHit : ?Types.CollateralValuation = null;
    for (v in vals.vals()) {
      if (v.token == debtToken and v.balance > 0) {
        sameTokenHit := ?v;
      };
    };
    switch (sameTokenHit) {
      case (?v) { return ?v };

(Liquidator.mo:88-98.) A one-base-unit holding of the debt token wins that pass. partialSeizeQty
clamps the seize to the holding (:187), giving seizeQty = 1, which passes the
seizeQty == 0 guard at :385. The direct repay path then floors it away:

        let toRepay = Nat.min(debt.principal, Fixed.div(seizeQty, pm, false));
        switch (BorrowEngine.repayFromVault(loans, vaultPrincipal, accounts, user, coll.token, toRepay, now)) {
          case (#ok(_)) { };
          case (#err(e)) { return #err("repay failed: " # e) };
        };

pm = 1.05e8, so Fixed.div(1, pm, false) = 0; writeOffLoan rejects zero
(BorrowEngine.mo:278, "Amount must be positive"); seizeOnce returns #err. On iteration 1 that
returns #err and is retried. On iteration 2 or later, madeProgress is already true, so it
break Ls into the classifier — and a user whose other, valuable collateral was never reached is
declared insolvent and has all remaining debt forgiven.

Adjacent, same trigger: this direct branch does not roll back its seize. The
subtractBalance/addBalance pair at :389-392 has already moved seizeQty to the vault when
:406 returns, and unlike the cross-token branch (:449-451, which restores the user's balance
before returning) nothing reverses it. Bounded to the seized quantity, but it contradicts
seizeOnce's own contract comment at :367 ("rolls back its own seize if the repay/valuation can't
complete").

Why it matters

This is the serious one in this issue. absorbBadDebt moves the residual out of the staked insurance
pool and, beyond it, onto uncoveredBadDebtUsd — a senior AMM-LP loss (main.mo:5810-5815). So the
loss is real and socialised, and it is taken against debt that was still fully collateralised at the
moment of the write-off. The user keeps min(remaining seizable collateral, residual debt) and,
because the loans entry is gone, no future pass can claw it back. Position shape is under user
control, so the eight-iteration case is constructible deliberately; the dust-triggered error case
needs only one base unit of the largest debt token to be held alongside the debt.

Relationship to #6 item 1 — please read these together, they are not duplicates

#6.1 and this finding cite the same break L, and then diverge at madeProgress:

	#6 item 1	This finding
Branch	madeProgress == false	madeProgress == true, or the iter < 8 bound
Return	#err (:531-534)	#insolvent (:576-577)
Effect	Nothing seized; retried on every sweep forever	Everything written off once; never revisited
Loss	Un-recovered loan, invisible to the risk panel	Insurance + LP loss, recorded, against solvent debt

Fixing #6.1 as suggested there (skip a candidate whose seize cannot repay, or continue to the next
collateral instead of break L) would remove the transient-error sub-case above. It would not
address the iteration bound, and it would not address the classifier, which is the actual defect
here: the loop's exit reason is discarded before the insolvency decision is made.

How to confirm

Static, no deployment needed — trace Liquidator.mo:497 → :521-526 → :576-580 → main.mo:8084-8089 → :5804-5821 and observe that no value flowing along that path carries the loop's
exit reason, and that absorbBadDebt reads only loans, never accounts.

To exercise it: give a cross margin pool debt in the largest-debt token plus a 1-base-unit balance of
that same token, and meaningful collateral in a different token. Drive health below 1.15 so that at
least one iteration succeeds against a different debt token first, then let the dust token become
largestDebt. Fire adminRunLiquidationBatch (main.mo:10709). Expected: a #insolvent
liquidation event, uncoveredBadDebtUsd or the insurance pool debited, and the other collateral
still in the pool's spendable balance with the loans entry deleted.

---

2. settleNettedPair moves value when its cash leg floors to zero, and the caller books nothing

Where: src/backend/lib/Liquidator.mo:304-322; caller at src/backend/main.mo:3449-3474.

This corrects a clearance in #7

#7's closing paragraph lists, among the things checked and found clean:

settleNettedPair's conservation (four-way clamp with a full rollback of the seller leg)

Both halves of that description are accurate as stated, and the conclusion still does not hold. The
four-way clamp constrains q. It does not constrain cash, which is derived from q by a
flooring multiply after the clamp and is never checked. And the rollback is indeed full for the
seller's balance leg — but it is also unreachable (the buyer-cash clamp guarantees the buyer can
always pay), so it does not protect the path that actually fires. We flag this specifically because
"checked and clean" on a conservation property is the kind of finding that stops getting re-examined.

What is wrong

    if (q > buyerDebtX)      { q := buyerDebtX };
    if (q == 0) { return zero };
    let cash = Fixed.mul(q, mid, false);
    // Seller: X → vault, ICPUSD debt written off by `cash`.
    if (not Accounts.subtractBalance(accounts, seller, baseToken, q)) { return zero };
    Accounts.addBalance(accounts, vaultPrincipal, baseToken, q);
    ignore BorrowEngine.writeOffLoan(loans, seller, Types.QUOTE_TOKEN, cash, now);
    // Buyer: ICPUSD → vault, X debt written off by `q`.
    if (not Accounts.subtractBalance(accounts, buyer, Types.QUOTE_TOKEN, cash)) {

q is validated non-zero; cash is not. When q ≥ 1 but q × mid < 10^8, Fixed.mul(…, false)
floors cash to 0 and each leg degrades independently:

• :307-308 — the seller's q base units move to the vault. This succeeds; q was clamped to the
  seller's balance.
• :309 — writeOffLoan(…, 0) returns #err("Amount must be positive") (BorrowEngine.mo:278) and
  is ignored. The seller receives no debt relief for the units they just gave up.
• :311 — subtractBalance(…, 0) returns true (Accounts.mo:56-58: current < 0 is never true),
  so the rollback does not fire. The buyer pays nothing.
• :318 — writeOffLoan(loans, buyer, baseToken, q, now) succeeds. The buyer's base debt is
  forgiven by q for zero consideration.

The function then returns { cash = 0; qty = q }, and the caller gates all of its bookkeeping on
cash:

              if (settled.cash > 0) {
                nettedVolumeUsd += settled.cash;

so this settle takes the else branch at :3466-3474 — the "neither side could move" path. Nothing
is recorded: no nettedVolumeUsd, no bookPoolSide for either pool, no sRem/bRem decrement, no
bumpUserVersionWithTrade. The comment block at :3451-3458 explains precisely why that booking
exists ("Without this the slice's realized PnL is never attributed"), and this is the path that skips
it.

Why it matters

Honestly scoped: the value moved is dust. cash == 0 requires q × mid < 10^8, so the transferred
base is worth strictly less than one ICPUSD base unit. This is not a funds-drain finding and we are
not presenting it as one.

What it is, is an unrecorded transfer on a settlement function — balances and the loan book
mutate while every ledger the system keeps of that mutation stays flat. Both pools' poolPositions
now disagree with real exposure until an unrelated reconcile re-derives them, and no version bump
fires, so clients do not refetch. It is reachable whenever the base mark is below $1.00 (ICP, or any
low-marked seeded token) and a netting slice clamps to a single base unit — which is exactly the
dust-heavy cascade regime, where it can repeat once per netting pair per sweep.

How to confirm

Arithmetic first: Fixed.mul(1, 50_000_000, false) = 1 × 5·10⁷ / 10⁸ = 0 under
Fixed.mulDiv (src/backend/lib/Fixed.mo:30-36), with roundUp = false.

Then verify the three enabling facts, each one line: writeOffLoan rejects zero at
BorrowEngine.mo:278; subtractBalance accepts zero at Accounts.mo:56-58; the caller keys on
cash at main.mo:3449.

To exercise it: mark a base token below $1.00, build one long-liquidatee (holds the base, owes
ICPUSD ≥ 1 base unit) and one short-liquidatee (holds ICPUSD, owes ≥ 1 base unit of the base token)
such that at least one of the four clamps drives q to 1, and run the batch. Expected: the seller's
base balance falls by 1, the buyer's base loan falls by 1, and nettedVolumeUsd, both
poolPositions rows, and both user versions are unchanged.

---

3. The netting matcher advances by planned quantity, not by which side actually bound

Where: src/backend/main.mo:3466-3474, against the plan quantities read at :3434-3435;
settleNettedPair's clamps at src/backend/lib/Liquidator.mo:293-303.

What is wrong

On a zero settle, the batch advances whichever side has the smaller planned remaining quantity:

              } else {
                // Neither side could move (balance/debt exhausted) —
                // advance the smaller remaining side to avoid a stall.
                if (sRem <= bRem) {
                  si += 1; if (si < sArr.size()) { sRem := sArr[si].baseQty };
                } else {
                  bi += 1; if (bi < bArr.size()) { bRem := bArr[bi].baseQty };
                };
              };

sRem and bRem are seeded and re-seeded from the plan's baseQty (:3434-3435).
settleNettedPair clamps against live state — seller balance, buyer cash, seller quote debt, buyer
base debt — and returns only { cash; qty }. There is no channel by which the caller can learn which
of the four clamps bound. Plan quantity routinely exceeds live capacity, because partialSeizeQty
sizes the seize against the whole portfolio debt (Liquidator.mo:158-189) while netting retires a
single ICPUSD or single base loan.

So when the genuinely exhausted party is the one holding the larger planned remainder, the loop
advances past the still-viable counterparty instead.

Why it matters — and where we think our own framing needs qualifying

We want to be precise about this one, because the obvious reading overstates it.

This is a deliberate anti-stall heuristic, and the comment says so. Without it, a pair where one side
is exhausted but retains planned quantity would spin. "Advance the smaller remaining side" is a
reasonable guess in the absence of information the function does not return. It is conditionally
wrong — wrong exactly when the exhausted side is the larger remainder — not deterministically wrong,
and the defect is symmetric (an exhausted buyer consumes viable sellers just as an exhausted seller
consumes viable buyers).

The consequence is also bounded. A skipped counterparty is not abandoned: they fall through to
Phase 3 tryLiquidate in the same sweep and are liquidated there. The cost is that they pay the
guaranteed 5% penalty (Types.mo:348, applied in seizeOnce) instead of taking the penalty-free
netting route that settleNettedPair's own header comment (Liquidator.mo:270-272) describes as the
reason the function exists. The penalty accrues to the insurance buffer, so no value leaves the
system.

Efficiency and fairness, then. It bites hardest in a crash, when many accounts are deep underwater
and the clamps bind on most pairs — which is when the netting engine is supposed to be earning its
keep.

How to confirm

Trace the two quantities: sArr[si].baseQty originates in Liquidator.planLiquidation's
partialSeizeQty sizing; the quantity actually settled originates in the four clamps at
Liquidator.mo:293-303. Confirm that settleNettedPair's return type (:286, { cash : Nat; qty : Nat }) carries nothing else.

To exercise it: construct one seller whose plan baseQty × mid exceeds their ICPUSD debt, so the
first settle fully retires that debt and leaves sRem > 0 while live capacity is 0. Add several
buyers each with bRem < sRem. Every subsequent settle against that seller returns zero and takes
bi += 1, consuming buyers who could still have netted against a later seller. Compare
nettedVolumeUsd and the count of Phase 3 liquidation events against a run where the seller's plan
quantity matches their debt.

Note on overlap

runLiquidationBatch (main.mo:3383-3494) is the same function #12 section 1 measured for the
uncapped-sweep trap, and the same region #6 items 1–2 touch. Those are independent defects in shared
code; none subsumes another.

---

4. The short-position liquidation price ignores the pool's other debt (display surfaces only)

Where: src/backend/main.mo:3697-3701, with src/backend/lib/MarginPools.mo:137-140.

What is wrong

positionLiqPrice computes pool-wide health h, then branches:

    if (size > 0) {
      MarginPools.liqPriceLong(otherColl, h.debtUsd, size, ltv, Types.MAINTENANCE_HEALTH_RATIO)
    } else {
      MarginPools.liqPriceShort(otherColl, Int.abs(size), Types.MAINTENANCE_HEALTH_RATIO)
    };

The long branch passes total debt. The short branch does not — and liqPriceShort has no debt term
at all:

  // Liquidation price for a SHORT: P = otherColl / (maint·|size|).
  public func liqPriceShort(otherCollUsd : Nat, sizeAbs : Nat, maintenance : Nat) : ?Nat {
    if (sizeAbs == 0 or maintenance == 0) { return null };
    ?Fixed.div(otherCollUsd, Fixed.mul(sizeAbs, maintenance, false), false)
  };

It solves P = otherColl / (maint × |size|), which is only correct if the base loan is the pool's
sole debt. For a cross pool carrying additional price-independent debt Dq — a leveraged long in
another market borrows exactly that — the true condition is otherColl < maint × (|size|·P + Dq),
giving P_true = (otherColl/maint − Dq)/|size|, strictly below the reported value. Since the long
branch already consumes h.debtUsd, the asymmetry does not read as deliberate cross-pool design.

Why it matters — and the limit of what it affects

We want this scoped correctly, because it looks worse than it is. Every caller of
positionLiqPrice is a read surface:

• main.mo:10115 — getMyPositions (query)
• main.mo:9591 — previewOpenPosition's estLiqPrice (query)
• main.mo:3816 — computeMarketHeatmap, the published liquidation heat map
• main.mo:4096 — tickMarketSideAgg's distance bucket

The liquidation engine does not consult it. tryLiquidate and planLiquidation both derive health
from BorrowEngine.getHealth, which counts all debt. So this is a published-number defect, not a
liquidation-trigger defect — the engine fires at the right price; the UI showed the wrong one.

That said, the error is directionally unsafe: it always overstates the distance to liquidation for a
cross-margined short. A pool short 1 unit at a mark of 100, with 50 ICPUSD borrowed elsewhere and 200
of price-independent collateral, reports 200/1.15 = 173.9 (74% away) against a true (200/1.15 − 50)/1 = 123.9 (24% away) — roughly three times safer than reality, across the position table, the
preview, and the public heat map simultaneously. Low severity, but it is the number a user checks
before deciding they have room.

How to confirm

Read MarginPools.mo:137-140 and confirm no parameter carries debt. Then confirm all four call sites
above are read paths, and that the liquidation decision at Liquidator.mo:499 uses
BorrowEngine.getHealth rather than positionLiqPrice.

To exercise it: open a cross margin pool, take a short in one market and a leveraged long in another
(the multi-market restriction applies to isolated pools only), then compare getMyPositions'
reported liquidation price for the short against the price at which getHealth actually crosses
1.15.

---

Severity summary

#	Finding	Severity	Class
1	Seize-loop exhaustion classified as insolvency	Medium–High	Recoverable debt forgiven; loss socialised to insurance then LPs
2	settleNettedPair cash leg floors to zero	Low	Dust-scale, but an unrecorded balance and loan mutation
3	Netting matcher advances by planned quantity	Low–Medium	Efficiency and fairness; skipped users still liquidate, penalised
4	Short liquidation price ignores other debt	Low	Display, preview, and aggregation only

Item 1 is the one we would fix first. Items 2 and 4 are contained; item 3 is a heuristic that needs
better information, not different logic.

Found and verified with Claude Opus 5. Every line number cited above was re-checked against source at
0241cba before filing.

[dominicwilliams]

Item 1 is confirmed and fixed. Item 2 is confirmed and open.

Item 1 — seize-loop exhaustion misclassifies collateralized users as insolvent. Confirmed, and this one corrected a fix we had just shipped. The remedy for OhShii's dust finding (#6.1) closed the dust trap and the missing rollback but left the classifier reading only the resulting health — so the two terminal states of the loop remained conflated:

• nothing seizable remains → genuinely #insolvent;
• the MAX_SEIZE_ITERS budget ran out mid-walk with seizable collateral standing → not insolvent at all.

The second reaching #insolvent means absorbBadDebt writes off every remaining loan and socialises the residual, booking a fully-collateralised position as a loss. Your central observation is the one that makes this obvious in hindsight and was missed by everyone who looked before you: the iteration bound is a message-size bound and carries no solvency meaning whatsoever. Reading a resource limit as a financial verdict is the actual defect; the misclassification is just where it surfaced.

Fixed as a named pure function, Liquidator.classifySeizingPass, so the distinction is testable in isolation rather than inferred from the driver's control flow. Budget exhaustion now reports #liquidated: the user stays in loans and the next sweep resumes from the improved health, which is the correct behaviour — the pass did real work, it simply did not finish.

Pinned by tests/Liquidator.test.mo: the classifier over all four terminal states, plus an invariant asserted across every liquidation shape in the file — #insolvent may only be returned when nothing seizable is left. That invariant is the durable part; it makes this class of regression fail loudly rather than quietly socialise a loss.

Item 2 — settleNettedPair's dust path. Confirmed, not fixed. cash floors to zero, writeOffLoan rejects it and the result is ignored, while the buyer's base debt is still forgiven. Note that this corrects a clearance we had already issued for that function in our own triage — we had looked at settleNettedPair and passed it. It is open.

The code is in #30, the first push to this mirror since the July snapshot; your line numbers against 0241cba still resolve.