1. 19 Mar, 2024 14 commits
  2. 18 Mar, 2024 6 commits
  3. 17 Mar, 2024 1 commit
  4. 15 Mar, 2024 2 commits
  5. 14 Mar, 2024 15 commits
  6. 13 Mar, 2024 2 commits
    • 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
    • smartcontracts's avatar
      feat(ct): unlock can be called while paused (#9819) · df32e7e8
      smartcontracts authored
      Modifies DelayedWETH.unlock so that it can be called while the
      system is paused. Same change was recently applied to the specs.
      Idea behind this change is that the unlock() function is required
      for a game to resolve, so pausing the system would also block
      games from resolving. We want games to be able to resolve, we
      simply don't want incorrectly resolved games to be able to remove
      ETH from the contract. As unlock does not distribute any ETH, this
      change is considered safe.
      df32e7e8