//! Class-condition byte predicates (`GNURUST.CLASS.1`): `IF data-item IS NUMERIC / ALPHABETIC /
//! ALPHABETIC-UPPER / ALPHABETIC-LOWER` over an **alphanumeric** (`PIC X`) field, proven byte-identical
//! to cobc.
//!
//! **Doctrine.** These are pure byte predicates over the raw field bytes — the ubiquitous legacy
//! validation idiom (`IF CUST-NO IS NUMERIC`). cobc's admitted rules (diagnosed from the oracle):
//! - **NUMERIC**: every byte is an ASCII digit `0x30..=0x39` (a space, sign, or letter ⇒ not numeric);
//! - **ALPHABETIC**: every byte is an ASCII letter (`A-Z`/`a-z`) or space;
//! - **ALPHABETIC-UPPER**: every byte is `A-Z` or space;
//! - **ALPHABETIC-LOWER**: every byte is `a-z` or space.
//!
//! **Not modelled:** the signed-numeric (overpunch) class test on a `PIC S9` field, user-defined `CLASS`
//! names, national/UTF-8/DBCS classes, and the locale collating sequence.

/// `IS NUMERIC` for an alphanumeric field: non-empty and every byte an ASCII digit.
pub fn is_numeric(bytes: &[u8]) -> bool {
    !bytes.is_empty() && bytes.iter().all(u8::is_ascii_digit)
}

/// `IS NUMERIC` for a signed DISPLAY field with the **default trailing sign** (`PIC S9(n)`): every byte but
/// the last is an ASCII digit, and the last byte is a digit (`0x30..=0x39`, positive) or an ASCII negative
/// overpunch (`0x70..=0x79`, `p`..`y`). cobc rejects the `{`/`A-I`/`}`/`J-R` overpunch forms here, and any
/// space/letter/punctuation.
pub fn is_numeric_signed_trailing(bytes: &[u8]) -> bool {
    match bytes.split_last() {
        Some((last, rest)) => {
            rest.iter().all(u8::is_ascii_digit) && (last.is_ascii_digit() || (0x70..=0x79).contains(last))
        }
        None => false,
    }
}

/// `IS NUMERIC` for `SIGN LEADING SEPARATE` (`+`/`-` byte, then digits).
pub fn is_numeric_sign_leading_separate(bytes: &[u8]) -> bool {
    match bytes.split_first() {
        Some((f, rest)) => (*f == b'+' || *f == b'-') && !rest.is_empty() && rest.iter().all(u8::is_ascii_digit),
        None => false,
    }
}

/// `IS NUMERIC` for `SIGN TRAILING SEPARATE` (digits, then a `+`/`-` byte).
pub fn is_numeric_sign_trailing_separate(bytes: &[u8]) -> bool {
    match bytes.split_last() {
        Some((l, rest)) => (*l == b'+' || *l == b'-') && !rest.is_empty() && rest.iter().all(u8::is_ascii_digit),
        None => false,
    }
}

/// `IS NUMERIC` for `SIGN LEADING` (overpunch on the FIRST digit: `0x30..=0x39` or `0x70..=0x79`).
pub fn is_numeric_sign_leading(bytes: &[u8]) -> bool {
    match bytes.split_first() {
        Some((f, rest)) => (f.is_ascii_digit() || (0x70..=0x79).contains(f)) && rest.iter().all(u8::is_ascii_digit),
        None => false,
    }
}

/// `IS ALPHABETIC`: every byte an ASCII letter or space.
pub fn is_alphabetic(bytes: &[u8]) -> bool {
    bytes.iter().all(|b| b.is_ascii_alphabetic() || *b == b' ')
}

/// `IS ALPHABETIC-UPPER`: every byte `A-Z` or space.
pub fn is_alphabetic_upper(bytes: &[u8]) -> bool {
    bytes.iter().all(|b| b.is_ascii_uppercase() || *b == b' ')
}

/// `IS ALPHABETIC-LOWER`: every byte `a-z` or space.
pub fn is_alphabetic_lower(bytes: &[u8]) -> bool {
    bytes.iter().all(|b| b.is_ascii_lowercase() || *b == b' ')
}

/// Fuzz entry (`GNURUST.CLASS.1`): the predicates are total over any bytes — never panic.
pub fn __fuzz_class(data: &[u8]) {
    let _ = (
        is_numeric(data),
        is_numeric_signed_trailing(data),
        is_numeric_sign_leading_separate(data),
        is_numeric_sign_trailing_separate(data),
        is_numeric_sign_leading(data),
        is_alphabetic(data),
        is_alphabetic_upper(data),
        is_alphabetic_lower(data),
    );
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn class_conditions_match_the_oracle() {
        assert!(is_numeric(b"0012"));
        assert!(!is_numeric(b" 12 ")); // spaces are not numeric
        assert!(!is_numeric(b"12AB"));
        assert!(!is_numeric(b"")); // empty is not numeric
        assert!(is_alphabetic(b"ABCD"));
        assert!(!is_alphabetic(b"AB12"));
        assert!(is_alphabetic(b"AB  ")); // spaces are alphabetic
        assert!(is_alphabetic(b"abcd"));
        assert!(is_alphabetic_upper(b"ABCD"));
        assert!(!is_alphabetic_upper(b"abcd"));
        assert!(is_alphabetic_lower(b"abcd"));
        assert!(!is_alphabetic_lower(b"ABCD"));
        assert!(is_alphabetic_upper(b"AB  ") && is_alphabetic_lower(b"ab  "));
        // signed-numeric (trailing overpunch) on a PIC S9 field:
        assert!(is_numeric_signed_trailing(b"012")); // positive plain digit
        assert!(is_numeric_signed_trailing(b"01r")); // 'r'=0x72 negative overpunch (-2)
        assert!(is_numeric_signed_trailing(b"01p") && is_numeric_signed_trailing(b"01y")); // p..y
        assert!(!is_numeric_signed_trailing(b"01A")); // 0x41 NOT accepted
        assert!(!is_numeric_signed_trailing(b"01z")); // 0x7a out of p..y
        assert!(!is_numeric_signed_trailing(b"01 ")); // space
        // sign separate + leading overpunch (observed):
        assert!(is_numeric_sign_leading_separate(b"+123") && is_numeric_sign_leading_separate(b"-123"));
        assert!(!is_numeric_sign_leading_separate(b" 123")); // space sign
        assert!(is_numeric_sign_trailing_separate(b"123+") && is_numeric_sign_trailing_separate(b"123-"));
        assert!(!is_numeric_sign_trailing_separate(b"123 "));
        assert!(is_numeric_sign_leading(b"123") && is_numeric_sign_leading(b"q23")); // q=0x71 (-1) leads
        assert!(!is_numeric_sign_leading(b"A23")); // 0x41 not accepted
    }
}

#[cfg(kani)]
mod kani_proofs {
    use super::*;
    // KANIFOR: GNURUST.CLASS.1
    /// the class predicates are total over symbolic bytes (never panic).
    #[kani::proof]
    #[kani::unwind(5)]
    fn class_predicates_are_total() {
        let bytes: [u8; 4] = kani::any();
        let _ = is_numeric(&bytes);
        let _ = is_numeric_signed_trailing(&bytes);
        let _ = is_numeric_sign_leading_separate(&bytes);
        let _ = is_numeric_sign_trailing_separate(&bytes);
        let _ = is_numeric_sign_leading(&bytes);
        let _ = is_alphabetic(&bytes);
        let _ = is_alphabetic_upper(&bytes);
        let _ = is_alphabetic_lower(&bytes);
    }
}
