This crate defines specification-friendly natural integers with an upper bound. Operations on these integers can be defined as modular (modulo the upper bound) or regular (with a panic on underflow or overflow).
As each integer gets its own Rust type, the compiler detects and prevent any mixing between all the diffent integers you would have defined.
Here is the macro used to defined the SizeNatExample type of this crate:
define_abstract_integer_checked!(SizeNatExample, 64);SizeNat is the name of the newly-created type. 64 is the number of bits of the machine
representation of the type. From the number of bits is derived an upper bound for the integer
for which all operations are checked for overflow.
The resulting integer type is copyable, and supports addition, substraction, multiplication,
integer division, remainder, comparison and equality. The from_literal method allows you to
convert integer literals into your new type.
On top of a previously defined abstract integer, you can define another type that lets you implement modular arithmetic. For instance, this crate defines the arithmetic field over the 9th Mersenne prime with:
define_refined_modular_integer!(
SizeNatFieldExample,
SizeNatExample,
SizeNatExample::pow2(61) - SizeNatExample::from_literal(1)
);The first argument of this new macro is the name of the newly defined refined type. The second argument is the name of the base abstract integer that will act as the representation. The third example is the modulo for all operations, defined as a value of the base type.