Optimize interaction with the SMT solver

[facundominguez]

AmericanFlag.hs takes near 20 seconds to verify, while z3 AmericanFlag.hs.smt2 takes only 2 seconds. It turns out most of the time is spent in Language.Fixpoint.Smt.Interface.command which is called 280000 times! Each invocation takes near 50 microseconds, which I conjecture is going to be difficult to speed up.

Maybe SMT solvers can be linked as libraries to cut on that, or maybe it would be possible to batch a few commands and see if just reducing the amount of exchanges with the SMT solver reduces the overall time.

Any thoughts?

[facundominguez]

Found a couple of solver-agnostic apis: https://github.com/makaimann/smt-switch https://github.com/sosy-lab/java-smt (calling the jvm from Haskell is a bit slow though).

[facundominguez]

There's also the chance that after studying the example we might find a way to verify it with less calls to the smt solver.

I tried some batching that removed some hFlush calls on the pipe to the smt solver. This produced a speed up (70% of the original time), but apparently we need a different solution if we want to get rid of all of the overhead.

[ranjitjhala]

Hi @facundominguez -- sorry for not replying, have been thinking this over. The data about AmericanFlag is very interesting -- I didn't realize we get a 50 ms hit per call -- if my math is right, thats 280000 * 50 / 1000000 = 14s (!) just spent in the interface? Does the 50ms include the serialization time? Or is it only the invocation?

The batching sounds very promising! The catch in general is that there is a dependency but still, there could be significant gains as your numbers show -- does AmericanFlag drop to about 10s with your edits?

I have been wary of in-memory APIs because the .smt logs are so useful for debugging but this is a lot of slowdown...

[facundominguez]

Does the 50ms include the serialization time?

Yes, it does include serialization.

Does AmericanFlag drop to about 10s with your edits?

AmericanFlag overall goes from 18 seconds to 14 seconds. The time spent in the command function goes down to 10 seconds.

I have been wary of in-memory APIs because the .smt logs are so useful for debugging but this is a lot of slowdown...

Perhaps LF could log just the same with a modest amount of work.

The main drawbacks of batching are: 1) It is limited to the cases that don't need intermediate results to influence subsequent queries 2) It really makes the code harder to read by splitting all the functions in the query-generation part and the result-collection part. 3) Both query-generation and result-collection need to be kept in sync. 4) Not all the overhead can be removed, we still need to serialize queries and deserialize results

The prospect just doesn't excite me :)

[facundominguez]

Here's a flamegraph. While some overhead can be attributed to the synchronization between processes it also shows that there are quite a few other areas to improve. It was created with SCCs for all top-level functions in liquid-fixpoint. americanflag.svg.zip

[facundominguez]

Here's the flamegraph after the improvements of #492.

[facundominguez]

With #493, the time of AmericanFlag is near 9 seconds.

liquid-fixpoint spends 7 seconds. From here, I'm finding it difficult to bring it down.

• The SMT solver spends near 2.5 seconds.
• The SMT interactions are near 1 second.
• HashMap lookups take near 1.5 seconds.
• Environment reduction spends 1 second and it does improve performance still.
• Elaboration, unification and other expression manipulations seem to take the rest.

I have added batching in #493. If we switched to using the FFI to talk to the SMT solver we might earn a second, two seconds, or none. It depends on how much overhead deserialization takes on the SMT side, and how much overhead it is to build the expressions in the FFI AST.

I can't figure out what else to trim down though. It is looking like we would need to reduce the amount of lookups or manipulations that we need to do in the common paths. e.g. who needs sort checking or elaboration? :) But I don't think removing those is possible.

[ranjitjhala]

Wow. Can you remind me where it started? 17-20s?

On Tue, Sep 21, 2021 at 9:16 AM Facundo Domínguez @.***> wrote:

With #493 https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_pull_493&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rpYbz1aYClZuxHv1TN9dAzhIsMXtBVqXa7TdP9RNSZo&s=BJncuSeYd1kQ8jKra4pSMZpXT75bY8gxsyGn9X_wzbk&e=, the time of AmericanFlag is near 9 seconds.

liquid-fixpoint spends 7 seconds. From here, I'm finding it difficult to bring it down.

• The SMT solver spends near 2.5 seconds.
• The SMT interactions are near 1 second.
• HashMap lookups take near 1.5 seconds.
• Environment reduction spends 1 second and it does improve performance still.
• Elaboration, unification and other expression manipulations seem to take the rest.

I have added batching in #493 https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_pull_493&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rpYbz1aYClZuxHv1TN9dAzhIsMXtBVqXa7TdP9RNSZo&s=BJncuSeYd1kQ8jKra4pSMZpXT75bY8gxsyGn9X_wzbk&e=. If we switched to using the FFI to talk to the SMT solver we might earn a second, two seconds, or none. It depends on how much overhead deserialization takes on the SMT side, and how much overhead it is to build the expressions in the FFI AST.

I can't figure out what else to trim down though. It is looking like we would need to reduce the amount of lookups or manipulations that we need to do in the common paths. e.g. who needs sort checking or elaboration? :) But I don't think removing those is possible.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_482-23issuecomment-2D924141825&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rpYbz1aYClZuxHv1TN9dAzhIsMXtBVqXa7TdP9RNSZo&s=PaBvqrjQKvj9i3wGQJ6ntEyor3UwilWs9wG-xdFNFEI&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OAXAQCOZ22APSIFAFDUDCVWFANCNFSM5CMG2QHA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rpYbz1aYClZuxHv1TN9dAzhIsMXtBVqXa7TdP9RNSZo&s=RGele1sdm2wAlKFm19_fUOM6GOmBx3dUJEYlolWxyDM&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rpYbz1aYClZuxHv1TN9dAzhIsMXtBVqXa7TdP9RNSZo&s=NiIecDfdTWuso9zp2LVe9reHCZGlNbHb6vPrSam3AqU&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rpYbz1aYClZuxHv1TN9dAzhIsMXtBVqXa7TdP9RNSZo&s=jbRkBFuaPHKqlNSpiIG0aUyLADU6ldryKIDE_pArubU&e=.

[facundominguez]

480 brought AmericanFlag from 28 to 14 seconds. #473 to 13 seconds. I think #492 and #493 are bringing it from there to 9 seconds.

[facundominguez]

I dived some more into the FFI path, and its looking laborious. smt-switch doesn't support parametric datatypes, apparently, and neither there is good documentation on the z3 bindings to define them. Add to that the modest improvement, and the hassle to mantain the FFI interface, and it doesn't look so attractive anymore.

There is a new hope though. I found that removing logical qualifiers from AmericanFlag.hs.fq speeds up LF from the current 7 seconds to 2 seconds. Maybe there is some room to either identify irrelevant qualifiers, or serve the qualifiers in an order that optimizes the time in the successful case.

One odd fact in this space is that out of 250 qualifiers, removing only two qualifiers accounts for most of the time reduction, these are:

qualif Auto(VV##0 : int, x : e##xo): ((VV##0 =
                                         (lexSize x))) // SourcePos {sourceName = "benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/AmericanFlag.hs", sourceLine = Pos 62, sourceColumn = Pos 3}
qualif Auto(VV##0 : int, x : e##xo): ((VV##0 <
                                         (lexSize x))) // SourcePos {sourceName = "benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/AmericanFlag.hs", sourceLine = Pos 65, sourceColumn = Pos 3}

Any ideas of what is special about these?

[ranjitjhala]

Wow that is remarkable! Am very surprised that just those two make such a difference!

They don’t look particularly special though. Do you know how the total number of iterations or z3 queries changes when those are removed?

On Sat, Sep 25, 2021 at 7:03 AM Facundo Domínguez @.***> wrote:

I dived some more into the FFI path, and its looking laborious. smt-switch doesn't support parametric datatypes, apparently, and neither there is good documentation on the z3 bindings to define them. Add to that the modest improvement, and the hassle to mantain the FFI interface, and it doesn't look so attractive anymore.

There is a new hope though. I found that removing logical qualifiers from AmericanFlag.hs.fq speeds up LF from the current 7 seconds to 2 seconds. Maybe there is some room to either identify irrelevant qualifiers, or serve the qualifiers in an order that optimizes the time.

One odd fact in this space is that out of 250 qualifiers, removing only two qualifiers amount for most of the time reduction, these are:

qualif Auto(VV##0 : int, x : e##xo): ((VV##0 = (lexSize x))) // SourcePos {sourceName = "benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/AmericanFlag.hs", sourceLine = Pos 62, sourceColumn = Pos 3} qualif Auto(VV##0 : int, x : e##xo): ((VV##0 < (lexSize x))) // SourcePos {sourceName = "benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/AmericanFlag.hs", sourceLine = Pos 65, sourceColumn = Pos 3}

Any ideas of what is special about these?

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_482-23issuecomment-2D927126081&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=6zEUGMy-73DrYBU_a1fvPEjmUNIggWoPbJ86nmNWJCo&s=QQFjcOboTmstqIvH5BKEQ2pc0Xa0fnNVUWxuBdm_Rgs&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4ODCOL5SK55B4M6I7XTUDXJD3ANCNFSM5CMG2QHA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=6zEUGMy-73DrYBU_a1fvPEjmUNIggWoPbJ86nmNWJCo&s=ZI-BbP5QxCMiwdQ_RHtd1uG820d8W8nj_LauPB31i6Y&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=6zEUGMy-73DrYBU_a1fvPEjmUNIggWoPbJ86nmNWJCo&s=Jr-KyJt3p8Sax1f2xiHnSzdWGjLz7Q5NJZV71TAV5cw&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=6zEUGMy-73DrYBU_a1fvPEjmUNIggWoPbJ86nmNWJCo&s=MpIcGRncvMuGXANpp1Sq4G77a03rIweTcJtEFrYLL9Q&e=.

[ranjitjhala]

Those last two bits of information are in the “solverstats” - I wonder how that changes. Also i presume the result (safe/unsafe) is unchanged by the qualifier removal?

On Sat, Sep 25, 2021 at 7:37 AM Ranjit Jhala @.***> wrote:

Wow that is remarkable! Am very surprised that just those two make such a difference!

They don’t look particularly special though. Do you know how the total number of iterations or z3 queries changes when those are removed?

On Sat, Sep 25, 2021 at 7:03 AM Facundo Domínguez < @.***> wrote:

I dived some more into the FFI path, and its looking laborious. smt-switch doesn't support parametric datatypes, apparently, and neither there is good documentation on the z3 bindings to define them. Add to that the modest improvement, and the hassle to mantain the FFI interface, and it doesn't look so attractive anymore.

There is a new hope though. I found that removing logical qualifiers from AmericanFlag.hs.fq speeds up LF from the current 7 seconds to 2 seconds. Maybe there is some room to either identify irrelevant qualifiers, or serve the qualifiers in an order that optimizes the time.

One odd fact in this space is that out of 250 qualifiers, removing only two qualifiers amount for most of the time reduction, these are:

qualif Auto(VV##0 : int, x : e##xo): ((VV##0 = (lexSize x))) // SourcePos {sourceName = "benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/AmericanFlag.hs", sourceLine = Pos 62, sourceColumn = Pos 3} qualif Auto(VV##0 : int, x : e##xo): ((VV##0 < (lexSize x))) // SourcePos {sourceName = "benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/AmericanFlag.hs", sourceLine = Pos 65, sourceColumn = Pos 3}

Any ideas of what is special about these?

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_482-23issuecomment-2D927126081&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=6zEUGMy-73DrYBU_a1fvPEjmUNIggWoPbJ86nmNWJCo&s=QQFjcOboTmstqIvH5BKEQ2pc0Xa0fnNVUWxuBdm_Rgs&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4ODCOL5SK55B4M6I7XTUDXJD3ANCNFSM5CMG2QHA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=6zEUGMy-73DrYBU_a1fvPEjmUNIggWoPbJ86nmNWJCo&s=ZI-BbP5QxCMiwdQ_RHtd1uG820d8W8nj_LauPB31i6Y&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=6zEUGMy-73DrYBU_a1fvPEjmUNIggWoPbJ86nmNWJCo&s=Jr-KyJt3p8Sax1f2xiHnSzdWGjLz7Q5NJZV71TAV5cw&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=6zEUGMy-73DrYBU_a1fvPEjmUNIggWoPbJ86nmNWJCo&s=MpIcGRncvMuGXANpp1Sq4G77a03rIweTcJtEFrYLL9Q&e=.

[facundominguez]

The result is unchanged when eliminating those qualifiers.

These are the stats with no modifications

# Sub Constraints     :   243
# WF  Constraints     :   102
# Constraints         :   208
# Refine Iterations   :   746
# SMT Brackets        :   655
# SMT Queries (Valid) : 53451
# SMT Queries (Total) : 70183
# Sliced Constraints  :   208
# Target Constraints  :    91

These are the stats with the two qualifiers removed:

# Sub Constraints     :   243
# WF  Constraints     :   102
# Constraints         :   208
# Refine Iterations   :   746
# SMT Brackets        :   655
# SMT Queries (Valid) : 30893
# SMT Queries (Total) : 41639
# Sliced Constraints  :   208
# Target Constraints  :    91

And these are the stats with as many qualifiers as I could remove without getting unsafe constraints (near 100 qualifiers survived):

# Sub Constraints     :   243
# WF  Constraints     :   102
# Constraints         :   208
# Refine Iterations   :   746
# SMT Brackets        :   582
# SMT Queries (Valid) : 20162
# SMT Queries (Total) : 23806
# Sliced Constraints  :   208
# Target Constraints  :    91

The runtime decreases linearly with the amount of queries at 1 second every 10000 queries.

[ranjitjhala]

Wow so those two irrelevant qualifiers are responsible for nearly 25K SMT queries!

[facundominguez]

Will the second parameter of the qualifier x : e##xo be substituted with values of any sort? This could perhaps explain a long list of qualifiers created by replacing x with various local values that then need to be discarded by calling to the SMT.

[ranjitjhala]

Yes that makes sense! I wonder what the source line is from where the qualifier has been obtained.

On Sat, Sep 25, 2021 at 6:12 PM Facundo Domínguez @.***> wrote:

Will the second parameter of the qualifier x : e##xo be substituted with values of any sort? This could perhaps explain a long list of qualifiers created by replacing x with various local values that then need to discarded by calling to the SMT.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_482-23issuecomment-2D927207398&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=I4PMkmD1JGrdQgBDj_FS2iCRv6tlKfU89xjTpJQttME&s=-ddlFmmJj1GDa1-jaj_5LMgMTaDRbEVGI1yw8iy_U3w&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OESBYJEKOFELTYMM73UDZXRFANCNFSM5CMG2QHA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=I4PMkmD1JGrdQgBDj_FS2iCRv6tlKfU89xjTpJQttME&s=sRBo5pIGMJBLGE5F6rxu9IxIv5k-3gM0JQxPJC1roE8&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=I4PMkmD1JGrdQgBDj_FS2iCRv6tlKfU89xjTpJQttME&s=1yPf4jaGuF9ttjrc8W2Ix27PCRFWtL7Lyrf41ZxmTlk&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=I4PMkmD1JGrdQgBDj_FS2iCRv6tlKfU89xjTpJQttME&s=g2nDdlzoAX6ZTyr0gsHdpXxYQEMPY_iys1lH_uYqdGI&e=.

[facundominguez]

They originate from the specification of typeclass methods.

class Lexicographic e where
  terminate :: e -> Int -> Bool
  size      :: e -> Int
  index     :: Int -> e -> Int

{-@ measure lexSize :: a -> Int                                           @-}
{-@ assume size  :: (Lexicographic e) => x:e -> {v:Nat | v = (lexSize x)}        @-}
{-@ assume index :: (Lexicographic e) => Int -> x:e -> {v:Nat | v < (lexSize x)} @-}

https://github.com/ucsd-progsys/liquidhaskell/blob/cecfe71415014456391e8c2d5d7c4f912ebd4458/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/AmericanFlag.hs#L70-L72

[ranjitjhala]

Interesting, so because fixpoint’s sort system doesn’t know anything about the class constraints, we end up instantiating these qualifiers for ALL types which then leads to these problems. Good find! Will have to think about how to convey this “class constraint” information to fixpoint…

On Sun, Sep 26, 2021 at 4:51 AM Facundo Domínguez @.***> wrote:

They originate from the specification of typeclass methods.

class Lexicographic e where terminate :: e -> Int -> Bool size :: e -> Int index :: Int -> e -> Int

{-@ measure lexSize :: a -> Int @-} {-@ assume size :: (Lexicographic e) => x:e -> {v:Nat | v = (lexSize x)} @-} {-@ assume index :: (Lexicographic e) => Int -> x:e -> {v:Nat | v < (lexSize x)} @-}

https://github.com/ucsd-progsys/liquidhaskell/blob/cecfe71415014456391e8c2d5d7c4f912ebd4458/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/AmericanFlag.hs#L70-L72 https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_blob_cecfe71415014456391e8c2d5d7c4f912ebd4458_benchmarks_vector-2Dalgorithms-2D0.5.4.2_Data_Vector_Algorithms_AmericanFlag.hs-23L70-2DL72&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Bgf33hKdtRtZZYfF9M3TqSHZfYmgLFaAb1KTpCbfdE8&s=bx_bRRFn3cLzGoIhb4kKlAoL2XKIU9Cqgoy3egazh44&e=

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_482-23issuecomment-2D927292228&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Bgf33hKdtRtZZYfF9M3TqSHZfYmgLFaAb1KTpCbfdE8&s=nIVDYLCNDSjZj0vE8HCPeXrG1Dw9HLMS_gjjYD6T5Uo&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OFVQLXLP2MDNCCWXS3UD4CMZANCNFSM5CMG2QHA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Bgf33hKdtRtZZYfF9M3TqSHZfYmgLFaAb1KTpCbfdE8&s=MC2rNYEy0GENZyBbG6LWz4mOfewGayfjH8Bl4jjknKM&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Bgf33hKdtRtZZYfF9M3TqSHZfYmgLFaAb1KTpCbfdE8&s=q9rZchTa_LkPm6nE7BvqQwkWEvzVLe5Ysuwbo67V8nk&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Bgf33hKdtRtZZYfF9M3TqSHZfYmgLFaAb1KTpCbfdE8&s=xrC0yjCRhyW8t-YCjiMbFkajzIe94ZbkWi9k1L3GqbQ&e=.

[ranjitjhala]

Oddly though those two qualifiers seem to come from somewhere else: as they respectively check if lexSize equals or is greater than 0?

On Sun, Sep 26, 2021 at 9:37 AM Ranjit Jhala @.***> wrote:

Interesting, so because fixpoint’s sort system doesn’t know anything about the class constraints, we end up instantiating these qualifiers for ALL types which then leads to these problems. Good find! Will have to think about how to convey this “class constraint” information to fixpoint…

On Sun, Sep 26, 2021 at 4:51 AM Facundo Domínguez < @.***> wrote:

They originate from the specification of typeclass methods.

class Lexicographic e where terminate :: e -> Int -> Bool size :: e -> Int index :: Int -> e -> Int

{-@ measure lexSize :: a -> Int @-} {-@ assume size :: (Lexicographic e) => x:e -> {v:Nat | v = (lexSize x)} @-} {-@ assume index :: (Lexicographic e) => Int -> x:e -> {v:Nat | v < (lexSize x)} @-}

https://github.com/ucsd-progsys/liquidhaskell/blob/cecfe71415014456391e8c2d5d7c4f912ebd4458/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/AmericanFlag.hs#L70-L72 https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_blob_cecfe71415014456391e8c2d5d7c4f912ebd4458_benchmarks_vector-2Dalgorithms-2D0.5.4.2_Data_Vector_Algorithms_AmericanFlag.hs-23L70-2DL72&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Bgf33hKdtRtZZYfF9M3TqSHZfYmgLFaAb1KTpCbfdE8&s=bx_bRRFn3cLzGoIhb4kKlAoL2XKIU9Cqgoy3egazh44&e=

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_482-23issuecomment-2D927292228&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Bgf33hKdtRtZZYfF9M3TqSHZfYmgLFaAb1KTpCbfdE8&s=nIVDYLCNDSjZj0vE8HCPeXrG1Dw9HLMS_gjjYD6T5Uo&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OFVQLXLP2MDNCCWXS3UD4CMZANCNFSM5CMG2QHA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Bgf33hKdtRtZZYfF9M3TqSHZfYmgLFaAb1KTpCbfdE8&s=MC2rNYEy0GENZyBbG6LWz4mOfewGayfjH8Bl4jjknKM&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Bgf33hKdtRtZZYfF9M3TqSHZfYmgLFaAb1KTpCbfdE8&s=q9rZchTa_LkPm6nE7BvqQwkWEvzVLe5Ysuwbo67V8nk&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Bgf33hKdtRtZZYfF9M3TqSHZfYmgLFaAb1KTpCbfdE8&s=xrC0yjCRhyW8t-YCjiMbFkajzIe94ZbkWi9k1L3GqbQ&e=.

[ranjitjhala]

Here's an idea that may address this problem without requiring any support for typeclasses/constraints in fixpoint:

restrict measures (e.g. lexSize) ONLY to the set of monomorphic sorts that they are already appear at in the rest of the constraints.

Right now the sort for lexSize is forall a. a -> int which is causing this blowup.

Instead, walk over the constraints -- after elaboration -- to find all existing terms of the form lexSize [@t] e and only allow lexSize to be subsequently instantiated at the sorts t.

This could greatly shrink the sorts at which valid instantiations are allowed, and shouldn't affect the constraint solving...

[facundominguez]

Oddly though those two qualifiers seem to come from somewhere else: as they respectively check if lexSize equals or is greater than 0?

Aren't the comparisons made with VV##0 rather than 0? I'm failing to notice why they should come from elsewhere.

Here's an idea that may address this problem without requiring any support for typeclasses/constraints in fixpoint

Worth considering. I'll try removing only the qualifiers that have unconstraint parameters and see how that goes.

[ranjitjhala]

Aren't the comparisons made with VV##0 rather than 0? I'm failing to notice why they should come from elsewhere.

Oops my apologies, you are correct!

[facundominguez]

Removing only the qualifiers with unrestricted parameters, gives

# Sub Constraints     :   243
# WF  Constraints     :   102
# Constraints         :   208
# Refine Iterations   :   746
# SMT Brackets        :   655
# SMT Queries (Valid) : 26631
# SMT Queries (Total) : 31949
# Sliced Constraints  :   208
# Target Constraints  :    91

Which isn't too bad.

My great discovery today was --minimizeqs which yields the following 10 qualifiers

qualif Auto(v : bool, n : int): ((((n + 1) >=
                                     maxPassesN) => v)) // SourcePos {sourceName = "AmericanFlag.hs.fq", sourceLine = Pos 1066, sourceColumn = Pos 8}
qualif Cmp(v : @(0), x : @(0)): ((v >
                                    x)) // SourcePos {sourceName = "AmericanFlag.hs.fq", sourceLine = Pos 1106, sourceColumn = Pos 8}
qualif Cmp(v : @(0), x : @(0)): ((v >=
                                    x)) // SourcePos {sourceName = "AmericanFlag.hs.fq", sourceLine = Pos 1108, sourceColumn = Pos 8}
qualif CmpZ(v : @(0)): ((v >
                           0)) // SourcePos {sourceName = "AmericanFlag.hs.fq", sourceLine = Pos 1128, sourceColumn = Pos 8}
qualif CmpZ(v : @(0)): ((v >=
                           0)) // SourcePos {sourceName = "AmericanFlag.hs.fq", sourceLine = Pos 1130, sourceColumn = Pos 8}
qualif EqSiz(x : @(0), y : @(1)): (((vsize x) =
                                      (vsize y))) // SourcePos {sourceName = "AmericanFlag.hs.fq", sourceLine = Pos 1142, sourceColumn = Pos 8}
qualif NonEmpty(v : @(0)): ((0 <
                               (vsize v))) // SourcePos {sourceName = "AmericanFlag.hs.fq", sourceLine = Pos 1168, sourceColumn = Pos 8}
qualif OkIdx(v : int, x : @(0)): ((v <
                                     (vsize x))) // SourcePos {sourceName = "AmericanFlag.hs.fq", sourceLine = Pos 1170, sourceColumn = Pos 8}
qualif OkIdx(v : int, x : @(0)): ((v <=
                                     (vsize x))) // SourcePos {sourceName = "AmericanFlag.hs.fq", sourceLine = Pos 1172, sourceColumn = Pos 8}
qualif Plus(v : int, x : int, y : int): (((v + x) =
                                            y)) // SourcePos {sourceName = "AmericanFlag.hs.fq", sourceLine = Pos 1179, sourceColumn = Pos 8}

with these, verification takes only 1 second in LF! (if I don't take into account the parsing overhead which I've been ignoring all along)

Which sends me into thinking if there could be a practical way to cache these 10 qualifiers and use them as a starting point whenever the user modifies the code.

# Sub Constraints     :  243
# WF  Constraints     :  102
# Constraints         :  208
# Refine Iterations   :  612
# SMT Brackets        :  405
# SMT Queries (Valid) : 6371
# SMT Queries (Total) : 7939
# Sliced Constraints  :  208
# Target Constraints  :   91