search

runtimeverification / avm-semantics

BSD 3-Clause "New" or "Revised" License
15 stars 4 forks source link

Inner transaction support #83

Closed nwatson22 closed 2 years ago

nwatson22 commented 2 years ago

Here's some of my thoughts on how we might go about adding inner transaction support. I'd like feedback on some of the design proposals and I will continue to update/organize this document.

Implementation of itxn_begin:

I'm not sure this has much of a semantics beyond causing the program to fail if this is not declared before populating itxn fields. Otherwise behaves like itxn_next.

Implementation of itxn_field

Inside <transaction>, we can store a list of "sub-transactions", using the same <transaction> cell type? The fields of this will be populated by itxn_field Field.

Implementation of itxn_next

Keep track of a "current" sub-transaction. itxn_next will add a new empty transaction to the sub-transaction list and increment this counter. Give the transaction a reference to its parent.

Implementation of itxn_submit

I want to be able to use the current infrastructure for executing a transaction group, but we need a way to store all relevant data to continue executing the top level transaction.

Can we store all of this within the transaction itself, similar to how group-scope-accessible scratch space and logs are stored right now (as AppCallTxFields)? That way we can avoid deep nesting of transactions.

We also need to keep track of current depth, because there is a limit.

Implementation of itxn/itxna/gitxn/gitxna

Depends on how transaction groups are stored, but with the flat design will have to store a reference to the last inner group and last inner transaction. These will be used to look up field values. the non-global versions can be defined as a special case of the global versions, similar to how I did it for the normal txn lookup variants.

geo2a commented 2 years ago

Application accounts should be implemented. Inner transacations charge the application account of the contract for the fees.

The application account is also charged for the amounts of the Payment and AssetTransfer inner transactions that the application submits.

Budget pooling should be handled, although we don't even have basic opcode budgeting right now.

Yes, this should be on our todo list, though I'd say it's low priority. We can add rules that calculate execution costs on top later. We will consult KEVM on that.

Update availability rules so that assets/apps created earlier by top level or inner transactions are available, as well as the contract accounts of contracts created in already executed inner transactions.

Yes, we should specify the availability rules as implemented in go-algorand:

Access to executed inner transactions' fields through itxn, itxna, gitxn, gitxna

In go-algorand, the transaction are access by the txnFieldToStack function, which is used by the whole *txn* family of opcodes. The function has an inner bool flag and changes its behaviour depending on whether the txn is inner or not. I suggest we also implement a centralised txn field accessor which will work for both normal and inner txns. More on that later.

Check how different program versions interact

The interaction is somewhat complicated. Basically, AVM6 (the current) smart contracts are not allowed to call older versions. I suggest we structure the semantics with AVM6 in mind and don't support older versions. We, however, may need to introduce versioning once we've implemented AVM6.

I'm replying to the rest of the questions in bulk, by proposing some more specific steps, let's discuss.

Digging through go-algorand, I see there's a very reasonable scheme of how transactions are stored when evaluating application calls.

The process starts in ledger/internal/eval.go transactionGroup which tries to execute the group. It iterates through the group, calling eval.transaction, which assigns the transaction id and calls applyTransaction, which refers to the logic specific for each transaction type, which we can call transaction applicators. We are mostly interested in ledger/apply/application.go ApplicationCall.

The ApplicationCall applicator is given a reference to an instance of ApplyData struct, which holds an EvalDelta. The EvalDelta, upon evaluating the app's approval/state program, will hold the app call's effects: changes to global and local state, logs and inner txns, which will have already been evaluated. Upon returning from the applicator (ApplicationCall function), the ApplyData instance will be validated and the transactions will be tentatively added to the block which is being built.

In go-algorand, the outer group's evaluation revolves around the ApplyData data structure (and, for app calls, its EvalDelta field) of each transaction:

type ApplyData struct {
    _struct struct{} `codec:",omitempty,omitemptyarray"`

    // Closing amount for transaction.
    ClosingAmount basics.MicroAlgos `codec:"ca"`

    // Closing amount for asset transaction.
    AssetClosingAmount uint64 `codec:"aca"`

    // Rewards applied to the Sender, Receiver, and CloseRemainderTo accounts.
    SenderRewards   basics.MicroAlgos `codec:"rs"`
    ReceiverRewards basics.MicroAlgos `codec:"rr"`
    CloseRewards    basics.MicroAlgos `codec:"rc"`
    EvalDelta       EvalDelta         `codec:"dt"`

    // If asa or app is being created, the id used. Else 0.
    // Names chosen to match naming the corresponding txn.
    // These are populated on when MaxInnerTransactions > 0 (TEAL 5)
    ConfigAsset   basics.AssetIndex `codec:"caid"`
    ApplicationID basics.AppIndex   `codec:"apid"`
}

type EvalDelta struct {
    _struct struct{} `codec:",omitempty,omitemptyarray"`

    GlobalDelta basics.StateDelta `codec:"gd"`

    // When decoding EvalDeltas, the integer key represents an offset into
    // [txn.Sender, txn.Accounts[0], txn.Accounts[1], ...]
    LocalDeltas map[uint64]basics.StateDelta `codec:"ld,allocbound=config.MaxEvalDeltaAccounts"`

    Logs []string `codec:"lg,allocbound=config.MaxLogCalls"`

    InnerTxns []SignedTxnWithAD `codec:"itx,allocbound=config.MaxInnerTransactionsPerDelta"`
}

An instance of [EvalParams](https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/logic/eval.go#L248()) is created in ledger/internal/eval.go transactionGroup and is reused for every transaction of the group.

How it translates to KAVM (coarse-grained)

I think it indeed makes sense to implement a "flat" transaction scheme and get rid of the <txGroup> cell. I think it makes sense to also refactor the configuration to closer match the entities in go-algorand. We should have several Map cells that will hold <transaction> sub-cells and move them around while evaluating. See the proposed refactor of AVM-CONFIGURATION:

  configuration
    <kavm>
      <k> $PGM:AVMSimulation </k>
      <returncode exit=""> 4 </returncode> // the simulator exit code
      <returnstatus>                       // the exit status message
        "Failure - AVM is stuck"
      </returnstatus>

      // Transactions as submitted.
      // We need to assign them IDs and perform some validation:
      // * It may be reasonable to require them all to have the same `group`
      <submittedTransactions>
          <transaction multiplicity="*" type="Map">
             ... // our normal <transaction> cell from `txn.md`
          </transaction>
      </submittedTransactions>

      // The transactions waiting to be evaluated, with txn IDs already assigned.
      // This cell will initially hold the outer group, and will be appended with
      // inner groups as they are submitted by `itxn_submit`.
      // The pool will be flat, and the grouping will be determined by the `<group>` cell.
      <transactionPool>
          <transaction multiplicity="*" type="Map">
             ... // our normal <transaction> cell from `txn.md`
          </transaction>
      <transactionPool>

      // That's where all the work will happen. This cell will roughly corresspond to the `<kavm>` cell pre-refactoring.
      // We need to be careful which transactions are brought into scope and how and when they are taken from it when confirmed.
      // I propose to bring them as a whole group and take them out also as a group, i.e.
      // when a transaction is confirmed, it does not leave the execution context (i.e. the `<activeTransactions>` set cell) until the whole group is confirmed.
      <avmExecution>
        <currentTx> _:Int </currentTx>
        <txnDeque>
          <deque>         .List </deque>
          <dequeIndexSet> .Set  </dequeIndexSet>
        </txnDeque>
        <executionContext>
          // Needed for `*txn*` opcodes which will access  `<transactionPool>`, `<confirmedTransactions>`,
          // but must be only be allowed to look at these specific IDs.
          // Another good name may be `<availibleTransactions>`.
          <activeTransactions>
              .Set[Int]
          </activeTransactions>
          <currentTxnExecution>
            // Globals are mostly immutable during the group execution,
            // besides the application-related fields: CurrentApplicationID, CreatorID
            // and CurrentApplicationAddress
            <globals/>

            // the `<teal>` cell will control evaluation of TEAL code of the current transaction.
            // The semantics of TEAL has *read-only* access to the `<blockchain>` cell
            // and *read-write* access to the `<effects>` cell.
            <teal/>

            // the inner group. When submitted with `itxn_submit`, the transactions should go to `<submittedTransactions>`.
            <innerTransactions>
            </innerTransactions>
          </currentTxnExecution>
        </executionContext>

        // This cell will hold a stack of `<executionContext>`. A context switch is triggered by `itxn_submit`.
        <contextStack>
            .List
        </contextStack>
      </avmExecution>

      // Successfully evaluated transactions
      <confirmedTransactions>
          <transaction multiplicity="*" type="Map">
             ... // our normal <transaction> cell from `txn.md`
          </transaction>
      <confirmedTransactions>

      // The blockchain state will be incrementally updated after
      // each transaction in the group. If one of the transactions fails,
      // we will see the partial update
      <blockchain/>
    </kavm>

We initialize the semantics with the "outer" transaction group in the <submittedTransactions>.

If itxn_submit is encountered, we should:

Once the deque is empty, we finalize the execution and commit the outer groups' changes if no error occurred. If at any point we encounter an error, we can carefully reconstruct the whole call-stack, precisely to the lines of TEAl code and transaction id in every call-stack frame.

At the end of a successful execution, the <transactionPool> must be empty; the <confirmedTransactions> must contain the outer transaction group first and then the inner groups it may have generated in the order of evaluation. The <executionCOntext> cell must be cleaned-up. If the execution fails, <transactionPool> will have the outer group, perhaps some of the inner groups and, at the end, the group which caused failure. The <executionContext> will have the partial execution of the rejected transaction in the last active group.

Excerpts from go-algorand (for reference)

Transaction evaluation

The TransactionPool is the top-level entry point for us. It handles transaction groups' validation and caches the valid ones to be included into the next block.

ledger/internal/eval.go transactionGroup tries to execute the group. Iterates through the group calling eval.transaction, which calls applyTransaction, which refers to the logic specific for each transaction type. The most interesting is ledger/apply/application.go ApplicationCall.

TEAL evaluation

Evaluation context

Evaluation flow

While evaluating, the deltas to global state, local state, logs and inner txns are recorded as EvalDelta.

Opcodes semantics

The rest of the data/transactions/logic/eval.go file contains functions that evaluate the TEAL opcodes and a number of helper functions. Some interesting ones are:

Account/App/ASA availability

Inner transactions

Transaction validation logic in go-algorand

It is vital that we perform the same checks that the reference implementation. The source code of the transaction validation logic can be found in the go-algorand/data/transactions/transaction.go.

https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/transaction.go#L302

jannotti commented 2 years ago

Warning: v6 will be able to call back to v4 as of the next consensus upgrade.

On Tue, Sep 6, 2022 at 6:13 AM Georgy Lukyanov @.***> wrote:

Application accounts should be implemented. Inner transacations charge the application account of the contract for the fees.

The application account is also charged for the amounts of the Payment and AssetTransfer inner transactions that the application submits.

Budget pooling should be handled, although we don't even have basic opcode budgeting right now.

Yes, this should be on our todo list, though I'd say it's low priority. We can add rules that calculate execution costs on top later. We will consult KEVM on that.

Update availability rules so that assets/apps created earlier by top level or inner transactions are available, as well as the contract accounts of contracts created in already executed inner transactions.

Yes, we should specify the availability rules as implemented in go-algorand:

-

availableAccount https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/logic/eval.go#L4326 --- push an available account address. Calls accountReference.

accountReference https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/logic/eval.go#L3659 --- push an account address and also checks account availability

availableApp https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/logic/eval.go#L4326 --- push an available app id. Calls appReference.

appReference https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/logic/eval.go#L4015 pushes an app id and also checks application availability

availableAsset https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/logic/eval.go#L4326 --- push an available asset id. Calls asaReference.

asaReference https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/logic/eval.go#L4057 pushes an asa id and also checks asset availability

Access to executed inner transactions' fields through itxn, itxna, gitxn, gitxna

In go-algorand, the transaction are access by the txnFieldToStack https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/logic/eval.go#L2302 function, which is used by the whole txn family of opcodes. The function has an inner bool flag and changes its behaviour depending on whether the txn is inner or not. I suggest we also implement a centralised txn field accessor which will work for both normal and inner txns. More on that later.

Check how different program versions interact

The interaction is somewhat complicated. Basically, AVM6 (the current) smart contracts are not allowed to call older versions. I suggest we structure the semantics with AVM6 in mind and don't support older versions. We, however, may need to introduce versioning once we've implemented AVM6.

I'm replying to the rest of the questions in bulk, by proposing some more specific steps, let's discuss.

Digging through go-algorand, I see there's a very reasonable scheme of how transactions are stored when evaluating application calls.

The process starts in ledger/internal/eval.go transactionGroup https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/ledger/internal/eval.go#L918 which tries to execute the group. It iterates through the group, calling eval.transaction https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/ledger/internal/eval.go#L1031, which assigns the transaction id and calls applyTransaction https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/ledger/internal/eval.go#L1109, which refers to the logic specific for each transaction type, which we can call transaction applicators. We are mostly interested in ledger/apply/application.go ApplicationCall https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/ledger/apply/application.go#L340 .

The ApplicationCall applicator is given a reference to an instance of ApplyData https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/transaction.go#L104 struct, which holds an EvalDelta https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/teal.go#L29. The EvalDelta, upon evaluating the app's approval/state program, will hold the app call's effects: changes to global and local state, logs and inner txns, which will have already been evaluated. Upon returning from the applicator (ApplicationCall function), the ApplyData instance will be validated and the transactions will be tentatively added to the block which is being built.

In go-algorand, the outer group's evaluation revolves around the ApplyData data structure (and, for app calls, its EvalDelta field) of each transaction:

type ApplyData struct { _struct struct{} codec:",omitempty,omitemptyarray"

// Closing amount for transaction. ClosingAmount basics.MicroAlgos codec:"ca"

// Closing amount for asset transaction. AssetClosingAmount uint64 codec:"aca"

// Rewards applied to the Sender, Receiver, and CloseRemainderTo accounts. SenderRewards basics.MicroAlgos codec:"rs" ReceiverRewards basics.MicroAlgos codec:"rr" CloseRewards basics.MicroAlgos codec:"rc" EvalDelta EvalDelta codec:"dt"

// If asa or app is being created, the id used. Else 0. // Names chosen to match naming the corresponding txn. // These are populated on when MaxInnerTransactions > 0 (TEAL 5) ConfigAsset basics.AssetIndex codec:"caid" ApplicationID basics.AppIndex codec:"apid" } type EvalDelta struct { _struct struct{} codec:",omitempty,omitemptyarray"

GlobalDelta basics.StateDelta codec:"gd"

// When decoding EvalDeltas, the integer key represents an offset into // [txn.Sender, txn.Accounts[0], txn.Accounts[1], ...] LocalDeltas map[uint64]basics.StateDelta codec:"ld,allocbound=config.MaxEvalDeltaAccounts"

Logs []string codec:"lg,allocbound=config.MaxLogCalls"

InnerTxns []SignedTxnWithAD codec:"itx,allocbound=config.MaxInnerTransactionsPerDelta" }

An instance of EvalParams https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/logic/eval.go#L248() is created in ledger/internal/eval.go transactionGroup https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/ledger/internal/eval.go#L918 and is reused for every transaction of the group.

How it translates to KAVM (coarse-grained)

I think it indeed makes sense to implement a "flat" transaction scheme and get rid of the cell. I think it makes sense to also refactor the configuration to closer match the entities in go-algorand. We should have several Map cells that will hold sub-cells and move them around while evaluating. See the proposed refactor of AVM-CONFIGURATION:

configuration

$PGM:AVMSimulation 4 // the simulator exit code // the exit status message "Failure - AVM is stuck" // Transactions as submitted. // We need to assign them IDs and perform some validation: // * It may be reasonable to require them all to have the same `group` ... // our normal cell from `txn.md` // The transactions waiting to be evaluated, with txn IDs already assigned. // This cell will initially hold the outer group, and will be appended with // inner groups as they are submitted by `itxn_submit`. // The pool will be flat, and the grouping will be determined by the `` cell. ... // our normal cell from `txn.md` // That's where all the work will happen. This cell will roughly corresspond to the `` cell pre-refactoring. // We need to be careful which transactions are brought into scope and how and when they are taken from it when confirmed. // I propose to bring them as a whole group and take them out also as a group, i.e. // when a transaction is confirmed, it does not leave the execution context (i.e. the `` set cell) until the whole group is confirmed. _:Int .List .Set // Needed for `*txn*` opcodes which will access ``, ``, // but must be only be allowed to look at these specific IDs. // Another good name may be ``. .Set[Int] // Globals are mostly immutable during the group execution, // besides the application-related fields: CurrentApplicationID, CreatorID // and CurrentApplicationAddress // the `` cell will control evaluation of TEAL code of the current transaction. // The semantics of TEAL has *read-only* access to the `` cell // and *read-write* access to the `` cell. // the inner group. When submitted with `itxn_submit`, the transactions should go to ``. // This cell will hold a stack of ``. A context switch is triggered by `itxn_submit`. .List // Successfully evaluated transactions ... // our normal cell from `txn.md` // The blockchain state will be incrementally updated after // each transaction in the group. If one of the transactions fails, // we will see the partial update

We initialize the semantics with the "outer" transaction group in the

. - We iterate through the transactions to assign them IDs and move them to . We append the IDs to the . Then we start the evaluation loop: pop a transaction from front and evaluate. The cell will hold encapsulate the references to data required for evaluation of the active group. Evaluation of every transaction will happen in the cell which roughly corresponds to the EvalContext structure of go-algorand. If itxn_submit is encountered, we should: - copy (or move?) the inner transaction from to - push the cell onto and initialize a new one - *push the current transaction id back onto the deque* - generate transaction IDs for the inner group (see here how) - *put them in front* of txnDeque, keeping their order and *burying the parent txn ID*. - proceed executing the transactions from the deque as normal, going up to 8 levels deep into inner calls (and failing if too deep). - before every execution, we check if the popped ID is the parent txn ID, and if it is, we *commit the inner group's changes* and restore the parent execution context. - proceed with the execution of the parent. Once the deque is empty, we finalize the execution and commit the outer groups' changes if no error occurred. If at any point we encounter an error, we can carefully reconstruct the whole call-stack, precisely to the lines of TEAl code and transaction id in every call-stack frame. At the end of a successful execution, the must be empty; the must contain the outer transaction group first and then the inner groups it may have generated in the order of evaluation. The cell must be cleaned-up. If the execution fails, will have the outer group, perhaps some of the inner groups and, at the end, the group which caused failure. The will have the partial execution of the rejected transaction in the last active group. ------------------------------ Excerpts from go-algorand (for reference) - Calculating transaction id - For inner txns, see here - ledger/internal/eval.go TestTransactionGroup checks that all txns have the same group id Transaction evaluation The TransactionPool is the top-level entry point for us. It handles transaction groups' validation and caches the valid ones to be included into the next block. ledger/internal/eval.go transactionGroup tries to execute the group. Iterates through the group calling eval.transaction , which calls applyTransaction , which refers to the logic specific for each transaction type. The most interesting is ledger/apply/application.go ApplicationCall . TEAL evaluation Evaluation context - LedgerForSignature --- what stateless programs (logic sigs) can access - LedgerForLogic --- what stateful programs (smart contracts) can access - EvalParams --- evaluation parameters of a TEAL program - NewEvalParams --- evaluation parameters to use while evaluating a *top-level* txgroup - NewInnerEvalParams --- evaluation parameters to use while evaluating an *inner* txgroup - EvalContext --- the execution context of AVM bytecode. Evaluation flow - The eval function evaluates the program by repeatedly calling the step function until either the program terminates or runs out of execution budget. - The check function iterates through the bytecode and performs static sanity-checks by calling checkStep . While evaluating, the deltas to global state, local state, logs and inner txns are recorded as EvalDelta . Opcodes semantics The rest of the data/transactions/logic/eval.go file contains functions that evaluate the TEAL opcodes and a number of helper functions. Some interesting ones are: - getTxId --- establishes the relation between transaction ids and their group index. Special logic for inner txns. - txnFieldToStack extracts a transaction field and serialises it into a stack-friendly value (uint64 or bytes). - stackIntoTxnField is the reverse of txnFieldToStack. - opTxnImpl --- unified implementation of txn/gtxn/itxn/etc. opcodes. - getLastInnerGroup --- extract the last inner transaction group. - getApplicationAddress --- get the address of the app's account. Calls data/basics/userBalance.go Address internally to compute the hash of the app id. Account/App/ASA availability - accountReference pushes an account address and also checks *account availability* - availableAccount --- wrapper over accountReference for newer opcodes - appReference pushes an app id and also checks *application availability* - availableApp --- wrapper over appReference for newer opcodes - asaReference pushes an asa id and also checks *asset availability* - availableAsset --- wrapper over assetReference for newer opcodes Inner transactions - addInnerTxn is the implementation of itxn_begin and itxn_next. It build a new txn and adds it to EvalContext.subtxns. - opItxnField implements itxn_field. Set a filed of the currently building inner txn. - opItxnSubmit implements itxn_submit. Checks that the built inner transactions are all authorised and well-formed and handles fee pooling. For app calls: disallows reentrancy and checks call depth by traversing the call stack. Calculates the group id for inners by folding the parent id and hashing, see here and here . Finally, calls Ledged.Perform to compute eval deltas to be recorded into EvalContex.txn.EvalDelta.InnerTxns. Transaction validation logic in go-algorand It is vital that we perform the same checks that the reference implementation. The source code of the transaction validation logic can be found in the go-algorand/data/transactions/transaction.go. - Single unsigned transaction validation https://github.com/algorand/go-algorand/blob/eeeb7c38f7c9bd1b9c44c3515d669579e9c6535d/data/transactions/transaction.go#L302 — Reply to this email directly, view it on GitHub , or unsubscribe . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>
nwatson22 commented 2 years ago

Some more thoughts and clarifications of my previous ones:

It seems like we might not need to keep track of effects as state deltas. It is easier to write the semantics to have immediate effects on the blockchain cell (they are already written that way). If we ever need to support rolling back for failed transactions (which we shouldn't have to yet), we could just make a copy of the blockchain cell before the outer transaction group executes and then restore it if it fails. There is also no need to do this for every inner transaction group, because if they fail, the blockchain is reverted to before the beginning of the first outer transaction. I might just not be understanding the intended purpose of the <effects> cell, though.

I like the idea to consolidate transaction logic into one function with an inner flag. Right now I have loadFromGroup. It currently uses the transaction's group index (index within the group) to identify transactions, does some checks, and calls getTxnField which is the actual lookup. This could also be used with inner transactions. We would just have to get the last inner group ID and pass that in.

I'm not sure if we need 3 separate transaction pools. I see how it might be cleaner to have access to the transactions unmodified, and to keep the finished and unfinished transactions logically separated, but is this actually needed for anything? (maybe for examining after failure)

The <contextStack> is indeed redundant. We'd be keeping two stacks that always mirror each other (<contextStack> and <txnDeque>. Maybe we should just put the execution context inside the transaction object? Or maybe have the context be a separate Map (TxnID -> Context).

Instead of keeping <activeTransactions> updated, can we just figure out a good way to associate transactions into groups?

<innerTransactions> (and, I think <lastTxnGroupID>) don't need to be saved as part of the execution context, since every time we switch contexts, we either submit/flush the inner transaction group being built there or are exiting from an inner transaction, and the last transaction group ID will change, since we are submitting a new group, or exiting from a transaction.

Non-exhaustive list of pre-transaction-execution checks:

Main configuration sketch:

  configuration
    <kavm>
      <k> $PGM:AVMSimulation </k>
      <returncode exit=""> 4 </returncode> // the simulator exit code
      <returnstatus>                       // the exit status message
        "Failure - AVM is stuck"
      </returnstatus>

      // All transactions seen so far. At the beginning, the outer transaction group will
      // be inserted into here and then each inner group will be added on `itxn_submit`.
      // The txn IDs and the group IDs should be computed before insertion.
      // The pool will be flat, and the grouping will be determined by the `<group>` cell.
      <transactionPool>
          <transaction multiplicity="*" type="Map">
             <txnExecutionContext/> // Copy of `<avmExecution>`
             ... // our normal <transaction> cell from `txn.md`
          </transaction>
      <transactionPool>

      // That's where all the work will happen. This cell will roughly corresspond to the `<kavm>` cell pre-refactoring.
      <avmExecution>
        <currentTx> _:Int </currentTx>
        <txnDeque>
          <deque>         .List </deque>
          <dequeIndexSet> .Set  </dequeIndexSet>
        </txnDeque>
        <executionContext>

          // Some globals are constant for all transactions
          //  - MinTxnFee, MinBalance, MaxTxnLife, ZeroAddress
          // some are constant within a single transaction but can vary within a group
          //  - CurrentApplicationID, CreatorAddress, CurrentApplicationAddress
          // some are constant within a single group
          //  - GroupSize, GroupID, CallerApplicationID?, CallerApplicationAddress?
          // some are dynamic properties of the blockchain
          //  - Round, LatestTimestamp
          // some are dynamic within a single transaction
          //  - OpcodeBudget
          // Unsure
          //  - LogicSigVersion
          // 
          // Due to this, storing some of the globals in the execution context is redundant, but necessary if
          // we want to keep all the globals logically together.
          <globals/>

          // logs and saved scratch space moved out from directly inside the transaction and into the
          // executionContext for uniformity
          <logs/>

          // the `<teal>` cell will control evaluation of TEAL code of the current transaction.
          // The semantics of TEAL should be able to simply read and immediately update the `<blockchain>` cell.
          <teal/>

        </executionContext>

        <lastTxnGroupID> _:Int </lastTxnGroupID>

        // the inner group. When submitted with `itxn_submit`, the transactions should go to `<submittedTransactions>`.
        <innerTransactions/>

      </avmExecution>

      // The blockchain state will be incrementally updated after
      // each transaction in the group. If one of the transactions fails,
      // we will see the partial update
      <blockchain/>
    </kavm>
geo2a commented 2 years ago

Thanks for the heads-up @jannotti!

geo2a commented 2 years ago

The contract-to-contact calls (AVM6) feature is in master.