simulations: special case for the stack with a single element

Author: clarus

CoqOfRust/revm/revm_interpreter/simulations/gas.v

@@ -112,8 +112,8 @@ Module Impl_Gas.
     set (ref_core := Ref.Core.Mutable _ _ _ _ _).
     epose proof (Run.GetSubPointer _ _ ref_core Gas.SubPointer.get_limit).
     apply H; clear H.
-    cbn; intros.
     apply Run.StateRead. {
+      cbn.
       epose proof (
         Stack.CanRead.Mutable
           [Self]
@@ -128,10 +128,38 @@ Module Impl_Gas.
     apply Run.Pure.
   Defined.
 
-  Lemma limit_eq (gas : Gas.t) :
-    M.evaluate run_limit (gas, tt) =
-    (Output.Success gas.(Gas.limit), (gas, tt)).
+  Lemma limit_eq (self : Self) :
+    M.evaluate run_limit self =
+    (Output.Success self.(Gas.limit), self).
   Proof.
     reflexivity.
   Qed.
+
+  (*
+      pub fn erase_cost(&mut self, returned: u64) {
+          self.remaining += returned;
+      }
+  *)
+  Definition run_erase_cost (returned : U64.t) :
+    let self := {| Ref.core := Ref.Core.Mutable 0%nat [] φ Some (fun _ => Some) |} in
+    {{ [Self] 🌲 links.M.evaluate (Impl_Gas.run_erase_cost self returned).(Run.run_f) }}.
+  Proof.
+    cbn.
+    set (ref_core := Ref.Core.Mutable _ _ _ _ _).
+    epose proof (Run.GetSubPointer _ _ ref_core Gas.SubPointer.get_remaining).
+    apply H; clear H.
+    apply Run.StateRead. {
+      cbn.
+      epose proof (
+        Stack.CanRead.Mutable
+          [Self]
+          0%nat
+          _
+          _
+          (fun big_a : links.gas.Impl_Gas.Self => Some big_a.(Gas.remaining))
+      ).
+      apply H.
+    }
+    cbn; intros.
+  Admitted.
 End Impl_Gas.

CoqOfRust/simulations/M.v

@@ -462,46 +462,40 @@ Module Stack.
   Definition t : Type :=
     list Set.
 
-  Fixpoint to_Set (stack : t) : Set :=
-    match stack with
+  Fixpoint to_Set_aux (A : Set) (Stack : t) : Set :=
+    match Stack with
+    | [] => A
+    | B :: Stack => A * to_Set_aux B Stack
+    end.
+
+  Definition to_Set (Stack : t) : Set :=
+    match Stack with
     | [] => unit
-    | A :: stack => A * to_Set stack
+    | A :: Stack => to_Set_aux A Stack
     end.
 
   Definition read_Set (Stack : t) (index : nat) : Set :=
     List.nth index Stack unit.
 
-  Fixpoint read {Stack : t} (stack : to_Set Stack) (index : nat) : read_Set Stack index.
+  Fixpoint read_aux {A : Set} {Stack : t}
+    (stack : to_Set_aux A Stack)
+    (index : nat)
+    {struct Stack} :
+    read_Set (A :: Stack) index.
   Proof.
-    destruct Stack as [|A Stack], index as [|index]; cbn in *.
-    { exact tt. }
-    { exact tt. }
+    destruct Stack as [|B Stack], index as [|index]; cbn in *.
+    { exact stack. }
+    { destruct index; exact tt. }
     { exact (fst stack). }
-    { exact (read _ (snd stack) index). }
+    { exact (read_aux _ _ (snd stack) index). }
   Defined.
 
-  (* Module Read.
-    Inductive t {A : Set} `{Link A} {Stack : Stack.t} (stack : to_Set Stack) :
-      Ref.Core.t A ->
-      option A ->
-      Set :=
-    | Immediate
-        (value : option A) :
-      t stack
-        (Ref.Core.Immediate value)
-        value
-    | Mutable
-        (index : nat)
-        (path : Pointer.Path.t)
-        (big_to_value : read_Set Stack index -> Value.t)
-        (projection : read_Set Stack index -> option A)
-        (injection : read_Set Stack index -> A -> option (read_Set Stack index)) :
-      t stack
-        (Ref.Core.Mutable (Address := nat) (Big_A := read_Set Stack index)
-          index path big_to_value projection injection
-        )
-        (projection (read stack index)).
-  End Read. *)
+  Definition read {Stack : t} (stack : to_Set Stack) (index : nat) : read_Set Stack index.
+  Proof.
+    destruct Stack; cbn in *.
+    { destruct index; exact tt. }
+    { apply (read_aux stack). }
+  Defined.
 
   Module CanRead.
     Inductive t {A : Set} `{Link A} (Stack : Stack.t) : Ref.Core.t A -> Set :=