CARVIEW |
Select Language
HTTP/2 302
date: Wed, 23 Jul 2025 03:08:33 GMT
content-type: text/html; charset=utf-8
content-length: 0
vary: X-PJAX, X-PJAX-Container, Turbo-Visit, Turbo-Frame, X-Requested-With,Accept-Encoding, Accept, X-Requested-With
location: https://github.com/ethereum/hevm/releases/tag/release/0.55.1
cache-control: no-cache
strict-transport-security: max-age=31536000; includeSubdomains; preload
x-frame-options: deny
x-content-type-options: nosniff
x-xss-protection: 0
referrer-policy: no-referrer-when-downgrade
content-security-policy: default-src 'none'; base-uri 'self'; child-src github.githubassets.com github.com/assets-cdn/worker/ github.com/assets/ gist.github.com/assets-cdn/worker/; connect-src 'self' uploads.github.com www.githubstatus.com collector.github.com raw.githubusercontent.com api.github.com github-cloud.s3.amazonaws.com github-production-repository-file-5c1aeb.s3.amazonaws.com github-production-upload-manifest-file-7fdce7.s3.amazonaws.com github-production-user-asset-6210df.s3.amazonaws.com *.rel.tunnels.api.visualstudio.com wss://*.rel.tunnels.api.visualstudio.com objects-origin.githubusercontent.com copilot-proxy.githubusercontent.com proxy.individual.githubcopilot.com proxy.business.githubcopilot.com proxy.enterprise.githubcopilot.com *.actions.githubusercontent.com wss://*.actions.githubusercontent.com productionresultssa0.blob.core.windows.net/ productionresultssa1.blob.core.windows.net/ productionresultssa2.blob.core.windows.net/ productionresultssa3.blob.core.windows.net/ productionresultssa4.blob.core.windows.net/ productionresultssa5.blob.core.windows.net/ productionresultssa6.blob.core.windows.net/ productionresultssa7.blob.core.windows.net/ productionresultssa8.blob.core.windows.net/ productionresultssa9.blob.core.windows.net/ productionresultssa10.blob.core.windows.net/ productionresultssa11.blob.core.windows.net/ productionresultssa12.blob.core.windows.net/ productionresultssa13.blob.core.windows.net/ productionresultssa14.blob.core.windows.net/ productionresultssa15.blob.core.windows.net/ productionresultssa16.blob.core.windows.net/ productionresultssa17.blob.core.windows.net/ productionresultssa18.blob.core.windows.net/ productionresultssa19.blob.core.windows.net/ github-production-repository-image-32fea6.s3.amazonaws.com github-production-release-asset-2e65be.s3.amazonaws.com insights.github.com wss://alive.github.com api.githubcopilot.com api.individual.githubcopilot.com api.business.githubcopilot.com api.enterprise.githubcopilot.com; font-src github.githubassets.com; form-action 'self' github.com gist.github.com copilot-workspace.githubnext.com objects-origin.githubusercontent.com; frame-ancestors 'none'; frame-src viewscreen.githubusercontent.com notebooks.githubusercontent.com; img-src 'self' data: blob: github.githubassets.com media.githubusercontent.com camo.githubusercontent.com identicons.github.com avatars.githubusercontent.com private-avatars.githubusercontent.com github-cloud.s3.amazonaws.com objects.githubusercontent.com release-assets.githubusercontent.com secured-user-images.githubusercontent.com/ user-images.githubusercontent.com/ private-user-images.githubusercontent.com opengraph.githubassets.com copilotprodattachments.blob.core.windows.net/github-production-copilot-attachments/ github-production-user-asset-6210df.s3.amazonaws.com customer-stories-feed.github.com spotlights-feed.github.com objects-origin.githubusercontent.com *.githubusercontent.com; manifest-src 'self'; media-src github.com user-images.githubusercontent.com/ secured-user-images.githubusercontent.com/ private-user-images.githubusercontent.com github-production-user-asset-6210df.s3.amazonaws.com gist.github.com; script-src github.githubassets.com; style-src 'unsafe-inline' github.githubassets.com; upgrade-insecure-requests; worker-src github.githubassets.com github.com/assets-cdn/worker/ github.com/assets/ gist.github.com/assets-cdn/worker/
server: github.com
set-cookie: _gh_sess=6tIFdBefUVRe7f9z6chJRkmLykrZVYOTlJS7wR1pdB8ThLMZVBRdCgonKz6ELx51nzTkHHLtrMRHAdWDeyGxLAiYGKvSdlYFPVLiJAM%2B9k5Werl55084%2FJNkNThuwyv3B7CfKmOWI1RuvIK7PClKV%2FGBDdGA2F2n7U%2FV8jktODTGOIWGEJ7fyklWU3T0Q6WXlwEcXVt0x6g7ROnLfaEvifI2cgTXPQZQbwM5DRnY%2BFj2aqUnkbGltA48R7tDjCkG1Z3N8s%2BGA35i7V4SQoVe7g%3D%3D--VppjxXs4G%2FPJO8nm--h15G%2BolHSuq5Cdpp8FcJdA%3D%3D; Path=/; HttpOnly; Secure; SameSite=Lax
set-cookie: _octo=GH1.1.1827902083.1753240113; Path=/; Domain=github.com; Expires=Thu, 23 Jul 2026 03:08:33 GMT; Secure; SameSite=Lax
set-cookie: logged_in=no; Path=/; Domain=github.com; Expires=Thu, 23 Jul 2026 03:08:33 GMT; HttpOnly; Secure; SameSite=Lax
x-github-request-id: C060:121670:2AC0B8:3C46E3:68805231
HTTP/2 200
date: Wed, 23 Jul 2025 03:08:34 GMT
content-type: text/html; charset=utf-8
vary: X-PJAX, X-PJAX-Container, Turbo-Visit, Turbo-Frame, X-Requested-With,Accept-Encoding, Accept, X-Requested-With
etag: W/"ebc215a03d8fd190c6bb8c4268a84dba"
cache-control: max-age=0, private, must-revalidate
strict-transport-security: max-age=31536000; includeSubdomains; preload
x-frame-options: deny
x-content-type-options: nosniff
x-xss-protection: 0
referrer-policy: no-referrer-when-downgrade
content-security-policy: default-src 'none'; base-uri 'self'; child-src github.githubassets.com github.com/assets-cdn/worker/ github.com/assets/ gist.github.com/assets-cdn/worker/; connect-src 'self' uploads.github.com www.githubstatus.com collector.github.com raw.githubusercontent.com api.github.com github-cloud.s3.amazonaws.com github-production-repository-file-5c1aeb.s3.amazonaws.com github-production-upload-manifest-file-7fdce7.s3.amazonaws.com github-production-user-asset-6210df.s3.amazonaws.com *.rel.tunnels.api.visualstudio.com wss://*.rel.tunnels.api.visualstudio.com objects-origin.githubusercontent.com copilot-proxy.githubusercontent.com proxy.individual.githubcopilot.com proxy.business.githubcopilot.com proxy.enterprise.githubcopilot.com *.actions.githubusercontent.com wss://*.actions.githubusercontent.com productionresultssa0.blob.core.windows.net/ productionresultssa1.blob.core.windows.net/ productionresultssa2.blob.core.windows.net/ productionresultssa3.blob.core.windows.net/ productionresultssa4.blob.core.windows.net/ productionresultssa5.blob.core.windows.net/ productionresultssa6.blob.core.windows.net/ productionresultssa7.blob.core.windows.net/ productionresultssa8.blob.core.windows.net/ productionresultssa9.blob.core.windows.net/ productionresultssa10.blob.core.windows.net/ productionresultssa11.blob.core.windows.net/ productionresultssa12.blob.core.windows.net/ productionresultssa13.blob.core.windows.net/ productionresultssa14.blob.core.windows.net/ productionresultssa15.blob.core.windows.net/ productionresultssa16.blob.core.windows.net/ productionresultssa17.blob.core.windows.net/ productionresultssa18.blob.core.windows.net/ productionresultssa19.blob.core.windows.net/ github-production-repository-image-32fea6.s3.amazonaws.com github-production-release-asset-2e65be.s3.amazonaws.com insights.github.com wss://alive.github.com api.githubcopilot.com api.individual.githubcopilot.com api.business.githubcopilot.com api.enterprise.githubcopilot.com; font-src github.githubassets.com; form-action 'self' github.com gist.github.com copilot-workspace.githubnext.com objects-origin.githubusercontent.com; frame-ancestors 'none'; frame-src viewscreen.githubusercontent.com notebooks.githubusercontent.com; img-src 'self' data: blob: github.githubassets.com media.githubusercontent.com camo.githubusercontent.com identicons.github.com avatars.githubusercontent.com private-avatars.githubusercontent.com github-cloud.s3.amazonaws.com objects.githubusercontent.com release-assets.githubusercontent.com secured-user-images.githubusercontent.com/ user-images.githubusercontent.com/ private-user-images.githubusercontent.com opengraph.githubassets.com copilotprodattachments.blob.core.windows.net/github-production-copilot-attachments/ github-production-user-asset-6210df.s3.amazonaws.com customer-stories-feed.github.com spotlights-feed.github.com objects-origin.githubusercontent.com *.githubusercontent.com; manifest-src 'self'; media-src github.com user-images.githubusercontent.com/ secured-user-images.githubusercontent.com/ private-user-images.githubusercontent.com github-production-user-asset-6210df.s3.amazonaws.com gist.github.com; script-src github.githubassets.com; style-src 'unsafe-inline' github.githubassets.com; upgrade-insecure-requests; worker-src github.githubassets.com github.com/assets-cdn/worker/ github.com/assets/ gist.github.com/assets-cdn/worker/
server: github.com
content-encoding: gzip
accept-ranges: bytes
x-github-request-id: C060:121670:2AC0C8:3C4704:68805231
Release 0.55.1 · ethereum/hevm · GitHub
Loading
Skip to content
Navigation Menu
{{ message }}
-
Notifications
You must be signed in to change notification settings - Fork 64
Compare
c145418
This commit was created on GitHub.com and signed with GitHub’s verified signature.
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 leading0x
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 theCopySlice
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 printhemv 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-
andB-
- 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 oftest
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
forwordToAddr
,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
andmaybeConcStoreSimp
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
intest
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 ofwordToAddr
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
Assets 5
1 person reacted
You can’t perform that action at this time.