From 38ad40784bceba0aec73ac0337e654eab44583c2 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Tue, 11 Jun 2024 15:45:13 +0800 Subject: [PATCH 1/3] Add initial `block.py` --- .../paris/vm/instructions/simulations/block.v | 389 ++++++++++++++++++ 1 file changed, 389 insertions(+) create mode 100644 CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v new file mode 100644 index 0000000..cb67a09 --- /dev/null +++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v @@ -0,0 +1,389 @@ +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. +Module Environment := __init__.Environment. + +Require ethereum.paris.vm.simulations.gas. +Definition GAS_BLOCK_HASH := gas.GAS_BLOCK_HASH. +Definition GAS_BASE := gas.GAS_BASE. +Definition charge_gas := gas.charge_gas. + +Require ethereum.paris.vm.simulations.stack. +Definition pop := stack.pop. +Definition push := stack.push. + +Import simulations.CoqOfPython.Notations. + +(* TODO: +- Address -> Byte20 -> Bytes -> U256 +*) + +(* def block_hash(evm: Evm) -> None: + """ + Push the hash of one of the 256 most recent complete blocks onto the + stack. The block number to hash is present at the top of the stack. + + Parameters + ---------- + evm : + The current EVM frame. + + Raises + ------ + :py:class:`~ethereum.paris.vm.exceptions.StackUnderflowError` + If `len(stack)` is less than `1`. + :py:class:`~ethereum.paris.vm.exceptions.OutOfGasError` + If `evm.gas_left` is less than `20`. + """ + # STACK + block_number = pop(evm.stack) + + # GAS + charge_gas(evm, GAS_BLOCK_HASH) + + # OPERATION + if evm.env.number <= block_number or evm.env.number > block_number + 256: + # Default hash to 0, if the block of interest is not yet on the chain + # (including the block which has the current executing transaction), + # or if the block's age is more than 256. + hash = b"\x00" + else: + hash = evm.env.block_hashes[-(evm.env.number - block_number)] + + push(evm.stack, U256.from_be_bytes(hash)) + + # PROGRAM COUNTER + evm.pc += 1 *) + +Definition block_hash : MS? Evm.t Exception.t unit := + (* STACK *) + letS? block_number := StateError.lift_lens Evm.Lens.stack pop in + (* GAS *) + letS? _ := charge_gas GAS_BLOCK_HASH in + (* OPERATION *) + (* Get the Evm.Rest.env.number *) + letS? evm := readS? in + let '(Evm.Make _ rest) := evm in + let evm_env_number := rest.(Evm.Rest.env).(Environment.number) in + (* Get the Evm.Rest.env.block_hashes *) + let evm_env_block_hashes := rest.(Evm.Rest.env).(Environment.block_hashes) in + + (* Construct correrctly the b"\x00" *) + let b := base_types.FixedBytes.Make [Ascii.ascii_of_N 0] in + let b1 := hash.Bytes32.Make b in + let b_x00 := __init__.Hash32.Make b1 in + + let hash := if (orb (Uint.get evm_env_number <=? U256.to_Z block_number) + (Uint.get evm_env_number >? U256.to_Z block_number + 256)) + then b_x00 (* __init__.Hash32.t *) + else List.nth + (Z.to_nat (-((Uint.get evm_env_number) - (U256.to_Z block_number)))) + evm_env_block_hashes + b_x00 (* Coq's nth function need to provide a default value *) + in + + (* Translate the type of hash from Hash32 to U256? *) + let h := __init__.Hash32.get hash in + let h1 := hash.Bytes32.get h in + let h2 := base_types.Uint.from_bytes h1 in + let h3 := base_types.Uint.get h2 in (* UInt to Z for convenience *) + let hash := U256.of_Z h3 in + + letS? _ := StateError.lift_lens Evm.Lens.stack (push hash) in + (* PROGRAM COUNTER *) + letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc => + (inl tt, Uint.__add__ pc (Uint.Make 1))) in + returnS? tt. + +(* def coinbase(evm: Evm) -> None: + """ + Push the current block's beneficiary address (address of the block miner) + onto the stack. + + Here the current block refers to the block in which the currently + executing transaction/call resides. + + Parameters + ---------- + evm : + The current EVM frame. + + Raises + ------ + :py:class:`~ethereum.paris.vm.exceptions.StackOverflowError` + If `len(stack)` is equal to `1024`. + :py:class:`~ethereum.paris.vm.exceptions.OutOfGasError` + If `evm.gas_left` is less than `2`. + """ + # STACK + pass + + # GAS + charge_gas(evm, GAS_BASE) + + # OPERATION + push(evm.stack, U256.from_be_bytes(evm.env.coinbase)) + + # PROGRAM COUNTER + evm.pc += 1 *) + +Definition coinbase : MS? Evm.t Exception.t unit := + (* GAS *) + letS? _ := charge_gas GAS_BASE in + (* Get evm.env.coinbase *) + letS? evm := readS? in + let '(Evm.Make _ rest) := evm in + (* Convert from Address to -> Byte20 -> Bytes -> U256 *) + let e := rest.(Evm.Rest.env).(Environment.coinbase) in + let e1 := fork_types.Address.get e in + let e2 := base_types.Bytes20.get e1 in + let e3 := base_types.Uint.from_bytes e2 in + let e4 := base_types.Uint.get e3 in + let evm_env_coinbase := U256.of_Z e4 in + + letS? _ := StateError.lift_lens Evm.Lens.stack (push evm_env_coinbase) in + (* PROGRAM COUNTER *) + letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc => + (inl tt, Uint.__add__ pc (Uint.Make 1))) in + returnS? tt. + +(* def timestamp(evm: Evm) -> None: + """ + Push the current block's timestamp onto the stack. Here the timestamp + being referred is actually the unix timestamp in seconds. + + Here the current block refers to the block in which the currently + executing transaction/call resides. + + Parameters + ---------- + evm : + The current EVM frame. + + Raises + ------ + :py:class:`~ethereum.paris.vm.exceptions.StackOverflowError` + If `len(stack)` is equal to `1024`. + :py:class:`~ethereum.paris.vm.exceptions.OutOfGasError` + If `evm.gas_left` is less than `2`. + """ + # STACK + pass + + # GAS + charge_gas(evm, GAS_BASE) + + # OPERATION + push(evm.stack, evm.env.time) + + # PROGRAM COUNTER + evm.pc += 1 *) +Definition timestamp : MS? Evm.t Exception.t unit := + (* GAS *) + letS? _ := charge_gas GAS_BASE in + (* Get evm.env.time *) + letS? evm := readS? in + let '(Evm.Make _ rest) := evm in + let evm_env_time := rest.(Evm.Rest.env).(Environment.time) in + + letS? _ := StateError.lift_lens Evm.Lens.stack (push evm_env_time) in + (* PROGRAM COUNTER *) + letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc => + (inl tt, Uint.__add__ pc (Uint.Make 1))) in + returnS? tt. + +(* def number(evm: Evm) -> None: + """ + Push the current block's number onto the stack. + + Here the current block refers to the block in which the currently + executing transaction/call resides. + + Parameters + ---------- + evm : + The current EVM frame. + + Raises + ------ + :py:class:`~ethereum.paris.vm.exceptions.StackOverflowError` + If `len(stack)` is equal to `1024`. + :py:class:`~ethereum.paris.vm.exceptions.OutOfGasError` + If `evm.gas_left` is less than `2`. + """ + # STACK + pass + + # GAS + charge_gas(evm, GAS_BASE) + + # OPERATION + push(evm.stack, U256(evm.env.number)) + + # PROGRAM COUNTER + evm.pc += 1 *) +Definition number : MS? Evm.t Exception.t unit := + (* GAS *) + letS? _ := charge_gas GAS_BASE in + (* Get evm.env.time *) + letS? evm := readS? in + let '(Evm.Make _ rest) := evm in + let e := rest.(Evm.Rest.env).(Environment.number) in + (* Conversion from Uint to U256 *) + let e1 := base_types.Uint.get e in + let evm_env_number := U256.of_Z e1 in + + letS? _ := StateError.lift_lens Evm.Lens.stack (push evm_env_number) in + (* PROGRAM COUNTER *) + letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc => + (inl tt, Uint.__add__ pc (Uint.Make 1))) in + returnS? tt. + + +(* def prev_randao(evm: Evm) -> None: + """ + Push the `prev_randao` value onto the stack. + + The `prev_randao` value is the random output of the beacon chain's + randomness oracle for the previous block. + + Parameters + ---------- + evm : + The current EVM frame. + + Raises + ------ + :py:class:`~ethereum.paris.vm.exceptions.StackOverflowError` + If `len(stack)` is equal to `1024`. + :py:class:`~ethereum.paris.vm.exceptions.OutOfGasError` + If `evm.gas_left` is less than `2`. + """ + # STACK + pass + + # GAS + charge_gas(evm, GAS_BASE) + + # OPERATION + push(evm.stack, U256.from_be_bytes(evm.env.prev_randao)) + + # PROGRAM COUNTER + evm.pc += 1 *) +Definition prev_randao : MS? Evm.t Exception.t unit := + (* GAS *) + letS? _ := charge_gas GAS_BASE in + (* Get evm.env.prev_randao *) + letS? evm := readS? in + let '(Evm.Make _ rest) := evm in + let e := rest.(Evm.Rest.env).(Environment.prev_randao) in + (* Convert the type from Bytes32 to U256 *) + let e1 := hash.Bytes32.get e in + let e2 := base_types.Uint.from_bytes e1 in + let e3 := base_types.Uint.get e2 in + let evm_env_prev_randao := U256.of_Z e3 in + + letS? _ := StateError.lift_lens Evm.Lens.stack (push evm_env_prev_randao) in + (* PROGRAM COUNTER *) + letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc => + (inl tt, Uint.__add__ pc (Uint.Make 1))) in + returnS? tt. + + +(* def gas_limit(evm: Evm) -> None: + """ + Push the current block's gas limit onto the stack. + + Here the current block refers to the block in which the currently + executing transaction/call resides. + + Parameters + ---------- + evm : + The current EVM frame. + + Raises + ------ + :py:class:`~ethereum.paris.vm.exceptions.StackOverflowError` + If `len(stack)` is equal to `1024`. + :py:class:`~ethereum.paris.vm.exceptions.OutOfGasError` + If `evm.gas_left` is less than `2`. + """ + # STACK + pass + + # GAS + charge_gas(evm, GAS_BASE) + + # OPERATION + push(evm.stack, U256(evm.env.gas_limit)) + + # PROGRAM COUNTER + evm.pc += 1 *) +Definition gas_limit : MS? Evm.t Exception.t unit := + (* GAS *) + letS? _ := charge_gas GAS_BASE in + (* Get evm.env.gas_limit *) + letS? evm := readS? in + let '(Evm.Make _ rest) := evm in + let evm_env_gas_limit := rest.(Evm.Rest.env).(Environment.gas_limit) in + + (* letS? _ := StateError.lift_lens Evm.Lens.stack (push evm_env_gas_limit) in *) + (* PROGRAM COUNTER *) + letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc => + (inl tt, Uint.__add__ pc (Uint.Make 1))) in + returnS? tt. + +(* +def chain_id(evm: Evm) -> None: + """ + Push the chain id onto the stack. + + Parameters + ---------- + evm : + The current EVM frame. + + Raises + ------ + :py:class:`~ethereum.paris.vm.exceptions.StackOverflowError` + If `len(stack)` is equal to `1024`. + :py:class:`~ethereum.paris.vm.exceptions.OutOfGasError` + If `evm.gas_left` is less than `2`. + """ + # STACK + pass + + # GAS + charge_gas(evm, GAS_BASE) + + # OPERATION + push(evm.stack, U256(evm.env.chain_id)) + + # PROGRAM COUNTER + evm.pc += 1 *) +Definition chain_id : MS? Evm.t Exception.t unit := + (* GAS *) + letS? _ := charge_gas GAS_BASE in + (* Get evm.env.gas_limit *) + letS? evm := readS? in + let '(Evm.Make _ rest) := evm in + (* Convert from U64 to U256 *) + let e := rest.(Evm.Rest.env).(Environment.chain_id) in + let '(base_types.U64.Make e1) := e in + let evm_env_chain_id := base_types.U256.Make e1 in + + letS? _ := StateError.lift_lens Evm.Lens.stack (push evm_env_chain_id) 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 From 2a8fa02751b0d5706257c71a09ff3f7f5b5fa663 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Tue, 11 Jun 2024 15:52:08 +0800 Subject: [PATCH 2/3] Update rest of the files --- CoqOfPython/ethereum/simulations/base_types.v | 75 ++++++++++++++++--- CoqOfPython/simulations/proofs/heap.v | 3 + 2 files changed, 68 insertions(+), 10 deletions(-) diff --git a/CoqOfPython/ethereum/simulations/base_types.v b/CoqOfPython/ethereum/simulations/base_types.v index 6659b0a..478afd6 100644 --- a/CoqOfPython/ethereum/simulations/base_types.v +++ b/CoqOfPython/ethereum/simulations/base_types.v @@ -10,7 +10,27 @@ Definition U255_CEIL_VALUE : Z := 2^255. Definition U256_CEIL_VALUE : Z := 2^256. +(* NOTE: A byte should consist of 2 hex digits or 4 binary digits + https://docs.python.org/3/library/stdtypes.html#bytes *) +Module FixedBytes. + Inductive t : Set := + | Make (bytes : list ascii). + (* NOTE: some draft that might be useful for future extension + Inductive ByteOrder := + | LittleEndian + | BigEndian + *) + (* Make (bytes: list ascii) (signed : bool) (byte_order : ByteOrder) *) + + Definition get (bytes : t) : list ascii := + match bytes with + | Make bytes => bytes + end. +End FixedBytes. + Module Uint. +(* NOTE: to_bytes would produce a list of byte with *undetermined* length +*) Inductive t : Set := | Make (value : Z). @@ -21,6 +41,49 @@ 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` *) + (* + def from_bytes(bytes, byteorder='big', signed=False): + if byteorder == 'little': + little_ordered = list(bytes) + elif byteorder == 'big': + little_ordered = list(reversed(bytes)) + else: + raise ValueError("byteorder must be either 'little' or 'big'") + + n = sum(b << i*8 for i, b in enumerate(little_ordered)) + if signed and little_ordered and (little_ordered[-1] & 0x80): + n -= 1 << 8*len(little_ordered) + + 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 + | (b::bs) => from_bytes_helper bs ((Z_of_N (N_of_ascii b)) * 8 + store) + end. + + 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 *) + 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 + Make ( + if ascii_xor_result =? 0 + then result - Z.shiftl 1 (Z_of_nat (List.length little_ordered)) + else result). End Uint. Module FixedUint. @@ -219,16 +282,6 @@ Module U64. end. End U64. -Module FixedBytes. - Inductive t : Set := - | Make (bytes : list ascii). - - Definition get (bytes : t) : list ascii := - match bytes with - | Make bytes => bytes - end. -End FixedBytes. - Module Bytes0. Inductive t : Set := | Make (bytes : FixedBytes.t). @@ -277,6 +330,8 @@ Module Bytes32. match bytes with | Make bytes => bytes end. + + Definition LENGTH := 32. End Bytes32. Module Bytes48. diff --git a/CoqOfPython/simulations/proofs/heap.v b/CoqOfPython/simulations/proofs/heap.v index 1df0da6..847dffa 100644 --- a/CoqOfPython/simulations/proofs/heap.v +++ b/CoqOfPython/simulations/proofs/heap.v @@ -9,6 +9,7 @@ Module U256 := base_types.U256. Require ethereum.paris.vm.simulations.__init__. Module Evm := __init__.Evm. +Module Environment := __init__.Environment. Module Address. Inductive t : Set := @@ -21,6 +22,7 @@ Module Heap. Record t : Set := { pc : Uint.t; gas_left : Uint.t; + env : Environment.t; }. End Evm. @@ -69,5 +71,6 @@ Module Heap. __init__.Evm.Rest.pc := heap.(evm).(Evm.pc); __init__.Evm.Rest.stack := heap.(stack); __init__.Evm.Rest.gas_left := heap.(evm).(Evm.gas_left); + __init__.Evm.Rest.env := heap.(evm).(Evm.env); |}. End Heap. From 6120e1fa2aa3b5f02eaa6957a972440fcc62275a Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Wed, 12 Jun 2024 15:33:23 +0800 Subject: [PATCH 3/3] Update `block.v` --- .../paris/vm/instructions/simulations/block.v | 48 +++++++++---------- 1 file changed, 22 insertions(+), 26 deletions(-) diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v index cb67a09..0d38488 100644 --- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v +++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/block.v @@ -23,10 +23,6 @@ Definition push := stack.push. Import simulations.CoqOfPython.Notations. -(* TODO: -- Address -> Byte20 -> Bytes -> U256 -*) - (* def block_hash(evm: Evm) -> None: """ Push the hash of one of the 256 most recent complete blocks onto the @@ -92,11 +88,11 @@ Definition block_hash : MS? Evm.t Exception.t unit := in (* Translate the type of hash from Hash32 to U256? *) - let h := __init__.Hash32.get hash in - let h1 := hash.Bytes32.get h in - let h2 := base_types.Uint.from_bytes h1 in - let h3 := base_types.Uint.get h2 in (* UInt to Z for convenience *) - let hash := U256.of_Z h3 in + let hash := __init__.Hash32.get hash in + let hash := hash.Bytes32.get hash in + let hash := base_types.Uint.from_bytes hash in + let hash := base_types.Uint.get hash in (* UInt to Z for convenience *) + let hash := U256.of_Z hash in letS? _ := StateError.lift_lens Evm.Lens.stack (push hash) in (* PROGRAM COUNTER *) @@ -143,12 +139,12 @@ Definition coinbase : MS? Evm.t Exception.t unit := letS? evm := readS? in let '(Evm.Make _ rest) := evm in (* Convert from Address to -> Byte20 -> Bytes -> U256 *) - let e := rest.(Evm.Rest.env).(Environment.coinbase) in - let e1 := fork_types.Address.get e in - let e2 := base_types.Bytes20.get e1 in - let e3 := base_types.Uint.from_bytes e2 in - let e4 := base_types.Uint.get e3 in - let evm_env_coinbase := U256.of_Z e4 in + let evm_env_coinbase := rest.(Evm.Rest.env).(Environment.coinbase) in + let evm_env_coinbase := fork_types.Address.get evm_env_coinbase in + let evm_env_coinbase := base_types.Bytes20.get evm_env_coinbase in + let evm_env_coinbase := base_types.Uint.from_bytes evm_env_coinbase in + let evm_env_coinbase := base_types.Uint.get evm_env_coinbase in + let evm_env_coinbase := U256.of_Z evm_env_coinbase in letS? _ := StateError.lift_lens Evm.Lens.stack (push evm_env_coinbase) in (* PROGRAM COUNTER *) @@ -237,10 +233,10 @@ Definition number : MS? Evm.t Exception.t unit := (* Get evm.env.time *) letS? evm := readS? in let '(Evm.Make _ rest) := evm in - let e := rest.(Evm.Rest.env).(Environment.number) in + let evm_env_number := rest.(Evm.Rest.env).(Environment.number) in (* Conversion from Uint to U256 *) - let e1 := base_types.Uint.get e in - let evm_env_number := U256.of_Z e1 in + let evm_env_number := base_types.Uint.get evm_env_number in + let evm_env_number := U256.of_Z evm_env_number in letS? _ := StateError.lift_lens Evm.Lens.stack (push evm_env_number) in (* PROGRAM COUNTER *) @@ -285,12 +281,12 @@ Definition prev_randao : MS? Evm.t Exception.t unit := (* Get evm.env.prev_randao *) letS? evm := readS? in let '(Evm.Make _ rest) := evm in - let e := rest.(Evm.Rest.env).(Environment.prev_randao) in + let evm_env_prev_randao := rest.(Evm.Rest.env).(Environment.prev_randao) in (* Convert the type from Bytes32 to U256 *) - let e1 := hash.Bytes32.get e in - let e2 := base_types.Uint.from_bytes e1 in - let e3 := base_types.Uint.get e2 in - let evm_env_prev_randao := U256.of_Z e3 in + let evm_env_prev_randao := hash.Bytes32.get evm_env_prev_randao in + let evm_env_prev_randao := base_types.Uint.from_bytes evm_env_prev_randao in + let evm_env_prev_randao := base_types.Uint.get evm_env_prev_randao in + let evm_env_prev_randao := U256.of_Z evm_env_prev_randao in letS? _ := StateError.lift_lens Evm.Lens.stack (push evm_env_prev_randao) in (* PROGRAM COUNTER *) @@ -378,9 +374,9 @@ Definition chain_id : MS? Evm.t Exception.t unit := letS? evm := readS? in let '(Evm.Make _ rest) := evm in (* Convert from U64 to U256 *) - let e := rest.(Evm.Rest.env).(Environment.chain_id) in - let '(base_types.U64.Make e1) := e in - let evm_env_chain_id := base_types.U256.Make e1 in + let evm_env_chain_id := rest.(Evm.Rest.env).(Environment.chain_id) in + let '(base_types.U64.Make evm_env_chain_id) := evm_env_chain_id in + let evm_env_chain_id := base_types.U256.Make evm_env_chain_id in letS? _ := StateError.lift_lens Evm.Lens.stack (push evm_env_chain_id) in (* PROGRAM COUNTER *)