Merge pull request #30 from formal-land/draft@AddKeccak

Add `keccak.py` simulation

CoqOfPython/ethereum/paris/simulations/fork_types.v

@@ -1,6 +1,7 @@
 Require Import CoqOfPython.CoqOfPython.
 Require ethereum.simulations.base_types.
 
+
 Module Address.
   Inductive t : Set :=
   | Make (address : base_types.Bytes20.t).

CoqOfPython/ethereum/paris/vm/instructions/simulations/keccak.v

@@ -0,0 +1,109 @@
+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.
+Module FixedBytes := base_types.FixedBytes.
+
+Definition bytearray := base_types.bytearray.
+
+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 ExtendMemory := gas.ExtendMemory.t.
+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.
+
+Require ethereum.utils.simulations.numeric.
+Definition ceil32 := numeric.ceil32.
+
+Import simulations.CoqOfPython.Notations.
+
+Definition keccak256 (bytes : bytearray) : 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`. *)
+Definition memory_read_bytes (memory : bytearray) (start_position size : U256.t) : bytearray.
+Admitted.
+(* 
+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 *)
+  (* 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 ((memory_start_index, size) :: []) in
+
+  letS? _ := charge_gas (Uint.Make ((Uint.get GAS_KECCAK256) + (Uint.get word_gas_cost) + (Uint.get extend_memory.(gas.ExtendMemory.cost)))) in
+  (* OPERATION *)
+  (* 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
+
+  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.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
+  returnS? tt.

CoqOfPython/ethereum/paris/vm/simulations/gas.v

@@ -52,4 +52,35 @@ 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.
+
+(* 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.
+
+(* 
+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 : bytearray) (extensions : list (U256.t * U256.t)), ExtendMemory.t.

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.

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.
+
 (* 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 +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
 *)
@@ -173,6 +181,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.
@@ -248,6 +259,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.
@@ -280,6 +294,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 Bytes0.

CoqOfPython/ethereum/utils/simulations/numeric.v

@@ -0,0 +1,41 @@
+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.
+
+    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 *)
+
+(* TODO: Finish below *)
+Definition ceil32 (value : Uint.t) : Uint.t. Admitted.
+ (* :=
+  let ceiling := Uint.Make 32 in
+  let remainder := value % ceiling in
+  if remainder =? Uint 0
+  then value
+  else value + ceiling - remainder. *)