Hypernova Settled Payout Safety
When a valid settled payout succeeds, the trader receives no more USDC than the requested gross amount. The same gross amount leaves account equity, the account stays at or above its starting equity, the withdrawal closes, and the signed nonce is consumed once.
Hypernova is a funded-trading platform that records its assessment and funded accounts, account rules, equity updates, and payouts on Arbitrum. A trader who passes an assessment receives a separate funded-account record. Once that account is flat and its equity is settled, it can become eligible for a profit payout.
This proof starts at that payout boundary. It covers one successful on-chain transition for one settled funded account: requestPayout validates the signed request and advances its nonce; _executePayout checks the settled-profit conditions, debits the gross amount, and calls the Vault; and processPayout applies the split and transfers native USDC to the trader. It does not prove how trading results or settlement equity were produced.
Why It Matters
A payout crosses an authorization boundary and two contracts. The signed gross amount must stay within settled profit. The account must lose exactly that gross amount, while the trader receives only the split-adjusted share. A mismatch could overpay the trader, reduce the funded account below its initial equity, or leave the same settlement open for another withdrawal.
The unit at risk is six-decimal Arbitrum USDC held by Hypernova's Vault. Traders depend on the credited amount matching the Vault debit. Hypernova depends on the shared signed nonce advancing once and the withdrawal flag closing after success. The proof also establishes that the trader's USDC transfer cannot exceed the authorized gross request. It does not claim that the event-only protocol share is separately reserved.
How This Was Modeled and Proven
We translated the deployed TradingAccounts payout path and the wired Vault into Verity. The model preserves the nested trader and funded-account storage key, the relevant account fields, deadline and EIP-712 fields, shared nonce increment, branch order, Solidity checked arithmetic, Vault caller check, basis-point clamp, floor division, and exact modeled native-USDC balance updates.
The main proof unfolds the complete requestPayout → _executePayout → processPayout transition. It proves storage-frame facts for the nested account words, derives the split bound instead of assuming it, and checks the post-state conjunction in settledPayoutSafety. A companion arithmetic proof shows that the clamped split cannot pay more than the gross request, including Uint256 modular multiplication and floor division.
Scope
Covered: requestPayout, _executePayout, processPayout, the exact signed fields and consumed nonce, relevant account storage, verified two-way TradingAccounts and Vault wiring, the configured payout domain, checked split arithmetic, one successful native-USDC transfer, exact Vault and trader balance deltas, and the modeled transaction boundary.
Model simplification: The model combines relevant TradingAccounts, Vault, and USDC state in disjoint namespaces for one atomic transaction. It keeps only account fields read or written by this path. The whole-word withdrawal flag is equivalent on canonical source-reachable states, where unused padding remains zero.
Scope exclusions: the economic truth of admin-fed equity and off-chain P&L, arbitrary ERC-20 behavior, proxy upgrades, owner-directed Vault rewiring, events, daily caps, flat-position detection, and reserve sufficiency beyond the transferred trader amount. The model computes the event's protocol amount but does not claim a separate protocol balance or transfer.
Proof artifacts
- Contract.lean contains the source-shaped composite transition and explicit cryptographic trust boundaries.
- Specs.lean defines
settledProfit,traderPayoutAmount, the successful request conditions, and the post-state guarantee. - Proofs.lean contains both reference proofs with no proof placeholders.
- Case directory contains the compile target. The complete benchmark change is in pull request 149.
| Function | Theorem | Status |
|---|---|---|
| requestPayout to processPayout | validSettledPayout_is_safe | Proven |
| processPayout split | successfulPayout_never_overpays | Proven |
Verify it yourself
git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark cd ethereum-verification-benchmark git checkout eb0a1326ed4d9bf0824bb5655961c581c9210ba5 lake build Benchmark.Cases.Hypernova.SettledPayoutSafety.Proofs
If the build succeeds, Lean has checked both reference theorems at the pinned benchmark revision under the assumptions listed below.
Hypotheses
The main theorem is proved from the following Lean conditions invalidSettledPayoutRequest. Executions where a guard or checked arithmetic operation fails are outside the proved successful post-state claim.
valid account and settled-profit stateThe user exists, is not suspended, the account is active and settled, equity exceeds initial equity, and the gross request is positive and no greater than settledProfitTradingAccounts successful path
Hypernova's admin-fed state supplies account status, equity, and the one-shot withdrawal flag. The proof treats those on-chain values as the pre-state.
payoutStaticHashOracleValue, payoutDigestOracleValue, payoutEcrecoverOracleValueThe recovered signer for the exact payout tuple, current nonce, pinned domain, and parsed signature words equals the traderThree narrow cryptographic proof-model axioms
The compiler model emits Verity's static hashing, EIP-712 digest, and ecrecover calls. The proof interpreter does not execute their cryptography, so these body-less axioms take every source input explicitly. The theorem does not prove Keccak, ECDSA, collision resistance, injectivity, or Solady signature-byte parsing.
pinnedDeploymentWiringTradingAccounts points to the verified Vault, the Vault immutable points back to the verified proxy, the payout domain is pinned, and the trader is not the VaultVerified Arbitrum deployment boundary
The proof covers the implementation and wiring observed for the deployed Arbitrum contracts. It does not cover a later proxy upgrade or an owner changing the configured Vault.
successful source guards and checked arithmeticThe authorization is unexpired, the Vault is unpaused and sufficiently funded, the request is under the per-transaction cap, and every modeled Uint256 addition, subtraction, and multiplication stays in rangeTradingAccounts and Vault successful path
These are the exact conditions needed to reach the successful post-state. Solidity reverts if one fails. The maximum withdrawal is per transaction, not a daily cap.
transferSucceedsThe pinned native-USDC transfer succeeds and changes the modeled Vault and trader balances by traderPayoutAmountNative USDC model boundary
The proof tracks exact balance deltas for Arbitrum native USDC. It does not model token bytecode, return-data variants, fee-on-transfer behavior, allowances, or unrelated balances.