From 897e74d752b155f1e90ea87f34bdeda171a100a5 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 12 Jun 2024 13:36:31 +0800
Subject: [PATCH 01/12] Initial draft

---
 .../ethereum/paris/simulations/fork_types.v   |   2 +
 .../vm/instructions/simulations/keccak.v      | 116 ++++++++++++++++++
 .../ethereum/paris/vm/simulations/gas.v       |  55 ++++++++-
 .../ethereum/utils/simulations/numeric.v      |  22 ++++
 4 files changed, 194 insertions(+), 1 deletion(-)
 create mode 100644 CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
 create mode 100644 CoqOfPython/ethereum/utils/simulations/numeric.v

diff --git a/CoqOfPython/ethereum/paris/simulations/fork_types.v b/CoqOfPython/ethereum/paris/simulations/fork_types.v
index 1efcb6c..d395e8a 100644
--- a/CoqOfPython/ethereum/paris/simulations/fork_types.v
+++ b/CoqOfPython/ethereum/paris/simulations/fork_types.v
@@ -1,6 +1,8 @@
 Require Import CoqOfPython.CoqOfPython.
 Require ethereum.simulations.base_types.
 
+
+
 Module Address.
   Inductive t : Set :=
   | Make (address : base_types.Bytes20.t).
diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
new file mode 100644
index 0000000..b1b419a
--- /dev/null
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
@@ -0,0 +1,116 @@
+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_KECCAK256 := gas.GAS_KECCAK256.
+Definition GAS_KECCAK256_WORD := gas.GAS_KECCAK256_WORD.
+Definition calculate_gas_extend_memory := gas.calculate_gas_extend_memory.
+Definition charge_gas := gas.charge_gas.
+
+Require ethereum.paris.vm.simulations.stack.
+Definition pop := stack.pop.
+Definition push := stack.push.
+
+Import simulations.CoqOfPython.Notations.
+
+(*  *)
+Axiom keccak256 (bytes : FixedBytes.t) : FixBytes.t. Admitted. 
+
+(* 
+from ethereum.utils.numeric import ceil32
+
+from .. import Evm
+from ..gas import (
+    GAS_KECCAK256,
+    GAS_KECCAK256_WORD,
+    calculate_gas_extend_memory,
+    charge_gas,
+)
+from ..memory import memory_read_bytes
+from ..stack import pop, push
+
+
+def keccak(evm: Evm) -> None:
+    """
+    Pushes to the stack the Keccak-256 hash of a region of memory.
+
+    This also expands the memory, in case the memory is insufficient to
+    access the data's memory location.
+
+    Parameters
+    ----------
+    evm :
+        The current EVM frame.
+
+    """
+    # STACK
+    memory_start_index = pop(evm.stack)
+    size = pop(evm.stack)
+
+    # GAS
+    words = ceil32(Uint(size)) // 32
+    word_gas_cost = GAS_KECCAK256_WORD * words
+    extend_memory = calculate_gas_extend_memory(
+        evm.memory, [(memory_start_index, size)]
+    )
+    charge_gas(evm, GAS_KECCAK256 + word_gas_cost + extend_memory.cost)
+
+    # OPERATION
+    evm.memory += b"\x00" * extend_memory.expand_by
+    data = memory_read_bytes(evm.memory, memory_start_index, size)
+    hash = keccak256(data)
+
+    push(evm.stack, U256.from_be_bytes(hash))
+
+    # PROGRAM COUNTER
+    evm.pc += 1
+*)
+Definition bitwise_and : MS? Evm.t Exception.t unit := 
+  (* STACK *)
+  letS? memory_start_index := StateError.lift_lens Evm.Lens.stack pop in
+  letS? size := StateError.lift_lens Evm.Lens.stack pop in
+  (* GAS *)
+  (* 
+    words = ceil32(Uint(size)) // 32
+    word_gas_cost = GAS_KECCAK256_WORD * words
+    extend_memory = calculate_gas_extend_memory(
+        evm.memory, [(memory_start_index, size)]
+    )
+    charge_gas(evm, GAS_KECCAK256 + word_gas_cost + extend_memory.cost)
+  *)
+  let words : Uint32 := _ in
+  let word_gas_cost := _ in
+  let evm_memory := _ in 
+  let extend_memory := calculate_gas_extend_memory _ in
+  letS? _ := charge_gas GAS_KECCAK256 + word_gas_cost + extend_memory.cost in
+  (* OPERATION *)
+  (* 
+    evm.memory += b"\x00" * extend_memory.expand_by
+    data = memory_read_bytes(evm.memory, memory_start_index, size)
+    hash = keccak256(data)
+
+    push(evm.stack, U256.from_be_bytes(hash))
+  *)
+  (* Construct correrctly the b"\x00" *)
+  let b_x00 := base_types.FixedBytes.Make [Ascii.ascii_of_N 0] in
+  let b_x00 := hash.Bytes32.Make b_x00 in
+  let b_x00 := __init__.Hash32.Make b_x00 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.
\ No newline at end of file
diff --git a/CoqOfPython/ethereum/paris/vm/simulations/gas.v b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
index 7cfb7ce..01cde41 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/gas.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
@@ -52,4 +52,57 @@ Definition GAS_COLD_SLOAD := Uint.Make 2100.
 Definition GAS_COLD_ACCOUNT_ACCESS := Uint.Make 2600.
 Definition GAS_WARM_ACCESS := Uint.Make 100.
 
-Parameter charge_gas : forall (amount : Uint.t), MS? Evm.t Exception.t unit.
+(* Parameter charge_gas : forall (amount : Uint.t), MS? Evm.t Exception.t unit. *)
+Parameter charge_gas : forall (amount : Uint.t), unit.
+
+(* 
+class ExtendMemory:
+    """
+    Define the parameters for memory extension in opcodes
+
+    `cost`: `ethereum.base_types.Uint`
+        The gas required to perform the extension
+    `expand_by`: `ethereum.base_types.Uint`
+        The size by which the memory will be extended
+    """
+
+    cost: Uint
+    expand_by: Uint
+*)
+Module ExtendMemory.
+  Record t : Set :={
+    cost : Uint.t;
+    expand_by : Uint.t;
+  }.
+End ExtendMemory.
+
+(* def calculate_gas_extend_memory(
+    memory: bytearray, extensions: List[Tuple[U256, U256]]
+) -> ExtendMemory: *)
+Parameter calculate_gas_extend_memory : 
+  forall (memory : list FixedBytes) (extensions : list (U256.t, U256.t)), ExtendMemory.
+
+  (* 
+  def ceil32(value: Uint) -> Uint:
+    """
+    Converts a unsigned integer to the next closest multiple of 32.
+
+    Parameters
+    ----------
+    value :
+        The value whose ceil32 is to be calculated.
+
+    Returns
+    -------
+    ceil32 : `ethereum.base_types.U256`
+        The same value if it's a perfect multiple of 32
+        else it returns the smallest multiple of 32
+        that is greater than `value`.
+    """
+    ceiling = Uint(32)
+    remainder = value % ceiling
+    if remainder == Uint(0):
+        return value
+    else:
+        return value + ceiling - remainder
+  *)
\ No newline at end of file
diff --git a/CoqOfPython/ethereum/utils/simulations/numeric.v b/CoqOfPython/ethereum/utils/simulations/numeric.v
new file mode 100644
index 0000000..776aa53
--- /dev/null
+++ b/CoqOfPython/ethereum/utils/simulations/numeric.v
@@ -0,0 +1,22 @@
+(* def ceil32(value: Uint) -> Uint:
+    """
+    Converts a unsigned integer to the next closest multiple of 32.
+
+    Parameters
+    ----------
+    value :
+        The value whose ceil32 is to be calculated.
+
+    Returns
+    -------
+    ceil32 : `ethereum.base_types.U256`
+        The same value if it's a perfect multiple of 32
+        else it returns the smallest multiple of 32
+        that is greater than `value`.
+    """
+    ceiling = Uint(32)
+    remainder = value % ceiling
+    if remainder == Uint(0):
+        return value
+    else:
+        return value + ceiling - remainder *)
\ No newline at end of file

From 8fb843d604989a073559b4811523c7b49a85e221 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 12 Jun 2024 14:34:32 +0800
Subject: [PATCH 02/12] Update

---
 CoqOfPython/ethereum/utils/simulations/numeric.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/CoqOfPython/ethereum/utils/simulations/numeric.v b/CoqOfPython/ethereum/utils/simulations/numeric.v
index 776aa53..9f95f6e 100644
--- a/CoqOfPython/ethereum/utils/simulations/numeric.v
+++ b/CoqOfPython/ethereum/utils/simulations/numeric.v
@@ -19,4 +19,12 @@
     if remainder == Uint(0):
         return value
     else:
-        return value + ceiling - remainder *)
\ No newline at end of file
+        return value + ceiling - remainder *)
+
+(* TODO: Finish below *)
+Definition ceil32 (value : Uint) : Uint :=
+  let ceiling := Uint.Make 32 in
+  let remainder := value % ceiling in
+  if remainder =? Uint 0
+  then value
+  else value + ceiling - remainder.
\ No newline at end of file

From 2db26a79cc920e422695cba2659c78d62d9b8c40 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Tue, 18 Jun 2024 21:06:09 +0800
Subject: [PATCH 03/12] minor updates

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

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
index b1b419a..29b9809 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
@@ -23,7 +23,7 @@ Definition push := stack.push.
 
 Import simulations.CoqOfPython.Notations.
 
-(*  *)
+(* TODO: Check the axiomatized parts are done correctly *)
 Axiom keccak256 (bytes : FixedBytes.t) : FixBytes.t. Admitted. 
 
 (* 

From 5552215690d8e58238f5fd71264f08896a406c03 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 13:26:41 +0800
Subject: [PATCH 04/12] Update current progress & conflict at `gas`

---
 .../vm/instructions/simulations/keccak.v      | 34 +++++++++++++++----
 .../ethereum/paris/vm/simulations/gas.v       | 29 ++--------------
 CoqOfPython/ethereum/simulations/base_types.v | 13 +++++++
 .../ethereum/utils/simulations/numeric.v      |  5 +--
 4 files changed, 46 insertions(+), 35 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
index 29b9809..9fed41c 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
@@ -8,6 +8,8 @@ Module U256 := base_types.U256.
 Definition U256_CEIL_VALUE := base_types.U256_CEIL_VALUE.
 Module Uint := base_types.Uint.
 
+Definition bytearray := base_types.bytearray.
+
 Require ethereum.paris.vm.simulations.__init__.
 Module Evm := __init__.Evm.
 
@@ -21,10 +23,20 @@ Require ethereum.paris.vm.simulations.stack.
 Definition pop := stack.pop.
 Definition push := stack.push.
 
+Require ethereum.utils.simulations.numeric.
+Definition ceil32 := numeric.ceil32.
+
 Import simulations.CoqOfPython.Notations.
 
 (* TODO: Check the axiomatized parts are done correctly *)
-Axiom keccak256 (bytes : FixedBytes.t) : FixBytes.t. Admitted. 
+Axiom keccak256 (bytes : FixedBytes.t) : FixBytes.t.
+(* 
+  def memory_read_bytes(
+      memory: bytearray, start_position: U256, size: U256
+  ) -> bytearray:
+*)
+(* NOTE: Upon further implementations on `memory`, we can move this axiomatized function to `memory.py`. *)
+Axiom memory_read_bytes (memory : bytearray) (start_position size : U256) : bytearray.
 
 (* 
 from ethereum.utils.numeric import ceil32
@@ -88,10 +100,17 @@ Definition bitwise_and : MS? Evm.t Exception.t unit :=
     )
     charge_gas(evm, GAS_KECCAK256 + word_gas_cost + extend_memory.cost)
   *)
-  let words : Uint32 := _ in
-  let word_gas_cost := _ in
-  let evm_memory := _ in 
-  let extend_memory := calculate_gas_extend_memory _ in
+  (* size : U256 -> Uint *)
+  let words := ceil32(U256.to_Uint size) in
+  let word_gas_cost := Uint.Make (Uint.get GAS_KECCAK256_WORD * Uint.get words) in
+
+  (* Get evm.memory *)
+  letS? evm := readS? in
+  let '(Evm.Make _ rest) := evm in
+  let evm_memory := rest.(Evm.Rest.memory) in
+
+  let extend_memory := calculate_gas_extend_memory evm_memory (list (memory_start_index, size)) in (* TODO: Fix this *)
+
   letS? _ := charge_gas GAS_KECCAK256 + word_gas_cost + extend_memory.cost in
   (* OPERATION *)
   (* 
@@ -106,10 +125,11 @@ Definition bitwise_and : MS? Evm.t Exception.t unit :=
   let b_x00 := hash.Bytes32.Make b_x00 in
   let b_x00 := __init__.Hash32.Make b_x00 in
 
-
+  let data := memory_read_bytes evm_memory memory_start_index size in
+  let hash := keccak256 data in
 
   letS? _ := StateError.lift_lens Evm.Lens.stack (
-    push (U256.bit_and x y)) in 
+    push (U256.make (FixedBytes.get hash))) in 
   (* PROGRAM COUNTER *) 
   letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
   (inl tt, Uint.__add__ pc (Uint.Make 1))) in
diff --git a/CoqOfPython/ethereum/paris/vm/simulations/gas.v b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
index 01cde41..bbe3fd6 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/gas.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
@@ -52,6 +52,8 @@ Definition GAS_COLD_SLOAD := Uint.Make 2100.
 Definition GAS_COLD_ACCOUNT_ACCESS := Uint.Make 2600.
 Definition GAS_WARM_ACCESS := Uint.Make 100.
 
+Definition bytearray := base_types.bytearray.
+
 (* Parameter charge_gas : forall (amount : Uint.t), MS? Evm.t Exception.t unit. *)
 Parameter charge_gas : forall (amount : Uint.t), unit.
 
@@ -80,29 +82,4 @@ End ExtendMemory.
     memory: bytearray, extensions: List[Tuple[U256, U256]]
 ) -> ExtendMemory: *)
 Parameter calculate_gas_extend_memory : 
-  forall (memory : list FixedBytes) (extensions : list (U256.t, U256.t)), ExtendMemory.
-
-  (* 
-  def ceil32(value: Uint) -> Uint:
-    """
-    Converts a unsigned integer to the next closest multiple of 32.
-
-    Parameters
-    ----------
-    value :
-        The value whose ceil32 is to be calculated.
-
-    Returns
-    -------
-    ceil32 : `ethereum.base_types.U256`
-        The same value if it's a perfect multiple of 32
-        else it returns the smallest multiple of 32
-        that is greater than `value`.
-    """
-    ceiling = Uint(32)
-    remainder = value % ceiling
-    if remainder == Uint(0):
-        return value
-    else:
-        return value + ceiling - remainder
-  *)
\ No newline at end of file
+  forall (memory : bytearray) (extensions : list (prod U256.t U256.t)), ExtendMemory.t.
\ No newline at end of file
diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v
index 6659b0a..7b52025 100644
--- a/CoqOfPython/ethereum/simulations/base_types.v
+++ b/CoqOfPython/ethereum/simulations/base_types.v
@@ -10,6 +10,9 @@ Definition U255_CEIL_VALUE : Z := 2^255.
 
 Definition U256_CEIL_VALUE : Z := 2^256.
 
+(* NOTE: Python built-in type. We put here for convenience. *)
+Definition bytearray := list ascii.
+
 Module Uint.
   Inductive t : Set :=
   | Make (value : Z).
@@ -110,6 +113,9 @@ Module FixedUint.
       MAX_VALUE := self.(MAX_VALUE);
       value := Z.lnot x;
     |}.
+
+  Definition to_Uint (self : t) : Uint.t :=
+    let x := self.(value)%Z in Uint.Make x.
 End FixedUint.
 
 Module U256.
@@ -185,6 +191,9 @@ Module U256.
     (* TODO: here 2^256 - 1 should be the max value of the corresponded class.
        To be modified in the future. *)
     else (U256.of_Z (Z.land value (2^256 - 1))).
+
+  Definition to_Uint (self : t) : Uint.t :=
+    let '(Make x) := self in FixedUint.to_Uint x.
 End U256.
 
 Module U32.
@@ -217,6 +226,10 @@ Module U64.
     match value with
     | Make value => value
     end.
+
+  Definition to_Uint (self : t) : Uint.t :=
+    let '(Make value) := self in 
+      FixedUint.to_Uint value.
 End U64.
 
 Module FixedBytes.
diff --git a/CoqOfPython/ethereum/utils/simulations/numeric.v b/CoqOfPython/ethereum/utils/simulations/numeric.v
index 9f95f6e..dc8c72e 100644
--- a/CoqOfPython/ethereum/utils/simulations/numeric.v
+++ b/CoqOfPython/ethereum/utils/simulations/numeric.v
@@ -22,9 +22,10 @@
         return value + ceiling - remainder *)
 
 (* TODO: Finish below *)
-Definition ceil32 (value : Uint) : Uint :=
+Definition ceil32 (value : Uint) : Uint. Admitted.
+ (* :=
   let ceiling := Uint.Make 32 in
   let remainder := value % ceiling in
   if remainder =? Uint 0
   then value
-  else value + ceiling - remainder.
\ No newline at end of file
+  else value + ceiling - remainder. *)
\ No newline at end of file

From 7e9c1d6fa9269b95e0182423d9bf2b7d9f575988 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 14:21:31 +0800
Subject: [PATCH 05/12] Update `keccak.v` & fixed all other files

---
 .../vm/instructions/simulations/keccak.v      | 21 +++++--------------
 .../ethereum/paris/vm/simulations/gas.v       |  4 ++--
 .../ethereum/utils/simulations/numeric.v      | 12 ++++++++++-
 3 files changed, 18 insertions(+), 19 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
index 9fed41c..5f5ea9d 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
@@ -7,6 +7,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.
+Module FixedBytes := base_types.FixedBytes.
 
 Definition bytearray := base_types.bytearray.
 
@@ -18,6 +19,7 @@ Definition GAS_KECCAK256 := gas.GAS_KECCAK256.
 Definition GAS_KECCAK256_WORD := gas.GAS_KECCAK256_WORD.
 Definition calculate_gas_extend_memory := gas.calculate_gas_extend_memory.
 Definition charge_gas := gas.charge_gas.
+Definition ExtendMemory := gas.ExtendMemory.
 
 Require ethereum.paris.vm.simulations.stack.
 Definition pop := stack.pop.
@@ -28,30 +30,17 @@ Definition ceil32 := numeric.ceil32.
 
 Import simulations.CoqOfPython.Notations.
 
-(* TODO: Check the axiomatized parts are done correctly *)
-Axiom keccak256 (bytes : FixedBytes.t) : FixBytes.t.
+Definition keccak256 (bytes : FixedBytes.t) : FixedBytes.t. Admitted.
 (* 
   def memory_read_bytes(
       memory: bytearray, start_position: U256, size: U256
   ) -> bytearray:
 *)
 (* NOTE: Upon further implementations on `memory`, we can move this axiomatized function to `memory.py`. *)
-Axiom memory_read_bytes (memory : bytearray) (start_position size : U256) : bytearray.
+Definition memory_read_bytes (memory : bytearray) (start_position size : U256.t) : bytearray.
+Admitted.
 
 (* 
-from ethereum.utils.numeric import ceil32
-
-from .. import Evm
-from ..gas import (
-    GAS_KECCAK256,
-    GAS_KECCAK256_WORD,
-    calculate_gas_extend_memory,
-    charge_gas,
-)
-from ..memory import memory_read_bytes
-from ..stack import pop, push
-
-
 def keccak(evm: Evm) -> None:
     """
     Pushes to the stack the Keccak-256 hash of a region of memory.
diff --git a/CoqOfPython/ethereum/paris/vm/simulations/gas.v b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
index bbe3fd6..e399ec5 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/gas.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
@@ -54,8 +54,8 @@ Definition GAS_WARM_ACCESS := Uint.Make 100.
 
 Definition bytearray := base_types.bytearray.
 
-(* Parameter charge_gas : forall (amount : Uint.t), MS? Evm.t Exception.t unit. *)
-Parameter charge_gas : forall (amount : Uint.t), unit.
+Parameter charge_gas : forall (amount : Uint.t), MS? Evm.t Exception.t unit.
+(* Parameter charge_gas : forall (amount : Uint.t), unit. *)
 
 (* 
 class ExtendMemory:
diff --git a/CoqOfPython/ethereum/utils/simulations/numeric.v b/CoqOfPython/ethereum/utils/simulations/numeric.v
index dc8c72e..c61fc1e 100644
--- a/CoqOfPython/ethereum/utils/simulations/numeric.v
+++ b/CoqOfPython/ethereum/utils/simulations/numeric.v
@@ -1,3 +1,13 @@
+Require Import CoqOfPython.CoqOfPython.
+Require Import simulations.CoqOfPython.
+Require Import simulations.builtins.
+
+Require ethereum.simulations.base_types.
+Module U256 := base_types.U256.
+Module Uint := base_types.Uint.
+
+Import simulations.CoqOfPython.Notations.
+
 (* def ceil32(value: Uint) -> Uint:
     """
     Converts a unsigned integer to the next closest multiple of 32.
@@ -22,7 +32,7 @@
         return value + ceiling - remainder *)
 
 (* TODO: Finish below *)
-Definition ceil32 (value : Uint) : Uint. Admitted.
+Definition ceil32 (value : Uint.t) : Uint.t. Admitted.
  (* :=
   let ceiling := Uint.Make 32 in
   let remainder := value % ceiling in

From 6321a77fde43fecaaefe0fe4f19159fba2258790 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 14:49:48 +0800
Subject: [PATCH 06/12] Fixing `ExtendMemory` not found issue on local br

---
 .../ethereum/paris/vm/instructions/simulations/keccak.v      | 2 +-
 CoqOfPython/ethereum/paris/vm/simulations/gas.v              | 5 ++++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
index 5f5ea9d..a4905e1 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
@@ -17,9 +17,9 @@ Module Evm := __init__.Evm.
 Require ethereum.paris.vm.simulations.gas.
 Definition GAS_KECCAK256 := gas.GAS_KECCAK256.
 Definition GAS_KECCAK256_WORD := gas.GAS_KECCAK256_WORD.
+Definition ExtendMemory := gas.ExtendMemory.
 Definition calculate_gas_extend_memory := gas.calculate_gas_extend_memory.
 Definition charge_gas := gas.charge_gas.
-Definition ExtendMemory := gas.ExtendMemory.
 
 Require ethereum.paris.vm.simulations.stack.
 Definition pop := stack.pop.
diff --git a/CoqOfPython/ethereum/paris/vm/simulations/gas.v b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
index e399ec5..449a070 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/gas.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
@@ -82,4 +82,7 @@ End ExtendMemory.
     memory: bytearray, extensions: List[Tuple[U256, U256]]
 ) -> ExtendMemory: *)
 Parameter calculate_gas_extend_memory : 
-  forall (memory : bytearray) (extensions : list (prod U256.t U256.t)), ExtendMemory.t.
\ No newline at end of file
+  forall (memory : bytearray) (extensions : list (prod U256.t U256.t)), ExtendMemory.t.
+
+Definition test. 
+End test.
\ No newline at end of file

From 7923cb061db08d064dee443b12073ad52a375618 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 15:10:33 +0800
Subject: [PATCH 07/12] Minor updates according to comments

---
 CoqOfPython/ethereum/paris/simulations/fork_types.v             | 1 -
 CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v | 2 +-
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/simulations/fork_types.v b/CoqOfPython/ethereum/paris/simulations/fork_types.v
index d395e8a..b345aac 100644
--- a/CoqOfPython/ethereum/paris/simulations/fork_types.v
+++ b/CoqOfPython/ethereum/paris/simulations/fork_types.v
@@ -2,7 +2,6 @@ Require Import CoqOfPython.CoqOfPython.
 Require ethereum.simulations.base_types.
 
 
-
 Module Address.
   Inductive t : Set :=
   | Make (address : base_types.Bytes20.t).
diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
index a4905e1..b6023a6 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
@@ -122,4 +122,4 @@ Definition bitwise_and : MS? Evm.t Exception.t unit :=
   (* PROGRAM COUNTER *) 
   letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
   (inl tt, Uint.__add__ pc (Uint.Make 1))) in
-  returnS? tt.
\ No newline at end of file
+  returnS? tt.

From ed326c75be330a12c4dfce05f6b44ddeb4f87cdd Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 15:24:29 +0800
Subject: [PATCH 08/12] minor updates

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

diff --git a/CoqOfPython/ethereum/paris/vm/simulations/gas.v b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
index 449a070..54c9481 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/gas.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
@@ -84,5 +84,5 @@ End ExtendMemory.
 Parameter calculate_gas_extend_memory : 
   forall (memory : bytearray) (extensions : list (prod U256.t U256.t)), ExtendMemory.t.
 
-Definition test. 
+Module test. 
 End test.
\ No newline at end of file

From 0e8a07cae0299259222976d2eecf9410f7a1d60b Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 16:28:39 +0800
Subject: [PATCH 09/12] More updates?

---
 CoqOfPython/ethereum/paris/vm/simulations/gas.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/simulations/gas.v b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
index 54c9481..dda0f97 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/gas.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
@@ -55,7 +55,7 @@ Definition GAS_WARM_ACCESS := Uint.Make 100.
 Definition bytearray := base_types.bytearray.
 
 Parameter charge_gas : forall (amount : Uint.t), MS? Evm.t Exception.t unit.
-(* Parameter charge_gas : forall (amount : Uint.t), unit. *)
+(* Definition charge_gas (amount : Uint.t) : unit. *)
 
 (* 
 class ExtendMemory:
@@ -76,13 +76,14 @@ Module ExtendMemory.
     cost : Uint.t;
     expand_by : Uint.t;
   }.
+
+  Definition test_function : unit. Admitted.
 End ExtendMemory.
 
+Definition testtest : ExtendMemory.t. Admitted.
+
 (* def calculate_gas_extend_memory(
     memory: bytearray, extensions: List[Tuple[U256, U256]]
 ) -> ExtendMemory: *)
 Parameter calculate_gas_extend_memory : 
   forall (memory : bytearray) (extensions : list (prod U256.t U256.t)), ExtendMemory.t.
-
-Module test. 
-End test.
\ No newline at end of file

From 8e43584c017b4ded810ff42e7b11145384aa30f5 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 17:36:52 +0800
Subject: [PATCH 10/12] Update: resolved `ExtendMemory` issue

---
 .../paris/vm/instructions/simulations/keccak.v        | 11 ++++++-----
 CoqOfPython/ethereum/paris/vm/simulations/gas.v       | 10 +++++-----
 CoqOfPython/ethereum/paris/vm/simulations/stack.v     |  1 +
 3 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
index b6023a6..ecaeb01 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
@@ -17,7 +17,7 @@ Module Evm := __init__.Evm.
 Require ethereum.paris.vm.simulations.gas.
 Definition GAS_KECCAK256 := gas.GAS_KECCAK256.
 Definition GAS_KECCAK256_WORD := gas.GAS_KECCAK256_WORD.
-Definition ExtendMemory := gas.ExtendMemory.
+Definition ExtendMemory := gas.ExtendMemory.t.
 Definition calculate_gas_extend_memory := gas.calculate_gas_extend_memory.
 Definition charge_gas := gas.charge_gas.
 
@@ -39,7 +39,6 @@ Definition keccak256 (bytes : FixedBytes.t) : FixedBytes.t. Admitted.
 (* NOTE: Upon further implementations on `memory`, we can move this axiomatized function to `memory.py`. *)
 Definition memory_read_bytes (memory : bytearray) (start_position size : U256.t) : bytearray.
 Admitted.
-
 (* 
 def keccak(evm: Evm) -> None:
     """
@@ -98,9 +97,11 @@ Definition bitwise_and : MS? Evm.t Exception.t unit :=
   let '(Evm.Make _ rest) := evm in
   let evm_memory := rest.(Evm.Rest.memory) in
 
-  let extend_memory := calculate_gas_extend_memory evm_memory (list (memory_start_index, size)) in (* TODO: Fix this *)
+  let helper : list (gas.U256.t * gas.U256.t) := memory_start_index :: size :: [] in
+
+  let extend_memory := calculate_gas_extend_memory evm_memory (memory_start_index :: size :: [] ) in
 
-  letS? _ := charge_gas GAS_KECCAK256 + word_gas_cost + extend_memory.cost in
+  letS? _ := charge_gas GAS_KECCAK256 + word_gas_cost + extend_memory.(gas.ExtendMemory.cost) in
   (* OPERATION *)
   (* 
     evm.memory += b"\x00" * extend_memory.expand_by
@@ -118,7 +119,7 @@ Definition bitwise_and : MS? Evm.t Exception.t unit :=
   let hash := keccak256 data in
 
   letS? _ := StateError.lift_lens Evm.Lens.stack (
-    push (U256.make (FixedBytes.get hash))) in 
+    push (U256.Make (FixedBytes.get hash))) in 
   (* PROGRAM COUNTER *) 
   letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
   (inl tt, Uint.__add__ pc (Uint.Make 1))) in
diff --git a/CoqOfPython/ethereum/paris/vm/simulations/gas.v b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
index dda0f97..3c834d7 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/gas.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
@@ -76,14 +76,14 @@ Module ExtendMemory.
     cost : Uint.t;
     expand_by : Uint.t;
   }.
-
-  Definition test_function : unit. Admitted.
 End ExtendMemory.
 
-Definition testtest : ExtendMemory.t. Admitted.
-
 (* def calculate_gas_extend_memory(
     memory: bytearray, extensions: List[Tuple[U256, U256]]
 ) -> ExtendMemory: *)
 Parameter calculate_gas_extend_memory : 
-  forall (memory : bytearray) (extensions : list (prod U256.t U256.t)), ExtendMemory.t.
+  forall (memory : bytearray) (extensions : list (U256.t * U256.t)), ExtendMemory.t.
+
+Definition t : U256.t. Admitted.
+
+Definition tt : list (U256.t * U256.t) := (t, t) :: [].
\ No newline at end of file
diff --git a/CoqOfPython/ethereum/paris/vm/simulations/stack.v b/CoqOfPython/ethereum/paris/vm/simulations/stack.v
index e50f7a7..61f0d35 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/stack.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/stack.v
@@ -3,6 +3,7 @@ Require Import simulations.CoqOfPython.
 Require Import simulations.builtins.
 
 Require Import simulations.base_types.
+(* TODO: Check if this Module should be changed into Definition *)
 Module U256 := base_types.U256.
 
 Import simulations.CoqOfPython.Notations.

From 55f8df50cd80a50e7b58f500eca1d0359e266b45 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 17:51:35 +0800
Subject: [PATCH 11/12] Finish `keccak`

---
 .../vm/instructions/simulations/keccak.v      | 25 +++----------------
 1 file changed, 4 insertions(+), 21 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
index ecaeb01..304b848 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v
@@ -30,7 +30,7 @@ Definition ceil32 := numeric.ceil32.
 
 Import simulations.CoqOfPython.Notations.
 
-Definition keccak256 (bytes : FixedBytes.t) : FixedBytes.t. Admitted.
+Definition keccak256 (bytes : bytearray) : FixedBytes.t. Admitted.
 (* 
   def memory_read_bytes(
       memory: bytearray, start_position: U256, size: U256
@@ -80,14 +80,6 @@ Definition bitwise_and : MS? Evm.t Exception.t unit :=
   letS? memory_start_index := StateError.lift_lens Evm.Lens.stack pop in
   letS? size := StateError.lift_lens Evm.Lens.stack pop in
   (* GAS *)
-  (* 
-    words = ceil32(Uint(size)) // 32
-    word_gas_cost = GAS_KECCAK256_WORD * words
-    extend_memory = calculate_gas_extend_memory(
-        evm.memory, [(memory_start_index, size)]
-    )
-    charge_gas(evm, GAS_KECCAK256 + word_gas_cost + extend_memory.cost)
-  *)
   (* size : U256 -> Uint *)
   let words := ceil32(U256.to_Uint size) in
   let word_gas_cost := Uint.Make (Uint.get GAS_KECCAK256_WORD * Uint.get words) in
@@ -97,19 +89,10 @@ Definition bitwise_and : MS? Evm.t Exception.t unit :=
   let '(Evm.Make _ rest) := evm in
   let evm_memory := rest.(Evm.Rest.memory) in
 
-  let helper : list (gas.U256.t * gas.U256.t) := memory_start_index :: size :: [] in
+  let extend_memory := calculate_gas_extend_memory evm_memory ((memory_start_index, size) :: []) in
 
-  let extend_memory := calculate_gas_extend_memory evm_memory (memory_start_index :: size :: [] ) in
-
-  letS? _ := charge_gas GAS_KECCAK256 + word_gas_cost + extend_memory.(gas.ExtendMemory.cost) in
+  letS? _ := charge_gas (Uint.Make ((Uint.get GAS_KECCAK256) + (Uint.get word_gas_cost) + (Uint.get extend_memory.(gas.ExtendMemory.cost)))) in
   (* OPERATION *)
-  (* 
-    evm.memory += b"\x00" * extend_memory.expand_by
-    data = memory_read_bytes(evm.memory, memory_start_index, size)
-    hash = keccak256(data)
-
-    push(evm.stack, U256.from_be_bytes(hash))
-  *)
   (* Construct correrctly the b"\x00" *)
   let b_x00 := base_types.FixedBytes.Make [Ascii.ascii_of_N 0] in
   let b_x00 := hash.Bytes32.Make b_x00 in
@@ -119,7 +102,7 @@ Definition bitwise_and : MS? Evm.t Exception.t unit :=
   let hash := keccak256 data in
 
   letS? _ := StateError.lift_lens Evm.Lens.stack (
-    push (U256.Make (FixedBytes.get hash))) in 
+    push (U256.of_Z (Uint.get (Uint.from_bytes hash)))) in 
   (* PROGRAM COUNTER *) 
   letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
   (inl tt, Uint.__add__ pc (Uint.Make 1))) in

From 6818d7c17473486e4a3ebf0be4c5005f315213f6 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 19 Jun 2024 19:13:39 +0800
Subject: [PATCH 12/12] Remove test codes & Fix format

---
 CoqOfPython/ethereum/paris/vm/simulations/gas.v  | 7 ++-----
 CoqOfPython/ethereum/simulations/base_types.v    | 5 +++++
 CoqOfPython/ethereum/utils/simulations/numeric.v | 2 +-
 3 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/CoqOfPython/ethereum/paris/vm/simulations/gas.v b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
index 3c834d7..da4a375 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/gas.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/gas.v
@@ -54,8 +54,9 @@ 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.
-(* Definition charge_gas (amount : Uint.t) : unit. *)
 
 (* 
 class ExtendMemory:
@@ -83,7 +84,3 @@ End ExtendMemory.
 ) -> ExtendMemory: *)
 Parameter calculate_gas_extend_memory : 
   forall (memory : bytearray) (extensions : list (U256.t * U256.t)), ExtendMemory.t.
-
-Definition t : U256.t. Admitted.
-
-Definition tt : list (U256.t * U256.t) := (t, t) :: [].
\ No newline at end of file
diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v
index 3b976e2..26e7568 100644
--- a/CoqOfPython/ethereum/simulations/base_types.v
+++ b/CoqOfPython/ethereum/simulations/base_types.v
@@ -31,6 +31,11 @@ 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 Uint.
 (* NOTE: to_bytes would produce a list of byte with *undetermined* length
 *)
diff --git a/CoqOfPython/ethereum/utils/simulations/numeric.v b/CoqOfPython/ethereum/utils/simulations/numeric.v
index c61fc1e..aa64640 100644
--- a/CoqOfPython/ethereum/utils/simulations/numeric.v
+++ b/CoqOfPython/ethereum/utils/simulations/numeric.v
@@ -38,4 +38,4 @@ Definition ceil32 (value : Uint.t) : Uint.t. Admitted.
   let remainder := value % ceiling in
   if remainder =? Uint 0
   then value
-  else value + ceiling - remainder. *)
\ No newline at end of file
+  else value + ceiling - remainder. *)