Skip to content

Commit

Permalink
precondition lf conversion (#11538)
Browse files Browse the repository at this point in the history 
* interfaces: lf conversion of preconditions

This adds the LF conversion of preconditions from the desugared GHC code
to Daml LF for preconditions. This depends on the corresponding patch of
the GHC fork.

CHANGELOG_BEGIN
CHANGELOG_END

* pin linux stackage snapshot

* added a test

CHANGELOG_BEGIN
CHANGELOG_END

* pinned linux stackage snapshot

CHANGELOG_BEGIN
CHANGELOG_END

* additional InterfacePrecondition test

this checks that that conjunction of all preconditions of intererfaces
and templates is checked.

CHANGELOG_BEGIN
CHANGELOG_END

* pin stackage snapshot

* pin windows stackage snapshot

* update compile.yml (again)

* pin linux stack snapshot

* fix InterfacePrecondition test

* pin windows stackage
  • Loading branch information
Robin Krom authored Nov 9, 2021
1 parent f722cf1 commit af1bee7
Show file tree
Hide file tree
Showing 8 changed files with 156 additions and 15 deletions.
2 changes: 1 addition & 1 deletion ci/da-ghc-lib/compile.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ jobs:
variables:
ghc-lib-sha: '42e5c306dcfbc84b83336fdd531023e93bfcc5b2'
base-sha: '9c787d4d24f2b515934c8503ee2bbd7cfac4da20'
patches: 'e9abc24560f623c9c575d96a7a1a234927e042b2 833ca63be2ab14871874ccb6974921e8952802e9'
patches: 'a4a78867205bc453416f58f1d6dce470a0e39d61 833ca63be2ab14871874ccb6974921e8952802e9'
flavor: 'ghc-8.8.1'
steps:
- checkout: self
Expand Down
19 changes: 18 additions & 1 deletion compiler/damlc/daml-lf-conversion/src/DA/Daml/LFConversion.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,7 @@ data Env = Env
-- packages does not cause performance issues.
,envLfVersion :: LF.Version
,envTemplateBinds :: MS.Map TypeConName TemplateBinds
,envInterfaceBinds :: MS.Map TypeConName InterfaceBinds
,envExceptionBinds :: MS.Map TypeConName ExceptionBinds
,envChoiceData :: MS.Map TypeConName [ChoiceData]
,envImplements :: MS.Map TypeConName [GHC.TyCon]
Expand Down Expand Up @@ -394,6 +395,18 @@ scrapeTemplateBinds binds = MS.filter (isJust . tbTyCon) $ MS.map ($ emptyTempla
, hasDamlTemplateCtx tpl
]

data InterfaceBinds = InterfaceBinds
{ ibEnsure :: Maybe (GHC.Expr Var)
}

scrapeInterfaceBinds :: [(Var, GHC.Expr Var)] -> MS.Map TypeConName InterfaceBinds
scrapeInterfaceBinds binds = MS.fromList
[ ( mkTypeCon [getOccText (GHC.tyConName iface)]
, InterfaceBinds { ibEnsure = Just expr} )
| (HasEnsureDFunId iface, expr) <- binds
, hasDamlInterfaceCtx iface
]

data ExceptionBinds = ExceptionBinds
{ ebTyCon :: GHC.TyCon
, ebMessage :: GHC.Expr Var
Expand Down Expand Up @@ -439,10 +452,12 @@ convertInterfaces env tyThings = interfaceClasses
convertInterface intName tyCon cls = do
let intLocation = convNameLoc (GHC.tyConName tyCon)
let intParam = this
let precond = fromMaybe (error $ "Missing precondition for interface " <> show intName)
$ (MS.lookup intName $ envInterfaceBinds env) >>= ibEnsure
withRange intLocation $ do
intMethods <- NM.fromList <$> mapM convertMethod (drop 4 $ classMethods cls)
intFixedChoices <- convertChoices env intName emptyTemplateBinds
let intPrecondition = ETrue -- TODO (drsk) #11397 Implement interface preconditions
intPrecondition <- useSingleMethodDict env precond (`ETmApp` EVar intParam)
pure DefInterface {..}

convertMethod :: Var -> ConvertM InterfaceMethod
Expand Down Expand Up @@ -537,6 +552,7 @@ convertModule lfVersion pkgMap stablePackages isGenerated file x depOrphanModule
, ty@(TypeCon _ [_, TypeCon _ [TypeCon tplTy _]]) <- [varType name]
]
templateBinds = scrapeTemplateBinds binds
interfaceBinds = scrapeInterfaceBinds binds
exceptionBinds
| lfVersion `supports` featureExceptions =
scrapeExceptionBinds binds
Expand All @@ -554,6 +570,7 @@ convertModule lfVersion pkgMap stablePackages isGenerated file x depOrphanModule
, envInterfaces = interfaceCons
, envInterfaceChoiceData = ifChoiceData
, envTemplateBinds = templateBinds
, envInterfaceBinds = interfaceBinds
, envExceptionBinds = exceptionBinds
, envImplements = tplImplements
, envInterfaceInstances = tplInterfaceInstances
Expand Down
7 changes: 7 additions & 0 deletions compiler/damlc/tests/daml-test-files/Interface.daml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ interface Token where
transferImpl : Party -> Update (ContractId Token)
noopImpl : () -> Update ()

ensure (getAmount this >= 0)

choice Split : (ContractId Token, ContractId Token)
with
splitAmount : Int
Expand Down Expand Up @@ -74,6 +76,11 @@ template Asset

main = scenario do
p <- getParty "Alice"
p `submitMustFail` do
create Asset with
issuer = p
owner = p
amount = -1
p `submit` do
cidAsset1 <- create Asset with
issuer = p
Expand Down
8 changes: 7 additions & 1 deletion compiler/damlc/tests/daml-test-files/InterfaceDesugared.daml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,12 @@ instance HasSignatory Token where
instance HasFetch Token where
fetch = GHC.Types.primitive @"UFetchInterface"

instance DA.Internal.Desugar.HasEnsure Token where
ensure this
= DA.Internal.Desugar.True
where
_ = this

instance IsToken Token where
toToken = GHC.Types.primitive @"EToInterface"
fromToken = GHC.Types.primitive @"EFromInterface"
Expand Down Expand Up @@ -184,7 +190,7 @@ instance HasSignatory Asset where
signatory Asset{..} = [issuer, owner]

instance HasEnsure Asset where
ensure _ = True
ensure this = getAmount this >= 0

instance HasAgreement Asset where
agreement _ = ""
Expand Down
111 changes: 111 additions & 0 deletions compiler/damlc/tests/daml-test-files/InterfacePrecondition.daml
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
-- Copyright (c) 2021 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
-- SPDX-License-Identifier: Apache-2.0

-- @SINCE-LF-FEATURE DAML_INTERFACE

module InterfacePrecondition where

interface Token1 where
getOwner1 : Party
getAmount1 : Int
splitImpl : Int -> Update (ContractId Token1, ContractId Token1)
transferImpl : Party -> Update (ContractId Token1)

ensure (getAmount1 this >= 0 && getAmount1 this <= 7)

choice Split : (ContractId Token1, ContractId Token1)
with
splitAmount : Int
controller getOwner1 this
do
splitImpl this splitAmount

choice Transfer : ContractId Token1
with
newOwner : Party
controller getOwner1 this, newOwner
do
transferImpl this newOwner


interface Token2 where
getOwner2 : Party
getAmount2 : Int
noopImpl : () -> Update ()

ensure (getAmount2 this >= 3 && getAmount2 this <= 10)

nonconsuming choice Noop : ()
with
nothing : ()
controller getOwner2 this
do
noopImpl this nothing

template Asset
with
issuer : Party
owner : Party
amount : Int
where
signatory issuer, owner

ensure (amount >= 5 && amount <= 6)

implements Token1 where
let getOwner1 = owner
let getAmount1 = amount
let splitImpl = \splitAmount -> do
assert (splitAmount < amount)
cid1 <- create this with amount = splitAmount
cid2 <- create this with amount = amount - splitAmount
pure (toToken1ContractId cid1, toToken1ContractId cid2)
let transferImpl = \newOwner -> do
cid <- create this with owner = newOwner
pure (toToken1ContractId cid)


implements Token2 where
let getOwner2 = owner
let getAmount2 = amount
let noopImpl = \nothing -> do
pure ()

main = scenario do
p <- getParty "Alice"
p `submitMustFail` do
create Asset with
issuer = p
owner = p
amount = -1 -- violates ensure of Token1 & Token2 & Asset

p `submitMustFail` do
create Asset with
issuer = p
owner = p
amount = 1 -- violates ensure of Token2 && Asset

p `submitMustFail` do
create Asset with
issuer = p
owner = p
amount = 3 -- violates ensure of Asset

p `submitMustFail` do
create Asset with
issuer = p
owner = p
amount = 7 -- violates ensure of Asset

p `submitMustFail` do
create Asset with
issuer = p
owner = p
amount = 8 -- violates ensure of Asset & Token2

p `submit` do
create Asset with
issuer = p
owner = p
amount = 5 -- works for Token1 & Token2 & Asset
pure ()
8 changes: 4 additions & 4 deletions stack-snapshot.yaml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@

resolver: lts-18.0
packages:
- archive: https://daml-binaries.da-ext.net/da-ghc-lib/ghc-lib-be4506a37225265fc1e0dab696b43c04.tar.gz
sha256: "4e0d25b83c965eb51386c62f59157bc064aa556497068ab2fde2a09d40137403"
- archive: https://daml-binaries.da-ext.net/da-ghc-lib/ghc-lib-parser-be4506a37225265fc1e0dab696b43c04.tar.gz
sha256: "ae2d9ace0d92346f3c25bfb4b47329e1d23a05ccfc72855002052fffe518fe3b"
- archive: https://daml-binaries.da-ext.net/da-ghc-lib/ghc-lib-f1468b856c4a52a7826bfc0c29dee4f4.tar.gz
sha256: "f939726fdc6dbe67db4aeac86b3f6bcd88997dcb5648dc0d7e7f221760074165"
- archive: https://daml-binaries.da-ext.net/da-ghc-lib/ghc-lib-parser-f1468b856c4a52a7826bfc0c29dee4f4.tar.gz
sha256: "fbbca516fc2f8fab9d3095cde1edb98d3f05af9ea2dfb927275ed745b394685c"
- github: digital-asset/hlint
commit: "c8246c1feb932858ff2b5d7e9e900068a974bf57"
sha256: "3da24baf789c5f00211a92e24153e6b88102befaa946ada1f707935554500fe2"
Expand Down
8 changes: 4 additions & 4 deletions stackage_snapshot.json
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
"__GENERATED_FILE_DO_NOT_MODIFY_MANUALLY": 1569617722,
"all-cabal-hashes": "https://raw.githubusercontent.com/commercialhaskell/all-cabal-hashes/a2d6c3907baf35bf093800454aad34fba00eb10c",
"__GENERATED_FILE_DO_NOT_MODIFY_MANUALLY": 952753112,
"all-cabal-hashes": "https://raw.githubusercontent.com/commercialhaskell/all-cabal-hashes/f54ac27a85d067a4f438deb45a321159713452c7",
"resolved": {
"Cabal": {"dependencies":[],"location":{"type":"core"},"name":"Cabal","version":"3.2.1.0"},
"Decimal": {"dependencies":["base","deepseq"],"location":{"type":"hackage","url":"https://hackage.haskell.org/package/Decimal-0.5.2/Decimal-0.5.2.tar.gz"},"name":"Decimal","pinned":{"url":["https://hackage.haskell.org/package/Decimal-0.5.2/Decimal-0.5.2.tar.gz","https://s3.amazonaws.com/hackage.fpcomplete.com/package/Decimal-0.5.2.tar.gz"],"sha256":"a37a0220424e4bcb8cae1d38844c7027ee314449758d0d14ff3e2e0a5c8a87a7","cabal-sha256":"83dd16a1c0737fd35fdb1088af36e1a53034e75090e3f0d4ad32296f1a35a13b"},"version":"0.5.2"},
Expand Down Expand Up @@ -100,8 +100,8 @@
"generic-deriving": {"dependencies":["base","containers","ghc-prim","template-haskell","th-abstraction"],"location":{"type":"hackage","url":"https://hackage.haskell.org/package/generic-deriving-1.14/generic-deriving-1.14.tar.gz"},"name":"generic-deriving","pinned":{"url":["https://hackage.haskell.org/package/generic-deriving-1.14/generic-deriving-1.14.tar.gz","https://s3.amazonaws.com/hackage.fpcomplete.com/package/generic-deriving-1.14.tar.gz"],"sha256":"d0abd5e423960b66867c6149c20b221b1351e3805d1bf787fc4efa3e7bb7cb02","cabal-sha256":"c9c6782a3cdce2f2bcaf891e0ffbf06df871e68498574b73a565771dc084273c"},"version":"1.14"},
"generics-sop": {"dependencies":["base","ghc-prim","sop-core","template-haskell","th-abstraction"],"location":{"type":"hackage","url":"https://hackage.haskell.org/package/generics-sop-0.5.1.1/generics-sop-0.5.1.1.tar.gz"},"name":"generics-sop","pinned":{"url":["https://hackage.haskell.org/package/generics-sop-0.5.1.1/generics-sop-0.5.1.1.tar.gz","https://s3.amazonaws.com/hackage.fpcomplete.com/package/generics-sop-0.5.1.1.tar.gz"],"sha256":"81b7c38b5c2a1ae3c790b1707a0e2a2031430e33b3683f88e2daa5b59ae4c5d8","cabal-sha256":"522a1a1da05d5acc03da448fa603c038cc15b991272846a591e26e7505d2b73a"},"version":"0.5.1.1"},
"ghc-byteorder": {"dependencies":["base"],"location":{"type":"hackage","url":"https://hackage.haskell.org/package/ghc-byteorder-4.11.0.0.10/ghc-byteorder-4.11.0.0.10.tar.gz"},"name":"ghc-byteorder","pinned":{"url":["https://hackage.haskell.org/package/ghc-byteorder-4.11.0.0.10/ghc-byteorder-4.11.0.0.10.tar.gz","https://s3.amazonaws.com/hackage.fpcomplete.com/package/ghc-byteorder-4.11.0.0.10.tar.gz"],"sha256":"86e50a89798181db4f44ec3848fc52940c73098e88549a351ceb54fefc691fb6","cabal-sha256":"e345720de7b28ba1bf434775d34d3b94da8e8dd5dc24469f008e1f82717c0352"},"version":"4.11.0.0.10"},
"ghc-lib": {"dependencies":["alex","array","base","binary","bytestring","containers","deepseq","directory","filepath","ghc-lib-parser","ghc-prim","happy","hpc","pretty","process","rts","time","transformers","unix"],"location":{"type":"archive","url":"https://daml-binaries.da-ext.net/da-ghc-lib/ghc-lib-be4506a37225265fc1e0dab696b43c04.tar.gz"},"name":"ghc-lib","pinned":{"sha256":"4e0d25b83c965eb51386c62f59157bc064aa556497068ab2fde2a09d40137403","strip-prefix":"ghc-lib-8.8.1.20211103"},"version":"8.8.1.20211103"},
"ghc-lib-parser": {"dependencies":["alex","array","base","binary","bytestring","containers","deepseq","directory","filepath","ghc-prim","happy","hpc","pretty","process","time","transformers","unix"],"location":{"type":"archive","url":"https://daml-binaries.da-ext.net/da-ghc-lib/ghc-lib-parser-be4506a37225265fc1e0dab696b43c04.tar.gz"},"name":"ghc-lib-parser","pinned":{"sha256":"ae2d9ace0d92346f3c25bfb4b47329e1d23a05ccfc72855002052fffe518fe3b","strip-prefix":"ghc-lib-parser-8.8.1.20211103"},"version":"8.8.1.20211103"},
"ghc-lib": {"dependencies":["alex","array","base","binary","bytestring","containers","deepseq","directory","filepath","ghc-lib-parser","ghc-prim","happy","hpc","pretty","process","rts","time","transformers","unix"],"location":{"type":"archive","url":"https://daml-binaries.da-ext.net/da-ghc-lib/ghc-lib-f1468b856c4a52a7826bfc0c29dee4f4.tar.gz"},"name":"ghc-lib","pinned":{"sha256":"f939726fdc6dbe67db4aeac86b3f6bcd88997dcb5648dc0d7e7f221760074165","strip-prefix":"ghc-lib-8.8.1.20211108"},"version":"8.8.1.20211108"},
"ghc-lib-parser": {"dependencies":["alex","array","base","binary","bytestring","containers","deepseq","directory","filepath","ghc-prim","happy","hpc","pretty","process","time","transformers","unix"],"location":{"type":"archive","url":"https://daml-binaries.da-ext.net/da-ghc-lib/ghc-lib-parser-f1468b856c4a52a7826bfc0c29dee4f4.tar.gz"},"name":"ghc-lib-parser","pinned":{"sha256":"fbbca516fc2f8fab9d3095cde1edb98d3f05af9ea2dfb927275ed745b394685c","strip-prefix":"ghc-lib-parser-8.8.1.20211108"},"version":"8.8.1.20211108"},
"ghc-lib-parser-ex": {"dependencies":["base","bytestring","containers","extra","ghc-lib-parser","uniplate"],"location":{"type":"hackage","url":"https://hackage.haskell.org/package/ghc-lib-parser-ex-8.8.5.8/ghc-lib-parser-ex-8.8.5.8.tar.gz"},"name":"ghc-lib-parser-ex","pinned":{"url":["https://hackage.haskell.org/package/ghc-lib-parser-ex-8.8.5.8/ghc-lib-parser-ex-8.8.5.8.tar.gz","https://s3.amazonaws.com/hackage.fpcomplete.com/package/ghc-lib-parser-ex-8.8.5.8.tar.gz"],"sha256":"b36ef8b49da4e8c78b00dca9b9546b7d4db0b09b10da5e313d3f0dbb4af581d7","cabal-sha256":"04f164fd6a4a5b0c5627cf7fadd79174c3b1d4c696dc481a9909266bd6a2a6aa"},"version":"8.8.5.8"},
"ghc-prim": {"dependencies":[],"location":{"type":"core"},"name":"ghc-prim","version":"0.6.1"},
"ghcide": {"dependencies":["aeson","async","base","binary","bytestring","containers","data-default","deepseq","dependent-map","dependent-sum","directory","extra","filepath","fuzzy","ghc-lib","ghc-lib-parser","haddock-library","hashable","hslogger","lsp","lsp-types","mtl","network-uri","prettyprinter","prettyprinter-ansi-terminal","regex-tdfa","rope-utf16-splay","safe-exceptions","shake","some","sorted-list","stm","syb","text","time","transformers","unix","unliftio","unordered-containers","utf8-string"],"location":{"type":"vendored"},"name":"ghcide","version":"0.1.0"},
Expand Down
Loading

0 comments on commit af1bee7

Please sign in to comment.