boundgraph_grant/

order.rs

//! The partial order `⊑` — "permits no more than".
//!
//! This is the relation Law I is stated in, and the whole attenuation check
//! (US-0403) reduces to it: a flow is legal when every child's grant is `⊑` its
//! parent's. Getting it wrong makes the security guarantee wrong, so the order
//! is verified as a partial order — reflexive, antisymmetric, transitive — by
//! property tests rather than assumed.
//!
//! Every comparison is three-valued. An `Unknown` is a refusal: the compiler
//! rejects rather than assume (US-0206).

use boundgraph_core::{GrantAtom, GrantSet};

use crate::pattern::{Pattern, Tri, covers};

/// Whether `inner` permits no more than `outer` — that is, `inner ⊑ outer`.
///
/// Atoms in different domains or with different actions are **incomparable**,
/// which is a definite [`Tri::No`], not an `Unknown`: they are unrelated, and
/// that is a decided fact rather than a gap in the solver.
pub fn atom_leq(inner: &GrantAtom, outer: &GrantAtom) -> Tri {
    if inner.domain != outer.domain || inner.action != outer.action {
        return Tri::No;
    }
    covers(&outer.resource, &inner.resource)
}

/// Whether two atoms denote exactly the same permission.
///
/// Distinct spellings of one pattern (`/src` and `/src/`) are equal here, which
/// is what makes the order antisymmetric over denotations rather than strings.
pub fn atom_eq(a: &GrantAtom, b: &GrantAtom) -> bool {
    a.domain == b.domain
        && a.action == b.action
        && Pattern::parse(&a.resource) == Pattern::parse(&b.resource)
}

/// Whether `inner ⊑ outer` for grant sets.
///
/// Every atom of `inner` must be permitted by *some* atom of `outer`. A single
/// broad atom can therefore cover many narrow ones, which is what makes
/// attenuation checks cheap in the common case.
///
/// The empty set is below everything — a step that declares nothing is always
/// within its parent's authority.
pub fn set_leq(inner: &GrantSet, outer: &GrantSet) -> Tri {
    Tri::all(inner.iter().map(|i| {
        // Does anything in `outer` permit this atom?
        Tri::any(outer.iter().map(|o| atom_leq(i, o)))
    }))
}

/// Whether two grant sets permit exactly the same thing.
pub fn set_eq(a: &GrantSet, b: &GrantSet) -> Tri {
    set_leq(a, b).and(set_leq(b, a))
}

/// Whether `inner ⊑ outer` **and** the two are not equal — a strict narrowing.
pub fn set_lt(inner: &GrantSet, outer: &GrantSet) -> Tri {
    match set_leq(inner, outer) {
        Tri::Yes => match set_leq(outer, inner) {
            Tri::Yes => Tri::No, // equal, so not strictly below
            Tri::No => Tri::Yes,
            Tri::Unknown => Tri::Unknown,
        },
        other => other,
    }
}

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

    fn atom(s: &str) -> GrantAtom {
        s.parse().expect("test atom should parse")
    }

    fn set(atoms: &[&str]) -> GrantSet {
        GrantSet::parse(atoms.iter().copied()).expect("test set should parse")
    }

    // ── atoms ───────────────────────────────────────────────────────────────

    #[test]
    fn an_atom_permits_no_more_than_itself() {
        for s in ["fs:read:/src/**", "time:now", "fs:read:{path}"] {
            assert_eq!(atom_leq(&atom(s), &atom(s)), Tri::Yes);
        }
    }

    #[test]
    fn a_narrower_resource_is_below_a_broader_one() {
        assert_eq!(
            atom_leq(&atom("fs:read:/src/lib/a.rs"), &atom("fs:read:/src/**")),
            Tri::Yes
        );
        assert_eq!(
            atom_leq(&atom("fs:read:/src/**"), &atom("fs:read:/src/lib/a.rs")),
            Tri::No
        );
    }

    #[test]
    fn different_domains_or_actions_are_incomparable_not_undecidable() {
        // This distinction matters: incomparable is a decided fact, so the
        // compiler rejects cleanly instead of reporting a solver gap.
        assert_eq!(
            atom_leq(&atom("fs:read:/src/**"), &atom("net:read:/src/**")),
            Tri::No
        );
        assert_eq!(
            atom_leq(&atom("fs:write:/src/**"), &atom("fs:read:/src/**")),
            Tri::No
        );
        assert!(
            !atom_leq(&atom("fs:write:/src/a"), &atom("fs:read:/src/**")).is_unknown(),
            "a domain or action mismatch is decidable"
        );
    }

    #[test]
    fn read_does_not_imply_write_or_the_reverse() {
        assert_eq!(
            atom_leq(&atom("fs:write:/src/a"), &atom("fs:read:/src/**")),
            Tri::No,
            "holding read must never confer write"
        );
    }

    #[test]
    fn undecidable_resources_report_unknown() {
        assert_eq!(
            atom_leq(&atom("fs:read:/src/main.rs"), &atom("fs:read:/src/*.rs")),
            Tri::Unknown
        );
    }

    #[test]
    fn atom_equality_is_over_denotations_not_spellings() {
        assert!(atom_eq(&atom("fs:read:/src/"), &atom("fs:read:/src")));
        assert!(!atom_eq(&atom("fs:read:/src"), &atom("fs:read:/src/**")));
    }

    // ── sets ────────────────────────────────────────────────────────────────

    #[test]
    fn the_empty_set_is_below_everything() {
        assert_eq!(
            set_leq(&GrantSet::EMPTY, &set(&["fs:read:/src/**"])),
            Tri::Yes
        );
        assert_eq!(set_leq(&GrantSet::EMPTY, &GrantSet::EMPTY), Tri::Yes);
    }

    #[test]
    fn nothing_nonempty_is_below_the_empty_set() {
        assert_eq!(
            set_leq(&set(&["fs:read:/src/**"]), &GrantSet::EMPTY),
            Tri::No
        );
    }

    #[test]
    fn one_broad_atom_can_cover_several_narrow_ones() {
        let child = set(&["fs:read:/src/a.rs", "fs:read:/src/lib/b.rs"]);
        let parent = set(&["fs:read:/src/**"]);
        assert_eq!(set_leq(&child, &parent), Tri::Yes);
        assert_eq!(set_leq(&parent, &child), Tri::No);
    }

    #[test]
    fn a_single_escaping_atom_sinks_the_whole_set() {
        let child = set(&["fs:read:/src/a.rs", "fs:read:/etc/passwd"]);
        let parent = set(&["fs:read:/src/**"]);
        assert_eq!(set_leq(&child, &parent), Tri::No);
    }

    #[test]
    fn an_undecidable_atom_makes_the_set_comparison_unknown() {
        let child = set(&["fs:read:/src/a.rs", "fs:read:{path}"]);
        let parent = set(&["fs:read:/src/**"]);
        assert_eq!(set_leq(&child, &parent), Tri::Unknown);
    }

    #[test]
    fn a_definite_violation_beats_an_undecidable_sibling() {
        // One atom is undecidable, another definitely escapes. The definite
        // violation must win, so the compiler reports the real problem.
        let child = set(&["fs:read:{path}", "fs:read:/etc/passwd"]);
        let parent = set(&["fs:read:/src/**"]);
        assert_eq!(set_leq(&child, &parent), Tri::No);
    }

    #[test]
    fn set_equality_and_strict_ordering() {
        let a = set(&["fs:read:/src/**"]);
        let b = set(&["fs:read:/src/"]);
        let narrow = set(&["fs:read:/src/a.rs"]);

        assert_eq!(set_eq(&a, &a), Tri::Yes);
        assert_eq!(
            set_lt(&a, &a),
            Tri::No,
            "a set is not strictly below itself"
        );
        assert_eq!(set_lt(&narrow, &a), Tri::Yes);
        assert_eq!(set_lt(&a, &narrow), Tri::No);
        assert_eq!(set_eq(&b, &b), Tri::Yes);
    }

    // ── the partial-order laws, on worked examples ──────────────────────────
    // Exhaustive generative coverage is US-0207; these pin the shape.

    #[test]
    fn the_order_is_reflexive() {
        for s in [
            set(&["fs:read:/src/**"]),
            set(&["fs:read:/a", "net:egress:h:1"]),
            GrantSet::EMPTY,
        ] {
            assert_eq!(set_leq(&s, &s), Tri::Yes);
        }
    }

    #[test]
    fn the_order_is_transitive() {
        let a = set(&["fs:read:/src/lib/a.rs"]);
        let b = set(&["fs:read:/src/lib/**"]);
        let c = set(&["fs:read:/src/**"]);
        assert_eq!(set_leq(&a, &b), Tri::Yes);
        assert_eq!(set_leq(&b, &c), Tri::Yes);
        assert_eq!(set_leq(&a, &c), Tri::Yes, "⊑ must compose");
    }

    #[test]
    fn the_order_is_antisymmetric_over_denotations() {
        let a = set(&["fs:read:/src"]);
        let b = set(&["fs:read:/src/"]);
        assert_eq!(set_leq(&a, &b), Tri::Yes);
        assert_eq!(set_leq(&b, &a), Tri::Yes);
        assert_eq!(set_eq(&a, &b), Tri::Yes, "mutual ⊑ means equal denotation");
    }
}