Add more links definitions for the gas

CoqOfRust/core/links/cmp.v

@@ -35,7 +35,7 @@ Proof.
   eapply Run.CallClosure. {
     apply (run_call_once compare (Ref.immediate _ v1, Ref.immediate _ v2)).
   }
-  intros [ordering |]; cbn; [|run_symbolic].
+  intros [ordering|]; run_symbolic.
   destruct ordering; run_symbolic.
 Defined.
 
@@ -110,8 +110,7 @@ Module Ord.
           {| Function2.run := run_cmp |}
       ).
     }
-    intros.
-    run_symbolic.
+    intros []; run_symbolic.
   Defined.
 
   Definition run_min {Self : Set} `{Link Self} (self other : Self)
@@ -146,8 +145,7 @@ Module Impl_Ord_for_u64.
       eapply Run.CallClosure. {
         apply (intrinsics.run_three_way_compare IntegerKind.U64).
       }
-      intros.
-      run_symbolic.
+      intros []; run_symbolic.
     }
   Defined.
 

CoqOfRust/core/links/intrinsics.v

@@ -9,3 +9,11 @@ Lemma run_three_way_compare (integer_kind : IntegerKind.t) (x y : Integer.t inte
   {{ intrinsics.three_way_compare [] [ Φ (Integer.t integer_kind) ] [ φ x; φ y ] 🔽 Ordering.t }}.
 Proof.
 Admitted.
+
+Lemma run_saturating_add (integer_kind : IntegerKind.t) (x y : Integer.t integer_kind) :
+  {{
+    intrinsics.saturating_add [] [ Φ (Integer.t integer_kind) ] [ φ x; φ y ] 🔽
+    Integer.t integer_kind
+  }}.
+Proof.
+Admitted.

CoqOfRust/core/links/option.v

@@ -2,12 +2,39 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
 
 Module Option.
-  Global Instance IsLink (A : Set) (_ : Link A) : Link (option A) := {
+  Global Instance IsLink (A : Set) `{Link A} : Link (option A) := {
     Φ := Ty.apply (Ty.path "core::option::Option") [] [Φ A];
     φ x :=
       match x with
       | None => Value.StructTuple "core::option::Option::None" []
       | Some x => Value.StructTuple "core::option::Option::Some" [φ x]
       end;
   }.
+
+  Lemma of_value_with_None {A : Set} `{Link A} :
+    Value.StructTuple "core::option::Option::None" [] =
+    φ (None (A := A)).
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_None : of_value.
+
+  Lemma of_value_with_Some {A : Set} `{Link A} (value : A) value' :
+    value' = φ value ->
+    Value.StructTuple "core::option::Option::Some" [value'] =
+    φ (Some value).
+  Proof. intros; subst; reflexivity. Qed.
+  Smpl Add apply of_value_with_Some : of_value.
+
+  Definition of_value_None {A : Set} `{Link A} :
+    OfValue.t (Value.StructTuple "core::option::Option::None" []).
+  Proof. eapply OfValue.Make with (A := option A); apply of_value_with_None. Defined.
+  Smpl Add eapply of_value_None : of_value.
+
+  Definition of_value_Some {A : Set} `{Link A} (value : A) value' :
+    value' = φ value ->
+    OfValue.t (Value.StructTuple "core::option::Option::Some" [value']).
+  Proof.
+    intros; eapply OfValue.Make with (A := option A).
+    apply of_value_with_Some; eassumption.
+  Defined.
+  Smpl Add eapply of_value_Some : of_value.
 End Option.

CoqOfRust/core/num/links/mod.v

@@ -0,0 +1,31 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.lib.
+Require Import CoqOfRust.links.M.
+Require Import core.num.mod.
+Require Import core.intrinsics.
+Require core.links.intrinsics.
+
+Import Run.
+
+Module Impl_u64.
+  Definition Self : Set := U64.t.
+
+  (*
+  pub const fn saturating_add(self, rhs: Self) -> Self {
+      intrinsics::saturating_add(self, rhs)
+  }
+  *)
+  Lemma run_saturating_add (self rhs: Self) :
+    {{ num.Impl_u64.saturating_add [] [] [ φ self; φ rhs ] 🔽 Self }}.
+  Proof.
+    run_symbolic.
+    eapply Run.CallPrimitiveGetFunction. {
+      eapply intrinsics.Function_saturating_add.
+    }
+    run_symbolic.
+    eapply Run.CallClosure. {
+      apply (intrinsics.run_saturating_add IntegerKind.U64).
+    }
+    intros []; run_symbolic.
+  Defined.
+End Impl_u64.

CoqOfRust/core/ops/links/function.v

@@ -43,8 +43,7 @@ Module Impl_FnOnce_for_Function2.
       eapply Run.CallClosure. {
         apply self.
       }
-      intros.
-      run_symbolic.
+      intros []; run_symbolic.
     }
   Defined.