sp1_core_machine/control_flow/jal/
air.rs

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

sp1_core_machine/control_flow/jal/
air.rs
