diff --git a/WORKSPACE b/WORKSPACE index aacc5532ea1b..53fa3d843623 100644 --- a/WORKSPACE +++ b/WORKSPACE @@ -896,6 +896,15 @@ nixpkgs_package( repositories = dev_env_nix_repos, ) +nixpkgs_package( + name = "z3_nix", + attribute_path = "z3", + fail_not_supported = False, + nix_file = "//nix:bazel.nix", + nix_file_deps = common_nix_file_deps, + repositories = dev_env_nix_repos, +) if not is_windows else None + dev_env_tool( name = "postgresql_dev_env", nix_include = [ diff --git a/bazel-haskell-deps.bzl b/bazel-haskell-deps.bzl index 7e5f6637b04a..7a1480c8e947 100644 --- a/bazel-haskell-deps.bzl +++ b/bazel-haskell-deps.bzl @@ -640,6 +640,7 @@ exports_files(["stack.exe"], visibility = ["//visibility:public"]) "semigroups", "semver", "silently", + "simple-smt", "sorted-list", "split", "stache", diff --git a/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Numeric.hs b/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Numeric.hs index 4b5dad234948..23293e2327a0 100644 --- a/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Numeric.hs +++ b/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Numeric.hs @@ -3,7 +3,7 @@ -- | DAML-LF Numeric literals, with scale attached. module DA.Daml.LF.Ast.Numeric - ( Numeric + ( Numeric (..) , NumericError (..) , E10 , numeric diff --git a/compiler/daml-lf-verify/BUILD.bazel b/compiler/daml-lf-verify/BUILD.bazel new file mode 100644 index 000000000000..f666e1a56627 --- /dev/null +++ b/compiler/daml-lf-verify/BUILD.bazel @@ -0,0 +1,131 @@ +# Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +load("//rules_daml:daml.bzl", "daml_compile") +load("//bazel_tools:haskell.bzl", "da_haskell_binary", "da_haskell_library", "da_haskell_test") +load("@os_info//:os_info.bzl", "is_windows") + +da_haskell_binary( + name = "daml-lf-verify", + srcs = glob(["src/**/*.hs"]), + data = [ + "@z3_nix//:bin/z3", + ] if not is_windows else [], + hackage_deps = [ + "aeson", + "base", + "bytestring", + "containers", + "deepseq", + "Decimal", + "extra", + "filepath", + "ghc-lib-parser", + "hashable", + "lens", + "mtl", + "optparse-applicative", + "prettyprinter", + "recursion-schemes", + "safe", + "scientific", + "simple-smt", + "template-haskell", + "text", + "time", + "unordered-containers", + "zip-archive", + ], + main_function = "DA.Daml.LF.Verify.main", + src_strip_prefix = "src", + visibility = ["//visibility:public"], + deps = [ + "//compiler/daml-lf-ast", + "//compiler/daml-lf-proto", + "//compiler/daml-lf-reader", + "//compiler/daml-lf-tools", + "//libs-haskell/bazel-runfiles", + "//libs-haskell/da-hs-base", + ], +) + +da_haskell_library( + name = "daml-lf-verify-lib", + srcs = glob(["src/**/*.hs"]), + data = [ + "@z3_nix//:bin/z3", + ] if not is_windows else [], + hackage_deps = [ + "aeson", + "base", + "bytestring", + "containers", + "deepseq", + "Decimal", + "extra", + "filepath", + "ghc-lib-parser", + "hashable", + "lens", + "mtl", + "optparse-applicative", + "prettyprinter", + "recursion-schemes", + "safe", + "scientific", + "simple-smt", + "template-haskell", + "text", + "time", + "unordered-containers", + "zip-archive", + ], + src_strip_prefix = "src", + visibility = ["//visibility:public"], + deps = [ + "//compiler/daml-lf-ast", + "//compiler/daml-lf-proto", + "//compiler/daml-lf-reader", + "//compiler/daml-lf-tools", + "//libs-haskell/bazel-runfiles", + "//libs-haskell/da-hs-base", + ], +) + +daml_compile( + name = "quickstart", + srcs = glob(["daml/quickstart/**/*.daml"]), + version = "1.0.0", +) + +daml_compile( + name = "conditionals", + srcs = glob(["daml/conditionals/**/*.daml"]), + version = "1.0.0", +) + +da_haskell_test( + name = "verify-tests", + srcs = glob(["tests/**/*.hs"]), + data = [ + ":conditionals.dar", + ":quickstart.dar", + ] if not is_windows else [], + hackage_deps = [ + "base", + "containers", + "filepath", + "tasty", + "tasty-hunit", + ], + main_function = "DA.Daml.LF.Verify.Tests.mainTest", + src_strip_prefix = "tests", + visibility = ["//visibility:public"], + deps = [ + ":daml-lf-verify-lib", + "//compiler/daml-lf-ast", + "//libs-haskell/bazel-runfiles", + "//libs-haskell/da-hs-base", + "//libs-haskell/test-utils", + ], +) if not is_windows else None diff --git a/compiler/daml-lf-verify/daml/conditionals/daml/Iou.daml b/compiler/daml-lf-verify/daml/conditionals/daml/Iou.daml new file mode 100644 index 000000000000..ddaa16544748 --- /dev/null +++ b/compiler/daml-lf-verify/daml/conditionals/daml/Iou.daml @@ -0,0 +1,61 @@ +-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + + +module Iou where + +template Iou with + owner: Party + content: Int + where + signatory owner + + choice SuccA: ContractId Iou + controller owner + do + if False + then create Iou with owner; content = content + else create Iou with owner; content = content + + choice SuccB: ContractId Iou + controller owner + do + if 1 == 1 + then create Iou with owner; content = content + else create Iou with owner; content = 0 + + choice SuccC: ContractId Iou + controller owner + do + if True + then do + _ <- create Iou with owner; content = content + create Iou with owner; content = 0 + else create Iou with owner; content = content + + choice SuccD: ContractId Iou + controller owner + do + if True + then do + cid1 <- create Iou with owner; content = content + archive cid1 + create Iou with owner; content = content + else create Iou with owner; content = content + + choice FailA: ContractId Iou + controller owner + do + if 1 == 1 + then create Iou with owner; content = 0 + else create Iou with owner; content = content + + choice FailB: ContractId Iou + controller owner + do + if False + then create Iou with owner; content = content + else do + _ <- create Iou with owner; content = content + create Iou with owner; content = content + diff --git a/compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml b/compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml new file mode 100644 index 000000000000..9bde3b1c5c69 --- /dev/null +++ b/compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml @@ -0,0 +1,86 @@ +-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + + +module Iou where + +type IouCid = ContractId Iou + +template Iou + with + issuer : Party + owner : Party + currency : Text + amount : Decimal + observers : [Party] + where + ensure amount > 0.0 + + signatory issuer, owner + + observer observers + + controller owner can + + -- Split the IOU by dividing the amount. + Iou_Split : (IouCid, IouCid) + with + splitAmount: Decimal + do + let restAmount = amount - splitAmount + splitCid <- create this with amount = splitAmount + restCid <- create this with amount = restAmount + return (splitCid, restCid) + + -- Merge two IOUs by aggregating their amounts. + Iou_Merge : IouCid + with + otherCid: IouCid + do + otherIou <- fetch otherCid + -- Check the two IOU's are compatible + assert ( + currency == otherIou.currency && + owner == otherIou.owner && + issuer == otherIou.issuer + ) + -- Retire the old Iou + archive otherCid + -- Return the merged Iou + create this with amount = amount + otherIou.amount + + Iou_Transfer : ContractId IouTransfer + with + newOwner : Party + do create IouTransfer with iou = this; newOwner + + Iou_AddObserver : IouCid + with + newObserver : Party + do create this with observers = newObserver :: observers + + Iou_RemoveObserver : IouCid + with + oldObserver : Party + do create this with observers = filter (/= oldObserver) observers + +template IouTransfer + with + iou : Iou + newOwner : Party + where + signatory iou.issuer, iou.owner + + controller iou.owner can + IouTransfer_Cancel : IouCid + do create iou + + controller newOwner can + IouTransfer_Reject : IouCid + do create iou + + IouTransfer_Accept : IouCid + do + create iou with + owner = newOwner + observers = [] diff --git a/compiler/daml-lf-verify/daml/quickstart/daml/IouTrade.daml b/compiler/daml-lf-verify/daml/quickstart/daml/IouTrade.daml new file mode 100644 index 000000000000..55acac3131d1 --- /dev/null +++ b/compiler/daml-lf-verify/daml/quickstart/daml/IouTrade.daml @@ -0,0 +1,49 @@ +-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + + +module IouTrade where + +import DA.Assert + +import Iou + +template IouTrade + with + buyer : Party + seller : Party + baseIouCid : IouCid + baseIssuer : Party + baseCurrency : Text + baseAmount : Decimal + quoteIssuer : Party + quoteCurrency : Text + quoteAmount : Decimal + where + signatory buyer + + controller seller can + IouTrade_Accept : (IouCid, IouCid) + with + quoteIouCid : IouCid + do + baseIou <- fetch baseIouCid + baseIssuer === baseIou.issuer + baseCurrency === baseIou.currency + baseAmount === baseIou.amount + buyer === baseIou.owner + quoteIou <- fetch quoteIouCid + quoteIssuer === quoteIou.issuer + quoteCurrency === quoteIou.currency + quoteAmount === quoteIou.amount + seller === quoteIou.owner + quoteIouTransferCid <- exercise quoteIouCid Iou_Transfer with + newOwner = buyer + transferredQuoteIouCid <- exercise quoteIouTransferCid IouTransfer_Accept + baseIouTransferCid <- exercise baseIouCid Iou_Transfer with + newOwner = seller + transferredBaseIouCid <- exercise baseIouTransferCid IouTransfer_Accept + return (transferredQuoteIouCid, transferredBaseIouCid) + + TradeProposal_Reject : () + do return () diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs new file mode 100644 index 000000000000..dc3be2772951 --- /dev/null +++ b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs @@ -0,0 +1,140 @@ +-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + +{-# LANGUAGE DataKinds #-} + +-- | Static verification of DAML packages. +module DA.Daml.LF.Verify + ( main + , verify + ) where + +import Data.Maybe +import qualified Data.NameMap as NM +import qualified Data.Text as T +import Data.Text.Prettyprint.Doc +import Data.Text.Prettyprint.Doc.Render.String +import Options.Applicative +import System.Exit +import System.IO + +import DA.Daml.LF.Ast.Base +import DA.Daml.LF.Verify.Generate +import DA.Daml.LF.Verify.Solve +import DA.Daml.LF.Verify.Read +import DA.Daml.LF.Verify.Context +import DA.Bazel.Runfiles + +getSolver :: IO FilePath +getSolver = locateRunfiles "z3_nix/bin/z3" + +main :: IO () +main = do + Options{..} <- execParser optionsParserInfo + let choiceTmpl = TypeConName [T.pack optChoiceTmpl] + choiceName = ChoiceName (T.pack optChoiceName) + fieldTmpl = TypeConName [T.pack optFieldTmpl] + fieldName = FieldName (T.pack optFieldName) + result <- verify optInputDar putStrLn choiceTmpl choiceName fieldTmpl fieldName + print result + +outputError :: Error + -- ^ The error message. + -> String + -- ^ An additional message providing context. + -> IO a +outputError err msg = do + hPutStrLn stderr msg + hPrint stderr err + exitFailure + +-- | Execute the full verification pipeline. +verify :: FilePath + -- ^ The DAR file to load. + -> (String -> IO ()) + -- ^ Function for debugging printouts. + -> TypeConName + -- ^ The template in which the given choice is defined. + -> ChoiceName + -- ^ The choice to be verified. + -> TypeConName + -- ^ The template in which the given field is defined. + -> FieldName + -- ^ The field to be verified. + -> IO Result +verify dar debug choiceTmplName choiceName fieldTmplName fieldName = do + -- Read the packages to analyse, and initialise the provided solver. + pkgs <- readPackages [dar] + solver <- getSolver + -- Find the given template names in the packages. + choiceTmpl <- findTemplate pkgs choiceTmplName + fieldTmpl <- findTemplate pkgs fieldTmplName + -- Start reading data type and value definitions. References to other + -- values are just stored as references at this point. + debug "Start value gathering" + case runEnv (genPackages pkgs) (emptyEnv :: Env 'ValueGathering) of + Left err-> outputError err "Value phase finished with error: " + Right env1 -> do + -- All value definitions have been handled. Start computing closures of + -- the stored value references. After this phase, all value references + -- should be inlined. + debug "Start value solving" + let env2 = solveValueReferences env1 + -- Start reading template definitions. References to choices are just + -- stored as references at this point. + debug "Start choice gathering" + case runEnv (genPackages pkgs) env2 of + Left err -> outputError err "Choice phase finished with error: " + Right env3 -> do + -- All choice definitions have been handled. Start computing closures + -- of the stored choice references. After this phase, all choice + -- references should be inlined. + debug "Start choice solving" + let env4 = solveChoiceReferences env3 + -- Construct the actual constraints to be solved by the SMT solver. + debug "Start constraint solving phase" + let cset = constructConstr env4 choiceTmpl choiceName fieldTmpl fieldName + debug $ renderString $ layoutCompact ("Create: " <+> pretty (_cCres cset)) + debug $ renderString $ layoutCompact ("Archive: " <+> pretty (_cArcs cset)) + -- Pass the constraints to the SMT solver. + solveConstr solver debug cset + where + -- | Lookup the first package that defines the given template. This avoids + -- having to pass in the package reference manually when using the tool. + findTemplate :: [(PackageId, (Package, Maybe PackageName))] + -- ^ The package from the DAR file. + -> TypeConName + -- ^ The template name. + -> IO (Qualified TypeConName) + findTemplate pkgs tem = maybe + (outputError (UnknownTmpl tem) "Parsing phase finished with error: ") + (\(pacid, mod) -> return $ Qualified (PRImport pacid) mod tem) + (listToMaybe $ mapMaybe (templateInPackage tem) pkgs) + + -- | Return the package id and the name of the module containing the given + -- template, if it exists. + templateInPackage :: TypeConName + -- ^ The template to look for. + -> (PackageId, (Package, Maybe PackageName)) + -- ^ The package to look in. + -> Maybe (PackageId, ModuleName) + templateInPackage tem (id, (pac,_)) = + case templateInModules tem $ NM.toList $ packageModules pac of + Nothing -> Nothing + Just mod -> Just (id, mod) + + -- | Return the name of the module containing the given template, if it + -- exists. + templateInModules :: TypeConName + -- ^ The template to look for. + -> [Module] + -- ^ The modules to look in. + -> Maybe ModuleName + templateInModules tem mods = + listToMaybe $ + mapMaybe ( \Module{..} -> + let tmpls = NM.toList moduleTemplates + in if not (any (\Template{..} -> tplTypeCon == tem) tmpls) + then Nothing + else Just moduleName ) + mods diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Context.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Context.hs new file mode 100644 index 000000000000..63ab306f825a --- /dev/null +++ b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Context.hs @@ -0,0 +1,900 @@ +-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} + +-- | Contexts for DAML LF static verification +module DA.Daml.LF.Verify.Context + ( Phase(..) + , GenPhase + , BoolExpr(..) + , Cond(..) + , Env(..) + , Error(..) + , MonadEnv + , UpdateSet(..) + , Upd(..) + , ChoiceData(..) + , UpdChoice(..) + , Skolem(..) + , getEnv + , runEnv + , genRenamedVar + , emptyEnv + , extVarEnv, extRecEnv, extValEnv, extChEnv, extDatsEnv, extCidEnv, extCtrRec + , extRecEnvLvl1 + , lookupVar, lookupRec, lookupVal, lookupChoice, lookupDataCon, lookupCid + , concatEnv + , emptyUpdateSet + , concatUpdateSet + , addUpd + , conditionalUpdateSet + , solveValueReferences + , solveChoiceReferences + , fieldName2VarName + , recTypConFields, recTypFields, recExpFields + ) where + +import Control.Monad.Error.Class (MonadError (..), throwError) +import Control.Monad.State.Lazy +import Data.Hashable +import GHC.Generics +import Data.Maybe (isJust, fromMaybe) +import Data.List (find) +import Data.Bifunctor +import qualified Data.HashMap.Strict as HM +import qualified Data.Text as T +import Debug.Trace + +import DA.Daml.LF.Ast hiding (lookupChoice) +import DA.Daml.LF.Verify.Subst + +-- TODO: Move these data types to a seperate file? +-- | Data type denoting the phase of the constraint generator. +data Phase + = ValueGathering + -- ^ The value phase gathers all value and data type definitions across modules. + | ChoiceGathering + -- ^ The choice phase gathers the updates performed in choice definitions. + | Solving + -- ^ During the solving phase, all definitions have been loaded and updates + -- have been inlined. + +-- | Data type denoting a boolean condition expression. This data type was +-- introduced as DAML-LF does not have build-in boolean operators, and using +-- prelude functions gets messy. +data BoolExpr + = BExpr Expr + -- ^ A daml-lf expression. + | BAnd BoolExpr BoolExpr + -- ^ And operator. + | BNot BoolExpr + -- ^ Not operator. + deriving Show + +-- | Data type denoting a potentially conditional value. +data Cond a + = Determined a + -- ^ Non-conditional value. + | Conditional BoolExpr [Cond a] [Cond a] + -- ^ Conditional value, with a (Boolean) condition, at least one value in case + -- the condition holds, and at least one value in case it doesn't. + -- Note that these branch lists should not be empty. + -- TODO: Encode this invariant in the type system? + deriving (Show, Functor) + +-- | Construct a simple conditional. +createCond :: BoolExpr + -- ^ The condition to depend on. + -> a + -- ^ The value in case the condition holds. + -> a + -- ^ The value in case the condition does not hold. + -> Cond a +createCond cond x y = Conditional cond [Determined x] [Determined y] + +-- | Shift the conditional inside the update set. +introCond :: Cond (UpdateSet ph) -> UpdateSet ph +introCond (Determined upds) = upds +introCond (Conditional e updx updy) = case getPhase updx of + UpdateSetVG{} -> UpdateSetVG + (buildCond updx updy _usvgUpdate) + (buildCond updx updy _usvgChoice) + (buildCond updx updy _usvgValue) + UpdateSetCG{} -> UpdateSetCG + (buildCond updx updy _uscgUpdate) + (buildCond updx updy _uscgChoice) + UpdateSetS{} -> UpdateSetS + (buildCond updx updy _ussUpdate) + where + -- | Construct a single conditional, if the input is not empty. + buildCond :: [Cond (UpdateSet ph)] + -- ^ The input for the true case. + -> [Cond (UpdateSet ph)] + -- ^ The input for the false case. + -> (UpdateSet ph -> [Cond a]) + -- ^ The fetch function. + -> [Cond a] + buildCond updx updy get = + let xs = concatCond updx get + ys = concatCond updy get + in [Conditional e xs ys | not (null xs && null ys)] + + -- TODO: Temporary solution. Make introCond a part of the GenPhase class instead. + getPhase :: [Cond (UpdateSet ph)] -> UpdateSet ph + getPhase lst = case head lst of + Determined upds -> upds + Conditional _ xs _ -> getPhase xs + +-- | Fetch the conditionals from the conditional update set, and flatten the +-- two layers into one. +concatCond :: [Cond (UpdateSet ph)] + -- ^ The conditional update set to fetch from. + -> (UpdateSet ph -> [Cond a]) + -- ^ The fetch function. + -> [Cond a] +concatCond upds get = + let upds' = map introCond upds + in concatMap get upds' + +-- | Data type denoting an update. +data Upd + = UpdCreate + -- ^ Data type denoting a create update. + { _creTemp :: !(Qualified TypeConName) + -- ^ Qualified type constructor corresponding to the contract template. + , _creField :: ![(FieldName, Expr)] + -- ^ The fields to be verified, together with their value. + } + | UpdArchive + -- ^ Data type denoting an archive update. + { _arcTemp :: !(Qualified TypeConName) + -- ^ Qualified type constructor corresponding to the contract template. + , _arcField :: ![(FieldName, Expr)] + -- ^ The fields to be verified, together with their value. + } + deriving Show + +-- | Data type denoting an exercised choice. +data UpdChoice = UpdChoice + { _choTemp :: !(Qualified TypeConName) + -- ^ Qualified type constructor corresponding to the contract template. + , _choName :: !ChoiceName + -- ^ The name of the choice. + } + deriving (Eq, Generic, Hashable, Show) + +-- | The collection of updates being performed. +data UpdateSet (ph :: Phase) where + UpdateSetVG :: + { _usvgUpdate :: ![Cond Upd] + -- ^ The list of updates. + , _usvgChoice :: ![Cond UpdChoice] + -- ^ The list of exercised choices. + , _usvgValue :: ![Cond (Qualified ExprValName)] + -- ^ The list of referenced values. + } -> UpdateSet 'ValueGathering + UpdateSetCG :: + { _uscgUpdate :: ![Cond Upd] + -- ^ The list of updates. + , _uscgChoice :: ![Cond UpdChoice] + -- ^ The list of exercised choices. + } -> UpdateSet 'ChoiceGathering + UpdateSetS :: + { _ussUpdate :: ![Cond Upd] + -- ^ The list of updates. + } -> UpdateSet 'Solving + +class GenPhase ph where + emptyUpdateSet :: UpdateSet ph + emptyEnv :: Env ph + +instance GenPhase 'ValueGathering where + emptyUpdateSet = UpdateSetVG [] [] [] + emptyEnv = EnvVG [] HM.empty HM.empty HM.empty [] + +instance GenPhase 'ChoiceGathering where + emptyUpdateSet = UpdateSetCG [] [] + emptyEnv = EnvCG [] HM.empty HM.empty HM.empty [] HM.empty + +instance GenPhase 'Solving where + emptyUpdateSet = UpdateSetS [] + emptyEnv = EnvS [] HM.empty HM.empty HM.empty [] HM.empty + +-- | Combine two update sets. +concatUpdateSet :: UpdateSet ph + -- ^ The first update set to be combined. + -> UpdateSet ph + -- ^ The second update set to be combined. + -> UpdateSet ph +concatUpdateSet (UpdateSetVG upd1 cho1 val1) (UpdateSetVG upd2 cho2 val2) = + UpdateSetVG (upd1 ++ upd2) (cho1 ++ cho2) (val1 ++ val2) +concatUpdateSet (UpdateSetCG upd1 cho1) (UpdateSetCG upd2 cho2) = + UpdateSetCG (upd1 ++ upd2) (cho1 ++ cho2) +concatUpdateSet (UpdateSetS upd1) (UpdateSetS upd2) = + UpdateSetS (upd1 ++ upd2) + +-- | Add a single Upd to an UpdateSet +addUpd :: UpdateSet ph + -- ^ The update set to extend. + -> Upd + -- ^ The update to add. + -> UpdateSet ph +addUpd upds@UpdateSetVG{..} upd = upds{_usvgUpdate = Determined upd : _usvgUpdate} +addUpd upds@UpdateSetCG{..} upd = upds{_uscgUpdate = Determined upd : _uscgUpdate} +addUpd upds@UpdateSetS{..} upd = upds{_ussUpdate = Determined upd : _ussUpdate} + +-- | Make an update set conditional. A second update set can also be introduced +-- for the case where the condition does not hold. +conditionalUpdateSet :: Expr + -- ^ The condition on which to combine the two update sets. + -> UpdateSet ph + -- ^ The update set in case the condition holds. + -> UpdateSet ph + -- ^ The update set in case the condition does not hold. + -> UpdateSet ph +conditionalUpdateSet exp upd1 upd2 = + introCond $ createCond (BExpr exp) upd1 upd2 + +-- | Refresh a given expression variable by producing a fresh renamed variable. +-- TODO: when a renamed var gets renamed again, it might overlap again. +-- We should have an additional field in VarName to denote its number. +genRenamedVar :: MonadEnv m ph + => ExprVarName + -- ^ The variable to be renamed. + -> m ExprVarName +genRenamedVar (ExprVarName x) = ExprVarName . T.append x . T.pack <$> fresh + +-- | Data type denoting a skolemized variable. +data Skolem + = SkolVar ExprVarName + -- ^ Skolemised term variable. + | SkolRec ExprVarName [FieldName] + -- ^ List of skolemised field names, with their variable. + -- e.g. `this.field` + deriving (Eq, Show) + +-- | Data type denoting a contract id. +data Cid + = CidVar ExprVarName + -- ^ An expression variable denoting a contract id. + | CidRec ExprVarName FieldName + -- ^ A record projection denoting a contract id. + deriving (Generic, Hashable, Eq, Show) + +-- | Convert an expression to a contract id, if possible. +expr2cid :: MonadEnv m ph + => Expr + -- ^ The expression to be converted. + -> m Cid +expr2cid (EVar x) = return $ CidVar x +expr2cid (ERecProj _ f (EVar x)) = return $ CidRec x f +expr2cid (EStructProj f (EVar x)) = return $ CidRec x f +expr2cid _ = throwError ExpectCid + +-- | Data type containing the data stored for a choice definition. +data ChoiceData (ph :: Phase) = ChoiceData + { _cdSelf :: ExprVarName + -- ^ The variable denoting `self`. + , _cdThis :: ExprVarName + -- ^ The variable denoting `this`. + , _cdArgs :: ExprVarName + -- ^ The variable denoting `args`. + , _cdUpds :: Expr -> Expr -> Expr -> UpdateSet ph + -- ^ Function from self, this and args to the updates performed by this choice. + , _cdType :: Type + -- ^ The return type of this choice. + } + +-- TODO: Could we alternatively just declare the variables that occur in the updates and drop the skolems? +-- | The environment for the DAML-LF verifier +data Env (ph :: Phase) where + EnvVG :: + { _envvgskol :: ![Skolem] + -- ^ The skolemised term variables and fields. + , _envvgvals :: !(HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ValueGathering)) + -- ^ The bound values. + , _envvgdats :: !(HM.HashMap TypeConName DefDataType) + -- ^ The set of data constructors. + , _envvgcids :: !(HM.HashMap Cid (ExprVarName, [ExprVarName])) + -- ^ The set of fetched cid's mapped to their current variable name, along + -- with a list of any potential old variable names. + , _envvgctrs :: ![(Expr, Expr)] + -- ^ Additional equality constraints. + } -> Env 'ValueGathering + EnvCG :: + { _envcgskol :: ![Skolem] + -- ^ The skolemised term variables and fields. + , _envcgvals :: !(HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ChoiceGathering)) + -- ^ The bound values. + , _envcgdats :: !(HM.HashMap TypeConName DefDataType) + -- ^ The set of data constructors. + , _envcgcids :: !(HM.HashMap Cid (ExprVarName, [ExprVarName])) + -- ^ The set of fetched cid's mapped to their current variable name, along + -- with a list of any potential old variable names. + , _envcgctrs :: ![(Expr, Expr)] + -- ^ Additional equality constraints. + , _envcgchs :: !(HM.HashMap UpdChoice (ChoiceData 'ChoiceGathering)) + -- ^ The set of relevant choices. + } -> Env 'ChoiceGathering + EnvS :: + { _envsskol :: ![Skolem] + -- ^ The skolemised term variables and fields. + , _envsvals :: !(HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'Solving)) + -- ^ The bound values. + , _envsdats :: !(HM.HashMap TypeConName DefDataType) + -- ^ The set of data constructors. + , _envscids :: !(HM.HashMap Cid (ExprVarName, [ExprVarName])) + -- ^ The set of fetched cid's mapped to their current variable name, along + -- with a list of any potential old variable names. + , _envsctrs :: ![(Expr, Expr)] + -- ^ Additional equality constraints. + , _envschs :: !(HM.HashMap UpdChoice (ChoiceData 'Solving)) + -- ^ The set of relevant choices. + } -> Env 'Solving + +-- | Combine two environments. +concatEnv :: Env ph + -- ^ The first environment to be combined. + -> Env ph + -- ^ The second environment to be combined. + -> Env ph +concatEnv (EnvVG vars1 vals1 dats1 cids1 ctrs1) (EnvVG vars2 vals2 dats2 cids2 ctrs2) = + EnvVG (vars1 ++ vars2) (vals1 `HM.union` vals2) (dats1 `HM.union` dats2) + (cids1 `HM.union` cids2) (ctrs1 ++ ctrs2) +concatEnv (EnvCG vars1 vals1 dats1 cids1 ctrs1 chos1) (EnvCG vars2 vals2 dats2 cids2 ctrs2 chos2) = + EnvCG (vars1 ++ vars2) (vals1 `HM.union` vals2) (dats1 `HM.union` dats2) + (cids1 `HM.union` cids2) (ctrs1 ++ ctrs2) (chos1 `HM.union` chos2) +concatEnv (EnvS vars1 vals1 dats1 cids1 ctrs1 chos1) (EnvS vars2 vals2 dats2 cids2 ctrs2 chos2) = + EnvS (vars1 ++ vars2) (vals1 `HM.union` vals2) (dats1 `HM.union` dats2) + (cids1 `HM.union` cids2) (ctrs1 ++ ctrs2) (chos1 `HM.union` chos2) + -- TODO: union makes me slightly nervous, as it allows overlapping keys + -- (and just uses the first). `unionWith concatUpdateSet` would indeed be better, + -- but this still makes me nervous as the expr and exprvarnames wouldn't be merged. + +-- | Convert a fieldname into an expression variable name. +fieldName2VarName :: FieldName -> ExprVarName +fieldName2VarName = ExprVarName . unFieldName + +-- | Type class constraint with the required monadic effects for functions +-- manipulating the verification environment. +type MonadEnv m ph = (MonadError Error m, MonadState (Int,Env ph) m) + +-- | Fetch the current environment. +getEnv :: MonadEnv m ph => m (Env ph) +getEnv = snd <$> get + +-- | Set the current environment. +putEnv :: MonadEnv m ph => Env ph -> m () +putEnv env = get >>= \(uni,_) -> put (uni,env) + +-- | Generate a new unique name. +fresh :: MonadEnv m ph => m String +fresh = do + (cur,env) <- get + put (cur + 1,env) + return $ show cur + +-- | Evaluate the MonadEnv to produce an error message or the final environment. +runEnv :: StateT (Int, Env ph) (Either Error) () + -- ^ The monadic computation to be evaluated. + -> Env ph + -- ^ The initial environment to start from. + -> Either Error (Env ph) +runEnv comp env0 = do + (_res, (_uni,env1)) <- runStateT comp (0,env0) + return env1 + +-- | Skolemise an expression variable and extend the environment. +extVarEnv :: MonadEnv m ph + => ExprVarName + -- ^ The expression variable to be skolemised. + -> m () +extVarEnv x = extSkolEnv (SkolVar x) + +-- | Skolemise a list of record projection and extend the environment. +extRecEnv :: MonadEnv m ph + => ExprVarName + -- ^ The variable on which is being projected. + -> [FieldName] + -- ^ The fields which should be skolemised. + -> m () +extRecEnv x fs = extSkolEnv (SkolRec x fs) + +-- | Extend the environment with a new skolem variable. +extSkolEnv :: MonadEnv m ph + => Skolem + -- ^ The skolem variable to add. + -> m () +extSkolEnv skol = getEnv >>= \case + env@EnvVG{..} -> putEnv env{_envvgskol = skol : _envvgskol} + env@EnvCG{..} -> putEnv env{_envcgskol = skol : _envcgskol} + env@EnvS{..} -> putEnv env{_envsskol = skol : _envsskol} + +-- | Extend the environment with a new value definition. +extValEnv :: MonadEnv m ph + => Qualified ExprValName + -- ^ The name of the value being defined. + -> Expr + -- ^ The (partially) evaluated value definition. + -> UpdateSet ph + -- ^ The updates performed by this value. + -> m () +extValEnv val expr upd = getEnv >>= \case + env@EnvVG{..} -> putEnv env{_envvgvals = HM.insert val (expr, upd) _envvgvals} + env@EnvCG{..} -> putEnv env{_envcgvals = HM.insert val (expr, upd) _envcgvals} + env@EnvS{..} -> putEnv env{_envsvals = HM.insert val (expr, upd) _envsvals} + +-- | Extends the environment with a new choice. +extChEnv :: MonadEnv m ph + => Qualified TypeConName + -- ^ The type of the template on which this choice is defined. + -> ChoiceName + -- ^ The name of the new choice. + -> ExprVarName + -- ^ Variable to bind the ContractId on which this choice is exercised on to. + -> ExprVarName + -- ^ Variable to bind the contract on which this choice is exercised on to. + -> ExprVarName + -- ^ Variable to bind the choice argument to. + -> UpdateSet ph + -- ^ The updates performed by the new choice. + -> Type + -- ^ The result type of the new choice. + -> m () +extChEnv tc ch self this arg upd typ = + let substUpd sExp tExp aExp = substituteTm (createExprSubst [(self,sExp),(this,tExp),(arg,aExp)]) upd + in getEnv >>= \case + EnvVG{} -> error "Impossible: extChEnv is not used in the value gathering phase" + env@EnvCG{..} -> putEnv env{_envcgchs = HM.insert (UpdChoice tc ch) (ChoiceData self this arg substUpd typ) _envcgchs} + env@EnvS{..} -> putEnv env{_envschs = HM.insert (UpdChoice tc ch) (ChoiceData self this arg substUpd typ) _envschs} + +-- | Extend the environment with a list of new data type definitions. +extDatsEnv :: MonadEnv m ph + => HM.HashMap TypeConName DefDataType + -- ^ A hashmap of the data constructor names, with their corresponding definitions. + -> m () +extDatsEnv hmap = getEnv >>= \case + env@EnvVG{..} -> putEnv env{_envvgdats = hmap `HM.union` _envvgdats} + env@EnvCG{..} -> putEnv env{_envcgdats = hmap `HM.union` _envcgdats} + env@EnvS{..} -> putEnv env{_envsdats = hmap `HM.union` _envsdats} + +-- | Extend the environment with a new contract id, and the variable to which +-- the fetched contract is bound. +extCidEnv :: MonadEnv m ph + => Expr + -- ^ The contract id expression. + -> ExprVarName + -- ^ The variable name to which the fetched contract is bound. + -> m () +extCidEnv exp var = do + prev <- do + { (cur, old) <- lookupCid exp + ; return $ cur : old } + `catchError` (\_ -> return []) + cid <- expr2cid exp + let new = (var, prev) + getEnv >>= \case + env@EnvVG{..} -> putEnv env{_envvgcids = HM.insert cid new _envvgcids} + env@EnvCG{..} -> putEnv env{_envcgcids = HM.insert cid new _envcgcids} + env@EnvS{..} -> putEnv env{_envscids = HM.insert cid new _envscids} + +-- | Extend the environment with additional equality constraints, between a +-- variable and its field values. +extCtrRec :: MonadEnv m ph + => ExprVarName + -- ^ The variable to be asserted. + -> [(FieldName, Expr)] + -- ^ The fields with their values. + -> m () +extCtrRec var fields = do + let ctrs = map (\(f, e) -> (EStructProj f (EVar var), e)) fields + getEnv >>= \case + env@EnvVG{..} -> putEnv env{_envvgctrs = ctrs ++ _envvgctrs} + env@EnvCG{..} -> putEnv env{_envcgctrs = ctrs ++ _envcgctrs} + env@EnvS{..} -> putEnv env{_envsctrs = ctrs ++ _envsctrs} + +-- TODO: Is one layer of recursion enough? +-- | Recursively skolemise the given record fields, when they have a record +-- type. Note that this only works 1 level deep. +extRecEnvLvl1 :: MonadEnv m ph + => [(FieldName, Type)] + -- ^ The record fields to skolemise, together with their types. + -> m () +extRecEnvLvl1 = mapM_ step + where + step :: MonadEnv m ph => (FieldName, Type) -> m () + step (f,typ) = do + { fsRec <- recTypFields typ + ; extRecEnv (fieldName2VarName f) fsRec + } + -- TODO: Temporary fix + `catchError` (\_ -> return ()) + +-- | Lookup an expression variable in the environment. Returns `True` if this variable +-- has been skolemised, or `False` otherwise. +lookupVar :: MonadEnv m ph + => ExprVarName + -- ^ The expression variable to look up. + -> m Bool +lookupVar x = getEnv >>= \case + EnvVG{..} -> return $ elem (SkolVar x) _envvgskol + EnvCG{..} -> return $ elem (SkolVar x) _envcgskol + EnvS{..} -> return $ elem (SkolVar x) _envsskol + +-- | Lookup a record project in the environment. Returns a boolean denoting +-- whether or not the record projection has been skolemised. +lookupRec :: MonadEnv m ph + => ExprVarName + -- ^ The expression variable on which is being projected. + -> FieldName + -- ^ The field name which is being projected. + -> m Bool +lookupRec x f = do + skols <- getEnv >>= \case + EnvVG{..} -> return _envvgskol + EnvCG{..} -> return _envcgskol + EnvS{..} -> return _envsskol + let fields = [ fs | SkolRec y fs <- skols, x == y ] + if not (null fields) + then return (elem f $ head fields) + else return False + +-- | Lookup a value name in the environment. Returns its (partially) evaluated +-- definition, together with the updates it performs. +lookupVal :: MonadEnv m ph + => Qualified ExprValName + -- ^ The value name to lookup. + -> m (Expr, UpdateSet ph) +lookupVal val = do + vals <- getEnv >>= \case + EnvVG{..} -> return _envvgvals + EnvCG{..} -> return _envcgvals + EnvS{..} -> return _envsvals + case HM.lookup val vals of + Just res -> return res + Nothing -> throwError (UnknownValue val) + +-- | Lookup a choice name in the environment. Returns a function which, once +-- self, this and args have been instantiated, returns the set of updates it +-- performs. Also returns the return type of the choice. +lookupChoice :: MonadEnv m ph + => Qualified TypeConName + -- ^ The template name in which this choice is defined. + -> ChoiceName + -- ^ The choice name to lookup. + -> m (Expr -> Expr -> Expr -> UpdateSet ph, Type) +lookupChoice tem ch = do + chs <- getEnv >>= \case + EnvVG{..} -> return HM.empty + EnvCG{..} -> return _envcgchs + EnvS{..} -> return _envschs + case HM.lookup (UpdChoice tem ch) chs of + Nothing -> throwError (UnknownChoice ch) + Just ChoiceData{..} -> return (_cdUpds, _cdType) + +-- | Lookup a data type definition in the environment. +lookupDataCon :: MonadEnv m ph + => TypeConName + -- ^ The data constructor to lookup. + -> m DefDataType +lookupDataCon tc = do + dats <- getEnv >>= \case + EnvVG{..} -> return _envvgdats + EnvCG{..} -> return _envcgdats + EnvS{..} -> return _envsdats + case HM.lookup tc dats of + Nothing -> throwError (UnknownDataCons tc) + Just def -> return def + +-- | Lookup a contract id in the environment. Returns the variable its fetched +-- contract is bound to, along with a list of any previous bindings. +lookupCid :: MonadEnv m ph + => Expr + -- ^ The contract id to lookup. + -> m (ExprVarName, [ExprVarName]) +lookupCid exp = do + cid <- expr2cid exp + cids <- getEnv >>= \case + EnvVG{..} -> return _envvgcids + EnvCG{..} -> return _envcgcids + EnvS{..} -> return _envscids + case HM.lookup cid cids of + Nothing -> throwError $ UnknownCid cid + Just var -> return var + +-- | Solves the value references by computing the closure of all referenced +-- values, for each value in the environment. +-- It thus empties `_usValue` by collecting all updates made by this closure. +solveValueReferences :: Env 'ValueGathering -> Env 'ChoiceGathering +solveValueReferences EnvVG{..} = + let valhmap = foldl (\hmap ref -> snd $ solveReference lookup_ref get_refs ext_upds intro_cond empty_upds [] hmap ref) _envvgvals (HM.keys _envvgvals) + in EnvCG _envvgskol (convertHMap valhmap) _envvgdats _envvgcids _envvgctrs HM.empty + where + lookup_ref :: Qualified ExprValName + -> HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ValueGathering) + -> (Expr, UpdateSet 'ValueGathering) + lookup_ref ref hmap = fromMaybe (error "Impossible: Undefined value ref while solving") + (HM.lookup ref hmap) + + get_refs :: (Expr, UpdateSet 'ValueGathering) + -> ([Cond (Qualified ExprValName)], (Expr, UpdateSet 'ValueGathering)) + get_refs (e, upds@UpdateSetVG{..}) = (_usvgValue, (e, upds{_usvgValue = []})) + + ext_upds :: (Expr, UpdateSet 'ValueGathering) -> (Expr, UpdateSet 'ValueGathering) + -> (Expr, UpdateSet 'ValueGathering) + ext_upds (e, upds1) (_, upds2) = (e, concatUpdateSet upds1 upds2) + + intro_cond :: Cond (Expr, UpdateSet 'ValueGathering) + -> (Expr, UpdateSet 'ValueGathering) + -- Note that the expression is not important here, as it will be ignored in + -- `ext_upds` later on. + intro_cond (Determined x) = x + intro_cond (Conditional cond cx cy) = + let xs = map intro_cond cx + ys = map intro_cond cy + e = fst $ head xs + updx = foldl concatUpdateSet emptyUpdateSet $ map snd xs + updy = foldl concatUpdateSet emptyUpdateSet $ map snd ys + in (e, introCond $ createCond cond updx updy) + + empty_upds :: (Expr, UpdateSet 'ValueGathering) + -> (Expr, UpdateSet 'ValueGathering) + empty_upds (e, _) = (e, emptyUpdateSet) + + convertHMap :: HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ValueGathering) + -> HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ChoiceGathering) + convertHMap = HM.map (second updateSetVG2CG) + + updateSetVG2CG :: UpdateSet 'ValueGathering -> UpdateSet 'ChoiceGathering + updateSetVG2CG UpdateSetVG{..} = if null _usvgValue + then UpdateSetCG _usvgUpdate _usvgChoice + else error "Impossible: There should be no references remaining after value solving" + +-- | Solves the choice references by computing the closure of all referenced +-- choices, for each choice in the environment. +-- It thus empties `_usChoice` by collecting all updates made by this closure. +solveChoiceReferences :: Env 'ChoiceGathering -> Env 'Solving +solveChoiceReferences EnvCG{..} = + let chhmap = foldl (\hmap ref -> snd $ solveReference lookup_ref get_refs ext_upds intro_cond empty_upds [] hmap ref) _envcgchs (HM.keys _envcgchs) + chshmap = convertChHMap chhmap + valhmap = HM.map (inlineChoices chshmap) _envcgvals + in EnvS _envcgskol valhmap _envcgdats _envcgcids _envcgctrs chshmap + where + lookup_ref :: UpdChoice + -> HM.HashMap UpdChoice (ChoiceData 'ChoiceGathering) + -> ChoiceData 'ChoiceGathering + lookup_ref upd hmap = fromMaybe (error "Impossible: Undefined choice ref while solving") + (HM.lookup upd hmap) + + get_refs :: ChoiceData 'ChoiceGathering + -> ([Cond UpdChoice], ChoiceData 'ChoiceGathering) + -- TODO: This is gonna result in a ton of substitutions + get_refs chdat@ChoiceData{..} = + -- TODO: This seems to be a rather common pattern. Abstract to reduce duplication. + let chos = _uscgChoice $ _cdUpds (EVar _cdSelf) (EVar _cdThis) (EVar _cdArgs) + updfunc1 (selfexp :: Expr) (thisexp :: Expr) (argsexp :: Expr) = + let upds@UpdateSetCG{..} = _cdUpds selfexp thisexp argsexp + in upds{_uscgChoice = []} + in (chos, chdat{_cdUpds = updfunc1}) + + ext_upds :: ChoiceData 'ChoiceGathering + -> ChoiceData 'ChoiceGathering + -> ChoiceData 'ChoiceGathering + ext_upds chdat1 chdat2 = + let updfunc (selfexp :: Expr) (thisexp :: Expr) (argsexp :: Expr) = + _cdUpds chdat1 selfexp thisexp argsexp `concatUpdateSet` + _cdUpds chdat2 selfexp thisexp argsexp + in chdat1{_cdUpds = updfunc} + + intro_cond :: GenPhase ph + => Cond (ChoiceData ph) + -> ChoiceData ph + -- Note that the expression and return type is not important here, as it + -- will be ignored in `ext_upds` later on. + intro_cond (Determined x) = x + intro_cond (Conditional cond cdatxs cdatys) = + let datxs = map intro_cond cdatxs + datys = map intro_cond cdatys + updfunc (selfexp :: Expr) (thisexp :: Expr) (argsexp :: Expr) = + introCond (createCond cond + (foldl + (\upd dat -> upd `concatUpdateSet` _cdUpds dat selfexp thisexp argsexp) + emptyUpdateSet datxs) + (foldl + (\upd dat -> upd `concatUpdateSet` _cdUpds dat selfexp thisexp argsexp) + emptyUpdateSet datys)) + in (head datxs){_cdUpds = updfunc} + + empty_upds :: ChoiceData 'ChoiceGathering + -> ChoiceData 'ChoiceGathering + empty_upds dat = dat{_cdUpds = \ _ _ _ -> emptyUpdateSet} + + inlineChoices :: HM.HashMap UpdChoice (ChoiceData 'Solving) + -> (Expr, UpdateSet 'ChoiceGathering) + -> (Expr, UpdateSet 'Solving) + inlineChoices chshmap (exp, UpdateSetCG{..}) = + let lookupRes = map + (intro_cond . fmap (\ch -> fromMaybe (error "Impossible: missing choice while solving") (HM.lookup ch chshmap))) + _uscgChoice + chupds = concatMap (\ChoiceData{..} -> _ussUpdate $ _cdUpds (EVar _cdSelf) (EVar _cdThis) (EVar _cdArgs)) lookupRes + in (exp, UpdateSetS (_uscgUpdate ++ chupds)) + + convertChHMap :: HM.HashMap UpdChoice (ChoiceData 'ChoiceGathering) + -> HM.HashMap UpdChoice (ChoiceData 'Solving) + convertChHMap = HM.map (\chdat@ChoiceData{..} -> + chdat{_cdUpds = \(selfExp :: Expr) (thisExp :: Expr) (argsExp :: Expr) -> + updateSetCG2S $ _cdUpds selfExp thisExp argsExp}) + + updateSetCG2S :: UpdateSet 'ChoiceGathering -> UpdateSet 'Solving + updateSetCG2S UpdateSetCG{..} = if null _uscgChoice + then UpdateSetS _uscgUpdate + else error "Impossible: There should be no references remaining after choice solving" + +-- | Solves a single reference by recursively inlining the references into updates. +solveReference :: forall updset ref. (Eq ref, Hashable ref) + => (ref -> HM.HashMap ref updset -> updset) + -- ^ Function for looking up references in the update set. + -> (updset -> ([Cond ref], updset)) + -- ^ Function popping the references from the update set. + -> (updset -> updset -> updset) + -- ^ Function for concatinating update sets. + -> (Cond updset -> updset) + -- ^ Function for moving conditionals inside the update set. + -> (updset -> updset) + -- ^ Function for emptying a given update set of all updates. + -> [ref] + -- ^ The references which have already been visited. + -> HM.HashMap ref updset + -- ^ The hashmap mapping references to update sets. + -> ref + -- ^ The reference to be solved. + -> (updset, HM.HashMap ref updset) +solveReference lookup getRefs extUpds introCond emptyUpds vis hmap0 ref0 = + -- Lookup updates performed by the given reference, and split in new + -- references and reference-free updates. + let upd0 = lookup ref0 hmap0 + (refs, upd1) = getRefs upd0 + -- Check for loops. If the references has already been visited, then the + -- reference should be flagged as recursive. + in if ref0 `elem` vis + -- TODO: Recursion! + then trace "Recursion!" (upd1, hmap0) -- TODO: At least remove the references? + -- When no recursion has been detected, continue inlining the references. + else let (upd2, hmap1) = foldl handle_ref (upd1, hmap0) refs + in (upd1, HM.insert ref0 upd2 hmap1) + where + -- | Extend the closure by computing and adding the reference closure for + -- the given reference. + handle_ref :: (updset, HM.HashMap ref updset) + -- ^ The current closure (update set) and the current map for reference to update. + -> Cond ref + -- ^ The reference to be computed and added. + -> (updset, HM.HashMap ref updset) + -- For a simple reference, the closure is computed straightforwardly. + handle_ref (upd_i0, hmap_i0) (Determined ref_i) = + let (upd_i1, hmap_i1) = + solveReference lookup getRefs extUpds introCond emptyUpds (ref0:vis) hmap_i0 ref_i + in (extUpds upd_i0 upd_i1, hmap_i1) + -- A conditional reference is more involved, as the conditional needs to be + -- preserved in the computed closure (update set). + handle_ref (upd_i0, hmap_i0) (Conditional cond refs_ia refs_ib) = + -- Construct an update set without any updates. + let upd_i0_empty = emptyUpds upd_i0 + -- Compute the closure for the true-case. + (upd_ia, hmap_ia) = foldl handle_ref (upd_i0_empty, hmap_i0) refs_ia + -- Compute the closure for the false-case. + (upd_ib, hmap_ib) = foldl handle_ref (upd_i0_empty, hmap_ia) refs_ib + -- Move the conditional inwards, in the update set. + upd_i1 = extUpds upd_i0 $ introCond $ createCond cond upd_ia upd_ib + in (upd_i1, hmap_ib) + +-- TODO: This should work recursively +-- | Lookup the field names and corresponding types, for a given record type +-- constructor name. +recTypConFields :: MonadEnv m ph + => TypeConName + -- ^ The record type constructor name to lookup. + -> m [(FieldName,Type)] +recTypConFields tc = lookupDataCon tc >>= \dat -> case dataCons dat of + DataRecord fields -> return fields + _ -> throwError ExpectRecord + +-- | Lookup the fields for a given record type. +recTypFields :: MonadEnv m ph + => Type + -- ^ The type to lookup. + -> m [FieldName] +recTypFields (TCon tc) = do + fields <- recTypConFields $ qualObject tc + return $ map fst fields +recTypFields (TStruct fs) = return $ map fst fs +recTypFields _ = throwError ExpectRecord + +-- | Lookup the record fields and corresponding values from a given expression. +recExpFields :: MonadEnv m ph + => Expr + -- ^ The expression to lookup. + -> m [(FieldName, Expr)] +recExpFields (EVar x) = do + skols <- getEnv >>= \case + EnvVG{..} -> return _envvgskol + EnvCG{..} -> return _envcgskol + EnvS{..} -> return _envsskol + let fss = [ fs | SkolRec y fs <- skols, x == y ] + if not (null fss) + -- TODO: I would prefer `this.amount` here + then return $ zip (head fss) (map (EVar . fieldName2VarName) $ head fss) + else throwError $ UnboundVar x +recExpFields (ERecCon _ fs) = return fs +recExpFields (EStructCon fs) = return fs +recExpFields (ERecUpd _ f recExp fExp) = do + fs <- recExpFields recExp + unless (isJust $ find (\(n, _) -> n == f) fs) (throwError $ UnknownRecField f) + return $ (f, fExp) : [(n, e) | (n, e) <- fs, n /= f] +recExpFields (ERecProj _ f e) = do + fields <- recExpFields e + case lookup f fields of + Just e' -> recExpFields e' + Nothing -> throwError $ UnknownRecField f +recExpFields (EStructProj f e) = do + fields <- recExpFields e + case lookup f fields of + Just e' -> recExpFields e' + Nothing -> throwError $ UnknownRecField f +recExpFields _ = throwError ExpectRecord + +instance SubstTm BoolExpr where + substituteTm s (BExpr e) = BExpr (substituteTm s e) + substituteTm s (BAnd e1 e2) = BAnd (substituteTm s e1) (substituteTm s e2) + substituteTm s (BNot e) = BNot (substituteTm s e) + +instance SubstTm a => SubstTm (Cond a) where + substituteTm s (Determined x) = Determined $ substituteTm s x + substituteTm s (Conditional e x y) = + Conditional (substituteTm s e) (map (substituteTm s) x) (map (substituteTm s) y) + +instance SubstTm (UpdateSet ph) where + substituteTm s UpdateSetVG{..} = UpdateSetVG susUpdate _usvgChoice _usvgValue + where susUpdate = map (substituteTm s) _usvgUpdate + substituteTm s UpdateSetCG{..} = UpdateSetCG susUpdate _uscgChoice + where susUpdate = map (substituteTm s) _uscgUpdate + substituteTm s UpdateSetS{..} = UpdateSetS susUpdate + where susUpdate = map (substituteTm s) _ussUpdate + +instance SubstTm Upd where + substituteTm s UpdCreate{..} = UpdCreate _creTemp + (map (second (substituteTm s)) _creField) + substituteTm s UpdArchive{..} = UpdArchive _arcTemp + (map (second (substituteTm s)) _arcField) + +-- | Data type representing an error. +data Error + = UnknownValue (Qualified ExprValName) + | UnknownDataCons TypeConName + | UnknownChoice ChoiceName + | UnboundVar ExprVarName + | UnknownRecField FieldName + | UnknownCid Cid + | UnknownTmpl TypeConName + | ExpectRecord + | ExpectCid + | CyclicModules [ModuleName] + +instance Show Error where + show (UnknownValue qname) = "Impossible: Unknown value definition: " + ++ (show $ unExprValName $ qualObject qname) + show (UnknownDataCons tc) = "Impossible: Unknown data constructor: " ++ show tc + show (UnknownChoice ch) = "Impossible: Unknown choice definition: " ++ show ch + show (UnboundVar name) = "Impossible: Unbound term variable: " ++ show name + show (UnknownRecField f) = "Impossible: Unknown record field: " ++ show f + show (UnknownCid cid) = "Impossible: Unknown contract id: " ++ show cid + show (UnknownTmpl tem) = "Impossible: Unknown template: " ++ show tem + show ExpectRecord = "Impossible: Expected a record type" + show ExpectCid = "Impossible: Expected a contract id" + show (CyclicModules mods) = "Cyclic modules: " ++ show mods diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs new file mode 100644 index 000000000000..003757c93937 --- /dev/null +++ b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs @@ -0,0 +1,487 @@ +-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} + +-- | Constraint generator for DAML LF static verification +module DA.Daml.LF.Verify.Generate + ( genPackages + , Phase(..) + ) where + +import Control.Monad.Error.Class (throwError) +import Data.Maybe (listToMaybe) +import qualified Data.NameMap as NM + +import DA.Daml.LF.Ast hiding (lookupChoice) +import DA.Daml.LF.Verify.Context +import DA.Daml.LF.Verify.Subst + +-- | Data type denoting the output of the constraint generator. +data Output (ph :: Phase) = Output + { _oExpr :: Expr + -- ^ The expression, evaluated as far as possible. + , _oUpdate :: UpdateSet ph + -- ^ The updates, performed by this expression. + } + +-- | Construct an output with no updates. +emptyOut :: GenPhase ph + => Expr + -- ^ The evaluated expression. + -> Output ph +emptyOut expr = Output expr emptyUpdateSet + +-- | Extend a generator output with the updates of the second generator output. +-- Note that the end result will contain only the first expression. +combineOut :: Output ph -> Output ph -> Output ph +combineOut out1 out2 = extendOutUpds (_oUpdate out2) out1 + +-- | Update an output with a new evaluated expression. +updateOutExpr :: Expr + -- ^ The new output expression. + -> Output ph + -- ^ The generator output to be updated. + -> Output ph +updateOutExpr expr out = out{_oExpr = expr} + +-- | Update an output with additional updates. +extendOutUpds :: UpdateSet ph + -- ^ The extension of the update set. + -> Output ph + -- ^ The generator output to be updated. + -> Output ph +extendOutUpds upds out@Output{..} = out{_oUpdate = concatUpdateSet upds _oUpdate} + +-- | Update an output with an additional Archive update. +addArchiveUpd :: Qualified TypeConName + -- ^ The template to be archived. + -> [(FieldName, Expr)] + -- ^ The fields to be archived, with their respective values. + -> Output 'ChoiceGathering + -- ^ The generator output to be updated. + -> Output 'ChoiceGathering +addArchiveUpd temp fs (Output expr upds) = + Output expr (addUpd upds $ UpdArchive temp fs) + +-- | Generate an environment for a given list of packages. +-- Depending on the generator phase, this either adds all value and data type +-- definitions to the environment, or all template definitions with their +-- respective choices. +genPackages :: (GenPhase ph, MonadEnv m ph) + => [(PackageId, (Package, Maybe PackageName))] + -- ^ The list of packages, as produced by `readPackages`. + -> m () +genPackages inp = mapM_ genPackage inp + +-- | Generate an environment for a given package. +-- Depending on the generator phase, this either adds all value and data type +-- definitions to the environment, or all template definitions with their +-- respective choices. +genPackage :: (GenPhase ph, MonadEnv m ph) + => (PackageId, (Package, Maybe PackageName)) + -- ^ The package, as produced by `readPackages`. + -> m () +genPackage (id, (pac, _)) = mapM_ (genModule (PRImport id)) (NM.toList $ packageModules pac) + +-- | Generate an environment for a given module. +-- Depending on the generator phase, this either adds all value and data type +-- definitions to the environment, or all template definitions with their +-- respective choices. +genModule :: (GenPhase ph, MonadEnv m ph) + => PackageRef + -- ^ A reference to the package in which this module is defined. + -> Module + -- ^ The module to analyse. + -> m () +genModule pac mod = getEnv >>= \case + EnvVG{} -> do + extDatsEnv (NM.toHashMap (moduleDataTypes mod)) + mapM_ (genValue pac (moduleName mod)) (NM.toList $ moduleValues mod) + EnvCG{} -> + mapM_ (genTemplate pac (moduleName mod)) (NM.toList $ moduleTemplates mod) + EnvS{} -> error "Impossible: genModule can't be used in the solving phase" + +-- | Analyse a value definition and add to the environment. +genValue :: (GenPhase ph, MonadEnv m ph) + => PackageRef + -- ^ A reference to the package in which this value is defined. + -> ModuleName + -- ^ The name of the module in which this value is defined. + -> DefValue + -- ^ The value to be analysed and added. + -> m () +genValue pac mod val = do + expOut <- genExpr True (instPRSelf pac $ dvalBody val) + let qname = Qualified pac mod (fst $ dvalBinder val) + extValEnv qname (_oExpr expOut) (_oUpdate expOut) + +-- | Analyse a choice definition and add to the environment. +-- TODO: Handle annotated choices, by returning a set of annotations. +genChoice :: MonadEnv m 'ChoiceGathering + => PackageRef + -- ^ A reference to the package in which this choice is defined. + -> Qualified TypeConName + -- ^ The template in which this choice is defined. + -> (ExprVarName,ExprVarName) + -- ^ The original and renamed variable `this` referencing the contract on + -- which this choice is called. + -> [FieldName] + -- ^ The list of fields available in the template. + -> TemplateChoice + -- ^ The choice to be analysed and added. + -> m () +genChoice pac tem (this',this) temFs TemplateChoice{..} = do + let self' = chcSelfBinder + arg' = fst chcArgBinder + self <- genRenamedVar self' + arg <- genRenamedVar arg' + extVarEnv self + extVarEnv arg + argFs <- recTypFields (snd chcArgBinder) + extRecEnv arg argFs + expOut <- genExpr True + $ substituteTm (createExprSubst [(self',EVar self),(this',EVar this),(arg',EVar arg)]) + $ instPRSelf pac chcUpdate + let out = if chcConsuming + then addArchiveUpd tem fields expOut + else expOut + extChEnv tem chcName self this arg (_oUpdate out) chcReturnType + where + fields = map (\f -> (f, ERecProj (TypeConApp tem []) f (EVar this))) temFs + +-- | Analyse a template definition and add all choices to the environment. +genTemplate :: MonadEnv m 'ChoiceGathering + => PackageRef + -- ^ A reference to the package in which this template is defined. + -> ModuleName + -- ^ The module in which this template is defined. + -> Template + -- ^ The template to be analysed and added. + -> m () +-- TODO: Take preconditions into account? +genTemplate pac mod Template{..} = do + let name = Qualified pac mod tplTypeCon + fields <- recTypConFields tplTypeCon + let fs = map fst fields + this <- genRenamedVar tplParam + extVarEnv this + extRecEnv this fs + extRecEnvLvl1 fields + mapM_ (genChoice pac name (tplParam,this) fs) (archive : NM.toList tplChoices) + where + archive :: TemplateChoice + archive = TemplateChoice Nothing (ChoiceName "Archive") True + (ENil (TBuiltin BTParty)) (ExprVarName "self") + (ExprVarName "arg", TStruct []) (TBuiltin BTUnit) + (EUpdate $ UPure (TBuiltin BTUnit) (EBuiltin BEUnit)) + +-- | Analyse an expression, and produce an Output storing its (partial) +-- evaluation result and the set of performed updates. +genExpr :: (GenPhase ph, MonadEnv m ph) + => Bool + -- ^ Argument denoting whether updates should be analysed. + -> Expr + -- ^ The expression to be analysed. + -> m (Output ph) +genExpr updFlag = \case + ETmApp fun arg -> genForTmApp updFlag fun arg + ETyApp expr typ -> genForTyApp updFlag expr typ + ELet bind body -> genForLet updFlag bind body + EVar name -> genForVar updFlag name + EVal w -> genForVal updFlag w + ERecProj tc f e -> genForRecProj updFlag tc f e + EStructProj f e -> genForStructProj updFlag f e + ELocation _ expr -> genExpr updFlag expr + ECase e cs -> genForCase updFlag e cs + EUpdate upd -> if updFlag + then do + (out, _, _) <- genUpdate upd + return out + else return $ emptyOut $ EUpdate upd + -- TODO: Extend additional cases + e -> return $ emptyOut e + +-- | Analyse an update expression, and produce both an Output, its return type +-- and potentially the field values of any created contracts. +genUpdate :: (GenPhase ph, MonadEnv m ph) + => Update + -- ^ The update expression to be analysed. + -> m (Output ph, Type, Maybe Expr) +genUpdate = \case + UCreate tem arg -> genForCreate tem arg + UExercise tem ch cid par arg -> genForExercise tem ch cid par arg + UBind bind expr -> genForBind bind expr + UPure typ expr -> do + out <- genExpr True expr + return (out, typ, Nothing) + -- TODO: Extend additional cases + UGetTime -> return (emptyOut (EUpdate UGetTime), TBuiltin BTTimestamp, Nothing) + u -> error ("Update not implemented yet: " ++ show u) + +-- | Analyse a term application expression. +genForTmApp :: (GenPhase ph, MonadEnv m ph) + => Bool + -- ^ Flag denoting whether updates should be analysed. + -> Expr + -- ^ The function expression. + -> Expr + -- ^ The argument expression. + -> m (Output ph) +genForTmApp updFlag fun arg = do + funOut <- genExpr updFlag fun + arout <- genExpr updFlag arg + case _oExpr funOut of + -- TODO: Should we rename here? + ETmLam bndr body -> do + let subst = singleExprSubst (fst bndr) (_oExpr arout) + resExpr = substituteTm subst body + resOut <- genExpr updFlag resExpr + return $ combineOut resOut + $ combineOut funOut arout + fun' -> return $ updateOutExpr (ETmApp fun' (_oExpr arout)) + $ combineOut funOut arout + +-- | Analyse a type application expression. +genForTyApp :: (GenPhase ph, MonadEnv m ph) + => Bool + -- ^ Flag denoting whether updates should be analysed. + -> Expr + -- ^ The function expression. + -> Type + -- ^ The argument type. + -> m (Output ph) +genForTyApp updFlag expr typ = do + exprOut <- genExpr updFlag expr + case _oExpr exprOut of + ETyLam bndr body -> do + let subst = singleTypeSubst (fst bndr) typ + resExpr = substituteTy subst body + resOut <- genExpr updFlag resExpr + return $ combineOut resOut exprOut + expr' -> return $ updateOutExpr (ETyApp expr' typ) exprOut + +-- | Analyse a let binding expression. +genForLet :: (GenPhase ph, MonadEnv m ph) + => Bool + -- ^ Flag denoting whether updates should be analysed. + -> Binding + -- ^ The binding to be bound. + -> Expr + -- ^ The expression in which the binding should be available. + -> m (Output ph) +genForLet updFlag bind body = do + bindOut <- genExpr updFlag (bindingBound bind) + let subst = singleExprSubst (fst $ bindingBinder bind) (_oExpr bindOut) + resExpr = substituteTm subst body + resOut <- genExpr updFlag resExpr + return $ combineOut resOut bindOut + +-- | Analyse an expression variable. +genForVar :: (GenPhase ph, MonadEnv m ph) + => Bool + -- ^ Flag denoting whether updates should be analysed. + -> ExprVarName + -- ^ The expression variable to be analysed. + -> m (Output ph) +genForVar _updFlag name = lookupVar name >> return (emptyOut (EVar name)) + +-- | Analyse a value reference. +genForVal :: (GenPhase ph, MonadEnv m ph) + => Bool + -- ^ Flag denoting whether updates should be analysed. + -> Qualified ExprValName + -- ^ The value reference to be analysed. + -> m (Output ph) +genForVal _updFlag w = getEnv >>= \case + EnvVG{} -> return $ Output (EVal w) (emptyUpdateSet{_usvgValue = [Determined w]}) + EnvCG{} -> lookupVal w >>= \ (expr, upds) -> return (Output expr upds) + EnvS{} -> error "Impossible: genForVal can't be used in the solving phase" + +-- | Analyse a record projection expression. +genForRecProj :: (GenPhase ph, MonadEnv m ph) + => Bool + -- ^ Flag denoting whether updates should be analysed. + -> TypeConApp + -- ^ The type constructor of the record which is projected. + -> FieldName + -- ^ The field which is projected. + -> Expr + -- ^ The record expression which is projected. + -> m (Output ph) +genForRecProj updFlag tc f body = do + bodyOut <- genExpr updFlag body + case _oExpr bodyOut of + -- TODO: I think we can reduce duplication a bit more here + EVar x -> do + skol <- lookupRec x f + if skol + then return $ updateOutExpr (ERecProj tc f (EVar x)) bodyOut + else error ("Impossible: expected skolem record: " ++ show x ++ "." ++ show f) + expr -> do + fs <- recExpFields expr + case lookup f fs of + Just expr -> genExpr updFlag expr + Nothing -> throwError $ UnknownRecField f + +-- | Analyse a struct projection expression. +genForStructProj :: (GenPhase ph, MonadEnv m ph) + => Bool + -- ^ Flag denoting whether updates should be analysed. + -> FieldName + -- ^ The field which is projected. + -> Expr + -- ^ The record expression which is projected. + -> m (Output ph) +genForStructProj updFlag f body = do + bodyOut <- genExpr updFlag body + case _oExpr bodyOut of + -- TODO: I think we can reduce duplication a bit more here + EVar x -> do + skol <- lookupRec x f + if skol + then return $ updateOutExpr (EStructProj f (EVar x)) bodyOut + else error ("Impossible: expected skolem record: " ++ show x ++ "." ++ show f) + expr -> do + fs <- recExpFields expr + case lookup f fs of + Just expr -> genExpr updFlag expr + Nothing -> throwError $ UnknownRecField f + +-- | Analyse a case expression. +-- TODO: Atm only boolean cases are supported +genForCase :: (GenPhase ph, MonadEnv m ph) + => Bool + -- ^ Flag denoting whether updates should be analysed. + -> Expr + -- ^ The expression to match on. + -> [CaseAlternative] + -- ^ The list of alternatives. + -> m (Output ph) +genForCase updFlag exp cs = do + expOut <- genExpr updFlag exp + case findBool True of + Just tru -> do + truOut <- genExpr updFlag tru + case findBool False of + Just fal -> do + falOut <- genExpr updFlag fal + let resExp = ECase (_oExpr expOut) + [ CaseAlternative (CPBool True) (_oExpr truOut) + , CaseAlternative (CPBool False) (_oExpr falOut) ] + resUpd = _oUpdate expOut `concatUpdateSet` + conditionalUpdateSet (_oExpr expOut) (_oUpdate truOut) (_oUpdate falOut) + return $ Output resExp resUpd + Nothing -> error "Impossible: Missing False-case in if statement" + Nothing -> return $ emptyOut (ECase exp cs) + where + findBool :: Bool -> Maybe Expr + findBool b1 = listToMaybe $ [e | CaseAlternative (CPBool b2) e <- cs, b1 == b2] + +-- | Analyse a create update expression. +-- Returns both the generator output and the return type. +genForCreate :: (GenPhase ph, MonadEnv m ph) + => Qualified TypeConName + -- ^ The template of which a new instance is being created. + -> Expr + -- ^ The argument expression. + -> m (Output ph, Type, Maybe Expr) +genForCreate tem arg = do + arout <- genExpr True arg + fs <- recExpFields (_oExpr arout) + return ( Output (EUpdate (UCreate tem $ _oExpr arout)) $ addUpd emptyUpdateSet (UpdCreate tem fs) + , TCon tem + , Just $ EStructCon fs ) + -- TODO: We could potentially filter here to only store the interesting fields? + +-- | Analyse an exercise update expression. +-- Returns both the generator output and the return type of the choice. +genForExercise :: (GenPhase ph, MonadEnv m ph) + => Qualified TypeConName + -- ^ The template on which a choice is being exercised. + -> ChoiceName + -- ^ The choice which is being exercised. + -> Expr + -- ^ The contract id on which the choice is being exercised. + -> Maybe Expr + -- ^ The party which exercises the choice. + -> Expr + -- ^ The arguments with which the choice is being exercised. + -> m (Output ph, Type, Maybe Expr) +genForExercise tem ch cid par arg = do + cidOut <- genExpr True cid + arout <- genExpr True arg + (updSubst, resType) <- lookupChoice tem ch + this <- fst <$> lookupCid (_oExpr cidOut) + -- TODO: Should we further eval after subst? But how to eval an update set? + let updSet = updSubst (_oExpr cidOut) (EVar this) (_oExpr arout) + return ( Output (EUpdate (UExercise tem ch (_oExpr cidOut) par (_oExpr arout))) updSet + , resType + , Nothing ) -- TODO! + +-- | Analyse a bind update expression. +-- Returns both the generator output and the return type. +genForBind :: (GenPhase ph, MonadEnv m ph) + => Binding + -- ^ The binding being bound with this update. + -> Expr + -- ^ The expression in which this binding is being made available. + -> m (Output ph, Type, Maybe Expr) +genForBind bind body = do + bindOut <- genExpr False (bindingBound bind) + bindUpd <- case _oExpr bindOut of + EUpdate (UFetch tc cid) -> do + bindCids (TContractId (TCon tc)) cid (EVar $ fst $ bindingBinder bind) Nothing + return emptyUpdateSet + EUpdate upd -> do + (updOut, updTyp, creFs) <- genUpdate upd + this <- genRenamedVar (ExprVarName "this") + bindCids updTyp (EVar $ fst $ bindingBinder bind) (EVar this) creFs + return $ _oUpdate updOut + _ -> return emptyUpdateSet + extVarEnv (fst $ bindingBinder bind) + bodyOut <- genExpr False body + case _oExpr bodyOut of + EUpdate bodyUpd -> do + (bodyUpdOut, bodyTyp, creFs) <- genUpdate bodyUpd + return ( Output + (_oExpr bodyUpdOut) + (_oUpdate bindOut + `concatUpdateSet` bindUpd + `concatUpdateSet` _oUpdate bodyOut + `concatUpdateSet` _oUpdate bodyUpdOut) + , bodyTyp + , creFs ) + _ -> error "Impossible: The body of a bind should be an update expression" + +bindCids :: (GenPhase ph, MonadEnv m ph) + => Type + -- ^ The type of the contract id's being bound. + -> Expr + -- ^ The contract id's being bound. + -> Expr + -- ^ The variables to bind them to. + -> Maybe Expr + -- ^ The field values for any created contracts, if available. + -> m () +bindCids (TContractId (TCon tc)) cid (EVar this) fsExp = do + fs <- recTypConFields $ qualObject tc + extRecEnv this (map fst fs) + cidOut <- genExpr True cid + extCidEnv (_oExpr cidOut) this + creFs <- maybe (pure []) recExpFields fsExp + extCtrRec this creFs +bindCids (TCon tc) cid (EVar this) fsExp = do + fs <- recTypConFields $ qualObject tc + extRecEnv this (map fst fs) + cidOut <- genExpr True cid + extCidEnv (_oExpr cidOut) this + creFs <- maybe (pure []) recExpFields fsExp + extCtrRec this creFs +bindCids (TBuiltin BTUnit) _ _ _ = return () +bindCids (TBuiltin BTTimestamp) _ _ _ = return () +-- TODO: Extend additional cases, like tuples. +bindCids typ _ _ _ = + error ("Binding contract id's for this particular type has not been implemented yet: " ++ show typ) diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs new file mode 100644 index 000000000000..9d3cf2a68bb1 --- /dev/null +++ b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs @@ -0,0 +1,77 @@ + +-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + +-- TODO: There is a lot of copying going on here from TsCodeGenMain.hs. +-- A nicer alternative would be to just change the exports from this module. + +-- | Reading dar files for DAML LF verification. +module DA.Daml.LF.Verify.Read + ( readPackages + , optionsParserInfo + , Options(..) + ) where + +import qualified DA.Daml.LF.Proto3.Archive as Archive +import qualified DA.Daml.LF.Reader as DAR +import qualified Data.ByteString as B +import qualified Data.ByteString.Lazy as BSL +import qualified Data.Text.Extended as T +import qualified "zip-archive" Codec.Archive.Zip as Zip +import Control.Monad.Extra +import Options.Applicative + +import DA.Daml.LF.Ast + +data Options = Options + { optInputDar :: FilePath + , optChoiceTmpl :: String + , optChoiceName :: String + , optFieldTmpl :: String + , optFieldName :: String + } + +optionsParser :: Parser Options +optionsParser = Options + <$> argument str + ( metavar "DAR-FILE" + <> help "DAR file to analyse" + ) + <*> argument str + ( metavar "CHOICE-TEMPLATE" + <> help "Template of the choice to analyse" + ) + <*> argument str + ( metavar "CHOICE-NAME" + <> help "Name of the choice to analyse" + ) + <*> argument str + ( metavar "FIELD-TEMPLATE" + <> help "Template of the field to verify" + ) + <*> argument str + ( metavar "FIELD-NAME" + <> help "Name of the field to verify" + ) + +optionsParserInfo :: ParserInfo Options +optionsParserInfo = info (optionsParser <**> helper) + ( fullDesc + <> progDesc "Perform static analysis on a DAR" + ) + +-- Build a list of packages from a list of DAR file paths. +readPackages :: [FilePath] -> IO [(PackageId, (Package, Maybe PackageName))] +readPackages dars = concatMapM darToPackages dars + where + darToPackages :: FilePath -> IO [(PackageId, (Package, Maybe PackageName))] + darToPackages dar = do + dar <- B.readFile dar + let archive = Zip.toArchive $ BSL.fromStrict dar + dalfs <- either fail pure $ DAR.readDalfs archive + DAR.DalfManifest{packageName} <- either fail pure $ DAR.readDalfManifest archive + packageName <- pure (PackageName . T.pack <$> packageName) + forM ((DAR.mainDalf dalfs, packageName) : map (, Nothing) (DAR.dalfs dalfs)) $ + \(dalf, mbPkgName) -> do + (pkgId, pkg) <- either (fail . show) pure $ Archive.decodeArchive Archive.DecodeAsMain (BSL.toStrict dalf) + pure (pkgId, (pkg, mbPkgName)) diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs new file mode 100644 index 000000000000..f1b2b9ef3673 --- /dev/null +++ b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs @@ -0,0 +1,402 @@ +-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + +{-# LANGUAGE DataKinds #-} + +-- | Constraint solver for DAML LF static verification +module DA.Daml.LF.Verify.Solve + ( constructConstr + , solveConstr + , ConstraintSet(..) + , Result(..) + ) where + +import Data.Bifunctor +import Data.Maybe +import Data.List +import Data.List.Extra (nubOrd) +import Data.Tuple.Extra (both) +import Data.Text.Prettyprint.Doc +import qualified Data.HashMap.Strict as HM +import qualified Data.Text as T +import qualified SimpleSMT as S + +import DA.Daml.LF.Ast.Base +import DA.Daml.LF.Ast.Numeric +import DA.Daml.LF.Verify.Context + +-- TODO: Since S.SExpr is so similar, we could just drop this. +-- | A simple form of expressions featuring basic arithmetic. +data ConstraintExpr + -- | Boolean value. + = CBool !Bool + -- | Integer value. + | CInt !Integer + -- | Real value. + | CReal !Rational + -- | Reference to an expression variable. + | CVar !ExprVarName + -- | Sum of two expressions. + | CAdd !ConstraintExpr !ConstraintExpr + -- | Subtraction of two expressions. + | CSub !ConstraintExpr !ConstraintExpr + -- | Equals operator. + | CEq !ConstraintExpr !ConstraintExpr + -- | Boolean and operator. + | CAnd !ConstraintExpr !ConstraintExpr + -- | Boolean not operator. + | CNot !ConstraintExpr + -- | If then else expression. + | CIf !ConstraintExpr !ConstraintExpr !ConstraintExpr + deriving Show + +instance Pretty ConstraintExpr where + pretty (CBool b) = pretty b + pretty (CInt i) = pretty i + pretty (CReal i) = pretty $ show i + pretty (CVar x) = pretty $ unExprVarName x + pretty (CAdd e1 e2) = pretty e1 <+> " <+> " <+> pretty e2 + pretty (CSub e1 e2) = pretty e1 <+> " - " <+> pretty e2 + pretty (CEq e1 e2) = pretty e1 <+> " == " <+> pretty e2 + pretty (CAnd e1 e2) = pretty e1 <+> " and " <+> pretty e2 + pretty (CNot e) = "not " <+> pretty e + pretty (CIf e1 e2 e3) = "if " <+> pretty e1 <+> " then " <+> pretty e2 + <+> " else " <+> pretty e3 + +-- | Add a bunch of constraint expressions. +addMany :: [ConstraintExpr] -> ConstraintExpr +addMany [] = CReal 0.0 +addMany [x] = x +addMany (x:xs) = CAdd x (addMany xs) + +-- | Class covering the types convertible to constraint expressions. +class ConstrExpr a where + -- | Convert the given data type to a constraint expression. + toCExp :: [(ExprVarName, ExprVarName)] + -- ^ The contract name synonyms, along with their current alias. + -> a + -- ^ The data to convert to a constraint expression. + -> ConstraintExpr + +instance ConstrExpr BoolExpr where + toCExp syns (BExpr e) = toCExp syns e + toCExp syns (BAnd b1 b2) = CAnd (toCExp syns b1) (toCExp syns b2) + toCExp syns (BNot b) = CNot (toCExp syns b) + +instance ConstrExpr Expr where + toCExp syns (EVar x) = case lookup x syns of + Just y -> CVar y + Nothing -> CVar x + toCExp syns (ERecProj _ f (EVar x)) = case lookup x syns of + Just y -> CVar $ recProj2Var y f + Nothing -> CVar $ recProj2Var x f + toCExp syns (EStructProj f (EVar x)) = case lookup x syns of + Just y -> CVar $ recProj2Var y f + Nothing -> CVar $ recProj2Var x f + toCExp syns (ETmApp (ETmApp op e1) e2) = case op of + (EBuiltin (BEEqual _)) -> CEq (toCExp syns e1) (toCExp syns e2) + (EBuiltin BEAddInt64) -> CAdd (toCExp syns e1) (toCExp syns e2) + (EBuiltin BESubInt64) -> CSub (toCExp syns e1) (toCExp syns e2) + (ETyApp (EBuiltin BEAddNumeric) _) -> CAdd (toCExp syns e1) (toCExp syns e2) + (ETyApp (EBuiltin BESubNumeric) _) -> CSub (toCExp syns e1) (toCExp syns e2) + (ETmApp (ETyApp (EVal (Qualified _ _ (ExprValName "+"))) _) _) -> + CAdd (toCExp syns e1) (toCExp syns e2) + (ETmApp (ETyApp (EVal (Qualified _ _ (ExprValName "-"))) _) _) -> + CSub (toCExp syns e1) (toCExp syns e2) + _ -> error ("Builtin: " ++ show op) + toCExp syns (ELocation _ e) = toCExp syns e + toCExp _syns (EBuiltin (BEBool b)) = CBool b + toCExp _syns (EBuiltin (BEInt64 i)) = CInt $ toInteger i + toCExp _syns (EBuiltin (BENumeric i)) = CReal $ toRational $ numericDecimal i + toCExp _syns e = error ("Conversion: " ++ show e) + +instance ConstrExpr a => ConstrExpr (Cond a) where + toCExp syns (Determined x) = toCExp syns x + -- TODO: Can we assume this should always be a sum? + toCExp syns (Conditional b x y) = CIf (toCExp syns b) + (addMany $ map (toCExp syns) x) + (addMany $ map (toCExp syns) y) + +-- | Gather all free variables in a constraint expression. +gatherFreeVars :: ConstraintExpr + -- ^ The constraint expression to traverse. + -> [ExprVarName] +gatherFreeVars (CBool _) = [] +gatherFreeVars (CInt _) = [] +gatherFreeVars (CReal _) = [] +gatherFreeVars (CVar x) = [x] +gatherFreeVars (CAdd e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 +gatherFreeVars (CSub e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 +gatherFreeVars (CEq e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 +gatherFreeVars (CAnd e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 +gatherFreeVars (CNot e) = gatherFreeVars e +gatherFreeVars (CIf e1 e2 e3) = gatherFreeVars e1 `union` + gatherFreeVars e2 `union` gatherFreeVars e3 + +-- | Gather the variable names bound within a skolem variable. +skol2var :: Skolem + -- ^ The skolem variable to handle. + -> [ExprVarName] +skol2var (SkolVar x) = [x] +skol2var (SkolRec x fs) = map (recProj2Var x) fs + +-- | Squash a record projection into a single variable name. +recProj2Var :: ExprVarName + -- ^ The variable on which is being projected. + -> FieldName + -- ^ The field name which is being projected. + -> ExprVarName +recProj2Var (ExprVarName x) (FieldName f) = ExprVarName (x `T.append` "." `T.append` f) + +-- | The set of constraints to be solved. +data ConstraintSet = ConstraintSet + { _cVars :: ![ExprVarName] + -- ^ The variables to be declared. + , _cCres :: ![ConstraintExpr] + -- ^ The field values of all newly created contracts. + , _cArcs :: ![ConstraintExpr] + -- ^ The field values of all archived contracts. + , _cCtrs :: ![(ConstraintExpr, ConstraintExpr)] + -- ^ Additional equality constraints. + } + deriving Show + +-- | Filters a single update to match the given template, and takes out the +-- field of interest. The update gets converted into a constraint expression. +-- It returns either a create or an archive update. +filterUpd :: Qualified TypeConName + -- ^ The template name to filter against. + -> [(ExprVarName, ExprVarName)] + -- ^ The contract name synonyms, along with their current alias. + -> FieldName + -- ^ The field name to be verified. + -> Upd + -- ^ The update expression to convert and filter. + -> (Maybe ConstraintExpr, Maybe ConstraintExpr) +filterUpd tem syns f UpdCreate{..} = if tem == _creTemp + then (Just (toCExp syns $ fromJust $ lookup f _creField), Nothing) + else (Nothing, Nothing) +filterUpd tem syns f UpdArchive{..} = if tem == _arcTemp + then (Nothing, Just (toCExp syns $ fromJust $ lookup f _arcField)) + else (Nothing, Nothing) + +-- | Filters and converts a conditional update into (possibly two) constraint +-- expressions, while splitting it into create and archive updates. +filterCondUpd :: Qualified TypeConName + -- ^ The template name to filter against + -> [(ExprVarName, ExprVarName)] + -- ^ The contract name synonyms, along with their current alias. + -> FieldName + -- ^ The field name to be verified. + -> Cond Upd + -- ^ The conditional update expression to convert and filter. + -> ([ConstraintExpr], [ConstraintExpr]) +filterCondUpd tem syns f (Determined x) = both maybeToList $ filterUpd tem syns f x +filterCondUpd tem syns f (Conditional b xs ys) = + let cb = toCExp syns b + (cxcre,cxarc) = both (addMany . concat) $ unzip $ map (filterCondUpd tem syns f) xs + (cycre,cyarc) = both (addMany . concat) $ unzip $ map (filterCondUpd tem syns f) ys + in ( [CIf cb cxcre cycre] + , [CIf cb cxarc cyarc] ) + +-- | Filter the given set of skolems, to only include those that occur in the +-- given constraint expressions. Remove duplicates in the process. +filterVars :: [ExprVarName] + -- ^ The list of skolems to filter. + -> [ConstraintExpr] + -- ^ The constraint expressions in which the skolems should occur. + -> [ExprVarName] +filterVars vars cexprs = + let freevars = foldl' (\fv e -> fv `union` gatherFreeVars e) [] cexprs + in freevars `intersect` vars + +-- | Construct a list of all contract name synonyms, along with their current +-- alias. +constructSynonyms :: [(ExprVarName, [ExprVarName])] + -- ^ The current contract names, along with any previous synonyms. + -> [(ExprVarName, ExprVarName)] +constructSynonyms = foldl step [] + where + step :: [(ExprVarName, ExprVarName)] -> (ExprVarName, [ExprVarName]) + -> [(ExprVarName, ExprVarName)] + step acc (cur, prevs) = acc ++ map (, cur) prevs + +-- | Constructs a constraint set from the generator environment, together with +-- the template name, the choice and field to be verified. +constructConstr :: Env 'Solving + -- ^ The generator environment to convert. + -> Qualified TypeConName + -- ^ The template name of the choice to be verified. + -> ChoiceName + -- ^ The choice name to be verified. + -> Qualified TypeConName + -- ^ The template name of the field to be verified. + -> FieldName + -- ^ The field name to be verified. + -> ConstraintSet +constructConstr env chtem ch ftem f = + case HM.lookup (UpdChoice chtem ch) (_envschs env) of + Just ChoiceData{..} -> + let upds = _ussUpdate $ _cdUpds (EVar _cdSelf) (EVar _cdThis) (EVar _cdArgs) + vars = concatMap skol2var (_envsskol env) + syns = constructSynonyms $ HM.elems $ _envscids env + ctrs = map (both (toCExp syns)) $ _envsctrs env + (cres, arcs) = foldl + (\(cs,as) upd -> let (cs',as') = filterCondUpd ftem syns f upd in (cs ++ cs',as ++ as')) + ([],[]) upds + in ConstraintSet vars cres arcs ctrs + Nothing -> error ("Choice not found " ++ show ch) + +-- | Convert a constraint expression into an SMT expression from the solving library. +cexp2sexp :: [(ExprVarName,S.SExpr)] + -- ^ The set of variable names, mapped to their corresponding SMT counterparts. + -> ConstraintExpr + -- ^ The constraint expression to convert. + -> IO S.SExpr +cexp2sexp _vars (CBool b) = return $ S.bool b +cexp2sexp _vars (CInt i) = return $ S.int i +cexp2sexp _vars (CReal i) = return $ S.real i +cexp2sexp vars (CVar x) = case lookup x vars of + Just exp -> return exp + Nothing -> error ("Impossible: variable not found " ++ show x) +cexp2sexp vars (CAdd ce1 ce2) = do + se1 <- cexp2sexp vars ce1 + se2 <- cexp2sexp vars ce2 + return $ S.add se1 se2 +cexp2sexp vars (CSub ce1 ce2) = do + se1 <- cexp2sexp vars ce1 + se2 <- cexp2sexp vars ce2 + return $ S.sub se1 se2 +cexp2sexp vars (CEq ce1 ce2) = do + se1 <- cexp2sexp vars ce1 + se2 <- cexp2sexp vars ce2 + return $ S.eq se1 se2 +cexp2sexp vars (CAnd ce1 ce2) = do + se1 <- cexp2sexp vars ce1 + se2 <- cexp2sexp vars ce2 + return $ S.and se1 se2 +cexp2sexp vars (CNot ce) = do + se <- cexp2sexp vars ce + return $ S.not se +cexp2sexp vars (CIf ce1 ce2 ce3) = do + se1 <- cexp2sexp vars ce1 + se2 <- cexp2sexp vars ce2 + se3 <- cexp2sexp vars ce3 + return $ S.ite se1 se2 se3 + +-- | Declare a list of variables for the SMT solver. Returns a list of the +-- declared variables, together with their corresponding SMT counterparts. +declareVars :: S.Solver + -- ^ The SMT solver. + -> [ExprVarName] + -- ^ The variables to be declared. + -> IO [(ExprVarName,S.SExpr)] +declareVars s xs = zip xs <$> mapM (\x -> S.declare s (var2str x) S.tReal) xs + where + var2str :: ExprVarName -> String + var2str (ExprVarName x) = T.unpack x + +-- | Assert the additional equality constraints. Binds and returns any +-- additional required variables. +declareCtrs :: S.Solver + -- ^ The SMT solver. + -> (String -> IO ()) + -- ^ Function for debugging printouts. + -> [(ExprVarName,S.SExpr)] + -- ^ The set of variable names, mapped to their corresponding SMT counterparts. + -> [(ConstraintExpr, ConstraintExpr)] + -- ^ The equality constraints to be declared. + -> IO [(ExprVarName,S.SExpr)] +declareCtrs sol debug cvars1 ctrs = do + let edges = map (\(l,r) -> (l,r,gatherFreeVars l ++ gatherFreeVars r)) ctrs + components = conn_comp edges + useful_nodes = map fst cvars1 + useful_components = filter + (\comp -> let comp_vars = concatMap (\(_,_,vars) -> vars) comp + in not $ null $ intersect comp_vars useful_nodes) + components + useful_equalities = concatMap (map (\(l,r,_) -> (l,r))) useful_components + required_vars = + nubOrd (concatMap (concatMap (\(_,_,vars) -> vars)) useful_components) + \\ useful_nodes + cvars2 <- declareVars sol required_vars + mapM_ (declare $ cvars1 ++ cvars2) useful_equalities + return cvars2 + where + -- | Compute connected components of the equality constraints graph. + -- Two edges are adjacent when at least one of their nodes shares a variable. + conn_comp :: [(ConstraintExpr,ConstraintExpr,[ExprVarName])] + -- ^ The edges of the graph, annotated with the contained variables. + -> [[(ConstraintExpr,ConstraintExpr,[ExprVarName])]] + conn_comp [] = [] + conn_comp (edge:edges) = let (comp,rem) = cc_step edges edge + in comp : conn_comp rem + + -- | Compute the strongly connected component containing a given edge from + -- the graph, as well as the remaining edges which do not belong to this + -- component. + cc_step :: [(ConstraintExpr,ConstraintExpr,[ExprVarName])] + -- ^ The edges of the graph, which do not yet belong to any component. + -> (ConstraintExpr,ConstraintExpr,[ExprVarName]) + -- ^ The current edge for which the component is being computed. + -> ( [(ConstraintExpr,ConstraintExpr,[ExprVarName])] + -- ^ The computed connected component. + , [(ConstraintExpr,ConstraintExpr,[ExprVarName])] ) + -- ^ The remaining edges which do not belong to the connected component. + cc_step [] _ = ([],[]) + cc_step edges0 (l,r,vars) = + let (neighbors,edges1) = partition (\(_,_,vars') -> not $ null $ intersect vars vars') edges0 + in foldl (\(conn,edges2) edge -> first (conn ++) $ cc_step edges2 edge) + ((l,r,vars):neighbors,edges1) neighbors + + declare :: [(ExprVarName,S.SExpr)] -> (ConstraintExpr, ConstraintExpr) -> IO () + declare vars (cexp1, cexp2) = do + sexp1 <- cexp2sexp vars cexp1 + sexp2 <- cexp2sexp vars cexp2 + debug ("Assert: " ++ S.ppSExpr sexp1 (" = " ++ S.ppSExpr sexp2 "")) + S.assert sol (sexp1 `S.eq` sexp2) + +-- | Data type denoting the outcome of the solver. +data Result + = Success + -- ^ The total field amount remains preserved. + | Fail [(S.SExpr, S.Value)] + -- ^ The total field amound does not remain the same. A counter example is + -- provided. + | Unknown + -- ^ The result is inconclusive. + deriving Eq + +instance Show Result where + show Success = "Success!" + show (Fail cs) = "Fail. Counter example:" ++ foldl (flip step) "" cs + where + step :: (S.SExpr, S.Value) -> String -> String + step (var, val) str = ("\n" ++) $ S.ppSExpr var $ (" = " ++) $ S.ppSExpr (S.value val) str + show Unknown = "Inconclusive." + +-- | Solve a give constraint set. Prints 'unsat' when the constraint set is +-- valid. It asserts that the set of created and archived contracts are not +-- equal. +solveConstr :: FilePath + -- ^ The path to the constraint solver. + -> (String -> IO ()) + -- ^ Function for debugging printouts. + -> ConstraintSet + -- ^ The constraint set to solve. + -> IO Result +solveConstr spath debug ConstraintSet{..} = do + log <- S.newLogger 1 + sol <- S.newSolver spath ["-in"] (Just log) + vars1 <- declareVars sol $ filterVars _cVars (_cCres ++ _cArcs) + vars2 <- declareCtrs sol debug vars1 _cCtrs + let vars = vars1 ++ vars2 + cre <- foldl S.add (S.real 0.0) <$> mapM (cexp2sexp vars) _cCres + arc <- foldl S.add (S.real 0.0) <$> mapM (cexp2sexp vars) _cArcs + S.assert sol (S.not (cre `S.eq` arc)) + S.check sol >>= \case + S.Sat -> do + counter <- S.getExprs sol $ map snd vars + return $ Fail counter + S.Unsat -> return Success + S.Unknown -> return Unknown diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Subst.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Subst.hs new file mode 100644 index 000000000000..32929048fbaf --- /dev/null +++ b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Subst.hs @@ -0,0 +1,211 @@ +-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + +-- | Term substitions for DAML LF static verification +module DA.Daml.LF.Verify.Subst + ( ExprSubst + , singleExprSubst + , singleTypeSubst + , createExprSubst + , SubstTm(..) + , SubstTy(..) + , InstPR(..) + ) where + +import Control.Lens hiding (Context) +import qualified Data.Map.Strict as Map +import DA.Daml.LF.Ast +import DA.Daml.LF.Ast.Type + +-- | Substitution of expressions for expression variables. +type ExprSubst = Map.Map ExprVarName Expr + +-- | Create an expression substitution from a single variable and expression. +singleExprSubst :: ExprVarName + -- ^ The expression variable to substitute. + -> Expr + -- ^ The expression to substitute with. + -> ExprSubst +singleExprSubst = Map.singleton + +-- | Create a type substitution from a single type variable and type. +singleTypeSubst :: TypeVarName + -- ^ The type variable to substitute. + -> Type + -- ^ The type to substitute with. + -> Subst +singleTypeSubst = Map.singleton + +-- | Create an expression substitution from a list of variables and expressions. +createExprSubst :: [(ExprVarName,Expr)] + -- ^ The variables to substitute, together with the expressions to replace them with. + -> ExprSubst +createExprSubst = Map.fromList + +-- | Get the domain from an expression substitution. +substDom :: ExprSubst + -- ^ The substitution to analyse. + -> [ExprVarName] +substDom = Map.keys + +-- | A class covering the data types to which an expression substitution can be applied. +class SubstTm a where + -- | Apply an expression substitution. + substituteTm :: ExprSubst + -- ^ The expression substitution to apply. + -> a + -- ^ The data to apply the substitution to. + -> a + +-- | A class covering the data types to which a type substitution can be applied. +class SubstTy a where + -- | Apply an type substitution. + substituteTy :: Subst + -- ^ The type substitution to apply. + -> a + -- ^ The data to apply the substitution to. + -> a + +-- TODO: We assume that for any substitution x |-> e : x notin e +-- and a |-> t : a notin t. +instance SubstTm Expr where + substituteTm s = \case + EVar x + | Just e <- Map.lookup x s -> e + | otherwise -> EVar x + ERecCon t fs -> ERecCon t $ map (over _2 (substituteTm s)) fs + ERecProj t f e -> ERecProj t f $ substituteTm s e + ERecUpd t f e1 e2 -> ERecUpd t f (substituteTm s e1) (substituteTm s e2) + EVariantCon t v e -> EVariantCon t v (substituteTm s e) + EStructCon fs -> EStructCon $ map (over _2 (substituteTm s)) fs + EStructProj f e -> EStructProj f (substituteTm s e) + EStructUpd f e1 e2 -> EStructUpd f (substituteTm s e1) (substituteTm s e2) + ETmApp e1 e2 -> ETmApp (substituteTm s e1) (substituteTm s e2) + ETyApp e t -> ETyApp (substituteTm s e) t + ETmLam (x,t) e -> if x `elem` substDom s + then ETmLam (x,t) e + else ETmLam (x,t) (substituteTm s e) + ETyLam (a,k) e -> ETyLam (a,k) (substituteTm s e) + ECase e cs -> ECase (substituteTm s e) + $ map (\CaseAlternative{..} -> CaseAlternative altPattern (substituteTm s altExpr)) cs + ELet Binding{..} e -> ELet (Binding bindingBinder $ substituteTm s bindingBound) + (substituteTm s e) + ECons t e1 e2 -> ECons t (substituteTm s e1) (substituteTm s e2) + ESome t e -> ESome t (substituteTm s e) + EToAny t e -> EToAny t (substituteTm s e) + EFromAny t e -> EFromAny t (substituteTm s e) + EUpdate u -> EUpdate $ substituteTm s u + ELocation l e -> ELocation l (substituteTm s e) + e -> e + +instance SubstTm Update where + substituteTm s = \case + UPure t e -> UPure t $ substituteTm s e + UBind Binding{..} e -> UBind (Binding bindingBinder $ substituteTm s bindingBound) + (substituteTm s e) + UCreate t e -> UCreate t $ substituteTm s e + UExercise t c e1 a e2 -> UExercise t c (substituteTm s e1) a (substituteTm s e2) + UFetch t e -> UFetch t $ substituteTm s e + UEmbedExpr t e -> UEmbedExpr t $ substituteTm s e + u -> u + +instance SubstTm a => SubstTm (Maybe a) where + substituteTm s m = substituteTm s <$> m + +instance SubstTy Expr where + substituteTy s = \case + ERecCon t fs -> ERecCon (substituteTy s t) $ map (over _2 (substituteTy s)) fs + ERecProj t f e -> ERecProj (substituteTy s t) f $ substituteTy s e + ERecUpd t f e1 e2 -> ERecUpd (substituteTy s t) f (substituteTy s e1) + (substituteTy s e2) + EVariantCon t v e -> EVariantCon (substituteTy s t) v (substituteTy s e) + EStructCon fs -> EStructCon $ map (over _2 (substituteTy s)) fs + EStructProj f e -> EStructProj f $ substituteTy s e + EStructUpd f e1 e2 -> EStructUpd f (substituteTy s e1) (substituteTy s e2) + ETmApp e1 e2 -> ETmApp (substituteTy s e1) (substituteTy s e2) + ETyApp e t -> ETyApp (substituteTy s e) (substitute s t) + ETmLam (n, t) e -> ETmLam (n, substitute s t) (substituteTy s e) + ETyLam b e -> ETyLam b $ substituteTy s e + ECase e cs -> ECase (substituteTy s e) (map (substituteTy s) cs) + ELet Binding{..} e -> ELet (Binding (over _2 (substitute s) bindingBinder) (substituteTy s bindingBound)) + (substituteTy s e) + ENil t -> ENil (substitute s t) + ECons t e1 e2 -> ECons (substitute s t) (substituteTy s e1) (substituteTy s e2) + ESome t e -> ESome (substitute s t) (substituteTy s e) + ENone t -> ENone (substitute s t) + EToAny t e -> EToAny (substitute s t) (substituteTy s e) + EFromAny t e -> EFromAny (substitute s t) (substituteTy s e) + ETypeRep t -> ETypeRep (substitute s t) + EUpdate u -> EUpdate (substituteTy s u) + ELocation l e -> ELocation l (substituteTy s e) + e -> e + +instance SubstTy Update where + substituteTy s = \case + UPure t e -> UPure (substitute s t) (substituteTy s e) + UBind Binding{..} e -> UBind (Binding (over _2 (substitute s) bindingBinder) (substituteTy s bindingBound)) + (substituteTy s e) + UCreate n e -> UCreate n (substituteTy s e) + UExercise n c e1 a e2 -> UExercise n c (substituteTy s e1) a (substituteTy s e2) + UFetch n e -> UFetch n (substituteTy s e) + UEmbedExpr t e -> UEmbedExpr (substitute s t) (substituteTy s e) + u -> u + +instance SubstTy TypeConApp where + substituteTy s (TypeConApp n ts) = TypeConApp n (map (substitute s) ts) + +instance SubstTy CaseAlternative where + substituteTy s (CaseAlternative p e) = CaseAlternative p (substituteTy s e) + +-- | A class covering the data types containing package references which can be +-- instantiated.. +class InstPR a where + -- | Instantiate `PRSelf` with the given package reference. + instPRSelf :: PackageRef + -- ^ The package reference to substitute with. + -> a + -- ^ The data type to substitute in. + -> a + +instance InstPR (Qualified a) where + instPRSelf pac qx@(Qualified pac' mod x) = case pac' of + PRSelf -> Qualified pac mod x + _ -> qx + +instance InstPR Expr where + instPRSelf pac = \case + EVal val -> EVal (instPRSelf pac val) + ERecCon t fs -> ERecCon t $ map (over _2 (instPRSelf pac)) fs + ERecProj t f e -> ERecProj t f $ instPRSelf pac e + ERecUpd t f e1 e2 -> ERecUpd t f (instPRSelf pac e1) (instPRSelf pac e2) + EVariantCon t v e -> EVariantCon t v (instPRSelf pac e) + EStructCon fs -> EStructCon $ map (over _2 (instPRSelf pac)) fs + EStructProj f e -> EStructProj f (instPRSelf pac e) + EStructUpd f e1 e2 -> EStructUpd f (instPRSelf pac e1) (instPRSelf pac e2) + ETmApp e1 e2 -> ETmApp (instPRSelf pac e1) (instPRSelf pac e2) + ETyApp e t -> ETyApp (instPRSelf pac e) t + ETmLam b e -> ETmLam b (instPRSelf pac e) + ETyLam b e -> ETyLam b (instPRSelf pac e) + ECase e cs -> ECase (instPRSelf pac e) + $ map (\CaseAlternative{..} -> CaseAlternative altPattern (instPRSelf pac altExpr)) cs + ELet Binding{..} e -> ELet (Binding bindingBinder $ instPRSelf pac bindingBound) + (instPRSelf pac e) + ECons t e1 e2 -> ECons t (instPRSelf pac e1) (instPRSelf pac e2) + ESome t e -> ESome t (instPRSelf pac e) + EToAny t e -> EToAny t (instPRSelf pac e) + EFromAny t e -> EFromAny t (instPRSelf pac e) + EUpdate u -> EUpdate $ instPRSelf pac u + ELocation l e -> ELocation l (instPRSelf pac e) + e -> e + +instance InstPR Update where + instPRSelf pac = \case + UPure t e -> UPure t (instPRSelf pac e) + UBind Binding{..} e -> UBind (Binding bindingBinder $ instPRSelf pac bindingBound) + (instPRSelf pac e) + UCreate tem arg -> UCreate (instPRSelf pac tem) (instPRSelf pac arg) + UExercise tem ch cid act arg -> UExercise (instPRSelf pac tem) ch + (instPRSelf pac cid) (instPRSelf pac <$> act) (instPRSelf pac arg) + UFetch tem cid -> UFetch (instPRSelf pac tem) (instPRSelf pac cid) + UEmbedExpr t e -> UEmbedExpr t (instPRSelf pac e) + u -> u diff --git a/compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs b/compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs new file mode 100644 index 000000000000..e8a8fada5859 --- /dev/null +++ b/compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs @@ -0,0 +1,98 @@ +-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + +module DA.Daml.LF.Verify.Tests + ( mainTest + ) where + +import System.FilePath +import Test.Tasty +import Test.Tasty.HUnit + +import DA.Daml.LF.Ast.Base +import DA.Daml.LF.Verify +import DA.Daml.LF.Verify.Solve +import DA.Bazel.Runfiles + +mainTest :: IO () +mainTest = defaultMain $ testGroup "DA.Daml.LF.Verify" + [ quickstartTests + , conditionalTests + ] + +quickstartTests :: TestTree +quickstartTests = testGroup "Quickstart" + [ testCase "Iou_Split" $ do + quickstartDar <- locateRunfiles (mainWorkspace "compiler/daml-lf-verify/quickstart.dar") + let tmpl = TypeConName ["Iou"] + choice = ChoiceName "Iou_Split" + field = FieldName "amount" + result <- verify quickstartDar debug tmpl choice tmpl field + assertEqual "Verification failed for Iou_Split - amount" + Success result + , testCase "Iou_Merge" $ do + quickstartDar <- locateRunfiles (mainWorkspace "compiler/daml-lf-verify/quickstart.dar") + let tmpl = TypeConName ["Iou"] + choice = ChoiceName "Iou_Merge" + field = FieldName "amount" + result <- verify quickstartDar debug tmpl choice tmpl field + assertEqual "Verification failed for Iou_Merge - amount" + Success result + ] + +conditionalTests :: TestTree +conditionalTests = testGroup "Conditionals" + [ testCase "Success A" $ do + condDar <- locateRunfiles (mainWorkspace "compiler/daml-lf-verify/conditionals.dar") + let tmpl = TypeConName ["Iou"] + choice = ChoiceName "SuccA" + field = FieldName "content" + result <- verify condDar debug tmpl choice tmpl field + assertEqual "Verification failed for SuccA - content" + Success result + , testCase "Success B" $ do + condDar <- locateRunfiles (mainWorkspace "compiler/daml-lf-verify/conditionals.dar") + let tmpl = TypeConName ["Iou"] + choice = ChoiceName "SuccB" + field = FieldName "content" + result <- verify condDar debug tmpl choice tmpl field + assertEqual "Verification failed for SuccB - content" + Success result + , testCase "Success C" $ do + condDar <- locateRunfiles (mainWorkspace "compiler/daml-lf-verify/conditionals.dar") + let tmpl = TypeConName ["Iou"] + choice = ChoiceName "SuccC" + field = FieldName "content" + result <- verify condDar debug tmpl choice tmpl field + assertEqual "Verification failed for SuccC - content" + Success result + , testCase "Success D" $ do + condDar <- locateRunfiles (mainWorkspace "compiler/daml-lf-verify/conditionals.dar") + let tmpl = TypeConName ["Iou"] + choice = ChoiceName "SuccD" + field = FieldName "content" + result <- verify condDar debug tmpl choice tmpl field + assertEqual "Verification failed for SuccD - content" + Success result + , testCase "Fail A" $ do + condDar <- locateRunfiles (mainWorkspace "compiler/daml-lf-verify/conditionals.dar") + let tmpl = TypeConName ["Iou"] + choice = ChoiceName "FailA" + field = FieldName "content" + verify condDar debug tmpl choice tmpl field >>= \case + Success -> assertFailure "Verification wrongfully passed for FailA - content" + Unknown -> assertFailure "Verification inconclusive for FailA - content" + Fail _ -> return () + , testCase "Fail B" $ do + condDar <- locateRunfiles (mainWorkspace "compiler/daml-lf-verify/conditionals.dar") + let tmpl = TypeConName ["Iou"] + choice = ChoiceName "FailB" + field = FieldName "content" + verify condDar debug tmpl choice tmpl field >>= \case + Success -> assertFailure "Verification wrongfully passed for FailB - content" + Unknown -> assertFailure "Verification inconclusive for FailB - content" + Fail _ -> return () + ] + +debug :: String -> IO () +debug _ = return () diff --git a/nix/bazel.nix b/nix/bazel.nix index 1e8deb421345..bf935abf9c2f 100644 --- a/nix/bazel.nix +++ b/nix/bazel.nix @@ -116,6 +116,8 @@ let shared = rec { ; }; + z3 = pkgs.z3; + bazel-cc-toolchain = pkgs.callPackage ./tools/bazel-cc-toolchain {}; }; in shared // (if pkgs.stdenv.isLinux then { diff --git a/stack-snapshot.yaml b/stack-snapshot.yaml index 588cce2aee03..01ab7e78949e 100644 --- a/stack-snapshot.yaml +++ b/stack-snapshot.yaml @@ -28,6 +28,7 @@ packages: - regex-base-0.94.0.0 - regex-tdfa-1.3.1.0 - shake-0.18.5 + - simple-smt-0.9.4 # Core packages, need to be listed for integer-simple flags. - integer-simple-0.1.1.1 - text-1.2.3.1