Spurious commands remain on the <k> cell after inner transaction

[geo2a]

Summary

Problem: <k> cell is not empty after successful execution Branch: master Test: tests/json-scenarios/txn-created-asset-id.json

Details

Executing the test scenario txn-created-asset-id.json that creates an asset with an inner transaction:

kavm run tests/json-scenarios/itxn-created-asset-id.json --teal-sources-dir tests/teal-sources/ --output pretty

Gives the following output:

  <k>
    #deactivateApp ( ) ~> #calcReturn ( ) ~> #stopIfError ( ) ~> #saveScratch ( ) ~>
    #popTxnFront ( ) ~> #evalNextTx ( ) ~> #checkExecutionResults ( 0 , 0 ) ~> .
  </k>
  <returncode>
    0
  </returncode>
  <returnstatus>
    "Success - transaction group accepted"
  </returnstatus>
  <paniccode>
    0
  </paniccode>
...
  <activeApps>
      .Set
  </activeApps>
...

The execution finished successfully (as intended), but the <k> cell seems to contain spurious items. It looks like the inner transaction execution rules try to execute more transactions than intended.

Info that I've gathered so far is:

• looking at the coverage report, I see that the #deactivateApp rule has been applied
• the <activeApps> cells contains .Set --- that is intended
• the #deactiveteApp rule is only introduced by the #finilizeExecution rule.

Considering all this, it looks like the #finilizeExecution is triggered more than once during the execution of this test. As far as I understand, this is an error.

This problem manifests in a larger example which I'm developing for the KAVM intro blogpost, but the existing test seems to isolate the problem rather well.

[geo2a]

Other inner transaction tests suffer from a similar issue, therefore the debugging should probably start with itxn-basic.json

[geo2a]

More investigation shows that the root cause probably is the itxn_submit rule:

  rule <k> itxn_submit => #incrementPC() ~> #checkItxns(T) ~> #executeItxnGroup()...</k>

Modifying the itxn-basic.teal to include an addtional err opcode after the trailing return causes this opcode to be executed.

[geo2a]

Looking more on all this, it seems like the context management implemented by means of <txnExecutionContext> causes non-determinism in TEAL execution. When we duplicate contexts to save them while executing an inner transaction, we also duplicate the <teal> cell. I think K becomes confused about where to apply the TEAL opcodes rules: to the duplicated cell or to the original one.