Draft: Arithmetic Operations

CoqOfPython/blacklist.txt

@@ -1 +1,8 @@
 ethereum/ethash.v
+ethereum/paris/vm/instructions/proofs/arithmetic.v
+ethereum/paris/vm/simulations/proofs/__init__.v
+ethereum/paris/vm/simulations/proofs/exceptions.v
+ethereum/paris/vm/simulations/proofs/stack.v
+ethereum/simulations/proofs/exceptions.v
+simulations/proofs/builtins.v
+simulations/proofs/heap.v

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

@@ -2,6 +2,7 @@ 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.
@@ -25,7 +26,108 @@ Definition push := stack.push.
 
 Import simulations.CoqOfPython.Notations.
 
+(* For sanity checks *)
+Axiom environment : __init__.Environment.t.
+Axiom message : __init__.Message.t Evm.t.
+
+Definition empty_evm : Evm.t :=
+  Evm.Make message {|
+    Evm.Rest.pc := Uint.Make 0;
+    Evm.Rest.stack := [];
+    Evm.Rest.memory := [];
+    Evm.Rest.code := __init__.Bytes.Make [];
+    Evm.Rest.gas_left := Uint.Make 0;
+    Evm.Rest.env := environment;
+    Evm.Rest.valid_jump_destinations := [];
+    Evm.Rest.logs := [];
+    Evm.Rest.refund_counter := 0;
+    Evm.Rest.running := true;
+    Evm.Rest.output := __init__.Bytes.Make [];
+    Evm.Rest.accounts_to_delete := [];
+    Evm.Rest.touched_accounts := [];
+    Evm.Rest.return_data := __init__.Bytes.Make [];
+    Evm.Rest.error := None;
+    Evm.Rest.accessed_addresses := [];
+    Evm.Rest.accessed_storage_keys := [];
+  |}.
+
+Definition evm_with_gas : Evm.t :=
+  Evm.Lens.gas_left.(Lens.write) empty_evm GAS_VERY_LOW.
+
+Definition evm_with_stack : Evm.t :=
+  Evm.Lens.stack.(Lens.write) evm_with_gas [
+    U256.of_Z 23;
+    U256.of_Z 3;
+    U256.of_Z 5
+  ].
+
+Definition wrapped_binary_operation wrapped_operation gas_charge : 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_charge in
+
+  (* OPERATION *)
+  let result := wrapped_operation 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.
+
 Definition add : MS? Evm.t Exception.t unit :=
+  wrapped_binary_operation U256.wrapping_add GAS_VERY_LOW.
+
+(* Compute add evm_with_stack. *)
+
+Definition sub : MS? Evm.t Exception.t unit :=
+  wrapped_binary_operation U256.wrapping_sub GAS_VERY_LOW.
+
+(* Compute sub evm_with_stack. *)
+
+Definition mul : MS? Evm.t Exception.t unit :=
+  wrapped_binary_operation U256.wrapping_mul GAS_VERY_LOW.
+
+(* Compute mul evm_with_stack. *)
+
+Definition div : MS? Evm.t Exception.t unit :=
+  (* STACK *)
+  letS? divisor := StateError.lift_lens Evm.Lens.stack pop in
+  letS? divident := StateError.lift_lens Evm.Lens.stack pop in
+
+  (* GAS *)
+  letS? _ := charge_gas GAS_VERY_LOW in
+
+  (* OPERATION *)
+
+  let division := 
+    match (U256.to_Z divident) with
+    | 0 =>
+      U256.of_Z 0
+    | _ =>
+      U256.of_Z ((U256.to_Z divisor) / (U256.to_Z divident))
+  end in
+
+  let result := division 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.
+
+(* Compute div evm_with_stack. *)
+
+(* Name collides with Coq's mod. *)
+
+Definition modulo : 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
@@ -34,12 +136,121 @@ Definition add : MS? Evm.t Exception.t unit :=
   letS? _ := charge_gas GAS_VERY_LOW in
 
   (* OPERATION *)
-  let result := U256.wrapping_add x y in
 
+  let modular y := 
+    match (U256.to_Z y) with
+    | 0 =>
+      U256.of_Z 0
+    | _ =>
+        U256.of_Z ((U256.to_Z x) mod (U256.to_Z y))
+  end
+  in
+
+  let result := modular 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.
+
+(* Compute modulo evm_with_stack. *)
+
+Definition add_mod : 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
+  letS? z := StateError.lift_lens Evm.Lens.stack pop in
+
+  (* GAS *)
+  letS? _ := charge_gas GAS_MID in
+
+  (* OPERATION *)
+
+  let addition_modular y := 
+  match (U256.to_Z y) with
+  | 0 =>
+    U256.of_Z 0
+  | _ =>
+      U256.of_Z (((U256.to_Z x) + (U256.to_Z y)) mod (U256.to_Z z))
+  end
+  in
+
+  let result := addition_modular 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.
+
+(* Compute add_mod evm_with_stack. *)
+
+Definition mul_mod : 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
+  letS? z := StateError.lift_lens Evm.Lens.stack pop in
+
+  (* GAS *)
+  letS? _ := charge_gas GAS_MID in
+
+  (* OPERATION *)
+
+  let multiplication_modular y := 
+    match (U256.to_Z y) with
+    | 0 =>
+      U256.of_Z 0
+    | _ =>
+      U256.of_Z (((U256.to_Z x) * (U256.to_Z y)) mod (U256.to_Z z))
+  end
+  in
+
+  let result := multiplication_modular 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.
+
+
+(* Compute mul_mod evm_with_stack. *)
+
+(* "This is equivalent to 1 + floor(log(y, 256))" *)
+
+Definition byte_length n :=
+  1 + Z.log2(n) / 8.
+
+Definition exp : MS? Evm.t Exception.t unit :=
+  (* STACK *)
+  letS? base := StateError.lift_lens Evm.Lens.stack pop in
+  letS? exponent := StateError.lift_lens Evm.Lens.stack pop in
+
+  let exponent_bytes := byte_length (U256.to_Z exponent) in
+  (* GAS *)
+  letS? _ := charge_gas (gas.Uint.Make 
+                           ((gas.Uint.get GAS_EXPONENTIATION)
+                          + (gas.Uint.get GAS_EXPONENTIATION_PER_BYTE)
+                          * exponent_bytes)) in 
+
+  (* OPERATION *)
+
+  let result := U256.of_Z ((Z.pow (U256.to_Z base) (U256.to_Z exponent)) mod U256_CEIL_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.
+
+(* Compute exp evm_with_stack. *)

CoqOfPython/ethereum/paris/vm/simulations/__init__.v

@@ -64,10 +64,10 @@ Module Evm.
     Record t : Set := {
       pc : Uint.t;
       stack : list (U256.t);
-      (* memory : list ascii;
-      code : Bytes.t; *)
+      memory : list ascii;
+      code : Bytes.t;
       gas_left : Uint.t;
-      (* env : Environment.t;
+      env : Environment.t;
       valid_jump_destinations : list Uint.t;
       logs : list unit;
       refund_counter : Z;
@@ -78,7 +78,7 @@ Module Evm.
       return_data : Bytes.t;
       error : option Exception.t;
       accessed_addresses : list Address.t;
-      accessed_storage_keys : list (Address.t * Bytes32.t) *)
+      accessed_storage_keys : list (Address.t * Bytes32.t)
     }.
   End Rest.
 
@@ -101,15 +101,15 @@ Module Evm.
       Lens.write '(Make message rest) stack := Make message rest<|Rest.stack := stack|>;
     |}.
 
-    (* Definition memory : Lens.t t (list ascii) := {|
+    Definition memory : Lens.t t (list ascii) := {|
       Lens.read '(Make _ rest) := rest.(Rest.memory);
       Lens.write '(Make message rest) memory := Make message rest<|Rest.memory := memory|>;
     |}.
 
     Definition code : Lens.t t Bytes.t := {|
       Lens.read '(Make _ rest) := rest.(Rest.code);
       Lens.write '(Make message rest) code := Make message rest<|Rest.code := code|>;
-    |}. *)
+    |}.
 
     Definition gas_left : Lens.t t Uint.t := {|
       Lens.read '(Make _ rest) := rest.(Rest.gas_left);

CoqOfPython/ethereum/simulations/base_types.v

@@ -45,6 +45,40 @@ Module FixedUint.
       MAX_VALUE := self.(MAX_VALUE);
       value := Z.modulo sum self.(MAX_VALUE);
     |}.
+
+  Definition __sub__ (self right_ : t) : M? Exception.t t :=
+    let result := (self.(value) - right_.(value))%Z in
+    if result >? self.(MAX_VALUE) then
+      Error.raise (Exception.ArithmeticError ArithmeticError.OverflowError)
+    else
+      return? {|
+        MAX_VALUE := self.(MAX_VALUE);
+        value := result;
+      |}.
+
+  Definition wrapping_sub (self right_ : t) : t :=
+    let sub := (self.(value) - right_.(value))%Z in
+    {|
+      MAX_VALUE := self.(MAX_VALUE);
+      value := Z.modulo sub self.(MAX_VALUE);
+    |}.
+
+  Definition __mul__ (self right_ : t) : M? Exception.t t :=
+    let result := (self.(value) * right_.(value))%Z in
+    if result >? self.(MAX_VALUE) then
+      Error.raise (Exception.ArithmeticError ArithmeticError.OverflowError)
+    else
+      return? {|
+        MAX_VALUE := self.(MAX_VALUE);
+        value := result;
+      |}.
+
+  Definition wrapping_mul (self right_ : t) : t :=
+    let mul := (self.(value) * right_.(value))%Z in
+    {|
+      MAX_VALUE := self.(MAX_VALUE);
+      value := Z.modulo mul self.(MAX_VALUE);
+    |}.
 
   Definition bit_and (self right_ : t) : t :=
     let x := self.(value)%Z in
@@ -95,6 +129,9 @@ Module U256.
   Definition to_Z (value : t) : Z :=
     FixedUint.value (get value).
 
+  Definition to_value (value : t) : Value.t :=
+    Value.Make globals "U256" (Pointer.Imm (Object.wrapper (Data.Integer (to_Z value)))).
+
   Definition MAX_VALUE : t := U256.of_Z (2^256 - 1).
 
   Definition __add__ (self right_ : t) : M? Exception.t t :=
@@ -104,6 +141,20 @@ Module U256.
   Definition wrapping_add (self right_ : t) : t :=
     Make (FixedUint.wrapping_add (get self) (get right_)).
 
+  Definition __sub__ (self right_ : t) : M? Exception.t t :=
+    let? result := FixedUint.__sub__ (get self) (get right_) in
+    return? (Make result).
+
+  Definition wrapping_sub (self right_ : t) : t :=
+    Make (FixedUint.wrapping_sub (get self) (get right_)).
+
+  Definition __mul__ (self right_ : t) : M? Exception.t t :=
+    let? result := FixedUint.__mul__ (get self) (get right_) in
+    return? (Make result).
+
+  Definition wrapping_mul (self right_ : t) : t :=
+    Make (FixedUint.wrapping_mul (get self) (get right_)).
+
   Definition bit_and (self right_ : t) : t :=
     Make (FixedUint.bit_and (get self) (get right_)).