Commit Graph

1 Commits

Author SHA1 Message Date
lucasmt 406a43d03e
ethereum: Add property tests and instructions for running them with KEVM (#2956)
* ethereum: Add Foundry tests written by RV

* ethereum: Add scripts and instructions to run proofs using KEVM

* ethereum: Fix typo on testSetup_after_setup_revert_KEVM

* ethereum: Edit Makefile to skip KEVM tests when running forge test

* ethereum: Fix commented-out lines in Foundry tests

* ethereum: Refactor GovernanceStructs invalid-size tests

* ethereum: Replace assume with bound in Foundry tests

Co-authored-by: Jeff Schroeder <jeffschroeder@computer.org>

* ethereum: Apply review suggestions to run-kevm script

Co-authored-by: Jeff Schroeder <jeffschroeder@computer.org>

* ethereum: explicit cast to uint8 for some vars

The bound() calls need to be explicitly cast to uint8 from the uint256
that forge-std's bound() returns.

* ethereum: updating some of the RV tests

The definitions don't compile with newer forge/solc.

* ethereum: Add assumption to test that guardian count > 0

Prevents an arithmetic over/underflow error in testCannotVerifySignaturesWithOutOfBoundsSignature, in the expression bound(outOfBoundsGuardian, 0, params.guardianCount - 1)

---------

Co-authored-by: Lucas MT <lucas.tabajara@runtimeverification.com>
Co-authored-by: Jeff Schroeder <jeffschroeder@computer.org>
2023-09-06 11:24:00 -04:00