• Juan C's avatar
    Add Kontrol proofs for OptimismPortal (#8634) · 81955146
    Juan C authored
    * 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: default avatarMatt Solomon <matt@mattsolomon.dev>
    
    * Update packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh
    Co-authored-by: default avatarMatt Solomon <matt@mattsolomon.dev>
    
    * Typo in packages/contracts-bedrock/test/kontrol/proofs/utils/KontrolUtils.sol
    Co-authored-by: default avatarMatt Solomon <matt@mattsolomon.dev>
    
    * Update description of packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh
    Co-authored-by: default avatarMatt 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: default avatarF-WRunTime <Freeman.Wenzl@runtimeverification.com>
    Co-authored-by: default avatarFreeman <105403280+F-WRunTime@users.noreply.github.com>
    Co-authored-by: default avatarMatt Solomon <matt@mattsolomon.dev>
    81955146
DeploymentSummaryCode.sol 148 KB