Opcode SHL

[silathdiir]

Spec: scroll-tech/zkevm-specs#43

Summary

1. Integrate both opcode SHL and SHR into mul_div_mod (rename to mul_div_mod_shl_shr).

2. Consider SHL as MUL (a * (1 << shift) = b) and SHR as DIV (a // (1 << shift) = b).

[icemelon]

one high level idea. is it possible to swap the a & b in the SHR and SHL to reuse most part of the constraints? e.g.

SHR: a >> shift = b
SHL: a << shift = b  <=>  b >> shift = a

[silathdiir]

one high level idea. is it possible to swap the a & b in the SHR and SHL to reuse most part of the constraints? e.g.

SHR: a >> shift = b
SHL: a << shift = b  <=>  b >> shift = a

Yes. I think it makes sense. Will give a try. Thanks.

[z2trillion]

SHL: a << shift = b <=> b >> shift = a

I don't think this is correct. E.g. for shift = 1, a = 0b100, and b = 0b1001, b >> shift = 0b1001 >> 1 = 0b100 = a, but a << shift = 0b100 << 1 = 0b1000.

[silathdiir]

Updated to merge both opcode SHL andSHR into mul_div_mod ( and rename to mul_div_mod_shl_shr).

[z2trillion]

I think you're still missing the power of 2 lookup conditions for SHL and SHR?

You can check that pop2 < 256 by checking that the value fits into the first byte with by constraining that RLC(pop2) == pop2.cells[0] btw.

[silathdiir]

It seems that there is no need to lookup Pow2 table. Since I calculated divisor = 1 << shf0 (if shf0 < 256) in function assign_exec_step directly (not sperated to low and high bytes). What do you think?

And I added another contraint to check pop1 == pop1.cells[0] for opcode SHL and SHR. Thanks.

cb.require_zero(
    "pop1 == pop1.cells[0] when divisor != 0 for opcode SHL and SHR",
    (is_shl.clone() + is_shr.clone())
        * (1.expr() - divisor_is_zero.expr())
        * (pop1.expr() - pop1.cells[0].expr()),
);

[z2trillion]

we definately need to add the lookup constraint here.

My model is that configure adds the constraints for the circuit and assign_exec_step generates a witness that satisfies those constraints. If you don't have enough constraints, then there can be multiple witnesses that satisfy them. In this case, without the lookup constraint, replacing line 177 with 5.expr() or many other expressions could still allow the constraints to all be satisfied.

[z2trillion]

we definately need to add the lookup constraint here.

My model is that configure adds the constraints for the circuit and assign_exec_step generates a witness that satisfies those constraints. If you don't have enough constraints, then there can be multiple witnesses that satisfy them. In this case, without the lookup constraint, replacing line 177 with 5.expr() or many other expressions could still allow the constraints to all be satisfied.

[silathdiir]

Hi @z2trillion , according to code review, I sperated shift[0] to shf_lo (less than 128) and shf_hi (greater than or equal to 128) to avoid overflow of Pow2 lookup table.

And I added two constraints to lookup divisor_lo = 2^shf_lo and divisor_hi = 2^shf_hi in Pow2 table (only for opcode SHL and SHR).

Could you help review the code again? Thanks a lot.

[z2trillion]

Lookups can have up to three values in them:

pub(crate) enum Lookup<F> {
    /// Lookup to fixed table, which contains serveral pre-built tables such as
    /// range tables or bitwise tables.
    Fixed {
        /// Tag to specify which table to lookup.
        tag: Expression<F>,
        /// Values that must satisfy the pre-built relationship.
        values: [Expression<F>; 3],
    },
    ...

I think a more direct (and easier to understand) approach would be to have

values = [
  input, 
  if input < 128 {1 << input} else {0}, 
  if input < 128 {0} else {1 << (input -128)}
]

You can then directly lookup up shift_hi and shift_lo without needing to use the divisor_lo_is_zero and divisor_hi_is_zero gadgets.

[silathdiir]

Updated Pow2 table and fixed to lookup (shf0, divisor_lo, divisor_hi) in this table.
Hi @z2trillion , please have review again when you have time. Thanks.

[silathdiir]

Thanks for code review. Moved to upstream privacy-scaling-explorations#578.