@@ -240,3 +240,121 @@ mod tests {
240240 }
241241 }
242242}
243+
244+ // ================================================================
245+ // Issue #500: insurance pool claim / reentrancy fuzzing
246+ // ================================================================
247+ #[ cfg( test) ]
248+ mod insurance_tests {
249+ use insurance_pool:: { InsuranceError , InsurancePool , InsurancePoolClient } ;
250+ use proptest:: prelude:: * ;
251+ use soroban_sdk:: { testutils:: Address as _, Address , Env } ;
252+
253+ const COVERAGE : i128 = 1_000_000_000 ;
254+
255+ struct InsFuzzEnv {
256+ env : Env ,
257+ client : InsurancePoolClient < ' static > ,
258+ }
259+
260+ fn setup_insurance ( ) -> InsFuzzEnv {
261+ let env = Env :: default ( ) ;
262+ env. mock_all_auths ( ) ;
263+
264+ let contract_id = env. register_contract ( None , InsurancePool ) ;
265+ let client = InsurancePoolClient :: new ( & env, & contract_id) ;
266+
267+ let admin = Address :: generate ( & env) ;
268+ client. initialize ( & admin, & COVERAGE ) ;
269+
270+ InsFuzzEnv { env, client }
271+ }
272+
273+ proptest ! {
274+ #![ proptest_config( ProptestConfig :: with_cases( 1000 ) ) ]
275+
276+ // claim must never panic-unwind for arbitrary invoice ids.
277+ // With an empty pool every claim must be rejected (PoolEmpty),
278+ // never silently succeed.
279+ #[ test]
280+ fn prop_claim_empty_pool_always_rejected( invoice_id in any:: <u64 >( ) ) {
281+ let t = setup_insurance( ) ;
282+
283+ // No premiums deposited => empty pool.
284+ prop_assert_eq!( t. client. get_pool_balance( ) , 0 ) ;
285+
286+ let res = t. client. try_claim( & invoice_id) ;
287+ // Empty pool must reject, not pay out.
288+ prop_assert_eq!(
289+ res,
290+ Err ( Ok ( soroban_sdk:: Error :: from( InsuranceError :: PoolEmpty ) ) )
291+ ) ;
292+ prop_assert!( !t. client. is_claimed( & invoice_id) ) ;
293+ }
294+
295+ // Double-claim rejection: a second claim for the same invoice id must
296+ // be rejected with AlreadyClaimed and must not pay out or drain the
297+ // pool a second time (reentrancy / double-spend guard).
298+ #[ test]
299+ fn prop_double_claim_rejected(
300+ invoice_id in any:: <u64 >( ) ,
301+ premium in 1i128 ..1_000_000_000_000i128 ,
302+ ) {
303+ let t = setup_insurance( ) ;
304+ let lp = Address :: generate( & t. env) ;
305+
306+ // Fund the pool so the first claim can pay out.
307+ t. client. deposit_premium( & lp, & premium) ;
308+ let balance_before = t. client. get_pool_balance( ) ;
309+
310+ // First claim succeeds and marks the invoice claimed.
311+ let first = t. client. claim( & invoice_id) ;
312+ prop_assert!( first > 0 ) ;
313+ prop_assert!( t. client. is_claimed( & invoice_id) ) ;
314+
315+ let balance_after_first = t. client. get_pool_balance( ) ;
316+ prop_assert_eq!( balance_after_first, balance_before - first) ;
317+
318+ // Second claim for the same invoice must be rejected.
319+ let second = t. client. try_claim( & invoice_id) ;
320+ prop_assert_eq!(
321+ second,
322+ Err ( Ok ( soroban_sdk:: Error :: from( InsuranceError :: AlreadyClaimed ) ) )
323+ ) ;
324+
325+ // Balance must be unchanged by the rejected double-claim.
326+ prop_assert_eq!( t. client. get_pool_balance( ) , balance_after_first) ;
327+ }
328+
329+ // General robustness: an interleaved sequence of claims across random
330+ // invoice ids never panics and never double-pays the same id.
331+ #[ test]
332+ fn prop_claim_sequence_never_double_pays(
333+ ids in prop:: collection:: vec( any:: <u64 >( ) , 1 ..8 ) ,
334+ premium in 1i128 ..1_000_000_000_000i128 ,
335+ ) {
336+ let t = setup_insurance( ) ;
337+ let lp = Address :: generate( & t. env) ;
338+ t. client. deposit_premium( & lp, & premium) ;
339+
340+ for id in ids. iter( ) {
341+ let already = t. client. is_claimed( id) ;
342+ let res = t. client. try_claim( id) ;
343+ if already {
344+ // A repeated id in the sequence must be rejected.
345+ prop_assert_eq!(
346+ res,
347+ Err ( Ok ( soroban_sdk:: Error :: from( InsuranceError :: AlreadyClaimed ) ) )
348+ ) ;
349+ } else {
350+ // Either paid (Ok) or rejected because the pool drained
351+ // (PoolEmpty) — never a panic-unwind.
352+ match res {
353+ Ok ( _) => prop_assert!( t. client. is_claimed( id) ) ,
354+ Err ( _) => { }
355+ }
356+ }
357+ }
358+ }
359+ }
360+ }
0 commit comments