-- Bank facts: organon-* (bank/invariants.json), the rules of the Organon collection's contract
-- (agent/contracts/HarmonicCollection.sol).
-- Machine checked with Lean 4.22.0, core only, no Mathlib (bank/proofs/lean-toolchain).
-- Check it: lean Organon.lean   (the #print axioms lines list only Lean's standard axioms)
/-
ORGANON: what the contract does, stated exactly and proved.

A drop opens with a folder of n pieces in a fixed order, its provenance published before the first mint.
Token ids in the drop run from `first` to `first + size - 1`, and size <= n. At the reveal one offset k is
drawn from a block nobody could know while minting, and token id gets the piece

    piece first k n id = (id - first + k) % n

which is `pieceOf` in the contract, line for line. Proved here, for every offset k:

  * one of one: two tokens of a drop never get the same piece,
  * in the folder: every token gets a piece the folder holds,
  * every piece found: a drop that sells its whole folder gives every piece to exactly one token,
  * the cap: no sequence of drops passes 1,111, and the supply never passes the drops' sizes,
  * the founder's piece: a drop that names its minter is minted by that wallet and no other,
  * every wei burns: over any sequence of mints the contract's balance never moves and every wei paid
    is a wei sent to the venue.

What is not proved here, because it is not a statement about arithmetic: that the reveal block's hash
could not be known while the drop was minting. That is the chain's property, not the contract's.
-/

/-- the reveal: token `id` of a drop starting at `first`, offset `k`, folder of `n` pieces -/
def piece (first k n id : Nat) : Nat := (id - first + k) % n

/-- below twice n, a remainder is the number itself or the number less n -/
theorem mod_of_lt_two (x n : Nat) (h : x < 2 * n) : x % n = x ∧ x < n ∨ x % n = x - n ∧ n ≤ x := by
  by_cases hx : x < n
  · exact Or.inl ⟨Nat.mod_eq_of_lt hx, hx⟩
  · have hn : n ≤ x := Nat.le_of_not_lt hx
    refine Or.inr ⟨?_, hn⟩
    rw [Nat.mod_eq_sub_mod hn]
    exact Nat.mod_eq_of_lt (by omega)

/-- adding the same offset and taking the same remainder never sends two places below n to one -/
theorem shift_injective (n k i j : Nat) (hi : i < n) (hj : j < n)
    (h : (i + k) % n = (j + k) % n) : i = j := by
  have hn : 0 < n := Nat.lt_of_le_of_lt (Nat.zero_le i) hi
  have hk : k % n < n := Nat.mod_lt k hn
  have ei : (i + k) % n = (i + k % n) % n := by
    rw [Nat.add_mod i k n, Nat.mod_eq_of_lt hi]
  have ej : (j + k) % n = (j + k % n) % n := by
    rw [Nat.add_mod j k n, Nat.mod_eq_of_lt hj]
  rw [ei, ej] at h
  have ri := mod_of_lt_two (i + k % n) n (by omega)
  have rj := mod_of_lt_two (j + k % n) n (by omega)
  omega

/-- ONE OF ONE: two tokens of the same drop never get the same piece, whatever the offset -/
theorem one_of_one (first size n k a b : Nat) (hsize : size ≤ n)
    (ha : first ≤ a ∧ a < first + size) (hb : first ≤ b ∧ b < first + size)
    (h : piece first k n a = piece first k n b) : a = b := by
  unfold piece at h
  have := shift_injective n k (a - first) (b - first) (by omega) (by omega) h
  omega

/-- IN THE FOLDER: every token of a drop gets a piece the folder holds -/
theorem in_folder (first k n id : Nat) (hn : 0 < n) : piece first k n id < n := by
  unfold piece
  exact Nat.mod_lt _ hn

/-- EVERY PIECE FOUND: when a drop sells its whole folder, every piece goes to some token of the drop -/
theorem every_piece_found (first k n p : Nat) (hp : p < n) :
    ∃ id, first ≤ id ∧ id < first + n ∧ piece first k n id = p := by
  have hn : 0 < n := Nat.lt_of_le_of_lt (Nat.zero_le p) hp
  have hk : k % n < n := Nat.mod_lt k hn
  refine ⟨first + (p + (n - k % n)) % n, by omega, ?_, ?_⟩
  · have := Nat.mod_lt (p + (n - k % n)) hn
    omega
  · unfold piece
    rw [Nat.add_sub_cancel_left, Nat.mod_add_mod]
    have hdk := Nat.div_add_mod k n
    have e : p + (n - k % n) + k = p + n * (k / n + 1) := by
      rw [Nat.mul_succ]
      omega
    rw [e, Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hp]

/-- and so, with one of one, a drop that sells its whole folder gives every piece to exactly one token -/
theorem exactly_one (first k n p : Nat) (hp : p < n) :
    ∃ id, (first ≤ id ∧ id < first + n ∧ piece first k n id = p) ∧
      ∀ id', first ≤ id' → id' < first + n → piece first k n id' = p → id' = id := by
  obtain ⟨id, h1, h2, h3⟩ := every_piece_found first k n p hp
  refine ⟨id, ⟨h1, h2, h3⟩, ?_⟩
  intro id' g1 g2 g3
  exact one_of_one first n n k id' id (Nat.le_refl n) ⟨g1, g2⟩ ⟨h1, h2⟩ (by rw [g3, h3])

/-- the cap: `openDrop` refuses any drop that would take the drops past 1,111 -/
def MAX_SUPPLY : Nat := 1111

def openAll : Nat → List Nat → Option Nat
  | t, [] => some t
  | t, s :: ss => if t + s ≤ MAX_SUPPLY then openAll (t + s) ss else none

/-- THE CAP: however many drops open, in whatever sizes, the drops never hold more than 1,111 -/
theorem cap (sizes : List Nat) (t r : Nat) (h0 : t ≤ MAX_SUPPLY) (h : openAll t sizes = some r) :
    r ≤ MAX_SUPPLY := by
  induction sizes generalizing t with
  | nil => simp [openAll] at h; omega
  | cons s ss ih =>
    simp only [openAll] at h
    split at h
    · exact ih (t + s) (by assumption) h
    · cases h

/-- the minted count of each drop, beside its size; `mint` refuses to pass a drop's size -/
def sumMinted : List (Nat × Nat) → Nat
  | [] => 0
  | (_, m) :: ds => m + sumMinted ds

def sumSize : List (Nat × Nat) → Nat
  | [] => 0
  | (s, _) :: ds => s + sumSize ds

def allWithin : List (Nat × Nat) → Prop
  | [] => True
  | (s, m) :: ds => m ≤ s ∧ allWithin ds

/-- THE SUPPLY: the tokens that exist never pass the drops' sizes, and so never pass 1,111 -/
theorem supply_le (ds : List (Nat × Nat)) (h : allWithin ds) : sumMinted ds ≤ sumSize ds := by
  induction ds with
  | nil => simp [sumMinted, sumSize]
  | cons d ds ih =>
    obtain ⟨s, m⟩ := d
    simp only [allWithin] at h
    simp only [sumMinted, sumSize]
    have := ih h.2
    omega

theorem supply_capped (ds : List (Nat × Nat)) (h : allWithin ds)
    (hcap : openAll 0 (ds.map Prod.fst) = some (sumSize ds)) : sumMinted ds ≤ MAX_SUPPLY :=
  Nat.le_trans (supply_le ds h) (cap _ 0 _ (by decide) hcap)

/-- the founder's piece: `mint` takes a reserved drop's minter (zero when the drop is open to all) -/
def mayMint (minter sender : Nat) : Prop := minter = 0 ∨ sender = minter

/-- THE FOUNDER'S PIECE: a drop that names its minter is minted by that wallet and by no other -/
theorem reserved_only (minter sender : Nat) (hr : minter ≠ 0) (h : mayMint minter sender) :
    sender = minter := by
  unfold mayMint at h
  cases h with
  | inl h0 => exact absurd h0 hr
  | inr hs => exact hs

/-- the contract's ETH and its two counters across a mint of value v: all of v goes to the venue
    (`venue.call{value: amountIn}` with amountIn = msg.value), and `mint` refuses to end holding more than
    it began with -/
structure Books where
  balance : Nat  -- the contract's ETH
  paid : Nat     -- totalPaid
  sent : Nat     -- ETH the venue received from the contract

def mintStep (b : Books) (v : Nat) : Books :=
  { balance := b.balance + v - v, paid := b.paid + v, sent := b.sent + v }

/-- EVERY WEI BURNS: over any sequence of mints the contract's balance never moves, and every wei
    paid is a wei sent to the venue to buy the coin it burns -/
theorem every_wei_burns (vs : List Nat) (b : Books) :
    (vs.foldl mintStep b).balance = b.balance ∧
      (vs.foldl mintStep b).paid - b.paid = (vs.foldl mintStep b).sent - b.sent ∧
      b.paid ≤ (vs.foldl mintStep b).paid ∧ b.sent ≤ (vs.foldl mintStep b).sent := by
  induction vs generalizing b with
  | nil => simp
  | cons v vs ih =>
    simp only [List.foldl]
    have := ih (mintStep b v)
    simp only [mintStep] at this ⊢
    omega

#print axioms shift_injective
#print axioms one_of_one
#print axioms in_folder
#print axioms every_piece_found
#print axioms exactly_one
#print axioms cap
#print axioms supply_le
#print axioms supply_capped
#print axioms reserved_only
#print axioms every_wei_burns