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

[rvnt9999]

OhShii Labs review, 4/8: vault and insurance — mint/redemption asymmetries and a guard evaluated on the wrong quantity

Fourth of eight. Theme: places where the mint side and the redemption side of a tranche disagree, so a round trip is not the identity.

The Menese team found a third asymmetry in the same two functions (#3 item 1 — the ERC-4626 virtual-share offset applied on mint but not redeem). That is a distinct root cause from item 2 below and both should be fixed together; we confirm their reading and their closed form.

---

1. Vault NAV subtracts insuranceOwedUsd, but LP redemption pays from gross holdings

Where: main.mo:12640-12652 (currentVaultValue), :11767 (mint), :13700-13715 (withdrawLp)

// NAV is haircut by the arrears
    let totalValue : Nat = if (totalAssets > insuranceOwedUsd) {
      (totalAssets - insuranceOwedUsd) : Nat
    } else { 0 };
// the mint prices against that NAV
    let minted = VaultMath.mintAmount(effectiveValue, vaultLPSupply, vaultBefore.totalQuoteValue);
// redemption reads HOLDINGS, not NAV
    let btcHeld = Accounts.getBalance(accounts, amm, "BTC");
    func netLeg(held : Nat) : Nat {
      Fixed.mulDiv(Fixed.mulDiv(held, lpAmount, vaultLPSupply, false), keepBps, 10_000, false);
    };

Why it matters. The code documents and correctly accepts the loan-book asymmetry — NAV includes vaultLentOutUsd() while redemption does not, which makes redemption ≤ fair and is therefore safe. Subtracting insuranceOwedUsd from NAV flips the sign of the same asymmetry: redemption now ignores a liability the mint priced in.

With H = holdings, L = lent out, O = arrears, S = supply, a deposit of V mints ≈ V·S/(H+L−O) and redeems ≈ (H+V)·minted/S' × 0.996. The payout ratio is (H+V)/(H+L−O+V) × 0.996, so whenever O − L > 0.004·(H+V) the round trip is net-positive, funded by the remaining LPs.

Worked example. H = $1,000,000, L = 0, O = $19,000 (a 5% penalty on a ~$400k cascade), S = 1,000,000 LP → NAV $981,000. The concentration cap allows V ≈ $272,000 on one base leg. minted ≈ 277,268; payout = 1,272,000 × 277,268/1,277,268 × 0.996 = $275,020. +$3,020 per leg, repeatable across all four base legs while O persists.

The deposit must be a base leg, not ICPUSD: cash would fund settleInsuranceArrears on the next beat and close the window, whereas a base deposit leaves vault cash untouched. getInsuranceFund().pendingYieldUsd (:10226) publishes O, so the window is observable.

Suggested direction. Make redemption symmetric — on withdrawLp, deduct the exiting share's slice of insuranceOwedUsd (Fixed.mulDiv(insuranceOwedUsd, lpAmount, vaultLPSupply, true)) from the ICPUSD leg, exactly parallel to how the loan book is already handled.

Confidence note. The arithmetic asymmetry is confirmed in source. The precondition (O > L + 0.4%·H, i.e. the vault cash-poor for at least one heartbeat) is narrow, and we did not establish it is currently reachable on the live book — that would need probing the deployment, which we did not do. To confirm locally: drive a liquidation cascade with the vault's ICPUSD drawn down, observe pendingYieldUsd > 0, then run the deposit/withdraw pair.

---

2. stakeInsurance mints against cash-only pool value, ignoring the fund's receivable

Where: main.mo:10581, :10625-10631, :5739-5741, :5782-5797, :10226

  func insurancePoolValue() : Nat {
    Accounts.getBalance(accounts, insurancePrincipal(), Types.QUOTE_TOKEN)   // cash only
  };
  ...
    let valueBefore = insurancePoolValue();
    let minted = ... Fixed.mulDiv(amount,
                     insuranceShareSupply + INSURANCE_VIRTUAL_SHARES,
                     valueBefore + INSURANCE_VIRTUAL_VALUE, false)   // denominator omits insuranceOwedUsd

Why it matters. insuranceOwedUsd is a receivable of the fund — penalties already earned by existing stakers (:4610-4613). The mint denominator excludes it, so shares are sold below their economic value, and when settleInsuranceArrears moves the cash across, the newcomer takes a pro-rata slice of a payment they did not earn.

The comment at :10213-10218 justifies excluding arrears from shareValueUsd so "an unstake can always be paid" — correct for the redemption side. But the same figure is reused as the mint denominator, where the right value is poolValue + owed. Note the virtual offsets at :10563-10564 exist specifically to stop share-price manipulation; this is the one input they do not cover.

Worked example. Pool $10,000, 10,000 shares (value 1.00), pendingYieldUsd = $5,000. Stake $10,000 → ≈10,000 shares, supply 20,000. Arrears settle → buffer $25,000, share value 1.25. Unstake 10,000 → $12,500. Profit $2,500; the stakers who actually earned the penalty receive $12,500 instead of $15,000.

Suggested direction. Use insurancePoolValue() + insuranceOwedUsd for the mint only; keep insuranceShareValue() cash-only so an unstake stays fully payable. The two figures should differ.

This is separate from the Menese finding. Theirs is the virtual-offset asymmetry between mint and redeem (redeem(mint(A)) > A whenever share value > 1.0, which is the normal state). Ours is the omitted receivable in the mint denominator. Fixing either alone leaves the other open.

Related, and noted by both of us: unstakeInsurance (:10654-10681) has no timelock, cooldown or exit fee — the only gates are share balance and own-debt. absorbBadDebt (:5804-5821) drains the pool for whoever remains, and it is driven by a 30 s-class heartbeat while getMarginRiskSummary and getMarginHeatmap* are public queries, so an approaching insolvency is visible to any poller. On a $100k pool with five stakers and $30k of bad debt, the first to exit keeps $20k whole and shifts $6k of loss onto the other four. The AMM LP tranche's LP_EXIT_FEE_BPS = 40 is the pattern to mirror.

---

3. vaultPricesStale tests a leg's value rather than its balance, so a held leg priced at zero is invisible to the mint guard

Where: main.mo:12765, :12710-12719 (vaultAssetValueUsd), :11627 (the trigger)

  func vaultPricesStale(now : Int, vv : VaultValue) : ?Text {
    let legs = [("BTC", "BTC-ICPUSD"), ("ETH", "ETH-ICPUSD"), ("SOL", "SOL-ICPUSD"), ("ICP", "ICP-ICPUSD")];
    for ((asset, market) in legs.vals()) {
      if (vaultAssetValueUsd(vv, asset) > 0) {  // "vault holds it (and it's priced)"

vaultAssetValueUsd is Fixed.mul(balance, price, false). When price == 0 the product is 0, so the leg is skipped entirely — no staleness check, no pending-jump check — while currentVaultValue simultaneously marks that whole leg at $0. The vaultLPSupply > 0 and totalQuoteValue == 0 backstop at :11764 fires only if the entire basket marks to zero.

The comment conflates two conditions ("holds it and it's priced") into one product, and the failure of the second silently disables the first.

Trigger. createAmmPool (:11627) unconditionally overwrites an existing pool with AMM.emptyPool(...), i.e. refPrice = 0 — a single controller call on a live market zeroes that leg's NAV contribution without pausing mints. We verified the price feed itself cannot produce this: applyFreshAggregate requires agg.price > 0.0 (:13205) and never writes 0.

Worked example. H = $1,000,000 of which BTC is $125,000; after the overwrite totalQuoteValue reads $875,000, S = 1,000,000. A $100,000 deposit on a different leg passes (BTC was skipped, totalQuoteValue > 0) and mints 114,286 shares; withdrawLp returns a pro-rata slice of all holdings including BTC: 1,100,000 × 114,286/1,114,286 × 0.996 = $112,392. +$12,392 on $100,000, from existing LPs.

Suggested direction. Test the balance, not the value (if (vv.basket.btc > 0)), and refuse the mint outright when a held leg's refPrice == 0 — a leg the vault holds but cannot price must block minting, not silently value at zero. Separately, make createAmmPool refuse to overwrite an existing pool, or carry refPrice/refPriceUpdatedNs forward.

---

4. Three unbacked-credit endpoints lack the IS_PRODUCTION interlock every sibling has

Where: main.mo:4852 (fundArbitrageur), :4884 (donateToVault, the fromTreasury = false branch), :4919 (extMarketSwap)

The codebase applies a uniform discipline: every path that credits balance with no backing debit is a hard no-op on #production — setTestBalance/bulkSetTestBalances (AdminOps.mo:41,55), addTestTokens (UserAccount.mo:123), seedInsuranceFund (:10692), resetExchange (:13913), resetSeason (:14234), withdraw (UserAccount.mo:189). These three do not have it.

seedInsuranceFund's own comment states the rule they break: "On #production balances enter only via the Bridge — insurance must be funded through a BACKED path … never minted by a controller." donateToVault(_, false) and fundArbitrageur mint exactly that way, and extMarketSwap mints synthetic base supply against no custody and is reachable by a non-controller principal (the wired arb canister), bounded only by ARB_MAX_SWAP_USD and ARB_HOURLY_CAP_USD.

This is a #production-readiness gap rather than a live #play issue — the interlock is missing, not the guard. donateToVault(_, true) (treasury → vault) is conservation-neutral and can stay.

Suggested direction. if (IS_PRODUCTION) { return #err("…") }; as the first statement of each, matching :10692.

---

For completeness, we checked and did not find problems in: the ERC-4626 first-depositor/donation inflation path on the AMM vault (closed by LP_MIN_FIRST_DEPOSIT_USD, the virtual offsets, and the supply>0/value==0 refusal); withdrawLp returning more than the shares represent (both mulDivs round down, the exit fee is retained, the burn precedes the transfer, and AMM reserved balances are excluded); the hasOutstandingDebt guards on withdrawLp and unstakeInsurance plus the gateInitialMargin projections that close the earlier collateral-escape class; settleNettedPair's conservation (four-way clamp with a full rollback of the seller leg); and the bad-debt waterfall ordering. Your mulDiv being arbitrary-precision Nat also removes the Solidity overflow class, as the Menese team noted.

— Ravenith, OhShii Labs

[rvnt9999]

@andreij6's #15 item 2 is correct - our settleNettedPair 'clean' was one clamp short on the dust path. Finding stands as a correction to our SAFE list.

[dominicwilliams]

All four findings confirmed and fixed. This report had the highest confirmation rate of the eight parts and needed the fewest corrections.

#7.1 — vault NAV vs withdrawLp. Confirmed exactly as filed: NAV haircuts insuranceOwedUsd while withdrawLp paid from gross holdings, which flips the sign of the loan-book asymmetry that was deliberately safe. Fixed.

#7.2 — stakeInsurance's mint denominator omits insuranceOwedUsd. Confirmed, and your framing was the important part: this is a distinct root cause from the mint/redeem asymmetry in #3.1, and fixing either alone leaves the other open. We would plausibly have treated them as one bug and shipped half a fix. Both are closed.

#7.3 — vaultPricesStale tests the wrong quantity. Confirmed: the guard tested a leg's value (balance × price) rather than its balance, so a leg priced at zero was skipped by the staleness guard while being marked at $0 in NAV. Also confirmed the createAmmPool overwrite with refPrice = 0; we agree with your read that it looks like an honest reconfiguration mistake rather than an attack path, and it is closed regardless.

One correction, immaterial to the finding: your worked example gives +$112,392, and your own formula yields $112,369.48. Direction and magnitude are right; the arithmetic is off by $22. Recorded for completeness, not held against the report.

#7.4 — production-readiness interlocks. Confirmed: three unbacked-credit endpoints lacked the IS_PRODUCTION interlock every sibling has, and extMarketSwap was reachable by a non-controller. Fixed.

Where we could not close the loop: you flagged your own confidence honestly on the vault arrears window, noting you had not established the precondition. Verification could not establish it either. It is left where you left it — open and honestly labelled — rather than quietly claimed as resolved.

The code is in #30, the first push to this mirror since the July snapshot. Your line numbers are against 0241cba and still resolve. The SECURITY.md advisory link — which 404'd and is why this report is public at all — is fixed in that same drop.