Merge branch 'ucsd-progsys:develop' into develop

Author: matheussbernardo

.gitmodules

@@ -1,3 +1,3 @@
 [submodule "liquid-fixpoint"]
 	path = liquid-fixpoint
-	url = https://github.com/ucsd-progsys/liquid-fixpoint.git
+	url = https://github.com/ucsd-progsys/liquid-fixpoint.git

CHANGES.md

@@ -2,6 +2,10 @@
 
 ## Next
 
+- Simplify kvar solutions in fqout files [liquid-fixpoint#741](https://github.com/ucsd-progsys/liquid-fixpoint/pull/741).
+
+## 0.9.10.1.2 (2025-03-06)
+
 - Implement opaque reflection, a feature to allow reflecting functions which
   call to non-reflected functions [#2323](https://github.com/ucsd-progsys/liquidhaskell/pull/2323).
 - Implement reflection from interface files, which can reflect functions from
@@ -15,11 +19,20 @@
   and constraint generation [#2336](https://github.com/ucsd-progsys/liquidhaskell/pull/2336).
 - Augmented the context of error messages [#2350](https://github.com/ucsd-progsys/liquidhaskell/pull/2350).
 - Add a new flag `--etabeta` to reason with lambdas in PLE [#2356](https://github.com/ucsd-progsys/liquidhaskell/pull/2356)
+- Add a new flag `--dependentcase` to expand support for higher-order reasoning [#2384](https://github.com/ucsd-progsys/liquidhaskell/pull/2384)
+- Add support for reflecting lambda expressions [#2465](https://github.com/ucsd-progsys/liquidhaskell/pull/2465).
 - Enabling the LiquidHaskell plugin now enables `-fno-ignore-interface-pragmas` ([#2326](https://github.com/ucsd-progsys/liquidhaskell/pull/2326))
   and `-dkeep-comments` ([#2367](https://github.com/ucsd-progsys/liquidhaskell/pull/2367)).
 - LiquidHaskell earned a new `--minimal` verbosity level as default that prints the banner with the
   amount of constraints checked ([#2395](https://github.com/ucsd-progsys/liquidhaskell/pull/2395)).
   This banner is now suppressed when the verbosity is set to `--quiet` ([#2391](https://github.com/ucsd-progsys/liquidhaskell/pull/2391)).
+- Avoid reparsing and retypechecking when verifying modules [#2389](https://github.com/ucsd-progsys/liquidhaskell/pull/2389).
+- Name resolution is done only when verifying a module. It is no longer done when
+  importing it [#2169](https://github.com/ucsd-progsys/liquidhaskell/issues/2169). One
+  side effect of this change is that LH can now pick up names in scope using import aliases
+  in most places (but see [#2481](https://github.com/ucsd-progsys/liquidhaskell/issues/2481)).
+- Allow to link Haskell definitions with logical primitives via `define` declarations [#2463](https://github.com/ucsd-progsys/liquidhaskell/pull/2463).
+- CVC5 solver is now supported for all logical theories, including Sets/Bags [#2483](https://github.com/ucsd-progsys/liquidhaskell/pull/2483)
 
 ## 0.9.10.1 (2024-08-21)
 

README.md

@@ -1,7 +1,7 @@
 ![LiquidHaskell](/resources/logo.png)
 
 
-[![Hackage](https://img.shields.io/hackage/v/liquidhaskell.svg)](https://hackage.haskell.org/package/liquidhaskell) [![Hackage-Deps](https://img.shields.io/hackage-deps/v/liquidhaskell.svg)](http://packdeps.haskellers.com/feed?needle=liquidhaskell) [![Build Status](https://img.shields.io/circleci/project/ucsd-progsys/liquidhaskell/master.svg)](https://circleci.com/gh/ucsd-progsys/liquidhaskell)
+[![Hackage](https://img.shields.io/hackage/v/liquidhaskell.svg)](https://hackage.haskell.org/package/liquidhaskell) [![Build Status](https://img.shields.io/circleci/project/ucsd-progsys/liquidhaskell/develop.svg)]([https://circleci.com/gh/ucsd-progsys/liquidhaskell](https://app.circleci.com/pipelines/github/ucsd-progsys/liquidhaskell?branch=develop))
 
 This is the **development** site of the LiquidHaskell formal verification tool.
 
@@ -98,7 +98,11 @@ For example:
 
     $ cabal build tests:unit-neg --ghc-options=-fplugin-opt=LiquidHaskell:--no-termination
 
-Or your favorite number of threads, depending on cores etc.
+Another useful option is to change the underlying solver:
+
+    $ cabal build tests:unit-pos --ghc-options=-fplugin-opt=LiquidHaskell:--smtsolver=cvc5
+
+You can also modify the number of used threads, depending on cores etc.
 
 You can directly extend and run the tests by modifying the files in
 

docs/mkDocs/docs/options.md

@@ -359,16 +359,15 @@ to run a given file with full-checking, add the pragma:
 
 **Options:** `smtsolver`
 
-By default, LiquidHaskell uses the SMTLIB2 interface for Z3.
+By default, LiquidHaskell uses the SMTLIB2 interface for [Z3](https://github.com/Z3Prover/z3).
 
 To run a different solver (supporting SMTLIB2) do:
 
     $ liquid --smtsolver=NAME foo.hs
 
-Currently, LiquidHaskell supports
+Currently, LiquidHaskell additionally supports
 
-+ [CVC4](http://cvc4.cs.stanford.edu/web/)
-+ [MathSat](http://mathsat.fbk.eu/download.html )
++ [CVC5](https://cvc5.github.io/)
 
 To use these solvers, you must install the corresponding binaries
 from the above web-pages into your `PATH`.

docs/mkDocs/docs/specifications.md

@@ -1026,3 +1026,22 @@ Or in a Haskell source file:
 - No support for abstract refinements. All abstract refinements are erased before relational typechecking. Notably, this happens for the standard list `[a]` and tuple `(a, b)` types!
 
 - Limited support for higher-order relational signatures. Use `!=>` instead of `:=>` after the function arguments to enable higher-order checking.
+
+## Lazy Variables
+
+A variable can be specified as `lazyvar` to defer its checking until it is used. This is useful in cases where a variable is defined in a `where` clause and should only be checked in the context where it is used.
+
+For example, consider the following code:
+
+```haskell
+{-@ safeDiv :: Int -> {v:Int | v /= 0} -> Int @-}
+safeDiv :: Int -> Int -> Int
+safeDiv x y
+  | y == 0 = help
+  | otherwise = x `div` y
+  where
+    {-@ lazyvar help @-}
+    help = error "lol"
+```
+
+In this example, the `lazyvar` annotation on `help` ensures that the check for `help` is deferred until it is used. Without this annotation, LiquidHaskell would incorrectly report an error like `Error: Liquid Type Mismatch`.

liquid-fixpoint

@@ -23,8 +23,8 @@ data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
 empty :: Bag k
 empty = Bag M.empty
 
-{-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Bag_count b k}  @-}
-{-@ define get               k      b                    = (Bag_count b k) @-}
+{-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Bag_count k b}  @-}
+{-@ define get               k      b                    = (Bag_count k b) @-}
 get :: (Ord k) => k -> Bag k -> Int
 get k b = M.findWithDefault 0 k (toMap b)
 

liquid-prelude/src/Language/Haskell/Liquid/Bag.hs

@@ -75,7 +75,7 @@ _ *** _ = ()
 
 data QED = Admit | QED
 
-{-@ measure isAdmit :: QED -> Bool @-}
+{-@ measure isAdmit @-}
 isAdmit :: QED -> Bool
 isAdmit Admit = True
 isAdmit QED   = False

liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs

@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               liquidhaskell-boot
-version:            0.9.10.1
+version:            0.9.10.1.2
 synopsis:           Liquid Types for Haskell
 description:        This package provides a plugin to verify Haskell programs.
                     But most likely you should be using the [liquidhaskell package](https://hackage.haskell.org/package/liquidhaskell)
@@ -142,7 +142,7 @@ library
                     , gitrev
                     , hashable             >= 1.3 && < 1.6
                     , hscolour             >= 1.22
-                    , liquid-fixpoint      == 0.9.6.3.1
+                    , liquid-fixpoint      == 0.9.6.3.2
                     , mtl                  >= 2.1
                     , optparse-applicative < 0.19
                     , githash
@@ -202,7 +202,6 @@ test-suite ghc-api-tests
 test-suite liquidhaskell-parser
   type:             exitcode-stdio-1.0
   main-is:          Parser.hs
-  other-modules:    Paths_liquidhaskell_boot
   hs-source-dirs:   tests
   build-depends:    base            >= 4.8.1.0 && < 5
                   , directory       >= 1.2.5 && < 1.4

liquidhaskell-boot/liquidhaskell-boot.cabal

@@ -58,6 +58,7 @@ import qualified Language.Haskell.Liquid.Bare.Axiom         as Bare
 import qualified Language.Haskell.Liquid.Bare.ToBare        as Bare
 import qualified Language.Haskell.Liquid.Bare.Class         as Bare
 import qualified Language.Haskell.Liquid.Bare.Check         as Bare
+import qualified Language.Haskell.Liquid.Bare.Resolve       as Resolve
 import qualified Language.Haskell.Liquid.Bare.Typeclass     as Bare
 import qualified Language.Haskell.Liquid.Transforms.CoreToLogic as CoreToLogic
 import           Language.Haskell.Liquid.UX.Config
@@ -178,7 +179,6 @@ ghcSpecEnv sp = F.notracepp "RENV" $ fromListSEnv binds
                  [ [(x,        rSort t) | (x, Loc _ _ t)  <- gsMeas     (_gsData sp)]
                  , [(symbol v, rSort t) | (v, Loc _ _ t)  <- gsCtors    (_gsData sp)]
                  , [(symbol v, vSort v) | v               <- gsReflects (_gsRefl sp)]
-                 , [(x,        vSort v) | (x, v)          <- gsFreeSyms (_gsName sp), Ghc.isConLikeId v ]
                  , [(x, RR s mempty)    | (x, s)          <- wiredSortedSyms       ]
                  , [(x, RR s mempty)    | (x, s)          <- _gsImps sp       ]
                  ]
@@ -252,7 +252,7 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
     , _gsRefl   = refl
     , _gsData   = sData
     , _gsQual   = qual
-    , _gsName   = makeSpecName env     tycEnv measEnv
+    , _gsName   = makeSpecName tycEnv measEnv dataConIds
     , _gsVars   = spcVars
     , _gsTerm   = spcTerm
 
@@ -334,12 +334,19 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
     embs     = makeEmbeds          src ghcTyLookupEnv (mySpec0 : map snd dependencySpecs)
     dm       = Bare.tcDataConMap tycEnv0
     (dg0, datacons, tycEnv0) = makeTycEnv0   cfg name env embs mySpec2 iSpecs2
-    env      = Bare.makeEnv cfg ghcTyLookupEnv usedDcs tcg instEnvs localVars src lmap ((name, targetSpec) : dependencySpecs)
+    env      = Bare.makeEnv cfg ghcTyLookupEnv dataConIds tcg instEnvs localVars src lmap ((name, targetSpec) : dependencySpecs)
     -- check barespecs
     name     = F.notracepp ("ALL-SPECS" ++ zzz) $ _giTargetMod  src
     zzz      = F.showpp (fst <$> mspecs)
 
     usedDcs  = collectAllDataCons (_giCbs src) $ targetSpec : map snd dependencySpecs
+    dataConIds =
+      [ Ghc.dataConWorkId dc
+      | lhn <- S.toList usedDcs
+      , Just (Ghc.AConLike (Ghc.RealDataCon dc)) <-
+          [maybeReflectedLHName lhn >>= Resolve.lookupGhcTyThingFromName ghcTyLookupEnv]
+      ]
+
 
 collectAllDataCons :: Ghc.CoreProgram -> [BareSpec] -> S.HashSet LHName
 collectAllDataCons cbs =
@@ -1183,16 +1190,16 @@ mkReft _ _ _ _
 
 -- REBARE: formerly, makeGhcSpec3
 -------------------------------------------------------------------------------------------
-makeSpecName :: Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> GhcSpecNames
+makeSpecName :: Bare.TycEnv -> Bare.MeasEnv -> [Ghc.Id] -> GhcSpecNames
 -------------------------------------------------------------------------------------------
-makeSpecName env tycEnv measEnv = SpNames
-  { gsFreeSyms = Bare.reSyms env
-  , gsDconsP   = [ F.atLoc dc (dcpCon dc) | dc <- datacons ++ cls ]
+makeSpecName tycEnv measEnv dataConIds = SpNames
+  { gsDconsP   = [ F.atLoc dc (dcpCon dc) | dc <- datacons ++ cls ]
   , gsTconsP   = tycons
   -- , gsLits = mempty                                              -- TODO-REBARE, redundant with gsMeas
   , gsTcEmbeds = Bare.tcEmbs     tycEnv
   , gsADTs     = Bare.tcAdts     tycEnv
   , gsTyconEnv = Bare.tcTyConMap tycEnv
+  , gsDataConIds = dataConIds
   }
   where
     datacons, cls :: [DataConP]
@@ -1373,12 +1380,10 @@ makeLiftedSpec name src env refl sData sig qual myRTE lSpec0 = lSpec0
   where
     myDCs         = filter (isLocalName . val . fst) $ mkSigs (gsCtors sData)
     mkSigs xts    = [ toBare (x, t) | (x, t) <- xts
-                    ,  S.member x sigVars && isExportedVar (toTargetSrc src) x
+                    , not (S.member x reflVars) && isExportedVar (toTargetSrc src) x
                     ]
     toBare (x, t) = (makeGHCLHNameLocatedFromId x, Bare.specToBare <$> t)
     xbs           = toBare <$> reflTySigs
-    sigVars       = S.difference defVars reflVars
-    defVars       = S.fromList (_giDefVars src)
     reflTySigs    = [(x, t) | (x,t,_) <- gsHAxioms refl]
     reflVars      = S.fromList (fst <$> reflTySigs)
     -- myAliases fld = M.elems . fld $ myRTE