From 582cabd743f670ba176c7a214ce9b6da05dee2e2 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 7 Oct 2024 14:36:41 +0200 Subject: [PATCH] Trying to fix issues regarding --code-a/--code-b inputs Better documentation, better error printing Related to #581 --- doc/src/equivalence-checking-tutorial.md | 16 ++++++++++++++++ src/EVM/Format.hs | 2 +- 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/doc/src/equivalence-checking-tutorial.md b/doc/src/equivalence-checking-tutorial.md index b0a93dc81..46e124ffc 100644 --- a/doc/src/equivalence-checking-tutorial.md +++ b/doc/src/equivalence-checking-tutorial.md @@ -102,3 +102,19 @@ consume the same amount of gas and have widely different EVM bytecodes. Yet for an outside observer, they behave the same. Notice that hevm didn't simply fuzz the contract and within a given out of time it didn't find a counterexample. Instead, it _proved_ the two equivalent from an outside observer perspective. + +## Dealing with Already Compiled Contracts + +If the contracts have already been compiled into a hex string, you can paste +them into files `a.txt` and `b.txt` and compare them via: + +```shell +$ hevm equivalence --code-a "$( ByteString -> ByteString hexByteString msg bs = case BS16.decodeBase16Untyped bs of Right x -> x - _ -> internalError $ "invalid hex bytestring for " ++ msg + _ -> internalError $ "invalid hex bytestring for '" ++ msg ++ "'. Bytestring provided: '" ++ show bs ++ "'" hexText :: Text -> ByteString hexText t =