bring up to date with functors-merge

.github/ci.sh

@@ -77,7 +77,7 @@ install_system_deps() {
   cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
   export PATH=$BIN:$PATH
   echo "$BIN" >> "$GITHUB_PATH"
-  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices
+  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices
 }
 
 check_docs() {
@@ -132,6 +132,7 @@ zip_dist_with_solvers() {
   sname="${name}-with-solvers"
   cp "$(which abc)"        dist/bin/
   cp "$(which cvc4)"       dist/bin/
+  cp "$(which cvc5)"       dist/bin/
   cp "$(which yices)"      dist/bin/
   cp "$(which yices-smt2)" dist/bin/
   cp "$(which z3)"         dist/bin/

.github/workflows/ci.yml

@@ -9,7 +9,7 @@ on:
   workflow_dispatch:
 
 env:
-  SOLVER_PKG_VERSION: "snapshot-20220812"
+  SOLVER_PKG_VERSION: "snapshot-20221212"
   # The CACHE_VERSION can be updated to force the use of a new cache if
   # the current cache contents become corrupted/invalid.  This can
   # sometimes happen when (for example) the OS version is changed but
@@ -315,6 +315,7 @@ jobs:
           .github/ci.sh install_system_deps
           .github/ci.sh deps bin/abc*
           .github/ci.sh deps bin/cvc4*
+          .github/ci.sh deps bin/cvc5*
           .github/ci.sh deps bin/yices-smt2*
           .github/ci.sh deps bin/z3*
           ghc_ver="$(ghc --numeric-version)"

CHANGES.md

@@ -30,10 +30,16 @@
 * Add a syntax highlight file for Vim,
   available in `syntax-highlight/cryptol.vim`
 
-* Add `:new-seed` and `:set-seed` commands to the REPL. 
+* Add `:new-seed` and `:set-seed` commands to the REPL.
   These affect random test generation,
   and help write reproducable Cryptol scripts.
 
+* Add support for the CVC5 solver, which can be selected with
+  `:set prover=cvc5`. If you want to specify a What4 or SBV backend, you can
+  use `:set prover=w4-cvc5` or `:set prover=sbv-cvc5`, respectively. (Note that
+  `sbv-cvc5` is non-functional on Windows at this time due to a downstream issue
+  with CVC5 1.0.4 and earlier.)
+
 * Add `:file-deps` commands to the REPL and Python API.
   It shows information about the source files and dependencies of
   modules or Cryptol files.

Dockerfile

@@ -14,7 +14,7 @@ USER cryptol
 WORKDIR /cryptol
 RUN mkdir -p rootfs/usr/local/bin
 WORKDIR /cryptol/rootfs/usr/local/bin
-RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220812/ubuntu-22.04-bin.zip"
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20221212/ubuntu-22.04-bin.zip"
 RUN unzip solvers.zip && rm solvers.zip && chmod +x *
 WORKDIR /cryptol
 ENV PATH=/cryptol/rootfs/usr/local/bin:/home/cryptol/.local/bin:/home/cryptol/.ghcup/bin:$PATH
@@ -40,6 +40,7 @@ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
 RUN    ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \
     #    && ! $(cryptol -c ":s prover=mathsat" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=cvc4" | tail -n +2 | grep -q .) \
+    && ! $(cryptol -c ":s prover=cvc5" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \
     # && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .)

README.md

@@ -25,7 +25,7 @@ predicates written in Cryptol against randomly-generated test vectors
 (in the style of
 [QuickCheck](http://hackage.haskell.org/package/QuickCheck)). There is
 also a `:prove` command, which calls out to SMT solvers, such as
-Yices, Z3, or CVC4, to prove predicates for all possible inputs.
+Yices, Z3, CVC4, or CVC5, to prove predicates for all possible inputs.
 
 # Getting Cryptol Binaries
 
@@ -46,7 +46,7 @@ Cryptol currently uses Microsoft Research's [Z3 SMT
 solver](https://github.com/Z3Prover/z3) by default to solve constraints
 during type checking, and as the default solver for the `:sat` and
 `:prove` commands.  Cryptol generally requires the most recent version
-of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20220812).
+of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20221212).
 
 You can download Z3 binaries for a variety of platforms from their
 [releases page](https://github.com/Z3Prover/z3/releases). If you

cabal.GHC-8.10.7.config

@@ -207,7 +207,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              s-cargot -build-example,
              any.safe ==0.3.19,
              any.safe-exceptions ==0.1.7.3,
-             any.sbv ==9.0,
+             any.sbv ==9.2,
              any.scientific ==0.3.7.0,
              scientific -bytestring-builder -integer-simple,
              any.scotty ==0.12.1,

cabal.GHC-9.2.4.config

@@ -208,7 +208,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              s-cargot -build-example,
              any.safe ==0.3.19,
              any.safe-exceptions ==0.1.7.3,
-             any.sbv ==9.0,
+             any.sbv ==9.2,
              any.scientific ==0.3.7.0,
              scientific -bytestring-builder -integer-simple,
              any.scotty ==0.12.1,

cabal.GHC-9.4.4.config

@@ -208,7 +208,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              s-cargot -build-example,
              any.safe ==0.3.19,
              any.safe-exceptions ==0.1.7.3,
-             any.sbv ==9.0,
+             any.sbv ==9.2,
              any.scientific ==0.3.7.0,
              scientific -bytestring-builder -integer-simple,
              any.scotty ==0.12.1,

cryptol-remote-api/Dockerfile

@@ -64,7 +64,7 @@ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
 RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
     && cp -r lib/* rootfs/"${CRYPTOLPATH}"
 WORKDIR /cryptol/rootfs/usr/local/bin
-RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220812/ubuntu-22.04-bin.zip" && \
+RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20221212/ubuntu-22.04-bin.zip" && \
     unzip solvers.zip && rm solvers.zip && chmod +x *
 USER root
 RUN chown -R root:root /cryptol/rootfs

cryptol-remote-api/cryptol-remote-api.cabal

@@ -55,7 +55,7 @@ common deps
     text                 >= 1.2.3 && < 2.1,
     tf-random,
     unordered-containers ^>= 0.2,
-    vector               ^>= 0.13,
+    vector               >= 0.12 && < 0.14,
 
   default-language:    Haskell2010
 

cryptol-remote-api/docs/Cryptol.rst

@@ -606,7 +606,7 @@ Parameter fields
 
 
 ``prover``
-  The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
+  The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-cvc5``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``cvc5``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-cvc5``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
   
   
 

cryptol-remote-api/python/cryptol/solver.py

@@ -52,6 +52,7 @@ class OfflineSolver(Solver):
 # Cryptol-supported SMT configurations/solvers
 # (see Cryptol.Symbolic.SBV Haskell module)
 CVC4: OnlineSolver          = OnlineSolver("cvc4")
+CVC5: OnlineSolver          = OnlineSolver("cvc5")
 YICES: OnlineSolver         = OnlineSolver("yices")
 Z3: OnlineSolver            = OnlineSolver("z3")
 BOOLECTOR: OnlineSolver     = OnlineSolver("boolector")
@@ -60,6 +61,7 @@ ABC: OnlineSolver           = OnlineSolver("abc")
 OFFLINE: OfflineSolver      = OfflineSolver("offline")
 ANY: OnlineSolver           = OnlineSolver("any")
 SBV_CVC4: OnlineSolver      = OnlineSolver("sbv-cvc4")
+SBV_CVC5: OnlineSolver      = OnlineSolver("sbv-cvc5")
 SBV_YICES: OnlineSolver     = OnlineSolver("sbv-yices")
 SBV_Z3: OnlineSolver        = OnlineSolver("sbv-z3")
 SBV_BOOLECTOR: OnlineSolver = OnlineSolver("sbv-boolector")
@@ -68,6 +70,7 @@ SBV_ABC: OnlineSolver       = OnlineSolver("sbv-abc")
 SBV_OFFLINE: OfflineSolver  = OfflineSolver("sbv-offline")
 SBV_ANY: OnlineSolver       = OnlineSolver("sbv-any")
 W4_CVC4: OnlineSolver       = OnlineSolver("w4-cvc4")
+W4_CVC5: OnlineSolver       = OnlineSolver("w4-cvc5")
 W4_YICES: OnlineSolver      = OnlineSolver("w4-yices")
 W4_Z3: OnlineSolver         = OnlineSolver("w4-z3")
 W4_BOOLECTOR: OnlineSolver  = OnlineSolver("w4-boolector")

cryptol.cabal

@@ -74,7 +74,7 @@ library
                        prettyprinter     >= 1.7.0,
                        pretty-show,
                        process           >= 1.2,
-                       sbv               >= 8.10 && < 9.1,
+                       sbv               >= 9.1 && < 9.3,
                        simple-smt        >= 0.9.7,
                        stm               >= 2.4,
                        strict,

cryptol/Main.hs

@@ -200,7 +200,7 @@ displayHelp errs = do
             , "via the `:edit` command"
             ]
           )
-        , ( "SBV_{ABC,BOOLECTOR,CVC4,MATHSAT,YICES,Z3}_OPTIONS"
+        , ( "SBV_{ABC,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"
           , [ "A string of command-line arguments to be passed to the"
             , "corresponding solver invoked for `:sat` and `:prove`"
             , "when using a prover via SBV"

src/Cryptol/ModuleSystem/Interface.hs

@@ -159,7 +159,7 @@ instance Monoid IfaceDecls where
                   , ifFunctors = mempty
                   , ifSignatures = mempty
                   }
-  mappend l r = l <> r
+  mappend = (<>)
   mconcat ds  = IfaceDecls
     { ifTySyns   = Map.unions (map ifTySyns   ds)
     , ifNewtypes = Map.unions (map ifNewtypes ds)

src/Cryptol/Symbolic/SBV.hs

@@ -81,6 +81,7 @@ doSBVEval m =
 proverConfigs :: [(String, SBV.SMTConfig)]
 proverConfigs =
   [ ("cvc4"     , SBV.cvc4     )
+  , ("cvc5"     , SBV.cvc5     )
   , ("yices"    , SBV.yices    )
   , ("z3"       , SBV.z3       )
   , ("boolector", SBV.boolector)
@@ -90,6 +91,7 @@ proverConfigs =
   , ("any"      , SBV.defaultSMTCfg )
 
   , ("sbv-cvc4"     , SBV.cvc4     )
+  , ("sbv-cvc5"     , SBV.cvc5     )
   , ("sbv-yices"    , SBV.yices    )
   , ("sbv-z3"       , SBV.z3       )
   , ("sbv-boolector", SBV.boolector)

src/Cryptol/Symbolic/What4.hs

@@ -83,6 +83,7 @@ import qualified What4.SWord as SW
 import           What4.Solver
 import qualified What4.Solver.Boolector as W4
 import qualified What4.Solver.CVC4 as W4
+import qualified What4.Solver.CVC5 as W4
 import qualified What4.Solver.ExternalABC as W4
 import qualified What4.Solver.Yices as W4
 import qualified What4.Solver.Z3 as W4
@@ -161,6 +162,7 @@ data W4ProverConfig
 proverConfigs :: [(String, W4ProverConfig)]
 proverConfigs =
   [ ("w4-cvc4"      , W4ProverConfig cvc4OnlineAdapter)
+  , ("w4-cvc5"      , W4ProverConfig cvc5OnlineAdapter)
   , ("w4-yices"     , W4ProverConfig yicesOnlineAdapter)
   , ("w4-z3"        , W4ProverConfig z3OnlineAdapter)
   , ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter)
@@ -186,6 +188,11 @@ cvc4OnlineAdapter =
   AnOnlineAdapter "CVC4" W4.cvc4Features W4.cvc4Options
          (Proxy :: Proxy (W4.Writer W4.CVC4))
 
+cvc5OnlineAdapter :: AnAdapter
+cvc5OnlineAdapter =
+  AnOnlineAdapter "CVC5" W4.cvc5Features W4.cvc5Options
+         (Proxy :: Proxy (W4.Writer W4.CVC5))
+
 boolectorOnlineAdapter :: AnAdapter
 boolectorOnlineAdapter =
   AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions
@@ -195,6 +202,7 @@ allSolvers :: W4ProverConfig
 allSolvers = W4Portfolio
   $ z3OnlineAdapter :|
   [ cvc4OnlineAdapter
+  , cvc5OnlineAdapter
   , boolectorOnlineAdapter
   , yicesOnlineAdapter
   , AnAdapter W4.externalABCAdapter

src/Cryptol/TypeCheck/Subst.hs

@@ -7,10 +7,7 @@
 -- Portability :  portable
 
 {-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveFoldable #-}
 {-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -265,7 +262,15 @@ apSubstMaybe su ty =
          Just (TUser f ts1 t1)
 
     TRec fs -> TRec `fmap` (anyJust (apSubstMaybe su) fs)
-    TNewtype nt ts -> TNewtype nt `fmap` anyJust (apSubstMaybe su) ts
+
+    {- We apply the substitution to the newtype as well, because it might
+    contain module parameters, which need to be substituted when
+    instantiating a functor. -}
+    TNewtype nt ts ->
+      uncurry TNewtype <$> anyJust2 (applySubstToNewtype su)
+                                    (anyJust (apSubstMaybe su))
+                                    (nt,ts)
+
     TVar x -> applySubstToVar su x
 
 lookupSubst :: TVar -> Subst -> Maybe Type
@@ -287,6 +292,16 @@ applySubstToVar su x =
       | suDefaulting su -> Just $! defaultFreeVar x
       | otherwise       -> Nothing
 
+
+applySubstToNewtype :: Subst -> Newtype -> Maybe Newtype
+applySubstToNewtype su nt =
+  do (cs,fs) <- anyJust2
+                  (anyJust (apSubstMaybe su))
+                  (anyJust (apSubstMaybe su))
+                  (ntConstraints nt, ntFields nt)
+     pure nt { ntConstraints = cs, ntFields = fs }
+
+
 class TVars t where
   apSubst :: Subst -> t -> t
   -- ^ Replaces free variables. To prevent space leaks when used with
@@ -432,7 +447,7 @@ instance TVars DeclGroup where
 
 instance TVars Decl where
   apSubst su d =
-    let !sig' = id $! apSubst su (dSignature d)
+    let !sig' = apSubst su (dSignature d)
         !def' = apSubst su (dDefinition d)
     in d { dSignature = sig', dDefinition = def' }
 

src/Cryptol/TypeCheck/Type.hs

@@ -1054,6 +1054,17 @@ ppNewtypeShort nt =
   ps  = ntParams nt
   nm = addTNames ps emptyNameMap
 
+ppNewtypeFull :: Newtype -> Doc
+ppNewtypeFull nt =
+  text "newtype" <+> pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
+  $$ nest 2 (cs $$ ("=" <+> pp (ntConName nt) $$ nest 2 fs))
+  where
+  ps = ntParams nt
+  nm = addTNames ps emptyNameMap
+  fs = vcat [ pp f <.> ":" <+> pp t | (f,t) <- canonicalFields (ntFields nt) ]
+  cs = vcat (map pp (ntConstraints nt))
+
+
 
 instance PP Schema where
   ppPrec = ppWithNamesPrec IntMap.empty

tests/issues/issue1503.cry

@@ -0,0 +1,4 @@
+add_mul_lemma : Integer -> Integer -> Integer -> Integer -> Bit
+add_mul_lemma m n p q =
+  (0 <= m /\ 0 <= n /\ 0 <= p /\ 0 <= q /\ n < q /\ p < m) ==>
+  (m * n + p < m * q)

tests/issues/issue1503.icry

@@ -0,0 +1,11 @@
+:l issue1503.cry
+
+:set prover=w4-cvc5
+:prove add_mul_lemma
+
+// We avoid testing sbv-cvc5 for now, as using CVC5 with SBV on Windows will go
+// likely go into an infinite loop.
+// See https://github.com/LeventErkok/sbv/issues/644.
+//
+// :set prover=sbv-cvc5
+// :prove add_mul_lemma

tests/issues/issue1503.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Q.E.D.

tests/modsys/functors/T040.cry

@@ -0,0 +1,17 @@
+
+submodule F where
+  parameter
+    type T : *
+
+  newtype NT = { field : T -> () }
+
+  nt : NT
+  nt = NT { field = \_ -> () }
+
+import submodule F where
+  type T = [32]
+
+
+x = nt.field 10
+
+

tests/modsys/functors/T040.icry

@@ -0,0 +1,2 @@
+:load T040.cry
+x

tests/modsys/functors/T040.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+()