simulations: more wip

Author: clarus

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

@@ -22,7 +22,12 @@ Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack, run_LoopControl_for_Control.
+  simulate_one_step.
   simulate.
+  { admit. }
+  { 
+
+  }
 Defined.
 
 (*

CoqOfRust/revm/revm_interpreter/simulations/interpreter.v

@@ -0,0 +1,43 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.simulations.M.
+Require Import revm.revm_interpreter.links.interpreter.
+
+Module Impl_Interpreter.
+  Definition Self
+    (IW : Set) `{Link IW}
+    {IW_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks IW_types}
+    (run_InterpreterTypes_for_IW : InterpreterTypes.Run IW IW_types) :
+    Set :=
+    Interpreter.t IW IW_types.
+
+  Instance run_step
+      (IW : Set) `{Link IW}
+      {IW_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks IW_types}
+      (run_InterpreterTypes_for_IW : InterpreterTypes.Run IW IW_types)
+      (H_ : Set) `{Link H_}
+      (FN : Set) `{Link FN}
+      (run_CustomInstruction_for_FN : CustomInstruction.Run FN IW IW_types H_)
+      (self : Ref.t Pointer.Kind.MutRef (Self IW run_InterpreterTypes_for_IW))
+      (instruction_table : Ref.t Pointer.Kind.Ref (array.t FN {| Integer.value := 256 |}))
+      (host : Ref.t Pointer.Kind.MutRef H_) :
+    Run.Trait
+      (interpreter.Impl_revm_interpreter_interpreter_Interpreter_IW.step (Φ IW))
+        []
+        [ Φ FN; Φ H_ ]
+        [ φ self; φ instruction_table; φ host ]
+      unit.
+  Proof.
+    constructor.
+    cbn.
+    eapply Run.Rewrite. {
+      erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_IW.
+      reflexivity.
+    }
+    destruct run_InterpreterTypes_for_IW.
+    destruct run_Jumps_for_Bytecode.
+    destruct run_CustomInstruction_for_FN.
+    destruct exec as [exec [H_exec run_exec]].
+    run_symbolic.
+  Defined.
+End Impl_Interpreter.

CoqOfRust/simulations/M.v

@@ -613,9 +613,9 @@ Module Stack.
         end
       end.
 
-    Axiom admit_access_for_now :
+    (* Axiom admit_access_for_now :
       forall {A : Set} `{Link A} (Stack : Stack.t) (ref_core : Ref.Core.t A),
-      t Stack ref_core.
+      t Stack ref_core. *)
 
     Ltac infer :=
       cbn ||
@@ -624,8 +624,7 @@ Module Stack.
         apply (runner r)
       end ||
       assumption ||
-      apply Stack.CanAccess.Immediate ||
-      apply admit_access_for_now.
+      apply Stack.CanAccess.Immediate.
   End CanAccess.
 End Stack.
 
@@ -813,12 +812,26 @@ Module Run.
       (e : LowM.t R Output')
       (k : Output.t R (Ref.t Pointer.Kind.Raw Output') -> LowM.t R Output)
     (H_e : {{ StackIn 🌲 e }})
-    (H_k : forall (ref_or_exception : Output.t R (Ref.t Pointer.Kind.Raw Output')),
+    (H_k : forall (value_or_exception : Output.t R Output'),
       let StackIn' :=
-        match ref_or_exception with
+        match value_or_exception with
         | Output.Success _ => StackIn ++ [Output']
         | Output.Exception _ => StackIn
         end in
+      let ref_or_exception : Output.t R (Ref.t Pointer.Kind.Raw Output') :=
+        match value_or_exception with
+        | Output.Success _ =>
+          Output.Success {|
+            Ref.core :=
+              Ref.Core.Mutable
+                (List.length StackIn)
+                []
+                φ
+                Some
+                (fun _ => Some)
+          |}
+        | Output.Exception exception => Output.Exception exception
+        end in
       {{ StackIn' 🌲 k ref_or_exception }}
     ) :
     {{ StackIn 🌲 LowM.LetAlloc e k }}
@@ -883,29 +896,22 @@ Proof.
   }
   { (* LetAlloc *)
     refine (
-      let '(output', stack_in') := evaluate _ _ _ _ run stack_in in
+      let '(value_or_exception, stack_in') := evaluate _ _ _ _ run stack_in in
+      _
+    ).
+    refine (
+      let result := H_k value_or_exception in
       _
     ).
-    destruct output' as [output' | exception].
+    destruct value_or_exception as [value | exception].
     { refine (
-        let ref_core :=
-          Ref.Core.Mutable
-            (List.length StackIn)
-            []
-            φ
-            Some
-            (fun _ => Some) in
-        let ref : Ref.t Pointer.Kind.Raw Output' := {| Ref.core := ref_core |} in
-        _
-      ).
-      refine (
         let '(output, stack_out) := _ in
         (output, fst (Stack.dealloc (A := Output') stack_out))
       ).
-      unshelve eapply (evaluate _ _ _ _ (H_k (Output.Success ref)) _).
-      exact (Stack.alloc stack_in' output').
+      unshelve eapply (evaluate _ _ _ _ result _).
+      exact (Stack.alloc stack_in' value).
     }
-    { exact (evaluate _ _ _ _ (H_k (Output.Exception exception)) stack_in'). }
+    { exact (evaluate _ _ _ _ result stack_in'). }
   }
 Defined.