Uniform result KECCAK result extraction for the KECCAK circuit

[OlivierBBB]

This is a follow up issue to issue #137.

Main point

For integrating the results of a KECCAK computation predicted by the arithmetization @Soleimani193 requires the same format everywhere for our RES prediction. This affects results coming from SHAKIRA and RLPADDR.

Discrepancies between SHAKIRA and RLPADDR

The way data is represented in both modules is different:

SHAKIRA:

• results are in a single column (LIMB)
• results aren't duplicated

RLPADDR:

• hi / lo parts of results live in separate columns (RAW_ADDR_HI and DEP_ADDR_LO)
• results are duplicated

Uniform approach

The arithmetization should provide her with selectors to produce (internal) duplicate free result columns or even better: with dedicated KECCAK_RES_HI / KECCAK_RES_LO columns. This is simple to do and would for instance take on the following form.

SHAKIRA:
- SELECTOR_KECCAK_RES_HI  =  IS_KECCAK_RESULT  *  (1 - INDEX)
- SELECTOR_KECCAK_RES_LO  =  IS_KECCAK_RESULT  *  INDEX

RLPADDR:
- SELECTOR_KECCAK_RES_HI  =  IS_FIRST_ROW
- SELECTOR_KECCAK_RES_LO  =  IS_FIRST_ROW

where IS_FIRST_ROW is binary and = 1 iff the RLPADDR stamp just jumped by 1 (and 0 on the first row) so e.g.

If RLPADDR_STAMP = 0  Then  IS_FIRST_ROW = 0
If RLPADDR_STAMP ≠ 0  Then  IS_FIRST_ROW = RLPADDR_STAMP[i] - RLPADDR_STAMP[i - 1]

Notes.

• @Soleimani193 confirmed to me that the fact that the SHAKIRA result columns would contain results that live on different rows is irrelevant to her
• "(Internal) duplicate free" means that there is no duplication for the same ID. This is due to this part of the "data aggregation" being done with a projection mapping rather than a lookup.

Originally posted by @OlivierBBB in #137 (comment)