Hacker News Reader

Comment by wongarsu | Hacker News Reader

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.

View on HN

>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.

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*?

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.

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.

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.

Oops, I flipped the conversion here, that should have been `u32_to_usize()`.

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.

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.

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

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.

Generally you run into the halting problem and whatnot real quick.

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

> 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.

Probably, yes.

That or forcing compilation to always target release.

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!

To be clear as there’s a lot of nuance. Assert unchecked is telling the compiler the condition must always hold. The optimizer and compiler don’t make any assumption about the assert. That information is then used by the compiler to optimize away checks it otherwise would have to do (eg making sure an Option is Some if you call unwrap).

If you have an assumption that gives unhelpful information, the optimizer will emit panic code. Worse, if the assumption is incorrect, then the compiler can easily miscompile the code (both in terms of UB because of an incorrectly omitted panic path AND because it can miscompile surprising deductions you didn’t think of that your assumption enables).

I would use the assume crate for this before this got standardized but very carefully in carefully profiled hotspots. Wrapping it in a safe call as in this article would have been unthinkable - the unsafe needs to live exactly where you are making the assumption, there’s no safety provided by the wrapper. Indeed I see this a lot where the safety is spuriously added at the function call boundary instead of making the safety the responsibility of the caller when your function wrapper doesn’t actually guarantee any of the safety invariants hold.

> Wrapping it in a safe call as in this article would have been unthinkable - the unsafe needs to live exactly where you are making the assumption, there’s no safety provided by the wrapper.

I want to be sure I understand your meaning. In your analysis, if the check_invariant function was marked unsafe, would the code be acceptable in your eyes?

Unsafe is the P0. I'd avoid this approach wholesale UNLESS it was a critical hot path with no other way to get safe Rust to elide the check (hint - you'd be surprised how much gets elided in idiomatic Rust). Basically, this is a nice sharp knife in the toolbox to know about and so sharp I'd rarely use it.

Reply on news.ycombinator.com