minerva 0.2.0

extern crate alloc;

use alloc::collections::BTreeSet;
use core::num::NonZeroU64;

use crate::metis::{Dot, DotSet};

use super::DotStore;

mod delta;
mod uncovered;

pub use uncovered::UncoveredDot;

/// A causal pair: a [`DotStore`] bracketed by the causal context that
/// vouches for everything it has ever seen.
///
/// The production-side half of the dotted-vector charter (PRD 0015; the
/// receipt-side half is [`DotSet`] itself). The `store` holds what
/// *survives*; the `context` records every dot ever seen, survivors and
/// superseded alike, and never forgets.
///
/// That asymmetry is the entire mechanism. A dot in a peer's context but
/// absent from its store was *seen there and dropped*, which is how
/// [`merge`](Self::merge) honours removals without tombstones and without
/// conflating "never seen" with "seen and removed." The two hand-rolled forms
/// of that conflation fail in opposite unrecoverable directions:
/// resurrected removals, or concurrent writes silently dropped as
/// superseded.
///
/// # State and delta are one type
///
/// A `Dotted<S>` is at once a replica's full state and the shape of every
/// delta. A write is a small pair (a fresh dot in a
/// [`singleton`](crate::metis::DotMap::singleton) store, the dot in the
/// context); a removal is a pure-context pair
/// ([`from_context`](Self::from_context)); and *the only write operation is
/// [`merge`](Self::merge)*. That keeps the type inside the crate's monotone
/// sea: folds and reads, no seriality hazard, and anti-entropy composing out
/// of the shipped reads in any join order.
///
/// # The invariant
///
/// A pair is *covered* when every store dot is in the context. Every
/// constructor but one holds it by construction;
/// [`try_new`](Self::try_new) is the boundary for foreign pairs and refuses
/// an uncovered one with an [`UncoveredDot`] witness. The semilattice laws
/// are stated over covered pairs.
///
/// # What this type refuses to own
///
/// Payload values (a value-carrying store is a caller [`DotStore`]),
/// add-wins versus remove-wins (which deltas a caller constructs, never a
/// merge property), transport, and sibling display order (a caller ranks
/// concurrent survivors itself, the natural discriminator being the
/// [`Kairos`](crate::kairos::Kairos) stamp).
#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
pub struct Dotted<S> {
    /// What survives: the causally tagged content.
    store: S,
    /// Everything ever seen, survivors and superseded alike; never forgets.
    context: DotSet,
}

impl<S: DotStore> Dotted<S> {
    /// The bottom pair: nothing held, nothing seen.
    #[must_use]
    pub fn new() -> Self {
        Self {
            store: S::default(),
            context: DotSet::new(),
        }
    }

    /// Wraps a store with exactly its own dots as context: a pair that has
    /// seen precisely what it holds. Covered by construction.
    ///
    /// This is the shape of a pure *write* delta (everything carried is
    /// alive); a delta that also supersedes is built with
    /// [`try_new`](Self::try_new) (store plus a strictly larger context), and
    /// a pure removal with [`from_context`](Self::from_context).
    #[must_use]
    pub fn from_store(store: S) -> Self {
        let mut context = DotSet::new();
        for dot in store.dots() {
            let _ = context.insert(dot);
        }
        Self { store, context }
    }

    /// Wraps a bare context with the bottom store: a pair that carries
    /// nothing and testifies to having seen `context`. Covered trivially.
    ///
    /// This is the shape of a *removal* delta: merging it supersedes every
    /// dot of `context` wherever the merge lands, because the receiving side
    /// sees them covered by a context whose store does not carry them. Which
    /// dots to put here is the caller's semantics (observed-remove passes
    /// exactly the dots it observed under a key; passing dots you have not
    /// observed is a remove-wins posture against concurrent writes).
    #[must_use]
    pub fn from_context(context: DotSet) -> Self {
        Self {
            store: S::default(),
            context,
        }
    }

    /// Assembles a pair from parts, refusing an uncovered one: every store
    /// dot must be in the context, or the first uncovered dot (in ascending
    /// [`Dot`] order) comes back as the [`UncoveredDot`] witness and nothing
    /// is built.
    ///
    /// The boundary constructor for pairs arriving from outside: a decoded
    /// frame, a caller-assembled delta. An uncovered pair lies about its own
    /// past --- it carries a dot it claims never to have seen --- and the
    /// survivor law would then double-deliver that dot's content instead of
    /// superseding it.
    ///
    /// Coverage is the whole contract; provenance is deliberately not
    /// checked. This is a structural gate, not a trust gate
    /// (`docs/metis-trust-grades.adoc`).
    ///
    /// # Errors
    ///
    /// [`UncoveredDot`] naming the first store dot the context fails to
    /// cover.
    pub fn try_new(store: S, context: DotSet) -> Result<Self, UncoveredDot> {
        for dot in store.dots() {
            if !context.contains(dot) {
                return Err(UncoveredDot { dot });
            }
        }
        Ok(Self { store, context })
    }

    /// The causal merge, the pair's only write: survivors by the survivor
    /// law under the two contexts, context by union.
    ///
    /// Commutative, associative, and idempotent over covered pairs, with
    /// [`new`](Self::new) the identity, so replicas may merge full states
    /// and deltas in any order, grouping, and multiplicity and converge.
    /// Where the plain [`DotSet::merge`] is the fold for *knowledge* and
    /// [`try_glue`](crate::metis::VersionVector::try_glue) the fold for
    /// *authority*, this is the fold for *survival*: the context coordinate
    /// is exactly the knowledge join, while the store coordinate is
    /// deliberately *below* the union, and the gap is exactly the dots one
    /// side saw and dropped.
    #[must_use]
    pub fn merge(&self, other: &Self) -> Self {
        Self {
            store: self
                .store
                .causal_merge(&self.context, &other.store, &other.context),
            context: self.context.merge(&other.context),
        }
    }

    /// The same causal merge, folded into this pair in place:
    /// observationally identical to `*self = self.merge(other)`, the
    /// [`clone_from`](Clone::clone_from) shape (S182).
    ///
    /// Semantically nothing new, so every law of [`merge`](Self::merge) (the
    /// semilattice on covered pairs, the survivor law, coveredness
    /// preservation) holds verbatim; the difference is cost. The pure form
    /// rebuilds both coordinates per fold. The S181 scale probe measured that
    /// cost as linear in the *document* per composed keystroke: 8.5 ms at
    /// 65,536 chars through the facade. This form instead delegates to the
    /// store's [`causal_merge_from`](DotStore::causal_merge_from), whose
    /// default is the pure merge; the in-tree hot stores override it
    /// delta-bounded. It grows the context by exactly the stations the delta
    /// names, so folding a keystroke-sized delta costs the delta.
    /// [`Composer`](crate::metis::Composer)'s write and receive flows run
    /// through here since S182.
    ///
    /// The store coordinate folds under the contexts *before* their union,
    /// exactly as [`merge`](Self::merge) reads them: the survivor law is
    /// stated over each side's own past.
    pub fn merge_from(&mut self, other: &Self) {
        self.store
            .causal_merge_from(&self.context, &other.store, &other.context);
        self.context.merge_from(&other.context);
    }

    /// The next fresh dot this pair would assign for `station`: one past
    /// the *context's* high water there. The dot-assignment read, the
    /// write path's first step ([`Producer`](crate::metis::Producer)-adjacent).
    ///
    /// Freshness comes from the context precisely because it never forgets.
    /// Assigning off the store --- or any structure that forgets removals ---
    /// re-issues a superseded dot, which every peer whose context covers it
    /// silently drops as already-seen: the *doomed dot* trap.
    ///
    /// # The delta's merge is what records the dot
    ///
    /// The write flow is read `next_dot`, attach the dot to content in a
    /// delta, then [`merge`](Self::merge) that delta here and ship it.
    /// Recording the dot *before* merging --- reserving it in the live
    /// context --- would make the merge read the delta's own dot as
    /// seen-and-dropped and discard the write, which is why no
    /// eager-reserving variant exists.
    ///
    /// Two consequences for the caller. Two reads without an intervening
    /// merge return the same dot, so merge each write's delta before
    /// assigning the next. And a delta shipped before it is durably merged
    /// locally can, after a crash, see the same dot reassigned to different
    /// content: persist-then-send is the caller's durability discipline,
    /// exactly as report honesty is `Stability`'s.
    ///
    /// Counters saturate at the [`u64`] ceiling like the rest of the crate
    /// (at the ceiling the dot is re-issued rather than wrapped; the horizon
    /// is unreachable in practice, matching
    /// [`increment`](crate::metis::VersionVector::increment)'s posture).
    #[must_use]
    pub fn next_dot(&self, station: u32) -> Dot {
        // One past the high water is one-based by construction: the
        // arithmetic starts at the nonzero one and only grows, so the result
        // is a dot without a re-check (ruling R-91). Saturation keeps the
        // ceiling posture the rustdoc states.
        let counter = NonZeroU64::MIN.saturating_add(self.context.high_water_of(station));
        Dot::new(station, counter)
    }

    /// The surviving store: what this pair currently carries.
    #[must_use]
    pub const fn store(&self) -> &S {
        &self.store
    }

    /// The causal context: everything this pair has ever seen, survivors
    /// and superseded alike.
    #[must_use]
    pub const fn context(&self) -> &DotSet {
        &self.context
    }

    /// The restriction of the pair to `roster`: both coordinates restricted
    /// (the base-change read, PRD 0013), coveredness preserved.
    ///
    /// Fiber-wise like every read here, so it commutes exactly with
    /// [`merge`](Self::merge); the one-way-witness discipline applies to any
    /// verdict taken on restrictions.
    #[must_use]
    pub fn restrict(&self, roster: impl IntoIterator<Item = u32>) -> Self {
        let roster: BTreeSet<u32> = roster.into_iter().collect();
        Self {
            store: self.store.restrict(roster.iter().copied()),
            context: self.context.restrict(roster.iter().copied()),
        }
    }
}