1delta Caller-Address Integrity

\texttt{erc20\_caller\_spec}(s,s\prime)

erc20_caller_spec
If the ERC20 pull occurrence flag is set in s', the recorded transferFrom source equals outerCallerWord(s).

\;\land\;

\texttt{permit2\_caller\_spec}(s,s\prime)

permit2_caller_spec
If the Permit2 pull occurrence flag is set in s', the recorded Permit2 from argument equals outerCallerWord(s).

\;\land\;

\texttt{v3\_direct\_caller\_spec}(s,s\prime)

v3_direct_caller_spec
If the V3 direct callback pull occurrence flag is set in s', the recorded ERC20 transferFrom source equals outerCallerWord(s).

Every modeled user-fund pull uses the original deltaCompose caller as the source address.

View Lean

1delta is a DeFi transaction composer for routing swaps, token transfers, permits, lending actions, flash loans, and callback continuations through compact calldata batches. This case studies the deployed Ethereum OneDeltaComposerEthereum contract, whose public entrypoint deltaCompose, captures the outer caller and routes the batch through an internal dispatcher.

The verified property is caller-address integrity for user-fund pulls. When a modeled transfer command or callback path calls ERC20 transferFrom or Permit2 transferFrom, the source address must remain the original batch caller, not a callback contract, the composer itself, or an address embedded in calldata.

Why It Matters

A composer contract often has access to powerful allowances. If a nested callback path used the wrong source address, a batch could pull from an unintended account or fail to enforce the allowance owner the user expected. The bug would not look like a balance equation failure; it would be an identity propagation failure.

The verified source makes the intended design explicit: deltaCompose passes msg.sender into _deltaComposeInternal, transfer commands receive a callerAddress parameter, and the modeled callback continuations forward that same identity.

How This Was Modeled and Proven

Verity is LFG Labs' formal-verification framework for translating focused Solidity behavior into Lean 4 models, specs, and machine-checked proofs. Instead of testing a few example transactions, Verity lets us state the property we expect to always hold and ask Lean to verify that the modeled contract logic cannot violate it.

For this 1delta case, we modeled a focused event-log slice of OneDeltaComposerEthereum. The model keeps the Solidity boundary names visible: deltaCompose, _deltaComposeInternal, _transfers, _transferFrom, and _permit2TransferFrom. External ERC20 and Permit2 calls are represented by occurrence flags plus storage slots recording the from word supplied to the call.

The verified property is caller-address integrity: whenever a modeled ERC20, Permit2, or V3 direct callback pull occurs, the recorded source address must equal the original deltaCompose caller.

Scope

Scope is limited to accepted transfer-command paths, flash-loan and swap callback continuations after callback authentication has decoded the intended outer caller, and the V3 direct callback pull shortcut. The model does not prove packed calldata byte parsing, token balances, amounts, receivers, callback authenticity, non-transfer swap and lending internals, or broader transferFrom call sites outside that scope.

Proof artifacts

The public verity-benchmark case includes Contract.lean, Specs.lean, Proofs.lean, and the case directory. The proof set checks the direct ERC20 and Permit2 pulls, the transfer dispatcher layers, callback pull surfaces, and an aggregate harness where every modeled pull occurs.

Function	Theorem	Status
deltaCompose	deltaComposeCallerPreserved	Proven
_transfers	transferPullsUseOriginalCaller	Proven
callback continuations	callbackPullsUseOriginalCaller	Proven

Verify it yourself

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
git checkout onedelta-caller-integrity
lake build Benchmark.Cases.OneDelta.CallerAddressIntegrity.Proofs
python3 scripts/validate_manifests.py

If the build succeeds, Lean has checked the model, spec, proof declarations, and manifest validation for this benchmark case.

Hypotheses

The proofs hold under the modeling assumptions below. Each one names the file where it is recorded.

calldata arrives already decoded
Contract.lean
The model assumes packed calldata is already decoded. The benchmark starts from decoded transfer command ids instead of proving byte-offset parsing. This preserves the caller identity question because the modeled transfer operations do not read their source address from calldata.
token calls are logged, not executed
Specs.lean
External calls are modeled by logging their arguments. ERC20 and Permit2 calls become event-style storage writes that record whether a pull occurred and which from address was supplied.
callback authentication is assumed
phase-1-research.md
Callback authentication is a precondition, not part of the proof. The callback proofs cover identity preservation after the callback layer has validated the pool or lender and decoded the intended outer caller.

Learn More

See the verified deployment source and the public transfer documentation for the operation format.

Kuru V2 Shared Withdrawal Budget

After any batch of ordinary withdrawals, the withdrawal budget drops by exactly what was paid out, whichever accounts or tokens were used.

for

Dromos MetaDEX Allocation Conservation

In the root-ledger model, chain allocations sum to committed voting power.

for

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.

for