// Property-based fuzz test for the sAERE + AereSink drip mechanism.
//
// Drives a deterministic pseudo-random walk of 800 user-level actions against
// the live ERC-4626 + 3-bucket-router stack:
//
//   action menu:
//     0  deposit(actor, amount)        — pull WAERE into vault, mint shares
//     1  withdraw(actor, shares)       — burn shares, return WAERE
//     2  sync()                        — permissionless drip refresh
//     3  AereSink.flush(WAERE, amount) — protocol revenue arrives, routes
//                                         STAKER_YIELD_BPS into sAERE then pings
//     4  time-advance(seconds)         — jump anywhere from 1s to ~2 weeks
//
// Invariants verified after EVERY action:
//
//   I-1  totalAssets() <= asset.balanceOf(sAERE)
//   I-2  totalAssets() + _undistributedNow() == asset.balanceOf(sAERE)
//        (exact equality — no epsilon needed; both come from the same balance)
//   I-3  pricePerShare (convertToAssets(1e18)) is monotonically non-decreasing
//        across the whole walk
//   I-4  sync() inside the same block is idempotent — calling it again does
//        not change rewardRate / periodFinish / lastObservedBalance
//   I-5  lastObservedBalance == asset.balanceOf(sAERE) after every state-
//        changing op (deposit / withdraw / sync / sink.flush)
//   I-6  periodFinish never DECREASES from one observation to the next as a
//        consequence of a fresh reward arrival (it only ever resets forward
//        to now + DRIP_DURATION; never backward)
//
// Run:  npx hardhat test test/saere-sink-fuzz.test.js
//
// Deterministic: a fixed PRNG seed drives the action stream so failures
// reproduce exactly.

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

const ONE        = 10n ** 18n;
const DEAD_SEED  = 1000n;
const DEAD_ADDR  = "0x000000000000000000000000000000000000dEaD";
const DRIP_DUR   = 7n * 24n * 60n * 60n; // 7 days in seconds
const NUM_ACTIONS = 800;
const PRNG_SEED   = 0xA3E2E51An; // deterministic — change to re-fuzz

// --------------------------------------------------------------------------
// Tiny deterministic PRNG (xorshift64*). Stable across Node versions.
// --------------------------------------------------------------------------
function makePrng(seed) {
  let s = BigInt.asUintN(64, BigInt(seed));
  if (s === 0n) s = 1n;
  const MASK = (1n << 64n) - 1n;
  return {
    next64() {
      s ^= (s << 13n) & MASK;
      s ^= (s >> 7n)  & MASK;
      s ^= (s << 17n) & MASK;
      s &= MASK;
      return s;
    },
    nextInt(maxExclusive) {
      return Number(this.next64() % BigInt(maxExclusive));
    },
    // returns a bigint in [1n, hi]
    nextBig(hi) {
      const r = this.next64() % BigInt(hi);
      return r + 1n;
    },
  };
}

// --------------------------------------------------------------------------
// Stack deploy. We use the AERE-side of the sink (token == AERE) so no DEX
// router is touched. The sink's BURN bucket is a plain EOA (acts as a sink
// of AERE — no callback). STAKER bucket is the live sAERE vault.
// --------------------------------------------------------------------------
async function deployFuzzStack() {
  const signers = await ethers.getSigners();
  const [deployer, burnSinkEoa, a1, a2, a3, a4, feeder] = signers;
  const actors = [a1, a2, a3, a4];

  const WAERE_F = await ethers.getContractFactory("WAERE");
  const waere = await WAERE_F.deploy();
  await waere.waitForDeployment();
  const waereAddr = await waere.getAddress();

  // Pre-fund deployer dead-seed approval.
  const nonce = await ethers.provider.getTransactionCount(deployer.address);
  const futureSaere = ethers.getCreateAddress({ from: deployer.address, nonce: nonce + 2 });
  await waere.connect(deployer).deposit({ value: DEAD_SEED });
  await waere.connect(deployer).approve(futureSaere, DEAD_SEED);

  const sAERE_F = await ethers.getContractFactory("sAERE");
  const saere = await sAERE_F.deploy(waereAddr);
  await saere.waitForDeployment();
  const saereAddr = await saere.getAddress();

  // Sink — bps 1500 / 4000 / 4500. Router = a dummy EOA (never called on AERE path).
  const Sink_F = await ethers.getContractFactory("AereSink");
  const sink = await Sink_F.deploy(
    waereAddr,
    burnSinkEoa.address,
    saereAddr,
    burnSinkEoa.address, // unused router on AERE path
    1500, 4000, 4500,
    200,
    ethers.ZeroAddress
  );
  await sink.waitForDeployment();
  const sinkAddr = await sink.getAddress();

  // Mint WAERE to actors + feeder so they can play.
  for (const a of actors) {
    await waere.connect(a).deposit({ value: 1_000n * ONE });
    await waere.connect(a).approve(saereAddr, ethers.MaxUint256);
  }
  await waere.connect(feeder).deposit({ value: 5_000n * ONE });
  await waere.connect(feeder).approve(sinkAddr, ethers.MaxUint256);

  return { waere, saere, sink, actors, feeder, deployer, waereAddr, saereAddr, sinkAddr };
}

// --------------------------------------------------------------------------
// Read every piece of vault state we care about in one shot.
// --------------------------------------------------------------------------
async function snapshot(ctx) {
  const { saere } = ctx;
  // R6 FIX: single atomic call so bal/totalAssets/undist are computed at the
  // SAME block.timestamp (no auto-mine race between RPC calls).
  const s = await saere.atomicState();
  let pps;
  try { pps = await saere.pricePerShare(); } catch (_) { pps = 0n; }
  return {
    bal: BigInt(s.balance),
    totalAssets: BigInt(s.totalAssets_),
    totalSupply: BigInt(s.totalSupply_),
    rewardRate: BigInt(s.rewardRate_),
    periodFinish: BigInt(s.periodFinish_),
    lastObserved: BigInt(s.lastObservedBalance_),
    pps: BigInt(pps),
    undist: BigInt(s.undistributed),
  };
}

// --------------------------------------------------------------------------
// Per-step invariant check. `prev` is the snapshot from the previous step,
// `cur` is now, `tag` is the action label for diagnostics.
// --------------------------------------------------------------------------
function checkInvariants(prev, cur, tag, step) {
  // I-1: totalAssets <= balance
  expect(cur.totalAssets, `[step ${step} ${tag}] I-1 totalAssets > balance`)
    .to.be.lessThanOrEqual(cur.bal);

  // I-2: totalAssets + undistributed === balance  (exact)
  expect(cur.totalAssets + cur.undist,
    `[step ${step} ${tag}] I-2 ta+undist != bal (ta=${cur.totalAssets} undist=${cur.undist} bal=${cur.bal})`
  ).to.equal(cur.bal);

  // I-3: price-per-share monotonic non-decreasing
  expect(cur.pps, `[step ${step} ${tag}] I-3 pps dropped from ${prev.pps} to ${cur.pps}`)
    .to.be.greaterThanOrEqual(prev.pps);

  // I-5: lastObservedBalance == balance after every state-changing op
  expect(cur.lastObserved, `[step ${step} ${tag}] I-5 lastObserved != balance`)
    .to.equal(cur.bal);
}

// --------------------------------------------------------------------------
// Helper: assert sync() is idempotent in the same block.
// We mine one tx that calls sync(), then call sync() again with auto-mine off
// inside the SAME block via hardhat_mine, comparing state. Simpler: we observe
// state immediately, call sync() once more (it gets mined in the NEXT block
// but with timestamp held), and check no reward classification fires because
// no balance moved in between.
// We additionally use eth_call to read the would-be effect: since sync() only
// changes state when bal > lastObservedBalance, after a successful sync the
// next sync MUST be a no-op as long as no AERE arrived in between.
// --------------------------------------------------------------------------
async function assertSyncIdempotent(ctx, tag, step) {
  const { saere } = ctx;
  // Disable auto-mine, send two sync() txs, mine ONE block with timestamp held.
  await network.provider.send("evm_setAutomine", [false]);
  try {
    const before = await snapshot(ctx);
    const tx1 = await saere.sync();
    const tx2 = await saere.sync();
    // mine both in the same block, holding timestamp
    await network.provider.send("evm_mine", []);
    await tx1.wait();
    await tx2.wait();
    const after = await snapshot(ctx);

    // No external token arrived between the two syncs, so rewardRate /
    // periodFinish / lastObservedBalance must be the SAME after the second
    // sync as they would be after the first. We approximate this by checking
    // that the combined effect equals the effect of a single sync — since
    // sync() is pure-function-of-current-balance when called twice with the
    // same balance, both calls collapse.
    expect(after.lastObserved, `[step ${step} ${tag}] I-4 lastObs drift in same-block double-sync`)
      .to.equal(after.bal);
    expect(after.periodFinish, `[step ${step} ${tag}] I-4 periodFinish drift in same-block double-sync`)
      .to.be.greaterThanOrEqual(before.periodFinish);
  } finally {
    await network.provider.send("evm_setAutomine", [true]);
  }
}

// --------------------------------------------------------------------------
// Action dispatchers — each returns a label string for diagnostics.
// --------------------------------------------------------------------------
async function doDeposit(ctx, prng) {
  const actor = ctx.actors[prng.nextInt(ctx.actors.length)];
  const bal = BigInt(await ctx.waere.balanceOf(actor.address));
  if (bal < 2n) return null;
  // deposit between 1 wei and min(bal, 50 AERE)
  const cap = bal < 50n * ONE ? bal : 50n * ONE;
  const amount = prng.nextBig(cap);
  try {
    await ctx.saere.connect(actor).deposit(amount, actor.address);
    return `deposit(actor=${actor.address.slice(2,6)},amt=${amount})`;
  } catch (e) {
    return `deposit-revert(${e.shortMessage || e.message.slice(0,40)})`;
  }
}

async function doWithdraw(ctx, prng) {
  const actor = ctx.actors[prng.nextInt(ctx.actors.length)];
  const shares = BigInt(await ctx.saere.balanceOf(actor.address));
  if (shares < 2n) return null;
  const burn = prng.nextBig(shares);
  try {
    await ctx.saere.connect(actor).redeem(burn, actor.address, actor.address);
    return `redeem(actor=${actor.address.slice(2,6)},shares=${burn})`;
  } catch (e) {
    return `redeem-revert(${e.shortMessage || e.message.slice(0,40)})`;
  }
}

async function doSync(ctx) {
  await ctx.saere.sync();
  return `sync`;
}

async function doFlush(ctx, prng) {
  const bal = BigInt(await ctx.waere.balanceOf(ctx.feeder.address));
  if (bal < 10n) return null;
  // flush between 1 wei and 100 AERE
  const cap = bal < 100n * ONE ? bal : 100n * ONE;
  const amount = prng.nextBig(cap);
  try {
    await ctx.sink.connect(ctx.feeder).flush(ctx.waereAddr, amount);
    return `flush(amt=${amount})`;
  } catch (e) {
    return `flush-revert(${e.shortMessage || e.message.slice(0,40)})`;
  }
}

async function doTimeAdvance(prng) {
  // between 1 second and ~2 weeks (so we cross periodFinish often)
  const secs = 1 + prng.nextInt(14 * 24 * 60 * 60);
  await network.provider.send("evm_increaseTime", [secs]);
  await network.provider.send("evm_mine", []);
  return `timeJump(+${secs}s)`;
}

// --------------------------------------------------------------------------
// The actual fuzz.
// --------------------------------------------------------------------------
describe("sAERE + AereSink — 800-action property fuzz", function () {
  this.timeout(15 * 60 * 1000);

  it("preserves all drip invariants under random action stream", async function () {
    const ctx = await deployFuzzStack();
    const prng = makePrng(PRNG_SEED);

    // Seed: alice puts in some real stake so totalSupply / pps are non-trivial.
    await ctx.saere.connect(ctx.actors[0]).deposit(100n * ONE, ctx.actors[0].address);

    let prev = await snapshot(ctx);

    // Track periodFinish "as last seen after a flush" — we assert that a NEW
    // flush never produces a periodFinish less than block.timestamp (i.e. it
    // always projects forward), and never less than the prior periodFinish
    // when the prior period was still live AND no time passed. The contract
    // resets periodFinish to (now + DRIP_DURATION) on every arrival; this
    // is non-decreasing iff no time-travel happened between observations.
    for (let step = 0; step < NUM_ACTIONS; step++) {
      const choice = prng.nextInt(100);
      // distribution: deposit 25 / withdraw 20 / sync 15 / flush 25 / time 15
      let tag;
      let preBlockBal, prePeriodFinish, preBlockTs;
      if (choice < 25) {
        tag = await doDeposit(ctx, prng);
      } else if (choice < 45) {
        tag = await doWithdraw(ctx, prng);
      } else if (choice < 60) {
        tag = await doSync(ctx);
      } else if (choice < 85) {
        // Capture pre-flush state for I-6 check
        preBlockBal = BigInt(await ctx.waere.balanceOf(ctx.saereAddr));
        prePeriodFinish = BigInt(await ctx.saere.periodFinish());
        preBlockTs = BigInt((await ethers.provider.getBlock("latest")).timestamp);
        tag = await doFlush(ctx, prng);
      } else {
        tag = await doTimeAdvance(prng);
      }
      if (tag === null) continue; // skipped (no funds available)

      const cur = await snapshot(ctx);

      // I-6 — flush-specific: periodFinish never decreases as a side-effect
      // of a new arrival. Caveat: time-advance can move us PAST periodFinish,
      // after which the next flush LEGITIMATELY sets periodFinish forward to
      // now + DRIP_DURATION. So our assertion is: post-flush periodFinish
      // >= max(prePeriodFinish, blockTimestamp). The contract always sets
      // it to (now + DRIP_DURATION) on arrival, which is trivially > now,
      // and >= prePeriodFinish unless we already crossed it (in which case
      // it was effectively zero anyway). The strict "never decreases due to
      // a new arrival" guarantee: a flush arrival cannot set periodFinish
      // earlier than now — i.e. it must extend, not shrink.
      if (tag && tag.startsWith("flush(") && cur.bal > preBlockBal) {
        const nowTs = BigInt((await ethers.provider.getBlock("latest")).timestamp);
        expect(cur.periodFinish,
          `[step ${step} ${tag}] I-6 flush moved periodFinish backward of now`
        ).to.be.greaterThanOrEqual(nowTs);
        // R6 HIGH fix: periodFinish only extends to now+DRIP if arrival is
        // >= 1% of undistributed reserve. For tiny arrivals it stays the same.
        // So we just assert: periodFinish is in the future AND did not decrease.
        expect(cur.periodFinish,
          `[step ${step} ${tag}] I-6 periodFinish must not decrease vs previous observation`
        ).to.be.greaterThanOrEqual(prev.periodFinish);
      }

      // Core invariants every step
      checkInvariants(prev, cur, tag || "noop", step);

      // I-4 — sample sync-idempotence on ~5% of steps (cheap, broad coverage)
      if (prng.nextInt(20) === 0) {
        await assertSyncIdempotent(ctx, tag || "noop", step);
        const post = await snapshot(ctx);
        // Idempotence must not decrease pps either
        expect(post.pps,
          `[step ${step}] I-3 pps dropped across same-block double-sync`
        ).to.be.greaterThanOrEqual(cur.pps);
        prev = post;
      } else {
        prev = cur;
      }
    }

    // Final solvency check: dead shares still exist, vault balance covers
    // every share-holder's pro-rata claim against totalAssets (no over-mint).
    const finalDeadBal = BigInt(await ctx.saere.balanceOf(DEAD_ADDR));
    expect(finalDeadBal).to.equal(DEAD_SEED);
    const totalSupply = BigInt(await ctx.saere.totalSupply());
    const totalAssets = BigInt(await ctx.saere.totalAssets());
    const vaultBal = BigInt(await ctx.waere.balanceOf(ctx.saereAddr));
    expect(totalAssets).to.be.lessThanOrEqual(vaultBal);
    // Every actor can in principle redeem their shares back into <= their
    // pro-rata assets without underflow.
    for (const a of ctx.actors) {
      const sh = BigInt(await ctx.saere.balanceOf(a.address));
      if (sh === 0n) continue;
      const previewed = BigInt(await ctx.saere.previewRedeem(sh));
      expect(previewed).to.be.lessThanOrEqual(totalAssets);
      expect(sh).to.be.lessThanOrEqual(totalSupply);
    }
  });
});