-- Bank fact: safe-an-unread-balance-is-never-a-zero (bank/invariants.json)
-- Machine checked with Lean 4.22.0, core only, no Mathlib (bank/proofs/lean-toolchain).
-- Check it: lean SafeHeld.lean   (the #print axioms lines list only Lean's standard axioms)
/-
HARMONIC ASSAY (first named SAFE): an unread balance is never a zero.

B is a partial map from wallets to balances (a wallet B sends to `none`
was not read), S the supply, G a group of wallets. `held` is the assay's
holding for the group in basis points: a number only when every wallet
in G was read, and unread (`none`) otherwise.
-/

def sumOf {α : Type} (B : α → Option Nat) : List α → Nat
  | [] => 0
  | w :: ws => (B w).getD 0 + sumOf B ws

def allRead {α : Type} (B : α → Option Nat) : List α → Bool
  | [] => true
  | w :: ws => (B w).isSome && allRead B ws

def held {α : Type} (B : α → Option Nat) (S : Nat) (G : List α) : Option Nat :=
  if allRead B G then some (10000 * sumOf B G / S) else none

theorem allRead_iff {α : Type} (B : α → Option Nat) (G : List α) :
    allRead B G = true ↔ ∀ w ∈ G, (B w).isSome = true := by
  induction G with
  | nil => simp [allRead]
  | cons w ws ih => simp [allRead, ih]

/-- unread exactly when some wallet of the group was not read -/
theorem held_none_iff {α : Type} (B : α → Option Nat) (S : Nat) (G : List α) :
    held B S G = none ↔ ∃ w ∈ G, B w = none := by
  unfold held
  by_cases h : allRead B G = true
  · simp only [h, if_true]
    constructor
    · intro hc; cases hc
    · rintro ⟨w, hw, hn⟩
      have := (allRead_iff B G).1 h w hw
      simp [hn] at this
  · simp only [h]
    constructor
    · intro _
      have : ¬ ∀ w ∈ G, (B w).isSome = true := fun hall => h ((allRead_iff B G).2 hall)
      simp only [Classical.not_forall] at this
      obtain ⟨w, hw, hs⟩ := this
      exact ⟨w, hw, by cases hb : B w <;> simp_all⟩
    · intro _; rfl

/-- the empty group holds nothing, as a number -/
theorem held_nil {α : Type} (B : α → Option Nat) (S : Nat) : held B S ([] : List α) = some 0 := by
  simp [held, allRead, sumOf]

/-- a number, when there is one, is exactly the floored basis points of the sum -/
theorem held_some {α : Type} (B : α → Option Nat) (S : Nat) (G : List α) (h : Nat) :
    held B S G = some h → h = 10000 * sumOf B G / S := by
  unfold held
  split <;> intro e <;> simp_all

/-- and it never exceeds the whole supply when the group holds at most the supply -/
theorem held_le {α : Type} (B : α → Option Nat) (S : Nat) (G : List α) (h : Nat)
    (hsum : sumOf B G ≤ S) : held B S G = some h → h ≤ 10000 := by
  intro e
  rw [held_some B S G h e]
  apply Nat.div_le_of_le_mul
  calc 10000 * sumOf B G ≤ 10000 * S := Nat.mul_le_mul_left _ hsum
    _ = S * 10000 := Nat.mul_comm _ _

#print axioms held_none_iff
#print axioms held_nil
#print axioms held_some
#print axioms held_le