vstd_extra/resource/pcm/
count.rs

1//! This module defines a reference counting PCM with authority and tokens.
2//!
3//! Authority can produce new tokens and tracks how many are outstanding.
4//! Tokens can be returned to authority or combined.
5use vstd::pcm::PCM;
6use vstd::prelude::*;
7
8verus! {
9
10/// A reference-counting PCM with authority and tokens.
11#[verifier::ext_equal]
12pub tracked enum CountR {
13    /// Unit element with no actual meaning.
14    Unit,
15    /// Authority: tracks how many tokens have been minted
16    Auth(nat),
17    /// Token: represents one reference
18    Token,
19    /// Combination of tokens
20    Tokens(nat),
21    /// Invalid state
22    Invalid,
23}
24
25impl PCM for CountR {
26    open spec fn valid(self) -> bool {
27        self !is Invalid
28    }
29
30    open spec fn op(self, other: Self) -> Self {
31        match (self, other) {
32            // Unit is identity element
33            (CountR::Unit, x) | (x, CountR::Unit) => x,
34            // Token combinations
35            (CountR::Token, CountR::Token) => CountR::Tokens(2),
36            (CountR::Token, CountR::Tokens(n))
37            | (CountR::Tokens(n), CountR::Token) => CountR::Tokens(n + 1),
38            (CountR::Tokens(n1), CountR::Tokens(n2)) => CountR::Tokens(n1 + n2),
39            // Auth reclaims tokens: Auth(n) + Token -> Auth(n-1)
40            (CountR::Auth(n), CountR::Token) | (CountR::Token, CountR::Auth(n)) => {
41                if n > 0 {
42                    CountR::Auth((n - 1) as nat)
43                } else {
44                    CountR::Invalid
45                }
46            },
47            // Auth reclaims multiple tokens: Auth(n) + Tokens(m) -> Auth(n-m)
48            (CountR::Auth(n), CountR::Tokens(m)) | (CountR::Tokens(m), CountR::Auth(n)) => {
49                if n >= m {
50                    CountR::Auth((n - m) as nat)
51                } else {
52                    CountR::Invalid
53                }
54            },
55            // Invalid combinations (Auth + Auth)
56            _ => CountR::Invalid,
57        }
58    }
59
60    open spec fn unit() -> Self {
61        CountR::Unit
62    }
63
64    proof fn closed_under_incl(a: Self, b: Self) {
65    }
66
67    proof fn commutative(a: Self, b: Self) {
68    }
69
70    proof fn associative(a: Self, b: Self, c: Self) {
71    }
72
73    proof fn op_unit(a: Self) {
74    }
75
76    proof fn unit_valid() {
77    }
78}
79
80} // verus!
vstd_extra/resource/pcm/count.rs

vstd_extra/resource/pcm/
count.rs
