iface: check for interface implementations precond (#11494)

* iface: check for interface implementations precond

We change speedy to also check all preconditions defined in interface
implementations upon a create.

CHANGELOG_BEGIN
CHANGELOG_END

* Update daml-lf/interpreter/src/main/scala/com/digitalasset/daml/lf/speedy/Compiler.scala

Co-authored-by: Remy <remy.haemmerle@daml.com>

* format

* interfaces: lfconversion for iface preconditions

This adds interface preconditions to the interface implementations
during completion phase in the LF conversion.

CHANGELOG_BEGIN
CHANGELOG_END

* format

* rebase

Co-authored-by: Remy <remy.haemmerle@daml.com>

compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Base.hs

@@ -905,6 +905,7 @@ data TemplateImplements = TemplateImplements
   , tpiMethods :: !(NM.NameMap TemplateImplementsMethod)
   , tpiInheritedChoiceNames :: !(S.Set ChoiceName)
     -- ^ Set of inherited fixed choice names.
+  , tpiPrecond :: !Expr
   }
   deriving (Eq, Data, Generic, NFData, Show)
 

compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Optics.hs

@@ -80,10 +80,11 @@ templateExpr f (Template loc tpl param precond signatories observers agreement c
   <*> (NM.traverse . templateImplementsExpr) f implements
 
 templateImplementsExpr :: Traversal' TemplateImplements Expr
-templateImplementsExpr f (TemplateImplements iface methods inheritedChoiceNames) =
+templateImplementsExpr f (TemplateImplements iface methods inheritedChoiceNames precond) =
   TemplateImplements iface
     <$> (NM.traverse . templateImplementsMethodExpr) f methods
     <*> pure inheritedChoiceNames
+    <*> f precond
 
 templateImplementsMethodExpr :: Traversal' TemplateImplementsMethod Expr
 templateImplementsMethodExpr f (TemplateImplementsMethod name body) =

compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Pretty.hs

@@ -633,12 +633,13 @@ pPrintTemplate lvl modName (Template mbLoc tpl param precond signatories observe
       implementsDoc = map (pPrintTemplateImplements lvl) (NM.toList implements)
 
 pPrintTemplateImplements :: PrettyLevel -> TemplateImplements -> Doc ann
-pPrintTemplateImplements lvl (TemplateImplements name methods inheritedChoices)
+pPrintTemplateImplements lvl (TemplateImplements name methods inheritedChoices precond)
   | NM.null methods = keyword_ "implements" <-> pPrintPrec lvl 0 name
-  | otherwise = vcat
-      $ (keyword_ "implements" <-> pPrintPrec lvl 0 name <-> keyword_ "where")
-      : nest 2 (keyword_ "inherits" <-> pPrintPrec lvl 0 (S.toList inheritedChoices))
-      : map (nest 2 . pPrintTemplateImplementsMethod lvl) (NM.toList methods)
+  | otherwise = vcat $
+      [ keyword_ "implements" <-> pPrintPrec lvl 0 name <-> keyword_ "where"
+      , nest 2 (keyword_ "ensure" <-> pPrintPrec lvl 0 precond)
+      , nest 2 (keyword_ "inherits" <-> pPrintPrec lvl 0 (S.toList inheritedChoices))
+      ] ++ map (nest 2 . pPrintTemplateImplementsMethod lvl) (NM.toList methods)
 
 pPrintTemplateImplementsMethod :: PrettyLevel -> TemplateImplementsMethod -> Doc ann
 pPrintTemplateImplementsMethod lvl (TemplateImplementsMethod name expr) =

compiler/daml-lf-proto/src/DA/Daml/LF/Proto3/DecodeV1.hs

@@ -344,6 +344,7 @@ decodeDefTemplateImplements LF1.DefTemplate_Implements{..} = TemplateImplements
   <$> mayDecode "defTemplate_ImplementsInterface" defTemplate_ImplementsInterface decodeTypeConName
   <*> decodeNM DuplicateMethod decodeDefTemplateImplementsMethod defTemplate_ImplementsMethods
   <*> decodeSet DuplicateChoice (decodeNameId ChoiceName) defTemplate_ImplementsInheritedChoiceInternedNames
+  <*> mayDecode "defTemplate_ImplementsPrecondition" defTemplate_ImplementsPrecond decodeExpr
 
 decodeDefTemplateImplementsMethod :: LF1.DefTemplate_ImplementsMethod -> Decode TemplateImplementsMethod
 decodeDefTemplateImplementsMethod LF1.DefTemplate_ImplementsMethod{..} = TemplateImplementsMethod

compiler/daml-lf-proto/src/DA/Daml/LF/Proto3/EncodeV1.hs

@@ -934,6 +934,7 @@ encodeTemplateImplements TemplateImplements{..} = do
     defTemplate_ImplementsInterface <- encodeQualTypeConName tpiInterface
     defTemplate_ImplementsMethods <- encodeNameMap encodeTemplateImplementsMethod tpiMethods
     defTemplate_ImplementsInheritedChoiceInternedNames <- encodeSet (encodeNameId unChoiceName) tpiInheritedChoiceNames
+    defTemplate_ImplementsPrecond <- encodeExpr tpiPrecond
     pure P.DefTemplate_Implements {..}
 
 encodeTemplateImplementsMethod :: TemplateImplementsMethod -> Encode P.DefTemplate_ImplementsMethod

compiler/daml-lf-tools/src/DA/Daml/LF/Completer.hs

@@ -32,5 +32,6 @@ completeTemplateImplements :: LF.World -> LF.TemplateImplements -> LF.TemplateIm
 completeTemplateImplements world tpi@TemplateImplements{..} =
     case lookupInterface tpiInterface world of
         Left _ -> error ("Could not find interface " <> T.unpack (T.intercalate "." (unTypeConName (qualObject tpiInterface))))
-        Right DefInterface { intFixedChoices } ->
-            tpi { tpiInheritedChoiceNames = S.fromList (NM.names intFixedChoices) }
+        Right DefInterface { intFixedChoices, intPrecondition } ->
+            tpi { tpiInheritedChoiceNames = S.fromList (NM.names intFixedChoices)
+                , tpiPrecond = intPrecondition}

compiler/damlc/daml-lf-conversion/src/DA/Daml/LFConversion.hs

@@ -973,7 +973,8 @@ convertImplements env tplTypeCon = NM.fromList <$>
                 , Just methodName <- [T.stripPrefix "m_" fieldName]
                 ]
         let inheritedChoiceNames = S.empty -- This is filled during LF post-processing (in the LF completer).
-        pure (TemplateImplements con methods inheritedChoiceNames)
+        let precond = ETrue -- This is filled during LF post-processing (in the LF completer).
+        pure (TemplateImplements con methods inheritedChoiceNames precond)
 
 convertChoices :: Env -> LF.TypeConName -> TemplateBinds -> ConvertM (NM.NameMap TemplateChoice)
 convertChoices env tplTypeCon tbinds =

daml-lf/archive/src/main/protobuf/com/daml/daml_lf_dev/daml_lf_1.proto

@@ -1459,6 +1459,7 @@ message DefTemplate {
     repeated ImplementsMethod methods = 2;
     repeated int32 inherited_choice_interned_names = 3;
       // ^ inherited fixed choice names as interned strings
+    Expr precond = 4;
   }
 
   // The type constructor for the template, acting as both

daml-lf/archive/src/main/scala/com/digitalasset/daml/lf/archive/DecodeV1.scala

@@ -610,6 +610,7 @@ private[archive] class DecodeV1(minor: LV.Minor) {
         inheritedChoices = lfImpl.getInheritedChoiceInternedNamesList.asScala
           .map(getInternedName(_, "TemplateImplements.inheritedChoices"))
           .toSet,
+        precond = decodeExpr(lfImpl.getPrecond, "TemplateImplements.precond"),
       )
 
     private[this] def decodeTemplateImplementsMethod(

daml-lf/interpreter/src/main/scala/com/digitalasset/daml/lf/speedy/Compiler.scala

@@ -1550,17 +1550,21 @@ private[lf] final class Compiler(
   private[this] def compileCreate(
       tmplId: Identifier,
       tmpl: Template,
-  ): (SDefinitionRef, SDefinition) =
+  ): (SDefinitionRef, SDefinition) = {
+    val precondsArray =
+      (Iterator(tmpl.precond) ++ (tmpl.implements.iterator.map(impl => impl._2.precond)))
+        .to(ImmArray)
+    val preconds = ECons(TBuiltin(BTBool), precondsArray, ENil(TBuiltin(BTBool)))
     // Translates 'create Foo with <params>' into:
     // CreateDefRef(tmplId) = \ <tmplArg> <token> ->
-    //   let _ = $checkPreconf(tmplId)(<tmplArg> [tmpl.precond]
+    //   let _ = $checkPrecond(tmplId)(<tmplArg> [tmpl.precond ++ [precond | precond <- tmpl.implements]]
     //   in $create <tmplArg> [tmpl.agreementText] [tmpl.signatories] [tmpl.observers] [tmpl.key]
     topLevelFunction2(CreateDefRef(tmplId)) { (tmplArgPos, _, _env) =>
       val env = _env.bindExprVar(tmpl.param, tmplArgPos)
       // We check precondition in a separated builtin to prevent
       // further evaluation of agreement, signatories, observers and key
       // in case of failed precondition.
-      let(env, SBCheckPrecond(tmplId)(env.toSEVar(tmplArgPos), compile(env, tmpl.precond))) {
+      let(env, SBCheckPrecond(tmplId)(env.toSEVar(tmplArgPos), compile(env, preconds))) {
         (_, env) =>
           SBUCreate(tmplId)(
             env.toSEVar(tmplArgPos),
@@ -1571,6 +1575,7 @@ private[lf] final class Compiler(
           )
       }
     }
+  }
 
   private[this] def compileCreateAndExercise(
       tmplId: Identifier,

daml-lf/interpreter/src/main/scala/com/digitalasset/daml/lf/speedy/SBuiltin.scala

@@ -886,7 +886,12 @@ private[lf] object SBuiltin {
     */
   final case class SBCheckPrecond(templateId: TypeConName) extends SBuiltinPure(2) {
     override private[speedy] def executePure(args: util.ArrayList[SValue]): SUnit.type = {
-      if (!getSBool(args, 1))
+      if (
+        !(getSList(args, 1).iterator.forall(_ match {
+          case SBool(b) => b
+          case otherwise => crash(s"type mismatch SBCheckPrecond: expected SBool, got $otherwise")
+        }))
+      )
         throw SErrorDamlException(
           IE.TemplatePreconditionViolated(
             templateId = templateId,

daml-lf/language/src/main/scala/com/digitalasset/daml/lf/language/Ast.scala

@@ -854,6 +854,7 @@ object Ast {
       interface: TypeConName,
       methods: Map[MethodName, GenTemplateImplementsMethod[E]],
       inheritedChoices: Set[ChoiceName],
+      precond: E,
   )
 
   final class GenTemplateImplementsCompanion[E] private[Ast] {
@@ -861,26 +862,28 @@ object Ast {
         interface: TypeConName,
         methods: Iterable[(MethodName, GenTemplateImplementsMethod[E])],
         inheritedChoices: Iterable[ChoiceName],
+        precond: E,
     ): GenTemplateImplements[E] = {
       val methodMap = toMapWithoutDuplicate(
         methods,
         (methodName: MethodName) =>
           throw PackageError(s"repeated method implementation $methodName"),
       )
-      new GenTemplateImplements[E](interface, methodMap, inheritedChoices.toSet)
+      new GenTemplateImplements[E](interface, methodMap, inheritedChoices.toSet, precond)
     }
 
     def apply(
         interface: TypeConName,
         methods: Map[MethodName, GenTemplateImplementsMethod[E]],
         inheritedChoices: Set[ChoiceName],
+        precond: E,
     ): GenTemplateImplements[E] =
-      GenTemplateImplements[E](interface, methods, inheritedChoices)
+      GenTemplateImplements[E](interface, methods, inheritedChoices, precond)
 
     def unapply(
         arg: GenTemplateImplements[E]
-    ): Some[(TypeConName, Map[MethodName, GenTemplateImplementsMethod[E]], Set[ChoiceName])] =
-      Some((arg.interface, arg.methods, arg.inheritedChoices))
+    ): Some[(TypeConName, Map[MethodName, GenTemplateImplementsMethod[E]], Set[ChoiceName], E)] =
+      Some((arg.interface, arg.methods, arg.inheritedChoices, arg.precond))
   }
 
   type TemplateImplements = GenTemplateImplements[Expr]

daml-lf/language/src/main/scala/com/digitalasset/daml/lf/language/Util.scala

@@ -222,11 +222,12 @@ object Util {
 
   private[this] def toSignature(implements: TemplateImplements): TemplateImplementsSignature =
     implements match {
-      case TemplateImplements(name, methods, inheritedChoices) =>
+      case TemplateImplements(name, methods, inheritedChoices, _) =>
         TemplateImplementsSignature(
           name,
           methods.transform((_, v) => toSignature(v)),
           inheritedChoices,
+          (),
         )
     }
 

daml-lf/parser/src/main/scala/com/digitalasset/daml/lf/testing/parser/AstRewriter.scala

@@ -281,11 +281,13 @@ private[daml] class AstRewriter(
             interface,
             methods,
             inheritedChoices,
+            precond,
           ) =>
         TemplateImplements(
           interface,
           methods.transform((_, x) => apply(x)),
           inheritedChoices,
+          apply(precond),
         )
     }
   def apply(x: TemplateImplementsMethod): TemplateImplementsMethod =

daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/iterable/ExprIterable.scala

@@ -179,8 +179,9 @@ private[validation] object ExprIterable {
             interface @ _,
             methods,
             inheritedChoices @ _,
+            precond,
           ) =>
-        methods.values.iterator.flatMap(iterator(_))
+        Iterator(precond) ++ methods.values.iterator.flatMap(iterator(_))
     }
 
   private[iterable] def iterator(x: TemplateImplementsMethod): Iterator[Expr] =

daml-lf/validation/src/main/scala/com/digitalasset/daml/lf/validation/iterable/TypeIterable.scala

@@ -225,8 +225,9 @@ private[validation] object TypeIterable {
 
   private[validation] def iterator(impl: TemplateImplements): Iterator[Type] =
     impl match {
-      case TemplateImplements(interface, methods, inheritedChoices @ _) =>
+      case TemplateImplements(interface, methods, inheritedChoices @ _, precond) =>
         Iterator(TTyCon(interface)) ++
+          iterator(precond) ++
           methods.values.flatMap(iterator(_))
     }