sp1_core_machine/control_flow/jalr/
air.rs

1use crate::{
2    adapter::{
3        register::i_type::{ITypeReader, ITypeReaderInput},
4        state::{CPUState, CPUStateInput},
5    },
6    air::{SP1CoreAirBuilder, SP1Operation},
7    eval_untrusted_program,
8    operations::AddOperationInput,
9    TrustMode, UserMode,
10};
11use slop_air::{Air, AirBuilder};
12use slop_algebra::{AbstractField, Field};
13use slop_matrix::Matrix;
14use sp1_core_executor::{ByteOpcode, Opcode, CLK_INC};
15use sp1_hypercube::Word;
16use std::borrow::Borrow;
17
18use crate::operations::AddOperation;
19
20use super::{JalrChip, JalrColumns};
21
22impl<AB, M> Air<AB> for JalrChip<M>
23where
24    AB: SP1CoreAirBuilder,
25    AB::Var: Sized,
26    M: TrustMode,
27{
28    #[inline(never)]
29    fn eval(&self, builder: &mut AB) {
30        let main = builder.main();
31        let local = main.row_slice(0);
32        let local: &JalrColumns<AB::Var, M> = (*local).borrow();
33
34        builder.assert_bool(local.is_real);
35
36        let opcode = Opcode::JALR.as_field::<AB::F>();
37        let funct3 = AB::Expr::from_canonical_u8(Opcode::JALR.funct3().unwrap());
38        let funct7 = AB::Expr::from_canonical_u8(Opcode::JALR.funct7().unwrap_or(0));
39        let base_opcode = AB::Expr::from_canonical_u32(Opcode::JALR.base_opcode().0);
40        let instr_type = AB::Expr::from_canonical_u32(Opcode::JALR.instruction_type().0 as u32);
41
42        // We constrain `next_pc` to be the sum of `op_b` and `op_c`.
43        let op_input = AddOperationInput::<AB>::new(
44            local.adapter.b().map(|x| x.into()),
45            local.adapter.c().map(|x| x.into()),
46            local.add_operation,
47            local.is_real.into(),
48        );
49        <AddOperation<AB::F> as SP1Operation<AB>>::eval(builder, op_input);
50
51        let next_pc = local.add_operation.value;
52        builder.assert_zero(next_pc[3]);
53
54        // Check that the `lsb` value is boolean.
55        builder.assert_bool(local.lsb);
56
57        // Check that the `next_pc` value is a multiple of 4 after clearing the LSB.
58        // `0 <= (next_pc[0] - lsb) / 4 < 2^14` shows `next_pc[0] - lsb` is a multiple of 4 that's
59        // u16. This shows `lsb` is the LSB of `next_pc[0]`, and that `next_pc == 0, 1 (mod 4)`.
60        builder.send_byte(
61            AB::Expr::from_canonical_u32(ByteOpcode::Range as u32),
62            (next_pc[0].into() - local.lsb.into()) * AB::F::from_canonical_u32(4).inverse(),
63            AB::Expr::from_canonical_u32(14),
64            AB::Expr::zero(),
65            local.is_real,
66        );
67
68        // Constrain the state of the CPU.
69        // The `next_pc` is constrained by the AIR.
70        // The clock is incremented by `8`.
71        <CPUState<AB::F> as SP1Operation<AB>>::eval(
72            builder,
73            CPUStateInput::new(
74                local.state,
75                [next_pc[0].into() - local.lsb.into(), next_pc[1].into(), next_pc[2].into()],
76                AB::Expr::from_canonical_u32(CLK_INC),
77                local.is_real.into(),
78            ),
79        );
80
81        let mut is_trusted: AB::Expr = local.is_real.into();
82
83        #[cfg(feature = "mprotect")]
84        builder.assert_eq(
85            builder.extract_public_values().is_untrusted_programs_enabled,
86            AB::Expr::from_bool(!M::IS_TRUSTED),
87        );
88
89        if !M::IS_TRUSTED {
90            let local = main.row_slice(0);
91            let local: &JalrColumns<AB::Var, UserMode> = (*local).borrow();
92
93            let instruction = local.adapter.instruction::<AB>(opcode);
94
95            #[cfg(not(feature = "mprotect"))]
96            builder.assert_zero(local.is_real);
97
98            eval_untrusted_program(
99                builder,
100                local.state.pc,
101                instruction,
102                [instr_type, base_opcode, funct3, funct7],
103                [local.state.clk_high::<AB>(), local.state.clk_low::<AB>()],
104                local.is_real.into(),
105                local.adapter_cols,
106            );
107
108            is_trusted = local.adapter_cols.is_trusted.into();
109        }
110
111        // Constrain the program and register reads.
112        <ITypeReader<AB::F> as SP1Operation<AB>>::eval(
113            builder,
114            ITypeReaderInput::new(
115                local.state.clk_high::<AB>(),
116                local.state.clk_low::<AB>(),
117                local.state.pc,
118                Opcode::JALR.as_field::<AB::F>().into(),
119                local.op_a_operation.value.map(|x| x.into()),
120                local.adapter,
121                local.is_real.into(),
122                is_trusted,
123            ),
124        );
125
126        builder.when_not(local.is_real).assert_zero(local.adapter.op_a_0);
127
128        // Verify that pc_abs + 4 is saved in op_a.
129        // When op_a is set to register X0, the RISC-V spec states that the jump instruction will
130        // not have a return destination address (it is effectively a GOTO command).  In this case,
131        // we shouldn't verify the return address.
132        let op_input = AddOperationInput::<AB>::new(
133            Word([
134                local.state.pc[0].into(),
135                local.state.pc[1].into(),
136                local.state.pc[2].into(),
137                AB::Expr::zero(),
138            ]),
139            Word([
140                AB::Expr::from_canonical_u16(4),
141                AB::Expr::zero(),
142                AB::Expr::zero(),
143                AB::Expr::zero(),
144            ]),
145            local.op_a_operation,
146            local.is_real.into() - local.adapter.op_a_0,
147        );
148        <AddOperation<AB::F> as SP1Operation<AB>>::eval(builder, op_input);
149        builder.assert_zero(local.op_a_operation.value[3]);
150        for i in 0..3 {
151            builder.when(local.adapter.op_a_0).assert_zero(local.op_a_operation.value[i]);
152        }
153    }
154}
sp1_core_machine/control_flow/jalr/air.rs

sp1_core_machine/control_flow/jalr/
air.rs
