Support for multiple contracts in equivalence check #167
Conversation
There was a problem hiding this comment.
looks very good in general, just a few small nits mostly.
As we discussed earlier today, it would be great to have some semi formal documentation about what we're doing here (especially regarding the live contract closure invariant), and also some clarification regarding the exact semantics of the Contract and address types, but I think it's ok to do that in a separate pr.
flake.nix
Outdated
| @@ -5,7 +5,7 @@ | |||
| flake-utils.url = "github:numtide/flake-utils"; | |||
| nixpkgs.url = "github:nixos/nixpkgs"; | |||
| hevmUpstream = { | |||
| url = "github:ethereum/hevm"; | |||
| url = "github:ethereum/hevm/f96f0993b73c2937db48bb38e29634d922c40af1"; | |||
There was a problem hiding this comment.
whats on this branch that still hasn't gone into main?
There was a problem hiding this comment.
Nothing, I believe. There was an unpushed commit from Oct 25 that updates the version.
src/HEVM.hs
Outdated
| offsetFromRef _ _ (SField _ _ _ _) = error "TODO contracts not supported" | ||
| updateNonce :: EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract | ||
| updateNonce (EVM.C code storage bal (Just n)) = EVM.C code storage bal (Just (n + 1)) | ||
| updateNonce (EVM.C _ _ _ Nothing) = error "Internal error: nonce must be a number" |
There was a problem hiding this comment.
Can't we just leave it as Nothing in this case?
src/HEVM.hs
Outdated
| store <- rewritesToExpr cmap upds | ||
| pure $ EVM.Success (preconds' <> caseconds') mempty ret' store | ||
|
|
||
| rewritesToExpr :: ContractMap -> [Rewrite] -> ActM ContractMap |
There was a problem hiding this comment.
idk if there could be a more descriptive name here, perhaps like applyRewrites or buildEndState or something?
There was a problem hiding this comment.
Done! Used applyRewrite(s)
src/CLI.hs
Outdated
|
|
||
| Solvers.withSolvers solver' 1 (naturalFromInteger <$> timeout) $ \solvers -> |
There was a problem hiding this comment.
Just a note that it would be nice to support parallel solvers here at some point, but doesn't need to change for this PR
src/CLI.hs
Outdated
| bytecodes cid solContents | ||
| (Nothing, Just c, Just i) -> pure (i, c) | ||
| bytecodes (Text.pack cid) solContents | ||
| (Nothing, Just _, Just _) -> render (text "Only Solidity file supported") >> exitFailure -- pure (i, c) |
Co-authored-by: dxo <[email protected]>
Co-authored-by: dxo <[email protected]>
…o multiple-contracts-behv
For example for the following storage layout,
we create (roughly) this contract map: