CalloraOrg · greatest0fallt1me · Jun 26, 2026 · Jun 25, 2026 · Jun 25, 2026
diff --git a/EVENT_SCHEMA.md b/EVENT_SCHEMA.md
@@ -811,6 +811,47 @@ Emitted by `set_vault()` when the admin updates the registered vault address.
 
 ---
 
+### `developer_force_credited`
+
+Emitted by `force_credit_developer()` when an admin manually credits a developer balance (escape hatch).
+
+This is an **admin-authorized inflow** — no on-ledger USDC is moved. It is designed for
+operational edge cases (off-chain payment reconciliation, dispute resolution).
+
+| Index         | Location | Type    | Description                                                     |
+|---------------|----------|---------|-----------------------------------------------------------------|
+| topic 0       | topics   | Symbol  | `"developer_force_credited"`                                    |
+| topic 1       | topics   | Address | `developer` — address whose balance was updated                  |
+| `developer`   | data     | Address | same as topic 1; duplicated for data-only indexers              |
+| `amount`      | data     | i128    | amount credited to the developer in USDC micro-units            |
+| `reason`      | data     | Symbol  | on-chain reason code for the manual credit                      |
+| `new_balance` | data     | i128    | developer's cumulative balance after this credit (post-state)   |
+
+```json
+{
+  "topics": ["developer_force_credited", "GDEV..."],
+  "data": {
+    "developer": "GDEV...",
+    "amount": 5000000,
+    "reason": "offline_settlement",
+    "new_balance": 7500000
+  }
+}
+```
+
+**Invariants.**
+- `new_balance = prior_balance + amount`, checked for `i128` overflow.
+- Only the contract admin may call `force_credit_developer`.
+- This is an audit-only path; every credit includes an on-chain `reason` Symbol.
+
+**Indexer guidance.**
+- Subscribe to `developer_force_credited` to track admin-initiated manual credits.
+- The `reason` field distinguishes different operational scenarios (e.g., `"dispute_resolution"`, `"offline_settlement"`, `"bulk_reconciliation"`).
+- This event is **never** paired with a `payment_received` event.
+- For full accounting, sum `balance_credited.amount` + `developer_force_credited.amount` to compute total developer inflows.
+
+---
+
 ## Indexer quick-reference
 
 | Event                    | Contract        | Trigger                                  |
@@ -845,6 +886,7 @@ Emitted by `set_vault()` when the admin updates the registered vault address.
 | `payment_received`       | settlement      | `receive_payment()`                      |
 | `balance_credited`       | settlement      | `receive_payment()` with `to_pool=false` |
 | `vault_changed`          | settlement      | `set_vault()`                            |
+| `developer_force_credited`| settlement     | `force_credit_developer()`               |
 
 ---
 
@@ -858,3 +900,4 @@ Emitted by `set_vault()` when the admin updates the registered vault address.
 | 0.0.1   | revenue-pool  | Full revenue pool event suite with JSON examples             |
 | 0.0.1   | revenue-pool  | Added `admin_changed` event on `set_admin` for explicit old/new admin intent |
 | 0.1.0   | settlement    | `payment_received`, `balance_credited`                       |
+| 0.1.0   | settlement    | `developer_force_credited` (admin escape hatch)               |
diff --git a/INVARIANTS.md b/INVARIANTS.md
@@ -483,3 +483,67 @@ The settlement, vault, and revenue-pool test suites provide practical evidence f
   - Verifies unauthorized callers cannot change the vault's settlement destination.
 
 Together with the explicit pre-/post-conditions above, these tests help auditors and maintainers validate that **cross-contract routing, accounting, and payout actions remain reachable only by the intended principals**.
+
+---
+
+## Revenue Pool On-Ledger Coverage Invariant
+
+**Invariant**: For every reachable state of [`RevenuePool`](contracts/revenue_pool/src/lib.rs#L45), the on-ledger USDC balance of the contract is always **greater than or equal to** the sum of all approved-but-not-yet-distributed payments (the "scheduled" or "pending" total).
+
+- **On-ledger balance**: `usdc.balance(&current_contract_address)` queried via [`balance(env)`](contracts/revenue_pool/src/lib.rs#L546)
+- **Pending total**: A virtual sum tracked off-chain by the backend. In the invariant test, this is simulated as a local `scheduled` variable.
+- **Guarantee**: The admin can always distribute the full set of pending payments without encountering an `ERR_INSUFFICIENT_BALANCE` panic, assuming no concurrent external USDC transfers out of the pool.
+
+### Functions That Modify the Balance
+
+| Function | Effect on balance | Effect on pending |
+|---|---|---|
+| [`receive_payment`](contracts/revenue_pool/src/lib.rs#L272) | None (event-only) | None |
+| [`distribute`](contracts/revenue_pool/src/lib.rs#L341) | Decreases by `amount` | Decreases by `amount` (on success) |
+| [`batch_distribute`](contracts/revenue_pool/src/lib.rs#L455) | Decreases by `sum(amounts)` | Decreases by `sum(amounts)` (on success) |
+| External USDC transfer in | Increases | None |
+| External USDC transfer out | Decreases | None (only admin-distribute paths are intended) |
+
+### Pre-conditions
+
+- `distribute` / `batch_distribute`:
+  - `caller == admin` (authorized)
+  - `amount > 0`
+  - `amount <= max_distribute`
+  - Pool is not paused
+  - `usdc.balance(&self) >= amount` (or `>= sum(amounts)` for batch)
+- `schedule` (off-chain backend action, simulated in test):
+  - Must be accompanied by a corresponding USDC deposit (or must not exceed available balance)
+
+### Post-conditions
+
+- After a successful `distribute` or `batch_distribute`:
+  - `balance' = balance - amount`
+  - `pending' = pending - amount`
+  - The invariant `balance' >= pending'` holds if it held before.
+- After an external USDC deposit (fund):
+  - `balance' = balance + amount`
+  - `pending' = pending`
+  - The invariant holds — more slack.
+- After a successful `schedule` (accompanied by funding):
+  - `balance' = balance + amount`
+  - `pending' = pending + amount`
+  - The invariant holds — both sides increase equally.
+- If any pre-condition fails, the call reverts and state is unchanged.
+
+### How Tests Support the Invariant
+
+The invariant test in [`test_invariant.rs`](contracts/revenue_pool/src/test_invariant.rs) provides Foundry-style stateful invariant coverage:
+
+- **128 deterministic seeded traces**: Each seed (0..127) generates a unique sequence of 75 stateful actions.
+- **Action types**:
+  - **Fund** (33%): Mint USDC to the pool, increasing the balance gap.
+  - **Schedule and fund** (25%): Mint USDC *and* increase the virtual `scheduled` total, simulating a backend approval with concurrent vault settlement.
+  - **Distribute single** (17%): Call `distribute` — on success, decrement `scheduled`.
+  - **Batch distribute** (8%): Call `batch_distribute` with 1-5 random legs — on success, decrement `scheduled` by the batch total. Duplicate recipient detection is implicitly exercised by random address selection.
+  - **Pause/unpause toggle** (8%): Guards are tested by toggling the pause flag.
+  - **Pause-then-distribute edge case** (8%): Pauses the pool, attempts a `distribute` (which must revert with `ERR_PAUSED`), then unpauses. Verifies that `scheduled` is unchanged after the failed attempt.
+- **Invariant check after every action**: `usdc.balance(pool) >= scheduled` is asserted after each of the 75 steps across all 128 traces — 9,600 invariant checks total.
+- **`catch_unwind` for expected reverts**: Actions that are expected to fail (e.g., distribute while paused, duplicate recipients, insufficient balance) are wrapped in `std::panic::catch_unwind` so that the test runner continues the trace and verifies the invariant after the revert.
+
+Together with the explicit design above, these tests help auditors and maintainers validate that **the revenue pool's on-ledger USDC never falls below the sum of pending scheduled distributions**.
diff --git a/contracts/revenue_pool/src/lib.rs b/contracts/revenue_pool/src/lib.rs
@@ -23,6 +23,8 @@ const ERR_UNAUTHORIZED: &str = "unauthorized: caller is not admin";
 const ERR_INSUFFICIENT_BALANCE: &str = "insufficient USDC balance";
 const ERR_NOT_INITIALIZED: &str = "revenue pool not initialized";
 const ERR_DUPLICATE_RECIPIENT: &str = "duplicate recipient in batch";
+const PAUSED_KEY: &str = "paused";
+const ERR_PAUSED: &str = "revenue pool is paused";
 const VERSION_KEY: &str = "version";
 
 pub const DEFAULT_MAX_DISTRIBUTE: i128 = i128::MAX;
@@ -596,3 +598,6 @@ mod test;
 
 #[cfg(test)]
 mod test_balance;
+
+#[cfg(test)]
+mod test_invariant;