Too many constraints generated

[oxarbitrage]

Hey, i am not sure if this is the best place to ask this as this i am not reporting any issue or requesting any feature so feel free to close or move.

I am trying liquidhaskell on my project, works good for my purposes by now. I am basically using it for checking input and output lengths but i also plan to keep adding more checks.

The problem i am having is that i have a file that it seems to be generating too many constrains (over 1 million) and that slows down a lot the compilation.

The file is https://github.com/oxarbitrage/hsalsa20/blob/main/src/Utils.hs . Keep in mind some functions are long and could be done in 1 line using Prelude functions but they are that way to make the solver pass. I think one or several of them are causing a considerable amount of constrains.

Here is the compilation logs:

Building library for salsa20-0.1.0.0..
[ 1 of 10] Compiling Operators

**** LIQUID: SAFE (0 constraints checked) **************************************
[ 2 of 10] Compiling Quarterround

**** LIQUID: SAFE (1865 constraints checked) ***********************************
[ 3 of 10] Compiling Paths_salsa20

**** LIQUID: SAFE (572 constraints checked) ************************************
[ 4 of 10] Compiling Utils

**** LIQUID: SAFE (1051227 constraints checked) ********************************
[ 5 of 10] Compiling Rowround

**** LIQUID: SAFE (972 constraints checked) ************************************
[ 6 of 10] Compiling Columnround

**** LIQUID: SAFE (19 constraints checked) *************************************
[ 7 of 10] Compiling Doubleround

**** LIQUID: SAFE (40 constraints checked) *************************************
[ 8 of 10] Compiling Hash

**** LIQUID: SAFE (36 constraints checked) *************************************
[ 9 of 10] Compiling Expansion

**** LIQUID: SAFE (51 constraints checked) *************************************
[10 of 10] Compiling Crypt

It will be great for me to at least know what are the constrains being generated, some sort of way to debug what function is generating the most constrains and stuff like that.

Thanks for the hard work, any feedback in the subject will be very appreciated.

[ranjitjhala]

Wow I have never seen a single file generate that many constraints (maybe that’s two orders of magnitude larger than anything I’ve seen!) - am on a plane right now, will definitely check it out when I get back home tomorrow! Thanks for trying LH and letting us know!

[facundominguez]

The problem i am having is that i have a file that it seems to be generating too many constrains (over 1 million) and that slows down a lot the compilation.

👋 Hello @oxarbitrage. As workarounds:

• Replacing _ specs with concrete specs might reduce the inference work that LH needs to do.
• Polymorphic functions sometimes make inference of specs more difficult (e.g. #1944). Perhaps making the definitions monomorphic or moving them to another module makes a difference.

Taming this in a controlled fashion is likely to require some debugging and diving into the implementation: Local Refinement Typing from the papers.

[oxarbitrage]

Replacing _ specs with concrete specs might reduce the inference work that LH needs to do.

I tried this in the past, it do not make a difference at all in the number of constraints.

Ill try the other suggestions and references. Thanks!

[oxarbitrage]

Polymorphic functions sometimes make inference of specs more difficult (e.g. #1944). Perhaps making the definitions monomorphic or moving them to another module makes a difference.

Yea, this makes a difference in the constraints amount. I made some modifications at oxarbitrage/hsalsa20@42ce603 and the number reduced to around 50k. The compile time is still long and the duplicated code more than i will like but it is still some improvement.

I will keep learning and improving it. Thanks again for the help.

[oxarbitrage]

Ok, sorry about the mess. I was able to isolate my issue.

First, i separated Utils.hs into https://github.com/oxarbitrage/hsalsa20/blob/main/src/Utils.hs and https://github.com/oxarbitrage/hsalsa20/blob/main/src/LittleEndian.hs

Now the problem is in LittleEndian.hs mod with the aument* functions, such as https://github.com/oxarbitrage/hsalsa20/blob/5d092f39ffe96f8a3cb3805a33d9b3332710d114/src/LittleEndian.hs#L123 . Note i had to ask liquidhaskell to ignore that, if i don't i get the error:

**** LIQUID: UNSAFE ************************************************************
            
/Users/alfredogarcia/haskell/salsa20/src/LittleEndian.hs:127:1: error:
    Liquid Type Mismatch
    .       
    The inferred type
      VV : {v : [GHC.Word.Word32] | len v >= 0}
    .       
    is not a subtype of the required type
      VV : {VV : [GHC.Word.Word32] | len VV == 64}
    .       
    Constraint id 170
    |       
127 | aument input = concat [extractBytes4 x | x <- input]
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
           

However, older versions like the one i had before: https://github.com/oxarbitrage/hsalsa20/blob/42ce6030cb2d8cf268aa36fa770dafd6f27c6998/src/Utils.hs#L196 will pass the checks but creating a lot of constrains and really long compiling time.

[facundominguez]

However, older versions like the one i had before ... will pass the checks but creating a lot of constrains and really long compiling time.

Unlike the old version, the new version of aument uses concat. I think that LH needs to be given a specification for concat that says something about the length of the output that allows it to prove that the result has size 64.

Suppose we have a hypothetical function to concat lists of length 8:

{-@ assume concat8 :: xs:[{i:[a] | len i == 8}] -> {v:[a] | 8 * len xs == len v} @-}
concat8 :: [[a]] -> [a]
concat8 = concat

It is also possible to write a spec close to:

{-@ assume concat :: xs:[[a]] -> {v:[a] | sum (map length xs) == len v} @-}

But then using it requires PLE and perhaps some lemmas.

[oxarbitrage]

Thanks @facundominguez . assume should be good enough to me for now.

https://github.com/oxarbitrage/hsalsa20/blob/9c9140ff668f81561cb991f492d6698d97352a21/src/Utils.hs#L186
https://github.com/oxarbitrage/hsalsa20/blob/9c9140ff668f81561cb991f492d6698d97352a21/src/LittleEndian.hs#L124

It seems PLE should be the proper way to do this so i will probably experiment with that as i keep going.

Great help, keep the good work :)

[ranjitjhala]

Thanks @facundominguez !!!