-- Bank fact: mindask-a-paid-answer-settles-only-after-delivery-and-nothing-to-say-releases-the-coin
-- (bank/invariants.json), the rule of the paid answers desk (agent/src/mindask.js, agent/scripts/compute-worker.mjs,
-- agent/contracts/ComputeEscrowV2.sol).
-- Machine checked with Lean 4.22.0, core only, no Mathlib (bank/proofs/lean-toolchain).
-- Check it: lean MindAsk.lean   (the #print axioms lines list only Lean's standard axioms)
/-
PAID ANSWERS: a job's coin reaches the house only after an answer is delivered, and a job the mind has
nothing to say to is released whole to the buyer. Stated exactly and proved.

The escrow holds a paid answer as a job in one of five states, and the only moves are funded to claimed
(the house's machine takes it), claimed to delivered (an answer is stored), delivered to settled (the buyer
accepts, or the hour closes) and claimed to released (the mind has nothing to say). Every path the job can
take from funded is listed by walking those moves, and proved over that list:

  * every path starts at funded and goes on only by the escrow's moves,
  * no path reaches settled without passing through delivered,
  * a path reaches released only from claimed, and never after a delivery, so a delivered answer is never
    undone and an undelivered one never charges,
  * in every state the buyer has paid the whole amount or nothing, never a value between, and
  * the house's income is the fee in the settled state and nothing in every other, so the house earns only
    on delivery.
-/
namespace MindAsk

inductive S where
  | funded | claimed | delivered | settled | released
  deriving DecidableEq, Repr

open S

/-- The escrow's moves for a paid answer. -/
def step : S → List S
  | funded => [claimed]
  | claimed => [delivered, released]
  | delivered => [settled]
  | settled => []
  | released => []

/-- Every path of at most n moves from s: the path that stops here, and each move continued. -/
def paths : Nat → S → List (List S)
  | 0, s => [[s]]
  | n + 1, s => [s] :: ((step s).map (fun t => (paths n t).map (fun p => s :: p))).foldr (· ++ ·) []

/-- Every path of the paid answer from funded. The machine is five states deep, so four moves cover it. -/
def allPaths : List (List S) := paths 4 funded

/-- What the buyer has paid out and not had back, as a share of the amount: whole when settled, nothing elsewhere. -/
def paidShare : S → Nat
  | settled => 1
  | _ => 0

/-- The house's income in a state, with fee f. -/
def house (f : Nat) : S → Nat
  | settled => f
  | _ => 0

/-- The last state of a path. -/
def last : List S → Option S
  | [] => none
  | [s] => some s
  | _ :: rest => last rest

/-- The state before the last. -/
def beforeLast : List S → Option S
  | [] => none
  | [_] => none
  | [s, _] => some s
  | _ :: rest => beforeLast rest

/-- Whether every move on a path is one of the escrow's. -/
def follows : List S → Bool
  | a :: b :: rest => (b ∈ step a) && follows (b :: rest)
  | _ => true

/-- The five paths, listed. -/
theorem allPaths_listed :
    allPaths = [[funded], [funded, claimed], [funded, claimed, delivered], [funded, claimed, delivered, settled], [funded, claimed, released]] := by
  decide

/-- Every path starts at funded and goes on only by the escrow's moves. -/
theorem paths_start_funded_and_follow_moves : ∀ p ∈ allPaths, p.head? = some funded ∧ follows p = true := by
  decide

/-- No path reaches settled without passing through delivered. -/
theorem settled_only_after_delivered : ∀ p ∈ allPaths, last p = some settled → delivered ∈ p := by
  decide

/-- Released is reached only from claimed. -/
theorem released_only_from_claimed : ∀ p ∈ allPaths, last p = some released → beforeLast p = some claimed := by
  decide

/-- A delivered answer is never undone: no path holds both delivered and released. -/
theorem delivered_never_released : ∀ p ∈ allPaths, ¬ (delivered ∈ p ∧ released ∈ p) := by
  decide

/-- In every state the buyer's coin is whole or returned, never a value between. -/
theorem coin_whole_or_returned (a : Nat) : ∀ s : S, paidShare s * a = a ∨ paidShare s * a = 0 := by
  intro s
  cases s <;> simp [paidShare]

/-- The house is paid only in the settled state. -/
theorem house_paid_only_when_settled (f : Nat) : ∀ s : S, house f s ≠ 0 → s = settled := by
  intro s h
  cases s <;> simp [house] at h <;> rfl

/-- And in that state it is paid the fee, while a released job pays it nothing and returns the coin. -/
theorem settled_pays_fee (f : Nat) : house f settled = f := rfl
theorem released_pays_nothing (f : Nat) : house f released = 0 ∧ paidShare released = 0 := ⟨rfl, rfl⟩

end MindAsk

#print axioms MindAsk.allPaths_listed
#print axioms MindAsk.paths_start_funded_and_follow_moves
#print axioms MindAsk.settled_only_after_delivered
#print axioms MindAsk.released_only_from_claimed
#print axioms MindAsk.delivered_never_released
#print axioms MindAsk.coin_whole_or_returned
#print axioms MindAsk.house_paid_only_when_settled
#print axioms MindAsk.settled_pays_fee
#print axioms MindAsk.released_pays_nothing