/ circuit / goldilocks.circom
goldilocks.circom
  1  
  2  pragma circom 2.2.0;
  3  
  4  include "field_params.circom";
  5  include "goldilocks_func.circom";
  6  include "misc.circom";
  7  
  8  //------------------------------------------------------------------------------
  9  
 10  // a type for bit-decomposed numbers
 11  // the invariant to respect is that the value is in the range [0..2^n-1]
 12  //
 13  bus Binary(n) {
 14    signal val;
 15    signal bits[n];
 16  }
 17  
 18  // the type of Goldilocks field elements.
 19  // the invariant to respect is that the value is in the range [0..P-1]
 20  //
 21  bus Goldilocks() {
 22    signal val;
 23  }
 24  
 25  //------------------------------------------------------------------------------
 26  
 27  // n-bit binary decomposition
 28  template ToBinary(n) {
 29    signal input  inp;
 30    output Binary(n) out;
 31  
 32    component tobits = ToBits(n);
 33    tobits.inp <== inp;
 34    tobits.out ==> out.bits;
 35    inp        ==> out.val;
 36  }
 37  
 38  //------------------------------------------------------------------------------
 39  
 40  //
 41  // do a range check for [0,P-1] where `P = 2^64 - 2^32 + 1`
 42  //
 43  
 44  template ToGoldilocks() {
 45    signal input  inp;
 46    output Goldilocks() out;
 47  
 48    // first we do a range check and bit decomposition to 64 bits
 49  
 50    var nbits = SolinasExpoBig();
 51    Binary(nbits) bin <== ToBinary(nbits)( inp );
 52  
 53    // compute the low and high 32 bit words
 54  
 55    var sum_lo = 0;
 56    for(var i=0; i < SolinasExpoSmall(); i++) {
 57      sum_lo += (2**i) * bin.bits[i];
 58    }
 59  
 60    var expo_jump = SolinasExpoBig() - SolinasExpoSmall();
 61  
 62    var sum_hi = 0;
 63    for(var i=0; i < expo_jump; i++) {
 64      sum_hi += (2**i) * bin.bits[ SolinasExpoSmall() + i ];
 65    }
 66  
 67    // now, since we have p-1 = 2^64 - 2^32 = 0xff...ff00...00
 68    //
 69    // we need to check that IF hi == 2^32-1 THEN lo == 0
 70  
 71    signal iseq <== IsEqual()( sum_hi , 2**expo_jump - 1 );
 72  
 73    iseq * sum_lo === 0;           // either (hi < 2^32-1) OR (lo == 0)
 74  
 75    out.val <== bin.val;
 76  }
 77  
 78  //------------------------------------------------------------------------------
 79  
 80  // reduce numbers in the range `0 <= x < 2^k * P` modulo P
 81  template ReduceModP(k) {
 82    signal input inp;
 83    output Goldilocks() out;
 84  
 85    var P = FieldPrime();
 86  
 87    signal quot <-- inp \ P;
 88    signal rem  <-- inp % P;
 89  
 90    // check that `quot` is in a `k` bit range!
 91    component bits = ToBits( k );
 92    bits.inp <== quot;                             
 93  
 94    inp === rem + P * quot;          // check the multiplication equation
 95    out <== ToGoldilocks()(rem);     // range check on the output
 96  }
 97  
 98  //------------------------------------------------------------------------------
 99  
100  //
101  // negation in the Goldilocks field
102  //
103  
104  template Neg() {
105    input  Goldilocks() A;
106    output Goldilocks() C;
107  
108    signal isz <== IsZero()( A.val );
109  
110    C.val <== (1 - isz) * (FieldPrime() - A.val);
111  }
112  
113  //--------------------------------------
114  
115  //
116  // addition in the Goldilocks field
117  //
118  
119  template Add() {
120    input  Goldilocks() A,B;
121    output Goldilocks() C;
122  
123    var P = FieldPrime();
124  
125    // A + B = C + P * bit
126  
127    var overflow = (A.val + B.val >= P);
128  
129    signal quot <-- (overflow ? 1 : 0);
130    signal rem  <-- A.val + B.val - quot * P;
131  
132    quot*(1-quot) === 0;                   // `quot` must be either zero or one
133    A.val + B.val === rem + P * quot;      // check the addition
134    C <== ToGoldilocks()(rem);             // range check on C
135  }
136  
137  //
138  // subtraction in the Goldilocks field
139  //
140  
141  template Sub() {
142    input  Goldilocks() A,B;
143    output Goldilocks() C;
144  
145    var P = FieldPrime();
146  
147    // A - B = C - P * bit
148  
149    var overflow = (A.val - B.val < 0);
150  
151    signal aquot <-- (overflow ? 1 : 0);         // absolute value of the quotient
152    signal rem   <-- A.val - B.val + aquot * P;
153  
154    aquot*(1-aquot) === 0;                       // `aquot` must be either zero or one
155    A.val - B.val === rem - P * aquot;           // check the subtraction
156    C <== ToGoldilocks()(rem);                   // range check on C
157  }
158  
159  //------------------------------------------------------------------------------
160  
161  //
162  // summation in the Goldilocks field
163  //
164  
165  template Sum(k) {
166    input  Goldilocks() A[k];
167    output Goldilocks() C;
168  
169    // sum A[i] = C + P * Q
170    // since all A[i] < 2^64, Q will have at most as many bits as `k` have
171    // so we can do a simple binary range-check on Q
172  
173    var sum = 0;
174    for(var i=0; i<k; i++) { sum += A[k].val; }
175  
176    C <== ReduceModP( CeilLog2(k) )( sum ); 
177  }
178  
179  //------------------------------------------------------------------------------
180  
181  //
182  // multiplication in the Goldilocks field
183  //
184  
185  template Mul() {
186    input  Goldilocks() A,B;
187    output Goldilocks() C;
188  
189    // A * B = C + P * Q
190  
191    C <== ReduceModP( SolinasExpoBig() )( A.val * B.val ); 
192  }
193  
194  //
195  // multiplication of 3 Goldilocks field elements
196  // as this still fits into 192 < 254 bits, we can do it a bit more efficiently
197  // than two multiplications.
198  //
199  
200  template Mul3() {
201    input  Goldilocks() A,B,C;
202    output Goldilocks() D;
203  
204    // A * B * C = D + P * Q
205  
206    signal AB <== A.val * B.val;
207  
208    D <== ReduceModP( 2 * SolinasExpoBig() )( AB * C.val ); 
209  }
210  
211  //--------------------------------------
212  
213  // Squaring (this is more interesting in the extension field case)
214  //
215  template Sqr() {
216    input  Goldilocks() A;
217    output Goldilocks() C;
218    C <== Mul()( A , A );
219  }
220  
221  //------------------------------------------------------------------------------
222  
223  //
224  // inversion in the Goldilocks field
225  // (maybe this could be optimized a bit?)
226  // 
227  
228  template Inv() {
229    input  Goldilocks() A;
230    output Goldilocks() C;
231  
232    // guess the result, and range-check it
233    signal candidate <-- goldilocks_inv(A.val);
234    C <== ToGoldilocks()(candidate);
235  
236    // is A = 0?
237    signal isz <== IsZero()(A.val);
238  
239    // multiply back, and check the equation (but only when A != 0)
240    Goldilocks() AC <== Mul()( A , C );
241    (1 - isz) * (AC.val - 1) === 0;
242  
243    // if A=0, we have to enforce C=0 too
244    isz * C.val === 0;
245  }
246  
247  //
248  // division in the Goldilocks field
249  // (maybe this could be optimized a bit?)
250  //
251  
252  template Div() {
253    input  Goldilocks() A,B;
254    output Goldilocks() C;
255  
256    // guess the result, and range-check it
257    signal candidate <-- goldilocks_div(A.val, B.val);
258    C <== ToGoldilocks()(candidate);
259  
260    // is B = 0?
261    signal isz <== IsZero()(B.val);
262   
263    // multiply back, and check the equation (but only when B != 0)
264    Goldilocks() BC <== Mul()( B , C );
265    (1 - isz) * (BC.val - A.val) === 0;
266  
267    // if B=0, we have to enforce C=0 too
268    isz * C.val === 0;
269  }
270  
271  //------------------------------------------------------------------------------