Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add Kontrol proofs for OptimismPortal #8634

Merged
merged 130 commits into from
Jan 16, 2024
Merged

Add Kontrol proofs for OptimismPortal #8634

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
130 commits
Select commit Hold shift + click to select a range
98ca6d8
Merge remote-tracking branch 'origin/develop' into pausability-verifi…
JuanCoRo Nov 30, 2023
5bf1166
Remove `OptimismPortal` from `Counter.t.sol`
JuanCoRo Nov 30, 2023
eed9bb3
Add simple state diff contract
JuanCoRo Nov 30, 2023
aa1eed8
Add `broadcast` modifier
JuanCoRo Dec 1, 2023
f9f8269
Add json cleaning scripts
JuanCoRo Dec 4, 2023
1c826dc
Add `statediff.sh`: execution script for summary contract generation
JuanCoRo Dec 4, 2023
9ad8642
Add second Counter instance
JuanCoRo Dec 5, 2023
d0f02c2
Update execution script
JuanCoRo Dec 5, 2023
d197901
Add `StateDiffCheatcode` contract
JuanCoRo Dec 6, 2023
4b190ae
`run-kontrol.sh`: run `StateDiffCheatcode.recreateDeployment` test
JuanCoRo Dec 6, 2023
c2fecae
`run-kontrol.sh`: Set `FOUNDRY_PROFILE` flag to `kontrol`
JuanCoRo Dec 6, 2023
ffb5e13
`run-kontrol.sh`: Remove `--no-forge-build`
JuanCoRo Dec 6, 2023
4789b8d
Add `stategen` foundry profile
JuanCoRo Dec 9, 2023
8e4ca03
Update instructions to create a custom deployment from `Deploy`
JuanCoRo Dec 9, 2023
4e476e0
Merge remote-tracking branch 'origin/develop' into simple-state-change
JuanCoRo Dec 9, 2023
90d33e9
Merge remote-tracking branch 'origin/develop' into pausability-verifi…
JuanCoRo Dec 9, 2023
93b24c7
Add `run-kontrol-local.sh`
JuanCoRo Dec 9, 2023
3fdcf56
Reflect `Counter.sol` being moved to kontrol folder
JuanCoRo Dec 9, 2023
727b7ab
`statediff.sh`: update for newest summary kontrol version
JuanCoRo Dec 9, 2023
9eff315
Merge pull request #2 from runtimeverification/simple-state-change
JuanCoRo Dec 9, 2023
b923ddd
Add `test/kontrol/state-change/` folder
JuanCoRo Dec 10, 2023
7833945
forge install: kontrol-cheatcodes
JuanCoRo Dec 10, 2023
8b57ce1
foundry.toml: add `kontrol-cheatcodes` remapping
JuanCoRo Dec 11, 2023
0be7f7b
statediff.sh: Execute custom deployment script with `kontrol` profile
JuanCoRo Dec 11, 2023
6ef200d
`run-kontrol-local.sh`: make `test_proveWithdrawalTransaction_paused`…
JuanCoRo Dec 11, 2023
e197aed
`statediff.sh`: create dummy save files if they don't exist
JuanCoRo Dec 11, 2023
32e910c
`statediff.sh`: replace mustGetAddress by getAddress in Deploy.s.sol
JuanCoRo Dec 11, 2023
79e81e5
`foundry.toml`: add `read` access to `kout` folder
JuanCoRo Dec 11, 2023
182222f
Update addresses to `internal constant`s
JuanCoRo Dec 11, 2023
c7a8fc6
`forge-std`: update version to `80a8f6e`
JuanCoRo Dec 12, 2023
c2433cd
Save guardian address
JuanCoRo Dec 12, 2023
4c1b2d1
Decrease `forge script` verbosity
JuanCoRo Dec 12, 2023
25fe43f
Update summary contracts to latest version
JuanCoRo Dec 12, 2023
f82378b
Rename `StateDiff` to `KontrolDeployment`
JuanCoRo Dec 13, 2023
5dd320f
Rename `statediff.sh` to `makeSummaryDeployment.sh` and move to `kont…
JuanCoRo Dec 13, 2023
ba6bd8b
Update `makeSummaryDeployment.sh`
JuanCoRo Dec 13, 2023
156df3c
Change summary name to `DeploymentSummary`
JuanCoRo Dec 13, 2023
46c194c
Move deployment files and `KontrolUtils` to `utils`
JuanCoRo Dec 13, 2023
20b5427
Rename `StateDiffTest.sol` to `OptimismPortal.k.sol`
JuanCoRo Dec 13, 2023
8fa1856
`OptimismPortal.k.sol`: fix typo renaming `DeploymentSummary`
JuanCoRo Dec 13, 2023
113f40c
Rename `state-change` to `proofs`
JuanCoRo Dec 13, 2023
0ec3fca
Move scripts under `kontrol/kontrol/scripts`
JuanCoRo Dec 13, 2023
dc05428
Add json cleaning scripts under `scripts/json` folder
JuanCoRo Dec 13, 2023
6a2c527
`run-kontrol-local.sh`: update module name
JuanCoRo Dec 13, 2023
1f0ffae
`DeploymentSummary.sol`: fix typo on importing code contract
JuanCoRo Dec 13, 2023
792a6ae
`KontrolDeployment`: do not save the guardian address
JuanCoRo Dec 13, 2023
af858fa
`run-kontrol-local.sh`: update proof names
JuanCoRo Dec 13, 2023
f8217b0
Update kontrol foundry profile names
JuanCoRo Dec 13, 2023
62d6911
`run-kontrol-local.sh`: remove unnecessary comments
JuanCoRo Dec 13, 2023
c4ecafe
`run-kontrol.sh`: add `proveWithdrawalTransaction` proof to run
JuanCoRo Dec 13, 2023
eaf6bfe
Tidy up `run-kontrol-local.sh`
JuanCoRo Dec 13, 2023
f8294bc
Update `run-kontrol.sh`
JuanCoRo Dec 13, 2023
aa08224
`OptimismPortal.k.sol`: clean file
JuanCoRo Dec 13, 2023
7cb55f4
`OptimismPortal.k.sol`: add `test_finalizeWithdrawalTransaction_pause…
JuanCoRo Dec 13, 2023
1f470bf
Add `test_finalizeWithdrawalTransaction_paused` to `run-kontrol-local…
JuanCoRo Dec 13, 2023
c0b8837
`.gitignore`: add `kout-deployment` and `kout-proofs`
JuanCoRo Dec 14, 2023
52d8295
`OptimismPortalKontrol`: make size of symbolic bytes param be 320
JuanCoRo Dec 14, 2023
1b7ec5b
`KontrolUtils`: optimizations for symbolic `withdrawalProof`
JuanCoRo Dec 14, 2023
ab6893f
Add `README.md`
JuanCoRo Dec 14, 2023
efe0062
Run `forge fmt`
JuanCoRo Dec 14, 2023
cf28b60
Move dummy tests to `proofs/tests`
JuanCoRo Dec 14, 2023
9d6b79d
Update `run-kontrol.sh`
JuanCoRo Dec 14, 2023
0d1c4ce
Update `DeploymentSummaryCode.sol`
JuanCoRo Dec 14, 2023
89477bf
`README.md`: add execution instructions
JuanCoRo Dec 14, 2023
c1a146e
Update symbolic optimizations
JuanCoRo Dec 14, 2023
451c9e4
Cleanup `make-summary-deployment.sh`
JuanCoRo Dec 14, 2023
9463f93
Cleanup `KontrolUtils`
JuanCoRo Dec 14, 2023
d81edc3
Merge pull request #3 from runtimeverification/final-proof-setting
JuanCoRo Dec 14, 2023
0ceaf3d
Merge remote-tracking branch 'origin/develop' into kontrol-proofs
JuanCoRo Dec 14, 2023
1a3b59d
`kontrol/README.md`: add description for `pausability-lemmas.k`
JuanCoRo Dec 19, 2023
fde811a
Add description for Kontrol Foundry profiles
JuanCoRo Dec 19, 2023
04eaafd
Move `kontrol/kontrol` contents to `kontrol`
JuanCoRo Dec 19, 2023
e2ac186
Change interface naming convention
JuanCoRo Dec 19, 2023
2709f9c
`make-summary-deployment.sh`: `set -euo pipefail`
JuanCoRo Dec 19, 2023
165f4e0
`run-kontrol.sh`: reorg `regen` and `rekompile` empty assignments
JuanCoRo Dec 19, 2023
8f02eba
`KontrolUtils`: update name parameters of `createWithdrawalTransaction`
JuanCoRo Dec 19, 2023
f5d55c5
`OptimismPortal.k.sol`: Replace `assert` by `requires`
JuanCoRo Dec 19, 2023
64bb26a
`OptimismPortal.k.sol`: remove `test_kontrol_in_foundry`
JuanCoRo Dec 19, 2023
59c4b06
`.gitignore`: update kontrol logs location
JuanCoRo Dec 19, 2023
f252a0a
`make-summary-deployment.sh`: change `sed` for `awk` and make its cha…
JuanCoRo Dec 19, 2023
2a4f6a2
`kontrol/README.md`: reflect dissolution of `kontrol/kontrol`
JuanCoRo Dec 20, 2023
4bd4f88
Keep track of statediff deployment json instead of `DeploymentSummary`
JuanCoRo Dec 20, 2023
532b66c
`KontrolUtils`: `freshAddress` typo
JuanCoRo Dec 20, 2023
c1aa757
`KontrolUtils`: set first symbolic workaround; symb `bytes[].length` 10
JuanCoRo Dec 20, 2023
de4ad35
forge install: forge-std
JuanCoRo Dec 20, 2023
5c5c379
`make-summary-deployment.sh`: explanation for `mustGetAddress` replac…
JuanCoRo Dec 20, 2023
f9b7597
Merge remote-tracking branch 'origin/develop' into kontrol-proofs
JuanCoRo Dec 20, 2023
14758cc
`make-summary-deployment.sh`: missing `utils` folder in summary dir
JuanCoRo Dec 21, 2023
6189106
Merging local and container script; New call methdo to run locally o…
F-WRunTime Dec 21, 2023
e48ad8d
Merge branch 'ethereum-optimism:develop' into kontrol-proofs
F-WRunTime Dec 21, 2023
afdb059
Enforcing new paramters local/container/dev for various run scenarios…
F-WRunTime Dec 21, 2023
0c8bdcb
usage wording improvement
F-WRunTime Dec 21, 2023
e29c4e0
Fixing scenario no arguments passed and shifting
F-WRunTime Dec 21, 2023
f65dfdc
Update packages/contracts-bedrock/test/kontrol/scripts/make-summary-d…
JuanCoRo Jan 10, 2024
edd96e0
Update packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh
JuanCoRo Jan 10, 2024
2fc73e6
Typo in packages/contracts-bedrock/test/kontrol/proofs/utils/KontrolU…
JuanCoRo Jan 10, 2024
05fface
Update description of packages/contracts-bedrock/test/kontrol/scripts…
JuanCoRo Jan 10, 2024
7b24c79
Document `run-kontrol.sh` in README
JuanCoRo Jan 10, 2024
9903889
README.md: Update description of the Kontrol folder
JuanCoRo Jan 10, 2024
3af5a68
README.md: refine foundry profile description
JuanCoRo Jan 10, 2024
187dc17
remove remaining `kontrol/kontrol` instances
JuanCoRo Jan 11, 2024
118b1a3
Merge remote-tracking branch 'origin/develop' into kontrol-proofs
JuanCoRo Jan 11, 2024
4322f80
correct location of `run-kontrol.sh` script
JuanCoRo Jan 11, 2024
6449a68
OptimismPortal.k.sol: rename `test_*` to `proof_*`
JuanCoRo Jan 11, 2024
cd0fccb
Kontrol-Deploy.json: update to latest code
JuanCoRo Jan 11, 2024
55682c0
make-summary-deployment.sh: add `forge fmt` as last summary gen step
JuanCoRo Jan 11, 2024
9df4f4a
README.md: fix formatting typo
JuanCoRo Jan 11, 2024
720262f
contracts-bedrock: update bindings (kontrol proofs)
JuanCoRo Jan 11, 2024
d12542e
Replace `/* */` comments by `//`
JuanCoRo Jan 11, 2024
c15feb1
OptimismPortal.k.sol: remove commented `_withdrawalProof` argument
JuanCoRo Jan 11, 2024
e722fd7
Remove `CounterNames.json`
JuanCoRo Jan 11, 2024
4432e6e
Merge remote-tracking branch 'origin/develop' into kontrol-proofs
JuanCoRo Jan 11, 2024
fda41c5
KontrolUtils.sol: remove unused functions
JuanCoRo Jan 12, 2024
e66e086
Describe `clean_json.py` and `reverse_key_values.py`
JuanCoRo Jan 12, 2024
fb78936
test/kontrol/README.md: fix typos
JuanCoRo Jan 12, 2024
9879b5d
OptimismPortal.k.sol: license and typo
JuanCoRo Jan 12, 2024
2130253
KontrolUtils: document the goal of `arrayLength` range
JuanCoRo Jan 12, 2024
520f0c7
`OptimismPortal.k.sol`: rename `proof_*` to `prove_*`
JuanCoRo Jan 12, 2024
49b1de9
Merge remote-tracking branch 'origin/develop' into kontrol-proofs
JuanCoRo Jan 12, 2024
a5ee642
Remove `createWithdrawalTransaction` function; better proof parameters
JuanCoRo Jan 12, 2024
41398d1
OptimismPortal.k.sol: Add tracking issue for symbolic `bytes` support
JuanCoRo Jan 12, 2024
c3b51ee
Merge remote-tracking branch 'origin/develop' into kontrol-proofs
JuanCoRo Jan 12, 2024
b11cb6d
Add deployment summaries license and disclaimer comment
JuanCoRo Jan 16, 2024
bb5cdb7
Merge remote-tracking branch 'origin/develop' into kontrol-proofs
JuanCoRo Jan 16, 2024
2c0641d
versions.json: bump Kontrol to 0.1.117
JuanCoRo Jan 16, 2024
9e3dc05
run-kontrol.sh: update Kontrol version getter method
JuanCoRo Jan 16, 2024
af73c2d
run-kontrol.sh: fix typo for enforcing local Kontrol version
JuanCoRo Jan 16, 2024
e7f9768
`OptimismPortal.k.sol`: remove `== true` no-ops
JuanCoRo Jan 16, 2024
00d7c48
Merge remote-tracking branch 'origin/develop' into kontrol-proofs
JuanCoRo Jan 16, 2024
b6ff288
contracts-bedrock: update bindings (kontrol proofs)
JuanCoRo Jan 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,9 @@
path = packages/contracts-bedrock/lib/safe-contracts
url = https://github.com/safe-global/safe-contracts
branch = v1.4.0
[submodule "packages/contracts-bedrock/lib/kontrol-cheatcodes"]
path = packages/contracts-bedrock/lib/kontrol-cheatcodes
url = https://github.com/runtimeverification/kontrol-cheatcodes
[submodule "packages/contracts-bedrock/lib/solady"]
path = packages/contracts-bedrock/lib/solady
url = https://github.com/Vectorized/solady
Expand Down
2 changes: 1 addition & 1 deletion op-bindings/bindings/weth9.go
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading