Is contract key uniqueness enforced at the choice, not command?

Please consider this slightly contrived (I am investigating a pattern) example

module Main where

import DA.Date

import Daml.Script

type Data = Text

doWork : Data -> Data
doWork s = s <> " Done!"

template THistory with
    s : Party
    observed : [(Data, Date)]
  where
    signatory s

    choice Observe : (ContractId THistory, ContractId T) with
        result : Data
        tId : ContractId T
      controller s
      do
        t <- fetch tId
        assertMsg "Must be same." $ t.workDatesId == self
        workDate <- toDateUTC <$> getTime
        workDatesId' <- create this with observed = (result, workDate) :: observed
        tId' <- create t with workDatesId = workDatesId'
        return (workDatesId', tId')


template T with
    s : Party
    workDatesId : ContractId THistory
  where
    signatory s

    key s : Party
    maintainer key

    postconsuming choice DoWork : ContractId T with
        input : Data
      controller s
      do
        let result = doWork input
        snd <$> exercise workDatesId Observe with tId = self, ..

demo : Script ()
demo = do

  s <- allocateParty "s"

  workDatesId <- s `submit` do
    createCmd THistory with
      s, observed = []

  tId <- s `submit` do
    createCmd T with ..

  tId' <- s `submit` do
    exerciseCmd tId DoWork with
      input = "Ok"

  pure ()

This throws a commit error on the unique key of T. Now the uniqueness of the key is important for this example, but i am confused as to why it is being violated by the DoWork choice. The postconsuming is intentional, but afaiu it does archive the current/old T at the end.

Thank you

Contract key uniqueness has to hold at each point (i.e., each step during execution or phrased differently after each node in the transaction) in your transaction not just at the beginning and end. Because DoWork archives the contract at the end, there is a point where uniqueness is violated and the transaction is rejected.

cocreature:

Contract key uniqueness has to hold at each point (i.e., each step during execution or phrased differently after each node in the transaction)

… Does it have to hold or is it just easier to check at every step?

I guess the simplest example of your point is that you can’t make this choice postconsuming:

template K with
    s : Party
  where
    signatory s
    key s : Party
    maintainer key

    postconsuming choice C : ContractId K 
      controller s
      do
        create this

Thank you for the explanation!

It’s not just about being easier, ensuring that it holds at any point in between allows you to split and merge transactions without breaking contract key uniqueness. That’s important for compositionality and to make sure you don’t run into issues with projections that may not see all nodes in a transaciton.

But wouldn’t you want your unit of composability to be a choice? So that you check uniqueness at the start and end of a choice body?

I do have to think about possible odd/out-of-sync projections though. That’s an interesting point.

As an aside I am also thinking about it being a Command but let’s stick with choices for now.