WIP typing of contract fields

src/Act/Coq.hs

@@ -279,7 +279,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 (VVar _ _ 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
@@ -293,7 +293,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 (VVar _ _ 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
@@ -325,10 +325,11 @@ coqexp (Create _ cid args) = parens $ T.pack cid <> "." <> T.pack cid <> " " <>
 -- 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"
+coqexp (Var _ _ _)  = error "Casting to contracts is not supported"
 
 -- | coq syntax for a proposition
 coqprop :: Exp a -> T.Text
@@ -345,6 +346,7 @@ coqprop (LEQ _ e1 e2)  = parens $ coqexp e1 <> " <= " <> coqexp e2
 coqprop (GT _ e1 e2)   = parens $ coqexp e1 <> " > "  <> coqexp e2
 coqprop (GEQ _ e1 e2)  = parens $ coqexp e1 <> " >= " <> coqexp e2
 coqprop (InRange _ t e) = coqprop (bound t e)
+
 coqprop e = error "ill formed proposition: " <> T.pack (show e)
 
 -- | coq syntax for a typed expression

src/Act/HEVM.hs

@@ -313,14 +313,34 @@ substExp subst expr = case expr of
   NEq pn st a b -> NEq pn st (substExp subst a) (substExp subst b)
 
   ITE pn a b c -> ITE pn (substExp subst a) (substExp subst b) (substExp subst c)
-  TEntry _ _ _ -> expr
-  Var _ st _ x -> case M.lookup x subst of
+  TEntry _ _ _ -> expr -- TODO must do ixs too
+  Var _ st (VVar _ _ x) -> case M.lookup x subst of
     Just (TExp st' exp') -> maybe (error "Internal error: type missmatch") (\Refl -> exp') $ testEquality st st'
     Nothing -> expr
 
-  Create pn a b -> Create pn a (substArgs subst b)
+  Var p st vref -> case substVarRef subst vref of
+    | Left ref -> TEntry p ?? (Item st ?? ref)
+    | Right ref -> Var p st ref
 
+  Create pn a b -> Create pn a (substArgs subst b)
 
+substVarRef :: M.Map Id TypedExp -> VarRef -> Either StorageRef VarRef 
+substVarRef subst (VVar _ _ x) = 
+  case M.lookup x subst of
+    Just (TExp st' (TEntry _ _ (Item _ _ ref)) -> Left ref
+    Just (TExp st' (Var _ _ ref)) -> Right ref
+    Nothing -> error "Internal error: cannot access fields of non-pointer var"
+substVarRef st subst (VField pn st vref c x) =
+  case substVarRef subst vref of
+    | Letf ref -> SField pn ref c x
+    | Right ref -> VField pn st ref c x
+substVarRef st subst (VMapping pn vref ixs) =
+  case substVarRef subst vref of
+    | Letf ref -> SMapping pn ref (substArgs subst ixs)
+    | Right ref -> VMapping pn ref (substArgs subst ixs)
+
+
+
 returnsToExpr :: Monad m => ContractMap -> Maybe TypedExp -> ActT m (EVM.Expr EVM.Buf)
 returnsToExpr _ Nothing = pure $ EVM.ConcreteBuf ""
 returnsToExpr cmap (Just r) = typedExpToBuf cmap r

src/Act/Print.hs

@@ -143,7 +143,7 @@ prettyExp e = case e of
   --polymorphic
   ITE _ a b c -> "(if " <> prettyExp a <> " then " <> prettyExp b <> " else " <> prettyExp c <> ")"
   TEntry _ t a -> timeParens t $ prettyItem a
-  Var _ _ _ x -> x
+  Var _ _ x -> prettyVar x
   where
     print2 sym a b = "(" <> prettyExp a <> " " <> sym <> " " <> prettyExp b <> ")"
 
@@ -161,6 +161,14 @@ prettyRef = \case
   where
     brackets str = "[" <> str <> "]"
 
+prettyVar :: VarRef t -> String
+prettyVar = \case
+  VVar _ _ n -> n
+  VMapping _ r args -> prettyVar r <> concatMap (brackets . prettyTypedExp) args
+  VField _ _ r _ n -> prettyVar r <> "." <> n
+  where
+    brackets str = "[" <> str <> "]"
+
 prettyLocation :: StorageLocation t -> String
 prettyLocation (Loc _ item) = prettyItem item
 
@@ -201,6 +209,11 @@ prettyInvPred = prettyExp . untime . fst
     untimeStorageRef (SMapping p e xs) = SMapping p (untimeStorageRef e) (fmap untimeTyped xs)
     untimeStorageRef (SField p e c x) = SField p (untimeStorageRef e) c x
 
+    untimeVarRef :: VarRef t -> VarRef Untimed
+    untimeVarRef (VVar p c a) = VVar p c a
+    untimeVarRef (VMapping p e xs) = VMapping p (untimeVarRef e) (fmap untimeTyped xs)
+    untimeVarRef (VField p st e c x) = VField p st (untimeVarRef e) c x
+
     untime :: Exp a t -> Exp a Untimed
     untime e = case e of
       And p a b   -> And p (untime a) (untime b)
@@ -235,7 +248,7 @@ prettyInvPred = prettyExp . untime . fst
       ITE p x y z -> ITE p (untime x) (untime y) (untime z)
       Slice p a b c -> Slice p (untime a) (untime b) (untime c)
       TEntry p _ (Item t vt a) -> TEntry p Neither (Item t vt (untimeStorageRef a))
-      Var p t at a -> Var p t at a
+      Var p at a -> Var p at (untimeVarRef a)
 
 
 -- | Doc type for terminal output

src/Act/SMT.hs

@@ -625,7 +625,7 @@ expToSMT2 expr = case expr of
   Eq _ _ a b -> binop "=" a b
   NEq p s a b -> unop "not" (Eq p s a b)
   ITE _ a b c -> triop "ite" a b c
-  Var _ _ _ a -> nameFromVarId a
+  Var _ _ a -> varref a
   TEntry _ w item -> entry item w
   where
     unop :: String -> Exp a -> Ctx SMT2
@@ -644,6 +644,13 @@ expToSMT2 expr = case expr of
       []       -> pure $ nameFromItem whn item
       (ix:ixs) -> select (nameFromItem whn item) (ix :| ixs)
 
+    varref :: VarRef -> Ctx SMT2
+    varref var = case ixsFromVarRef var of
+      []       -> nameFromVarRef var
+      (ix:ixs) -> do
+        name <- nameFromVarRef var
+        select name (ix :| ixs)
+
 -- | SMT2 has no support for exponentiation, but we can do some preprocessing
 --   if the RHS is concrete to provide some limited support for exponentiation
 simplifyExponentiation :: Exp AInteger -> Exp AInteger -> Exp AInteger
@@ -695,6 +702,13 @@ nameFromStorageRef (SVar _ c name) = c @@ name
 nameFromStorageRef (SMapping _ e _) = nameFromStorageRef e
 nameFromStorageRef (SField _ ref c x) = nameFromStorageRef ref @@ c @@ x
 
+nameFromVarRef :: VarRef -> Ctx Id
+nameFromVarRef (VVar _ _ name) = nameFromVarId name
+nameFromVarRef (VMapping _ v _) = nameFromVarRef v
+nameFromVarRef (VField _ _ ref c x) = do
+  name <- nameFromVarRef ref
+  pure $ name @@ c @@ x
+
 -- Construct the smt2 variable name for a given storage location
 nameFromLoc :: When -> StorageLocation -> Id
 nameFromLoc whn (Loc _ item) = nameFromItem whn item

src/Act/Syntax.hs

@@ -73,6 +73,9 @@ locFromUpdate (Update _ item _) = _Loc item
 locsFromItem :: TStorageItem a t -> [StorageLocation t]
 locsFromItem item = _Loc item : concatMap locsFromTypedExp (ixsFromItem item)
 
+locsFromVarRef :: VarRef t -> [StorageLocation t]
+locsFromVarRef var = concatMap locsFromTypedExp (ixsFromVarRef var)
+
 locsFromTypedExp :: TypedExp t -> [StorageLocation t]
 locsFromTypedExp (TExp _ e) = locsFromExp e
 
@@ -113,7 +116,7 @@ locsFromExp = nub . go
       Create _ _ es -> concatMap locsFromTypedExp es
       ITE _ x y z -> go x <> go y <> go z
       TEntry _ _ a -> locsFromItem a
-      Var {} -> []
+      Var _ _ v -> locsFromVarRef v
 
 createsFromExp :: Exp a t -> [Id]
 createsFromExp = nub . go
@@ -292,8 +295,14 @@ contractFromStorageRef (SField _ e _ _) = contractFromStorageRef e
 
 ixsFromItem :: TStorageItem a t -> [TypedExp t]
 ixsFromItem (Item _ _ (SMapping _ _ ixs)) = ixs
+-- TODO this must be fixed for multiple contracts
 ixsFromItem _ = []
 
+ixsFromVarRef :: VarRef t -> [TypedExp t]
+ixsFromVarRef (VMapping _ _ ixs) = ixs
+-- TODO this must be fixed for multiple contracts
+ixsFromVarRef _ = []
+
 contractsInvolved :: Behaviour t -> [Id]
 contractsInvolved = fmap contractFromUpdate . _stateUpdates
 

src/Act/Syntax/Annotated.hs

@@ -13,7 +13,7 @@ import qualified Act.Syntax.TimeAgnostic as Agnostic
 import Act.Syntax.TimeAgnostic (Timing(..),setPre,setPost)
 
 -- Reexports
-import Act.Syntax.TimeAgnostic as Act.Syntax.Annotated hiding (Timing(..),Timable(..),Time,Neither,Act,Contract,Invariant,InvariantPred,Constructor,Behaviour,StorageUpdate,StorageLocation,TStorageItem,Exp,TypedExp,StorageRef)
+import Act.Syntax.TimeAgnostic as Act.Syntax.Annotated hiding (Timing(..),Timable(..),Time,Neither,Act,Contract,Invariant,InvariantPred,Constructor,Behaviour,StorageUpdate,StorageLocation,TStorageItem,Exp,TypedExp,StorageRef,VarRef)
 import Act.Syntax.TimeAgnostic as Act.Syntax.Annotated (pattern Act, pattern Contract, pattern Invariant, pattern Constructor, pattern Behaviour, pattern Exp)
 
 
@@ -27,6 +27,7 @@ type Behaviour       = Agnostic.Behaviour       Timed
 type StorageUpdate   = Agnostic.StorageUpdate   Timed
 type StorageLocation = Agnostic.StorageLocation Timed
 type StorageRef      = Agnostic.StorageRef      Timed
+type VarRef          = Agnostic.VarRef          Timed
 type TStorageItem  a = Agnostic.TStorageItem  a Timed
 type Exp           a = Agnostic.Exp           a Timed
 type TypedExp        = Agnostic.TypedExp        Timed

src/Act/Syntax/TimeAgnostic.hs

@@ -171,11 +171,14 @@ instance Eq (StorageRef t) where
 -- the name of the field name.
 data VarRef (t :: Timing) where
   VVar :: Pn -> AbiType -> Id -> VarRef t
+  VMapping ::  Pn -> VarRef t -> [TypedExp t] -> VarRef t
   VField :: Pn -> SlotType -> VarRef t -> Id -> Id -> VarRef t
 deriving instance Show (VarRef t)
+-- TODO better way to do Vars and Storage entires without duplication 
 
 instance Eq (VarRef t) where
-  VVar _ t x == VVar _ t' x' = t == t' &&  x == x'
+  VVar _ at x == VVar _ at' x' = at == at' &&  x == x'
+  VMapping _ r ixs == VMapping _ r' ixs' = r == r' && ixs == ixs'
   VField _ r vt c x == VField _ r' vt' c' x' = vt == vt' && r == r' && c == c' && x == x'
   _ == _ = False
 
@@ -340,7 +343,7 @@ instance Timable (Exp a) where
     NEq p s x y -> NEq p s (go x) (go y)
     ITE p x y z -> ITE p (go x) (go y) (go z)
     TEntry p _ item -> TEntry p time (go item)
-    Var p t x -> Var p t (go x)
+    Var p at x -> Var p at (go x)
     where
       go :: Timable c => c Untimed -> c Timed
       go = setTime time
@@ -354,9 +357,11 @@ instance Timable StorageRef where
   setTime _ (SVar p c x) = SVar p c x
 
 instance Timable VarRef where
-  setTime time (VField p vt e c x) = VField p vt(setTime time e) c x
+  setTime time (VMapping p e ixs) = VMapping p (setTime time e) (setTime time <$> ixs)
+  setTime time (VField p slt e c x) = VField p slt (setTime time e) c x
   setTime _ (VVar p at x) = VVar p at x
 
+
 ------------------------
 -- * JSON instances * --
 ------------------------
@@ -465,9 +470,10 @@ instance ToJSON (StorageRef t) where
 
 instance ToJSON (VarRef t) where
   toJSON (VVar _ at x) = object [ "kind" .= pack "Var"
-                                , "var" .=  pack x
-                                , "abitype" .=  toJSON at
-                                ]
+                                  , "var" .=  pack x
+                                  , "abitype" .=  toJSON at
+                                  ]
+  toJSON (VMapping _ e xs) = mapping e xs
   toJSON (VField _ _ e c x) = field e c x
 
 mapping :: (ToJSON a1, ToJSON a2) => a1 -> a2 -> Value
@@ -614,3 +620,7 @@ uintmin _ = 0
 
 uintmax :: Int -> Integer
 uintmax a = 2 ^ a - 1
+
+
+_Var :: SingI a => AbiType -> Id -> Exp a t
+_Var atyp x = Var nowhere sing (VVar nowhere atyp x)

src/Act/Traversals.hs

@@ -137,7 +137,7 @@ mapExpM f = \case
     b' <- mapExpM f b
     c' <- mapExpM f c
     f (ITE p a' b' c')
-  Var p s a i -> f (Var p s a i)
+  Var p a r -> f (Var p a r)
   TEntry p t i -> do
     i' <- mapTStorageItemM f i
     f (TEntry p t i')

src/Act/Type.hs

@@ -386,16 +386,20 @@ validateEntry env entry =
 
 
 checkVar :: forall t. Typeable t => Env -> U.Entry -> Err (SlotType, Maybe Id, VarRef t)
-checkVar Env{contract,store,calldata, pointers} (U.EVar p name) = case (Map.lookup name store, Map.lookup name calldata) of
+checkVar Env{store,calldata, pointers} (U.EVar p name) = case (Map.lookup name store, Map.lookup name calldata) of
   (Just _, Just _) -> throw (p, "Ambiguous variable " <> name)
   (Nothing, Just typ) -> do
     pure (StorageValue (PrimitiveType typ), Map.lookup name pointers, VVar p typ name)
   (Just _, Nothing) ->  error $ "Internal error: Variable must be a calldata variable."
   (Nothing, Nothing) -> throw (p, "Unknown variable " <> show name)
   -- TODO more consitent check of name overlap between calldata and storage
-checkVar env (U.EMapping p e args) = throw (p, "Variables cannot have a mapping type")
+checkVar env (U.EMapping p v args) =
+  checkVar env v `bindValidation` \(typ, _, ref) -> case typ of
+    StorageValue _ -> throw (p, "Expression should have a mapping type" <> show v)
+    StorageMapping argtyps restyp ->
+      (StorageValue restyp, Nothing,) . VMapping p ref <$> checkIxs env p args (NonEmpty.toList argtyps)
 checkVar env@Env{theirs} (U.EField p e x) =
-  checkVar env e `bindValidation` \(typ, oc, ref) -> case oc of
+  checkVar env e `bindValidation` \(_, oc, ref) -> case oc of
     Just c -> case Map.lookup c theirs of
       Just cenv -> case Map.lookup x cenv of
         Just (st@(StorageValue (ContractType c')), _) -> pure (st, Just c', VField p st ref c x)
@@ -498,6 +502,7 @@ checkExpr env@Env{constructors} typ e = case (typ, e) of
   (SInteger, U.IntLit  p v1)    -> pure $ LitInt  p v1
   -- Constructor calls
   (SInteger, U.ECreate p c args) -> case Map.lookup c constructors of
+    -- TODO check contract types
     Just typs -> Create p c <$> checkIxs env p args (fmap PrimitiveType typs)
     Nothing -> throw (p, "Unknown constructor " <> show c)
   -- Control
@@ -514,9 +519,10 @@ checkExpr env@Env{constructors} typ e = case (typ, e) of
     Just AInteger -> throw (p, "Environment variable " <> show v1 <> " has type integer but an expression of type bytestring is expected.")
     Just AByteStr -> pure $ ByEnv p v1
     _             -> throw (p, "Unknown environment variable " <> show v1)
-  -- Variable references
+  -- Variable referencesΕΙΔΙΚΟΣ ΛΟΓΑΡΙΑΣΜΟΣ ΚΟΝΔΥΛΙΩΝ ΕΡΕΥΝΑΣ Ε.Μ.Π.
+
   (_, U.EUTEntry entry) | isCalldataEntry env entry -> validateVar env entry `bindValidation` \((FromVType typ'), ref) ->
-    checkTime (getPosEntry entry) <*> (Var (getPosEntry entry) typ ref <$ checkEq (getPosEntry entry) typ typ')
+    Var (getPosEntry entry) typ ref <$ checkEq (getPosEntry entry) typ typ'
   -- Storage references
   (_, U.EUTEntry entry) -> validateEntry env entry `bindValidation` \(vt@(FromVType typ'), ref) ->
     checkTime (getPosEntry entry) <*> (TEntry (getPosEntry entry) Neither (Item typ vt ref) <$ checkEq (getPosEntry entry) typ typ')
@@ -559,12 +565,11 @@ checkContractType env SInteger (ITE p _ a b) =
     (Just c1, Just c2) -> Just c1 <$ assert (p, "Type of if-then-else branches does not match") (c1 == c2)
     (_, _ )-> pure Nothing
 checkContractType _ SInteger (Create _ c _) = pure $ Just c
--- TODO Fix
 checkContractType Env{pointers} SInteger (Var _ _ (VVar _ _ x)) =
   case Map.lookup x pointers of
     Just c -> pure $ Just c
     Nothing -> pure Nothing
-checkContractType Env{pointers} SInteger (Var _ _ (VField _ st _ _ _)) =
+checkContractType _ SInteger (Var _ _ (VField _ st _ _ _)) =
   case st of
     StorageValue (ContractType c) -> pure $ Just c
     _ -> pure $ Nothing