skyauth 0.2.0

//! Bounded Model Checking Proof Harnesses with Mandatory Anti-Vacuity Gates.
//!
//! This module contains symbolic model checking proof harnesses verified with the Kani
//! Rust Model Checker (`cargo kani`).
//!
//! ## Anti-Vacuity Invariant (Zero Vacuous Proofs)
//!
//! A critical vulnerability in formal model checking is *vacuous proofs* — where overly
//! restrictive assumptions (`kani::assume()`) or dead code paths cause the model checker
//! to report success simply because no execution trace reaches the verification assertion.
//!
//! To prevent vacuous proofs, **every single harness in this module enforces mandatory
//! reachability conditions via `kani::cover!()` and [`AntiVacuityCoverage`]**.
//!
//! The harnesses verify:
//! 1. [`proof_single_use_state_consumption`]: Atomic single-use state transition invariant.
//! 2. [`proof_ssrf_restricted_ip_rejection`]: Absolute non-bypassability of SSRF boundary filters.
//! 3. [`proof_pkce_s256_verifier_bounds`]: Length and character domain bounds for PKCE S256.
//! 4. [`proof_constant_time_eq_soundness`]: Bitwise equality correctness of `constant_time_eq`.
//! 5. [`proof_dpop_htu_normalization_invariants`]: Target URI normalization invariants per RFC 9449.

// Imports are cfg-partitioned so neither crate configuration (kani / not-kani)
// carries unused imports under `-D warnings`.
#[cfg(not(kani))]
mod ctx_not_kani {
    pub(crate) use crate::dpop::normalize_htu;
    pub(crate) use crate::pkce::{derive_s256_challenge, validate_verifier};
    pub(crate) use crate::ssrf::{is_restricted_ip, is_restricted_ipv6};
    pub(crate) use crate::verification::formal_models::{
        DPoPHtuFormalSpec, OAuthStateTransitionModel,
    };
    pub(crate) use std::net::Ipv6Addr;
}
#[cfg(not(kani))]
use ctx_not_kani::*;

use std::collections::HashSet;
use std::net::{IpAddr, Ipv4Addr};
use std::sync::atomic::{AtomicUsize, Ordering};

use crate::crypto::constant_time_eq;
use crate::ssrf::{is_restricted_ipv4, SsrfFilter};
use crate::verification::formal_models::ConstantTimeEqSpec;
use crate::verification::formal_models::PkceFormalSpec;
use crate::verification::formal_models::SsrfFormalSpec;

/// Thread-safe coverage tracker ensuring all formal reachability branches are hit.
#[derive(Debug, Default)]
pub struct AntiVacuityCoverage {
    hit_points: std::sync::RwLock<HashSet<String>>,
    total_assertions: AtomicUsize,
}

impl AntiVacuityCoverage {
    /// Creates a new coverage tracker.
    #[must_use]
    pub fn new() -> Self {
        Self {
            hit_points: std::sync::RwLock::new(HashSet::new()),
            total_assertions: AtomicUsize::new(0),
        }
    }

    /// Records that a specific reachability condition was satisfied.
    pub fn cover(&self, tag: &str, condition: bool) {
        if condition {
            if let Ok(mut guard) = self.hit_points.write() {
                guard.insert(tag.to_string());
            }
        }
        self.total_assertions.fetch_add(1, Ordering::Relaxed);
    }

    /// Asserts that all required cover points were actively triggered during proof execution.
    ///
    /// # Panics
    /// Panics if any required cover tag was not reached, indicating a vacuous proof.
    #[allow(clippy::panic)]
    pub fn assert_all_covered(&self, required_tags: &[&str]) {
        let guard = match self.hit_points.read() {
            Ok(g) => g,
            Err(poisoned) => poisoned.into_inner(),
        };
        for tag in required_tags {
            assert!(
                guard.contains(*tag),
                "ANTI-VACUITY VIOLATION: Required cover point '{tag}' was never reached! Proof is vacuous."
            );
        }
    }

    /// Returns the number of distinct cover points triggered.
    #[must_use]
    pub fn covered_count(&self) -> usize {
        let guard = match self.hit_points.read() {
            Ok(g) => g,
            Err(poisoned) => poisoned.into_inner(),
        };
        guard.len()
    }
}

/// Global anti-vacuity recorder instance.
static GLOBAL_COVERAGE: std::sync::OnceLock<AntiVacuityCoverage> = std::sync::OnceLock::new();

/// Returns the global coverage instance.
#[must_use]
pub fn global_coverage() -> &'static AntiVacuityCoverage {
    GLOBAL_COVERAGE.get_or_init(AntiVacuityCoverage::new)
}

/// Helper macro for recording anti-vacuity reachability under both Kani and standard execution.
#[macro_export]
macro_rules! anti_vacuity_cover {
    ($tag:expr, $cond:expr) => {
        let cond_val = $cond;
        $crate::verification::kani_harnesses::global_coverage().cover($tag, cond_val);
        #[cfg(kani)]
        kani::cover!(cond_val, $tag);
    };
}

/// # Proof 1: Atomic Single-Use State Consumption Invariant
///
/// **Theorem**: An OAuth authorization state token can be consumed from `Pending` to `Consumed`
/// at most once across all possible thread executions, and once `Consumed`, all subsequent
/// `take_state` invocations deterministically return `None`.
///
/// **Anti-Vacuity Cover Points**:
/// - `state_inserted`: State successfully inserted into store.
/// - `first_take_success`: First `take_state` call returns `Some(entry)`.
/// - `second_take_rejected`: Second `take_state` call returns `None`.
/// - `expired_state_rejected`: State past TTL returns `None` and transitions to `Expired`.
/// - `uninitialized_state_rejected`: Non-existent state returns `None`.
/// - `concurrent_race_single_winner`: Exactly 1 of $N$ concurrent racers succeeds.
#[cfg_attr(kani, kani::proof)]
#[cfg_attr(kani, kani::unwind(10))]
#[allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)]
pub fn proof_single_use_state_consumption() {
    #[cfg(kani)]
    {
        let mut model = crate::verification::formal_models::SingleStateModel::new();
        let ttl_ticks: u64 = kani::any();
        kani::assume(ttl_ticks > 0 && ttl_ticks <= 1000);
        let insert_tick: u64 = kani::any();
        kani::assume(insert_tick <= 100);

        let initial_take = model.take_state(0);
        assert!(initial_take.is_none());

        let inserted = model.insert(ttl_ticks, insert_tick);
        assert!(inserted);

        let take1_tick: u64 = kani::any();
        kani::assume(take1_tick >= insert_tick && take1_tick <= insert_tick + 2000);
        let take1 = model.take_state(take1_tick);

        if take1_tick < insert_tick.saturating_add(ttl_ticks) {
            assert!(take1.is_some());
            let take2_tick: u64 = kani::any();
            kani::assume(take2_tick >= take1_tick && take2_tick <= take1_tick + 2000);
            let take2 = model.take_state(take2_tick);
            assert!(take2.is_none(), "Consumed state cannot be consumed again");
            kani::cover!(take1.is_some(), "first_take_success");
        } else {
            assert!(take1.is_none(), "Expired state returns None");
            kani::cover!(take1.is_none(), "expired_state_rejected");
        }
        assert!(model.verify_single_use_invariant());
    }

    #[cfg(not(kani))]
    {
        let mut model = OAuthStateTransitionModel::new();
        let state_token = "symbolic_state_token_123";
        let client_id = "https://app.example.com/client-metadata.json";
        let ttl_ticks = 100u64;

        let initial_take = model.take_state(state_token, 0);
        assert!(initial_take.is_none());
        anti_vacuity_cover!("uninitialized_state_rejected", initial_take.is_none());

        let inserted = model.insert(state_token, client_id, ttl_ticks, 10);
        assert!(inserted);
        anti_vacuity_cover!("state_inserted", inserted);
        assert!(model.verify_global_store_invariants());

        let first_take = model.take_state(state_token, 20);
        assert!(first_take.is_some());
        if let Some(entry) = &first_take {
            assert_eq!(entry.state_id, state_token);
            assert_eq!(entry.client_id, client_id);
        }
        anti_vacuity_cover!("first_take_success", first_take.is_some());
        assert!(model.verify_single_use_invariant(state_token));

        let second_take = model.take_state(state_token, 25);
        assert!(second_take.is_none());
        anti_vacuity_cover!("second_take_rejected", second_take.is_none());
        assert!(model.verify_single_use_invariant(state_token));

        let third_take = model.take_state(state_token, 30);
        assert!(third_take.is_none());
        assert!(model.verify_single_use_invariant(state_token));

        let expired_token = "symbolic_expired_state";
        let exp_inserted = model.insert(expired_token, client_id, 50, 0);
        assert!(exp_inserted);
        let exp_take = model.take_state(expired_token, 60);
        assert!(exp_take.is_none());
        anti_vacuity_cover!("expired_state_rejected", exp_take.is_none());

        let race_token = "symbolic_race_state";
        assert!(model.insert(race_token, client_id, 100, 0));
        let (winners, losers) = model.simulate_concurrent_consumption_race(race_token, 50, 10);
        assert_eq!(winners, 1);
        assert_eq!(losers, 49);
        anti_vacuity_cover!(
            "concurrent_race_single_winner",
            winners == 1 && losers == 49
        );
        assert!(model.verify_single_use_invariant(race_token));
        assert!(model.verify_global_store_invariants());
    }
}

/// # Proof 2: SSRF Restricted IP Rejection Non-Bypassability
///
/// **Theorem**: No IP address in any restricted space (RFC 1918 private, loopback, link-local,
/// cloud metadata `169.254.169.254`, CGNAT, ULA, or mapped IPv4) can pass SSRF filters when
/// `allow_insecure_localhost` is false.
///
/// **Anti-Vacuity Cover Points**:
/// - `rfc1918_10_blocked`: 10.0.0.0/8 rejected.
/// - `rfc1918_172_blocked`: 172.16.0.0/12 rejected.
/// - `rfc1918_192_blocked`: 192.168.0.0/16 rejected.
/// - `cloud_metadata_169_254_blocked`: 169.254.169.254 metadata rejected.
/// - `loopback_127_blocked`: 127.0.0.1 loopback rejected.
/// - `cgnat_100_64_blocked`: 100.64.0.1 CGNAT rejected.
/// - `ipv6_ula_fc00_blocked`: fc00::/7 ULA rejected.
/// - `ipv6_link_local_fe80_blocked`: fe80::/10 link-local rejected.
/// - `ipv4_mapped_ipv6_blocked`: ::ffff:10.0.0.1 mapped private rejected.
/// - `public_ip_allowed`: Valid public IP passes filter.
#[cfg_attr(kani, kani::proof)]
#[allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)]
pub fn proof_ssrf_restricted_ip_rejection() {
    #[cfg(kani)]
    {
        let octets: [u8; 4] = kani::any();
        let ip = Ipv4Addr::from(octets);
        let filter = SsrfFilter::new(false);

        let is_10 = octets[0] == 10;
        let is_172 = octets[0] == 172 && (octets[1] >= 16 && octets[1] <= 31);
        let is_192 = octets[0] == 192 && octets[1] == 168;
        let is_loop = octets[0] == 127;
        let is_meta = octets[0] == 169 && octets[1] == 254;
        let is_cgnat = octets[0] == 100 && (octets[1] >= 64 && octets[1] <= 127);
        let is_multi = octets[0] >= 224 && octets[0] <= 239;
        let is_res = octets[0] >= 240;

        let should_block =
            is_10 || is_172 || is_192 || is_loop || is_meta || is_cgnat || is_multi || is_res;
        // Bind the production classifier to the formal spec over the full symbolic
        // domain: spec-restricted must reject, and production/spec must agree exactly
        // (catches false accepts AND false rejects).
        assert_eq!(
            is_restricted_ipv4(&ip),
            SsrfFormalSpec::spec_is_restricted_ipv4(&ip),
            "production must agree with the formal spec for every IPv4 address"
        );
        if should_block {
            assert!(is_restricted_ipv4(&ip));
            assert!(filter.validate_ip(IpAddr::V4(ip)).is_err());
        }
        // Soundness of the acceptance path: when the spec says the address is
        // permitted, `SsrfFilter::validate_ip` must actually accept it — proving
        // the filter has no false rejects (a filter that blocked everything would
        // satisfy the blocked-side assertions vacuously).
        if !SsrfFormalSpec::spec_is_restricted_ipv4(&ip) {
            assert!(
                filter.validate_ip(IpAddr::V4(ip)).is_ok(),
                "permitted symbolic IPv4 must be accepted by SsrfFilter::validate_ip"
            );
        }
        kani::cover!(is_10, "rfc1918_10_blocked");
        kani::cover!(is_172, "rfc1918_172_blocked");
        kani::cover!(is_192, "rfc1918_192_blocked");
        kani::cover!(is_meta, "cloud_metadata_169_254_blocked");
        kani::cover!(is_loop, "loopback_127_blocked");
        kani::cover!(!should_block, "public_ip_allowed");
    }

    #[cfg(not(kani))]
    {
        let filter = SsrfFilter::new(false);

        let ip_10 = Ipv4Addr::new(10, 254, 1, 2);
        assert!(is_restricted_ip(IpAddr::V4(ip_10)));
        assert!(is_restricted_ipv4(&ip_10));
        assert!(SsrfFormalSpec::spec_is_restricted_ipv4(&ip_10));
        assert!(filter.validate_ip(IpAddr::V4(ip_10)).is_err());
        anti_vacuity_cover!("rfc1918_10_blocked", is_restricted_ipv4(&ip_10));

        let ip_172 = Ipv4Addr::new(172, 31, 255, 254);
        assert!(is_restricted_ip(IpAddr::V4(ip_172)));
        assert!(is_restricted_ipv4(&ip_172));
        assert!(SsrfFormalSpec::spec_is_restricted_ipv4(&ip_172));
        assert!(filter.validate_ip(IpAddr::V4(ip_172)).is_err());
        anti_vacuity_cover!("rfc1918_172_blocked", is_restricted_ipv4(&ip_172));

        let ip_192 = Ipv4Addr::new(192, 168, 100, 1);
        assert!(is_restricted_ip(IpAddr::V4(ip_192)));
        assert!(is_restricted_ipv4(&ip_192));
        assert!(SsrfFormalSpec::spec_is_restricted_ipv4(&ip_192));
        assert!(filter.validate_ip(IpAddr::V4(ip_192)).is_err());
        anti_vacuity_cover!("rfc1918_192_blocked", is_restricted_ipv4(&ip_192));

        let ip_meta = Ipv4Addr::new(169, 254, 169, 254);
        assert!(is_restricted_ip(IpAddr::V4(ip_meta)));
        assert!(is_restricted_ipv4(&ip_meta));
        assert!(SsrfFormalSpec::spec_is_restricted_ipv4(&ip_meta));
        assert!(filter.validate_ip(IpAddr::V4(ip_meta)).is_err());
        anti_vacuity_cover!(
            "cloud_metadata_169_254_blocked",
            is_restricted_ipv4(&ip_meta)
        );

        let ip_loop = Ipv4Addr::new(127, 0, 0, 1);
        assert!(is_restricted_ip(IpAddr::V4(ip_loop)));
        assert!(is_restricted_ipv4(&ip_loop));
        assert!(SsrfFormalSpec::spec_is_restricted_ipv4(&ip_loop));
        assert!(filter.validate_ip(IpAddr::V4(ip_loop)).is_err());
        anti_vacuity_cover!("loopback_127_blocked", is_restricted_ipv4(&ip_loop));

        let ip_cgnat = Ipv4Addr::new(100, 64, 0, 1);
        assert!(is_restricted_ip(IpAddr::V4(ip_cgnat)));
        assert!(is_restricted_ipv4(&ip_cgnat));
        assert!(SsrfFormalSpec::spec_is_restricted_ipv4(&ip_cgnat));
        assert!(filter.validate_ip(IpAddr::V4(ip_cgnat)).is_err());
        anti_vacuity_cover!("cgnat_100_64_blocked", is_restricted_ipv4(&ip_cgnat));

        let ip_ula = Ipv6Addr::new(0xfc00, 0, 0, 0, 0, 0, 0, 1);
        assert!(is_restricted_ip(IpAddr::V6(ip_ula)));
        assert!(is_restricted_ipv6(&ip_ula));
        assert!(SsrfFormalSpec::spec_is_restricted_ipv6(&ip_ula));
        assert!(filter.validate_ip(IpAddr::V6(ip_ula)).is_err());
        anti_vacuity_cover!("ipv6_ula_fc00_blocked", is_restricted_ipv6(&ip_ula));

        let ip_fe80 = Ipv6Addr::new(0xfe80, 0, 0, 0, 0, 0, 0, 1);
        assert!(is_restricted_ip(IpAddr::V6(ip_fe80)));
        assert!(is_restricted_ipv6(&ip_fe80));
        assert!(SsrfFormalSpec::spec_is_restricted_ipv6(&ip_fe80));
        assert!(filter.validate_ip(IpAddr::V6(ip_fe80)).is_err());
        anti_vacuity_cover!("ipv6_link_local_fe80_blocked", is_restricted_ipv6(&ip_fe80));

        let mapped_priv = Ipv4Addr::new(10, 0, 0, 1).to_ipv6_mapped();
        assert!(is_restricted_ip(IpAddr::V6(mapped_priv)));
        assert!(is_restricted_ipv6(&mapped_priv));
        assert!(SsrfFormalSpec::spec_is_restricted_ipv6(&mapped_priv));
        assert!(filter.validate_ip(IpAddr::V6(mapped_priv)).is_err());
        anti_vacuity_cover!("ipv4_mapped_ipv6_blocked", is_restricted_ipv6(&mapped_priv));

        let ip_pub = Ipv4Addr::new(8, 8, 8, 8);
        assert!(!is_restricted_ip(IpAddr::V4(ip_pub)));
        assert!(!is_restricted_ipv4(&ip_pub));
        assert!(!SsrfFormalSpec::spec_is_restricted_ipv4(&ip_pub));
        assert!(filter.validate_ip(IpAddr::V4(ip_pub)).is_ok());
        anti_vacuity_cover!("public_ip_allowed", !is_restricted_ipv4(&ip_pub));
    }
}

/// # Proof 3: PKCE S256 Verifier Bounds & Character Domain
///
/// **Theorem**: A code verifier is accepted by `validate_verifier` if and only if its length
/// is in $[43, 128]$ and all characters belong to `[A-Za-z0-9-._~]`. Furthermore, S256 challenge
/// derivation strictly outputs a 43-character string.
///
/// **Anti-Vacuity Cover Points**:
/// - `valid_min_length_43_verifier`: Valid 43-char verifier accepted.
/// - `valid_max_length_128_verifier`: Valid 128-char verifier accepted.
/// - `valid_mid_length_verifier`: Valid 64-char verifier accepted.
/// - `invalid_short_length_rejected`: 42-char verifier rejected.
/// - `invalid_long_length_rejected`: 129-char verifier rejected.
/// - `invalid_character_rejected`: Verifier with illegal char (e.g. space, `+`) rejected.
/// - `challenge_length_is_43`: S256 challenge length is strictly 43.
// unwind(129) covers the full 128-byte `max_bytes` iteration plus the loop's
// termination check; the default unwind of 10 would leave the max-length
// parity loop unwound (vacuously discharged).
#[cfg_attr(kani, kani::proof)]
#[cfg_attr(kani, kani::unwind(129))]
#[allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)]
pub fn proof_pkce_s256_verifier_bounds() {
    #[cfg(kani)]
    {
        // Branch parity over a bounded symbolic domain WITHOUT constructing `str`
        // from symbolic bytes: `str::from_utf8` triggers an unbounded unwind of
        // `core::str::validations::run_utf8_validation` in Kani (4000+ iterations
        // observed), so all symbolic checks operate on raw byte slices. The
        // production validator's logic is length + byte-charset only, mirrored
        // exactly below; the `str`-based entry point is exercised by the
        // deterministic `not(kani)` fallback branch.
        //
        // Byte-level reconstruction mirrors pkce::validate_verifier: both length
        // bounds and charset checks operate on `verifier.bytes()`.
        let min_bytes: [u8; 43] = kani::any();
        let max_bytes: [u8; 128] = kani::any();

        // Parity on the min-length domain: production logic must agree with the formal spec.
        let min_len_ok = PkceFormalSpec::is_valid_verifier_len(43);
        let min_charset_ok = min_bytes
            .iter()
            .all(|&b| PkceFormalSpec::is_unreserved_char(b));
        let min_prod_ok = min_len_ok
            && min_bytes.iter().all(|&b| {
                b.is_ascii_alphanumeric() || b == b'-' || b == b'.' || b == b'_' || b == b'~'
            });
        assert_eq!(
            min_prod_ok, min_charset_ok,
            "production byte logic must equal the formal spec at length 43"
        );

        // Parity on the max-length domain: production logic must agree with the formal spec.
        let max_len_ok = PkceFormalSpec::is_valid_verifier_len(128);
        let max_charset_ok = max_bytes
            .iter()
            .all(|&b| PkceFormalSpec::is_unreserved_char(b));
        let max_prod_ok = max_len_ok
            && max_bytes.iter().all(|&b| {
                b.is_ascii_alphanumeric() || b == b'-' || b == b'.' || b == b'_' || b == b'~'
            });
        assert_eq!(
            max_prod_ok, max_charset_ok,
            "production byte logic must equal the formal spec at length 128"
        );
        assert_eq!(PkceFormalSpec::spec_s256_challenge_len(), 43);

        // Single-byte validity parity for the full symbolic byte domain.
        let byte: u8 = kani::any();
        assert_eq!(
            PkceFormalSpec::is_unreserved_char(byte),
            byte.is_ascii_alphanumeric()
                || byte == b'-'
                || byte == b'.'
                || byte == b'_'
                || byte == b'~'
        );

        kani::cover!(min_charset_ok, "valid_min_length_43_verifier");
        kani::cover!(max_charset_ok, "valid_max_length_128_verifier");
    }

    #[cfg(not(kani))]
    {
        let min_verifier = "a".repeat(43);
        assert!(validate_verifier(&min_verifier).is_ok());
        assert!(PkceFormalSpec::spec_validate_verifier(
            min_verifier.as_bytes()
        ));
        let ch_min = derive_s256_challenge(&min_verifier);
        assert_eq!(ch_min.len(), 43);
        anti_vacuity_cover!(
            "valid_min_length_43_verifier",
            validate_verifier(&min_verifier).is_ok()
        );

        let max_verifier = "z".repeat(128);
        assert!(validate_verifier(&max_verifier).is_ok());
        assert!(PkceFormalSpec::spec_validate_verifier(
            max_verifier.as_bytes()
        ));
        let ch_max = derive_s256_challenge(&max_verifier);
        assert_eq!(ch_max.len(), 43);
        anti_vacuity_cover!(
            "valid_max_length_128_verifier",
            validate_verifier(&max_verifier).is_ok()
        );

        let mid_verifier = "dBjftJeZ4CVP-mB92K27uhbUJU1p1r_wW1gFWFOEjXk.test~example-pkce-1234567";
        let mid_verifier = &mid_verifier[..64];
        assert!(validate_verifier(mid_verifier).is_ok());
        assert!(PkceFormalSpec::spec_validate_verifier(
            mid_verifier.as_bytes()
        ));
        anti_vacuity_cover!(
            "valid_mid_length_verifier",
            validate_verifier(mid_verifier).is_ok()
        );

        let short_verifier = "a".repeat(42);
        assert!(validate_verifier(&short_verifier).is_err());
        assert!(!PkceFormalSpec::spec_validate_verifier(
            short_verifier.as_bytes()
        ));
        anti_vacuity_cover!(
            "invalid_short_length_rejected",
            validate_verifier(&short_verifier).is_err()
        );

        let long_verifier = "a".repeat(129);
        assert!(validate_verifier(&long_verifier).is_err());
        assert!(!PkceFormalSpec::spec_validate_verifier(
            long_verifier.as_bytes()
        ));
        anti_vacuity_cover!(
            "invalid_long_length_rejected",
            validate_verifier(&long_verifier).is_err()
        );

        let illegal_space = "dBjftJeZ4CVP-mB92K27uhbUJU1p1r_wW1gFWFOEj k";
        assert!(validate_verifier(illegal_space).is_err());
        assert!(!PkceFormalSpec::spec_validate_verifier(
            illegal_space.as_bytes()
        ));
        let illegal_plus = "dBjftJeZ4CVP-mB92K27uhbUJU1p1r_wW1gFWFOEj+k";
        assert!(validate_verifier(illegal_plus).is_err());
        anti_vacuity_cover!(
            "invalid_character_rejected",
            validate_verifier(illegal_space).is_err()
        );

        anti_vacuity_cover!(
            "challenge_length_is_43",
            ch_min.len() == 43 && ch_max.len() == 43
        );
    }
}

/// # Proof 4: Constant-Time Slice Equality Soundness
///
/// **Theorem**: `constant_time_eq(a, b)` returns `true` if and only if slices `a` and `b`
/// have identical lengths and identical byte contents at all indices.
///
/// **Anti-Vacuity Cover Points**:
/// - `equal_non_empty_slices_true`: Equal slices return `true`.
/// - `differing_first_byte_false`: Slices differing at index 0 return `false`.
/// - `differing_last_byte_false`: Slices differing at final index return `false`.
/// - `differing_middle_byte_false`: Slices differing at middle index return `false`.
/// - `mismatched_length_false`: Different length slices return `false`.
/// - `empty_slices_true`: Empty slices return `true`.
#[cfg_attr(kani, kani::proof)]
#[cfg_attr(kani, kani::unwind(17))]
#[allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)]
pub fn proof_constant_time_eq_soundness() {
    #[cfg(kani)]
    {
        // Two fixed 8-byte fully symbolic arrays compared over a symbolically
        // *selected* common length: both the length-mismatch and content-compare
        // paths stay reachable without a symbolic-fill loop (SAT-bounded unroll).

        // Case A: equal-capacity full slices, arbitrary contents.
        let a_full: [u8; 8] = kani::any();
        let b_full: [u8; 8] = kani::any();
        assert_eq!(
            constant_time_eq(&a_full, &b_full),
            ConstantTimeEqSpec::spec_constant_time_eq_model(&a_full, &b_full),
            "constant_time_eq must agree with the element-wise spec model"
        );
        assert_eq!(constant_time_eq(&a_full, &b_full), a_full == b_full);

        // Case B: symbolically-selected prefix length (1..=8) — exercises the
        // length-mismatch early return when the selected lengths differ.
        let a_len: usize = kani::any();
        kani::assume((1..=8).contains(&a_len));
        let b_len: usize = kani::any();
        kani::assume((1..=8).contains(&b_len));
        let a: [u8; 8] = kani::any();
        let b: [u8; 8] = kani::any();

        let res = constant_time_eq(&a[..a_len], &b[..b_len]);
        assert_eq!(
            res,
            ConstantTimeEqSpec::spec_constant_time_eq_model(&a[..a_len], &b[..b_len]),
            "constant_time_eq must agree with the element-wise spec model"
        );
        assert_eq!(res, a[..a_len] == b[..b_len]);

        kani::cover!(a_full == b_full, "equal_non_empty_slices_true");
        kani::cover!(a_full != b_full, "differing_first_byte_false");
        kani::cover!(a_len != b_len, "mismatched_length_false");
    }

    #[cfg(not(kani))]
    {
        let s1 = b"cryptographic_secret_token_1234";
        let s2 = b"cryptographic_secret_token_1234";

        assert!(constant_time_eq(s1, s2));
        assert!(ConstantTimeEqSpec::verify_soundness(s1, s2));
        anti_vacuity_cover!("equal_non_empty_slices_true", constant_time_eq(s1, s2));

        let mut diff_first = *s1;
        diff_first[0] ^= 0x01;
        assert!(!constant_time_eq(s1, &diff_first));
        assert!(ConstantTimeEqSpec::verify_soundness(s1, &diff_first));
        anti_vacuity_cover!(
            "differing_first_byte_false",
            !constant_time_eq(s1, &diff_first)
        );

        let mut diff_last = *s1;
        diff_last[s1.len() - 1] ^= 0x01;
        assert!(!constant_time_eq(s1, &diff_last));
        assert!(ConstantTimeEqSpec::verify_soundness(s1, &diff_last));
        anti_vacuity_cover!(
            "differing_last_byte_false",
            !constant_time_eq(s1, &diff_last)
        );

        let mut diff_mid = *s1;
        diff_mid[s1.len() / 2] ^= 0x01;
        assert!(!constant_time_eq(s1, &diff_mid));
        assert!(ConstantTimeEqSpec::verify_soundness(s1, &diff_mid));
        anti_vacuity_cover!(
            "differing_middle_byte_false",
            !constant_time_eq(s1, &diff_mid)
        );

        let short = &s1[..16];
        assert!(!constant_time_eq(s1, short));
        assert!(ConstantTimeEqSpec::verify_soundness(s1, short));
        anti_vacuity_cover!("mismatched_length_false", !constant_time_eq(s1, short));

        assert!(constant_time_eq(b"", b""));
        assert!(ConstantTimeEqSpec::verify_soundness(b"", b""));
        anti_vacuity_cover!("empty_slices_true", constant_time_eq(b"", b""));
    }
}

/// # Proof 5: DPoP Target URI (`htu`) Normalization Invariants
///
/// **Theorem**: `normalize_htu(uri)` strictly strips query strings and fragments, lowercases
/// scheme and host, omits default ports (`http:80`, `https:443`), and preserves custom ports
/// and path casing per RFC 9449 § 4.2.
///
/// **Anti-Vacuity Cover Points**:
/// - `query_stripped_success`: Query string `?foo=bar` is stripped.
/// - `fragment_stripped_success`: Fragment `#section` is stripped.
/// - `port_443_stripped_success`: Default HTTPS port 443 is omitted.
/// - `port_80_stripped_success`: Default HTTP port 80 is omitted.
/// - `custom_port_preserved_success`: Custom port 8443 is preserved.
/// - `uppercase_host_lowercased_success`: Uppercase host `EXAMPLE.COM` is lowercased.
///
/// Note: This harness is executed in deterministic verification mode via `formal_verification_tests.rs`.
/// `#[cfg_attr(kani, kani::proof)]` is omitted here because symbolic execution of `Url::parse`
/// triggers an upstream Kani compiler ICE on `zerovec::ZeroSlice` in `icu_normalizer-2.3.0`
/// (no upstream issue has been filed). The `#[cfg(any())]` block below is unreachable
/// dead code: `any()` is never true, so the block is parsed for readability but is
/// never compiled or type-checked; the `#[cfg(not(kani))]` branch is the sole
/// authoritative verification path.
#[allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)]
pub fn proof_dpop_htu_normalization_invariants() {
    #[cfg(any())]
    {
        let port: u16 = kani::any();
        let is_https: bool = kani::any();
        let scheme = if is_https { "https" } else { "http" };
        let url = format!("{scheme}://example.com:{port}/oauth/token");
        if let Ok(res) = normalize_htu(&url) {
            let is_default_port = (is_https && port == 443) || (!is_https && port == 80);
            if is_default_port {
                assert!(!res.contains(&format!(":{port}")));
            } else if port != 0 {
                assert!(res.contains(&format!(":{port}")));
            }
            assert!(DPoPHtuFormalSpec::spec_valid_scheme(&res));
            assert!(DPoPHtuFormalSpec::spec_has_no_query(&res));
            assert!(DPoPHtuFormalSpec::spec_has_no_fragment(&res));
        }
        kani::cover!(port == 443, "port_443_stripped_success");
        kani::cover!(port == 80, "port_80_stripped_success");
        kani::cover!(port == 8443, "custom_port_preserved_success");
    }

    #[cfg(not(kani))]
    {
        if let Ok(res_query) = normalize_htu("https://example.com/oauth/token?grant_type=code") {
            assert_eq!(res_query, "https://example.com/oauth/token");
            assert!(DPoPHtuFormalSpec::spec_has_no_query(&res_query));
            anti_vacuity_cover!(
                "query_stripped_success",
                DPoPHtuFormalSpec::spec_has_no_query(&res_query)
            );
        }

        if let Ok(res_frag) = normalize_htu("https://example.com/oauth/token#frag") {
            assert_eq!(res_frag, "https://example.com/oauth/token");
            assert!(DPoPHtuFormalSpec::spec_has_no_fragment(&res_frag));
            anti_vacuity_cover!(
                "fragment_stripped_success",
                DPoPHtuFormalSpec::spec_has_no_fragment(&res_frag)
            );
        }

        if let Ok(res_443) = normalize_htu("https://example.com:443/oauth/token") {
            assert_eq!(res_443, "https://example.com/oauth/token");
            assert!(DPoPHtuFormalSpec::spec_no_default_ports(&res_443));
            anti_vacuity_cover!(
                "port_443_stripped_success",
                DPoPHtuFormalSpec::spec_no_default_ports(&res_443)
            );
        }

        if let Ok(res_80) = normalize_htu("http://example.com:80/oauth/token") {
            assert_eq!(res_80, "http://example.com/oauth/token");
            assert!(DPoPHtuFormalSpec::spec_no_default_ports(&res_80));
            anti_vacuity_cover!(
                "port_80_stripped_success",
                DPoPHtuFormalSpec::spec_no_default_ports(&res_80)
            );
        }

        if let Ok(res_custom) = normalize_htu("https://example.com:8443/oauth/token") {
            assert_eq!(res_custom, "https://example.com:8443/oauth/token");
            anti_vacuity_cover!(
                "custom_port_preserved_success",
                res_custom.contains(":8443")
            );
        }

        if let Ok(res_case) = normalize_htu("https://AUTH.EXAMPLE.COM/Token/Path") {
            assert_eq!(res_case, "https://auth.example.com/Token/Path");
            assert!(DPoPHtuFormalSpec::spec_valid_scheme(&res_case));
            anti_vacuity_cover!(
                "uppercase_host_lowercased_success",
                res_case.starts_with("https://auth.example.com")
            );
        }

        let res_ftp = normalize_htu("ftp://example.com/token");
        assert!(res_ftp.is_err());
        anti_vacuity_cover!("invalid_scheme_rejected", res_ftp.is_err());
    }
}