LLZK 0.1.0
Veridise's ZK Language IR
Loading...
Searching...
No Matches

Intervals over a finite field. More...

#include <Intervals.h>

Classes

struct  Hash

Public Types

enum class  Type : std::uint8_t {
  TypeA = 0 , TypeB , TypeC , TypeF ,
  Empty , Degenerate , Entire
}

Public Member Functions

 Interval ()
 To satisfy the dataflow::ScalarLatticeValue requirements, this class must be default initializable.
UnreducedInterval toUnreduced () const
 Convert to an UnreducedInterval.
UnreducedInterval firstUnreduced () const
 Get the first side of the interval for TypeF intervals, otherwise just get the full interval as an UnreducedInterval (with toUnreduced).
UnreducedInterval secondUnreduced () const
 Get the second side of the interval for TypeA, TypeB, and TypeC intervals.
Interval join (const Interval &rhs) const
 Union.
Interval intersect (const Interval &rhs) const
 Intersect.
Interval difference (const Interval &other) const
 Computes and returns this - (this & other) if the operation produces a single interval.
Interval operator- () const
Interval operator~ () const
bool isEmpty () const
bool isNotEmpty () const
bool isDegenerate () const
bool isEntire () const
bool isTypeA () const
bool isTypeB () const
bool isTypeC () const
bool isTypeF () const
bool isBoolFalse () const
bool isBoolTrue () const
bool isBoolEither () const
bool isBoolean () const
template<Type... Types>
bool is () const
bool operator== (const Interval &rhs) const
const FieldgetField () const
llvm::DynamicAPInt width () const
llvm::DynamicAPInt lhs () const
llvm::DynamicAPInt rhs () const
void print (llvm::raw_ostream &os) const

Static Public Member Functions

static std::string_view TypeName (Type t)
static Interval Empty (const Field &f)
static Interval Degenerate (const Field &f, const llvm::DynamicAPInt &val)
static Interval False (const Field &f)
static Interval True (const Field &f)
static Interval Boolean (const Field &f)
static Interval Entire (const Field &f)
static Interval TypeA (const Field &f, const llvm::DynamicAPInt &a, const llvm::DynamicAPInt &b)
static Interval TypeB (const Field &f, const llvm::DynamicAPInt &a, const llvm::DynamicAPInt &b)
static Interval TypeC (const Field &f, const llvm::DynamicAPInt &a, const llvm::DynamicAPInt &b)
static Interval TypeF (const Field &f, const llvm::DynamicAPInt &a, const llvm::DynamicAPInt &b)
template<std::pair< Type, Type >... Pairs>
static bool areOneOf (const Interval &a, const Interval &b)

Static Public Attributes

static constexpr std::array< std::string_view, 7 > TypeNames

Friends

Interval operator+ (const Interval &lhs, const Interval &rhs)
Interval operator- (const Interval &lhs, const Interval &rhs)
Interval operator* (const Interval &lhs, const Interval &rhs)
Interval operator% (const Interval &lhs, const Interval &rhs)
mlir::FailureOr< Intervaloperator/ (const Interval &lhs, const Interval &rhs)
 Returns failure if a division-by-zero is encountered.
Interval operator& (const Interval &lhs, const Interval &rhs)
Interval operator<< (const Interval &lhs, const Interval &rhs)
Interval operator>> (const Interval &lhs, const Interval &rhs)
Interval boolAnd (const Interval &lhs, const Interval &rhs)
Interval boolOr (const Interval &lhs, const Interval &rhs)
Interval boolXor (const Interval &lhs, const Interval &rhs)
Interval boolNot (const Interval &iv)
llvm::raw_ostream & operator<< (llvm::raw_ostream &os, const Interval &i)

Detailed Description

Intervals over a finite field.

Based on the Picus implementation. An interval may be:

  • Empty
  • Entire (meaning any value across the entire field)
  • Degenerate (meaning it contains a single value)
  • Or Type A–F. For these types, refer to the below notes:

A range [a, b] can be split into 2 categories:

  • Internal: a <= b
  • External: a > b – equivalent to [a, p-1] U [0, b]

Internal range can be further split into 3 categories: (A) a, b < p/2. E.g., [10, 12] (B) a, b > p/2. OR: a, b \in {-p/2, 0}. E.g., [p-4, p-2] === [-4, -2] (C) a < p/2, b > p/2. E.g., [p/2 - 5, p/2 + 5]

External range can be further split into 3 categories: (D) a, b < p/2. OR: a \in {-p, -p/2}, b \in {0, p/2}. E.g., [12, 10] === [-p+12, 10] (E) a, b > p/2. OR: a \in {-p/2, 0} , b \in {p/2, p}. E.g., [p-2, p-4] === [-2, p-4] (F) a > p/2, b < p/2. OR: a \in {-p/2, 0} , b \in {0, p/2}. E.g., [p/2 + 5, p/2 - 5] === [-p/2 + 5, p/2 - 5]

<-------------------------------------------------------------> -p -p/2 0 p/2 p [ A ] [ A ] [ B ] [ B ] [ C ] [ C ] F ] [ F ] [ F <------------------------------------------------------------->

D ] [ D ] [ D E ] [ E ] [ E

For the sake of simplicity, let's just not care about D and E, which covers at least half of the field, and potentially more.

Now, there are 4 choose 2 possible non-self interactions:

A acts on B:

  • intersection: impossible
  • union: C or F

A acts on C:

  • intersection: A
  • union: C

A acts on F:

  • intersection: A
  • union: F

B acts on C

  • intersection: B
  • union: C

B acts on F:

  • intersection: B
  • union: F

C acts on F:

  • intersection: A, B, C, F

    E.g. [p/2 - 10, p/2 + 10] intersects [-p/2 + 2, p/2 - 2]

    = ((-p/2 - 10, -p/2 + 10) intersects (-p/2 + 2, p/2 - 2)) union (( p/2 - 10, p/2 + 10) intersects (-p/2 + 2, p/2 - 2))

    = (-p/2 + 2, -p/2 + 10) union (p/2 - 10, p/2 - 2)

  • union: don't care for now, we can revisit this later.

Definition at line 200 of file Intervals.h.

Member Enumeration Documentation

◆ Type

enum class llzk::Interval::Type : std::uint8_t
strong
Enumerator
TypeA 
TypeB 
TypeC 
TypeF 
Empty 
Degenerate 
Entire 

Definition at line 202 of file Intervals.h.

Constructor & Destructor Documentation

◆ Interval()

llzk::Interval::Interval ( )
inline

To satisfy the dataflow::ScalarLatticeValue requirements, this class must be default initializable.

The default interval is the full range of values.

Definition at line 243 of file Intervals.h.

Member Function Documentation

◆ areOneOf()

template<std::pair< Type, Type >... Pairs>
bool llzk::Interval::areOneOf ( const Interval & a,
const Interval & b )
inlinestatic

Definition at line 257 of file Intervals.h.

◆ Boolean()

Interval llzk::Interval::Boolean ( const Field & f)
inlinestatic

Definition at line 221 of file Intervals.h.

◆ Degenerate()

Interval llzk::Interval::Degenerate ( const Field & f,
const llvm::DynamicAPInt & val )
inlinestatic

Definition at line 213 of file Intervals.h.

◆ difference()

Interval llzk::Interval::difference ( const Interval & other) const

Computes and returns this - (this & other) if the operation produces a single interval.

Note that this is an interval difference, not a subtraction operation like the operator- below.

For example, given *this = [1, 10] and other = [5, 11], this function would return [1, 4], as this & other (the intersection) = [5, 10], so [1, 10] - [5, 10] = [1, 4].

For example, given *this = [1, 10] and other = [5, 6], this function should return [1, 4] and [7, 10], but we don't support having multiple disjoint intervals, so this is returned as-is.

Definition at line 292 of file Intervals.cpp.

◆ Empty()

Interval llzk::Interval::Empty ( const Field & f)
inlinestatic

Definition at line 211 of file Intervals.h.

◆ Entire()

Interval llzk::Interval::Entire ( const Field & f)
inlinestatic

Definition at line 223 of file Intervals.h.

◆ False()

Interval llzk::Interval::False ( const Field & f)
inlinestatic

Definition at line 217 of file Intervals.h.

◆ firstUnreduced()

UnreducedInterval llzk::Interval::firstUnreduced ( ) const

Get the first side of the interval for TypeF intervals, otherwise just get the full interval as an UnreducedInterval (with toUnreduced).

Definition at line 166 of file Intervals.cpp.

◆ getField()

const Field & llzk::Interval::getField ( ) const
inline

Definition at line 324 of file Intervals.h.

◆ intersect()

Interval llzk::Interval::intersect ( const Interval & rhs) const

Intersect.

Definition at line 231 of file Intervals.cpp.

◆ is()

template<Type... Types>
bool llzk::Interval::is ( ) const
inline

Definition at line 318 of file Intervals.h.

◆ isBoolean()

bool llzk::Interval::isBoolean ( ) const
inline

Definition at line 316 of file Intervals.h.

◆ isBoolEither()

bool llzk::Interval::isBoolEither ( ) const
inline

Definition at line 315 of file Intervals.h.

◆ isBoolFalse()

bool llzk::Interval::isBoolFalse ( ) const
inline

Definition at line 313 of file Intervals.h.

◆ isBoolTrue()

bool llzk::Interval::isBoolTrue ( ) const
inline

Definition at line 314 of file Intervals.h.

◆ isDegenerate()

bool llzk::Interval::isDegenerate ( ) const
inline

Definition at line 306 of file Intervals.h.

◆ isEmpty()

bool llzk::Interval::isEmpty ( ) const
inline

Definition at line 304 of file Intervals.h.

◆ isEntire()

bool llzk::Interval::isEntire ( ) const
inline

Definition at line 307 of file Intervals.h.

◆ isNotEmpty()

bool llzk::Interval::isNotEmpty ( ) const
inline

Definition at line 305 of file Intervals.h.

◆ isTypeA()

bool llzk::Interval::isTypeA ( ) const
inline

Definition at line 308 of file Intervals.h.

◆ isTypeB()

bool llzk::Interval::isTypeB ( ) const
inline

Definition at line 309 of file Intervals.h.

◆ isTypeC()

bool llzk::Interval::isTypeC ( ) const
inline

Definition at line 310 of file Intervals.h.

◆ isTypeF()

bool llzk::Interval::isTypeF ( ) const
inline

Definition at line 311 of file Intervals.h.

◆ join()

Interval llzk::Interval::join ( const Interval & rhs) const

Union.

Definition at line 178 of file Intervals.cpp.

◆ lhs()

llvm::DynamicAPInt llzk::Interval::lhs ( ) const
inline

Definition at line 328 of file Intervals.h.

◆ operator-()

Interval llzk::Interval::operator- ( ) const

Definition at line 354 of file Intervals.cpp.

◆ operator==()

bool llzk::Interval::operator== ( const Interval & rhs) const
inline

Definition at line 320 of file Intervals.h.

◆ operator~()

Interval llzk::Interval::operator~ ( ) const

Definition at line 356 of file Intervals.cpp.

◆ print()

void llzk::Interval::print ( llvm::raw_ostream & os) const

Definition at line 541 of file Intervals.cpp.

◆ rhs()

llvm::DynamicAPInt llzk::Interval::rhs ( ) const
inline

Definition at line 329 of file Intervals.h.

◆ secondUnreduced()

UnreducedInterval llzk::Interval::secondUnreduced ( ) const

Get the second side of the interval for TypeA, TypeB, and TypeC intervals.

Using this function is an error for all other interval types.

Definition at line 173 of file Intervals.cpp.

◆ toUnreduced()

UnreducedInterval llzk::Interval::toUnreduced ( ) const

Convert to an UnreducedInterval.

Definition at line 154 of file Intervals.cpp.

◆ True()

Interval llzk::Interval::True ( const Field & f)
inlinestatic

Definition at line 219 of file Intervals.h.

◆ TypeA()

Interval llzk::Interval::TypeA ( const Field & f,
const llvm::DynamicAPInt & a,
const llvm::DynamicAPInt & b )
inlinestatic

Definition at line 225 of file Intervals.h.

◆ TypeB()

Interval llzk::Interval::TypeB ( const Field & f,
const llvm::DynamicAPInt & a,
const llvm::DynamicAPInt & b )
inlinestatic

Definition at line 229 of file Intervals.h.

◆ TypeC()

Interval llzk::Interval::TypeC ( const Field & f,
const llvm::DynamicAPInt & a,
const llvm::DynamicAPInt & b )
inlinestatic

Definition at line 233 of file Intervals.h.

◆ TypeF()

Interval llzk::Interval::TypeF ( const Field & f,
const llvm::DynamicAPInt & a,
const llvm::DynamicAPInt & b )
inlinestatic

Definition at line 237 of file Intervals.h.

◆ TypeName()

std::string_view llzk::Interval::TypeName ( Type t)
inlinestatic

Definition at line 207 of file Intervals.h.

◆ width()

DynamicAPInt llzk::Interval::width ( ) const

Definition at line 454 of file Intervals.cpp.

◆ boolAnd

Interval boolAnd ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 467 of file Intervals.cpp.

◆ boolNot

Interval boolNot ( const Interval & iv)
friend

Definition at line 527 of file Intervals.cpp.

◆ boolOr

Interval boolOr ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 484 of file Intervals.cpp.

◆ boolXor

Interval boolXor ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 501 of file Intervals.cpp.

◆ operator%

Interval operator% ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 403 of file Intervals.cpp.

◆ operator&

Interval operator& ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 408 of file Intervals.cpp.

◆ operator*

Interval operator* ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 373 of file Intervals.cpp.

◆ operator+

Interval operator+ ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 360 of file Intervals.cpp.

◆ operator-

Interval operator- ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 371 of file Intervals.cpp.

◆ operator/

mlir::FailureOr< Interval > operator/ ( const Interval & lhs,
const Interval & rhs )
friend

Returns failure if a division-by-zero is encountered.

Definition at line 392 of file Intervals.cpp.

◆ operator<< [1/2]

Interval operator<< ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 423 of file Intervals.cpp.

◆ operator<< [2/2]

llvm::raw_ostream & operator<< ( llvm::raw_ostream & os,
const Interval & i )
friend

Definition at line 341 of file Intervals.h.

◆ operator>>

Interval operator>> ( const Interval & lhs,
const Interval & rhs )
friend

Definition at line 439 of file Intervals.cpp.

Member Data Documentation

◆ TypeNames

std::array<std::string_view, 7> llzk::Interval::TypeNames
staticconstexpr
Initial value:
= {"TypeA", "TypeB", "TypeC",
"TypeF", "Empty", "Degenerate",
"Entire"}

Definition at line 203 of file Intervals.h.


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