From 63b28d614a29daeb6efb2f2a211c83f54887114d Mon Sep 17 00:00:00 2001 From: zoep Date: Fri, 27 Oct 2023 18:49:24 +0300 Subject: [PATCH] Syntax: remove constant --- src/Coq.hs | 6 +- src/Enrich.hs | 28 ++-- src/HEVM.hs | 11 +- src/K.hs | 313 ------------------------------------- src/Print.hs | 5 +- src/SMT.hs | 32 ++-- src/Syntax.hs | 76 +++------ src/Syntax/Annotated.hs | 10 +- src/Syntax/TimeAgnostic.hs | 12 +- src/Syntax/Typed.hs | 5 +- src/Type.hs | 14 +- src/act.cabal | 2 +- 12 files changed, 75 insertions(+), 439 deletions(-) delete mode 100644 src/K.hs diff --git a/src/Coq.hs b/src/Coq.hs index 95520a4e..42d7ae73 100644 --- a/src/Coq.hs +++ b/src/Coq.hs @@ -77,7 +77,7 @@ reachable constructor behvs = inductive -- | non-recursive constructor for the reachable relation baseCase :: Constructor -> T.Text -baseCase (Constructor name i@(Interface _ decls) conds _ _ _ _) = +baseCase (Constructor name i@(Interface _ decls) conds _ _ _ ) = T.pack name <> baseSuffix <> " : " <> universal <> "\n" <> constructorBody where baseval = parens $ T.pack name <> " " <> envVar <> " " <> arguments i @@ -113,7 +113,7 @@ reachableStep (Behaviour name _ i conds cases _ _ _) = -- | definition of a base state base :: Store -> Constructor -> T.Text -base store (Constructor name i _ _ _ updates _) = +base store (Constructor name i _ _ _ updates) = definition (T.pack name) (envDecl <> " " <> interface i) $ stateval store name (\_ t -> defaultSlotValue t) updates @@ -121,7 +121,7 @@ transition :: Store -> Behaviour -> Fresh T.Text transition store (Behaviour name cname i _ _ _ rewrites _) = do name' <- fresh name return $ definition name' (envDecl <> " " <> stateDecl <> " " <> interface i) $ - stateval store cname (\ref _ -> storageRef ref) (updatesFromRewrites rewrites) + stateval store cname (\ref _ -> storageRef ref) rewrites -- | inductive definition of a return claim -- ignores claims that do not specify a return value diff --git a/src/Enrich.hs b/src/Enrich.hs index 09b9867a..f97c6228 100644 --- a/src/Enrich.hs +++ b/src/Enrich.hs @@ -18,13 +18,13 @@ enrich (Act store contracts) = Act store (enrichContract <$> contracts) -- |Adds type bounds for calldata , environment vars, and external storage vars as preconditions enrichConstructor :: Constructor -> Constructor -enrichConstructor ctor@(Constructor _ (Interface _ decls) pre _ invs _ storageUpdates) = +enrichConstructor ctor@(Constructor _ (Interface _ decls) pre _ invs rewrites) = ctor { _cpreconditions = pre' , _invariants = invs' } where pre' = pre <> mkCallDataBounds decls - <> mkStorageBounds storageUpdates + <> mkStorageBounds rewrites <> mkEthEnvBounds (ethEnvFromConstructor ctor) invs' = enrichInvariant ctor <$> invs @@ -40,14 +40,14 @@ enrichBehaviour behv@(Behaviour _ _ (Interface _ decls) pre _ _ stateUpdates _) -- | Adds type bounds for calldata, environment vars, and storage vars enrichInvariant :: Constructor -> Invariant -> Invariant -enrichInvariant (Constructor _ (Interface _ decls) _ _ _ _ _) inv@(Invariant _ preconds storagebounds (predicate,_)) = +enrichInvariant (Constructor _ (Interface _ decls) _ _ _ _) inv@(Invariant _ preconds storagebounds (predicate,_)) = inv { _ipreconditions = preconds', _istoragebounds = storagebounds' } where preconds' = preconds <> mkCallDataBounds decls <> mkEthEnvBounds (ethEnvFromExp predicate) storagebounds' = storagebounds - <> mkStorageBounds (Constant <$> locsFromExp predicate) + <> mkStorageBoundsLoc (locsFromExp predicate) mkEthEnvBounds :: [EthEnv] -> [Exp ABoolean] mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars @@ -74,17 +74,23 @@ mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars Nonce -> AbiUIntType 256 -- | extracts bounds from the AbiTypes of Integer values in storage -mkStorageBounds :: [Rewrite] -> [Exp ABoolean] +mkStorageBounds :: [StorageUpdate] -> [Exp ABoolean] mkStorageBounds refs = catMaybes $ mkBound <$> refs where - mkBound :: Rewrite -> Maybe (Exp ABoolean) - mkBound (Constant (Loc SInteger item)) = Just $ fromItem item - mkBound (Rewrite (Update SInteger item _)) = Just $ fromItem item + mkBound :: StorageUpdate -> Maybe (Exp ABoolean) + mkBound (Update SInteger item _) = Just $ fromItem item mkBound _ = Nothing - fromItem :: TStorageItem AInteger -> Exp ABoolean - fromItem item@(Item _ (PrimitiveType vt) _) = bound vt (TEntry nowhere Pre item) - fromItem (Item _ (ContractType _) _) = LitBool nowhere True +fromItem :: TStorageItem AInteger -> Exp ABoolean +fromItem item@(Item _ (PrimitiveType vt) _) = bound vt (TEntry nowhere Pre item) +fromItem (Item _ (ContractType _) _) = LitBool nowhere True + +mkStorageBoundsLoc :: [StorageLocation] -> [Exp ABoolean] +mkStorageBoundsLoc refs = catMaybes $ mkBound <$> refs + where + mkBound :: StorageLocation -> Maybe (Exp ABoolean) + mkBound (Loc SInteger item) = Just $ fromItem item + mkBound _ = Nothing mkCallDataBounds :: [Decl] -> [Exp ABoolean] mkCallDataBounds = concatMap $ \(Decl typ name) -> case fromAbiType typ of diff --git a/src/HEVM.hs b/src/HEVM.hs index d4f8509c..53965108 100644 --- a/src/HEVM.hs +++ b/src/HEVM.hs @@ -125,7 +125,7 @@ translateActConstr (Act store [Contract ctor _]) bytecode = translateConstructor translateActConstr (Act _ _) _ = error "TODO multiple contracts" translateConstructor :: Layout -> Constructor -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata, Sig) -translateConstructor layout (Constructor cid iface preconds _ _ upds _) bytecode = +translateConstructor layout (Constructor cid iface preconds _ _ upds) bytecode = (cid, [EVM.Success (snd calldata <> (fmap (toProp layout) $ preconds)) mempty (EVM.ConcreteBuf bytecode) (updatesToExpr layout cid upds initmap)], calldata, ifaceToSig iface) where @@ -163,10 +163,7 @@ ifaceToSig (Interface name args) = Sig (T.pack name) (fmap fromdecl args) translateBehv :: Layout -> BS.ByteString -> Behaviour -> EVM.Expr EVM.End translateBehv layout bytecode (Behaviour _ cid _ preconds caseconds _ upds ret) = - EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (rewritesToExpr layout cid upds bytecode) - -rewritesToExpr :: Layout -> Id -> [Rewrite] -> BS.ByteString -> ContractMap -rewritesToExpr layout cid rewrites bytecode = foldl (flip $ rewriteToExpr layout cid) initmap rewrites + EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (updatesToExpr layout cid upds initmap) where initcontract = EVM.C { EVM.code = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode) , EVM.storage = EVM.AbstractStore initAddr @@ -175,10 +172,6 @@ rewritesToExpr layout cid rewrites bytecode = foldl (flip $ rewriteToExpr layout } initmap = M.fromList [(initAddr, initcontract)] -rewriteToExpr :: Layout -> Id -> Rewrite -> ContractMap -> ContractMap -rewriteToExpr _ _ (Constant _) cmap = cmap -rewriteToExpr layout cid (Rewrite upd) cmap = updateToExpr layout cid upd cmap - updatesToExpr :: Layout -> Id -> [StorageUpdate] -> ContractMap -> ContractMap updatesToExpr layout cid upds initmap = foldl (flip $ updateToExpr layout cid) initmap upds diff --git a/src/K.hs b/src/K.hs deleted file mode 100644 index 56a6c8d3..00000000 --- a/src/K.hs +++ /dev/null @@ -1,313 +0,0 @@ -{-# LANGUAGE RecordWildCards #-} -{-# Language GADTs #-} -{-# Language OverloadedStrings #-} -{-# Language ScopedTypeVariables #-} -{-# Language TypeApplications #-} -{-# LANGUAGE ApplicativeDo #-} -{-# LANGUAGE OverloadedLists #-} - -module K where - -import Prelude hiding (GT, LT) - -import Syntax -import Syntax.Annotated hiding (SlotType(..)) - -import Error -import Data.Text (Text, pack, unpack) -import Data.List hiding (group) -import Data.Maybe -import qualified Data.Text as Text -import EVM.Types hiding (Expr(..)) - -import EVM.Solidity (SolcContract(..), StorageItem(..), SlotType(..)) -import Data.Map.Strict (Map) -- abandon in favor of [(a,b)]? -import qualified Data.Map.Strict as Map -- abandon in favor of [(a,b)]? - --- Transforms a RefinedSyntax.Behaviour --- to a k spec. - -type Err = Error String - -cell :: String -> String -> String -cell key value = "<" <> key <> "> " <> value <> " key <> "> \n" - -(|-) :: String -> String -> String -(|-) = cell - -infix 7 |- - -type KSpec = String - -getContractName :: Text -> String -getContractName = unpack . Text.concat . Data.List.tail . Text.splitOn ":" - -data KOptions = - KOptions { - gasExprs :: Map Id String, - storage :: Maybe String, - extractbin :: Bool - } - -makekSpec :: Map Text SolcContract -> KOptions -> Behaviour -> Err (String, String) -makekSpec sources _ behaviour = - let this = _contract behaviour - names = Map.fromList $ fmap (\(a, b) -> (getContractName a, b)) (Map.toList sources) - hasLayout = Map.foldr ((&&) . isJust . (\ SolcContract{..} -> storageLayout)) True sources - in - if hasLayout then do - thisSource <- validate - [(nowhere, unlines ["Bytecode not found for:", show this, "Sources available:", show $ Map.keys sources])] - (Map.lookup this) names - pure $ mkTerm thisSource names behaviour - - else throw (nowhere, "No storagelayout found") - -kCalldata :: Interface -> String -kCalldata (Interface a args) = - "#abiCallData(" - <> show a <> ", " - <> if null args then ".IntList" - else intercalate ", " (fmap (\(Decl typ varname) -> "#" <> show typ <> "(" <> kVar varname <> ")") args) - <> ")" - -kStorageName :: When -> TStorageItem a -> String -kStorageName t item = kVar (idFromItem item) <> "-" <> show t - <> intercalate "_" ("" : fmap kTypedExpr (ixsFromItem item)) - -kVar :: Id -> String -kVar a = (unpack . Text.toUpper . pack $ [head a]) <> tail a - -kAbiEncode :: Maybe TypedExp -> String -kAbiEncode Nothing = ".ByteArray" -kAbiEncode (Just (TExp SInteger a)) = "#enc(#uint256" <> kExpr a <> ")" -kAbiEncode (Just (TExp SBoolean _)) = ".ByteArray" -kAbiEncode (Just (TExp SByteStr _)) = ".ByteArray" -kAbiEncode (Just (TExp SContract _)) = error "contracts not supported" - -kTypedExpr :: TypedExp -> String -kTypedExpr (TExp SInteger a) = kExpr a -kTypedExpr (TExp SBoolean a) = kExpr a -kTypedExpr (TExp SByteStr _) = error "TODO: add support for TExp SByteStr to kExpr" -kTypedExpr (TExp SContract _) = error "contracts not supported" - -kExpr :: Exp a -> String --- integers -kExpr (Add _ a b) = "(" <> kExpr a <> " +Int " <> kExpr b <> ")" -kExpr (Sub _ a b) = "(" <> kExpr a <> " -Int " <> kExpr b <> ")" -kExpr (Mul _ a b) = "(" <> kExpr a <> " *Int " <> kExpr b <> ")" -kExpr (Div _ a b) = "(" <> kExpr a <> " /Int " <> kExpr b <> ")" -kExpr (Mod _ a b) = "(" <> kExpr a <> " modInt " <> kExpr b <> ")" -kExpr (Exp _ a b) = "(" <> kExpr a <> " ^Int " <> kExpr b <> ")" -kExpr (LitInt _ a) = show a -kExpr (IntMin p a) = kExpr $ LitInt p $ negate $ 2 ^ (a - 1) -kExpr (IntMax p a) = kExpr $ LitInt p $ 2 ^ (a - 1) - 1 -kExpr (UIntMin p _) = kExpr $ LitInt p 0 -kExpr (UIntMax p a) = kExpr $ LitInt p $ 2 ^ a - 1 -kExpr (IntEnv _ a) = show a - --- booleans -kExpr (And _ a b) = "(" <> kExpr a <> " andBool\n " <> kExpr b <> ")" -kExpr (Or _ a b) = "(" <> kExpr a <> " orBool " <> kExpr b <> ")" -kExpr (Impl _ a b) = "(" <> kExpr a <> " impliesBool " <> kExpr b <> ")" -kExpr (Neg _ a) = "notBool (" <> kExpr a <> ")" -kExpr (LT _ a b) = "(" <> kExpr a <> " kExpr b <> ")" -kExpr (LEQ _ a b) = "(" <> kExpr a <> " <=Int " <> kExpr b <> ")" -kExpr (GT _ a b) = "(" <> kExpr a <> " >Int " <> kExpr b <> ")" -kExpr (GEQ _ a b) = "(" <> kExpr a <> " >=Int " <> kExpr b <> ")" -kExpr (LitBool _ a) = show a -kExpr (NEq p t a b) = "notBool (" <> kExpr (Eq p t a b) <> ")" -kExpr (Eq _ t a b) = - let eqK typ = "(" <> kExpr a <> " ==" <> typ <> " " <> kExpr b <> ")" - in case t of - SInteger -> eqK "Int" - SBoolean -> eqK "Bool" - SByteStr -> eqK "K" - SContract -> error "contracts not supported" - --- bytestrings -kExpr (ByStr _ str) = show str -kExpr (ByLit _ bs) = show bs -kExpr (TEntry _ t item) = kStorageName t item -kExpr (Var _ _ _ a) = kVar a -kExpr v = error ("Internal error: TODO kExpr of " <> show v) ---kExpr (Cat a b) = ---kExpr (Slice a start end) = ---kExpr (ByEnv env) = - -fst' :: (a, b, c) -> a -fst' (x, _, _) = x - -snd' :: (a, b, c) -> b -snd' (_, y, _) = y - -trd' :: (a, b, c) -> c -trd' (_, _, z) = z - -kStorageEntry :: Map Text StorageItem -> Rewrite -> (String, (Int, String, String)) -kStorageEntry storageLayout update = - let (loc, offset) = kSlot update $ - fromMaybe - (error "Internal error: storageVar not found, please report this error") - (Map.lookup (pack (idFromRewrite update)) storageLayout) - in case update of - Rewrite (Update _ a b) -> (loc, (offset, kStorageName Pre a, kExpr b)) - Constant (Loc SInteger a) -> (loc, (offset, kStorageName Pre a, kStorageName Pre a)) - v -> error $ "Internal error: TODO kStorageEntry: " <> show v -- TODO should this really be separate? - ---packs entries packed in one slot -normalize :: Bool -> [(String, (Int, String, String))] -> String -normalize pass entries = foldr (\a acc -> case a of - (loc, [(_, pre, post)]) -> - loc <> " |-> (" <> pre - <> " => " <> (if pass then post else "_") <> ")\n" - <> acc - (loc, items) -> let (offsets, pres, posts) = unzip3 items - in loc <> " |-> ( #packWords(" - <> showSList (fmap show offsets) <> ", " - <> showSList pres <> ") " - <> " => " <> (if pass - then "#packWords(" - <> showSList (fmap show offsets) - <> ", " <> showSList posts <> ")" - else "_") - <> ")\n" - <> acc - ) - "\n" (group entries) - where group :: [(String, (Int, String, String))] -> [(String, [(Int, String, String)])] - group a = Map.toList (foldr (\(slot, (offset, pre, post)) acc -> Map.insertWith (<>) slot [(offset, pre, post)] acc) mempty a) - showSList :: [String] -> String - showSList = unwords - -kSlot :: Rewrite -> StorageItem -> (String, Int) -kSlot update StorageItem{..} = case slotType of - (StorageValue _) -> (show slot, offset) - (StorageMapping _ _) -> if null (ixsFromRewrite update) - then error $ "internal error: kSlot. Please report: " <> show update - else ( "#hashedLocation(\"Solidity\", " - <> show slot <> ", " <> unwords (kTypedExpr <$> ixsFromRewrite update) <> ")" - , offset ) - -kAccount :: Bool -> Id -> SolcContract -> [Rewrite] -> String -kAccount pass name SolcContract{..} updates = - "account" |- ("\n" - <> "acctID" |- kVar name - <> "balance" |- (kVar name <> "_balance") -- needs to be constrained to uint256 - <> "code" |- (kByteStack runtimeCode) - <> "storage" |- (normalize pass ( fmap (kStorageEntry (fromJust storageLayout)) updates) <> "\n.Map") - <> "origStorage" |- ".Map" -- need to be generalized once "kStorageEntry" is implemented - <> "nonce" |- "_" - ) - -kByteStack :: ByteString -> String -kByteStack bs = "#parseByteStack(\"" <> show (ByteStringS bs) <> "\")" - -defaultConditions :: String -> String -defaultConditions acct_id = - "#rangeAddress(" <> acct_id <> ")\n" <> - "andBool " <> acct_id <> " =/=Int 0\n" <> - "andBool " <> acct_id <> " >Int 9\n" <> - "andBool #rangeAddress( " <> show Caller <> ")\n" <> - "andBool #rangeAddress( " <> show Origin <> ")\n" <> - "andBool #rangeUInt(256, " <> show Timestamp <> ")\n" <> - -- "andBool #rangeUInt(256, ECREC_BAL)" <> - -- "andBool #rangeUInt(256, SHA256_BAL)" <> - -- "andBool #rangeUInt(256, RIP160_BAL)" <> - -- "andBool #rangeUInt(256, ID_BAL)" <> - -- "andBool #rangeUInt(256, MODEXP_BAL)" <> - -- "andBool #rangeUInt(256, ECADD_BAL)" <> - -- "andBool #rangeUInt(256, ECMUL_BAL)" <> - -- "andBool #rangeUInt(256, ECPAIRING_BAL)" <> - "andBool " <> show Calldepth <> " <=Int 1024\n" <> - "andBool #rangeUInt(256, " <> show Callvalue <> ")\n" <> - "andBool #rangeUInt(256, " <> show Chainid <> " )\n" - -indent :: Int -> String -> String -indent n text = unlines $ ((Data.List.replicate n ' ') <>) <$> (lines text) - -mkTerm :: SolcContract -> Map Id SolcContract -> Behaviour -> (String, String) -mkTerm SolcContract{..} accounts Behaviour{..} = (name, term) - where code = runtimeCode - pass = True - repl '_' = '.' - repl c = c - name = _contract <> "_" <> _name - term = "rule [" <> (fmap repl name) <> "]:\n" - <> "k" |- "#execute => #halt" - <> "exit-code" |- "1" - <> "mode" |- "NORMAL" - <> "schedule" |- "ISTANBUL" - <> "evm" |- indent 2 ("\n" - <> "output" |- kAbiEncode _returns - <> "statusCode" |- "EVMC_SUCCESS" - <> "callStack" |- "CallStack" - <> "interimStates" |- "_" - <> "touchedAccounts" |- "_" - <> "callState" |- indent 2 ("\n" - <> "program" |- kByteStack code - <> "jumpDests" |- ("#computeValidJumpDests(" <> kByteStack code <> ")") - <> "id" |- kVar _contract - <> "caller" |- (show Caller) - <> "callData" |- kCalldata _interface - <> "callValue" |- (show Callvalue) - -- the following are set to the values they have - -- at the beginning of a CALL. They can take a - -- more general value in "internal" specs. - <> "wordStack" |- ".WordStack => _" - <> "localMem" |- ".Map => _" - <> "pc" |- "0 => _" - <> "gas" |- "300000 => _" -- can be generalized in the future - <> "memoryUsed" |- "0 => _" - <> "callGas" |- "_ => _" - <> "static" |- "false" -- TODO: generalize - <> "callDepth" |- (show Calldepth) - ) - <> "substate" |- indent 2 ("\n" - <> "selfDestruct" |- "_ => _" - <> "log" |- "_ => _" --TODO: spec logs? - <> "refund" |- "_ => _" - ) - <> "gasPrice" |- "_" --could be environment var - <> "origin" |- show Origin - <> "blockhashes" |- "_" - <> "block" |- indent 2 ("\n" - <> "previousHash" |- "_" - <> "ommersHash" |- "_" - <> "coinbase" |- (show Coinbase) - <> "stateRoot" |- "_" - <> "transactionsRoot" |- "_" - <> "receiptsRoot" |- "_" - <> "logsBloom" |- "_" - <> "difficulty" |- (show Difficulty) - <> "number" |- (show Blocknumber) - <> "gasLimit" |- "_" - <> "gasUsed" |- "_" - <> "timestamp" |- (show Timestamp) - <> "extraData" |- "_" - <> "mixHash" |- "_" - <> "blockNonce" |- "_" - <> "ommerBlockHeaders" |- "_" - ) - ) - <> "network" |- indent 2 ("\n" - <> "activeAccounts" |- "_" - <> "accounts" |- indent 2 ("\n" <> (unpack $ - Text.unlines (flip fmap (contractFromRewrite <$> _stateUpdates) $ \a -> - pack $ - kAccount pass a - (fromMaybe - (error $ show a ++ " not found in accounts: " ++ show accounts) - $ Map.lookup a accounts - ) - (filter (\u -> contractFromRewrite u == a) _stateUpdates) - ))) - <> "txOrder" |- "_" - <> "txPending" |- "_" - <> "messages" |- "_" - ) - <> "\nrequires " - <> defaultConditions (kVar _contract) <> "\n andBool\n" - <> kExpr (mconcat _preconditions) - <> "\nensures " - <> kExpr (mconcat _postconditions) diff --git a/src/Print.hs b/src/Print.hs index 9b526967..e4dce6c7 100644 --- a/src/Print.hs +++ b/src/Print.hs @@ -31,10 +31,7 @@ prettyBehaviour (Behaviour name contract interface preconditions cases postcondi prettyCases p = header "case" >-< block (prettyExp <$> p) <> ":" prettyStorage [] = "" - prettyStorage s = header "storage" >-< block (prettyState <$> s) - - prettyState (Constant loc) = prettyLocation loc - prettyState (Rewrite rew) = prettyUpdate rew + prettyStorage s = header "storage" >-< block (prettyUpdate <$> s) prettyRet (Just ret) = header "returns" >-< " " <> prettyTypedExp ret prettyRet Nothing = "" diff --git a/src/SMT.hs b/src/SMT.hs index fd275b20..cec1cc6d 100644 --- a/src/SMT.hs +++ b/src/SMT.hs @@ -188,7 +188,7 @@ mkPostconditionQueriesBehv :: Behaviour -> [Query] mkPostconditionQueriesBehv behv@(Behaviour _ _ (Interface ifaceName decls) preconds caseconds postconds stateUpdates _) = mkQuery <$> postconds where -- declare vars - storage = concatMap (declareStorageLocation . locFromRewrite) stateUpdates + storage = concatMap (declareStorageLocation . locFromUpdate) stateUpdates args = declareArg ifaceName <$> decls envs = declareEthEnv <$> ethEnvFromBehaviour behv @@ -205,24 +205,22 @@ mkPostconditionQueriesBehv behv@(Behaviour _ _ (Interface ifaceName decls) preco mkQuery e = Postcondition (Behv behv) e (mksmt e) mkPostconditionQueriesConstr :: Constructor -> [Query] -mkPostconditionQueriesConstr constructor@(Constructor _ (Interface ifaceName decls) preconds postconds _ initialStorage stateUpdates) = mkQuery <$> postconds +mkPostconditionQueriesConstr constructor@(Constructor _ (Interface ifaceName decls) preconds postconds _ initialStorage) = mkQuery <$> postconds where -- declare vars localStorage = concatMap declareInitialStorage initialStorage - externalStorage = concatMap (declareStorageLocation . locFromRewrite) stateUpdates args = declareArg ifaceName <$> decls envs = declareEthEnv <$> ethEnvFromConstructor constructor -- constraints pres = mkAssert ifaceName <$> preconds - updates = encodeUpdate ifaceName <$> stateUpdates initialStorage' = encodeInitialStorage ifaceName <$> initialStorage mksmt e = SMTExp - { _storage = localStorage <> externalStorage + { _storage = localStorage , _calldata = args , _environment = envs - , _assertions = [mkAssert ifaceName . Neg nowhere $ e] <> pres <> updates <> initialStorage' + , _assertions = [mkAssert ifaceName . Neg nowhere $ e] <> pres <> initialStorage' } mkQuery e = Postcondition (Ctor constructor) e (mksmt e) @@ -253,25 +251,23 @@ mkInvariantQueries (Act _ contracts) = fmap mkQuery gathered getInvariants (Contract (c@Constructor{..}) behvs) = fmap (\i -> (i, c, behvs)) _invariants mkInit :: Invariant -> Constructor -> (Constructor, SMTExp) - mkInit (Invariant _ invConds _ (_,invPost)) ctor@(Constructor _ (Interface ifaceName decls) preconds _ _ initialStorage stateUpdates) = (ctor, smt) + mkInit (Invariant _ invConds _ (_,invPost)) ctor@(Constructor _ (Interface ifaceName decls) preconds _ _ initialStorage) = (ctor, smt) where -- declare vars localStorage = concatMap declareInitialStorage initialStorage - externalStorage = concatMap (declareStorageLocation . locFromRewrite) stateUpdates args = declareArg ifaceName <$> decls envs = declareEthEnv <$> ethEnvFromConstructor ctor -- constraints pres = mkAssert ifaceName <$> preconds <> invConds - updates = encodeUpdate ifaceName <$> stateUpdates initialStorage' = encodeInitialStorage ifaceName <$> initialStorage postInv = mkAssert ifaceName $ Neg nowhere invPost smt = SMTExp - { _storage = localStorage <> externalStorage + { _storage = localStorage , _calldata = args , _environment = envs - , _assertions = postInv : pres <> updates <> initialStorage' + , _assertions = postInv : pres <> initialStorage' } mkBehv :: Invariant -> Constructor -> Behaviour -> (Behaviour, SMTExp) @@ -281,21 +277,21 @@ mkInvariantQueries (Act _ contracts) = fmap mkQuery gathered (Interface ctorIface ctorDecls) = _cinterface ctor (Interface behvIface behvDecls) = _interface behv -- storage locs mentioned in the invariant but not in the behaviour - implicitLocs = Constant <$> (locsFromExp invPre \\ (locFromRewrite <$> _stateUpdates behv)) + implicitLocs = (locsFromExp invPre \\ (locFromUpdate <$> _stateUpdates behv)) -- declare vars invEnv = declareEthEnv <$> ethEnvFromExp invPre behvEnv = declareEthEnv <$> ethEnvFromBehaviour behv initArgs = declareArg ctorIface <$> ctorDecls behvArgs = declareArg behvIface <$> behvDecls - storage = concatMap (declareStorageLocation . locFromRewrite) (_stateUpdates behv <> implicitLocs) + storage = concatMap declareStorageLocation ((locFromUpdate <$> _stateUpdates behv) <> implicitLocs) -- constraints preInv = mkAssert ctorIface $ invPre postInv = mkAssert ctorIface . Neg nowhere $ invPost behvConds = mkAssert behvIface <$> _preconditions behv <> _caseconditions behv invConds' = mkAssert ctorIface <$> invConds <> invStorageBounds - implicitLocs' = encodeUpdate ctorIface <$> implicitLocs + implicitLocs' = encodeStorageLocation <$> implicitLocs updates = encodeUpdate behvIface <$> _stateUpdates behv smt = SMTExp @@ -529,6 +525,7 @@ parseSMTModel s = if length s0Caps == 1 -- | encodes a storage update from a constructor creates block as an smt assertion +-- TODO unify with encodeUpdate encodeInitialStorage :: Id -> StorageUpdate -> SMT2 encodeInitialStorage behvName (Update _ item expr) = let @@ -536,6 +533,8 @@ encodeInitialStorage behvName (Update _ item expr) = expression = withInterface behvName $ expToSMT2 expr in "(assert (= " <> postentry <> " " <> expression <> "))" +encodeStorageLocation :: StorageLocation -> SMT2 +encodeStorageLocation loc = "(assert (= " <> nameFromLoc Pre loc <> " " <> nameFromLoc Post loc <> "))" -- | declares a storage location with the given timing declareStorage :: [When] -> StorageLocation -> [SMT2] @@ -552,9 +551,8 @@ declareInitialStorage :: StorageUpdate -> [SMT2] declareInitialStorage upd = declareStorage [Post] (locFromUpdate upd) -- | encodes a storage update rewrite as an smt assertion -encodeUpdate :: Id -> Rewrite -> SMT2 -encodeUpdate _ (Constant loc) = "(assert (= " <> nameFromLoc Pre loc <> " " <> nameFromLoc Post loc <> "))" -encodeUpdate behvName (Rewrite update) = encodeInitialStorage behvName update +encodeUpdate :: Id -> StorageUpdate -> SMT2 +encodeUpdate behvName update = encodeInitialStorage behvName update -- | declares a storage location that exists both in the pre state and the post -- state (i.e. anything except a loc created by a constructor claim) diff --git a/src/Syntax.hs b/src/Syntax.hs index 76f48789..152c10ab 100644 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -18,7 +18,7 @@ import Data.Map (Map,empty,insertWith,unionsWith,unionWith,singleton) import Syntax.TimeAgnostic as Agnostic import qualified Syntax.Annotated as Annotated import qualified Syntax.Typed as Typed -import Syntax.Untyped hiding (Rewrite,Contract) +import Syntax.Untyped hiding (Contract) import qualified Syntax.Untyped as Untyped ----------------------------------------- @@ -34,16 +34,15 @@ locsFromBehaviour (Behaviour _ _ _ preconds cases postconds rewrites returns) = concatMap locsFromExp preconds <> concatMap locsFromExp cases <> concatMap locsFromExp postconds - <> concatMap locsFromRewrite rewrites + <> concatMap locsFromUpdate rewrites <> maybe [] locsFromTypedExp returns locsFromConstructor :: Annotated.Constructor -> [Annotated.StorageLocation] -locsFromConstructor (Constructor _ _ pre post inv initialStorage rewrites) = nub $ +locsFromConstructor (Constructor _ _ pre post inv initialStorage) = nub $ concatMap locsFromExp pre <> concatMap locsFromExp post <> concatMap locsFromInvariant inv - <> concatMap locsFromRewrite rewrites - <> concatMap locsFromRewrite (Rewrite <$> initialStorage) + <> concatMap locsFromUpdate initialStorage locsFromInvariant :: Annotated.Invariant -> [Annotated.StorageLocation] locsFromInvariant (Invariant _ pre bounds (predpre, predpost)) = @@ -63,19 +62,15 @@ behvsFromContracts contracts = concatMap (\(Contract _ b) -> b) contracts constrFromContracts :: [Contract t] -> [Constructor t] constrFromContracts contracts = fmap (\(Contract c _) -> c) contracts -locsFromRewrite :: Rewrite t -> [StorageLocation t] -locsFromRewrite update = nub $ case update of - Constant loc -> [loc] - Rewrite (Update _ item e) -> locsFromItem item <> locsFromExp e - -locFromRewrite :: Rewrite t -> StorageLocation t -locFromRewrite = onRewrite id locFromUpdate +locsFromUpdate :: StorageUpdate t -> [StorageLocation t] +locsFromUpdate update = nub $ case update of + (Update _ item e) -> locsFromItem item <> locsFromExp e locFromUpdate :: StorageUpdate t -> StorageLocation t locFromUpdate (Update _ item _) = _Loc item locsFromItem :: TStorageItem a t -> [StorageLocation t] -locsFromItem item = _Loc item : concatMap locsFromTypedExp (ixsFromItem item) +locsFromItem item = _Loc item : concatMap locsFromTypedExp (ixsFromItem item) locsFromTypedExp :: TypedExp t -> [StorageLocation t] locsFromTypedExp (TExp _ e) = locsFromExp e @@ -159,7 +154,7 @@ createsFromExp = nub . go Var {} -> [] createsFromItem :: TStorageItem a t -> [Id] -createsFromItem item = concatMap createsFromTypedExp (ixsFromItem item) +createsFromItem item = concatMap createsFromTypedExp (ixsFromItem item) createsFromTypedExp :: TypedExp t -> [Id] createsFromTypedExp (TExp _ e) = createsFromExp e @@ -168,28 +163,26 @@ createsFromContract :: Typed.Contract -> [Id] createsFromContract (Contract constr behvs) = createsFromConstructor constr <> concatMap createsFromBehaviour behvs -createsFromConstructor :: Typed.Constructor -> [Id] -createsFromConstructor (Constructor _ _ pre post inv initialStorage rewrites) = nub $ +createsFromConstructor :: Typed.Constructor -> [Id] +createsFromConstructor (Constructor _ _ pre post inv initialStorage) = nub $ concatMap createsFromExp pre <> concatMap createsFromExp post <> concatMap createsFromInvariant inv - <> concatMap createsFromRewrite rewrites - <> concatMap createsFromRewrite (Rewrite <$> initialStorage) + <> concatMap createsFromUpdate initialStorage createsFromInvariant :: Typed.Invariant -> [Id] createsFromInvariant (Invariant _ pre bounds ipred) = concatMap createsFromExp pre <> concatMap createsFromExp bounds <> createsFromExp ipred -createsFromRewrite :: Rewrite t ->[Id] -createsFromRewrite update = nub $ case update of - Constant _ -> [] - Rewrite (Update _ item e) -> createsFromItem item <> createsFromExp e +createsFromUpdate :: StorageUpdate t ->[Id] +createsFromUpdate update = nub $ case update of + Update _ item e -> createsFromItem item <> createsFromExp e createsFromBehaviour :: Behaviour t -> [Id] createsFromBehaviour (Behaviour _ _ _ _ preconds postconds rewrites returns) = nub $ concatMap createsFromExp preconds <> concatMap createsFromExp postconds - <> concatMap createsFromRewrite rewrites + <> concatMap createsFromUpdate rewrites <> maybe [] createsFromTypedExp returns ethEnvFromBehaviour :: Behaviour t -> [EthEnv] @@ -197,26 +190,24 @@ ethEnvFromBehaviour (Behaviour _ _ _ preconds cases postconds rewrites returns) concatMap ethEnvFromExp preconds <> concatMap ethEnvFromExp cases <> concatMap ethEnvFromExp postconds - <> concatMap ethEnvFromRewrite rewrites + <> concatMap ethEnvFromUpdate rewrites <> maybe [] ethEnvFromTypedExp returns ethEnvFromConstructor :: Annotated.Constructor -> [EthEnv] -ethEnvFromConstructor (Constructor _ _ pre post inv initialStorage rewrites) = nub $ +ethEnvFromConstructor (Constructor _ _ pre post inv initialStorage) = nub $ concatMap ethEnvFromExp pre <> concatMap ethEnvFromExp post <> concatMap ethEnvFromInvariant inv - <> concatMap ethEnvFromRewrite rewrites - <> concatMap ethEnvFromRewrite (Rewrite <$> initialStorage) + <> concatMap ethEnvFromUpdate initialStorage ethEnvFromInvariant :: Annotated.Invariant -> [EthEnv] ethEnvFromInvariant (Invariant _ pre bounds (predpre, predpost)) = concatMap ethEnvFromExp pre <> concatMap ethEnvFromExp bounds <> ethEnvFromExp predpre <> ethEnvFromExp predpost -ethEnvFromRewrite :: Rewrite t -> [EthEnv] -ethEnvFromRewrite rewrite = case rewrite of - Constant (Loc _ item) -> ethEnvFromItem item - Rewrite (Update _ item e) -> nub $ ethEnvFromItem item <> ethEnvFromExp e +ethEnvFromUpdate :: StorageUpdate t -> [EthEnv] +ethEnvFromUpdate rewrite = case rewrite of + Update _ item e -> nub $ ethEnvFromItem item <> ethEnvFromExp e ethEnvFromItem :: TStorageItem a t -> [EthEnv] ethEnvFromItem = nub . concatMap ethEnvFromTypedExp . ixsFromItem @@ -263,9 +254,6 @@ ethEnvFromExp = nub . go TEntry _ _ a -> ethEnvFromItem a Var {} -> [] -idFromRewrite :: Rewrite t -> Id -idFromRewrite = onRewrite idFromLocation idFromUpdate - idFromItem :: TStorageItem a t -> Id idFromItem (Item _ _ ref) = idFromStorageRef ref @@ -280,9 +268,6 @@ idFromUpdate (Update _ item _) = idFromItem item idFromLocation :: StorageLocation t -> Id idFromLocation (Loc _ item) = idFromItem item -contractFromRewrite :: Rewrite t -> Id -contractFromRewrite = onRewrite contractFromLoc contractFromUpdate - contractFromItem :: TStorageItem a t -> Id contractFromItem (Item _ _ ref) = contractFromStorageRef ref @@ -296,7 +281,7 @@ ixsFromItem (Item _ _ (SMapping _ _ ixs)) = ixs ixsFromItem _ = [] contractsInvolved :: Behaviour t -> [Id] -contractsInvolved = fmap contractFromRewrite . _stateUpdates +contractsInvolved = fmap contractFromUpdate . _stateUpdates contractFromLoc :: StorageLocation t -> Id contractFromLoc (Loc _ item) = contractFromItem item @@ -310,25 +295,12 @@ ixsFromLocation (Loc _ item) = ixsFromItem item ixsFromUpdate :: StorageUpdate t -> [TypedExp t] ixsFromUpdate (Update _ item _) = ixsFromItem item -ixsFromRewrite :: Rewrite t -> [TypedExp t] -ixsFromRewrite = onRewrite ixsFromLocation ixsFromUpdate - itemType :: TStorageItem a t -> ActType itemType (Item t _ _) = actType t isMapping :: StorageLocation t -> Bool isMapping = not . null . ixsFromLocation -onRewrite :: (StorageLocation t -> a) -> (StorageUpdate t -> a) -> Rewrite t -> a -onRewrite f _ (Constant a) = f a -onRewrite _ g (Rewrite a) = g a - -updatesFromRewrites :: [Rewrite t] -> [StorageUpdate t] -updatesFromRewrites rs = [u | Rewrite u <- rs] - -locsFromRewrites :: [Rewrite t] -> [StorageLocation t] -locsFromRewrites rs = [l | Constant l <- rs] - -------------------------------------- -- * Extraction from untyped ASTs * -- -------------------------------------- @@ -434,7 +406,7 @@ idFromRewrites e = case e of idFromEntry (EVar p x) = singleton x [p] idFromEntry (EMapping _ en xs) = unionWith (<>) (idFromEntry en) (idFromRewrites' xs) idFromEntry (EField _ en _) = idFromEntry en - + -- | True iff the case is a wildcard. isWild :: Case -> Bool isWild (Case _ (WildExp _) _) = True diff --git a/src/Syntax/Annotated.hs b/src/Syntax/Annotated.hs index da93016f..d32fc57e 100644 --- a/src/Syntax/Annotated.hs +++ b/src/Syntax/Annotated.hs @@ -13,8 +13,8 @@ import qualified Syntax.TimeAgnostic as Agnostic import Syntax.TimeAgnostic (Timing(..),setPre,setPost) -- Reexports -import Syntax.TimeAgnostic as Syntax.Annotated hiding (Timing(..),Timable(..),Time,Neither,Act,Contract,Invariant,InvariantPred,Constructor,Behaviour,Rewrite,StorageUpdate,StorageLocation,TStorageItem,Exp,TypedExp,StorageRef) -import Syntax.TimeAgnostic as Syntax.Annotated (pattern Act, pattern Contract, pattern Invariant, pattern Constructor, pattern Behaviour, pattern Rewrite, pattern Exp) +import Syntax.TimeAgnostic as Syntax.Annotated hiding (Timing(..),Timable(..),Time,Neither,Act,Contract,Invariant,InvariantPred,Constructor,Behaviour,StorageUpdate,StorageLocation,TStorageItem,Exp,TypedExp,StorageRef) +import Syntax.TimeAgnostic as Syntax.Annotated (pattern Act, pattern Contract, pattern Invariant, pattern Constructor, pattern Behaviour, pattern Exp) -- We shadow all timing-agnostic AST types with explicitly timed versions. @@ -24,7 +24,6 @@ type Invariant = Agnostic.Invariant Timed type InvariantPred = Agnostic.InvariantPred Timed type Constructor = Agnostic.Constructor Timed type Behaviour = Agnostic.Behaviour Timed -type Rewrite = Agnostic.Rewrite Timed type StorageUpdate = Agnostic.StorageUpdate Timed type StorageLocation = Agnostic.StorageLocation Timed type StorageRef = Agnostic.StorageRef Timed @@ -53,7 +52,6 @@ instance Annotatable Agnostic.Constructor where annotate ctor@Constructor{..} = ctor { _cpreconditions = setPre <$> _cpreconditions , _initialStorage = annotate <$> _initialStorage - , _cstateUpdates = annotate <$> _cstateUpdates , _invariants = annotate <$> _invariants } @@ -64,9 +62,5 @@ instance Annotatable Agnostic.Behaviour where , _stateUpdates = annotate <$> _stateUpdates } -instance Annotatable Agnostic.Rewrite where - annotate (Constant location) = Constant $ setPre location - annotate (Rewrite update) = Rewrite $ annotate update - instance Annotatable Agnostic.StorageUpdate where annotate (Update typ item expr) = Update typ (setPost item) (setPre expr) diff --git a/src/Syntax/TimeAgnostic.hs b/src/Syntax/TimeAgnostic.hs index 7204a001..c5749bb6 100644 --- a/src/Syntax/TimeAgnostic.hs +++ b/src/Syntax/TimeAgnostic.hs @@ -101,7 +101,6 @@ data Constructor t = Constructor , _cpostconditions :: [Exp ABoolean Timed] , _invariants :: [Invariant t] , _initialStorage :: [StorageUpdate t] - , _cstateUpdates :: [Rewrite t] } deriving instance Show (InvariantPred t) => Show (Constructor t) deriving instance Eq (InvariantPred t) => Eq (Constructor t) @@ -114,15 +113,10 @@ data Behaviour t = Behaviour , _preconditions :: [Exp ABoolean t] -- if preconditions are not satisfied execution is reverted , _caseconditions :: [Exp ABoolean t] -- if preconditions are satisfied and a case condition is not, some other instance of the bahaviour should apply , _postconditions :: [Exp ABoolean Timed] - , _stateUpdates :: [Rewrite t] + , _stateUpdates :: [StorageUpdate t] , _returns :: Maybe (TypedExp Timed) } deriving (Show, Eq) -data Rewrite t - = Constant (StorageLocation t) - | Rewrite (StorageUpdate t) - deriving (Show, Eq) - data StorageUpdate (t :: Timing) where Update :: SType a -> TStorageItem a t -> Exp a t -> StorageUpdate t deriving instance Show (StorageUpdate t) @@ -425,10 +419,6 @@ invariantJSON Invariant{..} predicate = object [ "kind" .= String "Invariant" , "storagebounds" .= toJSON _istoragebounds , "contract" .= _icontract ] -instance ToJSON (Rewrite t) where - toJSON (Constant a) = object [ "constant" .= toJSON a ] - toJSON (Rewrite a) = object [ "rewrite" .= toJSON a ] - instance ToJSON (StorageLocation t) where toJSON (Loc _ a) = object [ "location" .= toJSON a ] diff --git a/src/Syntax/Typed.hs b/src/Syntax/Typed.hs index 7438a2e9..f79d38aa 100644 --- a/src/Syntax/Typed.hs +++ b/src/Syntax/Typed.hs @@ -10,8 +10,8 @@ module Syntax.Typed (module Syntax.Typed) where import qualified Syntax.TimeAgnostic as Agnostic -- Reexports -import Syntax.TimeAgnostic as Syntax.Typed hiding (Act,Contract,Invariant,InvariantPred,Constructor,Behaviour,Rewrite,StorageUpdate,StorageLocation) -import Syntax.TimeAgnostic as Syntax.Typed (pattern Act, pattern Contract, pattern Invariant, pattern Constructor, pattern Behaviour, pattern Rewrite) +import Syntax.TimeAgnostic as Syntax.Typed hiding (Act,Contract,Invariant,InvariantPred,Constructor,Behaviour,StorageUpdate,StorageLocation) +import Syntax.TimeAgnostic as Syntax.Typed (pattern Act, pattern Contract, pattern Invariant, pattern Constructor, pattern Behaviour) -- We shadow all timing-agnostic AST types with versions -- that need to have implicit timings where possible. @@ -20,6 +20,5 @@ type Contract = Agnostic.Contract Untimed type Invariant = Agnostic.Invariant Untimed type Constructor = Agnostic.Constructor Untimed type Behaviour = Agnostic.Behaviour Untimed -type Rewrite = Agnostic.Rewrite Untimed type StorageUpdate = Agnostic.StorageUpdate Untimed type StorageLocation = Agnostic.StorageLocation Untimed diff --git a/src/Type.hs b/src/Type.hs index 5a9c162d..778a6adc 100644 --- a/src/Type.hs +++ b/src/Type.hs @@ -128,7 +128,7 @@ topologicalSort (Act store contracts) = -- map a contract name to the list of contracts that it calls and its code findCreates :: Contract -> (Id, ([Id], Contract)) - findCreates c@(Contract (Constructor cname _ _ _ _ _ _) _) = (cname, (createsFromContract c, c)) + findCreates c@(Contract (Constructor cname _ _ _ _ _) _) = (cname, (createsFromContract c, c)) --- Finds storage declarations from constructors lookupVars :: [U.Contract] -> Store @@ -244,7 +244,7 @@ checkTransition env (U.Transition _ name contract iface@(Interface _ decls) iffs -- TODO ensure non-overlapping and exhaustiveness (maybe with elaboration and mandatory wildcard?) -- | split case into pass and fail case - makeBehv :: [Exp ABoolean Untimed] -> [Exp ABoolean Timed] -> ([Exp ABoolean Untimed], [Rewrite], Maybe (TypedExp Timed)) -> Behaviour + makeBehv :: [Exp ABoolean Untimed] -> [Exp ABoolean Timed] -> ([Exp ABoolean Untimed], [StorageUpdate], Maybe (TypedExp Timed)) -> Behaviour makeBehv iffs' postcs (if',storage,ret) = Behaviour name contract iface iffs' if' postcs storage ret checkDefinition :: Env -> U.Definition -> Err Constructor @@ -255,7 +255,7 @@ checkDefinition env (U.Definition _ contract (Interface _ decls) iffs (U.Creates _ <- traverse (validStorage env') assigns ensures <- traverse (checkExpr env' SBoolean) postcs invs' <- fmap (Invariant contract [] []) <$> traverse (checkExpr env' SBoolean) invs - pure $ Constructor contract (Interface contract decls) iffs' ensures invs' stateUpdates [] + pure $ Constructor contract (Interface contract decls) iffs' ensures invs' stateUpdates where env' = addCalldata env decls @@ -282,7 +282,7 @@ validSlotType env p (StorageValue t) = validType env p t -- | Typechecks a case, returning typed versions of its preconditions, rewrites and return value. -checkCase :: Env -> U.Case -> Err ([Exp ABoolean Untimed], [Rewrite], Maybe (TypedExp Timed)) +checkCase :: Env -> U.Case -> Err ([Exp ABoolean Untimed], [StorageUpdate], Maybe (TypedExp Timed)) checkCase env c@(U.Case _ pre post) = do -- TODO isWild checks for WildExp, but WildExp is never generated if' <- traverse (checkExpr env SBoolean) $ if isWild c then [U.BoolLit nowhere True] else [pre] @@ -319,15 +319,15 @@ checkDefn pn env@Env{contract} keyType vt@(FromVType valType) name (U.Defn k val <*> checkExpr env valType val -- | Typechecks a postcondition, returning typed versions of its storage updates and return expression. -checkPost :: Env -> U.Post -> Err ([Rewrite], Maybe (TypedExp Timed)) +checkPost :: Env -> U.Post -> Err ([StorageUpdate], Maybe (TypedExp Timed)) checkPost env@Env{contract,theirs} (U.Post storage maybeReturn) = do returnexp <- traverse (typedExp $ focus contract) maybeReturn storage' <- checkEntries contract storage pure (storage', returnexp) where - checkEntries :: Id -> [U.Storage] -> Err [Rewrite] + checkEntries :: Id -> [U.Storage] -> Err [StorageUpdate] checkEntries name entries = for entries $ \case - U.Rewrite loc val -> Rewrite <$> checkStorageExpr (focus name) loc val + U.Rewrite loc val -> checkStorageExpr (focus name) loc val focus :: Id -> Env focus name = env diff --git a/src/act.cabal b/src/act.cabal index 39625cd4..abb1a958 100644 --- a/src/act.cabal +++ b/src/act.cabal @@ -44,7 +44,7 @@ library hs-source-dirs: . default-language: Haskell2010 exposed-modules: CLI Error Print SMT Syntax.Annotated Syntax.TimeAgnostic - other-modules: Lex Parse K Coq Syntax Syntax.Untyped Syntax.Typed Syntax.Types Syntax.Timing Type Enrich Dev HEVM Consistency + other-modules: Lex Parse Coq Syntax Syntax.Untyped Syntax.Typed Syntax.Types Syntax.Timing Type Enrich Dev HEVM Consistency executable act import: deps