asupersync 0.3.1

//! CALM analysis: monotonicity classification for saga operations (bd-2wrsc.1).
//!
//! The CALM theorem (Consistency As Logical Monotonicity, Hellerstein & Alvaro 2020)
//! proves that monotone programs can be implemented without coordination. This module
//! classifies each saga operation as monotone or non-monotone and provides runtime
//! markers for coordination-free optimization.
//!
//! # Classification Criteria
//!
//! - **Monotone**: Only adds information (inserts, appends, set unions, lattice joins,
//!   counter increments). Can execute coordination-free.
//! - **Non-monotone**: Depends on negation or absence (deletes, reads-before-writes,
//!   threshold checks, aggregations over incomplete sets). Requires synchronization.
//!
//! # Operations Classified
//!
//! | Operation | Classification | Justification |
//! |-----------|---------------|---------------|
//! | Reserve | Monotone | Pure insertion into obligation set |
//! | Commit | Non-monotone | Guard on current state = Reserved |
//! | Abort | Non-monotone | Guard on current state = Reserved |
//! | Send | Monotone | Channel append (grow-only) |
//! | Recv | Non-monotone | Destructive read (dequeue) |
//! | Acquire | Monotone | Lease creation (insertion) |
//! | Renew | Monotone | Deadline extension (max/join) |
//! | Release | Non-monotone | Guard on current state = active |
//! | RegionClose | Non-monotone | Quiescence barrier (aggregation) |
//! | Delegate | Monotone | Channel transfer (information flow) |
//! | CrdtMerge | Monotone | Join-semilattice merge |
//! | CancelRequest | Monotone | Monotone latch (false -> true) |
//! | CancelDrain | Non-monotone | Quiescence barrier |
//! | MarkLeaked | Non-monotone | Depends on absence of resolution |
//! | BudgetCheck | Non-monotone | Threshold on depleting counter |

use std::fmt;

/// Monotonicity classification per CALM theorem.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum Monotonicity {
    /// Operation only adds information; can execute coordination-free.
    Monotone,
    /// Operation depends on negation/absence; requires synchronization.
    NonMonotone,
}

impl fmt::Display for Monotonicity {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Monotone => write!(f, "monotone"),
            Self::NonMonotone => write!(f, "non_monotone"),
        }
    }
}

/// A saga operation with its CALM classification.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CalmClassification {
    /// Operation name.
    pub operation: &'static str,
    /// Protocol this operation belongs to.
    pub protocol: &'static str,
    /// CALM monotonicity classification.
    pub monotonicity: Monotonicity,
    /// Human-readable justification for the classification.
    pub justification: &'static str,
}

/// All CALM classifications for Asupersync saga operations.
///
/// Returns a static slice of classifications for every saga operation.
#[must_use]
pub fn classifications() -> &'static [CalmClassification] {
    &CLASSIFICATIONS
}

/// Returns the monotone ratio (monotone / total).
#[must_use]
pub fn monotone_ratio() -> f64 {
    let total = CLASSIFICATIONS.len();
    let mono = CLASSIFICATIONS
        .iter()
        .filter(|c| c.monotonicity == Monotonicity::Monotone)
        .count();
    #[allow(clippy::cast_precision_loss)]
    {
        mono as f64 / total as f64
    }
}

/// Returns only the coordination points (non-monotone operations).
#[must_use]
pub fn coordination_points() -> Vec<&'static CalmClassification> {
    CLASSIFICATIONS
        .iter()
        .filter(|c| c.monotonicity == Monotonicity::NonMonotone)
        .collect()
}

/// Returns only the coordination-free operations (monotone).
#[must_use]
pub fn coordination_free() -> Vec<&'static CalmClassification> {
    CLASSIFICATIONS
        .iter()
        .filter(|c| c.monotonicity == Monotonicity::Monotone)
        .collect()
}

static CLASSIFICATIONS: [CalmClassification; 16] = [
    CalmClassification {
        operation: "Reserve",
        protocol: "All",
        monotonicity: Monotonicity::Monotone,
        justification: "Pure insertion into obligation set; monotone in marking vector",
    },
    CalmClassification {
        operation: "Commit",
        protocol: "TwoPhase/SendPermit",
        monotonicity: Monotonicity::NonMonotone,
        justification: "Requires guard on current state=Reserved (negation of resolved)",
    },
    CalmClassification {
        operation: "Abort",
        protocol: "TwoPhase/SendPermit",
        monotonicity: Monotonicity::NonMonotone,
        justification: "Requires guard on current state=Reserved; conditional assignment",
    },
    CalmClassification {
        operation: "Send",
        protocol: "SendPermit",
        monotonicity: Monotonicity::Monotone,
        justification: "Channel append is set-union-like (grow-only)",
    },
    CalmClassification {
        operation: "Recv",
        protocol: "SendPermit",
        monotonicity: Monotonicity::NonMonotone,
        justification: "Destructive read (dequeue) depends on presence/absence",
    },
    CalmClassification {
        operation: "Acquire",
        protocol: "Lease",
        monotonicity: Monotonicity::Monotone,
        justification: "Lease creation is insertion; timer start has no absence dependency",
    },
    CalmClassification {
        operation: "Renew",
        protocol: "Lease",
        monotonicity: Monotonicity::Monotone,
        justification: "Deadline extension is max (lattice join on timestamps)",
    },
    CalmClassification {
        operation: "Release",
        protocol: "Lease",
        monotonicity: Monotonicity::NonMonotone,
        justification: "Requires current state=active; transition depends on negation",
    },
    CalmClassification {
        operation: "RegionClose",
        protocol: "StructuredConcurrency",
        monotonicity: Monotonicity::NonMonotone,
        justification: "Quiescence barrier: aggregation over incomplete obligation set",
    },
    CalmClassification {
        operation: "Delegate",
        protocol: "Composition",
        monotonicity: Monotonicity::Monotone,
        justification: "Channel transfer is monotone information flow",
    },
    CalmClassification {
        operation: "CrdtMerge",
        protocol: "Distributed",
        monotonicity: Monotonicity::Monotone,
        justification: "Join-semilattice merge with GCounter max (by construction)",
    },
    CalmClassification {
        operation: "CancelRequest",
        protocol: "Runtime",
        monotonicity: Monotonicity::Monotone,
        justification: "Monotone latch (false->true, never reverts); downward propagation",
    },
    CalmClassification {
        operation: "CancelDrain",
        protocol: "Runtime",
        monotonicity: Monotonicity::NonMonotone,
        justification: "Waiting for ALL obligations terminal is a barrier",
    },
    CalmClassification {
        operation: "MarkLeaked",
        protocol: "Obligation",
        monotonicity: Monotonicity::NonMonotone,
        justification: "Depends on timeout/absence of resolution",
    },
    CalmClassification {
        operation: "BudgetCheck",
        protocol: "Cx",
        monotonicity: Monotonicity::NonMonotone,
        justification: "Threshold check on depleting counter",
    },
    CalmClassification {
        operation: "LeakDetection",
        protocol: "Analysis",
        monotonicity: Monotonicity::NonMonotone,
        justification: "Depends on negation: NOT resolved before region close",
    },
];

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn classification_count_is_16() {
        assert_eq!(classifications().len(), 16);
    }

    #[test]
    fn monotone_ratio_is_correct() {
        let ratio = monotone_ratio();
        // 7 monotone out of 16 = 0.4375
        assert!((ratio - 0.4375).abs() < 0.001, "ratio = {ratio}");
    }

    #[test]
    fn coordination_points_are_non_monotone() {
        let points = coordination_points();
        assert_eq!(points.len(), 9);
        for p in &points {
            assert_eq!(p.monotonicity, Monotonicity::NonMonotone);
        }
    }

    #[test]
    fn coordination_free_are_monotone() {
        let free = coordination_free();
        assert_eq!(free.len(), 7);
        for f in &free {
            assert_eq!(f.monotonicity, Monotonicity::Monotone);
        }
    }

    #[test]
    fn all_operations_have_justification() {
        for c in classifications() {
            assert!(
                !c.justification.is_empty(),
                "{} has no justification",
                c.operation
            );
        }
    }

    #[test]
    fn monotonicity_display() {
        assert_eq!(Monotonicity::Monotone.to_string(), "monotone");
        assert_eq!(Monotonicity::NonMonotone.to_string(), "non_monotone");
    }

    #[test]
    fn reserve_is_monotone() {
        let reserve = classifications()
            .iter()
            .find(|c| c.operation == "Reserve")
            .unwrap();
        assert_eq!(reserve.monotonicity, Monotonicity::Monotone);
    }

    #[test]
    fn region_close_is_non_monotone() {
        let rc = classifications()
            .iter()
            .find(|c| c.operation == "RegionClose")
            .unwrap();
        assert_eq!(rc.monotonicity, Monotonicity::NonMonotone);
    }

    #[test]
    fn crdt_merge_is_monotone() {
        let merge = classifications()
            .iter()
            .find(|c| c.operation == "CrdtMerge")
            .unwrap();
        assert_eq!(merge.monotonicity, Monotonicity::Monotone);
    }

    #[test]
    fn all_seven_monotone_operations() {
        let expected = [
            "Reserve",
            "Send",
            "Acquire",
            "Renew",
            "Delegate",
            "CrdtMerge",
            "CancelRequest",
        ];
        let mono: Vec<&str> = coordination_free().iter().map(|c| c.operation).collect();
        // Verify exact membership rather than just the count.
        for exp in &expected {
            assert!(
                mono.contains(exp),
                "missing expected monotone operation {exp}"
            );
        }
        assert_eq!(mono.len(), 7);
    }

    // ── derive-trait coverage (wave 73) ──────────────────────────────────

    #[test]
    fn monotonicity_debug_clone_copy_eq_hash() {
        use std::collections::HashSet;

        let m = Monotonicity::Monotone;
        let m2 = m; // Copy
        let m3 = m;
        assert_eq!(m, m2);
        assert_eq!(m2, m3);

        let nm = Monotonicity::NonMonotone;
        assert_ne!(m, nm);

        let mut set = HashSet::new();
        set.insert(m);
        set.insert(m2);
        assert_eq!(set.len(), 1);
        set.insert(nm);
        assert_eq!(set.len(), 2);

        let dbg = format!("{m:?}");
        assert!(dbg.contains("Monotone"));
    }

    #[test]
    fn calm_classification_debug_clone_eq() {
        let c1 = CalmClassification {
            operation: "TestOp",
            protocol: "TestProto",
            monotonicity: Monotonicity::Monotone,
            justification: "test justification",
        };
        let c2 = c1.clone();
        assert_eq!(c1, c2);

        let c3 = CalmClassification {
            operation: "OtherOp",
            protocol: "TestProto",
            monotonicity: Monotonicity::NonMonotone,
            justification: "other justification",
        };
        assert_ne!(c1, c3);

        let dbg = format!("{c1:?}");
        assert!(dbg.contains("CalmClassification"));
        assert!(dbg.contains("TestOp"));
    }

    #[test]
    fn metamorphic_partitioned_views_preserve_classification_order() {
        let original = classifications();
        let monotone = coordination_free();
        let non_monotone = coordination_points();

        let reconstructed: Vec<(&'static str, Monotonicity)> = original
            .iter()
            .map(|classification| {
                let projection = match classification.monotonicity {
                    Monotonicity::Monotone => monotone
                        .iter()
                        .find(|candidate| candidate.operation == classification.operation)
                        .expect("monotone projection should contain every monotone operation"),
                    Monotonicity::NonMonotone => non_monotone
                        .iter()
                        .find(|candidate| candidate.operation == classification.operation)
                        .expect(
                            "non-monotone projection should contain every non-monotone operation",
                        ),
                };
                (projection.operation, projection.monotonicity)
            })
            .collect();

        let original_projection: Vec<(&'static str, Monotonicity)> = original
            .iter()
            .map(|classification| (classification.operation, classification.monotonicity))
            .collect();

        assert_eq!(
            reconstructed, original_projection,
            "projecting through monotone/non-monotone filtered views must preserve original order"
        );
    }
}