elicitation_kani 0.11.1

//! Kani proofs for the serde deserialization boundary.
//!
//! # What these proofs verify
//!
//! The serde bridge (Phase A) adds `Deserialize` impls that call the validated
//! constructor `Type::new(v)` under the hood. These harnesses prove the
//! **consistency invariant**:
//!
//! > `serde_json::from_value(v)` succeeds **iff** `Type::new(v)` succeeds.
//!
//! In other words: deserialization never creates a value that the constructor
//! would reject, and deserialization never rejects a value that the constructor
//! would accept.
//!
//! This is critical because it means:
//! 1. Agents cannot bypass validation by crafting JSON payloads.
//! 2. The serde bridge does not silently drop or corrupt valid inputs.
//!
//! # Proof strategy
//!
//! For integer types we can use `kani::any::<T>()` for full symbolic coverage.
//! For floats we cover boundary patterns concretely (Kani's float support is
//! limited for relational comparisons).
//! For URLs we test concrete representative strings.

// ============================================================================
// Integer serde boundary proofs
// ============================================================================

use elicitation::{
    I8NonNegative, I8NonZero, I8Positive, I8Range, I16NonNegative, I16NonZero, I16Positive,
    U8NonZero, U8Positive, U16NonZero, U16Positive,
};

/// Prove: I8Positive serde and constructor agree on every symbolic i8.
#[kani::proof]
fn serde_i8_positive_consistency() {
    let v: i8 = kani::any();
    let new_result = I8Positive::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<I8Positive, _> = serde_json::from_value(json);
    // They must agree: both succeed or both fail
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

/// Prove: if I8Positive deserialization succeeds, the invariant (> 0) holds.
#[kani::proof]
fn serde_i8_positive_invariant() {
    let v: i8 = kani::any();
    let json = serde_json::Value::Number(v.into());
    if let Ok(pos) = serde_json::from_value::<I8Positive>(json) {
        assert!(
            pos.get() > 0,
            "I8Positive invariant must hold after deserialization"
        );
    }
}

/// Prove: I8NonNegative serde and constructor agree on every symbolic i8.
#[kani::proof]
fn serde_i8_non_negative_consistency() {
    let v: i8 = kani::any();
    let new_result = I8NonNegative::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<I8NonNegative, _> = serde_json::from_value(json);
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

/// Prove: if I8NonNegative deserialization succeeds, invariant (>= 0) holds.
#[kani::proof]
fn serde_i8_non_negative_invariant() {
    let v: i8 = kani::any();
    let json = serde_json::Value::Number(v.into());
    if let Ok(nn) = serde_json::from_value::<I8NonNegative>(json) {
        assert!(
            nn.get() >= 0,
            "I8NonNegative invariant must hold after deserialization"
        );
    }
}

/// Prove: I8NonZero serde and constructor agree on every symbolic i8.
#[kani::proof]
fn serde_i8_non_zero_consistency() {
    let v: i8 = kani::any();
    let new_result = I8NonZero::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<I8NonZero, _> = serde_json::from_value(json);
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

/// Prove: if I8NonZero deserialization succeeds, invariant (!= 0) holds.
#[kani::proof]
fn serde_i8_non_zero_invariant() {
    let v: i8 = kani::any();
    let json = serde_json::Value::Number(v.into());
    if let Ok(nz) = serde_json::from_value::<I8NonZero>(json) {
        assert!(
            nz.get() != 0,
            "I8NonZero invariant must hold after deserialization"
        );
    }
}

/// Prove: I16Positive serde and constructor agree on every symbolic i16.
#[kani::proof]
fn serde_i16_positive_consistency() {
    let v: i16 = kani::any();
    let new_result = I16Positive::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<I16Positive, _> = serde_json::from_value(json);
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

/// Prove: I16NonNegative serde and constructor agree.
#[kani::proof]
fn serde_i16_non_negative_consistency() {
    let v: i16 = kani::any();
    let new_result = I16NonNegative::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<I16NonNegative, _> = serde_json::from_value(json);
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

/// Prove: I16NonZero serde and constructor agree.
#[kani::proof]
fn serde_i16_non_zero_consistency() {
    let v: i16 = kani::any();
    let new_result = I16NonZero::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<I16NonZero, _> = serde_json::from_value(json);
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

/// Prove: U8Positive serde and constructor agree on every symbolic u8.
#[kani::proof]
fn serde_u8_positive_consistency() {
    let v: u8 = kani::any();
    let new_result = U8Positive::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<U8Positive, _> = serde_json::from_value(json);
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

/// Prove: U8NonZero serde and constructor agree on every symbolic u8.
#[kani::proof]
fn serde_u8_non_zero_consistency() {
    let v: u8 = kani::any();
    let new_result = U8NonZero::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<U8NonZero, _> = serde_json::from_value(json);
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

/// Prove: U16Positive serde and constructor agree on every symbolic u16.
#[kani::proof]
fn serde_u16_positive_consistency() {
    let v: u16 = kani::any();
    let new_result = U16Positive::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<U16Positive, _> = serde_json::from_value(json);
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

/// Prove: U16NonZero serde and constructor agree on every symbolic u16.
#[kani::proof]
fn serde_u16_non_zero_consistency() {
    let v: u16 = kani::any();
    let new_result = U16NonZero::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<U16NonZero, _> = serde_json::from_value(json);
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

// ============================================================================
// Integer range serde boundary proofs
// ============================================================================

/// Prove: I8Range<0,100> serde and constructor agree on every symbolic i8.
#[kani::proof]
fn serde_i8_range_consistency() {
    let v: i8 = kani::any();
    let new_result = I8Range::<0, 100>::new(v);
    let json = serde_json::Value::Number(v.into());
    let serde_result: Result<I8Range<0, 100>, _> = serde_json::from_value(json);
    assert_eq!(new_result.is_ok(), serde_result.is_ok());
}

/// Prove: if I8Range<0,100> deserialization succeeds, value is in [0,100].
#[kani::proof]
fn serde_i8_range_invariant() {
    let v: i8 = kani::any();
    let json = serde_json::Value::Number(v.into());
    if let Ok(r) = serde_json::from_value::<I8Range<0, 100>>(json) {
        assert!(
            r.get() >= 0 && r.get() <= 100,
            "I8Range<0,100> invariant must hold after deserialization"
        );
    }
}

// ============================================================================
// Float serde boundary proofs (concrete — Kani float comparison limitations)
// ============================================================================

use elicitation::{F64Finite, F64NonNegative, F64Positive};

/// Prove: F64Positive serde invariant with concrete boundary values.
///
/// Uses concrete inputs instead of kani::any::<f64>() to avoid
/// Kani's symbolic float limitations with relational comparisons.
#[kani::proof]
fn serde_f64_positive_boundary_values() {
    // Positive: should succeed
    for v in [1.0_f64, 0.001, f64::MAX, f64::MIN_POSITIVE] {
        let json = serde_json::json!(v);
        assert!(
            serde_json::from_value::<F64Positive>(json).is_ok(),
            "F64Positive should accept positive value {v}"
        );
    }
    // Non-positive: should fail
    for v in [0.0_f64, -1.0, -f64::MIN_POSITIVE] {
        let json = serde_json::json!(v);
        assert!(
            serde_json::from_value::<F64Positive>(json).is_err(),
            "F64Positive should reject non-positive value {v}"
        );
    }
}

/// Prove: F64NonNegative serde invariant with concrete boundary values.
#[kani::proof]
fn serde_f64_non_negative_boundary_values() {
    // Non-negative: should succeed
    for v in [0.0_f64, 1.0, f64::MAX] {
        let json = serde_json::json!(v);
        assert!(
            serde_json::from_value::<F64NonNegative>(json).is_ok(),
            "F64NonNegative should accept {v}"
        );
    }
    // Negative: should fail
    for v in [-0.001_f64, -1.0, f64::NEG_INFINITY] {
        let json = serde_json::json!(v);
        // NEG_INFINITY is not a valid JSON number, so it becomes null
        // only test finite negatives as strict failures
        if v.is_finite() {
            assert!(
                serde_json::from_value::<F64NonNegative>(json).is_err(),
                "F64NonNegative should reject {v}"
            );
        }
    }
}

/// Prove: F64Finite rejects NaN and infinity representations.
///
/// JSON has no NaN/Infinity literals, but the constructor is the proof site.
#[kani::proof]
fn serde_f64_finite_accepts_finite() {
    for v in [0.0_f64, 1.0, -1.0, f64::MAX, f64::MIN] {
        let json = serde_json::json!(v);
        assert!(
            serde_json::from_value::<F64Finite>(json).is_ok(),
            "F64Finite should accept finite value {v}"
        );
    }
}

// ============================================================================
// String serde boundary proofs
// ============================================================================

use elicitation::StringNonEmpty;

/// Prove: StringNonEmpty rejects empty string, accepts non-empty.
#[kani::proof]
fn serde_string_non_empty_boundary() {
    // Should fail
    let json = serde_json::json!("");
    assert!(
        serde_json::from_value::<StringNonEmpty<4096>>(json).is_err(),
        "StringNonEmpty should reject empty string"
    );

    // Should succeed
    let json = serde_json::json!("hello");
    assert!(
        serde_json::from_value::<StringNonEmpty<4096>>(json).is_ok(),
        "StringNonEmpty should accept non-empty string"
    );

    // Single char — boundary
    let json = serde_json::json!("x");
    assert!(
        serde_json::from_value::<StringNonEmpty<4096>>(json).is_ok(),
        "StringNonEmpty should accept single-char string"
    );
}

// ============================================================================
// URL serde boundary proofs (concrete strings — URL parsing is opaque to Kani)
// ============================================================================

#[cfg(feature = "url")]
use elicitation::{UrlHttp, UrlHttps, UrlValid, UrlWithHost};

/// Prove: UrlHttps accepts HTTPS, rejects HTTP and invalid.
#[cfg(feature = "url")]
#[kani::proof]
fn serde_url_https_boundary() {
    // Valid HTTPS — should succeed
    let json = serde_json::json!("https://example.com");
    assert!(
        serde_json::from_value::<UrlHttps>(json).is_ok(),
        "UrlHttps should accept https://example.com"
    );

    // HTTP — should fail (not HTTPS)
    let json = serde_json::json!("http://example.com");
    assert!(
        serde_json::from_value::<UrlHttps>(json).is_err(),
        "UrlHttps should reject http://example.com"
    );

    // Invalid URL — should fail
    let json = serde_json::json!("not-a-url");
    assert!(
        serde_json::from_value::<UrlHttps>(json).is_err(),
        "UrlHttps should reject not-a-url"
    );

    // FTP — should fail
    let json = serde_json::json!("ftp://files.example.com");
    assert!(
        serde_json::from_value::<UrlHttps>(json).is_err(),
        "UrlHttps should reject ftp://files.example.com"
    );
}

/// Prove: UrlHttps serde is consistent with UrlHttps::new.
#[cfg(feature = "url")]
#[kani::proof]
fn serde_url_https_constructor_consistency() {
    // For each concrete test string, serde and constructor must agree
    let cases: &[&str] = &[
        "https://example.com",
        "http://example.com",
        "https://",
        "not-a-url",
        "ftp://files.example.com",
        "https://user:pass@host.example.com/path?q=1#frag",
    ];
    for s in cases {
        let new_result = UrlHttps::new(s);
        let json = serde_json::json!(s);
        let serde_result: Result<UrlHttps, _> = serde_json::from_value(json);
        assert_eq!(
            new_result.is_ok(),
            serde_result.is_ok(),
            "serde and constructor must agree for '{s}'"
        );
    }
}

/// Prove: UrlHttp accepts HTTP, rejects HTTPS.
#[cfg(feature = "url")]
#[kani::proof]
fn serde_url_http_boundary() {
    let json = serde_json::json!("http://example.com");
    assert!(serde_json::from_value::<UrlHttp>(json).is_ok());

    let json = serde_json::json!("https://example.com");
    assert!(serde_json::from_value::<UrlHttp>(json).is_err());
}

/// Prove: UrlValid accepts any valid URL, rejects invalid.
#[cfg(feature = "url")]
#[kani::proof]
fn serde_url_valid_boundary() {
    // Valid URLs of various schemes
    for s in [
        "https://example.com",
        "http://example.com",
        "ftp://files.example.com",
    ] {
        let json = serde_json::json!(s);
        assert!(
            serde_json::from_value::<UrlValid>(json).is_ok(),
            "UrlValid should accept '{s}'"
        );
    }

    // Invalid
    let json = serde_json::json!("not a url");
    assert!(
        serde_json::from_value::<UrlValid>(json).is_err(),
        "UrlValid should reject 'not a url'"
    );
}

/// Prove: UrlWithHost requires a host component.
#[cfg(feature = "url")]
#[kani::proof]
fn serde_url_with_host_boundary() {
    let json = serde_json::json!("https://example.com");
    assert!(serde_json::from_value::<UrlWithHost>(json).is_ok());
}

// ============================================================================
// Round-trip proofs: serialize then deserialize preserves value
// ============================================================================

/// Prove: I8Positive round-trip preserves the value.
#[kani::proof]
fn serde_i8_positive_round_trip() {
    let v: i8 = kani::any();
    if let Ok(pos) = I8Positive::new(v) {
        let json = serde_json::to_value(&pos).unwrap();
        let pos2: I8Positive = serde_json::from_value(json).unwrap();
        assert_eq!(pos.get(), pos2.get(), "Round-trip must preserve value");
    }
}

/// Prove: I8Range<0,100> round-trip preserves the value.
#[kani::proof]
fn serde_i8_range_round_trip() {
    let v: i8 = kani::any();
    if let Ok(r) = I8Range::<0, 100>::new(v) {
        let json = serde_json::to_value(&r).unwrap();
        let r2: I8Range<0, 100> = serde_json::from_value(json).unwrap();
        assert_eq!(r.get(), r2.get(), "Round-trip must preserve value");
    }
}