5 ms·

Is asserting the assumptions during code execution not standard practice for formally verified code?

• ngruhn 1y ago
  How would that look like if you accidentally assumed you have arbitrary large integers but in practice you have 64 bits?
  • appellations 1y ago
    Add(x,y): Assert( x >= 0 && y>= 0 ) z = x + y Assert( z >= x && z >= y ) return z There’s definitely smarter ways to do this, but in practice there is always some way to encode the properties you care about in ways that your assertions will be violated. If you can’t observe a violation, it’s not a violation https://en.wikipedia.org/wiki/Identity_of_indiscernibles https://en.wikipedia.org/wiki/Identity_of_indiscernibles
    • deleted 1y ago
      [deleted]
    • bluGill 1y ago
      In some languages overflow is asserted as a can't happen and so the optimizer will remove your checks
      • appellations 1y ago
        Care to share a language where the compiler infers the semantic meaning of asserts and optimizes them away? I’ve never heard of this optimization.
        • MindSpunk 1y ago
          Signed overflow is UB in C/C++ and several compilers will skip explicit overflow checks as a result. See: https://godbolt.org/z/WehcWj3G5 https://godbolt.org/z/WehcWj3G5
        • mrkeen 1y ago
          C. This is a great thread: https://mastodon.social/@regehr/113821964763012870 https://mastodon.social/@regehr/113821964763012870 (That was one of my texts at uni)
        • Maxatar 1y ago
          C and C++
      • appellations 1y ago
        Best I can tell is that overflow is undefined behavior for signed ints in C/C++ so -O3 with gcc might remove a check that could only be true if UB occurred. The compound predicate in my example above coupled with the fact that the compiler doesn’t reason about the precondition in the prior assert (y is non-negative) means this specific example wouldn’t be optimized away, but bluGill does have a point. An example of an assert that might be optimized away: int addFive(int x) { int y = x + 5; assert(y >= x); return y; }
        • comex 1y ago
          Clang is a bit smarter than GCC here (for some definition of 'smart') and does optimize the original version: https://gcc.godbolt.org/z/3Y4aheG6x https://gcc.godbolt.org/z/3Y4aheG6x
        • uecker 1y ago
          Yes, you can not meaningfully assert anything after UB in C/C++. But you can let the compiler add the trap for overflow -fsanitize=signed-integer-overflow -sanitize-trap=all, or you could also write your assertion in a way where it does not rely on the result (e.g. ckd_add), or you use "volatile" to write in a way the compiler is not allowed to assume anything.
• cowsandmilk 1y ago
  That’s impractical. Take binary search and the assumption the list is sorted. Verifying the list is sorted would negate the point of binary search as you would be inspecting every item in the list.
  • AnimalMuppet 1y ago
    Only if you verify it for every search. If you haven't touched the list since the last search, the verification is still good. For some (not all) situations, you can verify the list at the start of the program, and never have to verify it again.
  • voxl 1y ago
    ASSERTING the list is sorted as an assumption is significantly different form VERIFYING that the list is sorted before executing the search. Moreover, type systems can track that a list was previously sorted and maintained it's sorted status making the assumption reasonable to state.
    • jojomodding 1y ago
      What do you mean when you say "assert" and "verify"? In my head, given the context of this thread and the comment you're replying to, they can both only mean "add an `if not sorted then abort()`." But you make some sort of distinction here.
      • bluGill 1y ago
        Verify means you check. Assert means you say it is, but might or might not check.
        • nothrabannosir 1y ago
          This thread started with: > Is asserting the assumptions during code execution not standard practice for formally verified code? Are you using the same definition of "assert" as that post does?
• kragen 1y ago
  By "asserting X" do you mean "checking whether X is true and crashing the program if not", like the assert macro in C or the assert statement in Python? No, that is almost never done, for three reasons: • Crashing the program is often what you formally verified the program to prevent in the first place! A crashing program is what destroyed Ariane 5 on its maiden flight, for example. Crashing the program is often the worst possible outcome rather than an acceptable one. • Many of the assumptions are not things that a program can check are true. Examples from the post include "nothing is concurrently modifying [variables]", "the compiler worked correctly, the hardware isn't faulty, and the OS doesn't mess with things," and, "unsafe [Rust] code does not have [a memory bug] either." None of these assumptions could be reliably verified by any conceivable test a program could make. • Even when the program could check an assumption, it often isn't computationally feasible; for example, binary search of an array is only valid if the array is sorted, but checking that every time the binary search routine is invoked would take it from logarithmic time to linear time, typically an orders-of-magnitude slowdown that would defeat the purpose of using a binary search instead of a simpler sequential search. (I think Hillel tried to use this example in the article but accidentally wrote "binary sort" instead, which isn't a thing.) When crashing the program is acceptable and correctness preconditions can be efficiently checked, postconditions usually can be too. In those cases, it's common to use either runtime checks or property-based testing instead of formal verification, which is harder.
  • ip26 1y ago
    This becomes an interesting conversation then. First of all, it could mean "checking whether X is true and logging an error" instead of exiting the program. - But if you aren't comfortable crashing the program if the assumptions are violated, then what is your formal verification worth? Not much, because the formal verification only holds if the assumptions hold, and you are indicating you don't believe they will hold. - True, some are infeasible to check. In that case, you could then check them weakly or indirectly. For example, check if the first two indices of the input array are not sorted. You could also check them infrequently. Better to partially check your assumptions than not check at all.
    • 1y ago