1. 19 Mar, 2024 2 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 5 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
    • dependabot[bot]'s avatar
      dependabot(npm): bump @swc/core from 1.4.1 to 1.4.6 (#9833) · 18837289
      dependabot[bot] authored
      Bumps [@swc/core](https://github.com/swc-project/swc) from 1.4.1 to 1.4.6.
      - [Release notes](https://github.com/swc-project/swc/releases)
      - [Changelog](https://github.com/swc-project/swc/blob/main/CHANGELOG.md)
      - [Commits](https://github.com/swc-project/swc/compare/v1.4.1...v1.4.6)
      
      ---
      updated-dependencies:
      - dependency-name: "@swc/core"
        dependency-type: direct:development
        update-type: version-update:semver-patch
      ...
      Signed-off-by: default avatardependabot[bot] <support@github.com>
      Co-authored-by: default avatardependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
      18837289
    • tdot's avatar
      op-plasma: sync derivation with DA challenge contract state (#9682) · 802c2839
      tdot authored
      * feat: plasma e2e
      
      * feat: skip oversized inputs
      
      * fix: bring back metrics
      
      * feat: set usePlasma in e2e test params
      
      * fix: lint
      
      * fix: activate plasma flag in data source test
      
      * fix: add DA contract proxy to deploy config
      
      * more tests, fix leaky abstraction and refactor loadChallenges
      
      * fix: cleanup type assertion
      
      * support for l1 reorgs, proxy l1 finality signal and tests
      
      * fix: plasma disabled
      
      * add plasma specific e2e test run
      
      * strongly typed commitment
      
      * fix test
      
      * fix sync lookback
      
      * finalize with l1 signal events instead of derivation
      
      * adjust pipeline errors
      
      * fix batcher commitment encoding and invalid comm logging
      
      * fix: adjust plasma state pruning and use bool for DA resetting flag
      
      * fix: use l1 fetcher and check pq length
      802c2839
    • Sebastian Stammler's avatar
      op-batcher: Multi-blob Support (#9779) · 25985c12
      Sebastian Stammler authored
      * op-batcher: Prepare multi-frame support
      
      * op-batcher: adapt tests to multi-frame txData
      
      * op-batcher: add multi-blob transaction support
      
      The existing configuration parameter TargetNumFrames can be used to specify
      the desired number of blobs per transaction.
      
      * op-batcher: improve blobs configuration (for testing)
      
      * op-e2e: add multi-blob batcher test
      
      * op-batcher: consolidate txID String & TerminalString impls
      
      and add a test for it.
      
      * op-batcher: Fix config test
      
      * op-e2e: Improve multi-blob test to assert full blobs
      
      * op-batcher: resolve open TODOs & renames (multi-blob)
      
      * op-batcher: Test channel.NextTxData for single and multi frame txs
      25985c12
  7. 12 Mar, 2024 9 commits