|
| 1 | +use std::borrow::Borrow; |
| 2 | + |
| 3 | +use p3_air::{Air, AirBuilder, BaseAir}; |
| 4 | +use p3_field::PrimeCharacteristicRing; |
| 5 | +use p3_matrix::Matrix; |
| 6 | + |
| 7 | +use crate::*; |
| 8 | + |
| 9 | +/* |
| 10 | +
|
| 11 | +Bytecode columns: |
| 12 | +
|
| 13 | +0: OPERAND_A |
| 14 | +1: OPERAND_B |
| 15 | +2: OPERAND_C |
| 16 | +3: FLAG_A |
| 17 | +4: FLAG_B |
| 18 | +5: FLAG_C |
| 19 | +6: ADD |
| 20 | +7: MUL |
| 21 | +8: DEREF |
| 22 | +9: JUZ |
| 23 | +10: AUX |
| 24 | +
|
| 25 | +Execution columns: |
| 26 | +
|
| 27 | +11: VALUE_A (virtual) |
| 28 | +12: VALUE_B (virtual) |
| 29 | +13: VALUE_C (virtual) |
| 30 | +14: PC |
| 31 | +15: FP |
| 32 | +16: ADDR_A |
| 33 | +17: ADDR_B |
| 34 | +18: ADDR_C |
| 35 | +
|
| 36 | +*/ |
| 37 | + |
| 38 | +pub(crate) struct VMAir; |
| 39 | + |
| 40 | +impl<F> BaseAir<F> for VMAir { |
| 41 | + fn width(&self) -> usize { |
| 42 | + N_EXEC_AIR_COLUMNS |
| 43 | + } |
| 44 | + fn structured(&self) -> bool { |
| 45 | + true |
| 46 | + } |
| 47 | + fn degree(&self) -> usize { |
| 48 | + 5 |
| 49 | + } |
| 50 | +} |
| 51 | + |
| 52 | +impl<AB: AirBuilder> Air<AB> for VMAir { |
| 53 | + #[inline] |
| 54 | + fn eval(&self, builder: &mut AB) { |
| 55 | + let main = builder.main(); |
| 56 | + let up = main.row_slice(0).unwrap(); |
| 57 | + let up: &[AB::Var] = (*up).borrow(); |
| 58 | + assert_eq!(up.len(), N_EXEC_AIR_COLUMNS); |
| 59 | + let down = main.row_slice(1).unwrap(); |
| 60 | + let down: &[AB::Var] = (*down).borrow(); |
| 61 | + assert_eq!(down.len(), N_EXEC_AIR_COLUMNS); |
| 62 | + |
| 63 | + let (operand_a, operand_b, operand_c): (AB::Expr, AB::Expr, AB::Expr) = ( |
| 64 | + up[COL_INDEX_OPERAND_A].clone().into(), |
| 65 | + up[COL_INDEX_OPERAND_B].clone().into(), |
| 66 | + up[COL_INDEX_OPERAND_C].clone().into(), |
| 67 | + ); |
| 68 | + let (flag_a, flag_b, flag_c): (AB::Expr, AB::Expr, AB::Expr) = ( |
| 69 | + up[COL_INDEX_FLAG_A].clone().into(), |
| 70 | + up[COL_INDEX_FLAG_B].clone().into(), |
| 71 | + up[COL_INDEX_FLAG_C].clone().into(), |
| 72 | + ); |
| 73 | + let add: AB::Expr = up[COL_INDEX_ADD].clone().into(); |
| 74 | + let mul: AB::Expr = up[COL_INDEX_MUL].clone().into(); |
| 75 | + let deref: AB::Expr = up[COL_INDEX_DEREF].clone().into(); |
| 76 | + let juz: AB::Expr = up[COL_INDEX_JUZ].clone().into(); |
| 77 | + let aux: AB::Expr = up[COL_INDEX_AUX].clone().into(); |
| 78 | + |
| 79 | + let (value_a, value_b, value_c): (AB::Expr, AB::Expr, AB::Expr) = ( |
| 80 | + up[COL_INDEX_MEM_VALUE_A.index_in_air()].clone().into(), |
| 81 | + up[COL_INDEX_MEM_VALUE_B.index_in_air()].clone().into(), |
| 82 | + up[COL_INDEX_MEM_VALUE_C.index_in_air()].clone().into(), |
| 83 | + ); |
| 84 | + let (pc, next_pc): (AB::Expr, AB::Expr) = ( |
| 85 | + up[COL_INDEX_PC.index_in_air()].clone().into(), |
| 86 | + down[COL_INDEX_PC.index_in_air()].clone().into(), |
| 87 | + ); |
| 88 | + let (fp, next_fp): (AB::Expr, AB::Expr) = ( |
| 89 | + up[COL_INDEX_FP.index_in_air()].clone().into(), |
| 90 | + down[COL_INDEX_FP.index_in_air()].clone().into(), |
| 91 | + ); |
| 92 | + let (addr_a, addr_b, addr_c): (AB::Expr, AB::Expr, AB::Expr) = ( |
| 93 | + up[COL_INDEX_MEM_ADDRESS_A.index_in_air()].clone().into(), |
| 94 | + up[COL_INDEX_MEM_ADDRESS_B.index_in_air()].clone().into(), |
| 95 | + up[COL_INDEX_MEM_ADDRESS_C.index_in_air()].clone().into(), |
| 96 | + ); |
| 97 | + |
| 98 | + let nu_a = |
| 99 | + flag_a.clone() * operand_a.clone() + value_a.clone() * (AB::Expr::ONE - flag_a.clone()); |
| 100 | + let nu_b = |
| 101 | + flag_b.clone() * operand_b.clone() + value_b.clone() * (AB::Expr::ONE - flag_b.clone()); |
| 102 | + let nu_c = flag_c.clone() * fp.clone() + value_c.clone() * (AB::Expr::ONE - flag_c.clone()); |
| 103 | + |
| 104 | + builder.assert_zero( |
| 105 | + (AB::Expr::ONE - flag_a.clone()) * (addr_a.clone() - (fp.clone() + operand_a.clone())), |
| 106 | + ); |
| 107 | + builder.assert_zero( |
| 108 | + (AB::Expr::ONE - flag_b.clone()) * (addr_b.clone() - (fp.clone() + operand_b.clone())), |
| 109 | + ); |
| 110 | + builder.assert_zero( |
| 111 | + (AB::Expr::ONE - flag_c.clone()) * (addr_c.clone() - (fp.clone() + operand_c.clone())), |
| 112 | + ); |
| 113 | + |
| 114 | + builder.assert_zero(add.clone() * (nu_b.clone() - (nu_a.clone() + nu_c.clone()))); |
| 115 | + builder.assert_zero(mul.clone() * (nu_b.clone() - nu_a.clone() * nu_c.clone())); |
| 116 | + |
| 117 | + builder |
| 118 | + .assert_zero(deref.clone() * (addr_c.clone() - (value_a.clone() + operand_c.clone()))); |
| 119 | + builder.assert_zero(deref.clone() * aux.clone() * (value_c.clone() - nu_b.clone())); |
| 120 | + builder.assert_zero( |
| 121 | + deref.clone() * (AB::Expr::ONE - aux.clone()) * (value_c.clone() - fp.clone()), |
| 122 | + ); |
| 123 | + |
| 124 | + builder.assert_zero( |
| 125 | + (AB::Expr::ONE - juz.clone()) * (next_pc.clone() - (pc.clone() + AB::Expr::ONE)), |
| 126 | + ); |
| 127 | + builder.assert_zero((AB::Expr::ONE - juz.clone()) * (next_fp.clone() - fp.clone())); |
| 128 | + |
| 129 | + builder.assert_zero(juz.clone() * nu_a.clone() * (AB::Expr::ONE - nu_a.clone())); |
| 130 | + builder.assert_zero(juz.clone() * nu_a.clone() * (next_pc.clone() - nu_b.clone())); |
| 131 | + builder.assert_zero(juz.clone() * nu_a.clone() * (next_fp.clone() - nu_c.clone())); |
| 132 | + builder.assert_zero( |
| 133 | + juz.clone() |
| 134 | + * (AB::Expr::ONE - nu_a.clone()) |
| 135 | + * (next_pc.clone() - (pc.clone() + AB::Expr::ONE)), |
| 136 | + ); |
| 137 | + builder.assert_zero( |
| 138 | + juz.clone() * (AB::Expr::ONE - nu_a.clone()) * (next_fp.clone() - fp.clone()), |
| 139 | + ); |
| 140 | + } |
| 141 | +} |
0 commit comments