1. 19 Jun, 2024 1 commit
  2. 11 Jun, 2024 1 commit
  3. 17 Jan, 2024 1 commit
    • 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