Add extern_spec for PartialEq::eq on Option, Result and Box

Author: coord-e

std.rs

@@ -250,6 +250,13 @@ fn _extern_spec_box_new<T>(x: T) -> Box<T> where T: thrust_models::Model {
     Box::new(x)
 }
 
+#[thrust::extern_spec_fn]
+#[thrust::requires(true)]
+#[thrust::ensures(result == (x == y))]
+fn _extern_spec_box_partialeq_eq<T>(x: &Box<T>, y: &Box<T>) -> bool where T: thrust_models::Model + PartialEq {
+    <Box<T> as PartialEq>::eq(x, y)
+}
+
 #[thrust::extern_spec_fn]
 #[thrust::requires(true)]
 #[thrust::ensures(*x == ^y && *y == ^x)]
@@ -264,6 +271,13 @@ fn _extern_spec_std_mem_replace<T>(dest: &mut T, src: T) -> T where T: thrust_mo
     std::mem::replace(dest, src)
 }
 
+#[thrust::extern_spec_fn]
+#[thrust::requires(true)]
+#[thrust::ensures(result == (x == y))]
+fn _extern_spec_option_partialeq_eq<T>(x: &Option<T>, y: &Option<T>) -> bool where T: thrust_models::Model + PartialEq {
+    <Option<T> as PartialEq>::eq(x, y)
+}
+
 #[thrust::extern_spec_fn]
 #[thrust::requires(opt != std::option::Option::<T0>::None())]
 #[thrust::ensures(std::option::Option::<T0>::Some(result) == opt)]
@@ -353,6 +367,15 @@ fn _extern_spec_option_as_mut<T>(opt: &mut Option<T>) -> Option<&mut T> where T:
     Option::as_mut(opt)
 }
 
+#[thrust::extern_spec_fn]
+#[thrust::requires(true)]
+#[thrust::ensures(result == (x == y))]
+fn _extern_spec_result_partialeq_eq<T, E>(x: &Result<T, E>, y: &Result<T, E>) -> bool
+  where T: thrust_models::Model + PartialEq, E: thrust_models::Model + PartialEq
+{
+    <Result<T, E> as PartialEq>::eq(x, y)
+}
+
 #[thrust::extern_spec_fn]
 #[thrust::requires(exists x:T0. res == std::result::Result::<T0, T1>::Ok(x))]
 #[thrust::ensures(std::result::Result::<T0, T1>::Ok(result) == res)]