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
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 *)
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..3ee3c25
--- /dev/null
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/storage.v
@@ -0,0 +1,299 @@
+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.
+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.
+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.
+Definition GAS_WARM_ACCESS := gas.GAS_WARM_ACCESS.
+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.
+Definition pop := stack.pop.
+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 do on this draft:
+- Implement OutOfGasError
+- Figure out a way to simulate variable update within `if` clause
+- finish sstore
+*)
+
+(* 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 andb (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
+    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 : 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
+    (* GAS *)
+    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
+    letS? _ := 
+    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 *)
+      (* 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
+      (* 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
+    (* 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 *) 
+    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 *)
+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
+  (* 
+  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)
+  *)
+  let evm_env_state := rest.(Evm.Rest.env).(Environment.state) in
+  let evm_message_current_target := message.(Message.current_target) in
+
+  let original_value := get_storage_original evm_env_state evm_message_current_target key in
+  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
+    *)
+  letS? _ := 
+  if ~(pair_in (evm_message_current_target, key) evm_rest_accessed_storage_keys)
+  then (
+    (* evm.accessed_storage_keys.add((evm.message.current_target, key)) *)
+      (* 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
+  (* 
+    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 _ 
+  then _ 
+  else 
+
+  (* 
+      # 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)
+
+  *)
+  (* 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.
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.
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 26e7568..d7e75d1 100644
--- a/CoqOfPython/ethereum/simulations/base_types.v
+++ b/CoqOfPython/ethereum/simulations/base_types.v
@@ -13,6 +13,23 @@ Definition U256_CEIL_VALUE : Z := 2^256.
 (* NOTE: Python built-in type. We put here for convenience. *)
 Definition bytearray := list ascii.
 
+(* 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
+*)
+
+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.
@@ -31,14 +48,21 @@ 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 Bytes32.
+  Inductive t : Set :=
+  | Make (bytes : FixedBytes.t).
+
+  Definition get (bytes : t) : FixedBytes.t :=
+    match bytes with
+    | Make bytes => bytes
+    end.
+
+  Definition LENGTH := 32.
+
+  Scheme Boolean Equality for t. 
+End Bytes32.
 
 Module Uint.
-(* NOTE: to_bytes would produce a list of byte with *undetermined* length
-*)
   Inductive t : Set :=
   | Make (value : Z).
 
@@ -50,9 +74,9 @@ 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: 
+     - 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':
@@ -68,13 +92,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
@@ -84,7 +101,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
@@ -92,6 +109,36 @@ 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)
+  *)
+  (* NOTE: there might be order issues *)
+  Fixpoint to_bytes_helper (uint : Z) (order : nat) (store : list ascii): list ascii :=
+    match order with
+    | 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
+    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 '(Bytes.Make bytes) := bytes in
+    Bytes32.Make (FixedBytes.Make bytes).
 End Uint.
 
 Module FixedUint.
@@ -340,18 +387,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).
@@ -381,13 +416,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..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).
@@ -91,4 +93,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