Well-typed substitutions for singleton types

src/Act/Enrich.hs

@@ -82,7 +82,7 @@ mkStorageBounds refs = concatMap mkBound refs
     mkBound _ = []
 
 -- TODO why only Pre items here?
-fromItem :: TItem Storage AInteger -> Exp ABoolean
+fromItem :: TItem AInteger Storage -> Exp ABoolean
 fromItem item@(Item _ (PrimitiveType vt) _) = bound vt (TEntry nowhere Pre SStorage item)
 fromItem (Item _ (ContractType _) _) = LitBool nowhere True
 

src/Act/HEVM.hs

@@ -223,10 +223,6 @@ applyUpdate readMap writeMap (Update typ (Item _ _ ref) e) = do
       pure $ M.insert caddr' (updateStorage (EVM.SStore offset e') contract, cid) writeMap
     SByteStr -> error "Bytestrings not supported"
   where
-    -- isContract :: ValueType -> Bool
-    -- isContract (ContractType _) = True
-    -- isContract _ = False
-
     updateStorage :: (EVM.Expr EVM.Storage -> EVM.Expr EVM.Storage) -> EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract
     updateStorage updfun (EVM.C code storage tstorage bal nonce) = EVM.C code (updfun storage) tstorage bal nonce
     updateStorage _ (EVM.GVar _) = error "Internal error: contract cannot be a global variable"
@@ -264,20 +260,32 @@ substUpds :: M.Map Id TypedExp -> [StorageUpdate] -> [StorageUpdate]
 substUpds subst upds = fmap (substUpd subst) upds
 
 substUpd :: M.Map Id TypedExp -> StorageUpdate -> StorageUpdate
-substUpd subst (Update s item expr) = Update s (substItem subst item) (substExp subst expr)
-
-substItem :: M.Map Id TypedExp -> TItem a k -> TItem a k
-substItem subst (Item st vt sref) = Item st vt (substRef subst sref)
-
-substRef :: M.Map Id TypedExp -> Ref k -> Ref k
-substRef _ var@(SVar _ _ _) = var
-substRef _ var@(CVar _ _ x) = undefined
-  -- case M.lookup x subst of
-  --   Just (TExp _ (TEntry _ _ _ item)) -> ref
-  --   Just _ -> error "Internal error: cannot access fields of non-pointer var"
-  --   Nothing -> error "Internal error: ill-formed substitution"
-substRef subst (SMapping pn sref args) = SMapping pn (substRef subst sref) (substArgs subst args)
-substRef subst (SField pn sref x y) = SField pn (substRef subst sref) x y
+substUpd subst (Update s item expr) = case substItem subst item of
+  ETItem SStorage  i -> Update s i (substExp subst expr)
+  ETItem SCalldata _ -> error "Internal error: expecting storage item"
+
+-- | Existential packages to abstract away from reference kinds. Needed to
+-- define subtitutions. 
+-- Note: it would be nice to have these abstracted in one date type that
+-- abstracts the higher-kinded type, but Haskell does not allow partially
+-- applied type synonyms
+data ETItem t = forall k. ETItem (SRefKind k) (TItem t k)
+data ERef = forall k. ERef (SRefKind k) (Ref k)
+
+substItem :: M.Map Id TypedExp -> TItem a k -> ETItem a
+substItem subst (Item st vt sref) = case substRef subst sref of
+  ERef k ref -> ETItem k (Item st vt ref)
+
+substRef :: M.Map Id TypedExp -> Ref k -> ERef
+substRef _ var@(SVar _ _ _) = ERef SStorage var
+substRef subst (CVar _ _ x) = case M.lookup x subst of
+    Just (TExp _ (TEntry _ _ k (Item _ _ ref))) -> ERef k ref
+    Just _ -> error "Internal error: cannot access fields of non-pointer var"
+    Nothing -> error "Internal error: ill-formed substitution"
+substRef subst (SMapping pn sref args) = case substRef subst sref of
+  ERef k ref -> ERef k $ SMapping pn ref (substArgs subst args)
+substRef subst (SField pn sref x y) = case substRef subst sref of
+  ERef k ref -> ERef k $ SField pn ref x y
 
 substArgs :: M.Map Id TypedExp -> [TypedExp] -> [TypedExp]
 substArgs subst exps = fmap (substTExp subst) exps

src/Act/SMT.hs

@@ -688,7 +688,7 @@ sType' (TExp t _) = sType $ actType t
 --- ** Variable Names ** ---
 
 -- Construct the smt2 variable name for a given storage item
-nameFromSItem :: When -> TItem Storage a -> Id
+nameFromSItem :: When -> TItem a Storage -> Id
 nameFromSItem whn (Item _ _ ref) = nameFromSRef ref @@ show whn
 
 nameFromSRef :: Ref Storage -> Id

src/Act/Syntax.hs

@@ -70,7 +70,7 @@ locsFromUpdate update = nub $ case update of
 locFromUpdate :: StorageUpdate t -> StorageLocation t
 locFromUpdate (Update _ item _) = _Loc item
 
-locsFromItem :: SRefKind k -> TItem k a t -> [StorageLocation t]
+locsFromItem :: SRefKind k -> TItem a k t -> [StorageLocation t]
 locsFromItem SCalldata item = concatMap locsFromTypedExp (ixsFromItem item)
 locsFromItem SStorage item = _Loc item : concatMap locsFromTypedExp (ixsFromItem item)
 

src/Act/Syntax/TimeAgnostic.hs

@@ -13,6 +13,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE InstanceSigs #-}
 
 {-|
 Module      : Syntax.TimeAgnostic
@@ -123,24 +124,24 @@ data Behaviour t = Behaviour
 
 
 data StorageUpdate (t :: Timing) where
-  Update :: SType a -> TItem Storage a t -> Exp a t -> StorageUpdate t
+  Update :: SType a -> TItem a Storage t -> Exp a t -> StorageUpdate t
 deriving instance Show (StorageUpdate t)
 
 instance Eq (StorageUpdate t) where
-  Update SType i1 e1 == Update SType i2 e2 = eqS i1 i2 && eqS e1 e2
+  Update SType i1 e1 == Update SType i2 e2 = eqS' i1 i2 && eqS e1 e2
 
-_Update :: SingI a => TItem Storage a t -> Exp a t -> StorageUpdate t
+_Update :: SingI a => TItem a Storage t -> Exp a t -> StorageUpdate t
 _Update item expr = Update sing item expr
 
 data StorageLocation (t :: Timing) where
-  Loc :: SType a -> TItem Storage a t -> StorageLocation t
+  Loc :: SType a -> TItem a Storage t -> StorageLocation t
 deriving instance Show (StorageLocation t)
 
-_Loc :: TItem Storage a t -> StorageLocation t
+_Loc :: TItem a Storage t -> StorageLocation t
 _Loc item@(Item s _ _) = Loc s item
 
 instance Eq (StorageLocation t) where
-  Loc SType i1 == Loc SType i2 = eqS i1 i2
+  Loc SType i1 == Loc SType i2 = eqS' i1 i2
 
 
 -- | Distinguish the type of Refs to calladata variables and storage
@@ -169,8 +170,8 @@ pattern SRefKind :: () => (SingI a) => SRefKind a
 pattern SRefKind <- Sing
 {-# COMPLETE SRefKind #-}
 
--- | Compare equality of two things parametrized by types which have singletons.
-eqKind :: forall (a :: RefKind) (b :: RefKind) f t t'. (SingI a, SingI b, Eq (f a t t')) => f a t t' -> f b t t' -> Bool
+-- | Compare equality of two Items parametrized by different RefKinds.
+eqKind :: forall (a :: RefKind) (b :: RefKind) f t t'. (SingI a, SingI b, Eq (f t a t')) => f t a t' -> f t b t' -> Bool
 eqKind fa fb = maybe False (\Refl -> fa == fb) $ testEquality (sing @a) (sing @b)
 
 -- | Reference to an item in storage or a variable. It can be either a
@@ -185,10 +186,10 @@ data Ref (k :: RefKind) (t :: Timing) where
 deriving instance Show (Ref k t)
 
 instance Eq (Ref k t) where
-  SVar _ c x == SVar _ c' x' = c == c' && x == x'
+  SVar _ c x       == SVar _ c' x'       = c == c' && x == x'
   SMapping _ r ixs == SMapping _ r' ixs' = r == r' && ixs == ixs'
-  SField _ r c x == SField _ r' c' x' = r == r' && c == c' && x == x'
-  _ == _ = False
+  SField _ r c x   == SField _ r' c' x'  = r == r' && c == c' && x == x'
+  _                == _                  = False
 
 -- | Item is a reference together with its Act type. The type is
 -- parametrized on a timing `t`, a type `a`, and the reference kind
@@ -198,12 +199,12 @@ instance Eq (Ref k t) where
 -- referenced. Items are also annotated with the original ValueType
 -- that carries more precise type information (e.g., the exact
 -- contract type).
-data TItem (k :: RefKind) (a :: ActType) (t :: Timing) where
-  Item :: SType a -> ValueType -> Ref k t -> TItem k a t
-deriving instance Show (TItem k a t)
-deriving instance Eq (TItem k a t)
+data TItem (a :: ActType) (k :: RefKind) (t :: Timing) where
+  Item :: SType a -> ValueType -> Ref k t -> TItem a k t
+deriving instance Show (TItem a k t)
+deriving instance Eq (TItem a k t)
 
-_Item :: SingI a => ValueType -> Ref k t -> TItem k a t
+_Item :: SingI a => ValueType -> Ref k t -> TItem a k t
 _Item = Item sing
 
 -- | Expressions for which the return type is known.
@@ -261,7 +262,7 @@ data Exp (a :: ActType) (t :: Timing) where
   Eq  :: Pn -> SType a -> Exp a t -> Exp a t -> Exp ABoolean t
   NEq :: Pn -> SType a -> Exp a t -> Exp a t -> Exp ABoolean t
   ITE :: Pn -> Exp ABoolean t -> Exp a t -> Exp a t -> Exp a t
-  TEntry :: Pn -> Time t -> SRefKind k -> TItem k a t -> Exp a t
+  TEntry :: Pn -> Time t -> SRefKind k -> TItem a k t -> Exp a t
   -- Note: we could use a singleton types to avoid separating Entry and Var 
 deriving instance Show (Exp a t)
 
@@ -366,7 +367,7 @@ instance Timable (Exp a) where
       go :: Timable c => c Untimed -> c Timed
       go = setTime time
 
-instance Timable (TItem k a) where
+instance Timable (TItem a k) where
    setTime time (Item t vt ref) = Item t vt $ setTime time ref
 
 instance Timable (Ref k) where
@@ -470,7 +471,7 @@ instance ToJSON (StorageLocation t) where
 instance ToJSON (StorageUpdate t) where
   toJSON (Update _ a b) = object [ "location" .= toJSON a ,"value" .= toJSON b ]
 
-instance ToJSON (TItem k a t) where
+instance ToJSON (TItem a k t) where
   toJSON (Item t _ a) = object [ "item" .= toJSON a
                                , "type" .=  show t
                                ]

src/Act/Syntax/Types.hs

@@ -60,6 +60,10 @@ instance TestEquality SType where
 eqS :: forall (a :: ActType) (b :: ActType) f t. (SingI a, SingI b, Eq (f a t)) => f a t -> f b t -> Bool
 eqS fa fb = maybe False (\Refl -> fa == fb) $ testEquality (sing @a) (sing @b)
 
+-- | The same but when the higher-kinded type has two type arguments
+eqS' :: forall (a :: ActType) (b :: ActType) f t t'. (SingI a, SingI b, Eq (f a t t')) => f a t t' -> f b t t' -> Bool
+eqS' fa fb = maybe False (\Refl -> fa == fb) $ testEquality (sing @a) (sing @b)
+
 -- Defines which singleton to retrieve when we only have the type, not the
 -- actual singleton.
 instance SingI 'AInteger where sing = SInteger