Add support for sbv-12.0

grisette.cabal

@@ -1,37 +1,37 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.38.0.
+-- This file has been generated from package.yaml by hpack version 0.37.0.
 --
 -- see: https://github.com/sol/hpack
 
-name:               grisette
-version:            0.13.0.0
-synopsis:           Symbolic evaluation as a library
-description:        Grisette is a reusable symbolic evaluation library for Haskell. By
-                    translating programs into constraints, Grisette can help the development of
-                    program reasoning tools, including verification, synthesis, and more.
-                    .
-                    The "Grisette" module exports all the core APIs for building a symbolic
-                    evaluation tool. A high-level overview of the module structures are available
-                    there.
-                    .
-                    A detailed introduction to Grisette is available at "Grisette.Core". More
-                    lifted libraries are provided in @Grisette.Lib.*@ modules.
-                    .
-                    The "Grisette.Unified" module offers an experimental unified interface for
-                    symbolic and concrete evaluation. This module should be imported qualified.
-                    .
-                    For more details, please checkout the README and 
-                    [tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials).
-category:           Formal Methods, Theorem Provers, Symbolic Computation, SMT
-homepage:           https://github.com/lsrcz/grisette#readme
-bug-reports:        https://github.com/lsrcz/grisette/issues
-author:             Sirui Lu, Rastislav Bodík
-maintainer:         Sirui Lu (siruilu@cs.washington.edu)
-copyright:          2021-2024 Sirui Lu
-license:            BSD3
-license-file:       LICENSE
-build-type:         Simple
+name:           grisette
+version:        0.13.0.1
+synopsis:       Symbolic evaluation as a library
+description:    Grisette is a reusable symbolic evaluation library for Haskell. By
+                translating programs into constraints, Grisette can help the development of
+                program reasoning tools, including verification, synthesis, and more.
+                .
+                The "Grisette" module exports all the core APIs for building a symbolic
+                evaluation tool. A high-level overview of the module structures are available
+                there.
+                .
+                A detailed introduction to Grisette is available at "Grisette.Core". More
+                lifted libraries are provided in @Grisette.Lib.*@ modules.
+                .
+                The "Grisette.Unified" module offers an experimental unified interface for
+                symbolic and concrete evaluation. This module should be imported qualified.
+                .
+                For more details, please checkout the README and 
+                [tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials).
+category:       Formal Methods, Theorem Provers, Symbolic Computation, SMT
+homepage:       https://github.com/lsrcz/grisette#readme
+bug-reports:    https://github.com/lsrcz/grisette/issues
+author:         Sirui Lu, Rastislav Bodík
+maintainer:     Sirui Lu (siruilu@cs.washington.edu)
+copyright:      2021-2024 Sirui Lu
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
 tested-with:
     GHC == 8.10.7
   , GHC == 9.0.2
@@ -329,7 +329,7 @@ library
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2 && <3.3
     , prettyprinter >=1.5.0 && <1.8
-    , sbv >=8.17 && <12
+    , sbv >=8.17 && <13
     , stm ==2.5.*
     , template-haskell >=2.16 && <2.24
     , text >=1.2.4.1 && <2.2
@@ -378,7 +378,7 @@ test-suite doctest
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2 && <3.3
     , prettyprinter >=1.5.0 && <1.8
-    , sbv >=8.17 && <12
+    , sbv >=8.17 && <13
     , stm ==2.5.*
     , template-haskell >=2.16 && <2.24
     , text >=1.2.4.1 && <2.2
@@ -499,7 +499,7 @@ test-suite spec
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2 && <3.3
     , prettyprinter >=1.5.0 && <1.8
-    , sbv >=8.17 && <12
+    , sbv >=8.17 && <13
     , stm ==2.5.*
     , template-haskell >=2.16 && <2.24
     , test-framework >=0.8.2 && <0.9

package.yaml

@@ -1,5 +1,5 @@
 name: grisette
-version: 0.13.0.0
+version: 0.13.0.1
 synopsis: Symbolic evaluation as a library
 description: "Grisette is a reusable symbolic evaluation library for Haskell. By\ntranslating programs into constraints, Grisette can help the development of\nprogram reasoning tools, including verification, synthesis, and more.\n.\nThe \"Grisette\" module exports all the core APIs for building a symbolic\nevaluation tool. A high-level overview of the module structures are available\nthere.\n.\nA detailed introduction to Grisette is available at \"Grisette.Core\". More\nlifted libraries are provided in @Grisette.Lib.*@ modules.\n.\nThe \"Grisette.Unified\" module offers an experimental unified interface for\nsymbolic and concrete evaluation. This module should be imported qualified.\n.\nFor more details, please checkout the README and \n[tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials).\n"
 category: Formal Methods, Theorem Provers, Symbolic Computation, SMT
@@ -36,7 +36,7 @@ dependencies:
   - th-compat >= 0.1.2 && < 0.2
   - th-abstraction >= 0.4 && < 0.8
   - array >= 0.5.4 && < 0.6
-  - sbv >= 8.17 && < 12
+  - sbv >= 8.17 && < 13
   - parallel >= 3.2.2 && < 3.3
   - text >= 1.2.4.1 && < 2.2
   - QuickCheck >= 2.14 && < 2.17

src/Grisette/Internal/SymPrim/FP.hs

@@ -219,6 +219,28 @@ invalidFPMessage =
     <> "        sb `elem` [2 .. 4611686018427387902]\n\n"
     <> "  Given type falls outside of this range, or the sizes are not known naturals."
 
+#if MIN_VERSION_sbv(12,0,0)
+-- | Provide an (unsafe) type-level proof that the given floating-point type is
+-- valid.
+withUnsafeValidFP ::
+  forall eb sb r. (KnownNat eb, KnownNat sb) => ((ValidFP eb sb) => r) -> r
+withUnsafeValidFP r =
+  let eb = natVal (Proxy @eb)
+      sb = natVal (Proxy @sb)
+   in if checkDynamicValidFP eb sb
+        then case unsafeAxiom @True
+          @( ((CmpNat eb 2 == 'EQ) || (CmpNat eb 2 == 'GT))
+               && ( ((CmpNat eb 29 == 'EQ) || (CmpNat eb 29 == 'LT))
+                      && ( ((CmpNat sb 2 == 'EQ) || (CmpNat sb 2 == 'GT))
+                             && ( (CmpNat sb 1073741822 == 'EQ)
+                                    || (CmpNat sb 1073741822 == 'LT)
+                                )
+                         )
+                  )
+           ) of
+          Refl -> r
+        else error invalidFPMessage
+#else
 -- | Provide an (unsafe) type-level proof that the given floating-point type is
 -- valid.
 withUnsafeValidFP ::
@@ -239,6 +261,7 @@ withUnsafeValidFP r =
            ) of
           Refl -> r
         else error invalidFPMessage
+#endif
 
 -- | IEEE 754 floating-point number with @eb@ exponent bits and @sb@ significand
 -- bits.

stack-9.10.yaml

@@ -16,7 +16,7 @@
 #
 # resolver: ./custom-snapshot.yaml
 # resolver: https://example.com/snapshots/2018-01-01.yaml
-resolver: nightly-2025-07-03
+resolver: nightly-2025-07-14
 # User packages to be built.
 # Various formats can be used as shown in the example below.
 #

stack-9.10.yaml.lock

@@ -6,7 +6,7 @@
 packages: []
 snapshots:
 - completed:
-    sha256: 1e879c64480ca43c6b796e6d48f64fa07072cbed80c1b802b48db3265510df50
-    size: 722394
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/3.yaml
-  original: nightly-2025-07-03
+    sha256: 7a26eba54b469fc72b1e37b881dfec480a2c1cb0636136f96aec7d81be6c762f
+    size: 724509
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/14.yaml
+  original: nightly-2025-07-14

stack-9.8.yaml

@@ -16,7 +16,7 @@
 #
 # resolver: ./custom-snapshot.yaml
 # resolver: https://example.com/snapshots/2018-01-01.yaml
-resolver: lts-23.18
+resolver: lts-23.27
 # User packages to be built.
 # Various formats can be used as shown in the example below.
 #

stack-9.8.yaml.lock

@@ -1,12 +1,19 @@
 # This file was autogenerated by Stack.
 # You should not edit this file by hand.
 # For more information, please see the documentation at:
-#   https://docs.haskellstack.org/en/stable/lock_files
+#   https://docs.haskellstack.org/en/stable/topics/lock_files
 
-packages: []
+packages:
+- completed:
+    hackage: sbv-12.0@sha256:91e8297e444e43921d5a628408d5469894bbe3616c5236a6ebaae5e2a0650e8a,25606
+    pantry-tree:
+      sha256: 8e0feaff1d152467ac4641c3a9e6b82ee5e3741121d41ca06f4a393ffcb52715
+      size: 77084
+  original:
+    hackage: sbv-12.0
 snapshots:
 - completed:
-    sha256: d133abe75e408a407cce3f032c96ac1bbadf474a93b5156ebf4135b53382d56b
-    size: 683827
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/23/18.yaml
-  original: lts-23.18
+    sha256: 069c8189232279d04bd107557d3a62132c04ae5ce3c710649e6b40f67f10b9d5
+    size: 684285
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/23/27.yaml
+  original: lts-23.27

stack.yaml.lock

@@ -6,7 +6,7 @@
 packages: []
 snapshots:
 - completed:
-    sha256: 1e879c64480ca43c6b796e6d48f64fa07072cbed80c1b802b48db3265510df50
-    size: 722394
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/3.yaml
-  original: nightly-2025-07-03
+    sha256: 7a26eba54b469fc72b1e37b881dfec480a2c1cb0636136f96aec7d81be6c762f
+    size: 724509
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/14.yaml
+  original: nightly-2025-07-14