KPK Shares Settlement Accounting
A successful kpkShares settlement batch processes each eligible request at most once and accounts exactly for its fees, shares and asset transfers.
KPK manages onchain investment funds. Its kpkShares contract queues subscriptions and redemptions, then lets an operator settle requests at a supplied share price. Subscriptions exchange escrowed assets for shares; redemptions burn net shares and pull assets from the portfolio Safe.
Why It Matters
A batch changes several things at once: fee shares, investor shares, asset balances, allowances and pending-request totals. These must tell the same story. Counting a repeated request twice could mint too many shares or repeat a payout, even if each individual conversion were correct.
If an operator lists the same redemption in both the approved and rejected arrays, the first eligible resolution must make the later occurrence a no-op. The proof establishes this for arbitrary array lengths and repeated IDs, including approvals that expire into rejections. It also accounts for shared addresses, where a transfer to oneself has zero net balance effect but still produces a settlement record.
How This Was Modeled and Proven
A test checks a few batches. A formal proof checks all of them. We worked in three steps.
1. Rebuild the code in Lean. We rewrote kpkShares' processRequests in Lean, a proof language. We kept its checks, order and rounding, and its real token and fee-module calls.
2. Write the rule precisely. At the operator's price, each request resolves at most once, shares minted and burned match the price and the fees, and balances change by exactly the recorded amounts. The rule is in Specs.lean, short enough for a person to read and sign off.
3. Let Lean check it. Lean's kernel is a small program that accepts or rejects proofs. It checks the rule for every successful batch of the model, whatever its size or repeated IDs. A wrong proof would not compile.
The proof adds no custom axioms. The model is our link to the real contract, which is why the first hypothesis below is about it.
| Function | Theorem | Status |
|---|---|---|
| processRequests | settlement_accounting | Proven |
The model, rules and reference proof are in Contract.lean, Specs.lean and Proofs.lean. The theorem states more than the supply equation shown above; its full statement is in Specs.lean. The generated agent tasks keep editable proof holes by design. They are not the solved reference.
Scope
- One full settlement call. Fees, approvals, explicit rejections, expired approvals, skips, both request types and all duplicate occurrences are included. Request intake, cancellation, asset deletion, recovery, administration, upgrades and inherited external share transfers are other entry points with additional state changes. They need separate proofs. Initial escrow coverage is required; lifetime reachability and post-settlement escrow coverage are not established.
- Supplied-price accounting, not fresh NAV. The theorem proves the exact raw-unit conversion at the supplied price, including both checked division stages and minimum-output guards. It does not prove that the price is current, fair or equal to the basket's value. A NAV interpretation would additionally require complete basket value per outstanding share after this batch's fee issuance and before settlement, in the batch asset's units scaled by 1e8. We do not certify that condition.
- Fees accounted for, not economically certified. Management fees precede performance fees. The model proves the exact fee-module inputs, returned issuance, clock updates and external-state replay. A module's watermark policy or economically correct fee amount is outside this proof, as are operator scheduling and cross-currency valuation.
- Static conventional interfaces. Tokens and fee modules have separate modeled target types. Token callbacks, transfer taxes, rebasing and reentry add behavior this interface does not execute. They require separate models. Gas, ABI decoding, revert bytes, logs and physical storage layout are not certified.
- Manual translation. The model uses Verity state and arithmetic infrastructure at the pinned benchmark version. No mechanized Solidity-to-Lean, control-flow, compiler, Yul, EVM or deployed-bytecode refinement is produced.
Verify it yourself
git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark cd ethereum-verification-benchmark git checkout 491fff64fec1506ad18f13e23c0070c88254f1e7 python3 cases/kpk/shares_settlement_accounting/verify.py # Equivalent targets: lake build Benchmark.Cases.KPK.SharesSettlementAccounting.Proofs # and lake build Benchmark.Cases.KPK.SharesSettlementAccounting.Compile
Install the pinned Lean toolchain and dependencies first. The helper checks Proofs, Compile and executable regressions under per-Lean memory limits and target timeouts, using a temporary root configuration without changing dependency pins. The checked environment uses dependency caches; this is not a cold-build, globally serialized Lake-scheduler or aggregate-memory guarantee. The pinned revision is the merge commit of the benchmark pull request.
Source and deployment evidence
The selected source is kpkShares.sol at revision 714d3d66a6e0e2bc7849ae48c3a25f63f23e903f. Retained checks at Ethereum block 26,106,081 on October 2, 2026 matched its relevant source graph to the XAUt Carry and funded WBTC Carry implementations. This is a matching source revision, not proof of a unique original deployment Git commit or their state today.
The source pin records the observation and exact OpenZeppelin dependency gitlinks. Their package version is 5.4.0; this does not assert the audited release commit is used. kUSD and kETH use different dependency bundles and are not included. Source/backend runtime matching does not prove the Lean translation matches deployed bytecode.
Hypotheses
The proof covers one successful batch that starts from a healthy state. It does not cover every state the contract could reach. The price the operator supplies is taken as given, and whether it is fair is outside the proof (see Scope). Exact premises are in Specs.lean and Proofs.lean.
assumption: the Lean model matches the SolidityReal-code applicability
We translated kpkShares into Lean by hand. Lean proves the rules for that translation, but nothing checks the translation against the real code. If they differ in a way that matters for settlement, the result may not apply to the contract.
assumption: tokens behave like standard ERC20sExternal behavior
Each asset token moves exactly the amount requested, with no transfer fees, rebasing or callbacks. The proof treats a token call as a plain balance update, so a token that does anything else is outside it. Fee modules are also assumed not to be tokens.
premise: the starting records are consistent and fundedInitial WellFormed state
Before the batch, the contract's records agree with each other and its escrow is sufficient. Pending subscription totals match the pending requests, the contract holds enough of each token for them, and enough shares for pending redemptions. We prove one batch from such a state, not that the contract always stays in it.
premise: the setup is validInitial WellFormed and ExternalApplicability
The contract starts with real addresses for itself, the Safe and the fee receiver, fee rates of at most 20%, token decimals of at most 36, and numbers within normal ranges. Addresses and request IDs may repeat. The proof handles that.
runtime precondition: the batch succeedsModeled operation guards
The theorem covers a batch that finishes without reverting, at a price below 2^256. If a contract check fails, such as authorization, price deviation, a token transfer or a minimum output, the whole call reverts and nothing changes. This does not assume the price is fresh or that the Safe can pay in the future.