Inaccuracies in the specification

We collect here some inaccuracies in the specification spec/circuits/var_len_keccak.md that we encountered.

Example for multi-variable length query

In the example for the multi-variable length query, under Step 2, the matrix is missing two rows of zero at the bottom. The end result (the line before the next heading "Slice-Adder Matrix") is missing the 9 and a 0.

Reuse of variable k

In the "Slice-Adder Matrix" section, the slice-adder matrix $S_k$ is discussed, making $k$ bound. However, $k$ is reused when describing the number of columns of $S_k$ as ${\sum }_k{L}_k$, reusing $k$. Using a different variable in the sum would be better notation.

Keccak-circuit domain-tag calculation

The specification for the Keccak circuit (spec/circuits/var_len_keccak.md) does not accurately describe how domain tags are used after the changes made to the code. The specification describes as Step 3 conversion to a field element, which was relevant for use in the Poseidon hash function but is not relevant anymore (and hence not reflected in the code) after the switch to Keccak for circuitId calculation. We also noticed and reported this in our audit whose first draft was delivered August 8th 2024, under section 4.9.

Out-of-scope aspects remarked in earlier audits

This version of the spec still uses inaccurate LegoSNARK terminology for the gnark Groth16 extension. For more details, see section 4.2 in the report from June 7th. The specification also reflects a hash-to-field function that we discussed in 3.12 and 3.13 in our report from August 8th 2024.