Term Finance TermAuction Clearing Assignment

Invariant

Term Finance lets borrowers and lenders agree on fixed-rate loans through recurring auctions. Borrowers submit the highest rate they are willing to pay. Lenders submit the lowest rate they are willing to accept. The auction chooses one clearing rate for the matched loans and assigns purchase-token principal to both sides.

Why It Matters

The clearing price becomes the fixed interest rate for every matched loan. If a bid below that rate or an offer above that rate were assigned, one side could be forced into a worse rate than it submitted.

The auction also computes maxAssignable: the amount of principal that can be matched between borrowers and lenders at the clearing price. The same cap is passed to the bid assignment loop and the offer assignment loop. If the two sides assigned different purchase-token principal, the repo could become insolvent or leave funds stuck after the auction.

How This Was Modeled and Proven

The benchmark models _assignBids and _assignOffers as pure purchase-token assignment functions. It treats the clearing price and shared cap as outputs of the clearing step and assumes they satisfy the same eligible-demand and eligible-supply capacity relation returned by _calculateClearingPrice.

Scope is deliberate. The model covers successful assignment at purchase-token-principal level. It keeps sorted bid and offer arrays as the real input-boundary hypothesis, although the assignment proof is order-insensitive once the capacity relation is assumed. It does not prove the search loop that finds the clearing point. It also does not prove settlement-level repurchase value, because settlement floors interest and the protocol checks a bounded repo-balance threshold.

The proof status is PROOF for this scoped assignment theorem. The earlier residual-sweep obligations are now discharged by induction over the modeled bid and offer sweeps. The proof shows that the capped sweeps assign exactly maxAssignable when eligible demand and supply cover that cap, and that every positive assignment came from a branch whose price guard was true.

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.TermFinance.TermAuctionClearing.Proofs

Assumptions

The residual-sweep totals and rate guards are proved in Lean. The remaining assumptions are the protocol boundary conditions and scoped exclusions that define this assignment theorem.

• SortedAscendingBidsmerged bid array is ascending by price

  TermAuctionBidLocker input boundary

  TermAuction assumes sorted input. The locker validates revealed bid order, and this benchmark treats the merged assignment array as sorted. The current assignment theorem does not consume this order after clearing capacity is assumed, but it remains part of the production input boundary.

• SortedAscendingOffersmerged offer array is ascending by price

  TermAuctionOfferLocker input boundary

  TermAuction assumes sorted input. The locker validates revealed offer order, and this benchmark treats the merged assignment array as sorted. The current assignment theorem does not consume this order after clearing capacity is assumed, but it remains part of the production input boundary.

• ClearingPointCapacitymaxAssignable is covered by eligible demand and supply

  Contract.lean

  The model assumes the clearing step returned a cap no larger than bids with price at least the clearing price and offers with price at most the clearing price. The assignment theorem is proved from this capacity relation; the clearing-price search loop itself is not proved in this case.

• successful assignment pathpostcondition is about non-reverting assignment

  Contract.lean scope

  The benchmark models the successful path of assignment. External calls, events, controller checks, and token transfers are outside this purchase-token assignment slice.

• clearingOffset = 0nonzero clearing offsets are out of scope

  Contract.lean scope

  The benchmark proves the zero-offset assignment slice. It does not model offset-adjusted clearing prices.

• purchase-token principalsettlement-value rounding is out of scope

  Contract.lean scope

  The theorem proves exact equality of assigned principal. It does not prove the downstream bounded balance check after repurchase price rounding.

Learn More

• Term Finance auction documentation
• Pinned TermAuction.sol source
• Term Finance benchmark case