Merge pull request #2597 from ucsd-progsys/fd/remove-no-lazy-ple

Remove --no-lazy-ple, update LF, test LF-780

Author: facundominguez

.circleci/config.yml

@@ -10,8 +10,8 @@ commands:
           name: Install z3
           command: |
             # Config version
-            z3version="z3-4.8.17"
-            z3distributiontype="x64-glibc-2.31"
+            z3version="z3-4.15.1"
+            z3distributiontype="x64-glibc-2.39"
             z3full="${z3version}-${z3distributiontype}"
 
             # Download and install
@@ -145,14 +145,14 @@ jobs:
   # support GHC 9.12 yet.
   stack_900:
     machine:
-      image: default
+      image: ubuntu-2404:2025.09.1
     steps:
         - stack_build_and_test:
             stack_yaml_file: "stack.yaml"
             extra_build_flags: "--flag liquidhaskell-boot:devel"
   cabal_9122:
     machine:
-      image: default
+      image: ubuntu-2404:2025.09.1
     steps:
       - cabal_build_and_test:
           ghc_version: "9.12.2"

.github/workflows/cabal.yml

@@ -18,7 +18,7 @@ jobs:
         ghc:
           - "9.12.2"
         z3:
-          - "4.10.2"
+          - "4.15.1"
 
     steps:
       - uses: actions/checkout@v4
@@ -29,6 +29,7 @@ jobs:
         uses: pavpanchekha/setup-z3@6b2d476d7a9227e0d8d2b94f73cd9fcba91b5e98
         with:
           version: ${{ matrix.z3 }}
+          distribution: glibc-2.39
 
       - name: Workaround runner image issue
         # https://github.com/actions/runner-images/issues/7061

liquid-fixpoint

@@ -63,7 +63,6 @@ fixConfig tgt cfg = def
   , FC.extensionality = extensionality    cfg
   , FC.interpreter    = interpreter    cfg
   , FC.rwTermination  = rwTerminationCheck cfg
-  , FC.noLazyPLE      = noLazyPLE cfg
   , FC.fuel           = fuel      cfg
   , FC.noEnvReduction = not (environmentReduction cfg)
   , FC.inlineANFBinds = inlineANFBindings cfg

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs

@@ -374,11 +374,6 @@ defConfig = Config {
     = False
         &= name "skip-module"
         &= help "Completely skip this module, don't even compile any specifications in it."
-  ,
-    noLazyPLE
-    = False
-        &= name "no-lazy-ple"
-        &= help "Don't use Lazy PLE"
 
   , fuel
     = Nothing

liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs

@@ -103,7 +103,6 @@ data Config = Config
   , auxInline                :: Bool        -- ^
   , rwTerminationCheck       :: Bool       -- ^ Enable termination checking for rewriting
   , skipModule               :: Bool       -- ^ Skip this module entirely (don't even compile any specs in it)
-  , noLazyPLE                :: Bool
   , fuel                     :: Maybe Int  -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite)
   , environmentReduction     :: Bool       -- ^ Perform environment reduction
   , noEnvironmentReduction   :: Bool       -- ^ Don't perform environment reduction

liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs

@@ -1,6 +1,5 @@
 {-@ LIQUID "--reflection"  @-}
 {-@ LIQUID "--ple"         @-}
-{-@ LIQUID "--no-lazy-ple" @-}
 
 module Lists where
 

tests/benchmarks/sf/Lists.hs

@@ -0,0 +1,111 @@
+{-@ LIQUID "--ple" @-}
+-- | Tests that we can unfold reflected functions in the solutions
+-- of KVars.
+--
+-- https://github.com/ucsd-progsys/liquid-fixpoint/issues/780
+--
+module TestLF780 where
+
+import Data.Set as Set
+
+{-@ data State s a <p :: s -> Bool, q :: s -> a -> s -> Bool>
+      = State (x:s<p> -> (a, s)<\w -> {v:s<q x w> | true}>)
+  @-}
+data State s a  = State {runState :: s -> (a, s)}
+
+{-@ runState :: forall <p :: s -> Bool, q :: s -> a -> s -> Bool>.
+                State <p, q> s a -> x:s<p> -> (a, s)<\w -> {v:s<q x w> | true}> @-}
+
+instance Functor (State s) where
+{-@
+instance Functor (State s) where
+  fmap :: forall < p  :: s -> Bool
+                 , q :: s -> a -> s -> Bool
+                 , q2 :: s -> a -> s -> Bool
+                 , pa :: a -> Bool
+                 , pb :: b -> Bool
+                 >.
+            {x::a<pa>, s0::s<p>, y::b<pb> |- s<q s0 x> <: s<q2 s0 y>}
+            (a<pa> -> b<pb>)
+         -> State <p, q> s a<pa>
+         -> State <p, q2> s b<pb>
+@-}
+  fmap f x = State $ \s -> let (y, s') = runState x s in (f y, s')
+
+instance Applicative (State s) where
+{-@
+instance Applicative (State s) where
+  pure :: forall <p :: s -> Bool>.
+                x:a -> State <p, \w0 y -> {w1:s<p> | w0 == w1 && y == x}> s a
+@-}
+  pure x = State $ \s -> (x, s)
+  mf <*> mx = State $ \s ->
+    let (f, s1) = runState mf s
+        (x, s2) = runState mx s1
+    in (f x, s2)
+
+instance Monad (State s) where
+{-@
+instance Monad (State s) where
+  >>= :: forall < p  :: s -> Bool
+                    , p2 :: a -> s -> Bool
+                    , r  :: a -> Bool
+                    , q1 :: s -> a -> s -> Bool
+                    , q2 :: a -> s -> b -> s -> Bool
+                    , q  :: s -> b -> s -> Bool>.
+            {x::a<r>, w::s<p>|- s<q1 w x> <: s<p2 x>}
+            {w::s<p>, x::a, w1::s<q1 w x>, y::b |- s<q2 x w1 y> <: s<q w y>}
+            {x::a, w::s, w2::s<q1 w x>|- {v:a | v = x} <: a<r>}
+            State <p, q1> s a
+         -> (x:a<r> -> State <{v:s<p2 x> | true}, \w1 y -> {v:s<q2 x w1 y> | true}> s b)
+         -> State <p, q> s b ;
+  >>  :: forall < p   :: s -> Bool
+                    , p2  :: s -> Bool
+                    , q1 :: s -> a -> s -> Bool
+                    , q2 :: s -> b -> s -> Bool
+                    , q :: s -> b -> s -> Bool>.
+            {x::a, w::s<p>|- s<q1 w x> <: s<p2>}
+            {w::s<p>, w2::s<p2>, x::b, y::a |- s<q2 w2 x> <: s<q w x>}
+            State <p, q1> s a
+         -> State <p2, q2> s b
+         -> State <p, q> s b  ;
+  return :: forall <p :: s -> Bool>.
+                x:a -> State <p, \w0 y -> {w1:s<p> | w0 == w1 && y == x}> s a
+@-}
+  (State g) >>= f = State $ \x -> case g x of {(y, s) -> (runState (f y)) s}
+
+  (State g) >>  f = State $ \x -> case g x of {(y, s) -> (runState f    ) s}
+
+  return w      = State $ \s -> (w, s)
+
+
+{-@
+get :: forall <p :: s -> Bool>.
+   State <p, {\s0 v s -> v = s && s = s0}> s s<p>
+@-}
+get :: State s s
+get = State $ \s -> (s, s)
+
+{-@
+put :: forall <p :: s -> Bool>.
+   s0:s -> State <p, {\_ v s -> s = s0}> s ()
+@-}
+put :: s -> State s ()
+put s = State $ \_ -> ((), s)
+
+{-@ reflect gt0 @-}
+gt0 :: Int -> Bool
+gt0 x = x > 0
+
+{-@
+stFun
+  :: i:Int
+  -> State
+       <{\m0 ->  gt0 i }
+       , {\m0 v m -> v > 0 }>
+       _ _
+@-}
+stFun :: Int -> State Int Int
+stFun i = do
+  put i
+  get

tests/ple/pos/TestLF780.hs

@@ -2441,6 +2441,7 @@ executable ple-pos
                     , T1424A
                     , T1424
                     , T2582
+                    , TestLF780
                     , Tmp1
                     , Tmp
                     , ReaderEta