minerva 0.2.0

extern crate alloc;

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

/// A store of causally tagged state: the typed half of a causal pair
/// ([`Dotted`](crate::metis::Dotted)), holding content addressed by dots.
///
/// The crate's second deliberately open axis, after [`Gate`](crate::metis::Gate).
/// Minerva ships two *dot-shaped* instances: [`DotSet`] for bare presence and
/// [`DotMap`](crate::metis::DotMap) for caller-keyed composition. A
/// consumer whose store carries application values implements this trait for
/// its own type, keeping every payload and every application merge decision on
/// its own side of the boundary.
///
/// # The laws
///
/// These are what make [`Dotted::merge`](crate::metis::Dotted::merge)
/// converge. An implementation that breaks one breaks convergence two layers
/// up, so they are contract rather than guidance.
///
/// 1. *Support exactness.* [`dots`](Self::dots) enumerates exactly the dots
///    carried, each at most once; [`Default`] is bottom and
///    [`is_bottom`](Self::is_bottom) is true iff no state at all is carried.
///    Support emptiness and bottom are *distinct* facts for a store with a
///    recording plane beside its support
///    (`docs/metis-delta-context-law.adoc`). Across a composed shape a dot
///    appears under one place only, which [`DotMap`](crate::metis::DotMap)
///    enforces at insertion: a dot names one write, so straddling two keys
///    would break laws 2 and 3.
/// 2. *The survivor law.* In `self.causal_merge(sc, other, oc)`, a dot
///    survives iff it is in both stores, or in `self` and not covered by
///    `oc`, or in `other` and not covered by `sc`. Present in one store but
///    covered by the other side's context means *seen there and dropped*, so
///    the merge honours the drop rather than resurrecting. This is the one
///    law separating causal state from a plain union, and the point of the
///    axis.
/// 3. *Content follows the dot.* A surviving dot keeps whatever content the
///    shape attaches to it; the merge never invents, splits, or reassigns.
///    On the honest basis a dot names one write, so both sides carry equal
///    content and an implementation may keep either. The axis is
///    value-opaque, so this one is a *per-implementation* obligation no
///    generic conformance harness can reach. Test it against your own
///    accessors, as the in-tree suites do.
/// 4. *Semilattice on covered pairs.* Over states whose context covers their
///    store, `causal_merge` with the matching context merge is commutative,
///    associative, and idempotent, with the bottom pair as identity. Copy
///    the property-test shapes from `src/metis/tests/causal_store/`.
/// 5. *Restriction is fiber selection* (PRD 0013 R2).
///    [`restrict`](Self::restrict) keeps exactly the dots on the roster's
///    stations, with their content, and commutes with `causal_merge` under
///    restricted contexts.
pub trait DotStore: Default {
    /// Enumerates every dot the store carries, in ascending
    /// [`Dot`] order per shape component, each exactly once.
    fn dots(&self) -> impl Iterator<Item = Dot> + '_;

    /// Whether the store carries no dots at all (the lattice bottom).
    fn is_bottom(&self) -> bool;

    /// Whether a single dot survives the causal merge, given whether both
    /// stores carry it (`in_both`) and whether the *other* side's context
    /// covers it (`other_context_covers`): the survivor law (law 2) for one
    /// dot, provided so leaf impls stop copy-pasting the three-way branch.
    ///
    /// A dot held by this store survives iff both stores carry it, or the other
    /// side never saw it. Read from the *self* side, `other_context_covers`
    /// distinguishes "seen there and dropped" (covered, so superseded) from
    /// "never seen there" (survives as a concurrent write). Applied to the
    /// *other* side's dots by the caller's own read: pass `in_both = false` and
    /// `other_context_covers = self_context.covers(dot)`, which is why the one
    /// function serves both halves of a `causal_merge` fold. The default body
    /// is the law verbatim and no impl should need to override it; it is a trait
    /// method only so the axis's single distinguishing law has one home.
    #[must_use]
    fn survives(in_both: bool, other_context_covers: bool) -> bool {
        in_both || !other_context_covers
    }

    /// The causal merge of two stores, each read under its pair's context:
    /// the survivor law's fold (law 2 above).
    ///
    /// Callers merge whole pairs via [`Dotted::merge`](crate::metis::Dotted::merge), which threads the
    /// two contexts through here; the contexts are the *pair's*, never
    /// per-component, which is what lets one context vouch for every level
    /// of a composed store.
    #[must_use]
    fn causal_merge(&self, self_context: &DotSet, other: &Self, other_context: &DotSet) -> Self;

    /// The same causal merge, folded into `self` in place: observationally
    /// identical to `*self = self.causal_merge(self_context, other,
    /// other_context)`, which is exactly what this default body does (the
    /// [`clone_from`](Clone::clone_from) precedent: the pure form is the
    /// contract, the in-place form is the cost seam).
    ///
    /// An override is a cost optimization only, never a semantic choice: the
    /// one law is *agreement with [`causal_merge`](Self::causal_merge)* on
    /// every covered input, and the in-tree conformance suite pins it for
    /// every shipped instance beside the foreign-store harness. Overriding
    /// pays when a small delta folds into a large state: the pure form
    /// rebuilds the whole store per fold (the S181 scale probe measured the
    /// composed write path linear in the document, 8.5 ms per keystroke at
    /// 65,536 chars), where an in-place fold touches only what the delta
    /// names. [`Dotted::merge_from`](crate::metis::Dotted::merge_from) is the
    /// caller that threads the pair's contexts through here (S182).
    fn causal_merge_from(&mut self, self_context: &DotSet, other: &Self, other_context: &DotSet) {
        *self = self.causal_merge(self_context, other, other_context);
    }

    /// The restriction of the store to `roster`: the same content on the
    /// named stations' dots, nothing anywhere else (the base-change read,
    /// PRD 0013).
    #[must_use]
    fn restrict(&self, roster: impl IntoIterator<Item = u32>) -> Self;

    /// The store's support as a have-set: exactly the dots
    /// [`dots`](Self::dots) enumerates, folded into a [`DotSet`].
    ///
    /// The default body is that fold verbatim, so the law
    /// (`support().dots()` enumerates exactly `dots()`) holds for free; an
    /// override is a cost seam only, for a store that already *maintains*
    /// its support in have-set form and can hand back a compact clone
    /// instead of re-folding the document per call ([`DotSet`] is its own
    /// support; the sequence store's visible set is one). The owed reads
    /// ([`Dotted::delta_for`](crate::metis::Dotted::delta_for) and its
    /// witnessed sibling) rebuild this set per anti-entropy probe, which is
    /// where the fold's cost bites (arc 10).
    #[must_use]
    fn support(&self) -> DotSet {
        let mut support = DotSet::new();
        for dot in self.dots() {
            let _ = support.insert(dot);
        }
        support
    }

    /// The sub-store of exactly the dots this store carries that `context`
    /// does *not* cover, content preserved: the pair-anti-entropy selection
    /// (PRD 0015 open question 3, answered S97).
    ///
    /// A coverage-shaped sibling of [`restrict`](Self::restrict): where that
    /// selects whole station fibers, this selects individual dots by whether
    /// the peer already knows them. The store half of
    /// [`Dotted::delta_for`](crate::metis::Dotted::delta_for).
    ///
    /// Law-bearing: the result enumerates exactly the dots of
    /// [`dots`](Self::dots) outside `context`, each at most once, canonical
    /// form preserved.
    ///
    /// Selection reads on *support*, so a store carrying a recording plane
    /// ships that plane whole and a caught-up peer's fragment is
    /// support-empty rather than bottom
    /// (`docs/metis-delta-context-law.adoc`).
    #[must_use]
    fn novel_to(&self, context: &DotSet) -> Self;

    /// [`novel_to`](Self::novel_to) under a *recording-possession witness*:
    /// the anti-entropy selection when the peer states not only what it has
    /// seen (`context`, the survivor coordinate) but what recording state it
    /// *holds* (`recording`, the peer's own recording plane as a have-set).
    ///
    /// The default body ignores the witness, which is sound for every
    /// law-abiding store. An override is a *transfer* seam and never a
    /// semantic choice: it may withhold exactly the recording state the
    /// witness claims, because possession is claimed directly rather than
    /// inferred from coverage. The argument, and the duty an override owes
    /// whatever the witness claims, are
    /// `docs/metis-delta-context-law.adoc`.
    ///
    /// The law: support selection is [`novel_to`](Self::novel_to)'s
    /// unchanged, for every witness; and for every peer whose recording
    /// plane contains everything `recording` claims, merging the witnessed
    /// fragment converges it exactly as merging the whole state would. An
    /// over-claiming witness starves only the claimant, which is why it
    /// arrives as a bare [`DotSet`] claim rather than an evidence type.
    #[must_use]
    fn novel_to_witnessed(&self, context: &DotSet, recording: &DotSet) -> Self {
        let _ = recording;
        self.novel_to(context)
    }
}

/// The bare dot store: presence only, no content beyond the dots themselves.
///
/// The [`DotSet`] is both the *context* half of every causal pair and the
/// simplest store shape (the two roles are one lattice object, which is the
/// dotted-vector literature's own economy). As a store it models
/// enable-shaped state: a flag is on while any dot survives, off when every
/// minted dot has been superseded.
impl DotStore for DotSet {
    fn dots(&self) -> impl Iterator<Item = Dot> + '_ {
        // The inherent enumeration read is already the support.
        Self::dots(self)
    }

    fn is_bottom(&self) -> bool {
        *self == BOTTOM
    }

    fn causal_merge(&self, self_context: &DotSet, other: &Self, other_context: &DotSet) -> Self {
        // The survivor law, verbatim: kept by both, or held here and never
        // seen there, or held there and never seen here.
        let mut survivors = self.intersect(other);
        for dot in self.difference(other_context) {
            let _ = survivors.insert(dot);
        }
        for dot in other.difference(self_context) {
            let _ = survivors.insert(dot);
        }
        survivors
    }

    fn causal_merge_from(&mut self, self_context: &DotSet, other: &Self, other_context: &DotSet) {
        // The survivor law read as edits against `self` instead of a rebuild,
        // both sides bounded by what actually changed rather than what is held:
        //
        // * a held dot dies iff the other side has seen it and dropped it,
        //   i.e. it lies in `other_context` outside `other`'s store; that set
        //   is the residual `other_context \ other` (removals conveyed), never
        //   the document;
        // * a foreign dot enters iff this side has never seen it, the residual
        //   `other \ self_context`; a dot in both stores stays untouched, and
        //   a dot this context covers without holding was dropped *here*, so
        //   it must not resurrect (skipping it is the survivor law's third
        //   arm, not an optimization).
        //
        // The removal pass collects before mutating (the residual iterator
        // borrows `self` immutably through `contains`), sized by the delta's
        // removals, not the store.
        let removed: alloc::vec::Vec<Dot> = other_context
            .difference(other)
            .filter(|&dot| self.contains(dot))
            .collect();
        for dot in removed {
            let _ = self.remove(dot);
        }
        for dot in other.difference(self_context) {
            let _ = self.insert(dot);
        }
    }

    fn restrict(&self, roster: impl IntoIterator<Item = u32>) -> Self {
        // The inherent read is already the fiber selection.
        Self::restrict(self, roster)
    }

    fn support(&self) -> DotSet {
        // The store IS its support (the two roles are one lattice object),
        // so the compact form clones instead of re-folding per dot.
        self.clone()
    }

    fn novel_to(&self, context: &DotSet) -> Self {
        // Exactly the held dots the peer's context has not seen.
        let mut novel = Self::new();
        for dot in self.difference(context) {
            let _ = novel.insert(dot);
        }
        novel
    }
}