Key assertions

The docs here says that ‘Key assertions’ is one of the four actions in a transaction tree. However, there is no one ‘key assertion’ function or keyword in Daml. So what does this refer to? Is it any assertion involving keys, or is it a set of statements such as exerciseByKey, lookupByKey, NoSuchKey… etc?

Key assertion here refers to a negative lookupByKey. A positive key lookup is implicitly recorded as part of a fetch or exercise of a contract with the given key but we need a special primitive to record that there is no contract with a given key.

However, in practice, this is a case where the ledger model is slightly out of sync with the implementation. In the implementation, we don’t use NoSuchKey assertions but instead we have a separate LookupByKey node which can result both negative and positive assertions (fetchByKey and exerciseByKey are still recorded through regular fetch/exercise). We track that mismatch in Align Ledger Model docs to implementation · Issue #7113 · digital-asset/daml · GitHub.

So is it correct to say that the key assertion here means lookupByKey, and just that?

In the ledger model, it’s even more restrictive. It’s only a negative lookupByKey so one that returns None or in other words a NoSuchKey assertion.

Thanks @cocreature! For some reason, I am still having a hard time wrapping my head around this. Can you please point me to some code that uses this concept of ‘key assertion’?

Consider this Daml choice:

template T
  with
    …
  choice C : ()
    with
       k : SomeKeyType
  do None <- lookupByKey @SomeOtherTemplate k
     pure ()  

And now let’s say we do something like exercise cid (C yourkey).

The resulting transaction in the ledger model will look something like this:

exercise cid (C yourkey) -- That’s the exercise node as the root
  - NoSuchKey @SomeTemplate yourkey -- That’s the key assertion which is a child node of the exercise

Another way of looking at this is to take a look at the transaction graph in Daml studio. As I mentioned above the implementation uses LookupByKey nodes rather than “NoSuchKey” assertions but if you mentally replace a key lookup with “not found” by “NoSuchKey” you will see the same structure:

module Main where

import Daml.Script

data SomeKeyType = SomeKeyType 
  with
    p : Party
  deriving (Eq, Show)

template SomeTemplate
  with
    p : Party
  where
    signatory p
    key (SomeKeyType p) : SomeKeyType
    maintainer key.p

template T
  with
    p : Party
  where
    signatory p
    choice C : ()
      with
        k : SomeKeyType
      controller p
      do None <- lookupByKey @SomeTemplate k
         pure ()

script = do
  p <- allocateParty "p"
  c <- submit p $ createCmd (T p)
  submit p $ exerciseCmd c (C (SomeKeyType p))

Wow! Got it! Thanks a ton!