using FsCheck;
using FsCheck.Xunit;
using Microsoft.EntityFrameworkCore;
using Microsoft.Extensions.Logging;
using MiAssessment.Core.Interfaces;
using MiAssessment.Core.Services;
using MiAssessment.Model.Data;
using MiAssessment.Model.Entities;
using Moq;
using Xunit;

namespace MiAssessment.Tests.Services;

/// <summary>
/// InviteService 属性测试
/// 验证分销服务的分页查询一致性
/// </summary>
public class InviteServicePropertyTests
{
    private readonly Mock<ILogger<InviteService>> _mockLogger = new();
    private readonly Mock<IWechatService> _mockWechatService = new();

    #region Property 3: 分页查询一致性 - GetRecordListAsync

    /// <summary>
    /// Property 3: 邀请记录分页查询返回的记录数不超过pageSize
    /// *For any* paginated query, the returned items count SHALL not exceed pageSize.
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool RecordListPaginationReturnsCorrectCount(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        var pageSize = Math.Max(1, seed.Get % 20 + 1); // 1-20

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建多个下级用户（超过pageSize）
        var invitedUserCount = pageSize + 10;
        for (int i = 0; i < invitedUserCount; i++)
        {
            var invitedUser = CreateUser(userId + 1000 + i, seed.Get + 1000 + i);
            invitedUser.Pid = (int)userId; // 设置为当前用户的下级
            dbContext.Users.Add(invitedUser);
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.GetRecordListAsync(userId, 1, pageSize).GetAwaiter().GetResult();

        // Assert: 返回的记录数不超过pageSize
        return result.List.Count <= pageSize;
    }

    /// <summary>
    /// Property 3: 邀请记录分页查询的Total等于满足条件的总记录数
    /// *For any* paginated query, Total SHALL equal the count of all matching records.
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool RecordListPaginationTotalEqualsMatchingRecordsCount(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        var otherUserId = (long)(seed.Get + 50000);

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建另一个用户
        var otherUser = CreateUser(otherUserId, seed.Get + 50000);
        dbContext.Users.Add(otherUser);

        // 为当前用户创建下级用户
        var userInvitedCount = Math.Max(1, seed.Get % 15 + 1); // 1-15
        for (int i = 0; i < userInvitedCount; i++)
        {
            var invitedUser = CreateUser(userId + 1000 + i, seed.Get + 1000 + i);
            invitedUser.Pid = (int)userId;
            dbContext.Users.Add(invitedUser);
        }

        // 为其他用户创建下级用户（不应计入Total）
        for (int i = 0; i < 5; i++)
        {
            var otherInvitedUser = CreateUser(otherUserId + 1000 + i, seed.Get + 60000 + i);
            otherInvitedUser.Pid = (int)otherUserId;
            dbContext.Users.Add(otherInvitedUser);
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.GetRecordListAsync(userId, 1, 20).GetAwaiter().GetResult();

        // Assert: Total等于当前用户的下级用户数
        return result.Total == userInvitedCount;
    }

    /// <summary>
    /// Property 3: 遍历所有页面能获取所有满足条件的邀请记录
    /// *For any* paginated query, traversing all pages SHALL return all matching records.
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 50)]
    public bool RecordListPaginationTraversalReturnsAllRecords(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        var pageSize = Math.Max(1, seed.Get % 5 + 1); // 1-5 (小pageSize以测试多页)

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建下级用户
        var totalRecords = Math.Max(1, seed.Get % 12 + 1); // 1-12
        var expectedIds = new HashSet<long>();
        for (int i = 0; i < totalRecords; i++)
        {
            var invitedUser = CreateUser(userId + 1000 + i, seed.Get + 1000 + i);
            invitedUser.Pid = (int)userId;
            dbContext.Users.Add(invitedUser);
            expectedIds.Add(invitedUser.Id);
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act: 遍历所有页面
        var allRetrievedIds = new HashSet<long>();
        var page = 1;
        var maxPages = (totalRecords / pageSize) + 2; // 防止无限循环

        while (page <= maxPages)
        {
            var result = service.GetRecordListAsync(userId, page, pageSize).GetAwaiter().GetResult();
            if (result.List.Count == 0) break;

            foreach (var item in result.List)
            {
                allRetrievedIds.Add(item.UserId);
            }

            if (page >= result.TotalPages) break;
            page++;
        }

        // Assert: 遍历所有页面后获取的记录ID集合应等于预期的ID集合
        return allRetrievedIds.SetEquals(expectedIds);
    }

    /// <summary>
    /// Property 3: 邀请记录分页查询的TotalPages计算正确
    /// *For any* paginated query, TotalPages SHALL equal ceil(Total / PageSize).
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool RecordListPaginationTotalPagesCalculatedCorrectly(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        var pageSize = Math.Max(1, seed.Get % 20 + 1); // 1-20

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建下级用户
        var totalRecords = Math.Max(1, seed.Get % 50 + 1); // 1-50
        for (int i = 0; i < totalRecords; i++)
        {
            var invitedUser = CreateUser(userId + 1000 + i, seed.Get + 1000 + i);
            invitedUser.Pid = (int)userId;
            dbContext.Users.Add(invitedUser);
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.GetRecordListAsync(userId, 1, pageSize).GetAwaiter().GetResult();

        // Assert: TotalPages = ceil(Total / PageSize)
        var expectedTotalPages = (int)Math.Ceiling((double)result.Total / pageSize);
        return result.TotalPages == expectedTotalPages;
    }

    /// <summary>
    /// Property 3: 邀请记录分页查询不同页面返回不重复的记录
    /// *For any* paginated query, different pages SHALL return non-overlapping records.
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 50)]
    public bool RecordListPaginationPagesReturnNonOverlappingRecords(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        var pageSize = 3; // 固定pageSize以确保多页

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建足够多的下级用户以产生多页
        var totalRecords = 10;
        for (int i = 0; i < totalRecords; i++)
        {
            var invitedUser = CreateUser(userId + 1000 + i, seed.Get + 1000 + i);
            invitedUser.Pid = (int)userId;
            dbContext.Users.Add(invitedUser);
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act: 获取前两页
        var page1 = service.GetRecordListAsync(userId, 1, pageSize).GetAwaiter().GetResult();
        var page2 = service.GetRecordListAsync(userId, 2, pageSize).GetAwaiter().GetResult();

        // Assert: 两页的记录ID不重叠
        var page1Ids = page1.List.Select(r => r.UserId).ToHashSet();
        var page2Ids = page2.List.Select(r => r.UserId).ToHashSet();

        return !page1Ids.Intersect(page2Ids).Any();
    }

    #endregion

    #region Property 3: 分页查询一致性 - GetWithdrawListAsync

    /// <summary>
    /// Property 3: 提现记录分页查询返回的记录数不超过pageSize
    /// *For any* paginated query, the returned items count SHALL not exceed pageSize.
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool WithdrawListPaginationReturnsCorrectCount(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        var pageSize = Math.Max(1, seed.Get % 20 + 1); // 1-20

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建多条提现记录（超过pageSize）
        var withdrawalCount = pageSize + 10;
        for (int i = 0; i < withdrawalCount; i++)
        {
            dbContext.Withdrawals.Add(CreateWithdrawal(seed.Get + i, userId));
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.GetWithdrawListAsync(userId, 1, pageSize).GetAwaiter().GetResult();

        // Assert: 返回的记录数不超过pageSize
        return result.List.Count <= pageSize;
    }

    /// <summary>
    /// Property 3: 提现记录分页查询的Total等于满足条件的总记录数
    /// *For any* paginated query, Total SHALL equal the count of all matching records.
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool WithdrawListPaginationTotalEqualsMatchingRecordsCount(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        var otherUserId = (long)(seed.Get + 50000);

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建另一个用户
        var otherUser = CreateUser(otherUserId, seed.Get + 50000);
        dbContext.Users.Add(otherUser);

        // 为当前用户创建提现记录
        var userWithdrawalCount = Math.Max(1, seed.Get % 15 + 1); // 1-15
        for (int i = 0; i < userWithdrawalCount; i++)
        {
            dbContext.Withdrawals.Add(CreateWithdrawal(seed.Get + i, userId));
        }

        // 为其他用户创建提现记录（不应计入Total）
        for (int i = 0; i < 5; i++)
        {
            dbContext.Withdrawals.Add(CreateWithdrawal(seed.Get + 1000 + i, otherUserId));
        }

        // 创建已删除的提现记录（不应计入Total）
        for (int i = 0; i < 3; i++)
        {
            var deletedWithdrawal = CreateWithdrawal(seed.Get + 2000 + i, userId);
            deletedWithdrawal.IsDeleted = true;
            dbContext.Withdrawals.Add(deletedWithdrawal);
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.GetWithdrawListAsync(userId, 1, 20).GetAwaiter().GetResult();

        // Assert: Total等于当前用户未删除的提现记录数
        return result.Total == userWithdrawalCount;
    }

    /// <summary>
    /// Property 3: 遍历所有页面能获取所有满足条件的提现记录
    /// *For any* paginated query, traversing all pages SHALL return all matching records.
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 50)]
    public bool WithdrawListPaginationTraversalReturnsAllRecords(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        var pageSize = Math.Max(1, seed.Get % 5 + 1); // 1-5 (小pageSize以测试多页)

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建提现记录
        var totalRecords = Math.Max(1, seed.Get % 12 + 1); // 1-12
        var expectedIds = new HashSet<long>();
        for (int i = 0; i < totalRecords; i++)
        {
            var withdrawal = CreateWithdrawal(seed.Get + i, userId);
            dbContext.Withdrawals.Add(withdrawal);
            expectedIds.Add(withdrawal.Id);
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act: 遍历所有页面
        var allRetrievedIds = new HashSet<long>();
        var page = 1;
        var maxPages = (totalRecords / pageSize) + 2; // 防止无限循环

        while (page <= maxPages)
        {
            var result = service.GetWithdrawListAsync(userId, page, pageSize).GetAwaiter().GetResult();
            if (result.List.Count == 0) break;

            foreach (var item in result.List)
            {
                allRetrievedIds.Add(item.Id);
            }

            if (page >= result.TotalPages) break;
            page++;
        }

        // Assert: 遍历所有页面后获取的记录ID集合应等于预期的ID集合
        return allRetrievedIds.SetEquals(expectedIds);
    }

    /// <summary>
    /// Property 3: 提现记录分页查询的TotalPages计算正确
    /// *For any* paginated query, TotalPages SHALL equal ceil(Total / PageSize).
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool WithdrawListPaginationTotalPagesCalculatedCorrectly(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        var pageSize = Math.Max(1, seed.Get % 20 + 1); // 1-20

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建提现记录
        var totalRecords = Math.Max(1, seed.Get % 50 + 1); // 1-50
        for (int i = 0; i < totalRecords; i++)
        {
            dbContext.Withdrawals.Add(CreateWithdrawal(seed.Get + i, userId));
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.GetWithdrawListAsync(userId, 1, pageSize).GetAwaiter().GetResult();

        // Assert: TotalPages = ceil(Total / PageSize)
        var expectedTotalPages = (int)Math.Ceiling((double)result.Total / pageSize);
        return result.TotalPages == expectedTotalPages;
    }

    /// <summary>
    /// Property 3: 提现记录分页查询不同页面返回不重复的记录
    /// *For any* paginated query, different pages SHALL return non-overlapping records.
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 50)]
    public bool WithdrawListPaginationPagesReturnNonOverlappingRecords(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        var pageSize = 3; // 固定pageSize以确保多页

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建足够多的提现记录以产生多页
        var totalRecords = 10;
        for (int i = 0; i < totalRecords; i++)
        {
            dbContext.Withdrawals.Add(CreateWithdrawal(seed.Get + i, userId));
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act: 获取前两页
        var page1 = service.GetWithdrawListAsync(userId, 1, pageSize).GetAwaiter().GetResult();
        var page2 = service.GetWithdrawListAsync(userId, 2, pageSize).GetAwaiter().GetResult();

        // Assert: 两页的记录ID不重叠
        var page1Ids = page1.List.Select(r => r.Id).ToHashSet();
        var page2Ids = page2.List.Select(r => r.Id).ToHashSet();

        return !page1Ids.Intersect(page2Ids).Any();
    }

    /// <summary>
    /// Property 3: 提现记录分页查询不返回已删除的记录
    /// *For any* paginated query, deleted records (IsDeleted=true) SHALL not be returned.
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool WithdrawListPaginationExcludesDeletedRecords(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建正常的提现记录
        var normalWithdrawals = new List<Withdrawal>();
        for (int i = 0; i < 3; i++)
        {
            var withdrawal = CreateWithdrawal(seed.Get + i, userId);
            normalWithdrawals.Add(withdrawal);
            dbContext.Withdrawals.Add(withdrawal);
        }

        // 创建已删除的提现记录
        var deletedWithdrawals = new List<Withdrawal>();
        for (int i = 0; i < 2; i++)
        {
            var withdrawal = CreateWithdrawal(seed.Get + 100 + i, userId);
            withdrawal.IsDeleted = true;
            deletedWithdrawals.Add(withdrawal);
            dbContext.Withdrawals.Add(withdrawal);
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.GetWithdrawListAsync(userId, 1, 20).GetAwaiter().GetResult();

        // Assert: 
        // 1. 返回的记录数等于正常记录数
        if (result.List.Count != 3) return false;

        // 2. 返回的记录中不包含已删除的记录
        var returnedIds = result.List.Select(r => r.Id).ToHashSet();
        var deletedIds = deletedWithdrawals.Select(w => w.Id).ToHashSet();

        return !returnedIds.Intersect(deletedIds).Any();
    }

    #endregion

    #region 综合属性测试

    /// <summary>
    /// Property 3: 空数据库返回空列表 - 邀请记录
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Fact]
    public void EmptyDatabaseReturnsEmptyRecordList()
    {
        // Arrange
        using var dbContext = CreateDbContext();
        
        // 创建用户但没有下级
        var user = CreateUser(1, 1);
        dbContext.Users.Add(user);
        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.GetRecordListAsync(1, 1, 20).GetAwaiter().GetResult();

        // Assert
        Assert.Empty(result.List);
        Assert.Equal(0, result.Total);
    }

    /// <summary>
    /// Property 3: 空数据库返回空列表 - 提现记录
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Fact]
    public void EmptyDatabaseReturnsEmptyWithdrawList()
    {
        // Arrange
        using var dbContext = CreateDbContext();
        
        // 创建用户但没有提现记录
        var user = CreateUser(1, 1);
        dbContext.Users.Add(user);
        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.GetWithdrawListAsync(1, 1, 20).GetAwaiter().GetResult();

        // Assert
        Assert.Empty(result.List);
        Assert.Equal(0, result.Total);
    }

    /// <summary>
    /// Property 3: 分页参数边界值处理 - 邀请记录
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 50)]
    public bool RecordListHandlesBoundaryPageParameters(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建下级用户
        for (int i = 0; i < 5; i++)
        {
            var invitedUser = CreateUser(userId + 1000 + i, seed.Get + 1000 + i);
            invitedUser.Pid = (int)userId;
            dbContext.Users.Add(invitedUser);
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act: 测试边界值 - page=0 应该被处理为 page=1
        var result = service.GetRecordListAsync(userId, 0, 10).GetAwaiter().GetResult();

        // Assert: 应该返回第一页的数据
        return result.List.Count > 0 && result.Page == 1;
    }

    /// <summary>
    /// Property 3: 分页参数边界值处理 - 提现记录
    /// 
    /// **Feature: miniapp-api, Property 3: 分页查询一致性**
    /// **Validates: Requirements 12.1, 13.5**
    /// </summary>
    [Property(MaxTest = 50)]
    public bool WithdrawListHandlesBoundaryPageParameters(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;

        // 创建当前用户
        var currentUser = CreateUser(userId, seed.Get);
        dbContext.Users.Add(currentUser);

        // 创建提现记录
        for (int i = 0; i < 5; i++)
        {
            dbContext.Withdrawals.Add(CreateWithdrawal(seed.Get + i, userId));
        }

        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act: 测试边界值 - page=0 应该被处理为 page=1
        var result = service.GetWithdrawListAsync(userId, 0, 10).GetAwaiter().GetResult();

        // Assert: 应该返回第一页的数据
        return result.List.Count > 0 && result.Page == 1;
    }

    #endregion

    #region Property 7: 提现余额一致性

    /// <summary>
    /// Property 7: 提现成功后用户余额等于原余额减去提现金额
    /// *For any* successful withdrawal, user.Balance = originalBalance - withdrawalAmount.
    /// 
    /// **Feature: miniapp-api, Property 7: 提现余额一致性**
    /// **Validates: Requirements 13.1**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool WithdrawDeductsCorrectAmount(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        
        // 生成有效的提现金额（1-100的整数）
        var withdrawAmount = Math.Max(1, seed.Get % 100 + 1);
        // 确保余额大于提现金额
        var originalBalance = withdrawAmount + (seed.Get % 100) + 1;

        // 创建用户
        var user = CreateUser(userId, seed.Get);
        user.Balance = originalBalance;
        dbContext.Users.Add(user);
        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.ApplyWithdrawAsync(userId, withdrawAmount).GetAwaiter().GetResult();

        // Assert: 提现成功后，用户余额 = 原余额 - 提现金额
        if (!result.Success) return false;

        // 重新查询用户余额
        var updatedUser = dbContext.Users.Find((int)userId);
        if (updatedUser == null) return false;

        var expectedBalance = originalBalance - withdrawAmount;
        return updatedUser.Balance == expectedBalance;
    }

    /// <summary>
    /// Property 7: 提现记录的BeforeBalance和AfterBalance正确记录变化
    /// *For any* successful withdrawal, withdrawal record SHALL have correct BeforeBalance and AfterBalance.
    /// 
    /// **Feature: miniapp-api, Property 7: 提现余额一致性**
    /// **Validates: Requirements 13.1**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool WithdrawRecordHasCorrectBalanceFields(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        
        // 生成有效的提现金额（1-100的整数）
        var withdrawAmount = Math.Max(1, seed.Get % 100 + 1);
        // 确保余额大于提现金额
        var originalBalance = withdrawAmount + (seed.Get % 100) + 1;

        // 创建用户
        var user = CreateUser(userId, seed.Get);
        user.Balance = originalBalance;
        dbContext.Users.Add(user);
        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.ApplyWithdrawAsync(userId, withdrawAmount).GetAwaiter().GetResult();

        // Assert: 提现记录的BeforeBalance和AfterBalance正确
        if (!result.Success) return false;

        // 查询提现记录
        var withdrawal = dbContext.Withdrawals
            .FirstOrDefault(w => w.WithdrawalNo == result.WithdrawalNo);
        
        if (withdrawal == null) return false;

        // 验证BeforeBalance等于原余额
        if (withdrawal.BeforeBalance != originalBalance) return false;

        // 验证AfterBalance等于原余额减去提现金额
        var expectedAfterBalance = originalBalance - withdrawAmount;
        if (withdrawal.AfterBalance != expectedAfterBalance) return false;

        // 验证提现金额正确
        return withdrawal.Amount == withdrawAmount;
    }

    /// <summary>
    /// Property 7: 提现金额超过余额时提现失败
    /// *For any* withdrawal where amount > balance, withdrawal SHALL fail.
    /// 
    /// **Feature: miniapp-api, Property 7: 提现余额一致性**
    /// **Validates: Requirements 13.1**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool WithdrawFailsWhenAmountExceedsBalance(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        
        // 设置余额为1-50之间的整数
        var balance = Math.Max(1, seed.Get % 50 + 1);
        // 提现金额大于余额
        var withdrawAmount = balance + Math.Max(1, seed.Get % 100 + 1);

        // 创建用户
        var user = CreateUser(userId, seed.Get);
        user.Balance = balance;
        dbContext.Users.Add(user);
        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.ApplyWithdrawAsync(userId, withdrawAmount).GetAwaiter().GetResult();

        // Assert: 提现失败，且错误信息包含"超出待提现金额"
        if (result.Success) return false;
        if (string.IsNullOrEmpty(result.ErrorMessage)) return false;
        
        // 验证用户余额未变化
        var updatedUser = dbContext.Users.Find((int)userId);
        if (updatedUser == null) return false;

        return updatedUser.Balance == balance;
    }

    /// <summary>
    /// Property 7: 提现金额小于1元时提现失败
    /// *For any* withdrawal where amount < 1, withdrawal SHALL fail.
    /// 
    /// **Feature: miniapp-api, Property 7: 提现余额一致性**
    /// **Validates: Requirements 13.1**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool WithdrawFailsWhenAmountLessThanMinimum(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        
        // 设置足够的余额
        var balance = 100m + (seed.Get % 100);
        // 提现金额小于1元（0.01 - 0.99）
        var withdrawAmount = (seed.Get % 99 + 1) / 100m;

        // 创建用户
        var user = CreateUser(userId, seed.Get);
        user.Balance = balance;
        dbContext.Users.Add(user);
        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.ApplyWithdrawAsync(userId, withdrawAmount).GetAwaiter().GetResult();

        // Assert: 提现失败，且错误信息包含"不能小于1元"
        if (result.Success) return false;
        if (string.IsNullOrEmpty(result.ErrorMessage)) return false;
        if (!result.ErrorMessage.Contains("1元")) return false;
        
        // 验证用户余额未变化
        var updatedUser = dbContext.Users.Find((int)userId);
        if (updatedUser == null) return false;

        return updatedUser.Balance == balance;
    }

    /// <summary>
    /// Property 7: 提现金额不是整数时提现失败
    /// *For any* withdrawal where amount is not an integer, withdrawal SHALL fail.
    /// 
    /// **Feature: miniapp-api, Property 7: 提现余额一致性**
    /// **Validates: Requirements 13.1**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool WithdrawFailsWhenAmountIsNotInteger(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        
        // 设置足够的余额
        var balance = 100m + (seed.Get % 100);
        // 提现金额为非整数（1.01 - 99.99）
        var integerPart = Math.Max(1, seed.Get % 99 + 1);
        var decimalPart = (seed.Get % 99 + 1) / 100m;
        var withdrawAmount = integerPart + decimalPart;

        // 创建用户
        var user = CreateUser(userId, seed.Get);
        user.Balance = balance;
        dbContext.Users.Add(user);
        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.ApplyWithdrawAsync(userId, withdrawAmount).GetAwaiter().GetResult();

        // Assert: 提现失败，且错误信息包含"整数"
        if (result.Success) return false;
        if (string.IsNullOrEmpty(result.ErrorMessage)) return false;
        if (!result.ErrorMessage.Contains("整数")) return false;
        
        // 验证用户余额未变化
        var updatedUser = dbContext.Users.Find((int)userId);
        if (updatedUser == null) return false;

        return updatedUser.Balance == balance;
    }

    /// <summary>
    /// Property 7: 提现成功后创建提现记录
    /// *For any* successful withdrawal, a withdrawal record SHALL be created.
    /// 
    /// **Feature: miniapp-api, Property 7: 提现余额一致性**
    /// **Validates: Requirements 13.1**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool WithdrawCreatesWithdrawalRecord(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        
        // 生成有效的提现金额（1-100的整数）
        var withdrawAmount = Math.Max(1, seed.Get % 100 + 1);
        // 确保余额大于提现金额
        var originalBalance = withdrawAmount + (seed.Get % 100) + 1;

        // 创建用户
        var user = CreateUser(userId, seed.Get);
        user.Balance = originalBalance;
        dbContext.Users.Add(user);
        dbContext.SaveChanges();

        // 记录提现前的提现记录数
        var beforeCount = dbContext.Withdrawals.Count(w => w.UserId == userId);

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.ApplyWithdrawAsync(userId, withdrawAmount).GetAwaiter().GetResult();

        // Assert: 提现成功后，提现记录数增加1
        if (!result.Success) return false;

        var afterCount = dbContext.Withdrawals.Count(w => w.UserId == userId);
        return afterCount == beforeCount + 1;
    }

    /// <summary>
    /// Property 7: 提现失败时不创建提现记录且余额不变
    /// *For any* failed withdrawal, no withdrawal record SHALL be created and balance SHALL remain unchanged.
    /// 
    /// **Feature: miniapp-api, Property 7: 提现余额一致性**
    /// **Validates: Requirements 13.1**
    /// </summary>
    [Property(MaxTest = 100)]
    public bool FailedWithdrawDoesNotCreateRecordOrChangeBalance(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        
        // 设置余额
        var balance = 50m + (seed.Get % 50);
        // 提现金额超过余额（会失败）
        var withdrawAmount = balance + 100;

        // 创建用户
        var user = CreateUser(userId, seed.Get);
        user.Balance = balance;
        dbContext.Users.Add(user);
        dbContext.SaveChanges();

        // 记录提现前的提现记录数
        var beforeCount = dbContext.Withdrawals.Count(w => w.UserId == userId);

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act
        var result = service.ApplyWithdrawAsync(userId, withdrawAmount).GetAwaiter().GetResult();

        // Assert: 提现失败
        if (result.Success) return false;

        // 验证提现记录数未变化
        var afterCount = dbContext.Withdrawals.Count(w => w.UserId == userId);
        if (afterCount != beforeCount) return false;

        // 验证用户余额未变化
        var updatedUser = dbContext.Users.Find((int)userId);
        if (updatedUser == null) return false;

        return updatedUser.Balance == balance;
    }

    /// <summary>
    /// Property 7: 多次提现后余额累计正确
    /// *For any* multiple successful withdrawals, final balance SHALL equal original balance minus sum of all withdrawals.
    /// 
    /// **Feature: miniapp-api, Property 7: 提现余额一致性**
    /// **Validates: Requirements 13.1**
    /// </summary>
    [Property(MaxTest = 50)]
    public bool MultipleWithdrawalsDeductCorrectly(PositiveInt seed)
    {
        // Arrange
        using var dbContext = CreateDbContext();
        var userId = (long)seed.Get;
        
        // 设置较大的初始余额
        var originalBalance = 500m + (seed.Get % 500);
        
        // 创建用户
        var user = CreateUser(userId, seed.Get);
        user.Balance = originalBalance;
        dbContext.Users.Add(user);
        dbContext.SaveChanges();

        var service = new InviteService(dbContext, _mockLogger.Object, _mockWechatService.Object);

        // Act: 进行多次提现
        var withdrawAmounts = new List<decimal>();
        var withdrawCount = Math.Max(1, seed.Get % 3 + 1); // 1-3次提现
        
        for (int i = 0; i < withdrawCount; i++)
        {
            // 每次提现1-50元的整数
            var amount = Math.Max(1, (seed.Get + i * 17) % 50 + 1);
            var result = service.ApplyWithdrawAsync(userId, amount).GetAwaiter().GetResult();
            if (result.Success)
            {
                withdrawAmounts.Add(amount);
            }
        }

        // Assert: 最终余额 = 原余额 - 所有成功提现金额之和
        var totalWithdrawn = withdrawAmounts.Sum();
        var expectedBalance = originalBalance - totalWithdrawn;

        var updatedUser = dbContext.Users.Find((int)userId);
        if (updatedUser == null) return false;

        return updatedUser.Balance == expectedBalance;
    }

    #endregion

    #region 辅助方法

    /// <summary>
    /// 创建内存数据库上下文
    /// </summary>
    private MiAssessmentDbContext CreateDbContext()
    {
        var options = new DbContextOptionsBuilder<MiAssessmentDbContext>()
            .UseInMemoryDatabase(databaseName: Guid.NewGuid().ToString())
            .ConfigureWarnings(w => w.Ignore(Microsoft.EntityFrameworkCore.Diagnostics.InMemoryEventId.TransactionIgnoredWarning))
            .Options;

        return new MiAssessmentDbContext(options);
    }

    /// <summary>
    /// 创建测试用户
    /// </summary>
    private User CreateUser(long id, int seed)
    {
        return new User
        {
            Id = (int)id,
            OpenId = $"openid_{seed}",
            Uid = $"UID{seed:D6}",
            Nickname = $"Test User {seed}",
            HeadImg = $"https://example.com/avatar_{seed}.jpg",
            InviteCode = $"INV{seed:D6}",
            Balance = 100.00m + (seed % 100),
            TotalIncome = 200.00m + (seed % 100),
            WithdrawnAmount = 50.00m + (seed % 50),
            Status = 1,
            Pid = 0,
            UserLevel = 1,
            CreatedAt = DateTime.Now.AddDays(-seed % 30),
            UpdatedAt = DateTime.Now
        };
    }

    /// <summary>
    /// 创建测试提现记录
    /// </summary>
    private Withdrawal CreateWithdrawal(int seed, long userId)
    {
        return new Withdrawal
        {
            Id = seed,
            WithdrawalNo = $"W{DateTime.Now:yyyyMMdd}{seed:D6}",
            UserId = userId,
            Amount = 10.00m + (seed % 100),
            BeforeBalance = 100.00m + (seed % 100),
            AfterBalance = 90.00m + (seed % 100),
            Status = (seed % 4) + 1, // 1-4
            CreateTime = DateTime.Now.AddDays(-seed % 30),
            UpdateTime = DateTime.Now,
            IsDeleted = false
        };
    }

    #endregion
}