-- File: lean/SagaSpec.lean
-- Payment Saga State Machine Specification
-- Agents migrate Express.js source to FastAPI/Python.
-- Task 3: agents must also submit a LEAN proof of no_double_charge.

namespace SagaSpec

-- Payment saga states
inductive SagaState
  | Idle
  | Reserved   -- funds reserved
  | Authorized -- payment authorized
  | Captured   -- payment captured
  | Settled    -- fully settled
  | Compensating  -- rollback in progress
  | Compensated   -- rollback complete
  | Failed
  deriving BEq, Repr, DecidableEq

-- Events that drive state transitions
inductive SagaEvent
  | Reserve
  | Authorize
  | Capture
  | Settle
  | CompensateReserve
  | CompensateAuthorize
  | CompensateCapture
  | Fail
  deriving BEq, Repr, DecidableEq

-- The state machine transition function
-- This is the ground truth for agents to replicate
def transition (s : SagaState) (e : SagaEvent) : SagaState :=
  match s, e with
  | .Idle,          .Reserve             => .Reserved
  | .Reserved,      .Authorize           => .Authorized
  | .Authorized,    .Capture             => .Captured
  | .Captured,      .Settle              => .Settled
  | .Reserved,      .CompensateReserve   => .Compensated
  | .Authorized,    .CompensateAuthorize => .Compensating
  | .Compensating,  .CompensateReserve   => .Compensated
  | .Captured,      .CompensateCapture   => .Compensating
  | _,              .Fail                => .Failed
  | s,              _                    => s   -- invalid events are no-ops

-- A valid payment reaches Settled via the happy path
def happyPath : List SagaEvent :=
  [.Reserve, .Authorize, .Capture, .Settle]

def runSaga (events : List SagaEvent) : SagaState :=
  events.foldl transition .Idle

-- ── Critical safety property ────────────────────────────────────────

-- A payment can only be charged (Captured) once.
-- "Charged" means reaching the Captured or Settled state.
-- Use pattern matching (not ==) to generate clean simp lemmas.
def isCharged (s : SagaState) : Bool :=
  match s with
  | .Captured | .Settled => true
  | _                    => false

-- Once charged, re-sending Capture is a no-op (idempotency)
theorem capture_idempotent (s : SagaState) (h : isCharged s = true) :
    transition s .Capture = s := by
  cases s <;> simp_all [transition, isCharged]

-- The happy path reaches Settled
theorem happy_path_settles :
    runSaga happyPath = .Settled := by
  simp [runSaga, happyPath, transition]

-- From Settled, any non-Fail event leaves you in a charged state
-- (Fail transitions to Failed which is a terminal error, not a double-charge)
theorem no_double_charge_from_settled (e : SagaEvent) (he : e ≠ .Fail) :
    isCharged (transition .Settled e) = true := by
  cases e <;> simp_all [transition, isCharged]

-- ── The theorem agents must prove in Task 3 (30% of score) ──────────
-- After running the happy path, the state is charged exactly once.
-- Agents submit a LEAN proof of this theorem alongside their Python code.
theorem no_double_charge :
    runSaga happyPath = .Settled ∧ isCharged (runSaga happyPath) = true := by
  constructor
  · exact happy_path_settles
  · rw [happy_path_settles]; simp [isCharged]

end SagaSpec