From 71c27d8d79a5290c7356dfae3b920aec02275c89 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Tue, 20 Aug 2024 14:23:43 -0400 Subject: [PATCH 1/3] Adds challenge for core::time::Duration Signed-off-by: Felipe R. Monteiro --- doc/src/SUMMARY.md | 3 +- doc/src/challenges/0009-duration.md | 72 +++++++++++++++++++++++++++++ 2 files changed, 74 insertions(+), 1 deletion(-) create mode 100644 doc/src/challenges/0009-duration.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index bb064448efe87..de82e15a77aff 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -18,4 +18,5 @@ - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md) - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) - [Inductive data type](./challenges/0005-linked-list.md) - - [Contracts for SmallSort](./challenges/0008-smallsort.md) \ No newline at end of file + - [Contracts for SmallSort](./challenges/0008-smallsort.md) + - [Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) \ No newline at end of file diff --git a/doc/src/challenges/0009-duration.md b/doc/src/challenges/0009-duration.md new file mode 100644 index 0000000000000..addd2802de14c --- /dev/null +++ b/doc/src/challenges/0009-duration.md @@ -0,0 +1,72 @@ +# Challenge 9: Safe abstractions for `core::time::Duration` + +- **Status:** Open +- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/) +- **Start date:** *2024-08-20* +- **End date:** *2024-12-20* + +------------------- + + +## Goal + +In this challenge, the goal is to write function contracts for `core::time::Duration` that can be used as safe abstractions. +Even though the majority of `Duration` methods are safe, many of them are safe abstractions over unsafe code. + +For instance, the `new` method is implemented as follows in v1.3.0: +```rust +pub const fn new(secs: u64, nanos: u32) -> Duration { + if nanos < NANOS_PER_SEC { + // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range + Duration { secs, nanos: unsafe { Nanoseconds(nanos) } } + } else { + let secs = match secs.checked_add((nanos / NANOS_PER_SEC) as u64) { + Some(secs) => secs, + None => panic!("overflow in Duration::new"), + }; + let nanos = nanos % NANOS_PER_SEC; + // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range + Duration { secs, nanos: unsafe { Nanoseconds(nanos) } } + } +} +``` + +### Success Criteria + +Write contracts for the following public functions. + +1. `Duration::new(secs: u64, nanos: u32) -> Duration` +2. `Duration::from_secs(secs: u64) -> Duration` +3. `Duration::from_millis(millis: u64) -> Duration` +4. `Duration::from_micros(micros: u64) -> Duration` +5. `Duration::from_nanos(nanos: u64) -> Duration` + +6. `Duration::as_secs(&self) -> u64` +7. `Duration::as_millis(&self) -> u128` +8. `Duration::as_micros(&self) -> u128` +9. `Duration::as_nanos(&self) -> u128` +10. `Duration::subsec_millis(&self) -> u32` +11. `Duration::subsec_micros(&self) -> u32` +12. `Duration::subsec_nanos(&self) -> u32` + +13. `Duration::checked_add(&self, rhs: Duration) -> Option` +14. `Duration::checked_sub(&self, rhs: Duration) -> Option` +15. `Duration::checked_mul(&self, rhs: u32) -> Option` +16. `Duration::checked_div(&self, rhs: u32) -> Option` + +The memory safety and the contracts of the above listed functions must be verified +for all possible input values. + +### List of UBs + +In addition to any properties called out as `SAFETY` comments in the source +code, +all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory. +* Mutating immutable bytes. +* Producing an invalid value + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. From 9404048c46a63253c59705bbe332d6b16d8fb032 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sat, 24 Aug 2024 21:59:39 -0400 Subject: [PATCH 2/3] Adds type invariant to success criteria Signed-off-by: Felipe R. Monteiro --- doc/src/SUMMARY.md | 2 +- doc/src/challenges/0009-duration.md | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index de82e15a77aff..2a552bebb69fb 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -19,4 +19,4 @@ - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) - [Inductive data type](./challenges/0005-linked-list.md) - [Contracts for SmallSort](./challenges/0008-smallsort.md) - - [Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) \ No newline at end of file + - [Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) diff --git a/doc/src/challenges/0009-duration.md b/doc/src/challenges/0009-duration.md index addd2802de14c..e466a388fb9b0 100644 --- a/doc/src/challenges/0009-duration.md +++ b/doc/src/challenges/0009-duration.md @@ -1,7 +1,7 @@ # Challenge 9: Safe abstractions for `core::time::Duration` - **Status:** Open -- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/) +- **Tracking Issue:** [#72](https://github.com/model-checking/verify-rust-std/issues/72) - **Start date:** *2024-08-20* - **End date:** *2024-12-20* @@ -10,7 +10,7 @@ ## Goal -In this challenge, the goal is to write function contracts for `core::time::Duration` that can be used as safe abstractions. +Write function contracts for `core::time::Duration` that can be used as safe abstractions. Even though the majority of `Duration` methods are safe, many of them are safe abstractions over unsafe code. For instance, the `new` method is implemented as follows in v1.3.0: @@ -33,7 +33,7 @@ pub const fn new(secs: u64, nanos: u32) -> Duration { ### Success Criteria -Write contracts for the following public functions. +Write a type invariant for the struct `Duration`. Write function contracts for the following public functions. 1. `Duration::new(secs: u64, nanos: u32) -> Duration` 2. `Duration::from_secs(secs: u64) -> Duration` From 7d0b5bd43177483845757181d9f3b809499e0a21 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Tue, 27 Aug 2024 12:54:33 -0400 Subject: [PATCH 3/3] Add link to invariants in Kani Signed-off-by: Felipe R. Monteiro --- doc/src/challenges/0009-duration.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0009-duration.md b/doc/src/challenges/0009-duration.md index e466a388fb9b0..e2af60ec6c1bb 100644 --- a/doc/src/challenges/0009-duration.md +++ b/doc/src/challenges/0009-duration.md @@ -33,7 +33,7 @@ pub const fn new(secs: u64, nanos: u32) -> Duration { ### Success Criteria -Write a type invariant for the struct `Duration`. Write function contracts for the following public functions. +Write a [type invariant](https://model-checking.github.io/kani/crates/doc/kani/derive.Invariant.html) for the struct `Duration`. Write function contracts for the following public functions. 1. `Duration::new(secs: u64, nanos: u32) -> Duration` 2. `Duration::from_secs(secs: u64) -> Duration`