• 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
.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-dispute-mon Loading commit data...
op-e2e Loading commit data...
op-heartbeat Loading commit data...
op-node Loading commit data...
op-plasma 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...
.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...