More wip

Author: clarus

CoqOfRust/links/M.v

@@ -230,6 +230,9 @@ Module Integer.
   Global Instance IsPrimitiveEq {kind : IntegerKind.t} : PrimitiveEq.Trait (t kind) := {
     PrimitiveEq.eqb x y := x.(value) =? y.(value);
   }.
+
+  Definition wrap_of_Z {kind : IntegerKind.t} (z : Z) : t kind :=
+    {| value := Integer.normalize_wrap kind z |}.
 End Integer.
 
 (** ** Integer kinds for better readability *)
@@ -1038,14 +1041,21 @@ Module LowM.
   Inductive t (R Output : Set) : Set :=
   | Pure (value : Output.t R Output)
   | CallPrimitive {A : Set} (primitive : Primitive.t A) (k : A -> t R Output)
-  | Call {A : Set} `{Link A} {e : M} (run : {{ e 🔽 A, A }}) (k : SuccessOrPanic.t A -> t R Output)
+  (* | Call {A : Set} `{Link A}
+      {e : M}
+      (run : {{ e 🔽 A, A }})
+      (k : SuccessOrPanic.t A -> t R Output) *)
+  | Call {A : Set}
+      (e : t A A)
+      (k : SuccessOrPanic.t A -> t R Output)
   | LetAlloc {A : Set} `{Link A}
       (e : t R A)
       (k : Output.t R (Ref.t Pointer.Kind.Raw A) -> t R Output)
   | Loop {A : Set} (body : t R A) (k : Output.t R A -> t R Output).
   Arguments Pure {_ _}.
   Arguments CallPrimitive {_ _ _}.
-  Arguments Call {_ _ _ _ _}.
+  (* Arguments Call {_ _ _ _ _}. *)
+  Arguments Call {_ _ _}.
   Arguments LetAlloc {_ _ _ _}.
   Arguments Loop {_ _ _}.
 End LowM.
@@ -1144,7 +1154,8 @@ Proof.
   }
   { (* CallClosure *)
     eapply (LowM.Call (A := Output')). {
-      exact run.
+      (* exact run. *)
+      exact (evaluate _ _ _ _ _ run).
     }
     intros output'; eapply evaluate.
     match goal with

CoqOfRust/revm/revm_interpreter/instructions/simulations/arithmetic.v

@@ -23,6 +23,7 @@ Proof.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack, run_LoopControl_for_Control.
   simulate_one_step.
+  simulate_one_step.
   simulate.
   { admit. }
   { 

CoqOfRust/revm/revm_interpreter/interpreter/simulations/stack.v

@@ -6,26 +6,26 @@ Require Import core.links.array.
 Require Import revm.links.dependencies.
 Require Import revm_interpreter.interpreter.links.stack.
 
-(*
 Module Stack.
   (*
-    /// Returns the length of the stack in words.
-    #[inline]
-    pub fn len(&self) -> usize {
-        self.data.len()
-    }
+  pub struct Stack {
+      data: Vec<U256>,
+  }
   *)
-  Definition len '(Stack.data stack) : Z :=
-    Z.of_nat (List.length stack).
+  Record t : Set := {
+    data: list U256.t;
+  }.
+End Stack.
 
-  (*
-    /// Removes the topmost element from the stack and returns it, or `StackUnderflow` if it is
-    /// empty.
-    #[inline]
-    pub fn pop(&mut self) -> Result<U256, InstructionResult> {
-        self.data.pop().ok_or(InstructionResult::StackUnderflow)
-    }
-  *)
+Module Impl_Stack.
+  Definition Self : Set :=
+    Stack.t.
+
+  (* pub fn len(&self) -> usize *)
+  Definition len (self : Self) : Usize.t :=
+    Integer.wrap_of_Z (Z.of_nat (List.length self.(Stack.data))).
+
+  (* pub fn pop(&mut self) -> Result<U256, InstructionResult> *)
   Definition pop :
       MS? Stack.t string (U256.t + InstructionResult.t) :=
     letS? '(Stack.data stack) := readS? in
@@ -120,4 +120,3 @@ Module Stack.
     letS? pop2 := pop_unsafe in
     returnS? (pop1, pop2, top_unsafe).
 End Stack.
-*)

CoqOfRust/revm/revm_interpreter/simulations/gas.v

@@ -14,7 +14,18 @@ Module Impl_MemoryGas.
   Definition Self : Set :=
     MemoryGas.t.
 
-  Instance run_new Stack :
+  (* pub const fn new() -> Self *)
+  Instance run_new Stack (stack : Stack.to_Set Stack) :
+    Run.C Impl_MemoryGas.run_new (fun _ => unit) stack.
+  Proof.
+    constructor.
+    apply Run.Pure.
+    exact tt.
+  Defined.
+
+  (* Compute run_new. *)
+
+  (* Instance run_new Stack :
     Run.Trait Stack Impl_MemoryGas.run_new.
   Proof.
     constructor.
@@ -26,7 +37,39 @@ Module Impl_MemoryGas.
     (Output.Success Impl_Default_for_MemoryGas.default, tt).
   Proof.
     reflexivity.
-  Qed.
+  Qed. *)
+
+  (* pub fn record_new_len(&mut self, new_num: usize) -> Option<u64> *)
+  Instance run_record_new_len Stack (stack : Stack.to_Set Stack)
+      (self : Ref.t Pointer.Kind.MutRef Self)
+      (new_num : Usize.t)
+      (H_self : Stack.CanAccess.t Stack self.(Ref.core)) :
+    Run.C (Impl_MemoryGas.run_record_new_len self new_num) (fun _ => unit) stack.
+  Proof.
+    constructor.
+    Ltac simulate_reduce :=
+      repeat match goal with
+      | |- {{ StackM.let_ _ _ 🌲 _ }} =>
+        unfold StackM.let_
+      | |- {{ ?e 🌲 _ }} =>
+        let e' := eval hnf in e in
+        change e with e'
+      end.
+
+    Ltac simulate_get_can_access :=
+      match goal with
+      | |- {{ StackM.GetCanAccess _ _ _ 🌲 _ }} =>
+        unshelve eapply Run.GetCanAccess; [Stack.CanAccess.infer |]
+      end.
+
+    Time simulate_reduce; unshelve eapply Run.GetCanAccess. {
+      Time Stack.CanAccess.infer.
+    }
+    Time try (simulate_reduce; simulate_get_can_access).
+    simulate_reduce.
+    cbn.
+    Show.
+  Defined.
 End Impl_MemoryGas.
 
 Module Impl_Gas.
@@ -35,6 +78,41 @@ Module Impl_Gas.
   Definition Self : Set :=
     Gas.t.
 
+  Definition run_limit Stack (stack : Stack.to_Set Stack)
+      (self : Ref.t Pointer.Kind.Ref Self)
+      (H_self : Stack.CanAccess.t Stack self.(Ref.core)) :
+    RunEval.t (Impl_Gas.run_limit self).(Run.run_f) stack.
+  Proof.
+    unfold RunEval.t; cbn.
+    unshelve econstructor. {
+      repeat Stack.CanAccess.infer.
+    }
+    match goal with
+    | |- Run.t (match ?e with _ => _ end) =>
+      destruct e
+    end; constructor.
+  Defined.
+
+  Parameter limit : U64.t.
+
+  Definition self : Ref.t Pointer.Kind.Ref Self := Ref.immediate Pointer.Kind.Ref {|
+    Gas.limit := limit;
+    Gas.remaining := limit;
+    Gas.refunded := {| Integer.value := 0 |};
+    Gas.memory := Impl_Default_for_MemoryGas.default;
+  |}.
+
+  Definition H_self : Stack.CanAccess.t [] self.(Ref.core).
+  Proof.
+    repeat Stack.CanAccess.infer.
+  Defined.
+
+  Compute Run.eval (run_limit [] tt self H_self).
+
+  Compute fun self => Run.eval (
+    run_limit [] tt {| Ref.core := Ref.Core.Immediate (Some self) |} ltac:(now repeat Stack.CanAccess.infer)
+  ).
+
   (*
       pub const fn new(limit: u64) -> Self {
           Self {