|
| 1 | +use stwo_prover::{constraint_framework::logup::LookupElements, core::fields::m31::BaseField}; |
| 2 | + |
| 3 | +use crate::{ |
| 4 | + components::MAX_LOOKUP_TUPLE_SIZE, |
| 5 | + trace::{ |
| 6 | + eval::TraceEval, program_trace::ProgramTracesBuilder, sidenote::SideNote, ProgramStep, |
| 7 | + TracesBuilder, |
| 8 | + }, |
| 9 | + traits::MachineChip, |
| 10 | + virtual_column::{self, VirtualColumn}, |
| 11 | +}; |
| 12 | + |
| 13 | +use nexus_vm::riscv::InstructionType::BType; |
| 14 | + |
| 15 | +use crate::column::Column; |
| 16 | + |
| 17 | +use crate::trace::eval::trace_eval; |
| 18 | + |
| 19 | +pub struct TypeBChip; |
| 20 | + |
| 21 | +impl MachineChip for TypeBChip { |
| 22 | + fn fill_main_trace( |
| 23 | + traces: &mut TracesBuilder, |
| 24 | + row_idx: usize, |
| 25 | + vm_step: &Option<ProgramStep>, |
| 26 | + _program_trace: &mut ProgramTracesBuilder, |
| 27 | + _side_note: &mut SideNote, |
| 28 | + ) { |
| 29 | + let vm_step = match vm_step { |
| 30 | + Some(vm_step) => vm_step, |
| 31 | + None => { |
| 32 | + return; |
| 33 | + } |
| 34 | + }; |
| 35 | + let step = &vm_step.step; |
| 36 | + if step.instruction.ins_type != BType { |
| 37 | + return; |
| 38 | + } |
| 39 | + let op_c_raw = vm_step.step.instruction.op_c; |
| 40 | + |
| 41 | + // Fill auxiliary columns for type B immediate value parsing |
| 42 | + let op_c1_4 = ((op_c_raw >> 1) & 0b1111) as u8; |
| 43 | + let op_c5_7 = ((op_c_raw >> 5) & 0b111) as u8; |
| 44 | + let op_c8_10 = ((op_c_raw >> 8) & 0b111) as u8; |
| 45 | + let op_c11 = ((op_c_raw >> 11) & 0b1) as u8; |
| 46 | + let op_c12 = ((op_c_raw >> 12) & 0b1) as u8; |
| 47 | + |
| 48 | + traces.fill_columns(row_idx, op_c1_4, Column::OpC1_4); |
| 49 | + traces.fill_columns(row_idx, op_c5_7, Column::OpC5_7); |
| 50 | + traces.fill_columns(row_idx, op_c8_10, Column::OpC8_10); |
| 51 | + traces.fill_columns(row_idx, op_c11, Column::OpC11); |
| 52 | + traces.fill_columns(row_idx, op_c12, Column::OpC12); |
| 53 | + |
| 54 | + let op_a_raw = vm_step.step.instruction.op_a as u8; |
| 55 | + let op_a0 = op_a_raw & 0x1; |
| 56 | + let op_a1_4 = (op_a_raw >> 1) & 0b1111; |
| 57 | + |
| 58 | + traces.fill_columns(row_idx, op_a0, Column::OpA0); |
| 59 | + traces.fill_columns(row_idx, op_a1_4, Column::OpA1_4); |
| 60 | + |
| 61 | + let op_b_raw = vm_step.step.instruction.op_b as u8; |
| 62 | + let op_b0_3 = op_b_raw & 0b1111; |
| 63 | + let op_b4 = (op_b_raw >> 4) & 0b1; |
| 64 | + traces.fill_columns(row_idx, op_b0_3, Column::OpB0_3); |
| 65 | + traces.fill_columns(row_idx, op_b4, Column::OpB4); |
| 66 | + } |
| 67 | + |
| 68 | + fn add_constraints<E: stwo_prover::constraint_framework::EvalAtRow>( |
| 69 | + eval: &mut E, |
| 70 | + trace_eval: &TraceEval<E>, |
| 71 | + _lookup_elements: &LookupElements<MAX_LOOKUP_TUPLE_SIZE>, |
| 72 | + ) { |
| 73 | + let [is_type_b] = virtual_column::IsTypeB::eval(trace_eval); |
| 74 | + let [op_c1_4] = trace_eval!(trace_eval, Column::OpC1_4); |
| 75 | + let [op_c5_7] = trace_eval!(trace_eval, Column::OpC5_7); |
| 76 | + let [op_c8_10] = trace_eval!(trace_eval, Column::OpC8_10); |
| 77 | + let [op_c11] = trace_eval!(trace_eval, Column::OpC11); |
| 78 | + let [op_c12] = trace_eval!(trace_eval, Column::OpC12); |
| 79 | + let [op_c] = trace_eval!(trace_eval, Column::OpC); |
| 80 | + |
| 81 | + // Making sure that op_c matches its parts |
| 82 | + |
| 83 | + // is_type_b・(op_c1_4・2 + op_c5_7・2^5 + op_c8_10・2^8 + op_c11・2^11 + op_c12・2^12 – op_c) = 0 |
| 84 | + eval.add_constraint( |
| 85 | + is_type_b.clone() |
| 86 | + * (op_c1_4.clone() * BaseField::from(2) |
| 87 | + + op_c5_7.clone() * BaseField::from(1 << 5) |
| 88 | + + op_c8_10.clone() * BaseField::from(1 << 8) |
| 89 | + + op_c11.clone() * BaseField::from(1 << 11) |
| 90 | + + op_c12.clone() * BaseField::from(1 << 12) |
| 91 | + - op_c.clone()), |
| 92 | + ); |
| 93 | + |
| 94 | + let value_c = trace_eval!(trace_eval, Column::ValueC); |
| 95 | + |
| 96 | + // Computing c_val limbs and performing sign extension |
| 97 | + // (is_type_b)・ (op_c1_4・2 + op_c5_7・2^5 – c_val_1) = 0 // limb 1 |
| 98 | + // (is_type_b)・ (op_c8_10 + op_c11・2^3 + op_c12・(2^4-1)·2^4 – c_val_2) = 0 // limb 2 |
| 99 | + // (is_type_b)・ (op_c12・(2^8-1) – c_val_3) = 0 // limb 3 |
| 100 | + // (is_type_b)・ (op_c12・(2^8-1) – c_val_4) = 0 // limb 4 |
| 101 | + eval.add_constraint( |
| 102 | + is_type_b.clone() |
| 103 | + * (op_c1_4.clone() * BaseField::from(2) |
| 104 | + + op_c5_7.clone() * BaseField::from(1 << 5) |
| 105 | + - value_c[0].clone()), |
| 106 | + ); |
| 107 | + eval.add_constraint( |
| 108 | + is_type_b.clone() |
| 109 | + * (op_c8_10.clone() |
| 110 | + + op_c11.clone() * BaseField::from(1 << 3) |
| 111 | + + op_c12.clone() * BaseField::from((1 << 4) - 1) * BaseField::from(1 << 4) |
| 112 | + - value_c[1].clone()), |
| 113 | + ); |
| 114 | + eval.add_constraint( |
| 115 | + is_type_b.clone() |
| 116 | + * (op_c12.clone() * BaseField::from((1 << 8) - 1) - value_c[2].clone()), |
| 117 | + ); |
| 118 | + eval.add_constraint( |
| 119 | + is_type_b.clone() |
| 120 | + * (op_c12.clone() * BaseField::from((1 << 8) - 1) - value_c[3].clone()), |
| 121 | + ); |
| 122 | + |
| 123 | + let [op_a] = trace_eval!(trace_eval, Column::OpA); |
| 124 | + let [op_a0] = trace_eval!(trace_eval, Column::OpA0); |
| 125 | + let [op_a1_4] = trace_eval!(trace_eval, Column::OpA1_4); |
| 126 | + |
| 127 | + // Making sure that op_a matches its parts |
| 128 | + // (is_type_b)・ (op_a0 + op_a1_4・2 – op_a) = 0 |
| 129 | + eval.add_constraint( |
| 130 | + is_type_b.clone() |
| 131 | + * (op_a0.clone() + op_a1_4.clone() * BaseField::from(2) - op_a.clone()), |
| 132 | + ); |
| 133 | + |
| 134 | + let [op_b] = trace_eval!(trace_eval, Column::OpB); |
| 135 | + let [op_b0_3] = trace_eval!(trace_eval, Column::OpB0_3); |
| 136 | + let [op_b4] = trace_eval!(trace_eval, Column::OpB4); |
| 137 | + // Making sure that op_b matches its parts |
| 138 | + |
| 139 | + // (is_type_b)・ (op_b0_3 + op_b4・2^4 – op_b) = 0 |
| 140 | + eval.add_constraint( |
| 141 | + is_type_b.clone() |
| 142 | + * (op_b0_3.clone() + op_b4.clone() * BaseField::from(1 << 4) - op_b.clone()), |
| 143 | + ); |
| 144 | + |
| 145 | + let value_instr = trace_eval!(trace_eval, Column::InstrVal); |
| 146 | + // checking format of instructions - limb 1 |
| 147 | + // (is_type_b) ・ (b1100011 + op_c11 - instr_val_1) = 0 // limb 1 |
| 148 | + eval.add_constraint( |
| 149 | + is_type_b.clone() |
| 150 | + * (E::F::from(BaseField::from(0b1100011)) + op_c11.clone() |
| 151 | + - value_instr[0].clone()), |
| 152 | + ); |
| 153 | + |
| 154 | + let [is_beq] = trace_eval!(trace_eval, Column::IsBeq); |
| 155 | + let [is_bne] = trace_eval!(trace_eval, Column::IsBne); |
| 156 | + let [is_blt] = trace_eval!(trace_eval, Column::IsBlt); |
| 157 | + let [is_bge] = trace_eval!(trace_eval, Column::IsBge); |
| 158 | + let [is_bltu] = trace_eval!(trace_eval, Column::IsBltu); |
| 159 | + let [is_bgeu] = trace_eval!(trace_eval, Column::IsBgeu); |
| 160 | + |
| 161 | + // checking format of instructions - limb 2 |
| 162 | + // (is_beq) ・ (op_c1_4 + b000・2^4 + op_a0・2^7 - instr_val_2) = 0 // limb 2 - beq |
| 163 | + // (is_bne) ・ (op_c1_4 + b001・2^4 + op_a0・2^7 - instr_val_2) = 0 // limb 2 - bne |
| 164 | + // (is_blt) ・ (op_c1_4 + b100・2^4 + op_a0・2^7 - instr_val_2) = 0 // limb 2 - blt |
| 165 | + // (is_bge) ・ (op_c1_4 + b101・2^4 + op_a0・2^7 - instr_val_2) = 0 // limb 2 - bge |
| 166 | + // (is_bltu)・ (op_c1_4 + b110・2^4 + op_a0・2^7 - instr_val_2) = 0 // limb 2 - bltu |
| 167 | + // (is_bgeu)・ (op_c1_4 + b111・2^4 + op_a0・2^7 - instr_val_2) = 0 // limb 2 - bgeu |
| 168 | + |
| 169 | + eval.add_constraint( |
| 170 | + is_beq |
| 171 | + * (op_c1_4.clone() |
| 172 | + + E::F::from(BaseField::from(0b000) * BaseField::from(1 << 4)) |
| 173 | + + op_a0.clone() * BaseField::from(1 << 7) |
| 174 | + - value_instr[1].clone()), |
| 175 | + ); |
| 176 | + |
| 177 | + eval.add_constraint( |
| 178 | + is_bne |
| 179 | + * (op_c1_4.clone() |
| 180 | + + E::F::from(BaseField::from(0b001) * BaseField::from(1 << 4)) |
| 181 | + + op_a0.clone() * BaseField::from(1 << 7) |
| 182 | + - value_instr[1].clone()), |
| 183 | + ); |
| 184 | + eval.add_constraint( |
| 185 | + is_blt |
| 186 | + * (op_c1_4.clone() |
| 187 | + + E::F::from(BaseField::from(0b100) * BaseField::from(1 << 4)) |
| 188 | + + op_a0.clone() * BaseField::from(1 << 7) |
| 189 | + - value_instr[1].clone()), |
| 190 | + ); |
| 191 | + eval.add_constraint( |
| 192 | + is_bge |
| 193 | + * (op_c1_4.clone() |
| 194 | + + E::F::from(BaseField::from(0b101) * BaseField::from(1 << 4)) |
| 195 | + + op_a0.clone() * BaseField::from(1 << 7) |
| 196 | + - value_instr[1].clone()), |
| 197 | + ); |
| 198 | + eval.add_constraint( |
| 199 | + is_bltu |
| 200 | + * (op_c1_4.clone() |
| 201 | + + E::F::from(BaseField::from(0b110) * BaseField::from(1 << 4)) |
| 202 | + + op_a0.clone() * BaseField::from(1 << 7) |
| 203 | + - value_instr[1].clone()), |
| 204 | + ); |
| 205 | + eval.add_constraint( |
| 206 | + is_bgeu |
| 207 | + * (op_c1_4.clone() |
| 208 | + + E::F::from(BaseField::from(0b111) * BaseField::from(1 << 4)) |
| 209 | + + op_a0.clone() * BaseField::from(1 << 7) |
| 210 | + - value_instr[1].clone()), |
| 211 | + ); |
| 212 | + |
| 213 | + // checking format of instructions - limb 3 |
| 214 | + // (is_type_b) ・ (op_a1_4 + op_b0_3・2^4 - instr_val_3) = 0 // limb 3 |
| 215 | + eval.add_constraint( |
| 216 | + is_type_b.clone() |
| 217 | + * (op_a1_4.clone() + op_b0_3.clone() * BaseField::from(1 << 4) |
| 218 | + - value_instr[2].clone()), |
| 219 | + ); |
| 220 | + |
| 221 | + let [op_b4] = trace_eval!(trace_eval, Column::OpB4); |
| 222 | + // checking format of instructions - limb 4 |
| 223 | + // (is_type_b) ・ (op_b4 + op_c5_7・2 + op_c8_10・2^4 + op_c12・2^7 - instr_val_4) = 0 // limb 4 |
| 224 | + eval.add_constraint( |
| 225 | + is_type_b.clone() |
| 226 | + * (op_b4 |
| 227 | + + op_c5_7.clone() * BaseField::from(2) |
| 228 | + + op_c8_10.clone() * BaseField::from(1 << 4) |
| 229 | + + op_c12.clone() * BaseField::from(1 << 7) |
| 230 | + - value_instr[3].clone()), |
| 231 | + ); |
| 232 | + } |
| 233 | +} |
0 commit comments