# Basic Math Constraints

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](https://github.com/iden3/circomlib/blob/master/circuits/gates.circom)

Logical gates are, [according to Wikipedia](https://en.wikipedia.org/wiki/Logic_gate):

> an idealized or physical device implementing a [Boolean function](https://en.wikipedia.org/wiki/Boolean_function), a [logical operation](https://en.wikipedia.org/wiki/Logical_operation) performed on one or more [binary](https://en.wikipedia.org/wiki/Binary_number) inputs that produces a single binary output.&#x20;

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()`](https://github.com/iden3/circomlib/blob/master/circuits/gates.circom#L37-L43) 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](https://learn.microsoft.com/en-us/cpp/cpp/logical-or-operator-pipe-pipe?view=msvc-170#:~:text=Logical%20OR%20operator%3A%20%7C%7C\&text=The%20logical%20OR%20operator%20\(%20%7C%7C,left%2Dto%2Dright%20associativity.).

We can see the implementation of the `OR()` gate component in [`shot.circom`](https://github.com/BattleZips/BattleZips/blob/master/zk/circuits/shot.circom#L51-L63) from the BattleZips V1 codebase (abridged):&#x20;

```
.
.
.
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()`](https://github.com/iden3/circomlib/blob/master/circuits/gates.circom#L68) so we four `OR()` components together to reach a single boolean value representing whether or not any ships collide with the shot.

## [Comparators](https://github.com/iden3/circomlib/blob/master/circuits/comparators.circom)

[Wikipedia defines a comparator as](https://en.wikipedia.org/wiki/Digital_comparator) a function:

> that takes two numbers as input in [binary](https://en.wikipedia.org/wiki/Binary_numeral_system) 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()`](https://github.com/iden3/circomlib/blob/master/circuits/comparators.circom#L48-L57) (which relies on the simple [`IsZero()`](https://github.com/iden3/circomlib/blob/master/circuits/comparators.circom#L24-L34) 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`](https://github.com/BattleZips/RollupNC/blob/master/zk/circuits/helpers/if_gadgets.circom#L50-L66) in the BattleZips RollupNC repository via [`IfBothHighForceEqualEnabled()`](https://github.com/BattleZips/RollupNC/blob/master/zk/circuits/helpers/if_gadgets.circom#L50-L66):

```
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`](https://github.com/BattleZips/RollupNC/blob/master/zk/circuits/update_state_verifier.circom#L107-L112) 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](https://github.com/iden3/circomlib/blob/master/circuits/bitify.circom)

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`](https://github.com/iden3/circomlib/blob/243d2ec4fc9855780632fc498d24415b5534019f/circuits/eddsamimc.circom#L43-L52) 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`](https://github.com/BattleZips/BattleZips/blob/master/zk/circuits/templates/placeShip.circom) component used in the main [`board.circom`](https://github.com/BattleZips/BattleZips/blob/master/zk/circuits/board.circom) componnt (abridged to only show state change basics):

<details>

<summary>BattleZips use of Num2Bits</summary>

```
// 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;
}
```

</details>

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.&#x20;


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://battlezips.gitbook.io/battlezips/development/circomlib/basic-math-constraints.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.
