Certora specs #696
Closed
Certora specs #696
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* move state into Storage contract * remove withdrawal proof method
* feat: remove beaconChainOracle in favor of 4788 * modify verifyStaleBalance to use plural form * add pause flags for new methods * deprecate old state variables * minor cleanup and commenting * chore: get things compiling * i commented out/deleted a bajillion tests * fix: adjust storage footprint to be consistent with m2
* removes staleness concept from pod and manager state * clean: clean up start checkpoint logic * clean: remove comments * clean: remove outdated comment and rename proofs method * fix: remove unused variable and deprecate another
* feat: add events for checkpoint creation and progression * feat: remove unneeded oracle interface from EigenPodManager
* modify activateRestaking flow to use checkpointing * remove withdrawNonBeaconChainETHBalanceWei in favor of checkpointing
… interface * chore: fix comment, update interfaces, add event * chore: clarify comment on activateRestaking
* fix: finish rebase * chore: make bindings
* chore: make bindings
* test: basic epoch processing * wip: balance proofs somewhat functional * test: flesh out beacon chain abi and test workflow * test: cleanup * test: add basic invariant checks for checkpoint proofs * test: add tests for full exits
* also refactors and cleans up BeaconChainProofs * more refactor/cleanup to come * chore: more proof library cleanup, removing unused constants * chore: additional cleanup and renaming of proof constants for consistency * chore: clean comments and reorganize constants
* see PR comment for details
* fix: rename and add balance proof
* test: fix some unit tests and remove many outdated tests * test: start setting up new integration tests
* verifyWC -> startCheckpoint in the same block no longer results in a bricked checkpoint * verifyWC using a timestamp older than the current checkpoint no longer allows you to submit a checkpoint proof for the new validator * chore: fix outdated comment
* also reduced number of validators being generated by tests (for speed) * test: flesh out additional pod flows * chore: make bindings * test: add checks for several integration tests
* docs: clean and update EigenPodManager docs * chore: small wip to eigenpod docs and contract comment cleanup
* also minor clarity tweak in verifyCheckpointProofs
* test: testings init * test: eigenpod unit tests refactor * test: startCheckpoint unit tests * test: pod unit tests * fix: rebase changes * chore: make bindings * chore: revert pod changes * test: add several tests and checks --------- Co-authored-by: wadealexc <[email protected]>
* chore: cleanup dwr and unused code * chore: comment out pod specs
* chore: update IEigenPod interface with updated comments
* chore: fix bindings
…s into otakar/specs
|
Closing in favor of rebasing via #707 Will merge this over there. Thank you Otakar! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
All rules, config and setup from the audit.
Important files:
rules
setup files
confs
for the three libraries:
for EigenPod and EigenPodManager (can be extended to other files)
(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.)