Inline struct accessors to avoid Why3 polymorphism

[dewert99]

No description provided.

[dewert99]

This is currently failing the list_reversal_lasso test. I'm guessing this has to do with the fact that it is using Seq which causes eliminate_algebraic_if_poly to be activated. This transformations seems to sometimes encode match expressions using quantifiers, so in-lining the match expressions for the accessor may get encoded as a quantifier that doesn't get triggered. This wouldn't be a problem if we could fully eliminate polymorphism (in this case for Seq).

[xldenis]

Could you try regenerating the session in the editor? It should be achievable through auto level 3

[xldenis]

Lgtm, once ci passes go ahead and merge

[dewert99]

Sorry I'm struggling to fix the sessions, @xldenis do you want to try?

[xldenis]

@dewert99, something really weird is going on with that proof, at this point it is hinting to me that this inline:trivial change is not as positive as predicted; I've tried stabilizing the proofs using bisect hypothesis to no success. I don't know how to take this further, perhaps the issue is with inline:trivial on recursive types?

[dewert99]

I'm guessing the issue is with the eliminate_algebraic_if_poly transformation getting triggered by the polymorphism in the Seq type. Would it be possible to use our own monomorphic sequences?

[xldenis]

Hmm that would be possible, do you think you could experiment with it? I think it should be possible confirm this to be the case without too much effort

[dewert99]

Hmm that would be possible, do you think you could experiment with it? I think it should be possible confirm this to be the case without too much effort

In that case should we just revisit #903

[dewert99]

Are we still relying on why3 positivity check for the soundness of Snapshot?

[dewert99]

I'm trying to use prover modifiers to get Why3 to use Z3 sequences, but despite the multitude of meta "encoding:ignore_polymorphism_**" I can't seem to keep the polymorphism encoding from being triggered. I also tried to use a law to add axioms to help with Z3's triggering but that doesn't seem to be working either.

[jhjourdan]

Well, I don't see why you would need to disable polymorphism encoding to use Z3 sequences. SMT theories like algebraic types are being used even in the presence of polymorphism.

The main problem is that one need to rewrite Why3's library of sequences to make it compatible with SMT sequences.

[dewert99]

I'm trying to use Z3 sequences to disable the polymorphism encoding not the other way around. I've found that the polymorphism encoding sometimes creates matching loops, and the way Why3 encodes algebraic types in the presence of polymorphism sometimes creates unnecessary quantifiers.

[xldenis]

I've found that the polymorphism encoding sometimes creates matching loops, and the way Why3 encodes algebraic types in the presence of polymorphism sometimes creates unnecessary quantifiers.

Agreed, and I would like to see this encoding eliminated in practice.

I'm trying to use Z3 sequences to disable the polymorphism encoding not the other way around.

How's that supposed to work?

[dewert99]

How's that supposed to work?

I was hoping similar encoding Why3 Maps to Z3 Arrays prevents them from triggering polymorphism encoding

[dewert99]

Unfortunately I couldn't get it to work, one guess I had is that I couldn't use meta "encoding:ignore_polymorphism_ls" constant empty since it gave a syntax error, so maybe that is triggering the polymorphism encoding.

[xldenis]

I don't really see the link between the two? I think that we can eliminate the polymorphism encoding via your monomorphic sequence module (forgoing smt sequences, at least for now). Or we can ensure that the polymorphism encoding doesn't kick in just because we monomorphically used a polymorphic type (ie: fixing the encoding). I don't see how using the SMT sequences would cause why3 to stop encoding polymorphism though? The causality seems the wrong way around?

[dewert99]

@jhjourdan doesn't seem to want us to use a monomorphic seq library, so I was hoping translate Why3's polymorphic sequence functions into Z3's polymorphic sequence functions without triggering the polymorphism encoding. Z3 supports builtin polymorphic functions.

[jhjourdan]

I'm not really against using a monomorphic seq library. I think adapting the polymorphic library from Why3 is better, because then Why3 users can benefit from it, but if someone does the work of writing a monomorphic library which is based on the SMT native support, thn of course we will use it.

Now, both approaches have their own difficulties:

• If using a monomorphic library with clone, it is not clear to me that we will be able to teach the driver to use the native SMT support
• If using the polymorphic library, then, as you experienced, it is tedious to make sure that all the symbols get monomorphized and therefore that polymorphism detector does not trigger.

Nothing is really a blocker, but this requires time and work...