Skip to content

Commit 3bad7a1

Browse files
committed
cleanup
1 parent 112e406 commit 3bad7a1

File tree

3 files changed

+10
-29
lines changed

3 files changed

+10
-29
lines changed

program-libs/batched-merkle-tree/src/merkle_tree.rs

Lines changed: 4 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -834,41 +834,27 @@ impl<'a> BatchedMerkleTreeAccount<'a> {
834834
.batches
835835
.get_mut(previous_pending_batch_index)
836836
.ok_or(BatchedMerkleTreeError::InvalidBatchIndex)?;
837-
println!(
838-
"previous_pending_batch_index {}",
839-
previous_pending_batch_index
840-
);
837+
841838
let no_insert_since_last_batch_root = (previous_pending_batch
842839
.sequence_number
843840
.saturating_sub(root_history_len))
844841
== sequence_number;
845842
let previous_batch_is_inserted = previous_pending_batch.get_state() == BatchState::Inserted;
846843
let previous_batch_is_ready =
847844
previous_batch_is_inserted && !previous_pending_batch.bloom_filter_is_zeroed();
848-
println!("current_batch_is_half_full {}", current_batch_is_half_full);
849-
println!("previous_batch_is_ready {}", previous_batch_is_ready);
850-
println!(
851-
"no_insert_since_last_batch_root {}",
852-
no_insert_since_last_batch_root
853-
);
854845

855846
// Current batch is at least half full, previous batch is inserted, and not zeroed.
856847
if current_batch_is_half_full && previous_batch_is_ready && !no_insert_since_last_batch_root
857848
{
858849
// 3.1. Mark bloom filter zeroed.
859850
previous_pending_batch.set_bloom_filter_to_zeroed();
860851
let seq = previous_pending_batch.sequence_number;
861-
println!(
862-
"previous_pending_batch.sequence_number {}",
863-
previous_pending_batch.sequence_number
864-
);
865-
println!("current sequence_number {}", sequence_number);
866852
// previous_pending_batch.root_index is the index the root
867853
// of the last update of that batch was inserted at.
868854
// This is the last unsafe root index.
869855
// The next index is safe.
870-
// TODO: add init check that root history must be greater than 2x batch size.
871-
let first_safe_root_index = previous_pending_batch.root_index + 1;
856+
let first_safe_root_index =
857+
(previous_pending_batch.root_index + 1) % (self.root_history.len() as u32);
872858

873859
// 3.2. Zero out bloom filter.
874860
{
@@ -1315,11 +1301,7 @@ mod test {
13151301
println!("previous_roots: {:?}", previous_roots);
13161302
assert_ne!(previous_roots, current_roots);
13171303
let root_index = account.queue_batches.batches[0].root_index;
1318-
// assert_eq!(
1319-
// account.root_history[root_index as usize],
1320-
// previous_roots[root_index as usize]
1321-
// );
1322-
println!("last_batch0_root {:?}", last_batch0_root);
1304+
13231305
assert_eq!(
13241306
account.queue_batches.batches[0].get_state(),
13251307
BatchState::Inserted
@@ -1581,7 +1563,6 @@ mod test {
15811563
.queue_batches
15821564
.increment_pending_batch_index_if_inserted(state);
15831565
}
1584-
//last_batch1_root_update2 = account.root_history.last().unwrap();
15851566
assert_eq!(
15861567
account.queue_batches.batches[0].get_state(),
15871568
BatchState::Inserted

program-libs/batched-merkle-tree/tests/kani/batch.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -253,7 +253,7 @@ fn verify_start_slot_flag() {
253253
assert!(batch.start_slot_is_set());
254254
}
255255

256-
/// Verify start_slot getter/setter duality (Firecracker pattern)
256+
/// Verify start_slot getter/setter duality
257257
#[kani::proof]
258258
fn verify_start_slot_duality() {
259259
let mut batch = any_batch();
@@ -265,7 +265,7 @@ fn verify_start_slot_duality() {
265265
assert!(batch.start_slot_is_set());
266266
}
267267

268-
/// Verify that state transitions cover expected execution paths (Firecracker pattern)
268+
/// Verify that state transitions cover expected execution paths
269269
#[kani::proof]
270270
fn verify_state_transition_coverage() {
271271
let mut batch = any_batch();
@@ -283,7 +283,7 @@ fn verify_state_transition_coverage() {
283283
kani::cover!(batch.get_state() == BatchState::Fill);
284284
}
285285

286-
/// Verify that invalid transitions are properly covered (Firecracker pattern)
286+
/// Verify that invalid transitions are properly covered
287287
#[kani::proof]
288288
fn verify_invalid_transition_coverage() {
289289
let mut batch = any_batch();

program-libs/batched-merkle-tree/tests/kani/zero_out_roots.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ fn stub_hash_to_bn254(_input: &[u8]) -> [u8; 32] {
1212
}
1313

1414
// Helper to create a BatchedMerkleTreeAccount with bounded parameters for Kani
15-
// Uses CONCRETE values for initialization to avoid state explosion (Firecracker pattern)
15+
// Uses CONCRETE values for initialization to avoid state explosion
1616
// We only need symbolic inputs for zero_out_roots parameters, not for tree setup!
1717
//
1818
// NOTE: We use concrete values instead of kani::any() to eliminate state explosion
@@ -165,7 +165,7 @@ fn verify_zero_out_roots_error_too_many() {
165165
BatchedMerkleTreeError::CannotZeroCompleteRootHistory
166166
);
167167

168-
// Coverage: ensure error path is reachable (Firecracker pattern)
168+
// Coverage: ensure error path is reachable
169169
kani::cover!(true);
170170
}
171171

@@ -270,7 +270,7 @@ fn verify_zero_out_roots_wraparound() {
270270
kani::cover!(first_safe_root_index < oldest_root_index as u32);
271271
}
272272

273-
/// Verify that defensive assertion always holds (Firecracker pattern)
273+
/// Verify that defensive assertion always holds
274274
/// This tests the internal consistency check: oldest_root_index after zeroing == first_safe_root_index
275275
#[kani::proof]
276276
#[kani::stub(

0 commit comments

Comments
 (0)