Make unsafe keyword docs less confusing

[gregschmit]

This sentence stuck out to me as odd (emphasis mine):

...or the unsafe block could be inside an unsafe fn and use its own proof obligations to discharge the proof obligations of its callees.

I think it means to say that it would use its own proof obligations to discharge the proof obligations of its callers, because it would be the calling functions ("callers") that normally have the proof obligation that the callee has discharged by using an unsafe block.

Am I missing something?

[ehuss]

Hm, yea, the use of "callee" doesn't seem right, at least with my understanding in a caller/callee relationship of a function, the callee is the function itself.

However, I've had to re-read this sentence about a dozen times to try to make sure it is clear in my head and I'm thinking some of my struggle is the use of "its" twice. That makes me need to think a little harder to understand which "it" is being referred to, and the relationship.

I'm wondering, does the following seem clearer to you?

Suggested change

	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 callers.
	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 the unsafe block can use the safety requirements the unsafe function imposes on its callers to discharge the proof obligations of the unsafe block.

[gregschmit]

I'm not totally sure that's better, because the last part references ...to discharge the proof obligations of the unsafe block, when really I believe the sentence is trying to address the discharge of the proof obligations of the callers, and saying that the unsafe block discharges their proof obligations. In other words, normally you have (with an unsafe fn):

1. Safety requirements of unsafe fn, which normally are met by the:
2. Proof obligation of the caller(s)

In the case of using an unsafe block inside an unsafe fn we have an additional:

3. Proof obligation of the unsafe block, which discharges the proof obligation of the callers (2).

Also, the unsafe block would not be using the safety requirements the unsafe function imposes on its callers; rather, it's using its own proof obligations.

We could replace a couple of the "its" like this:

Suggested change

	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 callers.
	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 the block's own proof obligations to discharge the proof obligations of the `unsafe fn`'s callers.

[mattheww]

I think this paragraph is talking about the case where the unsafe block contains calls to unsafe functions, and when it says "callees" it's talking about those unsafe functions.

If that's right, "callees" was correct but "its own proof obligations" should instead have referred to the block's parent function's proof obligations.

I suggest writing something like

"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 in the block."

[ehuss]

Oh, that does seem to make more sense to me. FWIW, I am not well-versed in formal methods.

cc @RalfJung in case you have a chance to clarify. Does @mattheww's interpretation seem correct?

[RalfJung]

I think it means to say that it would use its own proof obligations to discharge the proof obligations of its callers, because it would be the calling functions ("callers") that normally have the proof obligation that the callee has discharged by using an unsafe block.

How could a block discharge it's callers proof obligations? I don't understand what that would even mean. callers discharge callee's proof obligations, not vice versa. (At least when talking about preconditions, which are usually the proof obligations we talk about here.)

get_unchecked has a proof obligation: the index must be in-bounds. When you write an unsafe fn like

/// Unsafe precondition: `idx < 4`
unsafe fn silly_example(slice: &[u8], idx: usize) {
  assert!(slice.len() >= 4);
  unsafe {
    slice.get_unchecked(idx);
  }
}

then you are using the idx < 4 (the proof obligation of the surrounding unsafe fn) to discharge the "idx in bounds" (the proof obligation of the callee).

What @mattheww wrote sounds good.

[gregschmit]

I think it means to say that it would use its own proof obligations to discharge the proof obligations of its callers, because it would be the calling functions ("callers") that normally have the proof obligation that the callee has discharged by using an unsafe block.

How could a block discharge it's callers proof obligations? I don't understand what that would even mean. callers discharge callee's proof obligations, not vice versa. (At least when talking about preconditions, which are usually the proof obligations we talk about here.)

get_unchecked has a proof obligation: the index must be in-bounds. When you write an unsafe fn like

/// Unsafe precondition: `idx < 4`
unsafe fn silly_example(slice: &[u8], idx: usize) {
  assert!(slice.len() >= 4);
  unsafe {
    slice.get_unchecked(idx);
  }
}

then you are using the idx < 4 (the proof obligation of the surrounding unsafe fn) to discharge the "idx in bounds" (the proof obligation of the callee).

What @mattheww wrote sounds good.

Ohh! Then in that case I totally misunderstood the sentence. I was mistaken, thinking it was trying to communicate that the unsafe block within the unsafe fn was discharging the proof obligations of the callers. Yeah your last edit makes it clearer IMO.

[RalfJung]

Looking good, thanks for bringing this up and working with us on a less confusing wording!

@bors r+ rollup

[RalfJung]

... oh, this is the reference. Let's wait for @ehuss to merge this then. :)

[ehuss]

Thank you everyone!