Remove Kani harnesses from time::Duration that autoharness takes care of

Author: tautschnig

.github/workflows/kani.yml

@@ -74,13 +74,15 @@ jobs:
           submodules: true
 
       # Step 2: Run Kani autoharness on the std library for selected functions.
-      # Uses "--include-pattern no::such::function" to make sure we do not try
-      # to run across all possible functions as that may take a lot longer than
-      # expected
+      # Uses "--include-pattern" to make sure we do not try to run across all
+      # possible functions as that may take a lot longer than expected
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
-            --include-pattern no:such::function:: \
+            --include-pattern time::Duration::from_micros \
+            --include-pattern time::Duration::from_millis \
+            --include-pattern time::Duration::from_nanos \
+            --include-pattern time::Duration::from_secs \
             --jobs=3 --output-format=terse
 
   run-kani-list:

library/core/src/time.rs

@@ -1756,30 +1756,6 @@ pub mod duration_verify {
         let _ = Duration::new(secs, nanos);
     }
 
-    #[kani::proof_for_contract(Duration::from_secs)]
-    fn duration_from_secs() {
-        let secs = kani::any::<u64>();
-        let _ = Duration::from_secs(secs);
-    }
-
-    #[kani::proof_for_contract(Duration::from_millis)]
-    fn duration_from_millis() {
-        let ms = kani::any::<u64>();
-        let _ = Duration::from_millis(ms);
-    }
-
-    #[kani::proof_for_contract(Duration::from_micros)]
-    fn duration_from_micros() {
-        let micros = kani::any::<u64>();
-        let _ = Duration::from_micros(micros);
-    }
-
-    #[kani::proof_for_contract(Duration::from_nanos)]
-    fn duration_from_nanos() {
-        let nanos = kani::any::<u64>();
-        let _ = Duration::from_nanos(nanos);
-    }
-
     #[kani::proof_for_contract(Duration::as_secs)]
     fn duration_as_secs() {
         let dur = safe_duration();