fix: move reusable invariants into shared module

fuzz/fuzz_targets/fuzz_multi_block_state_sequence.rs

@@ -17,23 +17,28 @@
 //!
 //! # Invariants
 //!
+//! The following per-transaction invariants are checked via the shared framework
+//! ([`fuzz_props::invariants::assert_invariants`]) on every iteration:
+//!
+//! - **StateIsolationOnFailure** — balances unchanged on rejection.
+//! - **BalanceConservation** — total balance conserved on success.
+//! - **FailedTxNonceStability** — nonces unchanged on rejection.
+//!
+//! In addition, [`assert_replay_rejection`] is called on every successful
+//! transaction (per-block replay check).
+//!
+//! The following multi-block aggregate invariant is checked **after** the loop:
+//!
 //! 1. **LongRangeBalanceConservation** — the total balance of the original genesis
 //!    accounts is the same at the end of all N blocks as at the beginning.  Failed
 //!    transactions and successful transfers between genesis accounts both preserve
 //!    the total; only mint/burn bugs or token-inflation bugs would break it.
-//!
-//! 2. **FailedTxNonceStability** — when `execute_check_on_state` returns `Err` for
-//!    a transaction, every genesis account nonce must be identical to what it was
-//!    before that transaction was attempted.  Nonce mutations on failed txs would
-//!    allow a griefing attack that permanently burns the victim's account.
-//!
-//! 3. **PerBlockReplayRejection** — every transaction that succeeded in block B is
-//!    rejected when replayed in block B+1.  This is the same per-tx invariant as
-//!    in `fuzz_state_transition` but exercised cumulatively across a longer
-//!    sequence so that interactions between successive nonce increments are tested.
 
 use arbitrary::{Arbitrary, Unstructured};
 use fuzz_props::generators::{arb_fuzz_native_transfer, arbitrary_fuzz_state, arbitrary_transaction};
+use fuzz_props::invariants::{
+    BalanceSnapshot, InvariantCtx, NonceSnapshot, assert_invariants, assert_replay_rejection,
+};
 use libfuzzer_sys::fuzz_target;
 use nssa::V03State;
 
@@ -52,7 +57,7 @@ fuzz_target!(|data: &[u8]| {
 
     let mut state = V03State::new_with_genesis_accounts(&init_accs, vec![], 0);
 
-    // Record starting balances for the long-range conservation check (invariant 1).
+    // Record starting balances for the long-range conservation check.
     let starting_total: u128 = init_accs
         .iter()
         .map(|&(id, _)| state.get_account_by_id(id).balance)
@@ -78,57 +83,51 @@ fuzz_target!(|data: &[u8]| {
         let block_id: u64 = 1 + u64::from(i);
         let timestamp: u64 = u64::from(i) * 1000;
 
-        // Snapshot nonces before this transaction for the nonce-stability check.
+        // Build per-transaction snapshots for the shared invariant framework.
-        let nonces_before: Vec<nssa_core::account::Nonce> = init_accs
+        let balances_before = BalanceSnapshot(
-            .iter()
+            init_accs
-            .map(|&(id, _)| state.get_account_by_id(id).nonce)
+                .iter()
-            .collect();
+                .map(|&(id, _)| (id, state.get_account_by_id(id).balance))
+                .collect(),
+        );
+        let nonces_before = NonceSnapshot(
+            init_accs
+                .iter()
+                .map(|&(id, _)| (id, state.get_account_by_id(id).nonce))
+                .collect(),
+        );
+        let state_snapshot = state.clone();
 
         let result = tx.execute_check_on_state(&mut state, block_id, timestamp);
+        let execution_succeeded = result.is_ok();
 
-        match result {
+        // ── Shared invariant checks ───────────────────────────────────────────
-            Err(_) => {
+        // Asserts per-transaction:
-                // ── Invariant 2: FailedTxNonceStability ──────────────────────
+        //   • StateIsolationOnFailure  — balances unchanged on rejection
-                for (k, &(acc_id, _)) in init_accs.iter().enumerate() {
+        //   • BalanceConservation      — total balance conserved on success
-                    let nonce_after = state.get_account_by_id(acc_id).nonce;
+        //   • FailedTxNonceStability   — nonces unchanged on rejection
-                    assert_eq!(
+        assert_invariants(&InvariantCtx {
-                        nonces_before[k],
+            state_before: &state_snapshot,
-                        nonce_after,
+            state_after: &state,
-                        "INVARIANT VIOLATION [FailedTxNonceStability]: \
+            execution_succeeded,
-                         nonce changed for account {:?} after a REJECTED transaction \
+            balances_before,
-                         in block {} (nonce before={:?}, nonce after={:?})",
+            nonces_before,
-                        acc_id,
+        });
-                        block_id,
+
-                        nonces_before[k],
+        // ── ReplayRejection (per-block) ───────────────────────────────────────
-                        nonce_after,
+        // execute_check_on_state returns the NSSATransaction on Ok; replay it
-                    );
+        // immediately in the next block and assert it is rejected (nonce consumed).
-                }
+        if let Ok(applied_tx) = result {
-            }
+            assert_replay_rejection(applied_tx, &mut state, block_id + 1, timestamp + 1);
-            Ok(applied_tx) => {
-                // ── Invariant 3: PerBlockReplayRejection ─────────────────────
-                let replay_result = applied_tx.execute_check_on_state(
-                    &mut state,
-                    block_id + 1,
-                    timestamp + 1,
-                );
-                assert!(
-                    replay_result.is_err(),
-                    "INVARIANT VIOLATION [PerBlockReplayRejection]: \
-                     a transaction accepted in block {} was accepted again in block {} \
-                     — nonce was not consumed",
-                    block_id,
-                    block_id + 1,
-                );
-            }
         }
     }
 
-    // ── Invariant 1: LongRangeBalanceConservation ─────────────────────────────
+    // ── LongRangeBalanceConservation ──────────────────────────────────────────
     // After all N blocks, the total balance of genesis accounts must equal the
     // starting total.  Successful transfers between genesis accounts cancel out;
-    // failed transactions must not mutate balances (covered by
+    // failed transactions must not mutate balances (covered per-tx by
-    // fuzz_state_transition's StateIsolationOnFailure, but we also verify the
+    // StateIsolationOnFailure above, verified cumulatively here to catch
-    // cumulative result here to catch interactions).
+    // interactions across the full sequence).
     let ending_total: u128 = init_accs
         .iter()
         .map(|&(id, _)| state.get_account_by_id(id).balance)

fuzz/fuzz_targets/fuzz_replay_prevention.rs

@@ -11,9 +11,22 @@
 //! testnet genesis) so that nonce-dependent edge cases — e.g. replay prevention
 //! at nonce 0, nonce `u128::MAX`, or when the sender has zero balance — are
 //! reachable by the fuzzer.
+//!
+//! # Invariants checked
+//!
+//! The shared framework ([`assert_invariants`]) enforces per-transaction:
+//! - **StateIsolationOnFailure** — balances unchanged on rejection
+//! - **BalanceConservation** — total balance conserved on success
+//! - **FailedTxNonceStability** — nonces unchanged on rejection
+//!
+//! The dedicated [`assert_replay_rejection`] function enforces:
+//! - **ReplayRejection** — accepted tx rejected on replay
 
 use arbitrary::{Arbitrary, Unstructured};
 use fuzz_props::generators::{arb_fuzz_native_transfer, arbitrary_fuzz_state, arbitrary_transaction};
+use fuzz_props::invariants::{
+    BalanceSnapshot, InvariantCtx, NonceSnapshot, assert_invariants, assert_replay_rejection,
+};
 use libfuzzer_sys::fuzz_target;
 use nssa::V03State;
 
@@ -45,15 +58,42 @@ fuzz_target!(|data: &[u8]| {
     // Stateless gate: skip structurally malformed transactions.
     let Ok(tx) = tx.transaction_stateless_check() else { return; };
 
+    // Build snapshots before execution.
+    let balances_before = BalanceSnapshot(
+        init_accs
+            .iter()
+            .map(|&(id, _)| (id, state.get_account_by_id(id).balance))
+            .collect(),
+    );
+    let nonces_before = NonceSnapshot(
+        init_accs
+            .iter()
+            .map(|&(id, _)| (id, state.get_account_by_id(id).nonce))
+            .collect(),
+    );
+    let state_snapshot = state.clone();
+
     // First application — may legitimately fail for state-level reasons.
     let result = tx.execute_check_on_state(&mut state, 1, 0);
+    let execution_succeeded = result.is_ok();
 
-    if let Ok(tx) = result {
+    // ── Shared invariant checks ───────────────────────────────────────────────
-        // tx is returned on success; try applying the identical transaction again.
+    // Asserts:
-        let result2 = tx.execute_check_on_state(&mut state, 2, 1);
+    //   • StateIsolationOnFailure  — balances unchanged on rejection
-        assert!(
+    //   • BalanceConservation      — total balance conserved on success
-            result2.is_err(),
+    //   • FailedTxNonceStability   — nonces unchanged on rejection
-            "INVARIANT VIOLATION: transaction accepted a second time — nonce replay not prevented"
+    assert_invariants(&InvariantCtx {
-        );
+        state_before: &state_snapshot,
+        state_after: &state,
+        execution_succeeded,
+        balances_before,
+        nonces_before,
+    });
+
+    // ── ReplayRejection ───────────────────────────────────────────────────────
+    // tx is returned on success; assert that applying it again in the next block
+    // is rejected (nonce was consumed on first acceptance).
+    if let Ok(applied_tx) = result {
+        assert_replay_rejection(applied_tx, &mut state, 2, 1);
     }
 });

fuzz/fuzz_targets/fuzz_state_transition.rs

@@ -2,6 +2,9 @@
 
 use arbitrary::{Arbitrary, Unstructured};
 use fuzz_props::generators::{arb_fuzz_native_transfer, arbitrary_fuzz_state, arbitrary_transaction};
+use fuzz_props::invariants::{
+    BalanceSnapshot, InvariantCtx, NonceSnapshot, assert_invariants, assert_replay_rejection,
+};
 use libfuzzer_sys::fuzz_target;
 use nssa::V03State;
 
@@ -45,8 +48,20 @@ fuzz_target!(|data: &[u8]| {
             continue;
         };
 
-        // Clone state before to detect state leakage on failure
+        // Build snapshots from the live state before this transaction so that the
-        let state_snapshot = state.clone();
+        // shared invariant framework can check isolation and conservation.
+        let balances_before = BalanceSnapshot(
+            init_accs
+                .iter()
+                .map(|&(id, _)| (id, state.get_account_by_id(id).balance))
+                .collect(),
+        );
+        let nonces_before = NonceSnapshot(
+            init_accs
+                .iter()
+                .map(|&(id, _)| (id, state.get_account_by_id(id).nonce))
+                .collect(),
+        );
 
         // Advance block_id and timestamp each iteration so the state machine
         // sees a realistic monotonically-increasing context.  Using the same
@@ -54,61 +69,30 @@ fuzz_target!(|data: &[u8]| {
         // when the block context changes across a multi-transaction sequence.
         let block_id: u64 = 1 + u64::from(i);
         let timestamp: u64 = u64::from(i);
+
+        // Snapshot state before execution for isolation checks.
+        let state_snapshot = state.clone();
         let result = tx.execute_check_on_state(&mut state, block_id, timestamp);
+        let execution_succeeded = result.is_ok();
 
-        match result {
+        // ── Shared invariant checks ───────────────────────────────────────────
-            Err(_) => {
+        // Asserts:
-                // INVARIANT: StateIsolationOnFailure — a rejected tx must leave
+        //   • StateIsolationOnFailure  — balances unchanged on rejection
-                // public account balances unchanged.
+        //   • BalanceConservation      — total balance conserved on success
-                for &(acc_id, _) in &init_accs {
+        //   • FailedTxNonceStability   — nonces unchanged on rejection
-                    let bal_before = state_snapshot.get_account_by_id(acc_id).balance;
+        assert_invariants(&InvariantCtx {
-                    let bal_after = state.get_account_by_id(acc_id).balance;
+            state_before: &state_snapshot,
-                    assert_eq!(
+            state_after: &state,
-                        bal_before, bal_after,
+            execution_succeeded,
-                        "INVARIANT VIOLATION [StateIsolationOnFailure]: balance changed \
+            balances_before,
-                         despite tx rejection for account {:?}",
+            nonces_before,
-                        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!(
-                    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
+        // ── ReplayRejection ───────────────────────────────────────────────────
-                // acceptance; replaying the identical transaction in the very next
+        // execute_check_on_state returns the NSSATransaction on Ok; replay it
-                // block must be rejected.
+        // immediately in the next block and assert it is rejected.
-                // `execute_check_on_state` returns the `ValidatedTransaction` on
+        if let Ok(applied_tx) = result {
-                // success, so we can feed it back without re-validating.
+            assert_replay_rejection(applied_tx, &mut state, block_id + 1, timestamp + 1);
-                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,
-                );
-            }
         }
     }
 });

fuzz_props/src/invariants.rs

@@ -1,5 +1,6 @@
 use common::transaction::NSSATransaction;
-use nssa::{V03State, error::NssaError};
+use nssa::V03State;
+use nssa_core::account::Nonce;
 
 /// Snapshot of public account balances used for conservation checks.
 #[derive(Clone, Debug)]
@@ -12,21 +13,39 @@ impl BalanceSnapshot {
     }
 }
 
-/// Shared context threaded through every invariant check.
+/// Snapshot of account nonces captured before a transaction is applied.
+///
+/// Mirrors [`BalanceSnapshot`]: one entry per account that should remain
+/// stable on a failed transaction (`FailedTxNonceStability` invariant).
+#[derive(Clone, Debug)]
+pub struct NonceSnapshot(pub std::collections::HashMap<nssa::AccountId, Nonce>);
+
+/// Shared context threaded through every per-transaction invariant check.
+///
+/// Build this **after** calling `execute_check_on_state` so that `state_after`
+/// reflects the post-execution state and `execution_succeeded` matches the
+/// actual outcome.
 pub struct InvariantCtx<'a> {
+    /// State snapshot captured **before** applying the transaction.
     pub state_before: &'a V03State,
+    /// Live state **after** applying (or attempting) the transaction.
     pub state_after: &'a V03State,
-    pub tx: &'a NSSATransaction,
+    /// `true` when `execute_check_on_state` returned `Ok`, `false` on `Err`.
-    pub result: &'a Result<(), NssaError>,
+    pub execution_succeeded: bool,
+    /// Per-account balances captured before the transaction.
     pub balances_before: BalanceSnapshot,
+    /// Per-account nonces captured before the transaction.
+    pub nonces_before: NonceSnapshot,
 }
 
+/// A named invariant violation with an actionable diagnostic message.
 #[derive(Debug)]
 pub struct InvariantViolation {
     pub invariant: &'static str,
     pub message: String,
 }
 
+/// A protocol rule that can be checked against a single transaction's context.
 pub trait ProtocolInvariant {
     fn name(&self) -> &'static str;
     fn check(&self, ctx: &InvariantCtx<'_>) -> Option<InvariantViolation>;
@@ -35,6 +54,9 @@ pub trait ProtocolInvariant {
 // ── Concrete invariants ───────────────────────────────────────────────────────
 
 /// Sum of all public account balances must never change when a transaction is rejected.
+///
+/// A balance mutation on failure means the protocol leaks state on error paths —
+/// e.g., a debit that is not rolled back after a later validation failure.
 pub struct StateIsolationOnFailure;
 
 impl ProtocolInvariant for StateIsolationOnFailure {
@@ -43,14 +65,15 @@ impl ProtocolInvariant for StateIsolationOnFailure {
     }
 
     fn check(&self, ctx: &InvariantCtx<'_>) -> Option<InvariantViolation> {
-        if ctx.result.is_err() {
+        if !ctx.execution_succeeded {
             for (acc_id, &expected_balance) in &ctx.balances_before.0 {
                 let actual_balance = ctx.state_after.get_account_by_id(*acc_id).balance;
                 if actual_balance != expected_balance {
                     return Some(InvariantViolation {
                         invariant: self.name(),
                         message: format!(
-                            "balance changed despite tx rejection: account {:?} had {expected_balance} before, {actual_balance} after",
+                            "balance changed despite tx rejection: account {:?} had \
+                             {expected_balance} before, {actual_balance} after",
                             acc_id,
                         ),
                     });
@@ -61,7 +84,88 @@ impl ProtocolInvariant for StateIsolationOnFailure {
     }
 }
 
+/// Total balance of all known accounts must be conserved when a transaction succeeds.
+///
+/// Catches double-credit and token-inflation bugs: a transfer path that credits the
+/// recipient without debiting the sender would inflate the sum of all known balances.
+/// The check uses the same account set captured in [`BalanceSnapshot`] so that new
+/// accounts silently created by execution are NOT included (see known limitation
+/// in `fuzz_validate_execute_consistency`).
+pub struct BalanceConservation;
+
+impl ProtocolInvariant for BalanceConservation {
+    fn name(&self) -> &'static str {
+        "BalanceConservation"
+    }
+
+    fn check(&self, ctx: &InvariantCtx<'_>) -> Option<InvariantViolation> {
+        if ctx.execution_succeeded {
+            let total_before = ctx.balances_before.total();
+            let total_after: u128 = ctx
+                .balances_before
+                .0
+                .keys()
+                .map(|&id| ctx.state_after.get_account_by_id(id).balance)
+                .fold(0u128, u128::saturating_add);
+            if total_before != total_after {
+                return Some(InvariantViolation {
+                    invariant: self.name(),
+                    message: format!(
+                        "total balance of known accounts changed after successful transaction: \
+                         before={total_before}, after={total_after} \
+                         (possible double-credit or token-inflation bug)",
+                    ),
+                });
+            }
+        }
+        None
+    }
+}
+
+/// When a transaction is rejected, every account's nonce must remain unchanged.
+///
+/// A nonce mutation on a failed transaction constitutes a griefing attack: an
+/// adversary could force arbitrary transactions to fail and permanently burn the
+/// victim's nonce, rendering their account unusable.
+pub struct FailedTxNonceStability;
+
+impl ProtocolInvariant for FailedTxNonceStability {
+    fn name(&self) -> &'static str {
+        "FailedTxNonceStability"
+    }
+
+    fn check(&self, ctx: &InvariantCtx<'_>) -> Option<InvariantViolation> {
+        if !ctx.execution_succeeded {
+            for (&acc_id, expected_nonce) in &ctx.nonces_before.0 {
+                let actual_nonce = ctx.state_after.get_account_by_id(acc_id).nonce;
+                if actual_nonce != *expected_nonce {
+                    return Some(InvariantViolation {
+                        invariant: self.name(),
+                        message: format!(
+                            "nonce changed despite tx rejection: account {:?} nonce was \
+                             {:?} before, {:?} after \
+                             (griefing attack — victim nonce permanently burned on failed tx)",
+                            acc_id, expected_nonce, actual_nonce,
+                        ),
+                    });
+                }
+            }
+        }
+        None
+    }
+}
+
 /// A successfully accepted transaction must be rejected when replayed.
+///
+/// # Note
+///
+/// This invariant **cannot** be exercised through [`InvariantCtx`] alone because
+/// the replay check requires re-applying the `NSSATransaction` that was consumed
+/// by `execute_check_on_state`.  The `ProtocolInvariant` impl here is a registry
+/// placeholder only; it always returns `None`.
+///
+/// Use the standalone [`assert_replay_rejection`] function instead, which accepts
+/// the `NSSATransaction` returned on success and performs the replay inline.
 pub struct ReplayRejection;
 
 impl ProtocolInvariant for ReplayRejection {
@@ -70,25 +174,69 @@ impl ProtocolInvariant for ReplayRejection {
     }
 
     fn check(&self, _ctx: &InvariantCtx<'_>) -> Option<InvariantViolation> {
-        // ReplayRejection cannot be fully exercised through InvariantCtx alone,
+        // ReplayRejection cannot be fully exercised through InvariantCtx alone.
-        // because the check requires *re-applying* the same ValidatedTransaction
+        // Use `assert_replay_rejection(applied_tx, state, next_block_id, next_ts)` instead.
-        // 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
     }
 }
 
-/// Run every registered invariant and panic with a structured message on first violation.
+// ── Standalone helpers ────────────────────────────────────────────────────────
+
+/// Assert that a successfully-applied transaction is **rejected** when replayed.
+///
+/// Call this immediately after `execute_check_on_state` returns `Ok(applied_tx)`,
+/// passing `applied_tx` as the first argument.  The transaction is re-applied to
+/// `state` at `next_block_id` / `next_timestamp`; if it is accepted a second time
+/// the function panics with a structured `INVARIANT VIOLATION [ReplayRejection]`
+/// message.
+///
+/// # Why a standalone function?
+///
+/// `execute_check_on_state` consumes the `NSSATransaction` and returns it on `Ok`,
+/// so the transaction is not available as a shared reference inside [`InvariantCtx`].
+/// This function accepts ownership of the returned transaction and performs the
+/// replay in-place.
+///
+/// # Example
+///
+/// ```rust,ignore
+/// let result = tx.execute_check_on_state(&mut state, block_id, timestamp);
+/// if let Ok(applied_tx) = result {
+///     assert_replay_rejection(applied_tx, &mut state, block_id + 1, timestamp + 1);
+/// }
+/// ```
+pub fn assert_replay_rejection(
+    applied_tx: NSSATransaction,
+    state: &mut V03State,
+    next_block_id: u64,
+    next_timestamp: u64,
+) {
+    let replay = applied_tx.execute_check_on_state(state, next_block_id, next_timestamp);
+    assert!(
+        replay.is_err(),
+        "INVARIANT VIOLATION [ReplayRejection]: transaction accepted a second time — \
+         nonce replay not prevented (replay block_id={next_block_id}, \
+         replay timestamp={next_timestamp})",
+    );
+}
+
+// ── Dispatcher ───────────────────────────────────────────────────────────────
+
+/// Run every registered [`ProtocolInvariant`] and panic with a structured message
+/// on the first violation.
+///
+/// Invariants checked:
+/// - [`StateIsolationOnFailure`] — balances unchanged on rejection
+/// - [`BalanceConservation`] — total balance conserved on success
+/// - [`FailedTxNonceStability`] — nonces unchanged on rejection
+/// - [`ReplayRejection`] — stub only; use [`assert_replay_rejection`] directly
 pub fn assert_invariants(ctx: &InvariantCtx<'_>) {
-    let invariants: &[&dyn ProtocolInvariant] = &[&StateIsolationOnFailure, &ReplayRejection];
+    let invariants: &[&dyn ProtocolInvariant] = &[
+        &StateIsolationOnFailure,
+        &BalanceConservation,
+        &FailedTxNonceStability,
+        &ReplayRejection,
+    ];
     for inv in invariants {
         if let Some(violation) = inv.check(ctx) {
             panic!(
@@ -100,13 +248,14 @@ pub fn assert_invariants(ctx: &InvariantCtx<'_>) {
     }
 }
 
+// ── Unit tests ────────────────────────────────────────────────────────────────
+
 #[cfg(test)]
 mod tests {
     use super::*;
     use nssa::V03State;
 
     fn make_empty_state() -> V03State {
-        //V03State::new_with_genesis_accounts(&[], &[])
         V03State::new_with_genesis_accounts(&[], vec![], 0)
     }
 
@@ -114,36 +263,89 @@ mod tests {
         BalanceSnapshot(std::collections::HashMap::new())
     }
 
+    fn make_empty_nonce_snapshot() -> NonceSnapshot {
+        NonceSnapshot(std::collections::HashMap::new())
+    }
+
     #[test]
     fn invariant_state_isolation_on_failure_does_not_panic_on_error() {
         let state = make_empty_state();
-        let tx = common::test_utils::produce_dummy_empty_transaction();
-        let result: Result<(), NssaError> = Err(NssaError::InvalidInput("test".to_owned()));
         let ctx = InvariantCtx {
             state_before: &state,
             state_after: &state,
-            tx: &tx,
+            execution_succeeded: false,
-            result: &result,
             balances_before: make_empty_snapshot(),
+            nonces_before: make_empty_nonce_snapshot(),
         };
-        // Should not panic — invariant check is a placeholder
         assert_invariants(&ctx);
     }
 
     #[test]
     fn invariant_replay_rejection_does_not_panic() {
         let state = make_empty_state();
-        let tx = common::test_utils::produce_dummy_empty_transaction();
-        let result: Result<(), NssaError> = Ok(());
         let ctx = InvariantCtx {
             state_before: &state,
             state_after: &state,
-            tx: &tx,
+            execution_succeeded: true,
-            result: &result,
             balances_before: make_empty_snapshot(),
+            nonces_before: make_empty_nonce_snapshot(),
         };
         assert_invariants(&ctx);
     }
+
+    #[test]
+    fn balance_conservation_catches_inflation_on_success() {
+        // Arrange: one account with balance 100.
+        let acc_id = nssa::AccountId::new([1u8; 32]);
+        let state_before = V03State::new_with_genesis_accounts(&[(acc_id, 100)], vec![], 0);
+        // Simulate execution that inflated the balance to 200.
+        let state_after = V03State::new_with_genesis_accounts(&[(acc_id, 200)], vec![], 0);
+
+        let mut balances = std::collections::HashMap::new();
+        balances.insert(acc_id, 100u128);
+
+        let ctx = InvariantCtx {
+            state_before: &state_before,
+            state_after: &state_after,
+            execution_succeeded: true,
+            balances_before: BalanceSnapshot(balances),
+            nonces_before: make_empty_nonce_snapshot(),
+        };
+
+        let result = std::panic::catch_unwind(|| assert_invariants(&ctx));
+        assert!(result.is_err(), "expected panic for balance inflation");
+    }
+
+    #[test]
+    fn failed_tx_nonce_stability_catches_nonce_mutation() {
+        let acc_id = nssa::AccountId::new([2u8; 32]);
+        // before: nonce 5; after: nonce 6 (should not happen on failure)
+        let state_before = V03State::new_with_genesis_accounts(&[(acc_id, 100)], vec![], 0);
+        let state_after = V03State::new_with_genesis_accounts(&[(acc_id, 100)], vec![], 0);
+
+        // We check the nonce snapshot directly; the states both return default nonce (0).
+        // Fake a discrepancy by inserting nonce=1 in the snapshot while state_after has nonce=0.
+        let mut nonces = std::collections::HashMap::new();
+        // Nonce(1) in snapshot, but state_after will return Nonce(0).
+        nonces.insert(acc_id, Nonce(1));
+
+        let mut balances = std::collections::HashMap::new();
+        balances.insert(acc_id, 100u128);
+
+        let ctx = InvariantCtx {
+            state_before: &state_before,
+            state_after: &state_after,
+            execution_succeeded: false,
+            balances_before: BalanceSnapshot(balances),
+            nonces_before: NonceSnapshot(nonces),
+        };
+
+        let result = std::panic::catch_unwind(|| assert_invariants(&ctx));
+        assert!(
+            result.is_err(),
+            "expected panic for nonce mutation on failure"
+        );
+    }
 }
 
 // ── ReplayRejection proptest suite ───────────────────────────────────────────
@@ -192,14 +394,10 @@ mod replay_proptest {
             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
+                // Use the shared framework function.  assert_replay_rejection uses
-                // immediately in the next block.
+                // assert!() rather than prop_assert!(); for structured proptest
-                let second_result = validated_tx.execute_check_on_state(&mut state, 2, 1);
+                // inputs the framework-level panic is equivalent.
-                prop_assert!(
+                super::assert_replay_rejection(validated_tx, &mut state, 2, 1);
-                    second_result.is_err(),
-                    "ReplayRejection violated: transaction accepted a second time (nonce \
-                     replay not prevented)"
-                );
             }
         }
     }