memory_opt_opcodes: constraints for MLOAD/MSTORE/MSTORE8

Author: Aurélien Nicolas

bus-mapping/src/circuit_input_builder/input_state_ref.rs

@@ -276,6 +276,7 @@ impl<'a> CircuitInputStateRef<'a> {
         step: &mut ExecStep,
         address: MemoryAddress, //Caution: make sure this address = slot passing
         value: Word,
+        // TODO: take value_prev as parameter.
     ) -> Result<(), Error> {
         let call_id = self.call()?.call_id;
         self.push_op(step, RW::WRITE, MemoryWordOp::new(call_id, address, value));

bus-mapping/src/evm/opcodes/mload.rs

@@ -28,57 +28,35 @@ impl Opcode for Mload {
         // Manage first stack read at latest stack position
         state.stack_read(&mut exec_step, stack_position, stack_value_read)?;
 
-        // Read the memory
-        let mut mem_read_addr: MemoryAddress = stack_value_read.try_into()?;
-        // Accesses to memory that hasn't been initialized are valid, and return
-        // 0.
+        // Read the memory value from the next step of the trace.
         let mem_read_value = geth_steps[1].stack.last()?;
 
-        // TODO: get two memory words (slot, slot + 32) at address if offset != 0, otherwise get one
-        // word at slot.
-        let mut memory = state.call_ctx_mut()?.memory.clone();
-        println!("before mload memory length is {}", memory.0.len());
-
         let offset = stack_value_read.as_u64();
-        // expand to offset + 64 to enusre addr_right_Word without out of boundary
-        let minimal_length = offset + 64;
-
-        memory.extend_at_least(minimal_length as usize);
-
         let shift = offset % 32;
         let slot = offset - shift;
-        println!(
-            "minimal_length {} , slot {},  shift {}, memory_length {}",
-            minimal_length,
-            slot,
-            shift,
-            memory.0.len()
-        );
+        println!("shift {}, slot {}", shift, slot);
 
-        let mut slot_bytes: [u8; 32] = [0; 32];
-        slot_bytes.clone_from_slice(&memory.0[(slot as usize)..(slot as usize + 32)]);
+        let (left_word, right_word) = {
+            // Get the memory chunk that contains the word, starting at an aligned slot address.
+            let slots_content = state.call_ctx()?.memory.read_chunk(slot.into(), 64.into());
 
-        let addr_left_Word = Word::from_big_endian(&slot_bytes);
-        // TODO: edge case: if shift = 0, skip to read right word ?
-        let mut word_right_bytes: [u8; 32] = [0; 32];
-        slot_bytes.clone_from_slice(&memory.0[(slot + 32) as usize..(slot + 64) as usize]);
-
-        let addr_right_Word = Word::from_little_endian(&word_right_bytes);
+            (
+                Word::from_little_endian(&slots_content[..32]),
+                Word::from_little_endian(&slots_content[32..64]),
+            )
+        };
 
         // First stack write
-        //
         state.stack_write(&mut exec_step, stack_position, mem_read_value)?;
 
-        // First mem read -> 32 MemoryOp generated.
-        state.memory_read_word(&mut exec_step, slot.into(), addr_left_Word)?;
-        state.memory_read_word(&mut exec_step, (slot + 32).into(), addr_right_Word)?;
+        state.memory_read_word(&mut exec_step, slot.into(), left_word)?;
+        state.memory_read_word(&mut exec_step, (slot + 32).into(), right_word)?;
 
-        // reconstruction
-        // "minimal_length - 32" subtract 32 as actual expansion size
+        // Expand memory if needed.
         state
             .call_ctx_mut()?
             .memory
-            .extend_at_least((minimal_length - 32) as usize);
+            .extend_at_least((offset + 32) as usize);
 
         Ok(vec![exec_step])
     }

bus-mapping/src/evm/opcodes/mstore.rs

@@ -30,102 +30,57 @@ impl<const IS_MSTORE8: bool> Opcode for Mstore<IS_MSTORE8> {
         let value_pos = geth_step.stack.nth_last_filled(1);
         state.stack_read(&mut exec_step, value_pos, value)?;
 
-        // First mem write -> 32 MemoryOp generated.
-        let offset_addr: MemoryAddress = offset.try_into()?;
-        // TODO: get two memory words (slot, slot + 32) at address if offset != 0, otherwise get one
-        // word at slot.
-
-        let mut memory = state.call_ctx_mut()?.memory.clone();
-        // expand memory size + 64 as slot
-        let minimal_length = offset_addr.0
-            + if IS_MSTORE8 {
-                1
-            } else {
-                64 /* 32 */
-            };
-        println!(
-            "minimal_length {} , IS_MSTORE8 {}, memory_length {}, value {}",
-            minimal_length,
-            IS_MSTORE8,
-            memory.0.len(),
-            value
-        );
-
-        memory.extend_at_least(minimal_length);
-
-        let offset_u64 = offset.as_u64();
+        let offset_u64 = offset.as_u64() as usize;
         let shift = offset_u64 % 32;
         let slot = offset_u64 - shift;
         println!("shift {}, slot {}", shift, slot);
-        // reconstruct memory with value
-        match IS_MSTORE8 {
-            true => {
-                //let bytes=  *value.to_le_bytes().to_vec();
-                let val = *value.to_le_bytes().first().unwrap();
-                let word_v8 = Word::from(val as u64);
-                memory.0[offset_u64 as usize] = val;
-            }
-            false => {
-                let bytes = value.to_be_bytes();
-                memory[offset_u64 as usize..offset_u64 as usize + 32].copy_from_slice(&bytes);
-            }
-        }
 
-        // after memory construction, we can get slot_Word(left_Word), right_word to fill buss
-        // mapping.
-        let mut slot_bytes: [u8; 32] = [0; 32];
-        let mut addr_left_Word = Word::zero();
+        let (left_word, right_word) = {
+            // Get the memory chunk that contains the word, starting at an aligned slot address.
+            let mut slots_content = state.call_ctx()?.memory.read_chunk(slot.into(), 64.into());
+
+            // reconstruct memory with value
+            match IS_MSTORE8 {
+                true => {
+                    let val = *value.to_le_bytes().first().unwrap();
+                    slots_content[shift] = val;
+                }
+                false => {
+                    let bytes = value.to_be_bytes();
+                    slots_content[shift..shift + 32].copy_from_slice(&bytes);
+                }
+            }
 
-        if IS_MSTORE8 {
-            let byte = *value.to_le_bytes().first().unwrap();
-            addr_left_Word = Word::from(byte as u64);
-        } else {
-            slot_bytes.clone_from_slice(&memory.0[(slot as usize)..(slot as usize + 32)]);
-            addr_left_Word = Word::from_big_endian(&slot_bytes);
-        }
+            // after memory construction, we can get the left and right words to fill bus mapping.
+            (
+                Word::from_little_endian(&slots_content[..32]),
+                Word::from_little_endian(&slots_content[32..64]),
+            )
+        };
 
-        // TODO: edge case: if shift = 0, no need to right word
-        let mut word_right_bytes: [u8; 32] = [0; 32];
-        let cur_memory_size = memory.0.len();
-        // when is_msotre8, skip word_right as mstore8 only affect one word.
+        // memory write left word for mstore8 and mstore.
+        state.memory_write_word(&mut exec_step, slot.into(), left_word)?;
 
-        // construct right word
-        let addr_right_Word = Word::from_big_endian(&word_right_bytes);
+        if !IS_MSTORE8 {
+            // memory write right word for mstore
+            state.memory_write_word(&mut exec_step, (slot + 32).into(), right_word)?;
 
-        // address = 100, slot = 96 shift = 4
-        // value = address + 32 = 132
-        // left word = slot ( 96...96+32 bytes) slot = 128...128+32 word(fill 0)
-        match IS_MSTORE8 {
-            true => {
-                // memory write operation for mstore8
-                state.memory_write_word(&mut exec_step, slot.into(), addr_left_Word)?;
-            }
-            false => {
-                // lookup left word
-                state.memory_write_word(&mut exec_step, slot.into(), addr_left_Word)?;
-                // look up right word
-                state.memory_write_word(&mut exec_step, (slot + 32).into(), addr_right_Word)?;
-            }
+            // TODO: edge case: if shift = 0, we could skip the right word?
         }
 
         // reconstruction
-        let offset = geth_step.stack.nth_last(0)?;
-        let value = geth_step.stack.nth_last(1)?;
-        let offset_addr: MemoryAddress = offset.try_into()?;
 
-        let minimal_length = offset_addr.0 + if IS_MSTORE8 { 1 } else { 32 };
+        let minimal_length = offset_u64 + if IS_MSTORE8 { 1 } else { 32 };
         state.call_ctx_mut()?.memory.extend_at_least(minimal_length);
 
-        let mem_starts = offset_addr.0;
-
         match IS_MSTORE8 {
             true => {
                 let val = *value.to_le_bytes().first().unwrap();
-                state.call_ctx_mut()?.memory.0[mem_starts] = val;
+                state.call_ctx_mut()?.memory.0[offset_u64] = val;
             }
             false => {
                 let bytes = value.to_be_bytes();
-                state.call_ctx_mut()?.memory[mem_starts..mem_starts + 32].copy_from_slice(&bytes);
+                state.call_ctx_mut()?.memory[offset_u64..offset_u64 + 32].copy_from_slice(&bytes);
             }
         }
 

zkevm-circuits/src/evm_circuit/execution/memory.rs

@@ -1,7 +1,7 @@
 use crate::{
     evm_circuit::{
         execution::ExecutionGadget,
-        param::{N_BYTES_MEMORY_ADDRESS, N_BYTES_MEMORY_WORD_SIZE},
+        param::{N_BYTES_MEMORY_ADDRESS, N_BYTES_MEMORY_CHUNK, N_BYTES_MEMORY_WORD_SIZE},
         step::ExecutionState,
         util::{
             common_gadget::SameContextGadget,
@@ -11,13 +11,14 @@ use crate::{
             },
             from_bytes,
             math_gadget::IsEqualGadget,
-            memory_gadget::{MemoryExpansionGadget, MemoryWordAddress},
+            memory_gadget::{MemoryExpansionGadget, MemoryMask, MemoryWordAddress},
             not, CachedRegion, Cell, MemoryAddress, Word,
         },
         witness::{Block, Call, ExecStep, Transaction},
     },
     util::Expr,
 };
+use array_init::array_init;
 use eth_types::{evm_types::OpcodeId, Field, ToLittleEndian, U256};
 use halo2_proofs::{circuit::Value, plonk::Error};
 
@@ -31,14 +32,20 @@ pub(crate) struct MemoryGadget<F> {
     //address: MemoryAddress<F>,
     address: MemoryWordAddress<F>,
     // consider move to MemoryWordAddress ?
+    /// The value poped from or pushed to the stack.
     value: Word<F>,
+    /// The left memory word read or written.
     value_left: Word<F>,
+    /// The left memory word before the write.
+    value_left_prev: Word<F>,
+    /// The right memory word read or written.
     value_right: Word<F>,
+    /// The right memory word before the write.
+    value_right_prev: Word<F>,
     memory_expansion: MemoryExpansionGadget<F, 1, N_BYTES_MEMORY_WORD_SIZE>,
     is_mload: IsEqualGadget<F>,
     is_mstore8: IsEqualGadget<F>,
-    // TODO: add mask
-    // mask: [Cell<F>, 5]
+    mask: MemoryMask<F>,
 }
 
 impl<F: Field> ExecutionGadget<F> for MemoryGadget<F> {
@@ -52,9 +59,12 @@ impl<F: Field> ExecutionGadget<F> for MemoryGadget<F> {
         // In successful case the address must be in 5 bytes
         let address = cb.query_word_rlc();
         let address_word = MemoryWordAddress::construct(cb, address.clone());
+        // TODO: we do not need the 32 bytes of the value, only the RLC.
         let value = cb.query_word_rlc();
         let value_left = cb.query_word_rlc();
+        let value_left_prev = cb.query_word_rlc();
         let value_right = cb.query_word_rlc();
+        let value_right_prev = cb.query_word_rlc();
 
         // Check if this is an MLOAD
         let is_mload = IsEqualGadget::construct(cb, opcode.expr(), OpcodeId::MLOAD.expr());
@@ -72,6 +82,33 @@ impl<F: Field> ExecutionGadget<F> for MemoryGadget<F> {
             [from_bytes::expr(&address.cells) + 1.expr() + (is_not_mstore8.clone() * 31.expr())],
         );
 
+        let shift_bits = address_word.shift_bits();
+
+        let mask = MemoryMask::construct(cb, &shift_bits, is_mstore8.expr());
+
+        // Extract word parts. Example with shift=4:
+        // Left  = Aaaa Bbbbbbbbbbbbbbbbbbbbbbbbbbbb
+        // Right = Cccc Dddddddddddddddddddddddddddd
+        let a = mask.get_left(cb, &value_left);
+        let a_prev = mask.get_left(cb, &value_left_prev);
+        let b = mask.get_right(cb, &value_left);
+        let c = mask.get_left(cb, &value_right);
+        let d = mask.get_right(cb, &value_right);
+        let d_prev = mask.get_right(cb, &value_right_prev);
+
+        cb.require_equal("unchanged left bytes: L' & M == L & M", a, a_prev);
+
+        cb.require_equal("unchanged right bytes: R' & !M == R & !M", d, d_prev);
+
+        // Compute powers of the RLC challenge. These are used to shift bytes in equations below.
+        let x = cb.challenges().evm_word();
+        // X**32
+        let x32 = MemoryMask::make_x32(x.clone());
+        // X**(31-shift)
+        let x31_shift = MemoryMask::make_x31_off(x.clone(), &shift_bits);
+        // X**(32-shift)
+        let x32_shift = x * x31_shift.clone();
+
         // Stack operations
         // Pop the address from the stack
         cb.stack_pop(address.expr());
@@ -83,8 +120,12 @@ impl<F: Field> ExecutionGadget<F> for MemoryGadget<F> {
             value.expr(),
         );
 
-        // TODO: replace with value_left = instruction.memory_lookup(RW.Write, addr_left)
         cb.condition(is_mstore8.expr(), |cb| {
+            cb.require_equal(
+                "W[0] * X³¹⁻ˢʰⁱᶠᵗ = B(X)",
+                value.cells[0].expr() * x31_shift.clone(),
+                b.clone(),
+            );
             cb.memory_lookup_word(1.expr(), address_word.addr_left(), value_left.expr(), None);
         });
 
@@ -95,6 +136,12 @@ impl<F: Field> ExecutionGadget<F> for MemoryGadget<F> {
         //    RW.Write if is_store == FQ(1) else RW.Read, addr_right
         // )
         cb.condition(is_not_mstore8, |cb| {
+            cb.require_equal(
+                "W(X) * X³²⁻ˢʰⁱᶠᵗ  =  B(X) * X³² + C(X)",
+                value.expr() * x32_shift,
+                b * x32 + c,
+            );
+
             cb.memory_lookup_word(
                 is_store.clone(),
                 address_word.addr_left(),
@@ -132,10 +179,13 @@ impl<F: Field> ExecutionGadget<F> for MemoryGadget<F> {
             address: address_word,
             value,
             value_left,
+            value_left_prev,
             value_right,
+            value_right_prev,
             memory_expansion,
             is_mload,
             is_mstore8,
+            mask,
         }
     }
 
@@ -167,11 +217,6 @@ impl<F: Field> ExecutionGadget<F> for MemoryGadget<F> {
         self.value
             .assign(region, offset, Some(value.to_le_bytes()))?;
 
-        // TODO: assign value_right
-        let address_u64 = address.as_u64();
-        let shift = address_u64 % 32;
-        let slot = address_u64 - shift;
-        println!("slot {}, shift {}", slot, shift);
         // Check if this is an MLOAD
         self.is_mload.assign(
             region,
@@ -187,6 +232,10 @@ impl<F: Field> ExecutionGadget<F> for MemoryGadget<F> {
             F::from(OpcodeId::MSTORE8.as_u64()),
         )?;
 
+        let shift = address.as_u64() % 32;
+        self.mask
+            .assign(region, offset, shift, is_mstore8 == F::one())?;
+
         // Memory expansion
         self.memory_expansion.assign(
             region,
@@ -203,11 +252,22 @@ impl<F: Field> ExecutionGadget<F> for MemoryGadget<F> {
             block.rws[step.rw_indices[3]].memory_word_value()
         };
 
+        // TODO: rm.
+        println!("address: {:?}", address);
+        println!("value (LE):  {:?}", value.to_le_bytes());
+        println!("value_left:  {:?}", value_left.to_le_bytes());
+        println!("value_right: {:?}", value_right.to_le_bytes());
+
+        // TODO: updated values for MSTORE.
         self.value_left
             .assign(region, offset, Some(value_left.to_le_bytes()))?;
+        self.value_left_prev
+            .assign(region, offset, Some(value_left.to_le_bytes()))?;
 
         self.value_right
             .assign(region, offset, Some(value_right.to_le_bytes()))?;
+        self.value_right_prev
+            .assign(region, offset, Some(value_right.to_le_bytes()))?;
         Ok(())
     }
 }