test: add property-based invariant tests for credit accrual (closes #75)

[Cyber-Mitch]

closes #75

Adds four property-based tests for the credit-accrual system, each backed by a closed-form derivation rather than a chosen tolerance. One important correction to the issue as filed: the tolerance the issue expects for deposit-granularity and checkpoint-frequency independence does not exist for this implementation — both properties hold as strict equalities, and the analysis below shows why, with the loss bound the issue anticipated shown to be structurally unreachable via those two paths (though reachable via a different, adjacent path — noted at the bottom).

The derivation

Notation: B(a,p) = ⌊a·p/100⌋ (the only nonlinearity in the whole accrual path). compute_total_stake (lib.rs:248-253) reduces to:

S(a,p,m) = (a − B(a,p)) + B(a,p)·m = a + B(a,p)·(m−1)

and compute_credits = S(a,p,m)·r·elapsed.

Where truncation loss actually comes from. For a partition A = a₁+…+aₙ, writing aᵢ·p/100 = qᵢ + fᵢ with fᵢ ∈ [0,1):

B(A,p) − Σᵢ B(aᵢ,p) = ⌊Σfᵢ⌋ ∈ [0, n−1]

Upper bound n−1, tight at p=99, aᵢ=1, n=100. An implementation that banked B separately per part would lose up to (n−1)(m−1)·r·elapsed credits — this is the issue's predicted loss, now with the constant pinned. I validated the formula empirically: 7 users staking 101 each vs. one user staking 707, at p=33, m=7 — predicted ⌊7·⅓⌋·(m−1) = 12, measured 12. Exact match.

But this loss is not reachable by splitting a single user's deposit. stake() does existing.amount += amount (lib.rs:688) before any later call to compute_total_stake, and every call site passes the cumulative stake.amount (lib.rs:271, 859). B is therefore only ever evaluated on the aggregate — the per-part truncation the issue's suggested tolerance was defending against never occurs in this code path.

Property A — deposit granularity → strict equality, tolerance = 0

Two facts: (1) a second stake() at the same ledger checkpoints with elapsed = 0, so credits_banked += S·r·0 = 0; (2) existing.amount += amount aggregates before B is next evaluated. After subdividing a deposit, UserStake is field-for-field identical to the unsplit case, so every later checkpoint observes identical state. Loss = 0, not bounded-by-ε.

Asserted against an independent closed-form oracle (credits = r · Σⱼ S(Aⱼ, p, m) · Δeⱼ, computed in the test) so the property can't pass by both the contract and the test being wrong the same way.

Property B — checkpoint frequency → strict equality, tolerance = 0

Chopping [t₀, T] into arbitrarily many sub-intervals t₀<t₁<…<t_k with A, p, m fixed: Σⱼ S·r·(tⱼ₊₁−tⱼ) = S·r·T by plain integer distributivity — no rounding is introduced by time-partitioning. The floor in B is a function of (amount, pct) only, evaluated once per checkpoint regardless of how many checkpoints occur. This is why the issue's expected tolerance doesn't exist here: the property is strictly stronger (==, not ≤ ε) than what was asked for, and a tolerance-bounded version would have been blind to a real regression of up to (n−1)(m−1)·r·e.

Preconditions stated in the test's doc comment, since outside them the property is false by design: credit_rate fixed, global_multiplier fixed (see Property E below), allocation_pct set before the first stake.

Property C — monotonicity → strict increase

get_credits = credits_banked + S(A,p,m)·r·elapsed. Every slope factor is ≥ 1: S ≥ A ≥ 1 (enforced, lib.rs:672), r ≥ 1 (#89's ceiling). So Δcredits ≥ 1 for Δelapsed ≥ 1 — strictly increasing, not merely non-decreasing. No truncation ambiguity: elapsed appears only as a multiplicand. Covers both get_credits and the lock/unlock credit path.

Property D — non-negativity

get_credits is a sum of products of provably non-negative factors: principal = A − B(A,p) ≥ 0 (since p ≤ 100 ⇒ B ≤ A), virtual = B·m ≥ 0, r > 0, elapsed ≥ 0. Generators respect the contract's own gates (amount > 0, min_stake_amount, pct ∈ 1..=100, whitelist default-disabled) so the property is never asserted on unreachable states.

Property E — flagged, not implemented (per the issue's own instruction not to encode a guess as a passing test)

Investigating deposit-granularity and checkpoint-frequency turned up a real, undertested asymmetry: checkpoint snapshots credit_rate into UserStake (lib.rs:278), so a mid-flight set_credit_rate change is not retroactive — but it re-reads global_multiplier live and applies it to the already-elapsed segment. Since set_global_multiplier cannot checkpoint other users first, this means an admin multiplier change retroactively reprices every user's currently-open segment.

Demonstrated concretely: m=2, p=100, A=10_000 earning 10_000 credits, then set_global_multiplier(3) with zero ledgers elapsed → credits jump to 30_000.

test_admin_multiplier_change_applies_from_next_checkpoint (test.rs:553) is named as though snapshot semantics hold, but it deliberately inserts a no-op checkpoint immediately before the multiplier bump (test.rs:562), so it never actually exercises the retroactive case.

Question for the maintainer: should global_multiplier be snapshotted into UserStake alongside credit_rate (making the change non-retroactive, matching the rate's documented semantics and the sibling test's name)? Or is retroactive repricing of open segments intended? Both readings are defensible and nothing in the codebase settles it — asserting either direction here would encode a guess as a passing test, so I left it as a documented comment block in the diff (test.rs:2638) rather than a test.

(Out of scope, recorded for completeness: the (n−1)(m−1)·r·e loss from the derivation above is reachable — via cross-user aggregation, not deposit splitting. That's an aggregation invariant, not a checkpoint-frequency one, and belongs to a separate issue.)

Coordination

• farming-pool: no fuzz/boundary test exercises i128 overflow boundaries in compute_credits/compute_total_stake #76 (overflow fuzz) — not landed; no proptest anywhere on upstream/main. Added it here; if farming-pool: no fuzz/boundary test exercises i128 overflow boundaries in compute_credits/compute_total_stake #76 lands first, it should reuse this dependency line rather than duplicate it.
• farming-pool: set_global_multiplier and set_credit_rate accept unbounded values with no sanity ceiling, guaranteeing compute_credits overflow at scale #89 (rate/multiplier ceilings) — landed. Generators import MAX_GLOBAL_MULTIPLIER and MAX_CREDIT_RATE directly rather than restating them, so ranges track any future ceiling change automatically. amount ∈ 1..=10¹² — worst case ~4.5×10²⁸, ~10 orders of magnitude below i128::MAX, deliberately far inside accounting-error territory only; overflow boundaries are farming-pool: no fuzz/boundary test exercises i128 overflow boundaries in compute_credits/compute_total_stake #76's job.

Mutation testing — proof these tests have teeth

Rather than trust the assertions by inspection, I deliberately broke the contract four ways and confirmed each mutation is caught by a different assertion independently, then restored lib.rs to pristine (git diff empty):

Mutation	Result
amount / 100 * pct (divide-before-multiply)	A and B both fail — caught by the oracle
checkpoint drops one ledger of elapsed time	Caught
Lossy zero-elapsed checkpoint accounting	A's oracle fails alone
Lossy set_boost checkpoint only	B's differential fails alone

All four assertions independently live.

Verification

Check	Result
cargo build --workspace --target wasm32v1-none --release	✅
cargo fmt --all -- --check	✅
cargo clippy --workspace --all-targets -- -D warnings	✅ clean
cargo test --workspace	✅ 188 passed, 0 failed (184 baseline + 4 new), 12.3s wall clock

New properties specifically (64 cases each): 3.15s / 3.02s / 1.40s / 1.33s individually, 4.34s run in parallel. proptest confirmed dev-only — strings on the release WASM shows zero proptest occurrences, grep -a proptest farming_pool.wasm absent, WASM builds clean.

Changed files

• Cargo.lock — 25 new packages (proptest's dependency tree), zero removed, zero existing versions changed.
• farming-pool/Cargo.toml — proptest = "1" as a plain [dev-dependencies] entry (not the testutils feature, which forwards into factory's dependency graph — kept separate so it can never reach the deployable build).
• farming-pool/src/test.rs — the four property tests plus the Property E comment block. lib.rs untouched — no contract logic changed.

Acceptance criteria

• proptest added as a dev-dependency
• Path-independence for deposit granularity, within a documented derived (not guessed) tolerance — turned out to be strict equality; bound shown so a reviewer can verify it independently
• Monotonicity for elapsed ledgers, strict, covering both credit-read paths
• Non-negativity, including zero boundaries
• Runs in CI without network access or excessive runtime — 4.34s parallel, 64 cases; capture_snapshot_at_drop: false prevents one snapshot JSON per proptest case
• Property E documented as deferred pending maintainer input, per the issue's own instruction not to encode an assumption as a passing test

Found, not fixed

1. global_multiplier retroactivity (Property E above) — real, demonstrated, needs your call on intended semantics.
2. Local cargo test --workspace requires a WASM pre-build step not documented outside ci.yml:38 — factory embeds farming_pool::WASM via contractimport!, so a stale/absent artifact throws Error(WasmVm, UnexpectedParameterLen) in 16 factory tests. Not introduced by this PR; worth a README note.
3. ~143 committed test_snapshots/*.json are stale, for two independent reasons (non-reproducible embedded-WASM-hash/instruction-count codegen, and some predating the MinStakeAmount/SchemaVersion fields). A full cargo test --workspace run rewrites them; I restored them to their committed state before finalizing this diff, so running the suite again will dirty them the same way. Not contract-logic breakage, not introduced here.

None of the above involves contract-logic changes — lib.rs is byte-identical to main.

[netlify]

✅ Deploy Preview for sdcontracts ready!

Name	Link
🔨 Latest commit	5d68d0a
🔍 Latest deploy log	https://app.netlify.com/projects/sdcontracts/deploys/6a8efd29045323000876f743
😎 Deploy Preview	https://deploy-preview-139--sdcontracts.netlify.app
📱 Preview on mobile	Toggle QR Code... Use your smartphone camera to open QR code link.

---

To edit notification comments on pull requests, go to your Netlify project configuration.

[Cyber-Mitch]

@prodbycorne Please review