abstract_integers

Crates.ioabstract_integers
lib.rsabstract_integers
version0.1.5
sourcesrc
created_at2019-02-07 16:23:42.294927
updated_at2023-03-20 11:58:24.807572
descriptionDefining specification-friendly bounded natural integer types
homepage
repositoryhttps://github.com/hacspec/hacspec
max_upload_size
id113379
size47,449
Franziskus Kiefer (franziskuskiefer)

documentation

README

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.

Defining a new integer type

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.

Refining an integer type for modular arithmetic

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.

Commit count: 1414

cargo fmt