Introducing the SIEVE Circuit-IR: Multiple Types and Conversions
Written: , Published: , Author: Kimberlee Model, Tags: SIEVE IR, Circuit-IR, v2.1.0,
In this series, we are examining the new SIEVE Circuit-IR. This installment will examine its type system and how it enables multiple types to be combined within the same relation.
One goal of this revision of the SIEVE IR is to support multiple fields in the same circuit. Although within a backend there may be significant distinctions between different fields, framing multiple fields, and even rings, as types of wires within the same circuit eases development for frontends. In one application, we found ourselves needing to integrate four primes: a pair of large primes for ED-DSA signatures, 2 for computing SHA hashes, and 261-1 for the proof’s "business logic".
Declaring Types
To understand the SIEVE-IR’s type system lets take a closer look at the header. The header’s we’ve seen so far have had just one field, but a circuits may list one or more types in its header (up to 256 types). Each type is assigned a type index, starting at 0 and incrementing.
@version 2.0.0; circuit; @type field 127; // type 0 @type field 2; // type 1 @begin
Prime fields are not the only types the IR allows. It also allows extension fields () and rings (modulo 2n).
- Prime Fields GF(p)
-
Prime fields behave like positive integers modulo some prime. Fields enjoy the broadest support by backends.
-
@type field [prime];
-
- Rings (modulo 2n)
-
Rings behave like positive integers modulo two to some power, n. They should feel familiar to anyone familiar with common unsigned int types.
-
@type ring [n];
-
- Extension Fields GF(pn)
-
Extension fields are polynomials of some base prime field, up to some degree, n. Rather than evaluating the polynomial at some particular point, we can add and multiply these by their coefficients, preventing the growth of new terms by modulus over an irreducible polynomial. In the IR, extension fields are defined by a base field — the type index of a prior prime field, baseidx — and an integer encoding of the irreducible polynomial, ipoly. ipoly is a single integer encoding of the coefficients, ci, using the base field’s prime, p. Most folk’s won’t need to use extension fields.
-
ipoly = Σ ci * pi
-
@type ext_field [baseidx] [n] [ipoly];
-
Using Multiple Types
Within the body of a circuit, each wire’s number is actually a pair of the type index and then the wire number.
This means there’s a different numbering space for every type.
By default, a gate will assume the type index is 0, however non-zero types may use the form @operation(index: $inputs) to set the type index of all wires accessed by the gate.
In general, all of a gates operands are of the same type (the circuit’s meaning would be somewhat nonsensical otherwise).
Here’s a sample circuit which uses prime fields 127 and 2.
// private inputs in each field. $0 <- @private(0); // wire 0:$0 (field 127, above) $0 <- @private(1); // wire 1:$0 (field 2, above) // Add and mul in each fields. $1 <- @add(0: $0, $0); $1 <- @mul(1: $0, $0); @end
Conversion Gates
Of course having multiple types is somewhat useless without being able to interact them with each other.
For this we introduce the @convert gate which converts wires from one type to another.
The convert gate will convert input wire(s) to output wires by accumulating each input wire as if it were a digit in a larger integer, then re-digitizing them in the output field.
This way an @convert gate which outputs to GF(2) is the equivalent of a big endian bit decomposition, and GF(3) would be a trit-decomposition.
Concretely, the convert gate introduces a wire range syntax expressing a sequence of wires.
A range has the form, $first … $last, meaning that every wire starting with $first up to and including $last.
Of course, $first must not be greater than $last, and if they are equal $last may be omitted.
Wire ranges serving as inputs must also obey memory contiguity rules, which will be discussed further on in this post.
For now, the @new($first … $last); directive will allocate contiguous space for any necessary range.
The convert gate has the syntax out_type: $output_first … $output_last ← @convert(in_type: $input_first … $input_last);.
When applicable, … $output_last and … $input_last may be omitted.
Here’s an example converting between GF(2), and GF(7).
@version 2.0.0; circuit; @type field 2; // type 0 @type field 7; // type 1 @begin // Convert all zeros @new($0...$2); $0 <- 0: <0>; // assigns a constant $1 <- 0: <0>; $2 <- 0: <0>; 1: $0 <- @convert(0: $0 ... $2); // Converts to 0 // Convert 1 @new($3...$5); $3 <- 0: <0>; $4 <- 0: <0>; $5 <- 0: <1>; 1: $1 <- @convert(0: $3 ... $5); // Converts to 1 // Convert 6 @new($6...$8); $6 <- 0: <1>; $7 <- 0: <1>; $8 <- 0: <0>; 1: $2 <- @convert(0: $3 ... $5); // Converts to 6 // Convert 7 @new($9...$11); $9 <- 0: <1>; $10 <- 0: <1>; $11 <- 0: <1>; 1: $3 <- @convert(0: $3 ... $5); // Converts to 7?! @end
The last example 1,1,1 should convert to 7, but that overflows the field.
The convert gate has an optional @modulus or @no_modulus tag specifying how it handles overflow, @convert(/* … */, @no_modulus).
-
In
@modulusmode an overflowing value wraps around modularly, in this case back to 0. -
In
@no_modulusmode an overflow causes the proof to be false — same as@assert_zeroof a non-zero wire.
Conclusion
Today’s installment overviewed how the Circuit-IR enables a proof to utilize multiple types, and convert wires from one type to another. Generally, conversions are fairly expensive in ZK, and should be avoided when possible. Sometimes they are necessary — when a subcomputation cannot be performed in one type, or when the savings from performing a subcomputation in an alternative field exceeds the cost of conversion.
Next up, we will have a look at Circuit-IR functions and memory management, features which enable a great amount of scalability.