Add Kontrol proofs for OptimismPortal #8634
Merged
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
Add deployment summary capabilities
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
tynes
reviewed
Jan 12, 2024
tynes
reviewed
Jan 12, 2024
maurelian
reviewed
Jan 12, 2024
packages/contracts-bedrock/test/kontrol/proofs/utils/KontrolUtils.sol
Outdated
Show resolved
Hide resolved
packages/contracts-bedrock/test/kontrol/proofs/interfaces/KontrolInterfaces.sol
Show resolved
Hide resolved
mds1
reviewed
Jan 12, 2024
packages/contracts-bedrock/test/kontrol/proofs/OptimismPortal.k.sol
Outdated
Show resolved
Hide resolved
mds1
approved these changes
Jan 16, 2024
tynes
reviewed
Jan 16, 2024
packages/contracts-bedrock/test/kontrol/proofs/OptimismPortal.k.sol
Outdated
Show resolved
Hide resolved
maurelian
approved these changes
Jan 16, 2024
github-merge-queue
bot
removed this pull request from the merge queue due to a conflict with the base branch
Merged
via the queue into
ethereum-optimism:develop
with commit Jan 16, 2024
8195514
64 checks passed
dshiell
pushed a commit
to polymerdao/optimism-dev
that referenced
this pull request
Jan 22, 2024
* Remove `OptimismPortal` from `Counter.t.sol` * Add simple state diff contract * Add `broadcast` modifier * Add json cleaning scripts * Add `statediff.sh`: execution script for summary contract generation * Add second Counter instance * Update execution script * Add `StateDiffCheatcode` contract * `run-kontrol.sh`: run `StateDiffCheatcode.recreateDeployment` test * `run-kontrol.sh`: Set `FOUNDRY_PROFILE` flag to `kontrol` * `run-kontrol.sh`: Remove `--no-forge-build` * Add `stategen` foundry profile * Update instructions to create a custom deployment from `Deploy` * Add `run-kontrol-local.sh` * Reflect `Counter.sol` being moved to kontrol folder * `statediff.sh`: update for newest summary kontrol version * Add `test/kontrol/state-change/` folder * forge install: kontrol-cheatcodes * foundry.toml: add `kontrol-cheatcodes` remapping * statediff.sh: Execute custom deployment script with `kontrol` profile * `run-kontrol-local.sh`: make `test_proveWithdrawalTransaction_paused` the default * `statediff.sh`: create dummy save files if they don't exist * `statediff.sh`: replace mustGetAddress by getAddress in Deploy.s.sol * `foundry.toml`: add `read` access to `kout` folder * Update addresses to `internal constant`s * `forge-std`: update version to `80a8f6e` * Save guardian address * Decrease `forge script` verbosity * Update summary contracts to latest version * Rename `StateDiff` to `KontrolDeployment` * Rename `statediff.sh` to `makeSummaryDeployment.sh` and move to `kontrol` folder * Update `makeSummaryDeployment.sh` * Change summary name to `DeploymentSummary` * Move deployment files and `KontrolUtils` to `utils` * Rename `StateDiffTest.sol` to `OptimismPortal.k.sol` * `OptimismPortal.k.sol`: fix typo renaming `DeploymentSummary` * Rename `state-change` to `proofs` * Move scripts under `kontrol/kontrol/scripts` * Add json cleaning scripts under `scripts/json` folder * `run-kontrol-local.sh`: update module name * `DeploymentSummary.sol`: fix typo on importing code contract * `KontrolDeployment`: do not save the guardian address * `run-kontrol-local.sh`: update proof names * Update kontrol foundry profile names * `run-kontrol-local.sh`: remove unnecessary comments * `run-kontrol.sh`: add `proveWithdrawalTransaction` proof to run * Tidy up `run-kontrol-local.sh` * Update `run-kontrol.sh` * `OptimismPortal.k.sol`: clean file * `OptimismPortal.k.sol`: add `test_finalizeWithdrawalTransaction_paused_reverts` proof * Add `test_finalizeWithdrawalTransaction_paused` to `run-kontrol-local.sh` * `.gitignore`: add `kout-deployment` and `kout-proofs` * `OptimismPortalKontrol`: make size of symbolic bytes param be 320 * `KontrolUtils`: optimizations for symbolic `withdrawalProof` * Add `README.md` * Run `forge fmt` * Move dummy tests to `proofs/tests` * Update `run-kontrol.sh` * Update `DeploymentSummaryCode.sol` * `README.md`: add execution instructions * Update symbolic optimizations * Cleanup `make-summary-deployment.sh` * Cleanup `KontrolUtils` * `kontrol/README.md`: add description for `pausability-lemmas.k` * Add description for Kontrol Foundry profiles * Move `kontrol/kontrol` contents to `kontrol` * Change interface naming convention * `make-summary-deployment.sh`: `set -euo pipefail` * `run-kontrol.sh`: reorg `regen` and `rekompile` empty assignments * `KontrolUtils`: update name parameters of `createWithdrawalTransaction` * `OptimismPortal.k.sol`: Replace `assert` by `requires` * `OptimismPortal.k.sol`: remove `test_kontrol_in_foundry` * `.gitignore`: update kontrol logs location * `make-summary-deployment.sh`: change `sed` for `awk` and make its changes transient * `kontrol/README.md`: reflect dissolution of `kontrol/kontrol` * Keep track of statediff deployment json instead of `DeploymentSummary` * `KontrolUtils`: `freshAddress` typo * `KontrolUtils`: set first symbolic workaround; symb `bytes[].length` 10 * forge install: forge-std v1.7.4 * `make-summary-deployment.sh`: explanation for `mustGetAddress` replacement * `make-summary-deployment.sh`: missing `utils` folder in summary dir * Merging local and container script; New call methdo to run locally otherwise no input expected or accepted * Enforcing new paramters local/container/dev for various run scenarios of version enforcement and developer god mode for expereimenting with versions/builds of kontrol * usage wording improvement * Fixing scenario no arguments passed and shifting * Update packages/contracts-bedrock/test/kontrol/scripts/make-summary-deployment.sh Co-authored-by: Matt Solomon <matt@mattsolomon.dev> * Update packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh Co-authored-by: Matt Solomon <matt@mattsolomon.dev> * Typo in packages/contracts-bedrock/test/kontrol/proofs/utils/KontrolUtils.sol Co-authored-by: Matt Solomon <matt@mattsolomon.dev> * Update description of packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh Co-authored-by: Matt Solomon <matt@mattsolomon.dev> * Document `run-kontrol.sh` in README * README.md: Update description of the Kontrol folder * README.md: refine foundry profile description * remove remaining `kontrol/kontrol` instances * correct location of `run-kontrol.sh` script * OptimismPortal.k.sol: rename `test_*` to `proof_*` * Kontrol-Deploy.json: update to latest code * make-summary-deployment.sh: add `forge fmt` as last summary gen step * README.md: fix formatting typo * contracts-bedrock: update bindings (kontrol proofs) * Replace `/* */` comments by `//` * OptimismPortal.k.sol: remove commented `_withdrawalProof` argument * Remove `CounterNames.json` * KontrolUtils.sol: remove unused functions * Describe `clean_json.py` and `reverse_key_values.py` * test/kontrol/README.md: fix typos * OptimismPortal.k.sol: license and typo * KontrolUtils: document the goal of `arrayLength` range * `OptimismPortal.k.sol`: rename `proof_*` to `prove_*` * Remove `createWithdrawalTransaction` function; better proof parameters * OptimismPortal.k.sol: Add tracking issue for symbolic `bytes` support * Add deployment summaries license and disclaimer comment * versions.json: bump Kontrol to 0.1.117 * run-kontrol.sh: update Kontrol version getter method * run-kontrol.sh: fix typo for enforcing local Kontrol version * `OptimismPortal.k.sol`: remove `== true` no-ops * contracts-bedrock: update bindings (kontrol proofs) --------- Co-authored-by: F-WRunTime <Freeman.Wenzl@runtimeverification.com> Co-authored-by: Freeman <105403280+F-WRunTime@users.noreply.github.com> Co-authored-by: Matt Solomon <matt@mattsolomon.dev>
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.
Description
This PR adds two proofs for the
OptimismPortalcontract and the necessary infrastructure to execute them successfully.Tests
Under
packages/contracts-bedrock/test/kontrol/proofs/OptimismPortal.k.sol, two symbolic property tests are addedprove_proveWithdawalTransaction_pausedprove_finalizeWithdrawalTransaction_pausedAdditional context
For more context on the structure of this PR and its files refer to
packages/contracts-bedrock/test/kontrol/README.md