Skip to content

Add bit_wise function simulations #27

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
May 24, 2024
Merged

Add bit_wise function simulations #27

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
aadfc0e
draft update
InfiniteEchoes May 23, 2024
5cce685
Merge branch 'main' into gy@AddBitSimulations
InfiniteEchoes May 23, 2024
4edc1ab
Add aux functions & `base_type` simulation
InfiniteEchoes May 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
314 changes: 309 additions & 5 deletions CoqOfPython/ethereum/paris/vm/instructions/simulations/bitwise.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,12 +24,45 @@ Definition pop := stack.pop.
Definition push := stack.push.

Import simulations.CoqOfPython.Notations.

(*
def bitwise_and(evm: Evm) -> None:
"""
Bitwise AND operation of the top 2 elements of the stack. Pushes the
result back on the stack.
Parameters
----------
evm :
The current EVM frame.
"""
# STACK
x = pop(evm.stack)
y = pop(evm.stack)
# GAS
charge_gas(evm, GAS_VERY_LOW)
# OPERATION
push(evm.stack, x & y)
# PROGRAM COUNTER
evm.pc += 1
*)
Definition bitwise_and : MS? Evm.t Exception.t unit :=
(* STACK *)
letS? x := StateError.lift_lens Evm.Lens.stack pop in
letS? y := StateError.lift_lens Evm.Lens.stack pop in
(* GAS *)
letS? _ := charge_gas GAS_VERY_LOW in
(* OPERATION *)
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.

(*
def bitwise_or(evm: Evm) -> None:
"""
Bitwise OR operation of the top 2 elements of the stack. Pushes the
result back on the stack.

Parameters
----------
Expand All @@ -45,21 +78,292 @@ def bitwise_and(evm: Evm) -> None:
charge_gas(evm, GAS_VERY_LOW)

# OPERATION
push(evm.stack, x & y)
push(evm.stack, x | y)

# PROGRAM COUNTER
evm.pc += 1
*)
Definition bitwise_and : MS? Evm.t Exception.t unit :=
Definition bitwise_or : MS? Evm.t Exception.t unit :=
(* STACK *)
letS? x := StateError.lift_lens Evm.Lens.stack pop in
letS? y := StateError.lift_lens Evm.Lens.stack pop in
(* GAS *)
letS? _ := charge_gas GAS_VERY_LOW in
(* OPERATION *)
letS? _ := StateError.lift_lens Evm.Lens.stack (
push (U256.bit_or 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.

(*
def bitwise_xor(evm: Evm) -> None:
"""
Bitwise XOR operation of the top 2 elements of the stack. Pushes the
result back on the stack.

Parameters
----------
evm :
The current EVM frame.

"""
# STACK
x = pop(evm.stack)
y = pop(evm.stack)

# GAS
charge_gas(evm, GAS_VERY_LOW)

# OPERATION
push(evm.stack, x ^ y)

# PROGRAM COUNTER
evm.pc += 1
*)
Definition bitwise_xor : MS? Evm.t Exception.t unit :=
(* STACK *)
letS? x := StateError.lift_lens Evm.Lens.stack pop in
letS? y := StateError.lift_lens Evm.Lens.stack pop in
(* GAS *)
letS? _ := charge_gas GAS_VERY_LOW in
(* OPERATION *)
letS? _ := StateError.lift_lens Evm.Lens.stack (
push (U256.wrapping_add x y)) in
push (U256.bit_xor 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.

(*
def bitwise_not(evm: Evm) -> None:
"""
Bitwise NOT operation of the top element of the stack. Pushes the
result back on the stack.

Parameters
----------
evm :
The current EVM frame.

"""
# STACK
x = pop(evm.stack)

# GAS
charge_gas(evm, GAS_VERY_LOW)

# OPERATION
push(evm.stack, ~x)

# PROGRAM COUNTER
evm.pc += 1
*)
Definition bitwise_not : MS? Evm.t Exception.t unit :=
(* STACK *)
letS? x := StateError.lift_lens Evm.Lens.stack pop in
(* GAS *)
letS? _ := charge_gas GAS_VERY_LOW in
(* OPERATION *)
letS? _ := StateError.lift_lens Evm.Lens.stack (
push (U256.bit_not x)) in
(* PROGRAM COUNTER *)
letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
(inl tt, Uint.__add__ pc (Uint.Make 1))) in
returnS? tt.

(*
def get_byte(evm: Evm) -> None:
"""
For a word (defined by next top element of the stack), retrieve the
Nth byte (0-indexed and defined by top element of stack) from the
left (most significant) to right (least significant).

Parameters
----------
evm :
The current EVM frame.

"""
# STACK
byte_index = pop(evm.stack)
word = pop(evm.stack)

# GAS
charge_gas(evm, GAS_VERY_LOW)

# OPERATION
if byte_index >= 32:
result = U256(0)
else:
extra_bytes_to_right = 31 - byte_index
# Remove the extra bytes in the right
word = word >> (extra_bytes_to_right * 8)
# Remove the extra bytes in the left
word = word & 0xFF
result = U256(word)

push(evm.stack, result)

# PROGRAM COUNTER
evm.pc += 1
*)
Definition get_byte : MS? Evm.t Exception.t unit :=
(* STACK *)
letS? byte_index := StateError.lift_lens Evm.Lens.stack pop in
letS? word := StateError.lift_lens Evm.Lens.stack pop in
(* GAS *)
letS? _ := charge_gas GAS_VERY_LOW in
(* OPERATION *)
let result :=
if ((U256.to_Z byte_index)>=? 32)
then (U256.of_Z 0)
else(
let extra_bytes_to_right := 31 - (U256.to_Z byte_index)%Z in
let word := (Z.shiftr (U256.to_Z word) (extra_bytes_to_right * 8)) in
let word := Z.land word (0XFF%Z) in
(U256.of_Z word)
)
in
letS? _ := StateError.lift_lens Evm.Lens.stack (
push result) in
(* PROGRAM COUNTER *)
letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
(inl tt, Uint.__add__ pc (Uint.Make 1))) in
returnS? tt.

(* def bitwise_shl(evm: Evm) -> None:
"""
Logical shift left (SHL) operation of the top 2 elements of the stack.
Pushes the result back on the stack.
Parameters
----------
evm :
The current EVM frame.
"""
# STACK
shift = pop(evm.stack)
value = pop(evm.stack)

# GAS
charge_gas(evm, GAS_VERY_LOW)

# OPERATION
if shift < 256:
result = U256((value << shift) % U256_CEIL_VALUE)
else:
result = U256(0)

push(evm.stack, result)

# PROGRAM COUNTER
evm.pc += 1 *)
Definition bitwise_shl : MS? Evm.t Exception.t unit :=
(* STACK *)
letS? shift := StateError.lift_lens Evm.Lens.stack pop in
letS? value := StateError.lift_lens Evm.Lens.stack pop in
(* GAS *)
letS? _ := charge_gas GAS_VERY_LOW in
(* OPERATION *)
let result :=
if (U256.to_Z shift) <? 256
then (U256.of_Z (Z.shiftr (U256.to_Z value) (U256.to_Z shift)))
else (U256.of_Z 0) in
letS? _ := StateError.lift_lens Evm.Lens.stack (push result) in
(* PROGRAM COUNTER *)
letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
(inl tt, Uint.__add__ pc (Uint.Make 1))) in
returnS? tt.

(* def bitwise_shr(evm: Evm) -> None:
"""
Logical shift right (SHR) operation of the top 2 elements of the stack.
Pushes the result back on the stack.
Parameters
----------
evm :
The current EVM frame.
"""
# STACK
shift = pop(evm.stack)
value = pop(evm.stack)

# GAS
charge_gas(evm, GAS_VERY_LOW)

# OPERATION
if shift < 256:
result = value >> shift
else:
result = U256(0)

push(evm.stack, result)

# PROGRAM COUNTER
evm.pc += 1 *)
Definition bitwise_shr : MS? Evm.t Exception.t unit :=
(* STACK *)
letS? shift := StateError.lift_lens Evm.Lens.stack pop in
letS? value := StateError.lift_lens Evm.Lens.stack pop in
(* GAS *)
letS? _ := charge_gas GAS_VERY_LOW in
(* OPERATION *)
let result :=
if (U256.to_Z shift) <? 256
then (U256.of_Z (Z.shiftr (U256.to_Z value) (U256.to_Z shift)))
else (U256.of_Z 0) in
letS? _ := StateError.lift_lens Evm.Lens.stack (push result) in
(* PROGRAM COUNTER *)
letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
(inl tt, Uint.__add__ pc (Uint.Make 1))) in
returnS? tt.

(*
def bitwise_sar(evm: Evm) -> None:
"""
Arithmetic shift right (SAR) operation of the top 2 elements of the stack.
Pushes the result back on the stack.
Parameters
----------
evm :
The current EVM frame.
"""
# STACK
shift = pop(evm.stack)
signed_value = pop(evm.stack).to_signed()

# GAS
charge_gas(evm, GAS_VERY_LOW)

# OPERATION
if shift < 256:
result = U256.from_signed(signed_value >> shift)
elif signed_value >= 0:
result = U256(0)
else:
result = U256.MAX_VALUE

push(evm.stack, result)

# PROGRAM COUNTER
evm.pc += 1 *)
Definition bitwise_sar : MS? Evm.t Exception.t unit :=
(* STACK *)
letS? shift := StateError.lift_lens Evm.Lens.stack pop in
letS? signed_value := StateError.lift_lens Evm.Lens.stack pop in
(* GAS *)
letS? _ := charge_gas GAS_VERY_LOW in
(* OPERATION *)
let result :=
if (U256.to_Z shift) <? 256
then (U256.from_signed (U256.of_Z (Z.shiftr (U256.to_Z signed_value) (U256.to_Z shift))))
else (
if (U256.to_Z signed_value >=? 0)
then (U256.of_Z 0)
else U256.MAX_VALUE) in
letS? _ := StateError.lift_lens Evm.Lens.stack (push result) in
(* PROGRAM COUNTER *)
letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>
(inl tt, Uint.__add__ pc (Uint.Make 1))) in
returnS? tt.
returnS? tt.
Loading
Loading