• 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
Name
Last commit
Last update
.changeset Loading commit data...
.circleci Loading commit data...
.github Loading commit data...
.husky Loading commit data...
.vscode Loading commit data...
bedrock-devnet Loading commit data...
cannon Loading commit data...
docs Loading commit data...
endpoint-monitor Loading commit data...
indexer Loading commit data...
op-batcher Loading commit data...
op-bindings Loading commit data...
op-bindings-e2e Loading commit data...
op-bootnode Loading commit data...
op-chain-ops Loading commit data...
op-challenger Loading commit data...
op-conductor Loading commit data...
op-e2e Loading commit data...
op-heartbeat Loading commit data...
op-node Loading commit data...
op-preimage Loading commit data...
op-program Loading commit data...
op-proposer Loading commit data...
op-service Loading commit data...
op-ufm Loading commit data...
op-wheel Loading commit data...
ops Loading commit data...
ops-bedrock Loading commit data...
packages Loading commit data...
proxyd Loading commit data...
specs Loading commit data...
ufm-test-services Loading commit data...
.coderabbit.yml Loading commit data...
.dockerignore Loading commit data...
.editorconfig Loading commit data...
.envrc.example Loading commit data...
.eslintrc.js Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitmodules Loading commit data...
.markdownlint.json Loading commit data...
.npmrc Loading commit data...
.nvmrc Loading commit data...
.pnpmfile.cjs Loading commit data...
.prettierrc.js Loading commit data...
.semgrepignore Loading commit data...
.shellcheckrc Loading commit data...
.snyk Loading commit data...
CITATION.cff Loading commit data...
CONTRIBUTING.md Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
README.md Loading commit data...
SECURITY.md Loading commit data...
cloudbuild.yaml Loading commit data...
codecov.yml Loading commit data...
docker-bake.hcl Loading commit data...
go.mod Loading commit data...
go.sum Loading commit data...
nx.json Loading commit data...
package.json Loading commit data...
pnpm-lock.yaml Loading commit data...
pnpm-workspace.yaml Loading commit data...
tsconfig.json Loading commit data...
versions.json Loading commit data...