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
76
77
78
79
80
//! Test that verus_proof() method works for user-defined types.
//!
//! This test verifies that the #[derive(Elicit)] macro correctly generates
//! verus_proof() methods that call field proofs, enabling compositional
//! verification.
use elicitation::{Elicit, Prompt, Select};
#[cfg(verus)]
use elicitation::Elicitation;
/// Simple struct for testing.
#[derive(Debug, Clone, Elicit, serde::Serialize, serde::Deserialize, schemars::JsonSchema)]
pub struct TestStruct {
pub name: String,
pub count: u32,
}
/// Enum with variants for testing.
#[derive(Debug, Clone, Elicit, serde::Serialize, serde::Deserialize, schemars::JsonSchema)]
pub enum TestEnum {
Simple,
WithData { value: String },
}
/// Nested struct for testing.
#[derive(Debug, Clone, Elicit, serde::Serialize, serde::Deserialize, schemars::JsonSchema)]
pub struct NestedStruct {
pub inner: TestStruct,
pub mode: TestEnum,
}
#[test]
fn test_verus_proof_trait_exists() {
// This test verifies that verus_proof() exists on user types.
// The #[cfg(verus)] gate means it won't be called in normal tests,
// but we can verify it compiles.
#[cfg(verus)]
{
TestStruct::verus_proof();
TestEnum::verus_proof();
NestedStruct::verus_proof();
}
// In non-verus builds, just verify types implement Elicitation
fn assert_elicitation<T: elicitation::Elicitation>() {}
assert_elicitation::<TestStruct>();
assert_elicitation::<TestEnum>();
assert_elicitation::<NestedStruct>();
}
#[test]
fn test_compositional_chain() {
// Verify the types compose correctly
#[cfg(verus)]
{
// Layer 1: primitives (String, u32) - handled by Rust
// Layer 2: TestStruct, TestEnum - derive generates verus_proof()
TestStruct::verus_proof();
TestEnum::verus_proof();
// Layer 3: NestedStruct - compose Layer 2 proofs
NestedStruct::verus_proof();
}
// The test passes if it compiles - the trait bounds ensure correctness
}
#[test]
fn test_contract_types_have_verus_proof() {
// Verify that contract types from elicitation also have verus_proof()
#[cfg(verus)]
{
use elicitation::verification::types::{BoolFalse, BoolTrue};
BoolTrue::verus_proof();
BoolFalse::verus_proof();
}
}