Introducing the SIEVE Intermediate Representation
Written: , Published: , Author: Kimberlee Model, Tags: SIEVE IR, v1.0.1, outdated,
Recently the DARPA SIEVE Program released a 1.0.1 version of its primary program-wide deliverable, the SIEVE Intermediate Representation (IR). As one of the primary developers of the IR, team Wizkit will write a series of posts about the IR, what it got right, what it got wrong, and what we’d like to see in upcoming versions. But today we will start the series with this post as more of an impartial introduction to the SIEVE IR. It is our hope that this will ease you into using the SIEVE IR in your own work, and (most importantly) enable you to read further posts in this series.
In writing this, we assume the reader has a cursory understanding of Zero-Knowledge Proofs (ZK). If you know who the "prover" and "verifier" are, and know what a "relation", "instance", and "witness" are, then you should be okay. An understanding of finite-field arithmetic in GF(p) and boolean arithmetic (equivalently, arithmetic in GF(2)) would also be helpful.
To be just a bit more precise, we’re working in the following setting: There are two parties, a "Prover" and a "Verifier". The Prover wants to prove some statement to the Verifier "in zero knowledge" — that is, informally, without allowing the Verifier to learn anything other than that the statement is true. As usual (and necessary) in the world of ZK, we assume that the statement to be proven amounts to a decision problem in the complexity class NP. As such, the statement can be formulated as "R(x,w)", where x is some public "instance" known to both the Prover and the Verifier, w is a secret "witness" known only to the Prover, and R is a public boolean NP relation (or, equivalently, a witness relation for some NP language L). The statement to be proven can be thought of as a statement "about" the instance x whose validity is "witnessed" by the witness w.
Finally, it should be noted that the IR has two syntaxes: text and binary. In this post, we will describe the IR by reference to the text format. To learn more about the binary format see section 5 of the IR spec.
Background
One of the mandates of the SIEVE Program is for performers to come up with a common Intermediate Representation, or "IR."
The IR is a simplistic programming language for representing the NP statements to prove in ZK.
It must be simple enough for ZK proof systems (which we will from here on out refer to as "ZK backends") to prove efficiently, but expressive enough as to not limit the frontend programming language that produces the statement.
The SIEVE IR (we will use this interchangeably with just "IR" from now on) represents NP statements using boolean or arithmetic circuits with values contained in "wires".
The reader should recall that boolean and arithmetic circuit satisfiability are NP-complete problems, and so any NP relation has such a representation.
We use the terminology "short witness" to refer to the prover’s secret inputs to the circuit.
We use the adjective "short" to contrast with a hypothetical "extended" witness which would consist of the values of every wire in a satisfying assignment of the circuit.
Boolean circuits have 0 or 1 values and logical AND, XOR, and NOT gates.
Arithmetic circuits have field element values with addition and multiplication gates.
The IR currently supports only fields GF(p) of prime field size p, that is, the integers modulo the prime p.
At the beginning of the program, we debated the merits of different levels of expressivity, but settled on a very simple "list-of-gates" IR, with the understanding that we would build upwards from this. The stated goal of this early IR (which we colloquially refer to as "IR0") had feature parity to Bristol Fashion, but with a spin towards ZK and an eye towards extension.
Early IR Development
Each wire of a circuit in IR0 was represented as an index to a global array of "wires", and each gate was listed in the relation as a function of its input wires assigned to its output wire.
The first 0 through n wires were assigned by the instance and the next n+1 through n+m were assigned by the short witness (for some appropriate n and m, of course).
IR0 also had a short header listing certain aspects of the circuit:
-
An IR version number
-
Whether to use arithmetic or boolean gates
-
A field description, consisting of
-
the characteristic p (for GF(p))
-
a vestigial degree n (for GF(pn)); however, this degree is currently fixed at 1, as we decided not to handle extension fields until a later phase.
-
-
The total number of wires in the circuit (including instance and short witness wires)
-
The number of instance wires
-
The number of short witness wires
Additionally, IR0 existed as a combination of three "resources" (files).
-
The Instance resource listed assignments of values to wires 0 through
n. -
The Short Witness resource assigns values to wires
n+1throughn+m. -
The Relation lists gates for assignments of the remaining wires in the circuit.
Each wire was assigned exactly once and had to be assigned a value before being used as a subsequent gate’s input. In other words, wires adhered to the following requirements: "Single Static Assignment" (SSA) and topological ordering.
A "Streaming" Modification
Soon after this, we made modifications that enabled "streaming" proof systems in cases where the entirety of an NP statement may not be available at the beginning of the proof computation, or loading the entirety of it may exceed available memory.
This is similar to piping awk, grep, and sed together for regular text manipulations.
To support such an operating paradigm, we made three changes:
-
Did away with the circuit size declarations.
-
Changed the instance and short witness to streams of values, rather than lists of assignments, where assignments are handled by "special"
@instanceand@short_witnessdirectives in the relation. Each of these directives behaves likeC'sfgetc(stream)for its stream, returning the next value, and advancing the stream by one. -
Added a special "delete" gate to indicate that certain wires are no longer needed and associated memory could be freed. Delete may be used with a single argument or with a first and last argument to indicate a range of wires.
This core IR is still present, although newer features have necessitated additional changes to the IR header. Here is an example of an NP statement encoded in what is now referred to as "IR-Simple". Given two legs (as their lengths), this example proves the existence of a right triangle with those legs using Pythagoras’s theorem.
version 1.0.1; // The latest IR version field // GF(p) as defined by characteristic 127 // this prime number p degree 1; // and a vestigial degree (always 1) relation // indicates that this resource is a relation gate_set: arithmetic; // Will use add/mul/addc/mulc instead of xor/and/not features: simple; // Only features of this "simple"/"streaming" IR are used @begin // The body of the relation $0 <- @instance; // leg A $3 <- @mul($0, $0); // A^2 $1 <- @instance; // leg B $4 <- @mul($1, $1); // B^2 $2 <- @short_witness; // hypotenuse C $5 <- @mul($2, $2); // C^2 @delete($0, $2); // We have the squares, so we don't need A, B, and C $6 <- @add($3, $4); // A^2 + B^2 // We want to prove that A^2 + B^2 == C^2, but we can't do equality directly // Instead show that A^2 + B^2 - C^2 == 0. $7 <- @mulc($5, <126>); // Negate C^2 by multiplying by p-1 $8 <- @add($6, $7); // add it all up, @assert_zero($8); // and prove it is zero. @end
For the more visually oriented, the circuit would look like this. Also, if you don’t mind us tooting our own horns, check out our wiztoolkit visualization tool.
The instance and witness would appear as the following for a "3 4 5" triangle.
version 1.0.1; field characteristic 127 degree 1; instance @begin <3>; // leg A <4>; // leg B @end
version 1.0.1; field characteristic 127 degree 1; short_witness @begin <5>; // hypotenuse C @end
|
Tip
|
Executing the IR with FIREALARM
To run the IR absent of ZK — that is, to simply evaluate an circuit with inputs from an instance and short witness "in the clear," rather than proving satisfiability in zero knowledge — for development, debugging, and education purposes, Stealth has developed the
To give it a try, copy and paste the triangle example above into text files (with appropriate suffixes) and try invoking firealarm in both modes: > wtk-firealarm circuit.rel > wtk-firealarm circuit.rel public_inputs.ins prover_inputs.wit |
Structuring the IR
Currently, the IR contains three features for adding program structure and control flow. This provides simplifying abstractions away from purely unstructured circuit formats such as Bristol Fashion.
- Function Gates
-
Encapsulate a sub-circuit for reuse elsewhere in the relation.
- Switch Case Statements
-
Conditionally branch between assignments of alternative sub-circuits.
- For Loops
-
Repeat a single sub-circuit many times.
Going into these features, understand that wires in SIEVE IR are not lexically scoped. The bodies (sub-circuits) of each structural element are as independent of each other as possible. Each sub-circuit defines its own wire-numbering space, each one starting back from zero.
It is worth reiterating that each sub-circuit’s numbering space must maintain the SSA and topological ordering principles described earlier.
Function Gates
Superficially, a function gate declares a sub-circuit. The sub-circuit can be "invoked" elsewhere, connecting wires from the caller to those of the function. An important consequence of this is that the internals of the function gate are isolated from the caller and locally scoped within the function. Because of this "connected isolation", the function gate is a building block for the other two features.
A function gate is declared at the top of a relation. Its declaration adds nothing to the relation until it is invoked later. It has 5 identifying characteristics.
-
Name
-
Number of Output wires
-
Number of Input wires
-
Number of Instance Consumptions
-
Number of Short Witness Consumptions
The first three allow the sub-circuit to be referenced and connected into another circuit. The latter two define the side-effects to be expected after the circuit’s invocation, which will become important for switch cases.
A mapping is used to connect wires from the calling scope into and out of the function’s scope.
In the function’s scope, output wires are numbered sequentially from 0 through number of outputs - 1, and inputs from number of outputs through number of outputs + number of inputs - 1.
At invocation, arguments are bound positionally.
The caller lists each output and then each input, and in that order they are bound to $0, $1, $2… in the callee’s scope.
Here is an example that squares the last input, then sums it with the first three input wire values.
@function(add4_sq_last, @out: 1, @in: 4, @instance: 0, @short_witness: 0) // $0: single output wire // $1, $2, $3, $4: input wires // $5 and onwards: local wires $5 <- @add($1, $2); $6 <- @mul($4, $4); $7 <- @add($3, $6); $0 <- @add($5, $7); @end // output assigns to $10, inputs are connected to $6, $7, $2, and $3 // $3 got squared $10 <- @call(add4_sq_last, $6, $7, $2, $3); // now $7 got squared $11 <- @call(add4_sq_last, $2, $3, $6, $7); // Sequential wires may be abbreviated to a range $12 <- @call(add4_sq_last, $2 ... $5); // And ranges may be mixed with single elements in a list $13 <- @call(add4_sq_last, $2 ... $4, $6);
An anonymous function invocation syntax is also available. This exists mainly to allow the appearance of nested loops and switch statements. Here is the same function body, now invoked as an inline function. Obviously, it doesn’t need a function name, but also the input and output wire counts are inferred. The example below illustrates this inference. The instance and short witness counts must still be declared in the anonymous function signature.
$14 <- @anon_call($10 ... $13, @instance: 0, @short_witness: 0) // Caller-scoped wires $10 ... $13 are mapped to locally scoped wires $1 ... $4. // Caller-scoped wire $14 is mapped to locally scoped wire $0. // Wires >= $5 are locally scoped. $5 <- @add($1, $2); $6 <- @mul($4, $4); $7 <- @add($3, $6); $0 <- @add($5, $7); @end
One last thing to note is that recursive function gates are prohibited. This is because a function gate is not a function; it emulates a circuit, not a processor, and thus there is no actual call stack.
Switch Case Statements
Switch statements allow a circuit to assign wires as the results of a conditional branch. Here is an example switch statement which either sums or multiplies some inputs. Neither case in this example has side effects.
// The following switch statement chooses between output wire $0 from each case. The case is selected based on the value of $4.
$5 <- @switch($4)
@case < 0 >: @anon_call($0...$3, @instance: 0, @short_witness: 0)
// Calling scope $5 corresponds to local scope $0
// Calling scope $0 ... $3 corresponds to local scope $1 ... $4
// $5 and $6 are local
$5 <- @add($1, $2);
$6 <- @add($3, $4);
$0 <- @add($5, $6);
@end
@case < 1 >: @anon_call($0...$3, @instance: 0, @short_witness: 0)
// Same scoping as above case.
$5 <- @mul($1, $2);
$6 <- @mul($3, $4);
$0 <- @mul($5, $6);
@end
@end
Notice that, as with the for loops described below, the body of each case is a function gate. Each case’s function gate is missing its output wire list; instead, all cases share the output list of the entire switch. In the above example, cases share output wire $5 at the very top, which is a wire list of length one.
In standard programming languages we are accustomed to conditional features skipping the evaluation of not-taken branches. This is not the case in the IR. Remember that one of our goals — in fact, the essence of ZK — is to reveal no more than just the statement’s validity; if two branches vary in length, then short-evaluating branches may leak some of the witness. Generally, this means that ZK backends must evaluate all branches, although some schemes can amortize this to the length of the longest branch.
Obviously evaluating all branches is not ideal because side effects in non-selected branches could cause program failures and unexpected behavior. To reduce the burden on ZK frontends to keep track of such side effects (e.g., advancing streams, and causing proof failures), the IR semantics disable them in non-selected branches. If the IR did not alleviate this burden, then ZK frontends would need to account for the side effects of non-taken branches and manually undo them in their relations.
Most IR directives (@and, @xor, @mul, etc, and even @call, etc.) don’t have side effects and have unchanged behavior within a non-selected branch.
However, three directives will cause side-effects which last beyond a branch.
The @assert_zero directive is the simplest effect to "cancel".
All it does is cause the prover to conditionally reject a proof, so it’s possible to change the condition such that it is always acceptable to the verifier by multiplying its input wire by either 0 or 1.
The @instance and @short_witness directives each consume a value from the instance or short witness (collectively input) streams.
This effect is harder to cancel, because if each case consumes a different number of values, different evaluations would need differently sized input streams.
Requiring differently sized streams reveals which case was taken, so this solution was rejected.
The next solution was to require inputs to contain sufficiently many values that the sum of all cases' input consumptions can be used, but this padding may require many extra values and is quite non-intuitive.
The solution we accepted is to require the switch to consume the maximum consumption of all cases, and repeat input values in each case.
In unselected cases, this means it likely processes garbage values, but the affects of any garbage would be disabled by the switch.
Here is an example of this in action, where we assume the instance and the short witness each assign three wire values.
@switch($0)
@case < 0 >: @anon_call(@instance: 3, @short_witness: 1)
$1 <- @instance;
$2 <- @instance;
$3 <- @instance;
$4 <- @short_witness;
$5 <- @add($1, $2);
$6 <- @add($3, $4);
$0 <- @add($5, $6);
@assert_zero($0);
@end
@case < 1 >: @anon_call(@instance: 1, @short_witness: 3)
$1 <- @instance;
$2 <- @short_witness;
$3 <- @short_witness;
$4 <- @short_witness;
$5 <- @mul($1, $2);
$6 <- @mul($3, $4);
$0 <- @mul($5, $6);
@assert_zero($0);
@end
@end
If the first case is taken, all instance values are "used", only one short witness value is "used", and the remaining short witness values are "discarded". If the second case is taken only one instance value is "used", all three short witness values are "used", and the remaining instance values are "discarded". However, in both cases the switch always consumes three instance values and three short witness values.
In the first case, it then asserts that the inputs sum to zero, while the second checks that the product of a different set of inputs is zero.
Assuming only one of these statements is true (and that the true one is the active branch), the @assert_zero in the non-active branch gets "disabled" by the ZK backend, for example, by multiplying by zero.
The "active" @assert_zero must similarly be "enabled", by multiplying by one.
For Loops
Now that we’ve understood function gates, a for loop is defined by a repetition of a function gate as its body over a prescribed range of repetitions. Here is an example that outputs the first 10 Fibonacci numbers.
$0 <- <1>;
$1 <- <1>;
$2 ... $10 <- @for i @first 2 @last 10
$i <- @anon_call($(i - 1), $(i - 2), @instance: 0, @short_witness: 0)
$0 <- @add($1, $2);
@end
@end
The above is equivalent to this sequence of function calls (although I did change from an anonymous to a named function, for succinctness):
@function(add_func, @out: 1, @in: 2, @instance: 0, @short_witness: 0) $0 <- @add($1, $2); @end $0 <- <1>; $1 <- <2>; $2 <- @call(add_func, $0, $1); $3 <- @call(add_func, $1, $2); $4 <- @call(add_func, $2, $3); $5 <- @call(add_func, $3, $4); $6 <- @call(add_func, $4, $5); $7 <- @call(add_func, $5, $6); $8 <- @call(add_func, $6, $7); $9 <- @call(add_func, $7, $8); $10 <- @call(add_func, $8, $9);
The loop itself assigns a list of output wires by repeating its body with an iterator (in the above example, i) that increments from a first to a last value.
The loop’s function gate allows a special syntax for the input and output wires (but not for wires within an anonymous function’s body, nor for the loop’s bounds and consumptions).
Namely, wire indices may be replaced by multiples and offsets of the loop’s iterator.
If this were not the case, then the function would uselessly repeat the same calculation and illegally reassign the same output wire.
The "iterator expression" syntax (for example, the input and output lists of the above for loop’s function) is used to express multiples and offsets of the iterator.
It may be composed of numeric constants and any in-scope loop iterators.
Allowed operations are addition (+), subtraction (-), multiplication (*) and division only by a constant (/).
There is no operator precedence, and all sub-expressions must be parenthesized.
For example, instead of writing $(48 + i - j * 5) you must use $(48 + (i - (j * 5))).
|
Note
|
Although wires use "remap" scoping where they must be passed as function-gate arguments, loop iterators follow lexical scoping rules. |
Example: Two’s Complement Calculator
Here’s an example that encapsulates what we’ve covered in this post. See the inline comments for explanation.
version 1.0.0;
field characteristic 2 degree 1;
relation
gate_set: boolean;
features: @function, @for, @switch;
@begin
@function(bit_adder, @out: 2, @in: 3, @instance: 0, @short_witness: 0)
// $0 is sum
// $1 is carry out
// $2 is a
// $3 is b
// $4 is carry out
// This is a 1-bit adder.
$5 <- @xor($2, $3);
$6 <- @xor($2, $4);
$7 <- @and($5, $6);
$1 <- @xor($7, $2);
$0 <- @xor($5, $4);
@end
// Lets fill the calculator ins/outs as follows
// $0 ... $31 will be the sum, Least-Significant-Bit (LSB) first, sign last
// $32 ... $63 input A, LSB-first, sign-last
$32 ... $63 <- @for i @first 0 @last 31
$(32 + i) <- @anon_call(@instance: 0, @short_witness: 1)
$0 <- @short_witness;
@end
@end
// $64 ... $95 input B, LSB-first, sign-last
$64 ... $95 <- @for i @first 0 @last 31
$(64 + i) <- @anon_call(@instance: 0, @short_witness: 1)
$0 <- @short_witness;
@end
@end
// $96 operation, 0 for add or 1 for subtract.
$96 <- @short_witness;
// $97 ... $28 are the adjusted input B
$97 ... $128 <- @switch($96)
@case <0>: @anon_call($64 ... $95, @instance: 0, @short_witness: 0)
// addition, don't adjust.
// $0 ... is the case's output mapping
// $32 ... is the case's input mapping
$0 ... $31 <- @for i @first 0 @last 31
$i <- @anon_call($(i + 32), @instance: 0, @short_witness: 0)
$0 <- $1;
@end
@end
@end
@case <1>: @anon_call($64 ... $95, @instance: 0, @short_witness: 0)
// subtraction, adjust by negating bits.
// $0 ... is the case's output mapping
// $32 ... is the case's input mapping
$0 ... $31 <- @for i @first 0 @last 31
$i <- @anon_call($(i + 32), @instance: 0, @short_witness: 0)
// don't adjust for addition.
$0 <- @not($1);
@end
@end
@end
@end
// Lets add it up now.
// $129 ... $160 can be carry bits.
// Carry in the operation (0=add, 1=sub) to finish the compliment.
$0, $129 <- @call(bit_adder, $32, $97, $96);
$1 ... $31, $130 ... $160 <- @for i @first 1 @last 31
$i, $(129 + i) <- @call(bit_adder, $(32 + i), $(97 + i), $(128 + i));
@end
// clean up the extra wires for adjusting and carry bits.
@delete($97, $128);
@delete($129, $159);
// And finally lets just assert that there was no overflow.
// (invert the overflow bit during subtraction)
$161 <- @xor($160, $96);
@assert_zero($161);
// And assert that the sum is as expected by the instance.
@for i @first 0 @last 31
@anon_call($i, @instance: 1, @short_witness: 0)
// $0: bit in sum
$1 <- @instance;
$2 <- @xor($0, $1);
@assert_zero($2);
@end
@end
@end
Concluding thoughts
We hope this introduction has given our readers an insight into the thought process and the mechanics of the SIEVE IR’s most recent revision. In upcoming posts we will take a look at some of what we like and dislike about this revision of the IR, to be concluded with our goals for and some of the mechanics we would like to see in the next revision.