-- Bank fact: rehearsal-a-verdict-flags-only-a-bound-that-was-asked-and-broken
-- Primary implementation: agent/kernels/rehearsal/rehearsal.c (rehearsal_slippage_bps, rehearsal_verdict), mirrored in
-- agent/src/rehearse.js (slippageBps, numericVerdict); the measure is agent/src/rehearse.js (measureOf).
-- Machine checked with Lean 4.22.0, core only, no Mathlib (bank/proofs/lean-toolchain).
-- Check it: lean Rehearsal.lean   (the #print axioms lines list only Lean's standard axioms)
/-
THE REHEARSAL VERDICT: a rehearsed transaction is judged only against the bounds its asker set, and a bound not
asked never fails. Stated exactly and proved.

A rehearsal runs a transaction on the chain's node before it is sent and measures what it would do: what the sender
receives of the token the asker quoted, what it receives of a floored token, what it spends of a capped token, the
largest allowance it leaves behind, and where a Morpho position would sit. The verdict holds those facts to the
asker's own bounds, red or amber, by the rule the C kernel carries (rehearsal.c) and the JavaScript mirrors. Proved
over that rule, for every value of every field:

  * a met quote has no slippage, and slippage is never past 10000 basis points,
  * receiving more of the quoted token never raises the slippage,
  * with no bound asked the verdict is clear, whatever the numbers say,
  * a red verdict names a bound that was asked and broken, one of five, and nothing else, and
  * better facts (more received, less spent, a smaller allowance left, a healthier position, every bound the same)
    never turn a verdict that was not red into a red one.
-/
namespace Rehearsal

/-- Slippage in basis points: 0 when the quote is met, else the shortfall's share of the quote, floored. -/
def slippageBps (got quote : Nat) : Nat :=
  if quote ≤ got then 0 else (quote - got) * 10000 / quote

/-- The facts a rehearsal measures and the bounds an asker set, each judged only where it was asked. -/
structure Facts where
  askQuote : Bool
  got : Nat
  quote : Nat
  maxSlippageBps : Nat
  askMinOut : Bool
  minOutGot : Nat
  minOut : Nat
  askMaxIn : Bool
  maxInSpent : Nat
  maxIn : Nat
  askAllowance : Bool
  allowanceLeft : Nat
  allowanceCap : Nat
  askHealth : Bool
  healthNum : Nat
  healthDen : Nat

/-- The quote missed by 5% or more. -/
def redSlippage (f : Facts) : Bool := f.askQuote && decide (1 ≤ f.quote) && decide (500 ≤ slippageBps f.got f.quote)
/-- The quote missed past the asker's allowance, under 5%. -/
def amberSlippage (f : Facts) : Bool :=
  f.askQuote && decide (1 ≤ f.quote) && decide (slippageBps f.got f.quote < 500) && decide (f.maxSlippageBps < slippageBps f.got f.quote)
def redMinOut (f : Facts) : Bool := f.askMinOut && decide (f.minOutGot < f.minOut)
def redMaxIn (f : Facts) : Bool := f.askMaxIn && decide (f.maxIn < f.maxInSpent)
def redAllowance (f : Facts) : Bool := f.askAllowance && decide (f.allowanceCap < f.allowanceLeft)
/-- A Morpho position under its liquidation floor after the move. -/
def redHealth (f : Facts) : Bool := f.askHealth && decide (f.healthNum < f.healthDen)
/-- A Morpho position above its floor and under 1.05x it. -/
def amberHealth (f : Facts) : Bool :=
  f.askHealth && decide (1 ≤ f.healthDen) && decide (f.healthDen ≤ f.healthNum) && decide (f.healthNum * 10000 / f.healthDen < 10500)

inductive Level where
  | clear | amber | red
  deriving DecidableEq, Repr

def red (f : Facts) : Bool := redSlippage f || redMinOut f || redMaxIn f || redAllowance f || redHealth f
def amber (f : Facts) : Bool := amberSlippage f || amberHealth f
/-- THE VERDICT: red when any red flag stands, amber when any amber flag stands, clear otherwise. -/
def level (f : Facts) : Level := if red f then .red else if amber f then .amber else .clear

/-- The same facts with no bound asked. -/
def nothingAsked (f : Facts) : Facts :=
  { f with askQuote := false, askMinOut := false, askMaxIn := false, askAllowance := false, askHealth := false }

/-- A met quote has no slippage. -/
theorem met_quote_no_slippage (got quote : Nat) (h : quote ≤ got) : slippageBps got quote = 0 := by
  simp [slippageBps, h]

/-- Slippage is never past 10000 basis points. -/
theorem slippage_le_10000 (got quote : Nat) : slippageBps got quote ≤ 10000 := by
  unfold slippageBps
  split
  · exact Nat.zero_le _
  · apply Nat.div_le_of_le_mul
    exact Nat.mul_le_mul_right 10000 (Nat.sub_le quote got)

/-- Receiving more of the quoted token never raises the slippage. -/
theorem more_received_never_more_slippage (got got' quote : Nat) (h : got ≤ got') :
    slippageBps got' quote ≤ slippageBps got quote := by
  unfold slippageBps
  by_cases h1 : quote ≤ got'
  · simp [h1]
  · have h2 : ¬ quote ≤ got := fun hq => h1 (Nat.le_trans hq h)
    simp only [h1, h2, if_false]
    apply Nat.div_le_div_right
    exact Nat.mul_le_mul_right 10000 (Nat.sub_le_sub_left h quote)

/-- With no bound asked the verdict is clear, whatever the numbers say. -/
theorem not_asked_never_fails (f : Facts) : level (nothingAsked f) = .clear := by
  simp [level, red, amber, redSlippage, amberSlippage, redMinOut, redMaxIn, redAllowance, redHealth, amberHealth, nothingAsked]

/-- A red verdict names a bound that was asked and broken: one of five, and nothing else. -/
theorem red_names_a_broken_bound (f : Facts) (h : red f = true) :
    (f.askQuote = true ∧ 1 ≤ f.quote ∧ 500 ≤ slippageBps f.got f.quote) ∨
    (f.askMinOut = true ∧ f.minOutGot < f.minOut) ∨
    (f.askMaxIn = true ∧ f.maxIn < f.maxInSpent) ∨
    (f.askAllowance = true ∧ f.allowanceCap < f.allowanceLeft) ∨
    (f.askHealth = true ∧ f.healthNum < f.healthDen) := by
  simp only [red, redSlippage, redMinOut, redMaxIn, redAllowance, redHealth, Bool.or_eq_true, Bool.and_eq_true,
    decide_eq_true_eq] at h
  rcases h with ((((h | h) | h) | h) | h)
  · exact Or.inl ⟨h.1.1, h.1.2, h.2⟩
  · exact Or.inr (Or.inl h)
  · exact Or.inr (Or.inr (Or.inl h))
  · exact Or.inr (Or.inr (Or.inr (Or.inl h)))
  · exact Or.inr (Or.inr (Or.inr (Or.inr h)))

/-- Better facts: more received, less spent, a smaller allowance left, a healthier position, every bound the same. -/
def better (f g : Facts) : Prop :=
  g.askQuote = f.askQuote ∧ g.quote = f.quote ∧ g.maxSlippageBps = f.maxSlippageBps ∧ f.got ≤ g.got ∧
  g.askMinOut = f.askMinOut ∧ g.minOut = f.minOut ∧ f.minOutGot ≤ g.minOutGot ∧
  g.askMaxIn = f.askMaxIn ∧ g.maxIn = f.maxIn ∧ g.maxInSpent ≤ f.maxInSpent ∧
  g.askAllowance = f.askAllowance ∧ g.allowanceCap = f.allowanceCap ∧ g.allowanceLeft ≤ f.allowanceLeft ∧
  g.askHealth = f.askHealth ∧ g.healthDen = f.healthDen ∧ f.healthNum ≤ g.healthNum

/-- Better facts never turn a verdict that was not red into a red one. -/
theorem better_never_turns_red (f g : Facts) (hb : better f g) (hf : red f = false) : red g = false := by
  obtain ⟨q1, q2, _, q4, m1, m2, m3, x1, x2, x3, a1, a2, a3, h1, h2, h3⟩ := hb
  simp only [red, redSlippage, redMinOut, redMaxIn, redAllowance, redHealth, Bool.or_eq_false_iff, Bool.and_eq_false_iff,
    decide_eq_false_iff_not, Nat.not_le, Nat.not_lt] at hf ⊢
  obtain ⟨⟨⟨⟨s, mo⟩, mi⟩, al⟩, he⟩ := hf
  have slip : slippageBps g.got g.quote ≤ slippageBps f.got f.quote := by
    rw [q2]; exact more_received_never_more_slippage f.got g.got f.quote q4
  refine ⟨⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩, ?_⟩
  · rcases s with (s | s) | s
    · exact Or.inl (Or.inl (by rw [q1]; exact s))
    · exact Or.inl (Or.inr (by rw [q2]; exact s))
    · exact Or.inr (Nat.lt_of_le_of_lt slip s)
  · rcases mo with mo | mo
    · exact Or.inl (by rw [m1]; exact mo)
    · exact Or.inr (by rw [m2]; exact Nat.le_trans mo m3)
  · rcases mi with mi | mi
    · exact Or.inl (by rw [x1]; exact mi)
    · exact Or.inr (by rw [x2]; exact Nat.le_trans x3 mi)
  · rcases al with al | al
    · exact Or.inl (by rw [a1]; exact al)
    · exact Or.inr (by rw [a2]; exact Nat.le_trans a3 al)
  · rcases he with he | he
    · exact Or.inl (by rw [h1]; exact he)
    · exact Or.inr (by rw [h2]; exact Nat.le_trans he h3)

/-- The kernel's own first lines, decided: a quote met is 0, 95 of 100 is 500, nothing of 100 is 10000, 999 of 1000 is 10. -/
theorem the_first_lines :
    slippageBps 100 100 = 0 ∧ slippageBps 95 100 = 500 ∧ slippageBps 0 100 = 10000 ∧ slippageBps 999 1000 = 10 := by
  decide

end Rehearsal

#print axioms Rehearsal.met_quote_no_slippage
#print axioms Rehearsal.slippage_le_10000
#print axioms Rehearsal.more_received_never_more_slippage
#print axioms Rehearsal.not_asked_never_fails
#print axioms Rehearsal.red_names_a_broken_bound
#print axioms Rehearsal.better_never_turns_red
#print axioms Rehearsal.the_first_lines