NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Remove hardhat-foundry and check harnesses compilation in CI (#4832)

Browse Source 
Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>
This commit is contained in:
Ernesto García
2024-01-17 13:32:32 -06:00
committed by GitHub
parent ec7ee76494
commit b27cd83eba
9 changed files with 83 additions and 69 deletions
Download Patch File Download Diff File Expand all files Collapse all files

20
certora/specs/EnumerableMap.spec
View File

@ -13,7 +13,7 @@ methods {
function get(bytes32) external returns (bytes32) envfree;
// FV
function _indexOf(bytes32) external returns (uint256) envfree;
function _positionOf(bytes32) external returns (uint256) envfree;
}
/*
@ -69,13 +69,13 @@ invariant atUniqueness(uint256 index1, uint256 index2)
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: index <> value relationship is consistent │
│ │
│ Note that the two consistencyXxx invariants, put together, prove that at_ and _indexOf are inverse of one another. │
│ This proves that we have a bijection between indices (the enumerability part) and keys (the entries that are set │
│ and removed from the EnumerableMap). │
│ Note that the two consistencyXxx invariants, put together, prove that at_ and _positionOf are inverse of one │
│ another. This proves that we have a bijection between indices (the enumerability part) and keys (the entries that │
│ are set and removed from the EnumerableMap). │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant consistencyIndex(uint256 index)
index < length() => to_mathint(_indexOf(key_at(index))) == index + 1
index < length() => to_mathint(_positionOf(key_at(index))) == index + 1
{
preserved remove(bytes32 key) {
requireInvariant consistencyIndex(require_uint256(length() - 1));
@ -84,16 +84,16 @@ invariant consistencyIndex(uint256 index)
invariant consistencyKey(bytes32 key)
contains(key) => (
_indexOf(key) > 0 &&
_indexOf(key) <= length() &&
key_at(require_uint256(_indexOf(key) - 1)) == key
_positionOf(key) > 0 &&
_positionOf(key) <= length() &&
key_at(require_uint256(_positionOf(key) - 1)) == key
)
{
preserved remove(bytes32 otherKey) {
requireInvariant consistencyKey(otherKey);
requireInvariant atUniqueness(
require_uint256(_indexOf(key) - 1),
require_uint256(_indexOf(otherKey) - 1)
require_uint256(_positionOf(key) - 1),
require_uint256(_positionOf(otherKey) - 1)
);
}
}

20
certora/specs/EnumerableSet.spec
View File

@ -9,7 +9,7 @@ methods {
function at_(uint256) external returns (bytes32) envfree;
// FV
function _indexOf(bytes32) external returns (uint256) envfree;
function _positionOf(bytes32) external returns (uint256) envfree;
}
/*
@ -52,13 +52,13 @@ invariant atUniqueness(uint256 index1, uint256 index2)
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: index <> key relationship is consistent │
│ │
│ Note that the two consistencyXxx invariants, put together, prove that at_ and _indexOf are inverse of one another. │
│ This proves that we have a bijection between indices (the enumerability part) and keys (the entries that are added │
│ and removed from the EnumerableSet). │
│ Note that the two consistencyXxx invariants, put together, prove that at_ and _positionOf are inverse of one │
│ another. This proves that we have a bijection between indices (the enumerability part) and keys (the entries that │
│ are added and removed from the EnumerableSet). │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant consistencyIndex(uint256 index)
index < length() => _indexOf(at_(index)) == require_uint256(index + 1)
index < length() => _positionOf(at_(index)) == require_uint256(index + 1)
{
preserved remove(bytes32 key) {
requireInvariant consistencyIndex(require_uint256(length() - 1));
@ -67,16 +67,16 @@ invariant consistencyIndex(uint256 index)
invariant consistencyKey(bytes32 key)
contains(key) => (
_indexOf(key) > 0 &&
_indexOf(key) <= length() &&
at_(require_uint256(_indexOf(key) - 1)) == key
_positionOf(key) > 0 &&
_positionOf(key) <= length() &&
at_(require_uint256(_positionOf(key) - 1)) == key
)
{
preserved remove(bytes32 otherKey) {
requireInvariant consistencyKey(otherKey);
requireInvariant atUniqueness(
require_uint256(_indexOf(key) - 1),
require_uint256(_indexOf(otherKey) - 1)
require_uint256(_positionOf(key) - 1),
require_uint256(_positionOf(otherKey) - 1)
);
}
}