• Juan C's avatar
    Final version for Kontrol pausability proofs (#9530) · 876e16ad
    Juan C authored
    * Update tests to native symbolic `bytes` and `bytes[]`
    
    * adding lemmas
    
    * `run-kontrol.sh`: add more sensible parameters
    
    * Change `startPrank` by `prank`
    
    * Replace `mockCall` workaround with `vm.mockCall`
    
    * Make `bytes` length symbolic
    
    * `KontrolUtils`: remove symbolic workarounds
    
    * `run-kontrol.sh`: add `prove_proveWithdrawalTransaction_paused`
    
    * `forge fmt`
    
    * `versions.json`: bump Kontrol from `0.1.127` to `0.1.156`
    
    * Remove `ASSUME` comments
    
    * ci: run kontrol on develop and allow manual dispatch
    
    * ci: rename parameter
    
    * `OptimismPortalKontrol`: add remaining ranges for `_withdrawalProof`
    
    * Add forge-like UX to `run-kontrol.sh`
    
    * `pausability-lemmas.k`: clean file
    
    * general tests, further lemmas, summary claim
    
    * Address shellcheck failures
    
    * Change `pausability-lemmas.k` to `pausability-lemmas.md`
    
    * `versions.json`: bump `kontrol` from `0.1.156` to `0.1.178`
    
    * `OptimismPortalKontrol`: update `kontrol` natspec to version 0.1.178
    
    * `pausability-lemmas.md`: remove unused `Lemmas` header
    
    * Update packages/contracts-bedrock/test/kontrol/pausability-lemmas.md
    Co-authored-by: default avatarMatt Solomon <matt@mattsolomon.dev>
    
    * Update packages/contracts-bedrock/test/kontrol/pausability-lemmas.md
    Co-authored-by: default avatarMatt Solomon <matt@mattsolomon.dev>
    
    * Update packages/contracts-bedrock/test/kontrol/pausability-lemmas.md
    Co-authored-by: default avatarMatt Solomon <matt@mattsolomon.dev>
    
    * Update packages/contracts-bedrock/test/kontrol/pausability-lemmas.md
    Co-authored-by: default avatarMatt Solomon <matt@mattsolomon.dev>
    
    * `pausability-lemmas.md`: fix spelling typo
    
    * `pausability-lemmas.md`: fix typo `bytearrays` to `byte arrays`
    
    * `run-kontrol.sh`: correctly format temorarily unexecuted lemmas
    
    * `common.sh`: execute `copy_to_docker` only when in docker mode
    
    * `make-summary-deployment.sh`: add argument check before parsing
    
    * Reflect `kontrol summary` change to `kontrol load-state-diff`
    
    From version `0.1.162`, `kontrol summary` has been renamed to `kontrol
    load-state-diff`.
    The reason of this renaming is that `kontrol summary` will be
    used by kontrol's compositional symbolic execution.
    Also, changing the name to `load-state-diff` makes more explicit what the
    command does.
    Related PR: https://github.com/runtimeverification/kontrol/pull/374
    
    * `pausability-lemmas.md`: remove upstreamed lemmas
    
    * fix: writing typos
    
    * lemma text pass
    
    * paragraph about summary maintainability
    
    * README.md: include latest changes
    
    * pausability-lemmas.md: markdown link typo
    
    * KontrolUtils: add documentation comment
    
    * pausability-lemmas.md: fix markdown typo vol2
    
    * pausability-lemmas.md: fix markdown typo vol3
    
    * Add specialized usage functions
    
    * `README.md`: remove `bash` in `make-summary-deployment.sh` description
    
    * `README.md`: complete `Add New Proofs` section
    
    * versions.json: bump kontrol from 0.1.178 to 0.1.196
    
    * run-kontrol.sh: add `--xml-test-report` flag
    
    * .gitignore: add `kontrol_prove_report.xml`
    
    * foundry.toml: set `ast = true` in `kprove` profile
    
    * config.yml: set correct path for kontrol `store_artifacts`
    
    * config.yml: add `store_test_results` step to `kontrol-tests` job
    
    * package.json: execute `run-kontrol.sh` with `script` option
    
    We run `run-kontrol.sh` with the `script` option to avoid executing all proofs
    
    * run-kontrol.sh: remove proof with 10 elements in favor of 0 and 1
    
    The longer the `_withdrawalProof` array the longer the execution time
    Adding the lengths 0 and 1 fits within the max cpus and won't take as long to run
    
    * chore: typos and formatting
    
    * ci: fix kontrol trigger
    
    * README.md: minor typo
    
    ---------
    Co-authored-by: default avatarPetar Maksimovic <petar.maksimovic@runtimeverification.com>
    Co-authored-by: default avatarMatt Solomon <matt@mattsolomon.dev>
    876e16ad
Name
Last commit
Last update
..
L1 Loading commit data...
L2 Loading commit data...
Safe Loading commit data...
actors Loading commit data...
cannon Loading commit data...
dispute Loading commit data...
governance Loading commit data...
invariants Loading commit data...
kontrol Loading commit data...
legacy Loading commit data...
libraries Loading commit data...
mocks Loading commit data...
periphery Loading commit data...
safe-tools Loading commit data...
setup Loading commit data...
universal Loading commit data...
vendor Loading commit data...
BenchmarkTest.t.sol Loading commit data...
ExtendedPause.t.sol Loading commit data...
Predeploys.t.sol Loading commit data...
Specs.t.sol Loading commit data...