whitaker-common 0.2.6

Internal common utilities for Whitaker lints
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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

//! Bounded model-checking harnesses for `propagate_labels`.

use crate::decomposition_advice::minimal_feature_vector;

use super::super::propagate_labels_report;
use super::shared::bounded_iteration_count;

const NODE_COUNT: usize = 3;

fn symbolic_vectors() -> [crate::decomposition_advice::vector::MethodFeatureVector; NODE_COUNT] {
    [
        minimal_feature_vector("gamma"),
        minimal_feature_vector("alpha"),
        minimal_feature_vector("beta"),
    ]
}

fn symbolic_adjacency() -> [Vec<(usize, u64)>; NODE_COUNT] {
    let mut node_0 = Vec::new();
    let mut node_1 = Vec::new();
    let mut node_2 = Vec::new();

    add_symbolic_edge(&mut node_0, 0, &mut node_1, 1);
    add_symbolic_edge(&mut node_0, 0, &mut node_2, 2);
    add_symbolic_edge(&mut node_1, 1, &mut node_2, 2);

    node_0.sort_by_key(|(neighbour, _)| *neighbour);
    node_1.sort_by_key(|(neighbour, _)| *neighbour);
    node_2.sort_by_key(|(neighbour, _)| *neighbour);

    [node_0, node_1, node_2]
}

fn add_symbolic_edge(
    left: &mut Vec<(usize, u64)>,
    left_index: usize,
    right: &mut Vec<(usize, u64)>,
    right_index: usize,
) {
    let is_active: bool = kani::any();
    if !is_active {
        return;
    }

    let weight: u64 = kani::any();
    kani::assume(weight > 0);
    left.push((right_index, weight));
    right.push((left_index, weight));
}

/// Verifies that propagation returns exactly one label per input vector.
#[kani::proof]
#[kani::unwind(10)]
fn verify_propagate_labels_returns_vector_per_input() {
    let adjacency = symbolic_adjacency();
    let vectors = symbolic_vectors();

    let report = propagate_labels_report(&vectors, &adjacency, bounded_iteration_count());

    assert_eq!(report.labels.len(), NODE_COUNT);
}

/// Verifies that every propagated label remains a valid node index.
#[kani::proof]
#[kani::unwind(10)]
fn verify_propagate_labels_preserves_label_indices() {
    let adjacency = symbolic_adjacency();
    let vectors = symbolic_vectors();

    let report = propagate_labels_report(&vectors, &adjacency, bounded_iteration_count());

    for &label in &report.labels {
        assert!(label < NODE_COUNT);
    }
}

/// Verifies that zero iterations keep the initial self labels unchanged.
#[kani::proof]
#[kani::unwind(10)]
fn verify_propagate_labels_zero_iterations_keeps_initial_labels() {
    let adjacency = symbolic_adjacency();
    let vectors = symbolic_vectors();

    let report = propagate_labels_report(&vectors, &adjacency, 0);

    assert_eq!(report.iteration_count, 0);
    for (index, &label) in report.labels.iter().enumerate() {
        assert_eq!(label, index);
    }
}

/// Verifies that the reported iteration count never exceeds the supplied
/// bound.
#[kani::proof]
#[kani::unwind(10)]
fn verify_propagate_labels_bounded_return_for_any_max_iterations() {
    let adjacency = symbolic_adjacency();
    let vectors = symbolic_vectors();
    let max_iterations = bounded_iteration_count();

    let report = propagate_labels_report(&vectors, &adjacency, max_iterations);

    assert_eq!(report.labels.len(), NODE_COUNT);
    assert!(report.iteration_count <= max_iterations);
}