From 73db6e6fa5de72f0aad2afe65f178245a6350e3c Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 19:31:44 +0800
Subject: [PATCH 01/26] Initial draft

---
 .../vm/instructions/simulations/storage.v     | 160 ++++++++++++++++++
 1 file changed, 160 insertions(+)
 create mode 100644 CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
new file mode 100644
index 0000000..e96fb9d
--- /dev/null
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -0,0 +1,160 @@
+(* 
+from ...state import get_storage, get_storage_original, set_storage
+from .. import Evm
+from ..exceptions import OutOfGasError, WriteInStaticContext
+from ..gas import (
+    GAS_CALL_STIPEND,
+    GAS_COLD_SLOAD,
+    GAS_STORAGE_CLEAR_REFUND,
+    GAS_STORAGE_SET,
+    GAS_STORAGE_UPDATE,
+    GAS_WARM_ACCESS,
+    charge_gas,
+) *)
+
+Require Import CoqOfPython.CoqOfPython.
+Require Import simulations.CoqOfPython.
+Require Import simulations.builtins.
+
+Require ethereum.simulations.base_types.
+Definition U255_CEIL_VALUE := base_types.U255_CEIL_VALUE.
+Module U256 := base_types.U256.
+Definition U256_CEIL_VALUE := base_types.U256_CEIL_VALUE.
+Module Uint := base_types.Uint.
+
+Require ethereum.paris.vm.simulations.__init__.
+Module Evm := __init__.Evm.
+
+Require ethereum.paris.vm.simulations.gas.
+Definition GAS_EXPONENTIATION := gas.GAS_EXPONENTIATION.
+Definition GAS_EXPONENTIATION_PER_BYTE := gas.GAS_EXPONENTIATION_PER_BYTE.
+Definition GAS_LOW := gas.GAS_LOW.
+Definition GAS_MID := gas.GAS_MID.
+Definition GAS_VERY_LOW := gas.GAS_VERY_LOW.
+Definition charge_gas := gas.charge_gas.
+
+Require ethereum.paris.vm.simulations.stack.
+Definition pop := stack.pop.
+Definition push := stack.push.
+
+Import simulations.CoqOfPython.Notations.
+
+(* def sload(evm: Evm) -> None:
+    """
+    Loads to the stack, the value corresponding to a certain key from the
+    storage of the current account.
+
+    Parameters
+    ----------
+    evm :
+        The current EVM frame.
+
+    """
+    # STACK
+    key = pop(evm.stack).to_be_bytes32()
+
+    # GAS
+    if (evm.message.current_target, key) in evm.accessed_storage_keys:
+        charge_gas(evm, GAS_WARM_ACCESS)
+    else:
+        evm.accessed_storage_keys.add((evm.message.current_target, key))
+        charge_gas(evm, GAS_COLD_SLOAD)
+
+    # OPERATION
+    value = get_storage(evm.env.state, evm.message.current_target, key)
+
+    push(evm.stack, value)
+
+    # PROGRAM COUNTER
+    evm.pc += 1 *)
+
+Definition sload (evm : Evm) : unit :=
+    (* STACK *)
+    (* key = pop(evm.stack).to_be_bytes32() *)
+    letS? key := StateError.lift_lens Evm.Lens.stack pop in
+    (* GAS *)
+    (* 
+    if (evm.message.current_target, key) in evm.accessed_storage_keys:
+        charge_gas(evm, GAS_WARM_ACCESS)
+    else:
+        evm.accessed_storage_keys.add((evm.message.current_target, key))
+        charge_gas(evm, GAS_COLD_SLOAD)
+    *)
+    letS? _ := charge_gas GAS_VERY_LOW in
+    (* OPERATION *)
+    (* 
+    value = get_storage(evm.env.state, evm.message.current_target, key)
+    push(evm.stack, value)
+    *)
+    let value := _ in
+    letS? _ := StateError.lift_lens Evm.Lens.stack (
+      push (U256.bit_and x y)) in 
+    (* PROGRAM COUNTER *) 
+    letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
+    (inl tt, Uint.__add__ pc (Uint.Make 1))) in
+    returnS? tt.
+
+
+(* def sstore(evm: Evm) -> None:
+    """
+    Stores a value at a certain key in the current context's storage.
+
+    Parameters
+    ----------
+    evm :
+        The current EVM frame.
+
+    """
+    # STACK
+    key = pop(evm.stack).to_be_bytes32()
+    new_value = pop(evm.stack)
+    if evm.gas_left <= GAS_CALL_STIPEND:
+        raise OutOfGasError
+
+    original_value = get_storage_original(
+        evm.env.state, evm.message.current_target, key
+    )
+    current_value = get_storage(evm.env.state, evm.message.current_target, key)
+
+    gas_cost = Uint(0)
+
+    if (evm.message.current_target, key) not in evm.accessed_storage_keys:
+        evm.accessed_storage_keys.add((evm.message.current_target, key))
+        gas_cost += GAS_COLD_SLOAD
+
+    if original_value == current_value and current_value != new_value:
+        if original_value == 0:
+            gas_cost += GAS_STORAGE_SET
+        else:
+            gas_cost += GAS_STORAGE_UPDATE - GAS_COLD_SLOAD
+    else:
+        gas_cost += GAS_WARM_ACCESS
+
+    # Refund Counter Calculation
+    if current_value != new_value:
+        if original_value != 0 and current_value != 0 and new_value == 0:
+            # Storage is cleared for the first time in the transaction
+            evm.refund_counter += int(GAS_STORAGE_CLEAR_REFUND)
+
+        if original_value != 0 and current_value == 0:
+            # Gas refund issued earlier to be reversed
+            evm.refund_counter -= int(GAS_STORAGE_CLEAR_REFUND)
+
+        if original_value == new_value:
+            # Storage slot being restored to its original value
+            if original_value == 0:
+                # Slot was originally empty and was SET earlier
+                evm.refund_counter += int(GAS_STORAGE_SET - GAS_WARM_ACCESS)
+            else:
+                # Slot was originally non-empty and was UPDATED earlier
+                evm.refund_counter += int(
+                    GAS_STORAGE_UPDATE - GAS_COLD_SLOAD - GAS_WARM_ACCESS
+                )
+
+    charge_gas(evm, gas_cost)
+    if evm.message.is_static:
+        raise WriteInStaticContext
+    set_storage(evm.env.state, evm.message.current_target, key, new_value)
+
+    # PROGRAM COUNTER
+    evm.pc += 1 *)
\ No newline at end of file

From d8a750afb8c995c87d48c39e04aea251a2d54df0 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 21:03:45 +0800
Subject: [PATCH 02/26] More draft updates

---
 .../vm/instructions/simulations/storage.v     | 15 +++++-
 CoqOfPython/ethereum/simulations/base_types.v | 48 ++++++++++++++-----
 2 files changed, 49 insertions(+), 14 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index e96fb9d..2ec6181 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -21,6 +21,7 @@ Definition U255_CEIL_VALUE := base_types.U255_CEIL_VALUE.
 Module U256 := base_types.U256.
 Definition U256_CEIL_VALUE := base_types.U256_CEIL_VALUE.
 Module Uint := base_types.Uint.
+Definition to_be_bytes32 := base_types.Uint.to_be_bytes32.
 
 Require ethereum.paris.vm.simulations.__init__.
 Module Evm := __init__.Evm.
@@ -68,10 +69,12 @@ Import simulations.CoqOfPython.Notations.
     # PROGRAM COUNTER
     evm.pc += 1 *)
 
-Definition sload (evm : Evm) : unit :=
+Definition sload : MS? Evm.t Exception.t unit := 
     (* STACK *)
     (* key = pop(evm.stack).to_be_bytes32() *)
     letS? key := StateError.lift_lens Evm.Lens.stack pop in
+    let key := Uint.Make (U256.to_Z key) in
+    let key := to_be_bytes32 key in
     (* GAS *)
     (* 
     if (evm.message.current_target, key) in evm.accessed_storage_keys:
@@ -80,7 +83,15 @@ Definition sload (evm : Evm) : unit :=
         evm.accessed_storage_keys.add((evm.message.current_target, key))
         charge_gas(evm, GAS_COLD_SLOAD)
     *)
-    letS? _ := charge_gas GAS_VERY_LOW in
+    let evm_message_current_target := _ in
+    (* TODO: evm.accessed_storage_keys.add *)
+
+    letS? _ := 
+    if _
+    then _
+    else _
+    in
+    charge_gas GAS_VERY_LOW in
     (* OPERATION *)
     (* 
     value = get_storage(evm.env.state, evm.message.current_target, key)
diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v
index 478afd6..94b159b 100644
--- a/CoqOfPython/ethereum/simulations/base_types.v
+++ b/CoqOfPython/ethereum/simulations/base_types.v
@@ -28,6 +28,18 @@ Module FixedBytes.
     end.
 End FixedBytes.
 
+Module Bytes32.
+  Inductive t : Set :=
+  | Make (bytes : FixedBytes.t).
+
+  Definition get (bytes : t) : FixedBytes.t :=
+    match bytes with
+    | Make bytes => bytes
+    end.
+
+  Definition LENGTH := 32.
+End Bytes32.
+
 Module Uint.
 (* NOTE: to_bytes would produce a list of byte with *undetermined* length
 *)
@@ -84,6 +96,30 @@ Module Uint.
       if ascii_xor_result =? 0
       then result - Z.shiftl 1 (Z_of_nat (List.length little_ordered))
       else result).
+
+  (* 
+  def to_bytes(n, length=1, byteorder='big', signed=False):
+    if byteorder == 'little':
+        order = range(length)
+    elif byteorder == 'big':
+        order = reversed(range(length))
+    else:
+        raise ValueError("byteorder must be either 'little' or 'big'")
+
+    return bytes((n >> i*8) & 0xff for i in order)
+  *)
+  Fixpoint to_bytes_helper (bytes : Z) : list ascii. Admitted.
+
+  Definition to_bytes (self : t) : Bytes. 
+  (* TODO: Finish this function *)
+  Admitted.
+
+  (* def to_be_bytes32(self) -> "Bytes32" *)
+  Definition to_be_bytes32 (self : t) : Bytes32 :=
+    let bytes := to_bytes self in
+    (* NOTE: For now we only do direct conversion without truncation *)
+    let '(Make bytes) := bytes in
+    Bytes32.Make bytes.
 End Uint.
 
 Module FixedUint.
@@ -322,18 +358,6 @@ Module Bytes20.
     end.
 End Bytes20.
 
-Module Bytes32.
-  Inductive t : Set :=
-  | Make (bytes : FixedBytes.t).
-
-  Definition get (bytes : t) : FixedBytes.t :=
-    match bytes with
-    | Make bytes => bytes
-    end.
-
-  Definition LENGTH := 32.
-End Bytes32.
-
 Module Bytes48.
   Inductive t : Set :=
   | Make (bytes : FixedBytes.t).

From 05a1abd8d67e38fa569d944eb62383b7da4d55be Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 21:04:02 +0800
Subject: [PATCH 03/26] Minor formatting

---
 .../ethereum/paris/vm/instructions/simulations/storage.v        | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 2ec6181..aa820bd 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -168,4 +168,4 @@ Definition sload : MS? Evm.t Exception.t unit :=
     set_storage(evm.env.state, evm.message.current_target, key, new_value)
 
     # PROGRAM COUNTER
-    evm.pc += 1 *)
\ No newline at end of file
+    evm.pc += 1 *)

From 83379da4181e5862a5df33bff2e7d09bddffe9a7 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 22:29:46 +0800
Subject: [PATCH 04/26] More updates

---
 .../paris/vm/instructions/simulations/storage.v  | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index aa820bd..4e185b9 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -25,6 +25,7 @@ Definition to_be_bytes32 := base_types.Uint.to_be_bytes32.
 
 Require ethereum.paris.vm.simulations.__init__.
 Module Evm := __init__.Evm.
+Module Message := __init__.Message.
 
 Require ethereum.paris.vm.simulations.gas.
 Definition GAS_EXPONENTIATION := gas.GAS_EXPONENTIATION.
@@ -83,13 +84,18 @@ Definition sload : MS? Evm.t Exception.t unit :=
         evm.accessed_storage_keys.add((evm.message.current_target, key))
         charge_gas(evm, GAS_COLD_SLOAD)
     *)
-    let evm_message_current_target := _ in
-    (* TODO: evm.accessed_storage_keys.add *)
+    letS? evm := readS? in
+    let '(Evm.Make message rest) := evm in
+    let evm_message_current_target := message.(Message.current_target) in
+    let evm_rest_accessed_storage_keys := rest.(Evm.Rest.accessed_storage_keys) in
+    (* NOTE: accessed_storage_keys.add is actually `pair.add` and now we just simulate directly *)
+    (* TODO: list `is_in` function *)
 
     letS? _ := 
-    if _
-    then _
-    else _
+    if List.has evm_rest_accessed_storage_keys (evm.message.current_target, key)
+    then charge_gas GAS_WARM_ACCESS
+    else (let _ := (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
+      charge_gas GAS_COLD_SLOAD)
     in
     charge_gas GAS_VERY_LOW in
     (* OPERATION *)

From 8dd935b11f5dc0baf63d50838a6c76c24d3c1acb Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 23:44:26 +0800
Subject: [PATCH 05/26] Basic draft for `sload`

---
 .../paris/vm/instructions/simulations/storage.v  | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 4e185b9..053029e 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -28,10 +28,8 @@ Module Evm := __init__.Evm.
 Module Message := __init__.Message.
 
 Require ethereum.paris.vm.simulations.gas.
-Definition GAS_EXPONENTIATION := gas.GAS_EXPONENTIATION.
-Definition GAS_EXPONENTIATION_PER_BYTE := gas.GAS_EXPONENTIATION_PER_BYTE.
-Definition GAS_LOW := gas.GAS_LOW.
-Definition GAS_MID := gas.GAS_MID.
+Definition GAS_COLD_SLOAD := gas.GAS_COLD_SLOAD.
+Definition GAS_WARM_ACCESS := gas.GAS_WARM_ACCESS.
 Definition GAS_VERY_LOW := gas.GAS_VERY_LOW.
 Definition charge_gas := gas.charge_gas.
 
@@ -92,20 +90,20 @@ Definition sload : MS? Evm.t Exception.t unit :=
     (* TODO: list `is_in` function *)
 
     letS? _ := 
-    if List.has evm_rest_accessed_storage_keys (evm.message.current_target, key)
+    if List.has evm_rest_accessed_storage_keys (evm_message_current_target, key)
     then charge_gas GAS_WARM_ACCESS
     else (let _ := (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
       charge_gas GAS_COLD_SLOAD)
     in
-    charge_gas GAS_VERY_LOW in
     (* OPERATION *)
     (* 
     value = get_storage(evm.env.state, evm.message.current_target, key)
     push(evm.stack, value)
     *)
-    let value := _ in
-    letS? _ := StateError.lift_lens Evm.Lens.stack (
-      push (U256.bit_and x y)) in 
+    (* TODO: implement get_storage *)
+    let evm_env_state := rest.(Evm.Rest.env).(Environment.state) in
+    let value := get_storage evm_env_state evm_message_current_target in
+    letS? _ := StateError.lift_lens Evm.Lens.stack (push value) in 
     (* PROGRAM COUNTER *) 
     letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
     (inl tt, Uint.__add__ pc (Uint.Make 1))) in

From ebf0891de4362bb835b90f13e588b8960f3f352f Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 20 Jun 2024 00:30:57 +0800
Subject: [PATCH 06/26] Update draft

---
 .../vm/instructions/simulations/storage.v     | 89 +++++++++++++++++++
 1 file changed, 89 insertions(+)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 053029e..e436968 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -31,6 +31,7 @@ Require ethereum.paris.vm.simulations.gas.
 Definition GAS_COLD_SLOAD := gas.GAS_COLD_SLOAD.
 Definition GAS_WARM_ACCESS := gas.GAS_WARM_ACCESS.
 Definition GAS_VERY_LOW := gas.GAS_VERY_LOW.
+Definition GAS_CALL_STIPEND := gas.GAS_CALL_STIPEND.
 Definition charge_gas := gas.charge_gas.
 
 Require ethereum.paris.vm.simulations.stack.
@@ -173,3 +174,91 @@ Definition sload : MS? Evm.t Exception.t unit :=
 
     # PROGRAM COUNTER
     evm.pc += 1 *)
+Definition sstore : MS? Evm.t Exception.t unit := 
+  (* STACK *)
+  (* 
+  key = pop(evm.stack).to_be_bytes32()
+  new_value = pop(evm.stack)
+  if evm.gas_left <= GAS_CALL_STIPEND:
+      raise OutOfGasError
+
+  original_value = get_storage_original(
+      evm.env.state, evm.message.current_target, key
+  )
+  current_value = get_storage(evm.env.state, evm.message.current_target, key)
+  *)
+  (* key = pop(evm.stack).to_be_bytes32() *)
+  letS? key := StateError.lift_lens Evm.Lens.stack pop in
+  let key := Uint.Make (U256.to_Z key) in
+  let key := to_be_bytes32 key in
+
+  letS? new_value := StateError.lift_lens Evm.Lens.stack pop in
+
+  (* TODO: Implement `raise OutOfGasError` *)
+
+  letS? evm := readS? in
+  let '(Evm.Make message message) := evm in
+  let evm_env_state := rest.(Evm.Rest.env).(Environment.state) in
+  let evm_message_current_target := message.(Message.current_target) in
+
+  (* TODO: Implement get_storage_original *)
+  let original_value := get_storage_original evm_env_state evm_message_current_target key in
+
+  (* TODO: Implement get_storage *)
+  let current_value := get_storage evm_env_state evm_message_current_target key in
+
+  let gas_cost := Uint.Make 0 in
+
+  (* if (evm.message.current_target, key) not in evm.accessed_storage_keys:
+    evm.accessed_storage_keys.add((evm.message.current_target, key))
+    gas_cost += GAS_COLD_SLOAD
+
+  if original_value == current_value and current_value != new_value:
+    if original_value == 0:
+        gas_cost += GAS_STORAGE_SET
+    else:
+        gas_cost += GAS_STORAGE_UPDATE - GAS_COLD_SLOAD
+  else:
+    gas_cost += GAS_WARM_ACCESS *)
+  letS? _ := 
+  if ~(List.has evm_rest_accessed_storage_keys (evm_message_current_target, key))
+  then (
+    (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
+    letS? _ := (* gas_cost += GAS_COLD_SLOAD *)
+  )
+  else tt in
+
+  (* 
+    if original_value == current_value and current_value != new_value:
+        if original_value == 0:
+            gas_cost += GAS_STORAGE_SET
+        else:
+            gas_cost += GAS_STORAGE_UPDATE - GAS_COLD_SLOAD
+    else:
+        gas_cost += GAS_WARM_ACCESS
+  *)
+
+  (* 
+      # Refund Counter Calculation
+    if current_value != new_value:
+        if original_value != 0 and current_value != 0 and new_value == 0:
+            # Storage is cleared for the first time in the transaction
+            evm.refund_counter += int(GAS_STORAGE_CLEAR_REFUND)
+
+        if original_value != 0 and current_value == 0:
+            # Gas refund issued earlier to be reversed
+            evm.refund_counter -= int(GAS_STORAGE_CLEAR_REFUND)
+
+        if original_value == new_value:
+            # Storage slot being restored to its original value
+            if original_value == 0:
+                # Slot was originally empty and was SET earlier
+                evm.refund_counter += int(GAS_STORAGE_SET - GAS_WARM_ACCESS)
+            else:
+                # Slot was originally non-empty and was UPDATED earlier
+                evm.refund_counter += int(
+                    GAS_STORAGE_UPDATE - GAS_COLD_SLOAD - GAS_WARM_ACCESS
+                )
+  *)
+
+  returnS? tt.
\ No newline at end of file

From e5dda558651d779820f5f35c248e824ac5f1413a Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 20 Jun 2024 00:41:11 +0800
Subject: [PATCH 07/26] Complete a rough draft to the end

---
 .../vm/instructions/simulations/storage.v     | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index e436968..a204234 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -88,10 +88,9 @@ Definition sload : MS? Evm.t Exception.t unit :=
     let evm_message_current_target := message.(Message.current_target) in
     let evm_rest_accessed_storage_keys := rest.(Evm.Rest.accessed_storage_keys) in
     (* NOTE: accessed_storage_keys.add is actually `pair.add` and now we just simulate directly *)
-    (* TODO: list `is_in` function *)
 
     letS? _ := 
-    if List.has evm_rest_accessed_storage_keys (evm_message_current_target, key)
+    if List.In evm_rest_accessed_storage_keys (evm_message_current_target, key)
     then charge_gas GAS_WARM_ACCESS
     else (let _ := (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
       charge_gas GAS_COLD_SLOAD)
@@ -221,7 +220,7 @@ Definition sstore : MS? Evm.t Exception.t unit :=
   else:
     gas_cost += GAS_WARM_ACCESS *)
   letS? _ := 
-  if ~(List.has evm_rest_accessed_storage_keys (evm_message_current_target, key))
+  if ~(List.In evm_rest_accessed_storage_keys (evm_message_current_target, key))
   then (
     (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
     letS? _ := (* gas_cost += GAS_COLD_SLOAD *)
@@ -261,4 +260,16 @@ Definition sstore : MS? Evm.t Exception.t unit :=
                 )
   *)
 
-  returnS? tt.
\ No newline at end of file
+  (* 
+      charge_gas(evm, gas_cost)
+
+  *)
+  (* PROGRAM *)
+  (*
+    if evm.message.is_static:
+        raise WriteInStaticContext
+    set_storage(evm.env.state, evm.message.current_target, key, new_value)
+  *)
+  letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
+  (inl tt, Uint.__add__ pc (Uint.Make 1))) in
+  returnS? tt.

From 9c9c900aede501d43fc60291f49c9ddc2e1fe1da Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 20 Jun 2024 00:49:43 +0800
Subject: [PATCH 08/26] Minor comment update

---
 .../ethereum/paris/vm/instructions/simulations/block.v        | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v
index 0d38488..d806c93 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v
@@ -230,7 +230,7 @@ Definition timestamp : MS? Evm.t Exception.t unit :=
 Definition number : MS? Evm.t Exception.t unit := 
   (* GAS *)
   letS? _ := charge_gas GAS_BASE in
-  (* Get evm.env.time *)
+  (* Get evm.env.number *)
   letS? evm := readS? in
   let '(Evm.Make _ rest) := evm in
   let evm_env_number := rest.(Evm.Rest.env).(Environment.number) in
@@ -370,7 +370,7 @@ def chain_id(evm: Evm) -> None:
 Definition chain_id : MS? Evm.t Exception.t unit := 
   (* GAS *)
   letS? _ := charge_gas GAS_BASE in
-  (* Get evm.env.gas_limit *)
+  (* Get evm.env.chain_id *)
   letS? evm := readS? in
   let '(Evm.Make _ rest) := evm in
   (* Convert from U64 to U256 *)

From 8967d614f2bdc55952a4c37b53a905e6e5d5e07c Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 20 Jun 2024 12:28:54 +0800
Subject: [PATCH 09/26] Draft: add `raiseS?` and `to_bytes` draft

---
 .../vm/instructions/simulations/storage.v     | 36 ++++++------
 CoqOfPython/ethereum/simulations/base_types.v | 57 ++++++++++---------
 CoqOfPython/simulations/CoqOfPython.v         |  2 +
 3 files changed, 48 insertions(+), 47 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index a204234..227aa7e 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -1,17 +1,3 @@
-(* 
-from ...state import get_storage, get_storage_original, set_storage
-from .. import Evm
-from ..exceptions import OutOfGasError, WriteInStaticContext
-from ..gas import (
-    GAS_CALL_STIPEND,
-    GAS_COLD_SLOAD,
-    GAS_STORAGE_CLEAR_REFUND,
-    GAS_STORAGE_SET,
-    GAS_STORAGE_UPDATE,
-    GAS_WARM_ACCESS,
-    charge_gas,
-) *)
-
 Require Import CoqOfPython.CoqOfPython.
 Require Import simulations.CoqOfPython.
 Require Import simulations.builtins.
@@ -30,8 +16,10 @@ Module Message := __init__.Message.
 Require ethereum.paris.vm.simulations.gas.
 Definition GAS_COLD_SLOAD := gas.GAS_COLD_SLOAD.
 Definition GAS_WARM_ACCESS := gas.GAS_WARM_ACCESS.
-Definition GAS_VERY_LOW := gas.GAS_VERY_LOW.
 Definition GAS_CALL_STIPEND := gas.GAS_CALL_STIPEND.
+Definition GAS_STORAGE_UPDATE := gas.GAS_STORAGE_UPDATE.
+Definition GAS_STORAGE_SET := gas.GAS_STORAGE_SET.
+Definition GAS_STORAGE_CLEAR_REFUND := gas.GAS_STORAGE_CLEAR_REFUND.
 Definition charge_gas := gas.charge_gas.
 
 Require ethereum.paris.vm.simulations.stack.
@@ -40,6 +28,10 @@ Definition push := stack.push.
 
 Import simulations.CoqOfPython.Notations.
 
+(* TODO: Delete this test code *)
+Definition error_test MS? Evm.t Exception.t unit := 
+  raiseS? (Exception.t.Raise (Value.Make "exceptions" "InvalidJumpDestError" (Pointer.Imm Object.empty)))
+
 (* def sload(evm: Evm) -> None:
     """
     Loads to the stack, the value corresponding to a certain key from the
@@ -87,12 +79,12 @@ Definition sload : MS? Evm.t Exception.t unit :=
     let '(Evm.Make message rest) := evm in
     let evm_message_current_target := message.(Message.current_target) in
     let evm_rest_accessed_storage_keys := rest.(Evm.Rest.accessed_storage_keys) in
-    (* NOTE: accessed_storage_keys.add is actually `pair.add` and now we just simulate directly *)
+    (* NOTE: accessed_storage_keys.add is actually `pair.add` and we simulate it directly *)
 
     letS? _ := 
     if List.In evm_rest_accessed_storage_keys (evm_message_current_target, key)
     then charge_gas GAS_WARM_ACCESS
-    else (let _ := (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
+    else (let _ := (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *) in
       charge_gas GAS_COLD_SLOAD)
     in
     (* OPERATION *)
@@ -109,7 +101,6 @@ Definition sload : MS? Evm.t Exception.t unit :=
     (inl tt, Uint.__add__ pc (Uint.Make 1))) in
     returnS? tt.
 
-
 (* def sstore(evm: Evm) -> None:
     """
     Stores a value at a certain key in the current context's storage.
@@ -193,8 +184,11 @@ Definition sstore : MS? Evm.t Exception.t unit :=
 
   letS? new_value := StateError.lift_lens Evm.Lens.stack pop in
 
-  (* TODO: Implement `raise OutOfGasError` *)
+  if _ 
+  then raiseS? OutOfGasError
+  else _ (* the full content of the rest of the code *)
 
+  (* TODO: connect with the :? above *)
   letS? evm := readS? in
   let '(Evm.Make message message) := evm in
   let evm_env_state := rest.(Evm.Rest.env).(Environment.state) in
@@ -236,6 +230,10 @@ Definition sstore : MS? Evm.t Exception.t unit :=
     else:
         gas_cost += GAS_WARM_ACCESS
   *)
+  letS? _ :=
+  if _ 
+  then _ 
+  else 
 
   (* 
       # Refund Counter Calculation
diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v
index 94b159b..4c1ad0f 100644
--- a/CoqOfPython/ethereum/simulations/base_types.v
+++ b/CoqOfPython/ethereum/simulations/base_types.v
@@ -10,6 +10,8 @@ Definition U255_CEIL_VALUE : Z := 2^255.
 
 Definition U256_CEIL_VALUE : Z := 2^256.
 
+(* TODO: Potentially, design all the conversions between the integer fully and clearly based on Z *)
+
 (* NOTE: A byte should consist of 2 hex digits or 4 binary digits
   https://docs.python.org/3/library/stdtypes.html#bytes *)
 Module FixedBytes.
@@ -28,6 +30,16 @@ Module FixedBytes.
     end.
 End FixedBytes.
 
+Module Bytes.
+  Inductive t : Set :=
+  | Make (bytes : list ascii).
+
+  Definition get (bytes : t) : list ascii :=
+    match bytes with
+    | Make bytes => bytes
+    end.
+End Bytes.
+
 Module Bytes32.
   Inductive t : Set :=
   | Make (bytes : FixedBytes.t).
@@ -41,8 +53,6 @@ Module Bytes32.
 End Bytes32.
 
 Module Uint.
-(* NOTE: to_bytes would produce a list of byte with *undetermined* length
-*)
   Inductive t : Set :=
   | Make (value : Z).
 
@@ -54,9 +64,11 @@ Module Uint.
   Definition __add__ (self right_ : t) : t :=
     Make (get self + get right_).
 
-  (* NOTE: Currently for convenience we only define "from fixedbytes to uint" 
-           An ideal translation should go from fixedbytes -> bytes -> uint *)
-  (* TODO: Distinguish between `from_be_bytes` and `from_le_bytes` *)
+  (* NOTE: 
+     - For convenience we only define "from fixedbytes to uint" 
+       An ideal translation should go from fixedbytes -> bytes -> uint 
+     - Currently we don't support between different endians
+     - Future plan: Distinguish between `from_be_bytes` and `from_le_bytes`*)
   (* 
     def from_bytes(bytes, byteorder='big', signed=False):
       if byteorder == 'little':
@@ -72,13 +84,6 @@ Module Uint.
 
       return n
   *)
-  (* 
-    NOTE:
-    - Currently we don't support between different endians
-    - From definition of related functions(?), it seems that `little_ordered` 
-      doesnt have a fixed length or even length of multiples of 2
-      (Question: Does Python check the length of byte array?)
-  *)
   Fixpoint from_bytes_helper (bytes : list ascii) (store : Z) : Z :=
     match bytes with
     | [] => 0
@@ -88,7 +93,7 @@ Module Uint.
   Definition from_bytes (bytes : FixedBytes.t) : t :=
     let '(FixedBytes.Make little_ordered) := bytes in
     let result := from_bytes_helper little_ordered 0 in
-    (* NOTE: last_byte provides a default value 0 *)
+    (* NOTE: Coq's last_byte provides a default value 0 *)
     let z0 := List.last little_ordered (ascii_of_N 0) in
     let z1 := Z.of_N (N_of_ascii z0) in
     let ascii_xor_result := Z.land z1 0x80 in
@@ -108,14 +113,20 @@ Module Uint.
 
     return bytes((n >> i*8) & 0xff for i in order)
   *)
-  Fixpoint to_bytes_helper (bytes : Z) : list ascii. Admitted.
+  Fixpoint to_bytes_helper (uint : Z) (order : Z) (store : list ascii): list ascii :=
+    match order with
+    | 0 => store
+    | _ => 
+      let byte := Z.land (Z.shiftr uint (order * 8)) 0xff in (* TODO: test & fix this *)
+      to_bytes_helper uint (order - 1) (byte :: store)
+    end.
 
-  Definition to_bytes (self : t) : Bytes. 
-  (* TODO: Finish this function *)
-  Admitted.
+  Definition to_bytes (self : t) : Bytes.t :=
+    let uint := get self in
+    to_bytes_helper uint uint [].
 
   (* def to_be_bytes32(self) -> "Bytes32" *)
-  Definition to_be_bytes32 (self : t) : Bytes32 :=
+  Definition to_be_bytes32 (self : t) : Bytes32.t :=
     let bytes := to_bytes self in
     (* NOTE: For now we only do direct conversion without truncation *)
     let '(Make bytes) := bytes in
@@ -387,13 +398,3 @@ Module Bytes256.
     | Make bytes => bytes
     end.
 End Bytes256.
-
-Module Bytes.
-  Inductive t : Set :=
-  | Make (bytes : list ascii).
-
-  Definition get (bytes : t) : list ascii :=
-    match bytes with
-    | Make bytes => bytes
-    end.
-End Bytes.
diff --git a/CoqOfPython/simulations/CoqOfPython.v b/CoqOfPython/simulations/CoqOfPython.v
index 004649c..d2a79a1 100644
--- a/CoqOfPython/simulations/CoqOfPython.v
+++ b/CoqOfPython/simulations/CoqOfPython.v
@@ -91,4 +91,6 @@ Module Notations.
   Notation "writeS?" := StateError.write.
 
   Notation "return?toS?" := StateError.lift_from_error.
+
+  Notation "raiseS?" := StateError.raise.
 End Notations.
\ No newline at end of file

From 8dd85f2a5b9d4403ff3f5687aafdabd222802e33 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 20 Jun 2024 12:34:17 +0800
Subject: [PATCH 10/26] Fix notes & redundant code after merge update

---
 CoqOfPython/ethereum/simulations/base_types.v | 25 ++++++-------------
 1 file changed, 7 insertions(+), 18 deletions(-)

diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v
index e0cc5d3..f1e9d1b 100644
--- a/CoqOfPython/ethereum/simulations/base_types.v
+++ b/CoqOfPython/ethereum/simulations/base_types.v
@@ -13,7 +13,12 @@ Definition U256_CEIL_VALUE : Z := 2^256.
 (* NOTE: Python built-in type. We put here for convenience. *)
 Definition bytearray := list ascii.
 
-(* TODO: Potentially, design all the conversions between the integer fully and clearly based on Z *)
+(* TODO: Implement consistent conversion functions between all the types. For example:
+- to_Uint: Apart from U_ series of modules, we might also need its def for FixedUint
+- bytearray, FixedBytes & Bytes: also define a consistent covert functions between them
+- Build all conversion functions clearly based on Z
+- Correctly truncate the values based on the max value being defined
+*)
 
 (* NOTE: A byte should consist of 2 hex digits or 4 binary digits
   https://docs.python.org/3/library/stdtypes.html#bytes *)
@@ -33,21 +38,6 @@ Module FixedBytes.
     end.
 End FixedBytes.
 
-(* TODO: Make some consistent definitions in the following modules:
-- to_Uint: Apart from U_ series of modules, we might also need its def for FixedUint
-- bytearray, FixedBytes & Bytes: also define a consistent covert functions between them
-*)
-
-Module Bytes.
-  Inductive t : Set :=
-  | Make (bytes : list ascii).
-
-  Definition get (bytes : t) : list ascii :=
-    match bytes with
-    | Make bytes => bytes
-    end.
-End Bytes.
-
 Module Bytes32.
   Inductive t : Set :=
   | Make (bytes : FixedBytes.t).
@@ -73,8 +63,6 @@ Module Uint.
     Make (get self + get right_).
 
   (* NOTE: 
-     - For convenience we only define "from fixedbytes to uint" 
-       An ideal translation should go from fixedbytes -> bytes -> uint 
      - Currently we don't support between different endians
      - Future plan: Distinguish between `from_be_bytes` and `from_le_bytes`*)
   (* 
@@ -121,6 +109,7 @@ Module Uint.
 
     return bytes((n >> i*8) & 0xff for i in order)
   *)
+  (* NOTE: there might be order issues *)
   Fixpoint to_bytes_helper (uint : Z) (order : Z) (store : list ascii): list ascii :=
     match order with
     | 0 => store

From b1580fce500ca839be40ce7ad78a7f7d9dc21dea Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 20 Jun 2024 14:52:05 +0800
Subject: [PATCH 11/26] Minor updates

---
 .../paris/vm/instructions/simulations/storage.v  | 16 ++++++++++++++--
 CoqOfPython/ethereum/paris/vm/simulations/gas.v  |  2 --
 CoqOfPython/ethereum/simulations/base_types.v    |  2 +-
 3 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 227aa7e..0a4a39e 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -28,6 +28,11 @@ Definition push := stack.push.
 
 Import simulations.CoqOfPython.Notations.
 
+(* TODO: (progress) things to test on this draft:
+- correctly implemented `raiseS?`
+- test how to update a value for evm
+- investigate `get_storage` functions
+*)
 (* TODO: Delete this test code *)
 Definition error_test MS? Evm.t Exception.t unit := 
   raiseS? (Exception.t.Raise (Value.Make "exceptions" "InvalidJumpDestError" (Pointer.Imm Object.empty)))
@@ -81,10 +86,17 @@ Definition sload : MS? Evm.t Exception.t unit :=
     let evm_rest_accessed_storage_keys := rest.(Evm.Rest.accessed_storage_keys) in
     (* NOTE: accessed_storage_keys.add is actually `pair.add` and we simulate it directly *)
 
+    (* Example code for value update:
+      | Address.evm => fun v => Some (h <| evm := v |>)
+      | Address.stack => fun v => Some (h <| stack := v |>)
+    *)
+
     letS? _ := 
-    if List.In evm_rest_accessed_storage_keys (evm_message_current_target, key)
+    if List.In evm_rest_accessed_storage_keys (evm_message_current_target, key) (* TODO: Identify the order of parms for `In` *)
     then charge_gas GAS_WARM_ACCESS
-    else (let _ := (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *) in
+    else (letS? _ := 
+      (fun v => evm_rest_accessed_storage_keys <| (evm.message.current_target, key) |>) (* ?????? *)
+    (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *) in
       charge_gas GAS_COLD_SLOAD)
     in
     (* OPERATION *)
diff --git a/CoqOfPython/ethereum/paris/vm/simulations/gas.v b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
index da4a375..a04d93c 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/gas.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
@@ -54,8 +54,6 @@ Definition GAS_WARM_ACCESS := Uint.Make 100.
 
 Definition bytearray := base_types.bytearray.
 
-(* TODO: Since there might be inconsistency issue, we might
-Definition charge_gas (amount : Uint.t) : unit. *)
 Parameter charge_gas : forall (amount : Uint.t), MS? Evm.t Exception.t unit.
 
 (* 
diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v
index f1e9d1b..389edc0 100644
--- a/CoqOfPython/ethereum/simulations/base_types.v
+++ b/CoqOfPython/ethereum/simulations/base_types.v
@@ -115,7 +115,7 @@ Module Uint.
     | 0 => store
     | _ => 
       let byte := Z.land (Z.shiftr uint (order * 8)) 0xff in (* TODO: test & fix this *)
-      to_bytes_helper uint (order - 1) (byte :: store)
+      to_bytes_helper uint (order - 1) (byte :: store) (* TODO: convert byte from Z to ascii *)
     end.
 
   Definition to_bytes (self : t) : Bytes.t :=

From fc7ad8f3b6ed2e69f9e297f5de5455aef41a423e Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 20 Jun 2024 14:58:49 +0800
Subject: [PATCH 12/26] Fix `List.In` parm

---
 .../paris/vm/instructions/simulations/storage.v   | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 0a4a39e..9bd7319 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -28,11 +28,16 @@ Definition push := stack.push.
 
 Import simulations.CoqOfPython.Notations.
 
+(* def get_storage(state: State, address: Address, key: Bytes) -> U256: *)
+Definition get_storage (state : State.t) (address : Address.t) (key : Bytes.t) : U256.t. Admitted.
+(* def get_storage_original(state: State, address: Address, key: Bytes) -> U256: *)
+Definition get_storage_original (state : State.t) (address : Address.t) (key : Bytes.t) : U256.t. Admitted.
+
 (* TODO: (progress) things to test on this draft:
 - correctly implemented `raiseS?`
 - test how to update a value for evm
-- investigate `get_storage` functions
 *)
+
 (* TODO: Delete this test code *)
 Definition error_test MS? Evm.t Exception.t unit := 
   raiseS? (Exception.t.Raise (Value.Make "exceptions" "InvalidJumpDestError" (Pointer.Imm Object.empty)))
@@ -92,7 +97,7 @@ Definition sload : MS? Evm.t Exception.t unit :=
     *)
 
     letS? _ := 
-    if List.In evm_rest_accessed_storage_keys (evm_message_current_target, key) (* TODO: Identify the order of parms for `In` *)
+    if List.In (evm_message_current_target, key) evm_rest_accessed_storage_keys
     then charge_gas GAS_WARM_ACCESS
     else (letS? _ := 
       (fun v => evm_rest_accessed_storage_keys <| (evm.message.current_target, key) |>) (* ?????? *)
@@ -104,7 +109,6 @@ Definition sload : MS? Evm.t Exception.t unit :=
     value = get_storage(evm.env.state, evm.message.current_target, key)
     push(evm.stack, value)
     *)
-    (* TODO: implement get_storage *)
     let evm_env_state := rest.(Evm.Rest.env).(Environment.state) in
     let value := get_storage evm_env_state evm_message_current_target in
     letS? _ := StateError.lift_lens Evm.Lens.stack (push value) in 
@@ -206,10 +210,7 @@ Definition sstore : MS? Evm.t Exception.t unit :=
   let evm_env_state := rest.(Evm.Rest.env).(Environment.state) in
   let evm_message_current_target := message.(Message.current_target) in
 
-  (* TODO: Implement get_storage_original *)
   let original_value := get_storage_original evm_env_state evm_message_current_target key in
-
-  (* TODO: Implement get_storage *)
   let current_value := get_storage evm_env_state evm_message_current_target key in
 
   let gas_cost := Uint.Make 0 in
@@ -226,7 +227,7 @@ Definition sstore : MS? Evm.t Exception.t unit :=
   else:
     gas_cost += GAS_WARM_ACCESS *)
   letS? _ := 
-  if ~(List.In evm_rest_accessed_storage_keys (evm_message_current_target, key))
+  if ~(List.In (evm_message_current_target, key) evm_rest_accessed_storage_keys)
   then (
     (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
     letS? _ := (* gas_cost += GAS_COLD_SLOAD *)

From 3bcfd573c103a5d724c2842ca42660a2374bc35b Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 21 Jun 2024 19:34:21 +0800
Subject: [PATCH 13/26] Update draft on `to_bytes`

---
 CoqOfPython/ethereum/simulations/base_types.v | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v
index 389edc0..bf5ef0d 100644
--- a/CoqOfPython/ethereum/simulations/base_types.v
+++ b/CoqOfPython/ethereum/simulations/base_types.v
@@ -110,17 +110,16 @@ Module Uint.
     return bytes((n >> i*8) & 0xff for i in order)
   *)
   (* NOTE: there might be order issues *)
-  Fixpoint to_bytes_helper (uint : Z) (order : Z) (store : list ascii): list ascii :=
+  Fixpoint to_bytes_helper (uint : Z) (order : nat) (store : list ascii): list ascii :=
     match order with
-    | 0 => store
-    | _ => 
-      let byte := Z.land (Z.shiftr uint (order * 8)) 0xff in (* TODO: test & fix this *)
-      to_bytes_helper uint (order - 1) (byte :: store) (* TODO: convert byte from Z to ascii *)
+    | O => store
+    | S n => let byte := ascii_of_N (N_of_Z (Z.land (Z.shiftr uint ((Z.of_nat order) * 8)) 0xff)) in 
+      to_bytes_helper uint (n) (byte :: store) 
     end.
 
   Definition to_bytes (self : t) : Bytes.t :=
     let uint := get self in
-    to_bytes_helper uint uint [].
+    to_bytes_helper uint (Z.of_nat uint) [].
 
   (* def to_be_bytes32(self) -> "Bytes32" *)
   Definition to_be_bytes32 (self : t) : Bytes32.t :=

From ef2d1b3dbd985c76803ee7655211a172fa9a91dd Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 21 Jun 2024 19:36:49 +0800
Subject: [PATCH 14/26] Finish defining `to_bytes` functions

---
 CoqOfPython/ethereum/simulations/base_types.v | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v
index bf5ef0d..c0b473e 100644
--- a/CoqOfPython/ethereum/simulations/base_types.v
+++ b/CoqOfPython/ethereum/simulations/base_types.v
@@ -20,6 +20,16 @@ Definition bytearray := list ascii.
 - Correctly truncate the values based on the max value being defined
 *)
 
+Module Bytes.
+  Inductive t : Set :=
+  | Make (bytes : list ascii).
+
+  Definition get (bytes : t) : list ascii :=
+    match bytes with
+    | Make bytes => bytes
+    end.
+End Bytes.
+
 (* NOTE: A byte should consist of 2 hex digits or 4 binary digits
   https://docs.python.org/3/library/stdtypes.html#bytes *)
 Module FixedBytes.
@@ -119,14 +129,14 @@ Module Uint.
 
   Definition to_bytes (self : t) : Bytes.t :=
     let uint := get self in
-    to_bytes_helper uint (Z.of_nat uint) [].
+    Bytes.Make (to_bytes_helper uint (Z.to_nat uint) []).
 
   (* def to_be_bytes32(self) -> "Bytes32" *)
   Definition to_be_bytes32 (self : t) : Bytes32.t :=
     let bytes := to_bytes self in
     (* NOTE: For now we only do direct conversion without truncation *)
-    let '(Make bytes) := bytes in
-    Bytes32.Make bytes.
+    let '(Bytes.Make bytes) := bytes in
+    Bytes32.Make (FixedBytes.Make bytes).
 End Uint.
 
 Module FixedUint.

From 9472d55f70f307665a52c461f4864bf8f8ed3d99 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 21 Jun 2024 20:29:31 +0800
Subject: [PATCH 15/26] Finish testing error raising code

---
 .../paris/vm/instructions/simulations/storage.v     | 13 +++++++------
 CoqOfPython/simulations/CoqOfPython.v               |  2 ++
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 9bd7319..7ea3a2e 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -8,10 +8,13 @@ Module U256 := base_types.U256.
 Definition U256_CEIL_VALUE := base_types.U256_CEIL_VALUE.
 Module Uint := base_types.Uint.
 Definition to_be_bytes32 := base_types.Uint.to_be_bytes32.
+Module Bytes := base_types.Bytes.
 
 Require ethereum.paris.vm.simulations.__init__.
 Module Evm := __init__.Evm.
 Module Message := __init__.Message.
+Module State := __init__.State.
+Module Address := __init__.Address.
 
 Require ethereum.paris.vm.simulations.gas.
 Definition GAS_COLD_SLOAD := gas.GAS_COLD_SLOAD.
@@ -34,14 +37,10 @@ Definition get_storage (state : State.t) (address : Address.t) (key : Bytes.t) :
 Definition get_storage_original (state : State.t) (address : Address.t) (key : Bytes.t) : U256.t. Admitted.
 
 (* TODO: (progress) things to test on this draft:
-- correctly implemented `raiseS?`
 - test how to update a value for evm
+- rest of the draft
 *)
 
-(* TODO: Delete this test code *)
-Definition error_test MS? Evm.t Exception.t unit := 
-  raiseS? (Exception.t.Raise (Value.Make "exceptions" "InvalidJumpDestError" (Pointer.Imm Object.empty)))
-
 (* def sload(evm: Evm) -> None:
     """
     Loads to the stack, the value corresponding to a certain key from the
@@ -201,7 +200,9 @@ Definition sstore : MS? Evm.t Exception.t unit :=
   letS? new_value := StateError.lift_lens Evm.Lens.stack pop in
 
   if _ 
-  then raiseS? OutOfGasError
+  then 
+  (* TODO: Fill in the correct error type *)
+    StateError.lift_from_error (Error.raise (Exception.ArithmeticError ArithmeticError.OverflowError))
   else _ (* the full content of the rest of the code *)
 
   (* TODO: connect with the :? above *)
diff --git a/CoqOfPython/simulations/CoqOfPython.v b/CoqOfPython/simulations/CoqOfPython.v
index d2a79a1..4b18b30 100644
--- a/CoqOfPython/simulations/CoqOfPython.v
+++ b/CoqOfPython/simulations/CoqOfPython.v
@@ -66,6 +66,8 @@ Module Notations.
 
   Notation "return?" := Error.return_.
 
+  Notation "raise?" := Error.raise.
+
   Notation "'let?' x ':=' X 'in' Y" :=
     (Error.bind X (fun x => Y))
     (at level 200, x name, X at level 100, Y at level 200).

From 7bbc8b2fed704b9296be14574f1f62dbe7ce594e Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 24 Jun 2024 15:00:04 +0800
Subject: [PATCH 16/26] Minor progress on `evm`

---
 .../vm/instructions/simulations/storage.v     | 28 ++++++++++++++-----
 1 file changed, 21 insertions(+), 7 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 7ea3a2e..83f11ef 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -15,6 +15,7 @@ Module Evm := __init__.Evm.
 Module Message := __init__.Message.
 Module State := __init__.State.
 Module Address := __init__.Address.
+Module Environment := __init__.Environment.
 
 Require ethereum.paris.vm.simulations.gas.
 Definition GAS_COLD_SLOAD := gas.GAS_COLD_SLOAD.
@@ -36,8 +37,9 @@ Definition get_storage (state : State.t) (address : Address.t) (key : Bytes.t) :
 (* def get_storage_original(state: State, address: Address, key: Bytes) -> U256: *)
 Definition get_storage_original (state : State.t) (address : Address.t) (key : Bytes.t) : U256.t. Admitted.
 
-(* TODO: (progress) things to test on this draft:
+(* TODO: (progress) things to do on this draft:
 - test how to update a value for evm
+- replace `List.In` with `List.find` + `is_none`(?)
 - rest of the draft
 *)
 
@@ -88,19 +90,31 @@ Definition sload : MS? Evm.t Exception.t unit :=
     let '(Evm.Make message rest) := evm in
     let evm_message_current_target := message.(Message.current_target) in
     let evm_rest_accessed_storage_keys := rest.(Evm.Rest.accessed_storage_keys) in
-    (* NOTE: accessed_storage_keys.add is actually `pair.add` and we simulate it directly *)
-
     (* Example code for value update:
       | Address.evm => fun v => Some (h <| evm := v |>)
       | Address.stack => fun v => Some (h <| stack := v |>)
-    *)
 
+      
+    Definition pc : Lens.t t Uint.t := {|
+      Lens.read '(Make _ rest) := rest.(Rest.pc);
+      Lens.write '(Make message rest) pc := Make message rest<|Rest.pc := pc|>;
+    |}.
+    *)
+    (* NOTE: accessed_storage_keys.add is actually `pair.add` and we simulate it directly *)
     letS? _ := 
     if List.In (evm_message_current_target, key) evm_rest_accessed_storage_keys
     then charge_gas GAS_WARM_ACCESS
-    else (letS? _ := 
-      (fun v => evm_rest_accessed_storage_keys <| (evm.message.current_target, key) |>) (* ?????? *)
-    (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *) in
+    else (letS? _ := unit
+    (* TODO: Correctly write a state-update code *)
+    (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
+    (* (fun v => evm_rest_accessed_storage_keys <| (evm.message.current_target, key) |>)  *)
+    (* 
+    TODO:
+    1. correctly construct the updated value
+    2. stuff the value into the evm correctly
+    3. update the evm using writeS?
+    *)
+    in
       charge_gas GAS_COLD_SLOAD)
     in
     (* OPERATION *)

From 734f6969a7e4e3428feec05aa876436d5ca0f838 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 24 Jun 2024 15:27:10 +0800
Subject: [PATCH 17/26] Finish testing a correct state update code

---
 .../vm/instructions/simulations/storage.v     | 39 +++++--------------
 1 file changed, 10 insertions(+), 29 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 83f11ef..289d234 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -38,7 +38,6 @@ Definition get_storage (state : State.t) (address : Address.t) (key : Bytes.t) :
 Definition get_storage_original (state : State.t) (address : Address.t) (key : Bytes.t) : U256.t. Admitted.
 
 (* TODO: (progress) things to do on this draft:
-- test how to update a value for evm
 - replace `List.In` with `List.find` + `is_none`(?)
 - rest of the draft
 *)
@@ -90,40 +89,22 @@ Definition sload : MS? Evm.t Exception.t unit :=
     let '(Evm.Make message rest) := evm in
     let evm_message_current_target := message.(Message.current_target) in
     let evm_rest_accessed_storage_keys := rest.(Evm.Rest.accessed_storage_keys) in
-    (* Example code for value update:
-      | Address.evm => fun v => Some (h <| evm := v |>)
-      | Address.stack => fun v => Some (h <| stack := v |>)
-
-      
-    Definition pc : Lens.t t Uint.t := {|
-      Lens.read '(Make _ rest) := rest.(Rest.pc);
-      Lens.write '(Make message rest) pc := Make message rest<|Rest.pc := pc|>;
-    |}.
-    *)
-    (* NOTE: accessed_storage_keys.add is actually `pair.add` and we simulate it directly *)
     letS? _ := 
-    if List.In (evm_message_current_target, key) evm_rest_accessed_storage_keys
+    if List.In (evm_message_current_target, key) evm_rest_accessed_storage_keys (* TODO: Fix the List.In *)
     then charge_gas GAS_WARM_ACCESS
-    else (letS? _ := unit
-    (* TODO: Correctly write a state-update code *)
-    (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
-    (* (fun v => evm_rest_accessed_storage_keys <| (evm.message.current_target, key) |>)  *)
-    (* 
-    TODO:
-    1. correctly construct the updated value
-    2. stuff the value into the evm correctly
-    3. update the evm using writeS?
-    *)
-    in
+    else (
+      (* TODO: check if the added element is added in the correct place *)
+      (* NOTE: accessed_storage_keys.add is actually `pair.add` and we simulate it directly *)
+      let evm_rest_accessed_storage_keys := 
+        (evm_message_current_target, key) :: evm_rest_accessed_storage_keys in
+      let rest := rest <| Evm.Rest.accessed_storage_keys := evm_rest_accessed_storage_keys |> in
+      let evm := Evm.Make message rest in
+      letS? _ := writeS? evm in
       charge_gas GAS_COLD_SLOAD)
     in
     (* OPERATION *)
-    (* 
-    value = get_storage(evm.env.state, evm.message.current_target, key)
-    push(evm.stack, value)
-    *)
     let evm_env_state := rest.(Evm.Rest.env).(Environment.state) in
-    let value := get_storage evm_env_state evm_message_current_target in
+    let value := get_storage evm_env_state evm_message_current_target key in
     letS? _ := StateError.lift_lens Evm.Lens.stack (push value) in 
     (* PROGRAM COUNTER *) 
     letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>

From b26e5d736c927c5b29dcf1f2c44803fb64c3bb67 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 24 Jun 2024 15:28:10 +0800
Subject: [PATCH 18/26] minor comment delections

---
 .../ethereum/paris/vm/instructions/simulations/storage.v  | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 289d234..bab8f9e 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -73,18 +73,10 @@ Definition get_storage_original (state : State.t) (address : Address.t) (key : B
 
 Definition sload : MS? Evm.t Exception.t unit := 
     (* STACK *)
-    (* key = pop(evm.stack).to_be_bytes32() *)
     letS? key := StateError.lift_lens Evm.Lens.stack pop in
     let key := Uint.Make (U256.to_Z key) in
     let key := to_be_bytes32 key in
     (* GAS *)
-    (* 
-    if (evm.message.current_target, key) in evm.accessed_storage_keys:
-        charge_gas(evm, GAS_WARM_ACCESS)
-    else:
-        evm.accessed_storage_keys.add((evm.message.current_target, key))
-        charge_gas(evm, GAS_COLD_SLOAD)
-    *)
     letS? evm := readS? in
     let '(Evm.Make message rest) := evm in
     let evm_message_current_target := message.(Message.current_target) in

From 4886df20d7d5d039c01a120a3298130412c6989f Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 24 Jun 2024 15:34:50 +0800
Subject: [PATCH 19/26] minor: comment update

---
 .../ethereum/paris/vm/instructions/simulations/storage.v   | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index bab8f9e..3651873 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -39,7 +39,7 @@ Definition get_storage_original (state : State.t) (address : Address.t) (key : B
 
 (* TODO: (progress) things to do on this draft:
 - replace `List.In` with `List.find` + `is_none`(?)
-- rest of the draft
+- finish sstore
 *)
 
 (* def sload(evm: Evm) -> None:
@@ -82,7 +82,8 @@ Definition sload : MS? Evm.t Exception.t unit :=
     let evm_message_current_target := message.(Message.current_target) in
     let evm_rest_accessed_storage_keys := rest.(Evm.Rest.accessed_storage_keys) in
     letS? _ := 
-    if List.In (evm_message_current_target, key) evm_rest_accessed_storage_keys (* TODO: Fix the List.In *)
+    (* TODO: Fix the List.In *)
+    if List.In (evm_message_current_target, key) evm_rest_accessed_storage_keys
     then charge_gas GAS_WARM_ACCESS
     else (
       (* TODO: check if the added element is added in the correct place *)
@@ -91,6 +92,8 @@ Definition sload : MS? Evm.t Exception.t unit :=
         (evm_message_current_target, key) :: evm_rest_accessed_storage_keys in
       let rest := rest <| Evm.Rest.accessed_storage_keys := evm_rest_accessed_storage_keys |> in
       let evm := Evm.Make message rest in
+      (* NOTE: After the state update, all previous variables like `evm_message_current_target`
+               should not be put into use anymore. This seems unsatisfying. *)
       letS? _ := writeS? evm in
       charge_gas GAS_COLD_SLOAD)
     in

From 8ea5670287888240dc910fdb5430cec697eec38f Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 24 Jun 2024 16:25:46 +0800
Subject: [PATCH 20/26] minor: comments & formats

---
 .../ethereum/paris/vm/instructions/simulations/storage.v    | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 3651873..9fefe1c 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -38,7 +38,7 @@ Definition get_storage (state : State.t) (address : Address.t) (key : Bytes.t) :
 Definition get_storage_original (state : State.t) (address : Address.t) (key : Bytes.t) : U256.t. Admitted.
 
 (* TODO: (progress) things to do on this draft:
-- replace `List.In` with `List.find` + `is_none`(?)
+- figure out a way to implement `list.contains` in coq
 - finish sstore
 *)
 
@@ -83,7 +83,9 @@ Definition sload : MS? Evm.t Exception.t unit :=
     let evm_rest_accessed_storage_keys := rest.(Evm.Rest.accessed_storage_keys) in
     letS? _ := 
     (* TODO: Fix the List.In *)
-    if List.In (evm_message_current_target, key) evm_rest_accessed_storage_keys
+    if has_some (List.find 
+    (* (evm_message_current_target, key)  *) _
+    evm_rest_accessed_storage_keys)
     then charge_gas GAS_WARM_ACCESS
     else (
       (* TODO: check if the added element is added in the correct place *)

From 1070351f899efe63d7488ffb1f2873ef74acf6a4 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 26 Jun 2024 00:53:46 +0800
Subject: [PATCH 21/26] feat: auto eqb predicate for inductive types

---
 CoqOfPython/ethereum/paris/simulations/fork_types.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CoqOfPython/ethereum/paris/simulations/fork_types.v b/CoqOfPython/ethereum/paris/simulations/fork_types.v
index b345aac..f7f5e2e 100644
--- a/CoqOfPython/ethereum/paris/simulations/fork_types.v
+++ b/CoqOfPython/ethereum/paris/simulations/fork_types.v
@@ -10,4 +10,8 @@ Module Address.
     match address with
     | Make address => address
     end.
+
+  Scheme Boolean Equality for t.
 End Address.
+
+Definition test_0 := Address.t_beq.
\ No newline at end of file

From 04c68ac08415ce45373cd4a75c5d9676d7a26d6d Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 26 Jun 2024 00:54:54 +0800
Subject: [PATCH 22/26] feat: lossless aliasing for mods to preserve funcs

---
 CoqOfPython/ethereum/paris/vm/simulations/__init__.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/CoqOfPython/ethereum/paris/vm/simulations/__init__.v b/CoqOfPython/ethereum/paris/vm/simulations/__init__.v
index 16baafb..49371c6 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/__init__.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/__init__.v
@@ -13,7 +13,12 @@ Require ethereum.crypto.simulations.hash.
 Module Hash32 := hash.Hash32.
 
 Require ethereum.paris.simulations.fork_types.
-Module Address := fork_types.Address.
+(* Module Address := fork_types.Address. *)
+
+Module Address. 
+(* Tyring to include the `t_beq` into this module as well *)
+Include fork_types.Address.
+End Address.
 
 Require ethereum.paris.simulations.state.
 Module State := state.State.

From a253eb3ee537e637196d98295570afd67b87c475 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 26 Jun 2024 00:55:20 +0800
Subject: [PATCH 23/26] minor: draft to test matching on pairs

---
 .../vm/instructions/simulations/storage.v     | 21 +++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 9fefe1c..41616a7 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -42,6 +42,27 @@ Definition get_storage_original (state : State.t) (address : Address.t) (key : B
 - finish sstore
 *)
 
+(* Scheme Boolean Equality for t. *)
+
+(* TODO: Test the following *)
+(* (* (evm_message_current_target, key)  *) _ *)
+(* TODO: generate a evm_message_current_target instance for testing *)
+Definition evm_message_current_target : Set. Admitted.
+
+(* TODO: test the following *)
+Definition test_0 : bool := Address.t_beq evm_message_current_target evm_message_current_target.
+
+Fixpoint pair_in (e : Address.t * Bytes32.t) (l : list (A * B)) : bool :=
+  let (a, k) := e in
+  match l with
+  | [] => false
+  | h :: tl => 
+    let (h1, h2) := h in
+    if (Address.t_beq a h1) && (Bytes32.t_beq k h2) 
+    then true 
+    else pair_in e tl
+  end.
+
 (* def sload(evm: Evm) -> None:
     """
     Loads to the stack, the value corresponding to a certain key from the

From eb3ae1c670ff4621971029b15473a421e9b529bf Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 27 Jun 2024 00:31:18 +0800
Subject: [PATCH 24/26] feat: finished testing `Address.t_beq`

---
 .../paris/vm/instructions/simulations/storage.v      | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 41616a7..5965c04 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -44,13 +44,15 @@ Definition get_storage_original (state : State.t) (address : Address.t) (key : B
 
 (* Scheme Boolean Equality for t. *)
 
-(* TODO: Test the following *)
-(* (* (evm_message_current_target, key)  *) _ *)
 (* TODO: generate a evm_message_current_target instance for testing *)
-Definition evm_message_current_target : Set. Admitted.
+Definition evm_message_current_target : MS? Evm.t Exception.t Address.t :=
+  letS? evm := readS? in
+  let '(Evm.Make message rest) := evm in
+  let evm_message_current_target := message.(Message.current_target) in
+  let test := Address.t_beq evm_message_current_target evm_message_current_target in
+  returnS? evm_message_current_target.
 
-(* TODO: test the following *)
-Definition test_0 : bool := Address.t_beq evm_message_current_target evm_message_current_target.
+(* TODO: Test Bytes32.b_eq *)
 
 Fixpoint pair_in (e : Address.t * Bytes32.t) (l : list (A * B)) : bool :=
   let (a, k) := e in

From a34cce2e57b2f4e732f3eba36c6a228ae0b49e6f Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 27 Jun 2024 01:15:14 +0800
Subject: [PATCH 25/26] feat: `list.contains` & `sload` simulation

---
 .../vm/instructions/simulations/storage.v     | 35 +++++++++----------
 CoqOfPython/ethereum/simulations/base_types.v |  2 ++
 2 files changed, 18 insertions(+), 19 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 5965c04..637e43a 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -8,7 +8,14 @@ Module U256 := base_types.U256.
 Definition U256_CEIL_VALUE := base_types.U256_CEIL_VALUE.
 Module Uint := base_types.Uint.
 Definition to_be_bytes32 := base_types.Uint.to_be_bytes32.
+Module FixedBytes := base_types.FixedBytes.
 Module Bytes := base_types.Bytes.
+Module Bytes32.
+(* We explicitly include the original module if we want to use its generated
+  boolean predicate. If the module is being alised through multiple files, 
+  such explicit inclusion is mandatory. *)
+Include base_types.Bytes32.
+End Bytes32.
 
 Require ethereum.paris.vm.simulations.__init__.
 Module Evm := __init__.Evm.
@@ -38,29 +45,18 @@ Definition get_storage (state : State.t) (address : Address.t) (key : Bytes.t) :
 Definition get_storage_original (state : State.t) (address : Address.t) (key : Bytes.t) : U256.t. Admitted.
 
 (* TODO: (progress) things to do on this draft:
-- figure out a way to implement `list.contains` in coq
 - finish sstore
 *)
 
-(* Scheme Boolean Equality for t. *)
-
-(* TODO: generate a evm_message_current_target instance for testing *)
-Definition evm_message_current_target : MS? Evm.t Exception.t Address.t :=
-  letS? evm := readS? in
-  let '(Evm.Make message rest) := evm in
-  let evm_message_current_target := message.(Message.current_target) in
-  let test := Address.t_beq evm_message_current_target evm_message_current_target in
-  returnS? evm_message_current_target.
-
-(* TODO: Test Bytes32.b_eq *)
-
-Fixpoint pair_in (e : Address.t * Bytes32.t) (l : list (A * B)) : bool :=
+(* Temorary `list.contains` implementation specifically for `sload`. I haven't figure out
+   a better way to generalize such function. *)
+Fixpoint pair_in (e : Address.t * Bytes32.t) (l : list (Address.t * Bytes32.t)) : bool :=
   let (a, k) := e in
   match l with
   | [] => false
   | h :: tl => 
     let (h1, h2) := h in
-    if (Address.t_beq a h1) && (Bytes32.t_beq k h2) 
+    if andb (Address.t_beq a h1) (Bytes32.t_beq k h2) 
     then true 
     else pair_in e tl
   end.
@@ -105,10 +101,7 @@ Definition sload : MS? Evm.t Exception.t unit :=
     let evm_message_current_target := message.(Message.current_target) in
     let evm_rest_accessed_storage_keys := rest.(Evm.Rest.accessed_storage_keys) in
     letS? _ := 
-    (* TODO: Fix the List.In *)
-    if has_some (List.find 
-    (* (evm_message_current_target, key)  *) _
-    evm_rest_accessed_storage_keys)
+    if pair_in (evm_message_current_target, key) evm_rest_accessed_storage_keys
     then charge_gas GAS_WARM_ACCESS
     else (
       (* TODO: check if the added element is added in the correct place *)
@@ -124,6 +117,10 @@ Definition sload : MS? Evm.t Exception.t unit :=
     in
     (* OPERATION *)
     let evm_env_state := rest.(Evm.Rest.env).(Environment.state) in
+    (* Change key type from `Bytes32` to `Bytes` *)
+    let '(Bytes32.Make key) := key in
+    let '(FixedBytes.Make key) := key in
+    let key := Bytes.Make key in
     let value := get_storage evm_env_state evm_message_current_target key in
     letS? _ := StateError.lift_lens Evm.Lens.stack (push value) in 
     (* PROGRAM COUNTER *) 
diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v
index c0b473e..d7e75d1 100644
--- a/CoqOfPython/ethereum/simulations/base_types.v
+++ b/CoqOfPython/ethereum/simulations/base_types.v
@@ -58,6 +58,8 @@ Module Bytes32.
     end.
 
   Definition LENGTH := 32.
+
+  Scheme Boolean Equality for t. 
 End Bytes32.
 
 Module Uint.

From ef31773d68485e0477443a829c8d3e46e1489f69 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 27 Jun 2024 01:33:54 +0800
Subject: [PATCH 26/26] minor: update on `sstore`

---
 .../vm/instructions/simulations/storage.v     | 70 +++++++++----------
 1 file changed, 35 insertions(+), 35 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
index 637e43a..3ee3c25 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -45,6 +45,8 @@ Definition get_storage (state : State.t) (address : Address.t) (key : Bytes.t) :
 Definition get_storage_original (state : State.t) (address : Address.t) (key : Bytes.t) : U256.t. Admitted.
 
 (* TODO: (progress) things to do on this draft:
+- Implement OutOfGasError
+- Figure out a way to simulate variable update within `if` clause
 - finish sstore
 *)
 
@@ -193,33 +195,31 @@ Definition sload : MS? Evm.t Exception.t unit :=
     evm.pc += 1 *)
 Definition sstore : MS? Evm.t Exception.t unit := 
   (* STACK *)
+  letS? key := StateError.lift_lens Evm.Lens.stack pop in
+  let key := Uint.Make (U256.to_Z key) in
+  let key := to_be_bytes32 key in
+
+  letS? new_value := StateError.lift_lens Evm.Lens.stack pop in
   (* 
-  key = pop(evm.stack).to_be_bytes32()
-  new_value = pop(evm.stack)
   if evm.gas_left <= GAS_CALL_STIPEND:
       raise OutOfGasError
+  *)
+  (* TODO: Get the evm.gas_left correctly *)
+  letS? evm := readS? in
+  let '(Evm.Make message rest) := evm in
+  let evm_gas_left := rest.(Evm.Rest.gas_left) in (* Uint *)
 
+  if (Uint.get evm_gas_left) <=? (Uint.get GAS_CALL_STIPEND)
+  then 
+    (* TODO: Implement the correct error type *)
+    StateError.lift_from_error (Error.raise (Exception.ArithmeticError ArithmeticError.OverflowError))
+  else
+  (* 
   original_value = get_storage_original(
       evm.env.state, evm.message.current_target, key
   )
   current_value = get_storage(evm.env.state, evm.message.current_target, key)
   *)
-  (* key = pop(evm.stack).to_be_bytes32() *)
-  letS? key := StateError.lift_lens Evm.Lens.stack pop in
-  let key := Uint.Make (U256.to_Z key) in
-  let key := to_be_bytes32 key in
-
-  letS? new_value := StateError.lift_lens Evm.Lens.stack pop in
-
-  if _ 
-  then 
-  (* TODO: Fill in the correct error type *)
-    StateError.lift_from_error (Error.raise (Exception.ArithmeticError ArithmeticError.OverflowError))
-  else _ (* the full content of the rest of the code *)
-
-  (* TODO: connect with the :? above *)
-  letS? evm := readS? in
-  let '(Evm.Make message message) := evm in
   let evm_env_state := rest.(Evm.Rest.env).(Environment.state) in
   let evm_message_current_target := message.(Message.current_target) in
 
@@ -231,30 +231,30 @@ Definition sstore : MS? Evm.t Exception.t unit :=
   (* if (evm.message.current_target, key) not in evm.accessed_storage_keys:
     evm.accessed_storage_keys.add((evm.message.current_target, key))
     gas_cost += GAS_COLD_SLOAD
-
-  if original_value == current_value and current_value != new_value:
-    if original_value == 0:
-        gas_cost += GAS_STORAGE_SET
-    else:
-        gas_cost += GAS_STORAGE_UPDATE - GAS_COLD_SLOAD
-  else:
-    gas_cost += GAS_WARM_ACCESS *)
+    *)
   letS? _ := 
-  if ~(List.In (evm_message_current_target, key) evm_rest_accessed_storage_keys)
+  if ~(pair_in (evm_message_current_target, key) evm_rest_accessed_storage_keys)
   then (
     (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
-    letS? _ := (* gas_cost += GAS_COLD_SLOAD *)
+      (* TODO: check if the added element is added in the correct place *)
+      let evm_rest_accessed_storage_keys := 
+        (evm_message_current_target, key) :: evm_rest_accessed_storage_keys in
+      let rest := rest <| Evm.Rest.accessed_storage_keys := evm_rest_accessed_storage_keys |> in
+      let evm := Evm.Make message rest in
+      (* NOTE: After the state update, all previous variables like `evm_message_current_target`
+               should not be put into use anymore. This seems unsatisfying. *)
+      letS? _ := writeS? evm in
+      (* TODO: gas_cost += GAS_COLD_SLOAD *)
   )
-  else tt in
-
+  else
   (* 
     if original_value == current_value and current_value != new_value:
-        if original_value == 0:
-            gas_cost += GAS_STORAGE_SET
-        else:
-            gas_cost += GAS_STORAGE_UPDATE - GAS_COLD_SLOAD
+      if original_value == 0:
+          gas_cost += GAS_STORAGE_SET
+      else:
+          gas_cost += GAS_STORAGE_UPDATE - GAS_COLD_SLOAD
     else:
-        gas_cost += GAS_WARM_ACCESS
+      gas_cost += GAS_WARM_ACCESS 
   *)
   letS? _ :=
   if _