Lesson: Differential pure-math testing for "fix A replaced by equivalent fix B"

Banked 2026-06-11 from the Aave v3.7 L-01 remediation-drift PoC (/home/babakinzo/bounty/findings/aave-l01-drift-poc-2026-06-11.md). Class: Rule-38 (post-audit regression) verification technique.

The Rule-38 sub-pattern this addresses

A high-signal regression class is NOT "audit fix reverted" but "audit fix REPLACED by a different-but-claimed-equivalent mechanism AFTER the auditor recommended the original." The audit acknowledgement text then references an approach the deployed code no longer uses. First banked as a Rule-38 sub-pattern in the 2026-06-11 hunt. This lesson is the VERIFICATION technique for closing such a candidate.

The technique: differential pure-math test, RPC-free

When the two mechanisms (audited vs HEAD) reduce to an arithmetic DECISION over scaled amounts / rounding, do NOT fork mainnet first. Instead:

Identify the two decision predicates (e.g. audited POST-transfer scaledBalanceOf==0 vs HEAD PRE-transfer predictedConsumed == scaledBalance).
Re-implement ONLY the decision logic as pure functions, IMPORTING THE PRODUCTION rounding libraries from src/ (here TokenMath + WadRayMath). Do not re-implement the rounding - import it, so the math is byte-exact deployed code.
For the ground-truth side, REPLAY the exact on-chain reduction SEQUENCE (multi-step burn then capped-fee transfer), not just the final formula. Sequence + per-step caps are where divergence hides.
Fuzz at 50k+ runs across decimals, indices (>= RAY growth regime), balances, and a dedicated boundary-dust property (collat sized to leave exactly 0..N wei). Add hand-crafted dust + low-decimal cases.
Assert the two decisions are always equal. PASS across all = equivalence confirmed.

Only needs forge-std + the two no-external-dep math source files. Compiles and runs even when the heavy solidity-utils submodule is empty/unfetched. Far more exhaustive than a fork PoC for a pure-math equivalence question.

Key analytical insight banked

Equivalence of "single capped comparison vs two-step capped reduction" hinges on the MIN-CAP at the intermediate step. For Aave L-01: - Prediction: min(b+f, S) == S <=> b+f >= S - Ground truth: (S-b) - min(f, S-b) == 0 <=> f >= S-b <=> b+f >= S (given b<=S)

The on-chain fee-transfer min-cap (re-read scaledBalanceOf after the collateral leg) is LOAD-BEARING - it is exactly what collapses the two-step flow to the one-shot prediction. General rule: when checking equivalence of a predicted vs realized depletion, find the intermediate min/cap operations - they are usually what makes the two forms agree, and their removal in a future refactor is what would re-break the invariant. Flag any such cap as a regression tripwire for future Rule-38 sweeps of the same file.

When this technique does NOT suffice

It isolates the math. It does NOT cover: live reserve state, interest accrual across blocks, multi-asset isolation-mode/LTV recomputation downstream of the decision, or re-entrancy in the full executeLiquidationCall. For a pure-math equivalence the math test is dispositive; if escalating a real divergence, a mainnet-fork full-flow test is the next layer. State the boundary explicitly in the verdict (done in the L-01 PoC).

Reusable checklist

[ ] Both fixes reduce to an arithmetic decision? -> pure-math differential applies.
[ ] Import production rounding libs, do not re-implement.
[ ] Ground-truth side replays the on-chain SEQUENCE incl. per-step caps.
[ ] Boundary-dust property (0..N wei leftover) + low-decimal + high-index fuzz.
[ ] Identify the intermediate min/cap that makes the forms agree; flag as tripwire.
[ ] State the full-flow scope NOT covered.