Tydro Position Account Limits and Authority

A successful open or close stays within the user's signed limits and follows the required authorization rules.

View Lean

Tydro lets users open and close leveraged positions on Aave. Users manage positions through separate position accounts that own the collateral and debt, check signed limits, and reject out-of-limit successful results.

Why It Matters

Opening a leveraged position involves a signed instruction, an Aave flash loan, a swap, and the final collateral and debt balances. A bad result could leave the user with too little collateral, too much debt, or a position below the health limit they chose.

Tydro's position account checks the result before it accepts the operation. It prevents the same signed instruction from being used twice and ties each Aave callback to the operation that created it. Only the owner can change eMode, the Aave setting for borrowing against correlated assets, or recover leftover tokens from the account.

How This Was Modeled and Proven

We recreated the account checks that decide whether an open or close may finish. The model covers the user's output, collateral, debt, and health limits, together with the owner, caller, nonce, callback, eMode, and recovery boundaries.

Lean proves that whenever those modeled stages succeed, every checked limit and authority rule holds. The exact source mapping, proof artifacts, and boundaries remain available below without interrupting the main explanation.

Scope

Covered: successful open and close limits, signed intent and nonce authority, one-shot Aave callback context, eMode bounds, and owner-only recovery.

The result applies when the modeled stages succeed. It does not claim that every contract behavior is covered.

Proof artifacts
  • Contract.lean contains the focused source-shaped model and trusted digest and recovery boundaries.
  • Specs.lean states the floor, lifecycle, composition, callback, eMode, and recovery guarantees.
  • Proofs.lean contains the reference proofs, including the two stage-composition theorems.
  • Compile.lean audits the terminal declarations. It reports no project-defined axioms or proof placeholders; the final theorems report only Lean foundational propext and Quot.sound.
  • Case directory and pull request 177 contain the benchmark change.
open limits
open_enforces_signed_floors
Proven
close limits
close_enforces_signed_floors
Proven
lifecycle authority
lifecycle_success_requires_owner_authority
Proven
open uint8 field
open_typed_fields_are_source_bounded
Proven
signed open
signed_open_success_respects_floor_and_authority
Proven
signed close
signed_close_success_respects_floor_and_authority
Proven
Aave callback
callback_success_requires_bound_context
Proven
eMode change
emode_success_requires_owner
Proven
aToken recovery
atoken_recovery_requires_owner
Proven
raw supply recovery
raw_supply_recovery_requires_owner
Proven
raw borrow recovery
raw_borrow_recovery_requires_owner
Proven
Verify it yourself
git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout d98f977b160ab39853aa3bd69562dc0f57944b64
lake build Benchmark.Cases.Tydro.PositionAccountFloorAuthority.Compile

Hypotheses

The guarantees rely on the three boundaries below.

  • cryptography is trustedthe modeled digest and signer recovery match the signed intent

    trusted helpers in Contract.lean

    EIP-712 encoding, Keccak-256, and ECDSA recovery are opaque trusted abstractions. The proofs make no cryptographic correctness claim.

  • Aave and swap results are inputsthe model receives measured amounts, balances, health, and Pool success

    successful-return model

    Aave, token, route, oracle, and Pool results are environment inputs. The proofs do not establish oracle, route, or other external-protocol behavior.

  • model and source correspondencethe Lean model covers the selected guards and modeled state

    public Blockscout source and benchmark scope

    The case makes no liveness, post-transaction health, public-call admission, ABI refinement, Solidity control-flow correspondence, ERC-1167 clone, or bytecode-refinement claim.

Learn More