halo2-repl

A browser interface for writing halo2 circuits in Javascript.

We've developed halo2-repl as a web browser interface to write halo2 circuits with Javascript bindings for halo2-lib. With halo2-repl, you can write your own ZK circuits, generate proving and verification keys, and generate proofs, all powered by WebAssembly bindings for halo2 in the browser. For technical discussion or collaboration, join the halo2-browser Telegram group.

Using halo2-repl

To write a ZK circuit with halo2-repl, you can use standard Javascript syntax and the allowed functions documented below. See the default circuit for an example. Once you've written a circuit, you can perform the following operations:

Test Circuit: Run a "mock proof" which fills in the constants and witnesses in your ZK circuit and generates the public input/outputs without actually generating a ZK proof. This should be used for testing purposes only.
Generate Keys: Generate proving and verification keys for your ZK circuit. Once generated, you can export the verification key under the Export tab.
Generate Proof: Actually generate the ZK proof. This requires Generate Keys to have been run. Once generated, you can download the proof under the Export tab.
Verify Proof: Verify the generated ZK proof against the verification key. At present, this step should always pass if both the proof and verification key have been generated.

You can also save and share your circuit as a Github Gist using the Save Gist button or using Ctrl-S.

Circuit Data Types

All variables inside halo2-repl are of type CircuitValue. A CircuitValue represents a 253-bit non-negative integer inside a single prime field element. Here are the methods available on a CircuitValue object:

class CircuitValue {
    // returns the value as a bigint
    value(): bigint;
    
    // returns the value as a number
    number(): number;
    
    // returns the value as an address string
    address(): string;
}

Circuit-Specific Functions

`witness`

This function creates a CircuitValue that can change between different runs of the circuit (think of it as a JavaScript let). For example, if you wanted to create a circuit that checks if a user's balance is above some threshold, you would make the user's address a witness so that the circuit could be used to prove that any address's balance is above the threshold.

/**
 * Creates a circuit variable from a number, bigint, or string.
 *
 * @param a - The raw circuit input.
 * @returns The witness cell.
 */
witness: (a: number | bigint | string) => CircuitValue;

`constant`

This function creates a CircuitValue that must be the same every time you run your circuit (think of it as JavaScript const). For example, from the example above, you could make the threshold a constant to enforce that everytime the circuit is run, the same threshold is used.

/**
 * Creates a circuit constant from a number, bigint, or string.
 *
 * @param a - The raw circuit input.
 * @returns The constant cell.
 */
constant: (a: number | bigint | string) => CircuitValue;

`log`

The log(...) function is used to debug the value of a CircuitValue (or some array of them). This is useful for debugging and checking that the values inside the circuit are what you would expect.

/**
 * Logs the provided *circuit* values to the console. 
 * Use `console.log` for normal logging.
 *
 * @param args - The values to log (can be `CircuitValue`s).
 */
log: (...args: (CircuitValue)[]) => void;

`makePublic`

This function is used to add values to the public input/output of the ZK circuit. You can call makePublic a maximum of 128 times inside halo2-repl.

/**
 * Adds a circuit value to the public input/output of the circuit. 
 *
 * @param a - The circuit value to add to the public input/output.
 */
makePublic: (a: CircuitValue) => void;

Compute Functions

The following compute functions are available to use in your ZK circuit. They are wrappers for the corresponding functions from halo2-lib.

/**
 * Adds two circuit values.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @returns The sum of the two circuit values.
 */
add: (a: CircuitValue, b: CircuitValue) => CircuitValue;

/**
 * Subtracts the second circuit value from the first circuit value.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @returns The difference between the two circuit values.
 */
sub: (a: CircuitValue, b: CircuitValue) => CircuitValue;

/**
 * Negates a circuit value.
 *
 * @param a - The circuit value to negate.
 * @returns The negation of the circuit value.
 */
neg: (a: CircuitValue) => CircuitValue;

/**
 * Multiplies two circuit values.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @returns The product of the two circuit values.
 */
mul: (a: CircuitValue, b: CircuitValue) => CircuitValue;

/**
 * Multiplies two circuit values and adds a third circuit value.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @param c - The third circuit value.
 * @returns The result of multiplying the first two circuit values and adding the third circuit value.
 */
mulAdd: (a: CircuitValue, b: CircuitValue, c: CircuitValue) => CircuitValue;

/**
 * Multiplies a circuit value by the negation of another circuit value.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @returns The result of multiplying the first circuit value by the negation of the second circuit value.
 */
mulNot: (a: CircuitValue, b: CircuitValue) => CircuitValue;

/**
 * Asserts that a circuit value is a bit.
 *
 * @param a - The circuit value to assert.
 */
assertBit: (a: CircuitValue) => void;

/**
 * Asserts that a circuit value is a constant.
 *
 * @param a - The circuit value to assert.
 * @param b - The raw value to compare to
 */
assertIsConst: (a: CircuitValue, b: number | bigint | string) => void;

/**
 * Computes the inner product of two arrays of circuit values.
 *
 * @param a - The first array of circuit values.
 * @param b - The second array of circuit values.
 * @returns The inner product of the two arrays.
 */
innerProduct: (a: CircuitValue[], b: CircuitValue[]) => CircuitValue;

/**
 * Computes the sum of an array of circuit values.
 *
 * @param arr - The array of circuit values.
 * @returns The sum of the array of circuit values.
 */
sum: (arr: CircuitValue[]) => CircuitValue;

/**
 * Performs an AND operation on two circuit values.
 * Assumes the CircuitValues are boolean.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @returns The a & b
 */
and: (a: CircuitValue, b: CircuitValue) => CircuitValue;

/**
 * Performs an OR operation on two circuit values.
 * Assumes the CircuitValues are boolean.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @returns a || b
 */
or: (a: CircuitValue, b: CircuitValue) => CircuitValue;

/**
 * Performs a NOT operation on a circuit value.
 *
 * @param a - The boolean circuit value.
 * @returns !a
 */
not: (a: CircuitValue) => CircuitValue;

/**
 * Decrements a circuit value by 1.
 *
 * @param a - The circuit value.
 * @returns a-1.
 */
dec: (a: CircuitValue) => CircuitValue;

/**
 * Selects a circuit value based on a condition.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @param c - The condition circuit value.
 * @returns The selected circuit value, given by c * a + (1 - c) * b
 */
select: (a: CircuitValue, b: CircuitValue, c: CircuitValue) => CircuitValue;

/**
 * Performs a OR-AND operation on three boolean circuit values.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @param c - The third circuit value.
 * @returns a || (b && c)
 */
orAnd: (a: CircuitValue, b: CircuitValue, c: CircuitValue) => CircuitValue;

/**
 * Converts an array of circuit values which are assumed to be bits to an 
 * indicator array.  The i_th returned circuit value is 1 if and only if 
 * i = (number represented by `bits` in little endian binary), and otherwise
 * it is 0.
 *
 * @param bits - The array of circuit values.
 * @returns The indicator array of circuit values.
 */
bitsToIndicator: (bits: CircuitValue[]) => CircuitValue[];

/**
 * Converts an index circuit value to a length `len` indicator array. The i_th
 * returned circuit value is 1 if and only if i == idx, and otherwise it is 0.
 *
 * @param idx - The index circuit value.
 * @param len - The length of the indicator circuit value.
 * @returns The indicator circuit value.
 */
idxToIndicator: (idx: CircuitValue, len: number | bigint | string) => CircuitValue[];

/**
 * Selects circuit values from an array based on an indicator array of circuit values.
 *
 * @param arr - The array of circuit values.
 * @param indicator - The indicator circuit values.
 * @returns The selected circuit value.
 */
selectByIndicator: (arr: CircuitValue[], indicator: CircuitValue[]) => CircuitValue;

/**
 * Selects a circuit value from an array based on an index circuit value.
 *
 * @param arr - The array of circuit values.
 * @param idx - The index circuit value.
 * @returns The selected circuit value.
 */
selectFromIdx: (arr: CircuitValue[], idx: CircuitValue) => CircuitValue;

/**
 * Checks if a circuit value is zero.
 *
 * @param a - The circuit value to check.
 * @returns The indicator circuit value representing whether the input is zero.
 */
isZero: (a: CircuitValue) => CircuitValue;

/**
 * Checks if two circuit values are equal.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @returns The indicator circuit value representing whether the two inputs are equal.
 */
isEqual: (a: CircuitValue, b: CircuitValue) => CircuitValue;

/**
 * Converts a circuit value to an array of bits.
 *
 * @param a - The circuit value to convert.
 * @param len - The length of the resulting bit array.
 * @returns The array of bits representing the input circuit value.
 */
numToBits: (a: CircuitValue, len: number | bigint | string) => CircuitValue;

/**
 * Asserts that two circuit values are equal.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 */
assertEqual: (a: CircuitValue, b: CircuitValue) => void;

/**
 * Checks if a circuit value is within a specified range.
 *
 * @param a - The circuit value to check.
 * @param b - The range of the circuit value, in number of bits.
 */
rangeCheck: (a: CircuitValue, b: number | bigint | string) => void;

/**
 * Asserts that the first circuit value is less than the second circuit value.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @param c - The bit range of the circuit values. Defaults to 253.
 */
checkLessThan: (a: CircuitValue, b: CircuitValue, c?: string) => void;

/**
 * Checks if the first circuit value is less than the second circuit value.
 *
 * @param a - The first circuit value.
 * @param b - The second circuit value.
 * @param c - The bit range of the circuit values. Defaults to 253.
 * @returns 1 if a < b, else 0
 */
isLessThan: (a: CircuitValue, b: CircuitValue, c?: string) => CircuitValue;

/**
 * Divides two circuit values and returns the quotient.  
 *
 * @param a - The dividend circuit value.
 * @param b - The divisor circuit value.
 * @param c - The bit range of `a`. Defaults to 253 bits.
 * @param d - The bit range of `b`. Defaults to 253 bits.
 * @returns The quotient.
 *
*/
div: (a: CircuitValue, b: CircuitValue, c?: string, d?: string) => CircuitValue;

/**
 * Divides two circuit values and returns the remainder.
 *
 * @param a - The dividend circuit value.
 * @param b - The divisor circuit value.
 * @param c - The bit range of `a`. Defaults to 253 bits.
 * @param d - The bit range of `b`. Defaults to 253 bits.
 * @returns The remainder.
 *
*/
mod: (a: CircuitValue, b: CircuitValue, c?: string, d?: string) => CircuitValue;

/**
 * Raises a circuit value to the power of another circuit value.
 *
 * @param a - The base circuit value.
 * @param b - The exponent circuit value.
 * @param c - The bit range of b. Defaults to 253 bits.
 * @returns The result of the exponentiation.
 */
pow: (a: CircuitValue, b: CircuitValue, c?: string) => CircuitValue;

/**
 * Computes the Poseidon hash of multiple circuit values.
 *
 * @param args - The circuit values to hash.
 * @returns The hash value.
 */
poseidon: (...args: CircuitValue[]) => CircuitValue;

/**
 * Retrieves the value of a circuit value.
 *
 * @param a - The circuit value.
 * @returns The value of the circuit value.
 */
value: (a: CircuitValue) => bigint;

PreviousGetting Started with Halo2

Last updated 1 year ago