//! Verus proofs for bool contract types.

#[cfg(feature = "verify-verus")]
#[allow(unused_imports)]
use builtin::*;
#[cfg(feature = "verify-verus")]
#[allow(unused_imports)]
use builtin_macros::*;

verus! {

/// Verify BoolTrue contract correctness.
///
/// **Verified Properties:**
/// - Construction succeeds ⟺ value == true
#[cfg(verus)]
pub fn verify_bool_true() {
    // Proof structure for Verus
}

/// Verify BoolFalse contract correctness.
#[cfg(verus)]
pub fn verify_bool_false() {
    // Proof structure for Verus
}

/// Verify CharAlphabetic contract correctness.
///
/// **Verified Properties:**
/// - Construction succeeds ⟺ char.is_alphabetic()

proof fn verify_bool_true_construction(value: bool)
    ensures
        value == true ==> BoolTrue::new(value).is_ok(),
        value == false ==> BoolTrue::new(value).is_err(),
{
    // Boolean reasoning (trivial)
}

proof fn verify_bool_false_construction(value: bool)
    ensures
        value == false ==> BoolFalse::new(value).is_ok(),
        value == true ==> BoolFalse::new(value).is_err(),
{
}


} // verus!
