minerva 0.2.0

//! The epoch re-foundation fold (PRD 0024 stage one).
//!
//! `refound` is the pure `state -> (state, map)` fold the charter specifies:
//! the recension at the cut bakes into placement, live elements re-mint per
//! original station in walk order (so the new store is born coalesced and
//! its recording have-set born floor-perfect), the movement record sweeps to
//! zero (the caller starts the new epoch's pair fresh), and the dot map is
//! closed-form per station: live-at-cut compaction below the ceiling, the
//! affine shift above it. Nothing here declares, gates, or seals: the caller
//! owes the witness that the input is a sealed stratum (stage two carries
//! that duty behind `Stability::watermark_cut`), and the fold refuses the
//! one shape that contradicts it locally, an unplaced woven dot or a pending
//! movement, since a witnessed cut is causally closed and can carry neither.
//!
//! Determinism is the whole point: same stratum, same fold, same output at
//! every replica, so re-minted ranks come from a fixed base per station
//! (never a live clock) and interiors step by the snapshot codec's own
//! successor law, the same spelling the identity plane coalesces.
//!
//! The R2 proof plan is split per ruling R-9: the identity arithmetic (the
//! per-station re-mint) is the dual-homed Creusot core in [`pure`], the
//! affine half of the dot map is the heap-free Kani harness below, and the
//! refusal shell plus the store folds stay sampled in `tests/refound.rs`.

extern crate alloc;

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

use crate::kairos::Kairos;
use crate::metis::metathesis::Metatheses;
use crate::metis::{DotSet, VersionVector};

use super::Rhapsody;
use super::placement::{Anchor, Dot, Locus};
use super::wire::apply_chain_step;

mod pure;
mod wire;

pub use wire::{RefoundMapDecodeBudget, RefoundMapDecodeError};

use pure::remint;

/// The refusal for a stratum that cannot be sealed.
///
/// A woven dot whose anchor chain does not reach the origin, or a movement
/// still pending its support. A witnessed cut is causally closed, so
/// neither can exist at one; their presence means the input is not the
/// sealed stratum the fold is defined on, and the fold refuses rather than
/// silently dropping content.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct UnsealedStratum {
    /// The first offending dot: unplaced content, or a pending movement's
    /// testimony.
    pub dot: Dot,
}

/// The re-foundation's dot map, frozen by the fold.
///
/// Live-at-cut dots carry their compacted image, dots above a station's
/// ceiling translate by the affine rule, and a swept order tombstone has no
/// image at all (it is answerable only in the old epoch's shadow, PRD 0024
/// R3).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct RefoundMap {
    /// Live at the cut, in walk order: old dot to new dot.
    compacted: BTreeMap<Dot, Dot>,
    /// Per-station cut ceilings: the woven high water of the sealed stratum.
    ceilings: VersionVector,
    /// Per-station live counts, the compacted range's width.
    live: BTreeMap<u32, u64>,
}

impl RefoundMap {
    /// Binds the affine half to the witnessed epoch cut.
    ///
    /// The standalone fold uses woven high water because it has no witness;
    /// an epoch stratum has the stronger boundary. Sparse or removed
    /// identities below that cut must remain untranslatable rather than
    /// masquerading as window births.
    pub(crate) fn bind_cut(&mut self, cut: &crate::metis::Cut) {
        debug_assert!(
            self.compacted
                .keys()
                .all(|dot| dot.counter() <= cut.as_vector().get(dot.station()))
        );
        self.ceilings = cut.as_vector().clone();
    }

    /// Translates one old-epoch dot. Live-at-cut dots compact, dots above
    /// the station's ceiling shift affinely (collision-free, order- and
    /// consecutiveness-preserving, so window-born chains survive verbatim),
    /// and a swept tombstone returns `None`: the map refuses to guess a
    /// position for an identity that did not cross.
    #[must_use]
    pub fn translate(&self, dot: Dot) -> Option<Dot> {
        if let Some(&new) = self.compacted.get(&dot) {
            return Some(new);
        }
        let ceiling = self.ceilings.get(dot.station());
        if dot.counter() > ceiling {
            let live = self.live.get(&dot.station()).copied().unwrap_or(0);
            // The affine image is `live + (dot - ceiling)` under
            // `ceiling < dot`, so it is at least one and the crossing back
            // into identity space never refuses (the Kani harness below
            // proves the bound); the read stays total rather than
            // asserting it (ruling R-91).
            return NonZeroU64::new(affine(live, ceiling, dot.counter()))
                .map(|counter| Dot::new(dot.station(), counter));
        }
        None
    }

    /// How many live elements crossed: the compacted domain's size.
    #[must_use]
    pub fn live_len(&self) -> usize {
        self.compacted.len()
    }

    #[cfg(feature = "instrumentation")]
    pub(crate) fn structural_counts(&self) -> (usize, usize, usize) {
        (
            self.compacted.len(),
            self.ceilings.iter().count(),
            self.live.len(),
        )
    }

    /// One station's compacted live count (crate-internal: the consignment's
    /// structural context translation, which describes the live images as
    /// the range `1..=live` instead of enumerating swept history).
    pub(crate) fn live_of(&self, station: u32) -> u64 {
        self.live.get(&station).copied().unwrap_or(0)
    }

    /// One station's frozen ceiling (crate-internal, the same seam: the
    /// affine window portion starts just above it).
    pub(crate) fn ceiling_of(&self, station: u32) -> u64 {
        self.ceilings.get(station)
    }
}

/// The affine half of the dot map: a dot above the ceiling lands `dot -
/// ceiling` slots above the compacted range. Sound because a station's live
/// count never exceeds its ceiling (each live dot is a distinct woven
/// counter at or below it), so the sum never overflows and always lands
/// strictly above the compacted range; the Kani harness below proves the
/// arithmetic over the full symbolic space.
fn affine(live: u64, ceiling: u64, dot: u64) -> u64 {
    debug_assert!(live <= ceiling && ceiling < dot);
    live + (dot - ceiling)
}

/// The fold's output: the re-founded store and the frozen dot map.
#[derive(Clone, Debug)]
pub struct Refounded {
    store: Rhapsody,
    map: RefoundMap,
}

impl Refounded {
    /// The re-founded store: live content only, born coalesced, its
    /// recording have-set floor-perfect by construction.
    #[must_use]
    pub const fn store(&self) -> &Rhapsody {
        &self.store
    }

    /// The frozen dot map.
    #[must_use]
    pub const fn map(&self) -> &RefoundMap {
        &self.map
    }

    /// Surrenders both halves.
    #[must_use]
    pub fn into_parts(self) -> (Rhapsody, RefoundMap) {
        (self.store, self.map)
    }
}

impl Rhapsody {
    /// The epoch re-foundation fold (PRD 0024 R2): a pure function of the
    /// sealed stratum. The recension over `moves` bakes into placement. Every
    /// live element re-mints per original station in walk order, so station
    /// `s`'s survivors become `(s, 1..=n_s)` and the new store is born
    /// coalesced. Order tombstones and superseded or refused testimonies
    /// vanish. The returned map carries the closed-form translation. The
    /// movement record sweeps to zero: the new epoch's pair starts empty,
    /// which is the caller's to construct.
    ///
    /// Refuses a stratum that a witnessed cut could not have produced (an
    /// unplaced woven dot, or a movement pending its support): folding one
    /// would silently drop content, and the fold will not guess.
    ///
    /// # Errors
    ///
    /// Returns [`UnsealedStratum`] naming the first offending dot.
    pub fn refound(&self, moves: &Metatheses) -> Result<Refounded, UnsealedStratum> {
        let recension = self.recension(moves);
        self.refound_recension(&recension)
    }

    /// The fold half of [`refound`](Self::refound), over an
    /// already-derived recension (PRD 0024's fused transition seam): the
    /// epoch stratum derives the decision surface once and both retains it
    /// and folds through it, instead of replaying the same pair three
    /// times (the S268 measurement's duplicate-derivation term).
    ///
    /// Crate-internal precondition: `recension` is the recension of
    /// exactly `(self, moves)` for the same movement record the caller
    /// validates against; the public door above discharges it by
    /// construction, and [`crate::metis::EpochStratum`] discharges it by
    /// deriving the recension from the pair it consumes.
    pub(in crate::metis) fn refound_recension(
        &self,
        recension: &super::recension::Recension,
    ) -> Result<Refounded, UnsealedStratum> {
        if let Some(&dot) = recension.pending().first() {
            return Err(UnsealedStratum { dot });
        }
        for dot in self.woven.dots() {
            if !recension.is_reachable(dot) {
                return Err(UnsealedStratum { dot });
            }
        }

        // The walk yields visible elements only (the `OrderWalk` contract),
        // so this is exactly the effective live order: tombstones never
        // enter the loop and never cross. The identity arithmetic (station
        // `s`'s `k`-th walk element mints `(s, k)`) is the proven pure core
        // (`pure::remint`, the R2 deductive obligations); this fold spells
        // loci over its output and folds the stores, the unproven-but-thin
        // adapter of the dual-homed discipline.
        let order = recension.order();
        // The proven pure core is tuple-typed by the dual-home constraint
        // (spec rule 10), so the adapter surrenders the identity proof at
        // its door and re-earns it on the way back.
        let raw_order: alloc::vec::Vec<(u32, u64)> =
            order.iter().copied().map(<(u32, u64)>::from).collect();
        let assignment = remint(&raw_order);
        debug_assert_eq!(order.len(), assignment.minted.len());

        let mut skeleton = BTreeMap::new();
        let mut visible = DotSet::new();
        let mut compacted = BTreeMap::new();
        let mut prev: Option<((u32, u64), Locus)> = None;
        for (&old, &raw_new) in order.iter().zip(&assignment.minted) {
            let station = raw_new.0;
            // The core mints `(s, 1..=n_s)` per station (its proven
            // compaction image), so every re-mint is an identity.
            let new_dot = Dot::try_from(raw_new)
                .expect("the re-mint core compacts onto the one-based range 1..=n");
            let locus = match prev {
                // The immediate walk predecessor on the same station: the
                // core's consecutiveness contract makes the dots successor-
                // adjacent, so the successor law's spelling keeps the chain
                // inline.
                Some((prev_dot, prev_locus)) if prev_dot.0 == station => {
                    apply_chain_step(prev_dot, &prev_locus, 0)
                }
                Some((prev_dot, _)) => Locus {
                    anchor: Anchor::After(prev_dot.into()),
                    rank: base_rank(station),
                },
                None => Locus {
                    anchor: Anchor::Origin,
                    rank: base_rank(station),
                },
            };
            let _ = skeleton.insert(new_dot, locus);
            let _ = visible.insert(new_dot);
            let _ = compacted.insert(old, new_dot);
            prev = Some((raw_new, locus));
        }

        Ok(Refounded {
            store: Self::from_parts(skeleton, visible),
            map: RefoundMap {
                compacted,
                ceilings: self.woven.high_water(),
                live: assignment.live.iter().copied().collect(),
            },
        })
    }
}

impl super::recension::Recension {
    /// The seal consignment's store half (PRD 0024 stage four, ruling R-50):
    /// the old epoch's complete final reading, re-spelled as the next
    /// generation's opening skeleton through the declaration-frozen map.
    ///
    /// The walk is the performed sequence's tombstone-inclusive slot
    /// order, so the outcome of every window judgment crosses whole: a
    /// window-born survivor is woven at its judged place, a window-moved
    /// element's image sits where the old world's replay put it, and a
    /// cut-live element the window deleted keeps its locus as an order
    /// tombstone (a native weave minted against the pristine plane may
    /// still anchor it). Two shapes do not cross: an identity dead at the
    /// cut has no image in the frozen map (it is answerable only in the
    /// shadow, and its subtree is linearized past it), and an identity
    /// born and superseded inside the window crosses as context only
    /// (nothing in the new plane can anchor it: natives never saw it, and
    /// old-addressed replays absorb at the recognizer). Identities come
    /// from the frozen map alone, never a fresh re-mint, because native
    /// content minted during the window already anchors those images; the
    /// spelling (chain anchors, fixed base ranks, the successor law on
    /// adjacent images) is `refound`'s own, so a future native mint's
    /// clock-born rank strictly dominates every carried head.
    ///
    /// Verbatim anchors cannot do this job: a window birth's honest rank
    /// can lose its old bucket's contest to a cut-live sibling whose rank
    /// the re-foundation re-based, flipping the pair's reading (the
    /// rank-contest falsifier beside the two S213 falsifiers, in
    /// `tests/epoch_shadow/`). Only the judged outcome is stable, so
    /// only the outcome crosses.
    ///
    /// Callers pass the cut-bound map of the epoch machinery; the epoch
    /// seal (`EpochShadow::consign`) is the one witnessed door. The fold
    /// refuses a reading a complete sealed window could not have produced
    /// (an unplaced birth, a pending movement): every mint rides its
    /// minter's own floor into the adoption join, so at a lawful seal
    /// both are unreachable.
    ///
    /// # Errors
    ///
    /// Returns [`UnsealedStratum`] naming the first unplaced birth or
    /// pending testimony.
    pub(in crate::metis) fn consign_store(
        &self,
        map: &RefoundMap,
    ) -> Result<Rhapsody, UnsealedStratum> {
        if let Some(&dot) = self.pending().first() {
            return Err(UnsealedStratum { dot });
        }
        let performed = self.performed();
        if let Some(&dot) = performed.unplaced.first() {
            return Err(UnsealedStratum { dot });
        }

        let mut skeleton = BTreeMap::new();
        let mut visible_set = DotSet::new();
        let mut prev: Option<(Dot, Locus)> = None;
        for (old, visible) in performed.thread.slots() {
            let Some(new_dot) = map.translate(old) else {
                // Dead at the cut: swept, answerable only in the shadow.
                continue;
            };
            if !visible && old.counter() > map.ceilings.get(old.station()) {
                // Born and superseded inside the window: context-only.
                continue;
            }
            let locus = match prev {
                // Adjacent images on one station keep the chain inline by
                // the successor law. Unlike `refound`'s fresh re-mint, the
                // frozen map does not renumber this walk, so adjacency is
                // checked, never assumed.
                Some((prev_dot, prev_locus))
                    if prev_dot.station() == new_dot.station()
                        && prev_dot.counter().checked_add(1) == Some(new_dot.counter()) =>
                {
                    apply_chain_step(prev_dot.into(), &prev_locus, 0)
                }
                Some((prev_dot, _)) => Locus {
                    anchor: Anchor::After(prev_dot.into()),
                    rank: base_rank(new_dot.station()),
                },
                None => Locus {
                    anchor: Anchor::Origin,
                    rank: base_rank(new_dot.station()),
                },
            };
            let _ = skeleton.insert(new_dot, locus);
            if visible {
                let _ = visible_set.insert(new_dot);
            }
            prev = Some((new_dot, locus));
        }

        Ok(Rhapsody::from_parts(skeleton, visible_set))
    }
}

/// The deterministic rank base for a station's re-minted heads. Every
/// replica folds the same stratum to the same ranks, so no live clock may
/// enter; ranks are sibling discriminators and replay keys, never
/// externally referenced values, and every re-minted bucket is a singleton,
/// so the fixed base carries no ordering weight of its own. A future native
/// mint's clock-born rank strictly dominates it, which is exactly the
/// visual-insert discipline's expectation.
fn base_rank(station: u32) -> Kairos {
    Kairos::new(0, 0, station, 0u16)
}

#[cfg(kani)]
mod proofs {
    use super::affine;

    /// The dot map's closed-form arithmetic, over the full symbolic space
    /// of the sealed bounds (PRD 0024 R2): under `live <= ceiling < dot`
    /// the shift never overflows (it is bounded by the old dot itself),
    /// always lands strictly above the compacted range, and preserves
    /// order, consecutiveness, and injectivity, so window-born chains
    /// survive translation verbatim.
    #[kani::proof]
    fn the_affine_shift_is_sound_over_the_sealed_bounds() {
        let live: u64 = kani::any();
        let ceiling: u64 = kani::any();
        let first: u64 = kani::any();
        let second: u64 = kani::any();
        kani::assume(live <= ceiling);
        kani::assume(ceiling < first);
        kani::assume(ceiling < second);

        let shifted_first = affine(live, ceiling, first);
        let shifted_second = affine(live, ceiling, second);

        assert!(shifted_first <= first);
        assert!(shifted_first > live);
        if first < second {
            assert!(shifted_first < shifted_second);
        }
        if first < u64::MAX && second == first + 1 {
            assert!(shifted_second == shifted_first + 1);
        }
        if first != second {
            assert!(shifted_first != shifted_second);
        }
    }
}