chore: add bmt formal verification

program-libs/batched-merkle-tree/Cargo.toml

@@ -9,6 +9,7 @@ edition = "2021"
 [features]
 default = ["solana"]
 test-only = []
+kani = []
 solana = [
     "solana-program-error",
     "solana-account-info",
@@ -59,6 +60,9 @@ light-merkle-tree-reference = { workspace = true }
 light-account-checks = { workspace = true, features = ["test-only"] }
 light-compressed-account = { workspace = true, features = ["new-unique"] }
 light-hasher = { workspace = true, features = ["keccak"] }
+light-indexed-array = { workspace = true }
+num-bigint = { workspace = true }
+num-traits = { workspace = true }
 
 [lints.rust.unexpected_cfgs]
 level = "allow"

program-libs/batched-merkle-tree/docs/CLAUDE.md

@@ -0,0 +1,148 @@
+# Batched Merkle Tree Library
+
+The `light-batched-merkle-tree` crate provides batched Merkle tree implementations for the Light Protocol account compression program. Instead of updating trees one leaf at a time, this library batches multiple insertions and updates them with zero-knowledge proofs (ZKPs), enabling efficient on-chain verification. Trees maintain a cyclic root history for validity proofs, and use bloom filters for non-inclusion proofs while batches are being filled.
+
+There are two tree types: **state trees** (two accounts tree account (input queue, tree metadata, roots), output queue account) for compressed accounts, and **address trees** (one account that contains the address queue, tree metadata, roots) for address registration.
+
+## Accounts
+
+### Account Types
+
+- **[TREE_ACCOUNT.md](TREE_ACCOUNT.md)** - BatchedMerkleTreeAccount (state and address trees)
+- **[QUEUE_ACCOUNT.md](QUEUE_ACCOUNT.md)** - BatchedQueueAccount (output queue for state trees)
+
+### Overview
+
+The batched merkle tree library uses two main Solana account types:
+
+**BatchedMerkleTreeAccount:**
+The main tree account storing tree roots, root history, and integrated input queue (bloom filters + hash chains for nullifiers or addresses). Used for both state trees and address trees.
+
+**Details:** [TREE_ACCOUNT.md](TREE_ACCOUNT.md)
+
+**BatchedQueueAccount:**
+Output queue account for state trees that temporarily stores compressed account hashes before tree insertion. Enables immediate spending via proof-by-index.
+
+**Details:** [QUEUE_ACCOUNT.md](QUEUE_ACCOUNT.md)
+
+### State Trees vs Address Trees
+
+**State Trees (2 accounts):**
+- `BatchedMerkleTreeAccount` with integrated input queue (for nullifiers)
+- Separate `BatchedQueueAccount` for output operations (appending new compressed accounts)
+
+**Address Trees (1 account):**
+- `BatchedMerkleTreeAccount` with integrated input queue (for addresses)
+- No separate output queue
+
+## Operations
+
+### Initialization
+- **[INITIALIZE_STATE_TREE.md](INITIALIZE_STATE_TREE.md)** - Create state tree + output queue pair (2 solana accounts)
+  - Source: [`src/initialize_state_tree.rs`](../src/initialize_state_tree.rs)
+
+- **[INITIALIZE_ADDRESS_TREE.md](INITIALIZE_ADDRESS_TREE.md)** - Create address tree with integrated queue (1 solana account)
+  - Source: [`src/initialize_address_tree.rs`](../src/initialize_address_tree.rs)
+
+### Queue Insertion Operations
+- **[INSERT_OUTPUT_QUEUE.md](INSERT_OUTPUT_QUEUE.md)** - Insert compressed account hash into output queue (state tree)
+  - Source: [`src/queue.rs`](../src/queue.rs) - `BatchedQueueAccount::insert_into_current_batch`
+
+- **[INSERT_INPUT_QUEUE.md](INSERT_INPUT_QUEUE.md)** - Insert nullifiers into input queue (state tree)
+  - Source: [`src/merkle_tree.rs`](../src/merkle_tree.rs) - `BatchedMerkleTreeAccount::insert_nullifier_into_queue`
+
+- **[INSERT_ADDRESS_QUEUE.md](INSERT_ADDRESS_QUEUE.md)** - Insert addresses into address queue
+  - Source: [`src/merkle_tree.rs`](../src/merkle_tree.rs) - `BatchedMerkleTreeAccount::insert_address_into_queue`
+
+### Tree Update Operations
+- **[UPDATE_FROM_OUTPUT_QUEUE.md](UPDATE_FROM_OUTPUT_QUEUE.md)** - Batch append with ZKP verification
+  - Source: [`src/merkle_tree.rs`](../src/merkle_tree.rs) - `BatchedMerkleTreeAccount::update_tree_from_output_queue_account`
+
+- **[UPDATE_FROM_INPUT_QUEUE.md](UPDATE_FROM_INPUT_QUEUE.md)** - Batch nullify/address updates with ZKP
+  - Source: [`src/merkle_tree.rs`](../src/merkle_tree.rs) - `update_tree_from_input_queue`, `update_tree_from_address_queue`
+
+## Key Concepts
+
+**Batching System:** Trees use 2 alternating batches. While one batch is being filled, the previous batch can be updated into the tree with a ZKP.
+
+**ZKP Batches:** Each batch is divided into smaller ZKP batches (`batch_size / zkp_batch_size`). Trees are updated incrementally by ZKP batch.
+
+**Bloom Filters:** Input queues (nullifier queue for state trees, address queue for address trees) use bloom filters for non-inclusion proofs. While a batch is filling, values are inserted into the bloom filter. After the batch is fully inserted into the tree and the next batch is 50% full, the bloom filter is zeroed to prevent false positives. Output queues do not use bloom filters.
+
+**Value Vecs:** Output queues store the actual compressed account hashes in value vectors (one per batch). Values can be accessed by leaf index even before they're inserted into the tree, enabling immediate spending of newly created compressed accounts.
+
+**Hash Chains:** Each ZKP batch has a hash chain storing the Poseidon hash of all values in that ZKP batch. These hash chains are used as public inputs for ZKP verification.
+
+**ZKP Verification:** Tree updates require zero-knowledge proofs proving the correctness of batch operations (old root + queue values → new root). Public inputs: old root, new root, hash chain (commitment to queue elements), and for appends: start_index (output queue) or next_index (address queue).
+
+**Root History:** Trees maintain a cyclic buffer of recent roots (default: 200). This enables validity proofs for recently spent compressed accounts even as the tree continues to update.
+
+**Rollover:** When a tree reaches capacity (2^height leaves), it must be replaced with a new tree. The rollover process creates a new tree and marks the old tree as rolled over, preserving the old tree's roots for ongoing validity proofs. A rollover can be performed once the rollover threshold  is met (default: 95% full).
+
+**State vs Address Trees:**
+- **State trees** have a separate `BatchedQueueAccount` for output operations (appending new leaves). Input operations (nullifying) use the integrated input queue on the tree account.
+- **Address trees** have only an integrated input queue on the tree account - no separate output queue.
+
+## ZKP Verification
+
+Batch update operations require zero-knowledge proofs generated by the Light Protocol prover:
+
+- **Prover Server:** `prover/server/` - Generates ZK proofs for batch operations
+- **Prover Client:** `prover/client/` - Client libraries for requesting proofs
+- **Batch Update Circuits:** `prover/server/prover/v2/` - Circuit definitions for batch append, batch update (nullify), and batch address append operations
+
+## Dependencies
+
+This crate relies on several Light Protocol libraries:
+
+- **`light-bloom-filter`** - Bloom filter implementation for non-inclusion proofs
+- **`light-hasher`** - Poseidon hash implementation for hash chains and tree operations
+- **`light-verifier`** - ZKP verification for batch updates
+- **`light-zero-copy`** - Zero-copy serialization for efficient account data access
+- **`light-merkle-tree-metadata`** - Shared metadata structures for merkle trees
+- **`light-compressed-account`** - Compressed account types and utilities
+- **`light-account-checks`** - Account validation and discriminator checks
+
+## Testing and Reference Implementations
+
+**IndexedMerkleTree Reference Implementation:**
+- **`light-merkle-tree-reference`** - Reference implementation of indexed Merkle trees (dev dependency)
+- Source: `program-tests/merkle-tree/src/indexed.rs` - Canonical IndexedMerkleTree implementation used for generating constants and testing
+- Used to generate constants like `ADDRESS_TREE_INIT_ROOT_40` in [`src/constants.rs`](../src/constants.rs)
+- Initializes address trees with a single leaf: `H(0, HIGHEST_ADDRESS_PLUS_ONE)`
+
+## Source Code Structure
+
+**Core Account Types:**
+- [`src/merkle_tree.rs`](../src/merkle_tree.rs) - `BatchedMerkleTreeAccount` (prove inclusion, nullify existing state, create new addresses)
+- [`src/queue.rs`](../src/queue.rs) - `BatchedQueueAccount` (add new state (transaction outputs))
+- [`src/batch.rs`](../src/batch.rs) - `Batch` state machine (Fill → Full → Inserted)
+- [`src/queue_batch_metadata.rs`](../src/queue_batch_metadata.rs) - `QueueBatches` metadata
+
+**Metadata and Configuration:**
+- [`src/merkle_tree_metadata.rs`](../src/merkle_tree_metadata.rs) - `BatchedMerkleTreeMetadata` and account size calculations
+- [`src/constants.rs`](../src/constants.rs) - Default configuration values
+
+**ZKP Infrastructure:**
+- `prover/server/` - Prover server that generates ZK proofs for batch operations
+- `prover/client/` - Client libraries for requesting proofs
+- `prover/server/prover/v2/` - Batch update circuit definitions (append, nullify, address append)
+
+**Initialization:**
+- [`src/initialize_state_tree.rs`](../src/initialize_state_tree.rs) - State tree initialization
+- [`src/initialize_address_tree.rs`](../src/initialize_address_tree.rs) - Address tree initialization
+- [`src/rollover_state_tree.rs`](../src/rollover_state_tree.rs) - State tree rollover
+- [`src/rollover_address_tree.rs`](../src/rollover_address_tree.rs) - Address tree rollover
+
+**Errors:**
+- [`src/errors.rs`](../src/errors.rs) - `BatchedMerkleTreeError` enum with all error types
+
+## Error Codes
+
+All errors are defined in [`src/errors.rs`](../src/errors.rs) and map to u32 error codes (14301-14312 range):
+- `BatchNotReady` (14301) - Batch is not ready to be inserted
+- `BatchAlreadyInserted` (14302) - Batch is already inserted
+- `TreeIsFull` (14310) - Batched Merkle tree reached capacity
+- `NonInclusionCheckFailed` (14311) - Value exists in bloom filter
+- `BloomFilterNotZeroed` (14312) - Bloom filter must be zeroed before reuse
+- Additional errors from underlying libraries (hasher, zero-copy, verifier, etc.)

program-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.md

@@ -0,0 +1,101 @@
+# Initialize Address Tree
+
+**path:** src/initialize_address_tree.rs
+
+**description:**
+Initializes an address tree with integrated address queue. This operation creates **one Solana account**:
+
+**Address Merkle tree account** (`BatchedMerkleTreeAccount`) - Stores tree roots, root history, and integrated address queue (bloom filters + hash chains for addresses)
+- Account layout `BatchedMerkleTreeAccount` defined in: src/merkle_tree.rs
+- Metadata `BatchedMerkleTreeMetadata` defined in: src/merkle_tree_metadata.rs
+- Tree type: `TreeType::AddressV2` (5)
+- Initial root: `ADDRESS_TREE_INIT_ROOT_40` (pre-initialized with one indexed array element)
+- Starts at next_index: 1 (index 0 contains sentinel element)
+- Discriminator: b`BatchMta` `[66, 97, 116, 99, 104, 77, 116, 97]` (8 bytes)
+
+Address trees are used for address registration in the Light Protocol. New addresses are inserted into the address queue, then batch-updated into the tree with ZKPs. Unlike state trees, address trees have no separate output queue - the address queue is integrated into the tree account.
+
+**Instruction data:**
+Instruction data is defined in: src/initialize_address_tree.rs
+
+`InitAddressTreeAccountsInstructionData` struct:
+
+**Tree configuration:**
+- `height`: u32 - Tree height (default: 40, capacity = 2^40 leaves)
+- `index`: u64 - Unchecked identifier of the address tree
+- `root_history_capacity`: u32 - Size of root history cyclic buffer (default: 200)
+
+**Batch sizes:**
+- `input_queue_batch_size`: u64 - Elements per address queue batch (default: 15,000)
+- `input_queue_zkp_batch_size`: u64 - Elements per ZKP batch for address insertions (default: 250)
+
+**Validation:** Batch size must be divisible by ZKP batch size. Error: `BatchSizeNotDivisibleByZkpBatchSize` if validation fails.
+
+**Bloom filter configuration:**
+- `bloom_filter_capacity`: u64 - Capacity in bits (default: batch_size * 8)
+- `bloom_filter_num_iters`: u64 - Number of hash functions (default: 3 for test, 10 for production)
+
+**Validation:**
+- Capacity must be divisible by 8
+- Capacity must be >= batch_size * 8
+
+**Access control:**
+- `program_owner`: Option<Pubkey> - Optional program owning the tree
+- `forester`: Option<Pubkey> - Optional forester pubkey for non-Light foresters
+- `owner`: Pubkey - Account owner (passed separately as function parameter, not in struct)
+
+**Rollover and fees:**
+- `rollover_threshold`: Option<u64> - Percentage threshold for rollover (default: 95%)
+- `network_fee`: Option<u64> - Network fee amount (default: 10,000 lamports)
+- `close_threshold`: Option<u64> - Placeholder, unimplemented
+
+**Accounts:**
+1. merkle_tree_account
+   - mutable
+   - Address Merkle tree account being initialized
+   - Must be rent-exempt for calculated size
+
+Note: No signer accounts required - account is expected to be pre-created with correct size
+
+**Instruction Logic and Checks:**
+
+1. **Calculate account size:**
+   - Merkle tree account size: Based on input_queue_batch_size, bloom_filter_capacity, input_queue_zkp_batch_size, root_history_capacity, and height
+   - Account size formula defined in: src/merkle_tree.rs (`get_merkle_tree_account_size`)
+
+2. **Verify rent exemption:**
+   - Check: merkle_tree_account balance >= minimum rent exemption for mt_account_size
+   - Uses: `check_account_balance_is_rent_exempt` from `light-account-checks`
+   - Store rent amount for rollover fee calculation
+
+3. **Initialize address Merkle tree account:**
+   - Set discriminator: `BatchMta` (8 bytes)
+   - Create tree metadata:
+     - tree_type: `TreeType::AddressV2` (5)
+     - associated_queue: Pubkey::default() (address trees have no separate queue)
+     - Calculate rollover_fee: Based on rollover_threshold, height, and merkle_tree_rent
+     - access_metadata: Set owner, program_owner, forester
+     - rollover_metadata: Set index, rollover_fee, rollover_threshold, network_fee, close_threshold, additional_bytes=None
+   - Initialize root history: Cyclic buffer with capacity=root_history_capacity, first entry = `ADDRESS_TREE_INIT_ROOT_40`
+   - Initialize integrated address queue:
+     - 2 bloom filter stores (one per batch), size = bloom_filter_capacity / 8 bytes each
+     - 2 hash chain stores (one per batch), capacity = (input_queue_batch_size / input_queue_zkp_batch_size) each
+     - Batch metadata with input_queue_batch_size and input_queue_zkp_batch_size
+   - Compute hashed_pubkey: Hash and truncate to 31 bytes for bn254 field compatibility
+   - next_index: 1 (starts at 1 because index 0 contains pre-initialized sentinel element)
+   - sequence_number: 0 (increments with each tree update)
+   - Rollover fee: Charged on address tree operations
+
+4. **Validate configurations:**
+   - root_history_capacity >= (input_queue_batch_size / input_queue_zkp_batch_size)
+   - Rationale: Ensures sufficient space for roots generated by address queue operations
+   - ZKP batch sizes must be 10 or 250 (only supported circuit sizes for address trees)
+   - height must be 40 (fixed for address trees)
+
+**Errors:**
+- `AccountError::AccountNotRentExempt` (error code: 12011) - Account balance insufficient for rent exemption at calculated size
+- `AccountError::InvalidAccountSize` (error code: 12006) - Account data length doesn't match calculated size requirements
+- `BatchedMerkleTreeError::BatchSizeNotDivisibleByZkpBatchSize` (error code: 14305) - Batch size is not evenly divisible by ZKP batch size
+- `MerkleTreeMetadataError::InvalidRolloverThreshold` - Rollover threshold value is invalid (must be percentage)
+- `ZeroCopyError::Size` - Account size mismatch during zero-copy deserialization
+- `BorshError` - Failed to serialize or deserialize metadata structures