0.57.0

Added

• We support RPC in equivalence checking now
• Inequality propagation in constant propagation to prune impossible execution paths earlier.
  The constraint solver now tracks lower and upper bounds for symbolic values and detects
  conflicts (e.g., x < 5 && x > 10), significantly reducing the number of paths explored
• Encode symbolic power of 2 as bit-shift in SMT encoding.
• Limit the expansion of the EXP operation to avoid blow-up in the size of the SMT expressions.
• New EXP rewrite rule for base-2 exponents

Fixed

• Fix incorrect simplification rule for PEq (Lit 1) (IsZero (LT a b))

Changed

• Replaced RPC mocking by a full block cache support. This allows users to cache responses from an RPC
  node via --cache-dir dir.
• Changed verify* methods to always require postcodition.
• We now use a symbolic execution queue, so as not to run out of resources when there are
  too many branches to explore.
• Removed type parameter of mutable memory from VM definition.
• Removed simplification that were rewriting concrete bytes-to-be-overwritten
  with zero bytes. Benefits were unclear while it had negative effect on
  analysis' performance.
• We now use the symbolic execution queue to also run the SMT solver in test mode,
  and verify the results using a cexHandler

What's Changed

• Fix incorrect prop simplification involving comparison by @blishko in #899
• Test: Ensure simplifications are tested properly by @blishko in #901
• Test: Small adjustments to run property tests faster by @blishko in #902
• EVM: Split symbolic and concrete sstore handling by @blishko in #903
• Added rpc cache serialization code by @gustavo-grieco in #893
• Quick check on concrete Lit by @msooseth in #905
• EVM: Separate symbolic and concrete handling of SLOAD by @blishko in #904
• SymEx: Always require postcondition in verify* methods by @blishko in #900
• Test: Fix parsing of contracts in ethereum-tests by @blishko in #908
• Test: Refactor blockchain tests to depend less on Contract type by @blishko in #910
• Test: Use single session for all blockchain tests by @blishko in #911
• Remove unnecessary simplification which causes problems in fuzztesting by @blishko in #914
• Move to macos15-intel by @msooseth in #916
• Allows empty RPC for equiv too, add warning to empty RPC by @msooseth in #909
• Test: Small reorganization of blockchain tests by @blishko in #915
• Adding back function and function export for Echidna by @msooseth in #918
• Also warn on precompile address fetch by @msooseth in #913
• Update cli tests to use solc rather than raw assemby by @msooseth in #919
• Unify blockchain tests code by @blishko in #921
• RPC: Small cleanup by @blishko in #923
• Remove type parameter from VM definition by @blishko in #927
• Expr: Remove expensive unnecessary simplification by @blishko in #926
• Expr: Canonicalize transformations by @blishko in #929
• Refactor RPC handling by @blishko in #925
• EVM: Simplify gas refund computation by @blishko in #912
• Fix doc by @gin in #930
• Symbolic execution queue by @msooseth in #906
• Symbolic execution queue should be used to run SMT as well by @msooseth in #934
• Stepper: Unify Fork and ForkMany instructions by @blishko in #942
• Propagate basic inequalities to discard some paths faster by @gustavo-grieco in #935
• CI: Clean up space in ubuntu worker for extra-tests by @blishko in #945
• Expr: Small cleanup in constPropagate by @blishko in #948
• [RFC] Track failures, expose stats, return cache info by @gustavo-grieco in #947
• This fixes release due to directory being too high by @msooseth in #943
• SymEx: Restrict and sort imports by @blishko in #954
• Expr: Further simplification of constPropagate by @blishko in #950
• Github actions: Update nix-quick-install by @blishko in #955
• Clean up worker on the release workflow by @blishko in #956
• Encode symbolic power of 2 as bit-shift in SMT by @gustavo-grieco in #949
• Fix issues with EXP handling, add testing, add more rules by @msooseth in #958
• Bump version for new release: 0.57.0 by @blishko in #959

Full Changelog: release/0.56.0...release/0.57.0