Revm: more links for the instructions

CoqOfRust/alloy_primitives/bytes/links/mod.v

@@ -121,3 +121,4 @@ Module Impl_From_Vec_u8_for_Bytes.
   Instance run : From.Run Self (Vec.t U8.t Global.t).
   Admitted.
 End Impl_From_Vec_u8_for_Bytes.
+Export Impl_From_Vec_u8_for_Bytes.

CoqOfRust/core/iter/traits/links/iterator.v

@@ -199,7 +199,7 @@ Module Iterator.
       Set :=
     TraitMethod.C (trait Self) "any" (fun method =>
       forall
-         (F : Set) `{Link F}
+         (F : Set) `(Link F)
          (self : Ref.t Pointer.Kind.MutRef Self)
          (f : F)
          `(FnMut.Run F Item bool),

CoqOfRust/core/links/default.v

@@ -61,10 +61,12 @@ Module Impl_Default_for_bool.
     Default.default := run_default;
   }.
 End Impl_Default_for_bool.
+Export Impl_Default_for_bool.
 
 Module Impl_Default_for_char.
   (* TODO *)
 End Impl_Default_for_char.
+Export Impl_Default_for_char.
 
 Module Impl_Default_for_integer.
   Definition Self (kind : IntegerKind.t) : Set :=
@@ -123,3 +125,4 @@ Module Impl_Default_for_integer.
     Default.default := run_default kind;
   }.
 End Impl_Default_for_integer.
+Export Impl_Default_for_integer.

CoqOfRust/core/links/option.v

@@ -1,6 +1,9 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
 Require Import core.convert.links.mod.
+Require Import core.links.default.
+Require Import core.links.hint.
+Require Import core.links.panickingAux.
 Require Import core.links.result.
 Require Import core.option.
 Require Import core.ops.links.function.
@@ -86,6 +89,26 @@ Module Option.
   End SubPointer.
 End Option.
 
+(* const fn unwrap_failed() -> ! *)
+Instance run_unwrap_failed :
+  Run.Trait
+    option.unwrap_failed [] [] []
+    Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
+(* const fn expect_failed(msg: &str) -> ! *)
+Instance run_expect_failed (msg : Ref.t Pointer.Kind.Ref string) :
+  Run.Trait
+    option.expect_failed [] [] [ φ msg ]
+    Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
 Module Impl_Option.
   Definition Self (T : Set) `{Link T} : Set := option T.
 
@@ -120,23 +143,35 @@ Module Impl_Option.
   Proof.
     constructor.
     run_symbolic.
-  Admitted.
+  Defined.
 
   (* pub const unsafe fn unwrap_unchecked(self) -> T *)
   Instance run_unwrap_unchecked {T : Set} `{Link T}
       (self : Self T) :
     Run.Trait
       (option.Impl_core_option_Option_T.unwrap_unchecked (Φ T)) [] [] [ φ self ]
       T.
-  Admitted.
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
 
-  (* pub fn unwrap_or_default(self) -> T *)
+  (*
+    pub fn unwrap_or_default(self) -> T
+    where
+        T: Default,
+  *)
   Instance run_unwrap_or_default {T : Set} `{Link T}
+      {run_Default_for_T : Default.Run T}
       (self : Self T) :
     Run.Trait
       (option.Impl_core_option_Option_T.unwrap_or_default (Φ T)) [] [] [ φ self ]
       T.
-  Admitted.
+  Proof.
+    constructor.
+    destruct run_Default_for_T.
+    run_symbolic.
+  Defined.
 
   (* pub fn unwrap_or(self, default: T) -> T *)
   Instance run_unwrap_or {T : Set} `{Link T}
@@ -155,7 +190,10 @@ Module Impl_Option.
     Run.Trait
       (option.Impl_core_option_Option_T.expect (Φ T)) [] [] [ φ self; φ msg ]
       T.
-  Admitted.
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
 End Impl_Option.
 Export Impl_Option.
 

CoqOfRust/core/links/panicking.v

@@ -4,21 +4,7 @@ Require Import core.fmt.links.mod.
 Require Import core.links.option.
 Require Import core.panicking.
 
-(* pub const fn panic_fmt(fmt: fmt::Arguments<'_>) -> ! *)
-Instance run_panic_fmt (fmt : Arguments.t) :
-  Run.Trait panicking.panic_fmt [] [] [φ fmt] Empty_set.
-Proof.
-  constructor.
-  run_symbolic.
-Admitted.
-
-(* pub const fn panic(expr: &'static str) -> ! *)
-Instance run_panic (expr : Ref.t Pointer.Kind.Ref string) :
-  Run.Trait panicking.panic [] [] [φ expr] Empty_set.
-Proof.
-  constructor.
-  run_symbolic.
-Admitted.
+Require Export core.links.panickingAux.
 
 (*
 pub enum AssertKind {

CoqOfRust/core/links/panickingAux.v

@@ -0,0 +1,31 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import core.fmt.links.mod.
+Require Import core.panicking.
+
+(* pub const fn panic_fmt(fmt: fmt::Arguments<'_>) -> ! *)
+Instance run_panic_fmt (fmt : Arguments.t) :
+  Run.Trait panicking.panic_fmt [] [] [φ fmt] Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Admitted.
+
+(* pub const fn panic(expr: &'static str) -> ! *)
+Instance run_panic (expr : Ref.t Pointer.Kind.Ref string) :
+  Run.Trait panicking.panic [] [] [φ expr] Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
+(* pub const fn panic_display<T: fmt::Display>(x: &T) -> ! *)
+Instance run_panic_display {T : Set} `{Link T}
+    (x : Ref.t Pointer.Kind.Ref T) :
+  Run.Trait
+    panicking.panic_display [] [Φ T] [φ x]
+    Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Admitted.

CoqOfRust/revm/revm_context_interface/links/host.v

@@ -17,10 +17,45 @@ pub struct SStoreResult {
 }
 *)
 Module SStoreResult.
-  Parameter t : Set.
+  Record t : Set := {
+    original_value : aliases.U256.t;
+    present_value : aliases.U256.t;
+    new_value : aliases.U256.t;
+  }.
 
-  Global Instance IsLink : Link t.
-  Admitted.
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "revm_context_interface::host::SStoreResult";
+    φ x :=
+      Value.StructRecord "revm_context_interface::host::SStoreResult" [] [] [
+        ("original_value", φ x.(original_value));
+        ("present_value", φ x.(present_value));
+        ("new_value", φ x.(new_value))
+      ]
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "revm_context_interface::host::SStoreResult").
+  Proof.
+    eapply OfTy.Make with (A := t).
+    reflexivity.
+  Defined.
+  Smpl Add apply of_ty : of_ty.
+
+  Lemma of_value_with
+      original_value' original_value
+      present_value' present_value
+      new_value' new_value :
+    original_value' = φ original_value ->
+    present_value' = φ present_value ->
+    new_value' = φ new_value ->
+    Value.StructRecord "revm_context_interface::host::SStoreResult" [] [] [
+      ("original_value", original_value');
+      ("present_value", present_value');
+      ("new_value", new_value')
+    ] = φ (Build_t original_value present_value new_value).
+  Proof.
+    now intros; subst.
+  Qed.
+  Smpl Add unshelve eapply of_value_with : of_value.
 End SStoreResult.
 
 (*

CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v

@@ -3,6 +3,7 @@ Require Import CoqOfRust.links.M.
 Require Import alloy_primitives.bits.links.address.
 Require Import alloy_primitives.bits.links.fixed.
 Require Import core.convert.links.mod.
+Require Import core.links.default.
 Require Import core.links.option.
 Require Import revm.revm_context_interface.links.host.
 Require Import revm.revm_context_interface.links.block.
@@ -256,4 +257,4 @@ Proof.
   destruct run_BlockGetter_for_Self.
   destruct run_Block_for_Block.
   run_symbolic.
-Defined.
+Defined.

CoqOfRust/revm/revm_interpreter/instructions/links/contract/call.v

@@ -66,4 +66,4 @@ Proof.
   destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
   destruct Impl_IntoAddress_for_U256.run.
   run_symbolic.
-Defined.
+Admitted.

CoqOfRust/revm/revm_interpreter/instructions/links/contract/call_code.v

@@ -67,4 +67,4 @@ Proof.
   destruct Impl_From_U256_for_FixedBytes_32.run.
   destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
   run_symbolic.
-Defined.
+Admitted.

CoqOfRust/revm/revm_interpreter/instructions/links/contract/delegate_call.v

@@ -66,4 +66,4 @@ Proof.
   destruct Impl_From_U256_for_FixedBytes_32.run.
   destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
   run_symbolic.
-Defined.
+Admitted.

CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall.v

@@ -66,4 +66,4 @@ Proof.
   destruct run_InputsTrait_for_Input.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Defined.
+Admitted.

CoqOfRust/revm/revm_interpreter/instructions/links/contract/extdelegatecall.v

@@ -65,4 +65,4 @@ Proof.
   destruct run_InputsTrait_for_Input.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Defined.
+Admitted.

CoqOfRust/revm/revm_interpreter/instructions/links/contract/extstaticcall.v

@@ -65,4 +65,4 @@ Proof.
   destruct run_InputsTrait_for_Input.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Defined.
+Admitted.

CoqOfRust/revm/revm_interpreter/instructions/links/contract/pop_extcall_target_address.v

@@ -61,4 +61,4 @@ Proof.
   destruct (Impl_Iterator_for_Iter.run U8.t).
   destruct (Impl_Index_for_FixedBytes_N.run {| Integer.value := 32 |} (RangeTo.t Usize.t)).
   run_symbolic.
-Defined.
+Admitted.

CoqOfRust/revm/revm_interpreter/instructions/links/contract/static_call.v

@@ -66,4 +66,4 @@ Proof.
   destruct Impl_From_U256_for_FixedBytes_32.run.
   destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
   run_symbolic.
-Defined.
+Admitted.

CoqOfRust/revm/revm_interpreter/instructions/links/control.v

@@ -1,7 +1,9 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import alloc.links.slice.
 Require Import alloy_primitives.bytes.links.mod.
 Require Import alloy_primitives.links.aliases.
+Require Import core.convert.links.mod.
 Require Import core.convert.links.num.
 Require Import core.links.option.
 Require Import core.links.result.
@@ -308,7 +310,9 @@ Proof.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_MemoryTrait_for_Memory.
+  destruct run_Deref_for_Synthetic1.
   destruct Impl_Default_for_Bytes.run.
+  destruct (Impl_Into_for_From_T.run Impl_From_Vec_u8_for_Bytes.run).
   run_symbolic.
 Admitted.