minerva 0.2.0

//! Sealed-stratum shadow model and its laws.

mod cases;
mod properties;

use super::*;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum Delta {
    Birth { dot: Dot, label: char, locus: Locus },
    Delete { target: Dot },
    Move(Movement),
}

/// The eager contract form: the old world judges the whole delivered set at
/// once. Births and deletes enter the basis, then the retained movement
/// record and the window's movements replay together in the one fixed
/// `(rank, testimony)` order, so the outcome is a pure function of the sets,
/// never of arrival order.
fn judge(raw: &State, record: &[Movement], window: &[Delta]) -> (State, Vec<Decision>) {
    let mut state = raw.clone();
    let mut movements = record.to_vec();
    for delta in window {
        match *delta {
            Delta::Birth { dot, label, locus } => state.insert(
                dot,
                Node {
                    label,
                    locus,
                    visible: true,
                },
            ),
            Delta::Delete { target } => {
                state
                    .nodes
                    .get_mut(&target)
                    .expect("a delete names a woven dot")
                    .visible = false;
            }
            Delta::Move(movement) => movements.push(movement),
        }
    }
    let decisions = replay(&mut state, &movements);
    (state, decisions)
}

/// The dot map, frozen at declaration from the sealed stratum alone: live
/// elements compact into `1..=n_live` in walk order, and window-born dots
/// (above the cut ceiling) shift by the affine rule `n_live + (index -
/// ceiling)`, collision-free and consecutive-preserving. A swept tombstone
/// has no image; it is answerable only inside the shadow.
#[derive(Clone, Debug, PartialEq, Eq)]
struct DotMap {
    next_epoch: Epoch,
    compacted: BTreeMap<Dot, Dot>,
    n_live: u8,
    cut_ceiling: u8,
}

impl DotMap {
    fn at_declaration(effective: &State) -> Self {
        let next_epoch = Epoch(effective.epoch.0.checked_add(1).expect("bounded toy epoch"));
        let cut_ceiling = effective
            .nodes
            .keys()
            .map(|dot| dot.index)
            .max()
            .unwrap_or(0);
        let mut compacted = BTreeMap::new();
        for dot in effective.walk() {
            if effective.nodes[&dot].visible {
                let index = u8::try_from(compacted.len() + 1).expect("bounded toy state");
                let _ = compacted.insert(
                    dot,
                    Dot {
                        epoch: next_epoch,
                        index,
                    },
                );
            }
        }
        let n_live = u8::try_from(compacted.len()).expect("bounded toy state");
        Self {
            next_epoch,
            compacted,
            n_live,
            cut_ceiling,
        }
    }

    fn translate(&self, old: Dot) -> Dot {
        self.compacted.get(&old).copied().unwrap_or_else(|| {
            assert!(
                old.index > self.cut_ceiling,
                "a swept tombstone stays in the shadow; only live-at-cut and window-born dots cross"
            );
            Dot {
                epoch: self.next_epoch,
                index: self
                    .n_live
                    .checked_add(old.index - self.cut_ceiling)
                    .expect("bounded toy state"),
            }
        })
    }
}

/// The maintained form of the boundary: the shadow retains the old epoch's
/// basis and movement record, folds old-addressed arrivals, and owes exact
/// agreement with [`judge`] over the delivered set at every moment.
struct Shadow {
    raw: State,
    record: Vec<Movement>,
    map: DotMap,
    window: Vec<Delta>,
    judged: State,
    decisions: Vec<Decision>,
}

impl Shadow {
    fn declare(raw: &State, record: &[Movement]) -> Self {
        let (judged, decisions) = judge(raw, record, &[]);
        let map = DotMap::at_declaration(&judged);
        Self {
            raw: raw.clone(),
            record: record.to_vec(),
            map,
            window: Vec::new(),
            judged,
            decisions,
        }
    }

    /// Fold one old-addressed arrival. Births and deletes extend the judged
    /// state directly: a fresh node never enters an existing ancestor chain
    /// and visibility is not consulted by the replay, so neither can change
    /// an already-issued verdict. A movement extends directly only when its
    /// replay key sorts after every movement already judged; an out-of-order
    /// arrival rebuilds from the frozen basis, the collation pattern at toy
    /// grade.
    fn deliver(&mut self, delta: Delta) {
        match delta {
            Delta::Birth { dot, label, locus } => {
                self.window.push(delta);
                self.judged.insert(
                    dot,
                    Node {
                        label,
                        locus,
                        visible: true,
                    },
                );
            }
            Delta::Delete { target } => {
                self.window.push(delta);
                self.judged
                    .nodes
                    .get_mut(&target)
                    .expect("a delete names a woven dot")
                    .visible = false;
            }
            Delta::Move(movement) => {
                let key = (movement.to.rank, movement.testimony);
                let last = self
                    .record
                    .iter()
                    .chain(self.window.iter().filter_map(|delta| match delta {
                        Delta::Move(movement) => Some(movement),
                        _ => None,
                    }))
                    .map(|movement| (movement.to.rank, movement.testimony))
                    .max();
                self.window.push(delta);
                if last.is_none_or(|last| key > last) {
                    let verdict = self.judged.apply(movement);
                    self.decisions.push(Decision {
                        testimony: movement.testimony,
                        verdict,
                    });
                } else {
                    let (judged, decisions) = judge(&self.raw, &self.record, &self.window);
                    self.judged = judged;
                    self.decisions = decisions;
                }
            }
        }
    }

    fn projected_reading(&self) -> Vec<char> {
        self.judged.reading()
    }

    /// The re-founded projection itself: every visible element crossed into
    /// the new epoch under the frozen map, in judged order. Total by
    /// construction, since a visible element is live at the cut or
    /// window-born; a swept tombstone is never visible and never asked for.
    /// [`Self::projected_reading`] is this sequence's label component.
    fn projected_identities(&self) -> Vec<(Dot, char)> {
        eager_projection(&self.map, &self.judged)
    }
}

/// Project a judged old-world state through a declaration-frozen map. The
/// maintained and eager boundary forms share this one projection rule; what
/// the agreement law varies is the judged state's construction (incremental
/// against recomputed) and the map object (the shadow's frozen copy against
/// one rebuilt from the stratum), with the map rule itself cross-checked
/// against `refound`'s independent compaction.
fn eager_projection(map: &DotMap, judged: &State) -> Vec<(Dot, char)> {
    judged
        .walk()
        .into_iter()
        .filter(|dot| judged.nodes[dot].visible)
        .map(|dot| (map.translate(dot), judged.nodes[&dot].label))
        .collect()
}

#[derive(Clone, Debug, PartialEq, Eq)]
struct ShadowBoundaryResult {
    fold_then_refound: Vec<char>,
    shadow_projection: Vec<char>,
    old_decisions: Vec<Decision>,
    shadow_decisions: Vec<Decision>,
}

impl ShadowBoundaryResult {
    fn commutes(&self) -> bool {
        self.fold_then_refound == self.shadow_projection
            && self.old_decisions == self.shadow_decisions
    }
}

/// The two squares under the shadow shape: fold the window in the old epoch
/// and re-found after, against declare at the cut and deliver old-addressed
/// through the shadow.
fn cross_boundary_shadow(
    raw_at_cut: &State,
    record: &[Movement],
    window: &[Delta],
) -> ShadowBoundaryResult {
    let (folded, old_decisions) = judge(raw_at_cut, record, window);
    let fold_then_refound = folded
        .refound(BoundarySupport::PositionOnly)
        .state
        .reading();

    let mut shadow = Shadow::declare(raw_at_cut, record);
    for delta in window {
        shadow.deliver(*delta);
    }

    ShadowBoundaryResult {
        fold_then_refound,
        shadow_projection: shadow.projected_reading(),
        old_decisions,
        shadow_decisions: shadow.decisions,
    }
}