…ion (#136) 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. --------- Co-authored-by: Cole Vick <cole.d.vick@gmail.com> Co-authored-by: Celina G. Val <celinval@amazon.com> Co-authored-by: Michael Tautschnig <tautschn@amazon.com>

Challenge 9: Safe abstractions for core::time::Duration #72

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Challenge 9: Safe abstractions for `core::time::Duration` #72