OhShii Labs review, round 12 · 6 findings (#49.1–#49.6): readiness for real custody, and a margin-limit bypass that is our own remedy shipped without its qualifier

Round 12 asked one question: what breaks on the day custody arrives? SECURITY.md:31 says the venue is play-money by construction with no real-asset custody, and docs/bridge-and-cks-design.md opens "Status: PROPOSAL (nothing implemented)". So the fund paths hold nothing real, need no inter-canister call, and are atomic by consequence rather than by design. That is a guarantee nobody wrote down, and it expires on a known date.

Nothing here is live-exploitable against funds or authorization. #49.1 is a live defect and needs an ordinary authenticated user acting on their own margin pool; the rest are readiness or observability.

Twenty refutation tasks over eighteen candidates, default verdict REFUTED: five killed, fifteen narrowed, none survived unchanged. The kills and the two corrections to our own instruments are in the last two sections, because they are the part that makes the rest checkable.

Severity

#49.1	the de-lever escape is a sign test with no quantity bound	[play: MEDIUM / prod: HIGH]
#49.2	the withdrawal half of custody has none of the machinery the deposit half already has	[play: INFO / prod: MEDIUM]
#49.3	placeMarketOrder returns #ok for an order that was never staged	[play: LOW / prod: LOW-MEDIUM]
#49.4	no writer of insuranceShareSupply lapses insuranceOwedUsd at supply zero	[play: LOW / prod: LOW-MEDIUM]
#49.5	the AMM's adverse-flow spread term is identically zero	[play: INFO / prod: LOW]
#49.6	Types.marginLTV's fail-closed on an unknown token is accidental	[play: INFO / prod: LOW]

A token-listing readiness specification travels with this issue as an unnumbered appendix. It is not a finding, carries no severity, and is not counted in the six above.

---

#49.1 — the de-lever escape is a sign test with no quantity bound [play: MEDIUM / prod: HIGH]

This is our own remedy, shipped without its qualifier. That has to come first.

Our #6.3 said: "Model the post-fill deleverage: for a fill whose sign is opposite to poolNetSize, credit the debt reduction. Minimum viable — return #full when the fill strictly reduces |poolNetSize(poolId, baseToken)| and does not increase debtUsd; or port gateInitialMargin's escape clause into the clamp."

main.mo:8790-8791, the shipped comment: "A fill whose sign OPPOSES the pool's net position in that base is a genuine de-lever: let it through." And :8794-8799:

let net = poolNetSize(poolId, baseToken);
let reducesExposure = switch (side) {
  case (#buy)  { net < 0 };   // short (owes base) buying back
  case (#sell) { net > 0 };   // long selling down
};
if (reducesExposure) { return #full };

Our first clause shipped near-verbatim. The qualifier that closes it was in the same sentence and did not. Sign only — no magnitude, no debt condition. :8788-8789 shows you had read the second option too ("gateInitialMargin has the newHealth < healthRatio escape that this clamp lacked"), so this is a transcription boundary rather than a shortcut.

What it permits

:8799 returns before the headroom branch at :8803-8817, so the bound the function computes for itself is unreachable whenever the pool holds any opposite-side exposure. And openPosition applies no initial-margin gate on either branch: a needle for checkInitialMargin|gateInitialMargin|clampToInitialMargin|validateNewOrder returns 0 over :9760-9891 against 17 file-wide, with a positive control (getAvailable) returning 2 on the same window.

A $1 dust short arms it. From a pool at the 1.25 floor, the escape permits 422.23178807 SOL where the clamp's own bound allows 0.03333333 — a factor of 12,667 — landing at health exactly 1.15, which survives because BorrowEngine.mo:142 tests ratio < Types.MAINTENANCE_HEALTH_RATIO strictly. Closed form: converting the whole quote leg into a token of LTV λ multiplies health by λ, so from 1.25 the landing point is 1.0625 for SOL and 1.0000 for ICP.

We do not claim the larger form. At 796 SOL the pool is liquidated in the same message — releaseDeferred adds the pool principal to the affected set at :2735, commitDeferredTrades passes it to adjustAffectedUsers at :2980, :8344 fires tryLiquidate — so it is self-punishing and yields nothing. The durable form is the one above.

Three arithmetic corrections we made against ourselves, all in the direction the maintainer already docked #7.3 for: steps 1–3 charged no taker fee, but the seller pays one (MatchingEngine.mo:387), so the pool holds $187,372.50 not $187,500; the withdrawal leaving $1 of headroom is $27,996.249 not $28,123.75; and the no-borrow maximum is 796.88625 SOL exactly, because one cent more triggers a borrow. The end state is exact; only the intermediate ledger was wrong.

And our invariant sentence was looser than your code. The property is "no risk-increasing action may lower health below 1.25", not "no action may leave health below it" — :8687-8689 allows any trade that holds or improves health, and gateInitialMargin conjoins newHealth < health.healthRatio at :8707. That correction strengthens the finding: gateInitialMargin's escape is bounded by health monotonicity, the clamp's by a sign, and the clamp's own comment says it was copying the former.

Bounded honestly: a margin-limit bypass, not a solvency break. Raw un-haircut collateral exceeds debt at every reachable landing point ($159,216.03 against $127,500), so no bad debt is created in one step. What is consumed is the buffer that absorbs price movement between a fill and the liquidator.

Remedy — direction, not tested. Restore the qualifier our own report dropped: conjoin the magnitude test and the debt condition, or port gateInitialMargin's health-monotonicity escape as the same comment says was intended.

---

#49.2 — the withdrawal half of custody has none of the machinery the deposit half already has [play: INFO / prod: MEDIUM]

Nothing is broken today, and that is the point: 31 of the 34 update methods that can reach a balance mutation contain no await anywhere in their call-graph closure. They are atomic — no interleaving, no stale read, no partial state — and they are atomic because nothing they touch is real.

docs/bridge-and-cks-design.md:7-12 puts custody in a separate NNS-controlled canister and leaves the DEX holding "virtual balances only", so the commit point appears in exactly one new place: the DEX→Bridge withdrawal. That is a good design and it is why this finding is narrow.

The gap is that every primitive that path will need already exists in this tree, written by you, and none of them is on it.

• The deposit half is already correct. creditAndRegister carries an idempotency high-water (creditedSeq :5471, advanced at :5557) and a fail-closed divergence refusal at :5510-5515, with the doctrine in your own comment: "A refusal costs one failed claim and is trivially repaired by advancing creditedSeq; a silent mint is unrecoverable." That is exactly what a withdrawal needs in mirror image.
• Two single-flight interlocks exist — _geptorInFlight (:3140-3181, released in a finally) and _shipInFlight (:7190, :7607). Neither is on a fund path.
• The only pending-outcome latch that IS on a fund path is _fuelPendingNotify — which is #47.2, whose sole unattended retry sits below a health gate that recovery itself closes.

After custody a transfer has a third outcome between success and failure. No structure in the tree can carry one, and the design document does not name it either. This is the same class as #44 and we file it in the same register: not a defect, a thing that must exist before a known change.

---

#49.3 — placeMarketOrder returns #ok for an order that was never staged [play: LOW / prod: LOW-MEDIUM]

The only genuinely novel ground in the four regions we had wrongly believed unexamined. A caller receives a success reply for an order that never entered the deferred queue, so a client that trusts the reply and does not poll believes it has an order resting when it has none. Adjacent to, and deduped against, our own #47.1.

#49.4 — no writer of insuranceShareSupply lapses insuranceOwedUsd at supply zero [play: LOW / prod: LOW-MEDIUM]

performWorldWipe zeroes every other insurance variable and leaves this one standing. settleInsuranceArrears does lapse it at :6040 when supply is zero, but only when it runs — so a wipe leaves a receivable owed to a tranche that no longer has holders.

#49.5 — the AMM's adverse-flow spread term is identically zero [play: INFO / prod: LOW]

The quote equation still adds an adverse-flow widening whose only data source is written from a path that cannot execute, so the term contributes nothing. A published-formula-versus-shipped-behaviour contradiction and an observability gap, not an LP-value loss. It also retires one of our own prior claims — that counterpartyStats grows unbounded. It does not, because nothing writes it.

#49.6 — Types.marginLTV's fail-closed on an unknown token is accidental [play: INFO / prod: LOW]

Types.mo:312's case (_) { null } means an unlisted token contributes zero collateral value. That is the right behaviour and it is the single line that would stop an unpriced asset being borrowed against. It is currently a property of the switch having no arm rather than a decision. If the token set ever opens, this is the line that must be preserved deliberately.

---

What this round killed, including one that two of three reviewers wanted to file

Five candidates died. One deserves naming because a majority would have filed it:

A candidate held that unstakeInsurance burns shares without reducing insuranceOwedUsd while the vault's senior tranche receives that write-off. It is false, and filing it would have re-filed our own prescribed remedy as a bug. insuranceOwedUsd has exactly three writes — :6027, :6040, :6047 — and none is in withdrawLp or unstakeInsurance; neither tranche writes it down. And the asymmetry that does exist is one we asked for: our #7 said "Use insurancePoolValue() + insuranceOwedUsd for the mint only; keep insuranceShareValue() cash-only so an unstake stays fully payable. The two figures should differ." Your comment at :11039-11042 is that sentence adopted.

Also killed: an AMM item that was documented design below your own cap; another whose two named harms both measured false; a duplicate of our own #7; and an oracle item that was not a defect.

And an evidenced negative worth having, so nobody re-walks it: OrderBook.remaining (lib/OrderBook.mo:413-415) is a bare quantity - filled with twelve call sites and fillOrder:756 has no cap — but the vector is closed by adjustOrderQuantity:788 refusing to lower quantity below filled, and by the reserve-aware match loop at MatchingEngine.mo:294-302. All five fillOrder call sites checked individually; the needle positive-controlled against the known guard.

Two of our own instruments failed, and both are recorded rather than quietly fixed

The coverage census was invalid. Our rounds 1–2 citations were filed against 0241cba; 1.60 inserted 709 lines into main.mo, so the same symbol moves by up to +625. Our own #27.4 cites main.mo:13099-13104; at this pin that code is at :13709. docs/issue-triage-2026-08.md:5-6 documents exactly this trap — you re-verify "by symbol lookup, not by trusting the reporters' line numbers … so citations drift" — and we adopted that file as a dedup root in round 10 without reading its methodology note. The 33.7% figure has been removed from #47 and #48. Keyed on symbols instead: 530 functions declared in main.mo, 334 named at least once across everything we have written, 196 never — stated with its limit, that named is not examined in either direction.

And this round's own scoping was wrong before it started. We first counted 13 of 17 synchronous fund movers; a slicer that cut each public shared declaration to the next public shared declaration rather than to the next declaration swallowed the private helpers between them and credited their balance operations to whichever method preceded them. setAmmConfig, adminResetLiquidationBreaker and openPosition have zero balance operations in their own bodies. Re-derived correctly the population is 31 of 34, and the defect reproduces: running the bad slicer returns exactly 17.

Dedup

Corpus: every filed issue body and comment for #2–#48, all six private advisories, our own local drafts, and your docs/issue-triage-2026-08.md. Where a candidate landed on ground already worked we credited the owner and dropped it — the oracle region to our own #9.1/#9.2/#27.3/#27.4 and @andreij6's #17; the deleverage region to his #13.2 and #19.41; the AMM quoting region to our own round-11 rejects file.

Nothing here re-files @andreij6's #13–#21, #42, #43 or Menese's #2, #3, #12, #22.

— OhShii Labs

Start with the margin clamp and openPosition regions in main.mo:8790-8817 and :9760-9891, then compare the stated behavior with BorrowEngine.mo:142. For the custody-readiness findings, read docs/bridge-and-cks-design.md and inspect creditAndRegister, _geptorInFlight, _shipInFlight, and _fuelPendingNotify. Done means each finding has a verified disposition and any required follow-up is explicitly scoped.