Attempts to avoid Why3's polymorphism encoding

[dewert99]

In order to continue trying to avoid matching loops/timeouts I am trying to avoid Why3's encoding_smt_if_poly and eliminate_algebraic_if_poly transformations. I created the driver z3_no_poly.drv which is mostly a copy of z3_486 but doesn't include these transformations. Most of the Why3 generated by Creusot is already monomorphic enough for the "smtv2.6" printer with the following exceptions (that I've found) which I've tried to resolve.

• Why3 standard library sequences
  • I replaced creusot_contracts::Seq with an implementation with opaque methods that aren't replaced with functions from Why3's sequences
  • I implemented it in terms of the original version so I could avoid using #[trusted]. Does CI check that creusot_contracts verify?
  • The implementation of Seq::EMPTY is somewhat hacky since Creusot doesn't support constants
  • Since Creusot doesn't support opaque structs the new Seq implementations still depend on the Why3 standard library so I made z3_no_poly.drv remove all why3 standard library sequence methods.
• Prelude ghost type
  • I made ghost_ty a single field struct, and made new and inner inline to the constructor and field accessor respectively
• ADT field accessor functions generated by Why3
  • I added the inline:trivial attribute, but this only worked for structs

Ideally, the field accessor functions would get their own monomorphic cloneable module so that inline:trivial wouldn't be necessary, and z3_no_poly.drv would also support enum accessors, but I didn't want to mess with the CloneMap especially when it may be removed soon. Personally, combining these changes (including the driver) with the --simple-triggers options got things to the pointer where errors were reported as Unknown instead of Timeout and z3's Array/Mapping extensionality axioms could be relied upon.

[jhjourdan]

I created the driver z3_no_poly.drv which is mostly a copy of z3_486 but doesn't include these transformations.

That should be useless. If the goal is already monomorphic, then encoding_smt_if_poly and eliminate_algebraic_if_poly should be no-ops. The real work to be done if we want to get rid of polymorphism encoding is to get rid of polymorphism.
(If that's not the case, then it's probably a bug in Why3.)

Does CI check that creusot_contracts verify?

No.

I replaced creusot_contracts::Seq with an implementation with opaque methods that aren't replaced with functions from Why3's sequences

But then this means that SMT solvers do not have access to Why3's stdlib lemmas on sequences? I'm a bit afraid of the loss of proof power, then!

Personally, combining these changes (including the driver) with the --simple-triggers options got things to the pointer where errors were reported as Unknown instead of Timeout and z3's Array/Mapping extensionality axioms could be relied upon.

Could you explain a bit more the issue you are facing?

I actually think that there is a simpler way to get rid of the matching loops caused by polymorphism encoding: if, after polymorphism encoding, we remove all the polymorphic instances of lemmas, then essentially you get a goal without all the noise of polymorphism encoding. That's incomplete, but in practice, I'm don't think the polymorphic instances are used so much (especially in goals generated by Creusot).

[dewert99]

That should be useless. If the goal is already monomorphic, then encoding_smt_if_poly and eliminate_algebraic_if_poly should be no-ops. The real work to be done if we want to get rid of polymorphism encoding is to get rid of polymorphism.
(If that's not the case, then it's probably a bug in Why3.)

I generally agree, but I found removing the transformations useful for debugging where there was polymorphism to get rid of (I prefer the error to silently using the polymorphism encoding)

But then this means that SMT solvers do not have access to Why3's stdlib lemmas on sequences? I'm a bit afraid of the loss of proof power, then!

I tried to give the sequence methods similar specifications to what they had in why3 so within the solver I would assume they would work similarly, but I guess you would lose the the extra lemmas when using the IDE.

Could you explain a bit more the issue you are facing?
I think there are two main issues.

1. the polymorphic instances of the Why3 sequence lemmas seem to contain a matching loop (I think it has to do with singleton)
2. The eliminate_algebraic transformation seems to generate quantifiers when translating a match expression that returns a boolean. This seems to sometimes cause matching loops and I can't seem to find a reference to it in the paper for eliminate_algebraic https://inria.hal.science/inria-00439232.
   • The encoding_smt transformation doesn't work without first running eliminate_algebraic so in order to avoid this issue we need the input Why3 to be completely monomorphic

I actually think that there is a simpler way to get rid of the matching loops caused by polymorphism encoding: if, after polymorphism encoding, we remove all the polymorphic instances of lemmas, then essentially you get a goal without all the noise of polymorphism encoding. That's incomplete, but in practice, I'm don't think the polymorphic instances are used so much (especially in goals generated by Creusot).

If we could get some sort of eliminate_polymorphism transformation at the Why3 level to run after discriminate instead of encoding_smt_if_poly and eliminate_algebraic_if_poly that would be great.

[dewert99]

In general, it might be beneficial for Why3 to have a version of eliminate_algebraic that does not introduce quantifiers when translating formulas

[voidc]

ghost_ty was intentionally made an opaque type in #823 to fix the issue with infinite values in #436.

[dewert99]

Sorry, maybe I'm missing something, but I thought the goal of #823 was to prevent unsound recursive type definitions involving Ghost in Rust, and I don't see how that is related to the way Ghost is encoded in Why3.

[voidc]

The check on the Rust level does not catch all unsound type definitions. For example, the following works:

struct Foo<T>(Ghost<T>);
struct Bad(Foo<Bad>);

To still prevent such unsound types, we additionally rely on the strict positivity check of Why3.
As Ghost is defined as opaque type, the parameter T of Foo is not considered strictly positive and thus the definition of Bad is rejected.

[dewert99]

I also noticed that the discriminate transformation doesn't seem to create a monomorphic instance of the Seq.create function even when using:

theory BuiltIn
  meta "select_inst" "all"
  meta "select_lskept" "all"
  meta "select_lsinst" "all"
  meta "select_kept" "all"
end

theory seq.Seq
  meta "encoding:lskept" function create
end

The result functions that seem to be generated by eliminate_epsilon also aren't monomorphized unless discriminate is run before eliminate_epsilon (I can seem to cause Seq.create to be monomorphized by running discriminate both before and after eliminate_epsilon but this creates duplicate hypotheses).

[dewert99]

Are there any plans to add a remove_polymorphism/eliminate_polymorphism transformation to Why3? I think it would be useful to have some way of bypassing Why3s polymorphism encoding either directly within Why3 or by having Creusot output monomorphic Why3.

[jhjourdan]

This has been on my TODO list for months, already.

The problem is that I'd like to experiment with a stronger discriminate to mitigate the fact that polymorphic lemmas do not exists.

[dewert99]

Unless I'm misunderstanding it seems like polymorphic lemmas do exist (eg. https://why3.lri.fr/stdlib/seq.html#associative_135), or do you mean that Creusot doesn't use any polymorphic lemmas?

[jhjourdan]

These lemmas do exist indeed and Creusot does use them. The goal of discriminate is to instantiate them at relevant types so that, in practice, we don't loose too much completeness by removing polymorphic versions.

[dewert99]

Were you planning on adding a single new transformation that does a better discriminate and removes polymorphism, or adding a better discriminate transformation and a remove polymorphism transformation separately? If you add them separately, would it be possible to make a public Why3 branch with just the remove polymorphism transformation sooner? I think combining it with the existing discriminate transformation would already be helpful even if it means that the Seq.create function was eliminated.

[dewert99]

I've able to mostly make Seq and Snapshot normal trusted Creusot types instead of having them defined in Why3. The one issue is handling slice length in FMIR since it is currently translated to a polymorphic function in the prelude.

[jhjourdan]

The issue with not using Why3's support for sequences is that we will not be able to use prover's native support for sequences.