0.56.0

Changes since 0.55.1:

Added

• Output geth compatible jsonl traces in hevm exec via --json-trace
• Allow dumping unsolved SMT files via --dump-unsolved
• Allow resolving unknown addresses to only those that are already deployed
  via option --only-deployed
• New empty solver option that simply makes sure that all SMT queries return
  unknown
• Allow verifyInputs to return partial expressions
• Counterexamples are now validated when running in hevm test mode
• RPC mocking framework that allows users to mock responses from an RPC
  node via --mock-file FILE.json. This will improve reliability of
  tests that depend on RPC responses
• We now map back (add,pc) warnings to lines of source code
• Calldata decoding is now more robust: we try to decode
  as much as possible even in case of trailing bytes

Fixed

• We now extract more Keccak computations than before from the Props to assert
  more Keccak equalities.
• Fixed false positive caused by loss of information about concrete
  Keccak computations.
• Faster word256Bytes and word160Bytes functions to help concrete execution
  performance
• We avoid crashing if a cheatcode or a precompiled is invalid or not implemented in concrete mode
• RPC fetching was sometimes incorrect in case of writing to storage
  before fetching it via RPC
• We no longer increment branch depth twice when branching both ways
• We now take into account loop heuristic setting for test
• We no longer fetch Latest more than once, thereby potentially having
  more than one interpretation of Latest. Instead, we fetch it once, and
  fix any further Latest block to the previously fetched fixed block number
• RPC fetching is now done through a single HTTPS session.
• RPC cache is now more effective, as it's persisted through different
  threads of the symbolic execution
• During running in --only-deployed mode, we forgot to force the address
  in the constraints to be the one we computed it to be. Fixed.
• We now properly collect all storage reads from the program and build
  a proper counterexample. Previously, some information might have been missing.
• Fixed int calldata decoding of solc's v1 ABI encoding

Changed

• Updated forge to 1.2.3 and forge-std to 60acb7aa (1.9.7+)
• We now gather Keccak axioms during setUp() and inject them into the SMT solver.
  This helps us finding more correct Keccak preimages
• The "origin" address is now symbolic by default when running in symbolic mode
• The printed expressions when running in symbolic mode are now simplified
• The printed reachable expression is now simplified
• hevm and solidity has been moved to under github.com/argotorg
• Extra range constraints for ABI symbolic types are no longer added. They are
  not needed as they are enforced in the bytecode.
• We no longer try to fuzz the Expr to find a concrete value that satisfies
  the expression. This was not very effective and made the system more complex
  to maintain. Echidna is an excellent fuzzer that can be used instead.
• Shrinking of the calldata is now more aggressive, shrinking even small (<1024B)
  buffers
• Rename confusing function name runSolidityTest to runForgeTest

PRs merged

• Add cost centers to opcodes, optimize by @elopez in #803
• Minor cleanup -- less brackets by @msooseth in #810
• More complete keccak computation by @msooseth in #812
• Update forge and forge-std to latest stable by @msooseth in #809
• Optimize word256Bytes, word160Bytes by @elopez in #808
• Collect keccaks during concrete running and inject them into the Props during query by @msooseth in #806
• Update readme to be more user-friendly by @msooseth in #813
• Use maxWidth instead of hardcoded value by @msooseth in #817
• Revert "Use maxWidth instead of hardcoded value" by @msooseth in #820
• Allow dumping unsolved SMT files by @msooseth in #814
• Add empty solver as an option by @msooseth in #815
• Better error propagation in reading bytecode from JSON by @blishko in #821
• Solidity: Reduce duplication of code by @blishko in #823
• Added missing assert condition to catch failures in solc < 0.8 by @gustavo-grieco in #824
• With --only-deployed, only resolve addresses to deployed contracts by @msooseth in #818
• Update quick install guide by @msooseth in #826
• Solidity: Refactor reading standard JSON from solc by @blishko in #825
• Allow verifyInputs to return partial expressions by @gustavo-grieco in #822
• Simplifications: Avoid unnecessary memory allocations by @blishko in #830
• SMT: Fix collecting storage reads by @blishko in #834
• Nix: Update nixpkgs by @blishko in #835
• SymExec: Pre-filter safe branches by @blishko in #833
• Expr: Avoid unnecessary allocations in Expr simplifications by @blishko in #836
• Implement toString cheatcode by @elopez in #838
• SymEx: Do not simplify whole program representation by @blishko in #843
• Bump dependency upper bounds by @elopez in #846
• Fixing missing loop heuristic usage in Test by @msooseth in #853
• Fixing double depth incrementing by @msooseth in #852
• SMT: Avoid unnecessary allocations during Expr translation by @blishko in #845
• We should simplify the printed expression by @msooseth in #858
• Mapping back of warnings to lines of code by @msooseth in #851
• Fixing RPC fetching and reading of slots, adding mocking to RPC for testing by @msooseth in #837
• Check that CEX-es can be reproduced in test mode by @msooseth in #827
• Explain warnings and validation issues in hevm.dev by @msooseth in #844
• Adding forcing of value for runAll by @msooseth in #856
• Initial SMT refactoring by @blishko in #860
• Make "origin" address symbolic in symbolic mode + simplify printed expression by @msooseth in #859
• SMT: Do not return unnecessary information from checkSatWithProps by @blishko in #864
• SMT: Do not parse term in get-val response by @blishko in #865
• SMT: Small changes towards efficiency by @blishko in #866
• Adding session use for RPC, along with shared cache and fixed Latest Block by @msooseth in #861
• Fixing build after RPC merging due to unused variable by @msooseth in #869
• SMT: Fix Keccak constraints to use definitions by @blishko in #867
• Moving repository to argotorg, adding Argot Collective by @msooseth in #870
• Fixing github page publishing via SSH deploy key by @msooseth in #871
• Simplifications: Normalize and add one more rule by @blishko in #872
• This flake lock update is automatic, adding as a change by @msooseth in #873
• Update symbolic benchmark runner to use Bitwuzla by @blishko in #874
• ABI: Do not add extra constraints for symbolic arguments by @blishko in #875
• Expr: Fix maxLitSigned by @blishko in #876
• Expr: Fix collecting reads from abstract storage by @blishko in #881
• Removing Cex fuzzer by @msooseth in #879
• cli/exec: expose json tracing option by @d-xo in #878
• Export a few more functions from Fetch by @gustavo-grieco in #885
• Expr: Add missing simplification for read over copyslice by @blishko in #877
• Fix GHC 9.10 warnings by @elopez in #883
• Fix missing information about concrete Keccak computations by @blishko in #888
• Rename confusing function name by @msooseth in #891
• More robust calldata decoding, more shrinking by @msooseth in #887
• Avoid unnecessary code duplication by @blishko in #892
• Revert instead of crash when a missing cheatcode or precompile is used in concrete mode by @gustavo-grieco in #840
• Fix int decoding when upper bits are not set by @gustavo-grieco in #894
• Bump version for new release, 0.56.0 by @msooseth in #896
• Fix release action by @msooseth in #897

Full Changelog: release/0.55.1...release/0.56.0