From 48a20098d2cf7611157c63a7f68646e435aabebd Mon Sep 17 00:00:00 2001 From: zoep Date: Tue, 3 Dec 2024 12:52:38 +0200 Subject: [PATCH] Well-typed substitutions for singleton types --- src/Act/Enrich.hs | 2 +- src/Act/HEVM.hs | 44 ++++++++++++++++++++-------------- src/Act/SMT.hs | 2 +- src/Act/Syntax.hs | 2 +- src/Act/Syntax/TimeAgnostic.hs | 39 +++++++++++++++--------------- src/Act/Syntax/Types.hs | 4 ++++ 6 files changed, 53 insertions(+), 40 deletions(-) diff --git a/src/Act/Enrich.hs b/src/Act/Enrich.hs index 91c4cd60..081e66f4 100644 --- a/src/Act/Enrich.hs +++ b/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 diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs index 33e0d1c2..4aee0123 100644 --- a/src/Act/HEVM.hs +++ b/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 diff --git a/src/Act/SMT.hs b/src/Act/SMT.hs index 9e83f928..c300763d 100644 --- a/src/Act/SMT.hs +++ b/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 diff --git a/src/Act/Syntax.hs b/src/Act/Syntax.hs index 3e9ede6d..b16a9320 100644 --- a/src/Act/Syntax.hs +++ b/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) diff --git a/src/Act/Syntax/TimeAgnostic.hs b/src/Act/Syntax/TimeAgnostic.hs index 3eead5d2..9506aa27 100644 --- a/src/Act/Syntax/TimeAgnostic.hs +++ b/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 ] diff --git a/src/Act/Syntax/Types.hs b/src/Act/Syntax/Types.hs index 7760a89e..be62376c 100644 --- a/src/Act/Syntax/Types.hs +++ b/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