vstd_extra/resource/pcm/
frac.rs

1//! Fractional resource algebra.
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 TOTAL 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>
10use vstd::arithmetic::*;
11use vstd::pcm::PCM;
12use vstd::prelude::*;
13
14verus! {
15
16/// Fractional PCM
17#[verifier::ext_equal]
18pub ghost enum FracR<T> {
19    Unit,
20    Frac(real, T),
21    Invalid,
22}
23
24impl<T: PartialEq> PCM for FracR<T> {
25    open spec fn valid(self) -> bool {
26        match self {
27            FracR::Unit => true,
28            FracR::Frac(q, _) => 0.0real < q && q <= 1.0real,
29            FracR::Invalid => false,
30        }
31    }
32
33    /// 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.
34    open spec fn op(self, other: Self) -> Self {
35        match (self, other) {
36            (FracR::Unit, x) => x,
37            (x, FracR::Unit) => x,
38            (FracR::Frac(q1, a1), FracR::Frac(q2, a2)) => {
39                if a1 == a2 && 0.0real < q1 && 0.0real < q2 && q1 + q2 <= 1.0real {
40                    FracR::Frac(q1 + q2, a1)
41                } else {
42                    FracR::Invalid
43                }
44            },
45            _ => FracR::Invalid,
46        }
47    }
48
49    open spec fn unit() -> Self {
50        FracR::Unit
51    }
52
53    proof fn closed_under_incl(a: Self, b: Self) {
54    }
55
56    proof fn commutative(a: Self, b: Self) {
57    }
58
59    proof fn associative(a: Self, b: Self, c: Self) {
60    }
61
62    proof fn op_unit(a: Self) {
63    }
64
65    proof fn unit_valid() {
66    }
67}
68
69} // verus!
vstd_extra/resource/pcm/frac.rs

vstd_extra/resource/pcm/
frac.rs
