Minor updates

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 *)

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.
 
 (* 

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