//! Pure, synchronous, deterministic core for the swactor actor framework.
//!
//! This crate contains the decision logic that maps 1:1 to a TLA+ specification.
//! Every public function is a pure function: `fn(inputs) -> output` with no side
//! effects, no IO, no allocation, and no panics.
//!
//! The runtime crate (`swactor`) calls these functions to make decisions; this crate
//! never calls back into the runtime. If you can't trivially transliterate a
//! function's signature into TLA+, it doesn't belong here.

#![no_std]
#![deny(unsafe_code)]

// ─── Actor Lifecycle Phase ───────────────────────────────────────────────────

/// The lifecycle phase of an actor slot.
///
/// Replaces the four boolean fields (`started`, `poisoned`, `stopping`, `suspended`)
/// with a single state machine. Every phase transition goes through
/// [`lifecycle_transition`].
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ActorPhase {
    /// Actor has been inserted into the pool but `on_start` has not been called yet.
    Unstarted,
    /// Actor is running normally — processing messages from its mailbox.
    Running,
    /// Actor is suspended — messages continue to queue but are not processed.
    Suspended,
    /// Actor has been requested to stop gracefully. `on_stop` will be called during cleanup.
    Stopping,
    /// Actor panicked during `on_start` or message handling. No further processing occurs.
    Poisoned,
}

// ─── Stop / Exit Reasons ─────────────────────────────────────────────────────

/// Reason an actor was removed from the runtime.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum StopReason {
    /// Graceful stop (via `ctx.stop_self()` or `Runtime::stop_actor()`).
    Normal,
    /// Actor panicked and could not be restarted.
    Panicked,
    /// Actor stopped with a typed exit value (via `Ctx::stop_with`).
    Completed,
}

/// Why an actor exited — delivered to watchers.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ExitReason {
    /// Actor was explicitly stopped or removed from the pool.
    Stopped,
    /// Actor panicked during message handling.
    Panicked,
    /// The node hosting the actor left the cluster (SWIM Dead).
    NodeDown,
    /// Actor stopped with a typed exit value (via `Ctx::stop_with`).
    Completed,
}

// ─── Mailbox ─────────────────────────────────────────────────────────────────

/// What to do when a bounded mailbox is full.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum MailboxOverflow {
    /// Drop the incoming message (newest). The message is silently discarded.
    DropNewest,
    /// Drop the oldest message in the queue to make room for the new one.
    DropOldest,
}

/// Result of the mailbox capacity check.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum MailboxDecision {
    /// The mailbox has room (or is unbounded). Accept the message.
    Accept,
    /// The mailbox is full and the policy is DropNewest — reject the incoming message.
    RejectNewest,
    /// The mailbox is full and the policy is DropOldest — evict the front of the queue.
    EvictOldest,
}

// ─── Lifecycle Events ────────────────────────────────────────────────────────

/// Events that drive the actor lifecycle state machine.
///
/// Each variant corresponds to a runtime action that may cause a phase transition.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum LifecycleEvent {
    /// `on_start` completed successfully.
    Started,
    /// `on_start` panicked.
    StartPanicked,
    /// A message handler panicked.
    MessagePanicked,
    /// A graceful stop was requested (via `ctx.stop_self()` or `StopSignal`).
    StopRequested,
    /// A stop-with-value was requested (via `ctx.stop_with()`).
    StopWithRequested,
    /// The actor was suspended (via `ctx.suspend_self()`).
    SuspendRequested,
    /// A suspended actor was resumed (via `ResumeSignal`).
    Resumed,
}

// ─── Deliver Decision ────────────────────────────────────────────────────────

/// What should happen when a message arrives at an actor in a particular phase.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum DeliverDecision {
    /// Enqueue the message in the actor's mailbox (subject to overflow policy).
    Enqueue,
    /// The actor is dead/stopping — discard the message silently.
    Discard,
    /// The actor is suspended — enqueue but do not process until resumed.
    Queue,
}

// ─── Pure Functions ─────────────────────────────────────────────────────────

// TLA+: LifecycleTransition
/// The actor lifecycle state machine.
///
/// Given the current phase and an event, returns the new phase. Every phase
/// transition in the runtime must go through this function.
///
/// Illegal transitions (e.g., `Resumed` on a non-suspended actor) return the
/// phase unchanged — the runtime is responsible for not issuing nonsensical
/// events, but the core never panics.
#[must_use]
pub fn lifecycle_transition(phase: ActorPhase, event: LifecycleEvent) -> ActorPhase {
    match (phase, event) {
        // Unstarted: waiting for on_start result
        (ActorPhase::Unstarted, LifecycleEvent::Started) => ActorPhase::Running,
        (ActorPhase::Unstarted, LifecycleEvent::StartPanicked) => ActorPhase::Poisoned,
        (ActorPhase::Unstarted, LifecycleEvent::StopRequested) => ActorPhase::Stopping,
        (ActorPhase::Unstarted, LifecycleEvent::StopWithRequested) => ActorPhase::Stopping,
        (ActorPhase::Unstarted, LifecycleEvent::SuspendRequested) => ActorPhase::Suspended,
        (ActorPhase::Unstarted, LifecycleEvent::MessagePanicked) => phase,
        (ActorPhase::Unstarted, LifecycleEvent::Resumed) => phase,

        // Running: normal operation
        (ActorPhase::Running, LifecycleEvent::MessagePanicked) => ActorPhase::Poisoned,
        (ActorPhase::Running, LifecycleEvent::StopRequested) => ActorPhase::Stopping,
        (ActorPhase::Running, LifecycleEvent::StopWithRequested) => ActorPhase::Stopping,
        (ActorPhase::Running, LifecycleEvent::SuspendRequested) => ActorPhase::Suspended,
        (ActorPhase::Running, LifecycleEvent::Started) => phase,
        (ActorPhase::Running, LifecycleEvent::StartPanicked) => phase,
        (ActorPhase::Running, LifecycleEvent::Resumed) => phase,

        // Suspended: waiting for resume or stop
        (ActorPhase::Suspended, LifecycleEvent::Resumed) => ActorPhase::Running,
        (ActorPhase::Suspended, LifecycleEvent::StopRequested) => ActorPhase::Stopping,
        (ActorPhase::Suspended, LifecycleEvent::StopWithRequested) => ActorPhase::Stopping,
        (ActorPhase::Suspended, LifecycleEvent::Started) => phase,
        (ActorPhase::Suspended, LifecycleEvent::StartPanicked) => phase,
        (ActorPhase::Suspended, LifecycleEvent::MessagePanicked) => phase,
        (ActorPhase::Suspended, LifecycleEvent::SuspendRequested) => phase,

        // Terminal states: Stopping and Poisoned absorb all events
        (ActorPhase::Stopping, _) => ActorPhase::Stopping,
        (ActorPhase::Poisoned, _) => ActorPhase::Poisoned,
    }
}

// TLA+: MailboxAccept
/// Decide what to do with an incoming message given mailbox state and policy.
///
/// `capacity` of 0 means unbounded (always accept). When the mailbox is full,
/// the overflow policy determines whether the newest or oldest message is dropped.
#[must_use]
pub fn mailbox_accept(
    mailbox_len: usize,
    capacity: usize,
    policy: MailboxOverflow,
) -> MailboxDecision {
    if capacity == 0 || mailbox_len < capacity {
        MailboxDecision::Accept
    } else {
        match policy {
            MailboxOverflow::DropNewest => MailboxDecision::RejectNewest,
            MailboxOverflow::DropOldest => MailboxDecision::EvictOldest,
        }
    }
}

// TLA+: ShouldTickActor
/// Whether an actor in the given phase should be ticked (i.e., have messages processed).
///
/// Returns `false` for `Poisoned`, `Stopping`, and `Suspended` — these actors
/// either cannot process messages or must not.
#[must_use]
pub fn should_tick_actor(phase: ActorPhase) -> bool {
    match phase {
        ActorPhase::Unstarted | ActorPhase::Running => true,
        ActorPhase::Suspended | ActorPhase::Stopping | ActorPhase::Poisoned => false,
    }
}

// TLA+: BudgetExhausted
/// Whether the per-actor message budget has been exhausted.
///
/// `budget` of 0 means unlimited — never exhausted.
#[must_use]
pub fn budget_exhausted(processed: usize, budget: usize) -> bool {
    budget > 0 && processed >= budget
}

// TLA+: CleanupStopReason
/// Determine the stop reason for a dead actor given its phase and whether
/// it has a typed exit value.
///
/// - `Poisoned` → `StopReason::Panicked`
/// - Has exit value → `StopReason::Completed`
/// - Otherwise → `StopReason::Normal`
#[must_use]
pub fn cleanup_stop_reason(phase: ActorPhase, has_exit_value: bool) -> StopReason {
    if phase == ActorPhase::Poisoned {
        StopReason::Panicked
    } else if has_exit_value {
        StopReason::Completed
    } else {
        StopReason::Normal
    }
}

// ─── Invariant Predicates ───────────────────────────────────────────────────

// TLA+: PhaseIsTerminal
/// Returns `true` if the phase is terminal — the actor will not process any
/// further messages and is awaiting cleanup.
#[must_use]
pub fn phase_is_terminal(phase: ActorPhase) -> bool {
    match phase {
        ActorPhase::Stopping | ActorPhase::Poisoned => true,
        ActorPhase::Unstarted | ActorPhase::Running | ActorPhase::Suspended => false,
    }
}

// TLA+: ValidPhaseTransition
/// Returns `true` only for transitions that exist in the lifecycle state machine.
///
/// This is an invariant predicate — useful for property-based testing and Kani
/// harnesses to verify that no illegal transition is ever taken.
#[must_use]
pub fn valid_phase_transition(from: ActorPhase, to: ActorPhase) -> bool {
    match (from, to) {
        // Self-transitions are always valid (no-op events)
        (a, b) if a == b => true,

        // From Unstarted
        (ActorPhase::Unstarted, ActorPhase::Running) => true,
        (ActorPhase::Unstarted, ActorPhase::Poisoned) => true,
        (ActorPhase::Unstarted, ActorPhase::Stopping) => true,
        (ActorPhase::Unstarted, ActorPhase::Suspended) => true,

        // From Running
        (ActorPhase::Running, ActorPhase::Poisoned) => true,
        (ActorPhase::Running, ActorPhase::Stopping) => true,
        (ActorPhase::Running, ActorPhase::Suspended) => true,

        // From Suspended
        (ActorPhase::Suspended, ActorPhase::Running) => true,
        (ActorPhase::Suspended, ActorPhase::Stopping) => true,

        // Terminal states never transition out
        (ActorPhase::Stopping, _) => false,
        (ActorPhase::Poisoned, _) => false,

        // Everything else is invalid
        _ => false,
    }
}