VaultLock credits the repayment of a loan issued after a lock to the locked shares that never funded it, so a borrow-then-repay round trip that leaves the vault byte-identical moves instant-withdrawal cash from the stayers to a locked exiter

Start with src/backend/lib/VaultLock.mo, specifically the settle and repayment logic around lines 28-41 and 181-215, then trace how main.mo calls reprovisionPool and settleVaultLocksNet. Run the repro.mo files from the repo root using the moc command in the issue to see the expected eA and eB values. Done means a borrow followed by its repayment leaves every lock and LP balance unchanged, with tests added in tests/VaultLock.test.mo.

Severity (proposed): Medium. Category: Solvency and conservation (AMM vault: allocation of held cash and loan-book exposure between LPs).

It breaks a stated guarantee: F1 (docs/amm-vault-design.md:291-299) says no LP can take more than their own share of held assets "across ANY number" of withdrawals, so "a first-come drain of the cash is impossible by construction". Any registered principal can trigger it on #play, and ordinary margin churn triggers it with no attacker. Medium, not High, because it is NAV-neutral (nothing is minted or lost; what moves is instant-withdrawal priority and who is left holding the loan book) and the preconditions are narrow (a lock exists only after an exit made while loans were outstanding; a deliberate wash needs vault borrow room). On #play the amounts are play money.

Summary

VaultLock (task 1788475756) fully locks the remaining shares of an LP who takes their cash share, closing the harmonic drain of the stayers' liquidity. Only a repayment releases a lock, pro rata to every LP's loan claim λ_i ("all loans are one class").

A loan issued after a lock is funded only by unlocked shares (locked shares hold no cash), but its repayment is released pro rata to every λ_i, locked shares included. A borrow followed by its repayment leaves H, L, NAV, S and every LP balance byte-identical, yet transfers a·λ_locked/(Lx + a) of instant-cash entitlement from the unlocked LPs to the locked ones. Repeated washes, deliberate or organic, drive Λ to 0 and restore the stateless cap and its harmonic drain.

Affected surface

Exchange canister at 7bcdde6 (1.80; the same code shipped in 1.75). Public methods, none gated on DEPLOY_MODE: withdrawLp (main.mo:22080), getMaxInstantWithdraw (:22335), createMarginPool (:14865), fundMarginPool (:14938), openPosition (:15061), closePosition (:15498), repayPoolDebt (:15035).

• src/backend/lib/VaultLock.mo:28-41: repayment released pro rata to λ_i; issuance claimed to "change no lock". settle at :181-215 applies the common factor c whenever repaidUsd > 0 (:195-207).
• src/backend/main.mo:3568-3571: poolFundForFill borrows (BorrowEngine.borrow debits the vault, BorrowEngine.mo:361-364), then reprovisionPool(party). Repayments reach reprovisionPool from deleveragePool (main.mo:7078) and repayPoolDebt (:15050); BorrowEngine.repay credits the vault (BorrowEngine.mo:426-427).
• src/backend/main.mo:19537-19640: vaultLockRepaidUsd (per-token shrink since the snapshot), vaultLockSnapshotNow, vaultLockClear, settleVaultLocksNet (settle, then re-snapshot), the task 1788727876 rationale (:19613-19636), settleVaultLocksOnMutation; called from reprovisionPool (:19768-19776).
• src/backend/main.mo:21680-21749: performLpWithdraw settles, caps by withinCap (:21683), re-locks via lockAfterExit (:21749).
• docs/amm-vault-design.md:207-299: the lock model (:207-227) and F1 (:291-299).
• tests/VaultLock.test.mo:87-89: issuance is tested only as "NAV up, H unchanged, R = 0". The vault's real issuance shape (H down by a, NAV unchanged) and a borrow followed by its repayment are never tested.

Mechanism

The lib prices every repayment against every loan claim, with no notion of when the repaid loan was issued (VaultLock.mo:28-30, :39-41):

// REPAYMENT. A net repayment R converts loan value into cash for every LP
// PRO RATA TO THEIR LOAN CLAIM λ_i = s_i·NAV/S − e_i (all loans are one
// class, so a repayment cannot tell whose loan it was): ...
// ISSUANCE and interest accrual change no lock: cash leaves every unlocked
// share uniformly and the loan claim grows uniformly, ...

The issuance statement holds per unlocked share only. A fully locked LP has e_i = 0, so issuance cannot touch their cash and their λ_i does not grow; the whole issuance a lands on the unlocked shares' λ.

At the borrow, poolFundForFill → reprovisionPool → settleVaultLocksOnMutation → settleVaultLocksNet. vaultLockRepaidUsd() is 0 (units only grew; if (snap > cur)), so c = 1, and vaultLockSnapshotNow() then includes the new loan. When it is repaid (deleveragePool at :7078, or repayPoolDebt at :15050), the next settle sees R = snap − cur = a, and settle (VaultLock.mo:195-206) computes c < 1 on every lock. The locked LP's e rises by a·λ_locked/(Lx + a); the unlocked LPs' e falls by the same amount; H and NAV are back where they were.

The borrow-site snapshot (main.mo:19626-19628, task 1788727876) was added to close the repay-then-reborrow order; it makes every borrow-then-repay pair register as a repayment. Even without it, a pair straddling any LP touch or heartbeat settle would transfer, so the defect is in the model, not the hook: the lib's arithmetic is correct, but it charges issuance to unlocked shares and credits its repayment across locked shares too, so the lock index is path-dependent.

Reproduction

Executed: the lock arithmetic against the unmodified src/backend/lib/VaultLock.mo, called as main.mo calls it (settle / capLp / lockAfterExit / rawFor for an exit, settle(…, 0) at a borrow, settle(…, a) at its repay); wash fees, interest and spread are not modelled. Traced only: the main.mo path and the trigger below; no replica was run. Each file runs from the repo root with:

moc $(mops sources) --package mdex src/backend --implicit-package=core -r repro.mo

Trigger (#play, non-controller principals only)

1. Victim B and attacker A are LPs in a vault with loans outstanding.
2. A calls withdrawLp for the cap getMaxInstantWithdraw shows. performLpWithdraw pays A their cash share and lockAfterExit locks all of A's remaining shares; a second withdrawLp is refused ("Withdrawable now: $0").
3. A, or anyone, borrows from the vault at a fill and repays it: e.g. createMarginPool + fundMarginPool, openPosition short where the vault has room (outstanding_T + a ≤ 0.5 × held_T, BorrowEngine.mo:191-197; the fill borrows via poolFundForFill, R = 0), then closePosition (deleveragePool, R = a); or a long, then repayPoolDebt. Cost: two 10 bp taker legs (main.mo:7343) plus spread.
4. A's getMaxInstantWithdraw is now above 0 and B's has fallen. A withdraws again; repeat 3-4.

Run 1: minimal round trip

State after A's max exit (no fee): S = 150k LP, A = 50k fully locked, B = 100k, H = $50k, NAV = $150k. Loan a = $10k.

import VL "mo:mdex/lib/VaultLock";
import Debug "mo:core/Debug";
let E8 : Nat = 100_000_000;
// post A-max-exit, no fee: S=150k, A=50k fully locked, B=100k, H=50k, NAV=150k
let S = 150_000 * E8; let sA = 50_000 * E8; let sB = 100_000 * E8;
var H = 50_000 * E8; let NAV = 150_000 * E8;
let rawA = VL.rawFor(sA, VL.SCALE); var scale = VL.SCALE;
func eA() : Nat { VL.capUsd(sA, VL.lockOf(rawA, scale, sA), S, VL.totalLock(rawA, scale, S), H, 10_000) };
func eB() : Nat { VL.capUsd(sB, 0, S, VL.totalLock(rawA, scale, S), H, 10_000) };
Debug.print("before: eA=" # debug_show (eA()/E8) # " eB=" # debug_show (eB()/E8));
let a = 10_000 * E8;
H -= a; scale := VL.settle(scale, rawA, S, H, NAV, 0).scale;          // borrow at fill, R=0
Debug.print("after borrow: eA=" # debug_show (eA()/E8) # " eB=" # debug_show (eB()/E8));
H += a; scale := VL.settle(scale, rawA, S, H, NAV, a).scale;          // repay, R=a
Debug.print("after repay (H,NAV,S identical): eA=" # debug_show (eA()/E8) # " eB=" # debug_show (eB()/E8) # "  expected eA = a*50k/110k = 4545");

before: eA=0 eB=50_000
after borrow: eA=0 eB=40_000
after repay (H,NAV,S identical): eA=4_545 eB=45_454  expected eA = a*50k/110k = 4545

Run 2: per-token borrow cap honoured

Five legs at $1/unit: $20k held in each of BTC, ETH, SOL, ICP, ICPUSD (H = $100k); $10k BTC and $10k ICPUSD outstanding (L = $20k, so those legs have no room); A and B hold 60k LP each. A "wash pass" borrows the full remaining room in every leg that has any, then repays it.

// Wash vs the lock index; per-token cap outstanding_T + a <= 0.5 x held_T honoured; $1/unit.
import VL "mo:mdex/lib/VaultLock";
import Debug "mo:core/Debug";
let KEEP : Nat = 9_960; let E8 : Nat = 100_000_000;
// held: BTC ETH SOL ICP ICPUSD = $20k each (H $100k); out: BTC $10k, ICPUSD $10k (L $20k) -> no room in BTC/ICPUSD
let held : [var Nat] = [var 20_000*E8, 20_000*E8, 20_000*E8, 20_000*E8, 20_000*E8];
let out  : [var Nat] = [var 10_000*E8, 0, 0, 0, 10_000*E8];
var S : Nat = 120_000 * E8; var sA : Nat = 60_000 * E8; let sB : Nat = 60_000 * E8;
var rawA : Nat = 0; var rawSum : Nat = 0; var scale : Nat = VL.SCALE;
func sum(a : [var Nat]) : Nat { var t = 0; for (x in a.vals()) { t += x }; t };
func H() : Nat { sum(held) }; func L() : Nat { sum(out) }; func nav() : Nat { H() + L() };
func lockA() : Nat { VL.lockOf(rawA, scale, sA) };
func lam() : Nat { VL.totalLock(rawSum, scale, S) };
func eA() : Nat { VL.capUsd(sA, lockA(), S, lam(), H(), 10_000) };
func eB() : Nat { VL.capUsd(sB, 0, S, lam(), H(), 10_000) };
func settle(r : Nat) { let s = VL.settle(scale, rawSum, S, H(), nav(), r); if (s.clear) { rawA := 0; rawSum := 0; scale := VL.SCALE } else { scale := s.scale } };
func usd(x : Nat) : Text { debug_show (x / E8) };
func maxExitA() : Nat {
  settle(0);
  let myLock = lockA(); let lt = lam(); let h = H(); let n = nav();
  let x = VL.capLp(sA, myLock, S, lt, h, n);
  if (x == 0) { return 0 };
  let paid = x * n * KEEP / (S * 10_000);
  let newLock = VL.lockAfterExit(sA, myLock, x, S, lt, h, n);
  var i = 0; while (i < 5) { held[i] -= held[i] * paid / h; i += 1 };   // in-kind pro-rata basket
  S -= x; sA -= x;
  let newRaw = VL.rawFor(newLock, scale);
  rawSum := (if (rawSum > rawA) { (rawSum - rawA : Nat) } else { 0 }) + newRaw; rawA := newRaw;
  paid
};
var notional = 0;
func washAll() {   // one max-room borrow+repay per leg that has room
  var i = 0;
  while (i < 5) {
    let cap = held[i] / 2;
    if (cap > out[i]) {
      let a : Nat = cap - out[i];
      notional += a;
      held[i] -= a; out[i] += a; settle(0);   // borrow at the fill: R = 0, snapshot moves
      held[i] += a; out[i] -= a; settle(a);   // repay (deleveragePool / repayPoolDebt): R = a
    };
    i += 1;
  };
};
Debug.print("start: H=$" # usd(H()) # " L=$" # usd(L()) # " eA=$" # usd(eA()) # " eB=$" # usd(eB()));
var takenA = maxExitA();
Debug.print("A max exit took $" # usd(takenA) # "; then eA=$" # usd(eA()) # " eB=$" # usd(eB()) # " H=$" # usd(H()) # "; second exit takes $" # usd(maxExitA()));
let h0 = H(); let l0 = L(); let s0 = S; let b0 = eB();
washAll();
assert (H() == h0 and L() == l0 and S == s0);
Debug.print("after 1 wash pass (H,L,NAV,S identical): eA=$" # usd(eA()) # " eB=$" # usd(b0) # "->$" # usd(eB()) # " notional $" # usd(notional));
var r = 0;
while (r < 20) { washAll(); takenA += maxExitA(); r += 1; if (r <= 4 or r == 10) { Debug.print("  round " # debug_show r # ": A total taken $" # usd(takenA) # ", eB=$" # usd(eB()) # ", lockA=" # usd(lockA()) # " of sA=" # usd(sA) # ", notional so far $" # usd(notional)) } };
Debug.print("after 20 x (wash pass + A max exit): A took $" # usd(takenA) # " total"
  # "; eB=$" # usd(eB()) # " of B NAV $" # usd(sB * nav() / S) # "; H=$" # usd(H()) # " L=$" # usd(L()) # "; wash notional $" # usd(notional));

start: H=$100_000 L=$20_000 eA=$50_000 eB=$50_000
A max exit took $49_800; then eA=$0 eB=$50_200 H=$50_200; second exit takes $0
after 1 wash pass (H,L,NAV,S identical): eA=$4_501 eB=$50_200->$45_698 notional $15_060
  round 1: A total taken $55_952, eB=$44_047, lockA=3_840 of sA=3_840, notional so far $30_120
  round 2: A total taken $57_532, eB=$42_467, lockA=2_258 of sA=2_258, notional so far $43_334
  round 3: A total taken $58_439, eB=$41_560, lockA=1_351 of sA=1_351, notional so far $56_074
  round 4: A total taken $58_974, eB=$41_025, lockA=816 of sA=816, notional so far $68_542
  round 10: A total taken $59_747, eB=$40_252, lockA=42 of sA=42, notional so far $141_514
after 20 x (wash pass + A max exit): A took $59_789 total; eB=$40_210 of B NAV $60_209; H=$40_210 L=$20_000; wash notional $262_176

One pass leaves H, L, NAV and S identical (asserted). After about $56k of wash notional (roughly $112 of taker fees at 20 bp per round trip, plus spread), A has taken $58.4k against the $49.8k the lock allows, while the whole $20k book is still outstanding. At the end B's $60.2k NAV is $40.2k cash plus the entire $20k book.

Run 3: ambient churn, no attacker

S = 200k LP, A = B = 100k, H = L = $100k. A makes one max exit; then only third-party borrow/repay pairs of H/8 (cap room assumed) run, with A idle.

// Ambient churn: one locked exiter, then third-party borrow+repay pairs only.
// borrow = H -= a, L += a, settle(R = 0); repay = H += a, L -= a, settle(R = a)
import VL "mo:mdex/lib/VaultLock";
import Debug "mo:core/Debug";
let E8 : Nat = 100_000_000; let KEEP : Nat = 9_960;
var S : Nat = 200_000 * E8; var sA : Nat = 100_000 * E8; let sB : Nat = 100_000 * E8;
var H : Nat = 100_000 * E8; var L : Nat = 100_000 * E8;
var rawA : Nat = 0; var rawSum : Nat = 0; var scale : Nat = VL.SCALE;
func nav() : Nat { H + L };
func lockA() : Nat { VL.lockOf(rawA, scale, sA) };
func lam() : Nat { VL.totalLock(rawSum, scale, S) };
func eA() : Nat { VL.capUsd(sA, lockA(), S, lam(), H, 10_000) };
func eB() : Nat { VL.capUsd(sB, 0, S, lam(), H, 10_000) };
func d(x : Nat) : Text { debug_show (x / E8) };   // whole dollars / whole LP
func settle(r : Nat) {
  let s = VL.settle(scale, rawSum, S, H, nav(), r);
  if (s.clear) { rawA := 0; rawSum := 0; scale := VL.SCALE } else {
    scale := s.scale;
    if (VL.needsRenorm(scale)) { rawA := VL.renormRaw(rawA, scale); rawSum := rawA; scale := VL.SCALE };
  };
};
// A's max exit, as performLpWithdraw does it
settle(0);
let x = VL.capLp(sA, 0, S, 0, H, nav());
let paid = x * nav() * KEEP / (S * 10_000);
let nl = VL.lockAfterExit(sA, 0, x, S, 0, H, nav());
S -= x; sA -= x; H -= paid; rawA := VL.rawFor(nl, scale); rawSum := rawA;
Debug.print("A max exit took $" # d(paid) # ": lockA=" # d(lockA()) # " of sA=" # d(sA) # " eA=$" # d(eA()) # " eB=$" # d(eB()));
var j = 0;
while (j < 100) {
  let a = H / 8; let h0 = H; let l0 = L;
  H -= a; L += a; settle(0); H += a; L -= a; settle(a);
  assert (H == h0 and L == l0);
  j += 1;
  if (j == 1 or j == 10 or j == 100) {
    Debug.print("after " # debug_show j # " third-party washes (H, L, S unchanged): lockA=" # d(lockA()) # " eA=$" # d(eA()) # " eB=$" # d(eB()) # " stateless sA/S*H=$" # d(sA * H / S));
  };
};

A max exit took $49_800: lockA=50_000 of sA=50_000 eA=$0 eB=$50_200
after 1 third-party washes (H, L, S unchanged): lockA=43_742 eA=$2_956 eB=$47_243 stateless sA/S*H=$16_733
after 10 third-party washes (H, L, S unchanged): lockA=10_018 eA=$14_338 eB=$35_861 stateless sA/S*H=$16_733
after 100 third-party washes (H, L, S unchanged): lockA=0 eA=$16_733 eB=$33_466 stateless sA/S*H=$16_733

Every pair leaves H, L and S unchanged (asserted), yet A's lock decays to 0 and A's entitlement reaches the stateless cap s_A/S × H exactly; B's instant cash falls from $50.2k to $33.5k. On a busy venue, locks decay to the pre-lock behaviour unaided.

Impact

Established (lib executed, call path traced): each post-lock borrow/repay pair moves a·λ_locked/(Lx + a) of instant-withdrawal entitlement from unlocked to locked LPs; repeated, a locked exiter turns their whole remaining loan claim into the stayers' cash ahead of the book repaying (the drain the lock was built to stop); ordinary third-party churn does the same with no attacker.

Bounds. No NAV changes; A's extra cash is bounded by A's own remaining NAV; the stayers' larger loan-book share becomes cash as loans repay.

Conditional, not shown as a realised loss. Losses are allocated one share class (docs/amm-vault-design.md:345-348), so an exiter who washed out of their locked shares escapes more of a later default: in Run 2, B ends up carrying the entire $20k book. An LP expecting a default could exit first this way.

Relationship to existing reports

• #62 (OhShii Labs, round 19), regression table row on VaultLock. It found "Σ caps = holdings … no LP transfer exists". Σ caps = H still holds; the borrow-then-repay pair is an LP-to-LP transfer that row did not exercise. The 1.75 code it audited already had the borrow-site settle, so this is not a 1.80 regression.
• #67 (OhShii Labs, round 20), negative result on liquidation, write-off and LP withdrawal limits. It found "the lock index moved only by cash actually received". That stays true here; the question is who that cash is attributed to, since it is the return of a loan the locked shares never funded.
• Task 1788727876 (docs/amm-vault-design.md:324-329, main.mo:19613-19636) closed the opposite order (repay-then-reborrow netting to R = 0). This builds on that fix.
• Task 1788752774 / disclosed residuals (i)-(iii) (docs/amm-vault-design.md:330-348) cover write-offs and losses, not cash-backed repayment of post-lock issuance.
• F1 (docs/amm-vault-design.md:291-299) is the guarantee broken; nothing in the docs accepts the round-trip asymmetry as a trade-off.

Suggested fix

Attribute cash-backed repayments to post-lock issuance first, reusing the netting settleVaultLocksNet already applies to write-offs (main.mo:19585: SafeMath.subOrZero(vaultLockRepaidUsd(), writtenOffUsd)):

1. Keep a stable per-token vaultLockIssuedUnits : Map<Text, Nat> (additive field, with a migration entry).
2. In poolFundForFill's #ok arm (main.mo:3569-3570), add short to vaultLockIssuedUnits[token] while vaultLockRawSum > 0, before reprovisionPool. Count only the borrow, not interest: interest accrues to every share one-class, so its repayment is correctly pooled. (The other BorrowEngine.borrow call, at :15468, is a discarded query simulation.)
3. In vaultLockRepaidUsd's per-token loop (:19537-19548), net each token's shrink first: n = min(d, issued_T), issued_T -= n, and price only d − n.
4. Clear the map in vaultLockClear (:19554-19558).

A borrow and its repayment then settle with R = 0 and the cash returns to the unlocked shares that lent it; only repayment beyond post-lock issuance releases locks. When an older loan repays while newer issuance is outstanding this under-releases, which is the conservative direction the lib's rounding section and the write-off netting already choose.

Also correct VaultLock.mo:39-41 and docs/amm-vault-design.md:226-227, and add a tests/VaultLock.test.mo case plus a tests/test_vault_lp.sh §7 case: borrow a (H − a, NAV unchanged, settle R = 0), repay a, assert every LP's withdrawableNowUsd is unchanged.

Part 13 of 28 from an independent review of MULTI/DEX 1.80 (7bcdde6), carried out with Claude Opus 5.5. Each finding was checked against the existing issues, advisories and fix briefs before filing; the severity is a proposal under CONTRIBUTORS.md. Where a step says "traced", it was read from source and not executed.