Different assert than intended

The assert_var_len_keccak_correctness function in circuits/src/keccak/chip.rs makes some consistency checks of a couple of parameters. They are not in-circuit checks, so they are not directly security relevant but rather sanity checks to defend against coding mistakes elsewhere. The function is implemented as follows:

/// Checks that the chip has executed [`keccak_var_len`](Self::keccak_var_len)
/// correctly. This function should be called before updating the chip inner state.
fn assert_var_len_keccak_correctness(
    &self,
    output_bytes: &[u8],
    output_assigned: &[AssignedValue<F>],
    max_input_bytes_length_after_padding: usize,
    unpadded_input_bytes_length: usize,
    byte_len_val: usize,
    max_len: usize,
) {
    assert!(max_len < max_input_bytes_length_after_padding);
    assert!(max_input_bytes_length_after_padding >= byte_len_val);
    assert_eq!(byte_len_val % NUM_BYTES_PER_WORD, 0);
    assert_eq!(max_input_bytes_length_after_padding % RATE, 0);
    assert_eq!(
        output_bytes.to_vec(),
        get_assigned_bytes_values(output_assigned)
    );
    assert_eq!(
        unpadded_input_bytes_length,
        max((max_len / RATE) * RATE, byte_len_val)
    );
}

Here, byte_len_val is the original input length, max_len is the maximum input length, and max_input_bytes_length_after_padding is the maximum input length after padding has been applied. The first assert checks that max_len < max_input_bytes_length_after_padding, which should hold as padding always increases the length. While max_input_bytes_length_after_padding >= byte_len_val should also hold for the same reason, checking for greater-or-equal here would be weaker than needed; max_input_bytes_length_after_padding should always be strictly bigger than byte_len_val. It is likely what is actually intended here is to check max_len >= byte_len_val, which should hold but is not currently checked by the implementation. Replacing the check in the second assert with this inequality would also imply the currently asserted inequality, as one would then have max_input_bytes_length_after_padding > max_len >= byte_len_val.

The assert was corrected as suggested in commit