test(invariant): I5 oracle-integrity stateful fuzz invariant#472
Merged
seongyun-ko merged 2 commits intoJun 15, 2026
Merged
Conversation
Stateful sequence test for I5 (oracle integrity) on EtherFiOracle + EtherFiAdmin: every applied OracleReport (advancing lastHandledReportRefSlot via executeTasks) must satisfy all three gates -- quorum (>= quorumSize sigs), APR cap (|rebase APR| <= acceptableRebaseAprInBps), freshness (past postReportWaitTimeInSlots). Proven via an independent, byte-faithful gate mirror that flips a ghost if any gate-violating apply ever occurs; mirror fidelity cross-checked against the contract's own revert reasons. Deterministic (not randomized invariant) because EtherFiOracle's strict slot/epoch state machine can't be driven reliably under Foundry's stateful- fuzz scheduling/shrinking -- matches how EtherFiOracle.t.sol tests it. 38 reports applied + 19/20/19 quorum/apr/freshness rejections, reproducible, 0 uncategorised reverts. src untouched.
Replaces the deterministic sequence test with a true randomized stateful fuzz-invariant (Foundry invariant engine, 64 runs x 1920 calls, 0 reverts). Root cause of the earlier vacuity (numApplied==0 under the invariant runner): the 'valid apply' scenario bounded its rebase reward to a blind 0..0.5 ether constant. The APR gate caps |apr| = 10000*reward*365d/(tvl*elapsedTime); on reports after the first, elapsedTime is just the ~1100-slot range moved, so 0.5 ether computes to ~11900 bps > the 10000 cap -> the supposedly-valid apply reverted on APR, leaving the report published-but-unapplied -> oracle stuck -> every later step bailed at the un-stuck guard. The fuzzer found this; the deterministic loop (tiny uniform rewards) never did. Fix: _maxSafeReward() sizes the apply/fresh-fail reward to half the per-range APR-cap boundary, so the accepting path is genuinely accepted regardless of the fuzzed magnitude or the range length the clock produces. Result: 60 reports applied + 30/30/30 quorum/apr/freshness rejections, mirror-consistent, stable across seeds. No gate-violating apply ever observed. No assertion weakened; src untouched.
seongyun-ko
changed the title
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
I5 — Oracle integrity (stateful FUZZ invariant)
Closes the SC-enforceable core of invariant I5 on
EtherFiOracle+EtherFiAdminas a true randomized stateful fuzz-invariant (Foundry invariant engine).Property: every applied
OracleReport(one that advancesEtherFiAdmin.lastHandledReportRefSlotviaexecuteTasks) MUST satisfy all three gates at execution time:quorumSize()committee signatures|rebase APR| ≤ acceptableRebaseAprInBps()currentSlot ≥ postReportWaitTimeInSlots + consensusSlotThe fuzzer drives
step(magnitude); each call exercises apply + all three reject scenarios against the real contracts. An independent, byte-faithful gate mirror flips a ghost if any state-advancing report ever violated a gate (the I5 proof), cross-checked against the contract's ownReportValidationFailedreasons so the safety ghosts can't be vacuously satisfied.Result: 4 invariants, 64 runs × 1920 calls, 0 reverts, stable across seeds. Non-vacuous: 60 reports applied + 30/30/30 quorum/APR/freshness rejections. No gate-violating apply ever observed.
Real bug the fuzzer caught (in the harness, documented inline)
The first cut bounded the "valid apply" reward to a blind
0..0.5 ether. The APR gate caps|apr| = 10000·reward·365d / (tvl·elapsedTime)— and on reports after the first,elapsedTimeis just the short range moved, so0.5 ethercomputes to ~11900 bps > the 10000 cap. The "valid" apply then reverted on APR, left a published-but-unapplied report, bricked the oracle, and every later step bailed → vacuousnumApplied==0. The deterministic loop (tiny uniform rewards) never hit this; the fuzzer did. Fix:_maxSafeReward()sizes the apply reward to half the per-range APR-cap boundary, so the accepting path is genuinely accepted regardless of fuzzed magnitude or range length. No assertion weakened.src/untouched (test/ only). Base:seongyun/fuzz/security-upgrades(same as #470).