Port to symbolic addresses (#160)

* HEVM: start from concrete store for constructors

* wip

* wip

* wip

* Compiling

* most examples are working

* hevm: port to sym addresses

* fix initcode argumentsin hevm

* ast: add ABI type tag to vars

* hevm: remove warnings

* CLI: cleanup

* HEVM: cleanup

* test: fix compilation errors

* flake: use hevm main

* HEVM: wip updating hevm

* hevm: fix nonce

* hevm: small nits

flake.nix

@@ -5,7 +5,7 @@
     flake-utils.url = "github:numtide/flake-utils";
     nixpkgs.url = "github:nixos/nixpkgs";
     hevmUpstream = {
-      url = "github:ethereum/hevm/308cf16788c29a3e98542d87125d3ffb237615e1";
+      url = "github:ethereum/hevm";
       inputs.nixpkgs.follows = "nixpkgs";
     };
   };

src/Coq.hs

@@ -281,7 +281,7 @@ coqexp :: Exp a -> T.Text
 -- booleans
 coqexp (LitBool _ True)  = "true"
 coqexp (LitBool _ False) = "false"
-coqexp (Var _ SBoolean name)  = T.pack name
+coqexp (Var _ SBoolean _ name)  = T.pack name
 coqexp (And _ e1 e2)  = parens $ "andb "   <> coqexp e1 <> " " <> coqexp e2
 coqexp (Or _ e1 e2)   = parens $ "orb"     <> coqexp e1 <> " " <> coqexp e2
 coqexp (Impl _ e1 e2) = parens $ "implb"   <> coqexp e1 <> " " <> coqexp e2
@@ -295,7 +295,7 @@ coqexp (GEQ _ e1 e2)  = parens $ coqexp e2 <> " <=? " <> coqexp e1
 
 -- integers
 coqexp (LitInt _ i) = T.pack $ show i
-coqexp (Var _ SInteger name)  = T.pack name
+coqexp (Var _ SInteger _ name) = T.pack name
 coqexp (Add _ e1 e2) = parens $ coqexp e1 <> " + " <> coqexp e2
 coqexp (Sub _ e1 e2) = parens $ coqexp e1 <> " - " <> coqexp e2
 coqexp (Mul _ e1 e2) = parens $ coqexp e1 <> " * " <> coqexp e2
@@ -323,12 +323,12 @@ coqexp (ITE _ b e1 e2) = parens $ "if "
 -- as the corresponding Haskell constructor
 coqexp (IntEnv _ envVal) = parens $ T.pack (show envVal) <> " " <> envVar
 -- Contracts
-coqexp (Var _ SContract name) = T.pack name
+coqexp (Var _ SContract _ name) = T.pack name
 coqexp (Create _ cid args) = parens $ T.pack cid <> "." <> T.pack cid <> " " <> envVar <> " " <> coqargs args
 -- unsupported
 coqexp Cat {} = error "bytestrings not supported"
 coqexp Slice {} = error "bytestrings not supported"
-coqexp (Var _ SByteStr _) = error "bytestrings not supported"
+coqexp (Var _ SByteStr _ _) = error "bytestrings not supported"
 coqexp ByStr {} = error "bytestrings not supported"
 coqexp ByLit {} = error "bytestrings not supported"
 coqexp ByEnv {} = error "bytestrings not supported"

src/Enrich.hs

@@ -88,5 +88,5 @@ mkStorageBounds refs = catMaybes $ mkBound <$> refs
 
 mkCallDataBounds :: [Decl] -> [Exp ABoolean]
 mkCallDataBounds = concatMap $ \(Decl typ name) -> case fromAbiType typ of
-  AInteger -> [bound typ (_Var name)]
+  AInteger -> [bound typ (_Var typ name)]
   _ -> []