import Mathlib.Data.Int.Basic
import Lean.Elab.Tactic.Omega

/-! Independent auction specification. No Yul, compiler, or EVM imports. -/
namespace Vickrey

inductive Player | zero | one deriving DecidableEq, Repr

/-- The on-chain domain is unsigned 128-bit integers, embedded in Nat. -/
def bidLimit : Nat := 2 ^ 128
abbrev Bid := Fin bidLimit

structure Outcome where
  winner : Player
  price : Nat
  deriving DecidableEq, Repr

/-- Fixed tie-breaking in favour of participant zero. -/
def auction (b₀ b₁ : Nat) : Outcome :=
  if b₁ ≤ b₀ then ⟨.zero, b₁⟩ else ⟨.one, b₀⟩

def allocation (o : Outcome) (i : Player) : Nat := if o.winner = i then 1 else 0
def payment (o : Outcome) (i : Player) : Nat := if o.winner = i then o.price else 0

/-- Quasilinear utility uses Int, so overbidding can yield negative utility. -/
def utility (o : Outcome) (i : Player) (value : Nat) : Int :=
  (if o.winner = i then (value : Int) else 0) - (payment o i : Int)

def ownOutcome (i : Player) (own rival : Nat) : Outcome :=
  match i with
  | .zero => auction own rival
  | .one => auction rival own

def revenue (o : Outcome) : Int := o.price
def transfer (o : Outcome) (i : Player) : Int := -(payment o i : Int)
def welfare (o : Outcome) (v₀ v₁ : Nat) : Nat :=
  match o.winner with | .zero => v₀ | .one => v₁

def firstPriceUtility₀ (value own rival : Nat) : Int :=
  if rival ≤ own then (value : Int) - (own : Int) else 0

end Vickrey