elicit_sqlx 0.10.0

Elicitation-enabled sqlx type wrappers — newtypes with JsonSchema and 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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75

//! Proof coverage tests — assert every Prop has non-empty kani/verus/creusot proofs,
//! and every wrapper type satisfies `ElicitComplete`.

use elicit_sqlx::{
    AnyColumn, AnyQueryResult, AnyRow, AnyTypeInfo, DbConnected, MigrateFragmentEmitted,
    QueryAsFragmentEmitted, QueryExecuted, QueryFragmentEmitted, QueryScalarFragmentEmitted,
    RowsFetched, SqlxError, TransactionCommitted, TransactionOpen, TransactionRolledBack,
};
use elicitation::{Elicitation as _, contracts::Prop};

macro_rules! assert_prop_proofs {
    ($($T:ty),+ $(,)?) => {
        $(
            assert!(!<$T as Prop>::kani_proof().is_empty(),
                "{} missing kani_proof", stringify!($T));
            assert!(!<$T as Prop>::verus_proof().is_empty(),
                "{} missing verus_proof", stringify!($T));
            assert!(!<$T as Prop>::creusot_proof().is_empty(),
                "{} missing creusot_proof", stringify!($T));
        )+
    };
}

#[test]
fn all_sqlx_props_have_proof_coverage() {
    assert_prop_proofs!(
        DbConnected,
        QueryExecuted,
        RowsFetched,
        TransactionOpen,
        TransactionCommitted,
        TransactionRolledBack,
        QueryFragmentEmitted,
        QueryAsFragmentEmitted,
        QueryScalarFragmentEmitted,
        MigrateFragmentEmitted,
    );
}

// ── Compile-time ElicitComplete bound checks ────────────────────────────────

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

#[test]
fn all_sqlx_wrapper_types_are_elicit_complete() {
    assert_elicit_complete::<AnyColumn>();
    assert_elicit_complete::<AnyQueryResult>();
    assert_elicit_complete::<AnyRow>();
    assert_elicit_complete::<AnyTypeInfo>();
    assert_elicit_complete::<SqlxError>();
}

#[test]
fn sqlx_wrapper_proofs_are_empty_by_design() {
    assert!(
        !AnyColumn::kani_proof().is_empty(),
        "AnyColumn kani_proof expected non-empty"
    );
    assert!(
        !AnyQueryResult::kani_proof().is_empty(),
        "AnyQueryResult kani_proof expected non-empty"
    );
    assert!(
        !AnyRow::kani_proof().is_empty(),
        "AnyRow kani_proof expected non-empty"
    );
    assert!(
        !AnyTypeInfo::kani_proof().is_empty(),
        "AnyTypeInfo kani_proof expected non-empty"
    );
    assert!(
        !SqlxError::kani_proof().is_empty(),
        "SqlxError kani_proof expected non-empty"
    );
}