Add links for utility and control function

CoqOfRust/alloy_primitives/links/common.v

@@ -0,0 +1,29 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.common.
+
+(*
+pub enum TxKind {
+    Create,
+    Call(Address),
+}
+*)
+Module TxKind.
+  Inductive t : Set :=
+  | Create
+  | Call (address : Address.t).
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "alloy_primitives::common::TxKind";
+    φ x :=
+      match x with
+      | Create => Value.StructTuple "alloy_primitives::common::TxKind::Create" []
+      | Call address => Value.StructTuple "alloy_primitives::common::TxKind::Call" [φ address]
+      end;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "alloy_primitives::common::TxKind").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+End TxKind.

CoqOfRust/alloy_primitives/log/links/mod.v

@@ -0,0 +1,24 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.log.mod.
+
+(*
+pub struct Log<T = LogData> {
+    pub address: Address,
+    pub data: T,
+}
+*)
+Module Log.
+  Parameter t : Set.
+
+  Parameter to_value : t -> Value.t.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "alloy_primitives::log::Log";
+    φ := to_value;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "alloy_primitives::log::Log").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+End Log.

CoqOfRust/core/convert/links/mod.v

@@ -137,3 +137,25 @@ Module TryFrom.
     try_from : Run_try_from Self T Error;
   }.
 End TryFrom.
+
+(*
+pub trait TryInto<T>: Sized {
+    type Error;
+
+    fn try_into(self) -> Result<T, Self::Error>;
+}
+*)
+Module TryInto.
+  Definition trait (Self T : Set) `{Link Self} `{Link T} : TraitMethod.Header.t :=
+    ("core::convert::TryInto", [], [Φ T], Φ Self).
+
+  Definition Run_try_into (Self T Error : Set) `{Link Self} `{Link T} `{Link Error} : Set :=
+    TraitMethod.C (trait Self T) "try_into" (fun method =>
+      forall (self : Self),
+        Run.Trait method [] [] [ φ self ] (Result.t T Error)
+    ).
+
+  Class Run (Self : Set) (T : Set) (Error : Set) `{Link Self} `{Link T} `{Link Error} : Set := {
+    try_into : Run_try_into Self T Error;
+  }.
+End TryInto.

CoqOfRust/core/convert/links/num.v

@@ -27,3 +27,25 @@ Module Impl_TryFrom_u64_for_usize.
     TryFrom.try_from := run_try_from;
   }.
 End Impl_TryFrom_u64_for_usize.
+
+Module Impl_TryFrom_u64_for_isize.
+  Definition Self : Set :=
+    Isize.t.
+
+  Definition run_try_from : TryFrom.Run_try_from Self U64.t TryFromIntError.t.
+  Proof.
+    eexists.
+    { eapply IsTraitMethod.Defined.
+      { apply convert.num.ptr_try_from_impls.Impl_core_convert_TryFrom_u64_for_isize.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      run_symbolic.
+      all: admit.
+    }
+  Admitted.
+
+  Instance run : TryFrom.Run Self U64.t TryFromIntError.t := {
+    TryFrom.try_from := run_try_from;
+  }.
+End Impl_TryFrom_u64_for_isize.

CoqOfRust/core/fmt/links/mod.v

@@ -3,6 +3,7 @@ Require Import CoqOfRust.links.M.
 Require Import core.fmt.links.rt.
 Require Import core.fmt.mod.
 Require Import core.links.array.
+
 (*
 pub struct Arguments<'a> {
     pieces: &'a [&'static str],
@@ -28,6 +29,16 @@ End Arguments.
 Module Impl_Arguments.
   Definition Self : Set := Arguments.t.
 
+  (* pub const fn new_const<const N: usize>(pieces: &'a [&'static str; N]) -> Self *)
+  Instance run_new_const
+      (N : Usize.t)
+      (pieces : Ref.t Pointer.Kind.Ref (array.t (Ref.t Pointer.Kind.Ref string) N)) :
+    Run.Trait fmt.Impl_core_fmt_Arguments.new_const [φ N] [] [φ pieces] Self.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
   (*
     pub fn new_v1<const P: usize, const A: usize>(
         pieces: &'a [&'static str; P],

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

@@ -259,7 +259,7 @@ Module Iterator.
       Set :=
     TraitMethod.C (trait Self) "next" (fun method =>
       forall (self : Ref.t Pointer.Kind.MutRef Self),
-      Run.Trait method [] [] [φ self] Item
+      Run.Trait method [] [] [φ self] (option Item)
     ).
 
   Definition Run_next_chunk

CoqOfRust/core/links/cmp.v

@@ -6,6 +6,34 @@ Require Import core.links.option.
 Require Import core.ops.links.function.
 Require Export core.links.cmpOrdering.
 
+(*
+pub trait PartialEq<Rhs: ?Sized = Self> {
+    fn eq(&self, other: &Rhs) -> bool;
+    fn ne(&self, other: &Rhs) -> bool;
+}
+*)
+Module PartialEq.
+  Definition trait (Self Rhs : Set) `{Link Self} `{Link Rhs} : TraitMethod.Header.t :=
+    ("core::cmp::PartialEq", [], [ Φ Rhs ], Φ Self).
+
+  Definition Run_eq (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set :=
+    TraitMethod.C (trait Self Rhs) "eq" (fun method =>
+      forall (self other : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self; φ other ] bool
+    ).
+
+  Definition Run_ne (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set :=
+    TraitMethod.C (trait Self Rhs) "ne" (fun method =>
+      forall (self other : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self; φ other ] bool
+    ).
+
+  Class Run (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set := {
+    eq : Run_eq Self Rhs;
+    ne : Run_ne Self Rhs;
+  }.
+End PartialEq.
+
 (*
     pub fn max_by<T, F: FnOnce(&T, &T) -> Ordering>(v1: T, v2: T, compare: F) -> T {
         match compare(&v1, &v2) {

CoqOfRust/core/links/error.v

@@ -0,0 +1,53 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+(* pub struct Request<'a>(Tagged<dyn Erased<'a> + 'a>); *)
+Module Request.
+  Parameter t : Set.
+
+  Parameter to_value : t -> Value.t.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "core::error::Request";
+    φ := to_value;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "core::error::Request").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+End Request.
+
+(*
+pub trait Error: Debug + Display {
+    // Provided methods
+    fn source(&self) -> Option<&(dyn Error + 'static)> { ... }
+    fn description(&self) -> &str { ... }
+    fn cause(&self) -> Option<&dyn Error> { ... }
+    fn provide<'a>(&'a self, request: &mut Request<'a>) { ... }
+}
+*)
+Module Error.
+  Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
+    ("core::error::Error", [], [], Φ Self).
+
+  Definition Run_description (Self : Set) `{Link Self} : Set :=
+    TraitMethod.C (trait Self) "description" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref string)
+    ).
+
+  Definition Run_provide (Self : Set) `{Link Self} : Set :=
+    TraitMethod.C (trait Self) "provide" (fun method =>
+      forall
+        (self : Ref.t Pointer.Kind.Ref Self)
+        (request : Ref.t Pointer.Kind.MutRef Request.t),
+      Run.Trait method [] [] [ φ self; φ request ] unit
+    ).
+
+  Class Run (Self : Set) `{Link Self} : Set := {
+    (* TODO: Add source *)
+    description : Run_description Self;
+    (* TODO: Add cause *)
+    provide : Run_provide Self;
+  }.
+End Error.

CoqOfRust/core/links/option.v

@@ -93,6 +93,14 @@ Module Impl_Option.
       (Result.t T E).
   Admitted.
 
+  (* pub const fn unwrap(self) -> T *)
+  Instance run_unwrap {T : Set} `{Link T}
+      (self : Self T) :
+    Run.Trait
+      (option.Impl_core_option_Option_T.unwrap (Φ T)) [] [] [ φ self ]
+      T.
+  Admitted.
+
   (* pub const unsafe fn unwrap_unchecked(self) -> T *)
   Instance run_unwrap_unchecked {T : Set} `{Link T}
       (self : Self T) :
@@ -108,4 +116,20 @@ Module Impl_Option.
       (option.Impl_core_option_Option_T.unwrap_or_default (Φ T)) [] [] [ φ self ]
       T.
   Admitted.
+
+  (* pub fn unwrap_or(self, default: T) -> T *)
+  Instance run_unwrap_or {T : Set} `{Link T}
+      (self : Self T) (default : T) :
+    Run.Trait
+      (option.Impl_core_option_Option_T.unwrap_or (Φ T)) [] [] [ φ self; φ default ]
+      T.
+  Admitted.
+
+  (* pub const fn expect(self, msg: &str) -> T *)
+  Instance run_expect {T : Set} `{Link T}
+      (self : Self T) (msg : Ref.t Pointer.Kind.Ref string) :
+    Run.Trait
+      (option.Impl_core_option_Option_T.expect (Φ T)) [] [] [ φ self; φ msg ]
+      T.
+  Admitted.
 End Impl_Option.

CoqOfRust/core/links/panicking.v

@@ -1,6 +1,7 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import core.fmt.links.mod.
+Require Import core.links.option.
 Require Import core.panicking.
 
 (* pub const fn panic_fmt(fmt: fmt::Arguments<'_>) -> ! *)
@@ -18,3 +19,84 @@ Proof.
   constructor.
   run_symbolic.
 Admitted.
+
+(*
+pub enum AssertKind {
+    Eq,
+    Ne,
+    Match,
+}
+*)
+Module AssertKind.
+  Inductive t : Set :=
+  | Eq
+  | Ne
+  | Match.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "core::panicking::AssertKind";
+    φ x :=
+      match x with
+      | Eq => Value.StructTuple "core::panicking::AssertKind::Eq" []
+      | Ne => Value.StructTuple "core::panicking::AssertKind::Ne" []
+      | Match => Value.StructTuple "core::panicking::AssertKind::Match" []
+      end;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "core::panicking::AssertKind").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+
+  Lemma of_value_with_Eq :
+    Value.StructTuple "core::panicking::AssertKind::Eq" [] = φ Eq.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Eq : of_value.
+
+  Lemma of_value_with_Ne :
+    Value.StructTuple "core::panicking::AssertKind::Ne" [] = φ Ne.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Ne : of_value.
+
+  Lemma of_value_with_Match :
+    Value.StructTuple "core::panicking::AssertKind::Match" [] = φ Match.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Match : of_value.
+
+  Definition of_value_Eq :
+    OfValue.t (Value.StructTuple "core::panicking::AssertKind::Eq" []).
+  Proof. econstructor; apply of_value_with_Eq. Defined.
+  Smpl Add apply of_value_Eq : of_value.
+
+  Definition of_value_Ne :
+    OfValue.t (Value.StructTuple "core::panicking::AssertKind::Ne" []).
+  Proof. econstructor; apply of_value_with_Ne. Defined.
+  Smpl Add apply of_value_Ne : of_value.
+
+  Definition of_value_Match :
+    OfValue.t (Value.StructTuple "core::panicking::AssertKind::Match" []).
+  Proof. econstructor; apply of_value_with_Match. Defined.
+  Smpl Add apply of_value_Match : of_value.
+End AssertKind.
+
+(*
+pub fn assert_failed<T, U>(
+    kind: AssertKind,
+    left: &T,
+    right: &U,
+    args: Option<fmt::Arguments<'_>>,
+) -> !
+*)
+Instance run_assert_failed
+  (T : Set) `{Link T}
+  (U : Set) `{Link U}
+  (kind : AssertKind.t)
+  (left : Ref.t Pointer.Kind.Ref T)
+  (right : Ref.t Pointer.Kind.Ref U)
+  (args : option Arguments.t) :
+  Run.Trait
+    panicking.assert_failed [] [ Φ T; Φ U ] [φ kind; φ left; φ right; φ args]
+    Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Admitted.