@@ -3,15 +3,24 @@ use deref::DerefInstruction;
33use dot_product:: DotProductInstruction ;
44use jump:: JumpIfNotZeroInstruction ;
55use multilinear_eval:: MultilinearEvalInstruction ;
6+ use p3_field:: PrimeCharacteristicRing ;
67use p3_symmetric:: Permutation ;
78use poseidon16:: Poseidon2_16Instruction ;
89use poseidon24:: Poseidon2_24Instruction ;
910
11+ use super :: operand:: { MemOrConstant , MemOrFp , MemOrFpOrConstant } ;
1012use crate :: {
13+ air:: constant:: {
14+ COL_INDEX_ADD , COL_INDEX_AUX , COL_INDEX_DEREF , COL_INDEX_FLAG_A , COL_INDEX_FLAG_B ,
15+ COL_INDEX_FLAG_C , COL_INDEX_JUZ , COL_INDEX_MUL , COL_INDEX_OPERAND_A , COL_INDEX_OPERAND_B ,
16+ COL_INDEX_OPERAND_C , N_INSTRUCTION_COLUMNS ,
17+ } ,
18+ bytecode:: operation:: Operation ,
1119 constant:: { DIMENSION , F } ,
1220 context:: run_context:: RunContext ,
1321 errors:: vm:: VirtualMachineError ,
1422 memory:: manager:: MemoryManager ,
23+ witness:: Witness ,
1524} ;
1625
1726pub mod computation;
@@ -107,4 +116,142 @@ impl Instruction {
107116 Self :: MultilinearEval ( instruction) => instruction. execute ( run_context, memory_manager) ,
108117 }
109118 }
119+
120+ /// Generates a witness for a precompile instruction, if applicable.
121+ ///
122+ /// This function checks the instruction type and, if it's a precompile, it calls the
123+ /// corresponding `generate_witness` method to capture the necessary data for the proof.
124+ /// For standard instructions, it returns `Ok(None)`.
125+ pub fn generate_witness (
126+ & self ,
127+ cycle : usize ,
128+ run_context : & RunContext ,
129+ memory_manager : & MemoryManager ,
130+ ) -> Result < Option < Witness > , VirtualMachineError > {
131+ match self {
132+ // If the instruction is Poseidon2_16, generate its witness.
133+ Self :: Poseidon2_16 ( instruction) => Ok ( Some ( Witness :: Poseidon16 (
134+ instruction. generate_witness ( cycle, run_context, memory_manager) ?,
135+ ) ) ) ,
136+ // If the instruction is Poseidon2_24, generate its witness.
137+ Self :: Poseidon2_24 ( instruction) => Ok ( Some ( Witness :: Poseidon24 (
138+ instruction. generate_witness ( cycle, run_context, memory_manager) ?,
139+ ) ) ) ,
140+ // If the instruction is a DotProduct, generate its witness.
141+ Self :: DotProduct ( instruction) => Ok ( Some ( Witness :: DotProduct (
142+ instruction. generate_witness ( cycle, run_context, memory_manager) ?,
143+ ) ) ) ,
144+ // If the instruction is a MultilinearEval, generate its witness.
145+ Self :: MultilinearEval ( instruction) => Ok ( Some ( Witness :: MultilinearEval (
146+ instruction. generate_witness ( cycle, run_context, memory_manager) ?,
147+ ) ) ) ,
148+ // For all other instruction types, no special witness is generated.
149+ _ => Ok ( None ) ,
150+ }
151+ }
152+
153+ /// Converts an instruction into its raw field representation for the execution trace.
154+ #[ must_use]
155+ pub fn field_representation ( & self ) -> Vec < F > {
156+ // Initialize a vector of zeros for all instruction-related columns.
157+ let mut repr = vec ! [ F :: ZERO ; N_INSTRUCTION_COLUMNS ] ;
158+
159+ // Populate the vector based on the instruction type.
160+ match self {
161+ Self :: Computation ( ComputationInstruction {
162+ operation,
163+ arg_a,
164+ arg_b,
165+ res,
166+ } ) => {
167+ // Set the appropriate opcode flag for ADD or MUL.
168+ match operation {
169+ Operation :: Add => repr[ COL_INDEX_ADD ] = F :: ONE ,
170+ Operation :: Mul => repr[ COL_INDEX_MUL ] = F :: ONE ,
171+ }
172+ // Convert operands to their field and flag representations.
173+ let ( op_a, flag_a) = op_to_field ( arg_a) ;
174+ let ( op_b, flag_b) = op_to_field_fp ( arg_b) ;
175+ let ( op_c, flag_c) = op_to_field ( res) ;
176+
177+ // Populate the representation vector.
178+ repr[ COL_INDEX_OPERAND_A ] = op_a;
179+ repr[ COL_INDEX_FLAG_A ] = flag_a;
180+ repr[ COL_INDEX_OPERAND_B ] = op_b;
181+ repr[ COL_INDEX_FLAG_B ] = flag_b;
182+ repr[ COL_INDEX_OPERAND_C ] = op_c;
183+ repr[ COL_INDEX_FLAG_C ] = flag_c;
184+ }
185+ Self :: Deref ( DerefInstruction {
186+ shift_0,
187+ shift_1,
188+ res,
189+ } ) => {
190+ // Set the DEREF opcode flag.
191+ repr[ COL_INDEX_DEREF ] = F :: ONE ;
192+ // The first-level pointer is always a memory access from `fp + shift_0`.
193+ repr[ COL_INDEX_OPERAND_A ] = F :: from_usize ( * shift_0) ;
194+ repr[ COL_INDEX_FLAG_A ] = F :: ZERO ;
195+ // The second-level offset is always an immediate value.
196+ repr[ COL_INDEX_OPERAND_C ] = F :: from_usize ( * shift_1) ;
197+ repr[ COL_INDEX_FLAG_C ] = F :: ONE ;
198+
199+ // Handle the different types of the result operand `res`.
200+ match res {
201+ MemOrFpOrConstant :: Constant ( c) => {
202+ repr[ COL_INDEX_OPERAND_B ] = * c;
203+ repr[ COL_INDEX_FLAG_B ] = F :: ONE ;
204+ repr[ COL_INDEX_AUX ] = F :: ONE ;
205+ }
206+ MemOrFpOrConstant :: MemoryAfterFp { offset } => {
207+ repr[ COL_INDEX_OPERAND_B ] = F :: from_usize ( * offset) ;
208+ repr[ COL_INDEX_FLAG_B ] = F :: ZERO ;
209+ repr[ COL_INDEX_AUX ] = F :: ONE ;
210+ }
211+ MemOrFpOrConstant :: Fp => {
212+ repr[ COL_INDEX_AUX ] = F :: ZERO ;
213+ }
214+ }
215+ }
216+ Self :: JumpIfNotZero ( JumpIfNotZeroInstruction {
217+ condition,
218+ dest,
219+ updated_fp,
220+ } ) => {
221+ // Set the JUZ opcode flag.
222+ repr[ COL_INDEX_JUZ ] = F :: ONE ;
223+ // Convert operands to their field and flag representations.
224+ let ( op_a, flag_a) = op_to_field ( condition) ;
225+ let ( op_b, flag_b) = op_to_field_fp ( updated_fp) ;
226+ let ( op_c, flag_c) = op_to_field ( dest) ;
227+
228+ // Populate the representation vector.
229+ repr[ COL_INDEX_OPERAND_A ] = op_a;
230+ repr[ COL_INDEX_FLAG_A ] = flag_a;
231+ repr[ COL_INDEX_OPERAND_B ] = op_b;
232+ repr[ COL_INDEX_FLAG_B ] = flag_b;
233+ repr[ COL_INDEX_OPERAND_C ] = op_c;
234+ repr[ COL_INDEX_FLAG_C ] = flag_c;
235+ }
236+ // Precompiles do not set flags in the main instruction columns.
237+ _ => { }
238+ }
239+ repr
240+ }
241+ }
242+
243+ /// Helper to convert a `MemOrConstant` operand into its (value, flag) pair.
244+ fn op_to_field ( op : & MemOrConstant ) -> ( F , F ) {
245+ match op {
246+ MemOrConstant :: Constant ( c) => ( * c, F :: ONE ) ,
247+ MemOrConstant :: MemoryAfterFp { offset } => ( F :: from_usize ( * offset) , F :: ZERO ) ,
248+ }
249+ }
250+
251+ /// Helper to convert a `MemOrFp` operand into its (value, flag) pair.
252+ fn op_to_field_fp ( op : & MemOrFp ) -> ( F , F ) {
253+ match op {
254+ MemOrFp :: Fp => ( F :: ZERO , F :: ONE ) , // Represents the `fp` register itself.
255+ MemOrFp :: MemoryAfterFp { offset } => ( F :: from_usize ( * offset) , F :: ZERO ) ,
256+ }
110257}
0 commit comments