sp1_core_machine/operations/
clk.rs

1use sp1_core_executor::{events::ByteRecord, ByteOpcode};
2use sp1_hypercube::air::SP1AirBuilder;
3
4use slop_air::AirBuilder;
5use slop_algebra::{AbstractField, Field};
6use sp1_derive::AlignedBorrow;
7
8use crate::air::WordAirBuilder;
9
10/// A set of columns needed to increment the clk and handle the carry.
11#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
12#[repr(C)]
13pub struct ClkOperation<T> {
14    next_clk_16_24: T,
15    next_clk_0_16: T,
16    is_overflow: T,
17}
18
19impl<T: Copy> ClkOperation<T> {
20    pub fn next_clk_high<AB>(&self, clk_high: AB::Var) -> AB::Expr
21    where
22        AB: SP1AirBuilder<Var = T>,
23        T: Into<AB::Expr>,
24    {
25        clk_high.into() + self.is_overflow
26    }
27
28    pub fn next_clk_low<AB>(&self) -> AB::Expr
29    where
30        AB: SP1AirBuilder<Var = T>,
31        T: Into<AB::Expr>,
32    {
33        self.next_clk_0_16.into()
34            + self.next_clk_16_24.into() * AB::Expr::from_canonical_u32(1 << 16)
35    }
36}
37
38impl<F: Field> ClkOperation<F> {
39    pub fn populate(&mut self, record: &mut impl ByteRecord, clk: u64, increment: u64) {
40        let next_clk = clk + increment;
41        let next_clk_16_24 = ((next_clk >> 16) & 0xFF) as u8;
42        let next_clk_0_16 = (next_clk & 0xFFFF) as u16;
43
44        let is_overflow = (next_clk >> 24) != (clk >> 24);
45        self.is_overflow = F::from_canonical_u8(is_overflow as u8);
46        self.next_clk_16_24 = F::from_canonical_u8(next_clk_16_24);
47        self.next_clk_0_16 = F::from_canonical_u16(next_clk_0_16);
48
49        record.add_bit_range_check(next_clk_0_16, 16);
50        record.add_u8_range_checks(&[next_clk_16_24, 0]);
51    }
52
53    // Check that `clk_low + increment` overflows 24 bits.
54    // Checks that `is_real` is boolean. If `is_real` is true, `next_clk` limbs are correct
55    // low 24 bits of `clk_low + increment`, and `is_overflow` is the carry.
56    // This function assumes that `clk_low` and `increment` is within 24 bits.
57    pub fn eval<AB: SP1AirBuilder>(
58        builder: &mut AB,
59        clk_low: AB::Expr,
60        increment: AB::Expr,
61        cols: ClkOperation<AB::Var>,
62        is_real: AB::Expr,
63    ) {
64        // Check that `is_real` is boolean.
65        builder.assert_bool(is_real.clone());
66
67        // Check that `is_overflow` is boolean.
68        builder.assert_bool(cols.is_overflow);
69
70        // Constrain the `next_clk_low` value.
71        // If `is_overflow` is false, then it's equal to `clk_low + increment`.
72        // If `is_overflow` is true, then it's equal to `clk_low + increment - 2^24`.
73        builder.when(is_real.clone()).assert_eq(
74            clk_low.clone() + increment.clone()
75                - cols.is_overflow.into() * AB::Expr::from_canonical_u32(1 << 24),
76            cols.next_clk_low::<AB>(),
77        );
78
79        // Constrain that `next_clk_low` is a valid 24 bit value by decomposing into two limbs.
80        builder.send_byte(
81            AB::Expr::from_canonical_u32(ByteOpcode::Range as u32),
82            cols.next_clk_0_16.into(),
83            AB::Expr::from_canonical_u32(16),
84            AB::Expr::zero(),
85            is_real.clone(),
86        );
87        builder
88            .slice_range_check_u8(&[cols.next_clk_16_24.into(), AB::Expr::zero()], is_real.clone());
89    }
90}
sp1_core_machine/operations/clk.rs

sp1_core_machine/operations/
clk.rs
