# Interval Merkle Tree: A Circuit-friendly Universal (Vector) Accumulator.
> This documents describes the APIs, inner working of **Interval Merkle Tree (IMT)**, a cryptographic accumulator that we use to instantiate _Nullifier Set_ which require efficient non-membership proof and member insertion in circuit.
## Complexity
For an IMT of height $h$ of size $N = 2^h$, batch insertion size $K=2^k, h > k$:
Both `Add` and `BatchAdd` circuit checked non-membership before inserting.
| | `Add` | `BatchAdd` |
| -------- | -------- | -------- |
| Native Execution |$O(\log N)$ |$O(K\cdot \log N)$ |
| Constraint Cost | $4h$ `hash` + $2$ `range_check` | $[2hK+2(h-k)+(K-1)]$ `hash` + $2K$ `range_check` |
E.g. $h=32, k=10$ for a Zcash sized Nullifier set and a ~1024 rollup capacity, `BatchAdd` requires `66,603` * Hash whereas naively `Add` one-by-one requires `131,072` Hash, and Sparse Merkle Tree would require `524,288` Hash! An almost **8x improvement in circuit size compared to SMT** (which is what Circom and Aztec Connect use) :rocket:
## Challenges
Compared to various non-membership constructions [in the literature](#Related-Work), our primary goal is **low circuit complexity**, as opposed to time & space complexity for different operations. Designing circuit-friendly data structures and their algorithms need to pay special attention to the following:
- **Input independence**: circuit configuration is independent of any input values (namely `(pub_input, secret_witness)` assignments), specifically this implies:
- _worse case complexity for loops_: constraining an algorithm that contains `for (i=0; i<n; i++)` loop with potential early return/termination requires always checking all `n` iterations in circuit.
- _combined branch complexity for conditions_: constraining an algorithm that contains `if (cond1) {do X} else if (cond2) {do Y} else {do Z}` conditional execution requires always constraining _all_ branches and chained together in a Disjunctive Normal Form: `(cond1=T AND cond2=F AND X) OR (cond1=F AND cond2=T AND Y) OR (cond1=F AND cond2=F AND Z)`.
- **Circuit-unfriendly Operations**: algebraic circuits natively execute finite field arithmetics and many operations could be expensive when translating to field operations, such as pairing in bilinear map, bit-wise operation (AND, XOR, SHL etc.), non-algebraic hash, non-native modular arithmetics. Apparently we want to minimize these operations as much as possible.
Here are some concrete implications:
- Sparse Merkle Tree (SMT) is very deep thus involves many hash operations for each Merkle path (accumulating field elements of 256 bits would require a binary SMT of height 256). Potential optimization leveraging on the observation that: "expected length of Merkle proof with $N$ accumulated elements is only $\log(N)$" leads to a rather complicated circuit logic dealing with many edge cases and occational longer paths.
- RSA accumulator requires modular arithmetics over a usually much larger modulus (for security) than that of the native field, which leads to high circuit complexity.
- Bilinear-map based accumulator usually involves pairing, another expensive operations. Worse, the number of group points in the Structured Reference String (SRS) required for these accumulators (such as [[DT08]](https://eprint.iacr.org/2008/538)) are linear with tree size. Currently, the [largest](https://github.com/weijiekoh/perpetualpowersoftau) trusted setup ceremony provides about $2^{28}$ such points, however, even for Zcash's [Nullifier set](https://raw.githubusercontent.com/zcash/zips/master/protocol/protocol.pdf#constants) is at least $2^{32}$ in capacity.
## Overview
**Core idea 1 (interval as leaf value):** transforming non-membership proof in set $X =\{x_1, x_2, \ldots, x_n \}$ to membership proof in set $Y = \{ (-\infty, x_1), (x_1, x_2), \ldots, (x_{n-1}, x_n) \}$.
E.g. for set $X=\{2,7\}$, we prove non-membership for $5$ by providing Merkle proof for the interval $(2,7)$ (in purple), and an interval check whether $2<5<7$ (in yellow):
```mermaid
flowchart TB
%% node shape & text def:
rt((rt)):::hl2
L((" ")):::none
R((" ")):::hl2
LL("(-#8734;, 2)"):::hl2
LR("(2, 7)"):::hl
RL("(7, +#8734;)"):::none
EMPTY("#8709;"):::none
%% graph def:
rt --- L & R
L --- LL & LR
R --- RL & EMPTY
nonmember([2< 5 <7]):::hl
classDef none fill:#f8f8f8,stroke:#595c5c;
classDef hl fill:#ffffde,stroke:#f3e4c5;
classDef hl2 fill:#f4ddff,stroke:#ebc3ff;
```
**Core idea 2 (replace and append):** During insertion of new member, split the containing interval into two smaller intervals. Replace the old interval, then append the other.
E.g. inserting $5$ will split $(2,7)$ into $(2,5), (5,7)$.
```mermaid
flowchart TB;
%% node shape & text def:
rt((rt)):::none
L((" ")):::none
R((" ")):::none
LL("(-#8734;, 2)"):::none
LR("(2, 5)"):::hl
RL("(7, +#8734;)"):::none
RR("(5, 7)"):::hl
%% graph def:
rt --- L & R
L --- LL & LR
R --- RL & RR
classDef none fill:#f8f8f8,stroke:#595c5c;
classDef hl fill:#ffffde,stroke:#f3e4c5;
```
Note that:
- The tree is of fixed height, _not_ an incremental tree.
- Intervals are bounded exclusively below and above (namely $2, 5 \notin (2,5)$).
- Intervals are unsorted/non-consecutive.
- Our IMT is a **universal accumulator** with dyanmic addition and deletion of elements, and support both membership and non-membership proofs.
- This accumulator is _order dependent_: different order of insertion of the same set may result in different tree state and digest.[^order_dep]
- If were not constraining correct insertion in circuit, we can enforce consecutive intervals (namely shift $(7,\infty)$ right 1 slot to make room for $(5,7)$), which will give order independence.
- Unfortunately, to keep the circuit [_input dependent_](#Challenges), we need to ensure a fixed number of "steps" for each insertion regardless of the state of the Merkle tree.
- The most efficient solution is leaving these intervals unordered during insertion[^alt_insert_sol], which necessitates another **"locator" to help remember the leaf indexes of inserted intervals** for fast locating. We instantiate this "locator" with a [B-Tree based Map](https://doc.rust-lang.org/std/collections/struct.BTreeMap.html) in practice. (detailed description [below](#Construction))
- due to order dependence, we should view IMT as a **vector accumulator scheme** (rather than a set accumulator) and the accumulator value as a vector commitment.
- This IMT was proposed way earlier by [Philippe et al.](https://users.dcc.uchile.cl/~pcamacho/papers/strongacc08.pdf) in 2008, but there are two problems of this data structure that potentially hinders its wider adoption in practice:
- requiring _structural integrity_ check: :warning: TODO (add def)
- _order dependence_ (as mentioned above): this results in either additional locator to help quickly locate insertion position at the cost of extra storage; or require sorting upon insertion & deletion which increase the cost of both operation to $O(n)$.[^insert_cost_CHKO08]
[^order_dep]: If deterministic reproducing of the accumulator state is required, then order dependent accumulator would be problematic _without total ordering of historical insertion instructions_. In our intended use case of Nullifier set in Blockchain, the total ordering is established externally since every transaction binds the order of nullifiers inside, and all transactions are further ordered using distributed consensus. Therefore all nullifiers to be inserted are ordered and every honest node can deterministically replay and get the same accumulator state.
_Order independence_ is more formally referred to as _quasi_
[^alt_insert_sol]: Otherwise we need to accommodate for the worst-case shift for every insertion since we can't have a variable number of shift per insertion. This solution is horrendously expensive.
[^insert_cost_CHKO08]: In [[CHKO08]](https://www.slideshare.net/philippecamacho/strong-accumulators-from-collisionresistant-hashing), the IMT is an incremental, balanced but NOT sorted tree, therefore, the insertion cost is already $O(n)$.
## Construction
We adapt from the definition, syntax and notation of a **trapdoorless universal accumulator** from [[BBF18]](https://eprint.iacr.org/2018/1188.pdf):
For optimization, we extend the definition above with one more algorithm:
- $\textbf{BatchAdd}(A_t, \{x_i\})\rightarrow \{A_{t+1}, \textbf{upmsg}\}\quad \text{batch insert new members}$
There are auxiliary output for accumulator update algorithms (namely $\textbf{Add, Del, BatchAdd}$) to help provers generate proof of correct update, which we highlight with :construction_worker:.
~~Note that due to impossibility of batch witness update by [[CH09]](https://eprint.iacr.org/2009/612.pdf), witness update for each time counter $t$ is enough, since info for batch update $\mathsf{upmsg}$ independent of number of updates (namely $|t_j - t_i|$) doesn't exist.~~
We further assume the existence of an algebraic hash function $\mathcal{H}: \mathbb{F}^2 \mapsto \mathbb{F}, \mathcal{H}_{*}: \mathbb{F}^3 \mapsto \mathbb{F}$, which we instantiate using [Rescue](https://eprint.iacr.org/2019/426) or [Poseidon](https://www.poseidon-hash.info/), modelled as a random oracle.
We denote $|\mathbb{F}|$ the bit-size of a prime field $\mathbb{F}$ with modulus $p$, any number represents a field element unless stated otherwise.
We denote _merkle path_ as the nodes along the path from leaf to root; _merkle proof_ as the slibing nodes along that path.
Our locator search trees should have the following APIs:
```rust!
use std::collections::BTreeMap;
let mut locator = BTreeMap::new(); // init setup
locator.insert(Fr::from(0), 0); // L=-inf at leaf index 0
locator.insert(Fr::from(2), 1); // L=2 at index 1
locator.insert(Fr::from(7), 2); // L=7 at index 2
locator.insert(Fr::from(5), 3); // L=5 at index 3
// leaves are now: (0,2), (2,5), (7,p-1), (5,7)
// task 1: checking if certain field element is a member
assert!(!locator.contains_key(&Fr::from(6)));
assert!(locator.contains_key(&Fr::from(5)));
// task 2: find the leaf index of a member
let idx = locator.get(&Fr::from(7)).unwrap();
asset_eq!(idx, 2);
// task 3: find the index of the interval a new member should insert into.
let idx = locator.range(Fr::from(6)).next().unwrap();
asset_eq!(idx, 3); // index 3 or 4th leaf is (5, 7) where 6 should insert
```
### Setup
- Inputs:
- security param: $\lambda =(|\mathbb{F}|, N)$
- initial set elements: $z =\{(0,p-1)\}$
- Outputs:
- public param: $\mathsf{pp} = (\mathbb{F}, N, \mathcal{H}, \mathcal{H}_*)$ include field $\mathbb{F}$, tree size $N$, hash function for internal nodes $\mathcal{H}$, for leaves $\mathcal{H}_*$,
- initial accumulator value: $A_0 =(\mathsf{rt, ctr})$ contains the root value plus a counter keeping track of number of non-empty leaves in the tree.
- Algorithms:
- Initialize locator tree: `let locator = BTreeMap::new();`
- Initialize IMT of size $N = 2^h$ with the first leaf being $(0,p-1)$ to represent the ideal $(-\infty,+\infty)$ using field elements; and populate the rest with $(0,0)$ as EMPTY leaves.
- Derive the merkle root `rt`, and assign the initial accumulator value $A_0=(rt, 1)$ to signify currently only 1 non-empty leaves.
- Update locator tree: `locator.insert(F::from(0), 0);`.
```mermaid
flowchart TB;
%% node shape & text def:
rt(["H( , ), ctr=1"]):::none
L(("H( , )")):::none
R((" ")):::none
LL(("H( , )")):::none
LR((" ")):::none
RL((" ")):::none
RR((" ")):::none
LLL("(0, p-1)"):::hl
LLR("(0, 0)"):::none
LRL("(0, 0)"):::none
LRR("(0, 0)"):::none
RLL("(0, 0)"):::none
RLR("(0, 0)"):::none
RRL("(0, 0)"):::none
RRR("(0, 0)"):::none
%% graph def:
rt --- L & R
L --- LL & LR
R --- RL & RR
LL --- LLL & LLR
LR --- LRL & LRR
RL --- RLL & RLR
RR --- RRL & RRR
classDef none fill:#f8f8f8,stroke:#595c5c;
classDef hl fill:#ffffde,stroke:#f3e4c5;
```
### Add
- Inputs
- current accumulator: $A_t$
- a new element: $x$
- Outputs
- updated accumlator: $A_{t+1}$
- info used to update proof: $\mathsf{upmsg}$
- :construction_worker: prover witness: $w_{+x}$
- Algorithms
- Query replacement index: `idx = locator.range(x).next().unwrap()` (`idx=0, ELEMS[idx]=(0,p-1)` in this example)
- Prepare new leaf $(L, R)$ to be inserted:
- $L = x$, $R=$`ELEMS[idx].R`
- Prepare replaced leaf $(L', R')$:
- $L'=$`ELEMS[idx].L`, $R'=x$
- Insert new leaf $(L, R)$ at position $A_t.\mathsf{ctr}$:
- add the Merkle proof of `ELEMS[ctr]` (exclude root) AND the new leaf to prover witenss: $w_{+x} \; ||= (L, R) \;|| \pi_+$ (purple nodes in diagram)
- append new leaf $(L, R)$ at position $A_t.\mathsf{ctr}$, update internal nodes, and finally compute the new root value $\mathsf{rt}_+$
- append to proof update info: $\mathsf{upmsg}\; ||= (ctr, path_{ctr})$ where $path$ is the _merkle path_ of `ELEMS[ctr]`
- in our example, path consists of _update_ values (w.r.t. $\mathsf{rt_+}$)
- update locator: `locator.insert((L,ctr)).unwrap();`
- Replace `LEAVES[idx]` with $(L', R')$:
- add the Merkle proof of `LEAVES[idx]` (exclude root which is $\mathsf{rt_+}$) to prover witness: $w_{+x} \; ||= \pi_\circlearrowleft$ (dashed nodes in the diagram, note that purple-dashed nodes were updated in the last step during insertion)
- note: $\pi_\circlearrowleft$ is basically the non-membership proof. It might be a little counterintuitive to see such a non-membership proof from an updated tree (with new leaf inserted) instead of the original tree. The main rationale is to unify circuit logic with $\textbf{BatchAdd}$ procedure
- replace `LEAVES[idx]` with $(L', R')$, update internal nodes, and compute the new root value $\mathsf{rt'}$ (transition from $\mathsf{rt_+}$)
- append to proof update info: $\mathsf{upmsg}\; ||= (idx, path_{idx})$
- Output $A_{t+1}= (\mathsf{rt', ctr\mathtt{++}}), \mathsf{upmsg}, w_{+x}$
```mermaid
flowchart TB;
%% node shape & text def:
rt(["H( , ), ctr=2"]):::none
L((" ")):::none
R((" ")):::hl2-dash
LL((" ")):::none
LR((" ")):::hl2-dash
RL((" ")):::none
RR((" ")):::none
LLL("(0, p-1)"):::hl2-dash
LLR("(0, 0)"):::hl2
LRL("(0, 0)"):::none
LRR("(0, 0)"):::none
RLL("(0, 0)"):::none
RLR("(0, 0)"):::none
RRL("(0, 0)"):::none
RRR("(0, 0)"):::none
LLL'("(0, 6)"):::none
LLR'("(6, p-1)"):::hl2-dash
new([x=6])
%% graph def:
rt --- L & R
L --- LL & LR
R --- RL & RR
LL --- LLL & LLR
LLL -.-> LLL'
LLR -.-> LLR'
LR --- LRL & LRR
RL --- RLL & RLR
RR --- RRL & RRR
classDef none fill:#f8f8f8,stroke:#595c5c;
classDef none-dash fill:#f8f8f8,stroke:#f66,stroke-width:2px,stroke-dasharray: 5 5;
classDef hl fill:#ffffde,stroke:#f3e4c5;
classDef hl2 fill:#f4ddff,stroke:#ebc3ff;
classDef hl2-dash fill:#f4ddff,stroke:#f66,stroke-width:2px,stroke-dasharray: 5 5;
```
### :star: BatchAdd
- Inputs
- current accumulator: $A_t$
- a batch of new elements: $\{x_i\}$
- :exclamation: we assume each batch has fixed size of $K=2^k$ for simpler circuit later, here we assume $K=4$
- we further assume $A_t.\mathsf{ctr} = a\cdot K -1$ for some $a\in\mathbb{N}_+$, namely there are in total $a\cdot K$ intervals/leaves.
(the problem with initial `(0,p-1)` leaf during setup can be dealt with using some "genesis block" mechanism to pad into multiple of $K$)
- Outputs
- updated accumlator: $A_{t+1}$
- info used to update proof: $\mathsf{upmsg}$
- :construction_worker: prover witness: $w_{+X}$
- Algorithm
- Prepare new leaves $\{(L_i^{new}, R_i^{new})\}_{i\in [K]}$ to be inserted:
- $L_i^{new} = x_i, R_i^{new}=\min{\{L_j: j<i \land L_j > L_i^{new}\}}$
- update locator: `locator.insert((L_i^new, ctr+i-1)).unwrap();`
- these intervals might be updated, but their `L` bound won't, thus it's safe to insert their positions to locator now
- Prepare leaves $\{(idx_j^{rep},L_j^{rep}, R_j^{rep})\}_{j\in [K]}$ to be replaced:
- query `idx_j = locator.range(x_j).next().unwrap();`
- $L_j^{rep} =$`LEAVES[idx_j].L`, $R_j^{rep} = x_j$
- Batch insert all new leaves:
- add merkle proof of the entire subtree to prover witness: $w_{+X} \; ||= \pi_+$ (red nodes in diagrams)
- note the root of the empty subtree is a public parameter and can be pre-computed
- insert $\{(L_i^{new}, R_i^{new})\}_{i\in [K]}$, compute the new subtree root, then update the overall tree root
- add all new leaves to prover witness: $w_{+X} \; ||= \{(L_i^{new}, R_i^{new})\}_{i\in [K]}$
- Replace leaves: for each $j\in[K]$, and its respective `idx_j` (searched during step 2):
- add merkle proof of `LEAVES[idx_j]` (against updated roots) to prover witness: $w_{+X} \; ||= \pi_\circlearrowleft^j$ (green nodes)
- replace leaf with $(L_j^{rep}, R_j^{rep})$, update roots
- add all replaced leaves to prover witness: $w_{+X} \; ||= \{(idx_j^{rep},L_j^{rep}, R_j^{rep})\}_{j\in [K]}$
- :warning: TODO: upmsg
- Output $A_{t+1}= (\mathsf{rt', ctr\mathtt{+=}}K), \mathsf{upmsg}, w_{+X}$
```mermaid
flowchart TB;
%% node shape & text def:
rt(["rt, ctr=4"]):::hl3
L((" ")):::hl3
R((" ")):::hl3
LL((" ")):::hl2
LR((" ")):::none
RL((" ")):::none
RR((" ")):::none
LLL("(0, 2)"):::none
LLR("(2, 6)"):::none
LRL("(9, p-1)"):::hl2
LRR("(6, 9)"):::hl2
RLL("(0, 0)"):::none
RLR("(0, 0)"):::none
RRL("(0, 0)"):::none
RRR("(0, 0)"):::none
new([inserted: 2,9,6. inserting: 12, 3, 20, 5])
RLL'("(12, p-1)"):::none
RLR'("(3, 6)"):::none
RRL'("(20, p-1)"):::none
RRR'("(5, 6)"):::none
LRL''("(9, 12)"):::none
LLR''("(2, 3)"):::none
RLL''("(12, 20)"):::none
RLR''("(3, 5)"):::none
%% graph def:
rt --- L & R
L --- LL & LR
LL --- LLL & LLR
LR --- LRL & LRR
LRL -..-> |j=1| LRL''
LLR -..-> |j=2| LLR''
subgraph batch insert K=4
direction LR
R --- RL & RR
RL --- RLL & RLR
RLL -.-> |i=1| RLL'
RLR -.-> |i=2| RLR'
RLL' -.-> |j=3| RLL''
RLR' -.-> |j=4| RLR''
RR --- RRL & RRR
RRL -.-> |i=3| RRL'
RRR -.-> |i=4| RRR'
end
classDef none fill:#f8f8f8,stroke:#595c5c;
classDef none-dash fill:#f8f8f8,stroke:#f66,stroke-width:2px,stroke-dasharray: 5 5;
classDef hl fill:#ffffde,stroke:#f3e4c5;
classDef hl2 fill:#ddffe7,stroke:#b6e2d3;
classDef hl3 fill:#ffd4db,stroke:#ef7c8e;
```
### Del
- Inputs
- current accumulator: $A_t$
- element to be removed: $x$
- Outputs
- updated accumlator: $A_{t+1}$
- info used to update proof: $\mathsf{upmsg}$
- :construction_worker: prover witness: $w_{-x}$ (TODO: will specify this later)
- Algorithm
- Query replacement positions: `idx_0 = locator.range(&9-1).next().unwrap(); idx_1 = locator.get(&9).unwrap();` (in our example, `idx_0=1, idx_1=3`)
- Replace `LEAVES[idx_0]` withx(LEAVES[idx_0].L, LEAVES[idx_1].R)`, updax Merkle root
- append updated nodes: $\mathsf{upmsg}\; ||= (idx_0, path_{idx_0})$
- Replace `LEAVES[idx_1]` with `LEAVES[ctr-1]`, update Merkle root
- append updated nodes: $\mathsf{upmsg}\; ||= (idx_1, path_{idx_1})$
- update locator: `locator.insert((LEAVES[ctr-1].L, idx_1)).unwrap();` and `locator.remove(x).unwrap();`
- Replace `LEAVES[ctr-1]` with `(0,0)`, update Merkle root
- append updated nodes: $\mathsf{upmsg}\; ||= (ctr-1, path_{ctr-1})$
- Decrement total non-empty leaves count: `ctr--`
- Output $A_{t+1}= (\mathsf{rt', ctr\mathtt{--}}), \mathsf{upmsg}, w_{
x}$
```mermaid
flowchart TB;
%% node shape & text def:
rt(["rt, ctr=5"]):::none
L((" ")):::none
R((" ")):::none
LL((" ")):::none
LR((" ")):::none
RL((" ")):::none
RR((" ")):::none
LLL("(0, 2)"):::none
LLR("(6, 9)"):::hl2
LRL("(2, 4)"):::none
LRR("(9, p-1)"):::hl2
RLL("(4, 6)"):::hl3
RLR("(0, 0)"):::none
RRL("(0, 0)"):::none
RRR("(0, 0)"):::none
new([insertion: 6,2,9,4. delete member: 9])
LLR'("(6, p-1)"):::hl2
LRR'("(4, 6)"):::hl3
RLL'("(0, 0)"):::none
%% graph def:
rt --- L & R
L --- LL & LR
R --- RL & RR
LL --- LLL & LLR
LLR -.-> LLR'
LR --- LRL & LRR
LRR -.-> LRR'
RL --- RLL & RLR
RLL -.-> RLL'
RR --- RRL & RRR
classDef none fill:#f8f8f8,stroke:#595c5c;
classDef none-dash fill:#f8f8f8,stroke:#f66,stroke-width:2px,stroke-dasharray: 5 5;
classDef hl fill:#ffffde,stroke:#f3e4c5;
classDef hl2 fill:#f4ddff,stroke:#ebc3ff;
classDef hl3 fill:#ffd4db,stroke:#ef7c8e;
```
### MemWitCreate
- Inputs
- accumulator at time $t$: $A_t$
- claimed member: $x$
- vector of elements inserted: $S=\emptyset$ (unnecessary for us)
- Outputs
- membership witness: $w_x^t$
- Algorithm
- Query position: `idx = locator.get(9).unwrap();` (`idx=3` in our example)
- Return the merkle proof of `LEAVES[idx]` (marked in purple) as $w_x^t$
```mermaid
flowchart TB;
%% node shape & text def:
rt(["rt, ctr=4"]):::hl2
L((" ")):::none
R((" ")):::hl2
LL((" ")):::hl2
LR((" ")):::none
RL((" ")):::none
RR((" ")):::none
LLL("(0, 2)"):::none
LLR("(6, 9)"):::none
LRL("(2, 4)"):::hl2
LRR("(9, p-1)"):::hl
RLL("(4, 6)"):::none
RLR("(0, 0)"):::none
RRL("(0, 0)"):::none
RRR("(0, 0)"):::none
new([insertion: 6,2,9,4. check member: 9])
%% graph def:
rt --- L & R
L --- LL & LR
R --- RL & RR
LL --- LLL & LLR
LR --- LRL & LRR
RL --- RLL & RLR
RR --- RRL & RRR
classDef none fill:#f8f8f8,stroke:#595c5c;
classDef none-dash fill:#f8f8f8,stroke:#f66,stroke-width:2px,stroke-dasharray: 5 5;
classDef hl fill:#ffffde,stroke:#f3e4c5;
classDef hl2 fill:#f4ddff,stroke:#ebc3ff;
classDef hl2-dash fill:#f4ddff,stroke:#f66,stroke-width:2px,stroke-dasharray: 5 5;
```
### NonMemWitCreate
- Inputs
- accumulator at time $t$: $A_t$
- claimed non-member: $x$
- vector of elements inserted: $S=\emptyset$ (unnecessary for us)
- Outputs
- non-membership witness: $u_x^t$
- Algorithm
- Query containing interval position: `idx = locator.get(12).unwrap();` (`idx=3` in our example, checking $12\notin S$ in the same diagram above)
- Return the merkle proof of `LEAVES[idx]` (marked in purple) as $u_x^t$
### MemWitUp & NonMemWitUp (same algorithm)
- Inputs
- old accumulator: $A_t$
- old (non)-membership proof: $w_x^t$ or $u_x^t$
- claimed (non)-member: $x$
- update info: $\mathsf{upmsg}_{t \rightarrow t+1}$
- Outputs
- new (non)-membership proof: $w_x^{t+1}$ or $u_x^t$
- Algorithm
- Query index of (non)-member: `let idx = locator.get(x).unwrap();`
- ```rust
// note: merkle_path is NOT merkle_proof,
// path: from leaf to root; proof: silbings of nodes along the path.
for (pos, merkle_path) in upmsg {
// e.g. the updated leaf `pos` is 010, `idx` of member is 000
// then the 0-prefix of `pos XOR idx` (which is first 0 in 010)
// indicates which node in `merkle_proof` should be updated.
// in this case: `merkle_proof[depth=1] = merkle_path[depth=1]`.
//
// Also always update the root: `merkle_proof[rt] = merkle_path[rt]`
update_merkle_proof(idx, &mut merkle_proof, pos, &merkle_path);
// another e.g.
// updated leaf `pos` is 010, `idx` of member is 011
// then `010 ^ 011 = 001`, thus `merkle_proof[depth=1,2]` would be
// updated with values `merkle_path[depth=1,2]`.
// finally, `merkle_proof[rt] = merkle_path[rt]`
}
```
- :warning: TODO: this algorithm is not complete, it's possible your non-membership leaf position gets updated. the above two steps only deal with situation where leaf position wasn't changed (such as all membership proof)
```mermaid
flowchart TB;
%% node shape & text def:
rt(["rt, ctr=3 -->4"]):::hl2
L((" ")):::hl2
R((" ")):::hl2
LL((" ")):::none
LR((" ")):::hl2
RL((" ")):::hl2
RR((" ")):::none
LLL("(0, 2)"):::none
LLR("(6, 9)"):::none
LRL("(2, 6)"):::hl2
LRR("(9, p-1)"):::none
RLL("(0, 0)"):::hl2
RLR("(0, 0)"):::none
RRL("(0, 0)"):::none
RRR("(0, 0)"):::none
new([insertion: 6,2,9. inserted at t: 4])
LRL'("(2, 4)"):::none
RLL'("(4, 6)"):::none
%% graph def:
rt --- |0| L
rt --- |1| R
L --- |00| LL
L --- |01| LR
R --- |10| RL
R --- |11| RR
LL --- |000| LLL
LL --- |001| LLR
LR --- |010| LRL
LR --- |011| LRR
LRL -.-> LRL'
RL --- |100| RLL
RL --- |101| RLR
RLL -.-> RLL'
RR --- |110| RRL
RR --- |111| RRR
classDef none fill:#f8f8f8,stroke:#595c5c;
classDef none-dash fill:#f8f8f8,stroke:#f66,stroke-width:2px,stroke-dasharray: 5 5;
classDef hl fill:#ffffde,stroke:#f3e4c5;
classDef hl2 fill:#f4ddff,stroke:#ebc3ff;
classDef hl2-dash fill:#f4ddff,stroke:#f66,stroke-width:2px,stroke-dasharray: 5 5;
```
### VerMem
- Inputs
- accumulator at time $t$: $A_t$
- claimed member: $x$
- membership witness: $w_x^t$
- Outputs
- success: $b\in \{0,1\}$
- Algorithm
- Verify Merkle proof $w_x^t$ of leaf $(L, R)$
- Check $x \overset{?}{=} L \land L \neq 0$
### VerNonMem
- Inputs
- accumulator at time $t$: $A_t$
- claimed member: $x$
- non-membership witness: $u_x^t$
- Outputs
- success: $b\in \{0,1\}$
- Algorithm
- Verify Merkle proof $u_x^t$ of leaf $(L, R)$
- Check $L < x < R$
## Constraints
### Building blocks
- `recompute_root(pos, leaf, proof) -> root`: given the leaf position `pos`, leaf value `leaf` and siblings of its path `proof`, recompute the `root` of this subtree
- cost: `len(proof) * Hash`
- `compute_root(leaves) -> root`: given $K=2^k$ leaves, compute the tree root.
- cost: $\sum_{i=1}^{k-1}{2^i}=2^k-1 = K-1$ `* Hash`
### Batch Check & Insert Gadget
- Statement: Given a correctly computed old accumulator $A_t$ of the IMT, there exists a vector of $K=2^k$ new non-members such that applying $\textbf{BatchAdd}(A_t, \{x_i\}_{i\in[K]})$ will result in new accumulator value $A_{t+1}$.
- Public Input:
- Old accumulator: $A_t$
- New accumulator: $A_{t+1}$
- Root of empty subtree of size $K$: $h_\emptyset^K$
- Secret Witness:
- New vector of non-members: $\{x_i\}_{i\in[K]}$
- Prover witness from `BatchAdd`: $w_{+X}$
- Circuit Logic:
- Verify correct $K$-subtree to insert:
- parse $\pi_+$ from $w_{+X}$ (red nodes)
- <u>enforce</u>: $A_t.\mathsf{rt} == \mathtt{recompute \_root}(A_t.\mathsf{ctr} \gg k, h_\emptyset^K, \pi_+)$
- Batch insert and update merkle root:
- parse $\{(L_i^{new}, R_i^{new})\}_{i \in [K]}$ from $w_{+X}$ (red dashed nodes)
- <u>check</u> $L_i^{new}<R_i^{new} \land L_i^{new} = x_i$ for $\forall i\in [K]$
- <u>compute</u> new $K$-subtree root: $h^K=\mathtt{compute\_root}( \{ (L_i^{new}, R_i^{new}) \}_{i\in[K]})$
- <u>compute new</u> root upon insertion: $\mathsf{rt}_+=\mathtt{recompute\_root}(A_t.\mathsf{ctr}\gg k, h^K, \pi_+)$
- Check and replace, parse $\{(idx_j^{rep}, L_j^{rep}, R_j^{rep})\}_{j \in [K]}$ (blue dashed nodes) and `LEAVES[idx_j]` (parent of blue dashed nodes) from $w_{+X}$ , let $\mathsf{rt}'=\mathsf{rt}_+$,
<u>for each $j\in [K]$, do:</u>
- Verify non-membership:
- <u>enforce</u> $\mathsf{rt}' ==\mathtt{recompute\_root}(idx_j^{rep}, (L_j^{rep}, R_j^{rep}), \pi_\circlearrowleft^j)$
- <u>enforce</u> (`LEAVES[idx_j].L`$<x_j$) AND (`LEAVES[idx_j].R` $=R_j^{new}$)
- note: we don't need to check $x_j<R_j$ because we effectively cover that during insertion
- <u>Check</u> correct replacement: `LEAVES[idx_j].L` $=L_j^{rep} \land R_j^{rep}=x_j$
- <u>compute</u> updated root after replacement: $\mathsf{rt}' = \mathtt{recompute\_root}(idx_j^{rep}, (L_j^{rep}, R_j^{rep}), \pi_\circlearrowleft^j)$
- Finally, check new accumulator:
- <u>check</u> $(\mathsf{rt}' == A_{t+1}.\mathsf{rt}) \land (A_t.\mathsf{ctr} + K = A_{t+1}.\mathsf{ctr})$
```mermaid
flowchart TB;
%% node shape & text def:
rt(["rt, ctr=4"]):::hl3
L((" ")):::hl3
R((" ")):::hl3
LL((" ")):::hl2
LR((" ")):::none
RL((" ")):::none
RR((" ")):::none
LLL("(0, 2)"):::none
LLR("(2, 6)"):::none
LRL("(9, p-1)"):::hl2
LRR("(6, 9)"):::hl2
RLL("(0, 0)"):::none
RLR("(0, 0)"):::none
RRL("(0, 0)"):::none
RRR("(0, 0)"):::none
new([inserted: 2,9,6. inserting: 12, 3, 20, 5])
RLL'("(12, p-1)"):::none-dash
RLR'("(3, 6)"):::none-dash
RRL'("(20, p-1)"):::none-dash
RRR'("(5, 6)"):::none-dash
LRL''("(9, 12)"):::none-dash2
LLR''("(2, 3)"):::none-dash2
RLL''("(12, 20)"):::none-dash2
RLR''("(3, 5)"):::none-dash2
%% graph def:
rt --- L & R
L --- LL & LR
LL --- LLL & LLR
LR --- LRL & LRR
LRL -..-> |j=1| LRL''
LLR -..-> |j=2| LLR''
subgraph batch insert K=4
direction LR
R --- RL & RR
RL --- RLL & RLR
RLL -.-> |i=1| RLL'
RLR -.-> |i=2| RLR'
RLL' -.-> |j=3| RLL''
RLR' -.-> |j=4| RLR''
RR --- RRL & RRR
RRL -.-> |i=3| RRL'
RRR -.-> |i=4| RRR'
end
classDef none fill:#f8f8f8,stroke:#595c5c;
classDef none-dash fill:#f8f8f8,stroke:#f66,stroke-width:2px,stroke-dasharray: 5 5;
classDef none-dash2 fill:#f8f8f8,stroke:#0000ff,stroke-width:2px,stroke-dasharray: 5 5;
classDef hl fill:#ffffde,stroke:#f3e4c5;
classDef hl2 fill:#ddffe7,stroke:#b6e2d3;
classDef hl3 fill:#ffd4db,stroke:#ef7c8e;
```
## Security Proofs
We show that the structure integrity of our IMT can be captured by the following 3 invariants:
1. All left range include all member _exactly once_ plus a negative infinity represented by `0`:$\{L_i\} = \{x_i\} \cup \{0\}$
2. All right range include all member _exactly once_ plus a positive infinity represented by `p-1`:$\{R_i\} = \{x_i\} \cup \{0\}$
3. $L_i < R_i$ for $\forall i<A_t.\mathsf{ctr}$
Then we proceed to prove that our `Add`, `BatchAdd`, `Del` preserves all 3 invariants.
:warning: TBD
Finally, we argue that our constraints sufficiently enforce the `BatchAdd` algorithm.
:warning: TBD
:warning: TODO: losing adaptive security (but still sufficient for our use cases) where adv hands you the accumulator and provide valid proof of membership AND non-membership.
## Caching Strategies
Given the _locator_ B-Tree, we are able to deterministically reconstruct the IMT.
By caching some Merkle path in the IMT, we can achieve space-time efficiency tradeoff during tree update.
When using IMT in a non-universal setting (specifically insertion only, no deletion, such as our Nullifier set), we could enjoy the following pruning:
The main observation is that
- "smaller the interval, less likely the leaf will be updated, so are the nodes on its Merkle path to the root".
- On one extreme, leaves with interval value such as $(23, 24)$ won't be updated.
- Merkle frontier will always gets updated during insertion, thus should be kept in cache.
## Adapting to Different Arity
Given different arity (i.e. number of children per internal node) of the Merkle Tree, we need to adapt all algorithms and constraints above.
We first demonstrate 3-ary tree:
## Related Work
TBD: simply literature review/related work, plus some comparison to justify our design and advantanges.
SMT, Balaced Tree, RSA accumulators, Bilinear-map accumulators.
Sign in with Wallet
Connect another wallet