> For the complete documentation index, see [llms.txt](https://validium.gitbook.io/docs/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://validium.gitbook.io/docs/components/prover/boojum-function-check_if_satisfied.md).

# Boojum Function - \`check\_if\_satisfied\`

***

*Note: Please read our other documentation and tests first before reading this page.*

Our circuits (and tests) depend on a function from Boojum called [`check_if_satisfied`](https://github.com/matter-labs/era-boojum/blob/main/src/cs/implementations/satisfiability_test.rs#L11). You don’t need to understand it to run circuit tests, but it can be informative to learn more about Boojum and our proof system.

First we prepare the constants, variables, and witness. As a reminder, the constants are just constant numbers, the variables circuit columns that are under PLONK copy-permutation constraints (so they are close in semantics to variables in programming languages), and the witness ephemeral values that can be used to prove certain constraints, for example by providing an inverse if the variable must be non-zero.

![Check\_if\_satisfied.png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied.png)

Next we prepare a view. Instead of working with all of the columns at once, it can be helpful to work with only a subset.

![Check\_if\_satisfied(1).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-1.png)

Next we create the paths\_mappings. For each gate in the circuit, we create a vector of booleans in the correct shape. Later, when we traverse the gates with actual inputs, we’ll be able to remember which gates should be satisfied at particular rows by computing the corresponding selector using constant columns and the paths\_mappings.

![Check\_if\_satisfied(2).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-2.png)

Now, we have to actually check everything. The checks for the rows depend on whether they are under general purpose columns, or under special purpose columns.

**General purpose rows:**

For each row and gate, we need several things.

* Evaluator for the gate, to compute the result of the gate
* Path for the gate from the paths\_mappings, to locate the gate
* Constants\_placement\_offset, to find the constants
* Num\_terms in the evaluator
  * If this is zero, we can skip the row since there is nothing to do
* Gate\_debug\_name
* num\_constants\_used
* this\_view
* placement (described below)
* evaluation function

![Check\_if\_satisfied(3).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-3.png)

Placement is either UniqueOnRow or MultipleOnRow. UniqueOnRow means there is only one gate on the row (typically because the gate is larger / more complicated). MultipleOnRow means there are multiple gates within the same row (typically because the gate is smaller). For example, if a gate only needs 30 columns, but we have 150 columns, we could include five copies for that gate in the same row.

Next, if the placement is UniqueOnRow, we call evaluate\_over\_general\_purpose\_columns. All of the evaluations should be equal to zero, or we panic.

![Check\_if\_satisfied(4).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-4.png)

If the placement is MultipleOnRow, we again call evaluate\_over\_general\_purpose\_columns. If any of the evaluations are non-zero, we log some extra debug information, and then panic.

![Check\_if\_satisfied(7).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-7.png)

This concludes evaluating and checking the generalized rows. Now we will check the specialized rows.

![Check\_if\_satisfied(8).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-8.png)

We start by initializing vectors for specialized\_placement\_data, evaluation\_functions, views, and evaluator\_names. Then, we iterate over each gate\_type\_id and evaluator.

![Check\_if\_satisfied(9).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-9.png)

If gate\_type\_id is a LookupFormalGate, we don’t need to do anything in this loop because it is handled by the lookup table. For all other cases, we need to check the evaluator’s total\_quotient\_terms\_over\_all\_repetitions is non-zero.

![Check\_if\_satisfied(11).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-11.png)

Next, we get num\_terms, num\_repetitions, and share\_constants, total\_terms, initial\_offset, per\_repetition\_offset, and total\_constants\_available. All of these together form our placement data.

![Check\_if\_satisfied(12).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-12.png)

![Check\_if\_satisfied(13).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-13.png)

Once we know the placement\_data, we can keep it for later, as well as the evaluator for this gate.

![Check\_if\_satisfied(14).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-14.png)

We also will keep the view and evaluator name. This is all the data we need from our specialized columns.

To complete the satisfaction test on the special columns, we just need to loop through and check that each of the evaluations are zero.

![Check\_if\_satisfied(16).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-16.png)

![Check\_if\_satisfied(17).png](https://docs.zksync.io/_ipx/q_90/images/zk-stack/Check_if_satisfied-17.png)

Now we have checked every value on every row, so the satisfaction test is passed, and we can return true.

<br>
