You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
## a << b OR a >> b
Adds shift opcodes `SHL` and `SHR` following some of the logic [here](https://github.com/AztecProtocol/aztec-packages/blame/bf7a99d8d8e3faa00c9395a17acf7f92b171a7a1/barretenberg/cpp/pil/avm/alu.pil#L518).
We reuse the decomposition columns for u128 mul & div to show:
- `SHL`: show that `a = 2^(max_bits - shift) * a_hi + a_lo` and assign `c = a_lo * 2^shift`
- includes range checking `a_hi` is less than `shift` bits and `a_lo` less than `max_bits - shift` bits
- `SHR`: show that `a = 2^shift * a_hi + a_lo` and assign `c = a_hi`
- includes range checking `a_hi` is less than `max_bits - shift` bits and `a_lo` less than `shift` bits
### Bit Size Overflow
If `shift > max_bits`, then `max_bits - shift` (used in both cases in the range checks) will underflow the field and fail. Since we just need to return `c = 0` in this case, I set `sel_shift_ops_no_overflow` as a gate for assigning `c`. If we have an overflow, we assign `a_lo = shift - max_bits` and range check it against `max_bits`. The range check proves we have a shift overflow (i.e. `SHIFT_OVERFLOW = sel_shift_ops * (1 - sel_shift_ops_no_overflow) <==> shift > max_bits`) and the result is assigned as 0. e.g. for `SHR`:
```
ic - sel_shift_ops_no_overflow * a_hi = 0;
```
### Errors
Like `DIV`, shift operations on `FF` values are invalid, so I reused columns/relations to assign `FF_TAG_ERR = 1` in this case. Mismatched `a` and `b` tags (to follow new noir style) also give an error (`sel_ab_tag_mismatch`). As before:
```
sel_tag_err = sel_ab_tag_mismatch + FF_TAG_ERR - sel_ab_tag_mismatch * FF_TAG_ERR;
```
### Notes
- To avoid more lookups than necessary, I use `precomputed.power_of_2` (to find the limb size of `a_lo`, either `2^shift` or `2^(max_bits - shift)`) once, then for `SHL` when we also need `2^shift`, I use `helper1` to inject the value and prove correctness in a relation. It might be cheaper in another way, or just clearer to always lookup the `2^shift` value and assign `helper1 = 2^(max_bits - shift)` - happy to change/discuss!
- Made some changes to `TaggedValue` behaviour to fix issues with overflowing the bit size - thank you Facundo for your help on this!
Co-authored-by: MirandaWood <[email protected]>
// For NOT opcode, an error occurs if the tag of a is FF. In this case, tracegen will set
141
141
// b's tag as 0 which, while it would currently pass the checks below, is not a tag inequality we
142
142
// want to throw with sel_ab_tag_mismatch:
143
-
pol CHECK_AB_TAGS = 1 - sel_op_not * sel_is_ff - sel_op_truncate - sel_op_shr - sel_op_shl; // note: shifts are temporary, they should be subject to AB checks
143
+
pol CHECK_AB_TAGS = 1 - sel_op_not * sel_is_ff - sel_op_truncate;
144
144
pol AB_TAGS_EQ = 1 - sel_ab_tag_mismatch;
145
145
pol commit ab_tags_diff_inv;
146
146
// Prove that sel_ab_tag_mismatch = 1 <==> we have a disallowed inequality between the tags:
0 commit comments