Add more links for system instructions

CoqOfRust/alloy_primitives/bits/links/address.v

@@ -24,16 +24,16 @@ Module Impl_Address.
     Address.t.
 
   (* pub fn from_word(word: FixedBytes<32>) -> Self *)
-  Instance run_from_word (word : fixed.FixedBytes.t {| Integer.value := 32 |}) :
+  Instance run_from_word (word : FixedBytes.t {| Integer.value := 32 |}) :
     Run.Trait
       bits.address.Impl_alloy_primitives_bits_address_Address.from_word [] [] [ φ word ]
       Self.
   Admitted.
 
   (* pub fn into_word(&self) -> FixedBytes<32> *)
-  Instance run_into_word (self : Address.t) :
+  Instance run_into_word (self : Ref.t Pointer.Kind.Ref Self) :
     Run.Trait
       bits.address.Impl_alloy_primitives_bits_address_Address.into_word [] [] [ φ self ]
-      (fixed.FixedBytes.t {| Integer.value := 32 |}).
+      (FixedBytes.t {| Integer.value := 32 |}).
   Admitted.
 End Impl_Address.

CoqOfRust/alloy_primitives/bits/links/fixed.v

@@ -1,35 +1,24 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import core.links.array.
+Require Import alloy_primitives.links.aliases.
+Require Export alloy_primitives.bits.links.fixed_FixedBytes.
 Require Import alloy_primitives.bits.fixed.
-
-(* pub struct FixedBytes<const N: usize>(pub [u8; N]); *)
-Module FixedBytes.
-  Parameter t : Usize.t -> Set.
-
-  Parameter to_value : forall {N: Usize.t}, t N -> Value.t.
-
-  Global Instance IsLink (N: Usize.t): Link (t N) := {
-    Φ := Ty.apply (Ty.path "alloy_primitives::bits::fixed::FixedBytes") [ φ N ] [];
-    φ := to_value;
-  }.
-
-  Definition of_ty (N' : Value.t) (N: Usize.t) :
-    N' = φ N ->
-    OfTy.t (Ty.apply (Ty.path "alloy_primitives::bits::fixed::FixedBytes") [ N' ] []).
-  Proof.
-    intros.
-    eapply OfTy.Make with (A := t N).
-    subst.
-    reflexivity.
-  Defined.
-  Smpl Add eapply of_ty : of_ty.
-End FixedBytes.
+Require Import core.convert.links.mod.
+Require Import core.links.array.
 
 Module Impl_FixedBytes.
   Definition Self (N: Usize.t) : Set :=
     FixedBytes.t N.
 
+  (* pub const ZERO: Self *)
+  Instance run_zero (N: Usize.t) :
+    Run.Trait
+      (bits.fixed.Impl_alloy_primitives_bits_fixed_FixedBytes_N.value_ZERO (φ N)) [] [] []
+      (Self N).
+  Proof.
+    constructor.
+  Admitted.
+
   (* pub fn new(bytes: [u8; N]) -> Self *)
   Instance run_new (N: Usize.t) (bytes: array.t U8.t N) :
     Run.Trait
@@ -40,3 +29,26 @@ Module Impl_FixedBytes.
     run_symbolic.
   Admitted.
 End Impl_FixedBytes.
+
+Module Impl_From_FixedBytes_32_for_U256.
+  Definition Self : Set :=
+    aliases.U256.t.
+
+  Definition run_from : From.Run_from aliases.U256.t (FixedBytes.t {| Integer.value := 32 |}).
+  Proof.
+    eexists.
+    { eapply IsTraitMethod.Defined.
+      { apply bits.fixed.Impl_core_convert_From_alloy_primitives_bits_fixed_FixedBytes_Usize_32_for_ruint_Uint_Usize_256_Usize_4.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      run_symbolic.
+      all: admit.
+    }
+  Admitted.
+
+  Instance run : From.Run aliases.U256.t (FixedBytes.t {| Integer.value := 32 |}) :=
+  {
+    From.from := run_from;
+  }.
+End Impl_From_FixedBytes_32_for_U256.

CoqOfRust/alloy_primitives/bits/links/fixed_FixedBytes.v

@@ -0,0 +1,25 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+(* pub struct FixedBytes<const N: usize>(pub [u8; N]); *)
+Module FixedBytes.
+  Parameter t : Usize.t -> Set.
+
+  Parameter to_value : forall {N: Usize.t}, t N -> Value.t.
+
+  Global Instance IsLink (N: Usize.t): Link (t N) := {
+    Φ := Ty.apply (Ty.path "alloy_primitives::bits::fixed::FixedBytes") [ φ N ] [];
+    φ := to_value;
+  }.
+
+  Definition of_ty (N' : Value.t) (N: Usize.t) :
+    N' = φ N ->
+    OfTy.t (Ty.apply (Ty.path "alloy_primitives::bits::fixed::FixedBytes") [ N' ] []).
+  Proof.
+    intros.
+    eapply OfTy.Make with (A := t N).
+    subst.
+    reflexivity.
+  Defined.
+  Smpl Add eapply of_ty : of_ty.
+End FixedBytes.

CoqOfRust/alloy_primitives/links/aliases.v

@@ -1,6 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import alloy_primitives.bits.links.fixed.
+Require Import alloy_primitives.bits.links.fixed_FixedBytes.
 Require Import alloy_primitives.signed.links.int.
 Require Import ruint.links.lib.
 

CoqOfRust/core/convert/links/mod.v

@@ -1,7 +1,7 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
 Require Import core.convert.mod.
-
+Require Import core.links.result.
 (*
 pub trait From<T>: Sized {
     fn from(value: T) -> Self;
@@ -17,7 +17,7 @@ Module From.
       Run.Trait method [] [] [ φ value ] Self
     ).
 
-  Class Run (Self : Set) {T : Set} `{Link Self} `{Link T} : Set := {
+  Class Run (Self : Set) (T : Set) `{Link Self} `{Link T} : Set := {
     from : Run_from Self T;
   }.
 End From.
@@ -33,11 +33,107 @@ Module Into.
 
   Definition Run_into (Self T : Set) `{Link Self} `{Link T} : Set :=
     TraitMethod.C (trait Self T) "into" (fun method =>
-      forall (self : Ref.t Pointer.Kind.Ref Self),
+      forall (self : Self),
         Run.Trait method [] [] [ φ self ] T
     ).
 
   Class Run (Self : Set) (T : Set) `{Link Self} `{Link T} : Set := {
     into : Run_into Self T;
   }.
 End Into.
+
+(*
+impl<T, U> Into<U> for T
+where
+    U: From<T>,
+*)
+Module Impl_Into_for_From_T.
+  Definition run_into
+    (T U : Set) `{Link T} `{Link U}
+    (run_From_for_U : From.Run U T) :
+    Into.Run_into T U.
+  Proof.
+    eexists.
+    { eapply IsTraitMethod.Defined.
+      { apply convert.Impl_core_convert_Into_where_core_convert_From_U_T_U_for_T.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      destruct run_From_for_U.
+      run_symbolic.
+    }
+  Defined.
+
+  Instance run
+    {T U : Set} `{Link T} `{Link U}
+    (run_From_for_U : From.Run U T) :
+    Into.Run T U :=
+  {
+    Into.into := run_into T U run_From_for_U;
+  }.
+End Impl_Into_for_From_T.
+
+(*
+pub trait AsRef<T: ?Sized> {
+    fn as_ref(&self) -> &T;
+}
+*)
+Module AsRef.
+  Definition trait (Self T : Set) `{Link Self} `{Link T} : TraitMethod.Header.t :=
+    ("core::convert::AsRef", [], [Φ T], Φ Self).
+
+  Definition Run_as_ref (Self T : Set) `{Link Self} `{Link T} : Set :=
+    TraitMethod.C (trait Self T) "as_ref" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+        Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref T)
+    ).
+
+  Class Run (Self : Set) (T : Set) `{Link Self} `{Link T} : Set := {
+    as_ref : Run_as_ref Self T;
+  }.
+End AsRef.
+
+(* impl<T> AsRef<[T]> for [T] *)
+Module Impl_AsRef_for_Slice.
+  Definition run_as_ref
+    (T : Set) `{Link T} :
+    AsRef.Run_as_ref (list T) (list T).
+  Proof.
+    eexists.
+    { eapply IsTraitMethod.Defined.
+      { apply convert.Impl_core_convert_AsRef_slice_T_for_slice_T.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      run_symbolic.
+    }
+  Defined.
+
+  Instance run
+    (T : Set) `{Link T} :
+    AsRef.Run (list T) (list T) :=
+  {
+    AsRef.as_ref := run_as_ref T;
+  }.
+End Impl_AsRef_for_Slice.
+
+(*
+pub trait TryFrom<T>: Sized {
+    type Error;
+    fn try_from(value: T) -> Result<Self, Self::Error>;
+}
+*)
+Module TryFrom.
+  Definition trait (Self T : Set) `{Link Self} `{Link T} : TraitMethod.Header.t :=
+    ("core::convert::TryFrom", [], [Φ T], Φ Self).
+
+  Definition Run_try_from (Self T Error : Set) `{Link Self} `{Link T} `{Link Error} : Set :=
+    TraitMethod.C (trait Self T) "try_from" (fun method =>
+      forall (value : T),
+        Run.Trait method [] [] [ φ value ] (Result.t Self Error)
+    ).
+
+  Class Run (Self : Set) (T : Set) (Error : Set) `{Link Self} `{Link T} `{Link Error} : Set := {
+    try_from : Run_try_from Self T Error;
+  }.
+End TryFrom.

CoqOfRust/core/convert/links/num.v

@@ -0,0 +1,29 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+Require Import core.convert.links.mod.
+Require Import core.convert.num.
+Require Import core.links.result.
+Require Import core.num.links.error.
+
+Module Impl_TryFrom_u64_for_usize.
+  Definition Self : Set :=
+    Usize.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_usize.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      run_symbolic.
+      instantiate (1 := Result.Ok _).
+      with_strategy transparent [φ] reflexivity.
+    }
+  Defined.
+
+  Instance run : TryFrom.Run Self U64.t TryFromIntError.t := {
+    TryFrom.try_from := run_try_from;
+  }.
+End Impl_TryFrom_u64_for_usize.

CoqOfRust/core/links/result.v

@@ -1,6 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
-
+Require Import core.result.
 Module Result.
   Inductive t {T E : Set} : Set :=
   | Ok : T -> t
@@ -26,3 +26,21 @@ Module Result.
   Defined.
   Smpl Add apply of_ty : of_ty.
 End Result.
+
+Module Impl_Result_T_E.
+  Definition Self (T E : Set) : Set :=
+    Result.t T E.
+
+  (* pub fn unwrap_or(self, default: T) -> T *)
+  Instance run_unwrap_or
+    (T E : Set) `{Link T} `{Link E}
+    (self : Self T E)
+    (default : T) :
+    Run.Trait
+      (result.Impl_core_result_Result_T_E.unwrap_or (Φ T) (Φ E)) [] [] [ φ self; φ default ]
+      T.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+End Impl_Result_T_E.

CoqOfRust/core/num/links/error.v

@@ -0,0 +1,19 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+Require Import core.num.error.
+
+(* pub struct TryFromIntError(/* private fields */); *)
+Module TryFromIntError.
+  Parameter t : Set.
+
+  Parameter to_value : t -> Value.t.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "core::num::error::TryFromIntError";
+    φ := to_value;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "core::num::error::TryFromIntError").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+End TryFromIntError.

CoqOfRust/core/num/links/mod.v

@@ -6,6 +6,22 @@ Require Import core.num.mod.
 Module Impl_u64.
   Definition Self : Set := U64.t.
 
+  (* pub const MIN: Self *)
+  Instance run_min :
+    Run.Trait num.Impl_u64.value_MIN [] [] [] (Ref.t Pointer.Kind.Raw Self).
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
+
+  (* pub const MAX: Self *)
+  Instance run_max :
+    Run.Trait num.Impl_u64.value_MAX [] [] [] (Ref.t Pointer.Kind.Raw Self).
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
+
   (* pub const fn saturating_add(self, rhs: Self) -> Self *)
   Instance run_saturating_add (self rhs: Self) :
     Run.Trait num.Impl_u64.saturating_add [] [] [ φ self; φ rhs ] Self.

CoqOfRust/lib/lib.v

@@ -246,14 +246,31 @@ Module BinOp.
     Definition shr : Value.t :=
       make_arithmetic Z.shiftr.
 
+    Definition make_bool_or_arithmetic
+      (bin_op_bool : bool -> bool -> bool)
+      (bin_op_Z : Z -> Z -> Z)
+      : Value.t :=
+      M.closure (fun args =>
+        match args with
+        | [Value.Bool b1; Value.Bool b2] => M.pure (Value.Bool (bin_op_bool b1 b2))
+        | [Value.Integer kind1 v1; Value.Integer kind2 v2] =>
+          if negb (IntegerKind.eqb kind1 kind2) then
+            M.impossible "expected the same kind of integers"
+          else
+            let z := bin_op_Z v1 v2 in
+            M.pure (Value.Integer kind1 (Integer.normalize_wrap kind1 z))
+        | _ => M.impossible "expected two values for bool or arithmetic"
+        end
+      ).
+
     Definition bit_xor : Value.t :=
-      make_arithmetic Z.lxor.
+      make_bool_or_arithmetic xorb Z.lxor.
 
     Definition bit_and : Value.t :=
-      make_arithmetic Z.land.
+      make_bool_or_arithmetic andb Z.land.
 
     Definition bit_or : Value.t :=
-      make_arithmetic Z.lor.
+      make_bool_or_arithmetic orb Z.lor.
   End Wrap.
 End BinOp.