5 ms·

The approach at the end of declaring invariants to the compiler so the compiler can eliminate panics seems accidentally genius. You can now add the same invaria

The approach at the end of declaring invariants to the compiler so the compiler can eliminate panics seems accidentally genius. You can now add the same invariants as panicking asserts at the end of each function, and the compiler will prove to you that your functions are upholding the invariants. And of course you can add more panicking asserts to show other claims to be true, all tested at compile time. You've basically built a little proof system. Sure, Rust is hardly the first language to include something like that and adoption of such systems tends to be ... spotty. But if it was reliable enough and had a better interface (that preferably allowed the rest of your program to sill have panics) this might be very useful for writing correct software.

jwatte 2y ago
For systems where correctness is actually important, not just a nice-to-have (in most systems, it's nice-to-have,) we have had an increasing number of options over the years. From tools like "spin" and "tla+" to proof assistants like Coq to full languages like Idris and Agda. Some of the stronger-typed languages already give us some of those benefits (Haskell, OCaml) and with restricted effects (like Haskell) we can even make the compiler do much of this work without it leaking into other parts of the program if we don't want it to.
haberman 2y ago
While I would love this to be true, I'm not sure that this design can statically prove anything. For an assert to fail, you would have to actually execute a code sequence that causes the invariant to be violated. I don't see how the compiler could prove at compile time that the invariants are upheld.
- wongarsu 2y ago
  An assert is just a fancy `if condition { panic(message) }`. If the optimizer can show that condition is always false, the panic is declared as dead code and eliminated. The post uses that to get the compiler to remove all panics to reduce the binary size. But you can also just check if panic code was generated (or associated code linked in), and if it was then the optimizer wasn't able to show that your assert can't happen. Of course this doesn't prove that the assert will happen. You would have to execute the code for that. But you can treat the fact that the optimizer couldn't eliminate your assert as failure, showing that either your code violates the assert, your preconditions in combination with the code aren't enough to show that the assert isn't violated, or the whole thing was too complicated for the optimizer to figure out and you have to restructure some code
  - haberman 2y ago
    Ah, I see what you are saying. Yes, if the optimizer is able to eliminate the postcondition check, I agree that it would constitute a proof that the code upholds the invariant. The big question is how much real-world code the optimizer would be capable of "solving" in this way. I wonder if most algorithms would eventually be solvable if you keep breaking them down into smaller pieces. Or if some would have some step of irreducible complexity that the optimizer cannot figure out, now matter how much you break it down.
    - saagarjha 2y ago
      Generally you run into the halting problem and whatnot real quick.
    - Yoric 2y ago
      I wonder if there is a simple way to stop compilation quickly, with a readable error message, if the optimizer isn't able to eliminate the check. edit: There is https://github.com/dtolnay/no-panic https://github.com/dtolnay/no-panic
      - vlovich123 2y ago
        > Functions that require some amount of optimization to prove that they do not panic may no longer compile in debug mode after being marked #[no_panic]. So you’re probably going to have to protect this with a cfg_attr to only apply the no_panic in release only.
        Yoric 2y ago
        Probably, yes. That or forcing compilation to always target release.
    - vlovich123 2y ago
      To be clear, the optimizer doesn’t uphold the post condition. It just says “the post condition is usable to elide other checks”. But if the condition itself is incorrect, the compiler will STILL elide those checks. If the compiler could prove the condition on its own it would have done so. That’s why that assert is named unchecked and is itself unsafe!
saghm 2y ago
This isn't quite the same, but it reminds me of something a bit less clever (and a lot less powerful) I came up with a little while back when writing some code to handle a binary format that used a lot of 32-bit integers that I needed to use for math on indexes in vectors. I was fairly confident that the code would never need to run on 16-bit platforms, but converting from a 32-bit integer to a usize in Rust technically is considered fallible due to the fact that you can't necessarily assume that a usize is more 16 bits, and frustrating `usize` only implements `TryFrom<u32>` rather than conditionally implementing `From<u32>` on 32-bit and 64-bit platforms. I wanted to avoid having to do any casting that could silently get messed up if I happened to switch any of the integer types I used later, but I also was irrationally upset at the idea of having to check at runtime for something that should be obvious at compile time. The solution I came up with was putting a static assertion that the target pointer width was either 32 or 64 bits inside the error-handling path, followed by marking the code path as `unreachable!()` that would never get executed (because either the error handling path wouldn't be taken, or the static assertion would stop the code from having been compiled in the first place. Even though this wasn't meaningfully different from just conditionally compiling to make sure the platform was suitable and then putting `unreachable!()` unconditionally in the error handling path, having the compile-time insertion locally in the spot where the error was being handled felt like I magically turned the runtime error into a compile-time one; it was quite literally possible to write it as a function that could be dropped into any codebase without having to make any other changes to ensure it was used safely.
- lilyball 2y ago
  What about just doing something like #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] #[inline(always)] const fn usize_to_u32(x: usize) -> u32 { x as u32 } and this way you can just call this function and you'll get a compile-time error (no such function) if you're on a 16-bit platform.
  - saghm 2y ago
    Even though I can visually verify that it's safe in this context, I really don't like casting integers as a rule when there's a reasonable alternative. The solution I came up with is pretty much equally readable in my opinion but has the distinction of not having code that might in other contexts look like it could silently have issues (compared to an `unreachable!()` macro which might also look sketchy but certainly wouldn't be quiet if it accidentally was used in the wrong spot). I also prefer having a compiler error explaining the invariant that's expected rather than a missing function (which could just as easily be due to a typo or something). You could put a `compile_error!()` invocation to conditionally compile when the pointer width isn't at least 32, but I'd argue that tilts the balance even more in favor of the solution I came up with; having a single item instead of two defined is more readable in my opinion. This wasn't a concern for me but I could also imagine some sort of linting being used to ensure that potentially lossy casts aren't done, and while it presumably could be manually suppressed, that also would just add to the noisiness.
Groxx 2y ago
>and the compiler will prove to you that your functions are upholding the invariants From the article and only vague background Rust knowledge, I'm under the impression that the opposite is true: the compiler does not prove that. Hence why it's "assert_unchecked" - you are informing the compiler that you know more than it does. You do get panics during debug, which is great for checking your assumptions, but that relies on you having adequate tests.
- tga_d 2y ago
  That's my understanding as well. The thing I was wondering as I read it: how difficult would it be for someone to make an extension or fork of Rust that allows annotating sufficient type information to prove these kinds of invariants, like F*?

jwatte 2y ago

For systems where correctness is actually important, not just a nice-to-have (in most systems, it's nice-to-have,) we have had an increasing number of options over the years. From tools like "spin" and "tla+" to proof assistants like Coq to full languages like Idris and Agda. Some of the stronger-typed languages already give us some of those benefits (Haskell, OCaml) and with restricted effects (like Haskell) we can even make the compiler do much of this work without it leaking into other parts of the program if we don't want it to.

haberman 2y ago

While I would love this to be true, I'm not sure that this design can statically prove anything. For an assert to fail, you would have to actually execute a code sequence that causes the invariant to be violated. I don't see how the compiler could prove at compile time that the invariants are upheld.

wongarsu 2y ago
An assert is just a fancy `if condition { panic(message) }`. If the optimizer can show that condition is always false, the panic is declared as dead code and eliminated. The post uses that to get the compiler to remove all panics to reduce the binary size. But you can also just check if panic code was generated (or associated code linked in), and if it was then the optimizer wasn't able to show that your assert can't happen. Of course this doesn't prove that the assert will happen. You would have to execute the code for that. But you can treat the fact that the optimizer couldn't eliminate your assert as failure, showing that either your code violates the assert, your preconditions in combination with the code aren't enough to show that the assert isn't violated, or the whole thing was too complicated for the optimizer to figure out and you have to restructure some code
- haberman 2y ago
  Ah, I see what you are saying. Yes, if the optimizer is able to eliminate the postcondition check, I agree that it would constitute a proof that the code upholds the invariant. The big question is how much real-world code the optimizer would be capable of "solving" in this way. I wonder if most algorithms would eventually be solvable if you keep breaking them down into smaller pieces. Or if some would have some step of irreducible complexity that the optimizer cannot figure out, now matter how much you break it down.
  - saagarjha 2y ago
    Generally you run into the halting problem and whatnot real quick.
  - Yoric 2y ago
    I wonder if there is a simple way to stop compilation quickly, with a readable error message, if the optimizer isn't able to eliminate the check. edit: There is https://github.com/dtolnay/no-panic https://github.com/dtolnay/no-panic
    - vlovich123 2y ago
      > Functions that require some amount of optimization to prove that they do not panic may no longer compile in debug mode after being marked #[no_panic]. So you’re probably going to have to protect this with a cfg_attr to only apply the no_panic in release only.
      - Yoric 2y ago
        Probably, yes. That or forcing compilation to always target release.
  - vlovich123 2y ago
    To be clear, the optimizer doesn’t uphold the post condition. It just says “the post condition is usable to elide other checks”. But if the condition itself is incorrect, the compiler will STILL elide those checks. If the compiler could prove the condition on its own it would have done so. That’s why that assert is named unchecked and is itself unsafe!

saghm 2y ago

This isn't quite the same, but it reminds me of something a bit less clever (and a lot less powerful) I came up with a little while back when writing some code to handle a binary format that used a lot of 32-bit integers that I needed to use for math on indexes in vectors. I was fairly confident that the code would never need to run on 16-bit platforms, but converting from a 32-bit integer to a usize in Rust technically is considered fallible due to the fact that you can't necessarily assume that a usize is more 16 bits, and frustrating `usize` only implements `TryFrom<u32>` rather than conditionally implementing `From<u32>` on 32-bit and 64-bit platforms. I wanted to avoid having to do any casting that could silently get messed up if I happened to switch any of the integer types I used later, but I also was irrationally upset at the idea of having to check at runtime for something that should be obvious at compile time. The solution I came up with was putting a static assertion that the target pointer width was either 32 or 64 bits inside the error-handling path, followed by marking the code path as `unreachable!()` that would never get executed (because either the error handling path wouldn't be taken, or the static assertion would stop the code from having been compiled in the first place. Even though this wasn't meaningfully different from just conditionally compiling to make sure the platform was suitable and then putting `unreachable!()` unconditionally in the error handling path, having the compile-time insertion locally in the spot where the error was being handled felt like I magically turned the runtime error into a compile-time one; it was quite literally possible to write it as a function that could be dropped into any codebase without having to make any other changes to ensure it was used safely.

lilyball 2y ago
What about just doing something like #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] #[inline(always)] const fn usize_to_u32(x: usize) -> u32 { x as u32 } and this way you can just call this function and you'll get a compile-time error (no such function) if you're on a 16-bit platform.
- saghm 2y ago
  Even though I can visually verify that it's safe in this context, I really don't like casting integers as a rule when there's a reasonable alternative. The solution I came up with is pretty much equally readable in my opinion but has the distinction of not having code that might in other contexts look like it could silently have issues (compared to an `unreachable!()` macro which might also look sketchy but certainly wouldn't be quiet if it accidentally was used in the wrong spot). I also prefer having a compiler error explaining the invariant that's expected rather than a missing function (which could just as easily be due to a typo or something). You could put a `compile_error!()` invocation to conditionally compile when the pointer width isn't at least 32, but I'd argue that tilts the balance even more in favor of the solution I came up with; having a single item instead of two defined is more readable in my opinion. This wasn't a concern for me but I could also imagine some sort of linting being used to ensure that potentially lossy casts aren't done, and while it presumably could be manually suppressed, that also would just add to the noisiness.

Groxx 2y ago

>and the compiler will prove to you that your functions are upholding the invariants From the article and only vague background Rust knowledge, I'm under the impression that the opposite is true: the compiler does not prove that. Hence why it's "assert_unchecked" - you are informing the compiler that you know more than it does. You do get panics during debug, which is great for checking your assumptions, but that relies on you having adequate tests.

tga_d 2y ago
That's my understanding as well. The thing I was wondering as I read it: how difficult would it be for someone to make an extension or fork of Rust that allows annotating sufficient type information to prove these kinds of invariants, like F*?