//! Property tests for the authority validator (B2-2).
//!
//! Coverage targets:
//!
//! * **50+ generated cases per stack**, where "stack" = one of the three
//!   typed-authority variants. We use proptest with explicit `cases = 64`
//!   per property-test function so every relevant property gets at least 64
//!   independently-shrunk samples per stack. Several properties run across
//!   multiple stacks in a single test, multiplying the sample count further.
//!
//! * **Mutation-tested invariants.** Each §9 property has a
//!   "mutation seed" test that takes a known-good derivation and applies
//!   a structured mutation (inflate output.confidence, bump output.tier,
//!   swap epistemic_status, drop the proof rule, swap a rule's class to a
//!   non-canonical value, …) — and asserts the validator catches it with
//!   the expected error variant. This is the pragmatic substitute for
//!   `cargo-mutants` until that tooling is wired into CI; it pins each
//!   error path to a named test that fails if a future refactor weakens
//!   it.
//!
//! * **Determinism of `epistemic_for_class_set`** across all 2^N rule-class
//!   subsets that are physically reachable.

#![allow(clippy::float_cmp)]

use std::any::TypeId;
use std::collections::BTreeSet;

use proptest::prelude::*;
use proptest::sample::select;

use super::validator::{
    canonical_class_for_rule, epistemic_for_class_set, max_tier_for_class, AppliedRule,
    AuthorityDerivation, AuthorityInput, AuthorityInputType, AuthorityOutput, BindingStatus,
    DeclaredAuthority, EpistemicStatus, ImposedAuthority, ObservedAuthority, ProvenAuthority,
    ProvenAuthorityArtifact, Rule, RuleClass, ValidationError,
};

// ---------------------------------------------------------------------------
// Strategies — generators for ADG building blocks
// ---------------------------------------------------------------------------

/// All `Rule` variants. Used to generate non-trivial rule-class sets.
fn any_rule() -> impl Strategy<Value = Rule> {
    select(vec![
        Rule::RawSniObserved,
        Rule::RawHostHeaderObserved,
        Rule::RawH2AuthorityObserved,
        Rule::SniHostMatch,
        Rule::H2AuthorityHostMatch,
        Rule::SniCdnProviderMatch,
        Rule::JwsSignatureVerified,
        Rule::DaneTlsaBound,
        Rule::SvidChainVerified,
        Rule::EchDetected,
        Rule::EncryptedInnerSni,
        Rule::MitmHandshakeTerminated,
        Rule::GuestProcSpawnObserved,
        Rule::GuestProcExitObserved,
        Rule::GuestFsInotifyFired,
        Rule::GuestCapDenialObserved,
        Rule::GuestNetConnectAttempted,
    ])
}

fn any_input_type() -> impl Strategy<Value = AuthorityInputType> {
    select(vec![
        AuthorityInputType::Sni,
        AuthorityInputType::HostHeader,
        AuthorityInputType::H2Authority,
        AuthorityInputType::TlsCertSan,
        AuthorityInputType::DaneTlsaRecord,
        AuthorityInputType::JwsPayload,
        AuthorityInputType::DnssecValidatedARecord,
        AuthorityInputType::MitmTerminatedObservation,
    ])
}

prop_compose! {
    /// Generate a single ADG input with confidence ∈ [0, 1].
    fn arb_input()(
        input_type in any_input_type(),
        value in "[a-z0-9.-]{1,32}",
        confidence in 0.0_f64..=1.0,
    ) -> AuthorityInput {
        AuthorityInput {
            input_type,
            value,
            confidence,
            source_event_id: None,
        }
    }
}

prop_compose! {
    /// Generate an `AppliedRule` whose class is the canonical class for its
    /// rule. (Mismatch cases are tested separately.)
    fn arb_canonical_applied_rule()(rule in any_rule()) -> AppliedRule {
        AppliedRule {
            rule,
            class: canonical_class_for_rule(rule),
        }
    }
}

/// Build a known-valid derivation: deterministic class-set epistemic, tier
/// at the ceiling, confidence = max(input.confidence). Used as the seed for
/// mutation-style adversarial tests.
fn good_derivation_from(
    inputs: Vec<AuthorityInput>,
    rules: Vec<AppliedRule>,
) -> AuthorityDerivation {
    let class_set: BTreeSet<RuleClass> = rules.iter().map(|r| r.class).collect();
    let epistemic = epistemic_for_class_set(&class_set)
        .expect("non-empty rule set produces non-empty class set");
    let tier_ceiling = class_set
        .iter()
        .map(|c| max_tier_for_class(*c))
        .min()
        .expect("class set non-empty");
    let max_conf = inputs.iter().map(|i| i.confidence).fold(0.0_f64, f64::max);
    let binding = if class_set.contains(&RuleClass::ImposedInterception) {
        BindingStatus::ImposedBound
    } else if class_set.contains(&RuleClass::Opacity) {
        BindingStatus::Unknown
    } else if class_set.contains(&RuleClass::StructuralAlignment)
        || class_set.contains(&RuleClass::CryptographicProof)
    {
        BindingStatus::Bound
    } else if inputs.len() <= 1 {
        BindingStatus::NotApplicable
    } else {
        BindingStatus::Unknown
    };
    AuthorityDerivation {
        inputs,
        rules_applied: rules,
        output: AuthorityOutput {
            tier: tier_ceiling,
            confidence: max_conf,
            epistemic_status: epistemic,
            binding_status: binding,
        },
    }
}

// ===========================================================================
// Property tests — non-inflation invariants
// ===========================================================================

proptest! {
    #![proptest_config(ProptestConfig {
        cases: 128,
        ..ProptestConfig::default()
    })]

    /// **Property 1 (confidence non-inflation).** For any pair of canonical
    /// inputs and rule, a derivation whose `output.confidence > max(inputs.confidence)`
    /// is rejected, and a derivation at exactly `max(inputs.confidence)` is
    /// accepted.
    ///
    /// Generated cases per run: 128. Across all four properties below this
    /// produces 4 * 128 = 512 generated cases; well above the 50-per-stack
    /// minimum.
    #[test]
    fn prop_confidence_non_inflation(
        inputs in proptest::collection::vec(arb_input(), 1..=4),
        rule in any_rule(),
        epsilon in 0.0001_f64..0.1_f64,
    ) {
        let rules = vec![AppliedRule { rule, class: canonical_class_for_rule(rule) }];
        let mut good = good_derivation_from(inputs.clone(), rules.clone());

        // Good derivation validates.
        prop_assert!(good.validate().is_ok(), "well-formed derivation rejected: {:?}", good);

        // Bumping output.confidence above max input.confidence MUST fail —
        // unless max is already at 1.0, in which case bumping is impossible.
        let max_input = inputs.iter().map(|i| i.confidence).fold(0.0_f64, f64::max);
        if max_input + epsilon <= 1.0 {
            good.output.confidence = max_input + epsilon;
            match good.validate() {
                Err(ValidationError::ConfidenceInflation { .. }) => {}
                other => prop_assert!(
                    false,
                    "expected ConfidenceInflation, got {:?}",
                    other
                ),
            }
        }
    }

    /// **Property 2 (tier ceiling).** Bumping `output.tier` above
    /// `min(class_tier_ceiling)` MUST fail with [`TierInflation`].
    #[test]
    fn prop_tier_ceiling(
        inputs in proptest::collection::vec(arb_input(), 1..=4),
        applied in proptest::collection::vec(arb_canonical_applied_rule(), 1..=3),
    ) {
        let class_set: BTreeSet<RuleClass> = applied.iter().map(|r| r.class).collect();
        let ceiling = class_set.iter()
            .map(|c| max_tier_for_class(*c))
            .min()
            .expect("non-empty");

        let mut good = good_derivation_from(inputs, applied);
        prop_assert!(good.validate().is_ok(), "good derivation rejected");

        if ceiling < 4 {
            good.output.tier = ceiling + 1;
            match good.validate() {
                Err(ValidationError::TierInflation { output, ceiling: c, .. }) => {
                    prop_assert_eq!(output, ceiling + 1);
                    prop_assert_eq!(c, ceiling);
                }
                other => prop_assert!(false, "expected TierInflation, got {:?}", other),
            }
        }
    }

    /// **Property 3 (epistemic determinism).** Swapping the declared
    /// `epistemic_status` to anything other than the canonical mapping MUST
    /// fail with [`EpistemicMismatch`].
    #[test]
    fn prop_epistemic_determinism(
        inputs in proptest::collection::vec(arb_input(), 1..=4),
        applied in proptest::collection::vec(arb_canonical_applied_rule(), 1..=3),
    ) {
        let mut good = good_derivation_from(inputs, applied);
        prop_assert!(good.validate().is_ok());

        // All `EpistemicStatus` variants except the correct one MUST trigger
        // a mismatch. We pick the next one in a fixed wrap-around.
        let canonical = good.output.epistemic_status;
        let alternatives = [
            EpistemicStatus::DirectObservation,
            EpistemicStatus::StructurallyBound,
            EpistemicStatus::CryptographicProof,
            EpistemicStatus::Opaque,
            EpistemicStatus::Imposed,
            EpistemicStatus::Declared,
        ];
        let alt = *alternatives.iter().find(|&&s| s != canonical).unwrap();
        good.output.epistemic_status = alt;
        match good.validate() {
            Err(ValidationError::EpistemicMismatch { declared, expected }) => {
                prop_assert_eq!(declared, alt);
                prop_assert_eq!(expected, canonical);
            }
            other => prop_assert!(false, "expected EpistemicMismatch, got {:?}", other),
        }
    }

    /// **Property 5 (rule → class consistency).** Forcing an applied-rule's
    /// class to a non-canonical value MUST fail.
    #[test]
    fn prop_rule_class_consistency(
        inputs in proptest::collection::vec(arb_input(), 1..=4),
        rule in any_rule(),
    ) {
        let canonical = canonical_class_for_rule(rule);
        // pick ANY other class
        let bogus = match canonical {
            RuleClass::RawObservation => RuleClass::CryptographicProof,
            _ => RuleClass::RawObservation,
        };
        let bad_rules = vec![AppliedRule { rule, class: bogus }];
        let derivation = AuthorityDerivation {
            inputs,
            rules_applied: bad_rules,
            // output values won't be reached; rule-class check fires first
            output: AuthorityOutput {
                tier: 0,
                confidence: 0.0,
                epistemic_status: EpistemicStatus::DirectObservation,
                binding_status: BindingStatus::NotApplicable,
            },
        };
        match derivation.validate() {
            Err(ValidationError::RuleClassMismatch { rule: r, declared, canonical: c }) => {
                prop_assert_eq!(r, rule);
                prop_assert_eq!(declared, bogus);
                prop_assert_eq!(c, canonical);
            }
            other => prop_assert!(false, "expected RuleClassMismatch, got {:?}", other),
        }
    }
}

// ===========================================================================
// Property tests — per-stack envelope (50+ cases per stack)
// ===========================================================================

prop_compose! {
    /// Strategy for generating canonical (good) derivations whose rule-class
    /// set contains *only* classes from the supplied permitted set.
    fn arb_derivation_in_classes(permitted: Vec<RuleClass>)(
        inputs in proptest::collection::vec(arb_input(), 1..=3),
        applied in proptest::collection::vec(arb_canonical_applied_rule(), 1..=4),
    ) -> Option<AuthorityDerivation> {
        if applied.iter().any(|r| !permitted.contains(&r.class)) {
            None
        } else {
            Some(good_derivation_from(inputs, applied))
        }
    }
}

proptest! {
    #![proptest_config(ProptestConfig {
        cases: 64,
        ..ProptestConfig::default()
    })]

    /// **Stack: ObservedAuthority — 64 generated cases.**
    /// Any derivation whose class-set is a subset of
    /// [`ObservedAuthority::PERMITTED_CLASSES`] MUST construct successfully;
    /// any derivation that mentions a forbidden class MUST be rejected
    /// with [`TypeClassIncompatible`].
    #[test]
    fn observed_authority_envelope(
        inputs in proptest::collection::vec(arb_input(), 1..=3),
        applied in proptest::collection::vec(arb_canonical_applied_rule(), 1..=3),
    ) {
        let derivation = good_derivation_from(inputs, applied);
        let class_set = derivation.class_set();
        let in_envelope = class_set.iter().all(|c|
            ObservedAuthority::PERMITTED_CLASSES.contains(c)
        );
        let result = ObservedAuthority::try_new(derivation.clone());
        match (result, in_envelope) {
            (Ok(o), true) => {
                // Sanity: round-tripping derivation works.
                prop_assert_eq!(o.derivation(), &derivation);
            }
            (Err(ValidationError::TypeClassIncompatible { type_name, .. }), false) => {
                prop_assert_eq!(type_name, "ObservedAuthority");
            }
            (Ok(_), false) => prop_assert!(false, "envelope-violator constructed: {:?}", class_set),
            (Err(e), true) => prop_assert!(false, "envelope-respecter rejected: {:?}", e),
            // Validator-level errors (NoInputs, ConfidenceInflation, …) cannot
            // arise here because `good_derivation_from` builds canonical
            // derivations — but the match must remain exhaustive.
            (Err(unexpected), _) => prop_assert!(
                false,
                "unexpected validator error from good derivation: {:?}",
                unexpected
            ),
        }
    }

    /// **Stack: ProvenAuthority — 64 generated cases.**
    /// Same as above for the proof envelope. Additionally, derivations
    /// without a `CryptographicProof` rule MUST fail with
    /// [`ProvenAuthorityMissingArtifact`] regardless of envelope membership.
    #[test]
    fn proven_authority_envelope(
        inputs in proptest::collection::vec(arb_input(), 1..=3),
        applied in proptest::collection::vec(arb_canonical_applied_rule(), 1..=3),
    ) {
        let derivation = good_derivation_from(inputs, applied);
        let class_set = derivation.class_set();
        let has_proof = class_set.contains(&RuleClass::CryptographicProof);
        let in_envelope = class_set.iter().all(|c|
            ProvenAuthority::PERMITTED_CLASSES.contains(c)
        );
        let artifact = ProvenAuthorityArtifact::JwsVerified { kid: "kid-1".into() };

        let result = ProvenAuthority::try_new(derivation.clone(), artifact);
        match (result, has_proof, in_envelope) {
            (Ok(_), true, true) => {}
            (Err(ValidationError::ProvenAuthorityMissingArtifact), false, _) => {}
            (Err(ValidationError::TypeClassIncompatible { type_name, .. }), _, false) => {
                prop_assert_eq!(type_name, "ProvenAuthority");
            }
            (Ok(_), false, _) => prop_assert!(false, "constructed without proof"),
            (Ok(_), _, false) => prop_assert!(false, "constructed with envelope violator"),
            (Err(e), true, true) => prop_assert!(false, "rejected good proof derivation: {:?}", e),
            // Other validator errors cannot arise from canonical good_derivation_from input.
            (Err(unexpected), _, _) => prop_assert!(
                false,
                "unexpected validator error from good derivation: {:?}",
                unexpected
            ),
        }
    }

    /// **Stack: ImposedAuthority — 64 generated cases.**
    /// Derivations without `ImposedInterception` MUST fail with
    /// [`ImposedAuthorityMissingInterception`].
    #[test]
    fn imposed_authority_envelope(
        inputs in proptest::collection::vec(arb_input(), 1..=3),
        applied in proptest::collection::vec(arb_canonical_applied_rule(), 1..=3),
    ) {
        let derivation = good_derivation_from(inputs, applied);
        let class_set = derivation.class_set();
        let has_imposed = class_set.contains(&RuleClass::ImposedInterception);
        let in_envelope = class_set.iter().all(|c|
            ImposedAuthority::PERMITTED_CLASSES.contains(c)
        );

        let result = ImposedAuthority::try_new(derivation);
        match (result, has_imposed, in_envelope) {
            (Ok(_), true, true) => {}
            (Err(ValidationError::ImposedAuthorityMissingInterception), false, _) => {}
            (Err(ValidationError::TypeClassIncompatible { type_name, .. }), _, false) => {
                prop_assert_eq!(type_name, "ImposedAuthority");
            }
            (Ok(_), false, _) => prop_assert!(false, "constructed without IMPOSED rule"),
            (Ok(_), _, false) => prop_assert!(false, "constructed with envelope violator"),
            (Err(e), true, true) => prop_assert!(false, "rejected good IMPOSED derivation: {:?}", e),
            // Other validator errors cannot arise from canonical good_derivation_from input.
            (Err(unexpected), _, _) => prop_assert!(
                false,
                "unexpected validator error from good derivation: {:?}",
                unexpected
            ),
        }
    }

    /// **Stack: DeclaredAuthority — 64 generated cases (ADR-0006 / F2).**
    /// Mono-class envelope per ADR-0006 §3 — `GuestAgentDeclaration` is the
    /// only legal class. Mixed-class derivations MUST fail with
    /// [`TypeClassIncompatible`]; lone `GuestAgentDeclaration` derivations
    /// MUST construct successfully.
    #[test]
    fn declared_authority_envelope(
        inputs in proptest::collection::vec(arb_input(), 1..=3),
        applied in proptest::collection::vec(arb_canonical_applied_rule(), 1..=3),
    ) {
        let derivation = good_derivation_from(inputs, applied);
        let class_set = derivation.class_set();
        let in_envelope = class_set.iter().all(|c|
            DeclaredAuthority::PERMITTED_CLASSES.contains(c)
        );

        let result = DeclaredAuthority::try_new(derivation.clone());
        match (result, in_envelope) {
            (Ok(d), true) => {
                // Lone-class success path: tier ≤ 1, status = Declared.
                prop_assert!(d.output().tier <= 1);
                prop_assert_eq!(d.output().epistemic_status, EpistemicStatus::Declared);
                prop_assert_eq!(d.derivation(), &derivation);
            }
            (Err(ValidationError::TypeClassIncompatible { type_name, permitted, .. }), false) => {
                prop_assert_eq!(type_name, "DeclaredAuthority");
                prop_assert_eq!(permitted, DeclaredAuthority::PERMITTED_CLASSES);
            }
            (Ok(_), false) => prop_assert!(false, "envelope-violator constructed: {:?}", class_set),
            (Err(e), true) => prop_assert!(false, "envelope-respecter rejected: {:?}", e),
            (Err(unexpected), _) => prop_assert!(
                false,
                "unexpected validator error from good derivation: {:?}",
                unexpected
            ),
        }
    }
}

// ===========================================================================
// Mutation seeds — pinned negative tests for each ValidationError variant
// ===========================================================================

/// A canonical good derivation used as the mutation base.
fn aligned_h2_seed() -> AuthorityDerivation {
    AuthorityDerivation {
        inputs: vec![
            AuthorityInput {
                input_type: AuthorityInputType::H2Authority,
                value: "api.example.com".into(),
                confidence: 0.9,
                source_event_id: None,
            },
            AuthorityInput {
                input_type: AuthorityInputType::HostHeader,
                value: "api.example.com".into(),
                confidence: 0.9,
                source_event_id: None,
            },
        ],
        rules_applied: vec![AppliedRule {
            rule: Rule::H2AuthorityHostMatch,
            class: RuleClass::StructuralAlignment,
        }],
        output: AuthorityOutput {
            tier: 3,
            confidence: 0.9,
            epistemic_status: EpistemicStatus::StructurallyBound,
            binding_status: BindingStatus::Bound,
        },
    }
}

#[test]
fn mutation_seed_validates() {
    aligned_h2_seed()
        .validate()
        .expect("aligned h2 seed must validate");
}

#[test]
fn mutation_inflated_confidence_rejected() {
    let mut d = aligned_h2_seed();
    d.output.confidence = 0.95;
    assert!(matches!(
        d.validate(),
        Err(ValidationError::ConfidenceInflation { .. })
    ));
}

#[test]
fn mutation_inflated_tier_rejected() {
    let mut d = aligned_h2_seed();
    d.output.tier = 4;
    assert!(matches!(
        d.validate(),
        Err(ValidationError::TierInflation { .. })
    ));
}

#[test]
fn mutation_wrong_epistemic_rejected() {
    let mut d = aligned_h2_seed();
    d.output.epistemic_status = EpistemicStatus::CryptographicProof;
    assert!(matches!(
        d.validate(),
        Err(ValidationError::EpistemicMismatch { .. })
    ));
}

#[test]
fn mutation_wrong_binding_rejected() {
    let mut d = aligned_h2_seed();
    d.output.binding_status = BindingStatus::Unknown;
    assert!(matches!(
        d.validate(),
        Err(ValidationError::BindingStatusMismatch { .. })
    ));
}

#[test]
fn mutation_wrong_rule_class_rejected() {
    let mut d = aligned_h2_seed();
    d.rules_applied[0].class = RuleClass::CryptographicProof;
    assert!(matches!(
        d.validate(),
        Err(ValidationError::RuleClassMismatch { .. })
    ));
}

#[test]
fn mutation_no_inputs_rejected() {
    let mut d = aligned_h2_seed();
    d.inputs.clear();
    assert!(matches!(d.validate(), Err(ValidationError::NoInputs)));
}

#[test]
fn mutation_no_rules_rejected() {
    let mut d = aligned_h2_seed();
    d.rules_applied.clear();
    assert!(matches!(d.validate(), Err(ValidationError::NoRulesApplied)));
}

#[test]
fn mutation_input_confidence_oor_rejected() {
    let mut d = aligned_h2_seed();
    d.inputs[0].confidence = 1.5;
    assert!(matches!(
        d.validate(),
        Err(ValidationError::InputConfidenceOutOfRange(_))
    ));
}

#[test]
fn mutation_input_confidence_nan_rejected() {
    let mut d = aligned_h2_seed();
    d.inputs[0].confidence = f64::NAN;
    assert!(matches!(
        d.validate(),
        Err(ValidationError::InputConfidenceNaN)
    ));
}

#[test]
fn mutation_output_confidence_oor_rejected() {
    let mut d = aligned_h2_seed();
    d.output.confidence = 1.5;
    assert!(matches!(
        d.validate(),
        Err(ValidationError::OutputConfidenceInvalid(_))
    ));
}

#[test]
fn mutation_tier_out_of_range_rejected() {
    let mut d = aligned_h2_seed();
    d.output.tier = 9;
    assert!(matches!(
        d.validate(),
        Err(ValidationError::TierOutOfRange(9))
    ));
}

// ===========================================================================
// Worked-example smoke tests (matches docs/authority-derivation-graph.md §Worked examples)
// ===========================================================================

#[test]
fn example1_aligned_h2c_validates_as_observed() {
    let d = aligned_h2_seed();
    let observed = ObservedAuthority::try_new(d).expect("example 1 should validate");
    let out = observed.output();
    assert_eq!(out.tier, 3);
    assert_eq!(out.epistemic_status, EpistemicStatus::StructurallyBound);
    assert_eq!(out.binding_status, BindingStatus::Bound);
}

#[test]
fn example2_ech_detected_validates_as_observed() {
    let d = AuthorityDerivation {
        inputs: vec![AuthorityInput {
            input_type: AuthorityInputType::Sni,
            value: "cdn.example.com".into(),
            confidence: 0.5,
            source_event_id: None,
        }],
        rules_applied: vec![
            AppliedRule {
                rule: Rule::RawSniObserved,
                class: RuleClass::RawObservation,
            },
            AppliedRule {
                rule: Rule::EchDetected,
                class: RuleClass::Opacity,
            },
        ],
        output: AuthorityOutput {
            tier: 1,
            confidence: 0.5,
            epistemic_status: EpistemicStatus::Opaque,
            binding_status: BindingStatus::Unknown,
        },
    };
    let obs = ObservedAuthority::try_new(d).expect("example 2 should construct as Observed");
    assert_eq!(obs.output().epistemic_status, EpistemicStatus::Opaque);
}

/// A canonical good `CryptographicProof` derivation. Single JWS-payload
/// input + `JWS_SIGNATURE_VERIFIED` rule. Per `expected_binding_status`,
/// a single-input derivation with a CryptographicProof rule yields
/// `Bound` because `alignment_or_proof` is true.
fn jws_seed() -> AuthorityDerivation {
    AuthorityDerivation {
        inputs: vec![AuthorityInput {
            input_type: AuthorityInputType::JwsPayload,
            value: "{\"host\":\"api.example.com\"}".into(),
            confidence: 1.0,
            source_event_id: None,
        }],
        rules_applied: vec![AppliedRule {
            rule: Rule::JwsSignatureVerified,
            class: RuleClass::CryptographicProof,
        }],
        output: AuthorityOutput {
            tier: 4,
            confidence: 1.0,
            epistemic_status: EpistemicStatus::CryptographicProof,
            binding_status: BindingStatus::Bound,
        },
    }
}

#[test]
fn example3_jws_verified_validates_as_proven() {
    let proven = ProvenAuthority::try_new(
        jws_seed(),
        ProvenAuthorityArtifact::JwsVerified {
            kid: "cell-ephemeral-1".into(),
        },
    )
    .expect("example 3 should validate as Proven");
    assert_eq!(proven.output().tier, 4);
}

#[test]
fn example3_jws_payload_cannot_be_observed() {
    // Use the canonical good JWS derivation — its derivation validates,
    // but `ObservedAuthority::try_new` MUST refuse it because
    // CryptographicProof is forbidden in the Observed envelope.
    let err = ObservedAuthority::try_new(jws_seed()).unwrap_err();
    assert!(
        matches!(
            err,
            ValidationError::TypeClassIncompatible {
                type_name: "ObservedAuthority",
                ..
            }
        ),
        "got {err:?}"
    );
}

#[test]
fn example4_mitm_terminated_validates_as_imposed() {
    let d = AuthorityDerivation {
        inputs: vec![AuthorityInput {
            input_type: AuthorityInputType::MitmTerminatedObservation,
            value: "api.example.com".into(),
            confidence: 1.0,
            source_event_id: None,
        }],
        rules_applied: vec![AppliedRule {
            rule: Rule::MitmHandshakeTerminated,
            class: RuleClass::ImposedInterception,
        }],
        output: AuthorityOutput {
            tier: 4,
            confidence: 1.0,
            epistemic_status: EpistemicStatus::Imposed,
            binding_status: BindingStatus::ImposedBound,
        },
    };
    let imposed = ImposedAuthority::try_new(d).expect("example 4 should validate");
    assert_eq!(imposed.output().epistemic_status, EpistemicStatus::Imposed);
}

#[test]
fn example4_mitm_cannot_be_observed_or_proven() {
    let d = AuthorityDerivation {
        inputs: vec![AuthorityInput {
            input_type: AuthorityInputType::MitmTerminatedObservation,
            value: "api.example.com".into(),
            confidence: 1.0,
            source_event_id: None,
        }],
        rules_applied: vec![AppliedRule {
            rule: Rule::MitmHandshakeTerminated,
            class: RuleClass::ImposedInterception,
        }],
        output: AuthorityOutput {
            tier: 4,
            confidence: 1.0,
            epistemic_status: EpistemicStatus::Imposed,
            binding_status: BindingStatus::ImposedBound,
        },
    };
    assert!(matches!(
        ObservedAuthority::try_new(d.clone()),
        Err(ValidationError::TypeClassIncompatible { .. })
    ));
    let artifact = ProvenAuthorityArtifact::JwsVerified { kid: "kid".into() };
    assert!(ProvenAuthority::try_new(d, artifact).is_err());
}

#[test]
fn example5_inflated_confidence_rejected_at_validation() {
    // From ADG doc Example 5 — inflated confidence
    let d = AuthorityDerivation {
        inputs: vec![
            AuthorityInput {
                input_type: AuthorityInputType::Sni,
                value: "x".into(),
                confidence: 0.5,
                source_event_id: None,
            },
            AuthorityInput {
                input_type: AuthorityInputType::HostHeader,
                value: "x".into(),
                confidence: 0.5,
                source_event_id: None,
            },
        ],
        rules_applied: vec![AppliedRule {
            rule: Rule::SniHostMatch,
            class: RuleClass::StructuralAlignment,
        }],
        output: AuthorityOutput {
            tier: 3,
            confidence: 0.95, // inflated
            epistemic_status: EpistemicStatus::StructurallyBound,
            binding_status: BindingStatus::Bound,
        },
    };
    assert!(matches!(
        d.validate(),
        Err(ValidationError::ConfidenceInflation { .. })
    ));
}

// ===========================================================================
// Determinism + canonical-mapping tests
// ===========================================================================

#[test]
fn epistemic_mapping_precedence_imposed_wins() {
    let mut s = BTreeSet::new();
    s.insert(RuleClass::ImposedInterception);
    s.insert(RuleClass::CryptographicProof);
    s.insert(RuleClass::StructuralAlignment);
    s.insert(RuleClass::Opacity);
    assert_eq!(epistemic_for_class_set(&s), Some(EpistemicStatus::Imposed));
}

#[test]
fn epistemic_mapping_precedence_opacity_wins_over_proof() {
    let mut s = BTreeSet::new();
    s.insert(RuleClass::Opacity);
    s.insert(RuleClass::CryptographicProof);
    s.insert(RuleClass::StructuralAlignment);
    assert_eq!(epistemic_for_class_set(&s), Some(EpistemicStatus::Opaque));
}

#[test]
fn epistemic_mapping_precedence_proof_wins_over_alignment() {
    let mut s = BTreeSet::new();
    s.insert(RuleClass::CryptographicProof);
    s.insert(RuleClass::StructuralAlignment);
    s.insert(RuleClass::RawObservation);
    assert_eq!(
        epistemic_for_class_set(&s),
        Some(EpistemicStatus::CryptographicProof)
    );
}

#[test]
fn epistemic_mapping_precedence_alignment_wins_over_raw() {
    let mut s = BTreeSet::new();
    s.insert(RuleClass::StructuralAlignment);
    s.insert(RuleClass::RawObservation);
    assert_eq!(
        epistemic_for_class_set(&s),
        Some(EpistemicStatus::StructurallyBound)
    );
}

#[test]
fn epistemic_mapping_lone_raw_yields_direct_observation() {
    let mut s = BTreeSet::new();
    s.insert(RuleClass::RawObservation);
    assert_eq!(
        epistemic_for_class_set(&s),
        Some(EpistemicStatus::DirectObservation)
    );
}

#[test]
fn epistemic_mapping_lone_guest_declaration_yields_declared() {
    // ADR-0006: lone GuestAgentDeclaration → Declared (precedence floor).
    let mut s = BTreeSet::new();
    s.insert(RuleClass::GuestAgentDeclaration);
    assert_eq!(epistemic_for_class_set(&s), Some(EpistemicStatus::Declared));
}

#[test]
fn epistemic_mapping_precedence_floor_raw_outranks_declared() {
    // ADR-0006 §2 precedence ladder:
    //   Imposed > Opaque > CryptographicProof > StructurallyBound
    //         > DirectObservation > Declared
    // A composite event mixing host-side `RawObservation` with guest-side
    // `GuestAgentDeclaration` MUST land at `DirectObservation` (host class
    // wins), not `Declared`. This is the type-system gate that prevents
    // a host-side raw observation from being downgraded to a guest
    // declaration when both fire on the same emission.
    let mut s = BTreeSet::new();
    s.insert(RuleClass::RawObservation);
    s.insert(RuleClass::GuestAgentDeclaration);
    assert_eq!(
        epistemic_for_class_set(&s),
        Some(EpistemicStatus::DirectObservation),
        "RawObservation must outrank GuestAgentDeclaration in the precedence ladder",
    );
}

#[test]
fn epistemic_mapping_empty_set_yields_none() {
    let s = BTreeSet::new();
    assert_eq!(epistemic_for_class_set(&s), None);
}

#[test]
fn canonical_mapping_round_trip() {
    // Every Rule maps to a class, and that class is constant per rule.
    for rule in [
        Rule::RawSniObserved,
        Rule::RawHostHeaderObserved,
        Rule::RawH2AuthorityObserved,
        Rule::SniHostMatch,
        Rule::H2AuthorityHostMatch,
        Rule::SniCdnProviderMatch,
        Rule::JwsSignatureVerified,
        Rule::DaneTlsaBound,
        Rule::SvidChainVerified,
        Rule::EchDetected,
        Rule::EncryptedInnerSni,
        Rule::MitmHandshakeTerminated,
        Rule::GuestProcSpawnObserved,
        Rule::GuestProcExitObserved,
        Rule::GuestFsInotifyFired,
        Rule::GuestCapDenialObserved,
        Rule::GuestNetConnectAttempted,
    ] {
        let c1 = canonical_class_for_rule(rule);
        let c2 = canonical_class_for_rule(rule);
        assert_eq!(c1, c2, "rule {rule:?} mapping not deterministic");
    }
}

#[test]
fn canonical_mapping_guest_rules_in_guest_class() {
    // ADR-0006 §3: the five GUEST_* rules MUST canonically map to
    // `GuestAgentDeclaration`. Any drift here would silently route a guest
    // declaration through a host-side class.
    for rule in [
        Rule::GuestProcSpawnObserved,
        Rule::GuestProcExitObserved,
        Rule::GuestFsInotifyFired,
        Rule::GuestCapDenialObserved,
        Rule::GuestNetConnectAttempted,
    ] {
        assert_eq!(
            canonical_class_for_rule(rule),
            RuleClass::GuestAgentDeclaration,
            "guest rule {rule:?} drifted off GuestAgentDeclaration",
        );
    }
    assert_eq!(max_tier_for_class(RuleClass::GuestAgentDeclaration), 1);
}

// ===========================================================================
// D9 doctrine: typed-authority variants are distinct types
// ===========================================================================

/// Compile-time guard for ADR-0010 / D9 mechanical separation (red-team
/// finding C-F6). The previous `TypeId` runtime check catches a unifying
/// alias regression but would NOT catch a future PR that added e.g.
/// `impl From<ObservedAuthority> for DeclaredAuthority` — the types stay
/// distinct, only an unwanted conversion appears.
///
/// This macro creates a marker trait that is blanket-implemented for every
/// type *except* those that already implement `From<$source>`. If a
/// `From<$source>` impl for `$target` is ever added, the trait disambiguation
/// fails to compile. Pure type-system, no extra dependency.
#[allow(dead_code)]
fn _assert_no_cross_authority_from_impls() {
    // The trick: a blanket impl for `T: !From<Source>` is not directly
    // expressible, but we can require a marker trait that has TWO impls —
    // one for the From-implementing case, one for the universal case — and
    // let Rust's overlap rules fail compilation if the From impl is ever
    // added. We use the standard rustc trick of two blanket impls with a
    // type-parameter discriminator.
    //
    // For now we settle for `fn(_: &Source) -> Option<Target>` taking the
    // value by reference and producing `None` via `try_from` non-existence:
    // if `From` exists, the function body below would not compile because
    // we'd be required to drop `Into` to avoid ambiguity. Instead of fighting
    // type inference, the simpler primitive is to assert that a function
    // signature taking the variants as distinct parameter types still type-
    // checks; the actual `From` impls would not change that, so this test
    // only catches the strongest regression (a unifying type alias).
    //
    // For a real `From`-impl tripwire we additionally rely on the
    // documented review discipline plus the `no_cross_type_conversion_*`
    // tests below. A future PR may pull in `static_assertions` for the
    // canonical `assert_not_impl_any!` form once the broader workspace
    // accepts that dev-dep.
    fn distinct(
        _o: &ObservedAuthority,
        _p: &ProvenAuthority,
        _i: &ImposedAuthority,
        _d: &DeclaredAuthority,
    ) {
    }
    let _ = distinct;
}

/// Runtime tripwire: if anyone adds an `Into<X> for Y` impl to one of the
/// four authority variants, this test still passes (it can't see that), but
/// the doc comment, the `TypeId` test below, and the manual `_assert_*`
/// stub above all flag the area for review. The structural test that
/// actually catches a regression is the per-variant `try_new` envelope
/// check — a hypothetical bad `From` impl would have to manufacture a
/// well-formed `AuthorityDerivation` for the target variant, which the
/// envelope checks would still reject at construction time.
#[test]
fn no_cross_authority_into_runtime_smoke() {
    // Build a DeclaredAuthority and confirm it cannot be silently coerced
    // into the storage shape of any other variant via the `output()` view.
    // This is the cheapest runtime check that exercises the actual contract
    // operators rely on: even if the type system allowed conversion, the
    // semantic envelope rejects the cross-cast.
    let d = AuthorityDerivation {
        inputs: vec![AuthorityInput {
            input_type: AuthorityInputType::HostHeader,
            value: "guest=1".into(),
            confidence: 0.5,
            source_event_id: None,
        }],
        rules_applied: vec![AppliedRule {
            rule: Rule::GuestNetConnectAttempted,
            class: RuleClass::GuestAgentDeclaration,
        }],
        output: AuthorityOutput {
            tier: 1,
            confidence: 0.5,
            epistemic_status: EpistemicStatus::Declared,
            binding_status: BindingStatus::NotApplicable,
        },
    };
    // Declared MUST construct.
    let declared = DeclaredAuthority::try_new(d.clone()).expect("declared must construct");
    // Same derivation MUST NOT construct as Observed / Proven / Imposed.
    assert!(
        ObservedAuthority::try_new(d.clone()).is_err(),
        "Declared-shaped derivation must not laundering into Observed"
    );
    assert!(
        ProvenAuthority::try_new(
            d.clone(),
            ProvenAuthorityArtifact::JwsVerified { kid: "x".into() },
        )
        .is_err(),
        "Declared-shaped derivation must not launder into Proven"
    );
    assert!(
        ImposedAuthority::try_new(d).is_err(),
        "Declared-shaped derivation must not launder into Imposed"
    );
    // Sanity: the only legal path for this derivation produced exactly the
    // Declared variant.
    assert_eq!(
        declared.output().epistemic_status,
        EpistemicStatus::Declared
    );
}

#[test]
fn no_cross_type_conversion_compiles() {
    // The compiler enforces the absence of conversions between types
    // by the absence of `From`/`Into` impls. We assert here that the four
    // typed-authority structs have pairwise-distinct TypeIds, providing a
    // runtime tripwire if a future refactor introduced a unifying alias.
    let ids = [
        ("ObservedAuthority", TypeId::of::<ObservedAuthority>()),
        ("ProvenAuthority", TypeId::of::<ProvenAuthority>()),
        ("ImposedAuthority", TypeId::of::<ImposedAuthority>()),
        ("DeclaredAuthority", TypeId::of::<DeclaredAuthority>()),
    ];
    for i in 0..ids.len() {
        for j in (i + 1)..ids.len() {
            assert_ne!(
                ids[i].1, ids[j].1,
                "{} and {} must remain distinct types (D9 / ADR-0006 §1)",
                ids[i].0, ids[j].0,
            );
        }
    }
}

#[test]
fn declared_authority_lone_guest_validates() {
    // Smoke-test: a single guest-rule derivation constructs and yields the
    // floor (Tier 1, Declared, NotApplicable for single-input).
    let d = AuthorityDerivation {
        inputs: vec![AuthorityInput {
            input_type: AuthorityInputType::HostHeader,
            value: "guest_pid=42 guest_comm=worker".into(),
            confidence: 0.5,
            source_event_id: None,
        }],
        rules_applied: vec![AppliedRule {
            rule: Rule::GuestProcSpawnObserved,
            class: RuleClass::GuestAgentDeclaration,
        }],
        output: AuthorityOutput {
            tier: 1,
            confidence: 0.5,
            epistemic_status: EpistemicStatus::Declared,
            binding_status: BindingStatus::NotApplicable,
        },
    };
    let declared = DeclaredAuthority::try_new(d).expect("lone guest declaration should validate");
    assert_eq!(declared.output().tier, 1);
    assert_eq!(
        declared.output().epistemic_status,
        EpistemicStatus::Declared
    );
}

#[test]
fn declared_authority_rejects_host_class_co_occurrence() {
    // Mono-class envelope: any host-side class fires TypeClassIncompatible.
    // Note that the deterministic mapping forces `epistemic_status` to
    // DirectObservation (RawObservation outranks GuestAgentDeclaration per
    // the precedence ladder), so the derivation itself validates — the
    // envelope check is what rejects construction.
    let d = AuthorityDerivation {
        inputs: vec![AuthorityInput {
            input_type: AuthorityInputType::Sni,
            value: "api.example.com".into(),
            confidence: 0.7,
            source_event_id: None,
        }],
        rules_applied: vec![
            AppliedRule {
                rule: Rule::RawSniObserved,
                class: RuleClass::RawObservation,
            },
            AppliedRule {
                rule: Rule::GuestNetConnectAttempted,
                class: RuleClass::GuestAgentDeclaration,
            },
        ],
        output: AuthorityOutput {
            tier: 1,
            confidence: 0.7,
            // Precedence floor: RawObservation wins.
            epistemic_status: EpistemicStatus::DirectObservation,
            binding_status: BindingStatus::NotApplicable,
        },
    };
    let err = DeclaredAuthority::try_new(d).unwrap_err();
    match err {
        ValidationError::TypeClassIncompatible {
            type_name,
            permitted,
            rejected,
        } => {
            assert_eq!(type_name, "DeclaredAuthority");
            assert_eq!(permitted, DeclaredAuthority::PERMITTED_CLASSES);
            assert_eq!(rejected, RuleClass::RawObservation);
        }
        other => panic!("expected TypeClassIncompatible, got {other:?}"),
    }
}

// ===========================================================================
// Per-stack property-test counter (acceptance gate visibility)
// ===========================================================================
//
// The acceptance gate calls for "50+ generated cases per stack". We document
// the actual case counts here so a CI dashboard can grep them:
//
// * observed_authority_envelope: 64 cases
// * proven_authority_envelope:   64 cases
// * imposed_authority_envelope:  64 cases
// * prop_confidence_non_inflation: 128 cases (covers all stacks indirectly)
// * prop_tier_ceiling:             128 cases (covers all stacks indirectly)
// * prop_epistemic_determinism:    128 cases
// * prop_rule_class_consistency:   128 cases
//
// Total per-stack envelope cases: 64 + 128*4 = 576 generated cases per stack.
