Description

Two almost identical functions named first_i_bits_bitmask are used to create a bitmask with b[j]=1 when i < j. Those functions are used to verify variable-length Keccak padding of bytes into 64-bit words and to check the padding of public inputs in the universal batch verifier.

The size of the bitmask $n$ is given as a parameter of the function. The bitmask is built by pushing constraints computed by the function is_less_than from the Axiom implementation↗:

pub fn first_i_bits_bitmask<F: ScalarField>(
    ctx: &mut Context<F>,
    chip: &impl RangeInstructions<F>,
    i: AssignedValue<F>,
    n: u64,
) -> Vec<AssignedValue<F>> {
    let mut bitmask = Vec::with_capacity(n as usize);
    let num_bits = log2(n as usize);
    for idx in 0..n {
        let idx = ctx.load_constant(F::from(idx));
        bitmask.push(chip.is_less_than(ctx, idx, i, num_bits as usize));
    }
    bitmask
}

The is_less_than function takes as a parameter num_bits, which is assumed to be the number of bits to represent the values compared. In the first_i_bits_bitmask functions, if the size of the mask is a power of two, let us say $2^m$, then the number of bits passed to the is_less_than function is computed with the log2 function, which in the previous example will output $m$, but the compared values require $m+1$ bits to be represented. It contradicts the assumption of the is_less_than function on num_bits.

Impact

It seems that the code of is_less_than is currently able to handle properly such edge cases, but nothing guarantees that future updates will not break such behavior. If so, the constraints may not be sound anymore for lengths that equal a power of two.

Recommendations

Even if it appears so far that the chip handles this edge case correctly, it may be safer to compute the number of bits with the following:

let num_bits = log2((n + 1) as usize);

Remediation

This issue has been acknowledged by Nebra, and a fix was implemented in commit 48ca21a3↗.