@@ -8,7 +8,7 @@ use crate::{
88 } ,
99 context:: run_context:: RunContext ,
1010 errors:: { math:: MathError , memory:: MemoryError , vm:: VirtualMachineError } ,
11- memory:: { manager:: MemoryManager , val:: MemoryValue } ,
11+ memory:: { address :: MemoryAddress , manager:: MemoryManager , val:: MemoryValue } ,
1212} ;
1313
1414#[ derive( Debug , Default ) ]
@@ -246,26 +246,73 @@ impl VirtualMachine {
246246 Ok ( ( ) )
247247 }
248248
249- /// Executes a double-dereference instruction ( `res = m[m[fp + shift_0] + shift_1]`) and asserts the result .
249+ /// Executes the `DEREF` instruction: `res = m[m[fp + shift_0] + shift_1]`.
250250 ///
251- /// This function handles instructions that require reading a pointer from one memory
252- /// location to access a value at another.
251+ /// It operates using a constraint satisfaction model with two primary modes:
253252 ///
254- /// # Errors
255- /// This function will return an `Err` if:
256- /// - Any memory access targets an uninitialized memory cell.
257- /// - The first memory access at `m[fp + shift_0]` does not yield a valid `MemoryAddress`.
258- /// - The final, dereferenced value does not match the expected value specified by `res`.
253+ /// 1. **Deduction of `res`**: If the `res` operand points to an unwritten memory
254+ /// location, this function performs the double-dereference to find the final
255+ /// value and writes it into `res`'s location.
256+ ///
257+ /// 2. **Constraint of `m[...]`**: If `res` holds a known value, that value is
258+ /// written to the final dereferenced address. The underlying memory model
259+ /// ensures this write is consistent, effectively asserting that
260+ /// `m[m[...]]` must equal the known `res` value.
259261 fn execute_deref < F > (
260- & self ,
261- _shift_0 : usize ,
262- _shift_1 : usize ,
263- _res : & MemOrFpOrConstant < F > ,
262+ & mut self ,
263+ shift_0 : usize ,
264+ shift_1 : usize ,
265+ res : & MemOrFpOrConstant < F > ,
264266 ) -> Result < ( ) , VirtualMachineError < F > >
265267 where
266268 F : PrimeField64 ,
267269 {
268- // TODO: implement this instruction.
270+ // Resolve the `res` operand first to determine which execution path to take.
271+ //
272+ // This will either be
273+ // - a known `Int`,
274+ // - an `Address` to an unwritten cell.
275+ let res_lookup_result = self
276+ . run_context
277+ . value_from_mem_or_fp_or_constant ( res, & self . memory_manager ) ?;
278+
279+ // Calculate the address of the first-level pointer, `fp + shift_0`.
280+ let ptr_shift_0_addr = self . run_context . fp . add_usize ( shift_0) ?;
281+
282+ // Read the pointer from memory. It must be a `MemoryAddress` type.
283+ let ptr: MemoryAddress = self
284+ . memory_manager
285+ . get ( ptr_shift_0_addr)
286+ . ok_or ( MemoryError :: UninitializedMemory ( ptr_shift_0_addr) ) ?
287+ . try_into ( ) ?;
288+
289+ // Calculate the final, second-level address: `ptr + shift_1`.
290+ let ptr_shift_1_addr = ptr. add_usize ( shift_1) ?;
291+
292+ // Branch execution based on whether `res` was a known value or an unwritten address.
293+ match res_lookup_result {
294+ // Case 1: `res` is an unwritten memory location.
295+ //
296+ // We deduce its value by reading from the final address.
297+ MemoryValue :: Address ( addr) => {
298+ // Read the value from the final dereferenced address `m[ptr + shift_1]`.
299+ let value = self
300+ . memory_manager
301+ . get ( ptr_shift_1_addr)
302+ . ok_or ( MemoryError :: UninitializedMemory ( ptr_shift_1_addr) ) ?;
303+
304+ // Write the deduced value into `res`'s memory location.
305+ self . memory_manager . memory . insert ( addr, value) ?;
306+ }
307+ // Case 2: `res` is a known integer value.
308+ //
309+ // We use this value to constrain the memory at the final address.
310+ MemoryValue :: Int ( value) => {
311+ // Write the known `res` value to the final dereferenced address.
312+ self . memory_manager . memory . insert ( ptr_shift_1_addr, value) ?;
313+ }
314+ }
315+
269316 Ok ( ( ) )
270317 }
271318
0 commit comments