automation-structures 0.1.1

Reusable, formally specified building blocks for composing automation systems.
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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120

//! Canonical Accumulator connective relations for partial results carried between steps.

use vstd::prelude::*;

verus! {

/// The accumulated prefix and pending suffix reconstruct the complete value sequence.
pub open spec fn carries<T>(
    complete: Seq<T>,
    accumulated: Seq<T>,
    pending: Seq<T>,
) -> bool {
    complete == accumulated.add(pending)
}

/// Segments that do not reconstruct the complete sequence are not a valid accumulation.
pub proof fn mismatched_partition_rejected<T>(
    complete: Seq<T>,
    accumulated: Seq<T>,
    pending: Seq<T>,
)
    requires complete != accumulated.add(pending),
    ensures !carries(complete, accumulated, pending),
{
}

/// One step appends a value to the carried partial result.
pub open spec fn append<T>(before: Seq<T>, after: Seq<T>, value: T) -> bool {
    after == before.push(value)
}

/// An unselected step preserves the carried partial result.
pub open spec fn stutter<T>(before: Seq<T>, after: Seq<T>) -> bool {
    after == before
}

/// Appending to a pending suffix preserves its accumulated prefix.
pub proof fn append_pending<T>(prefix: Seq<T>, pending: Seq<T>, value: T)
    ensures
        prefix.add(pending).push(value) == prefix.add(pending.push(value)),
{
    Seq::push_distributes_over_add(prefix, pending, value);
}

/// Moving one pending head into the accumulator preserves the reconstructed complete sequence.
pub proof fn consume_pending_head<T>(accumulated: Seq<T>, pending: Seq<T>)
    requires pending.len() > 0,
    ensures
        accumulated.add(pending)
            == accumulated.push(pending[0]).add(pending.skip(1)),
{
    assert(pending =~= seq![pending[0]].add(pending.skip(1)));
    assert(accumulated.push(pending[0]) =~= accumulated.add(seq![pending[0]]));
    assert(accumulated.add(pending)
        =~= accumulated.push(pending[0]).add(pending.skip(1)));
}

/// Moving one head between adjacent pending segments preserves the reconstructed sequence.
pub proof fn move_pending_head<T>(
    prefix: Seq<T>,
    destination: Seq<T>,
    source: Seq<T>,
)
    requires source.len() > 0,
    ensures
        prefix.add(destination).add(source)
            == prefix.add(destination.push(source[0])).add(source.skip(1)),
{
    assert(source =~= seq![source[0]].add(source.skip(1)));
    assert(destination.push(source[0]) =~= destination.add(seq![source[0]]));
    assert(prefix.add(destination).add(source)
        =~= prefix.add(destination.push(source[0])).add(source.skip(1)));
}

/// Moving one head between adjacent pending segments preserves any pending prefix and suffix.
pub proof fn move_pending_head_with_suffix<T>(
    prefix: Seq<T>,
    destination: Seq<T>,
    source: Seq<T>,
    suffix: Seq<T>,
)
    requires source.len() > 0,
    ensures
        prefix.add(destination).add(source).add(suffix)
            == prefix
                .add(destination.push(source[0]))
                .add(source.skip(1))
                .add(suffix),
{
    move_pending_head(prefix, destination, source);
}

/// Folding the first pending segment head preserves any later pending suffix.
pub proof fn consume_pending_head_with_suffix<T>(
    accumulated: Seq<T>,
    source: Seq<T>,
    suffix: Seq<T>,
)
    requires source.len() > 0,
    ensures
        accumulated.add(source.add(suffix))
            == accumulated.push(source[0]).add(source.skip(1).add(suffix)),
{
    consume_pending_head(accumulated, source);
    assert(accumulated.add(source.add(suffix))
        =~= accumulated.add(source).add(suffix));
    assert(accumulated.push(source[0]).add(source.skip(1).add(suffix))
        =~= accumulated.push(source[0]).add(source.skip(1)).add(suffix));
}

/// Skipping a present head commutes with appending a later pending suffix.
pub proof fn skip_pending_head_with_suffix<T>(source: Seq<T>, suffix: Seq<T>)
    requires source.len() > 0,
    ensures
        source.add(suffix).skip(1) == source.skip(1).add(suffix),
{
    assert(source.add(suffix).skip(1) =~= source.skip(1).add(suffix));
}

}