• 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
KontrolUtils.sol 1.13 KB