Add bitwise_and simulation

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

@@ -0,0 +1,65 @@
+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.
+
+Require ethereum.paris.vm.simulations.gas.
+Definition GAS_EXPONENTIATION := gas.GAS_EXPONENTIATION.
+Definition GAS_EXPONENTIATION_PER_BYTE := gas.GAS_EXPONENTIATION_PER_BYTE.
+Definition GAS_LOW := gas.GAS_LOW.
+Definition GAS_MID := gas.GAS_MID.
+Definition GAS_VERY_LOW := gas.GAS_VERY_LOW.
+Definition charge_gas := gas.charge_gas.
+
+Require ethereum.paris.vm.simulations.stack.
+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.wrapping_add 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.

CoqOfPython/ethereum/simulations/base_types.v

@@ -45,6 +45,15 @@ Module FixedUint.
       MAX_VALUE := self.(MAX_VALUE);
       value := Z.modulo sum self.(MAX_VALUE);
     |}.
+
+  Definition bit_and (self right_ : t) : t :=
+    let x := self.(value)%Z in
+    let y := right_.(value)%Z in
+    {|
+      MAX_VALUE := self.(MAX_VALUE);
+      value := Z.land x y;
+    |}.
+
 End FixedUint.
 
 Module U256.
@@ -70,6 +79,9 @@ Module U256.
 
   Definition wrapping_add (self right_ : t) : t :=
     Make (FixedUint.wrapping_add (get self) (get right_)).
+
+  Definition bit_and (self right_ : t) : t :=
+    Make (FixedUint.bit_and (get self) (get right_)).
 End U256.
 
 Module U32.