sp1_core_machine/operations/
fixed_rotate_right.rs

1use slop_air::AirBuilder;
2use slop_algebra::{AbstractField, Field};
3use sp1_core_executor::{events::ByteRecord, ByteOpcode};
4use sp1_derive::AlignedBorrow;
5use sp1_hypercube::air::SP1AirBuilder;
6use sp1_primitives::consts::u32_to_u16_limbs;
7
8/// A set of columns needed to compute `rotateright` of a u32 with a fixed offset R.
9///
10/// Note that we decompose rotate into a limb rotate and a bit rotate.
11#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
12#[repr(C)]
13pub struct FixedRotateRightOperation<T> {
14    /// The output value.
15    pub value: [T; 2],
16
17    /// The higher bits of each limb.
18    pub higher_limb: [T; 2],
19}
20
21impl<F: Field> FixedRotateRightOperation<F> {
22    pub const fn nb_limbs_to_rotate(rotation: usize) -> usize {
23        rotation / 16
24    }
25
26    pub const fn nb_bits_to_rotate(rotation: usize) -> usize {
27        rotation % 16
28    }
29
30    pub const fn carry_multiplier(rotation: usize) -> u32 {
31        let nb_bits_to_rotate = Self::nb_bits_to_rotate(rotation);
32        1 << (16 - nb_bits_to_rotate)
33    }
34
35    pub fn populate(&mut self, record: &mut impl ByteRecord, input: u32, rotation: usize) -> u32 {
36        let input_limbs = u32_to_u16_limbs(input);
37        let expected = input.rotate_right(rotation as u32);
38        self.value = [
39            F::from_canonical_u16((expected & 0xFFFF) as u16),
40            F::from_canonical_u16((expected >> 16) as u16),
41        ];
42
43        // Compute some constants with respect to the rotation needed for the rotation.
44        let nb_limbs_to_rotate = Self::nb_limbs_to_rotate(rotation);
45        let nb_bits_to_rotate = Self::nb_bits_to_rotate(rotation);
46
47        // Perform the limb rotate.
48        let input_limbs_rotated =
49            [input_limbs[nb_limbs_to_rotate % 2], input_limbs[(1 + nb_limbs_to_rotate) % 2]];
50
51        for i in (0..2).rev() {
52            let limb = input_limbs_rotated[i];
53            let lower_limb = (limb & ((1 << nb_bits_to_rotate) - 1)) as u16;
54            let higher_limb = (limb >> nb_bits_to_rotate) as u16;
55            self.higher_limb[i] = F::from_canonical_u16(higher_limb);
56            record.add_bit_range_check(lower_limb, nb_bits_to_rotate as u8);
57            record.add_bit_range_check(higher_limb, (16 - nb_bits_to_rotate) as u8);
58        }
59
60        expected
61    }
62
63    /// Evaluates the u32 fixed rotate right. Constrains that `is_real` is boolean.
64    /// If `is_real` is true, the result `value` will be the correct result with two u16 limbs.
65    /// This function assumes that the `input` is a u32 with valid two u16 limbs.
66    pub fn eval<AB: SP1AirBuilder>(
67        builder: &mut AB,
68        input: [AB::Var; 2],
69        rotation: usize,
70        cols: FixedRotateRightOperation<AB::Var>,
71        is_real: AB::Var,
72    ) {
73        // Constrains that `is_real` is boolean.
74        builder.assert_bool(is_real);
75
76        // Compute some constants with respect to the rotation needed for the rotation.
77        let nb_limbs_to_rotate = Self::nb_limbs_to_rotate(rotation);
78        let nb_bits_to_rotate = Self::nb_bits_to_rotate(rotation);
79        let carry_multiplier = AB::F::from_canonical_u32(Self::carry_multiplier(rotation));
80
81        // Perform the limb rotate.
82        let input_limbs_rotated =
83            [input[nb_limbs_to_rotate % 2], input[(1 + nb_limbs_to_rotate) % 2]];
84
85        // For each limb, constrain the lower and higher parts of the limb.
86        let mut lower_limb = [AB::Expr::zero(), AB::Expr::zero()];
87        for i in 0..2 {
88            let limb = input_limbs_rotated[i];
89
90            // Break down the limb into lower and higher parts.
91            //  - `limb = lower_limb + higher_limb * 2^bit_rotate`
92            //  - `lower_limb < 2^(bit_rotate)`
93            //  - `higher_limb < 2^(16 - bit_rotate)`
94            lower_limb[i] =
95                limb - cols.higher_limb[i] * AB::Expr::from_canonical_u32(1 << nb_bits_to_rotate);
96
97            // Check that `lower_limb < 2^(bit_rotate)`
98            builder.send_byte(
99                AB::F::from_canonical_u32(ByteOpcode::Range as u32),
100                lower_limb[i].clone(),
101                AB::F::from_canonical_u32(nb_bits_to_rotate as u32),
102                AB::Expr::zero(),
103                is_real,
104            );
105            // Check that `higher_limb < 2^(16 - bit_rotate)`
106            builder.send_byte(
107                AB::F::from_canonical_u32(ByteOpcode::Range as u32),
108                cols.higher_limb[i],
109                AB::Expr::from_canonical_u32(16 - nb_bits_to_rotate as u32),
110                AB::Expr::zero(),
111                is_real,
112            );
113        }
114
115        // Constrain the resulting value using the lower and higher parts.
116        builder.when(is_real).assert_eq(
117            cols.value[1],
118            cols.higher_limb[1] + lower_limb[0].clone() * carry_multiplier,
119        );
120        builder.when(is_real).assert_eq(
121            cols.value[0],
122            cols.higher_limb[0] + lower_limb[1].clone() * carry_multiplier,
123        );
124    }
125}
sp1_core_machine/operations/fixed_rotate_right.rs

sp1_core_machine/operations/
fixed_rotate_right.rs
