@@ -366,18 +366,21 @@ fn arb_tx_message() -> impl Strategy<Value = TxMessage> {
366366 any :: < u64 > ( ) . prop_filter ( "Valid gas limit" , |& g| g > 0 ) ,
367367 any :: < u64 > ( ) ,
368368 any :: < u64 > ( ) ,
369+ prop:: collection:: vec ( any :: < u8 > ( ) , 0 ..256 ) ,
369370 )
370371 . prop_map (
371- |( chain_id, nonce, from, to, value, gas_limit, max_fee, priority_fee) | TxMessage {
372- chain_id,
373- nonce,
374- from,
375- to,
376- value : value as u128 ,
377- data : vec ! [ ] ,
378- gas_limit,
379- max_fee_per_gas : max_fee as u128 ,
380- max_priority_fee_per_gas : priority_fee as u128 ,
372+ |( chain_id, nonce, from, to, value, gas_limit, max_fee, priority_fee, data) | {
373+ TxMessage {
374+ chain_id,
375+ nonce,
376+ from,
377+ to,
378+ value : value as u128 ,
379+ data,
380+ gas_limit,
381+ max_fee_per_gas : max_fee as u128 ,
382+ max_priority_fee_per_gas : priority_fee as u128 ,
383+ }
381384 } ,
382385 )
383386}
@@ -440,6 +443,95 @@ proptest! {
440443 let hash2 = tx. signing_hash( & leaf_hash2) ;
441444 prop_assert_ne!( hash1, hash2, "Different leaf hashes should produce different signing hashes" ) ;
442445 }
446+
447+ /// Property: Different calldata produces different signing hash
448+ #[ test]
449+ fn prop_tx_calldata_sensitivity(
450+ tx in arb_tx_message( ) ,
451+ leaf_hash in prop:: array:: uniform32( any:: <u8 >( ) ) ,
452+ extra_byte in any:: <u8 >( )
453+ ) {
454+ let hash1 = tx. signing_hash( & leaf_hash) ;
455+ let mut tx2 = tx. clone( ) ;
456+ tx2. data. push( extra_byte) ;
457+ let hash2 = tx2. signing_hash( & leaf_hash) ;
458+ prop_assert_ne!( hash1, hash2, "Adding a calldata byte must change the signing hash" ) ;
459+ }
460+
461+ /// Property: Empty calldata differs from non-empty calldata
462+ #[ test]
463+ fn prop_tx_empty_vs_nonempty_calldata(
464+ mut tx in arb_tx_message( ) ,
465+ leaf_hash in prop:: array:: uniform32( any:: <u8 >( ) ) ,
466+ nonempty_data in prop:: collection:: vec( any:: <u8 >( ) , 1 ..128 )
467+ ) {
468+ tx. data = vec![ ] ;
469+ let hash_empty = tx. signing_hash( & leaf_hash) ;
470+ tx. data = nonempty_data;
471+ let hash_nonempty = tx. signing_hash( & leaf_hash) ;
472+ prop_assert_ne!( hash_empty, hash_nonempty, "Empty vs non-empty calldata must produce different hash" ) ;
473+ }
474+ }
475+
476+ // ── Merkle leaf_index property tests ─────────────────────────────────────────
477+
478+ proptest ! {
479+ #![ proptest_config( ProptestConfig :: with_cases( 128 ) ) ]
480+
481+ /// Property: proof generated for index A fails verification with a different leaf hash
482+ #[ test]
483+ fn prop_merkle_proof_wrong_index_rejected(
484+ // Use distinct discriminants to produce unique, valid leaf scripts: [0x60, discriminant]
485+ discriminants in prop:: collection:: vec( any:: <u8 >( ) , 2 ..8 )
486+ ) {
487+ // Build leaves with script [0x60, d] (PUSH1 d) — always valid EVM
488+ let mut leaves: Vec <Leaf > = discriminants
489+ . into_iter( )
490+ . enumerate( )
491+ . map( |( i, d) | Leaf :: new( 0x01 , vec![ 0x60 , d. wrapping_add( i as u8 ) ] , "" ) . unwrap( ) )
492+ . collect( ) ;
493+
494+ leaves = dedup_leaves( leaves) ;
495+ prop_assume!( leaves. len( ) >= 2 ) ;
496+
497+ let tree = MerkleTree :: new( leaves. clone( ) ) . unwrap( ) ;
498+ let root = tree. auth_root( ) ;
499+
500+ let proof_for_0 = tree. proof( 0 ) . unwrap( ) ;
501+ let leaf_hash_0 = leaves[ 0 ] . hash( ) ;
502+ let leaf_hash_1 = leaves[ 1 ] . hash( ) ;
503+
504+ // Correct leaf hash verifies
505+ prop_assert!( MerkleTree :: verify( & leaf_hash_0, & proof_for_0, & root) . unwrap( ) ) ;
506+
507+ // Wrong leaf hash fails — leaf 1's hash does not belong at index 0's position
508+ prop_assert!( !MerkleTree :: verify( & leaf_hash_1, & proof_for_0, & root) . unwrap( ) ) ;
509+ }
510+
511+ /// Property: tampering with any sibling invalidates proof
512+ #[ test]
513+ fn prop_merkle_sibling_tamper_rejected(
514+ discriminants in prop:: collection:: vec( any:: <u8 >( ) , 2 ..8 ) ,
515+ tamper_byte in any:: <u8 >( )
516+ ) {
517+ let mut leaves: Vec <Leaf > = discriminants
518+ . into_iter( )
519+ . enumerate( )
520+ . map( |( i, d) | Leaf :: new( 0x01 , vec![ 0x60 , d. wrapping_add( i as u8 ) ] , "" ) . unwrap( ) )
521+ . collect( ) ;
522+ leaves = dedup_leaves( leaves) ;
523+ prop_assume!( leaves. len( ) >= 2 ) ;
524+
525+ let tree = MerkleTree :: new( leaves. clone( ) ) . unwrap( ) ;
526+ let root = tree. auth_root( ) ;
527+ let mut proof = tree. proof( 0 ) . unwrap( ) ;
528+ prop_assume!( !proof. siblings. is_empty( ) ) ;
529+
530+ // Tamper first sibling
531+ proof. siblings[ 0 ] [ 0 ] ^= tamper_byte | 0x01 ;
532+ let result = MerkleTree :: verify( & leaves[ 0 ] . hash( ) , & proof, & root) . unwrap( ) ;
533+ prop_assert!( !result, "Tampered sibling must fail verification" ) ;
534+ }
443535}
444536
445537// ── RotationRequest property tests ───────────────────────────────────────────
0 commit comments