From f011bee1da3bed5728c845680e069e0a327cc23c Mon Sep 17 00:00:00 2001 From: Stellar Wave Developer Date: Tue, 28 Apr 2026 12:16:18 +0100 Subject: [PATCH 1/3] feat: add fee-math-rounding bugfix spec with dust absorption requirements --- .kiro/specs/fee-math-rounding/.config.kiro | 1 + 1 file changed, 1 insertion(+) create mode 100644 .kiro/specs/fee-math-rounding/.config.kiro diff --git a/.kiro/specs/fee-math-rounding/.config.kiro b/.kiro/specs/fee-math-rounding/.config.kiro new file mode 100644 index 0000000..2819a34 --- /dev/null +++ b/.kiro/specs/fee-math-rounding/.config.kiro @@ -0,0 +1 @@ +{"specId": "e62baed1-6e47-408b-a634-7b5adfd1b9ba", "workflowType": "requirements-first", "specType": "bugfix"} \ No newline at end of file From d73de39024f958088492982d40a2e412a4ebce2c Mon Sep 17 00:00:00 2001 From: Stellar Wave Developer Date: Tue, 28 Apr 2026 12:23:01 +0100 Subject: [PATCH 2/3] feat: add fee-math-rounding bugfix requirements doc --- .kiro/specs/fee-math-rounding/bugfix.md | 61 +++++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 .kiro/specs/fee-math-rounding/bugfix.md diff --git a/.kiro/specs/fee-math-rounding/bugfix.md b/.kiro/specs/fee-math-rounding/bugfix.md new file mode 100644 index 0000000..54a3452 --- /dev/null +++ b/.kiro/specs/fee-math-rounding/bugfix.md @@ -0,0 +1,61 @@ +# Bugfix Requirements Document + +## Introduction + +When token amounts are split among multiple recipients or milestones using integer (i128/u128) +arithmetic, Rust's integer division silently truncates remainders. These dust fragments are +neither transferred to any recipient nor tracked by the protocol — they become permanently +stranded in the contract's token balance. The fix must ensure every remainder is explicitly +absorbed by a protocol-controlled balance variable so no capital is silently lost. + +## Bug Analysis + +### Current Behavior (Defect) + +1.1 WHEN a pool's collected amount is divided among N approved students and the amount is not + evenly divisible by N THEN the system silently discards the remainder (dust), leaving those + tokens permanently stranded in the contract with no owner. + +1.2 WHEN milestone amounts are set up such that their individual values involve integer division + (e.g., splitting an odd goal across milestones) THEN the system may accept a milestone set + whose per-milestone disbursements do not fully account for every token unit in the pool goal. + +1.3 WHEN `claim_funds` disburses a `claim_amount` that was derived from integer division of the + pool's collected balance THEN the system transfers only the truncated quotient, and the + remainder is never credited to any address or protocol variable. + +### Expected Behavior (Correct) + +2.1 WHEN a pool's collected amount is divided among N approved students and a non-zero remainder + exists THEN the system SHALL credit the remainder to a protocol dust-absorption balance + variable rather than leaving it unaccounted. + +2.2 WHEN milestone disbursements are computed and a non-zero remainder results from integer + division THEN the system SHALL route the remainder to the protocol dust-absorption balance + so that `sum(per_milestone_transfer) + dust_absorbed == total_collected`. + +2.3 WHEN `claim_funds` completes a disbursement cycle (all approved students have claimed their + share) THEN the system SHALL ensure that + `sum(all_claimed_amounts) + protocol_dust_balance == pool.collected`, with no tokens + unaccounted for. + +### Unchanged Behavior (Regression Prevention) + +3.1 WHEN a pool's collected amount is evenly divisible by the number of recipients THEN the + system SHALL CONTINUE TO transfer the full per-recipient share with zero dust absorbed. + +3.2 WHEN a student submits a valid `claim_amount` that is less than or equal to their remaining + approved allocation THEN the system SHALL CONTINUE TO transfer exactly `claim_amount` tokens + to the student without modification. + +3.3 WHEN `setup_application_milestones` is called with milestone amounts that sum exactly to the + pool goal THEN the system SHALL CONTINUE TO accept the milestone set and store it unchanged. + +3.4 WHEN `donate` is called on an open pool THEN the system SHALL CONTINUE TO increment + `pool.collected` by the exact donation amount with no truncation or rounding. + +3.5 WHEN an overdraw is attempted (amount_claimed + claim_amount > collected) THEN the system + SHALL CONTINUE TO panic with "Overdraw attempt". + +3.6 WHEN a student with a non-approved status attempts to call `claim_funds` THEN the system + SHALL CONTINUE TO panic with "Application is not approved". From d9ae72e0d9f6d36ce1e974290542939bd559ff22 Mon Sep 17 00:00:00 2001 From: Stellar Wave Developer Date: Tue, 28 Apr 2026 12:27:03 +0100 Subject: [PATCH 3/3] feat: add fee-math-rounding bugfix design doc --- .kiro/specs/fee-math-rounding/design.md | 289 ++++++++++++++++++++++++ 1 file changed, 289 insertions(+) create mode 100644 .kiro/specs/fee-math-rounding/design.md diff --git a/.kiro/specs/fee-math-rounding/design.md b/.kiro/specs/fee-math-rounding/design.md new file mode 100644 index 0000000..3337887 --- /dev/null +++ b/.kiro/specs/fee-math-rounding/design.md @@ -0,0 +1,289 @@ +# fee-math-rounding Bugfix Design + +## Overview + +Integer division in `claim_funds` and `setup_application_milestones` silently truncates +remainders when a pool's collected balance is split among N recipients or milestones. +The truncated dust is never transferred to any address and is never tracked, leaving tokens +permanently stranded in the contract's token balance. + +The fix introduces a per-pool `protocol_dust_balance: u128` storage variable. Whenever a +division produces a non-zero remainder, that remainder is added to `protocol_dust_balance` +rather than discarded. This restores the accounting invariant: + +``` +sum(all_claimed_amounts) + protocol_dust_balance == pool.collected +``` + +No existing transfer amounts, guard panics, or donation logic are changed. + +## Glossary + +- **Bug_Condition (C)**: The condition that triggers the bug — integer division of `collected` + (or a milestone total) by N produces a non-zero remainder that is neither transferred nor + tracked. +- **Property (P)**: The desired post-fix behavior — every remainder is credited to + `protocol_dust_balance` so the full accounting invariant holds. +- **Preservation**: All existing behaviors for non-dust paths (exact claims, donations, + overdraw guards, auth guards) must remain byte-for-byte identical. +- **`claim_funds`**: The function in `lib.rs` that disburses tokens to an approved student. + Currently uses `i128` arithmetic; the per-student share is computed externally and passed in + as `claim_amount`. +- **`setup_application_milestones`**: The function in `lib.rs` that stores per-milestone + amounts. Currently enforces `sum(milestones) == pool.goal` but does not account for + per-milestone integer-division remainders. +- **`protocol_dust_balance`**: The new per-pool `u128` storage field that absorbs all + integer-division remainders, ensuring no token unit is unaccounted for. +- **dust**: The non-zero remainder produced by `collected % N` (or `goal % N`) when the + division is not exact. + +## Bug Details + +### Bug Condition + +The bug manifests when a pool's `collected` (or `goal`) is divided by N and the result is +not exact. The contract performs the division, uses only the quotient, and silently drops +the remainder. There is no storage variable to receive the remainder, so those token units +are permanently stranded. + +**Formal Specification:** +``` +FUNCTION isBugCondition(collected: u128, n_recipients: u32) -> bool + INPUT: collected — total tokens in the pool (u128) + n_recipients — number of approved students or milestones (u32, > 0) + OUTPUT: boolean + + remainder := collected % (n_recipients as u128) + RETURN remainder != 0 +END FUNCTION +``` + +### Examples + +- `collected = 10, N = 3` → per-student share = 3, remainder = 1 stranded (bug) +- `collected = 100_000_001, N = 2` → per-student share = 50_000_000, remainder = 1 stranded (bug) +- `collected = 7, N = 7` → per-student share = 1, remainder = 0 → no dust (no bug) +- `collected = 9, N = 3` → per-student share = 3, remainder = 0 → no dust (no bug) + +## Expected Behavior + +### Preservation Requirements + +**Unchanged Behaviors:** +- `donate` MUST continue to increment `pool.collected` by the exact donation amount with no + rounding or truncation. +- A student calling `claim_funds` with an explicit `claim_amount` that is ≤ their remaining + approved allocation MUST continue to receive exactly `claim_amount` tokens. +- `setup_application_milestones` MUST continue to accept milestone sets whose amounts sum + exactly to the pool goal and store them unchanged. +- The overdraw guard (`amount_claimed + claim_amount > collected` → panic "Overdraw attempt") + MUST remain in place. +- The auth guard (non-approved status → panic "Application is not approved") MUST remain in + place. + +**Scope:** +All inputs where `collected % N == 0` (exact division) are completely unaffected by this fix. +The only behavioral change is that when a remainder exists, it is credited to +`protocol_dust_balance` instead of being silently dropped. + +## Hypothesized Root Cause + +1. **No remainder tracking variable**: The contract has no field or storage key to hold + integer-division remainders. When `claim_amount` is derived from `collected / N`, the + caller computes only the quotient; the `%` remainder is never computed or stored anywhere + in the contract. + +2. **Implicit truncation in Rust integer arithmetic**: Rust's `/` operator on integer types + truncates toward zero by definition. There is no compile-time or runtime warning when a + remainder is discarded, so the loss is invisible. + +3. **Missing invariant assertion**: No post-claim assertion verifies + `sum(claimed) + dust == collected`. Without this check, the accounting gap is never + surfaced during normal operation or existing tests. + +4. **Milestone validation only checks sum == goal**: `setup_application_milestones` enforces + `sum(milestones) == goal` but does not account for the case where individual milestone + amounts were themselves derived from integer division, potentially leaving a remainder + untracked at disbursement time. + +## Correctness Properties + +Property 1: Bug Condition — Full Accounting Invariant After All Claims + +_For any_ pool where `isBugCondition(collected, N)` is true (i.e., `collected % N != 0`), +after all N approved students have called `claim_funds` for their share, the fixed contract +SHALL satisfy: + +``` +sum(application.amount_claimed for all students) + protocol_dust_balance(pool_id) == pool.collected +``` + +No token unit may be unaccounted for. + +**Validates: Requirements 2.1, 2.2, 2.3** + +Property 2: Preservation — Exact-Division Pools Produce Zero Dust + +_For any_ pool where `isBugCondition(collected, N)` is false (i.e., `collected % N == 0`), +the fixed contract SHALL produce `protocol_dust_balance(pool_id) == 0` and each student +SHALL receive exactly `collected / N` tokens, identical to the behavior of the original +contract on the same input. + +**Validates: Requirements 3.1, 3.2** + +## Fix Implementation + +### Changes Required + +**File**: `Nevo/nevo_contract/contracts/hello-world/src/lib.rs` + +**New storage key constant:** +```rust +const DUST_BALANCE_PREFIX: &str = "dust_bal"; +``` + +**New public accessor (add to `impl Contract`):** +```rust +pub fn get_protocol_dust_balance(env: Env, pool_id: u32) -> u128 { + let key = (Symbol::new(&env, DUST_BALANCE_PREFIX), pool_id); + env.storage().persistent().get::<_, u128>(&key).unwrap_or(0) +} +``` + +**Specific Changes to `claim_funds`:** + +1. **Compute remainder at claim time**: After the overdraw check passes, compute + `remainder = (pool.collected as u128) % (n_approved_students as u128)` where + `n_approved_students` is the count of approved applications for the pool. + +2. **Credit remainder to `protocol_dust_balance`**: On the final claim (when + `application.amount_claimed + claim_amount == collected`), add the remainder to the + per-pool dust balance: + ```rust + let dust_key = (Symbol::new(&env, DUST_BALANCE_PREFIX), pool_id); + let current_dust: u128 = env.storage().persistent() + .get::<_, u128>(&dust_key).unwrap_or(0); + env.storage().persistent().set(&dust_key, &(current_dust + remainder)); + ``` + +3. **Alternative simpler approach** (recommended for minimal diff): Rather than tracking + "final claim", compute the remainder on every claim cycle and store it. The invariant + check can be done in a separate `assert_accounting_invariant` helper used in tests. + +**Specific Changes to `setup_application_milestones`:** + +4. **Relax the strict equality check**: Change `if sum != pool_data.1` to allow + `sum + remainder == pool_data.1` where `remainder` is credited to `protocol_dust_balance` + at milestone setup time, OR keep the strict check and require callers to pass + milestone amounts that already account for the remainder in the last milestone. + +5. **Recommended approach**: Keep the strict `sum == goal` check for milestones (requirement + 3.3 preservation) and handle dust only at `claim_funds` disbursement time, since that is + where the actual token transfer occurs. + +**Summary of minimal change set:** +- Add `DUST_BALANCE_PREFIX` constant +- Add `get_protocol_dust_balance` accessor +- In `claim_funds`, after updating `application.amount_claimed`, compute + `let remainder = (collected as u128) % (n_recipients as u128)` and persist it to + `protocol_dust_balance` when the remainder is non-zero and this is the cycle-closing claim + +## Testing Strategy + +### Validation Approach + +Two-phase approach: first run exploratory tests on the unfixed code to surface the accounting +gap as a concrete counterexample, then verify the fix satisfies Property 1 and Property 2. + +### Exploratory Bug Condition Checking + +**Goal**: Surface a counterexample demonstrating the stranded-dust bug on the unfixed code. +Confirm that `sum(claimed) < pool.collected` when `collected % N != 0`. + +**Test Plan**: Set up a pool with `collected = 10`, approve 3 students, have each claim +`10 / 3 = 3` tokens, then assert `sum(claimed) + protocol_dust_balance == 10`. On unfixed +code this assertion fails because `protocol_dust_balance` does not exist and `sum(claimed) = 9`. + +**Test Cases:** +1. **Odd split (3 students, 10 tokens)**: collected=10, N=3, each claims 3 → sum=9, 1 stranded + (will fail invariant check on unfixed code) +2. **Large remainder (2 students, 100_000_001 tokens)**: collected=100_000_001, N=2, each + claims 50_000_000 → sum=100_000_000, 1 stranded (will fail on unfixed code) +3. **Milestone remainder**: goal=7, 3 milestones of [2,2,2] → sum=6, 1 stranded (will fail + on unfixed code) +4. **Edge case — single student, indivisible**: collected=1, N=1 → no remainder, no bug + (should pass on both unfixed and fixed code) + +**Expected Counterexamples:** +- `sum(claimed) + 0 < pool.collected` — the gap equals `collected % N` +- No `protocol_dust_balance` storage key exists on unfixed code + +### Fix Checking + +**Goal**: Verify Property 1 — for all inputs where `isBugCondition` is true, the invariant +holds after the fix. + +**Pseudocode:** +``` +FOR ALL (collected, n_recipients) WHERE collected % n_recipients != 0 DO + pool := create_pool_with_collected(collected) + FOR i IN 1..=n_recipients DO + claim_funds(student_i, pool_id, collected / n_recipients) + END FOR + dust := get_protocol_dust_balance(pool_id) + total_claimed := sum(get_claimed_amount(pool_id, student_i) for i in 1..=n_recipients) + ASSERT total_claimed + dust == collected +END FOR +``` + +### Preservation Checking + +**Goal**: Verify Property 2 — for all inputs where `isBugCondition` is false (`collected % N == 0`), +the fixed contract behaves identically to the original. + +**Pseudocode:** +``` +FOR ALL (collected, n_recipients) WHERE collected % n_recipients == 0 DO + ASSERT get_protocol_dust_balance(pool_id) == 0 + ASSERT each student receives exactly collected / n_recipients + ASSERT claim_funds_original(input) == claim_funds_fixed(input) +END FOR +``` + +**Testing Approach**: Property-based testing is recommended because: +- It generates many `(collected, N)` pairs automatically, covering the full u128 domain +- It catches off-by-one errors in remainder computation that unit tests might miss +- It provides strong guarantees that exact-division behavior is unchanged + +**Test Cases:** +1. **Exact-division preservation**: collected=9, N=3 → each student gets 3, dust=0 +2. **Donation preservation**: `donate` still increments `collected` exactly +3. **Overdraw guard preservation**: claiming more than `collected` still panics +4. **Auth guard preservation**: non-approved student still panics + +### Unit Tests + +- `test_dust_absorbed_odd_split`: collected=10, N=3, assert invariant holds after fix +- `test_no_dust_even_split`: collected=9, N=3, assert `protocol_dust_balance == 0` +- `test_single_student_no_dust`: collected=100, N=1, assert dust=0 +- `test_large_remainder`: collected=100_000_001, N=2, assert dust=1 after both claims +- `test_overdraw_still_panics`: existing test must continue to pass unchanged +- `test_claim_funds_rejected_still_panics`: existing test must continue to pass unchanged + +### Property-Based Tests + +- Generate random `(collected: u128, n: u32 in 1..=10)` pairs; after all N claims assert + `sum(claimed) + dust == collected` (validates Property 1) +- Generate random `(collected: u128, n: u32)` where `collected % n == 0`; assert `dust == 0` + and each student receives exactly `collected / n` (validates Property 2) +- Generate random valid `claim_amount` values ≤ remaining allocation; assert transfer amount + is unchanged by the fix (preservation of explicit claims) + +### Integration Tests + +- Full pool lifecycle: create → donate (odd amount) → approve N students → all claim → assert + invariant +- Mixed claims: some students claim partial amounts across multiple calls → assert invariant + holds at each intermediate step and at completion +- Milestone flow: setup milestones with exact sum → disburse → assert no dust introduced by + milestone path