Enzyme Onyx Dynamic Fee Accounting
Invariant
In a successful settlement with projection-stable tracker callbacks, Onyx credits each returned management and performance fee exactly once. The performance call receives value after prior liabilities and the new management fee are deducted.
Enzyme Onyx is a modular vault system for tokenizing on-chain and off-chain value. Its FeeHandler records fee liabilities in the Shares value asset. This proof covers exact accounting when both dynamic fee trackers return successfully and their callbacks preserve the dynamic-fee accounting projection. It also checks disabled branches, selected failures, transactional rollback, and the selected configuration frame.
Why It Matters
Onyx calculates management fees before performance fees. The performance tracker must receive value after subtracting both fees already owed and the new management fee. Using gross value, or value before the management fee, can overstate performance and charge the vault for value that is already reserved as another liability.
The unit at risk is the Shares value asset accounting unit recorded as owed to fee recipients. If aggregate and per-recipient accounting diverge, vault holders can face misstated liabilities and a fee recipient can be under-credited or over-credited. Sequential writes also matter when management and performance fees use the same recipient. The second write must add to the first, not replace it.
How This Was Modeled and Proven
We translated settleDynamicFeesGivenPositionsValue and its two owed-value update helpers into Verity. The model preserves the nested Shares caller check, both optional tracker branches, management-first ordering, checked Uint256 arithmetic, the total liability slot, and the recipient mapping.
A universally quantified Verity environment supplies arbitrary success and return words for the Shares lookup and both tracker calls. Each oracle query encodes its dynamic target, ABI selector, and argument words. The Shares view lookup is modeled as a static call. Successful tracker calls can transform arbitrary unrelated state, while preserving the two tracker addresses, two recipient addresses, aggregate fees owed, and every per-user owed balance. The proof unfolds the transition, checks each arithmetic condition, and splits on whether the recipients are equal.
Scope
Covered: the Shares valuation-handler lookup, both dynamic trackers, exact external call shapes, prior-fee subtraction, management and performance inputs, successful checked additions, aggregate liability, recipient credits, shared-recipient accumulation, management-only and performance-only paths, a both-trackers-disabled no-op path, rollback after any modeled raw revert, and the selected dynamic-fee configuration frame.
Out of scope: the formulas and storage transitions inside each tracker, source-complete cross-contract reentrancy reachability, tracker trustworthiness, entrance and exit fees, fee claims and token payouts, event logs, configuration changes, and storage-layout collision freedom. A source-complete callback registry is absent; it would need to model setEntranceFee, setExitFee, setFeeAsset, setManagementFee, setPerformanceFee, claimFees, recursive dynamic settlement, entrance settlement, and exit settlement. External calls use Verity.Env oracle responses keyed by success, dynamic target, selector, and arguments. The model represents a successful call as one full return word and does not parse raw returndata. For the valuation-handler lookup, it projects the low 160 bits to an address. This conservatively admits non-canonical words that Solidity ABI decoding would reject. The modeled static lookup does not apply the reentry hook; STATICCALL rules out state-changing reentrant effects. Tracker calls apply the environment's reentry hook under the narrow projection-stability condition above. The model does not execute callee storage.
Proof artifacts
- Contract.lean contains the source-shaped FeeHandler transition and parametric external-call boundaries.
- Specs.lean defines the fee bases, fee amounts, post-management state, and exact settlement property.
- Proofs.lean proves the reference theorem without project-local axioms or proof placeholders.
- Case directory contains the compile target. The benchmark repository also contains the open generated proof task.
| Function | Theorem | Status |
|---|---|---|
| settleDynamicFeesGivenPositionsValue | settleDynamicFeesGivenPositionsValue_exact_accounting | Proven |
Verify it yourself
git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark cd ethereum-verification-benchmark git checkout b331097d08a17bedaa3274b2a5b37d19659b6fe8 lake build Benchmark.Cases.Enzyme.OnyxFeeHandler.Proofs
If the build succeeds, Lean has checked the reference theorem under the conditions listed below.
Assumptions
These conditions define the main successful execution theorem. It covers the path where FeeHandler's checked subtractions and additions all stay in range; if any would fail, Solidity reverts and this exact-success theorem does not apply. The supporting success theorems remain conditional on the authorized valuation-handler lookup and the arithmetic checks used by their branch. Enabled tracker paths also require their exact call and projection-stable callbacks. The both-disabled path needs no reentry assumption because it performs only the static Shares lookup.
hValuationCall, hCaller, and enabled trackersThe Shares lookup succeeds with the exact call shape, its return word authorizes the caller, and both tracker addresses are nonzeroFeeHandler successful path
The theorem follows the source entry gate and the path where both management and performance settlement branches run. It does not claim that disabled trackers accrue fees.
hManagementCall and hPerformanceCallBoth tracker oracle queries succeed and are keyed by the configured target, exact selector, and exact net-value argumentVerity cross-contract boundary
The proof checks how FeeHandler computes inputs and records arbitrary returndata. It does not assume either tracker's fee formula.
arithmetic checks succeedPrior-fee and management subtractions, both recipient additions, and both aggregate additions stay within Uint256Solidity checked arithmetic
FeeHandler first subtracts prior fees and then the management fee. It also adds each returned fee to its recipient balance and the aggregate balance. The theorem covers the successful path where these checks do not underflow or overflow. If any check fails, Solidity reverts and the exact-success theorem does not apply.
supporting branch conditionsAll three supporting paths keep the authorized lookup and the arithmetic checks used on that path; enabled branches also require their successful tracker call and projection-stable callbackSupporting branch theorems
These are conditional success and no-op results, not unconditional claims about every branch execution. The rollback theorem separately covers any execution whose raw modeled result is a revert.
hReentryEach tracker callback preserves both tracker addresses, both recipient addresses, aggregate fees owed, and every per-user owed balanceModel boundary
Verity.Env models arbitrary return data, call shape, and a reentry hook, not callee storage. Unrelated state may change. A conditional ReentrancySpec schedule-closure lemma discharges this condition when the hook is explicitly equated to a registered schedule whose transitions each preserve the projection. The pinned FeeHandler has no reentrancy guard, so proving that every runtime callback is in such a registry still requires deployment and cross-contract role assumptions. Tracker formulas, high-water-mark state, timestamps, ERC-7201 slot hashing, and deployment wiring are not verified here.