Is preconsuming meant to be semantically equivalent to consuming?

Hi!

Am I reading Reference: choices — Daml SDK 2.1.1 documentation correctly in thinking that preconsuming should be identical semantically to consuming?

While I was investigating the issue at Odd behavior with rollback nodes and archiving?

I found something odd about how preconsuming is compiled to daml-lf such that execution behavior can differ between preconsuming and consuming.

The preconsuming choice

    preconsuming choice Bar : ()
      controller owner
        do pure ()

is compiled as:

non-consuming choice Bar (self : ContractId Main:Foo) (arg : Main:Bar) : Unit
    controller Main:$$sc_Foo_5 this arg
    observer Nothing
    do ubind _ : Unit = Main:$carchive self
       in Main:$$sc_Foo_6 self this arg

whereas the consuming choice

    choice Bar : ()
      controller owner
        do pure (

compiles as

  consuming choice Bar (self : ContractId Main:Foo) (arg : Main:Bar) : Unit
    controller Main:$$sc_Foo_5 this arg
    observer Nothing
    do Main:$$sc_Foo_6 self this ar

Then, while the following program does not error out with a double spend

template Foo 
  with
    owner : Party
  where
    signatory owner 
    nonconsuming choice Catch : ()
      controller owner
        do try do
              exercise self Fail
            catch
              GeneralError _ -> pure ()
    choice Fail : ()
      controller owner
        do  abort ""

test: Script ()
test = script do
  a <- allocateParty "a"
  c <- submit a do
    createCmd Foo with
      owner = a
  submit a do
    exerciseCmd c Catch
  submit a do
    exerciseCmd c Catch

making Fail a preconsuming choice does error out with a double spend (since the preconsuming version compiles to the program in Odd behavior with rollback nodes and archiving?)

Thanks!
-Ming

Am I reading Reference: choices — Daml SDK 2.1.1 documentation correctly in thinking that preconsuming should be identical semantically to consuming?

This is not the case. To quote from the docs you linked

• The archival behavior is analogous to the consuming default behavior.

…but nothing else is. The more accurate semantic equivalent is stated in the last bullet point:

• Can be thought as a non-consuming choice that implicitly archives the contract before anything else happens

So, preconsuming is not consuming. It is nonconsuming, with an archive at the start (which…consumes it).

Ah, OK, so reading the doc again, there is a semantic difference is in consequence visibility? That is, both preconsuming and default consuming choices archive the contract before executing the choice body but for default consuming choices, “all contract stakeholders see all consequences of the action.”
whereas after executing a preconsuming choice, “Other [non-signatory/controller] stakeholders merely see an archive action.”

To be clear, is this the only semantic difference?

Hi Ming,

Yes. The difference between preconsuming and consuming is only in the transaction structure, which should only affect transaction node visibility, in the way you explained.

The difference in behavior you observed is actually a bug in daml studio. I added a ticket in the thread you linked to above. Thank you for reporting this.