Exponential growth of constraints on the number of lemma applications

[facundominguez]

The following example passes verification:

{-@ LIQUID "--exactdc" @-}
module Test where

import Language.Haskell.Liquid.ProofCombinators

{-@
f :: xs:[a]
  -> ys:[a]
  -> zs:[a]
  -> ws:[a]
  -> vs:[a]
  -> us:[a]
  -> { append xs (append ys (append zs (append ws (append vs us)))) =
       append (append (append (append (append xs ys) zs) ws) vs) us
     }
@-}
f :: [a] -> [a] -> [a] -> [a] -> [a] -> [a] -> ()
f xs ys zs ws vs us =
  () ? lemmaAssoc xs ys zs                                      --   1 constraint, 2 kvars
     ? lemmaAssoc xs ys (append zs (append ws (append vs us)))  --  65 constraints, 4 kvars
     ? lemmaAssoc (append xs ys) zs (append ws (append vs us))  -- 213 constraints, 6 kvars
     ? lemmaAssoc (append (append xs ys) zs) ws (append vs us)  -- 477 constraints, 8 kvars
     ? lemmaAssoc (append (append (append xs ys) zs) ws) vs us  -- 889 constraints, 10 kvars

{-@
assume lemmaAssoc
  :: xs:[a]
  -> ys:[a]
  -> zs:[a]
  -> { append xs (append ys zs) = append (append xs ys) zs}
@-}
lemmaAssoc :: [a] -> [a] -> [a] -> ()
lemmaAssoc _ _ _ = ()

append :: [a] -> [a] -> [a]
append [] ys = ys
append (x:xs) ys = x : append xs ys

{-@ reflect append @-}

LH reports 889 constraints were verified, and the fqout file shows 10 kvars.

If I comment the last application of lemmaAssoc the constraints drop roughly by half, although verification starts to fail, of course. The kvars also diminished as noted in the commments. Every time a lemma application is commented out the number of constraints halves again.

This doesn't look good for two reasons:

1. There is no inference of refinement types that could help verifying f, so introducing kvars doesn't seem to serve any purpose.
2. The exponential growth of constraints has a serious impact on performance in larger examples with 130 kvars and 56000 constraints.

Can we somehow cut on the number of kvars or checked constraints when introducing lemma applications?

[facundominguez]

Using this definition

infixl 3 ?                                                                                                                                                                                            
(?) :: a -> b -> a                                                                                                                                                                                    
(?) a _ = a 

instead of the one in ProofCombinators, limits the amount of kvars to only 5. The definition in ProofCombinators uses abstract predicates. But still checks 365 constraints, and the amount halves when commenting each lemma application.

---

One could use

{-@ rewriteWith f [lemmaAssoc] @-}

instead of lemma applications, which takes quite a while (10s), but only checks 2 constraints. It doesn't solve the problem, still, as using explicit lemma applications is necessary when debugging proofs to keep track of what LH has been able to prove when automatic methods fail.

---

Using --maxparam=0 cuts the checked constraints to 125. This flag has the effect of discarding qualifiers mined from the program to verify. From 248 qualifiers, it discards 180 qualifiers.

If I use --exclude-automatic-assumptions-for=base and import only the annotations (and qualifiers) from GHC.Types_LHAssumptions, I'm only left with 12 qualifiers in the .fq file, and LH checks only 1 constraint!

{-@ LIQUID "--exclude-automatic-assumptions-for=base" @-}
import GHC.Types_LHAssumptions ()

My take so far is that refinement type inference is going to need a finer way to control the qualifiers in scope, and that the LH user might need some way to influence where kvars are introduced, or how expensive a strategy is used to solve them.

[ranjitjhala]

Hmm. I thought that for the most part, kvars/qualifiers were disabled in reflection (i.e. theorem proving) mode. Specifically, "by default" LH instantiates signatures like a -> b -> a with kvars, but in reflection mode we don't do that -- the abstract refinements were added to specifically generate KVars for ? because we need to instantiate the b with the "post-condition" that is asserted by the lemma...

What happens if you run with {-@ LIQUID "--reflection" @-} ?

[ranjitjhala]

(But broadly your point is valid of course, its totally silly for there to be anything other than a single constraint with just 5 simple equality conjunctions for this example! Let me ponder a bit!)

[ranjitjhala]

@facundominguez -- I note that with just exactdc (the code as above) I indeed get

**** LIQUID: SAFE (889 constraints checked) ************************************

but when I added {-@ LIQUID "--reflection" @-} I get

**** LIQUID: SAFE (1 constraints checked) **************************************

I am a bit confused though, because the saved .fq files are about the same...

[ranjitjhala]

I wonder if its just fixpoint being clever and somehow fusing all the constraints together in the 1 constraint case...

@nilehmann this is an interesting use case of "Hindley" generics.

(?) :: forall <p :: b -> Prop>. a -> {y: b | p y} -> {v: a | p y}

Currently all the complexity of our constraints is due to generating kvars for the p above, but really that is a "hindley" generic that you can just syntactically solve at the call-site.

[nilehmann]

Interesting 🤔

I think you would need to attach the proof to a value for hindley generics to work. So something like

? :: forall<p: bool>. a -> Proof<p> -> {v: a | p}

or

? :: forall<p: b -> bool>. a -> {y: b | p y} -> Prop<p> -> {v: a | p}

if you really want the b. But this kind of defeats the purpose?

[nilehmann]

I suppose you could solve for the p "syntactically" in that position, but that would require higher-order unification.

[ranjitjhala]

Hi @facundominguez sorry I didn't get to the bottom of this yet -- should have some time next week to dig in a bit more!