Skip to content

[Certora] Precise calculation of earliestExecutionTime() #906

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jhoenicke wants to merge 4 commits into
base: main
Choose a base branch
from
Open

[Certora] Precise calculation of earliestExecutionTime() #906

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e2af3e7
specify precise minimum
jhoenicke Mar 9, 2026
fe3fe7c
sload hook
jhoenicke Mar 9, 2026
6a8bc63
use bytes32 and keccak256
jhoenicke Mar 9, 2026
9542a9c
run invariant only for current contract
jhoenicke Mar 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 37 additions & 5 deletions certora/specs/EarliestTime.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,19 @@ methods {
persistent ghost mapping(bytes4 => mathint) minDecreaseTimelock {
init_state axiom forall bytes4 selector. minDecreaseTimelock[selector] == max_uint256;
}
// Ghost to track the minimum possible execution time for every possible submission
persistent ghost mapping(bytes4 => mapping(bytes32 => mathint)) decreaseTimelockEET {
init_state axiom forall bytes4 selector. forall bytes32 hash. decreaseTimelockEET[selector][hash] == max_uint256;
}

definition minimumIsLowerBound(bytes4 selector) returns bool =
forall bytes32 hash. minDecreaseTimelock[selector] <= decreaseTimelockEET[selector][hash];

definition minimumIsAchievable(bytes4 selector) returns bool =
exists bytes32 hash. minDecreaseTimelock[selector] == decreaseTimelockEET[selector][hash];

definition earliestTimeFromValueDuration(uint256 value, uint256 duration) returns mathint =
value > 0 ? value + duration : max_uint256;

// Hook on executableAt writes to track decreaseTimelock submissions
hook Sstore executableAt[KEY bytes hookData] uint256 newValue (uint256 oldValue) {
Expand All @@ -26,11 +39,25 @@ hook Sstore executableAt[KEY bytes hookData] uint256 newValue (uint256 oldValue)
uint256 newDuration;
targetSelector, newDuration = EarliestTime.extractDecreaseTimelockArgs(hookData);

if (oldValue == 0 && newValue != 0 && minDecreaseTimelock[targetSelector] > newValue + newDuration) {
minDecreaseTimelock[targetSelector] = newValue + newDuration;
} else if (oldValue != 0 && newValue == 0) {
minDecreaseTimelock[targetSelector] = max_uint256;
}
decreaseTimelockEET[targetSelector][keccak256(hookData)] = earliestTimeFromValueDuration(newValue, newDuration);
bytes32 newMinimumWitness;
mathint newMinimum = decreaseTimelockEET[targetSelector][newMinimumWitness];
require forall bytes32 hash. newMinimum <= decreaseTimelockEET[targetSelector][hash], "Witness can be chosen for the minimum.";
minDecreaseTimelock[targetSelector] = newMinimum;
}
}

// Hook on executableAt writes to track decreaseTimelock submissions
hook Sload uint256 value executableAt[KEY bytes hookData] {
bytes4 selector = EarliestTime.getSelector(hookData);

if (selector == to_bytes4(sig:decreaseTimelock(bytes4, uint256).selector)) {
bytes4 targetSelector;
uint256 newDuration;
targetSelector, newDuration = EarliestTime.extractDecreaseTimelockArgs(hookData);

requireInvariant minimumCorrectlyTracked(targetSelector);
require decreaseTimelockEET[targetSelector][keccak256(hookData)] == earliestTimeFromValueDuration(value, newDuration), "ghost mirror";
}
}

Expand All @@ -53,6 +80,11 @@ function earliestExecutionTime(uint256 blockTimestamp, bytes4 selector, uint256
return min(viaDirectExecution, viaFreshSubmission, viaDecreaseTimelock);
}

invariant minimumCorrectlyTracked(bytes4 selector)
minimumIsLowerBound(selector) && minimumIsAchievable(selector)
filtered { f -> f.contract == currentContract }


// Similar to guardianUpdateTime from vault v1.
// Earliest execution time is monotonically non-decreasing across three paths:
// 1. Direct execution via executableAt[data] (if already submitted)
Expand Down