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] 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 :=