Added

• When a staticcall is made to a contract that does not exist, we overapproximate
  and return symbolic values
• More simplification rules for Props
• JoinBytes simplification rule
• New simplification rule to help deal with abi.encodeWithSelector
• More simplification rules for Props
• Using the SMT solver to get a single concrete value for a symbolic expression
  and continue running, whenever possible
• STATICCALL abstraction is now performed in case of symbolic arguments
• Better error messages for JSON parsing
• Multiple solutions are allowed for a single symbolic expression, and they are
  generated via iterative calls to the SMT solver for quicker solving
• Aliasing works much better for symbolic and concrete addresses
• Constant propagation for symbolic values
• Allow reading bytecode via --code-file or --code-a-file/--code-b-file. Strips
  \n, spaces, and ignores leading 0x to make it easier to use via e.g.
  jq '.deplayedBytecode.object file.json > file.txt' to parse Forge JSON output
  This alleviates the issue when the contract is large and does not fit the command line
  limit of 8192 characters
• Two more simplification rules: ReadByte & ReadWord when the CopySlice
  it is reading from is writing after the position being read, so the
  CopySlice can be ignored
• More simplification rules that help avoid symbolic copyslice in case of
  STATICCALL overapproximation
• Test to make sure we don't accidentally overapproximate a working, good STATICCALL
• Allow EXTCODESIZE/HASH, BALANCE to be abstracted to a symbolic value.
• Allow CALL to be extracted in case --promise-no-reent is given, promising
  no reentrancy of contracts. This may skip over reentrancy vulnerabilities
  but allows much more thorough exploration of the contract
• Allow controlling the max buffer sizes via --max-buf-size to something smaller than 2**64
  so we don't get too large buffers as counterexamples
• More symbolic overapproximation for Balance and ExtCodeHash opcodes, fixing
  CodeHash SMT representation
• Add deployment code flag to the equivalenceCheck function
• PNeg + PGT/PGEq/PLeq/PLT simplification rules
• We no longer dispatch Props to SMT that can be solved by a simplification
• Allow user to change the verbosity level via --verb. For the moment, this is only to
  print some warnings related to zero-address dereference and to print hemv test's
  output in case of failure
• Simple test cases for the CLI
• Allow limiting the branch depth and width limitation via --max-depth and --max-width
• When there are zero solutions to a multi-solution query it means that the
  currently executed branch is in fact impossible. In these cases, unwind all
  frames and return a Revert with empty returndata.
• More rewrite rules for PEq, PNeg, missing eqByte call, and distributivity for And
• Allow changing of the prefix from "prove" via --prefix in test mode
• More complete simplification during interpretation
• SMT-based resolving of addresses now works for delegatecall and staticcall
  opcodes as well
• UNSAT cache is now in Solvers.hs and is therefore shared across all threads.
  Hence, it is now active even during branch queries.
• Rewrite rule to deal with some forms of argument packing by Solidity
  via masking
• More rewrite rules for (PLT (Lit 0) _) and (PEq (Lit 1) _)
• Simplification can now be turned off from the cli via --no-simplify
• When doing Keccak concretization, and simplification is enabled,
  we do both until fixedpoint
• When gathering Keccak axioms, we simplify the bytestring that
  the keccak is applied to
• More rewrite rules for MulMod, AddMod, SHL, SHR, SLT, and SignExtend
• PLEq is now concretized in case it can be computed
• More SignExtend test cases
• Rewrite rules to deal with specific exponentiation patterns
• Added missing simplification and concretization of the SAR instruction

Fixed

• We now try to simplify expressions fully before trying to cast them to a concrete value
  This should improve issues when "Unexpected Symbolic Arguments to Opcode" was
  unnecessarily output
• Not all testcases ran due to incorrect filtering, fixed
• Removed dead code related to IOAct in the now deprecated and removed debugger
• Base case of exponentiation to 0 was not handled, leading to infinite loop
• Better exponential simplification
• Dumping of END states (.prop) files is now default for --debug
• When cheatcode is missing, we produce a partial execution warning
• Size of calldata can be up to 2**64, not 256. This is now reflected in the documentation
• We now have less noise during test runs, and assert more about symbolic copyslice tests
• CopySlice rewrite rule is now less strict while still being sound
• Assumptions about reading from buffer after its size are now the same in all cases.
  Previously, they were too weak in case of reading 32 bytes.
• The equivalence checker now is able to prove that an empty store is
  equivalent to a store with all slots initialized to 0.
• Equivalence checking was incorrectly assuming that overapproximated values
  were sequentially equivalent. We now distinguish these symbolic values with
  A- and B-
• Buffer of all zeroes was interpreted as an empty buffer during parsing SMT model.
  The length of the buffer is now properly taken into account.
• It was possible to enter an infinite recursion when trying to shrink a buffer found by
  the SMT solver. We now properly detect that it is not possible to shrink the buffer.
• Pretty printing of buffers is now more robust. Instead of throwing an internal error,
  we now try best to print everything we can, and print an appropriate error message
  instead of crashing.
• We no longer produce duplicate SMT assertions regarding concrete keccak values.
• Ord is now correctly implemented for Prop.
• Signed and unsigned integers have more refined ranges.
• Symbolic interpretation of assertGe/Gt/Le/Lt over signed integers now works correctly.
• SignExtend is now correctly being constant-folded
• Some of our property-based testing was ineffective because of inadvertent
  simplification happening before calling the SMT solver. This has now been fixed.
• When pranking an address, we used the non-pranked address' nonce
  to calculate the new address. This was incorrect, and lead to address clash,
  as the nonce was never incremented.
• We only report FAIL in test mode for assertion failures that match the
  string prefix "assertion failed", or match function selector Panic(uint256)
  with a parameter 0x1. Previously, require(a==b, "reason") was a cause for
  FAIL in case a!=b was possible. This has now been fixed.
• Out of bounds reads could occur in Haskell when trying to determine
  valid jump destinations. This has now been fixed.

Changed

• Warnings now lead printing FAIL. This way, users don't accidentally think that
  their contract is correct when there were cases/branches that hevm could not
  fully explore. Printing of issues is also now much more organized
• Expressions that are commutative are now canonicalized to have the smaller
  value on the LHS. This can significantly help with simplifications, automatically
  determining when (Eq a b) is true when a==b modulo commutativity
• hevm test's flag --verbose is now --verb, which also increases verbosity
  for other elements of the system
• Add --arrays-exp to cvc5 options.
• We now use Options.Applicative and a rather different way of parsing CLI options.
  This should give us much better control over the CLI options and their parsing.
• block.number can now be symbolic. This only affects library use of hevm
• Removed --smtoutput since it was never used
• We now build with -DCMAKE_POLICY_VERSION_MINIMUM=3.5 libff, as cmake deprecated 3.5
• CheckSatResult has now been unified with ProofResult via SMTResult
• If counterexample would require a buffer that's larger than 1GB, we abandon
  shrinking it.
• If solver is not able to solve a query while attempting to shrink the model, we
  abandon the attempt gracefully instead of crashing with internal error.
• Buffers are now handled more lazily when inspecting a model, which avoids some
  unnecesary internal errors.
• EVM memory is now grown on demand using a 2x factor, to avoid repeated smaller
  increases which hurt concrete execution performance due to their linear cost.
• The concrete MCOPY implementation has been optimized to avoid freezing the whole
  EVM memory.
• We no longer accept check as a prefix for test cases by default.
• The way we print warnings for symbolic mode now matches that of test mode.

PRs merged

• Adding a note about prank and delegatecall by @msooseth in #623
• There is no interactive debugger by @msooseth in #627
• Cleanups in preparation of GHC 9.8 by @elopez in #612
• Fixing missing concKeccakSimpExpr for wordToAddr, maybeLitByte, etc. by @msooseth in #619
• More Prop simplification rules by @msooseth in #628
• Allow dealing with abi.encodeWithSelector by @msooseth in #625
• Use the SMT solver to convert symbolic to concrete value(s) by @msooseth in #629
• Overapproximate staticcall in case we can't resolve callee by @msooseth in #620
• Removing IOAct which was not used by @msooseth in #630
• Adding an example using raw bytecodes to equivalence checking tutorial by @msooseth in #635
• Fixing staticcall abstraction, test case search, and commenting out bug with solidity by @msooseth in #632
• Forgot to set dumpEndStates for --debug by @msooseth in #636
• Better error messages for JSON parsing by @msooseth in #633
• Adding missing base-case for exponentiation && improve Exp handling via simplification and "ite" in SMT by @msooseth in #638
• Fixing partial warning for missing cheatcode by @msooseth in #640
• Gas fixes by @msooseth in #639
• Constant propagation over Props by @msooseth in #642
• Update more precise smt address encoding PR by @msooseth in #641
• Early multi-solutions system by @msooseth in #643
• Better results printing, WARNING-s make the check FAIL now. by @msooseth in #645
• Update description of calldata in documentation by @msooseth in #648
• Faster test running by default by @msooseth in #626
• Faster multi-solution system by @msooseth in #652
• tests: run evm on its own directory by @elopez in #663
• Two simplifications that will be needed to deal with @zoep's issues regarding initcode equivalence by @msooseth in #655
• Allow reading deployedBytecode.object code object from JSON file by @msooseth in #659
• Fix printing during tests, add proper asserts by @msooseth in #668
• New CopySlice rule that helps to avoid symbolic copyslice in case of overapproximation by @msooseth in #667
• Removing some unused code by @msooseth in #672
• Reading code plain from a file instead of JSON by @msooseth in #675
• Much better overapproximation, and maxBufSize limitation by @msooseth in #658
• Fix encoding of assumptions about reading after buffer size. by @blishko in #680
• More symbolic overapproximation when the remote contract cannot be fetched, adding CodeHash SMT representation by @msooseth in #673
• Don't dispatch SMT queries that can be proven False via simplification by @msooseth in #683
• Canonicalize all commutative operators in Expr by @msooseth in #684
• fixed maxBufSize breaking bug by @scottbuckley in #687
• Equivalence fixes by @msooseth in #681
• One more equivalence test by @msooseth in #689
• Use single conf.verb, warn users on zero-address use by @msooseth in #686
• Improve docs by @msooseth in #690
• CLI upgrade for more control and less duplication by @msooseth in #691
• Add --arrays-exp to CVC5 options by @zoep in #694
• Fix windows build by @msooseth in #696
• Removing --smtoutput since it's never used in the code by @msooseth in #699
• Fix interpretation of buffer model value by @blishko in #701
• Fix infinite recursion when trying to shrink buffer by @blishko in #702
• Limiting the branching factor and the depth of branching by @msooseth in #674
• Symbolic block number is now allowed in library mode by @msooseth in #692
• Better structuring of simplify by @msooseth in #693
• Unifying result type by @msooseth in #700
• Avoid eager translation of buffer models by @blishko in #703
• Finish all frames in case there are no solutions to multisol query by @msooseth in #708
• Improve documentation, README, and tutorial by @msooseth in #705
• Limit shrinking to at most 1GB, after that, abandon by @msooseth in #712
• No need for solc to run hevm by @msooseth in #714
• More robust printing by @msooseth in #717
• More rewrite rules for PEq, PNeg, missing eqByte call, and distributivity for And by @msooseth in #716
• Add test case for robust printing by @msooseth in #718
• Rewrite of equivalence checking, now also printing reasons by @msooseth in #713
• Optimize memory representation and operations by @elopez in #707
• Cleanup code, use a struct for loop detection configuration by @msooseth in #721
• Replace actions from DeterminateSystems by @blishko in #723
• Optimize maybeLit{Byte,Word,Addr}Simp and maybeConcStoreSimp by @elopez in #729
• Do not create duplicate assertions about concrete Keccak values by @blishko in #730
• Speed up running tests mostly by avoiding unnecessary work by @blishko in #726
• Remove leftovers after removal of abstraction-refinement loop by @blishko in #731
• Remove unnecessary use of State monad in a helper function by @blishko in #734
• Fix Windows CI build by @elopez in #738
• Avoid internal error when attempting to shrink buffers in model by @blishko in #741
• Fix implementation of Ord for Prop by @blishko in #746
• Fix unsat cache in equivalence checking by @blishko in #747
• Minor cleanup of some code by @msooseth in #748
• Add benchmarking with Solidity examples by @elopez in #744
• Allow changing prefix from prove via --prefix in test mode by @msooseth in #745
• Increase exploration depth when exploring both side of branches with symbolic conditions by @gustavo-grieco in #750
• Use Storable vectors for memory by @elopez in #737
• More complete simplification of branching during interpretation by @msooseth in #749
• Filter out duplicate read assumptions by @blishko in #754
• Use forceAddr in staticcall and delegatecall instead of wordToAddr by @msooseth in #755
• Small refactor of verify to output SMTResult instead of VerifyResult by @gustavo-grieco in #733
• Move unsat cache to Solvers.hs by @msooseth in #743
• Avoid fixpoint for literals and concrete storage by @elopez in #760
• Use a map to implement litToArrayPreimage by @gustavo-grieco in #740
• Allow signed integers to be in the expected range by @gustavo-grieco in #761
• Update tests to highlight bug and fix a test by @msooseth in #768
• Fixing signed assert symbolic interpretation by @msooseth in #769
• Masking rewrite rule by @msooseth in #756
• Correctly print and return partials path logs when symbolic exploration is done by @gustavo-grieco in #762
• More Prop rewrite rules for PLT and PEq by @msooseth in #773
• No need for this extra function, it's the same as genLit by @msooseth in #772
• SignExtend rewrites + Allow turning off simplification from the CLI + fix property-based tests by @msooseth in #774
• For multi-query, print the original query dispatched to the SMT solver by @msooseth in #764
• Use the pranked address' nonce by @msooseth in #777
• Update nix packages to get new bitwuzla 0.7 by @msooseth in #781
• Small update to SMT encoding of MulMod and AddMod by @blishko in #782
• Adding a number of serious improvements to dispatched SMT2 query by @msooseth in #783
• Optimized OpSwap by @elopez in #789
• Make checkSat a public function, allow cached props to be Nothing by @msooseth in #795
• Fixing checking assert failure by @msooseth in #753
• Rewrite exponentiation to bitshift by @blishko in #794
• Fix argument order of shift operation in rewrite rule by @blishko in #796
• Tests: Small fixes in equivalence tests by @blishko in #799
• Print warnings using printWarnings in "symbolic" mode as well by @msooseth in #797
• Fixing out of bounds vector access during Jump Destination validation by @msooseth in #798
• Adding missing SAR simplification by @msooseth in #800

New Contributors

• @scottbuckley made their first contribution in #687
• @gustavo-grieco made their first contribution in #750

Full Changelog: release/0.54.2...release/0.55.0