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