From d2b549affcd44a9b1d12232b7e4bb62f433f9c2a Mon Sep 17 00:00:00 2001
From: Hamy Ratoanina <hamy.ratoanina@toposware.com>
Date: Fri, 3 Nov 2023 19:52:12 -0400
Subject: [PATCH] Constrain uninitialized memory to 0 (#1318)

---
 evm/src/memory/memory_stark.rs | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/evm/src/memory/memory_stark.rs b/evm/src/memory/memory_stark.rs
index 74aa8787..725ae79d 100644
--- a/evm/src/memory/memory_stark.rs
+++ b/evm/src/memory/memory_stark.rs
@@ -324,10 +324,14 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
         yield_constr.constraint_transition(range_check - computed_range_check);
 
         // Enumerate purportedly-ordered log.
+        // We assume that memory is initialized with 0. This means that if the first operation of a new address
+        // is a read, then its value must be 0.
         for i in 0..8 {
             yield_constr.constraint_transition(
                 next_is_read * address_unchanged * (next_values_limbs[i] - value_limbs[i]),
             );
+            yield_constr
+                .constraint_transition(next_is_read * not_address_unchanged * next_values_limbs[i]);
         }
     }
 
@@ -445,11 +449,17 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
         yield_constr.constraint_transition(builder, range_check_diff);
 
         // Enumerate purportedly-ordered log.
+        // We assume that memory is initialized with 0. This means that if the first operation of a new address
+        // is a read, then its value must be 0.
         for i in 0..8 {
             let value_diff = builder.sub_extension(next_values_limbs[i], value_limbs[i]);
             let zero_if_read = builder.mul_extension(address_unchanged, value_diff);
             let read_constraint = builder.mul_extension(next_is_read, zero_if_read);
             yield_constr.constraint_transition(builder, read_constraint);
+            let first_read_value =
+                builder.mul_extension(next_values_limbs[i], not_address_unchanged);
+            let first_read_constraint = builder.mul_extension(first_read_value, next_is_read);
+            yield_constr.constraint_transition(builder, first_read_constraint);
         }
     }