sp1_core_machine/program/
instruction_decode.rs

1use core::{
2    borrow::{Borrow, BorrowMut},
3    mem::{size_of, MaybeUninit},
4};
5
6use crate::{
7    air::{SP1CoreAirBuilder, SP1Operation, WordAirBuilder},
8    operations::{IsZeroOperation, IsZeroOperationInput},
9    program::InstructionCols,
10    utils::next_multiple_of_32,
11};
12use slop_air::{Air, AirBuilder, BaseAir};
13use slop_algebra::{AbstractField, PrimeField32};
14use slop_matrix::Matrix;
15use sp1_core_executor::{ExecutionRecord, InstructionType, Opcode, Program};
16use sp1_derive::AlignedBorrow;
17use sp1_hypercube::{
18    air::{MachineAir, SP1AirBuilder},
19    Word,
20};
21
22use rrs_lib::instruction_formats::{
23    OPCODE_AUIPC, OPCODE_BRANCH, OPCODE_JAL, OPCODE_JALR, OPCODE_LOAD, OPCODE_LUI, OPCODE_OP,
24    OPCODE_OP_32, OPCODE_OP_IMM, OPCODE_OP_IMM_32, OPCODE_STORE,
25};
26
27/// The number of program columns.
28pub const NUM_INSTRUCTION_DECODE_COLS: usize = size_of::<InstructionDecodeCols<u8>>();
29
30/// The column layout for the chip.
31#[derive(AlignedBorrow, Clone, Copy, Default)]
32#[repr(C)]
33pub struct InstructionDecodeCols<T> {
34    pub multiplicity: T,
35    pub instruction: InstructionCols<T>,
36    pub instr_type: T,
37    pub funct3: T,
38    pub funct7: T,
39    pub is_r_type: T,
40    pub is_i_type: T,
41    pub is_i_type_shamt: T,
42    pub is_i_type_shamt_32: T,
43    pub is_j_type: T,
44    pub is_b_type: T,
45    pub is_s_type: T,
46    pub is_u_type: T,
47    pub is_a_0: IsZeroOperation<T>,
48    pub encoded_instruction: [T; 2],
49    pub encoded_instruction_bits: [T; 32],
50}
51
52/// A chip that implements instruction decoding.
53#[derive(Default)]
54pub struct InstructionDecodeChip;
55
56impl InstructionDecodeChip {
57    pub const fn new() -> Self {
58        Self {}
59    }
60}
61
62impl<F: PrimeField32> MachineAir<F> for InstructionDecodeChip {
63    type Record = ExecutionRecord;
64
65    type Program = Program;
66
67    fn name(&self) -> &'static str {
68        "InstructionDecode"
69    }
70
71    fn generate_dependencies(&self, _input: &ExecutionRecord, _output: &mut ExecutionRecord) {
72        // Do nothing since this chip has no dependencies.
73    }
74
75    fn generate_trace_into(
76        &self,
77        input: &ExecutionRecord,
78        _output: &mut ExecutionRecord,
79        buffer: &mut [MaybeUninit<F>],
80    ) {
81        let padded_nb_rows =
82            <InstructionDecodeChip as MachineAir<F>>::num_rows(self, input).unwrap();
83        let num_event_rows = input.instruction_decode_events.len();
84
85        unsafe {
86            let padding_start = num_event_rows * NUM_INSTRUCTION_DECODE_COLS;
87            let padding_size = (padded_nb_rows - num_event_rows) * NUM_INSTRUCTION_DECODE_COLS;
88            if padding_size > 0 {
89                core::ptr::write_bytes(buffer[padding_start..].as_mut_ptr(), 0, padding_size);
90            }
91        }
92
93        let buffer_ptr = buffer.as_mut_ptr() as *mut F;
94        let values = unsafe {
95            core::slice::from_raw_parts_mut(
96                buffer_ptr,
97                num_event_rows * NUM_INSTRUCTION_DECODE_COLS,
98            )
99        };
100
101        values.chunks_mut(NUM_INSTRUCTION_DECODE_COLS).enumerate().for_each(|(idx, row)| {
102            let cols: &mut InstructionDecodeCols<F> = row.borrow_mut();
103            let event = &input.instruction_decode_events[idx];
104
105            let instruction = event.instruction;
106            cols.instruction.populate(&instruction);
107            cols.is_a_0.populate(instruction.op_a.into());
108
109            // Check that the encoded instruction is correct
110            let encoding_check = instruction.encode();
111            assert_eq!(event.encoded_instruction, encoding_check);
112
113            cols.encoded_instruction[0] = F::from_canonical_u32(event.encoded_instruction & 0xFFFF);
114            cols.encoded_instruction[1] =
115                F::from_canonical_u32((event.encoded_instruction >> 16) & 0xFFFF);
116
117            for (i, bit) in event
118                .encoded_instruction
119                .to_le_bytes()
120                .iter()
121                .flat_map(|byte| {
122                    let mut bits = [0u8; 8];
123                    for j in 0..8 {
124                        bits[j] = (byte >> j) & 1;
125                    }
126                    bits
127                })
128                .enumerate()
129            {
130                cols.encoded_instruction_bits[i] = F::from_canonical_u8(bit);
131            }
132
133            if instruction.opcode != Opcode::UNIMP {
134                let (instr_type, instr_type_imm) = instruction.opcode.instruction_type();
135                let instr_type = if instr_type_imm.is_some() && instruction.imm_c {
136                    instr_type_imm.unwrap()
137                } else {
138                    instr_type
139                };
140                cols.instr_type = F::from_canonical_u32(instr_type as u32);
141
142                let (base_opcode, base_imm_opcode) = instruction.opcode.base_opcode();
143                let base_opcode = if base_imm_opcode.is_some() && instruction.imm_c {
144                    base_imm_opcode.unwrap()
145                } else {
146                    base_opcode
147                };
148                let funct3 = instruction.opcode.funct3().unwrap_or(0);
149                let funct7 = instruction.opcode.funct7().unwrap_or(0);
150                cols.funct3 = F::from_canonical_u8(funct3);
151                cols.funct7 = F::from_canonical_u8(funct7);
152
153                cols.is_r_type =
154                    F::from_bool(base_opcode == OPCODE_OP || base_opcode == OPCODE_OP_32);
155
156                let is_i_type = matches!(
157                    base_opcode,
158                    OPCODE_OP_IMM | OPCODE_OP_IMM_32 | OPCODE_LOAD | OPCODE_JALR
159                );
160                if is_i_type {
161                    if matches!(funct3, 0b001 | 0b101) && base_opcode == OPCODE_OP_IMM {
162                        cols.is_i_type_shamt = F::one();
163                    } else if matches!(funct3, 0b001 | 0b101) && base_opcode == OPCODE_OP_IMM_32 {
164                        cols.is_i_type_shamt_32 = F::one();
165                    } else {
166                        cols.is_i_type = F::one();
167                    }
168                }
169
170                cols.is_j_type = F::from_bool(base_opcode == OPCODE_JAL);
171                cols.is_b_type = F::from_bool(base_opcode == OPCODE_BRANCH);
172                cols.is_s_type = F::from_bool(base_opcode == OPCODE_STORE);
173                cols.is_u_type =
174                    F::from_bool(base_opcode == OPCODE_AUIPC || base_opcode == OPCODE_LUI);
175            }
176
177            cols.multiplicity = F::from_canonical_usize(event.multiplicity);
178        });
179    }
180
181    fn included(&self, shard: &Self::Record) -> bool {
182        if let Some(shape) = shard.shape.as_ref() {
183            shape.included::<F, _>(self)
184        } else {
185            !shard.instruction_decode_events.is_empty()
186        }
187    }
188
189    fn num_rows(&self, input: &Self::Record) -> Option<usize> {
190        let nb_rows = next_multiple_of_32(
191            input.instruction_decode_events.len(),
192            input.fixed_log2_rows::<F, _>(self),
193        );
194        Some(nb_rows)
195    }
196}
197
198impl<F> BaseAir<F> for InstructionDecodeChip {
199    fn width(&self) -> usize {
200        NUM_INSTRUCTION_DECODE_COLS
201    }
202}
203
204impl<AB> Air<AB> for InstructionDecodeChip
205where
206    AB: SP1CoreAirBuilder,
207{
208    fn eval(&self, builder: &mut AB) {
209        let main = builder.main();
210        let local = main.row_slice(0);
211        let local: &InstructionDecodeCols<AB::Var> = (*local).borrow();
212
213        // We do not allow untrusted instructions to make ecalls.
214        builder.assert_bool(local.is_r_type);
215        builder.assert_bool(local.is_i_type);
216        builder.assert_bool(local.is_i_type_shamt);
217        builder.assert_bool(local.is_i_type_shamt_32);
218        builder.assert_bool(local.is_j_type);
219        builder.assert_bool(local.is_b_type);
220        builder.assert_bool(local.is_s_type);
221        builder.assert_bool(local.is_u_type);
222
223        let is_real: AB::Expr = local.is_r_type
224            + local.is_i_type
225            + local.is_i_type_shamt
226            + local.is_i_type_shamt_32
227            + local.is_j_type
228            + local.is_b_type
229            + local.is_s_type
230            + local.is_u_type;
231
232        // Assert that at most one of the instruction selectors is set.
233        builder.assert_bool(is_real.clone());
234
235        // Assert that the right instruction selector is set.
236        builder.assert_eq(
237            local.instr_type,
238            local.is_r_type * AB::Expr::from_canonical_u32(InstructionType::RType as u32)
239                + local.is_i_type * AB::Expr::from_canonical_u32(InstructionType::IType as u32)
240                + local.is_i_type_shamt
241                    * AB::Expr::from_canonical_u32(InstructionType::ITypeShamt as u32)
242                + local.is_i_type_shamt_32
243                    * AB::Expr::from_canonical_u32(InstructionType::ITypeShamt32 as u32)
244                + local.is_j_type * AB::Expr::from_canonical_u32(InstructionType::JType as u32)
245                + local.is_b_type * AB::Expr::from_canonical_u32(InstructionType::BType as u32)
246                + local.is_s_type * AB::Expr::from_canonical_u32(InstructionType::SType as u32)
247                + local.is_u_type * AB::Expr::from_canonical_u32(InstructionType::UType as u32),
248        );
249
250        let (
251            decoded_base_opcode,
252            decoded_funct3,
253            decoded_funct7_rtype,
254            decoded_funct7_i_type_shamt,
255            decoded_rd,
256            decoded_rs1,
257            decoded_rs2,
258        ) = self.decode_instruction(builder, local);
259
260        self.r_type_eval(
261            builder,
262            local,
263            decoded_funct3.clone(),
264            decoded_funct7_rtype.clone(),
265            decoded_rd.clone(),
266            decoded_rs1.clone(),
267            decoded_rs2.clone(),
268        );
269        self.i_type_eval(
270            builder,
271            local,
272            decoded_funct3.clone(),
273            decoded_rd.clone(),
274            decoded_rs1.clone(),
275        );
276        self.i_type_shamt_eval(
277            builder,
278            local,
279            decoded_funct3.clone(),
280            decoded_funct7_i_type_shamt.clone(),
281            decoded_rd.clone(),
282            decoded_rs1.clone(),
283        );
284        self.i_type_shamt_32_eval(
285            builder,
286            local,
287            decoded_funct3.clone(),
288            decoded_funct7_i_type_shamt.clone(),
289            decoded_rd.clone(),
290            decoded_rs1.clone(),
291        );
292        self.j_type_eval(builder, local, decoded_rd.clone());
293        self.b_type_eval(
294            builder,
295            local,
296            decoded_funct3.clone(),
297            decoded_rs1.clone(),
298            decoded_rs2.clone(),
299        );
300        self.s_type_eval(
301            builder,
302            local,
303            decoded_funct3.clone(),
304            decoded_rs1.clone(),
305            decoded_rs2.clone(),
306        );
307        self.u_type_eval(builder, local, decoded_rd.clone());
308
309        // Check the op_a_0 column.
310        IsZeroOperation::<AB::F>::eval(
311            builder,
312            IsZeroOperationInput::new(local.instruction.op_a.into(), local.is_a_0, is_real.clone()),
313        );
314        builder.when(is_real.clone()).assert_eq(local.is_a_0.result, local.instruction.op_a_0);
315
316        // Constrain the interaction with instruction decode table
317        let untrusted_instruction_const_fields = [
318            local.instr_type.into(),
319            decoded_base_opcode,
320            local.funct3.into(),
321            local.funct7.into(),
322        ];
323
324        builder.when_not(is_real).assert_zero(local.multiplicity);
325
326        builder.receive_instruction_decode(
327            [local.encoded_instruction[0].into(), local.encoded_instruction[1].into()],
328            local.instruction,
329            untrusted_instruction_const_fields,
330            local.multiplicity.into(),
331        );
332    }
333}
334
335impl InstructionDecodeChip {
336    fn decode_instruction<AB: SP1AirBuilder>(
337        &self,
338        builder: &mut AB,
339        local: &InstructionDecodeCols<AB::Var>,
340    ) -> (AB::Expr, AB::Expr, AB::Expr, AB::Expr, AB::Expr, Word<AB::Expr>, Word<AB::Expr>) {
341        let mut reconstructed_first_limb = AB::Expr::zero();
342        for (i, bit) in local.encoded_instruction_bits[0..16].iter().enumerate() {
343            builder.assert_bool(*bit);
344            reconstructed_first_limb =
345                reconstructed_first_limb.clone() + AB::Expr::from_wrapped_u32(1 << i) * *bit;
346        }
347
348        let mut reconstructed_second_limb = AB::Expr::zero();
349        for (i, bit) in local.encoded_instruction_bits[16..32].iter().enumerate() {
350            builder.assert_bool(*bit);
351            reconstructed_second_limb =
352                reconstructed_second_limb.clone() + AB::Expr::from_wrapped_u32(1 << i) * *bit;
353        }
354
355        builder.assert_eq(local.encoded_instruction[0].into(), reconstructed_first_limb);
356        builder.assert_eq(local.encoded_instruction[1].into(), reconstructed_second_limb);
357
358        // True for all instruction types
359        let mut reconstructed_base_opcode = AB::Expr::zero();
360        for (i, bit) in local.encoded_instruction_bits[0..7].iter().enumerate() {
361            reconstructed_base_opcode =
362                reconstructed_base_opcode.clone() + AB::Expr::from_wrapped_u32(1 << i) * *bit;
363        }
364
365        // True for R, I, U, J, Not right for S, B
366        let mut reconstructed_rd = AB::Expr::zero();
367        for (i, bit) in local.encoded_instruction_bits[7..12].iter().enumerate() {
368            reconstructed_rd = reconstructed_rd.clone() + AB::Expr::from_wrapped_u32(1 << i) * *bit;
369        }
370
371        // True for R, I, S, B, Not right for U, J
372        let mut reconstructed_funct3 = AB::Expr::zero();
373        for (i, bit) in local.encoded_instruction_bits[12..15].iter().enumerate() {
374            reconstructed_funct3 =
375                reconstructed_funct3.clone() + AB::Expr::from_wrapped_u32(1 << i) * *bit;
376        }
377
378        // True for R, I, S, B, Not right for U, J
379        let reconstructed_rs1 =
380            Word::from_le_bits::<AB>(&local.encoded_instruction_bits[15..20], false);
381
382        // True for R, S, B, Not right for I, U, J
383        let reconstructed_rs2 =
384            Word::from_le_bits::<AB>(&local.encoded_instruction_bits[20..25], false);
385
386        let mut reconstructed_funct7_rtype = AB::Expr::zero();
387        for (i, bit) in local.encoded_instruction_bits[25..32].iter().enumerate() {
388            reconstructed_funct7_rtype =
389                reconstructed_funct7_rtype.clone() + AB::Expr::from_wrapped_u32(1 << i) * *bit;
390        }
391
392        let mut reconstructed_funct7_i_type_shamt = AB::Expr::zero();
393        for (i, bit) in local.encoded_instruction_bits[26..32].iter().enumerate() {
394            reconstructed_funct7_i_type_shamt = reconstructed_funct7_i_type_shamt.clone()
395                + AB::Expr::from_wrapped_u32(1 << i) * *bit;
396        }
397        reconstructed_funct7_i_type_shamt =
398            reconstructed_funct7_i_type_shamt.clone() * AB::Expr::from_wrapped_u32(2);
399
400        (
401            reconstructed_base_opcode,
402            reconstructed_funct3,
403            reconstructed_funct7_rtype,
404            reconstructed_funct7_i_type_shamt,
405            reconstructed_rd,
406            reconstructed_rs1,
407            reconstructed_rs2,
408        )
409    }
410
411    #[allow(clippy::too_many_arguments)]
412    fn r_type_eval<AB: SP1CoreAirBuilder>(
413        &self,
414        builder: &mut AB,
415        local: &InstructionDecodeCols<AB::Var>,
416        decoded_funct3: AB::Expr,
417        decoded_funct7: AB::Expr,
418        decoded_rd: AB::Expr,
419        decoded_rs1: Word<AB::Expr>,
420        decoded_rs2: Word<AB::Expr>,
421    ) {
422        let mut r_type_builder = builder.when(local.is_r_type);
423
424        r_type_builder.assert_eq(local.funct3, decoded_funct3);
425        r_type_builder.assert_eq(local.funct7, decoded_funct7);
426
427        r_type_builder.assert_eq(local.instruction.op_a, decoded_rd);
428        r_type_builder.assert_word_eq(local.instruction.op_b, decoded_rs1);
429        r_type_builder.assert_word_eq(local.instruction.op_c, decoded_rs2);
430
431        r_type_builder.assert_zero(local.instruction.imm_b);
432        r_type_builder.assert_zero(local.instruction.imm_c);
433    }
434
435    fn i_type_eval<AB: SP1AirBuilder>(
436        &self,
437        builder: &mut AB,
438        local: &InstructionDecodeCols<AB::Var>,
439        decoded_funct3: AB::Expr,
440        decoded_rd: AB::Expr,
441        decoded_rs1: Word<AB::Expr>,
442    ) {
443        let mut i_type_builder = builder.when(local.is_i_type);
444
445        i_type_builder.assert_eq(local.funct3, decoded_funct3);
446        i_type_builder.assert_eq(local.funct7, AB::Expr::zero());
447
448        i_type_builder.assert_eq(local.instruction.op_a, decoded_rd);
449        i_type_builder.assert_word_eq(local.instruction.op_b, decoded_rs1);
450
451        let mut imm_le_bits = Vec::new();
452        imm_le_bits.extend(local.encoded_instruction_bits[20..32].iter().map(|x| (*x).into()));
453        let sign_extended_imm = Word::from_le_bits::<AB>(&imm_le_bits, true);
454
455        i_type_builder.assert_word_eq(local.instruction.op_c, sign_extended_imm);
456
457        i_type_builder.assert_zero(local.instruction.imm_b);
458        i_type_builder.assert_one(local.instruction.imm_c);
459    }
460
461    fn i_type_shamt_eval<AB: SP1AirBuilder>(
462        &self,
463        builder: &mut AB,
464        local: &InstructionDecodeCols<AB::Var>,
465        decoded_funct3: AB::Expr,
466        decoded_funct7: AB::Expr,
467        decoded_rd: AB::Expr,
468        decoded_rs1: Word<AB::Expr>,
469    ) {
470        let mut i_type_shamt_builder = builder.when(local.is_i_type_shamt);
471
472        i_type_shamt_builder.assert_eq(local.funct3, decoded_funct3);
473        i_type_shamt_builder.assert_eq(local.funct7, decoded_funct7);
474
475        i_type_shamt_builder.assert_eq(local.instruction.op_a, decoded_rd);
476        i_type_shamt_builder.assert_word_eq(local.instruction.op_b, decoded_rs1);
477
478        let shamt = Word::from_le_bits::<AB>(&local.encoded_instruction_bits[20..26], false);
479        i_type_shamt_builder.assert_word_eq(local.instruction.op_c, shamt);
480
481        i_type_shamt_builder.assert_zero(local.instruction.imm_b);
482        i_type_shamt_builder.assert_one(local.instruction.imm_c);
483    }
484
485    fn i_type_shamt_32_eval<AB: SP1AirBuilder>(
486        &self,
487        builder: &mut AB,
488        local: &InstructionDecodeCols<AB::Var>,
489        decoded_funct3: AB::Expr,
490        decoded_funct7: AB::Expr,
491        decoded_rd: AB::Expr,
492        decoded_rs1: Word<AB::Expr>,
493    ) {
494        let mut i_type_shamt_32_builder = builder.when(local.is_i_type_shamt_32);
495
496        i_type_shamt_32_builder.assert_eq(local.funct3, decoded_funct3);
497        i_type_shamt_32_builder.assert_eq(local.funct7, decoded_funct7);
498
499        i_type_shamt_32_builder.assert_eq(local.instruction.op_a, decoded_rd);
500        i_type_shamt_32_builder.assert_word_eq(local.instruction.op_b, decoded_rs1);
501
502        let shamt = Word::from_le_bits::<AB>(&local.encoded_instruction_bits[20..25], false);
503        i_type_shamt_32_builder.assert_word_eq(local.instruction.op_c, shamt);
504
505        i_type_shamt_32_builder.assert_zero(local.encoded_instruction_bits[25]);
506
507        i_type_shamt_32_builder.assert_zero(local.instruction.imm_b);
508        i_type_shamt_32_builder.assert_one(local.instruction.imm_c);
509    }
510
511    fn j_type_eval<AB: SP1AirBuilder>(
512        &self,
513        builder: &mut AB,
514        local: &InstructionDecodeCols<AB::Var>,
515        decoded_rd: AB::Expr,
516    ) {
517        {
518            let mut imm_le_bits = Vec::new();
519
520            // The least significant bit (bit 0) is always 0.
521            imm_le_bits.push(AB::Expr::zero());
522            imm_le_bits.extend(local.encoded_instruction_bits[21..31].iter().map(|x| (*x).into()));
523            imm_le_bits.push(local.encoded_instruction_bits[20].into());
524            imm_le_bits.extend(local.encoded_instruction_bits[12..20].iter().map(|x| (*x).into()));
525            imm_le_bits.push(local.encoded_instruction_bits[31].into());
526
527            let sign_extended_word = Word::from_le_bits::<AB>(&imm_le_bits, true);
528
529            let mut j_type_builder = builder.when(local.is_j_type);
530
531            j_type_builder.assert_eq(local.funct3, AB::Expr::zero());
532            j_type_builder.assert_eq(local.funct7, AB::Expr::zero());
533
534            j_type_builder.assert_eq(local.instruction.op_a, decoded_rd);
535            j_type_builder.assert_word_eq(local.instruction.op_b, sign_extended_word);
536            j_type_builder.assert_word_zero(local.instruction.op_c);
537
538            j_type_builder.assert_one(local.instruction.imm_b);
539            j_type_builder.assert_one(local.instruction.imm_c);
540        }
541    }
542
543    fn b_type_eval<AB: SP1AirBuilder>(
544        &self,
545        builder: &mut AB,
546        local: &InstructionDecodeCols<AB::Var>,
547        decoded_funct3: AB::Expr,
548        decoded_rs1: Word<AB::Expr>,
549        decoded_rs2: Word<AB::Expr>,
550    ) {
551        let mut b_type_builder = builder.when(local.is_b_type);
552
553        b_type_builder.assert_eq(local.funct3, decoded_funct3);
554        b_type_builder.assert_eq(local.funct7, AB::Expr::zero());
555
556        let op_a_word = Word::extend_expr::<AB>(local.instruction.op_a.into());
557        b_type_builder.assert_word_eq(op_a_word, decoded_rs1);
558        b_type_builder.assert_word_eq(local.instruction.op_b, decoded_rs2);
559
560        let mut imm_le_bits = Vec::new();
561        imm_le_bits.push(AB::Expr::zero());
562        imm_le_bits.extend(local.encoded_instruction_bits[8..12].iter().map(|x| (*x).into()));
563        imm_le_bits.extend(local.encoded_instruction_bits[25..31].iter().map(|x| (*x).into()));
564        imm_le_bits.push(local.encoded_instruction_bits[7].into());
565        imm_le_bits.push(local.encoded_instruction_bits[31].into());
566
567        let signed_extended_imm = Word::from_le_bits::<AB>(&imm_le_bits, true);
568        b_type_builder.assert_word_eq(local.instruction.op_c, signed_extended_imm);
569
570        b_type_builder.assert_zero(local.instruction.imm_b);
571        b_type_builder.assert_one(local.instruction.imm_c);
572    }
573
574    fn s_type_eval<AB: SP1AirBuilder>(
575        &self,
576        builder: &mut AB,
577        local: &InstructionDecodeCols<AB::Var>,
578        decoded_funct3: AB::Expr,
579        decoded_rs1: Word<AB::Expr>,
580        decoded_rs2: Word<AB::Expr>,
581    ) {
582        let mut s_type_builder = builder.when(local.is_s_type);
583
584        s_type_builder.assert_eq(local.funct3, decoded_funct3);
585        s_type_builder.assert_eq(local.funct7, AB::Expr::zero());
586
587        let op_a_word = Word::extend_expr::<AB>(local.instruction.op_a.into());
588        s_type_builder.assert_word_eq(op_a_word, decoded_rs2);
589        s_type_builder.assert_word_eq(local.instruction.op_b, decoded_rs1);
590
591        let mut imm_le_bits = Vec::new();
592        imm_le_bits.extend(local.encoded_instruction_bits[7..12].iter().map(|x| (*x).into()));
593        imm_le_bits.extend(local.encoded_instruction_bits[25..32].iter().map(|x| (*x).into()));
594        let signed_extended_imm = Word::from_le_bits::<AB>(&imm_le_bits, true);
595
596        s_type_builder.assert_word_eq(local.instruction.op_c, signed_extended_imm);
597
598        s_type_builder.assert_zero(local.instruction.imm_b);
599        s_type_builder.assert_one(local.instruction.imm_c);
600    }
601
602    fn u_type_eval<AB: SP1AirBuilder>(
603        &self,
604        builder: &mut AB,
605        local: &InstructionDecodeCols<AB::Var>,
606        decoded_rd: AB::Expr,
607    ) {
608        let mut imm_le_bits = Vec::new();
609        // The first 12 bits are all 0.
610        for _ in 0..12 {
611            imm_le_bits.push(AB::Expr::zero());
612        }
613        imm_le_bits.extend(local.encoded_instruction_bits[12..32].iter().map(|x| (*x).into()));
614
615        let reconstructed_imm = Word::from_le_bits::<AB>(&imm_le_bits, true);
616
617        let mut utype_builder = builder.when(local.is_u_type);
618
619        utype_builder.assert_eq(local.funct3, AB::Expr::zero());
620        utype_builder.assert_eq(local.funct7, AB::Expr::zero());
621
622        utype_builder.assert_eq(local.instruction.op_a, decoded_rd);
623        utype_builder.assert_word_eq(local.instruction.op_b, reconstructed_imm.clone());
624        utype_builder.assert_word_eq(local.instruction.op_c, reconstructed_imm);
625
626        utype_builder.assert_one(local.instruction.imm_b);
627        utype_builder.assert_one(local.instruction.imm_c);
628    }
629}
630
631#[cfg(test)]
632mod tests {
633    #![allow(clippy::print_stdout)]
634
635    use std::sync::Arc;
636
637    use sp1_primitives::SP1Field;
638
639    use slop_matrix::dense::RowMajorMatrix;
640    use sp1_core_executor::{ExecutionRecord, Instruction, Opcode, Program};
641    use sp1_hypercube::air::MachineAir;
642
643    use crate::program::InstructionDecodeChip;
644
645    #[test]
646    fn generate_trace() {
647        // main:
648        //     addi x29, x0, 5
649        //     addi x30, x0, 37
650        //     add x31, x30, x29
651        let instructions = vec![
652            Instruction::new(Opcode::ADDI, 29, 0, 5, false, true),
653            Instruction::new(Opcode::ADDI, 30, 0, 37, false, true),
654            Instruction::new(Opcode::ADD, 31, 30, 29, false, false),
655        ];
656        let shard = ExecutionRecord {
657            program: Arc::new(Program::new(instructions, 0, 0)),
658            ..Default::default()
659        };
660        let chip = InstructionDecodeChip::new();
661        let trace: RowMajorMatrix<SP1Field> =
662            chip.generate_trace(&shard, &mut ExecutionRecord::default());
663        println!("{:?}", trace.values)
664    }
665}
sp1_core_machine/program/instruction_decode.rs

sp1_core_machine/program/
instruction_decode.rs
