New bitvector interface with hidden type-level length

LICENSE

@@ -27,4 +27,39 @@ LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+-------------------------------------------------------------------------------
+
+This repository contains code from the parameterized-utils package:
+
+Copyright (c) 2013-2022 Galois Inc.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+  * Redistributions of source code must retain the above copyright
+    notice, this list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above copyright
+    notice, this list of conditions and the following disclaimer in
+    the documentation and/or other materials provided with the
+    distribution.
+
+  * Neither the name of Galois, Inc. nor the names of its contributors
+    may be used to endorse or promote products derived from this
+    software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

grisette.cabal

@@ -109,6 +109,8 @@ library
       Grisette.Lib.Data.List
       Grisette.Lib.Data.Traversable
       Grisette.Lib.Mtl
+      Grisette.Utils
+      Grisette.Utils.Parameterized
   other-modules:
       Paths_grisette
   hs-source-dirs:

src/Grisette.hs

@@ -19,6 +19,9 @@ module Grisette
 
     -- * Solver backend
     module Grisette.Backend.SBV,
+
+    -- * Utils
+    module Grisette.Utils,
   )
 where
 
@@ -27,3 +30,4 @@ import Grisette.Core
 import Grisette.IR.SymPrim
 import Grisette.Lib.Base
 import Grisette.Lib.Mtl
+import Grisette.Utils

src/Grisette/Backend/SBV/Data/SMT/Lowering.hs

@@ -56,31 +56,10 @@ import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
 import Grisette.IR.SymPrim.Data.Prim.Model as PM
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
 import Grisette.IR.SymPrim.Data.TabularFun
+import Grisette.Utils.Parameterized
 import qualified Type.Reflection as R
 import Unsafe.Coerce
 
-newtype NatRepr (n :: Nat) = NatRepr Natural
-
-withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
-withKnownNat (NatRepr nVal) v =
-  case someNatVal nVal of
-    SomeNat (Proxy :: Proxy n') ->
-      case unsafeAxiom :: n :~: n' of
-        Refl -> v
-
-data LeqProof (m :: Nat) (n :: Nat) where
-  LeqProof :: m <= n => LeqProof m n
-
--- | Assert a proof of equality between two types.
--- This is unsafe if used improperly, so use this with caution!
-unsafeAxiom :: forall a b. a :~: b
-unsafeAxiom = unsafeCoerce (Refl @a)
-{-# NOINLINE unsafeAxiom #-} -- Note [Mark unsafe axioms as NOINLINE]
-
-unsafeLeqProof :: forall m n. LeqProof m n
-unsafeLeqProof = unsafeCoerce (LeqProof @0 @0)
-{-# NOINLINE unsafeLeqProof #-} -- Note [Mark unsafe axioms as NOINLINE]
-
 cachedResult ::
   forall integerBitWidth a.
   (SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
@@ -276,38 +255,32 @@ lowerSinglePrimImpl' config t@(BVConcatTerm _ (bv1 :: Term x) (bv2 :: Term y)) =
 lowerSinglePrimImpl' config t@(BVSelectTerm _ (ix :: R.TypeRep ix) w (bv :: Term x)) =
   case (R.typeRep @a, R.typeRep @x) of
     (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy xn)) ->
-      withKnownNat n1 $
+      withKnownProof (unsafeKnownProof @(na + ix - 1) (natVal (Proxy @na) + natVal (Proxy @ix) - 1)) $
         case ( unsafeAxiom @(na + ix - 1 - ix + 1) @na,
                unsafeLeqProof @(na + ix - 1 + 1) @xn,
                unsafeLeqProof @ix @(na + ix - 1)
              ) of
           (Refl, LeqProof, LeqProof) ->
             lowerUnaryTerm' config t bv (SBV.bvExtract (Proxy @(na + ix - 1)) (Proxy @ix))
-      where
-        n1 :: NatRepr (na + ix - 1)
-        n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)
     (SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy xn)) ->
-      withKnownNat n1 $
+      withKnownProof (unsafeKnownProof @(na + ix - 1) (natVal (Proxy @na) + natVal (Proxy @ix) - 1)) $
         case ( unsafeAxiom @(na + ix - 1 - ix + 1) @na,
                unsafeLeqProof @(na + ix - 1 + 1) @xn,
                unsafeLeqProof @ix @(na + ix - 1)
              ) of
           (Refl, LeqProof, LeqProof) ->
             lowerUnaryTerm' config t bv (SBV.bvExtract (Proxy @(na + ix - 1)) (Proxy @ix))
-      where
-        n1 :: NatRepr (na + ix - 1)
-        n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)
     _ -> translateTernaryError "bvselect" ix w (R.typeRep @x) (R.typeRep @a)
 lowerSinglePrimImpl' config t@(BVExtendTerm _ signed (n :: R.TypeRep n) (bv :: Term x)) =
   case (R.typeRep @a, R.typeRep @x) of
     (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->
-      withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - nx)) $
+      withKnownProof (unsafeKnownProof @(na - nx) (natVal (Proxy @na) - natVal (Proxy @nx))) $
         case (unsafeLeqProof @(nx + 1) @na, unsafeLeqProof @1 @(na - nx)) of
           (LeqProof, LeqProof) ->
             bvIsNonZeroFromGEq1 @(na - nx) $
               lowerUnaryTerm' config t bv (if signed then SBV.signExtend else SBV.zeroExtend)
     (SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->
-      withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - nx)) $
+      withKnownProof (unsafeKnownProof @(na - nx) (natVal (Proxy @na) - natVal (Proxy @nx))) $
         case (unsafeLeqProof @(nx + 1) @na, unsafeLeqProof @1 @(na - nx)) of
           (LeqProof, LeqProof) ->
             bvIsNonZeroFromGEq1 @(na - nx) $
@@ -669,38 +642,32 @@ lowerSinglePrimImpl config t@(BVConcatTerm _ (bv1 :: Term x) (bv2 :: Term y)) m
 lowerSinglePrimImpl config t@(BVSelectTerm _ (ix :: R.TypeRep ix) w (bv :: Term x)) m =
   case (R.typeRep @a, R.typeRep @x) of
     (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy xn)) ->
-      withKnownNat n1 $
+      withKnownProof (unsafeKnownProof @(na + ix - 1) (natVal (Proxy @na) + natVal (Proxy @ix) - 1)) $
         case ( unsafeAxiom @(na + ix - 1 - ix + 1) @na,
                unsafeLeqProof @(na + ix - 1 + 1) @xn,
                unsafeLeqProof @ix @(na + ix - 1)
              ) of
           (Refl, LeqProof, LeqProof) ->
             lowerUnaryTerm config t bv (SBV.bvExtract (Proxy @(na + ix - 1)) (Proxy @ix)) m
-      where
-        n1 :: NatRepr (na + ix - 1)
-        n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)
     (SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy xn)) ->
-      withKnownNat n1 $
+      withKnownProof (unsafeKnownProof @(na + ix - 1) (natVal (Proxy @na) + natVal (Proxy @ix) - 1)) $
         case ( unsafeAxiom @(na + ix - 1 - ix + 1) @na,
                unsafeLeqProof @(na + ix - 1 + 1) @xn,
                unsafeLeqProof @ix @(na + ix - 1)
              ) of
           (Refl, LeqProof, LeqProof) ->
             lowerUnaryTerm config t bv (SBV.bvExtract (Proxy @(na + ix - 1)) (Proxy @ix)) m
-      where
-        n1 :: NatRepr (na + ix - 1)
-        n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)
     _ -> translateTernaryError "bvselect" ix w (R.typeRep @x) (R.typeRep @a)
 lowerSinglePrimImpl config t@(BVExtendTerm _ signed (n :: R.TypeRep n) (bv :: Term x)) m =
   case (R.typeRep @a, R.typeRep @x) of
     (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->
-      withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - nx)) $
+      withKnownProof (unsafeKnownProof @(na - nx) (natVal (Proxy @na) - natVal (Proxy @nx))) $
         case (unsafeLeqProof @(nx + 1) @na, unsafeLeqProof @1 @(na - nx)) of
           (LeqProof, LeqProof) ->
             bvIsNonZeroFromGEq1 @(na - nx) $
               lowerUnaryTerm config t bv (if signed then SBV.signExtend else SBV.zeroExtend) m
     (SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->
-      withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - nx)) $
+      withKnownProof (unsafeKnownProof @(na - nx) (natVal (Proxy @na) - natVal (Proxy @nx))) $
         case (unsafeLeqProof @(nx + 1) @na, unsafeLeqProof @1 @(na - nx)) of
           (LeqProof, LeqProof) ->
             bvIsNonZeroFromGEq1 @(na - nx) $
@@ -742,18 +709,6 @@ lowerSinglePrimImpl config t@(ModIntegerTerm _ arg1 arg2) m =
     _ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
 lowerSinglePrimImpl _ _ _ = error "Should never happen"
 
-unsafeMkNatRepr :: Int -> NatRepr w
-unsafeMkNatRepr x = NatRepr (fromInteger $ toInteger x)
-
-unsafeWithNonZeroKnownNat :: forall w r. Int -> ((KnownNat w, 1 <= w) => r) -> r
-unsafeWithNonZeroKnownNat i r
-  | i <= 0 = error "Not an nonzero natural number"
-  | otherwise = withKnownNat @w (unsafeMkNatRepr i) $ unsafeBVIsNonZero r
-  where
-    unsafeBVIsNonZero :: ((1 <= w) => r) -> r
-    unsafeBVIsNonZero r1 = case unsafeAxiom :: w :~: 1 of
-      Refl -> r1
-
 bvIsNonZeroFromGEq1 :: forall w r. (1 <= w) => ((SBV.BVIsNonZero w) => r) -> r
 bvIsNonZeroFromGEq1 r1 = case unsafeAxiom :: w :~: 1 of
   Refl -> r1
@@ -782,12 +737,13 @@ parseModel _ (SBVI.SMTModel _ _ assoc uifuncs) mp = foldr gouifuncs (foldr goass
           R.App a (n :: R.TypeRep w) ->
             case R.eqTypeRep (R.typeRepKind n) (R.typeRep @Nat) of
               Just R.HRefl ->
-                unsafeWithNonZeroKnownNat @w bitWidth $
-                  case (R.eqTypeRep a (R.typeRep @IntN), R.eqTypeRep a (R.typeRep @WordN)) of
-                    (Just R.HRefl, _) ->
-                      fromInteger i
-                    (_, Just R.HRefl) -> fromInteger i
-                    _ -> error "Bad type"
+                case (unsafeKnownProof @w (fromIntegral bitWidth), unsafeLeqProof @1 @w) of
+                  (KnownProof, LeqProof) ->
+                    case (R.eqTypeRep a (R.typeRep @IntN), R.eqTypeRep a (R.typeRep @WordN)) of
+                      (Just R.HRefl, _) ->
+                        fromInteger i
+                      (_, Just R.HRefl) -> fromInteger i
+                      _ -> error "Bad type"
               _ -> error "Bad type"
           _ -> error "Bad type"
     resolveSingle _ _ = error "Unknown cv"
@@ -826,35 +782,35 @@ parseModel _ (SBVI.SMTModel _ _ assoc uifuncs) mp = foldr gouifuncs (foldr goass
     gougfuncResolve idx ta1 ta2 (l, s) =
       case ta2 of
         GFunType (ta2' :: R.TypeRep a2) (tr2' :: R.TypeRep r2) ->
-          let sym = WithInfo (IndexedSymbol "arg" idx) FunArg
+          let sym = IndexedSymbol "arg" idx
               funs = second (\r -> gougfuncResolve (idx + 1) ta2' tr2' (r, s)) <$> partition ta1 l
               def = gougfuncResolve (idx + 1) ta2' tr2' ([], s)
               body =
                 foldl'
                   ( \acc (v, f) ->
                       pevalITETerm
-                        (pevalEqvTerm (iinfosymTerm "arg" idx FunArg) (conTerm v))
+                        (pevalEqvTerm (symTerm sym) (conTerm v))
                         (conTerm f)
                         acc
                   )
                   (conTerm def)
                   funs
-           in GeneralFun sym body
+           in buildGeneralFun sym body
         _ ->
-          let sym = WithInfo (IndexedSymbol "arg" idx) FunArg
+          let sym = IndexedSymbol "arg" idx
               vs = bimap (resolveSingle ta1 . head) (resolveSingle ta2) <$> l
               def = resolveSingle ta2 s
               body =
                 foldl'
                   ( \acc (v, a) ->
                       pevalITETerm
-                        (pevalEqvTerm (iinfosymTerm "arg" idx FunArg) (conTerm v))
+                        (pevalEqvTerm (symTerm sym) (conTerm v))
                         (conTerm a)
                         acc
                   )
                   (conTerm def)
                   vs
-           in GeneralFun sym body
+           in buildGeneralFun sym body
     partition :: R.TypeRep a -> [([SBVI.CV], SBVI.CV)] -> [(a, [([SBVI.CV], SBVI.CV)])]
     partition t = case (R.eqTypeRep t (R.typeRep @Bool), R.eqTypeRep t (R.typeRep @Integer)) of
       (Just R.HRefl, _) -> partitionWithOrd . resolveFirst t

src/Grisette/Backend/SBV/Data/SMT/Solving.hs

@@ -170,8 +170,8 @@ solveTermWith config term = SBV.runSMTWith (sbvConfig config) $ do
       _ -> return (m, Left r)
 
 instance Solver (GrisetteSMTConfig n) SBVC.CheckSatResult where
-  solve config (Sym t) = snd <$> solveTermWith config t
-  solveMulti config n s@(Sym t)
+  solve config (SymBool t) = snd <$> solveTermWith config t
+  solveMulti config n s@(SymBool t)
     | n > 0 = SBV.runSMTWith (sbvConfig config) $ do
         (newm, a) <- lowerSinglePrim config t
         SBVC.query $ do
@@ -258,7 +258,7 @@ instance CEGISSolver (GrisetteSMTConfig n) SBVC.CheckSatResult where
         IO (Either SBVC.CheckSatResult ([inputs], PM.Model))
       go cexFormula inputs allInputs pre post =
         SBV.runSMTWith (sbvConfig config) $ do
-          let Sym t = phi &&~ cexFormula
+          let SymBool t = phi &&~ cexFormula
           (newm, a) <- lowerSinglePrim config t
           SBVC.query $
             snd <$> do
@@ -285,7 +285,7 @@ instance CEGISSolver (GrisetteSMTConfig n) SBVC.CheckSatResult where
               return (evaluateSym False newm inputs, newm)
           guess :: Model -> SymBiMap -> Query (SymBiMap, Either SBVC.CheckSatResult PM.Model)
           guess candidate origm = do
-            let Sym evaluated = evaluateSym False candidate phi
+            let SymBool evaluated = evaluateSym False candidate phi
             let (lowered, newm) = lowerSinglePrim' config evaluated origm
             SBV.constrain lowered
             r <- SBVC.checkSat

src/Grisette/Core.hs

@@ -74,7 +74,8 @@ module Grisette.Core
     -- The values of unsolvable types are __/partially/__ merged in a symbolic
     -- union, which is essentially an if-then-else tree.
     --
-    -- For example, assume that the lists have the type @[SymBool]@.
+    -- For example, assume that the lists have the type
+    -- @['Grisette.IR.SymPrim.SymBool']@.
     -- In the following example, the result shows that @[b]@ and @[c]@ can be
     -- merged together in the same symbolic union because they have the same
     -- length:
@@ -125,10 +126,14 @@ module Grisette.Core
     -- Grisette
     -- currently provides an implementation for the following solvable types:
     --
-    -- * @SymBool@ or @Sym Bool@ (symbolic Booleans)
-    -- * @SymInteger@ or @Sym Integer@ (symbolic unbounded integers)
-    -- * @SymIntN n@ or @Sym (IntN n)@ (symbolic signed bit vectors of length @n@)
-    -- * @SymWordN n@ or @Sym (WordN n)@ (symbolic unsigned bit vectors of length @n@)
+    -- * 'Grisette.IR.SymPrim.SymBool' (symbolic Booleans)
+    -- * 'Grisette.IR.SymPrim.SymInteger' (symbolic unbounded integers)
+    -- * @'Grisette.IR.SymPrim.SymIntN' n@ (symbolic signed bit vectors of length @n@)
+    -- * @'Grisette.IR.SymPrim.SymWordN' n@ (symbolic unsigned bit vectors of length @n@)
+    --
+    -- The two bit vector types has their lengths checked at compile time.
+    -- Grisette also provides runtime-checked versions of these types:
+    -- 'Grisette.IR.SymPrim.SomeSymIntN' and 'Grisette.IR.SymPrim.SomeSymWordN'.
     --
     -- Values of a solvable type can consist of concrete values, symbolic
     -- constants (placeholders for concrete values that can be assigned by a
@@ -176,10 +181,15 @@ module Grisette.Core
     SEq (..),
     SymBoolOp,
     SOrd (..),
-    BVConcat (..),
-    BVExtend (..),
-    BVSelect (..),
-    bvextract,
+    SomeBV (..),
+    someBVZext',
+    someBVSext',
+    someBVExt',
+    someBVSelect',
+    someBVExtract,
+    someBVExtract',
+    SizedBV (..),
+    sizedBVExtract,
     SignedDivMod (..),
     UnsignedDivMod (..),
     SignedQuotRem (..),

src/Grisette/Core/Control/Monad/Union.hs

@@ -25,5 +25,5 @@ import Grisette.Core.Data.Class.SimpleMergeable
 -- >>> import Grisette.Core
 -- >>> import Grisette.IR.SymPrim
 
--- | Class for monads that support union-like operations and 'Mergeable' knowledge propagation.
+-- | Class for monads that support union-like operations and 'Grisette.Core.Data.Class.Mergeable' knowledge propagation.
 type MonadUnion u = (UnionLike u, Monad u)

src/Grisette/Core/Control/Monad/UnionM.hs

@@ -387,6 +387,7 @@ instance (Mergeable a, EvaluateSym a) => EvaluateSym (UnionM a) where
           (go t)
           (go f)
 
+{-
 instance (Mergeable a, SubstituteSym a) => SubstituteSym (UnionM a) where
   substituteSym sym val x = go $ underlyingUnion x
     where
@@ -397,6 +398,7 @@ instance (Mergeable a, SubstituteSym a) => SubstituteSym (UnionM a) where
           (substituteSym sym val cond)
           (go t)
           (go f)
+          -}
 
 instance
   (ExtractSymbolics a) =>