diff --git a/CoqOfPython/ethereum/paris/simulations/fork_types.v b/CoqOfPython/ethereum/paris/simulations/fork_types.v index 1efcb6c..b345aac 100644 --- a/CoqOfPython/ethereum/paris/simulations/fork_types.v +++ b/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). 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..304b848 --- /dev/null +++ b/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. diff --git a/CoqOfPython/ethereum/paris/vm/simulations/gas.v b/CoqOfPython/ethereum/paris/vm/simulations/gas.v index 7cfb7ce..da4a375 100644 --- a/CoqOfPython/ethereum/paris/vm/simulations/gas.v +++ b/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. 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. diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v index 478afd6..26e7568 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. + (* 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. diff --git a/CoqOfPython/ethereum/utils/simulations/numeric.v b/CoqOfPython/ethereum/utils/simulations/numeric.v new file mode 100644 index 0000000..aa64640 --- /dev/null +++ b/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. *)