From 3c3c084d034f8a58e3812bbc70cbe7c300aa77a5 Mon Sep 17 00:00:00 2001 From: "Gregory N. Schmit" Date: Sat, 8 Jul 2023 22:46:20 -0500 Subject: [PATCH 1/2] Clarify which proof obligations are referenced. Co-authored-by: Ralf Jung --- src/unsafe-keyword.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/unsafe-keyword.md b/src/unsafe-keyword.md index 5fa5deea6..7eb6fa0c2 100644 --- a/src/unsafe-keyword.md +++ b/src/unsafe-keyword.md @@ -27,9 +27,9 @@ this can be changed by enabling the [`unsafe_op_in_unsafe_fn`] lint. By putting operations into an unsafe block, the programmer states that they have taken care of satisfying the extra safety conditions of all operations inside that block. Unsafe blocks are the logical dual to unsafe functions: -where unsafe functions define a proof obligation that callers must uphold, unsafe blocks state that all relevant proof obligations have been discharged. +where unsafe functions define a proof obligation that callers must uphold, unsafe blocks state that all relevant proof obligations of functions or operations called inside the block have been discharged. There are many ways to discharge proof obligations; -for example, there could be run-time checks or data structure invariants that guarantee that certain properties are definitely true, or the unsafe block could be inside an `unsafe fn` and use its own proof obligations to discharge the proof obligations of its callees. +for example, there could be run-time checks or data structure invariants that guarantee that certain properties are definitely true, or the unsafe block could be inside an `unsafe fn`, in which case the block can use the proof obligations of that function to discharge the proof obligations of any unsafe functions called inside the block. Unsafe blocks are used to wrap foreign libraries, make direct use of hardware or implement features not directly present in the language. For example, Rust provides the language features necessary to implement memory-safe concurrency in the language but the implementation of threads and message passing in the standard library uses unsafe blocks. From 451a8e4542cb6500a7aca9de5902075e6c8ec188 Mon Sep 17 00:00:00 2001 From: Greg Schmit <14255284+gregschmit@users.noreply.github.com> Date: Tue, 18 Jul 2023 22:27:30 -0500 Subject: [PATCH 2/2] Improve wording of unsafe proof obligations. Co-authored-by: Ralf Jung --- src/unsafe-keyword.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/unsafe-keyword.md b/src/unsafe-keyword.md index 7eb6fa0c2..a29fc9432 100644 --- a/src/unsafe-keyword.md +++ b/src/unsafe-keyword.md @@ -29,7 +29,7 @@ By putting operations into an unsafe block, the programmer states that they have Unsafe blocks are the logical dual to unsafe functions: where unsafe functions define a proof obligation that callers must uphold, unsafe blocks state that all relevant proof obligations of functions or operations called inside the block have been discharged. There are many ways to discharge proof obligations; -for example, there could be run-time checks or data structure invariants that guarantee that certain properties are definitely true, or the unsafe block could be inside an `unsafe fn`, in which case the block can use the proof obligations of that function to discharge the proof obligations of any unsafe functions called inside the block. +for example, there could be run-time checks or data structure invariants that guarantee that certain properties are definitely true, or the unsafe block could be inside an `unsafe fn`, in which case the block can use the proof obligations of that function to discharge the proof obligations arising inside the block. Unsafe blocks are used to wrap foreign libraries, make direct use of hardware or implement features not directly present in the language. For example, Rust provides the language features necessary to implement memory-safe concurrency in the language but the implementation of threads and message passing in the standard library uses unsafe blocks.