Skip to content

Fix/pausability invariants concurrency verification - #1013

Merged
Junirezz merged 5 commits into
Junirezz:mainfrom
Mosas2000:fix/pausability-invariants-concurrency-verification
Jul 28, 2026
Merged

Fix/pausability invariants concurrency verification#1013
Junirezz merged 5 commits into
Junirezz:mainfrom
Mosas2000:fix/pausability-invariants-concurrency-verification

Conversation

@Mosas2000

Copy link
Copy Markdown
Contributor

Summary
This pull request addresses and resolves four open issues across the Soroban smart contracts and Node/TypeScript backend in YieldVault-RWA:

#960: Implement role-restricted pausability controls allowing a designated Pauser address alongside Admin.
#959: Add unit and property-based invariant test coverage asserting share-price monotonicity ($P_{t+1} \ge P_t$).
#957: Introduce optimistic concurrency controls (OCC) in the backend persistence layer.
#968: Add formal verification specifications and executable invariant tests for critical accounting logic.
Issue Breakdowns & Changes Implemented

  1. Contract: Implement pausability controls with role-restricted access #960 Contract: Implement pausability controls with role-restricted access
    Role Assignment: Added DataKey::Pauser in DataKey enum and implemented set_pauser(env, pauser) (admin-only) and pauser(env) query.
    Role-Restricted Execution: Added pause_with_role(env, caller, reason) and unpause_with_role(env, caller) functions enforcing authorization via permissions::require_pauser_or_admin_auth.
    Test Coverage: Added test_role_restricted_pausability_controls in contracts/vault/src/feature_tests.rs.
  2. Contract: Add invariant tests for share-price monotonicity #959 Contract: Add invariant tests for share-price monotonicity
    Vault Invariant Suite: Added test_invariant_share_price_monotonicity_under_yield_accrual and test_invariant_share_price_monotonicity_under_deposits_and_withdrawals in contracts/vault/src/invariant_tests.rs.
    Math Fuzz Assertions: Extended contracts/share-price-math/src/fuzz_invariants.rs to assert $P_{after} \ge P_{before}$ across arbitrary positive yield accruals.
  3. Backend: Introduce optimistic concurrency controls in persistence layer #957 Backend: Introduce optimistic concurrency controls in persistence layer
    Schema Extensions: Added version Int @default(1) column to stateful models (VaultState, BulkExportJob, WebhookEndpoint, EmailQueue, TransactionBackfillJob) in backend/prisma/schema.prisma.
    OCC Handler & Retries: Implemented OptimisticConcurrencyError, assertVersionMatch, and executeWithOptimisticConcurrency with exponential backoff and randomized jitter in backend/src/optimisticConcurrency.ts.
    Test Coverage: Created backend/src/tests/optimisticConcurrency.test.ts covering version matching, collision detection, and retry bounds.
  4. Contract: Add formal verification notes for critical accounting logic #968 Contract: Add formal verification notes for critical accounting logic
    Mathematical Specification: Created docs/FORMAL_VERIFICATION_ACCOUNTING.md documenting formal theorems for share conversion, share-price monotonicity, solvency bounds, and round-trip loss invariants.
    Executable Formal Property Suite: Created contracts/vault/src/formal_verification_tests.rs verifying Theorems 1–3 in Soroban contract tests.
    Architecture References: Updated docs/CONTRACTS_ARCHITECTURE.md to index formal verification notes.
    Related Issues
    Closes Contract: Implement pausability controls with role-restricted access #960
    Closes Contract: Add invariant tests for share-price monotonicity #959
    Closes Backend: Introduce optimistic concurrency controls in persistence layer #957
    Closes Contract: Add formal verification notes for critical accounting logic #968

@drips-wave

drips-wave Bot commented Jul 26, 2026

Copy link
Copy Markdown

@Mosas2000 Great news! 🎉 Based on an automated assessment of this PR, the linked Wave issue(s) no longer count against your application limits.

You can now already apply to more issues while waiting for a review of this PR. Keep up the great work! 🚀

Learn more about application limits

@Junirezz
Junirezz merged commit f18ae96 into Junirezz:main Jul 28, 2026
12 of 18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

2 participants