chore: add bmt formal verification #2030
Draft
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
WalkthroughAdds Kani (formal verification) support and extensive docs/tests to the batched Merkle tree and zero-copy crates. Introduces cfg(kani) code paths, Kani-only helpers/ghost state, new error variant, many end-to-end tests and Kani proofs, and Cargo feature/lint updates. No production API semantics intentionally changed. Changes
Sequence Diagram(s)sequenceDiagram
participant Builder as Build (normal)
participant Kani as Build (kani)
participant Code as Library
Note over Builder,Kani: Batched account (de)serialization/init
alt Normal build (no kani)
Builder->>Code: from_bytes / init
Code->>Code: use zerocopy::Ref to map metadata & slices
Code->>Code: construct Ref-based BatchedMerkleTreeAccount
else Kani build
Kani->>Code: from_bytes / init
Code->>Code: manually check sizes, unsafe read/write metadata
Code->>Code: construct direct &mut metadata, Vec-backed stores
Code->>Code: initialize GhostRoots for verification tracking
end
Note over Builder,Kani: Update flow (tree update)
alt Normal: runtime verification
Builder->>Code: verify_update(proof, public_inputs)
Code->>Code: compute/verify hash chains and update root_history
else Kani: verification stubbed
Kani->>Code: stub verify_update -> Ok
Code->>Code: track root in GhostRoots, skip heavy hashing
end
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60–90 minutes Areas to focus review on:
Possibly related PRs
Suggested reviewers
Poem
Pre-merge checks and finishing touches✅ Passed checks (3 passed)
✨ Finishing touches
🧪 Generate unit tests (beta)
Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Actionable comments posted: 5
🧹 Nitpick comments (3)
program-tests/batched-merkle-tree-test/Cargo.toml (1)
25-25: Minor formatting inconsistency: add space before closing brace.Line 25 is missing a space before the closing brace to match the style of other lines in the file (e.g., line 11).
-light-array-map = { workspace = true} +light-array-map = { workspace = true }Also applies to: 25-25
program-libs/batched-merkle-tree/tests/constants.rs (1)
24-25: Consider importing HIGHEST_ADDRESS_PLUS_ONE from a shared constant.The value matches the JS constant in
js/stateless.js/src/constants.ts. If this constant exists in a shared Rust module (or should be added to one), importing it would reduce duplication and ensure consistency.program-libs/batched-merkle-tree/src/batch.rs (1)
262-270: LGTM!The getter methods are well-implemented and provide a consistent API surface.
Note: Since
batch_size(line 75) andzkp_batch_size(line 78) are already public fields, these getters are currently redundant. However, they're useful if you plan to make those fields private in the future for better encapsulation.
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
⛔ Files ignored due to path filters (1)
Cargo.lockis excluded by!**/*.lock
📒 Files selected for processing (28)
program-libs/batched-merkle-tree/Cargo.toml(2 hunks)program-libs/batched-merkle-tree/docs/CLAUDE.md(1 hunks)program-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.md(1 hunks)program-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md(1 hunks)program-libs/batched-merkle-tree/docs/INSERT_ADDRESS_QUEUE.md(1 hunks)program-libs/batched-merkle-tree/docs/INSERT_INPUT_QUEUE.md(1 hunks)program-libs/batched-merkle-tree/docs/INSERT_OUTPUT_QUEUE.md(1 hunks)program-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.md(1 hunks)program-libs/batched-merkle-tree/docs/TREE_ACCOUNT.md(1 hunks)program-libs/batched-merkle-tree/docs/UPDATE_FROM_INPUT_QUEUE.md(1 hunks)program-libs/batched-merkle-tree/docs/UPDATE_FROM_OUTPUT_QUEUE.md(1 hunks)program-libs/batched-merkle-tree/src/batch.rs(1 hunks)program-libs/batched-merkle-tree/src/errors.rs(2 hunks)program-libs/batched-merkle-tree/src/merkle_tree.rs(23 hunks)program-libs/batched-merkle-tree/tests/constants.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/batch.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rs(1 hunks)program-libs/batched-merkle-tree/tests/merkle_tree.rs(1 hunks)program-tests/batched-merkle-tree-test/Cargo.toml(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e_tests/address.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e_tests/e2e.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e_tests/mod.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e_tests/simulate_txs.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e_tests/state.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/merkle_tree.rs(0 hunks)
💤 Files with no reviewable changes (1)
- program-tests/batched-merkle-tree-test/tests/merkle_tree.rs
🧰 Additional context used
🧠 Learnings (43)
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/account_compression_cpi/mod.rs : Export each new operation module by adding pub mod <operation>; and re-export with pub use <operation>::*.
Applied to files:
program-tests/batched-merkle-tree-test/tests/e2e.rsprogram-libs/batched-merkle-tree/tests/kani.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/mod.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs
📚 Learning: 2025-10-15T03:46:43.242Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: sdk-tests/sdk-token-test/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:43.242Z
Learning: Applies to sdk-tests/sdk-token-test/**/tests/**/*.rs : Every test should only contain functional integration tests
Applied to files:
program-tests/batched-merkle-tree-test/tests/e2e.rs
📚 Learning: 2025-10-15T03:46:43.242Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: sdk-tests/sdk-token-test/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:43.242Z
Learning: Run tests with: cargo test-sbf -p sdk-token-test --test <test-file-name>
Applied to files:
program-tests/batched-merkle-tree-test/tests/e2e.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/docs/{CLAUDE.md,ACCOUNT_INFO_TRAIT.md,ACCOUNT_CHECKS.md,ACCOUNT_ITERATOR.md,ERRORS.md,DISCRIMINATOR.md,PACKED_ACCOUNTS.md} : Keep component documentation up to date in the corresponding docs/*.md files listed
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.mdprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/UPDATE_FROM_OUTPUT_QUEUE.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.md
📚 Learning: 2025-10-15T03:46:03.556Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/docs/instructions/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:03.556Z
Learning: Applies to programs/compressed-token/program/docs/instructions/**/CLAUDE.md : Maintain CLAUDE.md (this file) as the documentation structure guide for the compressed token program docs
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.md
📚 Learning: 2025-10-16T06:33:55.362Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:55.362Z
Learning: Applies to programs/compressed-token/program/docs/ACCOUNTS.md : Account documentation must include: description, discriminator, state layout, serialization example, hashing (only for compressed accounts), derivation (only for PDAs), and associated instructions
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.mdprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/UPDATE_FROM_OUTPUT_QUEUE.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/{ACCOUNT_INFO_TRAIT.md,ACCOUNT_CHECKS.md,ACCOUNT_ITERATOR.md,DISCRIMINATOR.md,ERRORS.md,PACKED_ACCOUNTS.md} : Each document should focus on a single module or concept
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.mdprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.md
📚 Learning: 2025-10-16T06:33:19.426Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/compressible/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:19.426Z
Learning: Applies to program-libs/compressible/docs/CONFIG_ACCOUNT.md : Document the CompressibleConfig account structure and methods in docs/CONFIG_ACCOUNT.md
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.mdprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-15T03:46:03.556Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/docs/instructions/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:03.556Z
Learning: Applies to programs/compressed-token/program/docs/instructions/**/ACCOUNTS.md : Provide complete account layouts and data structures in ACCOUNTS.md
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.mdprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-15T03:45:40.038Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/docs/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:45:40.038Z
Learning: Applies to programs/compressed-token/program/docs/**/ACCOUNTS.md : Maintain ACCOUNTS.md with complete account layouts and data structures
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.mdprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-15T03:45:40.038Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/docs/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:45:40.038Z
Learning: Applies to programs/compressed-token/program/docs/**/CLAUDE.md : Include a CLAUDE.md in each relevant documentation directory that serves as the documentation structure guide for that directory
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.md
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/PACKED_ACCOUNTS.md : PACKED_ACCOUNTS.md must document index-based dynamic account access, including accessing mint, owner, and delegate accounts by index with bounds checking
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.mdprogram-libs/batched-merkle-tree/docs/INSERT_ADDRESS_QUEUE.mdprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/ACCOUNT_ITERATOR.md : ACCOUNT_ITERATOR.md must document the enhanced account iterator, including sequential processing, automatic validation, and location-based error reporting for debugging
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.mdprogram-libs/batched-merkle-tree/docs/INSERT_ADDRESS_QUEUE.mdprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/UPDATE_FROM_OUTPUT_QUEUE.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Load accounts according to type before check_forester: batched via BatchedMerkleTreeAccount::type_from_account_info(); regular via ctx.accounts.account.load()?.metadata; use custom deserialization when required.
Applied to files:
program-libs/batched-merkle-tree/docs/CLAUDE.mdprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.mdprogram-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/address.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/{solana.rs,pinocchio.rs,test_account_info.rs} : Gate SDK-specific implementations with #[cfg(feature = "solana"|"pinocchio"|"test-only")]
Applied to files:
program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rsprogram-libs/batched-merkle-tree/Cargo.tomlprogram-libs/batched-merkle-tree/tests/constants.rsprogram-tests/batched-merkle-tree-test/Cargo.tomlprogram-tests/batched-merkle-tree-test/tests/e2e_tests/mod.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/**/Cargo.toml : Define features solana, pinocchio, and test-only in Cargo.toml; default build should enable none
Applied to files:
program-libs/batched-merkle-tree/Cargo.tomlprogram-tests/batched-merkle-tree-test/Cargo.toml
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/account_info_trait.rs : Ensure the crate compiles with no features enabled by keeping trait definitions free of SDK-specific dependencies
Applied to files:
program-libs/batched-merkle-tree/Cargo.toml
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/!(account_info)/**/*.rs : Use AccountInfoTrait for runtime-agnostic account handling; avoid direct solana-program or pinocchio AccountInfo in general logic
Applied to files:
program-libs/batched-merkle-tree/Cargo.toml
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/packed_accounts.rs : For dynamic account sets, use PackedAccounts for index-based access with bounds checks instead of manual indexing
Applied to files:
program-libs/batched-merkle-tree/Cargo.toml
📚 Learning: 2025-10-16T06:33:19.426Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/compressible/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:19.426Z
Learning: Applies to program-libs/compressible/src/config.rs : Ensure serialization compatibility across Anchor, Pinocchio, and Borsh for core account types used by dependent programs
Applied to files:
program-libs/batched-merkle-tree/Cargo.tomlprogram-libs/batched-merkle-tree/tests/constants.rsprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.mdprogram-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/test_account_info.rs : Use the mock AccountInfo implementation under the test-only feature for unit tests
Applied to files:
program-libs/batched-merkle-tree/Cargo.tomlprogram-tests/batched-merkle-tree-test/tests/e2e_tests/simulate_txs.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/{solana.rs,pinocchio.rs,test_account_info.rs} : Provide SDK-specific AccountInfoTrait implementations in account_info/{solana.rs,pinocchio.rs,test_account_info.rs}
Applied to files:
program-libs/batched-merkle-tree/Cargo.toml
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/checks.rs : Expose and maintain account validation helpers (check_owner, check_program, check_mut/non_mut, check_signer, check_discriminator, set_discriminator, check_pda_seeds, check_account_balance_is_rent_exempt, account_info_init) in checks.rs
Applied to files:
program-libs/batched-merkle-tree/Cargo.tomlprogram-libs/batched-merkle-tree/tests/constants.rsprogram-libs/batched-merkle-tree/src/errors.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/account_compression_cpi/*.rs : Context structs for wrapper instructions must include standard accounts: optional registered_forester_pda (mut), authority Signer, cpi_authority with seeds/bump for CPI_AUTHORITY_PDA_SEED, registered_program_pda, target program handle, log_wrapper, and mutable target_account.
Applied to files:
program-libs/batched-merkle-tree/Cargo.tomlprogram-libs/batched-merkle-tree/docs/TREE_ACCOUNT.md
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/discriminator.rs : Define and keep discriminator constants and the Discriminator trait in discriminator.rs for compile-time verification
Applied to files:
program-libs/batched-merkle-tree/tests/constants.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/ACCOUNT_INFO_TRAIT.md : ACCOUNT_INFO_TRAIT.md must document the AccountInfoTrait abstraction, including trait definition, implementations, and runtime-agnostic usage across Solana and Pinocchio
Applied to files:
program-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.md
📚 Learning: 2025-10-15T03:46:03.556Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/docs/instructions/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:03.556Z
Learning: Refer to ../ACCOUNTS.md for account structure reference from instruction docs
Applied to files:
program-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/DISCRIMINATOR.md : DISCRIMINATOR.md must document 8-byte discriminators, the Discriminator trait, constant arrays for compile-time checks, and integration with account initialization
Applied to files:
program-libs/batched-merkle-tree/docs/TREE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : Validate account type with 8-byte discriminators using check_discriminator before deserialization
Applied to files:
program-libs/batched-merkle-tree/docs/QUEUE_ACCOUNT.mdprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-08-14T00:36:53.191Z
Learnt from: ananas-block
Repo: Lightprotocol/light-protocol PR: 1909
File: program-libs/zero-copy/src/init_mut.rs:241-249
Timestamp: 2025-08-14T00:36:53.191Z
Learning: In the light-protocol zero-copy crate, performance is prioritized over safety checks for edge cases like Vec lengths exceeding u32::MAX, even when there might be wire format inconsistencies.
Applied to files:
program-tests/batched-merkle-tree-test/Cargo.toml
📚 Learning: 2025-10-15T03:46:03.556Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/docs/instructions/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:03.556Z
Learning: Applies to programs/compressed-token/program/docs/instructions/instructions/CREATE_TOKEN_ACCOUNT.md : Document Create Token Account & Associated Token Account instructions in instructions/CREATE_TOKEN_ACCOUNT.md
Applied to files:
program-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-15T03:45:40.038Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/docs/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:45:40.038Z
Learning: Applies to programs/compressed-token/program/docs/**/instructions/CREATE_TOKEN_ACCOUNT.md : Provide CREATE_TOKEN_ACCOUNT.md in the instructions/ directory documenting create token account and associated token account instructions
Applied to files:
program-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : On account initialization, call account_info_init to set the 8-byte discriminator
Applied to files:
program-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.mdprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Wrapper instruction handlers must: (1) load the target account metadata; (2) call check_forester with correct authority, target, forester PDA (optional), and computed work_units; (3) delegate via a CPI using a PDA signer.
Applied to files:
program-libs/batched-merkle-tree/docs/INITIALIZE_ADDRESS_TREE.mdprogram-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-16T06:33:19.426Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/compressible/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:19.426Z
Learning: Applies to program-libs/compressible/src/error.rs : Define error types with numeric codes in the 19xxx range and propagate hasher errors in the 7xxx range; include ProgramError conversions (Anchor, Pinocchio, Solana) in src/error.rs
Applied to files:
program-libs/batched-merkle-tree/src/errors.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/error.rs : Maintain stable mapping of AccountError to ProgramError, including Pinocchio code mapping (1–11), in error.rs
Applied to files:
program-libs/batched-merkle-tree/src/errors.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : Return AccountError variants (codes 12006–12021) and rely on automatic ProgramError conversions; avoid returning raw ProgramError directly
Applied to files:
program-libs/batched-merkle-tree/src/errors.rs
📚 Learning: 2025-10-16T06:33:55.362Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:55.362Z
Learning: Applies to programs/compressed-token/program/programs/compressed-token/anchor/src/lib.rs : Define all program-specific error codes in anchor_compressed_token::ErrorCode in programs/compressed-token/anchor/src/lib.rs; return errors as ProgramError::Custom(error_code as u32)
Applied to files:
program-libs/batched-merkle-tree/src/errors.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_iterator.rs : Use AccountIterator for sequential account retrieval to get precise file:line:column error locations; avoid manual index handling
Applied to files:
program-libs/batched-merkle-tree/src/errors.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-15T03:46:03.556Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/docs/instructions/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:03.556Z
Learning: Applies to programs/compressed-token/program/docs/instructions/instructions/{CREATE_TOKEN_ACCOUNT,MINT_ACTION,TRANSFER2,CLAIM,CLOSE_TOKEN_ACCOUNT,DECOMPRESSED_TRANSFER,WITHDRAW_FUNDING_POOL}.md : Every instruction description must include sections: path, description, instruction_data, Accounts, instruction logic and checks, Errors
Applied to files:
program-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-16T06:33:55.362Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:55.362Z
Learning: Applies to programs/compressed-token/program/src/create_token_account.rs : Create Token Account instruction must validate that the config state is ACTIVE only
Applied to files:
program-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-16T06:33:55.362Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:55.362Z
Learning: Applies to programs/compressed-token/program/src/create_associated_token_account.rs : Create Associated Token Account instruction must validate that the config state is ACTIVE only
Applied to files:
program-libs/batched-merkle-tree/docs/INITIALIZE_STATE_TREE.md
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Instruction handlers must compute work_units by operation type: batch operations use account.queue_batches.batch_size; single operations use DEFAULT_WORK_V1; custom operations compute based on complexity.
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
🧬 Code graph analysis (9)
program-tests/batched-merkle-tree-test/tests/e2e_tests/e2e.rs (5)
program-libs/batched-merkle-tree/src/initialize_state_tree.rs (1)
init_batched_state_merkle_tree_accounts(117-200)program-libs/batched-merkle-tree/src/merkle_tree.rs (2)
get_merkle_tree_account_size_default(982-985)state_from_bytes(133-139)program-libs/batched-merkle-tree/src/queue.rs (2)
get_output_queue_account_size_default(574-589)BatchedQueueAccount(662-662)prover/client/src/prover.rs (1)
spawn_prover(17-51)program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs (4)
rng(852-852)get_rnd_bytes(851-855)perform_input_update(857-921)assert_merkle_tree_update(117-530)
program-tests/batched-merkle-tree-test/tests/e2e_tests/state.rs (5)
program-libs/batched-merkle-tree/src/initialize_state_tree.rs (2)
init_batched_state_merkle_tree_accounts(117-200)get_state_merkle_tree_account_size_from_params(353-363)program-libs/batched-merkle-tree/src/queue.rs (3)
get_output_queue_account_size_from_params(591-608)BatchedQueueAccount(662-662)output_from_bytes(181-186)program-libs/hasher/src/hash_chain.rs (1)
create_hash_chain_from_slice(23-32)prover/client/src/prover.rs (1)
spawn_prover(17-51)program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs (6)
rng(852-852)get_rnd_bytes(851-855)assert_output_queue_insert(1154-1241)get_random_leaf(923-930)assert_nullifier_queue_insert(932-964)perform_input_update(857-921)
program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rs (4)
program-libs/batched-merkle-tree/src/merkle_tree.rs (6)
BatchedMerkleTreeAccount(1128-1128)BatchedMerkleTreeAccount(1138-1138)BatchedMerkleTreeAccount(1148-1148)pubkey(965-967)init(218-338)address_from_bytes(175-180)program-libs/compressed-account/src/pubkey.rs (1)
new_from_array(79-81)program-libs/hasher/src/hash_to_field_size.rs (1)
hash_to_bn254_field_size_be(99-101)program-libs/zero-copy/src/cyclic_vec.rs (1)
first_index(200-206)
program-libs/batched-merkle-tree/tests/kani.rs (1)
program-libs/batched-merkle-tree/src/merkle_tree.rs (1)
zero_out_roots(752-784)
program-libs/batched-merkle-tree/tests/constants.rs (1)
js/stateless.js/src/constants.ts (1)
HIGHEST_ADDRESS_PLUS_ONE(48-50)
program-tests/batched-merkle-tree-test/tests/e2e_tests/simulate_txs.rs (6)
program-libs/batched-merkle-tree/src/initialize_state_tree.rs (1)
init_batched_state_merkle_tree_accounts(117-200)program-libs/batched-merkle-tree/src/merkle_tree.rs (4)
assert_batch_append_event_event(1059-1086)assert_nullify_event(1030-1056)get_merkle_tree_account_size_default(982-985)state_from_bytes(133-139)program-libs/batched-merkle-tree/src/queue.rs (3)
get_output_queue_account_size_default(574-589)BatchedQueueAccount(662-662)output_from_bytes(181-186)program-libs/hasher/src/hash_chain.rs (1)
create_hash_chain_from_slice(23-32)prover/client/src/prover.rs (1)
spawn_prover(17-51)program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs (6)
rng(852-852)get_rnd_bytes(851-855)get_random_leaf(923-930)assert_nullifier_queue_insert(932-964)assert_output_queue_insert(1154-1241)assert_merkle_tree_update(117-530)
program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs (4)
program-libs/batched-merkle-tree/src/merkle_tree.rs (3)
assert_batch_adress_event(1089-1114)address_from_bytes(175-180)state_from_bytes(133-139)program-libs/batched-merkle-tree/src/queue_batch_metadata.rs (1)
get_previous_batch(72-74)program-libs/array-map/src/lib.rs (1)
find(69-71)program-libs/batched-merkle-tree/src/batch.rs (3)
get_num_inserted_elements(258-260)get_state(122-124)bloom_filter_is_zeroed(126-128)
program-tests/batched-merkle-tree-test/tests/e2e_tests/address.rs (5)
program-libs/batched-merkle-tree/src/initialize_address_tree.rs (2)
get_address_merkle_tree_account_size_from_params(172-182)init_batched_address_merkle_tree_account(83-129)prover/client/src/prover.rs (1)
spawn_prover(17-51)program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs (4)
rng(852-852)get_rnd_bytes(851-855)assert_input_queue_insert(969-1148)perform_address_update(25-115)program-libs/batched-merkle-tree/src/merkle_tree.rs (1)
address_from_bytes(175-180)program-libs/batched-merkle-tree/src/batch.rs (2)
bloom_filter_is_zeroed(126-128)get_state(122-124)
program-libs/batched-merkle-tree/tests/kani/batch.rs (1)
program-libs/batched-merkle-tree/src/batch.rs (15)
new(95-119)get_state(122-124)bloom_filter_is_zeroed(126-128)advance_state_to_full(200-212)advance_state_to_inserted(184-196)advance_state_to_fill(155-180)from(20-27)from(31-33)start_slot_is_set(142-144)get_num_zkp_batches(273-275)get_num_hash_chain_store(278-280)get_num_inserted_elements(258-260)get_num_elements_inserted_into_tree(253-255)batch_is_ready_to_insert(224-226)get_num_ready_zkp_updates(230-233)
🪛 LanguageTool
program-libs/batched-merkle-tree/docs/UPDATE_FROM_INPUT_QUEUE.md
[grammar] ~22-~22: Ensure spelling is correct
Context: ...trees: increments nullifier_next_index (offchain indexer tracking only) 6. Marks ZKP bat...
(QB_NEW_EN_ORTHOGRAPHY_ERROR_IDS_1)
[grammar] ~85-~85: Ensure spelling is correct
Context: ...e proof verifies old_leaf value against onchain root, ensuring correct position - If ol...
(QB_NEW_EN_ORTHOGRAPHY_ERROR_IDS_1)
[grammar] ~199-~199: Ensure spelling is correct
Context: ...nullifier_next_index by zkp_batch_size (offchain indexer tracking) - Address: Increme...
(QB_NEW_EN_ORTHOGRAPHY_ERROR_IDS_1)
[grammar] ~235-~235: Ensure spelling is correct
Context: ..._index: Incremented by zkp_batch_size (offchain indexer tracking) - sequence_number`: ...
(QB_NEW_EN_ORTHOGRAPHY_ERROR_IDS_1)
program-libs/batched-merkle-tree/docs/INSERT_INPUT_QUEUE.md
[grammar] ~43-~43: Use a hyphen to join words.
Context: ..._hash. The only requirement is that post nullifier insertion we cannot prove incl...
(QB_NEW_EN_HYPHEN)
program-libs/batched-merkle-tree/docs/UPDATE_FROM_OUTPUT_QUEUE.md
[style] ~53-~53: This phrase is redundant. Consider writing “filled”.
Context: ... Fill (still being filled) or Full (completely filled) state 3. **Create public inputs hash:...
(COMPLETELY_ANNIHILATE)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (21)
- GitHub Check: system-programs (sdk-libs, light-sdk-macros light-sdk light-program-test light-client light-compr...
- GitHub Check: system-programs (anchor & pinocchio, ["cargo-test-sbf -p sdk-anchor-test", "cargo-test-sbf -p sdk...
- GitHub Check: system-programs (native, ["cargo-test-sbf -p sdk-native-test", "cargo-test-sbf -p sdk-v1-native-t...
- GitHub Check: stateless-js-v1
- GitHub Check: system-programs (token test, ["cargo-test-sbf -p sdk-token-test"])
- GitHub Check: lint
- GitHub Check: cli-v2
- GitHub Check: stateless-js-v2
- GitHub Check: Forester e2e test
- GitHub Check: cli-v1
- GitHub Check: programs (system-cpi-test-v2-functional-account-infos, ["cargo-test-sbf -p system-cpi-v2-test -- ...
- GitHub Check: programs (system-cpi-test, ["cargo-test-sbf -p system-cpi-test", "cargo test -p light-system-prog...
- GitHub Check: programs (system-cpi-test-v2-functional-read-only, ["cargo-test-sbf -p system-cpi-v2-test -- func...
- GitHub Check: programs (light-system-program-address, ["cargo-test-sbf -p system-test -- test_with_address", "c...
- GitHub Check: programs (compressed-token-batched-tree, ["cargo-test-sbf -p compressed-token-test -- test_transf...
- GitHub Check: programs (light-system-program-compression, ["cargo-test-sbf -p system-test -- test_with_compress...
- GitHub Check: programs (compressed-token-and-e2e, ["cargo-test-sbf -p compressed-token-test --test v1", "cargo-...
- GitHub Check: programs (account-compression-and-registry, ["cargo-test-sbf -p account-compression-test", "cargo...
- GitHub Check: Test batched-merkle-tree-simulate
- GitHub Check: Test program-libs-slow
- GitHub Check: Test program-libs-fast
🔇 Additional comments (15)
program-tests/batched-merkle-tree-test/Cargo.toml (1)
25-25: Dev-dependency is properly used in integration tests—approved.The
light-array-mapdev-dependency is confirmed to be actively imported and used across three integration test files:state.rs,simulate_txs.rs, andshared.rs. The addition to the test harness is appropriate and justified.program-libs/batched-merkle-tree/Cargo.toml (2)
12-12: Kani feature flag is properly implemented and gates verification code as intended—no changes needed.Verification confirms the
kanifeature is correctly defined in Cargo.toml and actively gates Kani-specific code throughout the crate:
- Test modules (
tests/kani/zero_out_roots.rs,tests/kani/batch.rs) use module-level#![cfg(feature = "kani")]- The
zero_out_roots_kani()function insrc/merkle_tree.rs(line 786) is gated with#[cfg(feature = "kani")]- Contract annotations use
#[cfg_attr(feature = "kani", kani::requires(...))]patterns for preconditions/postconditionsThe empty feature definition is appropriate for formal verification workflows—it acts as a compile-time flag without requiring additional dependencies.
63-65: Remove unused dev-dependencies:light-indexed-arrayandnum-traits.Verification found that
light-indexed-arrayis not imported or used anywhere in the test suite. Additionally,num-traitsis imported inconstants.rsbut never referenced in the actual test logic. Onlynum-bigintis legitimately used (forBigUint::from_str_radix()operations). Remove the two unused dependencies fromCargo.toml(lines 63-65) to keep the manifest clean and reduce unnecessary build overhead.⛔ Skipped due to learnings
Learnt from: CR Repo: Lightprotocol/light-protocol PR: 0 File: program-libs/account-checks/CLAUDE.md:0-0 Timestamp: 2025-10-11T21:59:25.222Z Learning: Applies to program-libs/account-checks/src/account_info/account_info_trait.rs : Ensure the crate compiles with no features enabled by keeping trait definitions free of SDK-specific dependenciesLearnt from: CR Repo: Lightprotocol/light-protocol PR: 0 File: program-libs/account-checks/CLAUDE.md:0-0 Timestamp: 2025-10-11T21:59:25.222Z Learning: Applies to program-libs/account-checks/**/Cargo.toml : Define features solana, pinocchio, and test-only in Cargo.toml; default build should enable noneprogram-libs/batched-merkle-tree/tests/constants.rs (3)
1-8: LGTM! Well-structured test setup.The imports are clean and the test function name clearly describes its purpose.
9-16: LGTM! Clean verification using the library.Method 1 provides a straightforward verification by directly comparing the library's tree root with the constant.
27-45: LGTM! Thorough manual verification.Method 2 provides an independent verification by manually computing the expected root. The logic correctly:
- Creates the initial leaf hash from zero and HIGHEST_ADDRESS_PLUS_ONE
- Builds the root through 40 levels (1 initial + 39 loop iterations)
- Uses level-specific zero bytes as siblings
This dual-method approach gives strong confidence in the constant's correctness.
program-libs/batched-merkle-tree/tests/merkle_tree.rs (1)
1-1: Clarify the purpose and content of this empty test file.This file is new but contains no code, test scaffolding, or comments. Given that the PR focuses on refactoring and adding comprehensive test infrastructure (including Kani verification tests and end-to-end integration tests), it's unclear why this file was added empty.
Is this file intentionally a placeholder, or should it contain test implementations? If it's a placeholder, consider either:
- Adding a comment documenting what tests should go here
- Removing the file if not needed at this time
- Adding initial test scaffolding or imports to clarify its purpose
Please clarify whether this relates to the test restructuring mentioned in the PR context (such as the removal of the test module at
program-tests/batched-merkle-tree-test/tests/merkle_tree.rs).program-tests/batched-merkle-tree-test/tests/e2e.rs (1)
1-2: LGTM!Clean module organization for the refactored e2e test suite.
program-libs/batched-merkle-tree/tests/kani.rs (1)
1-7: LGTM!Well-documented Kani test entry point with clear instructions for running formal verification tests.
program-libs/batched-merkle-tree/src/errors.rs (2)
54-55: LGTM!Clear error variant for root history zeroing safety checks.
75-75: LGTM!Error code 14313 is correctly assigned and follows the existing 143xx range pattern for batched Merkle tree errors.
program-tests/batched-merkle-tree-test/tests/e2e_tests/mod.rs (1)
1-4: LGTM!Clean module organization exposing the e2e test components.
program-libs/batched-merkle-tree/docs/CLAUDE.md (1)
1-148: Excellent documentation!Comprehensive and well-structured overview of the batched Merkle tree library. The documentation clearly explains account types, operations, key concepts, and dependencies with appropriate cross-references.
program-libs/batched-merkle-tree/docs/INSERT_OUTPUT_QUEUE.md (1)
1-90: Excellent operational documentation!Thorough documentation of the output queue insertion workflow, including clear explanations of the two-batch system, hash chains, and proof-by-index functionality.
program-libs/batched-merkle-tree/docs/UPDATE_FROM_INPUT_QUEUE.md (1)
1-264: Outstanding technical documentation!Comprehensive documentation of the input queue update workflows with detailed explanations of the ZKP verification circuits for both Batch Nullify and Batch Address Append operations. The circuit logic, public inputs, and state transitions are clearly described.
Contributor
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
program-libs/batched-merkle-tree/src/merkle_tree.rs (1)
117-333: Removeprintln!to keep the library BPF-safe.
assert_merkle_tree_update(and the other new helpers just below) are in the main library module and contain a large number ofprintln!calls. When we build this crate for the Solana BPF target we compile withno_std; pulling inprintln!drags instdand the build fails. Please either gate these helpers (and their logging) behind#[cfg(any(test, feature = "test-only"))]or switch tosolana_program::msg!under thesolanafeature so the production path stays no_std compliant. As written the program build is broken.
♻️ Duplicate comments (2)
program-tests/batched-merkle-tree-test/tests/e2e_tests/address.rs (1)
262-270: Guard previous root lookup against underflow.
root_indexis a cyclic cursor; when it is0,root_index - 1underflows and the test panics instead of asserting the invariant. Compute the predecessor with wrapping arithmetic before indexing.- assert_eq!( - merkle_tree_account.root_history[root_index - 1], - [0u8; 32] - ); + let prev_index = (root_index + merkle_tree_account.root_history.len() - 1) + % merkle_tree_account.root_history.len(); + assert_eq!(merkle_tree_account.root_history[prev_index], [0u8; 32]);program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rs (1)
25-62: Make the Kani setup satisfiable.
create_test_treebuilds aTreeType::AddressV2account withheight = 26. Outsidecfg(test)the initializer rejects address trees whose height differs from 40, soBatchedMerkleTreeAccount::initdeterministically returnsErr(MerkleTreeMetadataError::InvalidHeight). The subsequentkani::assume(init_result.is_ok())is therefore unsatisfiable, and every proof here becomes vacuous. Use a tree configuration that actually initializes—either switch to the state-tree variant or use the canonical address height and account layout—so the assumptions describe a real state.- let height = 26; + let height = 26; ... - TreeType::AddressV2, + TreeType::StateV2, ... - let tree_result = BatchedMerkleTreeAccount::address_from_bytes(account_data, &pubkey); + let tree_result = BatchedMerkleTreeAccount::state_from_bytes(account_data, &pubkey);
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (10)
program-libs/batched-merkle-tree/Cargo.toml(2 hunks)program-libs/batched-merkle-tree/src/merkle_tree.rs(23 hunks)program-libs/batched-merkle-tree/tests/kani.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/batch.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e_tests/address.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e_tests/simulate_txs.rs(1 hunks)program-tests/batched-merkle-tree-test/tests/e2e_tests/state.rs(1 hunks)program-tests/registry-test/tests/tests.rs(2 hunks)
🚧 Files skipped from review as they are similar to previous changes (1)
- program-libs/batched-merkle-tree/tests/kani/batch.rs
🧰 Additional context used
🧠 Learnings (16)
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/{solana.rs,pinocchio.rs,test_account_info.rs} : Gate SDK-specific implementations with #[cfg(feature = "solana"|"pinocchio"|"test-only")]
Applied to files:
program-libs/batched-merkle-tree/tests/kani.rsprogram-libs/batched-merkle-tree/tests/kani/zero_out_roots.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rsprogram-libs/batched-merkle-tree/Cargo.toml
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/checks.rs : Expose and maintain account validation helpers (check_owner, check_program, check_mut/non_mut, check_signer, check_discriminator, set_discriminator, check_pda_seeds, check_account_balance_is_rent_exempt, account_info_init) in checks.rs
Applied to files:
program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rsprogram-libs/batched-merkle-tree/Cargo.toml
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Load accounts according to type before check_forester: batched via BatchedMerkleTreeAccount::type_from_account_info(); regular via ctx.accounts.account.load()?.metadata; use custom deserialization when required.
Applied to files:
program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/address.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/test_account_info.rs : Use the mock AccountInfo implementation under the test-only feature for unit tests
Applied to files:
program-tests/batched-merkle-tree-test/tests/e2e_tests/simulate_txs.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs
📚 Learning: 2025-10-16T06:33:19.426Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/compressible/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:19.426Z
Learning: Applies to program-libs/compressible/src/config.rs : Ensure serialization compatibility across Anchor, Pinocchio, and Borsh for core account types used by dependent programs
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/**/Cargo.toml : Define features solana, pinocchio, and test-only in Cargo.toml; default build should enable none
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rsprogram-libs/batched-merkle-tree/Cargo.toml
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : Validate account type with 8-byte discriminators using check_discriminator before deserialization
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : On account initialization, call account_info_init to set the 8-byte discriminator
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/discriminator.rs : Define and keep discriminator constants and the Discriminator trait in discriminator.rs for compile-time verification
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/DISCRIMINATOR.md : DISCRIMINATOR.md must document 8-byte discriminators, the Discriminator trait, constant arrays for compile-time checks, and integration with account initialization
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_iterator.rs : Use AccountIterator for sequential account retrieval to get precise file:line:column error locations; avoid manual index handling
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rsprogram-tests/batched-merkle-tree-test/tests/e2e_tests/address.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Instruction handlers must compute work_units by operation type: batch operations use account.queue_batches.batch_size; single operations use DEFAULT_WORK_V1; custom operations compute based on complexity.
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/!(account_info)/**/*.rs : Use AccountInfoTrait for runtime-agnostic account handling; avoid direct solana-program or pinocchio AccountInfo in general logic
Applied to files:
program-libs/batched-merkle-tree/Cargo.toml
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/account_info_trait.rs : Ensure the crate compiles with no features enabled by keeping trait definitions free of SDK-specific dependencies
Applied to files:
program-libs/batched-merkle-tree/Cargo.toml
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/{solana.rs,pinocchio.rs,test_account_info.rs} : Provide SDK-specific AccountInfoTrait implementations in account_info/{solana.rs,pinocchio.rs,test_account_info.rs}
Applied to files:
program-libs/batched-merkle-tree/Cargo.toml
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/{ACCOUNT_INFO_TRAIT.md,ACCOUNT_CHECKS.md,ACCOUNT_ITERATOR.md,DISCRIMINATOR.md,ERRORS.md,PACKED_ACCOUNTS.md} : Code examples should demonstrate both Solana and Pinocchio usage where applicable
Applied to files:
program-libs/batched-merkle-tree/Cargo.toml
🧬 Code graph analysis (6)
program-libs/batched-merkle-tree/tests/kani.rs (1)
program-libs/batched-merkle-tree/src/merkle_tree.rs (1)
zero_out_roots(752-784)
program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rs (4)
program-libs/batched-merkle-tree/src/merkle_tree.rs (6)
BatchedMerkleTreeAccount(1128-1128)BatchedMerkleTreeAccount(1138-1138)BatchedMerkleTreeAccount(1148-1148)pubkey(965-967)init(218-338)address_from_bytes(175-180)program-libs/compressed-account/src/pubkey.rs (1)
new_from_array(79-81)program-libs/hasher/src/hash_to_field_size.rs (1)
hash_to_bn254_field_size_be(99-101)program-libs/zero-copy/src/cyclic_vec.rs (1)
first_index(200-206)
program-tests/batched-merkle-tree-test/tests/e2e_tests/simulate_txs.rs (6)
program-libs/batched-merkle-tree/src/initialize_state_tree.rs (1)
init_batched_state_merkle_tree_accounts(117-200)program-libs/batched-merkle-tree/src/merkle_tree.rs (7)
assert_batch_append_event_event(1059-1086)assert_nullify_event(1030-1056)BatchedMerkleTreeAccount(1128-1128)BatchedMerkleTreeAccount(1138-1138)BatchedMerkleTreeAccount(1148-1148)pubkey(965-967)state_from_bytes(133-139)program-libs/batched-merkle-tree/src/queue.rs (3)
get_output_queue_account_size_default(574-589)BatchedQueueAccount(662-662)output_from_bytes(181-186)program-libs/hasher/src/hash_chain.rs (1)
create_hash_chain_from_slice(23-32)prover/client/src/prover.rs (1)
spawn_prover(17-51)program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs (6)
rng(847-847)get_rnd_bytes(846-850)get_random_leaf(918-925)assert_nullifier_queue_insert(927-959)assert_output_queue_insert(1149-1236)assert_merkle_tree_update(117-525)
program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs (3)
program-libs/batched-merkle-tree/src/merkle_tree.rs (8)
assert_batch_adress_event(1089-1114)BatchedMerkleTreeAccount(1128-1128)BatchedMerkleTreeAccount(1138-1138)BatchedMerkleTreeAccount(1148-1148)pubkey(965-967)address_from_bytes(175-180)get_metadata(908-910)state_from_bytes(133-139)program-libs/batched-merkle-tree/src/queue_batch_metadata.rs (1)
get_previous_batch(72-74)program-libs/batched-merkle-tree/src/batch.rs (2)
get_state(122-124)bloom_filter_is_zeroed(126-128)
program-tests/batched-merkle-tree-test/tests/e2e_tests/address.rs (5)
program-libs/batched-merkle-tree/src/initialize_address_tree.rs (2)
get_address_merkle_tree_account_size_from_params(172-182)init_batched_address_merkle_tree_account(83-129)program-libs/batched-merkle-tree/src/merkle_tree.rs (5)
BatchedMerkleTreeAccount(1128-1128)BatchedMerkleTreeAccount(1138-1138)BatchedMerkleTreeAccount(1148-1148)pubkey(965-967)address_from_bytes(175-180)prover/client/src/prover.rs (1)
spawn_prover(17-51)program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs (4)
rng(847-847)get_rnd_bytes(846-850)assert_input_queue_insert(964-1143)perform_address_update(25-115)program-libs/batched-merkle-tree/src/batch.rs (2)
bloom_filter_is_zeroed(126-128)get_state(122-124)
program-tests/batched-merkle-tree-test/tests/e2e_tests/state.rs (6)
program-libs/batched-merkle-tree/src/initialize_state_tree.rs (2)
init_batched_state_merkle_tree_accounts(117-200)get_state_merkle_tree_account_size_from_params(353-363)program-libs/batched-merkle-tree/src/merkle_tree.rs (5)
BatchedMerkleTreeAccount(1128-1128)BatchedMerkleTreeAccount(1138-1138)BatchedMerkleTreeAccount(1148-1148)pubkey(965-967)state_from_bytes(133-139)program-libs/batched-merkle-tree/src/queue.rs (3)
get_output_queue_account_size_from_params(591-608)BatchedQueueAccount(662-662)output_from_bytes(181-186)program-libs/hasher/src/hash_chain.rs (1)
create_hash_chain_from_slice(23-32)prover/client/src/prover.rs (1)
spawn_prover(17-51)program-tests/batched-merkle-tree-test/tests/e2e_tests/shared.rs (5)
rng(847-847)get_rnd_bytes(846-850)assert_output_queue_insert(1149-1236)get_random_leaf(918-925)assert_nullifier_queue_insert(927-959)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (21)
- GitHub Check: cli-v2
- GitHub Check: system-programs (anchor & pinocchio, ["cargo-test-sbf -p sdk-anchor-test", "cargo-test-sbf -p sdk...
- GitHub Check: programs (system-cpi-test-v2-functional-account-infos, ["cargo-test-sbf -p system-cpi-v2-test -- ...
- GitHub Check: lint
- GitHub Check: system-programs (token test, ["cargo-test-sbf -p sdk-token-test"])
- GitHub Check: system-programs (sdk-libs, light-sdk-macros light-sdk light-program-test light-client light-compr...
- GitHub Check: Test program-libs-fast
- GitHub Check: programs (account-compression-and-registry, ["cargo-test-sbf -p account-compression-test", "cargo...
- GitHub Check: system-programs (native, ["cargo-test-sbf -p sdk-native-test", "cargo-test-sbf -p sdk-v1-native-t...
- GitHub Check: programs (system-cpi-test-v2-functional-read-only, ["cargo-test-sbf -p system-cpi-v2-test -- func...
- GitHub Check: programs (light-system-program-address, ["cargo-test-sbf -p system-test -- test_with_address", "c...
- GitHub Check: programs (compressed-token-and-e2e, ["cargo-test-sbf -p compressed-token-test --test v1", "cargo-...
- GitHub Check: programs (compressed-token-batched-tree, ["cargo-test-sbf -p compressed-token-test -- test_transf...
- GitHub Check: programs (system-cpi-test, ["cargo-test-sbf -p system-cpi-test", "cargo test -p light-system-prog...
- GitHub Check: stateless-js-v1
- GitHub Check: programs (light-system-program-compression, ["cargo-test-sbf -p system-test -- test_with_compress...
- GitHub Check: stateless-js-v2
- GitHub Check: Forester e2e test
- GitHub Check: Test batched-merkle-tree-simulate
- GitHub Check: Test program-libs-slow
- GitHub Check: cli-v1
🔇 Additional comments (1)
program-tests/registry-test/tests/tests.rs (1)
1883-1883: LGTM: Test iteration redistribution is neutral.The loop iteration counts have been adjusted (6 iterations instead of 4, then 3 instead of 5), but the total number of batch address merkle tree updates remains unchanged at 10. This redistribution may be intentional to test different state transitions or batch boundaries earlier in the test flow.
Also applies to: 1931-1931
Contributor
There was a problem hiding this comment.
Actionable comments posted: 1
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (3)
program-libs/batched-merkle-tree/src/merkle_tree.rs(22 hunks)program-libs/batched-merkle-tree/tests/kani/batch.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rs(1 hunks)
🚧 Files skipped from review as they are similar to previous changes (1)
- program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rs
🧰 Additional context used
🧠 Learnings (9)
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/{solana.rs,pinocchio.rs,test_account_info.rs} : Gate SDK-specific implementations with #[cfg(feature = "solana"|"pinocchio"|"test-only")]
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/**/Cargo.toml : Define features solana, pinocchio, and test-only in Cargo.toml; default build should enable none
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : Validate account type with 8-byte discriminators using check_discriminator before deserialization
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : On account initialization, call account_info_init to set the 8-byte discriminator
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/discriminator.rs : Define and keep discriminator constants and the Discriminator trait in discriminator.rs for compile-time verification
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/DISCRIMINATOR.md : DISCRIMINATOR.md must document 8-byte discriminators, the Discriminator trait, constant arrays for compile-time checks, and integration with account initialization
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Load accounts according to type before check_forester: batched via BatchedMerkleTreeAccount::type_from_account_info(); regular via ctx.accounts.account.load()?.metadata; use custom deserialization when required.
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_iterator.rs : Use AccountIterator for sequential account retrieval to get precise file:line:column error locations; avoid manual index handling
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Instruction handlers must compute work_units by operation type: batch operations use account.queue_batches.batch_size; single operations use DEFAULT_WORK_V1; custom operations compute based on complexity.
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
🧬 Code graph analysis (1)
program-libs/batched-merkle-tree/tests/kani/batch.rs (1)
program-libs/batched-merkle-tree/src/batch.rs (15)
new(95-119)get_state(122-124)bloom_filter_is_zeroed(126-128)advance_state_to_full(200-212)advance_state_to_inserted(184-196)advance_state_to_fill(155-180)from(20-27)from(31-33)start_slot_is_set(142-144)get_num_zkp_batches(273-275)get_num_hash_chain_store(278-280)get_num_inserted_elements(258-260)get_num_elements_inserted_into_tree(253-255)batch_is_ready_to_insert(224-226)get_num_ready_zkp_updates(230-233)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (21)
- GitHub Check: lint
- GitHub Check: cli-v1
- GitHub Check: stateless-js-v1
- GitHub Check: Forester e2e test
- GitHub Check: programs (system-cpi-test-v2-functional-account-infos, ["cargo-test-sbf -p system-cpi-v2-test -- ...
- GitHub Check: cli-v2
- GitHub Check: programs (system-cpi-test, ["cargo-test-sbf -p system-cpi-test", "cargo test -p light-system-prog...
- GitHub Check: programs (system-cpi-test-v2-functional-read-only, ["cargo-test-sbf -p system-cpi-v2-test -- func...
- GitHub Check: stateless-js-v2
- GitHub Check: programs (light-system-program-compression, ["cargo-test-sbf -p system-test -- test_with_compress...
- GitHub Check: programs (compressed-token-batched-tree, ["cargo-test-sbf -p compressed-token-test -- test_transf...
- GitHub Check: programs (light-system-program-address, ["cargo-test-sbf -p system-test -- test_with_address", "c...
- GitHub Check: programs (compressed-token-and-e2e, ["cargo-test-sbf -p compressed-token-test --test v1", "cargo-...
- GitHub Check: programs (account-compression-and-registry, ["cargo-test-sbf -p account-compression-test", "cargo...
- GitHub Check: Test batched-merkle-tree-simulate
- GitHub Check: Test program-libs-fast
- GitHub Check: Test program-libs-slow
- GitHub Check: system-programs (sdk-libs, light-sdk-macros light-sdk light-program-test light-client light-compr...
- GitHub Check: system-programs (token test, ["cargo-test-sbf -p sdk-token-test"])
- GitHub Check: system-programs (native, ["cargo-test-sbf -p sdk-native-test", "cargo-test-sbf -p sdk-v1-native-t...
- GitHub Check: system-programs (anchor & pinocchio, ["cargo-test-sbf -p sdk-anchor-test", "cargo-test-sbf -p sdk...
ananas-block
force-pushed
the
jorrit/refactor-tests
branch
from
246f394 to
3bad7a1
Compare
stash root fv works refactor: verify_no_unsafe_roots_minimal add invariants test: address tree scenarios
ananas-block
commented
Nov 3, 2025
Contributor
There was a problem hiding this comment.
Actionable comments posted: 4
🧹 Nitpick comments (1)
program-libs/batched-merkle-tree/tests/kani/address_tree_update.rs (1)
90-93: Fix unreachable coverage probe
kani::cover!(i == 99, "Loop iteration 29")can never trigger becauseiranges from 0 to 29. This silently defeats the intended coverage check. Please change the guard toi == 29(or adjust the loop bound accordingly) so the harness actually exercises the final iteration.- kani::cover!(i == 99, "Loop iteration 29"); + kani::cover!(i == 29, "Loop iteration 29");
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (16)
program-libs/account-checks/src/checks.rs(1 hunks)program-libs/batched-merkle-tree/Cargo.toml(2 hunks)program-libs/batched-merkle-tree/src/batch.rs(3 hunks)program-libs/batched-merkle-tree/src/merkle_tree.rs(37 hunks)program-libs/batched-merkle-tree/src/merkle_tree_metadata.rs(1 hunks)program-libs/batched-merkle-tree/src/queue.rs(7 hunks)program-libs/batched-merkle-tree/tests/kani.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/address_tree_update.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/ghost_state.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/mod.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/state_tree_update.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/utils.rs(1 hunks)program-libs/zero-copy/Cargo.toml(2 hunks)program-libs/zero-copy/src/cyclic_vec.rs(6 hunks)program-libs/zero-copy/src/vec.rs(7 hunks)program-libs/zero-copy/tests/kani.rs(1 hunks)
✅ Files skipped from review due to trivial changes (1)
- program-libs/batched-merkle-tree/tests/kani/mod.rs
🚧 Files skipped from review as they are similar to previous changes (2)
- program-libs/batched-merkle-tree/Cargo.toml
- program-libs/batched-merkle-tree/tests/kani.rs
🧰 Additional context used
📓 Path-based instructions (2)
program-libs/account-checks/src/checks.rs
📄 CodeRabbit inference engine (program-libs/account-checks/CLAUDE.md)
Expose and maintain account validation helpers (check_owner, check_program, check_mut/non_mut, check_signer, check_discriminator, set_discriminator, check_pda_seeds, check_account_balance_is_rent_exempt, account_info_init) in checks.rs
Files:
program-libs/account-checks/src/checks.rs
program-libs/account-checks/src/**/*.rs
📄 CodeRabbit inference engine (program-libs/account-checks/CLAUDE.md)
program-libs/account-checks/src/**/*.rs: On account initialization, call account_info_init to set the 8-byte discriminator
Validate account type with 8-byte discriminators using check_discriminator before deserialization
Return AccountError variants (codes 12006–12021) and rely on automatic ProgramError conversions; avoid returning raw ProgramError directly
Files:
program-libs/account-checks/src/checks.rs
🧠 Learnings (22)
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/{solana.rs,pinocchio.rs,test_account_info.rs} : Gate SDK-specific implementations with #[cfg(feature = "solana"|"pinocchio"|"test-only")]
Applied to files:
program-libs/batched-merkle-tree/tests/kani/ghost_state.rsprogram-libs/batched-merkle-tree/src/queue.rsprogram-libs/zero-copy/Cargo.tomlprogram-libs/account-checks/src/checks.rsprogram-libs/batched-merkle-tree/tests/kani/utils.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-08-14T00:36:53.191Z
Learnt from: ananas-block
Repo: Lightprotocol/light-protocol PR: 1909
File: program-libs/zero-copy/src/init_mut.rs:241-249
Timestamp: 2025-08-14T00:36:53.191Z
Learning: In the light-protocol zero-copy crate, performance is prioritized over safety checks for edge cases like Vec lengths exceeding u32::MAX, even when there might be wire format inconsistencies.
Applied to files:
program-libs/zero-copy/tests/kani.rsprogram-libs/batched-merkle-tree/src/queue.rsprogram-libs/zero-copy/src/cyclic_vec.rsprogram-libs/zero-copy/src/vec.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-16T06:33:55.362Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:55.362Z
Learning: Applies to programs/compressed-token/program/program-libs/ctoken-types/** : Define all state and instruction data structures in the light-ctoken-types crate (program-libs/ctoken-types), including state/, instructions/, and state/extensions/
Applied to files:
program-libs/batched-merkle-tree/tests/kani/state_tree_update.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/account_compression_cpi/mod.rs : Export each new operation module by adding pub mod <operation>; and re-export with pub use <operation>::*.
Applied to files:
program-libs/batched-merkle-tree/tests/kani/state_tree_update.rsprogram-libs/batched-merkle-tree/tests/kani/utils.rs
📚 Learning: 2025-10-16T06:33:19.426Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/compressible/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:19.426Z
Learning: Applies to program-libs/compressible/src/config.rs : Ensure serialization compatibility across Anchor, Pinocchio, and Borsh for core account types used by dependent programs
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/zero-copy/src/cyclic_vec.rsprogram-libs/account-checks/src/checks.rsprogram-libs/batched-merkle-tree/tests/kani/utils.rsprogram-libs/zero-copy/src/vec.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Load accounts according to type before check_forester: batched via BatchedMerkleTreeAccount::type_from_account_info(); regular via ctx.accounts.account.load()?.metadata; use custom deserialization when required.
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/discriminator.rs : Define and keep discriminator constants and the Discriminator trait in discriminator.rs for compile-time verification
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/account-checks/src/checks.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/account_info_trait.rs : Ensure the crate compiles with no features enabled by keeping trait definitions free of SDK-specific dependencies
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/account-checks/src/checks.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/{solana.rs,pinocchio.rs,test_account_info.rs} : Provide SDK-specific AccountInfoTrait implementations in account_info/{solana.rs,pinocchio.rs,test_account_info.rs}
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/account-checks/src/checks.rsprogram-libs/batched-merkle-tree/tests/kani/utils.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/packed_accounts.rs : For dynamic account sets, use PackedAccounts for index-based access with bounds checks instead of manual indexing
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/test_account_info.rs : Use the mock AccountInfo implementation under the test-only feature for unit tests
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/batched-merkle-tree/tests/kani/utils.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : Validate account type with 8-byte discriminators using check_discriminator before deserialization
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/account-checks/src/checks.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/!(account_info)/**/*.rs : Use AccountInfoTrait for runtime-agnostic account handling; avoid direct solana-program or pinocchio AccountInfo in general logic
Applied to files:
program-libs/batched-merkle-tree/src/queue.rs
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/DISCRIMINATOR.md : DISCRIMINATOR.md must document 8-byte discriminators, the Discriminator trait, constant arrays for compile-time checks, and integration with account initialization
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/account-checks/src/checks.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : On account initialization, call account_info_init to set the 8-byte discriminator
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/account-checks/src/checks.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-16T06:33:55.362Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:55.362Z
Learning: Applies to programs/compressed-token/program/docs/ACCOUNTS.md : Account documentation must include: description, discriminator, state layout, serialization example, hashing (only for compressed accounts), derivation (only for PDAs), and associated instructions
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Instruction handlers must compute work_units by operation type: batch operations use account.queue_batches.batch_size; single operations use DEFAULT_WORK_V1; custom operations compute based on complexity.
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/batched-merkle-tree/src/merkle_tree_metadata.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/checks.rs : Expose and maintain account validation helpers (check_owner, check_program, check_mut/non_mut, check_signer, check_discriminator, set_discriminator, check_pda_seeds, check_account_balance_is_rent_exempt, account_info_init) in checks.rs
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/account-checks/src/checks.rsprogram-libs/batched-merkle-tree/tests/kani/utils.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_iterator.rs : Use AccountIterator for sequential account retrieval to get precise file:line:column error locations; avoid manual index handling
Applied to files:
program-libs/batched-merkle-tree/src/queue.rsprogram-libs/batched-merkle-tree/src/merkle_tree_metadata.rsprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/**/Cargo.toml : Define features solana, pinocchio, and test-only in Cargo.toml; default build should enable none
Applied to files:
program-libs/zero-copy/Cargo.tomlprogram-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/{ACCOUNT_INFO_TRAIT.md,ACCOUNT_CHECKS.md,ACCOUNT_ITERATOR.md,DISCRIMINATOR.md,ERRORS.md,PACKED_ACCOUNTS.md} : Code examples should demonstrate both Solana and Pinocchio usage where applicable
Applied to files:
program-libs/zero-copy/Cargo.toml
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/account_compression_cpi/**/*.rs : Pass the data Vec<u8> through unchanged from the wrapper to the target program CPI; the target program performs deserialization.
Applied to files:
program-libs/zero-copy/src/cyclic_vec.rsprogram-libs/account-checks/src/checks.rsprogram-libs/zero-copy/src/vec.rs
🧬 Code graph analysis (9)
program-libs/batched-merkle-tree/tests/kani/ghost_state.rs (2)
program-libs/batched-merkle-tree/tests/kani/utils.rs (3)
stub_hash_to_bn254(12-14)create_test_tree_small(58-96)setup_batches(144-161)program-libs/batched-merkle-tree/src/batch.rs (2)
bloom_filter_is_zeroed(126-128)batch_is_ready_to_insert(233-235)
program-libs/zero-copy/tests/kani.rs (2)
program-libs/zero-copy/src/vec.rs (7)
capacity(262-264)required_size_for_capacity(257-259)new(57-59)len(267-269)is_empty(272-274)push(199-211)get(277-282)program-libs/zero-copy/src/cyclic_vec.rs (7)
capacity(335-337)required_size_for_capacity(325-327)new(56-58)len(330-332)is_empty(340-342)push(212-229)get(345-350)
program-libs/batched-merkle-tree/tests/kani/state_tree_update.rs (5)
program-libs/batched-merkle-tree/src/merkle_tree.rs (4)
BatchedMerkleTreeAccount(1553-1553)BatchedMerkleTreeAccount(1563-1563)BatchedMerkleTreeAccount(1573-1573)pubkey(1346-1348)program-libs/batched-merkle-tree/src/queue.rs (2)
BatchedQueueAccount(764-764)pubkey(514-516)program-libs/hasher/src/hash_to_field_size.rs (1)
hash_to_bn254_field_size_be(99-101)program-libs/batched-merkle-tree/tests/kani/utils.rs (7)
stub_hash_to_bn254(12-14)create_test_tree_small_state(99-137)setup_batches(144-161)setup_zkp_batches(166-182)create_test_output_queue(223-258)setup_output_queue_batches(262-281)setup_output_queue_zkp_batches(285-301)program-libs/batched-merkle-tree/src/batch.rs (2)
batch_is_ready_to_insert(233-235)get_state(122-124)
program-libs/batched-merkle-tree/src/queue.rs (2)
program-libs/zero-copy/src/vec.rs (10)
size_of(102-102)size_of(164-164)size_of(243-243)size_of(253-253)core(105-105)core(167-167)from_bytes_at(123-178)from_bytes(118-120)new(57-59)new_at(61-115)program-libs/batched-merkle-tree/src/merkle_tree.rs (7)
from_bytes(240-313)pubkey(1346-1348)Self(183-183)Self(198-198)Self(210-210)Self(226-226)Self(237-237)
program-libs/zero-copy/src/cyclic_vec.rs (1)
program-libs/zero-copy/src/errors.rs (4)
from(72-91)from(96-98)from(103-105)from(117-129)
program-libs/batched-merkle-tree/tests/kani/utils.rs (3)
program-libs/batched-merkle-tree/src/merkle_tree.rs (8)
BatchedMerkleTreeAccount(1553-1553)BatchedMerkleTreeAccount(1563-1563)BatchedMerkleTreeAccount(1573-1573)pubkey(1346-1348)get_merkle_tree_account_size(1427-1452)std(254-254)std(339-339)init(316-482)program-libs/batched-merkle-tree/src/queue.rs (7)
pubkey(514-516)std(213-213)std(280-280)init(55-90)init(259-346)BatchedQueueAccount(764-764)get_output_queue_account_size(652-667)program-libs/batched-merkle-tree/src/batch.rs (2)
new(95-119)get_num_zkp_batches(338-340)
program-libs/batched-merkle-tree/tests/kani/address_tree_update.rs (2)
program-libs/batched-merkle-tree/tests/kani/utils.rs (6)
stub_hash_to_bn254(12-14)create_test_tree_small(58-96)setup_batches(144-161)setup_zkp_batches(166-182)get_total_ready_zkp_batches(185-197)get_available_zkp_space(200-220)program-libs/batched-merkle-tree/src/batch.rs (2)
batch_is_ready_to_insert(233-235)get_state(122-124)
program-libs/zero-copy/src/vec.rs (2)
program-libs/zero-copy/src/errors.rs (4)
from(72-91)from(96-98)from(103-105)from(117-129)program-libs/zero-copy/src/lib.rs (1)
align_of(34-34)
program-libs/batched-merkle-tree/src/merkle_tree.rs (5)
program-libs/batched-merkle-tree/src/batch.rs (5)
from(20-27)from(31-33)new(95-119)batch_is_ready_to_insert(233-235)get_num_inserted_zkps(313-315)program-libs/zero-copy/src/vec.rs (12)
size_of(102-102)size_of(164-164)size_of(243-243)size_of(253-253)core(105-105)core(167-167)from_bytes(118-120)from_bytes_at(123-178)new(57-59)len(267-269)new_at(61-115)iter(416-418)program-libs/zero-copy/src/cyclic_vec.rs (7)
size_of(110-110)from_bytes(121-123)from_bytes_at(126-179)new(56-58)len(330-332)new_at(60-119)iter(285-292)program-libs/batched-merkle-tree/src/queue.rs (5)
from_bytes(200-256)pubkey(514-516)Self(167-167)Self(186-186)Self(197-197)program-libs/verifier/src/lib.rs (1)
verify_batch_append_with_proofs(366-384)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (21)
- GitHub Check: Forester e2e test
- GitHub Check: programs (system-cpi-test-v2-functional-read-only, ["cargo-test-sbf -p system-cpi-v2-test -- func...
- GitHub Check: programs (system-cpi-test-v2-functional-account-infos, ["cargo-test-sbf -p system-cpi-v2-test -- ...
- GitHub Check: programs (compressed-token-and-e2e, ["cargo-test-sbf -p compressed-token-test --test v1", "cargo-...
- GitHub Check: programs (light-system-program-compression, ["cargo-test-sbf -p system-test -- test_with_compress...
- GitHub Check: programs (compressed-token-batched-tree, ["cargo-test-sbf -p compressed-token-test -- test_transf...
- GitHub Check: programs (light-system-program-address, ["cargo-test-sbf -p system-test -- test_with_address", "c...
- GitHub Check: programs (system-cpi-test, ["cargo-test-sbf -p system-cpi-test", "cargo test -p light-system-prog...
- GitHub Check: programs (account-compression-and-registry, ["cargo-test-sbf -p account-compression-test", "cargo...
- GitHub Check: Test program-libs-slow
- GitHub Check: Test program-libs-fast
- GitHub Check: Test batched-merkle-tree-simulate
- GitHub Check: system-programs (token test, ["cargo-test-sbf -p sdk-token-test"])
- GitHub Check: system-programs (native, ["cargo-test-sbf -p sdk-native-test", "cargo-test-sbf -p sdk-v1-native-t...
- GitHub Check: stateless-js-v1
- GitHub Check: system-programs (anchor & pinocchio, ["cargo-test-sbf -p sdk-anchor-test", "cargo-test-sbf -p sdk...
- GitHub Check: system-programs (sdk-libs, light-sdk-macros light-sdk light-program-test light-client light-compr...
- GitHub Check: lint
- GitHub Check: stateless-js-v2
- GitHub Check: cli-v1
- GitHub Check: cli-v2
🔇 Additional comments (1)
program-libs/account-checks/src/checks.rs (1)
69-71: Verify that skipping the zero-check in Kani builds aligns with verification goals.The
check_data_is_zeroedcall is now gated to exclude Kani verification builds. This means Kani won't verify that accounts are uninitialized before setting the discriminator, which could miss double-initialization bugs during formal verification.If this is intentional (e.g., the check interferes with symbolic execution or Kani focuses on other properties), consider adding a brief comment in the function documentation noting the conditional behavior.
Comment on lines
+1177
to
+1188
| // Condition 1 & 2: Current batch is at least half full and not inserted | ||
| let current_batch_is_half_full = { | ||
| let current_batch_is_not_inserted = | ||
| self.queue_batches.batches[current_batch].get_state() != BatchState::Inserted; | ||
| let num_inserted_elements = | ||
| self.queue_batches.batches[current_batch].get_num_inserted_elements(); | ||
| num_inserted_elements >= batch_size / 2 && current_batch_is_not_inserted | ||
| }; | ||
|
|
||
| // Condition 3 & 4: Previous batch is inserted but not zeroed | ||
| let previous_batch_is_ready = { | ||
| let previous_batch = &self.queue_batches.batches[previous_batch_index]; |
Contributor
There was a problem hiding this comment.
Fix “half full” check to require a true 50 % fill.
The predicate currently compares num_inserted_elements >= batch_size / 2. Because integer division truncates, an odd batch (e.g. size = 3) is treated as “half full” after only one insertion (33 %), which contradicts the documented “wait until next batch is 50 % full” grace period and allows bloom filters to be zeroed too early.
Compute the ceiling instead to map odd sizes correctly:
- let current_batch_is_half_full = {
+ let half_threshold = batch_size.saturating_add(1) / 2;
+ let current_batch_is_half_full = {
let current_batch_is_not_inserted =
self.queue_batches.batches[current_batch].get_state() != BatchState::Inserted;
let num_inserted_elements =
self.queue_batches.batches[current_batch].get_num_inserted_elements();
- num_inserted_elements >= batch_size / 2 && current_batch_is_not_inserted
+ num_inserted_elements >= half_threshold && current_batch_is_not_inserted
};This keeps the even case unchanged while preserving the intended 50 % bar for odd batch sizes.
🤖 Prompt for AI Agents
In program-libs/batched-merkle-tree/src/merkle_tree.rs around lines 1177 to
1188, the "half full" check uses integer truncating division
(num_inserted_elements >= batch_size / 2) which treats odd batch sizes
incorrectly; change the threshold to the ceiling of half the batch (e.g. compute
half_threshold = (batch_size + 1) / 2) and compare num_inserted_elements >=
half_threshold so odd sizes require a true 50% fill while even sizes remain
unchanged.
Comment on lines
+519
to
+524
| #[cfg(kani)] | ||
| impl<'a> BatchedQueueAccount<'a> { | ||
| pub fn kani_mock_insert(&mut self, batch_idx: usize) -> Result<(), BatchedMerkleTreeError> { | ||
| self.batch_metadata.batches[batch_idx].kani_mock_output_insert() | ||
| } | ||
| } |
Contributor
There was a problem hiding this comment.
🛠️ Refactor suggestion | 🟠 Major
Restore next_index updates in the Kani mock insert
kani_mock_insert never bumps batch_metadata.next_index, so under cfg(kani) the queue’s logical cursor stays at 0. As a result tree_is_full() and any start-index bookkeeping that relies on next_index never change, which breaks the invariants these harnesses are supposed to cover. Please mirror the real insert_into_current_batch behaviour by incrementing next_index on each mock insert.
pub fn kani_mock_insert(&mut self, batch_idx: usize) -> Result<(), BatchedMerkleTreeError> {
- self.batch_metadata.batches[batch_idx].kani_mock_output_insert()
+ self.batch_metadata.batches[batch_idx].kani_mock_output_insert()?;
+ self.batch_metadata.next_index += 1;
+ Ok(())
}🤖 Prompt for AI Agents
In program-libs/batched-merkle-tree/src/queue.rs around lines 519 to 524, the
cfg(kani) helper kani_mock_insert calls kani_mock_output_insert but does not
update batch_metadata.next_index, leaving the logical cursor at 0 and breaking
invariants; fix by incrementing self.batch_metadata.next_index after a
successful kani_mock_output_insert to mirror insert_into_current_batch behavior
(respect existing bounds/overflow semantics used in the real insert — e.g., only
increment on Ok and propagate any error if next_index would exceed batch
capacity).
Comment on lines
+34
to
+37
| // Allocate using mem::zeroed() reduces branches in Kani | ||
| let account_data: &'static mut [u8; 8096] = Box::leak(Box::new(unsafe { std::mem::zeroed() })); | ||
| let account_data: &'static mut [u8] = &mut account_data[..size]; | ||
| let pubkey = Pubkey::new_from_array([1u8; 32]); |
Contributor
There was a problem hiding this comment.
Avoid slicing a fixed buffer by a larger runtime size.
get_merkle_tree_account_size already computes the exact length required for the account. If that length ever exceeds the hard-coded 8 096 bytes (for example after a metadata enlargement—which is very plausible given the ghost-state additions in this PR), &mut account_data[..size] will panic before Kani even exercises the tree. The same pattern appears in the smaller helpers (lines 76-78 and 117-118), so they carry the same risk.
Allocate the buffer to size up front and then leak it, e.g.
- let account_data: &'static mut [u8; 8096] = Box::leak(Box::new(unsafe { std::mem::zeroed() }));
- let account_data: &'static mut [u8] = &mut account_data[..size];
+ let account_data: &'static mut [u8] =
+ Box::leak(vec![0u8; size].into_boxed_slice());Repeat for the other helpers (using size instead of 2 048). This removes the panic hazard without changing the rest of the initialization flow.
🤖 Prompt for AI Agents
In program-libs/batched-merkle-tree/tests/kani/utils.rs around lines 34 to 37,
avoid allocating a fixed 8_096-byte array and then slicing it by a runtime size
(which can panic if size > 8_096); instead allocate a buffer of length size up
front and leak that (e.g., create a Vec<u8> of length size, convert to a boxed
slice and Box::leak to get &'static mut [u8]). Apply the same change to the
other helpers at lines ~76-78 and ~117-118 (use size rather than the hard-coded
2_048) so the buffer always matches the required account size and eliminates the
panic hazard.
Comment on lines
+108
to
+117
| #[cfg(feature = "kani")] | ||
| let (slice, remaining_bytes) = { | ||
| let needed_size = capacity_usize * size_of::<T>(); | ||
| let (slice_bytes, remaining) = bytes.split_at_mut(needed_size); | ||
| let slice = unsafe { | ||
| let ptr = slice_bytes.as_mut_ptr() as *mut T; | ||
| core::slice::from_raw_parts_mut(ptr, capacity_usize) | ||
| }; | ||
| (slice, remaining) | ||
| }; |
Contributor
There was a problem hiding this comment.
Prevent panics when the backing slice is too small
Line 112 calls split_at_mut(needed_size) without first checking bytes.len() >= needed_size. In the non-kani path this guard is provided by Ref::from_prefix_with_elems, which returns ZeroCopyError instead of unwinding. With the new kani branch, any undersized buffer (exactly the scenario formal proofs should explore) now triggers a panic, breaking the function’s contract. Please restore the explicit length check and return ZeroCopyError::InsufficientMemoryAllocated to match the existing behavior.
- #[cfg(feature = "kani")]
- let (slice, remaining_bytes) = {
- let needed_size = capacity_usize * size_of::<T>();
+ #[cfg(feature = "kani")]
+ let (slice, remaining_bytes) = {
+ let needed_size = capacity_usize * size_of::<T>();
+ if bytes.len() < needed_size {
+ return Err(ZeroCopyError::InsufficientMemoryAllocated(
+ bytes.len() + metadata_size,
+ needed_size + metadata_size,
+ ));
+ }
let (slice_bytes, remaining) = bytes.split_at_mut(needed_size);
let slice = unsafe {
let ptr = slice_bytes.as_mut_ptr() as *mut T;
core::slice::from_raw_parts_mut(ptr, capacity_usize)
};
(slice, remaining)
};Committable suggestion skipped: line range outside the PR's diff.
🤖 Prompt for AI Agents
In program-libs/zero-copy/src/cyclic_vec.rs around lines 108 to 117, the kani
branch calls split_at_mut(needed_size) without checking bytes.len(), which can
panic; add an explicit check like if bytes.len() < needed_size { return
Err(ZeroCopyError::InsufficientMemoryAllocated); } before computing
needed_size/splitting so the function mirrors the non-kani path and returns
ZeroCopyError instead of unwinding; keep the rest of the slice creation logic
unchanged.
Contributor
There was a problem hiding this comment.
Actionable comments posted: 0
♻️ Duplicate comments (1)
program-libs/batched-merkle-tree/src/merkle_tree.rs (1)
1185-1192: Fix "half full" check to require a true 50% fill.The predicate currently compares
num_inserted_elements >= batch_size / 2. Because integer division truncates, an odd batch (e.g. size = 3) is treated as "half full" after only one insertion (33%), which contradicts the documented "wait until next batch is 50% full" grace period.Compute the ceiling instead:
// Condition 1 & 2: Current batch is at least half full and not inserted + let half_threshold = batch_size.saturating_add(1) / 2; let current_batch_is_half_full = { let current_batch_is_not_inserted = self.queue_batches.batches[current_batch].get_state() != BatchState::Inserted; let num_inserted_elements = self.queue_batches.batches[current_batch].get_num_inserted_elements(); - num_inserted_elements >= batch_size / 2 && current_batch_is_not_inserted + num_inserted_elements >= half_threshold && current_batch_is_not_inserted };
🧹 Nitpick comments (5)
program-libs/batched-merkle-tree/tests/kani/state_tree_update.rs (5)
49-59: Remove unnecessary outer loop.The outer loop
for i in 0..1executes exactly once and serves no purpose. Additionally, the inner loop variableishadows the (unused) outer loop variable.Apply this diff to simplify the code:
- for i in 0..1 { - let num_insertions: u8 = 6; - for i in 1..=num_insertions { - let new_root: [u8; 32] = [i; 32]; - let result = tree.update_tree_from_input_queue(InstructionDataBatchNullifyInputs { - new_root, - compressed_proof: CompressedProof::default(), // we stub proof verification internally so the proof doesnt matter - }); - kani::cover!(result.is_ok(), "Update succeeded"); - } + let num_insertions: u8 = 6; + for i in 1..=num_insertions { + let new_root: [u8; 32] = [i; 32]; + let result = tree.update_tree_from_input_queue(InstructionDataBatchNullifyInputs { + new_root, + compressed_proof: CompressedProof::default(), // we stub proof verification internally so the proof doesnt matter + }); + kani::cover!(result.is_ok(), "Update succeeded"); }
166-168: Fix postcondition numbering in comment.The comment refers to "Postcondition 4" but based on the documented postconditions at the top of the function (lines 115-116), this should be "Postcondition 3."
Apply this diff:
- // Postcondition 4: Root history contains [6u8; 32] + // Postcondition 3: Root history contains [6u8; 32] let contains_root_5 = (0..tree.root_history.len()).any(|i| tree.root_history[i] == [6u8; 32]); assert!(contains_root_5);
256-263: Function name doesn't match implementation.The function is named
verify_state_tree_mixed_randombut the implementation uses a deterministic index progression (index += 1) rather than random/symbolic choices. The commented-out code (lines 309-342) useskani::any()which would actually provide non-deterministic behavior matching the "random" name.Consider either:
- Renaming the function to
verify_state_tree_mixed_deterministicorverify_state_tree_mixed_sequential, or- Uncommenting lines 309-342 to enable the random exploration that matches the function name
264-264: Remove unnecessary parentheses.The parentheses around the range expression are unnecessary.
Apply this diff:
- for i in (0..10u8) { + for i in 0..10u8 {
309-342: Remove or uncomment large code block.This large commented-out code block (34 lines) uses
kani::any()for symbolic exploration, which would align with the function name "random".If this code is still needed for exploration, uncomment it. Otherwise, remove it to reduce maintenance burden.
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (4)
.gitignore(1 hunks)program-libs/batched-merkle-tree/src/merkle_tree.rs(37 hunks)program-libs/batched-merkle-tree/tests/kani/address_tree_update.rs(1 hunks)program-libs/batched-merkle-tree/tests/kani/state_tree_update.rs(1 hunks)
✅ Files skipped from review due to trivial changes (1)
- .gitignore
🚧 Files skipped from review as they are similar to previous changes (1)
- program-libs/batched-merkle-tree/tests/kani/address_tree_update.rs
🧰 Additional context used
🧠 Learnings (16)
📚 Learning: 2025-10-16T06:33:55.362Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:55.362Z
Learning: Applies to programs/compressed-token/program/program-libs/ctoken-types/** : Define all state and instruction data structures in the light-ctoken-types crate (program-libs/ctoken-types), including state/, instructions/, and state/extensions/
Applied to files:
program-libs/batched-merkle-tree/tests/kani/state_tree_update.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/account_compression_cpi/mod.rs : Export each new operation module by adding pub mod <operation>; and re-export with pub use <operation>::*.
Applied to files:
program-libs/batched-merkle-tree/tests/kani/state_tree_update.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Load accounts according to type before check_forester: batched via BatchedMerkleTreeAccount::type_from_account_info(); regular via ctx.accounts.account.load()?.metadata; use custom deserialization when required.
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-16T06:33:19.426Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/compressible/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:19.426Z
Learning: Applies to program-libs/compressible/src/config.rs : Ensure serialization compatibility across Anchor, Pinocchio, and Borsh for core account types used by dependent programs
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_info/{solana.rs,pinocchio.rs,test_account_info.rs} : Gate SDK-specific implementations with #[cfg(feature = "solana"|"pinocchio"|"test-only")]
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/**/Cargo.toml : Define features solana, pinocchio, and test-only in Cargo.toml; default build should enable none
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-08-14T00:36:53.191Z
Learnt from: ananas-block
Repo: Lightprotocol/light-protocol PR: 1909
File: program-libs/zero-copy/src/init_mut.rs:241-249
Timestamp: 2025-08-14T00:36:53.191Z
Learning: In the light-protocol zero-copy crate, performance is prioritized over safety checks for edge cases like Vec lengths exceeding u32::MAX, even when there might be wire format inconsistencies.
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/discriminator.rs : Define and keep discriminator constants and the Discriminator trait in discriminator.rs for compile-time verification
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:52.712Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/docs/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:52.712Z
Learning: Applies to program-libs/account-checks/docs/**/DISCRIMINATOR.md : DISCRIMINATOR.md must document 8-byte discriminators, the Discriminator trait, constant arrays for compile-time checks, and integration with account initialization
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : Validate account type with 8-byte discriminators using check_discriminator before deserialization
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-16T06:33:55.362Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/compressed-token/program/CLAUDE.md:0-0
Timestamp: 2025-10-16T06:33:55.362Z
Learning: Applies to programs/compressed-token/program/docs/ACCOUNTS.md : Account documentation must include: description, discriminator, state layout, serialization example, hashing (only for compressed accounts), derivation (only for PDAs), and associated instructions
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/**/*.rs : On account initialization, call account_info_init to set the 8-byte discriminator
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/checks.rs : Expose and maintain account validation helpers (check_owner, check_program, check_mut/non_mut, check_signer, check_discriminator, set_discriminator, check_pda_seeds, check_account_balance_is_rent_exempt, account_info_init) in checks.rs
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/packed_accounts.rs : For dynamic account sets, use PackedAccounts for index-based access with bounds checks instead of manual indexing
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-11T21:59:25.222Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: program-libs/account-checks/CLAUDE.md:0-0
Timestamp: 2025-10-11T21:59:25.222Z
Learning: Applies to program-libs/account-checks/src/account_iterator.rs : Use AccountIterator for sequential account retrieval to get precise file:line:column error locations; avoid manual index handling
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
📚 Learning: 2025-10-15T03:46:26.767Z
Learnt from: CR
Repo: Lightprotocol/light-protocol PR: 0
File: programs/registry/CLAUDE.md:0-0
Timestamp: 2025-10-15T03:46:26.767Z
Learning: Applies to programs/registry/src/lib.rs : Instruction handlers must compute work_units by operation type: batch operations use account.queue_batches.batch_size; single operations use DEFAULT_WORK_V1; custom operations compute based on complexity.
Applied to files:
program-libs/batched-merkle-tree/src/merkle_tree.rs
🧬 Code graph analysis (2)
program-libs/batched-merkle-tree/tests/kani/state_tree_update.rs (5)
program-libs/batched-merkle-tree/src/merkle_tree.rs (4)
BatchedMerkleTreeAccount(1561-1561)BatchedMerkleTreeAccount(1571-1571)BatchedMerkleTreeAccount(1581-1581)pubkey(1354-1356)program-libs/batched-merkle-tree/src/queue.rs (2)
BatchedQueueAccount(764-764)pubkey(514-516)program-libs/hasher/src/hash_to_field_size.rs (1)
hash_to_bn254_field_size_be(99-101)program-libs/batched-merkle-tree/tests/kani/utils.rs (7)
stub_hash_to_bn254(12-14)create_test_tree_small_state(99-137)setup_batches(144-161)setup_zkp_batches(166-182)create_test_output_queue(223-258)setup_output_queue_batches(262-281)setup_output_queue_zkp_batches(285-301)program-libs/batched-merkle-tree/src/batch.rs (2)
batch_is_ready_to_insert(233-235)get_state(122-124)
program-libs/batched-merkle-tree/src/merkle_tree.rs (5)
program-libs/batched-merkle-tree/src/batch.rs (6)
from(20-27)from(31-33)new(95-119)batch_is_ready_to_insert(233-235)get_num_inserted_zkps(313-315)get_state(122-124)program-libs/zero-copy/src/vec.rs (12)
size_of(102-102)size_of(164-164)size_of(243-243)size_of(253-253)core(105-105)core(167-167)from_bytes(118-120)from_bytes_at(123-178)new(57-59)len(267-269)new_at(61-115)iter(416-418)program-libs/zero-copy/src/cyclic_vec.rs (7)
size_of(110-110)from_bytes(121-123)from_bytes_at(126-179)new(56-58)len(330-332)new_at(60-119)iter(285-292)program-libs/batched-merkle-tree/src/queue.rs (5)
from_bytes(200-256)pubkey(514-516)Self(167-167)Self(186-186)Self(197-197)program-libs/verifier/src/lib.rs (1)
verify_batch_append_with_proofs(366-384)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (13)
- GitHub Check: lint
- GitHub Check: Forester e2e test
- GitHub Check: Test batched-merkle-tree-simulate
- GitHub Check: Test program-libs-slow
- GitHub Check: Test program-libs-fast
- GitHub Check: programs (system-cpi-test-v2-functional-read-only, ["cargo-test-sbf -p system-cpi-v2-test -- func...
- GitHub Check: programs (account-compression-and-registry, ["cargo-test-sbf -p account-compression-test", "cargo...
- GitHub Check: programs (system-cpi-test-v2-functional-account-infos, ["cargo-test-sbf -p system-cpi-v2-test -- ...
- GitHub Check: programs (system-cpi-test, ["cargo-test-sbf -p system-cpi-test", "cargo test -p light-system-prog...
- GitHub Check: programs (compressed-token-and-e2e, ["cargo-test-sbf -p compressed-token-test --test v1", "cargo-...
- GitHub Check: programs (compressed-token-batched-tree, ["cargo-test-sbf -p compressed-token-test -- test_transf...
- GitHub Check: programs (light-system-program-compression, ["cargo-test-sbf -p system-test -- test_with_compress...
- GitHub Check: programs (light-system-program-address, ["cargo-test-sbf -p system-test -- test_with_address", "c...
🔇 Additional comments (7)
program-libs/batched-merkle-tree/src/merkle_tree.rs (7)
26-29: LGTM: Clean conditional compilation structure.The dual struct definitions and conditional imports are well-structured. The Kani variant adds ghost state tracking without affecting production builds, and the separation is clear.
Also applies to: 81-144
252-266: Verify alignment assumptions in Kani deserialization.The Kani branch uses
read_unaligned/write_unalignedfollowed by creating a mutable reference. While this is verification-only code, creating&mutfrom a potentially unaligned pointer is undefined behavior. The providedzero-copysnippets show similar patterns but include explicit alignment checks (e.g.,is_multiple_of(align_of::<T>())).Consider adding an explicit alignment check or document why
BatchedMerkleTreeMetadataalignment is guaranteed here:#[cfg(kani)] let (metadata, account_data) = { let size = std::mem::size_of::<BatchedMerkleTreeMetadata>(); if account_data.len() < size { return Err(ZeroCopyError::Size.into()); } let (meta_bytes, remaining) = account_data.split_at_mut(size); + // Verify alignment before creating mutable reference + if !(meta_bytes.as_ptr() as usize).is_multiple_of(core::mem::align_of::<BatchedMerkleTreeMetadata>()) { + return Err(ZeroCopyError::UnalignedPointer.into()); + } let metadata = unsafe { let ptr = meta_bytes.as_mut_ptr() as *mut BatchedMerkleTreeMetadata; - // Read potentially unaligned, write back, then get mutable ref - core::ptr::write_unaligned(ptr, core::ptr::read_unaligned(ptr as *const _)); - &mut *ptr + &mut *ptr // Safe after alignment check }; (metadata, remaining) };
337-351: Same alignment verification needed in init.The same unaligned pointer issue exists here. Either add an alignment check or document the safety invariant.
1008-1040: LGTM: Correct fix for unsafe root zeroing.The change from
1..num_remaining_rootsto0..num_remaining_rootscorrectly zeros all unsafe roots (not just all-but-one), and the newCannotZeroCompleteRootHistorycheck prevents deleting the entire tree state. This aligns with the PR objectives.
1259-1260: LGTM: Modulo precedence correctly fixed.The expression now properly wraps:
(previous_pending_batch.root_index + 1) % (self.root_history.len() as u32), ensuring correct wrap-around behavior. This addresses the previous review comment.
1365-1395: LGTM: Clean Kani-only test helpers.The
kani_mock_inserthelper and conditionalDerefimplementations are well-structured and properly isolated to verification builds.Also applies to: 1407-1432
1705-1776: LGTM: Test updates correctly verify the fix.The test modifications properly verify:
- The new
CannotZeroCompleteRootHistorycheck (lines 1705-1716)- That all unsafe roots are zeroed, not just all-but-one (lines 1776, 1881, 1988-1991)
- That the first safe root (at
root_index + 1) remains intactThe assertions using
!root_history.iter().any(|x| *x == last_batch0_root)confirm no unsafe roots remain after zeroing.Also applies to: 1856-1881, 1982-1992
ananas-block
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
formal verification branch should not be merged at this time.
Summary by CodeRabbit
New Features
Tests