LLZK 0.1.0
Veridise's ZK Language IR
|
Intervals over a finite field. More...
#include <IntervalAnalysis.h>
Classes | |
struct | Hash |
Public Types | |
enum class | Type { 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 |
bool | isEmpty () const |
bool | isNotEmpty () const |
bool | isDegenerate () const |
bool | isEntire () const |
bool | isTypeA () const |
bool | isTypeB () const |
bool | isTypeC () const |
bool | isTypeF () const |
template<Type... Types> | |
bool | is () const |
bool | operator== (const Interval &rhs) const |
const Field & | getField () const |
llvm::APSInt | width () const |
llvm::APSInt | lhs () const |
llvm::APSInt | rhs () const |
void | print (mlir::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, llvm::APSInt val) |
static Interval | Boolean (const Field &f) |
static Interval | Entire (const Field &f) |
static Interval | TypeA (const Field &f, llvm::APSInt a, llvm::APSInt b) |
static Interval | TypeB (const Field &f, llvm::APSInt a, llvm::APSInt b) |
static Interval | TypeC (const Field &f, llvm::APSInt a, llvm::APSInt b) |
static Interval | TypeF (const Field &f, llvm::APSInt a, llvm::APSInt 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< Interval > | operator/ (const Interval &lhs, const Interval &rhs) |
Returns failure if a division-by-zero is encountered. | |
mlir::raw_ostream & | operator<< (mlir::raw_ostream &os, const Interval &i) |
Intervals over a finite field.
Based on the Picus implementation. An interval may be:
A range [a, b] can be split into 2 categories:
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:
A acts on C:
A acts on F:
B acts on C
B acts on 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)
Definition at line 290 of file IntervalAnalysis.h.
|
strong |
Enumerator | |
---|---|
TypeA | |
TypeB | |
TypeC | |
TypeF | |
Empty | |
Degenerate | |
Entire |
Definition at line 292 of file IntervalAnalysis.h.
|
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 329 of file IntervalAnalysis.h.
Definition at line 343 of file IntervalAnalysis.h.
Definition at line 307 of file IntervalAnalysis.h.
Definition at line 303 of file IntervalAnalysis.h.
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 345 of file IntervalAnalysis.cpp.
Definition at line 301 of file IntervalAnalysis.h.
Definition at line 309 of file IntervalAnalysis.h.
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 213 of file IntervalAnalysis.cpp.
|
inline |
Definition at line 395 of file IntervalAnalysis.h.
Intersect.
Definition at line 281 of file IntervalAnalysis.cpp.
|
inline |
Definition at line 389 of file IntervalAnalysis.h.
|
inline |
Definition at line 382 of file IntervalAnalysis.h.
|
inline |
Definition at line 380 of file IntervalAnalysis.h.
|
inline |
Definition at line 383 of file IntervalAnalysis.h.
|
inline |
Definition at line 381 of file IntervalAnalysis.h.
|
inline |
Definition at line 384 of file IntervalAnalysis.h.
|
inline |
Definition at line 385 of file IntervalAnalysis.h.
|
inline |
Definition at line 386 of file IntervalAnalysis.h.
|
inline |
Definition at line 387 of file IntervalAnalysis.h.
Union.
Definition at line 225 of file IntervalAnalysis.cpp.
|
inline |
Definition at line 399 of file IntervalAnalysis.h.
Interval llzk::Interval::operator- | ( | ) | const |
Definition at line 408 of file IntervalAnalysis.cpp.
|
inline |
Definition at line 391 of file IntervalAnalysis.h.
void llzk::Interval::print | ( | mlir::raw_ostream & | os | ) | const |
Definition at line 457 of file IntervalAnalysis.cpp.
|
inline |
Definition at line 400 of file IntervalAnalysis.h.
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 220 of file IntervalAnalysis.cpp.
UnreducedInterval llzk::Interval::toUnreduced | ( | ) | const |
Convert to an UnreducedInterval.
Definition at line 203 of file IntervalAnalysis.cpp.
|
inlinestatic |
Definition at line 311 of file IntervalAnalysis.h.
|
inlinestatic |
Definition at line 315 of file IntervalAnalysis.h.
|
inlinestatic |
Definition at line 319 of file IntervalAnalysis.h.
|
inlinestatic |
Definition at line 323 of file IntervalAnalysis.h.
|
inlinestatic |
Definition at line 297 of file IntervalAnalysis.h.
|
inline |
Definition at line 397 of file IntervalAnalysis.h.
Definition at line 449 of file IntervalAnalysis.cpp.
Definition at line 417 of file IntervalAnalysis.cpp.
Definition at line 410 of file IntervalAnalysis.cpp.
Definition at line 415 of file IntervalAnalysis.cpp.
Returns failure if a division-by-zero is encountered.
Definition at line 437 of file IntervalAnalysis.cpp.
|
friend |
Definition at line 412 of file IntervalAnalysis.h.
|
staticconstexpr |
Definition at line 293 of file IntervalAnalysis.h.