Write contracts + pre/post conditions for all unsafe methods in duration

[sgpthomas]

Resolves#72

We added invariants for Nanoseconds and Duration to match the safety conditions for those types.

We add safety requirements to the following methods:

• new, from_secs, from_millis, from_micros, from_nanos, as_secs, as_millis, as_micros, as_nanos, subsec_millis, subsec_micros, subsec_nanos, checked_add, checked_sub, checked_mul, checked_div

We additionally add correctness conditions to the following methods:

• from_secs, as_secs, subsec_millis, subsec_micros, subsec_nanos, as_millis, as_micros

Support for kani::Invariant depends on #87. For the interim we implemented a proxy trait TempInvariant that exposes the same is_safe method. We will update this once #87 is merged.

While the safety check for Duration::as_nanos() succeeds, we ran into timeouts for Duration::as_nanos() when we tried to use a correctness contract and we're looking for advice on how to speed up that verification time. We were able to prove it for u16::MAX, but hit timeouts for larger numbers.

We are unsure if the pre-conditions for Duration::new() are acceptable because they limit the range of values that you can call Duration::new() with. However, we think it's reasonable since we limit the values to values that don't panic. Let us know if this is a thing that we should change.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

That's awesome! Thank you

[celinval]

Awesome! Thanks

[tautschnig]

I don't think we should have anything other than true as a requires clause on safe functions.