Skip to content

Commit

Permalink
Merge pull request #1056 from 0xPolygonMiden/bobbin-tsmt-wrapup
Browse files Browse the repository at this point in the history
SMT cleanup and `peek` decorator
  • Loading branch information
bobbinth authored Aug 31, 2023
2 parents 7a05e66 + 0aa1ffc commit 3a51a58
Show file tree
Hide file tree
Showing 11 changed files with 505 additions and 332 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
- Added support for the arithmetic expressions in constant values (#1026).
- Added support for module aliases (#1037).
- Added `adv.insert_hperm` decorator (#1042).
- Added `adv.push_smtpeek` decorator (#1056).

#### VM Internals
- Simplified range checker and removed 1 main and 1 auxiliary trace column (#949).
Expand Down
36 changes: 21 additions & 15 deletions assembly/src/ast/nodes/advice.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,8 @@ pub enum AdviceInjectorNode {
PushU64div,
PushExt2intt,
PushSmtGet,
PushSmtInsert,
PushSmtSet,
PushSmtPeek,
PushMapVal,
PushMapValImm { offset: u8 },
PushMapValN,
Expand All @@ -37,7 +38,8 @@ impl From<&AdviceInjectorNode> for AdviceInjector {
PushU64div => Self::DivU64,
PushExt2intt => Self::Ext2Intt,
PushSmtGet => Self::SmtGet,
PushSmtInsert => Self::SmtInsert,
PushSmtSet => Self::SmtSet,
PushSmtPeek => Self::SmtPeek,
PushMapVal => Self::MapValueToStack {
include_len: false,
key_offset: 0,
Expand Down Expand Up @@ -72,7 +74,8 @@ impl fmt::Display for AdviceInjectorNode {
PushU64div => write!(f, "push_u64div"),
PushExt2intt => write!(f, "push_ext2intt"),
PushSmtGet => write!(f, "push_smtget"),
PushSmtInsert => write!(f, "push_smtinsert"),
PushSmtSet => write!(f, "push_smtset"),
PushSmtPeek => write!(f, "push_smtpeek"),
PushMapVal => write!(f, "push_mapval"),
PushMapValImm { offset } => write!(f, "push_mapval.{offset}"),
PushMapValN => write!(f, "push_mapvaln"),
Expand All @@ -92,16 +95,17 @@ impl fmt::Display for AdviceInjectorNode {
const PUSH_U64DIV: u8 = 0;
const PUSH_EXT2INTT: u8 = 1;
const PUSH_SMTGET: u8 = 2;
const PUSH_SMTINSERT: u8 = 3;
const PUSH_MAPVAL: u8 = 4;
const PUSH_MAPVAL_IMM: u8 = 5;
const PUSH_MAPVALN: u8 = 6;
const PUSH_MAPVALN_IMM: u8 = 7;
const PUSH_MTNODE: u8 = 8;
const INSERT_MEM: u8 = 9;
const INSERT_HDWORD: u8 = 10;
const INSERT_HDWORD_IMM: u8 = 11;
const INSERT_HPERM: u8 = 12;
const PUSH_SMTSET: u8 = 3;
const PUSH_SMTPEEK: u8 = 4;
const PUSH_MAPVAL: u8 = 5;
const PUSH_MAPVAL_IMM: u8 = 6;
const PUSH_MAPVALN: u8 = 7;
const PUSH_MAPVALN_IMM: u8 = 8;
const PUSH_MTNODE: u8 = 9;
const INSERT_MEM: u8 = 10;
const INSERT_HDWORD: u8 = 11;
const INSERT_HDWORD_IMM: u8 = 12;
const INSERT_HPERM: u8 = 13;

impl Serializable for AdviceInjectorNode {
fn write_into<W: ByteWriter>(&self, target: &mut W) {
Expand All @@ -110,7 +114,8 @@ impl Serializable for AdviceInjectorNode {
PushU64div => target.write_u8(PUSH_U64DIV),
PushExt2intt => target.write_u8(PUSH_EXT2INTT),
PushSmtGet => target.write_u8(PUSH_SMTGET),
PushSmtInsert => target.write_u8(PUSH_SMTINSERT),
PushSmtSet => target.write_u8(PUSH_SMTSET),
PushSmtPeek => target.write_u8(PUSH_SMTPEEK),
PushMapVal => target.write_u8(PUSH_MAPVAL),
PushMapValImm { offset } => {
target.write_u8(PUSH_MAPVAL_IMM);
Expand Down Expand Up @@ -139,7 +144,8 @@ impl Deserializable for AdviceInjectorNode {
PUSH_U64DIV => Ok(AdviceInjectorNode::PushU64div),
PUSH_EXT2INTT => Ok(AdviceInjectorNode::PushExt2intt),
PUSH_SMTGET => Ok(AdviceInjectorNode::PushSmtGet),
PUSH_SMTINSERT => Ok(AdviceInjectorNode::PushSmtInsert),
PUSH_SMTSET => Ok(AdviceInjectorNode::PushSmtSet),
PUSH_SMTPEEK => Ok(AdviceInjectorNode::PushSmtPeek),
PUSH_MAPVAL => Ok(AdviceInjectorNode::PushMapVal),
PUSH_MAPVAL_IMM => {
let offset = source.read_u8()?;
Expand Down
8 changes: 6 additions & 2 deletions assembly/src/ast/parsers/adv_ops.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,12 @@ pub fn parse_adv_inject(op: &Token) -> Result<Node, ParsingError> {
2 => AdvInject(PushSmtGet),
_ => return Err(ParsingError::extra_param(op)),
},
"push_smtinsert" => match op.num_parts() {
2 => AdvInject(PushSmtInsert),
"push_smtset" => match op.num_parts() {
2 => AdvInject(PushSmtSet),
_ => return Err(ParsingError::extra_param(op)),
},
"push_smtpeek" => match op.num_parts() {
2 => AdvInject(PushSmtPeek),
_ => return Err(ParsingError::extra_param(op)),
},
"push_mapval" => match op.num_parts() {
Expand Down
20 changes: 18 additions & 2 deletions core/src/operations/decorators/advice.rs
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,22 @@ pub enum AdviceInjector {
/// - (1, 0): depth 32 -> 48
/// - (1, 1): depth 16, 32, or 48 -> 64
/// - E_KEY and E_VALUE are the key-value pair for a leaf which is to be replaced by a subtree.
SmtInsert,
SmtSet,

/// Pushes onto the advice stack the value associated with the specified key in a Sparse
/// Merkle Tree defined by the specified root.
///
/// If no value was previously associated with the specified key, [ZERO; 4] is pushed onto
/// the advice stack.
///
/// Inputs:
/// Operand stack: [KEY, ROOT, ...]
/// Advice stack: [...]
///
/// Outputs:
/// Operand stack: [KEY, ROOT, ...]
/// Advice stack: [VALUE, ...]
SmtPeek,

// ADVICE MAP INJECTORS
// --------------------------------------------------------------------------------------------
Expand Down Expand Up @@ -253,7 +268,8 @@ impl fmt::Display for AdviceInjector {
Self::Ext2Inv => write!(f, "ext2_inv"),
Self::Ext2Intt => write!(f, "ext2_intt"),
Self::SmtGet => write!(f, "smt_get"),
Self::SmtInsert => write!(f, "smt_insert"),
Self::SmtSet => write!(f, "smt_set"),
Self::SmtPeek => write!(f, "smt_peek"),
Self::MemToMap => write!(f, "mem_to_map"),
Self::HdwordToMap { domain } => write!(f, "hdword_to_map.{domain}"),
Self::HpermToMap => write!(f, "hperm_to_map"),
Expand Down
5 changes: 3 additions & 2 deletions docs/src/user_docs/assembly/io_operations.md
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,9 @@ Advice injectors fall into two categories: (1) injectors which push new data ont
| adv.push_mtnode | [d, i, R, ... ] | [d, i, R, ... ] | Pushes a node of a Merkle tree with root $R$ at depth $d$ and index $i$ from Merkle store onto the advice stack. |
| adv.push_u64div | [b1, b0, a1, a0, ...] | [b1, b0, a1, a0, ...] | Pushes the result of `u64` division $a / b$ onto the advice stack. Both $a$ and $b$ are represented using 32-bit limbs. The result consists of both the quotient and the remainder. |
| adv.push_ext2intt | [osize, isize, iptr, ... ] | [osize, isize, iptr, ... ] | Given evaluations of a polynomial over some specified domain, interpolates the evaluations into a polynomial in coefficient form and pushes the result into the advice stack. |
| adv.smt_get | [K, R, ... ] | [K, R, ... ] | Pushes values onto the advice stack which are required for successful retrieval of a value under the key $K$ from a Sparse Merkle Tree with root $R$. |
| adv.smt_insert | [V, K, R, ...] | [V, K, R, ...] | Pushes values onto the advice stack which are required for successful insertion of a key-value pair $(K, V)$ into a Sparse Merkle Tree with root $R$. |
| adv.smt_get | [K, R, ... ] | [K, R, ... ] | Pushes values onto the advice stack which are required for successful retrieval of a value under the key $K$ from a Sparse Merkle Tree with root $R$. |
| adv.smt_set | [V, K, R, ...] | [V, K, R, ...] | Pushes values onto the advice stack which are required for successful insertion of a key-value pair $(K, V)$ into a Sparse Merkle Tree with root $R$. |
| adv.smt_peek | [K, R, ... ] | [K, R, ... ] | Pushes value onto the advice stack which is associated with key $K$ in a Sparse Merkle Tree with root $R$. |
| adv.insert_mem | [K, a, b, ... ] | [K, a, b, ... ] | Reads words $data \leftarrow mem[a] .. mem[b]$ from memory, and save the data into $advice\_map[K] \leftarrow data$. |
| adv.insert_hdword <br> adv.insert_hdword.*d* | [B, A, ... ] | [B, A, ... ] | Reads top two words from the stack, computes a key as $K \leftarrow hash(A || b, d)$, and saves the data into $advice\_map[K] \leftarrow [A, B]$. $d$ is an optional domain value which can be between $0$ and $255$, default value $0$. |
| adv.insert_hperm | [B, A, C, ...] | [B, A, C, ...] | Reads top three words from the stack, computes a key as $K \leftarrow permute(C, A, B).digest$, and saves data into $advice\_mpa[K] \leftarrow [A, B]$. |
Expand Down
40 changes: 30 additions & 10 deletions docs/src/user_docs/stdlib/collections.md
Original file line number Diff line number Diff line change
@@ -1,22 +1,42 @@
# Collections
Namespace `std::collections` contains modules for commonly authenticated data structures.
Namespace `std::collections` contains modules for commonly-used authenticated data structures. This includes:

- A Merkle Mountain range.
- A Sparse Merkle Tree with 64-bit keys.
- A Sparse Merkle Tree with 256-bit keys.

## Merkle Mountain Range
Module `std::collections::mmr` contains procedures for manipulating [Merkle Mountain Range](https://github.com/opentimestamps/opentimestamps-server/blob/master/doc/merkle-mountain-range.md) data structure which can be used as an append-only log.

| Procedure | Description |
The following procedures are available to read data from and make updates to a Merkle Mountain Range.

| Procedure | Description |
| ----------- | ------------- |
| get | Loads the leaf at the absolute `pos` in the MMR onto the stack.<br /><br />Valid range for `pos` is between $0$ and $2^{32} - 1$ (both inclusive).<br /><br />Inputs:<br />- Operand stack: [pos, mmr_ptr, ...]<br /><br />Output:<br />- Operand stack: [N, ...]<br /><br />Where `N` is the leaf loaded from the MMR whose memory location starts at `mmr_ptr`. |
| add | Adds a new leaf to the MMR.<br /><br />This will update the MMR peaks in the VM's memory and the advice provider with any merged nodes.<br /><br />Inputs:<br />- Operand stack: [N, mmr_ptr, ...]<br /><br />Outputs:<br />- Operand stack: [...]<br /><br />Where `N` is the leaf added to the MMR whose memory locations starts at `mmr_ptr`. |
| pack | Computes the hash of the given MMR and copies it to the Advice Map using its hash as a key.<br /><br />Inputs:<br />- Operand stack: [mmr_ptr, ...]<br /><br />Outputs:<br />- Operand stack: [HASH, ...]<br /><br /> |
| unpack | Load the MMR peak data based on its hash.<br /><br />Inputs:<br />- Operand stack: [HASH, mmr_ptr, ...]<br /><br />Outputs:<br />- Operand stack: [...]<br /><br />Where:<br />- `HASH`: is the MMR peak hash, the hash is expected to be padded to an even length and to have a minimum size of 16 elements.<br />- The advice map must contain a key with `HASH`, and its value is `num_leaves \|\| hash_data`, and hash_data is the data used to computed `HASH`<br />- `mmt_ptr`: the memory location where the MMR data will be written, starting with the MMR forest (the total count of its leaves) followed by its peaks. |
| get | Loads the leaf at the absolute position `pos` in the MMR onto the stack.<br /><br />Valid range for `pos` is between $0$ and $2^{32} - 1$ (both inclusive).<br /><br />Inputs: `[pos, mmr_ptr, ...]`<br />Output: `[N, ...]`<br /><br />Where `N` is the leaf loaded from the MMR whose memory location starts at `mmr_ptr`. |
| add | Adds a new leaf to the MMR.<br /><br />This will update the MMR peaks in the VM's memory and the advice provider with any merged nodes.<br /><br />Inputs: `[N, mmr_ptr, ...]`<br />Outputs: `[...]`<br /><br />Where `N` is the leaf added to the MMR whose memory locations starts at `mmr_ptr`. |
| pack | Computes a commitment to the given MMR and copies the MMR to the Advice Map using the commitment as a key.<br /><br />Inputs: `[mmr_ptr, ...]`<br />Outputs: `[HASH, ...]`<br /><br /> |
| unpack | Load the MMR peak data based on its hash.<br /><br />Inputs: `[HASH, mmr_ptr, ...]`<br />Outputs: `[...]`<br /><br />Where:<br />- `HASH`: is the MMR peak hash, the hash is expected to be padded to an even length and to have a minimum size of 16 elements.<br />- The advice map must contain a key with `HASH`, and its value is `num_leaves \|\| hash_data`, and hash_data is the data used to computed `HASH`<br />- `mmt_ptr`: the memory location where the MMR data will be written, starting with the MMR forest (the total count of its leaves) followed by its peaks. |

## Sparse Merkle Tree (64)

Module `std::collections::smt64` contains procedures for manipulating key-value maps with single-element keys and 4-element values. The current implementation is a thin wrapper over a simple Sparse Merkle Tree of depth 64. In the future, this will be replaced with a compact Sparse Merkle Tree implementation.

| Procedure | Description |
The following procedures are available to read data from and make updates to a Sparse Merkle Tree.

| Procedure | Description |
| ----------- | ------------- |
| get | Returns the value located under the specified key in the Sparse Merkle Tree defined by the specified root.<br /><br />If no values had been previously inserted under the specified key, an empty word is returned.<br /><br />Inputs: `[key, ROOT, ...]`<br />Outputs: `[VALUE, ROOT, ...]`<br /><br />Fails if the tree with the specified root does not exist in the VM's advice provider. |
| set | Inserts the specified value under the specified key in a Sparse Merkle Tree defined by the specified root. If the insert is successful, the old value located under the specified key is returned via the stack.<br /><br />If `VALUE` is an empty word, the new state of the tree is guaranteed to be equivalent to the state as if the updated value was never inserted.<br /><br />Inputs: `[VALUE, key, ROOT, ...]`<br />Outputs: `[OLD_VALUE, NEW_ROOT, ...]`<br /><br />Fails if the tree with the specified root does not exits in the VM's advice provider. |
| insert | Inserts the specified value under the specified key in a Sparse Merkle Tree defined by the specified root. If the insert is successful, the old value located under the specified key is returned via the stack.<br /><br />This procedure requires that `VALUE` be a non-empty word.<br /><br />Inputs: `[VALUE, key, ROOT, ...]`<br />Outputs: `[OLD_VALUE, NEW_ROOT, ...]`<br /><br />Fails if:<br />- The tree with the specified root does not exits in the VM's advice provider.<br />- The provided value is an empty word. |

## Sparse Merkle Tree (256)

Module `std::collections::smt` contains procedures for manipulating key-value maps with 4-element keys and 4-element values. The underlying implementation is a Tiered (compacted) Sparse Merkle where leaves can exist only at specific depths called "tiers". These depths are: 16, 32, 48, and 64. Initially, when a tree is empty, it is equivalent to an empty Sparse Merkle Tree of depth 64 (i.e., leaves at depth 64 are set to [ZERO; 4]). As non-empty values are inserted into the tree, they are added to the first available tier.

The following procedures are available to read data from and make updates to a Sparse Merkle Tree.

| Procedure | Description |
| ----------- | ------------- |
| get | Returns the value located under the specified key in the Sparse Merkle Tree defined by the specified root.<br /><br />If no values had been previously inserted under the specified key, an empty word (i.e., [ZERO; 4]) is returned.<br /><br />Inputs:<br />- Operand stack: [key, ROOT, ...]<br /><br />Outputs:<br />-Operand stack: [VALUE, ROOT, ...]<br /><br />Fails if the tree with the specified root does not exist in the VM's advice provider. |
| set | Inserts the specified value under the specified key in a Sparse Merkle Tree defined by the specified root. If the insert is successful, the old value located under the specified key is returned via the stack.<br /><br />If `VALUE` is an empty word (i.e., [ZERO; 4]), the new state of the tree is guaranteed to be equivalent to the state as if the updated value was never inserted.<br /><br />Inputs:<br /> - Operand stack: [VALUE, key, ROOT, ...]<br /><br />Outputs:<br />- Operand stack: [OLD_VALUE, NEW_ROOT, ...]<br /><br />Fails if the tree with the specified root does not exits in the VM's advice provider. |
| insert | Inserts the specified value under the specified key in a Sparse Merkle Tree defined by the specified root. If the insert is successful, the old value located under the specified key is returned via the stack.<br /><br />This procedure requires that `VALUE` be a non-empty word (i.e., not [ZERO; 4]).<br /><br />Inputs:<br />- Operand stack: [VALUE, key, ROOT, ...]<br /><br />Outputs:<br /> -Operand stack: [OLD_VALUE, NEW_ROOT, ...]<br /><br />Fails if:<br />- The tree with the specified root does not exits in the VM's advice provider.<br />- The provided value is an empty word. |
| get | Returns the value located under the specified key in the Sparse Merkle Tree defined by the specified root.<br /><br />If no values had been previously inserted under the specified key, an empty word is returned.<br /><br />Inputs: `[KEY, ROOT, ...]`<br />Outputs: `[VALUE, ROOT, ...]`<br /><br />Fails if the tree with the specified root does not exist in the VM's advice provider. |
| set | Inserts the specified value under the specified key in a Sparse Merkle Tree defined by the specified root. If the insert is successful, the old value located under the specified key is returned via the stack.<br /><br />If `VALUE` is an empty word, the new state of the tree is guaranteed to be equivalent to the state as if the updated value was never inserted.<br /><br />Inputs: `[VALUE, KEY, ROOT, ...]`<br />Outputs: `[OLD_VALUE, NEW_ROOT, ...]`<br /><br />Fails if the tree with the specified root does not exits in the VM's advice provider. |
| insert | Inserts the specified value under the specified key in a Sparse Merkle Tree defined by the specified root. If the insert is successful, the old value located under the specified key is returned via the stack.<br /><br />This procedure requires that `VALUE` be a non-empty word.<br /><br />Inputs: `[VALUE, KEY, ROOT, ...]`<br />Outputs: `[OLD_VALUE, NEW_ROOT, ...]`<br /><br />Fails if:<br />- The tree with the specified root does not exits in the VM's advice provider.<br />- The provided value is an empty word. |
Loading

0 comments on commit 3a51a58

Please sign in to comment.