Boogie Backend Redesign

[DavePearce]

(see also #72, #120 and #142)

This is an attempt to log the various problems with the current approach.

• Functions. Translating a Whiley function as a boogie function is fraught with difficulties (why?). A better solution would be to translate them as procedures. This has a bunch of knock-on effects. In particular, we cannot use preconditions / postconditions in procedures. Instead, we must use assume and assert statements. Also, it means function calls have to be pulled out of expressions. In effect, we end up with something much closer to bytecode.
• Properties. These are translated into boogie functions. But, how do we enforce their preconditions / postconditions (e.g. parameter / return types). Likewise, internal consistency requirements, such as indices within bounds? Potentially, a separate property check procedure is required for this.
• Control Flow. Current challenges with extracting method calls from conditions mean that we often fall back to unstructured control-flow (e.g. for loops). Overall, I thing its simply better to do this all the time.
• Boxing / Unboxing. It should be possible to eliminate the need for boxing / unboxing. This can done using algebraic datatypes, and types like Vec. See also #109. Questions remain around the heap and template.
• Types. Dafny uses something like <A>[ref, Field A]A for representing parts of the heap (see Memory T below). Boogie also has built-in support for "sequences" (see here), and supports tuple assignments.
• Casts. These appear to be a problem in my current design.
• Error Reporting. You can supply messages in assertions which can help with error reporting (see here). Syntax is {:msg "your text goes here"}

[DavePearce]

Some observations from the move prover (see here):

• Defines Vec T for implementing arrays.
• Defines Memory T for implementing a memory holding type T.
• Defines specific bitwise operators over int types. This will be useful for Whiley when I remove byte.

See also this paper:

• Reasoning About Vectors using an SMT Theory of Sequences, https://arxiv.org/abs/2205.08095

[DavePearce]

More thoughts:

• Will need overflow checking for fixed-width types
• Can a procedure ever be pure? If not cannot implement Whiley function perfectly using them.
• Can property call functions? If not, could inline their preconditions. Also use a separate check for their return values / internal conditions.

[DavePearce]

Useful documentation on Boogie:

• This is Boogie 2.
• Language Reference.
• The Boogie 2 Type System
• Why Just Boogie? Translating Between Intermediate Verification Languages
• A Polymorphic Intermediate Verification Language: Design and Logical Encoding
• The Civl Verifier
• The Boogie Intermediate Verification Language (Alex Summers)
• To Goto Where No Statement Has Gone Before

To Look At:

• https://arxiv.org/abs/2205.08095
• https://civl-verifier.github.io/doc.html
• https://www.microsoft.com/en-us/research/video/practical-boogie-on-the-example-of-vcc/
• https://homepage.cs.uiowa.edu/~tinelli/classes/181/Papers/dafny-reference.pdf