• 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
make-summary-deployment.sh 2.17 KB
#!/bin/bash
set -euo pipefail

# create deployments/hardhat/.deploy and snapshots/state-diff/Deploy.json if necessary
if [ ! -d "deployments/hardhat" ]; then
  mkdir deployments/hardhat;
fi
if [ ! -f "deployments/hardhat/.deploy" ]; then
  touch deployments/hardhat/.deploy;
fi
if [ ! -d "snapshots/state-diff" ]; then
  mkdir snapshots/state-diff;
fi
if [ ! -f "snapshots/state-diff/Deploy.json" ]; then
  touch snapshots/state-diff/Deploy.json;
fi

DEPLOY_SCRIPT="./scripts/Deploy.s.sol"

# Create a backup
cp ${DEPLOY_SCRIPT} ${DEPLOY_SCRIPT}.bak

# Replace mustGetAddress by getAddress in Deploy.s.sol
# This is needed because the Kontrol deployment is only a partial
# version of the full Optimism deployment. Since not all the components
# of the system are deployed, we'd get some reverts on the `mustGetAddress` functions
awk '{gsub(/mustGetAddress/, "getAddress")}1' ${DEPLOY_SCRIPT} > temp && mv temp ${DEPLOY_SCRIPT}

FOUNDRY_PROFILE=kdeploy forge script -vvv test/kontrol/KontrolDeployment.sol:KontrolDeployment --sig 'runKontrolDeployment()'
echo "Created state diff json"

# Restore the file from the backup
cp ${DEPLOY_SCRIPT}.bak ${DEPLOY_SCRIPT}
rm ${DEPLOY_SCRIPT}.bak

# Clean and store the state diff json in snapshots/state-diff/Kontrol-Deploy.json
JSON_SCRIPTS=test/kontrol/scripts/json
GENERATED_STATEDIFF=Deploy.json # Name of the statediff json produced by the deployment script
STATEDIFF=Kontrol-${GENERATED_STATEDIFF} # Name of the Kontrol statediff
mv snapshots/state-diff/${GENERATED_STATEDIFF} snapshots/state-diff/${STATEDIFF}
python3 ${JSON_SCRIPTS}/clean_json.py snapshots/state-diff/${STATEDIFF}
echo "Cleaned state diff json"

CONTRACT_NAMES=deployments/hardhat/.deploy
python3 ${JSON_SCRIPTS}/reverse_key_values.py ${CONTRACT_NAMES} ${CONTRACT_NAMES}Reversed
CONTRACT_NAMES=${CONTRACT_NAMES}Reversed

SUMMARY_DIR=test/kontrol/proofs/utils
SUMMARY_NAME=DeploymentSummary
LICENSE=MIT
kontrol summary ${SUMMARY_NAME} snapshots/state-diff/${STATEDIFF} --contract-names ${CONTRACT_NAMES} --output-dir ${SUMMARY_DIR} --license ${LICENSE}
forge fmt ${SUMMARY_DIR}/${SUMMARY_NAME}.sol
forge fmt ${SUMMARY_DIR}/${SUMMARY_NAME}Code.sol
echo "Added state updates to ${SUMMARY_DIR}/${SUMMARY_NAME}.sol"