|
LLZK 0.1.0
Veridise's ZK Language IR
|
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 Field & | getField () 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< Interval > | operator/ (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) |
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 200 of file Intervals.h.
|
strong |
| Enumerator | |
|---|---|
| TypeA | |
| TypeB | |
| TypeC | |
| TypeF | |
| Empty | |
| Degenerate | |
| Entire | |
Definition at line 202 of file Intervals.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 243 of file Intervals.h.
Definition at line 257 of file Intervals.h.
Definition at line 221 of file Intervals.h.
|
inlinestatic |
Definition at line 213 of file Intervals.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 292 of file Intervals.cpp.
Definition at line 211 of file Intervals.h.
Definition at line 223 of file Intervals.h.
Definition at line 217 of file Intervals.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 166 of file Intervals.cpp.
|
inline |
Definition at line 324 of file Intervals.h.
Intersect.
Definition at line 231 of file Intervals.cpp.
|
inline |
Definition at line 318 of file Intervals.h.
|
inline |
Definition at line 316 of file Intervals.h.
|
inline |
Definition at line 315 of file Intervals.h.
|
inline |
Definition at line 313 of file Intervals.h.
|
inline |
Definition at line 314 of file Intervals.h.
|
inline |
Definition at line 306 of file Intervals.h.
|
inline |
Definition at line 304 of file Intervals.h.
|
inline |
Definition at line 307 of file Intervals.h.
|
inline |
Definition at line 305 of file Intervals.h.
|
inline |
Definition at line 308 of file Intervals.h.
|
inline |
Definition at line 309 of file Intervals.h.
|
inline |
Definition at line 310 of file Intervals.h.
|
inline |
Definition at line 311 of file Intervals.h.
Union.
Definition at line 178 of file Intervals.cpp.
|
inline |
Definition at line 328 of file Intervals.h.
| Interval llzk::Interval::operator- | ( | ) | const |
Definition at line 354 of file Intervals.cpp.
|
inline |
Definition at line 320 of file Intervals.h.
| Interval llzk::Interval::operator~ | ( | ) | const |
Definition at line 356 of file Intervals.cpp.
| void llzk::Interval::print | ( | llvm::raw_ostream & | os | ) | const |
Definition at line 541 of file Intervals.cpp.
|
inline |
Definition at line 329 of file Intervals.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 173 of file Intervals.cpp.
| UnreducedInterval llzk::Interval::toUnreduced | ( | ) | const |
Convert to an UnreducedInterval.
Definition at line 154 of file Intervals.cpp.
Definition at line 219 of file Intervals.h.
|
inlinestatic |
Definition at line 225 of file Intervals.h.
|
inlinestatic |
Definition at line 229 of file Intervals.h.
|
inlinestatic |
Definition at line 233 of file Intervals.h.
|
inlinestatic |
Definition at line 237 of file Intervals.h.
|
inlinestatic |
Definition at line 207 of file Intervals.h.
| DynamicAPInt llzk::Interval::width | ( | ) | const |
Definition at line 454 of file Intervals.cpp.
Definition at line 467 of file Intervals.cpp.
Definition at line 527 of file Intervals.cpp.
Definition at line 484 of file Intervals.cpp.
Definition at line 501 of file Intervals.cpp.
Definition at line 403 of file Intervals.cpp.
Definition at line 408 of file Intervals.cpp.
Definition at line 373 of file Intervals.cpp.
Definition at line 360 of file Intervals.cpp.
Definition at line 371 of file Intervals.cpp.
Returns failure if a division-by-zero is encountered.
Definition at line 392 of file Intervals.cpp.
Definition at line 423 of file Intervals.cpp.
|
friend |
Definition at line 341 of file Intervals.h.
Definition at line 439 of file Intervals.cpp.
|
staticconstexpr |
Definition at line 203 of file Intervals.h.