Introduction

A "shifted value index" is basically an XOR-of-shifts of prover data elements. The number of things XOR'd, the indices of these elements, and finally the shift amounts and directions, are all "known at compile time" (hardcoded into the constraint system). Only the actual public and witness prover elements upon which these indices act arise at "runtime".

Both our public data and our witness data are just long lists of 64-bit words. A shifted value index is an XOR-of-shifts of elements of this prover data, like e.g.:

w[123] << 44 ^ w[456] ~>> 55 ^ w[789] >> 3.

We allow logical left shifts (<<), logical right shifts (>>), and arithmetic right shifts (~>>). Here, we write w for the prover's witness data. Actually it's more accurate to think of w as the concatenation of the prover's public (input–output) data and his witness data. The numbers above (123, 44, etc.) should be thought of as fixed in advance; the actual values of w (at the positions w[123], etc.) will be runtime-dependent.

Constraints

We describe our constraint system language more formally in the AND constraints and MUL constraints pages. Here, we drop a sketch of what's to come.

An AND constraint demands that a & b == c, where each of the three operands $a$, $b$ and $c$ are shifted value indices. Here, & is bitwise AND of 64-bit words.

For example, let's say we have a = w[123] << 44 ^ w[456] ~>> 55, b = w[111] ^ w[444] >> 4, and c = w[777]. When we assert the constraint a & b == c, we're asserting: Whatever the prover's witness $w$ is, it should satisfy

(w[123] << 44 ^ w[456] ~>> 55) & (w[111] ^ w[444] >> 4) == w[777].

Everything above is hardcoded into the constraint system except the witness w itself; i.e., all the indices and shift amounts are hardcoded. It'll be the prover's job to supply a witness $w$ for which the above thing actually holds. Note that both sides of the above equality are 64-bit words.

Each particular assertion of this form makes up an AND constraint; we allow there to be arbitrarily many AND constraints.

MUL constraints are similar, except that instead of bitwise AND we have unsigned multiplication of 64-bit integers. The result is double-width; those constraints take the form a * b == hi || lo, where hi and lo are themselves further shifted value indices. Here, we're saying that the shifted value indices hi and lo should yield the high and low halves, respectively, of a * b.