Snapshot + recomputed-share postcondition = safe-by-construction new entry-paths (EtherFi PriorityWithdrawalQueue, 2026-06-21)

Pattern (positive case study / invariant)

A share-accounted withdrawal queue can add NEW user entry-paths (new token, new permit variant) safely WITHOUT re-auditing the accounting, IF every entry-path: 1. takes a balance snapshot BEFORE any external interaction: lpEthBefore = LP.balance; queueSharesBefore = shareToken.shares(address(this)); 2. funnels into ONE shared internal _queueWithdrawRequest(user, amount, amountWithFee); and 3. ends with a postcondition that asserts the EXACT expected delta recomputed from the SAME amount: - shareToken.shares(this) == queueSharesBefore + sharesForAmount(amount) (exact, not >=), AND - LP.balance == lpEthBefore (no surprise ETH movement).

Why it's safe-by-construction: the actual shares moved by an amount-denominated transfer are sharesForAmount(amount) (the share token converts amount->shares with its own rounding), and the postcondition expects sharesForAmount(amount) for the SAME amount -> they match by identity regardless of the amount<->share round-trip rounding. Any deviation (unsafe downcast truncation, reentrancy moving shares, the unwrap/transfer touching LP ETH, a fee-on-transfer token, double-credit) makes the == false and REVERTS. So a whole class of accounting bugs is converted into a revert, not a loss.

The concrete instance

EtherFi PriorityWithdrawalQueue added requestWithdrawWithWeETH/...AndPermit AFTER its 2026-03-05 Certora audit (which covered only the eETH path). The new path does weETH.unwrap(weEthAmount) (which = eETH.transfer(this, amountForShare(weEthAmount)), moving sharesForAmount(eEthAmount) shares) then the SAME _verifyRequestPostConditions(.., eEthAmount) that asserts +sharesForAmount(eEthAmount). Exact match. The uint96(weETH.unwrap(...)) unsafe downcast is also neutralized: a truncated eEthAmount makes the postcondition expect the wrong (small) delta while the queue actually received the large delta -> revert, no loss (needs ~79B ETH to trigger anyway).

How to use this when auditing post-audit drift

• When new code ADDS an entry-path that converges on an already-audited internal function guarded by a snapshot+exact-delta postcondition, the drift is usually WALK-CLEAN - prove it by checking the postcondition recomputes from the same value the new path passes down. Don't burn cycles hunting rounding there.
• Conversely, the BUG surfaces when a new path: (a) bypasses the shared postcondition, (b) passes a DIFFERENT amount to the postcondition than what actually moved (e.g., pre-fee vs post-fee, pre-unwrap vs post-unwrap), or (c) the postcondition uses >=/<= instead of == (leaving slack an attacker can fill via donation/rounding). Grep new entry-paths for: does it call the same _verify*? same amount var? == vs inequality?
• This is the EtherFi house pattern (_snapshotBalances/_verifyRequestPostConditions/_verifyClaimPostConditions/_verifyCancelPostConditions); expect it across the withdrawal cluster. Note the claim/cancel postconditions use INEQUALITIES (>=/<= -> revert) which is correct there (direction-of-change checks), vs the request one uses strict == (exact-delta). A future bug would be an inequality where an equality is needed, or vice-versa. Related: [[2026-06-11-metamorpho-totalassets-is-share-accounted-not-donation-inflatable]] (share-accounting beats donation), [[2026-06-10-cycle213-restaking-slash-vs-withdrawal-epoch-union-bound]].