fix: improved replay rejection detection

fuzz/fuzz_targets/fuzz_state_transition.rs

@@ -56,37 +56,59 @@ fuzz_target!(|data: &[u8]| {
         let timestamp: u64 = u64::from(i);
         let result = tx.execute_check_on_state(&mut state, block_id, timestamp);
 
-        if result.is_err() {
-            // INVARIANT: a rejected tx must leave public account balances unchanged
-            for &(acc_id, _) in &init_accs {
-                let bal_before = state_snapshot.get_account_by_id(acc_id).balance;
-                let bal_after = state.get_account_by_id(acc_id).balance;
+        match result {
+            Err(_) => {
+                // INVARIANT: StateIsolationOnFailure — a rejected tx must leave
+                // public account balances unchanged.
+                for &(acc_id, _) in &init_accs {
+                    let bal_before = state_snapshot.get_account_by_id(acc_id).balance;
+                    let bal_after = state.get_account_by_id(acc_id).balance;
+                    assert_eq!(
+                        bal_before, bal_after,
+                        "INVARIANT VIOLATION [StateIsolationOnFailure]: balance changed \
+                         despite tx rejection for account {:?}",
+                        acc_id
+                    );
+                }
+            }
+            Ok(applied_tx) => {
+                // INVARIANT: BalanceConservation — total balance of known accounts
+                // must be conserved on success.  Catches double-credit and
+                // token-inflation bugs — two transfer paths that each credit the
+                // recipient without debiting the sender would inflate the total, but
+                // neither the rejection check nor any other per-account check catches
+                // it unless we compare the aggregate.
+                let total_before: u128 = init_accs
+                    .iter()
+                    .map(|&(acc_id, _)| state_snapshot.get_account_by_id(acc_id).balance)
+                    .fold(0u128, u128::saturating_add);
+                let total_after: u128 = init_accs
+                    .iter()
+                    .map(|&(acc_id, _)| state.get_account_by_id(acc_id).balance)
+                    .fold(0u128, u128::saturating_add);
                 assert_eq!(
-                    bal_before, bal_after,
-                    "INVARIANT VIOLATION: balance changed despite tx rejection for account {:?}",
-                    acc_id
+                    total_before,
+                    total_after,
+                    "INVARIANT VIOLATION [BalanceConservation]: total balance of genesis \
+                     accounts changed after successful transaction (double-credit / \
+                     token-inflation bug)",
+                );
+
+                // INVARIANT: ReplayRejection — the nonce is consumed on first
+                // acceptance; replaying the identical transaction in the very next
+                // block must be rejected.
+                // `execute_check_on_state` returns the `ValidatedTransaction` on
+                // success, so we can feed it back without re-validating.
+                let replay_result =
+                    applied_tx.execute_check_on_state(&mut state, block_id + 1, timestamp + 1);
+                assert!(
+                    replay_result.is_err(),
+                    "INVARIANT VIOLATION [ReplayRejection]: transaction accepted twice — \
+                     nonce replay not prevented (first block_id={block_id}, replay \
+                     block_id={})",
+                    block_id + 1,
                 );
             }
-        } else {
-            // INVARIANT: total balance of known accounts must be conserved on success.
-            // Catches double-credit and token-inflation bugs — two transfer paths that
-            // each credit the recipient without debiting the sender would inflate the
-            // total, but neither the rejection check nor any other per-account check
-            // catches it unless we compare the aggregate.
-            let total_before: u128 = init_accs
-                .iter()
-                .map(|&(acc_id, _)| state_snapshot.get_account_by_id(acc_id).balance)
-                .fold(0u128, u128::saturating_add);
-            let total_after: u128 = init_accs
-                .iter()
-                .map(|&(acc_id, _)| state.get_account_by_id(acc_id).balance)
-                .fold(0u128, u128::saturating_add);
-            assert_eq!(
-                total_before,
-                total_after,
-                "INVARIANT VIOLATION: total balance of genesis accounts changed after successful \
-                 transaction (possible double-credit or token-inflation bug)",
-            );
         }
     }
 });

fuzz_props/src/invariants.rs

@@ -70,7 +70,18 @@ impl ProtocolInvariant for ReplayRejection {
     }
 
     fn check(&self, _ctx: &InvariantCtx<'_>) -> Option<InvariantViolation> {
-        // Implemented at the generator level in proptest (see generators.rs)
+        // ReplayRejection cannot be fully exercised through InvariantCtx alone,
+        // because the check requires *re-applying* the same ValidatedTransaction
+        // to the post-execution state.  InvariantCtx holds `tx: &NSSATransaction`,
+        // and `transaction_stateless_check()` consumes `self`, so re-validation
+        // from a shared reference is not possible.
+        //
+        // The invariant is enforced in two complementary ways instead:
+        //   1. `fuzz_state_transition.rs` — captures the `ValidatedTransaction`
+        //      returned on `Ok` by `execute_check_on_state` and immediately
+        //      re-applies it at block_id+1; asserts the replay is rejected.
+        //   2. The proptest suite in this module (`replay_rejection_proptest`)
+        //      exercises the same property with structured, reproducible inputs.
         None
     }
 }
@@ -134,3 +145,62 @@ mod tests {
         assert_invariants(&ctx);
     }
 }
+
+// ── ReplayRejection proptest suite ───────────────────────────────────────────
+//
+// This suite constitutes the formal, reproducible exercise of the ReplayRejection
+// invariant.  It generates a realistic initial state and a correctly-signed
+// native-transfer transaction, applies it once, and asserts that a second
+// application is rejected.
+//
+// Run with: cargo test -p fuzz_props replay_rejection
+#[cfg(test)]
+mod replay_proptest {
+    use crate::generators::{arb_native_transfer_tx, test_accounts};
+    use nssa::V03State;
+    use proptest::prelude::*;
+
+    /// Build a `V03State` from the testnet accounts, assigning each a fixed
+    /// balance large enough for any reasonable transfer amount.
+    fn make_test_state() -> V03State {
+        let accounts = test_accounts();
+        let init_accs: Vec<(nssa::AccountId, u128)> = accounts
+            .iter()
+            .map(|(id, _)| (*id, 1_000_000u128))
+            .collect();
+        V03State::new_with_genesis_accounts(&init_accs, vec![], 0)
+    }
+
+    proptest! {
+        /// **ReplayRejection** — a transaction accepted in block N must be
+        /// rejected when replayed in block N+1, because the nonce is consumed
+        /// on first acceptance.
+        #[test]
+        fn replay_rejection_proptest(tx in arb_native_transfer_tx(test_accounts())) {
+            let mut state = make_test_state();
+
+            // Stateless gate — skip structurally invalid transactions (e.g. those
+            // whose public key does not match the declared sender).
+            let validated_tx = match tx.transaction_stateless_check() {
+                Ok(v) => v,
+                Err(_) => return Ok(()),
+            };
+
+            // First application — may fail for state-level reasons (e.g. sender
+            // has insufficient balance, wrong nonce).  In that case there is
+            // nothing to replay.
+            let first_result = validated_tx.execute_check_on_state(&mut state, 1, 0);
+
+            if let Ok(validated_tx) = first_result {
+                // The same ValidatedTransaction is returned on Ok; replay it
+                // immediately in the next block.
+                let second_result = validated_tx.execute_check_on_state(&mut state, 2, 1);
+                prop_assert!(
+                    second_result.is_err(),
+                    "ReplayRejection violated: transaction accepted a second time (nonce \
+                     replay not prevented)"
+                );
+            }
+        }
+    }
+}