Challenge 9: Safe abstractions for core::time::Duration
#72
Assignees
Labels
Challenge
Used to tag a challenge
Comments
feliperodri
changed the title
core::time::Duration
feliperodri
changed the title
core::time::Duration
|
I'm working on this challenge. Will keep you updated on any progress I make. |
|
@sgpthomas With #136 about to be merged, could you please create a separate PR closing this challenge, akin to #206? Thank you! |
Merged
github-merge-queue bot
pushed a commit
that referenced
this issue
Dec 11, 2024
…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 <[email protected]> Co-authored-by: Celina G. Val <[email protected]> Co-authored-by: Michael Tautschnig <[email protected]>
github-merge-queue bot
pushed a commit
that referenced
this issue
Dec 11, 2024
Resolves #72 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Challenge 9: Safe abstractions for core::time::Duration
The text was updated successfully, but these errors were encountered: