As you are well aware, this is an inappropriate summary of the safety approach that's generally used by the Rust ecosystem.
2 Likes
Apology for my ambiguity. I mean (in my understanding of what they are doing) they do not have both public and internal spec. They have only one spec, and that spec indicates the initialization before calling. Based on that spec, they cannot verify Vec::split_off.
The suggestion may out of topic of this thread, and require many efforts thinking it. I would post my suggestions if I have a proper one.
1 Like
Oh I see. Indeed, they'll have to deal with this issue. That's probably going to help safety contracts make progress, because I believe they've been blind to this problem for the longest time now.
1 Like
Good point, I've refined it.
You are still claiming that by design, safe code can cause UB. I consider this an incorrect claim, dropping key parts of the truth. I don't know why you are doing that but to me it seems like you want this to sound more dramatic than it is. I would appreciate if you could prioritize accuracy over dramatic effect.
The example you have in mind involves unsafe code.
2 Likes
Then what would be a correct claim? Here are some equivalent formulations of an accurate description of the truth based on prior discussions:
- Safe code can cause UB outside its dependencies
- Safe code cannot cause UB in its dependencies
- Safe clients cannot cause UB (that's the formulation I used in the Rustonomicon)
Maybe you think about an orthogonal claim, namely that safe code cannot have UB. This claim is useful in the context of the type system (it defines what code must be unsafe), but it is useless in the context of verification (which this thread is about). What matters for verification is the location of the soundness bug, not the location of the UB. To review a program for soundness, you have to review safe code.
Or maybe you think that safe code means safe program? By safe code I mean a piece of code that doesn't contain an unsafe block, an unsafe impl, or an unsafe attribute, I don't mean a whole program (because then it would be just about the soundness of the type system, while here I'm talking about the encapsulation property of the type system, which Rust is only partially implementing by design).
There's a chain of causes for the UB that involves some safe code that doesn't implement its expected contract, and some unsafe code that relies on the safe code implementing its contract. Together they cause UB. When A+B causes C, it is misleading to say "A causes C".
To review a program for soundness, you have to review safe code.
You have to review the safe code that unsafe code relies on, indeed.
By safe code I mean a piece of code that doesn't contain an unsafe block, an unsafe impl, or an unsafe attribute
I agree with that definition.
3 Likes
I've explained why this view misses an important detail here. Not all nodes of the chain of causes are similarly at fault. We can categorize all functions of an execution of a program in 6 categories:
| Precondition | Postcondition | Explanation |
|---|---|---|
| Satisfied | Satisfied | Does not participate to a chain |
| Satisfied | Violated | Creates a chain (bug) |
| Violated | Violated | Participates to a chain |
| Violated | Satisfied | Ends a chain without UB |
| Violated | N/A | Ends a chain with UB |
| Satisfied | N/A | Creates and ends a chain with UB (bug) |
What you say is that all nodes in a chain (creation, participation, and final UB) are equally responsible. What I say is that only creation nodes are responsible, all other nodes have a violated precondition, so they are not at fault. In particular a correct unsafe function does not cause the UB it has.
Maybe this is just a terminology issue, but I believe my terminology of "cause" and "bug" is the most common one. If a function fails to satisfy its postcondition because its precondition is violated, then I don't think we should call this a bug.
So in my opinion, what's misleading is to say that "A+B causes C", when B is actually correct (has no bug), at least in the context of program verification. Maybe there are other contexts where it's meaningful, but they don't come to mind right now.
It's misleading to call a function "correct" when its behavior is wrong (or worse, undefined) due to using a buggy dependency.
The bug is in the calling unsafe block, not in the called unsafe function. If an unsafe function has its preconditions violated, there must have been some unsafe block earlier that called the function with unsatisfied pre-conditions, and that calling code is buggy.
2 Likes
Your terminology fails to accurate reflect a very important point: it takes unsafe code to elevate buggy code to UB. I think that point is so fundamental to how Rust works that we should not use terminology which actively tries to hide this point.
We are talking about the situation where unsafe code relies on a safe dependency for correctness. For instance, imagine unsafe code relying on is_aligned. If is_aligned is buggy, and if unsafe code relies on its correctness, there could be UB. The only bug is in safe code. But unsafe code still is involved in turning this bug into UB.
3 Likes
Sure, I was just responding to a statement that talked about a completely correct unsafe function whose pre-conditions were violated, which is a different case. Of course the bug isn't in that function (or in the function's dependencies), but in whatever unsafe block called it with invalid pre-conditions (or in that block's other dependencies used earlier).
Arguably if we implemented is_aligned as always returning true, the bug would be in is_aligned, not in the unsafe code that relies on is_aligned. After all, to fix the problem, we'd change is_aligned and nothing else.
But it takes unsafe code to elevate that bug to UB.
1 Like
I agree with all that but this scenario has nothing to do with the statement I was responding to. Here, the function we're talking about (the one that calls is_aligned etc) presumably didn't have its pre-conditions violated, so it's a different scenario.
I described what I understood to be the scenario that we were discussing in this thread when you joined the conversation. It seems you are thinking of a different scenario but that wasn't what @ia0 and me were in disagreement about.
1 Like
Here is what I was responding to:
If this is the question, and this is the scenario:
I believe the most accurate description is "a verified code can never cause UB in any verified usages" when Rust has contract infrastructures. And the negation of any part can lead to UB, including:
-
not-verified code with verified usages
Buggy
is_aligned, while the unsafe usage depends on its alignness post-condition -
verified code with not-verified usages
Correct
is_aligned, while the unsafe usage does not depend on its post-condition and raise UBs
And a certain code being "not-verified" can result from multiple reasons:
- a safe function, while it fails to fulfill its post-condition
- an unsafe operation, while it fails to fulfill this operation's pre-condition
When Rust has contract infrastructure, the only difference between safe and unsafe functions is that safe functions do not have explicit pre-conditions (except for type invariants), while unsafe functions have.
2 Likes
That's covered by the orthogonal claim I was talking about:
If there's UB, then there's unsafe code involved. That's the soundness property of the type system. We can say even more, if there's UB, then the code where there's UB is unsafe. In my categorization of functions, it would be: "Ends a chain with UB" can only happen in unsafe code.
Maybe you would prefer this formulation:
- Safe code can only cause UB in unsafe code outside its dependencies.
But this is simply a corollary of the following properties:
- Safe code cannot have UB (soundness of the type system).
- Safe code cannot cause UB in its dependencies (Rust-style encapsulation of the type system).
A type system with proper encapsulation (like the unsafe mental model) would have the following property:
- Safe code cannot cause UB.
But as explained in other discussions, proper encapsulation has a non-negligible cost on ergonomics: too much unsafe, not clear what to guarantee, programmers are not mathematicians, etc. This is why Rust made the design decision of only having client-encapsulation, thus letting safe code cause UB outside its dependencies.
Yes, that's one of the reasons I'm not pushing for robust, because unsafe and robust in APIs will be made redundant by contracts and type-hygiene (values must be well-typed):
- A function is
unsafeif and only if it has a non-trivial#[requires] - A function is
robustif and only if it has a non-trivial#[ensures]
Thinking about it, this "safety-claim" is not just a corollary of soundness and client-encapsulation. It is actually equivalent to them, under the "unsafe-tautology" assumption that unsafe code can cause UB everywhere.
We essentially have the following partitioning of "X can cause UB in Y"[1]:
| can cause UB in | safe code. | unsafe code. | |
|---|---|---|---|
| Safe code | Never | Outside dependencies | (safety-claim) |
| Unsafe code | Always | Always | (unsafe-tautology) |
| (soundness) | (client-encapsulation) |
We can read this table by rows or by columns, giving the 2 equivalent versions. The second row is an assumption and not part of the reading.
When reading by columns, we are essentially reading the 2 top cells:
- Safe code can never cause UB in safe code. (soundness)
- Safe code can only cause UB in unsafe code outside its dependencies. (client-encapsulation)
When reading by rows, we are essentially reading the first row:
- Safe code can never cause UB in safe code and can only cause UB in unsafe code outside its dependencies. (safety-claim)
So I guess I can see how the safety-claim statement is superior. It captures both soundness and client-encapsulation (assuming unsafe-tautology).
In case of multiple root causes (with my terminology of "root cause"), we merge them into "safe code" if they are all in "safe code", and "unsafe code" if at least one is in "unsafe code" ↩︎
Given that we are discussing this for the n-th time, it seems unlikely that we will agree on the terminology now.
But everyone else reading along should realize that "safe code can cause UB" requires a non-standard "unsafe mental model" and very specific definitions of the term "can cause", and safe code cannot cause UB in the usual sense that most people use those terms. What happens is that unsafe code can rely on the correctness of safe code if it invokes a concrete safe function (such as ptr::is_aligned), so if you do an unsafe code audit, you may find yourself auditing safe code eventually. Many people find this surprising the first time they hear about it, but then quickly find it natural as there's not really a practical alternative.
I find the concept of a "robust function" useful, and your term for that is better than "super-safe" which we sometimes used for that concept before you shared your mental model. But to conclude from this that "safe code can cause UB" is going too far.
4 Likes