sp1-core-machine 6.0.0-beta.1

SP1 is a performant, 100% open-source, contributor-friendly zkVM.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129

use slop_air::AirBuilder;
use slop_algebra::{AbstractField, Field};
use sp1_core_executor::{events::ByteRecord, ByteOpcode};
use sp1_derive::AlignedBorrow;
use sp1_hypercube::air::SP1AirBuilder;
use sp1_primitives::consts::u32_to_u16_limbs;

use crate::utils::u32_to_half_word;

/// A set of columns needed to compute `>>` of an u32 with a fixed offset R.
///
/// Note that we decompose shifts into a limb shift and a bit shift.
#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
#[repr(C)]
pub struct FixedShiftRightOperation<T> {
    /// The output value.
    pub value: [T; 2],

    /// The higher bits of each limb.
    pub higher_limb: [T; 2],
}

impl<F: Field> FixedShiftRightOperation<F> {
    pub const fn nb_limbs_to_shift(rotation: usize) -> usize {
        rotation / 16
    }

    pub const fn nb_bits_to_shift(rotation: usize) -> usize {
        rotation % 16
    }

    pub const fn carry_multiplier(rotation: usize) -> u32 {
        let nb_bits_to_shift = Self::nb_bits_to_shift(rotation);
        1 << (16 - nb_bits_to_shift)
    }

    pub fn populate(&mut self, record: &mut impl ByteRecord, input: u32, rotation: usize) -> u32 {
        let input_limbs = u32_to_u16_limbs(input);
        let expected = input >> rotation;
        self.value = u32_to_half_word(expected);

        // Compute some constants with respect to the rotation needed for the rotation.
        let nb_limbs_to_shift = Self::nb_limbs_to_shift(rotation);
        let nb_bits_to_shift = Self::nb_bits_to_shift(rotation);

        // Perform the limb shift.
        let mut word = [0u16; 2];
        for i in 0..2 {
            if i + nb_limbs_to_shift < 2 {
                word[i] = input_limbs[i + nb_limbs_to_shift];
            }
        }

        for i in (0..2).rev() {
            let limb = word[i];
            let lower_limb = (limb & ((1 << nb_bits_to_shift) - 1)) as u16;
            let higher_limb = (limb >> nb_bits_to_shift) as u16;
            self.higher_limb[i] = F::from_canonical_u16(higher_limb);
            record.add_bit_range_check(lower_limb, nb_bits_to_shift as u8);
            record.add_bit_range_check(higher_limb, (16 - nb_bits_to_shift) as u8);
        }

        expected
    }

    /// Evaluates the u32 fixed shift right. Constrains that `is_real` is boolean.
    /// If `is_real` is true, the result `value` will be the correct result with two u16 limbs.
    /// This function assumes that the `input` is a u32 with valid two u16 limbs.
    pub fn eval<AB: SP1AirBuilder>(
        builder: &mut AB,
        input: [AB::Var; 2],
        rotation: usize,
        cols: FixedShiftRightOperation<AB::Var>,
        is_real: AB::Var,
    ) {
        builder.assert_bool(is_real);

        // Compute some constants with respect to the rotation needed for the rotation.
        let nb_limbs_to_shift = Self::nb_limbs_to_shift(rotation);
        let nb_bits_to_shift = Self::nb_bits_to_shift(rotation);
        let carry_multiplier = AB::F::from_canonical_u32(Self::carry_multiplier(rotation));

        // Perform the limb shift.
        let input_limbs_shifted: [AB::Expr; 2] = std::array::from_fn(|i| {
            if i + nb_limbs_to_shift < 2 {
                input[i + nb_limbs_to_shift].into()
            } else {
                AB::Expr::zero()
            }
        });

        // For each limb, constrain the lower and higher parts of the limb.
        let mut lower_limb = [AB::Expr::zero(), AB::Expr::zero()];
        for i in 0..2 {
            let limb = input_limbs_shifted[i].clone();

            // Break down the limb into lower and higher parts.
            //  - `limb = lower_limb + higher_limb * 2^bit_shift`
            //  - `lower_limb < 2^(bit_shift)`
            //  - `higher_limb < 2^(16 - bit_shift)`
            lower_limb[i] =
                limb - cols.higher_limb[i] * AB::Expr::from_canonical_u32(1 << nb_bits_to_shift);

            // Check that `lower_limb < 2^(bit_shift)`
            builder.send_byte(
                AB::F::from_canonical_u32(ByteOpcode::Range as u32),
                lower_limb[i].clone(),
                AB::F::from_canonical_u32(nb_bits_to_shift as u32),
                AB::Expr::zero(),
                is_real,
            );
            // Check that `higher_limb < 2^(16 - bit_shift)`
            builder.send_byte(
                AB::F::from_canonical_u32(ByteOpcode::Range as u32),
                cols.higher_limb[i],
                AB::Expr::from_canonical_u32(16 - nb_bits_to_shift as u32),
                AB::Expr::zero(),
                is_real,
            );
        }

        // Constrain the resulting value using the lower and higher parts.
        builder.when(is_real).assert_eq(cols.value[1], cols.higher_limb[1]);
        builder.when(is_real).assert_eq(
            cols.value[0],
            cols.higher_limb[0] + lower_limb[1].clone() * carry_multiplier,
        );
    }
}