Audit of Linea's gnark std
May 20th, 2024

Description. multicommitter collects variables from multiple functions and commits them with underlying Committer to get the initial commitment $c$. Then it derives the commitment for all the functions by continuously squaring: $c \leftarrow {c}^2$.

func (mct *multicommitter) commitAndCall(api frontend.API) error {
    ...
    cmt, err := commiter.Commit(mct.vars...)
    ...
    for i := 1; i < len(mct.cbs); i++ {
        // cmt <-- cmt * cmt
        cmt = api.Mul(cmt, cmt)
        if err := mct.cbs[i](api, cmt); err != nil {
            return fmt.Errorf("callback %d: %w", i, err)
        }
    }
    return nil
}

The way it derives the commitement is not binding. This will make the fiat-shamir transformation not sound.

One observation is that: in prime field $\mathbb{F}_p$, for some $c$ the following sequence will converge to $1$:

$c, c^2, c^4, c^8, \ldots, c^{2^i}, c^{2^{i+1}}, \ldots$

This is because if $c^{2^i} \equiv 1 \mod p$ then $c^{2^{i+1}} \equiv 1 \mod p$.

This means if there are many $c$ in $\mathbb{F}_p$ that makes the sequence converge to $1$, the attacker can easily find two different inputs both committed to $1$. This will make multicommitter lose binding.

Now let's see in $\mathbb{F}_p$ how many $c$ will eventually converge to $1$ in the sequence: $c, c^2, c^4, c^8, \ldots, c^{2^i}, c^{2^{i+1}}, \ldots$

Denote $g$ as the generator in $\mathbb{F}_p$. Then $g^{p-1} \equiv 1 \mod p$. Then $c = g^k$ for some $k$. We have:

$c^{2^n} = (g^{k})^{2^n} = g^{k \cdot 2^n}$

Suppose the sequence converge to $1$ at $n$:

$c^{2^n} \equiv g^{k \cdot 2^n} \equiv 1 \mod p$

This means $p-1$ divides $k \cdot 2^n$:

$(p-1) \mid k \cdot 2^n$

Factorize $p-1$ as $a \cdot 2^m$, with $m$ being the largest possible value. If $a \mid k$, then $a\cdot 2^m \mid k \cdot 2^n$ for $m \le n$, implying that $(p-1) \mid k \cdot 2^n$ and $g^{k \cdot 2^n} \equiv 1 \mod p$. This means the sequence converges to $1$ if and only if $a \mid k$. Consequently, if $a \mid k$, the sequence converges to $1$ in at most $m$ steps.

In $\mathbb{F}_p$, there are approximately $p/a$ elements divisible by $a$. If one randomly chooses an element in $\mathbb{F}_p$, the probability that the element is divisible by $a$ (i.e., the sequence converges to $1$) is $1/a$.

For some prime fields, $1/a$ is non-negligible. For instance, gnark supports the Stark Curve, where $p = 2^{251} + 17 \cdot 2^{192} + 1$. Consequently, $p-1 = 2^{192} \cdot (2^{59} + 17)$, which means $a = 2^{59} + 17$ and $m = 192$. Suppose the circuit makes $192$ calls to the multicommitter. Then, an attacker could find two different inputs, both committed to $1$ in the 192nd call, in $O(2^{59} + 17)$ attempts.

This indicates that in some prime fields, the multicommitter is not binding.

Recommendation: Avoid using a squaring sequence. Consider using $c^i$ to derive the sequence.

Client Response. https://github.com/Consensys/gnark/pull/1212

Description. The Partition() function partitions a value v into two parts (a lower part and an upper part) at a specific bit offset. In order to be sound, the following should hold:

1. $v = lower + 2^{split} \times upper$.
2. $lower < 2^{split}$.
3. $upper < 2^{split'}$, where $split'=nbScalar-split$.

Unfortunately, in the implementation the upper part is incorrectly constrained to be $upper < 2^{nbScalar}$. Then any lower and upper pairs that satisfy the first two constraints will pass the check. Thus, the implementation is not sound.

func Partition(api frontend.API, v frontend.Variable, split uint, opts ...Option) (lower, upper frontend.Variable) {
    ...
    upperBound := api.Compiler().FieldBitLen()
    if opt.digits > 0 {
        upperBound = opt.digits
    }
    // incorrect constraint here
    rh.Check(upper, upperBound)
    rh.Check(lower, int(split))

    m := big.NewInt(1)
    m.Lsh(m, split)
    composed := api.Add(lower, api.Mul(upper, m))
    api.AssertIsEqual(composed, v)
    return
}

Besides, the function supports input nbDigits to constrain the bit number of v. If nbDigits is not specified (nbDigits = api.Compiler().FieldBitLen()), there can be two ways to split the value. For example, to split $1$, we can make $lower + 2^{split} \times upper$ equals to $1$ or $p+1$, where p is the field modulus. If nbDigits is specified and nbDigits > api.Compiler().FieldBitLen() holds, there will be multiple ways to split the value.

Recommendation. Constrain the upper part to be of the correct size:

rh.Check(upper, upperBound - int(split))

In addition, add an assertion in the function to ensure that

nbDigits < api.Compiler().FieldBitLen()

Client Response. https://github.com/Consensys/gnark/pull/1165

Description. Gnark's standard library defines some gadgets to emulate uint32 and uint64 types.

An important aspect of these interfaces is to ensure that the conversion from native circuit field elements and the uint types is sound. This is done through the ValueOf and ToValue functions. Here is the ValueOf function that is written generically for both the uint32 and uint64 types:

func (bf *BinaryField[T]) ByteValueOf(a frontend.Variable) U8 {
    bf.rchecker.Check(a, 8)
    return U8{Val: a, internal: true}
}

func (bf *BinaryField[T]) ValueOf(a frontend.Variable) T {
    var r T
    bts, err := bf.api.Compiler().NewHint(toBytes, len(r), len(r), a)
    if err != nil {
        panic(err)
    }
    // TODO: add constraint which ensures that map back to
    for i := range bts {
        r[i] = bf.ByteValueOf(bts[i])
    }
    return r
}

The problem with this code is that the hinted bytestring is not checked to be a correct representation of the original value. As such, it can be arbitrarily set to any value by the prover, leading to a soundness issue.

Recommendation. As with the ToBits function, recompose the bytestring into a value and assert that it is equal to the original one. For example:

    for i := range bts {
        r[i] = bf.ByteValueOf(bts[i])
    }
+    expectedValue := bf.ToValue(r)
+    bf.api.AssertIsEqual(a, expectedValue)  

In addition, document that overflows are forbidden, as the current implementation does not allow for overflows.

Client Response. https://github.com/Consensys/gnark/pull/1139

Description. The enforceWidthConditional is used in several places in the circuit to constrain that the limbs of foreign field elements are correctly formed (i.e. that they are of the correct bitlength).

The function relies on a hash function HashCode() to mark if a linear combination has been seen and constrained before:

func (f *Field[T]) enforceWidthConditional(a *Element[T]) (didConstrain bool) {
    // TRUNCATED...
    for i := range a.Limbs {
        // TRUNCATED...
        if vv, ok := a.Limbs[i].(interface{ HashCode() uint64 }); ok {
            // okay, this is a canonical variable and it has a hashcode. We use
            // it to see if the limb is already constrained.
            h := vv.HashCode()
            if _, ok := f.constrainedLimbs[h]; !ok {
                // we found a limb which hasn't yet been constrained. This means
                // that we should enforce width for the whole element. But we
                // still iterate over all limbs just to mark them in the table.
                didConstrain = true
                f.constrainedLimbs[h] = struct{}{}
            }
        } else {
            // we have no way of knowing if the limb has been constrained. To be
            // on the safe side constrain the whole element again.
            didConstrain = true
        }
    }
    if didConstrain {
        f.enforceWidth(a, true)
    }
    return
}

This hash function is unfortunately not cryptographically secure, as the following code shows:

// -- gnark/frontend/internal/expr/linear_expression.go --
func (l LinearExpression) HashCode() uint64 {
    h := uint64(17)
    for _, val := range l {
        h = h*23 + val.HashCode() // TODO @gbotrel revisit
    }
    return h
}

// -- gnark/frontend/internal/expr/term.go --
func (t Term) HashCode() uint64 {
    return t.Coeff[0]*29 + uint64(t.VID<<12)
}

As such, it might be possible for a malicious circuit developer to create a circuit in which two different circuit variables collide and produce the same digest, leading to only one of them being properly constrained.

Note that other parts of the gnark library use the HashCode() function, for example, MarkBoolean and IsBoolean.

Recommendation. We recommend using a cryptographically secure hash function that would have both collision resistance and pre-image resistance, in order to ensure that circuit builders cannot produce stealthily underconstrained circuits.

Client Response. https://github.com/Consensys/gnark/pull/1197

Description. IsZero returns a boolean indicating if all the limbs of the element are exactly zero. The safe (slow) way is to check if each of the limbs is zero one-by-one. The fast way is to check if the sum of all the limbs is zero, provided it won't cause an overflow in the native field. However, the condition of judging if it will cause overflow is flipped.

// IsZero returns a boolean indicating if the element is strictly zero.
func (f *Field[T]) IsZero(a *Element[T]) frontend.Variable {
    ...
    // every addition adds a bit to the overflow
    totalOverflow := len(ca.Limbs) - 1
    // the condition here is incorrect.
    if totalOverflow < int(f.maxOverflow()) {
        // safe way: check if each limb is zero, one by one.
        res := f.api.IsZero(ca.Limbs[0])
        for i := 1; i < len(ca.Limbs); i++ {
            res = f.api.Mul(res, f.api.IsZero(ca.Limbs[i]))
        }
        return res
    }
    // fast way: check if the sum of all the limbs is zero.
    limbSum := ca.Limbs[0]
    for i := 1; i < len(ca.Limbs); i++ {
        limbSum = f.api.Add(limbSum, ca.Limbs[i])
    }
    return f.api.IsZero(limbSum)
}

Here, if totalOverflow >= int(f.maxOverflow()) is true, it means the sum will cause an overflow and it should use the safe way. However, The code indirectly routes it to the fast way, which may lead to overflow. A malicious prover can prove non-zero element to be zero utilizing the overflow.

In current gnark's parameter setting, totalOverflow < int(f.maxOverflow()) is always true. This means it will always route to the safe way. Therefore it only leads to downgraded efficiency. However, it can be problematic for the downstream users if they have different parameter settings.

Recommendation. Change it to the right condition. For example:

func (f *Field[T]) IsZero(a *Element[T]) frontend.Variable {
    ...
    if totalOverflow > int(f.maxOverflow())
    ...
}

Client Response. https://github.com/Consensys/gnark/pull/1145

Description. Gnark's standard library implements the MiMC hash function using the Miyaguchi–Preneel construction. The Miyaguchi–Preneel construction is a known way to turn a block cipher into a compression function, which can then be used to build a hash function.

Such an instantiation is well-studied and known to be secure against most attacks, except length-extension attacks. Length-extension attacks occur when a secret is used in the hash function to produce a keyed hash, for example, if one produces a digest as hash(secret || public_data) where || is a concatenation, someone else could pick up where the hashing was left off and produce a new digest hash(secret || public_data || more_data) without knowing the secret. Fundamentally, this is because the digest produced by the algorithm is the internal state of the hash function, which can be reused without issue to continue hashing.

As such, one could imagine an innocent developer producing a circuit where data and the digest are made public (through public inputs, for example) and then used in another protocol and circuit to produce a different keyed-hash on some related data (as explained above). For example:

type Circuit1 struct {
    Key frontend.Variable `gnark:",secret"`
    Data [1]frontend.Variable `gnark:",public"`
    Expected frontend.Variable `gnark:",public"`
}

type Circuit2 struct {
    Key frontend.Variable `gnark:",secret"`
    Data [2]frontend.Variable `gnark:",public"`
    Expected frontend.Variable `gnark:",public"`
}

func (c *CircuitN) Define(api frontend.API) error {
    h, err := mimc.New(api)
    if err != nil { return err }
    h.Write(c.Key)
    h.Write(c.Data[:]...)
    res := h.Sum()
    api.AssertIsEqual(res, c.Expected)
}

In addition, the MiMC website's FAQ also states:

In our original paper we propose to instantiate a hash function via plugging the MiMC permutation into a Sponge construction. The reason back then was security analysis. A mode like Miyaguchi-Preneel makes it harder, and in 2016 we did not feel confident in proposing this. In the meanwhile we did more security analysis, improving our understanding and confidence, but our recommendation remains unchanged.

Note that we could not find usages of this API being used with secret data, but the API itself remains exposed to end users and does not forbid the caller to use it with secret data.

Recommendation. Document the API to make it clear that it should not be used with secret data.

Client Response. https://github.com/Consensys/gnark/pull/1198

Description. modSub function performs sub operation on emulated Element over given modulus p. To calculate (a - b) % p, gnark uses a padding pad to avoid any possible underflow and overflow in the native field. Then it calculates a[i] + pad[i] - b[i] for all i and recomposes the result.

The pad should satisfies:

1. correctness: pad % p = 0.
2. avoid underflow: pad[i] >= b[i] for all i.
3. avoid overflow pad[i] + a[i] < native_field for all i.

Unfortunately, pad is given by a hint function and misses a constraint to enforce condition 2. A malicious prover may provide a pad that satisfies 1 and 3, but causes underflow when calculating a[i] + p[i] - b[i]. In this way the modSub function will return incorrect results.

func (f *Field[T]) computeSubPaddingHint(overflow uint, nbLimbs uint, modulus *Element[T]) *Element[T] {
    var fp T
    inputs := []frontend.Variable{fp.NbLimbs(), fp.BitsPerLimb(), overflow, nbLimbs}
    inputs = append(inputs, modulus.Limbs...)
    res, err := f.api.NewHint(subPaddingHint, int(nbLimbs), inputs...)
    if err != nil {
        panic(fmt.Sprintf("sub padding hint: %v", err))
    }
    for i := range res {
        // enforce condition 3
        f.checker.Check(res[i], int(fp.BitsPerLimb()+overflow+1))
    }
    padding := f.newInternalElement(res, fp.BitsPerLimb()+overflow+1)
    // enforce condition 1
    f.checkZero(padding, modulus)
    return padding
}

Another issue is incorrect overflow setting. The overflow of padding should be overflow+1 instead of fp.BitsPerLimb()+overflow+1. In the modSub function, nextOverflow is calculated as nextOverflow := max(b.overflow+1, a.overflow) + 1. This will be an issue if nextOverflow > f.maxOf().

Recommendation. Add constraint to enforce pad[i] >= b[i] for all i. Correctly enforce the overflow setting.

Client Response. https://github.com/Consensys/gnark/pull/1200

Description. Non-native field elements are represented as Element variables in gnark circuits. Such variables can be provided by the prover and are checked to have limbs of the correct bitlength (as explained in the introduction of this report). Let's call this bitlength $n$.

There are two kinds of overflows that can happen with these values:

1. bit overflows: when the limbs comprising the Element variable now need to track larger bitstrings (e.g. $n+1$-bit limbs) because an overflow might have happened. This also means that the value being tracked might potentially be larger than the modulus.
2. modulus overflow with no bit overflow: the value is larger than the modulus, but its limbs did not have bit overflows. This is the kind of overflow that we are interested in.

Note that Element variables that are known to have no bit overflows are marked as internal.

A Reduce function is provided which only performs a modular reduction if it detects no bit overflow. This means that it is possible that the function returns a value larger than the modulus in the case of modulus overflow with no bit overflow. For example, it could return $f+1$ with $f$ the foreign modulus.

This behavior implies that the codebase makes the following general assumptions:

1. Either functions don't care about modulus overflow with no bit overflow, as they can deal with it. This is the case of many of the non-native arithmetic operations like Add and Mul.
2. Or functions care, and they will call the AssertIsInRange() function to prevent malicious provers from using values that are larger than the modulus.

Both of these assumptions are not necessarily true.

The first assumption doesn't hold for the ToBits and Exp functions. For example, ToBits(f+1) and ToBits(1) will return different bits. Looking at ToBits first, we can see that the comment below is misleading because the Reduce function won't reduce a modulus overflow with no bit overflow (and thus won't generate a canonical representation of Element as a bitstring).

// ToBits returns the bit representation of the Element in little-endian (LSB
// first) order. The returned bits are constrained to be 0-1. The number of
// returned bits is nbLimbs*nbBits+overflow. To obtain the bits of the canonical
// representation of Element, reduce Element first and take less significant
// bits corresponding to the bitwidth of the emulated modulus.
func (f *Field[T]) ToBits(a *Element[T]) []frontend.Variable {
    f.enforceWidthConditional(a)
    ...

The Exp function uses ToBits to generate the bits and perform exponentiation by squaring. As ToBits may generate different bits, Exp will generate incorrect results.

// Exp computes base^exp modulo the field order. The returned Element has default
// number of limbs and zero overflow.
func (f *Field[T]) Exp(base, exp *Element[T]) *Element[T] {
    expBts := f.ToBits(exp)
    n := len(expBts)
    res := f.Select(expBts[0], base, f.One())
    base = f.Mul(base, base)
    for i := 1; i < n-1; i++ {
        res = f.Select(expBts[i], f.Mul(base, res), res)
        base = f.Mul(base, base)
    }
    res = f.Select(expBts[n-1], f.Mul(base, res), res)
    return res
}

Take the below case as an example. A malicious prover can choose f.ModMul(b, c) to be either l or f+l. Then further choose the result of f.ModExp(a, l):

l := f.ModMul(b, c)
res := f.ModExp(a, l)

Going back to our two cases, the second case (calling AssertIsInRange to enforce a smaller-than-modulus value) can be seen, for example, in the start of the implementation of the IsZero function:

// AssertIsInRange ensures that a is less than the emulated modulus. When we
// call [Reduce] then we only ensure that the result is width-constrained, but
// not actually less than the modulus. This means that the actual value may be
// either x or x + p. For arithmetic it is sufficient, but for binary comparison
// it is not. For binary comparison the values have both to be below the
// modulus.
func (f *Field[T]) AssertIsInRange(a *Element[T]) {
    // we omit conditional width assertion as is done in ToBits down the calling stack
    f.AssertIsLessOrEqual(a, f.modulusPrev())
}

// IsZero returns a boolean indicating if the element is strictly zero. The
// method internally reduces the element and asserts that the value is less than
// the modulus.
func (f *Field[T]) IsZero(a *Element[T]) frontend.Variable {
    ca := f.Reduce(a)
    f.AssertIsInRange(ca)

The issue with this pattern is that it assumes that no illegitimate Element value (one that would be larger than the modulus but with no bit overflow) can be produced at runtime, besides a direct hint from the prover (which in this case would not matter, as they would be shooting themselves in the foot).

While this might be true, it is not necessarily obviously true. We can expect that all field operations will increase the overflow of the element variable, which will in turn trigger the Reduce function and perform a modular reduction in legitimate cases (before the call to AssertIsLessOrEqual), but further code changes might introduce edge cases where this is not true anymore, potentially leading to completeness issues.

Recommendation. Change the name of the Reduce function to avoid confusing developers making use of the function. Keep track of Element variables that might not be "fully reduced", in the sense that they might be larger than the modulus, and enforce a modular reduction if this is the case in functions like ToBits and Exp.

Furthermore, consider taking a slightly different approach and always enforcing that Element values are less than the modulus if they have no bit overflow. See Field API Is A Leaky Abstraction for a related issue.

Client Response. https://github.com/Consensys/gnark/pull/1224

Description. gnark uses GLV decomposition to speedup scalar multiplication in native field. To compute $P=[s]Q$, one key step is to decompose $s$ into two smaller parts $s_1$ and $s_2$ such that $s_1 + \lambda \cdot s_2 = s \mod r$, where $\lambda$ is fixed value and $r$ is the scalar field. To do that, gnark uses a hint and obtains $s_1$ and $s_2$, it then check if the equation holds:

    // s1 + λ * s2 == s mod r
    api.AssertIsEqual(
        api.Add(s1, api.Mul(s2, cc.lambda)),
        api.Add(s, api.Mul(cc.fr, m)),
    )

This check is intended to ensure there exists $m$ such that $s_1 + \lambda \cdot s_2 = s + m \cdot r$. However, this check is performed in the native field and may incur overflow. It's actually checking that there exists $m$ and $n$ such that $s_1 + \lambda \cdot s_2 = s + m \cdot r + n \cdot B$ (where $B$ is the native field). As $m$ and $n$ can be arbitrary values, there can be multiple ways to decompose $s$. The decomposition check is not sound.

Recommendation. The decomposition check should be done in the scalar field instead of the base field (i.e. native field). Consider performing the check using an emulated field types.

Client Response. "The issue applies for BLS24 which is out of scope and is not used in Linea." https://github.com/Consensys/gnark/pull/1167

Description. ToNAF returns the NAF decomposition of given input. The non-adjacent form (NAF) of a number is a unique signed-digit representation, in which non-zero values cannot be adjacent.

gnark uses a hint and obtains the NAF decomposition bits. Then it performs checks to ensure the sum of the bits equals to the input value and each of the bits is -1, 0 or 1.

// ToNAF returns the NAF decomposition of given input.
// The non-adjacent form (NAF) of a number is a unique signed-digit representation,
// in which non-zero values cannot be adjacent. For example, NAF(13) = [1, 0, -1, 0, 1].
func ToNAF(api frontend.API, v frontend.Variable, opts ...BaseConversionOption) []frontend.Variable {
    ...
    c := big.NewInt(1)

    bits, err := api.Compiler().NewHint(nNaf, cfg.NbDigits, v)
    if err != nil {
        panic(err)
    }

    var Σbi frontend.Variable
    Σbi = 0
    for i := 0; i < cfg.NbDigits; i++ {
        Σbi = api.Add(Σbi, api.Mul(bits[i], c))
        c.Lsh(c, 1)
        if !cfg.UnconstrainedOutputs {
            // b * (1 - b) * (1 + b) == 0
            // TODO this adds 3 constraint, not 2. Need api.Compiler().AddConstraint(...)
            b := bits[i]
            y := api.Mul(api.Sub(1, b), api.Add(1, b))
            api.AssertIsEqual(api.Mul(b, y), 0)
        }
    }

    // record the constraint Σ (2**i * b[i]) == v
    api.AssertIsEqual(Σbi, v)

    return bits
}

Unfortunately, the function doesn't enforce "non-zero values cannot be adjacent" in the circuit. Thus a malicious prover can generate a representation with adjacent non-zero values, which may poison the subsequent computation.

Recommendation. Add constraints to enforce "non-zero values cannot be adjacent" in the circuit.

Client Response. https://github.com/Consensys/gnark/pull/1164

Description. Gnark uses wrapped_hash to wrap MiMC function for computing the challenges inside the circuit. The inputs are bits (or native field elements) and outputs are elements in the emulated field.

wrapped_hash batches the input bits and only writes a whole batch at a time to the underlying hash function. For the last batch, it will fill with zeros if the input bits don't fill up the batch. This means that wrapped_hash won't distinguish whether the trailing bits are input bits or just padding. Then, it's easy to construct two preimages of different lengths that produce the same hash:

func TestCollision(t *testing.T) {
    h, err := recursion.NewShort(ecc.BLS12_377.ScalarField(), ecc.BN254.ScalarField())
    if err != nil {
        panic(err)
    }

    h.Write([]byte{0x00})
    hash := h.Sum(nil)
    fmt.Printf("%x\n", hash) // 34373b65f439c874734ff51ea349327c140cde2e47a933146e6f9f2ad8eb17
    h.Reset()

    h.Write([]byte{0x00})
    h.Write([]byte{0x00})
    fmt.Printf("%x\n", h.Sum(nil)) // 34373b65f439c874734ff51ea349327c140cde2e47a933146e6f9f2ad8eb17
}

Currently, this is not an issue because wrapped_hash is created to generate challenges that have a fixed input length. However, it may introduce vulnerabilities when downstream users use it.

Recommendation. Add warnings in the doc to avoid misuse.

Client Response. https://github.com/Consensys/gnark/pull/1198

Description. Foreign field elements are represented as Element variable types in circuits.

Element variables have an internal field called internal which is set only if created through field.NewElement or through the foreign field methods defined in the emulated package. This field indicates that the limbs of the Element variable were constrained to be of the correct bitlength.

This Element type can be introduced through hints, or through private inputs to the circuit if included in the circuit struct. For example:

type someCircuit struct {
    SomeVariable Element[Secp256k1Fp]
}

When passed as private inputs, Element variables do not have their limbs constrained and as such do not have their internal field set to true.

For this reason, it is therefore the responsibility of functions making use of it to remember to call enforceWidthConditional to make sure that the field element gets properly constrained (i.e. number of limbs is correct and each limb is of the correct bitlength). For example, the checkZero, Reduce, Select, Lookup2, Mux, AssertIsEqual, mulMod, reduceAndOp, ToBits, Sum, all call the enforceWidthConditional function.

Note: it still does not mean that the value is less than the modulus, as we discuss in Reduce Function Is Misleading And Could Lead To Soundness and Completeness Issues.

This is a dangerous pattern that could lead to soundness issues if functions of the standard library, or user-written functions to extend the standard library, forget to call enforceWidthConditional on an Element variable.

Recommendation. We recommend ensuring that no Element variable can be created without its limb being properly constrained. This could be done in the compiler Compile() function in the parseCircuit() logic that walks through the circuit's public and private inputs.

Client Response. Won't fix ("We have considered another approach, but the current approach allows us to decouple non-native arithmetic from the circuit frontend design, keeping it relatively lightweight.")