← back to lessons

Restaking: slash-vs-withdrawal-epoch invariant + the union-bound vs per-capture-subset trap

Date: 2026-06-10 Banked from: Cycle 213 - Symbiotic core (Cantina $500K bug bounty, WALK CLEAN) Class: restaking / shared-security / epoch-based withdrawal accounting Status: reusable lens for any restaking target (Symbiotic + forks, EigenLayer, Karak, Mellow-on-Symbiotic, Tenderize-style)

The primitive shape

Restaking vaults let a staker exit (withdraw) but keep their collateral SLASHABLE for a delay window so that misbehavior committed while they were backing the network can still be punished after they queued the exit. The exit is bucketed by epoch:

Two reporting/settlement surfaces exist and they DELIBERATELY differ:

  1. slashableBalanceOf(acct) at epoch E = active + withdrawals[E] + withdrawals[E+1]. This is a UNION upper-bound: the maximum that COULD be slashed across all currently-valid capture epochs.

  2. onSlash(amount, captureTimestamp) gates captureEpoch in {current-1, current} and slashes a SUBSET chosen by the capture epoch: - captureEpoch == current -> slashes active + withdrawals[current+1] (NOT withdrawals[current]). - captureEpoch == current-1 -> slashes active + withdrawals[current] + withdrawals[current+1].

The trap (and how to not false-positive on it)

You WILL observe: slashableBalanceOf reports more than a single onSlash(captureEpoch==current) can take. In Cycle 213: reported 1000, current-capture slash took only 600, leaving a 400 "escape" in withdrawals[current]. This LOOKS like collateral dodging the slash. STOP - that is the false positive.

The 400 in withdrawals[current] was REQUESTED IN THE PRIOR EPOCH. It is not backing CURRENT-epoch misbehavior, so excluding it from a current-epoch capture is correct. The decisive test is to slash with a capture in the OTHER valid epoch (the one where those funds WERE backing stake): the captureEpoch<current branch fires and the 400 IS slashed. So:

slashableBalanceOf = UNION over valid capture epochs; each individual slash slashes the capture-appropriate SUBSET. "reported > slashed-at-one-capture" is NOT a leak, as long as EVERY epoch's funds are reachable by SOME valid capture. Verify by testing both capture branches.

This is the restaking analog of the Paxos C206 "measure the sign, do not stop at the surface discrepancy" rule and the Rheo/Midnight maturity-boundary lens: a boundary that looks asymmetric is fine if each side is reachable by the correct key (here, the correct captureTimestamp).

Where a REAL bug would live (checklist for the next restaking target)

  1. EPOCH OFF-BY-ONE in the gate: does onSlash accept captureEpoch == current-1 AND current? If the window is one epoch too SHORT, freshly-queued withdrawals become unslashable a block early = slash-dodge. If too LONG, already-claimed funds could be double-counted. Check the exact </<= on captureEpoch < currentEpoch_ - 1 and captureEpoch > currentEpoch_, and on the slasher's captureTimestamp < now - epochDuration || captureTimestamp >= now.
  2. CLAIM-BEFORE-SLASH race: can a staker claim() an epoch's withdrawal before the latest valid slash for that epoch's misbehavior can land? In Symbiotic claim requires epoch < currentEpoch() and the capture gate expires at current-1, so claim (epoch N+2 for an epoch-N request) coincides with capture-N expiry. Re-derive this timeline on every target; an off-by-one here is the crown-jewel slash-dodge.
  3. UNION COMPLETENESS: is EVERY epoch bucket that slashableBalanceOf counts reachable by some valid capture? If slashableBalanceOf includes a bucket that NO capture epoch can actually slash, that is a real under-slash / escape (the opposite of the Cycle 213 false positive). Test all branches.
  4. DOUBLE-SLASH guard: slashableStake = stakeAt(capture) - min(cumulativeSlash_now - cumulativeSlashAt(capture), stakeAt) plus latestSlashedCaptureTimestamp monotonic gate. Verify a network cannot replay an old capture to slash the same stake twice, and cannot slash beyond stakeAt.

Negative rule banked: checkpoint-tracked vaults are donation/inflation-proof

Symbiotic's activeStake is a CHECKPOINT value (Checkpoints.Trace256, pushed on deposit/withdraw/slash), NOT derived from collateral.balanceOf(vault). Therefore: - A raw collateral.transfer(vault, X) does NOT change activeStake -> the classic ERC4626 first-depositor / donation / inflation front-run is STRUCTURALLY IMPOSSIBLE. (Confirmed empirically: transferring 10000e18 left activeStake at 1 wei.) - The OZ virtual-offset (+1 on assets+shares, _decimalsOffset()==0) is belt-and-suspenders on top.

Do NOT spend cycles hunting share-inflation on a vault whose total-assets is checkpoint/internal-counter tracked rather than balanceOf-tracked. The whole class is dead there. (Contrast: balanceOf-tracked 4626 vaults remain vulnerable - keep the C200/C206 lens for those.)

Doctrine

For restaking withdrawal-delay accounting, the two load-bearing invariants are: (1) collateral stays slashable for the FULL epoch(s) it was backing stake (no early-exit dodge), and (2) the slashable REPORT is a union over valid capture epochs while each slash takes the correct subset - test BOTH capture branches before calling a report/settlement mismatch a bug. And the share-math hunt is only live if total-assets is balanceOf-derived; checkpoint-tracked is donation-proof.

Generated 2026-07-02 13:15:03 UTC | auto-sync /15min