o1vm/interpreters/mips/
column.rs

1use crate::{
2    interpreters::mips::Instruction::{self, IType, JType, RType},
3    RelationColumnType,
4};
5use kimchi_msm::{
6    columns::{Column, ColumnIndexer},
7    witness::Witness,
8};
9use std::ops::{Index, IndexMut};
10use strum::EnumCount;
11
12use super::{ITypeInstruction, JTypeInstruction, RTypeInstruction};
13
14pub(crate) const SCRATCH_SIZE_WITHOUT_KECCAK: usize = 45;
15/// The number of hashes performed so far in the block
16pub(crate) const MIPS_HASH_COUNTER_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK;
17/// The number of bytes of the preimage that have been read so far in this hash
18pub(crate) const MIPS_BYTE_COUNTER_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 1;
19/// A flag indicating whether the preimage has been read fully or not
20pub(crate) const MIPS_END_OF_PREIMAGE_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 2;
21/// The number of preimage bytes processed in this step
22pub(crate) const MIPS_NUM_BYTES_READ_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 3;
23/// The at most 4-byte chunk of the preimage that has been read in this step.
24/// Contains a field element of at most 4 bytes.
25pub(crate) const MIPS_PREIMAGE_CHUNK_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 4;
26/// The at most 4-bytes of the preimage that are currently being processed
27/// Consists of 4 field elements of at most 1 byte each.
28pub(crate) const MIPS_PREIMAGE_BYTES_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 5;
29/// The at most 4-bytes of the length that are currently being processed
30pub(crate) const MIPS_LENGTH_BYTES_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 5 + 4;
31/// Flags indicating whether at least N bytes have been processed in this step
32pub(crate) const MIPS_HAS_N_BYTES_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 5 + 4 + 4;
33/// The maximum size of a chunk (4 bytes)
34pub(crate) const MIPS_CHUNK_BYTES_LEN: usize = 4;
35/// The location of the preimage key as a field element of 248bits
36pub(crate) const MIPS_PREIMAGE_KEY: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 5 + 4 + 4 + 4;
37
38// MIPS + hash_counter + byte_counter + eof + num_bytes_read + chunk + bytes
39// + length + has_n_bytes + chunk_bytes + preimage
40pub const SCRATCH_SIZE: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 5 + 4 + 4 + 4 + 1;
41
42/// Number of columns used by the MIPS interpreter to keep values to be
43/// inverted.
44pub const SCRATCH_SIZE_INVERSE: usize = 12;
45
46/// The number of columns used for relation witness in the MIPS circuit
47pub const N_MIPS_REL_COLS: usize = SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2;
48
49/// The number of witness columns used to store the instruction selectors.
50/// NOTE: The +1 is coming from the NoOp instruction.
51pub const N_MIPS_SEL_COLS: usize =
52    RTypeInstruction::COUNT + JTypeInstruction::COUNT + ITypeInstruction::COUNT + 1;
53
54/// All the witness columns used in MIPS
55pub const N_MIPS_COLS: usize = N_MIPS_REL_COLS + N_MIPS_SEL_COLS;
56
57/// Abstract columns (or variables of our multi-variate polynomials) that will
58/// be used to describe our constraints.
59#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
60pub enum ColumnAlias {
61    // Can be seen as the abstract indexed variable X_{i}
62    ScratchState(usize),
63    // A column whose value needs to be inverted in the final witness.
64    // We're keeping a separate column to perform a batch inversion at the end.
65    ScratchStateInverse(usize),
66    InstructionCounter,
67    Selector(usize),
68}
69
70/// The columns used by the MIPS circuit. The MIPS circuit is split into three
71/// main opcodes: RType, JType, IType. The columns are shared between different
72/// instruction types. (the total number of columns refers to the maximum of
73/// columns used by each mode)
74impl From<ColumnAlias> for usize {
75    fn from(alias: ColumnAlias) -> usize {
76        // Note that SCRATCH_SIZE + 1 is for the error
77        match alias {
78            ColumnAlias::ScratchState(i) => {
79                assert!(i < SCRATCH_SIZE);
80                i
81            }
82            ColumnAlias::ScratchStateInverse(i) => {
83                assert!(i < SCRATCH_SIZE_INVERSE);
84                SCRATCH_SIZE + i
85            }
86            ColumnAlias::InstructionCounter => SCRATCH_SIZE + SCRATCH_SIZE_INVERSE,
87            ColumnAlias::Selector(s) => SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 1 + s,
88        }
89    }
90}
91
92/// Returns the corresponding index of the corresponding DynamicSelector column.
93impl From<Instruction> for usize {
94    fn from(instr: Instruction) -> usize {
95        match instr {
96            RType(rtype) => N_MIPS_REL_COLS + rtype as usize,
97            JType(jtype) => N_MIPS_REL_COLS + RTypeInstruction::COUNT + jtype as usize,
98            IType(itype) => {
99                N_MIPS_REL_COLS + RTypeInstruction::COUNT + JTypeInstruction::COUNT + itype as usize
100            }
101            Instruction::NoOp => {
102                N_MIPS_REL_COLS
103                    + RTypeInstruction::COUNT
104                    + JTypeInstruction::COUNT
105                    + ITypeInstruction::COUNT
106            }
107        }
108    }
109}
110
111/// Represents one line of the execution trace of the virtual machine
112/// It contains
113/// + [SCRATCH_SIZE] columns
114/// + 1 column to keep track of the instruction index
115/// + 1 column for the system error code
116/// + [N_MIPS_SEL_COLS]  columns for the instruction selectors.
117///   The columns are, in order,
118/// - the 32 general purpose registers
119/// - the low and hi registers used by some arithmetic instructions
120/// - the current instruction pointer
121/// - the next instruction pointer
122/// - the heap pointer
123/// - the preimage key, split in 8 consecutive columns representing 4 bytes
124///   of the 32 bytes long preimage key
125/// - the preimage offset, i.e. the number of bytes that have been read for the
126///   currently processing preimage
127/// - `[SCRATCH_SIZE] - 46` intermediate columns that can be used by the
128///   instruction set
129/// - the hash counter
130/// - the flag to indicate if the current instruction is a preimage syscall
131/// - the flag to indicate if the current instruction is reading a preimage
132/// - the number of bytes read so far for the current preimage
133/// - how many bytes are left to be read for the current preimage
134/// - the (at most) 4 bytes of the preimage key that are currently being
135///   processed
136/// - 4 helpers to check if at least n bytes were read in the current row
137pub type MIPSWitness<T> = Witness<N_MIPS_COLS, T>;
138
139// IMPLEMENTATIONS FOR COLUMN ALIAS
140
141impl<T: Clone> Index<ColumnAlias> for MIPSWitness<T> {
142    type Output = T;
143
144    /// Map the column alias to the actual column index.
145    fn index(&self, index: ColumnAlias) -> &Self::Output {
146        &self.cols[usize::from(index)]
147    }
148}
149
150impl<T: Clone> IndexMut<ColumnAlias> for MIPSWitness<T> {
151    fn index_mut(&mut self, index: ColumnAlias) -> &mut Self::Output {
152        &mut self.cols[usize::from(index)]
153    }
154}
155
156impl ColumnIndexer<RelationColumnType> for ColumnAlias {
157    const N_COL: usize = N_MIPS_COLS;
158
159    fn to_column(self) -> Column<RelationColumnType> {
160        match self {
161            Self::ScratchState(ss) => {
162                assert!(
163                    ss < SCRATCH_SIZE,
164                    "The maximum index is {}, got {}",
165                    SCRATCH_SIZE,
166                    ss
167                );
168                Column::Relation(RelationColumnType::Scratch(ss))
169            }
170            Self::ScratchStateInverse(ss) => {
171                assert!(
172                    ss < SCRATCH_SIZE_INVERSE,
173                    "The maximum index is {}, got {}",
174                    SCRATCH_SIZE_INVERSE,
175                    ss
176                );
177                Column::Relation(RelationColumnType::ScratchInverse(ss))
178            }
179            Self::InstructionCounter => Column::Relation(RelationColumnType::InstructionCounter),
180            // TODO: what happens with error? It does not have a corresponding alias
181            Self::Selector(s) => {
182                assert!(
183                    s < N_MIPS_SEL_COLS,
184                    "The maximum index is {}, got {}",
185                    N_MIPS_SEL_COLS,
186                    s
187                );
188                Column::DynamicSelector(s)
189            }
190        }
191    }
192}
193
194// IMPLEMENTATIONS FOR SELECTOR
195
196impl<T: Clone> Index<Instruction> for MIPSWitness<T> {
197    type Output = T;
198
199    /// Map the column alias to the actual column index.
200    fn index(&self, index: Instruction) -> &Self::Output {
201        &self.cols[usize::from(index)]
202    }
203}
204
205impl<T: Clone> IndexMut<Instruction> for MIPSWitness<T> {
206    fn index_mut(&mut self, index: Instruction) -> &mut Self::Output {
207        &mut self.cols[usize::from(index)]
208    }
209}
210
211impl ColumnIndexer<usize> for Instruction {
212    const N_COL: usize = N_MIPS_REL_COLS + N_MIPS_SEL_COLS;
213    fn to_column(self) -> Column<usize> {
214        Column::DynamicSelector(usize::from(self) - N_MIPS_REL_COLS)
215    }
216}
o1vm/interpreters/mips/column.rs

o1vm/interpreters/mips/
column.rs
