elicit_jiff 0.11.1

Elicitation-enabled jiff datetime wrappers with MCP reflect methods
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

//! Proof coverage tests for `elicit_jiff`.
//!
//! Verifies that every wrapper type satisfies the [`ElicitComplete`] supertrait
//! at compile time. Proof methods are intentionally empty for external wrapper
//! types.
//!
//! [`ElicitComplete`]: elicitation::ElicitComplete

use elicitation::Elicitation as _;

fn assert_elicit_complete<T: elicitation::ElicitComplete>() {}

#[test]
fn all_jiff_types_are_elicit_complete() {
    assert_elicit_complete::<elicit_jiff::Timestamp>();
    assert_elicit_complete::<elicit_jiff::Zoned>();
}

#[test]
fn jiff_wrapper_proofs_are_empty_by_design() {
    assert!(
        !elicit_jiff::Timestamp::kani_proof().is_empty(),
        "Timestamp kani_proof expected non-empty"
    );
    assert!(
        !elicit_jiff::Zoned::kani_proof().is_empty(),
        "Zoned kani_proof expected non-empty"
    );
}