Skip to content
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

update halmos tests for max consolidations = 2 #2

Merged
merged 2 commits into from
Jan 25, 2025
Merged

update halmos tests for max consolidations = 2 #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e30995e
update halmos tests for max consolidation block = 2
daejunpark Jan 22, 2025
4878003
chore: fix links in readme
daejunpark Jan 23, 2025
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
10 changes: 5 additions & 5 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ The system contract provides two operations: `get()` and `set()`.

#### Halmos Test Properties:

We created [halmos tests](test/EIP2935.t.sol.in) to confirm the correct behavior of both operations.
We created [halmos tests](test/EIP2935.t.sol) to confirm the correct behavior of both operations.

For the get() operation, halmos tests verify that it:
- Checks for valid input range, reverting if not valid.
Expand Down Expand Up @@ -141,7 +141,7 @@ The genesis block (`block.number == 0`) is excluded from verification, as its be

The selected calldata sizes were chosen based on branching conditions in the code related to `data.length == 32`. Provided that no additional code paths depend on calldata sizes not considered, (as confirmed by manual inspection of the bytecode implementation), this bounded verification ensures a sufficient correctness guarantee.

The full halmos tests for EIP-2935 can be found [here](test/EIP2935.t.sol.in).
The full halmos tests for EIP-2935 can be found [here](test/EIP2935.t.sol).


### EIP-7002: Withdrawal Requests Queue
Expand Down Expand Up @@ -187,7 +187,7 @@ The fee calculation employs an approximation of `e^x`, called `fake_exponential(

#### Halmos Test Properties:

We developed [halmos tests](test/EIP7002.t.sol.in) to verify the correct behavior of both operations.
We developed [halmos tests](test/EIP7002.t.sol) to verify the correct behavior of both operations.

For the user operation, halmos tests ensure that it:
- Inserts a new element into the queue with accurate encoding and zero-padding as required.
Expand Down Expand Up @@ -372,7 +372,7 @@ The main loop in `fake_exponential()` is unbounded, but current halmos tests ver

Similar to the EIP-2935 tests, the selected calldata sizes were chosen based on branching conditions in the code related to `data.length == 56`. Provided that no additional code paths depend on calldata sizes not considered, (as confirmed by manual inspection of the bytecode implementation), this bounded verification ensures a sufficient correctness guarantee. Additionally, the upper limit on balances does not impact completeness, as `2**96` wei (more than 70 billion ether) far exceeds the current total Ether supply.

The full halmos tests for EIP-7002 can be found [here](test/EIP7002.t.sol.in).
The full halmos tests for EIP-7002 can be found [here](test/EIP7002.t.sol).


### EIP-7251: Consolidation Requests Queue
Expand All @@ -384,7 +384,7 @@ The EIP-7251 system contract closely mirrors the EIP-7002 contract, except that

For the verification of the EIP-7251 contract, we leveraged the existing properties developed for the EIP-7002 system contract. Adjustments were made to account for the differences in queue element size and encoding specific to consolidation requests. These properties inherit the same level of verification completeness.

The full halmos tests for EIP-7251 can be found [here](test/EIP7251.t.sol.in).
The full halmos tests for EIP-7251 can be found [here](test/EIP7251.t.sol).


## Findings from Verification Process
Expand Down
2 changes: 1 addition & 1 deletion sys-asm
Open in desktop
Submodule sys-asm updated 5 files
+7 −11 src/beacon_root/main.eas
+19 −19 src/consolidations/main.eas
+6 −4 src/execution_hash/main.eas
+28 −27 src/withdrawals/main.eas
+20 −17 test/Consolidation.t.sol
2 changes: 1 addition & 1 deletion test/EIP7251.t.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ contract EIP7251Test is SymTest, Test {
uint256 constant CONSOLIDATION_REQUEST_QUEUE_HEAD_STORAGE_SLOT = 2;
uint256 constant CONSOLIDATION_REQUEST_QUEUE_TAIL_STORAGE_SLOT = 3;
uint256 constant CONSOLIDATION_REQUEST_QUEUE_STORAGE_OFFSET = 4;
uint256 constant MAX_CONSOLIDATION_REQUESTS_PER_BLOCK = 1;
uint256 constant MAX_CONSOLIDATION_REQUESTS_PER_BLOCK = 2;
uint256 constant TARGET_CONSOLIDATION_REQUESTS_PER_BLOCK = 1;
uint256 constant MIN_CONSOLIDATION_REQUEST_FEE = 1;
uint256 constant CONSOLIDATION_REQUEST_FEE_UPDATE_FRACTION = 17;
Expand Down