Merge the `Error` variants

[sonmarcho]

Today Error (used by Result.fail) has quite a few variants. They should be merged into panic (for panicking executions) and ub (for executions that trigger UB): this would allow reasoning about panicking executions, while enforcing that we always need to prove that an execution doesn't trigger UB.

[protz]

This means that we need to tweak the signature of the unchecked operations like get_unchecked to reflect that failure to be in bounds triggers UB, not panic.

[joshlf]

Slight preference for ub being top-level (i.e., Result.ub) since encountering UB means any execution is possible, including running forever. By contrast, the current div/fail split implies that fail cases always halt execution.

If we want to be really pedantic (which we don't - I'm just presenting this to explain my mental model), the way I model this in my head is:

inductive Error where
   ...

inductive WellDefResult (α : Type u) where
  | ok (v: α): WellDefResult α
  | fail (e: Error): WellDefResult α
  | div

inductive Result (α : Type u) where
  | defined (r: WellDefResult α)
  | ub

In practice, I think it's fine (and probably more ergonomic) to do:

inductive Error where
   ...

inductive Result (α : Type u) where
  | ok (v: α): Result α
  | fail (e: Error): Result α
  | div
  | ub

[mdittmer]

This means that we need to tweak the signature of the unchecked operations like get_unchecked to reflect that failure to be in bounds triggers UB, not panic.

@protz I had naively assumed that all possible source of UB appear as opaque holes in Aeneas's transformation. Is that not the case? Do we have a sense of "how many of the sources of UB" show up as a transparent Aeneas transformation?

[joshlf]

This means that we need to tweak the signature of the unchecked operations like get_unchecked to reflect that failure to be in bounds triggers UB, not panic.

@protz I had naively assumed that all possible source of UB appear as opaque holes in Aeneas's transformation. Is that not the case? Do we have a sense of "how many of the sources of UB" show up as a transparent Aeneas transformation?

If I'm reading this correctly - that currently get_unchecked being called with an out-of-bounds index is modeled as panicking - then that aspect of Aeneas is incorrect in the sense that it incorrectly represents the behavior of a Rust program. For example, you could prove something like "this program will not send my crypto keys to not-malware.ru - all it does is panic!" which is actually not a sound guarantee in the presence of UB.

[sonmarcho]

"currently get_unchecked being called with an out-of-bounds index is modeled as panicking": yes, there are places where we use panic instead of UB in the model today, and this means that currently the verification is sound only if you prove the absence of failures - we can't soundly reason about potentially panicking programs today. This being said, making it sound is rather straightforward.

"encountering UB means any execution is possible": I think you're looking at it from the compiler point of view. From the verification point of view UB means that no guarantee whatsoever can ever hold, so you always want to forbid it. The fact that in our model the execution stops at UB doesn't make much difference: reasoning about what potential behavior may happen if we trigger UB is not pertinent, we should always prove that we never reach UB in the first place.

[Nadrieril]

we can't soundly reason about potentially panicking programs today

We can as long as the program is compiled with panic=abort, right? It's unwinding that's hard

[joshlf]

Okay so to summarize:

• Currently UB is modeled as panicking, which means that you must prove absence of panics; if you don't, you haven't proven anything at all (since that admits UB, which makes your program meaningless)
• If we model UB as distinct from panicking, then if you prove absence of UB, you can say some interesting things about the program even if it panics

If we did model panicking and UB as distinct, and you had a panic=abort program, you could say interesting things. What if you unwind instead? Would Aeneas's model of panicking - in the face of unwinding - actually faithfully represent the program's real behavior?

[mdittmer]

I believe #1226 "forbids" ub in bindings to mvcgen. Among other things, I think that means that postconditions such as ⦃ ⇓? r => my_postcondition r ⦄ can be read as "result is divergence, failure, or return of r satisfying my_postcondition r", and not as "result is divergence, UB, failure, or return of r satisfying my_postcondition r".

[ia0]

I'm a bit confused by this thread. My understanding of the top post is: Let's only keep panic and undef in Error, and (written between the lines) let's have pspec and dpspec for postconditions that authorize panics and panics+divergence respectively. (There's no postcondition that authorizes UB, as expected.)

Regarding existing unsafe functions like get_unchecked I don't understand the issue either. UB is not modeled as panic. It's just that you can't tell whether failing the precondition leads to panic or UB (until we get pspec and dpspec to distinguish). So it's more like "UB and panic are modeled the same: as not being permitted" rather than "UB is modeled as panic".

Regarding the top post, in my opinion it would be even clearer to just get rid of Error and have Result be (ignoring bikeshedding):

inductive Result (α : Type u) where
  | ok (v: α): Result α
  | diverge
  | panic
  | undef

And we have the following notations (with the obvious definitions for spec, dspec, pspec, and dpspec using True instead of False to say "may X" with X in {diverge, panic}):

`($e ⦃ $p ⦄) => do `(spec $e $p)
`($e ⦃ $p ⦄diverge) => do `(dspec $e $p)
`($e ⦃ $p ⦄panic) => do `(pspec $e $p)
`($e ⦃ $p ⦄diverge+panic) => do `(dpspec $e $p)

As @Nadrieril said, the difficulty is with unwinding, since then you might want a postcondition for the panicking scenario which may be different than the postcondition for successful termination (VeriFast does that), so you end up with $e ⦃ $p ⦄panic⦃ $q ⦄. And that's ignoring the infrastructure needed to support unwinding in the first place.

[Nadrieril]

Would Aeneas's model of panicking - in the face of unwinding - actually faithfully represent the program's real behavior?

Today's model doesn't drop anything on unwind, which is wrong. So a program that neither panics nor UBs is faithfully represented, but trying to prove properties about an otherwise UB-free program that panics may be wrong (and even miss some UB).

It's not otherwise fundamentally hard to get unwinding right: it's just extra code on every function call, to drop what needs to be dropped. LLBC has the information, Aeneas could choose to translate it.

[mdittmer]

@ia0 IMHO, your design sketch is solid (again, eliding bike-shedding on precise naming). IIUC, #1226 is quite close to this. It does not add specialized panic cases (it keeps the .fail Error pattern, with panicking as one Error), but it does (deliberately) fail to provide a flavour that admits UB.

One thing I am not clear on is how important it is to retain other kinds of failure (other than panicking) that are currently supported.

For additional context: I picked up this issues as the closest thing to something that Anneal needs, which is a distinction between undefined behaviour other results (including normal termination, diverging, panicking, et al).