Basic Math Constraints

Constraining validity of basic logical and arithmetic computations made in zero knowledge

You can perform basic arithmetic operations as expected to variables in the Circom language. However, ensuring the circuit constrains execution according to a specified calculation with target signal values requires boilerplate code. The following libraries provide the patterns you need to accomplish these goals.

Gates

Logical gates are, according to Wikipedia:

an idealized or physical device implementing a Boolean function, a logical operation performed on one or more binary inputs that produces a single binary output.

An in exhaustive list of gate operands you may be used to: ||, &&, !

You would extend one of the gates.circom components when you want to constrain the circuit to only generate a valid proof if one of these logical assertions holds true. For instance, take the OR() component:

template OR() {
    signal input a;
    signal input b;
    signal output out;

    out <== a + b - a*b;
}

By using the OR() component, we assume a and b input signals are binary. We can use the out ouput signal with confidence that it is a constrained binary evaluation of the || operator.

We can see the implementation of the OR() gate component in shot.circom from the BattleZips V1 codebase (abridged):

.
.
.
component or;
ors[0] = OR();
ors[0].a <== _hit[0];
ors[0].b <== _hit[1];
_ors[0] <== ors[0].out;
.
.
.

In this snippet, in our shot proof we are checking whether or not the publicly inputted shot x/y coordinate pair collides with the privately inputted board arrangement (specifically the first and second ships). circomlib did not include a MultiOR() as it does with MultiAND() so we four OR() components together to reach a single boolean value representing whether or not any ships collide with the shot.

Comparators

Wikipedia defines a comparator as a function:

that takes two numbers as input in binary form and determines whether one number is greater than, less than or equal to the other number

An in exhaustive list of gate operands you may be used to: >=, ==, !=, >

For example, let us take the toggled equality comparator component ForceEqualIfEnabled() (which relies on the simple IsZero() comparator component):

template ForceEqualIfEnabled() {
    signal input enabled;
    signal input in[2];

    component isz = IsZero();

    in[1] - in[0] ==> isz.in;

    // no proof for your circuit can be computed with inputs that fail this check
    // **proof malleability**
    // circuit execution with failed inputs would halt here
    (1 - isz.out)*enabled === 0; 
}

We can see the implementation of ForceEqualIfEnabled() in if_gadgets.circom in the BattleZips RollupNC repository via IfBothHighForceEqualEnabled():

template IfBothHighForceEqual() {
    // check if these are both high, if so constrain equality on a and b
    signal input check1;
    signal input check2;

    signal input a;
    signal input b;

    component allHigh = AllHigh(2);
    allHigh.in[0] <== check1;
    allHigh.in[1] <== check2;

    component equalIf = ForceEqualIfEnabled();
    equalIf.in[0] <== a;
    equalIf.in[1] <== b;
    equalIf.enabled <== allHigh.out;
}

IfHighForceEqualIfEnabled() in RollupNC demonstrates constrained conditional computation and evaluation of state by an equality comparator.

A "high" signal value is a value >= 1. In the context of RollupNC, update_state_verifier.circom contains a check if a transaction's send and receipt token type are the same or not. I

• If toTokenType and fromTokenType are equal, debit from to and credit to from

• If fromTokenType is 0, debit from to but do not debit from burn address

• If from is not 0x00 address or fromTokenType is not 0 and does not match toTokenType, fail verification at unrelated point

Bitify

For many reasons, you may need to access the bits that compose an integer value contained in a signal. In low level cryptographic applications this can be seen in the eddsa.circom template:

.
.
.
component snum2bits = Num2Bits(253);
snum2bits.in <== S;

component  compConstant = CompConstant(2736030358979909402780800718157159386076813972158567259200215660948447373040);

for (i=0; i<253; i++) {
   snum2bits.out[i] ==> compConstant.in[i];
}
compConstant.in[253] <== 0;
compConstant.out === 0;
.
.
.

This may be incredibly confusing, but that is okay! Using the circomlibjs library abstracts away the worst of the cryptographic expertise needed. Alternatively, lets look at another simple use-case for num2bits in the BattleZips V1 placeShip.circom component used in the main board.circom componnt (abridged to only show state change basics):

BattleZips use of Num2Bits

// n is the length of the ship expected (not checked) in range [2, 5]
template PlaceShip(n) {

    signal input boardIn; // board state in single signal before placement
    signal input ship[3]; // x, y, z of ships
    signal output boardOut; // board state in single signal after placement
    
    component toBits = Num2Bits(100); // turns numerical board to bitmap
    component boardMux = Mux1(); // select board to return
    component toNumH = Bits2Num(100); // horizontal board Bits2Num
    component toNumV = Bits2Num(100); // vertical board Bits2Num
    
    .
    .
    .
    
    /// DECODE BOARD SIGNAL INTO BITMAP SIGNAL ARRAY ///
    // store decoded board state in variables for conditional computation
    toBits.in <== boardIn; // turn integer signal into 100 binary singals
    var boardH[10][10]; 
    for (var i = 0; i < 100; i++) {
        boardH[i \ 10][i % 10] = toBits.out[i];
    }
    var boardV[10][10] = boardH;
    
    .
    .
    .
    
    /// ENCODE BOARD BITMAP SIGNAL ARRAY INTO SINGLE SIGNAL ///
    for (var i = 0; i < 100; i++) {
        toNumH.in[i] <-- boardH[i \ 10][i % 10];
        toNumV.in[i] <-- boardV[i \ 10][i % 10];
    }
    
    // mux boards to get next state
    boardMux.c[0] <== toNumH.out;
    boardMux.c[1] <== toNumV.out;
    boardMux.s <== ship[2];
    boardOut <== boardMux.out;
}

In the Solidity verifier contract generated for you by SnarkJS, each additional input incurs additional gas cost in the EVM. This demonstrates a straight-forward use of the bitify.circom component file to accomplish state computation in Zero Knowledge as effectively as presently possible given these tools.