runtimeverification/evm-semantics

Issues

• Unexpected behaviour in proving `sum-to-n-foundry-spec.k`

  #2617 opened 3 months ago by PetarMax
  7

• using this semantics in Coq

  #2552 opened 4 months ago by aa755
  2

• Add Dencun upgrade changes

  #2356 opened 8 months ago by palinatolmach
  2

• Upstream symbolic bytes lemmas for CSE

  #2476 opened 6 months ago by palinatolmach
  0

• Constructor calls with symbolic parameters

  #2219 opened 6 months ago by RaoulSchaffranek
  2

• Eliminate `klabel(_)` and `symbol` attributes

  #2462 opened 6 months ago by anvacaru
  1

• Eliminate complex `KLabel`s from Python code

  #2456 opened 6 months ago by tothtamas28
  0

• Opt in to new type inference method

  #2213 opened 6 months ago by Baltoli
  2

• Refactor kompilation cache in the intergration tests

  #2419 opened 6 months ago by geo2a
  0

• Issues running kclaim style proofs

  #2088 opened a year ago by ehildenb
  5

• Unable to run claims with `kevm prove`

  #2367 opened 7 months ago by lucasmt
  2

• `freshUInt` cheatcode: replace `#bufStrict` by `#buf`

  #2038 opened 8 months ago by iFrostizz
  0

• Outdated examples in KEVM

  #2338 opened 9 months ago by anvacaru
  2

• Kontrol does not `kup install` in system aarch64-linux

  #2162 opened a year ago by spencerhaoxiao
  0

• Rename `kevm-pyk` to `kevm`

  #2122 opened a year ago by tothtamas28
  0

• Rule coverage and configuration well-formedness

  #2291 opened 10 months ago by PetarMax
  1

• Failure to make libcryptopp libff libsecp256k1

  #2339 opened 9 months ago by ACassimiro
  3

• Examples in `VERIFICATION.md` do not work as expected

  #2289 opened 9 months ago by gl3nng0uld
  0

• `kore-rpc` produces a three-way branch for `JUMPI` in KEVM

  #2151 opened 9 months ago by geo2a
  8

• Tests missing from Pytest harness

  #2275 opened 9 months ago by anvacaru
  1

• KEVM build instructions are out of date

  #2189 opened 9 months ago by radumereuta
  0

• Investigate SMT timeout in `test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec.k`

  #2314 opened 9 months ago by palinatolmach
  0

• Bound env variables (`NUMBER`, `TIMESTAMP`) by reasonable values

  #2143 opened a year ago by palinatolmach
  3

• Turn off `fast_check_subsumption` in CLI by default

  #2295 opened 9 months ago by palinatolmach
  0

• `fast_check_subsumption` causes `Could not convert ML predicate to sort Bool` error

  #2290 opened 10 months ago by palinatolmach
  0

• Default Behavior for Lemma File and Module Import in Kontrol

  #2274 opened 10 months ago by RaoulSchaffranek
  0

• Fix warnings on non-exhaustive matches for rules

  #2248 opened a year ago by anvacaru
  2

• De-duplicate rules introduced as part of the no-gas PR

  #2228 opened 10 months ago by PetarMax
  0

• Start K Server for CI tests

  #2124 opened a year ago by ehildenb
  1

• Duplicate lemmas between two different files

  #2250 opened 10 months ago by ehildenb
  2

• Add option to break on every basic block

  #2240 opened a year ago by ehildenb
  1

• Segfaults on arm64 macOS

  #2238 opened a year ago by Baltoli
  0

• `#parseHexBytes` should be declared total

  #2199 opened a year ago by goodlyrottenapple
  6

• Add `--port`, `--maude-port` to `rpc_args`

  #2177 opened a year ago by palinatolmach
  0

• Improve help messages for `show-kcfg` and `view-kcfg`

  #2157 opened a year ago by anvacaru
  0

• `Directory does not exist` error in `kevm prove`

  #2156 opened a year ago by palinatolmach
  1

• Remove rule label `FOUNDRY.foundry.call` from `kevm_prove`

  #2120 opened a year ago by tothtamas28
  1

• Update documentation to reflect the latest version of Kontrol

  #2133 opened a year ago by RaoulSchaffranek
  2

• Remove `kontrolx`

  #2113 opened a year ago by tothtamas28
  1

• Outdated K causes incorrect KEVM/Kontrol output

  #2097 opened a year ago by palinatolmach
  2

• Docker CI build step too slow

  #2150 opened a year ago by goodlyrottenapple
  1

• `import inotify.adapters` does not work on M1 Mac

  #2145 opened a year ago by PetarMax
  0

• Remove `foundry.md`

  #2140 opened a year ago by tothtamas28
  0

• `setUp()` branches due to out-of-gas in Foundry proofs

  #2058 opened a year ago by palinatolmach
  2

• Clarify and Improve `--test` Parameter Functionality in `kevm foundry-prove`

  #2063 opened a year ago by RaoulSchaffranek
  2

• Replace `--test test,id` by `--test test:id` in the `foundry-prove` test argument

  #2052 opened a year ago by iFrostizz
  0

• `setUp()` function proof not reinitializing when the tests change

  #2073 opened a year ago by nwatson22
  3

• Segmentation Fault Encountered While Generating a Proof

  #2070 opened a year ago by RaoulSchaffranek
  0

• solc-select not integrating with kevm-pyk

  #2061 opened a year ago by anvacaru
  0

• `exec_run` and `exec_kast` take `save_directory` argument but the corresponding commands don't have those options

  #2040 opened a year ago by nwatson22
  0