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 =