sp1_core_machine/adapter/
state.rs

1use crate::air::WordAirBuilder;
2use serde::{Deserialize, Serialize};
3use slop_algebra::{AbstractField, Field};
4use sp1_core_executor::{events::ByteRecord, ByteOpcode};
5use sp1_derive::{AlignedBorrow, InputExpr, InputParams, IntoShape, SP1OperationBuilder};
6use sp1_hypercube::air::SP1AirBuilder;
7use struct_reflection::{StructReflection, StructReflectionHelper};
8
9use crate::air::SP1Operation;
10
11/// A set of columns to describe the state of the CPU.
12/// The state is composed of the shard, clock, and the program counter.
13/// The clock is split into 24 bits, 8 bits, 16 bits limbs.
14#[derive(
15    AlignedBorrow,
16    Default,
17    Debug,
18    Clone,
19    Copy,
20    Serialize,
21    Deserialize,
22    IntoShape,
23    SP1OperationBuilder,
24    StructReflection,
25)]
26#[repr(C)]
27pub struct CPUState<T> {
28    pub clk_high: T,
29    pub clk_16_24: T,
30    pub clk_0_16: T,
31    pub pc: [T; 3],
32}
33
34impl<T: Copy> CPUState<T> {
35    pub fn clk_high<AB>(&self) -> AB::Expr
36    where
37        AB: SP1AirBuilder<Var = T>,
38        T: Into<AB::Expr>,
39    {
40        self.clk_high.into()
41    }
42    pub fn clk_low<AB>(&self) -> AB::Expr
43    where
44        AB: SP1AirBuilder<Var = T>,
45        T: Into<AB::Expr>,
46    {
47        self.clk_0_16.into() + self.clk_16_24.into() * AB::Expr::from_canonical_u32(1 << 16)
48    }
49}
50
51impl<F: Field> CPUState<F> {
52    #[allow(clippy::too_many_arguments)]
53    pub fn populate(&mut self, blu_events: &mut impl ByteRecord, clk: u64, pc: u64) {
54        let clk_high = (clk >> 24) as u32;
55        let clk_16_24 = ((clk >> 16) & 0xFF) as u8;
56        let clk_0_16 = (clk & 0xFFFF) as u16;
57        self.clk_high = F::from_canonical_u32(clk_high);
58        self.clk_16_24 = F::from_canonical_u8(clk_16_24);
59        self.clk_0_16 = F::from_canonical_u16(clk_0_16);
60        self.pc = [
61            F::from_canonical_u16((pc & 0xFFFF) as u16),
62            F::from_canonical_u16(((pc >> 16) & 0xFFFF) as u16),
63            F::from_canonical_u16(((pc >> 32) & 0xFFFF) as u16),
64        ];
65
66        // 0 <= (clk_0_16 - 1) / 8 < 2^13 shows clk == 1 (mod 8) and clk_0_16 is 16 bits.
67        blu_events.add_bit_range_check((clk_0_16 - 1) / 8, 13);
68        blu_events.add_u8_range_checks(&[clk_16_24, 0]);
69    }
70
71    #[allow(clippy::too_many_arguments)]
72    pub fn eval<AB: SP1AirBuilder>(
73        builder: &mut AB,
74        cols: CPUState<AB::Var>,
75        next_pc: [AB::Expr; 3],
76        clk_increment: AB::Expr,
77        is_real: AB::Expr,
78    ) {
79        let clk_high = cols.clk_high::<AB>();
80        let clk_low = cols.clk_low::<AB>();
81        builder.assert_bool(is_real.clone());
82        builder.receive_state(clk_high.clone(), clk_low.clone(), cols.pc, is_real.clone());
83        builder.send_state(
84            clk_high.clone(),
85            clk_low.clone() + clk_increment,
86            next_pc,
87            is_real.clone(),
88        );
89
90        builder.send_byte(
91            AB::Expr::from_canonical_u32(ByteOpcode::Range as u32),
92            (cols.clk_0_16 - AB::Expr::one()) * AB::F::from_canonical_u8(8).inverse(),
93            AB::Expr::from_canonical_u32(13),
94            AB::Expr::zero(),
95            is_real.clone(),
96        );
97
98        builder.slice_range_check_u8(&[cols.clk_16_24.into(), AB::Expr::zero()], is_real.clone());
99    }
100}
101
102#[derive(Clone, InputParams, InputExpr)]
103pub struct CPUStateInput<AB: SP1AirBuilder> {
104    pub cols: CPUState<AB::Var>,
105    pub next_pc: [AB::Expr; 3],
106    pub clk_increment: AB::Expr,
107    pub is_real: AB::Expr,
108}
109
110impl<AB: SP1AirBuilder> SP1Operation<AB> for CPUState<AB::F> {
111    type Input = CPUStateInput<AB>;
112    type Output = ();
113
114    fn lower(builder: &mut AB, input: Self::Input) -> Self::Output {
115        Self::eval(builder, input.cols, input.next_pc, input.clk_increment, input.is_real);
116    }
117}
sp1_core_machine/adapter/state.rs

sp1_core_machine/adapter/
state.rs
