[Bug] Under-constraint output signal & circomlib misuse

[Mag041108]

I noticed several possible bugs/inappropriate practices in circuit/templates/helpers/jwt/BracketsDepthMap.circom (commit 2710c87).

1. out[0] is never assigned or constrained

Description: out[0] is never assigned or constrained. A prover can set out[0] arbitrarily.

Fix: In fact, out[0] should always be 0, so a constraint out[0] === 0; can be added.

2. Circom computation is calculated on finite field

Description: In Circom, all computations are performed over a finite field, which means all values are actually non-negative integers from 0 to
p - 1, and p is the prime number of that finite field. If prelim_out1[i] = 0, consider prelim_out2[i] <== prelim_out1[i]-1;, and prelim_out2[i] will be p-1 rather than -1.

3. Incorrect sign check with LessThan

Description: Here is the implication of LessThan: https://circom.erhant.me/comparators/
The BracketsDepthMap code tries to detect negative values via LessThan(20)([prelim_out2[i], 0]). LessThan enforce that inputs are in [0, 2^n). They do not support negative values. So when prelim_out2[i] = -1 in Real field, it actually be p - 1 in circom field, and making “is_neg” effectively always 0.

Fix: Check if prelim_out2[i] === p-1; may be fine.