automation_structures/connectives/
counter.rs

1//! Counter connective relations for retained integer progress.
2
3use vstd::prelude::*;
4
5verus! {
6
7/// A retained count remains nonnegative.
8pub open spec fn nonnegative(value: int) -> bool {
9    0 <= value
10}
11
12/// A retained generation or occurrence count is present and nonzero.
13pub open spec fn positive(value: int) -> bool {
14    &&& nonnegative(value)
15    &&& value > 0
16}
17
18/// One occurrence advances retained progress by one.
19pub open spec fn increment(pre: int, post: int) -> bool {
20    post == pre + 1
21}
22
23/// A counted occurrence that leaves its retained count unchanged is rejected.
24pub proof fn stalled_increment_rejected(pre: int)
25    ensures !increment(pre, pre),
26{
27}
28
29/// An unselected occurrence preserves retained progress.
30pub open spec fn stutter(pre: int, post: int) -> bool {
31    post == pre
32}
33
34/// One selected occurrence decrements while every unselected occurrence stutters.
35pub open spec fn decrement_if(pre: int, post: int, selected: bool) -> bool {
36    post == pre - if selected { 1int } else { 0int }
37}
38
39/// A selected decrement has available credit and preserves nonnegativity.
40pub open spec fn guarded_decrement_if(pre: int, post: int, selected: bool) -> bool {
41    &&& nonnegative(pre)
42    &&& decrement_if(pre, post, selected)
43    &&& nonnegative(post)
44    &&& (selected ==> 0 < pre)
45}
46
47/// A retained nonnegative occurrence or generation count.
48#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
49pub struct Counter {
50    /// Retained occurrence or generation count.
51    pub value: u64,
52}
53
54impl Counter {
55    /// Mathematical view of the retained count.
56    pub open spec fn value_spec(&self) -> nat {
57        self.value as nat
58    }
59
60    /// Construct a counter at `value`.
61    pub fn new(value: u64) -> (counter: Self)
62        ensures counter.value_spec() == value as nat,
63    {
64        Self { value }
65    }
66
67    /// Current retained count.
68    pub fn value(&self) -> (value: u64)
69        ensures value as nat == self.value_spec(),
70    {
71        self.value
72    }
73
74    /// Increment unless the `u64` representation is exhausted.
75    #[must_use]
76    pub fn try_increment(&mut self) -> (accepted: bool)
77        ensures
78            accepted == (old(self).value_spec() < u64::MAX as nat),
79            accepted ==> final(self).value_spec() == old(self).value_spec() + 1,
80            !accepted ==> final(self).value_spec() == old(self).value_spec(),
81    {
82        if self.value == u64::MAX {
83            return false;
84        }
85        self.value = self.value + 1;
86        true
87    }
88
89    /// Decrement when positive.
90    #[must_use]
91    pub fn try_decrement(&mut self) -> (accepted: bool)
92        ensures
93            accepted == (old(self).value_spec() > 0),
94            accepted ==> final(self).value_spec() + 1 == old(self).value_spec(),
95            !accepted ==> final(self).value_spec() == old(self).value_spec(),
96    {
97        if self.value == 0 {
98            return false;
99        }
100        self.value = self.value - 1;
101        true
102    }
103}
104
105}
automation_structures/connectives/counter.rs

automation_structures/connectives/
counter.rs
