//! Property test for `policy`: random grant sets, states and requests, each decided twice, once
//! by `policy::decide` and once by an oracle. Every case must agree. Do not edit.
//!
//! The generator and the oracle are in `support/oracle.rs`. If this test fails, the oracle is
//! the specification and `policy` is wrong.
//!
//! The generator is a seeded xorshift, so a failure can be replayed: the message names the seed
//! and the case. `BOXMAKER_POLICY_SEED=<n>` runs one more seed, and `BOXMAKER_POLICY_CASES=<n>`
//! changes how many cases each seed runs (default 3000).

#[path = "support/oracle.rs"]
mod oracle;

use brokerd::grants::{GrantSet, LoadedGrant};
use brokerd::policy::{Outcome, SessionState, decide, redecide};
use oracle::{CLASSES, Expected, NOW_MS, Rng, oracle, some_grant, some_grants, some_request};
use proto::{DataClass, DenyReason, Mode, Timestamp};

const SEEDS: [u64; 5] = [1, 2, 3, 0xB0C5, 20_260_918];

// ---------------------------------------------------------------------------------------------
// The comparison.

fn observed(outcome: &Outcome) -> Expected {
    match outcome {
        Outcome::Allowed(d) => Expected::Allowed {
            grant: d.grant().to_string(),
            path: d.matched_path().map(str::to_string),
            class: d.label().class,
            untrusted: d.label().untrusted,
        },
        Outcome::Ask(a) => Expected::Ask {
            grant: a.grant().to_string(),
            path: a.matched_path().map(str::to_string),
            class: a.label().class,
            untrusted: a.label().untrusted,
        },
        Outcome::Denied(denial) => Expected::Denied {
            reason: denial.reason,
            grant: denial.grant.clone(),
        },
    }
}

/// Allowed is 0, ask is 1, denied is 2.
fn restrictiveness(expected: &Expected) -> u8 {
    match expected {
        Expected::Allowed { .. } => 0,
        Expected::Ask { .. } => 1,
        Expected::Denied { .. } => 2,
    }
}

fn cases() -> usize {
    match std::env::var("BOXMAKER_POLICY_CASES") {
        Ok(text) => text
            .parse()
            .expect("BOXMAKER_POLICY_CASES must be a number"),
        Err(_) => 3000,
    }
}

fn seeds() -> Vec<u64> {
    let mut seeds = SEEDS.to_vec();
    if let Ok(text) = std::env::var("BOXMAKER_POLICY_SEED") {
        seeds.push(text.parse().expect("BOXMAKER_POLICY_SEED must be a number"));
    }
    seeds
}

fn now() -> Timestamp {
    Timestamp::from_unix_millis(NOW_MS).unwrap()
}

fn state(rng: &mut Rng) -> SessionState {
    SessionState {
        taint: rng.pick(&CLASSES),
        untrusted: rng.chance(50),
    }
}

fn valid(grants: &[LoadedGrant]) -> GrantSet {
    GrantSet::from_grants(grants.to_vec()).expect("the generator only makes valid grants")
}

#[test]
fn decide_agrees_with_the_oracle() {
    let mut kinds = [0usize; 3];
    for seed in seeds() {
        let mut rng = Rng::new(seed);
        for case in 0..cases() {
            let grants = some_grants(&mut rng);
            let request = some_request(&mut rng);
            let state = state(&mut rng);
            let want = oracle(&request, &grants, state);
            let got = observed(&decide(request.clone(), &valid(&grants), state, now()));
            assert_eq!(
                got, want,
                "seed {seed} case {case}\nrequest: {request:?}\nstate: {state:?}\ngrants: {grants:#?}"
            );
            kinds[restrictiveness(&want) as usize] += 1;
        }
    }
    // The generator must reach every kind of outcome, or the test proves little.
    for (kind, count) in ["allowed", "ask", "denied"].iter().zip(kinds) {
        assert!(count > 200, "only {count} cases were {kind}");
    }
}

#[test]
fn redecide_agrees_with_the_oracle_under_new_grants_and_a_new_state() {
    let mut approvals = 0;
    for seed in seeds() {
        let mut rng = Rng::new(seed ^ 0xA5A5);
        for case in 0..cases() {
            let grants = some_grants(&mut rng);
            let request = some_request(&mut rng);
            let first = state(&mut rng);
            let Outcome::Ask(ask) = decide(request.clone(), &valid(&grants), first, now()) else {
                continue;
            };
            approvals += 1;
            // Half the time nothing has changed; otherwise the grants or the state have.
            let (later_grants, later) = if rng.chance(50) {
                (grants.clone(), first)
            } else {
                (some_grants(&mut rng), state(&mut rng))
            };
            let want = oracle(&request, &later_grants, later);
            let got = redecide(ask, &valid(&later_grants), later, now());
            let context = format!(
                "seed {seed} case {case}\nrequest: {request:?}\nlater: {later:?}\ngrants: {later_grants:#?}"
            );
            match (want, got) {
                (
                    Expected::Allowed {
                        grant,
                        path,
                        class,
                        untrusted,
                    },
                    Ok(d),
                )
                | (
                    Expected::Ask {
                        grant,
                        path,
                        class,
                        untrusted,
                    },
                    Ok(d),
                ) => {
                    assert_eq!(d.grant(), grant, "{context}");
                    assert_eq!(d.matched_path().map(str::to_string), path, "{context}");
                    assert_eq!(
                        (d.label().class, d.label().untrusted),
                        (class, untrusted),
                        "{context}"
                    );
                    assert_eq!(d.request(), &request, "{context}");
                }
                (Expected::Denied { reason, grant }, Err(denial)) => {
                    assert_eq!((denial.reason, denial.grant), (reason, grant), "{context}");
                }
                (want, got) => panic!("wanted {want:?}, got {got:?}\n{context}"),
            }
        }
    }
    assert!(approvals > 200, "only {approvals} cases asked");
}

/// Adding a `deny` grant to a set never makes any outcome less restrictive.
#[test]
fn adding_a_deny_grant_never_loosens_an_outcome() {
    for seed in seeds() {
        let mut rng = Rng::new(seed ^ 0x5A5A);
        for case in 0..cases() {
            let grants = some_grants(&mut rng);
            let request = some_request(&mut rng);
            let state = state(&mut rng);
            let mut extra = some_grant(&mut rng, 90);
            extra.grant.mode = Mode::Deny;
            extra.grant.max_taint = DataClass::Secret;
            let mut with_deny = grants.clone();
            with_deny.push(extra);

            let before = observed(&decide(request.clone(), &valid(&grants), state, now()));
            let after = observed(&decide(request.clone(), &valid(&with_deny), state, now()));
            assert!(
                restrictiveness(&after) >= restrictiveness(&before),
                "seed {seed} case {case}: {before:?} became {after:?}\nrequest: {request:?}\ngrants: {with_deny:#?}"
            );
        }
    }
}

/// A call that is `denied_by_grant` at one taint is `denied_by_grant` at every higher taint:
/// reading a secret can never switch off a prohibition.
#[test]
fn a_prohibition_holds_at_every_higher_taint() {
    let mut prohibitions = 0;
    for seed in seeds() {
        let mut rng = Rng::new(seed ^ 0x0F0F);
        for case in 0..cases() {
            let grants = some_grants(&mut rng);
            let request = some_request(&mut rng);
            let mut denied_below = false;
            for taint in CLASSES {
                let state = SessionState {
                    taint,
                    untrusted: false,
                };
                let outcome = observed(&decide(request.clone(), &valid(&grants), state, now()));
                let by_grant = matches!(
                    outcome,
                    Expected::Denied {
                        reason: DenyReason::DeniedByGrant,
                        ..
                    }
                );
                assert!(
                    by_grant || !denied_below,
                    "seed {seed} case {case}: a deny stopped applying at {taint:?}\nrequest: {request:?}\ngrants: {grants:#?}"
                );
                denied_below = by_grant;
            }
            prohibitions += usize::from(denied_below);
        }
    }
    assert!(
        prohibitions > 200,
        "only {prohibitions} cases were prohibited"
    );
}