3 ms·

> In particular, you could have unsafe code in crate A, whose data are then used by crate B. Is this backwards? If B consumes data from A then to me that does

> In particular, you could have unsafe code in crate A, whose data are then used by crate B. Is this backwards? If B consumes data from A then to me that does not imply that A depends on anything from B; for a more concrete example that sentence reads to me like A is basically "throwing data over the wall" to B and whatever B does with said data is of no relevance to A. As a result, if B changes that shouldn't affect A. Also for what it's worth I get the impression you and treyd might be talking about slightly different things when talking about whether unsafe code composes. I believe treyd is referring to the RustBelt series of papers [0, 1], for which the statement "unsafe code composes" means (at a high level) that adding a module with a memory-safe API to a memory-safe system will result in a memory-safe system as long as the implementation upholds the safe semantics. Yes, the last bit can be a rather significant caveat, as you said. What you're talking about seems more along the lines of needing to look beyond the boundaries of unsafe blocks to prove that the unsafe block upholds its invariants, which is also true. I think you only need to check within whatever safe encapsulation boundary is relevant, though, rather than globally. [0]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf [1]: https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf

toast0 14d ago
> Is this backwards? If B consumes data from A then to me that does not imply that A depends on anything from B; for a more concrete example that sentence reads to me like A is basically "throwing data over the wall" to B and whatever B does with said data is of no relevance to A. As a result, if B changes that shouldn't affect A. This is a specifically crafted bad idea, but you could have module A use unsafe to craft a Vec<u8> that is safe to use to read or write, but not to grow or shrink. You declare an invariant that the receiver shalt not grow or shrink the Vec. If B only reads and write, you're good. But if a future B breaks the invariant, bad things happen. As I said, specifically a bad idea; there's a much better type to use if the thing can't grow or shrink... No real world example, because I don't think we've run into memory safety issues with unsafe in the Rust code base I work in... but we only use unsafe where it's required (syscalls and other FFI).
- aw1621107 14d ago
  Hrm, I had assumed that A was providing a safe API, in which case I think A would be considered "at fault".
  - toast0 14d ago
    Sure, A is at fault, but it only broke when B changed behavior.
    - aw1621107 13d ago
      Fair. I suppose that even in such a scenario you shouldn't need truly global analysis to prove safety - in principle an analysis of A should reveal the soundness precondition on a safe API - though that's probably easier said than done.

toast0 14d ago

> Is this backwards? If B consumes data from A then to me that does not imply that A depends on anything from B; for a more concrete example that sentence reads to me like A is basically "throwing data over the wall" to B and whatever B does with said data is of no relevance to A. As a result, if B changes that shouldn't affect A. This is a specifically crafted bad idea, but you could have module A use unsafe to craft a Vec<u8> that is safe to use to read or write, but not to grow or shrink. You declare an invariant that the receiver shalt not grow or shrink the Vec. If B only reads and write, you're good. But if a future B breaks the invariant, bad things happen. As I said, specifically a bad idea; there's a much better type to use if the thing can't grow or shrink... No real world example, because I don't think we've run into memory safety issues with unsafe in the Rust code base I work in... but we only use unsafe where it's required (syscalls and other FFI).

aw1621107 14d ago
Hrm, I had assumed that A was providing a safe API, in which case I think A would be considered "at fault".
- toast0 14d ago
  Sure, A is at fault, but it only broke when B changed behavior.
  - aw1621107 13d ago
    Fair. I suppose that even in such a scenario you shouldn't need truly global analysis to prove safety - in principle an analysis of A should reveal the soundness precondition on a safe API - though that's probably easier said than done.