Draft version constraint generation

digital-asset · Gertjan423 · May 20, 2020 · Apr 7, 2020 · Apr 8, 2020 · Apr 9, 2020
commit 040ef56c4239ceaad510d8427df32a3a3a28b11b
diff --git a/compiler/daml-lf-verify/BUILD.bazel b/compiler/daml-lf-verify/BUILD.bazel
@@ -0,0 +1,41 @@
+# Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+load("//bazel_tools:haskell.bzl", "da_haskell_library")
+
+da_haskell_library(
+    name = "daml-lf-verify",
+    srcs = glob(["src/**/*.hs"]),
+    hackage_deps = [
+        "aeson",
+        "base",
+        "bytestring",
+        "containers",
+        "deepseq",
+        "Decimal",
+        "extra",
+        "filepath",
+        "ghc-lib-parser",
+        "hashable",
+        "lens",
+        "mtl",
+        "optparse-applicative",
+        "recursion-schemes",
+        "safe",
+        "scientific",
+        "template-haskell",
+        "text",
+        "time",
+        "unordered-containers",
+        "zip-archive",
+    ],
+    src_strip_prefix = "src",
+    visibility = ["//visibility:public"],
+    deps = [
+        "//compiler/daml-lf-ast",
+        "//compiler/daml-lf-tools",
+        "//compiler/daml-lf-proto",
+        "//compiler/daml-lf-reader",
+        "//libs-haskell/da-hs-base",
+    ],
+)
diff --git a/compiler/daml-lf-verify/daml-lf-verify.cabal b/compiler/daml-lf-verify/daml-lf-verify.cabal
@@ -0,0 +1,57 @@
+cabal-version: 2.4
+name: daml-lf-verify
+build-type: Simple
+version: 0.1.0
+synopsis: DAML-LF Verification
+license: Apache-2.0
+author: Digital Asset
+maintainer: Digital Asset
+copyright: Digital Asset 2020
+homepage: https://github.com/digital-asset/daml#readme
+bug-reports: https://github.com/digital-asset/daml/issues
+
+source-repository head
+    type: git
+    location: https://github.com/digital-asset/daml.git
+
+library
+    default-language: Haskell2010
+    hs-source-dirs: src
+    build-depends:
+      base,
+      containers,
+      da-hs-base,
+      daml-lf-ast,
+      deepseq,
+      extra,
+      hashable,
+      lens,
+      mtl,
+      recursion-schemes,
+      safe,
+      scientific,
+      template-haskell,
+      text,
+      time,
+      unordered-containers
+    exposed-modules:
+      DA.Daml.LF.Verify
+      DA.Daml.LF.Verify.Generate
+    default-extensions:
+      BangPatterns
+      DeriveDataTypeable
+      DeriveFoldable
+      DeriveFunctor
+      DeriveGeneric
+      DeriveTraversable
+      FlexibleContexts
+      GeneralizedNewtypeDeriving
+      LambdaCase
+      NamedFieldPuns
+      PackageImports
+      OverloadedStrings
+      RecordWildCards
+      ScopedTypeVariables
+      StandaloneDeriving
+      TypeApplications
+      ViewPatterns
diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs
@@ -0,0 +1,22 @@
+-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+-- | Static verification of DAML packages.
+module DA.Daml.LF.Verify
+  ( module LF
+  , main
+  ) where
+
+import Options.Applicative
+
+import DA.Daml.LF.Verify.Generate as LF
+import DA.Daml.LF.Verify.Read as LF
+import DA.Daml.LF.Verify.Context as LF
+
+main :: IO ()
+main = do
+  Options{..} <- execParser optionsParserInfo
+  pkgs <- readPackages optInputDars
+  let _delta = runDelta $ genPackages pkgs
+  putStrLn "Constraints generated."
+
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
@@ -0,0 +1,138 @@
+-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+-- | Contexts for DAML LF static verification
+module DA.Daml.LF.Verify.Context
+  ( Delta
+  , MonadDelta, devars, devals
+  , UpdateSet(..)
+  , UpdCreate(..), usCre, usArc, usCho
+  , UpdArchive(..)
+  , UpdChoice(..)
+  , runDelta
+  , emptyDelta
+  , introDelta, extVarDelta
+  , lookupDExprVar, lookupDVal, lookupDChoice
+  , concatDelta
+  , emptyUpdateSet
+  , concatUpdateSet
+  ) where
+
+import Control.Lens hiding (Context)
+import Control.Monad.Error.Class (MonadError (..))
+import Control.Monad.Reader
+import Data.HashMap.Strict (HashMap, union, empty)
+
+import DA.Daml.LF.Ast
+import DA.Daml.LF.TypeChecker.Error
+
+data UpdCreate = UpdCreate
+  { _creTemp  :: !(Qualified TypeConName)
+    -- ^ Qualified type constructor corresponding to the contract template.
+  , _creField :: ![(FieldName, Expr)]
+    -- ^ The fields to be verified, together with their value.
+  }
+data UpdArchive = UpdArchive
+  { _arcTemp  :: !(Qualified TypeConName)
+    -- ^ Qualified type constructor corresponding to the contract template.
+  , _arcField :: ![(FieldName, Expr)]
+    -- ^ The fields to be verified, together with their value.
+  }
+data UpdChoice = UpdChoice
+  { _choTemp  :: !(Qualified TypeConName)
+    -- ^ Qualified type constructor corresponding to the contract template.
+  , _choName  :: !ChoiceName
+    -- ^ The name of the choice.
+  }
+
+-- | The List of updates being performed
+data UpdateSet = UpdateSet
+  { _usCre :: ![UpdCreate]
+    -- ^ The list of create updates.
+  , _usArc :: ![UpdArchive]
+    -- ^ The list of archive updates.
+  , _usCho :: ![UpdChoice]
+    -- ^ The list of choice updates.
+  }
+
+makeLenses ''UpdateSet
+
+emptyUpdateSet :: UpdateSet
+emptyUpdateSet = UpdateSet [] [] []
+
+concatUpdateSet :: UpdateSet -> UpdateSet -> UpdateSet
+concatUpdateSet (UpdateSet cres1 arcs1 chos1) (UpdateSet cres2 arcs2 chos2) =
+  UpdateSet (cres1 ++ cres2) (arcs1 ++ arcs2) (chos1 ++ chos2)
+
+-- | The environment for the DAML-LF verifier
+data Delta = Delta
+  { _devars :: ![ExprVarName]
+    -- ^ The skolemised term variables.
+  , _devals :: !(HashMap (Qualified ExprValName) (Expr, UpdateSet))
+    -- ^ The bound values.
+  , _dchs :: !(HashMap ((Qualified TypeConName), ChoiceName) UpdateSet)
-  , _dchs :: !(HashMap ((Qualified TypeConName), ChoiceName) UpdateSet)
+  , _dchs :: !(HashMap (Qualified TypeConName, ChoiceName) UpdateSet)
-  , _dchs :: !(HashMap ((Qualified TypeConName), ChoiceName) UpdateSet)
+  , _dchs :: !(HashMap (Qualified TypeConName, ChoiceName) UpdateSet)
+    -- ^ The set of relevant choices.
+  -- TODO: split this off into data types for readability?
+  }
+
+makeLenses ''Delta
+
+emptyDelta :: Delta
+emptyDelta = Delta [] empty empty
+
+concatDelta :: Delta -> Delta -> Delta
+concatDelta (Delta vars1 vals1 chs1) (Delta vars2 vals2 chs2) =
+  Delta (vars1 ++ vars2) (union vals1 vals2) (union chs1 chs2)
+  -- TODO: union makes me slightly nervous, as it allows overlapping keys
+  -- (and just uses the first)
+
+-- | Type class constraint with the required monadic effects for functions
+-- manipulating the verification environment.
+type MonadDelta m = (MonadError Error m, MonadReader Delta m)
+
+runDelta :: ReaderT Delta (Either Error) a -> Either Error a
+runDelta act = runReaderT act emptyDelta
+
+-- | Run a computation in the current environment, with an additional
+-- environment extension.
+introDelta :: MonadDelta m => Delta -> m a -> m a
+introDelta delta = local (concatDelta delta)
+
+extVarDelta :: MonadDelta m => ExprVarName -> m a -> m a
+extVarDelta x = local (over devars ((:) x))
+
+lookupDExprVar :: MonadDelta m => ExprVarName -> m ()
+lookupDExprVar x = ask >>= \ del -> unless (elem x $ del ^. devars)
+                                          $ throwError $ EUnknownExprVar x
-lookupDExprVar x = ask >>= \ del -> unless (elem x $ del ^. devars)
-                                          $ throwError $ EUnknownExprVar x
+lookupDExprVar x = do
+  del <- ask
+  unless (x `elem` _devars del) $ throwError $ EUnknownExprVar x
-lookupDExprVar x = ask >>= \ del -> unless (elem x $ del ^. devars)
-                                          $ throwError $ EUnknownExprVar x
+lookupDExprVar x = do
+  del <- ask
+  unless (x `elem` _devars del) $ throwError $ EUnknownExprVar x
+
+lookupDVal :: MonadDelta m => (Qualified ExprValName) -> m (Expr, UpdateSet)
+lookupDVal w = view (devals . at w) >>= match _Just (EEmptyCase)
+-- TODO: This is a random error. The thing we really want to write is:
+-- lookupDVal w = view (devals . at w) >>= match _Just (EUnknownDefinition $ LEValue w)
+-- The issue here is that our values are currently stored in Delta instead
+-- of in the world like in the type checker.
+-- This means that we can't throw the error we want to throw here.
+-- 2 options:
+--   + either define our own errors, as they don't correspond 100% to the type
+--   checking errors anyway.
+--   + or create our own world environment to store values. This also makes
+--   sense as these values work similar to how they work in the type checker,
+--   except that we need to store a partially evaluated definition as well.
+-- Both approaches make sense, but both imply a lot of code duplication, so they
+-- don't sound that enticing...
+
+lookupDChoice :: MonadDelta m => (Qualified TypeConName) -> ChoiceName
+             -> m UpdateSet
+lookupDChoice tem ch = view (dchs . at (tem, ch)) >>= match _Just EEmptyCase
+-- TODO: Random error.
+
+-- | Helper functions mirrored from Env.
+-- TODO: Reduce duplication by abstracting over MonadGamma and MonadDelta?
+match :: MonadDelta m => Prism' a b -> Error -> a -> m b
+match p e x = either (const (throwError e)) pure (matching p x)
+-- TODO: no context, like in Gamma
+