Expand description
Fractional resource algebra.
Unlike the FracGhost in vstd,
which requires a compile-time constant TOTAL to define integer-based fractions,
we model fractions as real numbers q : real in (0, 1] like Iris, where 1.0 is full
ownership, which allows arbitrary splitting of fractions at runtime.
For Iris definition, see: https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/frac.v
Enumsยง
- FracR
- Fractional PCM