aex-core 2.0.0-beta.1

//! Property-based tests for `aex-core` (Sprint 3 plan task 9).
//!
//! Covers the four areas where unit-level coverage felt shakiest:
//!
//! 1. `EndpointHealth` state machine — the asymmetric debouncer
//!    (ADR-0021) has several edge cases (counter overflow, transient
//!    flaps, repeat fires of the same outcome) that unit tests only
//!    hit at fixed seeds. Proptest hammers the fold function with
//!    arbitrary outcome sequences and asserts the invariants that
//!    MUST hold no matter what the history looks like.
//! 2. `Endpoint` JSON serde — roundtrip is easy to break with a
//!    rename or a missing `#[serde(default)]`. Proptest generates
//!    arbitrary valid-ASCII kinds and URLs and asserts
//!    `from_str(to_str(x)) == x` across the search space.
//! 3. `is_within_clock_skew` — the helper is specifically advertised
//!    as overflow-safe against adversarial `i64::MIN`/`MAX`
//!    timestamps. Proptest runs it against every (i64, i64) pair
//!    proptest picks and confirms (a) no panic, (b) the symmetry
//!    and boundary invariants.
//! 4. Canonical wire-format bytes — `registration_challenge_bytes`,
//!    `transfer_intent_bytes`, `transfer_receipt_bytes`, and
//!    `rotate_key_challenge_bytes` must be deterministic and reject
//!    any field containing newline / NUL / non-ASCII. A random-input
//!    sweep guarantees we don't accept a character that would
//!    corrupt the canonical framing.

use aex_core::wire::{
    is_within_clock_skew, registration_challenge_bytes, rotate_key_challenge_bytes,
    transfer_intent_bytes, transfer_receipt_bytes, MAX_CLOCK_SKEW_SECS, MAX_NONCE_LEN,
    MIN_NONCE_LEN,
};
use aex_core::{Endpoint, EndpointHealth, HealthStatus};
use proptest::prelude::*;

// ---------- EndpointHealth state machine ----------

#[derive(Debug, Clone, Copy)]
enum Outcome {
    Success,
    Failure,
}

fn arb_outcome() -> impl Strategy<Value = Outcome> {
    prop_oneof![Just(Outcome::Success), Just(Outcome::Failure)]
}

fn apply(h: EndpointHealth, o: Outcome, now: i64) -> EndpointHealth {
    match o {
        Outcome::Success => h.on_probe_success(now),
        Outcome::Failure => h.on_probe_failure(now),
    }
}

proptest! {
    /// Counters are always bounded at the threshold — a long run of
    /// the same outcome can never wrap the u8.
    #[test]
    fn health_counters_stay_bounded(outcomes in proptest::collection::vec(arb_outcome(), 0..200)) {
        let mut h = EndpointHealth::fresh_healthy(0);
        for (i, o) in outcomes.iter().enumerate() {
            h = apply(h, *o, 1 + i as i64);
            prop_assert!(h.consecutive_fails <= EndpointHealth::FAIL_THRESHOLD);
            prop_assert!(h.consecutive_successes <= EndpointHealth::SUCCESS_THRESHOLD);
        }
    }

    /// After three consecutive failures from Healthy, the endpoint
    /// MUST be Unhealthy. This is the ADR-0021 debounce contract at
    /// the lower bound.
    #[test]
    fn three_consecutive_failures_flip_unhealthy(start_unix in any::<i64>().prop_filter(
        "avoid overflow when adding 3",
        |&v| v < i64::MAX - 3,
    )) {
        let mut h = EndpointHealth::fresh_healthy(start_unix);
        for i in 1..=3 {
            h = h.on_probe_failure(start_unix + i);
        }
        prop_assert_eq!(h.status, HealthStatus::Unhealthy);
    }

    /// Symmetric: after two consecutive successes on an Unhealthy
    /// endpoint, it heals. Builds the pre-state directly (not via
    /// three-failure fold) so a regression in the failure path
    /// doesn't mask a regression in the success path.
    #[test]
    fn two_consecutive_successes_heal_unhealthy(start_unix in any::<i64>().prop_filter(
        "avoid overflow when adding 2",
        |&v| v < i64::MAX - 2,
    )) {
        let mut h = EndpointHealth {
            status: HealthStatus::Unhealthy,
            consecutive_fails: 0,
            consecutive_successes: 0,
            last_probe_unix: Some(start_unix),
        };
        h = h.on_probe_success(start_unix + 1);
        h = h.on_probe_success(start_unix + 2);
        prop_assert_eq!(h.status, HealthStatus::Healthy);
    }

    /// A success always resets the fail counter. Specifically: no
    /// matter how many failures preceded, one success wipes
    /// `consecutive_fails` to zero so partial accrual can't stack
    /// with a future transient fault.
    #[test]
    fn success_always_resets_consecutive_fails(
        failures in 0u8..=10,
    ) {
        let mut h = EndpointHealth::fresh_healthy(0);
        for i in 0..failures {
            h = h.on_probe_failure(1 + i as i64);
        }
        h = h.on_probe_success(100);
        prop_assert_eq!(h.consecutive_fails, 0);
    }

    /// The last_probe_unix field always reflects the most recent
    /// probe. In particular it is always equal to the timestamp of
    /// the last call, not a running max.
    #[test]
    fn last_probe_unix_tracks_most_recent_call(outcomes in proptest::collection::vec(arb_outcome(), 1..20)) {
        let mut h = EndpointHealth::fresh_healthy(0);
        let final_ts = 1000 + outcomes.len() as i64;
        for (i, o) in outcomes.iter().enumerate() {
            h = apply(h, *o, 1000 + i as i64);
        }
        // The last call was at (1000 + outcomes.len() - 1), so
        // last_probe_unix should be that.
        prop_assert_eq!(
            h.last_probe_unix,
            Some(final_ts - 1),
            "last probe of a {}-outcome fold",
            outcomes.len()
        );
    }
}

// ---------- Endpoint JSON roundtrip ----------

/// Generate a string safe to embed in a wire field: printable ASCII
/// excluding the framing characters the canonical formats forbid.
/// Restricting to a-zA-Z0-9 plus a handful of punctuation matches
/// the shape of real `kind`/`url`/`nonce` values without tripping
/// the canonical-field validator.
fn arb_ascii_token(min: usize, max: usize) -> impl Strategy<Value = String> {
    let re = format!("[a-zA-Z0-9_:\\-./@]{{{},{}}}", min, max);
    proptest::string::string_regex(&re).expect("ascii token regex compiles")
}

proptest! {
    /// Any Endpoint round-trips through JSON. Forward-compat fields
    /// (`health_hint_unix`, `health`) randomly present/absent.
    #[test]
    fn endpoint_serde_roundtrip(
        kind in arb_ascii_token(1, 32),
        url in arb_ascii_token(1, 128),
        priority in any::<i32>(),
        hint in proptest::option::of(any::<i64>()),
        include_health in any::<bool>(),
        status_variant in 0u8..2,
        fails in 0u8..=EndpointHealth::FAIL_THRESHOLD,
        successes in 0u8..=EndpointHealth::SUCCESS_THRESHOLD,
        last_probe in proptest::option::of(any::<i64>()),
    ) {
        let health = if include_health {
            Some(EndpointHealth {
                status: if status_variant == 0 {
                    HealthStatus::Healthy
                } else {
                    HealthStatus::Unhealthy
                },
                consecutive_fails: fails,
                consecutive_successes: successes,
                last_probe_unix: last_probe,
            })
        } else {
            None
        };

        let ep = Endpoint {
            kind,
            url,
            priority,
            health_hint_unix: hint,
            health,
        };
        let json = serde_json::to_string(&ep).unwrap();
        let back: Endpoint = serde_json::from_str(&json).unwrap();
        prop_assert_eq!(ep, back);
    }
}

// ---------- is_within_clock_skew ----------

proptest! {
    /// The function must return for any (i64, i64) pair — no panic
    /// on `i64::MIN` / `MAX` or on arithmetic that would overflow if
    /// the implementation used plain `(now - issued_at).abs()`.
    #[test]
    fn clock_skew_never_panics(now in any::<i64>(), issued_at in any::<i64>()) {
        let _ = is_within_clock_skew(now, issued_at);
    }

    /// Inside the window: any `(now, issued_at)` with `|now - issued_at| <= 300`
    /// must return true. Generated such that subtraction can't overflow.
    #[test]
    fn inside_window_is_accepted(
        now in (i64::MIN / 2)..(i64::MAX / 2),
        delta in -MAX_CLOCK_SKEW_SECS..=MAX_CLOCK_SKEW_SECS,
    ) {
        prop_assert!(is_within_clock_skew(now, now + delta));
    }

    /// Just outside the window: `(now, now + 301)` or
    /// `(now, now - 301)` must be rejected. Again with safe
    /// subtraction space.
    #[test]
    fn outside_window_is_rejected(
        now in (i64::MIN / 2)..(i64::MAX / 2),
        delta_over in (MAX_CLOCK_SKEW_SECS + 1)..10_000,
    ) {
        prop_assert!(!is_within_clock_skew(now, now + delta_over));
        prop_assert!(!is_within_clock_skew(now, now - delta_over));
    }
}

// ---------- Canonical wire bytes ----------

fn arb_ascii_label() -> impl Strategy<Value = String> {
    proptest::string::string_regex("[a-zA-Z0-9_-]{1,64}").expect("label regex compiles")
}

fn arb_nonce() -> impl Strategy<Value = String> {
    let re = format!("[0-9a-f]{{{},{}}}", MIN_NONCE_LEN, MAX_NONCE_LEN);
    proptest::string::string_regex(&re).expect("nonce regex compiles")
}

fn arb_pubkey_hex() -> impl Strategy<Value = String> {
    proptest::string::string_regex("[0-9a-f]{64}").expect("pubkey regex compiles")
}

proptest! {
    /// Registration canonical bytes are deterministic: same inputs
    /// twice yield byte-identical output. Failure here would mean
    /// non-determinism slipped into the encoder.
    #[test]
    fn registration_bytes_deterministic(
        pub_hex in arb_pubkey_hex(),
        org in arb_ascii_label(),
        name in arb_ascii_label(),
        nonce in arb_nonce(),
        ts in any::<i64>(),
    ) {
        let a = registration_challenge_bytes(&pub_hex, &org, &name, &nonce, ts).unwrap();
        let b = registration_challenge_bytes(&pub_hex, &org, &name, &nonce, ts).unwrap();
        prop_assert_eq!(a, b);
    }

    /// Any newline inserted into any text field is rejected — this
    /// is the invariant that makes the canonical format safe against
    /// smuggling. A byte-level injection of `\n` into `org` (say)
    /// must bounce before the formatter runs.
    #[test]
    fn registration_rejects_newline_in_fields(
        org_prefix in "[a-zA-Z]{1,10}",
        org_suffix in "[a-zA-Z]{1,10}",
    ) {
        let org = format!("{org_prefix}\n{org_suffix}");
        let result = registration_challenge_bytes(
            "aa",
            &org,
            "alice",
            "0123456789abcdef0123456789abcdef",
            0,
        );
        prop_assert!(result.is_err());
    }

    /// Rotate-key canonical bytes: same inputs → same output. Also
    /// rejects old_pub == new_pub (client-level invariant we want
    /// enforced in the shared canonical helper).
    #[test]
    fn rotate_key_bytes_deterministic_and_distinct(
        agent in arb_ascii_token(5, 64),
        old_pub in arb_pubkey_hex(),
        new_pub in arb_pubkey_hex(),
        nonce in arb_nonce(),
        ts in any::<i64>(),
    ) {
        if old_pub == new_pub {
            let err = rotate_key_challenge_bytes(&agent, &old_pub, &new_pub, &nonce, ts);
            prop_assert!(err.is_err());
        } else {
            let a = rotate_key_challenge_bytes(&agent, &old_pub, &new_pub, &nonce, ts).unwrap();
            let b = rotate_key_challenge_bytes(&agent, &old_pub, &new_pub, &nonce, ts).unwrap();
            prop_assert_eq!(a, b);
        }
    }

    /// Transfer intent: same inputs → same output for every legal
    /// combination of optional/empty fields.
    #[test]
    fn transfer_intent_bytes_deterministic(
        sender in arb_ascii_token(5, 64),
        recipient in arb_ascii_token(1, 128),
        size in any::<u64>(),
        mime in "[a-zA-Z0-9/_.-]{0,64}",
        filename in "[a-zA-Z0-9_.-]{0,64}",
        nonce in arb_nonce(),
        ts in any::<i64>(),
    ) {
        let a = transfer_intent_bytes(&sender, &recipient, size, &mime, &filename, &nonce, ts).unwrap();
        let b = transfer_intent_bytes(&sender, &recipient, size, &mime, &filename, &nonce, ts).unwrap();
        prop_assert_eq!(a, b);
    }

    /// Transfer receipt: same inputs → same output; unknown action
    /// strings are rejected.
    #[test]
    fn transfer_receipt_rejects_unknown_action(
        recipient in arb_ascii_token(5, 64),
        transfer in arb_ascii_token(3, 64),
        action in "[a-zA-Z]{3,10}".prop_filter(
            "skip valid actions",
            |s| !["download", "ack", "inbox", "request_ticket"].contains(&s.as_str()),
        ),
        nonce in arb_nonce(),
        ts in any::<i64>(),
    ) {
        let result = transfer_receipt_bytes(&recipient, &transfer, &action, &nonce, ts);
        prop_assert!(result.is_err());
    }
}