Skip to content

Commit

Permalink
Remove comments
Browse files Browse the repository at this point in the history
  • Loading branch information
InfiniteEchoes authored and clarus committed May 23, 2024
1 parent e29f5d2 commit 7966321
Showing 1 changed file with 0 additions and 63 deletions.
63 changes: 0 additions & 63 deletions CoqOfPython/ethereum/paris/vm/instructions/simulations/bitwise.v
Original file line number Diff line number Diff line change
Expand Up @@ -25,55 +25,6 @@ Definition push := stack.push.

Import simulations.CoqOfPython.Notations.

(*
def add(evm: Evm) -> None:
"""
Adds the top two elements of the stack together, and 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
result = x.wrapping_add(y)
push(evm.stack, result)
# PROGRAM COUNTER
evm.pc += 1
*)

(*
Definition add : 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 *)
let result := U256.wrapping_add x y 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_and(evm: Evm) -> None:
"""
Expand All @@ -99,20 +50,6 @@ def bitwise_and(evm: Evm) -> None:
# PROGRAM COUNTER
evm.pc += 1
*)
Print pop. (* MS? (list stack.U256.t) Exception.t stack.U256.t *)
Print push. (* stack.U256.t -> MS? (list stack.U256.t) Exception.t unit *)
Definition test1 := StateError.lift_lens Evm.Lens.stack pop.
Print test1. (* MS? Evm.t Exception.t stack.U256.t *)

Definition test2 :=
letS? x := StateError.lift_lens Evm.Lens.stack pop in
letS? y := StateError.lift_lens Evm.Lens.stack pop in
returnS? (U256.to_Z x).

Print test2.

Definition test3 := Z.land 2 3.

Definition bitwise_and : MS? Evm.t Exception.t unit :=
(* STACK *)
letS? x := StateError.lift_lens Evm.Lens.stack pop in
Expand Down

0 comments on commit 7966321

Please sign in to comment.