Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Transaction docs copy edit #589

Merged
merged 7 commits into from
Apr 15, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion docs/architecture/execution.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ The Miden execution model describes how state progresses on an individual level

Every transaction results in a ZK proof that attests to its correctness.

As mentioned in [transaction modes](transactions/modes.md), there are two types of transactions: local and network. For every transaction there is a proof which is either created by the user in the Miden client or by the operator using the Miden node.
There are two types of transactions: local and network. For every transaction there is a proof which is either created by the user in the Miden client or by the operator using the Miden node.

## Transaction batching

Expand Down
28 changes: 18 additions & 10 deletions docs/architecture/transactions/contexts.md
Original file line number Diff line number Diff line change
@@ -1,16 +1,22 @@
Miden assembly program execution can span multiple isolated contexts. An execution context defines its own memory space which is not accessible from other execution contexts. Note scripts cannot directly write into account data. This should be possible if only if the account exposes respective functions.
## Context overview

The kernel program always starts executing in a root context. Thus, the prologue sets the memory for the root context. To move execution into a different context, we can invoke a procedure using the `call` or `dyncall` instruction. In fact, any time we invoke a procedure using the `call` instruction, the procedure is executed in a new context.
Miden assembly program execution, the code the transaction kernel runs, spans multiple isolated contexts. An execution context defines its own memory space which is inaccessible from other execution contexts. Note scripts cannot directly write to account data which should only be possible if the account exposes relevant functions.

While executing in a note, account, or tx script context, we can request to execute some procedures in the kernel context, which is where all necessary information was stored during the prologue. Switching to the kernle context can be done via the `syscall` instruction. The set of procedures which can be invoked via the `syscall` instruction is limited by the [transaction kernel API](https://github.com/0xPolygonMiden/miden-base/blob/main/miden-lib/asm/kernels/transaction/api.masm). Once the procedure call via `syscall` returns, the execution moves back to the note, account, or tx script from which it was invoked.
## Specific contexts

The kernel program always starts executing from a root context. Thus, the prologue sets the memory for the root context. To move execution into a different context, the kernel invokes a procedure using the `call` or `dyncall` instruction. In fact, any time the kernel invokes a procedure using the `call` instruction, it executes in a new context.

While executing in a note, account, or tx script context, the kernel executes some procedures in the kernel context, which is where all necessary information was stored during the prologue. The kernel switches context via the `syscall` instruction. The set of procedures invoked via the `syscall` instruction is limited by the [transaction kernel API](https://github.com/0xPolygonMiden/miden-base/blob/main/miden-lib/asm/kernels/transaction/api.masm). When the procedure called via `syscall` returns, execution moves back to the note, account, or tx script where it was invoked.

## Context switches

<center>
![Architecture core concepts](../../img/architecture/transaction/transaction-contexts.png)
![Transaction contexts](../../img/architecture/transaction/transaction-contexts.png)
</center>

The above diagram shows different context switches in a simple transaction. In this example, an account consumes a [P2ID](https://github.com/0xPolygonMiden/miden-base/blob/main/miden-lib/asm/note_scripts/P2ID.masm) note and receives the asset into its vault. As with in any MASM program, the transaction kernel program starts in the root context. It executes the Prologue and stores all necessary information into the root memory.
The above diagram shows different context switches in a simple transaction. In this example, an account consumes a [P2ID](https://github.com/0xPolygonMiden/miden-base/blob/main/miden-lib/asm/note_scripts/P2ID.masm) note and receives the asset into its vault. As with any MASM program, the transaction kernel program starts in the root context. It executes the prologue and stores all necessary information into the root memory.

The next step, note processing, starts with a `dyncall` and in doing so, invoking the note script. This command moves execution into a different context **(1)**. In this new context, the note has no access to the kernel memory. After a successful ID check, which changes back to the kernel context twice to get the note inputs and the account id, the script executes the `add_note_assets_to_account` procedure.
The next step, note processing, starts with a `dyncall` which invokes the note script. This command moves execution into a different context **(1)**. In this new context, the note has no access to the kernel memory. After a successful ID check, which changes back to the kernel context twice to get the note inputs and the account id, the script executes the `add_note_assets_to_account` procedure.

```arduino
# Pay-to-ID script: adds all assets from the note to the account, assuming ID of the account
Expand All @@ -25,7 +31,7 @@ begin
end
```

The procedure cannot simply add assets to the account, because it is executed in a note context. Therefore, it needs to `call` the account interface. And in doing so, it moves execution into a second context - Account context - isolated from the note context **(2)**.
The procedure cannot simply add assets to the account, because it is executed in a note context. Therefore, it needs to `call` the account interface. This moves execution into a second context - account context - isolated from the note context **(2)**.

```arduino
#! Helper procedure to add all assets of a note to an account.
Expand All @@ -45,7 +51,7 @@ proc.add_note_assets_to_account
end
```

The [wallet](https://github.com/0xPolygonMiden/miden-base/blob/main/miden-lib/asm/miden/contracts/wallets/basic.masm) smart contract provides an interface for accounts to recieve and send assets. In this new context, the wallet calls the `add_asset` procedure of the account API.
The [wallet](https://github.com/0xPolygonMiden/miden-base/blob/main/miden-lib/asm/miden/contracts/wallets/basic.masm) smart contract provides an interface that accounts use to receive and send assets. In this new context, the wallet calls the `add_asset` procedure of the account API.

```arduino
export.receive_asset
Expand All @@ -54,7 +60,7 @@ export.receive_asset
end
```

The [account API](https://github.com/0xPolygonMiden/miden-base/blob/main/miden-lib/asm/miden/account.masm#L162) exposes procedures to manage accounts. This particular procedure that was called by the wallet invokes a `syscall` to return back to the root context **(3)**, where the account vault is stored in memory (see Prologue). `syscall` can incoke all procedures defined in the [Kernel API](https://github.com/0xPolygonMiden/miden-base/blob/main/miden-lib/asm/kernels/transaction/api.masm).
The [account API](https://github.com/0xPolygonMiden/miden-base/blob/main/miden-lib/asm/miden/account.masm#L162) exposes procedures to manage accounts. This particular procedure that was called by the wallet invokes a `syscall` to return back to the root context **(3)**, where the account vault is stored in memory (see prologue). `syscall` can incoke all procedures defined in the [Kernel API](https://github.com/0xPolygonMiden/miden-base/blob/main/miden-lib/asm/kernels/transaction/api.masm).

```arduino
#! Add the specified asset to the vault.
Expand All @@ -64,4 +70,6 @@ export.add_asset
end
```

Now, the asset can be safely added to the vault within the kernel context and the note successfully be processed.
Now, the asset can be safely added to the vault within the kernel context, and the note can be successfully processed.

<br/>
52 changes: 31 additions & 21 deletions docs/architecture/transactions/execution.md
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you think we need a transition to the next chapter, the kernel?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

let's chat about the flow in this doc because i need to understand it better, and to answer your question, maybe yes

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, let's have a short call. I will ping you after lunch

Original file line number Diff line number Diff line change
@@ -1,38 +1,48 @@
# Transaction Execution
Transactions are being executed by the Miden Transaction Executor. Transaction execution results in a `ExecutedTransaction` object and consists of the following steps:
The Miden transaction executor is the component that executes transactions.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know how yet, but we could also try embedding this explanation here (https://crates.io/crates/miden-tx) into this chapter.

My explanation has more information, but I like how concise the explanation on crate.io is. Also, when we show this code, it might be easier for some readers to follow.

What do you think?

------8<------

The first requirement is to have a DataStore implementation. DataStore objects are responsible to load the data needed by the transactions executor, specially the account's code, the reference block data, and the note's inputs.

let store = DataStore:new();

Once a store is available, a TransactionExecutor object can be used to execute a transaction. Consuming a zero or more notes, and possibly calling some of the account's code.

let executor = TransactionExecutor::new(store);
let executed_transaction = executor.execute_transaction(account_id, block_ref, note_ids, tx_args);

With the transaction execution done, it is then possible to create a proof:

let prover = TransactionProver::new(ProvingOptions::default());
let proven_transaction = prover.prove_transaction(executed_transaction);

And to verify a proof:

let verifier = TransactionVerifier::new(SECURITY_LEVEL);
verifier.verify(proven_transaction);

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is more of an API doc so I would add it separately in an API section of the docs, not in the architecture section ... let me know and i can do that

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok, indeed. Let's keep this as an architecture section

Transaction execution consists of the following steps and results in a `ExecutedTransaction` object:

1. Fetch the data required to execute a transaction from the data store.
2. Compile the transaction into an executable [MASM](https://0xpolygonmiden.github.io/miden-vm/user_docs/assembly/main.html) program using the transaction compiler.
3. Execute the transaction program and create an `ExecutedTransaction` object.
4. Prove the `ExecutedTransaction` using the Transaction Prover.
4. Prove the `ExecutedTransaction` using the transaction prover.

<center>
![Architecture core concepts](../../img/architecture/transaction/transaction-execution-process.png)
![Transaction execution process](../../img/architecture/transaction/transaction-execution-process.png)
</center>

One of the main reasons for splitting execution and proving is that it allows to have "stateless provers" - i.e., the executed transaction contains all data needed to re-execute and prove a transaction (no database access is needed). This is very powerful and allows the distribution of proof generation much more easily.
One of the main reasons for separating out the execution and proving steps is to allow _stateless provers_; i.e. the executed transaction has all the data it needs to re-execute and prove a transaction without database access. This supports easier proof-generation distribution.

## Data store and transaction inputs

The data store defines the interface that transaction objects use to fetch the data for transaction executions. Specifically, it provides the following inputs to the transaction:

- `Account` data which includes the [AccountID](../accounts.md#account-id) and the [AccountCode](../accounts.md#code) that is executed during the transaction.
- A `BlockHeader` which contains metadata about the block, commitments to the current state of the chain, and the hash of the proof that attests to the integrity of the chain.
- A `ChainMmr` which authenticates consumed notes during transaction execution. Authentication is achieved by providing an inclusion-proof for the transaction's consumed notes against the `ChainMmr`-root associated with the latest block known at the time of transaction execution.
- `InputNotes` consumed by the transaction that include the corresponding note data, e.g. the [note script](../notes.md#the-note-script) and serial number.

!!! note
- `InputNotes` must be already recorded on-chain in order for the transaction to succeed. - There is no nullifier-check during a transaction. Nullifiers are checked by the Miden operator during transaction verification. So at the transaction level, there is "double spending".

## Transaction compiler

Every transaction is executed within the Miden VM to generate a transaction proof. In Miden, there is a proof for every transaction.

## The Data Store and Transaction Inputs
The data store defines the interface that transaction objects use to fetch data required for transaction execution. It stores account, chain, and input note data required to execute a transaction against the account with the specified ID.
The transaction compiler is responsible for building executable programs. The generated MASM programs can then be executed by the Miden VM which generates a zk-proof. In addition to transaction compilation, the transaction compiler provides methods for compiling Miden account code, note scripts, and transaction scripts.

Specifically, it must provide the following inputs to the transaction
Compilation results in an executable MASM program. The program includes the provided account interface and notes, an optional transaction script, and the [transaction kernel program](kernel.md). The transaction kernel program defines procedures and the memory layout for all parts of the transaction.

- the `Account` including the [AccountID](https://0xpolygonmiden.github.io/miden-base/architecture/accounts.html#account-id) and the [AccountCode](https://0xpolygonmiden.github.io/miden-base/architecture/accounts.html#code) which will be executed during the transaction.
- the `BlockHeader`, which contains metadata about the block, commitments to the current state of the chain and the hash of the proof that attests to the integrity of the chain.
- the `ChainMmr`, which allows for efficient authentication of consumed notes during transaction execution. Authentication is achieved by providing an inclusion proof for the consumed notes in the transaction against the `ChainMmr`-root associated with the latest block known at the time of transaction execution.
- the `InputNotes` that are being consumed in the transaction (InputNotes), including the corresponding note data, e.g. the [note script](https://0xpolygonmiden.github.io/miden-base/architecture/notes.html#script) and [serial number](https://0xpolygonmiden.github.io/miden-base/architecture/notes.html#serial-number).
After compilation, assuming correctly-populated inputs, including the advice provider, the transaction can be executed.

_Note: The `InputNotes` must all be already recorded on-chain in order for the transaction to succeed. And there is no Nullifier-check during a transaction. Nullifiers are being checked by the Miden Operator during transaction verification. So at the transaction level, there is "double spending"._
## Executed transactions and the transaction outputs

## The Transaction Compiler
Every transaction must be executed within the Miden VM to generate a transaction proof. In Miden there is a proof for every transaction. The transaction compiler is responsible for building executable programs. The generated programs - MASM programs - can then be executed on the Miden VM which generates a zkProof. In addition to transaction compilation, the transaction compiler provides methods which can be used to compile Miden account code, note scripts, and transaction scripts.
The `ExecutedTransaction` object represents the result of a transaction not its proof. From this object, the account and storage delta can be extracted. Furthermore, the `ExecutedTransaction` is an input to the transaction prover.

Compilation results in an executable MASM Program, including the provided account interface and notes, an optional transaction script and the [Transaction Kernel Program](kernel.md). The Transaction Kernel Program defines procedures and the memory layout for all parts of the transaction. A detailed description can be found in the next section.
A successfully executed transaction results in a new account state which is a vector of all created notes (`OutputNotes`) and a vector of all the consumed notes (`InputNotes`) together with their nullifiers.

Finally, after the transaction program has been compiled and the inputs including the advice provider were correctly populated, the transaction can be executed.
## Transaction prover

## The Executed Transaction and the Transaction Outputs
The `ExecutedTransaction` object represents the result of a transaction - not its proof yet. From it, the account, and storage delta can be extracted. Furthermore, it serves as an input of the transaction prover to generate the proof. A successfully executed transaction results in a new state of the provided account, a vector of all created Notes (`OutputNotes`) and a vector of all the consumed Notes (`InputNotes`) together with their Nullifiers.
The transaction prover proves the inputted `ExecutedTransaction` and returns a `ProvenTransaction` object. The Miden node verifies the `ProvenTransaction` object using the transaction verifier and, if valid, updates the [state](../state.md) databases.

## The Transaction Prover
The Transaction Prover proves the provided `ExecutedTransaction` and returns a `ProvenTransaction` object. This object can be verified by the Miden Node using the Transaction Verifier and if valid updating the [State](../../architecture/state.md) databases.
<br/>
Loading
Loading