mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekay
6907bfc6e6
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning.
62 lines
1.8 KiB
Lean4
62 lines
1.8 KiB
Lean4
/-
|
|
Flash Loan Safety
|
|
|
|
Atomic borrow-use-repay within a single transaction.
|
|
If repayment fails, entire transaction reverts.
|
|
|
|
Properties:
|
|
- Atomicity: borrow + use + repay in one tx
|
|
- Solvency: pool balance ≥ pre-loan balance after tx
|
|
- Fee accrual: flash loan fee goes to LPs
|
|
- No residual debt: loan is fully repaid or fully reverted
|
|
|
|
Author: Lux Research
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace DeFi.FlashLoan
|
|
|
|
structure LoanState where
|
|
poolBalance : Nat
|
|
feeBps : Nat -- flash loan fee (e.g., 9 = 0.09%)
|
|
|
|
structure FlashLoan where
|
|
amount : Nat
|
|
fee : Nat
|
|
repaid : Bool
|
|
|
|
def executeLoan (s : LoanState) (amount : Nat) (repaid : Bool) : LoanState :=
|
|
if repaid && amount ≤ s.poolBalance then
|
|
let fee := amount * s.feeBps / 10000
|
|
{ s with poolBalance := s.poolBalance + fee } -- pool gains fee
|
|
else s -- revert: no change
|
|
|
|
/-- SOLVENCY: Pool never loses money on flash loans -/
|
|
theorem flash_loan_solvent (s : LoanState) (amount : Nat) (repaid : Bool) :
|
|
(executeLoan s amount repaid).poolBalance ≥ s.poolBalance := by
|
|
unfold executeLoan
|
|
split
|
|
· simp
|
|
· exact le_refl _
|
|
|
|
/-- NO REPAY = NO LOAN: Unreturned loan reverts -/
|
|
theorem no_repay_reverts (s : LoanState) (amount : Nat) :
|
|
executeLoan s amount false = s := by
|
|
simp [executeLoan]
|
|
|
|
/-- FEE ACCRUAL: Successful loan increases pool by fee -/
|
|
theorem fee_accrues (s : LoanState) (amount : Nat)
|
|
(h : amount ≤ s.poolBalance) (_hf : s.feeBps > 0) :
|
|
(executeLoan s amount true).poolBalance ≥ s.poolBalance := by
|
|
simp [executeLoan, h]
|
|
|
|
/-- OVERDRAFT BLOCKED: Can't borrow more than pool has -/
|
|
theorem overdraft_blocked (s : LoanState) (amount : Nat)
|
|
(h : amount > s.poolBalance) :
|
|
executeLoan s amount true = s := by
|
|
simp [executeLoan, Nat.not_le.mpr h]
|
|
|
|
end DeFi.FlashLoan
|