proofs: add executable run statement

CoqOfPython/CoqOfPython.v

@@ -146,6 +146,12 @@ Module Object.
       internal := Some data;
       fields := [];
     |}.
+
+  Definition empty {Value : Set} : t Value :=
+    {|
+      internal := None;
+      fields := [];
+    |}.
 End Object.
 
 Module Pointer.
@@ -187,10 +193,7 @@ End Locals.
 (** ** Constants *)
 Module Constant.
   Definition None_ : Value.t :=
-    Value.Make "builtins" "NoneType" (Pointer.Imm {|
-      Object.internal := None;
-      Object.fields := [];
-    |}).
+    Value.Make "builtins" "NoneType" (Pointer.Imm Object.empty).
 
   Definition ellipsis : Value.t :=
     Value.Make "builtins" "ellipsis" (Pointer.Imm (Object.wrapper Data.Ellipsis)).
@@ -411,7 +414,8 @@ Module M.
 
   Parameter delete : Value.t -> M.
 
-  Parameter return_ : Value.t -> M.
+  Definition return_ (value : Value.t) : M :=
+    LowM.Pure (inr (Exception.Return value)).
 
   Parameter pass : M.
 
@@ -423,6 +427,14 @@ Module M.
 
   Parameter assert : Value.t -> M.
 
+  Definition catch_return (m : M) : M :=
+    let- v := m in
+    match v with
+    | inl v => pure v
+    | inr (Exception.Return v) => pure v
+    | inr e => LowM.Pure (inr e)
+    end.
+
   Parameter if_then_else : Value.t -> M -> M -> M.
 
   Parameter for_ : Value.t -> Value.t -> M -> M -> M.

CoqOfPython/builtins.v

@@ -2,6 +2,8 @@ Require Import CoqOfPython.CoqOfPython.
 
 Definition globals : Globals.t := "builtins".
 
+Definition locals_stack : list Locals.t := [].
+
 Definition type : Value.t :=
   make_klass {|
     Klass.bases := [];
@@ -26,5 +28,14 @@ Definition str : Value.t :=
   |}.
 Axiom str_in_globals : IsInGlobals "builtins" "str" str.
 
-Parameter len : Value.t -> Value.t -> M.
+Definition len : Value.t -> Value.t -> M :=
+  fun (args kwargs : Value.t) =>
+    let- locals_stack := M.create_locals locals_stack args kwargs [ "value" ] in
+    let* value := M.get_name globals locals_stack "value" in
+    let '(Value.Make _ _ pointer) := value in
+    let- object := M.read pointer in
+    match object.(Object.internal) with
+    | Some (Data.List list) => M.pure (Constant.int (Z.of_nat (List.length list)))
+    | _ => M.impossible
+    end.
 Axiom len_in_globals : IsInGlobals globals "len" (make_function len).

CoqOfPython/ethereum/paris/vm/simulations/proofs/exceptions.v

@@ -0,0 +1,35 @@
+Require Import CoqOfPython.CoqOfPython.
+Require Import simulations.proofs.CoqOfPython.
+Require Import simulations.proofs.heap.
+
+Require Import ethereum.paris.vm.simulations.exceptions.
+
+Import Run.
+
+Module ExceptionalHalt.
+  Definition to_value (exn : ExceptionalHalt.t) : Value.t :=
+    match exn with
+    | ExceptionalHalt.StackUnderflowError =>
+      Value.Make "exceptions" "StackUnderflowError" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.StackOverflowError =>
+      Value.Make "exceptions" "StackOverflowError" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.OutOfGasError =>
+      Value.Make "exceptions" "OutOfGasError" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.InvalidOpcode code =>
+      Value.Make "exceptions" "InvalidOpcode" (Pointer.Imm (Object.wrapper (Data.Integer code)))
+    | ExceptionalHalt.InvalidJumpDestError =>
+      Value.Make "exceptions" "InvalidJumpDestError" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.StackDepthLimitError =>
+      Value.Make "exceptions" "StackDepthLimitError" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.WriteInStaticContext =>
+      Value.Make "exceptions" "WriteInStaticContext" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.OutOfBoundsRead =>
+      Value.Make "exceptions" "OutOfBoundsRead" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.InvalidParameter =>
+      Value.Make "exceptions" "InvalidParameter" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.InvalidContractPrefix =>
+      Value.Make "exceptions" "InvalidContractPrefix" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.AddressCollision =>
+      Value.Make "exceptions" "AddressCollision" (Pointer.Imm Object.empty)
+    end.
+End ExceptionalHalt.

CoqOfPython/ethereum/paris/vm/simulations/proofs/stack.v

@@ -1,12 +1,14 @@
 Require Import CoqOfPython.CoqOfPython.
-Require Import proofs.CoqOfPython.
-Require Import simulations.CoqOfPython.
-Require Import proofs.heap.
+Require Import simulations.proofs.CoqOfPython.
+Require Import simulations.proofs.heap.
 
 Require ethereum.paris.vm.simulations.stack.
 Require ethereum.paris.vm.stack.
+Require CoqOfPython.builtins.
 
 Require ethereum.paris.vm.simulations.proofs.__init__.
+Require simulations.proofs.builtins.
+
 Module Evm := __init__.Evm.
 
 Import Run.
@@ -28,39 +30,122 @@ Module PopLocals.
     ].
 End PopLocals.
 
-Lemma run_pop (stack : Stack.t) (heap : Heap.t) :
-  let evm := Heap.to_evm heap in
-  let '(result, evm') := StateError.lift_lens Evm.Lens.stack simulations.stack.pop evm in
-  let result :=
-    match result with
-    | inl s' => inl Constant.None_
-    | inr exn => inr (Exception.Raise (Some Constant.None_))
-    end in
-  exists fresh_stack heap',
+(** Run for the function [get_length]. *)
+Definition run_get_length (stack : Stack.t) (heap : Heap.t) :
   {{ stack, heap |
-    stack.pop (make_list [Evm.stack_to_value]) (make_dict []) ⇓
-    result
-  | stack ++ fresh_stack, heap' }} /\
-  evm' = Heap.to_evm heap'.
+    stack.get_length (make_list [Evm.stack_to_value]) (make_dict []) ⇓
+    (fun (n : Z) => inl (Constant.int n))
+  |
+    fun stack' => stack' = stack,
+    fun heap' => heap' = heap
+  }}.
 Proof.
+  cbn.
+  apply Run.CallPrimitiveStateAllocImm.
+  cbn.
+  eapply Run.CallPrimitiveGetInGlobals. {
+    apply builtins_is_imported.
+    apply builtins.len_in_globals.
+  }
+  cbn.
+  eapply Run.CallClosure. {
+    eapply builtins.run_len.
+    { pose proof (H := IsRead.Heap stack heap Address.stack).
+      now apply H.
+    }
+    { reflexivity. }
+  }
   intros.
-  destruct StateError.lift_lens as [result evm'] eqn:?.
-  unfold stack.pop, simulations.stack.pop in *.
-  cbn in *.
-  repeat eexists.
-  { eapply Run.CallPrimitiveStateAllocMutable. {
-      now apply (IsAlloc.Stack PopLocals.to_object (PopLocals.init evm)).
+  cbn.
+  now eapply Run.Pure.
+Defined.
+
+(** Very simple version of the function [get_length], that actually only return the length of the
+    stack. *)
+Definition simple_get_length (heap : Heap.t) : Z :=
+  Z.of_nat (List.length heap.(Heap.stack)).
+
+(** We can show that it only returns the length of the stack by reflexivity! *)
+Lemma simple_get_length_eq stack heap :
+  simple_get_length heap =
+  let '(l, _, _) := evaluate (run_get_length stack heap) in
+  l.
+Proof.
+  reflexivity.
+Qed.
+
+(** Test module for demo purposes that could be removed later. *)
+Module TestGetLength.
+  (** Dummy value used for the compute below. *)
+  Definition dummy_heap : Heap.t := {|
+    Heap.evm := {|
+      Heap.Evm.pc := Uint.Make 12;
+      Heap.Evm.gas_left := Uint.Make 23;
+    |};
+    Heap.stack := [
+      U256.of_Z 42;
+      U256.of_Z 43;
+      U256.of_Z 44
+    ];
+  |}.
+
+  Definition current_length : Z :=
+    let '(l, _, _) := evaluate (run_get_length [] dummy_heap) in
+    l.
+
+  (* Should return 3 *)
+  (* Compute current_length. *)
+End TestGetLength.
+
+(** Run of the [pop] function. *)
+Definition run_pop (stack : Stack.t) (heap : Heap.t) :
+  {{ stack, heap |
+    stack.pop (make_list [Evm.stack_to_value]) (make_dict []) ⇓
+    (fun (result : unit + builtins.Exception.t) =>
+      match result with
+      | inl tt => inl Constant.None_
+      | inr exn => inr (Exception.Raise (Some (builtins.Exception.to_value exn)))
+      end)
+  |
+    fun stack' => exists fresh_stack, stack' = stack ++ fresh_stack,
+    fun heap' => True
+  }}.
+Proof.
+  cbn.
+  apply Run.CallPrimitiveStateAllocImm.
+  cbn.
+  eapply Run.CallPrimitiveGetInGlobals. {
+    apply builtins_is_imported.
+    apply builtins.len_in_globals.
+  }
+  cbn.
+  eapply Run.CallClosure. {
+    eapply builtins.run_len.
+    { pose proof (H := IsRead.Heap stack heap Address.stack).
+      now apply H.
     }
-    cbn.
-    eapply Run.CallPrimitiveStateRead. {
-      apply IsRead.Stack.
-      now erewrite Stack.read_length_eq.
+    { reflexivity. }
+  }
+  intros.
+  cbn.
+  replace (Compare.eq (Constant.int value_inter) (Constant.int 0))
+    with (M.pure (Constant.bool (value_inter =? 0)))
+    by admit.
+  cbn.
+  match goal with
+  | |- context [ M.if_then_else (Constant.bool ?cond) ] =>
+    replace (M.if_then_else (Constant.bool cond))
+      with (fun (success error : M) => if cond then success else error)
+      by admit
+  end.
+  destruct (_ =? _); cbn.
+  { admit. }
+  { eapply Run.CallPrimitiveStateRead. {
+      pose proof (H2 := IsRead.Heap stack_inter heap_inter Address.stack).
+      now apply H2.
     }
     cbn.
-    eapply Run.CallPrimitiveGetInGlobals. {
-      apply builtins_is_imported.
-      admit.
-    }
+    (* TODO: implement method calls *)
     admit.
   }
 Admitted.

CoqOfPython/ethereum/paris/vm/stack.v

@@ -30,6 +30,38 @@ Axiom ethereum_paris_vm_exceptions_imports_StackOverflowError :
 Axiom ethereum_paris_vm_exceptions_imports_StackUnderflowError :
   IsImported globals "ethereum.paris.vm.exceptions" "StackUnderflowError".
 
+Definition get_length : Value.t -> Value.t -> M :=
+  fun (args kwargs : Value.t) =>
+    let- locals_stack := M.create_locals locals_stack args kwargs [ "evm" ] in
+    M.catch_return ltac:(M.monadic (
+    let _ := Constant.str "
+    Returns the length of the stack.
+
+    Parameters
+    ----------
+    evm :
+        EVM stack.
+
+    Returns
+    -------
+    length : `int`
+        Length of the stack.
+
+    " in
+    let _ := M.return_ (|
+      M.call (|
+        M.get_name (| globals, locals_stack, "len" |),
+        make_list [
+          M.get_name (| globals, locals_stack, "evm" |)
+        ],
+        make_dict []
+      |)
+    |) in
+    M.pure Constant.None_)).
+
+Axiom get_length_in_globals :
+  IsInGlobals globals "get_length" (make_function get_length).
+
 Definition pop : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "stack" ] in

CoqOfPython/ethereum/simulations/proofs/exceptions.v

@@ -0,0 +1,16 @@
+Require Import CoqOfPython.CoqOfPython.
+Require Import simulations.proofs.CoqOfPython.
+Require Import simulations.proofs.heap.
+
+Require ethereum.paris.vm.simulations.proofs.exceptions.
+Require ethereum.simulations.exceptions.
+
+Import Run.
+
+Module EthereumException.
+  Definition to_value (exn : exceptions.EthereumException.t) : Value.t :=
+    match exn with
+    | exceptions.EthereumException.ExceptionalHalt exn =>
+      Value.Make "exceptions" "ExceptionalHalt" (Pointer.Imm Object.empty)
+    end.
+End EthereumException.