//! The group-aware failpoint model (scope 4-A3 deliverable 3, ruling 9.3).
//!
//! `levcs_protocol::oracle::append_publication_expectation` is a
//! *single-transaction* contract. A real group carries up to
//! `max_group_transactions` frames behind one fence, and a failpoint fires at
//! one victim frame inside it. This module layers the group answer on top of
//! the frozen oracle; per ruling 9.3 it does not extend the oracle.
//!
//! # The contract is a contiguous adopted prefix, not a per-frame answer
//!
//! Each individual unfenced frame is independently either-whole via page
//! writeback, so a *per-frame* formulation would permit "frame 3 absent, frame
//! 4 committed". Recovery step 6 (scope 3.8) forbids exactly that, and an
//! implementation that adopts a syntactically valid frame sitting after a hole
//! is the single most consequential recovery bug this phase can ship. This
//! module therefore answers with a window of legal prefix lengths:
//!
//! > there exists some *p* ≤ `victim_index` such that frames `0..p` are
//! > committed and frames `p..group_len` are absent; nothing at or after the
//! > victim is ever committed.
//!
//! [`verify_adopted_prefix`] is the checker that turns that statement into a
//! failure for an adopt-past-a-hole implementation, which a per-frame
//! formulation could not do.
//!
//! # Degeneracy
//!
//! [`group_failpoint_expectation`] must reduce to the frozen oracle at
//! `group_len == 1`, and per ruling 9.3's condition that reduction must hold
//! for **every** physical state class, not only the torn one. The proof lives
//! in `crash_matrix.rs` and iterates every failpoint, which covers every class
//! by construction because [`PhysicalStateClass::ALL`] is asserted to be
//! exactly the set of classes witnessed by some failpoint.

#![allow(dead_code)]

use levcs_protocol::oracle::{append_publication_expectation, RecoveredTailFact, RecoveryOutcome};
use levcs_store::failpoints::Failpoint;

/// The structural half of the prefix contract, shared verbatim with
/// `store-crash-driver` and `store-bench` rather than restated here.
///
/// The reconcilers and this model must not disagree about what "contiguous"
/// means; the review that produced this include found them disagreeing, with
/// the binaries carrying the weaker rule.
#[path = "../../src/bin/support/adopted_set.rs"]
pub mod adopted_set;

use adopted_set::{classify_adopted_set, SequenceFault};

// ---------------------------------------------------------------------------
// Physical state classes
// ---------------------------------------------------------------------------

/// What a failpoint leaves on the device, independent of what any in-memory
/// state believes.
///
/// This is the first of the crash matrix's two independent derivations: the
/// class determines the required recovery outcome through
/// [`PhysicalStateClass::required_outcome`], and the frozen oracle determines
/// it again through `append_publication_expectation`. The matrix asserts both
/// and requires them to agree.
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
pub enum PhysicalStateClass {
    /// Not one byte of the group reached the file.
    NoBytes,
    /// The victim frame's bytes are truncated. A short write is not an error;
    /// it leaves a durable prefix (scope 3.7).
    PartialFrame,
    /// Every frame up to the victim is byte-complete, but no fence has
    /// returned successfully. Whether any of it reached durable storage is
    /// precisely what production recovery must decide.
    WholeFrameUnfenced,
    /// `fdatasync` returned success over the frames written before it.
    WholeFrameFenced,
    /// Fenced *and* the committed root was published, so an acknowledgment is
    /// already permitted.
    WholeFrameFencedAndPublished,
}

impl PhysicalStateClass {
    pub const ALL: &'static [PhysicalStateClass] = &[
        PhysicalStateClass::NoBytes,
        PhysicalStateClass::PartialFrame,
        PhysicalStateClass::WholeFrameUnfenced,
        PhysicalStateClass::WholeFrameFenced,
        PhysicalStateClass::WholeFrameFencedAndPublished,
    ];

    /// The four classes ruling 9.3 names for the degeneracy condition. The
    /// published class is a Wave B refinement of `WholeFrameFenced` and is
    /// listed separately so the matrix can carry the scope 4-A3 table's
    /// "`WholeFrameFenced` + published" rows verbatim.
    pub const RULING_9_3_CLASSES: &'static [PhysicalStateClass] = &[
        PhysicalStateClass::NoBytes,
        PhysicalStateClass::PartialFrame,
        PhysicalStateClass::WholeFrameUnfenced,
        PhysicalStateClass::WholeFrameFenced,
    ];

    /// Name as it appears in `tests/fixtures/phase1-failpoints.json`.
    pub const fn name(self) -> &'static str {
        match self {
            PhysicalStateClass::NoBytes => "NoBytes",
            PhysicalStateClass::PartialFrame => "PartialFrame",
            PhysicalStateClass::WholeFrameUnfenced => "WholeFrameUnfenced",
            PhysicalStateClass::WholeFrameFenced => "WholeFrameFenced",
            PhysicalStateClass::WholeFrameFencedAndPublished => "WholeFrameFencedAndPublished",
        }
    }

    /// Parse without a catch-all arm: a linear search over `ALL` rather than a
    /// `match` with a fallback binding, so adding a class cannot silently
    /// acquire a default.
    pub fn from_name(name: &str) -> Option<Self> {
        Self::ALL.iter().copied().find(|c| c.name() == name)
    }

    /// The class-derived half of the crash matrix's expectation.
    ///
    /// Exactly scope 4-A3's table: absent bytes and torn bytes are absent and
    /// retriable, unfenced whole bytes are `EitherWhole`, fenced whole bytes
    /// are committed.
    pub const fn required_outcome(self) -> RecoveryOutcome {
        match self {
            PhysicalStateClass::NoBytes => RecoveryOutcome::AbsentRetriable,
            PhysicalStateClass::PartialFrame => RecoveryOutcome::AbsentRetriable,
            PhysicalStateClass::WholeFrameUnfenced => RecoveryOutcome::EitherWhole,
            PhysicalStateClass::WholeFrameFenced => RecoveryOutcome::Committed,
            PhysicalStateClass::WholeFrameFencedAndPublished => RecoveryOutcome::Committed,
        }
    }

    /// Whether an acknowledgment is already permitted when the failpoint
    /// fires. Only the published class permits one; scope 4-A3's table marks
    /// exactly those two rows "ack allowed".
    pub const fn acknowledgment_allowed(self) -> bool {
        match self {
            PhysicalStateClass::NoBytes => false,
            PhysicalStateClass::PartialFrame => false,
            PhysicalStateClass::WholeFrameUnfenced => false,
            PhysicalStateClass::WholeFrameFenced => false,
            PhysicalStateClass::WholeFrameFencedAndPublished => true,
        }
    }

    /// Which terminal outcome a `StagedProjection` payload's adoption pin must
    /// carry when this class is produced (scope 6.2 item 9).
    ///
    /// This is the class-derived half of the adoption expectation, and the
    /// fixture's stated `adoption_outcome` is the other. The matrix requires
    /// them to agree, exactly as it already does for `required_outcome`.
    ///
    /// The rule is the physical one and nothing else: **whether a frame
    /// binding these artifacts exists on the device.**
    ///
    /// * No bytes reached the file, so no frame names the artifacts. They are
    ///   unreferenced and reclaiming them is correct, which is what
    ///   `DefinitivePreAppendFailure` licenses.
    /// * A torn or unfenced frame is `AbsentRetriable` for the transaction,
    ///   but it is **not** `DefinitivePreAppendFailure` for the pin. Bytes are
    ///   on the device and recovery decides what they mean; telling staging to
    ///   reclaim now would race that decision. Only recovery can resolve it.
    /// * A fenced frame is durable and binds the manifest, so the pin outlives
    ///   the process and recovery notifies staging of the resolution.
    /// * Fenced *and* published means the committed root already references
    ///   the artifacts and the shard sequence is known, so the writer settled
    ///   `Adopted` before this failpoint could fire. A failure after that
    ///   point cannot un-adopt what a published root points into.
    ///
    /// Note the asymmetry against `required_outcome`: `PartialFrame` and
    /// `WholeFrameUnfenced` are `AbsentRetriable` there and
    /// `TransferredToRecovery` here. A transaction that will not commit and a
    /// pin whose artifacts may be referenced are different questions, and
    /// collapsing them is how a retriable refusal would come to delete
    /// content.
    pub const fn adoption_outcome(self) -> AdoptionOutcomeExpectation {
        match self {
            PhysicalStateClass::NoBytes => AdoptionOutcomeExpectation::DefinitivePreAppendFailure,
            PhysicalStateClass::PartialFrame => AdoptionOutcomeExpectation::TransferredToRecovery,
            PhysicalStateClass::WholeFrameUnfenced => {
                AdoptionOutcomeExpectation::TransferredToRecovery
            }
            PhysicalStateClass::WholeFrameFenced => {
                AdoptionOutcomeExpectation::TransferredToRecovery
            }
            PhysicalStateClass::WholeFrameFencedAndPublished => AdoptionOutcomeExpectation::Adopted,
        }
    }
}

/// The terminal outcome expected of an adoption pin, as the matrix names it.
///
/// A test-side mirror of `ProjectionAdoptionOutcome` without the payload:
/// `Adopted` carries a committed shard sequence the matrix cannot predict, and
/// an expectation that had to guess it would assert less, not more.
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
pub enum AdoptionOutcomeExpectation {
    Adopted,
    DefinitivePreAppendFailure,
    TransferredToRecovery,
}

impl AdoptionOutcomeExpectation {
    pub const ALL: &'static [AdoptionOutcomeExpectation] = &[
        AdoptionOutcomeExpectation::Adopted,
        AdoptionOutcomeExpectation::DefinitivePreAppendFailure,
        AdoptionOutcomeExpectation::TransferredToRecovery,
    ];

    /// Name as it appears in `tests/fixtures/phase1-failpoints.json`.
    pub const fn name(self) -> &'static str {
        match self {
            AdoptionOutcomeExpectation::Adopted => "Adopted",
            AdoptionOutcomeExpectation::DefinitivePreAppendFailure => "DefinitivePreAppendFailure",
            AdoptionOutcomeExpectation::TransferredToRecovery => "TransferredToRecovery",
        }
    }

    /// Parsed by linear search over `ALL`, for the reason
    /// `PhysicalStateClass::from_name` is: adding a variant must not silently
    /// acquire a default.
    pub fn from_name(name: &str) -> Option<Self> {
        Self::ALL.iter().copied().find(|o| o.name() == name)
    }
}

/// Which payload a Wave B row drives the failpoint's location with.
///
/// The third independent axis of a submit row, alongside the location the
/// failpoint names and the action the driver chooses. It is an axis rather
/// than a second list of failpoints because the locations do not change: a
/// staged-projection adoption reaches every one of the eight Wave B locations,
/// and giving it its own rows would produce a parallel list that drifts from
/// this one the first time a location is added to either.
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
pub enum PayloadKind {
    /// Objects carried in the frame, which is every Wave B row today.
    Inline,
    /// A `StagedProjectionInstallV1` descriptor adopting sealed artifacts,
    /// with an adoption pin whose terminal outcome is asserted.
    StagedProjection,
}

impl PayloadKind {
    pub const ALL: &'static [PayloadKind] = &[PayloadKind::Inline, PayloadKind::StagedProjection];

    /// Name as it appears in `tests/fixtures/phase1-failpoints.json`.
    pub const fn name(self) -> &'static str {
        match self {
            PayloadKind::Inline => "inline",
            PayloadKind::StagedProjection => "staged_projection",
        }
    }

    pub fn from_name(name: &str) -> Option<Self> {
        Self::ALL.iter().copied().find(|k| k.name() == name)
    }

    /// Whether driving this kind requires an adoption pin whose outcome the
    /// row must assert.
    pub const fn carries_adoption(self) -> bool {
        match self {
            PayloadKind::Inline => false,
            PayloadKind::StagedProjection => true,
        }
    }
}

/// The physical state class each failpoint produces.
///
/// One arm per failpoint, deliberately unfactored. Grouping the arms would
/// save lines and lose the property that adding a failpoint breaks the build
/// here rather than inheriting a neighbour's class — the failure mode contract
/// review 2026-07-24-A was about.
pub const fn physical_state_class(point: Failpoint) -> PhysicalStateClass {
    match point {
        Failpoint::BeforeAppend => PhysicalStateClass::NoBytes,
        Failpoint::AfterMarkedResolving => PhysicalStateClass::NoBytes,
        Failpoint::EvidenceHandoffFailure => PhysicalStateClass::NoBytes,

        Failpoint::DuringFrameWriteTorn => PhysicalStateClass::PartialFrame,

        Failpoint::AfterFrameWrite => PhysicalStateClass::WholeFrameUnfenced,
        Failpoint::BeforeFence => PhysicalStateClass::WholeFrameUnfenced,
        Failpoint::FenceFailed => PhysicalStateClass::WholeFrameUnfenced,
        Failpoint::FenceAmbiguous => PhysicalStateClass::WholeFrameUnfenced,
        Failpoint::WriterPanicBeforeFence => PhysicalStateClass::WholeFrameUnfenced,

        Failpoint::AfterSuccessfulFence => PhysicalStateClass::WholeFrameFenced,
        Failpoint::DuringCommittedRootBuild => PhysicalStateClass::WholeFrameFenced,
        Failpoint::AllocationFailureBeforePublication => PhysicalStateClass::WholeFrameFenced,
        Failpoint::BeforeRootCas => PhysicalStateClass::WholeFrameFenced,
        Failpoint::DuringRootCasRetry => PhysicalStateClass::WholeFrameFenced,
        Failpoint::WriterPanicAfterFence => PhysicalStateClass::WholeFrameFenced,

        Failpoint::AfterRootCasBeforeWaiterWake => PhysicalStateClass::WholeFrameFencedAndPublished,
        Failpoint::BeforeResponse => PhysicalStateClass::WholeFrameFencedAndPublished,
    }
}

// ---------------------------------------------------------------------------
// Victim placement
// ---------------------------------------------------------------------------

/// Where in a group of `group_len` frames a failpoint's victim sits.
///
/// Recorded per row in the fixture so a reviewer can see that a post-fence row
/// is group-wide rather than assume it.
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
pub enum VictimPlacement {
    /// The fault precedes any frame, so the victim is frame 0 and no frame of
    /// the group is written.
    First,
    /// The fault truncates one frame. The harness tears the last frame of the
    /// group, which degenerates to frame 0 at `group_len == 1`.
    Last,
    /// The fault has no per-frame victim: the whole group's bytes were emitted
    /// before it fired. The victim index is `group_len`, which is what makes
    /// "∃ p ≤ victim_index" permit the whole group.
    GroupWide,
}

impl VictimPlacement {
    pub const ALL: &'static [VictimPlacement] = &[
        VictimPlacement::First,
        VictimPlacement::Last,
        VictimPlacement::GroupWide,
    ];

    pub const fn name(self) -> &'static str {
        match self {
            VictimPlacement::First => "first",
            VictimPlacement::Last => "last",
            VictimPlacement::GroupWide => "group-wide",
        }
    }

    pub fn from_name(name: &str) -> Option<Self> {
        Self::ALL.iter().copied().find(|p| p.name() == name)
    }

    /// Resolve to a concrete victim index for a group of `group_len` frames.
    pub fn index(self, group_len: usize) -> usize {
        match self {
            VictimPlacement::First => 0,
            VictimPlacement::Last => group_len.saturating_sub(1),
            VictimPlacement::GroupWide => group_len,
        }
    }
}

/// The placement each physical state class implies.
///
/// This is derived from the class rather than stated per failpoint, because it
/// is a property of what the device holds, not of where in the code the fault
/// was injected.
pub const fn victim_placement(class: PhysicalStateClass) -> VictimPlacement {
    match class {
        PhysicalStateClass::NoBytes => VictimPlacement::First,
        PhysicalStateClass::PartialFrame => VictimPlacement::Last,
        PhysicalStateClass::WholeFrameUnfenced => VictimPlacement::GroupWide,
        PhysicalStateClass::WholeFrameFenced => VictimPlacement::GroupWide,
        PhysicalStateClass::WholeFrameFencedAndPublished => VictimPlacement::GroupWide,
    }
}

// ---------------------------------------------------------------------------
// The group expectation
// ---------------------------------------------------------------------------

/// A window of legal contiguous adopted prefixes.
///
/// Recovery is correct for this group iff it adopted frames `0..p` and nothing
/// else, for some `p` in `min_prefix..=max_prefix`. `max_prefix` never exceeds
/// the victim index, which is the "nothing at or after the victim is ever
/// committed" half of the contract.
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
pub struct AdoptedPrefixExpectation {
    pub point: Failpoint,
    pub class: PhysicalStateClass,
    pub group_len: usize,
    pub victim_index: usize,
    pub min_prefix: usize,
    pub max_prefix: usize,
}

impl AdoptedPrefixExpectation {
    /// The outcome the model permits for one frame of the group.
    ///
    /// Below `min_prefix` the frame is committed under every legal `p`; at or
    /// above `max_prefix` it is absent under every legal `p`; in between the
    /// two the model is genuinely undetermined, which is `EitherWhole` and is
    /// the only honest answer for an unfenced frame.
    pub fn outcome_for_frame(&self, frame_index: usize) -> RecoveryOutcome {
        if frame_index < self.min_prefix {
            RecoveryOutcome::Committed
        } else if frame_index >= self.max_prefix {
            RecoveryOutcome::AbsentRetriable
        } else {
            RecoveryOutcome::EitherWhole
        }
    }

    /// The outcome for the victim frame itself. Equal to the class's required
    /// outcome by construction; the matrix asserts the equality rather than
    /// assuming it.
    pub fn victim_outcome(&self) -> RecoveryOutcome {
        self.class.required_outcome()
    }

    /// Structural invariants the model must satisfy for any input.
    pub fn check_invariants(&self) {
        assert!(self.group_len >= 1, "a group has at least one frame");
        assert!(
            self.victim_index <= self.group_len,
            "victim {} is outside a group of {}",
            self.victim_index,
            self.group_len
        );
        assert!(
            self.min_prefix <= self.max_prefix,
            "empty prefix window for {:?}",
            self.point
        );
        assert!(
            self.max_prefix <= self.victim_index,
            "the model must never permit adopting the victim frame or anything \
             after it: {:?} allows p={} with victim {}",
            self.point,
            self.max_prefix,
            self.victim_index
        );
    }
}

/// Layered group expectation. Scope 4-A3 deliverable 3, ruling 9.3.
///
/// `victim_index` is the index of the first frame the fault prevented from
/// completing; it equals `group_len` for a fault with no per-frame victim.
/// The function is total: every `(victim_index, group_len)` pair with
/// `victim_index <= group_len` has a meaningful answer, so the matrix never
/// has to special-case a row.
pub fn group_failpoint_expectation(
    point: Failpoint,
    victim_index: usize,
    group_len: usize,
) -> AdoptedPrefixExpectation {
    assert!(group_len >= 1, "a group has at least one frame");
    assert!(
        victim_index <= group_len,
        "victim index {victim_index} is outside a group of {group_len}"
    );

    let class = physical_state_class(point);
    let (min_prefix, max_prefix) = match class {
        // No byte of the group reached the file, so p is pinned at 0
        // regardless of where the caller places the victim.
        PhysicalStateClass::NoBytes => (0, 0),

        // Frames before the victim are byte-complete but unfenced, so each is
        // independently either-whole; the victim is truncated and can never be
        // adopted; everything after it was never written. p ranges over the
        // whole window below the victim.
        PhysicalStateClass::PartialFrame => (0, victim_index),

        // Every frame below the victim is byte-complete and unfenced. Same
        // window as the torn case — which is the point: an unfenced whole
        // frame and an unfenced whole frame sitting before a tear are the same
        // physical situation, and only the victim differs.
        PhysicalStateClass::WholeFrameUnfenced => (0, victim_index),

        // The fence returned success over everything written before it, which
        // is frames `0..victim_index`. p is pinned, not a window: a fence that
        // returned success and then lost data is a hardware finding surfaced
        // by the external ACK journal (scope 3.8), never a legal outcome the
        // model may admit.
        PhysicalStateClass::WholeFrameFenced => (victim_index, victim_index),
        PhysicalStateClass::WholeFrameFencedAndPublished => (victim_index, victim_index),
    };

    let expectation = AdoptedPrefixExpectation {
        point,
        class,
        group_len,
        victim_index,
        min_prefix,
        max_prefix,
    };
    expectation.check_invariants();
    expectation
}

/// The expectation for a row driven with the canonical placement of its class.
pub fn canonical_group_expectation(point: Failpoint, group_len: usize) -> AdoptedPrefixExpectation {
    let placement = victim_placement(physical_state_class(point));
    group_failpoint_expectation(point, placement.index(group_len), group_len)
}

// ---------------------------------------------------------------------------
// Prefix verification
// ---------------------------------------------------------------------------

/// How an observed adoption set fails the contiguous-prefix contract.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum PrefixViolation {
    /// Recovery adopted a frame that sits after a gap. This is the bug the
    /// whole prefix formulation exists to catch: recovery step 6 stops at the
    /// first incomplete frame unconditionally, even when a later region holds
    /// a syntactically complete, checksum-valid frame.
    AdoptedPastAHole { expected_next: u64, observed: u64 },
    /// The adopted set is not sorted/unique, so it is not a prefix at all.
    NotAscendingUnique { observed: Vec<u64> },
    /// Recovery started somewhere other than the group's first sequence.
    WrongStart { expected: u64, observed: u64 },
    /// More frames adopted than the failpoint can possibly have made durable.
    PrefixTooLong { adopted: usize, max_prefix: usize },
    /// Fewer frames adopted than a successful fence guarantees.
    PrefixTooShort { adopted: usize, min_prefix: usize },
}

/// Prove an observed adoption set is a contiguous prefix inside the model's
/// window.
///
/// `observed` is the set of `shard_sequence` values recovery adopted **from
/// this group**, and `first_sequence` is the sequence assigned to frame 0.
/// Returns the adopted prefix length `p` on success.
pub fn verify_adopted_prefix(
    observed: &[u64],
    first_sequence: u64,
    expectation: &AdoptedPrefixExpectation,
) -> Result<usize, PrefixViolation> {
    let report = classify_adopted_set(observed);
    if report.repeated_adoptions() != 0 {
        return Err(PrefixViolation::NotAscendingUnique {
            observed: observed.to_vec(),
        });
    }

    if let Some(first) = observed.first() {
        if *first != first_sequence {
            return Err(PrefixViolation::WrongStart {
                expected: first_sequence,
                observed: *first,
            });
        }
    }

    if let Some(SequenceFault::ForwardGap {
        expected_next,
        observed,
    }) = report.first_fault
    {
        return Err(PrefixViolation::AdoptedPastAHole {
            expected_next,
            observed,
        });
    }

    let adopted = observed.len();
    if adopted > expectation.max_prefix {
        return Err(PrefixViolation::PrefixTooLong {
            adopted,
            max_prefix: expectation.max_prefix,
        });
    }
    if adopted < expectation.min_prefix {
        return Err(PrefixViolation::PrefixTooShort {
            adopted,
            min_prefix: expectation.min_prefix,
        });
    }
    Ok(adopted)
}

// ---------------------------------------------------------------------------
// Outcome admission
// ---------------------------------------------------------------------------

/// Whether a concrete observed tail fact is admitted by an expected outcome.
///
/// `EitherWhole` is the only outcome that admits two facts, and it admits them
/// only through the frozen `resolve_ambiguous_tail`, so an implementation
/// cannot resolve an ambiguous fence deterministically before recovery re-reads
/// the device (scope 5 charter item 4).
pub fn outcome_admits(expected: RecoveryOutcome, fact: RecoveredTailFact) -> bool {
    let resolved = levcs_protocol::oracle::resolve_ambiguous_tail(fact);
    match expected {
        RecoveryOutcome::AbsentRetriable => resolved == RecoveryOutcome::AbsentRetriable,
        RecoveryOutcome::Committed => resolved == RecoveryOutcome::Committed,
        RecoveryOutcome::EitherWhole => {
            resolved == RecoveryOutcome::AbsentRetriable || resolved == RecoveryOutcome::Committed
        }
    }
}

/// The frozen oracle's half of the matrix's two derivations.
pub fn oracle_recovery_outcome(point: Failpoint) -> RecoveryOutcome {
    append_publication_expectation(point.into()).recovery_outcome
}