Set measures generate erroneous constraints when applied to non-polymorphic datatypes

[clayrat]

Typechecking the following program:

{-@ LIQUID "--reflection" @-}

module SngBug where

import Data.Set

data Lst a = Emp | Cons a (Lst a)

{-@ measure lstHd @-}
lstHd :: Ord a => Lst a -> Set a
lstHd  Emp       = empty
lstHd (Cons x _) = singleton x

lcons ::  Lst l -> Lst (Lst l)
{-@ lcons :: p: Lst l -> {v:Lst (Lst l) | v = Cons p Emp } @-}
lcons p = Cons p Emp

crashes with the error:

crash: SMTLIB2 respSat = Error "line 3 column 25217: unknown constant smt_set_sng ((SngBug.Lst Int)) declared: (declare-fun smt_set_sng (Int) (Array Int Bool)) "

The error disappears if lstHd is declared reflect instead of measure. It triggers both with and without PLE.

It looks like the internal Lst l type doesn't get converted to Int which is what the encoding of sets as Array Int Bool expects. We currently think there are two possible solutions for this:

1. Only generate set operations for elements whose type can be encoded as Int (simpler solution, will turn a crash into a proper typechecking error)
2. Generate multiple set types for each potential set element type (more complex, but allows for expressing more programs)

[ranjitjhala]

hi @clayrat -- i have a new laptop and am still installing stuff, can you remind me what smt_set_sng is declared as? i.e. there should be a line in the .liquid/foo.hs.smt2 file that says how it is declared?

[nikivazou]

The problem is that the set elements as declared on SMT as int so every time the set operations are applied (via measures) to elements that are not encoded as int (e.g., list of lists) there is an SMT crash.

Also, .liquid/foo.hs.smt2 does not contain the declaration of smt_set_sng. I assume this is an optimization made by @facundominguez ?

[facundominguez]

Also, .liquid/foo.hs.smt2 does not contain the declaration of smt_set_sng. I assume this is an optimization made by @facundominguez ?

Not an optimization that I remember doing, but I could still be responsible :)

[clayrat]

It looks like this optimization was added in ucsd-progsys/liquid-fixpoint#641

[ranjitjhala]

hmm that is mysterious, we have to declare smt_set_sng somewhere surely...

[nikivazou]

It is declared by fixpoint and I assume it is sent to the Z3. But, it is not printed at the .smt2 file (after the optimization).

[ranjitjhala]

ah ... that's unfortunate, the .smt2 files are supposed to be "standalone" i.e. you can just run `z3 blah.smt2` so it looks like the optimization breaks that? Anyways that is separate from your original point up at the top about set elems being declared as `int`; seems like we need multiple monomorphized "versions" of smt_set_* specialized to different sorts (like we do for `apply`) ?

…

On Mon, Mar 4, 2024 at 6:45 AM Niki Vazou ***@***.***> wrote: It is declared by fixpoint and I assume it is sent to the Z3. But, it is not printed at the .smt2 file (after the optimization). — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2272*issuecomment-1976745648__;Iw!!Mih3wA!G6QUXkb0n144Es03K71kf67Gs9vxXndI3ysyIsfpzX0tUcURaye0XpgqUOp0F1j2OoQDGaZ9EvkvH9wDwg9uiyDw$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OABYHRP2GU4W5POUQLYWSCI3AVCNFSM6AAAAABEBVJHWGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNZWG42DKNRUHA__;!!Mih3wA!G6QUXkb0n144Es03K71kf67Gs9vxXndI3ysyIsfpzX0tUcURaye0XpgqUOp0F1j2OoQDGaZ9EvkvH9wDwhOWb3iP$> . You are receiving this because you commented.Message ID: ***@***.***>

-- - Ranjit.

[clayrat]

I've created a LF PR to fix the preamble logging: ucsd-progsys/liquid-fixpoint#681

[ranjitjhala]

Occurs to me that maybe we should ping the SMTLIB people about this — would be much cleaner if they just supported polymorphic sorts for these theories! - Ranjit.

…

On Mon, Mar 4, 2024 at 6:59 AM Alex Gryzlov ***@***.***> wrote: I've created a LF PR to fix the preamble logging: ucsd-progsys/liquid-fixpoint#681 <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/pull/681__;!!Mih3wA!F0ESa9OZ7XhLq2lmGugQW5_0Bdc_GZsko8IsuT1kFazZy4qoYZl0Ia-9GrlH5q2HHWK25XmfYxZI8UguNDAp18KI$> — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2272*issuecomment-1976776508__;Iw!!Mih3wA!F0ESa9OZ7XhLq2lmGugQW5_0Bdc_GZsko8IsuT1kFazZy4qoYZl0Ia-9GrlH5q2HHWK25XmfYxZI8UguNP1NZr0D$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OEFCEGPMFHEW24PGSLYWSD4NAVCNFSM6AAAAABEBVJHWGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNZWG43TMNJQHA__;!!Mih3wA!F0ESa9OZ7XhLq2lmGugQW5_0Bdc_GZsko8IsuT1kFazZy4qoYZl0Ia-9GrlH5q2HHWK25XmfYxZI8UguNPfetDPg$> . You are receiving this because you commented.Message ID: ***@***.***>

[nikivazou]

That is indeed a good idea! cvc5 seems to have "polymorphic" arrays that we could use to define sets.
So maybe we should:

1. put cvc5 in the benchmark tests (to see if it behaves as well as z3).
2. create a minimum z3 test with the feature we want and as in the z3 github if there is a way to support it.

[facundominguez]

ah ... that's unfortunate, the .smt2 files are supposed to be "standalone" i.e. you can just run z3 blah.smt2 so it looks like the optimization breaks that?

Maybe we could test that the smt2 files produce no errors in CI. I don't know if there is an easy way to test if the answers provided by z3 match the answers provided by LF.

[ranjitjhala]

Looks like CVC5 does have polymorphic sets out of the box though, we should definitely try it out!

https://cvc5.github.io/docs/cvc5-1.0.0/theories/sets-and-relations.html#finite-sets

[ranjitjhala]

@nikivazou -- I believe z3 also has polymorphic arrays? the problem if I recall correctly is that we define set using the z3 map functionality, but only do it "monomorphically"

https://stackoverflow.com/questions/17706219/defining-a-theory-of-sets-with-z3-smt-lib2

[ranjitjhala]

Actually, it occurs to me that the "problem" with our encoding is we try to use the Z3 "function" declaration (e.g. smt_set_sng) which requires us to give a sort to that function, which has to be monomorphic (because I think functions can't be polymorphic?)

If instead we just inlined the function definition, then we wouldn't need any sorts :-)