# Non-Deterministic Witness (`non-det-wit`

)

## Summary and Usage

The Non-Deterministic Witness (NDW) detector warns the user about non-deterministic witness code (i.e., dataflow operations) in their ZK circuit, which occurs when dataflow is dependent on conditional branches or conditional assignments. Conditional assignments are difficult to properly constrain and likely to lead to unconstrained values, which can lead to significant security risks as unconstrained values could allow for the construction of bogus proofs.

### Usage

The NDW detector is invoked by selecting "Non-deterministic dataflow"
(`non-det-wit`

) in the Detector selection during the tool configuration step.

## Example and Explanation

The following circuit is designed to determine whether the input `in`

is 0 or not.
If `in = 0`

, then `out = 1`

.
For any other value of `in`

where `in != 0`

, then `out = 0`

.

`pragma circom 2.0.0;`

template IsZero() {

signal input in;

signal output out;

signal inv;

inv <-- in!=0 ? 1/in : 0; // conditional expression in inv assignment

out <== -in*inv +1;

}

component main = IsZero();

To implement this functionality, the circuit first computes the inverse `inv`

of the input `in`

, but uses a conditional assignment such that `inv`

will be 0
if `in`

is 0, with `inv = 1/in`

otherwise (line 9).
With this conditional assignment, it follows thaat the value of `-in*inv`

should be
-1 (mod p) if `in`

is non-zero, and 0 otherwise.
Therefore, the computation and assignment of `out <== -in*inv + 1`

should be
1 if `in`

is 0, and 0 if `in`

is non zero.

However, this code has a bug: there is no constraint that requires `out`

to be a boolean
value (i.e., 0 or 1).
`out`

being boolean a consequence of `inv`

being the inverse of `in`

, which
is *not* a constraint in this circuit due to the use of the conditional assignment
used to create `inv`

.
This allows a malicious actor to set `inv`

to be any value independent of `in`

as
long as the `out <== -in*inv +1`

constraint is satisfied.
The witness assignment of `in = 1`

, `inv = -1 (mod p)`

, and `out = 2`

would therefore
satisfy the circuit's constraints, but violates the intended output of the circuit,
which is that if `in = 1`

, `out`

should be `0`

.

This example demonstrates that conditional assignments often require additional and more nuanced constraints than normal unconditional assignments may require. These challenges are why the NDW detector can be a useful tool in flagging conditional logic for further scrutiny.

This example is adapted from the `IsZero`

circuit provided by circomlib.
However, unlike our above example, the version in circomlib (found in comparators.circom) is properly constrained:

`template IsZero() {`

signal input in;

signal output out;

signal inv;

inv <-- in!=0 ? 1/in : 0;

out <== -in*inv +1;

in*out === 0;

}

The addition of the `in*out === 0`

constraint on line 13 fixes the issue pointed out in
our example, as it forces one of `in`

and `out`

to be 0.

## Usage Example

Running the above example circuit in ZK Vanguard using the `non-det-wit`

detector yields
the following output text log:

## ZK Vanguard Output

`----Running Vanguard with non-det-wit detector----`

Running detector: non-det-wit

[Critical] Found signal in component that are used in conditional expressions IsZero @ non_det_wit_bug.circom:3

Reported By: vanguard:non-det-wit

Location: IsZero @ non_det_wit_bug.circom:3

Confidence: 0.99

More Info: placeholder

Details:

Found signal in component that are used in conditional expressions IsZero @ non_det_wit_bug.circom:3

* Signal in in expression IsZero @ non_det_wit_bug.circom:9

Line 3 of the above log tells us that the NDW detector has found a signal that is used in a conditional expression.
Lines 9–10 of the above log tell us that the input signal `in`

is being used in a conditional expression on
line 9 of `non_det_wit_bug.circom`

, which is the assignment `inv <-- in!=0 ? 1/in : 0`

.
This finding tells us we need to confirm that `inv`

and `in`

are sufficiently constrained
given the conditional assignment.

## Limitations

The NDW detector flags conditional expressions and the signals used in those conditional expressions,
but is unable to determine if the conditional expressions are properly constrained or not,
as this requires knowledge of what the design goal of the circuit is.
For example, the NDW detector would still report the same issue for circomlib's `IsZero`

circuit, even
though it is properly constrained.

## Assesing Severity

The severity of a non-deterministic witness computation depends heavily on whether or not the involved signals have been properly constrained according to the design of the circuit. Assuming that the finding is not a false positive, then the consequences can be severe, as the verifier may accept a proof with signal assignments outside of what is intended, allowing malicious users to prove invalid statements.