minerva 0.2.0

//! Generated sealed-shadow boundary laws.

extern crate alloc;

use alloc::collections::BTreeSet;
use alloc::vec::Vec;

use proptest::prelude::*;

use super::*;

/// A seed program is interpreted into a causally valid history. The
/// boundary is crossed at every split and under every causal window arrival
/// order, where the maintained shadow must match eager judgment at every
/// prefix in reading, decisions, and injective identities.
#[derive(Clone, Copy, Debug)]
enum OpSeed {
    Birth {
        anchor: u8,
        side: bool,
        rank: u8,
    },
    Delete {
        target: u8,
    },
    Move {
        target: u8,
        anchor: u8,
        side: bool,
        rank: u8,
    },
}

fn pick_anchor(dots: &[Dot], seed: u8, side: bool) -> Anchor {
    let slot = usize::from(seed) % (dots.len() + 1);
    if slot == dots.len() {
        Anchor::Origin
    } else if side {
        Anchor::Before(dots[slot])
    } else {
        Anchor::After(dots[slot])
    }
}

fn interpret(seeds: &[OpSeed]) -> Vec<Delta> {
    let mut deltas = Vec::new();
    let mut dots: Vec<Dot> = Vec::new();
    let mut next_index = 1u8;
    let mut next_testimony = 1u8;
    for seed in seeds {
        match *seed {
            OpSeed::Birth { anchor, side, rank } => {
                let locus = Locus {
                    anchor: pick_anchor(&dots, anchor, side),
                    rank: rank % 3,
                };
                let dot = Dot::old(next_index);
                deltas.push(Delta::Birth {
                    dot,
                    label: char::from(b'a' + (next_index - 1) % 26),
                    locus,
                });
                dots.push(dot);
                next_index += 1;
            }
            OpSeed::Delete { target } => {
                if dots.is_empty() {
                    continue;
                }
                deltas.push(Delta::Delete {
                    target: dots[usize::from(target) % dots.len()],
                });
            }
            OpSeed::Move {
                target,
                anchor,
                side,
                rank,
            } => {
                if dots.is_empty() {
                    continue;
                }
                deltas.push(Delta::Move(Movement {
                    testimony: Testimony(next_testimony),
                    target: dots[usize::from(target) % dots.len()],
                    to: Locus {
                        anchor: pick_anchor(&dots, anchor, side),
                        rank: rank % 3,
                    },
                }));
                next_testimony += 1;
            }
        }
    }
    deltas
}

fn stratum(prefix: &[Delta]) -> (State, Vec<Movement>) {
    let mut raw = State::new();
    let mut record = Vec::new();
    for delta in prefix {
        match *delta {
            Delta::Birth { dot, label, locus } => raw.insert(
                dot,
                Node {
                    label,
                    locus,
                    visible: true,
                },
            ),
            Delta::Delete { target } => {
                raw.nodes
                    .get_mut(&target)
                    .expect("a delete names a woven dot")
                    .visible = false;
            }
            Delta::Move(movement) => record.push(movement),
        }
    }
    (raw, record)
}

fn references(delta: &Delta) -> Vec<Dot> {
    match *delta {
        Delta::Birth { locus, .. } => locus.anchor.dot().into_iter().collect(),
        Delta::Delete { target } => [target].into(),
        Delta::Move(movement) => core::iter::once(movement.target)
            .chain(movement.to.anchor.dot())
            .collect(),
    }
}

fn is_causal(order: &[Delta]) -> bool {
    let mut born: BTreeSet<Dot> = BTreeSet::new();
    for delta in order {
        if !references(delta).iter().all(|dot| born.contains(dot)) {
            return false;
        }
        if let Delta::Birth { dot, .. } = delta {
            let _ = born.insert(*dot);
        }
    }
    true
}

/// Every causal arrival order, exhaustively. The generated history is
/// bounded to five deltas so this enumeration never samples. The original
/// order is causal by construction, so at least one order survives.
fn causal_orders(window: &[Delta], stratum_dots: &BTreeSet<Dot>) -> Vec<Vec<Delta>> {
    let causal_over = |order: &[Delta]| -> bool {
        let mut born: BTreeSet<Dot> = stratum_dots.clone();
        for delta in order {
            if !references(delta).iter().all(|dot| born.contains(dot)) {
                return false;
            }
            if let Delta::Birth { dot, .. } = delta {
                let _ = born.insert(*dot);
            }
        }
        true
    };

    let mut orders = Vec::new();
    permute(&mut window.to_vec(), 0, &mut |candidate| {
        if causal_over(candidate) {
            orders.push(candidate.to_vec());
        }
    });
    orders
}

fn permute<T: Copy>(items: &mut [T], from: usize, visit: &mut impl FnMut(&[T])) {
    if from == items.len() {
        visit(items);
        return;
    }
    for pivot in from..items.len() {
        items.swap(from, pivot);
        permute(items, from + 1, visit);
        items.swap(from, pivot);
    }
}

proptest! {
    #[test]
    fn prop_the_boundary_holds_reading_equality_at_every_split(
        seeds in proptest::collection::vec(
            prop_oneof![
                (any::<u8>(), any::<bool>(), any::<u8>())
                    .prop_map(|(anchor, side, rank)| OpSeed::Birth { anchor, side, rank }),
                any::<u8>().prop_map(|target| OpSeed::Delete { target }),
                (any::<u8>(), any::<u8>(), any::<bool>(), any::<u8>()).prop_map(
                    |(target, anchor, side, rank)| OpSeed::Move { target, anchor, side, rank }
                ),
            ],
            0..6,
        )
    ) {
        let history = interpret(&seeds);
        prop_assert!(is_causal(&history));
        for split in 0..=history.len() {
            let (raw, record) = stratum(&history[..split]);
            let window = &history[split..];

            let eager = cross_boundary_shadow(&raw, &record, window);
            prop_assert!(eager.commutes(), "split {split}: {eager:?}");

            // Two independent declaration rules must mint the same live
            // compaction: the S213 refound and the shadow's map both read
            // the effective stratum in walk order, never dot order.
            let (effective, _) = judge(&raw, &record, &[]);
            let stratum_map = DotMap::at_declaration(&effective);
            let refounded = effective.refound(BoundarySupport::PositionOnly);
            prop_assert_eq!(&refounded.translation.dots, &stratum_map.compacted);

            let stratum_dots: BTreeSet<Dot> = raw.nodes.keys().copied().collect();
            for order in causal_orders(window, &stratum_dots) {
                let mut shadow = Shadow::declare(&raw, &record);
                let frozen = shadow.map.clone();
                let mut delivered: Vec<Delta> = Vec::new();
                for delta in order {
                    shadow.deliver(delta);
                    delivered.push(delta);
                    let (expected, expected_decisions) = judge(&raw, &record, &delivered);
                    prop_assert_eq!(shadow.projected_reading(), expected.reading());
                    prop_assert_eq!(&shadow.decisions, &expected_decisions);
                    prop_assert_eq!(
                        shadow.projected_identities(),
                        eager_projection(&stratum_map, &expected)
                    );
                }
                prop_assert_eq!(&shadow.map, &frozen);
                prop_assert_eq!(shadow.projected_reading(), eager.shadow_projection.clone());

                let identities = shadow.projected_identities();
                let distinct: BTreeSet<Dot> = identities.iter().map(|(dot, _)| *dot).collect();
                prop_assert_eq!(distinct.len(), identities.len());
                prop_assert!(identities.iter().all(|(dot, _)| dot.epoch == Epoch(1)));
            }
        }
    }
}