minerva 0.2.0

use super::super::support::arb_vv;
use super::quorum::Quorum;
use crate::metis::{
    And, AndProgress, Causal, EpochAddress, EpochGate, Fifo, Gate, GateLawCheckError, GateLawPoint,
    check_gate_laws,
};
use proptest::prelude::*;

fn epoch_address(generation: u64, station: u32, counter: u64) -> EpochAddress {
    EpochAddress::try_from_parts(generation, (station, counter))
        .expect("property strategy generates valid addresses")
}

proptest! {
    /// The causal gate is terminal and disjoint over arbitrary comparable progresses.
    #[test]
    fn prop_causal_gate_is_terminal(
        low in arb_vv(), delta in arb_vv(), sender in 0u32..6, dep in arb_vv(),
    ) {
        let high = low.merge(&delta);
        prop_assert_eq!(check_gate_laws::<Causal>(&low, &high, sender, &dep), Ok(()));
    }

    /// The scalar FIFO gate satisfies the same laws.
    #[test]
    fn prop_fifo_gate_is_terminal(
        low in arb_vv(), delta in arb_vv(), sender in 0u32..6, seq in 0u64..16,
    ) {
        let high = low.merge(&delta);
        prop_assert_eq!(check_gate_laws::<Fifo>(&low, &high, sender, &seq), Ok(()));
    }

    /// The non-causal Quorum gate proves the harness is not secretly causal-shaped.
    #[test]
    fn prop_quorum_gate_is_terminal(
        low in arb_vv(), delta in arb_vv(), sender in 0u32..6, required in 0u64..8,
    ) {
        let high = low.merge(&delta);
        prop_assert_eq!(check_gate_laws::<Quorum>(&low, &high, sender, &required), Ok(()));
    }

    /// The product gate satisfies the laws under its componentwise progress order.
    #[test]
    fn prop_and_gate_is_terminal(
        left in arb_vv(), right in arb_vv(),
        left_delta in arb_vv(), right_delta in arb_vv(),
        sender in 0u32..6, dep in arb_vv(), required in 0u64..8,
    ) {
        let low = AndProgress::new(left, right);
        let high = AndProgress::new(
            low.left().merge(&left_delta),
            low.right().merge(&right_delta),
        );
        prop_assert_eq!(
            check_gate_laws::<And<Causal, Quorum>>(
                &low,
                &high,
                sender,
                &(dep, required),
            ),
            Ok(()),
        );
    }

    /// The externally opened epoch gate satisfies the laws over its reachable states.
    #[test]
    fn prop_epoch_gate_is_terminal(
        generation in 1u64..32,
        station in any::<u32>(),
        counter in 1u64..32,
        dep_generation in 1u64..32,
        dep_station in any::<u32>(),
        dep_counter in 1u64..32,
    ) {
        let adopted = epoch_address(generation, station, counter);
        let dep = epoch_address(dep_generation, dep_station, dep_counter);
        let bottom = None;
        let latched = Some(adopted);

        prop_assert_eq!(check_gate_laws::<EpochGate>(&bottom, &bottom, station, &dep), Ok(()));
        prop_assert_eq!(check_gate_laws::<EpochGate>(&bottom, &latched, station, &dep), Ok(()));
        prop_assert_eq!(check_gate_laws::<EpochGate>(&latched, &latched, station, &dep), Ok(()));
    }
}

struct ProductOrderGate;

impl Gate for ProductOrderGate {
    type Dep = ();
    type Progress = AndProgress<u8, u8>;

    fn deliverable(_progress: &Self::Progress, _sender: u32, _dep: &Self::Dep) -> bool {
        false
    }

    fn advance(_progress: &mut Self::Progress, _sender: u32, _dep: &Self::Dep) {}

    fn stale(_progress: &Self::Progress, _sender: u32, _dep: &Self::Dep) -> bool {
        false
    }
}

#[derive(Clone, Copy)]
enum Fault {
    RegressLower,
    RegressUpper,
    OverlapLower,
    OverlapUpper,
    StaleReopens,
    StableReopens,
}

struct FaultyGate;

impl Gate for FaultyGate {
    type Dep = Fault;
    type Progress = u8;

    fn deliverable(progress: &Self::Progress, _sender: u32, fault: &Self::Dep) -> bool {
        matches!(
            (fault, progress),
            (Fault::OverlapLower | Fault::StableReopens, 1) | (Fault::OverlapUpper, 2)
        )
    }

    fn advance(progress: &mut Self::Progress, _sender: u32, fault: &Self::Dep) {
        match (fault, *progress) {
            (Fault::RegressLower, 1) => *progress = 0,
            (Fault::RegressUpper, 2) => *progress = 1,
            _ => {}
        }
    }

    fn stale(progress: &Self::Progress, _sender: u32, fault: &Self::Dep) -> bool {
        matches!(
            (fault, progress),
            (Fault::OverlapLower | Fault::StaleReopens, 1) | (Fault::OverlapUpper, 2)
        )
    }
}

#[test]
fn gate_law_checker_rejects_malformed_progress_pairs() {
    assert_eq!(
        check_gate_laws::<ProductOrderGate>(
            &AndProgress::new(2, 2),
            &AndProgress::new(1, 1),
            0,
            &(),
        ),
        Err(GateLawCheckError::ProgressDescends),
    );
    assert_eq!(
        check_gate_laws::<ProductOrderGate>(
            &AndProgress::new(1, 0),
            &AndProgress::new(0, 1),
            0,
            &(),
        ),
        Err(GateLawCheckError::ProgressIncomparable),
    );
}

#[test]
fn gate_law_checker_reports_each_observable_law() {
    let cases = [
        (
            Fault::RegressLower,
            GateLawCheckError::AdvanceNotMonotone {
                at: GateLawPoint::Lower,
            },
        ),
        (
            Fault::RegressUpper,
            GateLawCheckError::AdvanceNotMonotone {
                at: GateLawPoint::Upper,
            },
        ),
        (
            Fault::OverlapLower,
            GateLawCheckError::DeliverableAndStale {
                at: GateLawPoint::Lower,
            },
        ),
        (
            Fault::OverlapUpper,
            GateLawCheckError::DeliverableAndStale {
                at: GateLawPoint::Upper,
            },
        ),
        (Fault::StaleReopens, GateLawCheckError::StaleNotTerminal),
        (
            Fault::StableReopens,
            GateLawCheckError::StableNotUpwardClosed,
        ),
    ];

    for (fault, expected) in cases {
        assert_eq!(
            check_gate_laws::<FaultyGate>(&1, &2, 0, &fault),
            Err(expected),
        );
    }
}