// =============================================================================
// SEEDED RANDOMIZED PROPERTY / STATEFUL-INVARIANT test for AereLendingMarket
// (isolated single-pair money market, immutable LTV) + its oracle adapter.
//
// TOOLCHAIN: hardhat-based randomized invariant fuzzing (NOT Foundry — `forge`
// is not installed here and the repo builds through hardhat with OZ 4.9.6 +
// viaIR + a cancun hardfork override). Per the task we drive long random
// sequences of multi-actor actions with varied amounts / timing / prices via a
// SEEDED mulberry32 PRNG (reproducible) and assert the market invariants AFTER
// EVERY STEP. Every random choice comes from mulberry32(seed); the base seed is
// printed at suite start and can be pinned with FUZZ_SEED. On any invariant
// break the failing action (campaign, step, actor, values, prices) is embedded
// in the assertion message, giving a minimal repro.
//
// INVARIANTS UNDER TEST (the point of the exercise):
//   [SOLV-BORROW]  a successful borrow always leaves the position healthy at the
//                  immutable LTV (colVal*LTV/1e4 >= debtVal); an oversized borrow
//                  reverts (never borrow value beyond collateral capacity).
//   [SOLV-WITHDRAW] a successful collateral withdraw with open debt leaves the
//                  position healthy at LTV; withdrawing all collateral under debt
//                  reverts.
//   [LIQ-GATE]     liquidation succeeds ONLY when genuinely under the liquidation
//                  threshold; a clearly-healthy position reverts PositionHealthy.
//   [LIQ-BOUND]    liquidation never seizes more collateral than the close /
//                  bonus permits (value seized <= value repaid * (1+bonus)); never
//                  seizes more than the borrower holds; liquidator pays <= request
//                  and <= real debt.
//   [LIQ-PAUSE]    liquidation stays available while borrow+deposit are paused.
//   [INDEX-MONO]   borrowIndex and supplyIndex are monotonic non-decreasing.
//   [ACCT-SCALED]  sum(debtOf)==totalBorrowsScaled and
//                  sum(supplierScaled)==totalSuppliedScaled at all times.
//   [ACCT-COL]     sum(collateralOf)==COLLATERAL.balanceOf(market) (collateral
//                  conservation) at all times.
//   [ACCT-DEBT]    every debt-token op moves EXACTLY the expected amount in/out of
//                  the market (transfer consistency; no mint/burn drift).
//   [REPAY-FLOOR]  repay never drives debt negative and never over-charges past
//                  the real debt (clamp), even on gross overpay.
//
// SCOPE: run this file in ISOLATION (the full hardhat suite OOM/segfaults on the
// unrelated ML-DSA PQC KAT tests):
//     npx hardhat test test/invariant-lending-market-property.test.js
// TEST-ONLY: one new file, NO contract logic changed, NOTHING deployed to any
// live node.
// =============================================================================

const { expect } = require("chai");
const { ethers, network } = require("hardhat");

/* ----------------------------- seeded PRNG -------------------------------- */
function mulberry32(a) {
  return function () {
    a |= 0;
    a = (a + 0x6d2b79f5) | 0;
    let t = Math.imul(a ^ (a >>> 15), 1 | a);
    t = (t + Math.imul(t ^ (t >>> 7), 61 | t)) ^ t;
    return ((t ^ (t >>> 14)) >>> 0) / 4294967296;
  };
}
const BASE_SEED = process.env.FUZZ_SEED ? Number(process.env.FUZZ_SEED) : 0x1E4D2800;
function rngFor(tag, campaign) {
  let h = BASE_SEED ^ (campaign * 0x9e3779b1);
  for (let i = 0; i < tag.length; i++) h = (Math.imul(h, 31) + tag.charCodeAt(i)) | 0;
  return mulberry32(h >>> 0);
}
const ri = (rng, min, max) => min + Math.floor(rng() * (max - min + 1)); // inclusive
const pick = (rng, arr) => arr[Math.floor(rng() * arr.length)];
const chance = (rng, p) => rng() < p;

/* ----------------------------- fixed-point USD math ----------------------- */
// Prices are 18-decimal USD-per-whole-token, mirroring AereLendingMarket._price.
const TEN = (n) => 10n ** BigInt(n);
function scaleUp(amount, dec) {
  // dec is always <= 18 in these campaigns; mirrors _scaleUp.
  return dec === 18 ? amount : amount * TEN(18 - dec);
}
function scaleDown(amount18, dec) {
  return dec === 18 ? amount18 : amount18 / TEN(18 - dec);
}
// USD value (18-dec) of `amount` token units, replicating the contract exactly:
//   _scaleUp(amount, dec) * price / 1e18
function usdVal(amount, dec, price) {
  return (scaleUp(amount, dec) * price) / TEN(18);
}

/* ----------------------------- config knobs ------------------------------- */
const N = {
  CAMPAIGNS: Number(process.env.LEND_CAMPAIGNS || 10),
  STEPS: Number(process.env.LEND_STEPS || 70),
};
const DECIMAL_CONFIGS = [
  { col: 18, debt: 6 },
  { col: 8, debt: 6 },
  { col: 18, debt: 18 },
  { col: 6, debt: 18 },
  { col: 8, debt: 8 },
];

async function advance(seconds) {
  await network.provider.send("evm_increaseTime", ["0x" + seconds.toString(16)]);
  await network.provider.send("evm_mine", []);
}

describe("INVARIANT: AereLendingMarket solvency / liquidation / accounting", function () {
  this.timeout(0);

  let signers, ERC20F, OracleF, MarketF;

  before(async function () {
    signers = await ethers.getSigners();
    ERC20F = await ethers.getContractFactory("MockERC20Lending");
    OracleF = await ethers.getContractFactory("MockPriceOracle"); // getPrice(address)->uint256, setRevert
    MarketF = await ethers.getContractFactory("AereLendingMarket");
    console.log(`      [lend] base seed 0x${BASE_SEED.toString(16)}, ${N.CAMPAIGNS} campaigns x ${N.STEPS} steps`);
  });

  it("drives multi-actor supply/borrow/repay/withdraw/liquidate across price moves; invariants hold every step", async function () {
    // Global tallies (asserted at the end to prove the campaigns really exercised each path).
    let steps = 0;
    let okBorrows = 0, okWithdraws = 0, okSupplies = 0, okRedeems = 0, okRepays = 0, okDeposits = 0;
    let liqSuccess = 0, liqHealthyRevert = 0, liqBorderline = 0;
    let oversizedBorrowBlocked = 0, oversizedWithdrawBlocked = 0;
    let overpayRepays = 0, pauseLiqProbes = 0;
    let invariantChecks = 0;

    for (let c = 0; c < N.CAMPAIGNS; c++) {
      const rng = rngFor("lend", c);

      // ---- random-but-valid market config for this campaign ----
      const dc = pick(rng, DECIMAL_CONFIGS);
      const colDec = dc.col, debtDec = dc.debt;
      const ltvBps = ri(rng, 3000, 8500);
      const liqThresholdBps = ri(rng, ltvBps, Math.min(9500, ltvBps + 1200)); // >= ltv, < 10000
      const liqBonusBps = ri(rng, 100, 1500);
      const borrowFeeBps = ri(rng, 0, 3000);

      const collateral = await ERC20F.deploy("COL", "COL", colDec);
      await collateral.waitForDeployment();
      const debt = await ERC20F.deploy("DEBT", "DEBT", debtDec);
      await debt.waitForDeployment();
      const oracle = await OracleF.deploy();
      await oracle.waitForDeployment();
      const colAddr = await collateral.getAddress();
      const debtAddr = await debt.getAddress();

      // Prices in 18-dec USD. Start both at $1.00.
      let colPrice = TEN(18);   // $1
      let debtPrice = TEN(18);  // $1
      await (await oracle.setPrice(colAddr, colPrice)).wait();
      await (await oracle.setPrice(debtAddr, debtPrice)).wait();

      const marketCap = 100_000_000n * TEN(debtDec); // effectively non-binding
      const market = await MarketF.deploy({
        collateral: colAddr,
        debtToken: debtAddr,
        sink: signers[9].address, // never flushed in this test; just needs to be nonzero
        oracle: await oracle.getAddress(),
        ltvBps, liqThresholdBps, liqBonusBps, borrowFeeBps,
        marketDebtCap: marketCap,
        collateralDecimals: colDec,
        debtDecimals: debtDec,
      });
      await market.waitForDeployment();
      const mAddr = await market.getAddress();
      const owner = signers[0];

      // Actors: users borrow/supply; a dedicated liquidator only liquidates.
      const users = [signers[1], signers[2], signers[3], signers[4], signers[5]];
      const liquidator = signers[6];
      const allCollateralHolders = [...users, liquidator]; // for the collateral-sum invariant

      // Fund + approve generously (fresh tokens per campaign, so balances don't leak state).
      const bigCol = 10_000_000n * TEN(colDec);
      const bigDebt = 10_000_000n * TEN(debtDec);
      for (const u of [...users, liquidator]) {
        await (await collateral.mint(u.address, bigCol)).wait();
        await (await debt.mint(u.address, bigDebt)).wait();
        await (await collateral.connect(u).approve(mAddr, ethers.MaxUint256)).wait();
        await (await debt.connect(u).approve(mAddr, ethers.MaxUint256)).wait();
      }

      // Seed deep debt-token liquidity so borrows are not liquidity-starved.
      await (await market.connect(users[0]).supply(2_000_000n * TEN(debtDec))).wait();
      await (await market.connect(users[1]).supply(1_000_000n * TEN(debtDec))).wait();

      // Give each borrower some starting collateral so early borrows can happen.
      for (const u of users) {
        await (await market.connect(u).depositCollateral(BigInt(ri(rng, 500, 5000)) * TEN(colDec))).wait();
      }

      let prevBorrowIndex = await market.borrowIndex();
      let prevSupplyIndex = await market.supplyIndex();

      // ---- the core invariant checker, run after EVERY step ----
      async function assertInvariants(ctx) {
        // [INDEX-MONO]
        const bi = await market.borrowIndex();
        const si = await market.supplyIndex();
        expect(bi, `[INDEX-MONO] borrowIndex decreased | ${ctx}`).to.be.gte(prevBorrowIndex);
        expect(si, `[INDEX-MONO] supplyIndex decreased | ${ctx}`).to.be.gte(prevSupplyIndex);
        prevBorrowIndex = bi;
        prevSupplyIndex = si;

        // [ACCT-SCALED] sum(debtOf)==totalBorrowsScaled, sum(supplierScaled)==totalSuppliedScaled
        let sumDebt = 0n, sumSup = 0n, sumCol = 0n;
        for (const u of allCollateralHolders) {
          sumDebt += await market.debtOf(u.address);
          sumSup += await market.supplierScaled(u.address);
          sumCol += await market.collateralOf(u.address);
        }
        expect(sumDebt, `[ACCT-SCALED] sum(debtOf)!=totalBorrowsScaled | ${ctx}`).to.equal(await market.totalBorrowsScaled());
        expect(sumSup, `[ACCT-SCALED] sum(supplierScaled)!=totalSuppliedScaled | ${ctx}`).to.equal(await market.totalSuppliedScaled());

        // [ACCT-COL] collateral conservation
        expect(sumCol, `[ACCT-COL] sum(collateralOf)!=market collateral balance | ${ctx}`).to.equal(await collateral.balanceOf(mAddr));

        invariantChecks++;
      }

      await assertInvariants(`c${c} seed setup`);

      // Compute a user's remaining borrow capacity (in debt-token units) from on-chain state.
      async function remainingBorrowTokens(u) {
        const col = await market.collateralOf(u.address);
        const debtReal = await market.debtBalance(u.address);
        const colValue = usdVal(col, colDec, colPrice);
        const debtValue = usdVal(debtReal, debtDec, debtPrice);
        const maxDebtValue = (colValue * BigInt(ltvBps)) / 10_000n;
        if (maxDebtValue <= debtValue) return 0n;
        const remainingValue = maxDebtValue - debtValue;
        // value -> debt tokens: value18 / price -> 18dec token, then scaleDown to debtDec
        const tokens18 = (remainingValue * TEN(18)) / debtPrice;
        return scaleDown(tokens18, debtDec);
      }

      for (let s = 0; s < N.STEPS; s++) {
        const action = pick(rng, [
          "borrow", "borrow", "repay", "supply", "redeem", "deposit", "deposit",
          "withdraw", "price", "price", "accrue", "liquidate", "liquidate",
          "oversizedBorrow", "oversizedWithdraw", "setRate",
        ]);
        const u = pick(rng, users);
        const ctx = () => `c${c} s${s} act=${action} actor=${users.indexOf(u) + 1} colDec=${colDec} debtDec=${debtDec} ltv=${ltvBps} liqTh=${liqThresholdBps} bonus=${liqBonusBps} fee=${borrowFeeBps} colPx=${colPrice} debtPx=${debtPrice}`;

        try {
          if (action === "accrue") {
            await advance(ri(rng, 1, 90 * 24 * 3600)); // up to ~90 days
            await (await market.accrueInterest()).wait();

          } else if (action === "price") {
            // Move collateral price (cents in [15c, 320c]) and debt price ([90c,110c]).
            colPrice = BigInt(ri(rng, 15, 320)) * TEN(16);
            debtPrice = BigInt(ri(rng, 90, 110)) * TEN(16);
            await (await oracle.setPrice(colAddr, colPrice)).wait();
            await (await oracle.setPrice(debtAddr, debtPrice)).wait();

          } else if (action === "setRate") {
            // Owner bumps the borrow rate (bounded by the contract's own cap).
            const cap = 317_097_919_837_645_865_000n;
            const rate = BigInt(ri(rng, 1, 100)) * (cap / 100n);
            await (await market.connect(owner).setBorrowRate(rate)).wait();

          } else if (action === "deposit") {
            const amt = BigInt(ri(rng, 1, 5000)) * TEN(colDec);
            await (await market.connect(u).depositCollateral(amt)).wait();
            okDeposits++;

          } else if (action === "supply") {
            const amt = BigInt(ri(rng, 1, 100000)) * TEN(debtDec);
            const before = await debt.balanceOf(mAddr);
            await (await market.connect(u).supply(amt)).wait();
            expect((await debt.balanceOf(mAddr)) - before, `[ACCT-DEBT] supply delta | ${ctx()}`).to.equal(amt);
            okSupplies++;

          } else if (action === "redeem") {
            // Best-effort: bounded by user's real balance and available liquidity.
            const bal = await market.supplierBalance(u.address);
            if (bal > 0n) {
              const amt = (bal * BigInt(ri(rng, 1, 100))) / 100n;
              if (amt > 0n) {
                const before = await debt.balanceOf(mAddr);
                await (await market.connect(u).redeem(amt)).wait();
                expect(before - (await debt.balanceOf(mAddr)), `[ACCT-DEBT] redeem delta | ${ctx()}`).to.equal(amt);
                okRedeems++;
              }
            }

          } else if (action === "borrow") {
            const remain = await remainingBorrowTokens(u);
            if (remain > 0n) {
              const liq = (await debt.balanceOf(mAddr)) - (await market.pendingSinkFee());
              let amt = (remain * BigInt(ri(rng, 30, 92))) / 100n;
              if (amt > liq - 1n) amt = liq > 1n ? liq - 1n : 0n;
              if (amt > 0n) {
                const before = await debt.balanceOf(mAddr);
                await (await market.connect(u).borrow(amt)).wait();
                expect(before - (await debt.balanceOf(mAddr)), `[ACCT-DEBT] borrow delta | ${ctx()}`).to.equal(amt);
                okBorrows++;
                // [SOLV-BORROW]: position must be healthy at LTV right after a successful borrow.
                const col = await market.collateralOf(u.address);
                const dReal = await market.debtBalance(u.address);
                const cv = usdVal(col, colDec, colPrice);
                const dv = usdVal(dReal, debtDec, debtPrice);
                expect((cv * BigInt(ltvBps)) / 10_000n, `[SOLV-BORROW] borrowed into insolvency | ${ctx()} col=${col} debt=${dReal}`).to.be.gte(dv);
              }
            }

          } else if (action === "oversizedBorrow") {
            // Deliberately request far beyond capacity: MUST revert (never over-borrow).
            const remain = await remainingBorrowTokens(u);
            const base = remain > 0n ? remain : 1n * TEN(debtDec);
            const amt = base * 5n + 1000n * TEN(debtDec);
            await expect(market.connect(u).borrow(amt), `[SOLV-BORROW] oversized borrow did NOT revert | ${ctx()}`).to.be.reverted;
            oversizedBorrowBlocked++;

          } else if (action === "repay") {
            const dReal = await market.debtBalance(u.address);
            if (dReal > 0n) {
              const overpay = chance(rng, 0.35);
              const amt = overpay ? dReal + BigInt(ri(rng, 1, 5000)) * TEN(debtDec) : (dReal * BigInt(ri(rng, 1, 100))) / 100n;
              if (amt > 0n) {
                const payerBefore = await debt.balanceOf(u.address);
                const mBefore = await debt.balanceOf(mAddr);
                await (await market.connect(u).repay(amt)).wait();
                const paid = payerBefore - (await debt.balanceOf(u.address));
                // [ACCT-DEBT] market received exactly `paid`.
                expect((await debt.balanceOf(mAddr)) - mBefore, `[ACCT-DEBT] repay delta | ${ctx()}`).to.equal(paid);
                // [REPAY-FLOOR] never pull more than the payer offered.
                expect(paid, `[REPAY-FLOOR] charged more than offered | ${ctx()} amt=${amt} paid=${paid}`).to.be.lte(amt);
                // debtReal only grows between the view-read and the tx (accrual runs inside repay),
                // so a small slack covers up to one block of interest.
                const accrualSlack = dReal / 1_000_000n + 2n * TEN(debtDec);
                if (overpay) {
                  // [REPAY-FLOOR] a gross overpay clamps to the real debt (never over-charges) and zeroes it.
                  expect(await market.debtBalance(u.address), `[REPAY-FLOOR] overpay did not zero debt | ${ctx()}`).to.equal(0n);
                  expect(paid, `[REPAY-FLOOR] overpay took more than real debt | ${ctx()} dReal=${dReal} paid=${paid}`).to.be.lte(dReal + accrualSlack);
                  overpayRepays++;
                } else {
                  // amt <= dReal(view) <= dReal(tx), so the clamp does not bind: exactly `amt` is applied.
                  expect(paid, `[REPAY-FLOOR] partial repay applied != offered | ${ctx()} amt=${amt} paid=${paid}`).to.equal(amt);
                }
                okRepays++;
              }
            }

          } else if (action === "withdraw") {
            const col = await market.collateralOf(u.address);
            if (col > 0n) {
              const amt = (col * BigInt(ri(rng, 1, 100))) / 100n;
              if (amt > 0n) {
                const hadDebt = (await market.debtBalance(u.address)) > 0n;
                const before = await collateral.balanceOf(mAddr);
                try {
                  await (await market.connect(u).withdrawCollateral(amt)).wait();
                  expect(before - (await collateral.balanceOf(mAddr)), `[ACCT-COL] withdraw delta | ${ctx()}`).to.equal(amt);
                  okWithdraws++;
                  if (hadDebt) {
                    // [SOLV-WITHDRAW]: still healthy at LTV after pulling collateral out.
                    const nc = await market.collateralOf(u.address);
                    const dReal = await market.debtBalance(u.address);
                    const cv = usdVal(nc, colDec, colPrice);
                    const dv = usdVal(dReal, debtDec, debtPrice);
                    expect((cv * BigInt(ltvBps)) / 10_000n, `[SOLV-WITHDRAW] withdrew into insolvency | ${ctx()} nc=${nc} debt=${dReal}`).to.be.gte(dv);
                  }
                } catch (e) {
                  // A revert is only acceptable if the position had debt (health guard) or dust rounding.
                  // If it had NO debt, withdraw of an owned amount must succeed.
                  if (!hadDebt) throw e;
                }
              }
            }

          } else if (action === "oversizedWithdraw") {
            // Withdraw ALL collateral while holding debt MUST revert (health guard).
            const col = await market.collateralOf(u.address);
            const dReal = await market.debtBalance(u.address);
            if (col > 0n && dReal > 0n) {
              await expect(market.connect(u).withdrawCollateral(col), `[SOLV-WITHDRAW] full withdraw under debt did NOT revert | ${ctx()}`).to.be.reverted;
              oversizedWithdrawBlocked++;
            }

          } else if (action === "liquidate") {
            // Sync interest, then read the health factor at the liquidation threshold.
            await (await market.accrueInterest()).wait();
            const target = pick(rng, users);
            const dReal = await market.debtBalance(target.address);
            const colBefore = await market.collateralOf(target.address);
            if (dReal === 0n) {
              // [LIQ-GATE] no debt => not liquidatable.
              await expect(market.connect(liquidator).liquidate(target.address, 1n * TEN(debtDec)),
                `[LIQ-GATE] liquidated a zero-debt position | ${ctx()}`).to.be.revertedWithCustomError(market, "PositionHealthy");
              liqHealthyRevert++;
            } else {
              const hf = await market.healthFactor(target.address); // >=10000 healthy@threshold, <10000 liquidatable
              const repayReq = (dReal * BigInt(ri(rng, 10, 100))) / 100n + 1n;
              if (hf >= 10100n) {
                // [LIQ-GATE] clearly healthy => must revert.
                await expect(market.connect(liquidator).liquidate(target.address, repayReq),
                  `[LIQ-GATE] liquidated a healthy position hf=${hf} | ${ctx()}`).to.be.revertedWithCustomError(market, "PositionHealthy");
                liqHealthyRevert++;
              } else if (hf <= 9900n) {
                // [LIQ-GATE] clearly under threshold => must succeed and respect the seize bound.
                const kDebtBefore = await debt.balanceOf(liquidator.address);
                const kColBefore = await collateral.balanceOf(liquidator.address);
                const mColBefore = await collateral.balanceOf(mAddr);
                const mDebtBefore = await debt.balanceOf(mAddr);
                await (await market.connect(liquidator).liquidate(target.address, repayReq)).wait();
                const paid = kDebtBefore - (await debt.balanceOf(liquidator.address));
                const seized = (await collateral.balanceOf(liquidator.address)) - kColBefore;

                // [ACCT-DEBT]/[ACCT-COL] transfer consistency for the liquidation legs.
                expect((await debt.balanceOf(mAddr)) - mDebtBefore, `[ACCT-DEBT] liq pay-in delta | ${ctx()}`).to.equal(paid);
                expect(mColBefore - (await collateral.balanceOf(mAddr)), `[ACCT-COL] liq seize delta | ${ctx()}`).to.equal(seized);

                // [LIQ-BOUND] never seize more than the borrower held; borrower col reduced by exactly seized.
                expect(seized, `[LIQ-BOUND] seized more than borrower held | ${ctx()} seized=${seized} colBefore=${colBefore}`).to.be.lte(colBefore);
                expect(await market.collateralOf(target.address), `[LIQ-BOUND] borrower collateral bookkeeping | ${ctx()}`).to.equal(colBefore - seized);

                // [LIQ-BOUND] liquidator paid no more than requested and no more than the real debt (+1s accrual slack).
                const debtSlack = dReal / 1_000_000n + 2n * TEN(debtDec);
                expect(paid, `[LIQ-BOUND] paid more than requested | ${ctx()} paid=${paid} req=${repayReq}`).to.be.lte(repayReq);
                expect(paid, `[LIQ-BOUND] paid more than real debt | ${ctx()} paid=${paid} dReal=${dReal}`).to.be.lte(dReal + debtSlack);

                // [LIQ-BOUND] value seized <= value repaid * (1 + bonus) (+ rounding tolerance of a couple token-units).
                const valPaid = usdVal(paid, debtDec, debtPrice);
                const valSeized = usdVal(seized, colDec, colPrice);
                const allowed = (valPaid * BigInt(10_000 + liqBonusBps)) / 10_000n;
                const tol = usdVal(2n, colDec, colPrice) + usdVal(2n, debtDec, debtPrice) + 1n;
                expect(valSeized, `[LIQ-BOUND] seized value exceeds bonus cap | ${ctx()} valSeized=${valSeized} allowed=${allowed} paid=${paid} seized=${seized}`).to.be.lte(allowed + tol);
                liqSuccess++;
              } else {
                // Borderline band: exercise it but don't strictly gate (rounding across the boundary).
                try {
                  const kColBefore = await collateral.balanceOf(liquidator.address);
                  await (await market.connect(liquidator).liquidate(target.address, repayReq)).wait();
                  const seized = (await collateral.balanceOf(liquidator.address)) - kColBefore;
                  expect(seized, `[LIQ-BOUND] borderline seized more than held | ${ctx()}`).to.be.lte(colBefore);
                } catch (_) { /* PositionHealthy at the exact boundary is acceptable */ }
                liqBorderline++;
              }
            }
          }
        } catch (e) {
          // Best-effort actions (borrow/redeem/withdraw/repay under shifting prices+interest) may
          // legitimately revert; the directed probes above use expect(...).to.be.reverted and are
          // NOT swallowed here because they don't throw on the expected revert. Re-throw anything
          // that is clearly one of OUR invariant assertions.
          if (e && e.message && /\[(SOLV|LIQ|ACCT|INDEX|REPAY)-/.test(e.message)) throw e;
          // otherwise: an ordinary contract revert on a best-effort action — ignore and continue.
        }

        await assertInvariants(ctx());
        steps++;
      }

      // ---- Directed finale per campaign: [LIQ-PAUSE] liquidation survives a full pause. ----
      // Force a borrower deeply underwater via a collateral-price crash, pause borrow+deposit,
      // and prove the liquidation path is still open (and borrow/deposit are genuinely blocked).
      {
        const victim = users[2];
        // Ensure the victim actually has debt; if not, set up a fresh position.
        await (await market.accrueInterest()).wait();
        let vDebt = await market.debtBalance(victim.address);
        if (vDebt === 0n) {
          colPrice = TEN(18); debtPrice = TEN(18);
          await (await oracle.setPrice(colAddr, colPrice)).wait();
          await (await oracle.setPrice(debtAddr, debtPrice)).wait();
          await (await market.connect(victim).depositCollateral(1000n * TEN(colDec))).wait();
          const cap = await remainingBorrowTokens(victim);
          if (cap > 0n) {
            const liq = (await debt.balanceOf(mAddr)) - (await market.pendingSinkFee());
            let amt = (cap * 80n) / 100n;
            if (amt > liq - 1n) amt = liq > 1n ? liq - 1n : 0n;
            if (amt > 0n) await (await market.connect(victim).borrow(amt)).wait();
          }
          vDebt = await market.debtBalance(victim.address);
        }
        const vCol = await market.collateralOf(victim.address);
        if (vDebt > 0n && vCol > 0n) {
          // Crash collateral to ~40% of the exact liquidation-threshold price for THIS position,
          // so it is guaranteed well under threshold regardless of prior collateralisation.
          debtPrice = TEN(18);
          const thresholdColPrice = (scaleUp(vDebt, debtDec) * debtPrice * 10_000n) / (scaleUp(vCol, colDec) * BigInt(liqThresholdBps));
          colPrice = thresholdColPrice * 4n / 10n;
          if (colPrice < 1n) colPrice = 1n;
          await (await oracle.setPrice(colAddr, colPrice)).wait();
          await (await oracle.setPrice(debtAddr, debtPrice)).wait();
          await (await market.connect(owner).setPaused(true, true)).wait(); // borrow + deposit paused
          // Borrow + deposit are blocked while paused...
          await expect(market.connect(users[3]).depositCollateral(1n * TEN(colDec)),
            `[LIQ-PAUSE] deposit not blocked while paused | c${c}`).to.be.revertedWithCustomError(market, "DepositPausedErr");
          await expect(market.connect(users[3]).borrow(1n * TEN(debtDec)),
            `[LIQ-PAUSE] borrow not blocked while paused | c${c}`).to.be.revertedWithCustomError(market, "BorrowPausedErr");
          // ...but liquidation is STILL available.
          const hf = await market.healthFactor(victim.address);
          expect(hf, `[LIQ-PAUSE] victim not underwater after crash hf=${hf} | c${c}`).to.be.lt(10000n);
          const colBefore = await market.collateralOf(victim.address);
          const kColBefore = await collateral.balanceOf(liquidator.address);
          await (await market.connect(liquidator).liquidate(victim.address, vDebt)).wait();
          const seized = (await collateral.balanceOf(liquidator.address)) - kColBefore;
          expect(seized, `[LIQ-PAUSE] liquidation seized nothing while paused | c${c}`).to.be.gt(0n);
          expect(seized, `[LIQ-PAUSE] seized more than held while paused | c${c}`).to.be.lte(colBefore);
          await (await market.connect(owner).setPaused(false, false)).wait();
          pauseLiqProbes++;
        }
        await assertInvariants(`c${c} pause-finale`);
      }
    }

    console.log(`      [lend] steps=${steps} invariantChecks=${invariantChecks}`);
    console.log(`      [lend] borrows=${okBorrows} deposits=${okDeposits} supplies=${okSupplies} redeems=${okRedeems} repays=${okRepays}(overpay=${overpayRepays}) withdraws=${okWithdraws}`);
    console.log(`      [lend] liq: success=${liqSuccess} healthyReverts=${liqHealthyRevert} borderline=${liqBorderline} pauseProbes=${pauseLiqProbes}`);
    console.log(`      [lend] directed: oversizedBorrowBlocked=${oversizedBorrowBlocked} oversizedWithdrawBlocked=${oversizedWithdrawBlocked}`);

    // Coverage floors: prove the campaigns actually exercised the interesting paths.
    expect(invariantChecks, "expected hundreds of full invariant sweeps").to.be.greaterThan(400);
    expect(okBorrows, "expected many successful borrows").to.be.greaterThan(30);
    expect(okRepays, "expected repays").to.be.greaterThan(15);
    expect(liqSuccess, "expected genuine liquidations").to.be.greaterThan(5);
    expect(liqHealthyRevert, "expected healthy-position liquidation reverts").to.be.greaterThan(5);
    expect(oversizedBorrowBlocked, "expected oversized borrows to be blocked").to.be.greaterThan(5);
    expect(pauseLiqProbes, "expected the pause-liquidation probe to run").to.be.greaterThan(0);
  });
});