vstd_extra/resource/pcm/
frac.rs

1//! This module defines the real-based fractional permissions PCM.
2//!
3//! Unlike the [`FracGhost`](https://verus-lang.github.io/verus/verusdoc/vstd/tokens/frac/struct.FracGhost.html) in vstd,
4//! which requires a compile-time constant TOTTL to define integer-based fractions,
5//! we model fractions as real numbers `q : real` in (0, 1] like Iris, where 1.0 is full
6//! ownership, which allows arbitrary splitting of fractions at runtime.
7//!
8//! For Iris definition, see:
9//! <https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/frac.v>
10
11use vstd::arithmetic::*;
12use vstd::pcm::PCM;
13use vstd::prelude::*;
14
15verus! {
16
17/// Fractional PCM
18#[verifier::ext_equal]
19pub tracked enum FracR<T> {
20    Unit,
21    Frac(real, T),
22    Invalid,
23}
24
25impl<T: PartialEq> PCM for FracR<T> {
26    open spec fn valid(self) -> bool {
27        match self {
28            FracR::Unit => true,
29            FracR::Frac(q, _) => 0.0real < q && q <= 1.0real,
30            FracR::Invalid => false,
31        }
32    }
33
34    /// Two Frac combine iff they agree on the value and the sum of fractions does not exceed 1.0. This follows the original Iris design.
35    open spec fn op(self, other: Self) -> Self {
36        match (self, other) {
37            (FracR::Unit, x) => x,
38            (x, FracR::Unit) => x,
39            (FracR::Frac(q1, a1), FracR::Frac(q2, a2)) => {
40                if a1 == a2 && 0.0real < q1 && 0.0real < q2 && q1 + q2 <= 1.0real {
41                    FracR::Frac(q1 + q2, a1)
42                } else {
43                    FracR::Invalid
44                }
45            }
46            _ => FracR::Invalid,
47        }
48    }
49
50    open spec fn unit() -> Self { FracR::Unit }
51
52    proof fn closed_under_incl(a: Self, b: Self) {
53    }
54
55    proof fn commutative(a: Self, b: Self) {
56    }
57
58    proof fn associative(a: Self, b: Self, c: Self) {
59    }
60
61    proof fn op_unit(a: Self) {
62    }
63
64    proof fn unit_valid() {
65    }
66}
67
68} // verus!
vstd_extra/resource/pcm/frac.rs

vstd_extra/resource/pcm/
frac.rs
