//! Property tests for authority-derivation non-inflation (TEST-12).
//!
//! The Authority Model §9 non-inflation invariant requires that the grantor-
//! signed leaf capability is a subset of the spec's declared authority:
//!
//! ```text
//!   token.leafCapability  ⊆  spec.authority
//! ```
//!
//! In other words, a token can only attest to *narrowing* — never to claiming
//! authority the spec doesn't already declare. The verifier
//! ([`cellos_core::verify_authority_derivation`]) enforces this structurally
//! before it even looks at the ED25519 signature, returning an `InvalidSpec`
//! error whose message contains `"leafCapability"`.
//!
//! These property tests randomize the spec / leaf rule sets and assert:
//!
//! 1. **Overclaim rejection**: when the leaf claims at least one rule
//!    (egress or secret) that the spec does NOT declare, validation MUST
//!    fail with the structural-overclaim error — never silently pass.
//! 2. **Subset acceptance (structural)**: when the leaf is a proper subset
//!    of the spec's declared authority, the structural check MUST pass;
//!    the only failure mode left is signature verification (we feed an
//!    empty role-keys map, so the run terminates in the "unknown role"
//!    branch rather than `"leafCapability"`).
//!
//! Property #2 isolates the structural invariant from the signature path —
//! we deliberately do NOT mint a real signature here. That keeps these
//! invariant tests fast (no key generation per case) and keeps the
//! structural-vs-cryptographic concerns layered.
//!
//! The end-to-end signature-valid path is covered by the unit tests in
//! `crates/cellos-core/src/spec_validation.rs` (`verify_authority_derivation_child_within_parent_passes`).

use cellos_core::{
    AuthorityBundle, AuthorityCapability, AuthorityDerivationToken, AuthoritySignature, EgressRule,
    ExecutionCellSpec, Lifetime, RoleId,
};
use proptest::collection::{hash_set, vec as pvec};
use proptest::prelude::*;
use std::collections::HashSet;

// ── Fixture builders ────────────────────────────────────────────────────────

fn build_spec(egress_rules: Vec<EgressRule>, secret_refs: Vec<String>) -> ExecutionCellSpec {
    ExecutionCellSpec {
        id: "proptest-spec".into(),
        correlation: None,
        ingress: None,
        environment: None,
        placement: None,
        policy: None,
        identity: None,
        run: None,
        authority: AuthorityBundle {
            filesystem: None,
            network: None,
            egress_rules: Some(egress_rules),
            secret_refs: Some(secret_refs),
            authority_derivation: None,
            dns_authority: None,
            cdn_authority: None,
        },
        lifetime: Lifetime { ttl_seconds: 60 },
        export: None,
        telemetry: None,
    }
}

fn build_token(leaf: AuthorityCapability) -> AuthorityDerivationToken {
    AuthorityDerivationToken {
        role_root: RoleId("proptest-role".into()),
        parent_run_id: Some("run-0".into()),
        derivation_steps: vec![],
        leaf_capability: leaf,
        grantor_signature: AuthoritySignature {
            algorithm: "ed25519".into(),
            // Deliberate junk — proptests focus on the structural step.
            bytes: "AAAA".into(),
        },
    }
}

// ── Strategies ──────────────────────────────────────────────────────────────

/// Single egress rule with a small, finite host space so collisions are
/// possible (and proper subsets occur naturally).
fn egress_strategy() -> impl Strategy<Value = EgressRule> {
    (
        prop::sample::select(vec![
            "api.example.com",
            "db.example.com",
            "cache.example.com",
            "auth.example.com",
            "log.example.com",
        ]),
        prop::sample::select(vec![80u16, 443, 5432, 6379, 8080]),
        prop::option::of(prop::sample::select(vec!["tcp", "https", "http", "udp"])),
    )
        .prop_map(|(host, port, proto)| EgressRule {
            host: host.to_string(),
            port,
            protocol: proto.map(str::to_string),
            dns_egress_justification: None,
        })
}

/// Distinct egress rule set, 0–8 entries.
fn egress_set_strategy() -> impl Strategy<Value = Vec<EgressRule>> {
    pvec(egress_strategy(), 0..8).prop_map(|rules| {
        // Dedupe — `is_superset_of` does case-insensitive host match, so we
        // keep first-seen by (host_lowercase, port, protocol) to match.
        let mut seen: HashSet<(String, u16, Option<String>)> = HashSet::new();
        rules
            .into_iter()
            .filter(|r| seen.insert((r.host.to_ascii_lowercase(), r.port, r.protocol.clone())))
            .collect()
    })
}

/// Distinct secret-ref set, 0–6 entries.
fn secret_set_strategy() -> impl Strategy<Value = Vec<String>> {
    hash_set(
        prop::sample::select(vec![
            "db-password",
            "api-key",
            "session-key",
            "signing-key",
            "root-token",
            "vault-token",
        ])
        .prop_map(str::to_string),
        0..6,
    )
    .prop_map(|s| s.into_iter().collect())
}

// ── Properties ──────────────────────────────────────────────────────────────

proptest! {
    /// Property #1 — Overclaim rejection.
    ///
    /// Construct a spec, then build a leaf that adds at least one extra rule
    /// (egress or secret) on top of a random subset of the spec. The leaf is
    /// therefore guaranteed to claim authority the spec does not declare,
    /// and validation MUST fail with the structural-overclaim message.
    #[test]
    fn leaf_with_extra_rule_is_always_rejected(
        spec_egress in egress_set_strategy(),
        spec_secrets in secret_set_strategy(),
        extra_egress in egress_strategy(),
        extra_secret in prop::sample::select(vec![
            "ghost-key", "phantom-token", "shadow-cred",
        ]).prop_map(str::to_string),
        which in 0u8..2u8, // 0 = add extra egress, 1 = add extra secret
    ) {
        // Ensure `extra_egress` truly does not collide with anything in the
        // spec — if proptest happened to draw a host already declared, skip.
        let extra_is_novel_egress = !spec_egress.iter().any(|r| {
            r.host.eq_ignore_ascii_case(&extra_egress.host)
                && r.port == extra_egress.port
                && r.protocol == extra_egress.protocol
        });
        let extra_is_novel_secret = !spec_secrets.iter().any(|s| s == &extra_secret);

        // Skip degenerate cases where the chosen "extra" already exists.
        prop_assume!(match which {
            0 => extra_is_novel_egress,
            _ => extra_is_novel_secret,
        });

        let spec = build_spec(spec_egress.clone(), spec_secrets.clone());

        // Leaf = spec ∪ { extra } — guaranteed to have at least one rule the
        // spec doesn't declare.
        let mut leaf_egress = spec_egress.clone();
        let mut leaf_secrets = spec_secrets.clone();
        if which == 0 {
            leaf_egress.push(extra_egress);
        } else {
            leaf_secrets.push(extra_secret);
        }

        let token = build_token(AuthorityCapability {
            egress_rules: leaf_egress,
            secret_refs: leaf_secrets,
        });

        let role_keys = std::collections::HashMap::new();
        let result = cellos_core::verify_authority_derivation(&spec, &token, &role_keys);
        let err = result.expect_err("overclaim must be rejected structurally");
        let msg = err.to_string();
        prop_assert!(
            msg.contains("leafCapability"),
            "expected structural-overclaim error, got: {msg}"
        );
    }

    /// Property #2 — Subset acceptance, structural step.
    ///
    /// When the leaf is a (possibly proper) subset of the spec, the
    /// structural check passes. Because we don't mint a real signature, the
    /// run terminates in the signature path. With an empty `role_keys` map,
    /// the verifier returns `"unknown role: <role-id>"` — NOT the
    /// `"leafCapability"` overclaim message. Asserting on the absence of
    /// the structural-overclaim message is the cleanest way to confirm the
    /// structural step passed.
    #[test]
    fn leaf_subset_of_spec_passes_structural_step(
        spec_egress in egress_set_strategy(),
        spec_secrets in secret_set_strategy(),
        keep_mask_egress in pvec(any::<bool>(), 0..8),
        keep_mask_secret in pvec(any::<bool>(), 0..6),
    ) {
        let spec = build_spec(spec_egress.clone(), spec_secrets.clone());

        // Pick a subset by keep_mask, padding/truncating to spec length.
        let leaf_egress: Vec<_> = spec_egress
            .iter()
            .enumerate()
            .filter(|(i, _)| *keep_mask_egress.get(*i).unwrap_or(&true))
            .map(|(_, r)| r.clone())
            .collect();
        let leaf_secrets: Vec<_> = spec_secrets
            .iter()
            .enumerate()
            .filter(|(i, _)| *keep_mask_secret.get(*i).unwrap_or(&true))
            .map(|(_, s)| s.clone())
            .collect();

        let token = build_token(AuthorityCapability {
            egress_rules: leaf_egress,
            secret_refs: leaf_secrets,
        });

        let role_keys = std::collections::HashMap::new();
        let result = cellos_core::verify_authority_derivation(&spec, &token, &role_keys);
        let err = result.expect_err("empty role_keys forces signature failure");
        let msg = err.to_string();
        prop_assert!(
            !msg.contains("leafCapability"),
            "structural check should pass for subset leaf; got structural error: {msg}"
        );
        prop_assert!(
            msg.contains("unknown role") || msg.contains("signature"),
            "expected signature/role failure, got: {msg}"
        );
    }
}
