diff --git a/fuzz/fuzz_targets/fuzz_state_transition.rs b/fuzz/fuzz_targets/fuzz_state_transition.rs index 8ae0825..e40f9c8 100644 --- a/fuzz/fuzz_targets/fuzz_state_transition.rs +++ b/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)", - ); } } }); diff --git a/fuzz_props/src/invariants.rs b/fuzz_props/src/invariants.rs index 7ea34e9..e949058 100644 --- a/fuzz_props/src/invariants.rs +++ b/fuzz_props/src/invariants.rs @@ -70,7 +70,18 @@ impl ProtocolInvariant for ReplayRejection { } fn check(&self, _ctx: &InvariantCtx<'_>) -> Option { - // 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)" + ); + } + } + } +}