bex-cloud-staking/bex-cloud-staking-service/src/test/java/com/bex/staking/engine/RaisedCapacityInvariantPropertyTest.java

package com.bex.staking.engine;

import static org.assertj.core.api.Assertions.assertThat;

import java.math.BigDecimal;
import java.util.List;
import net.jqwik.api.Arbitraries;
import net.jqwik.api.Arbitrary;
import net.jqwik.api.Combinators;
import net.jqwik.api.Example;
import net.jqwik.api.ForAll;
import net.jqwik.api.Property;
import net.jqwik.api.Provide;

/**
 * 募集上限不变量的属性测试（PBT，jqwik，Property 9）。
 *
 * <p>对应设计文档 Correctness Properties 的 Property 9「募集上限不变量」。
 *
 * <p>验证：对任意针对同一产品的下单序列，任意被接受的下单完成后，产品 {@code raisedAmount} 始终满足
 * {@code raisedAmount ≤ totalCapacity}；任何会导致超出上限的下单都被拒绝。
 *
 * <h2>被测逻辑与内存模型的对应关系</h2>
 *
 * <p>募集上限校验在 SQL 层完成，见 {@code StakingProductMapper.xml} 的 {@code increaseRaisedAmount}：
 *
 * <pre>{@code
 * UPDATE staking_product
 * SET raised_amount = raised_amount + #{amount}, version = version + 1
 * WHERE id = #{id} AND version = #{version} AND deleted = 0
 *   AND raised_amount + #{amount} <= total_capacity
 * }</pre>
 *
 * <p>该语句返回受影响行数：满足 {@code raised_amount + amount <= total_capacity} 时累加并返回 1（接受），
 * 否则不更新返回 0（拒绝）。{@code OrderEngine.confirmStake(...)} 据返回 0 抛出 {@code 40005}
 * （{@code StakingErrorCode.CAPACITY_EXCEEDED}）拒绝下单（见 OrderEngine 第 6 步）。
 *
 * <p>本属性测试以纯内存模型 {@link CapacityModel#tryRaise(BigDecimal)} 模拟该条件累加语义：当且仅当
 * {@code raised + amount ≤ totalCapacity} 时执行 {@code raised += amount} 并返回 {@code true}（对应 SQL 返回 1），
 * 否则保持 {@code raised} 不变并返回 {@code false}（对应 SQL 返回 0）。模型的判定条件与生产 SQL 的 WHERE 子句
 * {@code raised_amount + amount <= total_capacity} 完全对应，从而在不依赖数据库与 Spring 的前提下验证该不变量。
 *
 * <p>金额一律使用 {@link BigDecimal} 生成，并以 {@link BigDecimal#compareTo} 判定数值大小关系（忽略标度差异，
 * 对齐数据库 {@code DECIMAL(36,18)} 精度与生产代码内部判定方式）。
 *
 * <p>Validates: Requirements 5.7
 */
class RaisedCapacityInvariantPropertyTest {

    /** {@code DECIMAL(36,18)} 的最小单位（1e-18），用于「超出上限 1 单位」的边界用例。 */
    private static final BigDecimal ONE_UNIT = new BigDecimal("0.000000000000000001");

    // ==================== 内存模型（与 increaseRaisedAmount SQL 语义一致） ====================

    /**
     * 募集上限内存模型，模拟 {@code StakingProductMapper.xml} 的 {@code increaseRaisedAmount} 条件累加语义。
     *
     * <p>持有当前已募集金额 {@code raised} 与总募集上限 {@code totalCapacity}；{@link #tryRaise(BigDecimal)}
     * 等价于一次乐观锁累加 SQL 的执行结果。
     */
    static final class CapacityModel {

        /** 当前已募集金额（对应 staking_product.raised_amount）。 */
        private BigDecimal raised;

        /** 总募集上限（对应 staking_product.total_capacity），构造后不变。 */
        private final BigDecimal totalCapacity;

        CapacityModel(BigDecimal initialRaised, BigDecimal totalCapacity) {
            this.raised = initialRaised;
            this.totalCapacity = totalCapacity;
        }

        /**
         * 尝试累加一笔下单金额，模拟 increaseRaisedAmount 的 WHERE 条件
         * {@code raised_amount + amount <= total_capacity}。
         *
         * @param amount 本笔下单金额（正数）
         * @return 满足 {@code raised + amount ≤ totalCapacity} 时累加并返回 {@code true}（对应 SQL 返回 1，接受）；
         *     否则保持 {@code raised} 不变并返回 {@code false}（对应 SQL 返回 0，拒绝）
         */
        boolean tryRaise(BigDecimal amount) {
            if (raised.add(amount).compareTo(totalCapacity) <= 0) {
                raised = raised.add(amount);
                return true;
            }
            return false;
        }

        BigDecimal raised() {
            return raised;
        }

        BigDecimal totalCapacity() {
            return totalCapacity;
        }
    }

    /**
     * 下单序列场景：同一产品的总募集上限、起始已募集金额与一串下单金额序列。
     *
     * @param totalCapacity 总募集上限（正数）
     * @param initialRaised 起始已募集金额（{@code [0, totalCapacity]}，覆盖全新产品与已部分募集产品）
     * @param orderAmounts 针对同一产品的下单金额序列（每笔为正数）
     */
    record CapacityScenario(BigDecimal totalCapacity, BigDecimal initialRaised, List<BigDecimal> orderAmounts) {}

    // ==================== 生成器 ====================

    /** 正总募集上限 totalCapacity：[1, 1e9]，scale=18，覆盖整数与长尾小数。 */
    @Provide
    Arbitrary<BigDecimal> totalCapacity() {
        return Arbitraries.bigDecimals()
                .between(BigDecimal.ONE, new BigDecimal("1000000000"))
                .ofScale(18)
                .filter(v -> v.signum() > 0);
    }

    /**
     * 下单序列场景生成器。
     *
     * <p>先生成 {@code totalCapacity}，再据其构造：起始已募集金额 {@code initialRaised ∈ [0, totalCapacity]}；
     * 每笔下单金额 {@code ∈ (0, 2 × totalCapacity]}——上界达到上限的 2 倍，使序列同时覆盖「单笔即超过上限（立即拒绝）」
     * 与「单笔不超上限但多笔累加后超过剩余额度（后续拒绝）」两类输入；序列长度 1~40，保证接受与拒绝都被充分覆盖。
     */
    @Provide
    Arbitrary<CapacityScenario> scenarios() {
        return totalCapacity().flatMap(cap -> {
            Arbitrary<BigDecimal> initialRaised = Arbitraries.bigDecimals()
                    .between(BigDecimal.ZERO, cap)
                    .ofScale(18)
                    .filter(v -> v.signum() >= 0);
            Arbitrary<BigDecimal> amount = Arbitraries.bigDecimals()
                    .between(ONE_UNIT, cap.multiply(new BigDecimal("2")))
                    .ofScale(18)
                    .filter(v -> v.signum() > 0);
            return Combinators.combine(
                            initialRaised, amount.list().ofMinSize(1).ofMaxSize(40))
                    .as((init, amounts) -> new CapacityScenario(cap, init, amounts));
        });
    }

    // ==================== Property 9：募集上限不变量 ====================

    // Feature: staking-service, Property 9: 募集上限不变量
    // 对任意同一产品的下单序列逐笔 tryRaise（模拟 increaseRaisedAmount 的条件累加），验证：
    //   (1) 任意时刻 raised ≤ totalCapacity 恒成立（不变量）；
    //   (2) 每笔被接受 ⟺ 接受前 raised + amount ≤ totalCapacity；
    //   (3) 被拒绝的下单不改变 raised。
    // Validates: Requirements 5.7
    @Property(tries = 100)
    void raisedAmountNeverExceedsCapacityAndOverflowOrdersRejected(
            @ForAll("scenarios") CapacityScenario scenario) {
        CapacityModel model = new CapacityModel(scenario.initialRaised(), scenario.totalCapacity());

        // 初始不变量：起始 raised ≤ totalCapacity
        assertThat(model.raised().compareTo(model.totalCapacity()))
                .as("初始 raisedAmount 应满足 raisedAmount ≤ totalCapacity")
                .isLessThanOrEqualTo(0);

        for (BigDecimal amount : scenario.orderAmounts()) {
            BigDecimal beforeRaised = model.raised();
            // 接受前的判定条件，与 SQL WHERE 子句 raised_amount + amount <= total_capacity 完全对应
            boolean expectedAccept =
                    beforeRaised.add(amount).compareTo(model.totalCapacity()) <= 0;

            boolean accepted = model.tryRaise(amount);

            // (2) 接受 ⟺ 接受前 raised + amount ≤ totalCapacity
            assertThat(accepted)
                    .as("下单被接受当且仅当 接受前 raised + amount ≤ totalCapacity（对应 increaseRaisedAmount 返回 1）")
                    .isEqualTo(expectedAccept);

            if (accepted) {
                // 被接受：raised 恰好累加 amount
                assertThat(model.raised().compareTo(beforeRaised.add(amount)))
                        .as("被接受的下单应使 raised 恰好累加 amount")
                        .isZero();
            } else {
                // (3) 被拒绝：raised 保持不变（对应 increaseRaisedAmount 返回 0，OrderEngine 抛 40005）
                assertThat(model.raised().compareTo(beforeRaised))
                        .as("被拒绝的下单不改变 raised")
                        .isZero();
            }

            // (1) 不变量：任意一笔（无论接受或拒绝）之后 raised ≤ totalCapacity 恒成立
            assertThat(model.raised().compareTo(model.totalCapacity()))
                    .as("任意时刻 raisedAmount ≤ totalCapacity")
                    .isLessThanOrEqualTo(0);
        }
    }

    // Feature: staking-service, Property 9: 募集上限不变量
    // 子性质：raised 随被接受的下单单调不减，且最终 raised 等于起始值加上全部被接受金额之和（账本守恒）。
    // Validates: Requirements 5.7
    @Property(tries = 100)
    void raisedIsMonotonicAndEqualsInitialPlusAcceptedSum(@ForAll("scenarios") CapacityScenario scenario) {
        CapacityModel model = new CapacityModel(scenario.initialRaised(), scenario.totalCapacity());
        BigDecimal acceptedSum = BigDecimal.ZERO;

        for (BigDecimal amount : scenario.orderAmounts()) {
            BigDecimal beforeRaised = model.raised();
            boolean accepted = model.tryRaise(amount);

            if (accepted) {
                acceptedSum = acceptedSum.add(amount);
            }

            // 单调不减：raised 永不因下单而减少
            assertThat(model.raised().compareTo(beforeRaised))
                    .as("raised 随下单序列单调不减")
                    .isGreaterThanOrEqualTo(0);
        }

        // 账本守恒：最终 raised == 起始 raised + 全部被接受金额之和
        assertThat(model.raised().compareTo(scenario.initialRaised().add(acceptedSum)))
                .as("最终 raised 应等于 起始 raised 加上全部被接受下单金额之和")
                .isZero();
    }

    // ==================== 边界锚定示例 ====================

    // Feature: staking-service, Property 9: 募集上限不变量
    // 边界：恰好等于上限的下单被接受（raised + amount == totalCapacity），且接受后 raised == totalCapacity。
    // Validates: Requirements 5.7
    @Example
    void orderExactlyAtCapacityIsAccepted() {
        CapacityModel model = new CapacityModel(BigDecimal.ZERO, new BigDecimal("1000"));

        boolean accepted = model.tryRaise(new BigDecimal("1000"));

        assertThat(accepted).as("恰好等于上限的下单应被接受").isTrue();
        assertThat(model.raised().compareTo(new BigDecimal("1000")))
                .as("接受后 raised 应恰好等于 totalCapacity")
                .isZero();
        assertThat(model.raised().compareTo(model.totalCapacity()))
                .as("接受后仍满足 raisedAmount ≤ totalCapacity")
                .isLessThanOrEqualTo(0);
    }

    // Feature: staking-service, Property 9: 募集上限不变量
    // 边界：超出上限 1 个最小单位（1e-18）的下单被拒绝，且 raised 保持不变。
    // Validates: Requirements 5.7
    @Example
    void orderExceedingCapacityByOneUnitIsRejected() {
        CapacityModel model = new CapacityModel(BigDecimal.ZERO, new BigDecimal("1000"));

        boolean accepted = model.tryRaise(new BigDecimal("1000").add(ONE_UNIT));

        assertThat(accepted).as("超出上限 1 个最小单位的下单应被拒绝").isFalse();
        assertThat(model.raised().compareTo(BigDecimal.ZERO))
                .as("被拒绝的下单不改变 raised")
                .isZero();
    }

    // Feature: staking-service, Property 9: 募集上限不变量
    // 边界：已募集达到上限后，任意正数下单都被拒绝，raised 恒等于 totalCapacity。
    // Validates: Requirements 5.7
    @Example
    void furtherOrdersRejectedOnceCapacityReached() {
        CapacityModel model = new CapacityModel(new BigDecimal("1000"), new BigDecimal("1000"));

        assertThat(model.tryRaise(ONE_UNIT)).as("达到上限后任意正数下单都应被拒绝").isFalse();
        assertThat(model.tryRaise(new BigDecimal("0.5"))).as("达到上限后任意正数下单都应被拒绝").isFalse();
        assertThat(model.raised().compareTo(model.totalCapacity()))
                .as("被拒绝的下单后 raised 仍恒等于 totalCapacity")
                .isZero();
    }
}