Upcoming changes to Boogie

[shazqadeer]

What change in documentation do you suggest?

cc: @alexanderjsummers, @mueller55, @zvonimir, @bkragl, @Chris-Hawblitzel, @akashlal

Thanks to my collaboration with @gauravpartha, the feature for monomorphization of polymorphic Boogie programs is complete; all Boogie features including polymorphic quantifiers, lambdas, and maps are being handled. Upon running the entire Boogie test repository with monomorphization turned on, I discovered discrepancy in verifier outputs for 6 files, all due to inadequate type instantiation for polymorphic quantifiers. The current strategy is best effort using instantiations of polymorphic functions and types used in the body of the quantifier to infer hints for a finite set of type instantiations for the enclosing quantifier. This strategy (and I imagine any finite instantiation strategy) is not sound unless there are extra side conditions on the placement of polymorphic type quantifiers. A Boogie client can enforce the appropriate set of side conditions to make the verification sound. I encourage the Dafny community to play with the monomorphization feature and provide feedback about how it can be made more useful.

On to the changes:

• The default for /typeEncoding will change from TypeEncoding.Predicates to TypeEncoding.Monomorphic. The option /monomorphize will be eliminated.
• The option /useArrayTheory will be eliminated. The SMT array theory will be the default for Boogie maps. A new option /useArrayAxioms will be introduced to translate arrays via the axioms that are currently used when /useArrayTheory is not supplied.
• Thanks to extensive advice by @RustanLeino and @bkragl, the Civl extension for Boogie is complete. Documentation is available here. The new features comprise a significant increase in Boogie's modeling capability and the Boogie version will be bumped to 3.0.

[alexanderjsummers]

Hi @shazqadeer (and @gauravpartha!), thanks a lot for the details - sounds very interesting and impressive work. I'm curious about the unsoundness you describe; I would have expected incompleteness if the quantifiers are being instantiated partially. Is it unsound in the sense that you get sat where you expect unsat (but notionally it would be unknown : incomplete quantifiers if the quantifiers were really there)?

Thanks for all the hard work on this! We will have to benchmark the Viper tests and other tools - I'm very curious.

Cheers, Alex

[shazqadeer]

Hi @shazqadeer (and @gauravpartha!), thanks a lot for the details - sounds very interesting and impressive work. I'm curious about the unsoundness you describe; I would have expected incompleteness if the quantifiers are being instantiated partially. Is it unsound in the sense that you get sat where you expect unsat (but notionally it would be unknown : incomplete quantifiers if the quantifiers were really there)?

Both unsoundness and incompleteness are possible. Suppose you have

assert forall<T> x:T :: foo(x)

and no instance is found for T then the resulting program has

assert true;

This is unsound. Incompleteness will happen if we had an assume instead of an assert.

The reason for all this nonsense is that quantified types are very general in Boogie. They are attached to any quantifier which means they can anywhere in the program text and potentially nested inside expressions. From what I have seen, typical usage of quantified types is much more restrictive than the available generality.

The discussion on this PR is pertinent to the issues of soundness and completeness.

[atomb]

I feel like you read my mind. :) I was just experimenting with monomorphization in Dafny, and found that it provided a significant performance benefit. Unfortunately, I also saw it fail with some programs, including some with bit vectors, and was planning to file an issue. It looks as though your recent PR may address the issues I saw, among other things, and I'm looking forward to trying it with Dafny!

[atomb]

In my early experiments, I'm finding that about 12 of the programs in the Boogie test suite fail, and a few more time out. Is this something you're already aware of and working on, @shazqadeer? Most of the errors are sort errors from the solver.

I'm also curious whether you have any pointers as to where to look for any changes to the invariants required in the AST. When generating .bpl files from Dafny and submitting them to Boogie as a separate process, I'm able to apply monomorphization to some complex Dafny programs. However, when linking to the latest Boogie as a library, Boogie sometimes has various assertion failures while traversing the AST generated programmatically from Dafny. I imagine the Dafny -> Boogie translation needs to be updated to ensure some new or modified invariant.

[shazqadeer]

In my early experiments, I'm finding that about 12 of the programs in the Boogie test suite fail, and a few more time out. Is this something you're already aware of and working on, @shazqadeer? Most of the errors are sort errors from the solver.

On top of the Boogie version currently in master, I changed the initialization of Monomorphize field in CommandLineOptions (line 517 in CommandLineOptions.cs) to true. Then I ran all the regression tests and found the following failures:

  Boogie :: prover/z3mutl.bpl                   Trace reordering
  Boogie :: test15/CommonVariablesPruning.bpl   Model reordering
  Boogie :: test2/LambdaExt.bpl                 Proves one more
  Boogie :: test2/LambdaPoly.bpl                Insufficient type instantiation in quantifier
  Boogie :: test20/PolyPolyPoly2.bpl            Not monomorphizable
  Boogie :: test20/TypeSynonyms2.bpl            Printing
  Boogie :: test21/DisjointDomains2.bpl         Error reordering
  Boogie :: test21/InterestingExamples1.bpl     Insufficient type instantiation in quantifier
  Boogie :: test21/InterestingExamples3.bpl     Insufficient type instantiation in quantifier
  Boogie :: test21/InterestingExamples4.bpl     Likely insufficient instantiation of first-order variables
  Boogie :: test21/Maps1.bpl                    Insufficient type instantiation in quantifier
  Boogie :: test21/PolyList.bpl                 Trace reordering

Over the weekend, I had fixed some bugs that were creating the sort errors you are referring to but all such failures are gone now. For each of the 12 failing tests, I have noted my conjecture about the root cause. You can do a similar analysis by examining the monomorphized output; use /printInstrumented.

I'm also curious whether you have any pointers as to where to look for any changes to the invariants required in the AST. When generating .bpl files from Dafny and submitting them to Boogie as a separate process, I'm able to apply monomorphization to some complex Dafny programs. However, when linking to the latest Boogie as a library, Boogie sometimes has various assertion failures while traversing the AST generated programmatically from Dafny. I imagine the Dafny -> Boogie translation needs to be updated to ensure some new or modified invariant.

Hmm. I understand your problem but I have nothing better to suggest at the moment than "let us get on a video call and look at the crashes together". You could try sending me (use email instead of this forum) some of the stack traces from the crash; perhaps something will occur to me.

[atomb]

I'm also curious whether you have any pointers as to where to look for any changes to the invariants required in the AST. When generating .bpl files from Dafny and submitting them to Boogie as a separate process, I'm able to apply monomorphization to some complex Dafny programs. However, when linking to the latest Boogie as a library, Boogie sometimes has various assertion failures while traversing the AST generated programmatically from Dafny. I imagine the Dafny -> Boogie translation needs to be updated to ensure some new or modified invariant.

Hmm. I understand your problem but I have nothing better to suggest at the moment than "let us get on a video call and look at the crashes together". You could try sending me (use email instead of this forum) some of the stack traces from the crash; perhaps something will occur to me.

I'll dig into the problem a bit more and gather some information over the next couple of days, and I'll drop you an email when I have something more specific.

[gauravpartha]

The SMT array theory makes Boogie maps extensional, which may not be desired. So it's good that there is an option to switch off the SMT array theory. I think this is a fairly major change and it would be good to document it. For instance, the This is Boogie 2 publication by @RustanLeino explicitly states that maps need not be extensional (I know that Boogie has evolved a lot since that publication, but it may still mislead users).

Moreover, the current monomorphization of polymorphic maps together with the SMT array theory would make polymorphic Boogie maps extensional too. I still want to discuss some details with @shazqadeer regarding the monomorphization of polymorphic maps that I am unsure about, which might lead to extensionality not holding for polymorphic maps with the SMT array theory.

As pointed out in https://github.com/dafny-lang/dafny/issues/2463 the soundness of the Dafny encoding currently relies on polymorphic Boogie maps not being extensional. So, if Dafny wants to use the SMT array option together with the monomorphic encoding, then the encoding might have to change in order to remain sound.

[shazqadeer]

This is Boogie 2 publication by @RustanLeino explicitly states that maps need not be extensional (I know that Boogie has evolved a lot since that publication, but it may still mislead users).

"This is Boogie 2" is pretty old and does not match the current state of Boogie. We should drop the reference to this document from the Boogie github page.

The SMT array theory makes Boogie maps extensional, which may not be desired. So it's good that there is an option to switch off the SMT array theory.

To be clear, the Boogie option that affects the translation of arrays is -useArrayAxioms which treats Select/Update as uninterpreted functions and injects some axioms about them in the prelude. This option is relevant only if monomorphic encoding is used; for the other encodings axioms are always used.

So, if Dafny wants to use the SMT array option together with the monomorphic encoding, then the encoding might have to change in order to remain sound.

Z3 supports two options for adjusting its array theory---array.extensional and array.weak. Extensionality can be turned off using the former option. Therefore, it is not necessary to use the Boogie-generated axioms just for the purpose of turning extensionality off.

While I understand the attachment to non-extensional arrays since extensionality has a performance cost, I am less supportive of continued attachment to the array axioms spit out by Boogie. The completeness of these axioms will depend on potentially long chain of matching applications which is likely atypical of the reasoning required for quantified expressions in user-supplied specifications. Conflating the two sources of quantifiers may have unintended negative consequences for performance and proof stability.