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

//! `VerifiedWorkflow` validation tests for elicit_sqlx propositions.

use elicit_sqlx::{
    DbConnected, MigrateFragmentEmitted, QueryAsFragmentEmitted, QueryExecuted,
    QueryFragmentEmitted, QueryScalarFragmentEmitted, RowsFetched, TransactionCommitted,
    TransactionOpen, TransactionRolledBack,
};
use elicitation::VerifiedWorkflow;
use elicitation::contracts::And;

#[track_caller]
fn assert_verified<T: VerifiedWorkflow>(label: &str) {
    assert!(T::validate_proofs_non_empty(), "{label}: proofs are empty");
}

#[test]
fn sqlx_workflow_props_non_empty() {
    assert_verified::<DbConnected>("DbConnected");
    assert_verified::<QueryExecuted>("QueryExecuted");
    assert_verified::<RowsFetched>("RowsFetched");
    assert_verified::<TransactionOpen>("TransactionOpen");
    assert_verified::<TransactionCommitted>("TransactionCommitted");
    assert_verified::<TransactionRolledBack>("TransactionRolledBack");
}

#[test]
fn sqlx_frag_props_non_empty() {
    assert_verified::<QueryFragmentEmitted>("QueryFragmentEmitted");
    assert_verified::<QueryAsFragmentEmitted>("QueryAsFragmentEmitted");
    assert_verified::<QueryScalarFragmentEmitted>("QueryScalarFragmentEmitted");
    assert_verified::<MigrateFragmentEmitted>("MigrateFragmentEmitted");
}

#[test]
fn sqlx_and_contains_constituents() {
    type ConnQuery = And<DbConnected, QueryExecuted>;
    type ConnRows = And<DbConnected, RowsFetched>;
    type OpenCommit = And<TransactionOpen, TransactionCommitted>;

    assert!(ConnQuery::kani_proof_contains::<DbConnected>());
    assert!(ConnQuery::kani_proof_contains::<QueryExecuted>());
    assert!(ConnRows::kani_proof_contains::<RowsFetched>());
    assert!(OpenCommit::kani_proof_contains::<TransactionOpen>());
    assert!(OpenCommit::kani_proof_contains::<TransactionCommitted>());
}