Information about the prime finite field used for the interval analysis. More...

#include <Field.h>

Classes
struct	Hash
	Hash the prime modulus (consistent with the equality operator). More...

Public Member Functions
	Field ()=delete
	Field (const Field &)=default
	Field (Field &&) noexcept=default
Field &	operator= (const Field &)=default
llvm::DynamicAPInt	prime () const
	For the prime field p, returns p.
llvm::DynamicAPInt	half () const
	Returns ceil(p / 2), the first negative signed representative.
llvm::DynamicAPInt	felt (int i) const
	Returns i as a signed field element.
llvm::DynamicAPInt	zero () const
	Returns the zero field element.
llvm::DynamicAPInt	one () const
	Returns the unit field element.
llvm::DynamicAPInt	maxVal () const
	Returns p - 1, which is the max value possible in a prime field described by p.
llvm::DynamicAPInt	inv (const llvm::DynamicAPInt &i) const
	Returns the multiplicative inverse of i in prime field p.
llvm::DynamicAPInt	reduce (const llvm::DynamicAPInt &i) const
	Returns the canonical representative of i mod p in [0, p).
llvm::DynamicAPInt	reduce (int64_t i) const
llvm::DynamicAPInt	toSigned (const llvm::DynamicAPInt &i) const
	Converts a canonical field element to its signed integer representation: toSigned(f) = f if f < field.half() toSigned(f) = f - p if f >= field.half() (field.half() == ceil(p/2) == floor(p/2) + 1 for odd prime p).
unsigned	bitWidth () const
	Width sufficient for the modulus and its representatives, independent of literal storage.
llvm::StringRef	name () const
llvm::SMTExprRef	createSymbol (const llvm::SMTSolverRef &solver, const char *name) const
	Create a SMT solver symbol with the current field's bitwidth.
mlir::IntegerAttr	getPrimeAttr (mlir::MLIRContext *context, unsigned bitWidth) const
	Return the field prime modulus materialized as an integer attribute at bitWidth.

Static Public Member Functions
static void	addField (llvm::StringRef fieldName, const llvm::DynamicAPInt &prime, EmitErrorFn errFn)
	Add a new field to the set of available prime fields.
static void	addField (llvm::StringRef fieldName, llvm::StringRef primeStr, EmitErrorFn errFn)
static llvm::FailureOr< std::reference_wrapper< const Field > >	tryGetField (llvm::StringRef fieldName)
	Get a Field from a given field name string, or failure if the field is not defined.
static llvm::LogicalResult	verifyFieldDefined (llvm::StringRef fieldName, EmitErrorFn errFn)
	Search for a field with the given name, reporting an error if the field is not found.
static const Field &	getField (llvm::StringRef fieldName, EmitErrorFn errFn)
	Get a Field from a given field name string.
static const Field &	getField (llvm::StringRef fieldName)

Friends
bool	operator== (const Field &lhs, const Field &rhs)
bool	operator< (const Field &lhs, const Field &rhs)

Detailed Description

Information about the prime finite field used for the interval analysis.

Note: See implementation of initKnownFields for supported primes.; We use DynamicAPInt to support arithmetic that may require increasing or signed arithmetic (e.g., multiplying field elements before applying the modulus).

Definition at line 36 of file Field.h.

Constructor & Destructor Documentation

◆ Field() [1/3]

llzk::Field::Field ( )

delete

◆ Field() [2/3]

llzk::Field::Field ( const Field & )

default

◆ Field() [3/3]

llzk::Field::Field ( Field && )

defaultnoexcept

Member Function Documentation

◆ addField() [1/2]

void llzk::Field::addField	(	llvm::StringRef	fieldName,
		const llvm::DynamicAPInt &	prime,
		EmitErrorFn	errFn )

inlinestatic

Add a new field to the set of available prime fields.

Reports an error if the field is invalid or conflicts with an existing definition.

Definition at line 41 of file Field.h.

◆ addField() [2/2]

void llzk::Field::addField	(	llvm::StringRef	fieldName,
		llvm::StringRef	primeStr,
		EmitErrorFn	errFn )

static

◆ bitWidth()

unsigned llzk::Field::bitWidth ( ) const

inline

Width sufficient for the modulus and its representatives, independent of literal storage.

Definition at line 103 of file Field.h.

◆ createSymbol()

llvm::SMTExprRef llzk::Field::createSymbol	(	const llvm::SMTSolverRef &	solver,
		const char *	name ) const

inline

Create a SMT solver symbol with the current field's bitwidth.

Definition at line 108 of file Field.h.

◆ felt()

llvm::DynamicAPInt llzk::Field::felt ( int i ) const

inline

Returns i as a signed field element.

Definition at line 76 of file Field.h.

◆ getField() [1/2]

const Field & llzk::Field::getField ( llvm::StringRef fieldName )

inlinestatic

Definition at line 60 of file Field.h.

◆ getField() [2/2]

const Field & llzk::Field::getField	(	llvm::StringRef	fieldName,
		EmitErrorFn	errFn )

static

Get a Field from a given field name string.

Throws a fatal error if the field is unsupported.

Parameters

fieldName	The name of the field.
errFn	The error reporting function to use if the field is not found.

◆ getPrimeAttr()

IntegerAttr llzk::Field::getPrimeAttr	(	mlir::MLIRContext *	context,
		unsigned	bitWidth ) const

Return the field prime modulus materialized as an integer attribute at bitWidth.

Definition at line 163 of file Field.cpp.

◆ half()

llvm::DynamicAPInt llzk::Field::half ( ) const

inline

Returns ceil(p / 2), the first negative signed representative.

Definition at line 73 of file Field.h.

◆ inv()

DynamicAPInt llzk::Field::inv ( const llvm::DynamicAPInt & i ) const

Returns the multiplicative inverse of i in prime field p.

Definition at line 161 of file Field.cpp.

◆ maxVal()

llvm::DynamicAPInt llzk::Field::maxVal ( ) const

inline

Returns p - 1, which is the max value possible in a prime field described by p.

Definition at line 85 of file Field.h.

◆ name()

llvm::StringRef llzk::Field::name ( ) const

inline

Definition at line 105 of file Field.h.

◆ one()

llvm::DynamicAPInt llzk::Field::one ( ) const

inline

Returns the unit field element.

Definition at line 82 of file Field.h.

◆ operator=()

Field & llzk::Field::operator= ( const Field & )

default

◆ prime()

llvm::DynamicAPInt llzk::Field::prime ( ) const

inline

For the prime field p, returns p.

Definition at line 70 of file Field.h.

◆ reduce() [1/2]

llvm::DynamicAPInt llzk::Field::reduce ( const llvm::DynamicAPInt & i ) const

Returns the canonical representative of i mod p in [0, p).

Field elements are returned as signed integers so that negation functions as expected (i.e., reducing -1 will yield p-1).

◆ reduce() [2/2]

llvm::DynamicAPInt llzk::Field::reduce ( int64_t i ) const

inline

Definition at line 94 of file Field.h.

◆ toSigned()

DynamicAPInt llzk::Field::toSigned ( const llvm::DynamicAPInt & i ) const

Converts a canonical field element to its signed integer representation: toSigned(f) = f if f < field.half() toSigned(f) = f - p if f >= field.half() (field.half() == ceil(p/2) == floor(p/2) + 1 for odd prime p).

Definition at line 159 of file Field.cpp.

◆ tryGetField()

FailureOr< std::reference_wrapper< const Field > > llzk::Field::tryGetField ( llvm::StringRef fieldName )

static

Get a Field from a given field name string, or failure if the field is not defined.

Parameters

fieldName The name of the field.

Definition at line 54 of file Field.cpp.

◆ verifyFieldDefined()

LogicalResult llzk::Field::verifyFieldDefined	(	llvm::StringRef	fieldName,
		EmitErrorFn	errFn )

static

Search for a field with the given name, reporting an error if the field is not found.

Definition at line 65 of file Field.cpp.

◆ zero()

llvm::DynamicAPInt llzk::Field::zero ( ) const

inline

Returns the zero field element.

Definition at line 79 of file Field.h.

◆ operator<

bool operator<	(	const Field &	lhs,
		const Field &	rhs )

friend

Definition at line 124 of file Field.h.

◆ operator==

bool operator==	(	const Field &	lhs,
		const Field &	rhs )

friend

Definition at line 115 of file Field.h.

The documentation for this class was generated from the following files:

include/llzk/Util/Field.h
lib/Util/Field.cpp

Classes

Public Member Functions

Static Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Field() [1/3]

◆ Field() [2/3]

◆ Field() [3/3]

Member Function Documentation

◆ addField() [1/2]

◆ addField() [2/2]

◆ bitWidth()

◆ createSymbol()

◆ felt()

◆ getField() [1/2]

◆ getField() [2/2]

◆ getPrimeAttr()

◆ half()

◆ inv()

◆ maxVal()

◆ name()

◆ one()

◆ operator=()

◆ prime()

◆ reduce() [1/2]

◆ reduce() [2/2]

◆ toSigned()

◆ tryGetField()

◆ verifyFieldDefined()

◆ zero()

Friends And Related Symbol Documentation

◆ operator<

◆ operator==