From 8e25aba9c08cab686c0bf8ec2489483dd2a24333 Mon Sep 17 00:00:00 2001 From: Pablo Ragalli Date: Thu, 22 Oct 2026 09:14:18 -0300 Subject: [PATCH 1/4] docs: separate role and signature tests --- docs/TESTING.md | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/docs/TESTING.md b/docs/TESTING.md index ca832e7b..219e4951 100644 --- a/docs/TESTING.md +++ b/docs/TESTING.md @@ -42,9 +42,21 @@ library, which manages their TTL itself. ## Authorization -Most tests sign every call with `mock_all_auths`. A refusal test then clears -all signatures with `set_auths(&[])` and checks the call fails and changes -nothing. +Authorization is tested in two separate layers. + +**Who may call (roles).** Each privileged entrypoint is called by an account +that holds the role and by accounts that do not: an unrelated address, or +another authority such as governance calling a manager-only entrypoint. Role +membership is the contract's real state, not a mock. Most of these tests run +with `mock_all_auths`, so every signature is granted and a refusal can only +come from the role check. + +**Whether a signature is required.** A refusal test clears all signatures with +`set_auths(&[])` and checks the call fails and changes nothing, which proves the +entrypoint requires the right address to sign. + +The per-entrypoint role matrix, with the refusal test for each, is in +[AUTHORIZATION_MATRIX.md](./AUTHORIZATION_MATRIX.md). | Behaviour | Tests | Key test names | | --- | --- | --- | From 4b3201b59e90786cc7c7c6444a3d994bca865f76 Mon Sep 17 00:00:00 2001 From: Pablo Ragalli Date: Thu, 22 Oct 2026 09:14:18 -0300 Subject: [PATCH 2/4] docs: render kit spec math on GitHub --- docs/kit-spec.md | 66 ++++++++++++++++++++++++++++++++---------------- 1 file changed, 44 insertions(+), 22 deletions(-) diff --git a/docs/kit-spec.md b/docs/kit-spec.md index 345b408a..b8c05fea 100644 --- a/docs/kit-spec.md +++ b/docs/kit-spec.md @@ -14,25 +14,37 @@ It covers: The contracts enforce a set of mathematical and state-machine invariants across all operations. Each invariant is stated below as a formal, testable property matching the on-chain test suite. ### Invariant 1: Escrow Stays, Only Free Reserve Moves -- **Definition**: Cancellable subscription escrow never leaves the vault, and only the free reserve can move to the custodian. Priced redemption liabilities (`committed`) may exceed the liquid reserve; the shortfall is reported as `uncovered`, not refused. Here $\text{held}$ is the vault's balance of the settlement asset. +- **Definition**: Cancellable subscription escrow never leaves the vault, and only the free reserve can move to the custodian. Priced redemption liabilities (`committed`) may exceed the liquid reserve; the shortfall is reported as `uncovered`, not refused. Here $`\text{held}`$ is the vault's balance of the settlement asset. - **Mathematical Statement**: - $$\text{liquid\_reserve} = \text{held} - \text{cancellable\_escrow}$$ - $$\text{free\_reserve} = \max(\text{liquid\_reserve} - \text{committed} - \text{wind\_down\_owed}, 0)$$ - $$\text{uncovered} = \max(\text{committed} - \text{liquid\_reserve}, 0)$$ -- **Testable Property**: `deploy_to_custodian(assets)` is refused with `ReserveCommittedToExits` when $\text{assets} > \text{free\_reserve}$, so after every operation $\text{held} \ge \text{cancellable\_escrow}$. While $\text{uncovered} > 0$, the free reserve is zero and nothing leaves for the custodian. + ```math + \text{liquid\_reserve} = \text{held} - \text{cancellable\_escrow} + ``` + ```math + \text{free\_reserve} = \max(\text{liquid\_reserve} - \text{committed} - \text{wind\_down\_owed}, 0) + ``` + ```math + \text{uncovered} = \max(\text{committed} - \text{liquid\_reserve}, 0) + ``` +- **Testable Property**: `deploy_to_custodian(assets)` is refused with `ReserveCommittedToExits` when $`\text{assets} > \text{free\_reserve}`$, so after every operation $`\text{held} \ge \text{cancellable\_escrow}`$. While $`\text{uncovered} > 0`$, the free reserve is zero and nothing leaves for the custodian. - **Enforcement**: `deploy_to_custodian` is the only outbound path to the custodian, and it moves at most the free reserve. ### Invariant 2: Notice Period Respected - **Definition**: An epoch cannot be fulfilled or priced until its standing notice period has fully elapsed. - **Mathematical Statement**: - $$\text{priceable\_at} = \text{closed\_at} + \text{notice}$$ - $$\text{fulfill\_epoch}(\text{epoch}) \implies \text{ledger.timestamp} \ge \text{priceable\_at}$$ + ```math + \text{priceable\_at} = \text{closed\_at} + \text{notice} + ``` + ```math + \text{fulfill\_epoch}(\text{epoch}) \implies \text{ledger.timestamp} \ge \text{priceable\_at} + ``` - **Testable Property**: Invocations of `fulfill_epoch` before `priceable_at` are rejected with `NoticeNotElapsed`. Changing the notice period via `set_notice` applies only to future epochs and never shortens the notice of an already closed epoch. ### Invariant 3: Post-Close Valuation Timing - **Definition**: An epoch is never priced against a valuation accepted before that epoch closed. - **Mathematical Statement**: - $$\text{attested\_at} \ge \text{closed\_at}$$ + ```math + \text{attested\_at} \ge \text{closed\_at} + ``` - **Testable Property**: If the latest oracle attestation timestamp precedes `closed_at`, `fulfill_epoch` is rejected with `AttestationBeforeClose`. A valuation accepted in the exact closing ledger timestamp or later is accepted. ### Invariant 4: Covered Claims Always Pay (Exit Guarantee) @@ -62,25 +74,35 @@ The contracts enforce a set of mathematical and state-machine invariants across ### Invariant 7: Directional Rounding & Non-Creation of Value - **Definition**: Arithmetic conversions round in the vault's favor, preventing arbitrage and value creation from rounding residue. - **Mathematical Statement**: - $$\text{assets\_to\_shares}(a) = \lfloor (a \cdot \text{SCALE}) / \text{NAV} \rfloor$$ - $$\text{shares\_to\_assets}(s) = \lfloor (s \cdot \text{NAV}) / \text{SCALE} \rfloor$$ - $$\text{assets\_to\_shares}(\text{shares\_to\_assets}(s)) \le s$$ -- **Testable Property**: For all values of $a, s \in [1, 10^{30}]$ and $\text{NAV} \in [\text{min\_answer}, \text{max\_answer}]$, a round-trip conversion never creates value. Remainder satisfies: - $$(a \cdot \text{SCALE}) - (s \cdot \text{NAV}) < \text{NAV}$$ + ```math + \text{assets\_to\_shares}(a) = \lfloor (a \cdot \text{SCALE}) / \text{NAV} \rfloor + ``` + ```math + \text{shares\_to\_assets}(s) = \lfloor (s \cdot \text{NAV}) / \text{SCALE} \rfloor + ``` + ```math + \text{assets\_to\_shares}(\text{shares\_to\_assets}(s)) \le s + ``` +- **Testable Property**: For all values of $`a, s \in [1, 10^{30}]`$ and $`\text{NAV} \in [\text{min\_answer}, \text{max\_answer}]`$, a round-trip conversion never creates value. Remainder satisfies: + ```math + (a \cdot \text{SCALE}) - (s \cdot \text{NAV}) < \text{NAV} + ``` ### Invariant 8: Bounded Governance Timelocks - **Definition**: Upgrades and wind-downs cannot execute without advance notice, and delays cannot be set to invalid boundaries. - **Testable Property**: - - Upgrade delay $\in [7 \text{ days}, 90 \text{ days}]$ and $\text{delay} \ge \text{notice}$. - - Wind-down delay $\le 90 \text{ days}$. - - Applying an upgrade before $\text{proposed\_time} + \text{delay}$ reverts with `UpgradeDelayNotElapsed`. + - Upgrade delay $`\in [7 \text{ days}, 90 \text{ days}]`$ and $`\text{delay} \ge \text{notice}`$. + - Wind-down delay $`\le 90 \text{ days}`$. + - Applying an upgrade before $`\text{proposed\_time} + \text{delay}`$ reverts with `UpgradeDelayNotElapsed`. - Pausing freezes the upgrade timelock clock and pushes the ETA by the duration paused. - Renouncing admin is permanently refused (`AdminRequired`). ### Invariant 9: Wind-Down Pro-Rata Solvency - **Definition**: In an active wind-down, total round payouts across all share claims can never exceed the capital credited to that round. - **Mathematical Statement**: - $$\sum_{i} \text{payout}_i \le \text{round\_assets}$$ + ```math + \sum_{i} \text{payout}_i \le \text{round\_assets} + ``` - **Testable Property**: In any distribution round with arbitrary share distributions and rounding remainders, the vault remains solvent for the last claimant. Active wind-down is strictly irreversible. --- @@ -104,12 +126,12 @@ Deploying the Strata Vault Kit involves five contracts configured via `environme | **`nav_oracle`** | `admin` | `Address` | Oracle admin multisig (Governance) | `nav_oracle.constructor_args` | | **`nav_oracle`** | `attester` | `Address` | Authorized reporter multisig for NAV attestations | `nav_oracle.constructor_args` | | **`nav_oracle`** | `guardian` | `Address` | Guardian multisig authorized to raise ripcord | `nav_oracle.constructor_args` | -| **`nav_oracle`** | `config.freshness_duration` | `u64` (seconds) | Validity window of an attestation before it is stale ($> 0$) | `nav_oracle.constructor_args` | +| **`nav_oracle`** | `config.freshness_duration` | `u64` (seconds) | Validity window of an attestation before it is stale ($`> 0`$) | `nav_oracle.constructor_args` | | **`nav_oracle`** | `config.cooldown_secs` | `u64` (seconds) | Minimum time between consecutive price attestations | `nav_oracle.constructor_args` | -| **`nav_oracle`** | `config.max_up_bps` | `u32` (basis points) | Maximum allowable upward price jump (1 bps = 0.01%, $> 0$) | `nav_oracle.constructor_args` | +| **`nav_oracle`** | `config.max_up_bps` | `u32` (basis points) | Maximum allowable upward price jump (1 bps = 0.01%, $`> 0`$) | `nav_oracle.constructor_args` | | **`nav_oracle`** | `config.max_down_bps` | `Option` (bps) | Maximum allowable downward jump (`null` = loss of any size allowed) | `nav_oracle.constructor_args` | | **`nav_oracle`** | `config.min_answer` | `i128` (18 decimals) | Absolute floor price per share (cannot be zero or negative) | `nav_oracle.constructor_args` | -| **`nav_oracle`** | `config.max_answer` | `i128` (18 decimals) | Absolute ceiling price per share ($\ge \text{min\_answer}$) | `nav_oracle.constructor_args` | +| **`nav_oracle`** | `config.max_answer` | `i128` (18 decimals) | Absolute ceiling price per share ($`\ge \text{min\_answer}`$) | `nav_oracle.constructor_args` | | **`async_vault`** | `asset` | `Address` | Settlement asset SAC contract address (e.g. USDC) | `async_vault.constructor_args` | | **`async_vault`** | `share_token` | `Address` | Deployed share token contract address | `async_vault.constructor_args` | | **`async_vault`** | `oracle` | `Address` | Deployed NAV oracle contract address | `async_vault.constructor_args` | @@ -133,11 +155,11 @@ The `async_vault` constructor strictly verifies pairwise separation across autho | Parameter | Method | Authority | Constraints & Defaults | |---|---|---|---| -| **Standing Notice** | `set_notice(secs: u64)` | Governance | Notice wait before pricing. Default: `0`. Must satisfy $\text{secs} \le \text{upgrade\_delay}$ and $\text{secs} \le 30 \text{ days}$ (`MAX_NOTICE_SECS`). | +| **Standing Notice** | `set_notice(secs: u64)` | Governance | Notice wait before pricing. Default: `0`. Must satisfy $`\text{secs} \le \text{upgrade\_delay}`$ and $`\text{secs} \le 30 \text{ days}`$ (`MAX_NOTICE_SECS`). | | **Custodian Address** | `set_custodian(custodian: Address)` | Governance | Recipient address for off-chain capital deployment. Required before `deploy_to_custodian`. | | **Deposit Cap** | `set_deposit_cap(cap: Option)` | Governance | Maximum capacity for deposited capital. `None` = unbounded. Refuses negative cap. | | **Wind-Down Delay** | `set_wind_down_delay(secs: u64)` | Governance | Minimum notice before wind-down activation. Default: `0`. Capped at 90 days (`MAX_WIND_DOWN_DELAY`). | -| **Upgrade Delay** | `propose_upgrade_delay(secs: u64)` | Governance | Timelock delay for wasm upgrades. Must be $\ge 7 \text{ days}$, $\le 90 \text{ days}$, and $\ge \text{notice}$. | +| **Upgrade Delay** | `propose_upgrade_delay(secs: u64)` | Governance | Timelock delay for wasm upgrades. Must be $`\ge 7 \text{ days}`$, $`\le 90 \text{ days}`$, and $`\ge \text{notice}`$. | | **Oracle Configuration** | `set_config(config: OracleConfig)` | Governance | Updates oracle parameters. Follows same validation rules as constructor. | --- From 401d3bbef3ae55e40b1a821f6e973b7492dfad0f Mon Sep 17 00:00:00 2001 From: Pablo Ragalli Date: Thu, 22 Oct 2026 09:15:10 -0300 Subject: [PATCH 3/4] wip: math test --- docs/_math-test.md | 56 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 docs/_math-test.md diff --git a/docs/_math-test.md b/docs/_math-test.md new file mode 100644 index 00000000..ac8c70b3 --- /dev/null +++ b/docs/_math-test.md @@ -0,0 +1,56 @@ +# math test + +A top-level fence, escaped underscore: + +```math +\text{a\_b} = 1 +``` + +B top-level fence, double backslash: + +```math +\text{a\\_b} = 1 +``` + +C top-level dollar block: + +$$\text{a\_b} = 1$$ + +D inline-backtick form alone on a line: + +$`\text{a\_b} = 1`$ + +E fence with mathrm: + +```math +\mathrm{a\_b} = 1 +``` + +F fence with textunderscore: + +```math +\text{a\textunderscore b} = 1 +``` + +G fence with plain spaces: + +```math +\text{a b} = 1 +``` + +H fence without text wrapper: + +```math +a\_b = 1 +``` + +- nested list fence escaped: + ```math + \text{a\_b} = 1 + ``` +- nested list fence textunderscore: + ```math + \text{a\textunderscore b} = 1 + ``` +- nested list inline form: + $`\text{a\_b} = 1`$ From 441e7d1f1b776f1c6ea411b6499e006fbbf99f7e Mon Sep 17 00:00:00 2001 From: Pablo Ragalli Date: Thu, 22 Oct 2026 09:16:05 -0300 Subject: [PATCH 4/4] docs: render kit spec formulas inline in lists --- docs/_math-test.md | 56 ---------------------------------------------- docs/kit-spec.md | 49 +++++++++++++--------------------------- 2 files changed, 16 insertions(+), 89 deletions(-) delete mode 100644 docs/_math-test.md diff --git a/docs/_math-test.md b/docs/_math-test.md deleted file mode 100644 index ac8c70b3..00000000 --- a/docs/_math-test.md +++ /dev/null @@ -1,56 +0,0 @@ -# math test - -A top-level fence, escaped underscore: - -```math -\text{a\_b} = 1 -``` - -B top-level fence, double backslash: - -```math -\text{a\\_b} = 1 -``` - -C top-level dollar block: - -$$\text{a\_b} = 1$$ - -D inline-backtick form alone on a line: - -$`\text{a\_b} = 1`$ - -E fence with mathrm: - -```math -\mathrm{a\_b} = 1 -``` - -F fence with textunderscore: - -```math -\text{a\textunderscore b} = 1 -``` - -G fence with plain spaces: - -```math -\text{a b} = 1 -``` - -H fence without text wrapper: - -```math -a\_b = 1 -``` - -- nested list fence escaped: - ```math - \text{a\_b} = 1 - ``` -- nested list fence textunderscore: - ```math - \text{a\textunderscore b} = 1 - ``` -- nested list inline form: - $`\text{a\_b} = 1`$ diff --git a/docs/kit-spec.md b/docs/kit-spec.md index b8c05fea..80ce0d84 100644 --- a/docs/kit-spec.md +++ b/docs/kit-spec.md @@ -16,35 +16,26 @@ The contracts enforce a set of mathematical and state-machine invariants across ### Invariant 1: Escrow Stays, Only Free Reserve Moves - **Definition**: Cancellable subscription escrow never leaves the vault, and only the free reserve can move to the custodian. Priced redemption liabilities (`committed`) may exceed the liquid reserve; the shortfall is reported as `uncovered`, not refused. Here $`\text{held}`$ is the vault's balance of the settlement asset. - **Mathematical Statement**: - ```math - \text{liquid\_reserve} = \text{held} - \text{cancellable\_escrow} - ``` - ```math - \text{free\_reserve} = \max(\text{liquid\_reserve} - \text{committed} - \text{wind\_down\_owed}, 0) - ``` - ```math - \text{uncovered} = \max(\text{committed} - \text{liquid\_reserve}, 0) - ``` + $`\text{liquid\_reserve} = \text{held} - \text{cancellable\_escrow}`$ + + $`\text{free\_reserve} = \max(\text{liquid\_reserve} - \text{committed} - \text{wind\_down\_owed}, 0)`$ + + $`\text{uncovered} = \max(\text{committed} - \text{liquid\_reserve}, 0)`$ - **Testable Property**: `deploy_to_custodian(assets)` is refused with `ReserveCommittedToExits` when $`\text{assets} > \text{free\_reserve}`$, so after every operation $`\text{held} \ge \text{cancellable\_escrow}`$. While $`\text{uncovered} > 0`$, the free reserve is zero and nothing leaves for the custodian. - **Enforcement**: `deploy_to_custodian` is the only outbound path to the custodian, and it moves at most the free reserve. ### Invariant 2: Notice Period Respected - **Definition**: An epoch cannot be fulfilled or priced until its standing notice period has fully elapsed. - **Mathematical Statement**: - ```math - \text{priceable\_at} = \text{closed\_at} + \text{notice} - ``` - ```math - \text{fulfill\_epoch}(\text{epoch}) \implies \text{ledger.timestamp} \ge \text{priceable\_at} - ``` + $`\text{priceable\_at} = \text{closed\_at} + \text{notice}`$ + + $`\text{fulfill\_epoch}(\text{epoch}) \implies \text{ledger.timestamp} \ge \text{priceable\_at}`$ - **Testable Property**: Invocations of `fulfill_epoch` before `priceable_at` are rejected with `NoticeNotElapsed`. Changing the notice period via `set_notice` applies only to future epochs and never shortens the notice of an already closed epoch. ### Invariant 3: Post-Close Valuation Timing - **Definition**: An epoch is never priced against a valuation accepted before that epoch closed. - **Mathematical Statement**: - ```math - \text{attested\_at} \ge \text{closed\_at} - ``` + $`\text{attested\_at} \ge \text{closed\_at}`$ - **Testable Property**: If the latest oracle attestation timestamp precedes `closed_at`, `fulfill_epoch` is rejected with `AttestationBeforeClose`. A valuation accepted in the exact closing ledger timestamp or later is accepted. ### Invariant 4: Covered Claims Always Pay (Exit Guarantee) @@ -74,19 +65,13 @@ The contracts enforce a set of mathematical and state-machine invariants across ### Invariant 7: Directional Rounding & Non-Creation of Value - **Definition**: Arithmetic conversions round in the vault's favor, preventing arbitrage and value creation from rounding residue. - **Mathematical Statement**: - ```math - \text{assets\_to\_shares}(a) = \lfloor (a \cdot \text{SCALE}) / \text{NAV} \rfloor - ``` - ```math - \text{shares\_to\_assets}(s) = \lfloor (s \cdot \text{NAV}) / \text{SCALE} \rfloor - ``` - ```math - \text{assets\_to\_shares}(\text{shares\_to\_assets}(s)) \le s - ``` + $`\text{assets\_to\_shares}(a) = \lfloor (a \cdot \text{SCALE}) / \text{NAV} \rfloor`$ + + $`\text{shares\_to\_assets}(s) = \lfloor (s \cdot \text{NAV}) / \text{SCALE} \rfloor`$ + + $`\text{assets\_to\_shares}(\text{shares\_to\_assets}(s)) \le s`$ - **Testable Property**: For all values of $`a, s \in [1, 10^{30}]`$ and $`\text{NAV} \in [\text{min\_answer}, \text{max\_answer}]`$, a round-trip conversion never creates value. Remainder satisfies: - ```math - (a \cdot \text{SCALE}) - (s \cdot \text{NAV}) < \text{NAV} - ``` + $`(a \cdot \text{SCALE}) - (s \cdot \text{NAV}) < \text{NAV}`$ ### Invariant 8: Bounded Governance Timelocks - **Definition**: Upgrades and wind-downs cannot execute without advance notice, and delays cannot be set to invalid boundaries. @@ -100,9 +85,7 @@ The contracts enforce a set of mathematical and state-machine invariants across ### Invariant 9: Wind-Down Pro-Rata Solvency - **Definition**: In an active wind-down, total round payouts across all share claims can never exceed the capital credited to that round. - **Mathematical Statement**: - ```math - \sum_{i} \text{payout}_i \le \text{round\_assets} - ``` + $`\sum_{i} \text{payout}_i \le \text{round\_assets}`$ - **Testable Property**: In any distribution round with arbitrary share distributions and rounding remainders, the vault remains solvent for the last claimant. Active wind-down is strictly irreversible. ---