1delta Caller-Address Integrity

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 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.

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.

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

Assumptions

• decoded commandspacked calldata is already decoded

  Contract.lean

  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.

• external callscall arguments are logged

  Specs.lean

  ERC20 and Permit2 calls are modeled by event-style storage writes that record whether a pull occurred and which from address was supplied.

• callbacksauthentication is preconditioned

  phase-1-research.md

  The callback proofs cover identity preservation after the callback layer has validated the pool or lender and decoded the intended outer caller.