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.

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

test: update certora for pepe #707

Open
wants to merge 1 commit into
base: dev
Choose a base branch
from
Open

Conversation

wadealexc
Copy link
Collaborator

@wadealexc wadealexc commented Aug 26, 2024

All rules, config and setup from the audit.

Important files:

rules

  • certora/specs/libraries/BeaconChainProofs.spec
  • certora/specs/libraries/Endian.spec
  • certora/specs/libraries/Merkle.spec
  • certora/specs/pods/EigenPod.spec // bellow the line "Added by Certora"
  • certora/specs/pods/EigenPodHooks.spec
  • certora/specs/pods/EigenPodManager.spec // bellow the line "Added by Certora"

setup files

  • setup.spec
  • methodsAndAliases.spec
  • EigenPodMethodsAndSimplifications.spec - most NONDET summaries, simplifications

confs

for the three libraries:

  • certora/confs/beaconChainProofs.conf
  • certora/confs/endian.conf
  • certora/confs/merkle.conf

for EigenPod and EigenPodManager (can be extended to other files)

  • certora/confs/full.conf

(All specs will compile on the audited branch feat/partial-withdrawal-batching. I merged in the latest changes but I didn't yet rerun everything to be sure the specs are synced with the current code. I will adjust it if needed.)

@wadealexc wadealexc force-pushed the alex/certora-specs-rebase branch from d69ac0e to 1ba7b16 Compare August 26, 2024 14:41
@wadealexc wadealexc mentioned this pull request Aug 26, 2024
Copy link

Reading tracefile ./lcov.info.pruned
                                             |Lines      |Functions|Branches  
Filename                                       |Rate    Num|Rate  Num|Rate   Num
================================================================================
[src/contracts/]
core/AVSDirectory.sol                          |85.2%    27|88.9%   9|    -    0
core/DelegationManager.sol                     |96.5%   198|92.3%  39|    -    0
core/RewardsCoordinator.sol                    |92.4%   119|84.4%  32|    -    0
core/StrategyManager.sol                       |97.6%    83| 100%  24|    -    0
libraries/BeaconChainProofs.sol                | 100%    22| 100%  11|    -    0
libraries/BytesLib.sol                         | 0.0%   156| 0.0%  14|    -    0
libraries/EIP1271SignatureUtils.sol            | 100%     3| 100%   1|    -    0
libraries/Endian.sol                           | 100%     2| 100%   1|    -    0
libraries/Merkle.sol                           | 100%    38| 100%   5|    -    0
libraries/StructuredLinkedList.sol             | 0.0%    45| 0.0%  19|    -    0
permissions/Pausable.sol                       |95.7%    23|90.9%  11|    -    0
permissions/PauserRegistry.sol                 | 100%    12| 100%   6|    -    0
pods/EigenPod.sol                              | 100%   122|96.2%  26|    -    0
pods/EigenPodManager.sol                       | 100%    75|92.9%  14|    -    0
strategies/EigenStrategy.sol                   | 0.0%    10| 0.0%   5|    -    0
strategies/StrategyBase.sol                    |90.9%    44|78.9%  19|    -    0
strategies/StrategyBaseTVLLimits.sol           | 100%    12| 100%   6|    -    0
strategies/StrategyFactory.sol                 | 100%    35| 100%   9|    -    0
token/BackingEigen.sol                         |80.0%    25|60.0%  10|    -    0
token/Eigen.sol                                |43.6%    39|58.3%  12|    -    0
utils/UpgradeableSignatureCheckingUtils.sol    | 0.0%     6| 0.0%   4|    -    0
================================================================================
                                       Total:|75.3%  1096|75.8% 277|    -    0

1 similar comment
Copy link

Reading tracefile ./lcov.info.pruned
                                             |Lines      |Functions|Branches  
Filename                                       |Rate    Num|Rate  Num|Rate   Num
================================================================================
[src/contracts/]
core/AVSDirectory.sol                          |85.2%    27|88.9%   9|    -    0
core/DelegationManager.sol                     |96.5%   198|92.3%  39|    -    0
core/RewardsCoordinator.sol                    |92.4%   119|84.4%  32|    -    0
core/StrategyManager.sol                       |97.6%    83| 100%  24|    -    0
libraries/BeaconChainProofs.sol                | 100%    22| 100%  11|    -    0
libraries/BytesLib.sol                         | 0.0%   156| 0.0%  14|    -    0
libraries/EIP1271SignatureUtils.sol            | 100%     3| 100%   1|    -    0
libraries/Endian.sol                           | 100%     2| 100%   1|    -    0
libraries/Merkle.sol                           | 100%    38| 100%   5|    -    0
libraries/StructuredLinkedList.sol             | 0.0%    45| 0.0%  19|    -    0
permissions/Pausable.sol                       |95.7%    23|90.9%  11|    -    0
permissions/PauserRegistry.sol                 | 100%    12| 100%   6|    -    0
pods/EigenPod.sol                              | 100%   122|96.2%  26|    -    0
pods/EigenPodManager.sol                       | 100%    75|92.9%  14|    -    0
strategies/EigenStrategy.sol                   | 0.0%    10| 0.0%   5|    -    0
strategies/StrategyBase.sol                    |90.9%    44|78.9%  19|    -    0
strategies/StrategyBaseTVLLimits.sol           | 100%    12| 100%   6|    -    0
strategies/StrategyFactory.sol                 | 100%    35| 100%   9|    -    0
token/BackingEigen.sol                         |80.0%    25|60.0%  10|    -    0
token/Eigen.sol                                |43.6%    39|58.3%  12|    -    0
utils/UpgradeableSignatureCheckingUtils.sol    | 0.0%     6| 0.0%   4|    -    0
================================================================================
                                       Total:|75.3%  1096|75.8% 277|    -    0

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant