> For the complete documentation index, see [llms.txt](https://battlezips.gitbook.io/battlezips/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://battlezips.gitbook.io/battlezips/development/circomlib/basic-math-constraints.md). # 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. 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): ``` . . . 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):
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.