diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,14 +1,33 @@ * Hackage: * GitHub: +### Version 14.4, 2026-07-03 + + * Add `curry` and `uncurry` (for symbolic 2-tuples) and `curry3` and `uncurry3` (for + symbolic 3-tuples) to `Data.SBV.Tuple`, mirroring `Prelude.curry`/`Prelude.uncurry`. + + * New example `Documentation.SBV.Examples.BitPrecise.Adders`, building ripple-carry and + carry-lookahead adders out of logic gates and proving them correct (equal to bit-vector + addition, equal to each other, and the carry-out equal to the overflow flag) fully + automatically by bit-blasting. + + * New example `Documentation.SBV.Examples.TP.Adder`, the inductive companion to the above: + it models the operands as arbitrary-length symbolic bit lists and proves, for all widths + at once, that a ripple-carry adder computes the integer value of the bits, and that a + parallel-prefix (carry-lookahead) tree computes the same carry as the ripple---resting on + the associativity of the generate/propagate carry operator. + + * Use str.to_re (instead of str.to.re) in regular-expression construction, which is the standard + naming in SMTLib2. Thanks to May Torrence for reporting the discrepancy. + ### Version 14.3, 2026-06-19 * Improve fpRoundToIntegralH to remove redundant internal check. Thanks to Ryan Scott for the report. * Add support for arctan/arcsin/arccos in CVC5. Thanks to Ryan Scott for pointing out support for it. - * Improved backed-solver communication so that if a solver returns an error message SBV now makes - sure it gets captured and displayed properly before the solver-process itselfs terminates. + * Improved backend-solver communication so that if a solver returns an error message SBV now makes + sure it gets captured and displayed properly before the solver-process itself terminates. * Drop support for pi as an SReal: The whole premise of SReal is it represents algebraic-reals (i.e., those that are roots of polynomials) exactly. But pi is not representable as such, since @@ -308,7 +327,7 @@ * Replace internal SMT-lib program representation from plain String to Text. This should improve performance and memory behavior in certain cases. Since solver time - dominates for most cases, this is not going to be noticable by end-users, except + dominates for most cases, this is not going to be noticeable by end-users, except for very large programs. In any case, it should at least improve memory usage. NB. Historical note: Most of these transformations were done by Claude code; the era of AI coding had its first contributions to SBV. I' duly impressed by Claude's @@ -393,7 +412,7 @@ * Added Documentation.SBV.Examples.TP.Peano, modeling peano numbers using an ADT and demonstrating many proofs. * Added Documentation.SBV.Examples.TP.VM demonstrating the correctness of a simple interpreter over an expression - language with respect to a version that compiles the expression and runs the insturctions over a virtual machine. + language with respect to a version that compiles the expression and runs the instructions over a virtual machine. * [BACKWARDS COMPATIBILITY] The old functions 'mkSymbolicEnumeration' and 'mkUninterpretedSort' are now removed, since their functionality is subsumed by 'mkSymbolic'. @@ -474,7 +493,7 @@ - Documentation.SBV.Examples.TP.Majority: Proof of Boyer-Moore's majority selection algorithm correct. - Documentation.SBV.Examples.TP.McCarthy91: Proof of correctness for McCarthy's 91 function. - Documentation.SBV.Examples.TP.PowerMod: Proving arithmetic properties relating power operation and modular arithmetic. - - Documentation.SBV.Examples.TP.ReverseAcc: Proving the accummulating reverse definition is correct. + - Documentation.SBV.Examples.TP.ReverseAcc: Proving the accumulating reverse definition is correct. - Documentation.SBV.Examples.TP.Reverse: Proving a definition of reverse that uses no auxiliary definitions is correct. - Documentation.SBV.Examples.TP.SumReverse: Proving summing a list and its reverse are equivalent. @@ -535,7 +554,7 @@ ### Version 11.4, 2025-03-12 - * Generalize the strong-induction principle to use lexicographic order for simultanous + * Generalize the strong-induction principle to use lexicographic order for simultaneous induction over two lists. * Added a proof of correctness for the merge-sort algorithm using KnuckleDragger @@ -569,11 +588,11 @@ the SMT solver to find tricky proofs. See Documentation/SBV/Examples/KnuckleDragger directory for many examples demonstrating the new features. - * Generalize support for polyorphic and higher-order functions. These are still experimental, as SMTLib's + * Generalize support for polymorphic and higher-order functions. These are still experimental, as SMTLib's higher-order function support is nascent. (Version 3 of SMTLib will have proper support for such functions, which is not released yet.) Currently, SBV can handle polymorphic and higher-order usage of: 'reverse', 'any', 'all', 'filter', 'map', 'foldl', 'foldr', 'zip', and 'zipWith'; all exported from the 'Data.SBV.List' module. - These functions are supported polymporphically, and (except reverse and zip) all take a function as + These functions are supported polymorphically, and (except reverse and zip) all take a function as an argument. SBV firstifies these functions, and the resulting code is compatible with Z3 and CVC5. (Firstification might change in the future, as SMTLib gains support for more higher-order features itself.) Proof-support in backend solvers for higher-order functions is still quite weak, @@ -657,14 +676,14 @@ * Fix a few custom-floating-point format conversion bugs. Thanks to Sirui Lu for the patch. - * Add a few OVERLAPPABLE pragms to generic Queriable instances to make them easily overridable by + * Add a few OVERLAPPABLE pragmas to generic Queriable instances to make them easily overridable by user programs. Thanks to Marco Zocca for reporting. * Add signedMulOverflow, which checks whether multiplication of two signed-bitvectors can overflow. SBV already had a method (bvMulO) that served this purpose, translating to the corresponding predicate in SMTLib. Unfortunately not all solvers support this predicate efficiently. In particular, as of Aug 2024, bitwuzla has a performant checker for this overflow, but z3 does not. In case you cannot use bitwuzla for - some reason, you might want to use the new signedMulOverflow funtion for better performance. + some reason, you might want to use the new signedMulOverflow function for better performance. ### Version 10.11, 2024-07-26 @@ -819,7 +838,7 @@ ForallN and ExistsN for creating multiple variables at the same time. The new function skolemize can be used to skolemize quantified formulas: The skolemized version of a - formula has no existential (replaced by uninterpeted functions), and is equisatisfiable to the original. + formula has no existential (replaced by uninterpreted functions), and is equisatisfiable to the original. See the following files demonstrating reasoning with quantifiers: @@ -840,7 +859,7 @@ * Added new SList functions: map, mapi, foldl, foldr, foldli, foldri, zip, zipWith, filter, all, any. Note that these work on arbitrary--but finite--length lists, with all terminating elements, per usual SBV interpretation. These functions map to the underlying solver's fold and map functions, - via lambda-abtractions. Note that the SMT engines remain incomplete with respect to sequence + via lambda-abstractions. Note that the SMT engines remain incomplete with respect to sequence theories. (That is, any property that requires induction for its proof will cause unknown answers, or will not terminate.) However, basic properties, especially when the solver can determine the shape of the sequence arguments (i.e., number of elements), should go through. @@ -1022,7 +1041,7 @@ significand. This format is affectionately called "brain-float" because it's often used in modeling neural networks machine-learning applications, offering a wider-range than IEEE's half-float, at the - exponse of reduced precision. It has 8-exponent bits and 8-significand + expense of reduced precision. It has 8-exponent bits and 8-significand bits, including the hidden bit. * Add support for SRational type, rational values built out of the ratio @@ -1036,7 +1055,7 @@ use cases. (Essentially, when there are no uninterpreted values or sorts present.) The new algorithm has been measured to be at least an order of magnitude faster or more in common cases as it splits the search space into disjoint - models, reducing the burden of accummulated lemmas over multiple calls. (See + models, reducing the burden of accumulated lemmas over multiple calls. (See http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations for details.) @@ -1099,7 +1118,7 @@ * Use SMTLib's int2bv if supported by the backend solver. If not, we still do a manual translation. (CVC4 and z3 support it natively, Yices and MathSAT does not, for which we do the manual translation. ABC and dReal - doesn't support the coversion at all, since former doesn't support integers + doesn't support the conversion at all, since former doesn't support integers and the latter doesn't support bit-vectors.) Thanks to Martin Lundfall for the initial pull request. @@ -1904,7 +1923,7 @@ Note that currently only Z3 and CVC4 has support for this logic, and they do differ in some details. Various character/string operations are supported, including length, concatenation, - regular-expression matching, substrig operations, recognizers, etc. + regular-expression matching, substring operations, recognizers, etc. If you use this logic, you are likely to find bugs in solvers themselves as support is rather new: Please report. diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -690,7 +690,7 @@ Goals can be lexicographically (default), independently, or pareto-front optimized. The relevant functions are: * 'minimize': Minimize a given arithmetic goal - * 'maximize': Minimize a given arithmetic goal + * 'maximize': Maximize a given arithmetic goal Goals can be optimized at a regular or an extended value: An extended value is either positive or negative infinity (for unbounded integers and reals) or positive or negative epsilon differential from a real value (for reals). @@ -836,7 +836,7 @@ overflow/underflow as it is the case with the bounded types, such as 'SWord8', 'SInt16', etc. However, some bit-vector based operations are /not/ supported for the 'SInteger' type while in the verification mode. That is, you can use these operations on 'SInteger' values during normal programming/simulation. -but the SMT translation will not support these operations since there corresponding operations are not supported in SMT-Lib. +but the SMT translation will not support these operations since their corresponding operations are not supported in SMT-Lib. Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixed-size bit-vectors. The operations that are restricted to bounded word/int sizes are: @@ -893,10 +893,10 @@ -} {- $partitionIntro -The function 'allSatPartition' one to restrict the results returned by calls to 'Data.SBV.allSat'. +The function 'allSatPartition' allows one to restrict the results returned by calls to 'Data.SBV.allSat'. In certain cases, we might consider certain models to be "equivalent," i.e., we might want to create equivalence classes over the search space when it comes to what we consider all satisfying -solutions. In these cases, we can use 'allSatPartition' tell SBV what classes of solutions to consider +solutions. In these cases, we can use 'allSatPartition' to tell SBV what classes of solutions to consider as unique. Consider: >>> :{ @@ -929,8 +929,8 @@ Found 4 different solutions. Without the call to 'allSatPartition' the above example, 'allSat' would return all possible combinations of @x@ and @y@ subject to the constraints. (Since we have none here, -the call would try to enumerate the infinite set of all integer tuples!) But 'allSatPartition' us to restrict our attention to the examples that satisfy the partitioning -constraints. The first argument to 'allSatPartition' simply a name, for diagnostic purposes. Note that the conditions given by 'allSatPartition' /not/ imposed on the search +the call would try to enumerate the infinite set of all integer tuples!) But 'allSatPartition' allows us to restrict our attention to the examples that satisfy the partitioning +constraints. The first argument to 'allSatPartition' is simply a name, for diagnostic purposes. Note that the conditions given by 'allSatPartition' are /not/ imposed on the search space at all: They're only used when we construct the search space. In the above example, we pick one example from each quadrant. Furthermore, while it is typical to pass a boolean as a partitioning argument, it is not required: Any expression is OK, whose value creates the equivalence class: @@ -966,7 +966,7 @@ ... @ -The first constraint requires @x@ to be larger than @y@. The scond one says that +The first constraint requires @x@ to be larger than @y@. The second one says that sum of @x@ and @y@ must be at least @12@, and the final one says that @y@ to be at least @3@. Constraints provide an easy way to assert additional properties on the input domain, right at the point of the introduction of variables. @@ -1312,7 +1312,7 @@ Conversions to float: 'toSFloat' and 'toSDouble' simply return the nearest representable float from the given type based on the rounding mode provided. Similarly, 'toSFloatingPoint' converts to a generalized -floating-point number with specified exponent and significand bith widths. +floating-point number with specified exponent and significand bit widths. Conversions from float: 'fromSFloat', 'fromSDouble', 'fromSFloatingPoint' functions do the reverse conversion. However some care is needed when given values diff --git a/Data/SBV/Client.hs b/Data/SBV/Client.hs --- a/Data/SBV/Client.hs +++ b/Data/SBV/Client.hs @@ -39,6 +39,7 @@ import Data.Generics import Control.Monad (filterM, mapAndUnzipM, zipWithM) +import Data.Function (fix) import Test.QuickCheck (Arbitrary(..), elements) import qualified Control.Exception as C @@ -352,10 +353,17 @@ (TH.normalB (TH.caseE [| sequenceA $(TH.listE [ [| unlitCV $(TH.varE a) |] | a <- as ]) |] [ TH.match [p|Just $(TH.varP c)|] - (TH.normalB [| let k = kindOf (undefined `asTypeOf` res) - res = SBV $ SVal k (Left (CV k (CADT (bnm, $(TH.varE c))))) - in res - |]) + -- We need the kind of the result type to build the value, but the + -- result type can only be recovered from the (signature-pinned) result + -- itself: a parametric type may carry the parameter in a phantom + -- position (e.g. the @a@ in @Right :: b -> Either a b@) that no argument + -- mentions. We tie the kind to the result via 'fix'. Crucially, 'fix' + -- binds @res@ as a /lambda-bound/ variable, which is always monomorphic; + -- a plain @let@ group would be generalized when the monomorphism + -- restriction is off (as it is at the GHCi prompt), yielding a spurious + -- ambiguous @HasKind@. ('kindOf' ignores its argument, so 'fix' is safe.) + (TH.normalB [| fix (\res -> let k = kindOf res + in SBV $ SVal k (Left (CV k (CADT (bnm, $(TH.varE c)))))) |]) [] , TH.match [p|Nothing|] (TH.normalB (foldl (\a b -> [| $a $b |]) [| mkADTConstructor bnm |] (map TH.varE as))) diff --git a/Data/SBV/Control/BaseIO.hs b/Data/SBV/Control/BaseIO.hs --- a/Data/SBV/Control/BaseIO.hs +++ b/Data/SBV/Control/BaseIO.hs @@ -240,7 +240,7 @@ -- for this call to not error out! -- -- To get an interpolant for a pair of formulas @A@ and @B@, use a 'Data.SBV.constrainWithAttribute' call to attach --- interplation groups to @A@ and @B@. Then call 'getInterpolantMathSAT' @[\"A\"]@, assuming those are the names +-- interpolation groups to @A@ and @B@. Then call 'getInterpolantMathSAT' @[\"A\"]@, assuming those are the names -- you gave to the formulas in the @A@ group. -- -- An interpolant for @A@ and @B@ is a formula @I@ such that: diff --git a/Data/SBV/Control/Types.hs b/Data/SBV/Control/Types.hs --- a/Data/SBV/Control/Types.hs +++ b/Data/SBV/Control/Types.hs @@ -164,7 +164,7 @@ -- logics that might be supported on new solvers. See for the official list. data Logic = AUFLIA -- ^ Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values. - | AUFLIRA -- ^ Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value. + | AUFLIRA -- ^ Linear formulas with free sort and function symbols over one- and two-dimensional arrays of integer index and real value. | AUFNIRA -- ^ Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value. | LRA -- ^ Linear formulas in linear real arithmetic. | QF_ABV -- ^ Quantifier-free formulas over the theory of bit-vectors and bit-vector arrays. diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -404,7 +404,7 @@ nm <- findName st uiMap -- Read the uiMap again here. Why? Because the act of finding the name might've - -- introduced it as an uninterperted name! + -- introduced it as an uninterpreted name! newUIMap <- liftIO $ readIORef rUIMap case nm `Map.lookup` newUIMap of Nothing -> cantFind newUIMap @@ -1193,7 +1193,7 @@ getUICVal :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, (Bool, Maybe [String], SBVType)) -> m CV getUICVal mbi (nm, (_, _, t)) = case t of SBVType [k] -> extractValue mbi nm k - _ -> error $ "SBV.getUICVal: Expected to be called on an uninterpeted value of a base type, received something else: " ++ show (nm, t) + _ -> error $ "SBV.getUICVal: Expected to be called on an uninterpreted value of a base type, received something else: " ++ show (nm, t) -- | Generalization of 'Data.SBV.Control.getUIFunCVAssoc' getUIFunCVAssoc :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, (Bool, Maybe [String], SBVType)) -> m (Either String ([([CV], CV)], CV)) @@ -1929,7 +1929,7 @@ Nothing -> pure () Just QueryState{queryTerminate} -> queryTerminate maybeForwardedException - -- If this is an extrnal query and there are objectives, let's add those to the list before we run + -- If this is an external query and there are objectives, let's add those to the list before we run -- Here we only allow Lexicographic; we might want to make that configurable later. let userQuery = case queryContext of QueryInternal -> originalQuery diff --git a/Data/SBV/Core/AlgReals.hs b/Data/SBV/Core/AlgReals.hs --- a/Data/SBV/Core/AlgReals.hs +++ b/Data/SBV/Core/AlgReals.hs @@ -130,8 +130,8 @@ instance Show AlgReal where show (AlgRational exact a) = showRat exact a show (AlgPolyRoot (i, p) mbApprox) = "root(" ++ show i ++ ", " ++ show p ++ ")" ++ maybe "" app mbApprox - where app v | last v == '?' = " = " ++ init v ++ "..." - | True = " = " ++ v + where app v | not (null v) && last v == '?' = " = " ++ init v ++ "..." + | True = " = " ++ v show (AlgInterval a b) = case (a, b) of (OpenPoint l, OpenPoint h) -> "(" ++ show l ++ ", " ++ show h ++ ")" (OpenPoint l, ClosedPoint h) -> "(" ++ show l ++ ", " ++ show h ++ "]" @@ -197,7 +197,7 @@ toRational (AlgRational True v) = v toRational x = error $ "AlgReal.toRational: Argument cannot be represented as a rational value: " ++ algRealToHaskell x --- | Random instance for rational needs to be careful to split the generator twice for numerator and denumerator +-- | Random instance for rational needs to be careful to split the generator twice for numerator and denominator instance Random Rational where random g = (a % b', g'') where (a, g') = random g diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -1791,7 +1791,7 @@ consumers :: Map.Map SV [(SV, Op)] consumers = foldl' addConsumers Map.empty dagList where addConsumers m (sv, SBVApp op args) = - foldl' (\m' a -> Map.insertWith (++) a [(sv, op)] m') m args + foldl' (\m' a -> Map.insertWith (\_ old -> (sv, op) : old) a [(sv, op)] m') m args -- A recursive call is guarded if at least one of its consumers is a constructor isGuarded sv = case Map.lookup sv consumers of @@ -3889,7 +3889,7 @@ resKind (KArray _ k) = resKind k resKind k = k --- | SMT definable constants and functions, which can also be uninterpeted. +-- | SMT definable constants and functions, which can also be uninterpreted. -- This class captures functions that we can generate standalone-code for -- in the SMT solver. Note that we also allow uninterpreted constants and -- functions too. An uninterpreted constant is a value that is indexed by its name. The only @@ -4004,10 +4004,10 @@ symWithKind :: String -> a symWithKind = sym - -- | Render an uninterpeted value as an SMTLib definition + -- | Render an uninterpreted value as an SMTLib definition sbv2smt :: ExtractIO m => a -> m String - -- | Render an uninterpeted value function as an SMTLib definition + -- | Render an uninterpreted value function as an SMTLib definition sbvFun2smt :: (SymVals as, ExtractIO m) => (SBVs as -> a) -> m String -- | Make this name a constructor, coming from an ADT. Only used internally @@ -4577,7 +4577,7 @@ res = f xsbv sbvToSV st res --- | Class of things that we can logically reduce to a boolean, by saturating and then asserting equivalance to itself +-- | Class of things that we can logically reduce to a boolean, by saturating and then asserting equivalence to itself class QSaturate m a where qSaturate :: a -> m () diff --git a/Data/SBV/Core/Operations.hs b/Data/SBV/Core/Operations.hs --- a/Data/SBV/Core/Operations.hs +++ b/Data/SBV/Core/Operations.hs @@ -593,7 +593,7 @@ -> error $ "cCompare: Mismatching ADT field kinds in comparison: " ++ show (op, k, map fst fks, map fst fks') | True -> let fmatch = zipWith (\(fk, v1) (_, v2) -> cCompare fk op v1 v2) fks fks' - undecided = any isNothing fmatch -- Field comparison undecive + undecided = any isNothing fmatch -- Field comparison undecided allEq = all (== Just EQ) fmatch -- All fields Equal in if undecided then Nothing @@ -648,7 +648,7 @@ defsMatch = def1 == def2 -- Check if keys cover everything. Clearly, we can't do this for all kinds; but only finite ones - -- For the time being, we're retricting ourselves to bool only. Might want to extend this later. + -- For the time being, we're restricting ourselves to bool only. Might want to extend this later. complete = case k1 of KBool -> let bools = map cvVal [falseCV, trueCV] covered asc = all (`elem` map fst asc) bools @@ -1075,8 +1075,8 @@ signedInfinity :: forall a. Floating a => a signedInfinity = if neg then -infinity else infinity --- | Create a NaN infinity value of the given kind. If the 'Bool' argument is --- 'True', then use negative infinity; otherwise, use positive infinity. +-- | Create a signed zero value of the given kind. If the 'Bool' argument is +-- 'True', then use negative zero; otherwise, use positive zero. svFPZero :: Kind -> Bool -> SVal svFPZero k neg = SVal k $ Left $ fpConstCV k signedZero signedZero (fpZero neg) where @@ -1161,7 +1161,7 @@ svFPMax :: SVal -> SVal -> SVal svFPMax = liftFPSym2 "max" (mkSymOp (IEEEFP FP_Max)) fpMaxH fpMaxH fpMax --- | Floating-point fused-multipy-add (FMA). +-- | Floating-point fused-multiply-add (FMA). -- Note that this operation is defined somewhat unusually because Haskell lacks -- a native FMA operation to use for concrete evaluation of 'Float's and @@ -1856,7 +1856,7 @@ _ -> True where rmIsRne | RoundNearestTiesToEven <- rm = True - | otherwise = False + | True = False noInt :: String -> Integer -> Integer -> a noInt o a b = error $ "SBV.Integer." ++ o ++ ": Unexpected arguments: " ++ show (a, b) @@ -1940,7 +1940,7 @@ Left (CV _ (CInteger w')) -> SVal kindTo $ Left $ CV kindTo $ CFloat $ wordToFloat $ fromInteger w' _ -> SVal kindTo $ Right $ cache y - | otherwise + | True = error $ "svSWord32AsFloat: not a 32-bit word type: " ++ show kindFrom where kindTo = KFloat y st = do svw <- svToSV st w @@ -1957,7 +1957,7 @@ Left (CV _ (CInteger w')) -> SVal kindTo $ Left $ CV kindTo $ CDouble $ wordToDouble $ fromInteger w' _ -> SVal kindTo $ Right $ cache y - | otherwise + | True = error $ "svSWord64AsDouble: not a 64-bit word type: " ++ show kindFrom where kindTo = KDouble y st = do svw <- svToSV st w @@ -1976,7 +1976,7 @@ Left (CV _ (CInteger w')) -> SVal kindTo $ Left $ CV kindTo $ CFP $ fpFromBits eb sb $ fromInteger w' _ -> SVal kindTo $ Right $ cache y - | otherwise + | True = error $ "svSWordAsFloatingPoint: non-word type: " ++ show kindFrom where kindTo = KFP eb sb y st = do svw <- svToSV st w diff --git a/Data/SBV/Core/SizedFloats.hs b/Data/SBV/Core/SizedFloats.hs --- a/Data/SBV/Core/SizedFloats.hs +++ b/Data/SBV/Core/SizedFloats.hs @@ -109,7 +109,7 @@ -- | Abbreviation for IEEE double precision float, bit width 64 = 11 + 53. type FPDouble = FloatingPoint 11 53 --- | Abbreviation for IEEE quadruble precision float, bit width 128 = 15 + 113. +-- | Abbreviation for IEEE quadruple precision float, bit width 128 = 15 + 113. type FPQuad = FloatingPoint 15 113 -- | Show instance for Floats. By default we print in base 10, with standard scientific notation. @@ -142,7 +142,7 @@ -- Manually implemented instance as GHC generated a non-IEEE 754 compliant instance. -- Note that we cannot pack the values in a tuple and then compare them as that will --- also give non-IEEE 754 compilant results. +-- also give non-IEEE 754 compliant results. -- -- NB. Refrain from letting GHC derive @>@ and @>=@ and define -- it ourselves. Why? Because the default definition of @x > y@ diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -179,7 +179,7 @@ swNodeId (SV _ nid) = nid -- | Forcing an argument; this is a necessary evil to make sure all the arguments --- to an uninterpreted function are evaluated before called; the semantics of uinterpreted +-- to an uninterpreted function are evaluated before called; the semantics of uninterpreted -- functions is necessarily strict; deviating from Haskell's forceSVArg :: SV -> IO () forceSVArg (SV k n) = k `seq` n `seq` pure () @@ -237,7 +237,7 @@ | SetOp SetOp -- Set operations, categorized separately | TupleConstructor Int -- Construct an n-tuple | TupleAccess Int Int -- Access element i of an n-tuple; second argument is n - | RationalConstructor -- Construct a rational. Note that there's no access to numerator or denumerator, since we cannot store rationals in canonical form + | RationalConstructor -- Construct a rational. Note that there's no access to numerator or denominator, since we cannot store rationals in canonical form | ADTOp ADTOp -- ADT access/construction/testing -- Arrays @@ -466,7 +466,7 @@ -- | Convert a RegExp to text, parameterized by how strings are converted regExpToText :: (String -> Text) -> RegExp -> Text -regExpToText fs (Literal s) = "(str.to.re " <> fs s <> ")" +regExpToText fs (Literal s) = "(str.to_re " <> fs s <> ")" regExpToText _ All = "re.all" regExpToText _ AllChar = "re.allchar" regExpToText _ None = "re.nostr" @@ -840,7 +840,7 @@ , reskinds :: Set.Set Kind -- ^ kinds used in the program , resTraces :: [(String, CV)] -- ^ quick-check counter-example information (if any) , resObservables :: [(String, CV -> Bool, SV)] -- ^ observable expressions (part of the model) - , resUISegs :: [(String, [String])] -- ^ uninterpeted code segments + , resUISegs :: [(String, [String])] -- ^ uninterpreted code segments , resParams :: ResultInp -- ^ top-inputs or lambda params , resConsts :: (CnstMap, [(SV, CV)]) -- ^ constants , resTables :: [((Int, Kind, Kind), [SV])] -- ^ tables (automatically constructed) (tableno, index-type, result-type) elts @@ -2101,7 +2101,7 @@ case (h `IMap.lookup` stored) >>= (sn `lookup`) of Just r -> pure r Nothing -> do r <- f st - r `seq` R.modifyIORef' rCache (IMap.insertWith (++) h [(sn, r)]) + r `seq` R.modifyIORef' rCache (IMap.insertWith (\_ old -> (sn, r) : old) h [(sn, r)]) pure r -- | Representation of SMTLib Program versions. As of June 2015, we're dropping support diff --git a/Data/SBV/Either.hs b/Data/SBV/Either.hs --- a/Data/SBV/Either.hs +++ b/Data/SBV/Either.hs @@ -63,15 +63,15 @@ -- True mkSymbolic [''Either] --- | Declare a symbolic maybe. +-- | Declare a symbolic either. sEither :: (SymVal a, SymVal b) => String -> Symbolic (SEither a b) sEither = free --- | Declare a symbolic maybe, unnamed. +-- | Declare a symbolic either, unnamed. sEither_ :: (SymVal a, SymVal b) => Symbolic (SEither a b) sEither_ = free_ --- | Declare a list of symbolic maybes. +-- | Declare a list of symbolic eithers. sEithers :: (SymVal a, SymVal b) => [String] -> Symbolic [SEither a b] sEithers = symbolics diff --git a/Data/SBV/Lambda.hs b/Data/SBV/Lambda.hs --- a/Data/SBV/Lambda.hs +++ b/Data/SBV/Lambda.hs @@ -61,7 +61,7 @@ (Maybe [(Quantifier, T.Text)]) -- Param declaration groups, if any (Int -> T.Text) -- Body, given the tab amount. --- | Maka a new substate from the incoming state, sharing parts as necessary +-- | Make a new substate from the incoming state, sharing parts as necessary inSubState :: MonadIO m => LambdaScope -> State -> (State -> m b) -> m b inSubState scope inState comp = do @@ -152,7 +152,7 @@ ] --- | Generic creator for anonymous lamdas. +-- | Generic creator for anonymous lambdas. lambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => LambdaScope -> (Defn -> b) -> State -> Kind -> a -> m b lambdaGen scope trans inState fk f = inSubState scope inState $ \st -> handle <$> convert st fk (mkLambda st f) where handle d@(Defn _ frees _ _) @@ -312,7 +312,7 @@ tbls -- Tables - _uis -- Uninterpeted constants: nothing to do with them + _uis -- Uninterpreted constants: nothing to do with them _axs -- Axioms definitions : nothing to do with them pgm -- Assignments diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -92,7 +92,7 @@ import Prelude hiding (head, tail, init, last, length, take, drop, splitAt, concat, null, elem, notElem, reverse, (++), (!!), map, concatMap, foldl, foldr, zip, zipWith, filter, all, any, and, or, replicate, fst, snd, sum, product, Enum(..), lookup, - takeWhile, dropWhile, minimum, maximum) + takeWhile, dropWhile, minimum, maximum, uncurry) import qualified Prelude as P import Data.SBV.Core.Kind @@ -476,7 +476,7 @@ | True -- either symbolic, or something is out-of-bounds = lift3 False (SeqSubseq (kindOf (Proxy @a))) Nothing l offset len --- | @`replace` l src dst@. Replace the first occurrence of @src@ by @dst@ in @s@ +-- | @`replace` l src dst@. Replace the first occurrence of @src@ by @dst@ in @l@ -- -- >>> prove $ \l -> replace [sEnum|1..5|] l [sEnum|6..10|] .== [sEnum|6..10|] .=> l .== [sEnum|1..5::SWord8|] -- Q.E.D. @@ -677,7 +677,7 @@ = literal concResult | True = sbvFoldl $ tuple (base, l) - where sbvFoldl = smtHOFunction "sbv.foldl" (uncurry f . untuple) + where sbvFoldl = smtHOFunction "sbv.foldl" (uncurry f) $ \exs -> [sCase| exs of (e, []) -> e (e, h : t) -> sbvFoldl (tuple (e `f` h, t)) @@ -709,7 +709,7 @@ -- [5,4,3,2,1] :: [SInteger] foldr :: func -> SBV b -> SList a -> SBV b - -- | Handle the concrete case for folding left. Used internally only. + -- | Handle the concrete case for folding right. Used internally only. concreteFoldr :: func -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> Maybe b concreteFoldr _ f sb sas | Just b <- unliteral sb, Just as <- unliteral sas @@ -729,7 +729,7 @@ = literal concResult | True = sbvFoldr $ tuple (base, l) - where sbvFoldr = smtHOFunction "sbv.foldr" (uncurry f . untuple) + where sbvFoldr = smtHOFunction "sbv.foldr" (uncurry f) $ \exs -> [sCase| exs of (e, []) -> e (e, h : t) -> h `f` sbvFoldr (tuple (e, t)) @@ -749,7 +749,7 @@ |] -- | @`zip` xs ys@ zips the lists to give a list of pairs. The length of the final list is --- the minumum of the lengths of the given lists. +-- the minimum of the lengths of the given lists. -- -- >>> zip [sEnum|1..10 :: SInteger|] [sEnum|11..20 :: SInteger|] -- [(1,11),(2,12),(3,13),(4,14),(5,15),(6,16),(7,17),(8,18),(9,19),(10,20)] :: [(SInteger, SInteger)] @@ -773,7 +773,7 @@ -- functions, and we instantiate this class appropriately so it can handle both cases. class (SymVal a, SymVal b, SymVal c) => SZipWith func a b c | func -> a b c where -- | @`zipWith` f xs ys@ zips the lists to give a list of pairs, applying the function to each pair of elements. - -- The length of the final list is the minumum of the lengths of the given lists. + -- The length of the final list is the minimum of the lengths of the given lists. -- -- >>> zipWith ((+) @SInteger) ([sEnum|1..10::SInteger|]) ([sEnum|11..20::SInteger|]) -- [12,14,16,18,20,22,24,26,28,30] :: [SInteger] @@ -800,7 +800,7 @@ = literal concResult | True = sbvZipWith $ tuple (xs, ys) - where sbvZipWith = smtHOFunction "sbv.zipWith" (uncurry f . untuple) + where sbvZipWith = smtHOFunction "sbv.zipWith" (uncurry f) $ \asbs -> [sCase| asbs of ([], _ ) -> [] (_, [] ) -> [] @@ -1033,7 +1033,7 @@ -- [2,3,4,5,6,7,8,9,10] :: [SInteger] dropWhile :: func -> SList a -> SList a - -- | Handle the concrete case of take-while. Used internally only. + -- | Handle the concrete case of drop-while. Used internally only. concreteDropWhile :: func -> (SBV a -> SBool) -> SList a -> Maybe [a] concreteDropWhile _ f sas | Just as <- unliteral sas diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -633,7 +633,7 @@ -- The following is a possible definition, but it lets us write properties that -- are not useful.. Such as: prove $ \x y -> (x::SInt8) == y -- Running that will throw an exception since Haskell's equality is not be supported by symbolic things. (Needs .==). --- So, we avoid these insteances. +-- So, we avoid these instances. instance ExtractIO m => ProvableM m Bool where proofArgReduce x = proofArgReduce (if x then sTrue else sFalse :: SBool) diff --git a/Data/SBV/RegExp.hs b/Data/SBV/RegExp.hs --- a/Data/SBV/RegExp.hs +++ b/Data/SBV/RegExp.hs @@ -88,7 +88,7 @@ -- >>> let phone = pre * "-" * post -- >>> sat $ \(s :: SString) -> s `match` phone -- Satisfiable. Model: --- s0 = "400-8000" :: String +-- s0 = "422-2222" :: String class RegExpMatchable a where -- | @`match` s r@ checks whether @s@ is in the language generated by @r@. match :: a -> RegExp -> SBool @@ -166,7 +166,7 @@ -- | Recognize a newline. Also includes carriage-return and form-feed. -- -- >>> newline --- (re.union (str.to.re "\n") (str.to.re "\r") (str.to.re "\f")) +-- (re.union (str.to_re "\n") (str.to_re "\r") (str.to_re "\f")) -- >>> prove $ \c -> c `match` newline .=> isSpaceL1 c -- Q.E.D. newline :: RegExp @@ -175,7 +175,7 @@ -- | Recognize a tab. -- -- >>> tab --- (str.to.re "\t") +-- (str.to_re "\t") -- >>> prove $ \c -> c `match` tab .=> c .== literal '\t' -- Q.E.D. tab :: RegExp @@ -281,7 +281,7 @@ -- | Recognize an octal number. Must have a prefix of the form @0o@\/@0O@. -- -- >>> octal --- (re.++ (re.union (str.to.re "0o") (str.to.re "0O")) (re.+ (re.range "0" "7"))) +-- (re.++ (re.union (str.to_re "0o") (str.to_re "0O")) (re.+ (re.range "0" "7"))) -- >>> prove $ \(s :: SString) -> s `match` octal .=> sAny (.== take 2 s) ["0o", "0O"] -- Q.E.D. octal :: RegExp @@ -290,7 +290,7 @@ -- | Recognize a hexadecimal number. Must have a prefix of the form @0x@\/@0X@. -- -- >>> hexadecimal --- (re.++ (re.union (str.to.re "0x") (str.to.re "0X")) (re.+ (re.union (re.range "0" "9") (re.range "a" "f") (re.range "A" "F")))) +-- (re.++ (re.union (str.to_re "0x") (str.to_re "0X")) (re.+ (re.union (re.range "0" "9") (re.range "a" "f") (re.range "A" "F")))) -- >>> prove $ \(s :: SString) -> s `match` hexadecimal .=> sAny (.== take 2 s) ["0x", "0X"] -- Q.E.D. hexadecimal :: RegExp diff --git a/Data/SBV/SEnum.hs b/Data/SBV/SEnum.hs --- a/Data/SBV/SEnum.hs +++ b/Data/SBV/SEnum.hs @@ -159,7 +159,7 @@ constStep :: Exp -> Exp -> Maybe Integer constStep from thn | bf == bt = Just (kt - kf) - | otherwise = Nothing + | True = Nothing where (bf, kf) = peel from (bt, kt) = peel thn diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -146,7 +146,7 @@ "Falsifiable in an extension field:\n" r --- User friendly way of printing satisfiablity results +-- User friendly way of printing satisfiability results instance Show SatResult where show (SatResult r) = showSMTResult "Unsatisfiable" "Unknown" diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -215,7 +215,7 @@ QueryInternal -> if supportsBitVectors solverCaps then [logicString cfg picked] else [logicString cfg Logic_ALL] -- fall-thru - where picked + where picked | needsQuantifiers = Logic_ALL | True = case (hasArrays, null uis && null tbls) of (False, False) -> QF_UFBV @@ -742,7 +742,7 @@ | True = lift2 "=" sgn sbvs -- Do not use distinct on floats; because +0/-0, and NaNs mess - -- up the meaning. Just go with reqular equals. + -- up the meaning. Just go with regular equals. notEqual sgn sbvs | fpOp || not hasDistinct = liftP sbvs | True = liftN "distinct" sgn sbvs diff --git a/Data/SBV/TP/Kernel.hs b/Data/SBV/TP/Kernel.hs --- a/Data/SBV/TP/Kernel.hs +++ b/Data/SBV/TP/Kernel.hs @@ -169,7 +169,7 @@ , quantifiedBool (\(Forall x) (Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) -> pf xs a b c d e .=> pf (x .: xs) a b c d e)] .=> quantifiedBool (\(Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) -> pf xs a b c d e) --- | Accept the given definition as a fact. Usually used to introduce definitial axioms, +-- | Accept the given definition as a fact. Usually used to introduce definitional axioms, -- giving meaning to uninterpreted symbols. Note that we perform no checks on these propositions, -- if you assert nonsense, then you get nonsense back. So, calls to 'axiom' should be limited to -- definitions, or basic axioms (like commutativity, associativity) of uninterpreted function symbols. diff --git a/Data/SBV/TP/TP.hs b/Data/SBV/TP/TP.hs --- a/Data/SBV/TP/TP.hs +++ b/Data/SBV/TP/TP.hs @@ -79,7 +79,7 @@ import qualified Test.QuickCheck as QC import Test.QuickCheck (quickCheckWithResult) --- | Captures the steps for a calculationa proof +-- | Captures the steps for a calculational proof data CalcStrategy = CalcStrategy { calcIntros :: SBool , calcProofTree :: TPProof , calcQCInstance :: [Int] -> Symbolic SBool diff --git a/Data/SBV/TP/Utils.hs b/Data/SBV/TP/Utils.hs --- a/Data/SBV/TP/Utils.hs +++ b/Data/SBV/TP/Utils.hs @@ -48,7 +48,7 @@ import Data.Typeable (typeOf, TypeRep) import Data.Char (isSpace) -import Data.List (intercalate, isPrefixOf, isSuffixOf, isInfixOf, nub, nubBy, sort, dropWhileEnd) +import Data.List (intercalate, isPrefixOf, isSuffixOf, isInfixOf, nub, sort, dropWhileEnd) import Data.Int (Int64) import Data.SBV.Utils.Lib (unQuote) @@ -365,7 +365,7 @@ | TPQC -- qc (quick-check) | TPNoTermCheck -- no termination check (smtFunctionNoTermination) | TPUser Int64 -- user given - deriving (NFData, Generic, Eq) + deriving (NFData, Generic, Eq, Ord) -- | Proof for a property. This type is left abstract, i.e., the only way to create on is via a -- call to lemma/theorem etc., ensuring soundness. (Note that the trusted-code base here @@ -396,10 +396,20 @@ | True = s where s = proofName p +-- | Deduplicate proof objects by their unique id, keeping the first occurrence. +-- Same result as @nubBy ((==) \`on\` uniqId)@, but O(n log n) instead of O(n^2). +nubByUniqId :: [ProofObj] -> [ProofObj] +nubByUniqId = go Set.empty + where go _ [] = [] + go seen (p:ps) + | u `Set.member` seen = go seen ps + | True = p : go (Set.insert u seen) ps + where u = uniqId p + -- | Nicely format a bunch of proof-names, shortened and uniquified. Note that if we get a dependency -- via multiple routes, they can get different uniqid's; so we do a bit of compression here. shortProofNames :: [ProofObj] -> String -shortProofNames = intercalate ", " . map merge . compress . sort . map shortProofName . nubBy (\a b -> uniqId a == uniqId b) +shortProofNames = intercalate ", " . map merge . compress . sort . map shortProofName . nubByUniqId where compress [] = [] compress (a:as) = case span (a ==) as of (same, other) -> (a, length same + 1) : compress other @@ -417,7 +427,7 @@ -- | Trust forms a semigroup instance Semigroup RootOfTrust where - RootOfTrust as <> RootOfTrust bs = RootOfTrust $ nubBy (\a b -> uniqId a == uniqId b) <$> (as <> bs) + RootOfTrust as <> RootOfTrust bs = RootOfTrust $ nubByUniqId <$> (as <> bs) -- | Trust forms a monoid instance Monoid RootOfTrust where diff --git a/Data/SBV/Tools/GenTest.hs b/Data/SBV/Tools/GenTest.hs --- a/Data/SBV/Tools/GenTest.hs +++ b/Data/SBV/Tools/GenTest.hs @@ -53,7 +53,7 @@ | True = do t <- tc gen (i+1) (t:sofar) tc = do (_, Result {resTraces=tvals, resConsts=(_, cs), resDefinitions=definitions, resConstraints=cstrs, resOutputs=os}) <- runSymbolic defaultSMTCfg (Concrete Nothing) (m >>= output) - let cval = fromMaybe (error "Cannot generate tests in the presence of uninterpeted constants!") . (`lookup` cs) + let cval = fromMaybe (error "Cannot generate tests in the presence of uninterpreted constants!") . (`lookup` cs) cond = and [cvToBool (cval v) | (False, _, v) <- F.toList cstrs] -- Only pick-up "hard" constraints, as indicated by False in the fist component unless (null definitions) $ error "Cannot generate tests in the presence of 'smtFunction' calls!" if cond diff --git a/Data/SBV/Tools/Overflow.hs b/Data/SBV/Tools/Overflow.hs --- a/Data/SBV/Tools/Overflow.hs +++ b/Data/SBV/Tools/Overflow.hs @@ -325,7 +325,7 @@ -- -- The result is at most N-2 for an N-bit word. Later we add two of these, so the maximum -- value we need to represent is 2N-4. This will require 1 + lg(2N-4) = 2 + log(N-1) bits. - -- To suppor the case N=0, we return a (2 + log N) bit word. + -- To support the case N=0, we return a (2 + log N) bit word. -- -- Example for 3 bits: -- diff --git a/Data/SBV/Tools/STree.hs b/Data/SBV/Tools/STree.hs --- a/Data/SBV/Tools/STree.hs +++ b/Data/SBV/Tools/STree.hs @@ -57,7 +57,7 @@ writeSTree s i j = walk (blastBE i) s where walk [] _ = SLeaf j walk (b:bs) (SBin l r) = SBin (ite b l (walk bs l)) (ite b (walk bs r) r) - walk _ _ = error $ "SBV.STree.writeSTree: Impossible happened while reading: " ++ show i + walk _ _ = error $ "SBV.STree.writeSTree: Impossible happened while writing: " ++ show i -- | Construct the fully balanced initial tree using the given values. mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e diff --git a/Data/SBV/Tools/WeakestPreconditions.hs b/Data/SBV/Tools/WeakestPreconditions.hs --- a/Data/SBV/Tools/WeakestPreconditions.hs +++ b/Data/SBV/Tools/WeakestPreconditions.hs @@ -315,7 +315,7 @@ -- Condition 1: Invariant must hold prior to loop entry invHoldsPrior <- wp start Skip (\st -> [(inv st, InvariantPre nm st)]) - -- Condition 2: If we iterate, invariant must be maitained by the body + -- Condition 2: If we iterate, invariant must be maintained by the body invMaintained <- wp st' body (\st -> [(iterates .=> inv st, InvariantMaintain nm st' st)]) -- Condition 3: If we terminate, invariant must be strong enough to establish the post condition diff --git a/Data/SBV/Tuple.hs b/Data/SBV/Tuple.hs --- a/Data/SBV/Tuple.hs +++ b/Data/SBV/Tuple.hs @@ -27,6 +27,8 @@ , tuple, untuple -- * Swapping, only for 2-tuples , swap + -- * Currying and uncurrying + , curry, uncurry, curry3, uncurry3 -- * Extractors for 2-tuple , fst, snd -- * Extractors for 3-tuple @@ -39,7 +41,7 @@ import Data.SBV.Core.Symbolic import Data.SBV.Core.Model -import Prelude hiding (fst, snd) +import Prelude hiding (fst, snd, curry, uncurry) #ifdef DOCTEST -- $setup @@ -61,6 +63,29 @@ swap t = tuple (b, a) where (a, b) = untuple t +-- | Symbolic currying: turn a function that takes a symbolic 2-tuple into one +-- that takes its two components separately. The inverse of 'uncurry'. +curry :: (SymVal a, SymVal b) => (STuple a b -> r) -> SBV a -> SBV b -> r +curry f a b = f (tuple (a, b)) + +-- | Symbolic uncurrying: turn a function of two arguments into one that takes a +-- symbolic 2-tuple. The inverse of 'curry'. +uncurry :: (SymVal a, SymVal b) => (SBV a -> SBV b -> r) -> STuple a b -> r +uncurry f t = f a b + where (a, b) = untuple t + +-- | Symbolic currying for 3-tuples: turn a function that takes a symbolic +-- 3-tuple into one that takes its three components separately. The inverse of +-- 'uncurry3'. +curry3 :: (SymVal a, SymVal b, SymVal c) => (STuple3 a b c -> r) -> SBV a -> SBV b -> SBV c -> r +curry3 f a b c = f (tuple (a, b, c)) + +-- | Symbolic uncurrying for 3-tuples: turn a function of three arguments into +-- one that takes a symbolic 3-tuple. The inverse of 'curry3'. +uncurry3 :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b -> SBV c -> r) -> STuple3 a b c -> r +uncurry3 f t = f a b c + where (a, b, c) = untuple t + -- | First of a tuple fst :: (SymVal a, SymVal b) => STuple a b -> SBV a fst t = a where (a, _) = untuple t @@ -77,7 +102,7 @@ snd3 :: (SymVal a, SymVal b, SymVal c) => STuple3 a b c -> SBV b snd3 t = b where (_, b, _) = untuple t --- | Thirdd of a 3-tuple +-- | Third of a 3-tuple thd3 :: (SymVal a, SymVal b, SymVal c) => STuple3 a b c -> SBV c thd3 t = c where (_, _, c) = untuple t diff --git a/Data/SBV/Utils/PrettyNum.hs b/Data/SBV/Utils/PrettyNum.hs --- a/Data/SBV/Utils/PrettyNum.hs +++ b/Data/SBV/Utils/PrettyNum.hs @@ -26,7 +26,7 @@ import Data.Char (intToDigit, ord, chr) import Data.Int (Int8, Int16, Int32, Int64) import Data.List (isPrefixOf) -import Data.Maybe (fromJust, fromMaybe, listToMaybe) +import Data.Maybe (fromMaybe, listToMaybe) import Data.Ratio (numerator, denominator) import Data.Word (Word8, Word16, Word32, Word64) import Data.Text (Text) @@ -300,7 +300,7 @@ -- | Binary printer s2 :: (Show a, Integral a) => a -> String -s2 v = showIntAtBase 2 dig v "" where dig = fromJust . flip lookup [(0, '0'), (1, '1')] +s2 v = showIntAtBase 2 intToDigit v "" -- | Hex printer s16 :: (Show a, Integral a) => a -> String diff --git a/Documentation/SBV/Examples/ADT/Expr.hs b/Documentation/SBV/Examples/ADT/Expr.hs --- a/Documentation/SBV/Examples/ADT/Expr.hs +++ b/Documentation/SBV/Examples/ADT/Expr.hs @@ -110,9 +110,9 @@ -- -- >>> evalSat -- Satisfiable. Model: --- e = Let "k" (Val 2) (Mul (Val 1) (Var "k")) :: Expr --- a = 18 :: Integer --- b = 10 :: Integer +-- e = Let "h" (Val 1) (Var "h") :: Expr +-- a = 9 :: Integer +-- b = 10 :: Integer evalSat :: IO SatResult evalSat = sat $ do e :: SExpr <- free "e" constrain $ isValid e @@ -129,8 +129,8 @@ -- -- >>> genE -- Satisfiable. Model: --- e1 = Let "p" (Val 5) (Val 3) :: Expr --- e2 = Val (-2) :: Expr +-- e1 = Let "k" (Mul (Val 1) (Mul (Val (-3)) (Val (-1)))) (Var "k") :: Expr +-- e2 = Val (-2) :: Expr genE :: IO SatResult genE = sat $ do e1 :: SExpr <- free "e1" e2 :: SExpr <- free "e2" @@ -146,7 +146,7 @@ -- | Query mode example. -- -- >>> queryE --- e1: (let p = 5 in 3) +-- e1: (let k = (1 * (-3 * -1)) in k) -- e2: -2 queryE :: IO () queryE = runSMT $ do diff --git a/Documentation/SBV/Examples/ADT/Param.hs b/Documentation/SBV/Examples/ADT/Param.hs --- a/Documentation/SBV/Examples/ADT/Param.hs +++ b/Documentation/SBV/Examples/ADT/Param.hs @@ -111,7 +111,7 @@ evalPlus5 = prove $ do e :: SExpr String Integer <- free "e" pure $ eval (e + 5) .== 5 + eval e --- | Is this a string identifier? Lowercase letter followed by any number of upeer-lower case letters nd digits. +-- | Is this a string identifier? Lowercase letter followed by any number of upper-lower case letters and digits. isId :: SString -> SBool isId s = s `match` (asciiLower * KStar (asciiLetter + digit)) @@ -119,9 +119,9 @@ -- -- >>> evalSat -- Satisfiable. Model: --- e = Let "k" (Val (-2)) (Mul (Val (-1)) (Var "k")) :: Expr String Integer --- a = 18 :: Integer --- b = 10 :: Integer +-- e = Let "h" (Val 1) (Var "h") :: Expr String Integer +-- a = 9 :: Integer +-- b = 10 :: Integer evalSat :: IO SatResult evalSat = sat $ do e :: SExpr String Integer <- free "e" constrain $ isValid isId e @@ -138,7 +138,7 @@ -- -- >>> genE -- Satisfiable. Model: --- e1 = Let "p" (Val 5) (Val 3) :: Expr String Integer +-- e1 = Let "h" (Val 5) (Val 3) :: Expr String Integer -- e2 = Val (-2) :: Expr String Integer genE :: IO SatResult genE = sat $ do e1 :: SExpr String Integer <- free "e1" @@ -155,9 +155,9 @@ -- | Query mode example. -- -- >>> queryE --- e1: (let a = (-3 * (8 + -7)) in ((a * (4 + a)) * -1)) +-- e1: (let a = ((let x = 20 in 4) * -5) in (-1 * -3)) -- e2: -2 --- e3: (let h = 257 % 258 in h) +-- e3: (let h = 79 % 80 in h) queryE :: IO () queryE = runSMT $ do e1 :: SExpr String Integer <- free "e1" diff --git a/Documentation/SBV/Examples/ADT/Types.hs b/Documentation/SBV/Examples/ADT/Types.hs --- a/Documentation/SBV/Examples/ADT/Types.hs +++ b/Documentation/SBV/Examples/ADT/Types.hs @@ -66,7 +66,7 @@ -> tc b (srng t) -- Application case. In this case, we ask the solver to give us the type of the - -- function, and then ensure the whole thing is well-formedvx + -- function, and then ensure the whole thing is well-formed App f a -> let tf = typeOf f in isTArr tf -- f must have an arrow type .&& tc f tf -- The function must type-check with that type diff --git a/Documentation/SBV/Examples/BitPrecise/Adders.hs b/Documentation/SBV/Examples/BitPrecise/Adders.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/BitPrecise/Adders.hs @@ -0,0 +1,185 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.BitPrecise.Adders +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Build two textbook binary adders out of logic gates and prove them correct, +-- fully automatically, by bit-blasting. +-- +-- We model each adder as a Haskell function over a statically-known list of +-- symbolic bits, producing a fixed Boolean circuit. We then prove---for a +-- chosen word size---that the circuit computes the same result as SBV's native +-- bit-vector addition @(+)@: +-- +-- * A /ripple-carry/ adder, which threads a carry sequentially through a +-- chain of full adders. +-- +-- * A /carry-lookahead/ adder, which computes every carry directly from the +-- generate\/propagate signals of all lower bits, with no sequential +-- dependency. +-- +-- Besides proving each adder equal to @(+)@, we also prove the two adders equal +-- to /each other/: the fast, parallel carry-lookahead circuit computes exactly +-- the same result as the simple ripple-carry reference. +-- +-- All proofs here are discharged by a single decidable bit-vector query at a +-- fixed width. See "Documentation.SBV.Examples.TP.Adder" for the companion +-- development that instead proves a ripple-carry adder correct for /all/ widths +-- at once, by induction. +----------------------------------------------------------------------------- + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Documentation.SBV.Examples.BitPrecise.Adders where + +import Data.SBV hiding (fullAdder) +import GHC.TypeLits (KnownNat) + +#ifdef DOCTEST +-- $setup +-- >>> import Data.SBV +-- >>> :set -XDataKinds -XTypeApplications -XScopedTypeVariables +#endif + +-- | A symbolic bit is just a symbolic boolean. +type Bit = SBool + +-- * Logic gates + +-- | A half adder takes two bits and produces their sum bit and carry bit: +-- @sum = a xor b@, @carry = a and b@. +halfAdder :: Bit -> Bit -> (Bit, Bit) +halfAdder a b = (a .<+> b, a .&& b) + +-- | A full adder takes two bits and an incoming carry, and produces the sum bit +-- together with the outgoing carry. We build it out of two half adders, in the +-- usual way. +fullAdder :: Bit -> Bit -> Bit -> (Bit, Bit) +fullAdder a b cin = (s, c0 .|| c1) + where (s0, c0) = halfAdder a b + (s, c1) = halfAdder s0 cin + +-- * Ripple-carry adder + +-- | The ripple-carry adder. Given an incoming carry and a little-endian list of +-- bit pairs (one pair per bit position, least-significant first), it threads the +-- carry through a chain of full adders, returning the list of sum bits together +-- with the final carry-out. +rippleAdd :: Bit -> [(Bit, Bit)] -> ([Bit], Bit) +rippleAdd cin [] = ([], cin) +rippleAdd cin ((a, b) : ps) = (s : ss, cout) + where (s, c) = fullAdder a b cin + (ss, cout) = rippleAdd c ps + +-- * Carry-lookahead adder + +-- | Generate and propagate signals for a bit position: a position /generates/ a +-- carry when both inputs are set, and /propagates/ an incoming carry when +-- exactly one input is set. +generatePropagate :: Bit -> Bit -> (Bit, Bit) +generatePropagate a b = (a .&& b, a .<+> b) + +-- | The carry-lookahead adder. Rather than rippling the carry through the chain, +-- it computes the carry /into/ each position directly from the +-- generate\/propagate signals of all lower positions, using the textbook +-- expansion +-- +-- @ +-- c(i) = g(i-1) + p(i-1).g(i-2) + ... + p(i-1)...p(1).g(0) + p(i-1)...p(0).cin +-- @ +-- +-- so that every carry is an independent flat formula with no sequential +-- dependency. The sum bit at position @i@ is then @p(i) xor c(i)@, and the +-- carry-out is the carry into the (nonexistent) position just past the top. +lookaheadAdd :: Bit -> [(Bit, Bit)] -> ([Bit], Bit) +lookaheadAdd cin ps = (sums, carryInto n) + where n = length ps + gps = [ generatePropagate a b | (a, b) <- ps ] + + g k = fst (gps !! k) + p k = snd (gps !! k) + + -- product of the propagate signals over positions [lo .. hi-1] + prodP lo hi = sAnd [ p k | k <- [lo .. hi - 1] ] + + -- carry into position i, expanded over all lower positions + carryInto i = sOr $ (cin .&& prodP 0 i) + : [ g j .&& prodP (j + 1) i | j <- [0 .. i - 1] ] + + sums = [ p i .<+> carryInto i | i <- [0 .. n - 1] ] + +-- * Lifting to words + +-- | Run an adder over the bits of two words. We blast both operands into +-- little-endian bit lists, feed them to the adder with no incoming carry, and +-- reassemble the sum bits into a word. The carry-out is dropped, matching the +-- wrap-around semantics of bit-vector @(+)@. +addWith :: forall n. (KnownNat n, BVIsNonZero n) => (Bit -> [(Bit, Bit)] -> ([Bit], Bit)) -> SWord n -> SWord n -> SWord n +addWith adder x y = fromBitsLE ss + where (ss, _) = adder sFalse (zip (blastLE x) (blastLE y)) + +-- | The ripple-carry adder, lifted to words. +rippleAddWord :: (KnownNat n, BVIsNonZero n) => SWord n -> SWord n -> SWord n +rippleAddWord = addWith rippleAdd + +-- | The carry-lookahead adder, lifted to words. +lookaheadAddWord :: (KnownNat n, BVIsNonZero n) => SWord n -> SWord n -> SWord n +lookaheadAddWord = addWith lookaheadAdd + +-- * Correctness + +-- | The ripple-carry adder computes bit-vector addition. We prove it here at +-- width 8, but the same call proves it at any width you instantiate: +-- +-- >>> rippleCorrect @8 +-- Q.E.D. +-- +-- Adder-versus-@(+)@ equivalence is one of the easy cases for bit-blasting (the +-- carry chain is linear), so this stays fast even at large widths---it is the +-- cheap baseline to compare the lookahead proofs against. +rippleCorrect :: forall n. (KnownNat n, BVIsNonZero n) => IO ThmResult +rippleCorrect = prove $ \(x :: SWord n) (y :: SWord n) -> rippleAddWord x y .== x + y + +-- | The carry-lookahead adder computes bit-vector addition: +-- +-- >>> lookaheadCorrect @8 +-- Q.E.D. +-- +-- Note that, unlike 'rippleCorrect', this proof slows down noticeably as the +-- width grows. The lookahead carry is the flat \(O(n^2)\) generate\/propagate +-- expansion, so the formula handed to the solver grows quadratically in the +-- width---try @lookaheadCorrect \@64@, @\@128@, @\@256@ to watch it climb. +lookaheadCorrect :: forall n. (KnownNat n, BVIsNonZero n) => IO ThmResult +lookaheadCorrect = prove $ \(x :: SWord n) (y :: SWord n) -> lookaheadAddWord x y .== x + y + +-- | The fast carry-lookahead adder agrees with the simple ripple-carry adder on +-- every input---the parallel carry computation refines the sequential one: +-- +-- >>> rippleEqLookahead @8 +-- Q.E.D. +-- +-- This proof drags in the same \(O(n^2)\) lookahead carry expansion as +-- 'lookaheadCorrect', so it scales the same way: comfortable at small widths, +-- visibly slower as the width grows. +rippleEqLookahead :: forall n. (KnownNat n, BVIsNonZero n) => IO ThmResult +rippleEqLookahead = prove $ \(x :: SWord n) (y :: SWord n) -> rippleAddWord x y .== lookaheadAddWord x y + +-- | The carry-out of the ripple-carry adder is exactly the unsigned overflow +-- flag: it is set precisely when the true sum does not fit in @n@ bits, which +-- for an addition with no incoming carry is detectable as the result wrapping +-- below either operand: +-- +-- >>> rippleOverflow @8 +-- Q.E.D. +rippleOverflow :: forall n. (KnownNat n, BVIsNonZero n) => IO ThmResult +rippleOverflow = prove $ \(x :: SWord n) (y :: SWord n) -> + let (_, cout) = rippleAdd sFalse (zip (blastLE x) (blastLE y)) + in cout .== ((x + y) .< x) diff --git a/Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs b/Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs --- a/Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs +++ b/Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs @@ -25,7 +25,7 @@ -- OD -- @ -- --- PDEP (parallel deposit) is similar, except the assigment is: +-- PDEP (parallel deposit) is similar, except the assignment is: -- -- @ -- DEST[m] := TEMP[k] diff --git a/Documentation/SBV/Examples/Crypto/Prince.hs b/Documentation/SBV/Examples/Crypto/Prince.hs --- a/Documentation/SBV/Examples/Crypto/Prince.hs +++ b/Documentation/SBV/Examples/Crypto/Prince.hs @@ -6,8 +6,7 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental -- --- Implementation of Prince encryption and decrytion, following the spec --- +-- Implementation of Prince encryption and decryption. ----------------------------------------------------------------------------- {-# LANGUAGE CPP #-} diff --git a/Documentation/SBV/Examples/Existentials/Diophantine.hs b/Documentation/SBV/Examples/Existentials/Diophantine.hs --- a/Documentation/SBV/Examples/Existentials/Diophantine.hs +++ b/Documentation/SBV/Examples/Existentials/Diophantine.hs @@ -114,7 +114,7 @@ -- (k, 2+k', 2k+k') -- -- That is, for arbitrary @k@ and @k'@, we have two different solutions. (An infinite family.) --- You can verify these solutuions by substituting the values for @x@, @y@ and @z@ in the above, for each choice. +-- You can verify these solutions by substituting the values for @x@, @y@ and @z@ in the above, for each choice. -- It's harder to see that they cover all possibilities, but a moments thought reveals that is indeed the case. test :: IO Solution test = ldn (Proxy @4) Nothing [([2,1,-1], 2)] diff --git a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs --- a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs +++ b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs @@ -178,7 +178,7 @@ -- >>> sat skolemEx1 -- Satisfiable -- --- But this isn't really illimunating. We can first skolemize, and then ask to satisfy: +-- But this isn't really illuminating. We can first skolemize, and then ask to satisfy: -- -- >>> sat $ skolemize skolemEx1 -- Satisfiable. Model: diff --git a/Documentation/SBV/Examples/Misc/ProgramPaths.hs b/Documentation/SBV/Examples/Misc/ProgramPaths.hs --- a/Documentation/SBV/Examples/Misc/ProgramPaths.hs +++ b/Documentation/SBV/Examples/Misc/ProgramPaths.hs @@ -30,7 +30,7 @@ d1 :: SInteger -> SInteger -> SInteger d1 x y = ite (y .< x - 2) 7 2 --- | Symbolic version of @d2 x y = if y > 3 then 10 else 50@ +-- | Symbolic version of @d2 y = if y > 3 then 10 else 50@ d2 :: SInteger -> SInteger d2 y = ite (y .> 3) 10 50 diff --git a/Documentation/SBV/Examples/ProofTools/Strengthen.hs b/Documentation/SBV/Examples/ProofTools/Strengthen.hs --- a/Documentation/SBV/Examples/ProofTools/Strengthen.hs +++ b/Documentation/SBV/Examples/ProofTools/Strengthen.hs @@ -22,7 +22,7 @@ -- Where @*@ stands for non-deterministic choice. For each program we try to prove that @y >= 1@ is an invariant. -- -- It turns out that the property @y >= 1@ is indeed an invariant, but is --- not inductive for either program. We proceed to strengten the invariant +-- not inductive for either program. We proceed to strengthen the invariant -- and establish it for the first case. We then note that the same strengthening -- doesn't work for the second program, and find a further strengthening to -- establish that case as well. This example follows the introductory example diff --git a/Documentation/SBV/Examples/Puzzles/AOC_2021_24.hs b/Documentation/SBV/Examples/Puzzles/AOC_2021_24.hs --- a/Documentation/SBV/Examples/Puzzles/AOC_2021_24.hs +++ b/Documentation/SBV/Examples/Puzzles/AOC_2021_24.hs @@ -12,7 +12,7 @@ -- computer with 4 integer registers (w, x, y, z), and 6 instructions (inp, add, mul, div, mod, eql). -- You are given a program (hilariously called "monad"), and your goal is to figure out what -- the maximum and minimum inputs you can provide to this program such that when it runs --- register z ends up with the value 1. Please refer to the above link for the full description. +-- register z ends up with the value 0. Please refer to the above link for the full description. -- -- While there are multiple ways to solve this problem in SBV, the solution here demonstrates -- how to turn programs in this fictional language into actual Haskell/SBV programs, i.e., diff --git a/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs b/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs --- a/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs +++ b/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs @@ -102,7 +102,7 @@ -- | We can let years to range over arbitrary integers. But that complicates the -- job of the solver. So, based on what we know from the problem, we restrict --- our attention to years betweek 1900 and 2100. Note that there are only +-- our attention to years between 1900 and 2100. Note that there are only -- two years that satisfy this in that range: 1936 and 2025. (Any other square -- year makes no sense for the setting of the problem.) To simplify the square-root -- computation, we also store the square root in this list as the second component: @@ -155,7 +155,7 @@ ----------------------------------- myBirthday <- symDate "My Birthday" - -- I was born in the last millenium + -- I was born in the last millennium constrain $ syear myBirthday .< 2000 .&& syear myBirthday .>= 1900 -- My next birthday will be a square diff --git a/Documentation/SBV/Examples/Puzzles/Tower.hs b/Documentation/SBV/Examples/Puzzles/Tower.hs --- a/Documentation/SBV/Examples/Puzzles/Tower.hs +++ b/Documentation/SBV/Examples/Puzzles/Tower.hs @@ -110,7 +110,7 @@ -- * Example run ------------------------------------------------------------------- --- | Solve the puzzle descibed above. We get: +-- | Solve the puzzle described above. We get: -- -- >>> example -- 1 2 3 2 2 4 diff --git a/Documentation/SBV/Examples/Queries/GuessNumber.hs b/Documentation/SBV/Examples/Queries/GuessNumber.hs --- a/Documentation/SBV/Examples/Queries/GuessNumber.hs +++ b/Documentation/SBV/Examples/Queries/GuessNumber.hs @@ -42,7 +42,7 @@ DSat{} -> error "Unexpected delta-sat result.." -- Won't really happen Unsat -> -- This cannot happen! If it does, the input was - -- not properly constrainted. Note that we found this + -- not properly constrained. Note that we found this -- by getting an Unsat, not by checking the value! error $ unlines [ "There's no solution!" , "Guess sequence: " ++ show (reverse sofar) diff --git a/Documentation/SBV/Examples/Queries/UnsatCore.hs b/Documentation/SBV/Examples/Queries/UnsatCore.hs --- a/Documentation/SBV/Examples/Queries/UnsatCore.hs +++ b/Documentation/SBV/Examples/Queries/UnsatCore.hs @@ -44,7 +44,7 @@ -- >>> ucCore -- Unsat core is: ["less than 5","more than 10"] -- --- Demonstrating that the constraint @a .> b@ is /not/ needed for unsatisfiablity in this case. +-- Demonstrating that the constraint @a .> b@ is /not/ needed for unsatisfiability in this case. ucCore :: IO () ucCore = do mbCore <- runSMT p case mbCore of diff --git a/Documentation/SBV/Examples/TP/Adder.hs b/Documentation/SBV/Examples/TP/Adder.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/TP/Adder.hs @@ -0,0 +1,395 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.TP.Adder +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Prove binary adders correct by induction, for /all/ widths at once. +-- +-- This is the inductive companion to +-- "Documentation.SBV.Examples.BitPrecise.Adders", which proves fixed-width +-- adders correct automatically by bit-blasting. Here, instead, we model the +-- operands as arbitrary-length, little-endian symbolic bit lists and prove---by +-- induction on the list---properties that hold with no bound on the width: +-- +-- * a ripple-carry adder agrees with the mathematical value of the bits +-- (@correctness@); +-- +-- * a parallel-prefix (carry-lookahead) tree computes the same carry as the +-- ripple, because the generate\/propagate carry operator is associative +-- (@lookaheadCorrect@); and +-- +-- * that lookahead carry is exactly the carry the ripple adder threads +-- (@lookaheadMatchesAdder@). +-- +-- A number is represented by a little-endian list of bit pairs: one +-- @(a, b)@ per position, least-significant first, where @a@ is a bit of the +-- first operand and @b@ the corresponding bit of the second. The integer value +-- of such a list is @sum_i bit_i * 2^i@. +----------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE TypeApplications #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Documentation.SBV.Examples.TP.Adder where + +import Prelude hiding (fst, snd, foldl, map, curry, uncurry, (++)) + +import Data.SBV hiding (fullAdder) +import Data.SBV.List (foldl, map, (++)) +import Data.SBV.Tuple +import Data.SBV.TP + +import Documentation.SBV.Examples.TP.Lists (foldlOverAppend) + +-- We reuse the very same combinational gates that the fixed-width, bit-blasted +-- companion proves correct---only the adder driver differs (a symbolic, +-- inductive recursion here versus a metalevel one there). The 'Data.SBV.fullAdder' +-- word-level operation is hidden above so 'fullAdder' refers to that gate. +import Documentation.SBV.Examples.BitPrecise.Adders (Bit, fullAdder, generatePropagate) + +#ifdef DOCTEST +-- $setup +-- >>> :set -XOverloadedLists +-- >>> import Data.SBV +-- >>> import Data.SBV.TP +#endif + +-- * Bits, values, and the adder + +-- | The integer value of a single bit: @1@ if set, @0@ otherwise. +bitVal :: Bit -> SInteger +bitVal b = ite b 1 0 + +-- | The integer value of a little-endian bit list: @sum_i bit_i * 2^i@. +val :: SList Bool -> SInteger +val = smtFunction "val" + $ \bs -> [sCase| bs of + [] -> 0 + x : xs -> bitVal x + 2 * val xs + |] + +-- | The value of the first operand, read off the first components of the pairs. +valA :: SList (Bool, Bool) -> SInteger +valA = smtFunction "valA" + $ \ps -> [sCase| ps of + [] -> 0 + (a, _) : qs -> bitVal a + 2 * valA qs + |] + +-- | The value of the second operand, read off the second components of the pairs. +valB :: SList (Bool, Bool) -> SInteger +valB = smtFunction "valB" + $ \ps -> [sCase| ps of + [] -> 0 + (_, b) : qs -> bitVal b + 2 * valB qs + |] + +-- | The ripple-carry adder. Given an incoming carry and a little-endian list of +-- bit pairs, thread the carry through a chain of full adders (the same +-- 'fullAdder' gate the bit-blasted companion verifies), emitting each sum bit +-- and, at the end, the final carry-out as the most-significant bit. The result +-- is therefore one bit longer than the input, so its value is exactly the full +-- sum---no truncation. +rca :: Bit -> SList (Bool, Bool) -> SList Bool +rca = smtFunction "rca" + $ \c ps -> [sCase| ps of + [] -> [c] + p : qs -> let (s, co) = uncurry fullAdder p c + in s .: rca co qs + |] + +-- * Correctness + +-- | The ripple-carry adder computes the sum of its operands, for any width: +-- +-- @val (rca 0 ps) == valA ps + valB ps@ +-- +-- We prove it via a more general lemma that tracks the incoming carry, since the +-- recursive calls feed each stage's carry-out into the next. +-- +-- >>> runTP correctness +-- Lemma: fullAdderCorrect Q.E.D. +-- Inductive lemma: rcaCorrect +-- Step: Base Q.E.D. +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Step: 3 Q.E.D. +-- Step: 4 Q.E.D. +-- Step: 5 Q.E.D. +-- Result: Q.E.D. +-- Lemma: adderCorrect Q.E.D. +-- Functions proven terminating: rca, val, valA, valB +-- [Proven] adderCorrect :: Ɐps ∷ [(Bool, Bool)] → Bool +correctness :: TP (Proof (Forall "ps" [(Bool, Bool)] -> SBool)) +correctness = do + + -- A single full adder is arithmetically correct: the sum bit plus twice the + -- carry-out equals the sum of the three input bits. This is a finite boolean + -- fact, discharged directly. + faC <- lemma "fullAdderCorrect" + (\(Forall @"a" a) (Forall @"b" b) (Forall @"c" c) -> + let (s, co) = fullAdder a b c + in bitVal s + 2 * bitVal co .== bitVal a + bitVal b + bitVal c) + [] + + -- The general statement, tracking the incoming carry. Induct on the list of + -- bit pairs; the carry is universally quantified so the induction hypothesis + -- applies at the carry-out fed to the recursive call. + rcaC <- induct "rcaCorrect" + (\(Forall @"ps" ps) (Forall @"c" c) -> + val (rca c ps) .== valA ps + valB ps + bitVal c) $ + \ih (p, ps) c -> + let a = fst p + b = snd p + (s, co) = fullAdder a b c + in [] |- val (rca c (p .: ps)) + =: val (s .: rca co ps) + =: bitVal s + 2 * val (rca co ps) + ?? ih `at` Inst @"c" co + =: bitVal s + 2 * (valA ps + valB ps + bitVal co) + ?? faC `at` (Inst @"a" a, Inst @"b" b, Inst @"c" c) + =: (bitVal a + 2 * valA ps) + (bitVal b + 2 * valB ps) + bitVal c + =: valA (p .: ps) + valB (p .: ps) + bitVal c + =: qed + + -- The headline corollary: with no incoming carry, the adder computes the sum. + lemma "adderCorrect" + (\(Forall ps) -> val (rca sFalse ps) .== valA ps + valB ps) + [proofOf rcaC] + +-- * Carry-lookahead, via a parallel-prefix tree +-- +-- $lookahead +-- A ripple-carry adder is slow because each stage waits for the carry from the +-- one below it. A /carry-lookahead/ adder breaks that chain by computing the +-- carries in parallel. The key is to summarize a contiguous block of positions +-- by a @(generate, propagate)@ /section/: whether the block produces a carry on +-- its own (@generate@), and whether it would pass an incoming carry straight +-- through (@propagate@). Adjacent sections combine with the associative operator +-- 'dot', so the carries can be gathered by a balanced /tree/ of 'dot's rather +-- than a linear ripple. +-- +-- We prove that tree correct against the ripple as follows. 'dot' is an +-- associative monoid with identity 'idSec', and applying a section to an +-- incoming carry ('applyC') is its action. The ripple carry is the /linear/ +-- fold of 'dot' over the sections (@carryIsFold@), and a balanced tree of 'dot's +-- computes that /same/ fold by associativity (@treeIsFold@). Hence the parallel +-- tree and the sequential ripple agree. + +-- | Combine two adjacent @(generate, propagate)@ sections, lower-order first. +-- The combined block generates a carry if the high part does, or if it +-- propagates one generated by the low part; it propagates only if both do. +dot :: SBV (Bool, Bool) -> SBV (Bool, Bool) -> SBV (Bool, Bool) +dot lo hi = tuple (fst hi .|| (snd hi .&& fst lo), snd hi .&& snd lo) + +-- | The identity section: generates nothing, propagates everything. +idSec :: SBV (Bool, Bool) +idSec = tuple (sFalse, sTrue) + +-- | Apply a section to an incoming carry, giving the carry out of that section. +applyC :: SBV (Bool, Bool) -> Bit -> Bit +applyC sec c = fst sec .|| (snd sec .&& c) + +-- | The sequential ripple carry-out: thread the incoming carry through the +-- sections, left to right. +carry :: Bit -> SList (Bool, Bool) -> Bit +carry = smtFunction "carry" + $ \c gps -> [sCase| gps of + [] -> c + b : rest -> carry (applyC b c) rest + |] + +-- | The @(generate, propagate)@ section of a single operand bit-pair @(a, b)@, +-- using the very same 'generatePropagate' gate as the bit-blasted companion. +gpOf :: SBV (Bool, Bool) -> SBV (Bool, Bool) +gpOf p = tuple (uncurry generatePropagate p) + +-- | The carry-out actually threaded by the ripple adder 'rca': fold the +-- incoming carry through the full-adder carry of each position. (This is 'rca' +-- with the sum bits dropped---it threads the identical carry, via the same +-- 'fullAdder'.) +rcaCarry :: Bit -> SList (Bool, Bool) -> Bit +rcaCarry = smtFunction "rcaCarry" + $ \c ps -> [sCase| ps of + [] -> c + p : qs -> let (_, co) = uncurry fullAdder p c + in rcaCarry co qs + |] + +-- | The headline lookahead result, in textbook parallel-prefix form: the ripple +-- carry over a concatenation equals combining the two halves' sections +-- /independently/ and then applying the result to the incoming carry. Since +-- 'dot' is associative, the halves can be split the same way recursively---so +-- the carries can be gathered by a balanced /tree/ of 'dot's instead of a linear +-- ripple, and this says every such tree computes the same carry. +-- +-- The proof rests on two pieces: @carryIsFold@ (the ripple carry /is/ the linear +-- fold of 'dot'), kept as its own reusable lemma, and @foldlDotSplit@ (the fold +-- distributes over append---the associativity law that licenses any tree). +-- +-- >>> runTP lookaheadCorrect +-- Lemma: dotAssoc Q.E.D. +-- Lemma: dotLeftUnit Q.E.D. +-- Lemma: applyCDot Q.E.D. +-- Inductive lemma: foldlDotShift +-- Step: Base Q.E.D. +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Step: 3 Q.E.D. +-- Step: 4 Q.E.D. +-- Step: 5 Q.E.D. +-- Step: 6 Q.E.D. +-- Result: Q.E.D. +-- Inductive lemma: carryIsFold +-- Step: Base Q.E.D. +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Step: 3 Q.E.D. +-- Step: 4 Q.E.D. +-- Step: 5 Q.E.D. +-- Step: 6 Q.E.D. +-- Result: Q.E.D. +-- Inductive lemma: foldlOverAppend +-- Step: Base Q.E.D. +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Step: 3 Q.E.D. +-- Result: Q.E.D. +-- Lemma: foldlDotSplit +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Result: Q.E.D. +-- Lemma: treeCarry +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Result: Q.E.D. +-- Functions proven terminating: carry, sbv.foldl +-- [Proven] treeCarry :: Ɐc ∷ Bool → Ɐxs ∷ [(Bool, Bool)] → Ɐys ∷ [(Bool, Bool)] → Bool +lookaheadCorrect :: TP (Proof (Forall "c" Bool -> Forall "xs" [(Bool, Bool)] -> Forall "ys" [(Bool, Bool)] -> SBool)) +lookaheadCorrect = do + + -- 'dot' is an associative monoid with identity 'idSec'; 'applyC' is its + -- action. All finite boolean facts. + assoc <- lemma "dotAssoc" (\(Forall @"x" x) (Forall @"y" y) (Forall @"z" z) -> dot x (dot y z) .== dot (dot x y) z) [] + lunit <- lemma "dotLeftUnit" (\(Forall @"x" x) -> dot idSec x .== x) [] + act <- lemma "applyCDot" (\(Forall @"lo" lo) (Forall @"hi" hi) (Forall @"c" c) -> applyC (dot lo hi) c .== applyC hi (applyC lo c)) [] + + -- Folding with an initial section @s@ equals @s@ combined with the fold from + -- the identity. (Accumulator reassociation, à la Lists.foldrFoldl.) + fldShift <- induct "foldlDotShift" + (\(Forall @"xs" xs) (Forall @"s" s) -> + foldl dot s xs .== dot s (foldl dot idSec xs)) $ + \ih (x, xs) s -> [] |- foldl dot s (x .: xs) + =: foldl dot (dot s x) xs + ?? ih `at` Inst @"s" (dot s x) + =: dot (dot s x) (foldl dot idSec xs) + ?? assoc + =: dot s (dot x (foldl dot idSec xs)) + ?? ih `at` Inst @"s" x + =: dot s (foldl dot x xs) + ?? lunit + =: dot s (foldl dot (dot idSec x) xs) + =: dot s (foldl dot idSec (x .: xs)) + =: qed + + -- The reusable link: the sequential ripple carry is the left fold of 'dot' + -- over the sections, applied to the incoming carry. Induct on the sections; + -- the carry is the threaded argument, so the hypothesis applies at the next + -- carry-in. + cif <- induct "carryIsFold" + (\(Forall @"gps" gps) (Forall @"c" c) -> + carry c gps .== applyC (foldl dot idSec gps) c) $ + \ih (b, gps) c -> [] |- carry c (b .: gps) + =: carry (applyC b c) gps + ?? ih `at` Inst @"c" (applyC b c) + =: applyC (foldl dot idSec gps) (applyC b c) + ?? act `at` (Inst @"lo" b, Inst @"hi" (foldl dot idSec gps), Inst @"c" c) + =: applyC (dot b (foldl dot idSec gps)) c + ?? fldShift `at` (Inst @"xs" gps, Inst @"s" b) + =: applyC (foldl dot b gps) c + ?? lunit + =: applyC (foldl dot (dot idSec b) gps) c + =: applyC (foldl dot idSec (b .: gps)) c + =: qed + + -- foldl of 'dot' distributes over append (imported from the Lists examples). + foa <- foldlOverAppend dot + + -- The split/homomorphism law: reducing a concatenation equals reducing the + -- halves independently and combining them with 'dot'. This is what licenses + -- any balanced (tree) grouping of the sections. + splitLaw <- calc "foldlDotSplit" + (\(Forall @"xs" xs) (Forall @"ys" ys) -> + foldl dot idSec (xs ++ ys) .== dot (foldl dot idSec xs) (foldl dot idSec ys)) $ + \xs ys -> [] |- foldl dot idSec (xs ++ ys) + ?? foa `at` (Inst @"xs" xs, Inst @"ys" ys, Inst @"e" idSec) + =: foldl dot (foldl dot idSec xs) ys + ?? fldShift `at` (Inst @"xs" ys, Inst @"s" (foldl dot idSec xs)) + =: dot (foldl dot idSec xs) (foldl dot idSec ys) + =: qed + + -- Headline: the ripple carry of a concatenation equals applying the + -- independently-combined half-sections to the incoming carry. + calc "treeCarry" + (\(Forall @"c" c) (Forall @"xs" xs) (Forall @"ys" ys) -> + carry c (xs ++ ys) .== applyC (dot (foldl dot idSec xs) (foldl dot idSec ys)) c) $ + \c xs ys -> [] |- carry c (xs ++ ys) + ?? cif `at` (Inst @"gps" (xs ++ ys), Inst @"c" c) + =: applyC (foldl dot idSec (xs ++ ys)) c + ?? splitLaw `at` (Inst @"xs" xs, Inst @"ys" ys) + =: applyC (dot (foldl dot idSec xs) (foldl dot idSec ys)) c + =: qed + +-- | The capstone, tying the lookahead machinery back to the actual adder: +-- running the (foldable, tree-groupable) section 'carry' over the operands' +-- generate\/propagate signals reproduces exactly the carry that the ripple adder +-- 'rca' threads. Combined with @treeCarry@, this says the adder's own carry can +-- be computed by any balanced prefix tree. +-- +-- >>> runTP lookaheadMatchesAdder +-- Lemma: applyCgpOf Q.E.D. +-- Inductive lemma: lookaheadMatchesAdder +-- Step: Base Q.E.D. +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Step: 3 Q.E.D. +-- Step: 4 Q.E.D. +-- Step: 5 Q.E.D. +-- Result: Q.E.D. +-- Functions proven terminating: carry, rcaCarry, sbv.map +-- [Proven] lookaheadMatchesAdder :: Ɐps ∷ [(Bool, Bool)] → Ɐc ∷ Bool → Bool +lookaheadMatchesAdder :: TP (Proof (Forall "ps" [(Bool, Bool)] -> Forall "c" Bool -> SBool)) +lookaheadMatchesAdder = do + + -- Applying a position's generate/propagate section to a carry is exactly the + -- full-adder carry-out. A finite boolean fact. + applyGP <- lemma "applyCgpOf" + (\(Forall @"p" p) (Forall @"c" c) -> + let (_, co) = uncurry fullAdder p c + in applyC (gpOf p) c .== co) + [] + + -- Induct on the operands; the carry is threaded, so the hypothesis applies at + -- the next carry-in. + induct "lookaheadMatchesAdder" + (\(Forall @"ps" ps) (Forall @"c" c) -> carry c (map gpOf ps) .== rcaCarry c ps) $ + \ih (p, ps) c -> let (_, co) = uncurry fullAdder p c + in [] |- carry c (map gpOf (p .: ps)) + =: carry c (gpOf p .: map gpOf ps) + =: carry (applyC (gpOf p) c) (map gpOf ps) + ?? applyGP `at` (Inst @"p" p, Inst @"c" c) + =: carry co (map gpOf ps) + ?? ih `at` Inst @"c" co + =: rcaCarry co ps + =: rcaCarry c (p .: ps) + =: qed diff --git a/Documentation/SBV/Examples/TP/GCD.hs b/Documentation/SBV/Examples/TP/GCD.hs --- a/Documentation/SBV/Examples/TP/GCD.hs +++ b/Documentation/SBV/Examples/TP/GCD.hs @@ -176,11 +176,11 @@ -- -- ==== __Proof__ -- >>> runTP zeroGCD --- Lemma: negGCD Q.E.D. +-- Lemma: zeroGCD Q.E.D. -- Functions proven terminating: nGCD --- [Proven] negGCD :: Ɐa ∷ Integer → Bool +-- [Proven] zeroGCD :: Ɐa ∷ Integer → Bool zeroGCD :: TP (Proof (Forall "a" Integer -> SBool)) -zeroGCD = lemma "negGCD" (\(Forall a) -> gcd a 0 .== gcd 0 a .&& gcd 0 a .== abs a .&& gcd 0 0 .== 0) [] +zeroGCD = lemma "zeroGCD" (\(Forall a) -> gcd a 0 .== gcd 0 a .&& gcd 0 a .== abs a .&& gcd 0 0 .== 0) [] -- * Even and odd @@ -842,7 +842,7 @@ -- * GCD via subtraction --- | @nGCDSub@ is the original verision of Euclid, which uses subtraction instead of modulus. This is the version that +-- | @nGCDSub@ is the original version of Euclid, which uses subtraction instead of modulus. This is the version that -- works on non-negative numbers. It has the precondition that @a >= b >= 0@, and maintains this invariant in each -- recursive call. nGCDSub :: SInteger -> SInteger -> SInteger diff --git a/Documentation/SBV/Examples/TP/InsertionSort.hs b/Documentation/SBV/Examples/TP/InsertionSort.hs --- a/Documentation/SBV/Examples/TP/InsertionSort.hs +++ b/Documentation/SBV/Examples/TP/InsertionSort.hs @@ -168,7 +168,7 @@ =: qed -------------------------------------------------------------------------------------------- - -- Part III. Prove that the output of insertion sort is a permuation of its input + -- Part III. Prove that the output of insertion sort is a permutation of its input -------------------------------------------------------------------------------------------- insertIsElem <- diff --git a/Documentation/SBV/Examples/TP/Lists.hs b/Documentation/SBV/Examples/TP/Lists.hs --- a/Documentation/SBV/Examples/TP/Lists.hs +++ b/Documentation/SBV/Examples/TP/Lists.hs @@ -1490,7 +1490,7 @@ (\(Forall @"xs" xs) (Forall @"n" n) -> n .<= 0 .=> take n (map f xs) .== map f (take n xs)) [] - h2 <- induct "take_map.n > 0" + h2 <- inductWith cvc5 "take_map.n > 0" (\(Forall @"xs" xs) (Forall @"n" n) -> n .> 0 .=> take n (map f xs) .== map f (take n xs)) $ \ih (x, xs) n -> [n .> 0] |- take n (map f (x .: xs)) =: take n (f x .: map f xs) @@ -1813,7 +1813,7 @@ uninterleave :: SymVal a => SList a -> STuple [a] [a] uninterleave lst = uninterleaveGen lst (tuple ([], [])) --- | Generalized form of uninterleave with the auxilary lists made explicit. +-- | Generalized form of uninterleave with the auxiliary lists made explicit. uninterleaveGen :: SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a] uninterleaveGen = smtFunction "uninterleave" $ \xs alts -> let (es, os) = untuple alts diff --git a/Documentation/SBV/Examples/TP/MergeSort.hs b/Documentation/SBV/Examples/TP/MergeSort.hs --- a/Documentation/SBV/Examples/TP/MergeSort.hs +++ b/Documentation/SBV/Examples/TP/MergeSort.hs @@ -225,7 +225,7 @@ |] -------------------------------------------------------------------------------------------- - -- Part III. Prove that the output of merge sort is a permuation of its input + -- Part III. Prove that the output of merge sort is a permutation of its input -------------------------------------------------------------------------------------------- mergeCount <- sInduct "mergeCount" diff --git a/Documentation/SBV/Examples/TP/QuickSort.hs b/Documentation/SBV/Examples/TP/QuickSort.hs --- a/Documentation/SBV/Examples/TP/QuickSort.hs +++ b/Documentation/SBV/Examples/TP/QuickSort.hs @@ -680,7 +680,7 @@ =: x .: xs =: qed - -- A nice corrollary to the above is that if quicksort changes its input, that implies the input was not non-decreasing: + -- A nice corollary to the above is that if quicksort changes its input, that implies the input was not non-decreasing: _ <- lemma "ifChangedThenUnsorted" (\(Forall @"xs" xs) -> quickSort xs ./= xs .=> sNot (nonDecreasing xs)) [proofOf unchangedIfNondecreasing] diff --git a/Documentation/SBV/Examples/TP/RevAcc.hs b/Documentation/SBV/Examples/TP/RevAcc.hs --- a/Documentation/SBV/Examples/TP/RevAcc.hs +++ b/Documentation/SBV/Examples/TP/RevAcc.hs @@ -6,7 +6,7 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental -- --- Proves that the accummulating version of reverse is equivalent to the +-- Proves that the accumulating version of reverse is equivalent to the -- standard definition. ----------------------------------------------------------------------------- @@ -32,9 +32,9 @@ -- >>> :set -XTypeApplications #endif --- * Reversing with an accummulator. +-- * Reversing with an accumulator. --- | Accummulating reverse. +-- | Accumulating reverse. revAcc :: SymVal a => SList a -> SList a -> SList a revAcc = smtFunction "revAcc" $ \acc xs -> [sCase| xs of diff --git a/Documentation/SBV/Examples/Uninterpreted/Sort.hs b/Documentation/SBV/Examples/Uninterpreted/Sort.hs --- a/Documentation/SBV/Examples/Uninterpreted/Sort.hs +++ b/Documentation/SBV/Examples/Uninterpreted/Sort.hs @@ -21,7 +21,7 @@ -- in the backend SMT solver. data Q --- | Make 'Q' an uinterpreted sort. This will automatically introduce the +-- | Make 'Q' an uninterpreted sort. This will automatically introduce the -- type 'SQ' into our environment, which is the symbolic version of the -- carrier type 'Q'. mkSymbolic [''Q] diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Append.hs b/Documentation/SBV/Examples/WeakestPreconditions/Append.hs --- a/Documentation/SBV/Examples/WeakestPreconditions/Append.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Append.hs @@ -37,7 +37,7 @@ -- * Program state --- | The state of the length program, paramaterized over the element type @a@ +-- | The state of the length program, parameterized over the element type @a@ data AppS a = AppS { xs :: a -- ^ The first input list , ys :: a -- ^ The second input list , ts :: a -- ^ Temporary variable diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs --- a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs @@ -39,7 +39,7 @@ -- * Program state --- | The state for the sum program, parameterized over a base type @a@. +-- | The state for the fibonacci program, parameterized over a base type @a@. data FibS a = FibS { n :: a -- ^ The input value , i :: a -- ^ Loop counter , k :: a -- ^ tracks @fib (i+1)@ diff --git a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs --- a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs @@ -45,7 +45,7 @@ -- * Program state --- | The state for the sum program, parameterized over a base type @a@. +-- | The state for the GCD program, parameterized over a base type @a@. data GCDS a = GCDS { x :: a -- ^ First value , y :: a -- ^ Second value , i :: a -- ^ Copy of x to be modified diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Length.hs b/Documentation/SBV/Examples/WeakestPreconditions/Length.hs --- a/Documentation/SBV/Examples/WeakestPreconditions/Length.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Length.hs @@ -31,7 +31,7 @@ -- * Program state --- | The state of the length program, paramaterized over the element type @a@ +-- | The state of the length program, parameterized over the element type @a@ data LenS a b = LenS { xs :: a -- ^ The input list , ys :: a -- ^ Copy of input , l :: b -- ^ Running length diff --git a/SBVTestSuite/GoldFiles/adt_gen00.gold b/SBVTestSuite/GoldFiles/adt_gen00.gold --- a/SBVTestSuite/GoldFiles/adt_gen00.gold +++ b/SBVTestSuite/GoldFiles/adt_gen00.gold @@ -267,11 +267,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (Let "m" - (Add (Val 1) (Mul (Val (- 2)) (Val 0))) - (Let "k" (Val 11) (Add (Add (Val (- 1)) (Val 2)) (Var "k")))))) +[RECV] ((s0 (Let "l" + (Val 6) + (Let "a" (Val 0) (Add (Mul (Val 3) (Let "p" (Val 4) (Var "p"))) (Var "a")))))) -Got: (let m = (1 + (-2 * 0)) in (let k = 11 in ((-1 + 2) + k))) +Got: (let l = 6 in (let a = 0 in ((3 * (let p = 4 in p)) + a))) DONE *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/adt_pgen00.gold b/SBVTestSuite/GoldFiles/adt_pgen00.gold --- a/SBVTestSuite/GoldFiles/adt_pgen00.gold +++ b/SBVTestSuite/GoldFiles/adt_pgen00.gold @@ -267,11 +267,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (Let "l" - (Let "n" (Val (- 1)) (Mul (Val (- 2)) (Add (Var "n") (Var "n")))) - (Let "d" (Val 4) (Add (Add (Var "d") (Var "d")) (Var "d")))))) +[RECV] ((s0 (Let "t" + (Val 4) + (Let "l" (Val 7) (Add (Val (- 28281)) (Let "x" (Val 28293) (Var "x"))))))) -Got: (let l = (let n = -1 in (-2 * (n + n))) in (let d = 4 in ((d + d) + d))) +Got: (let t = 4 in (let l = 7 in (-28281 + (let x = 28293 in x)))) DONE *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/doctest_sanity.gold b/SBVTestSuite/GoldFiles/doctest_sanity.gold --- a/SBVTestSuite/GoldFiles/doctest_sanity.gold +++ b/SBVTestSuite/GoldFiles/doctest_sanity.gold @@ -1,3 +1,3 @@ -Total: 1226; Tried: 1226; Skipped: 0; Success: 1226; Errors: 0; Failures 0 -Examples: 1079; Tried: 1079; Skipped: 0; Success: 1079; Errors: 0; Failures 0 -Setup: 147; Tried: 147; Skipped: 0; Success: 147; Errors: 0; Failures 0 +Total: 1238; Tried: 1238; Skipped: 0; Success: 1238; Errors: 0; Failures 0 +Examples: 1086; Tried: 1086; Skipped: 0; Success: 1086; Errors: 0; Failures 0 +Setup: 152; Tried: 152; Skipped: 0; Success: 152; Errors: 0; Failures 0 diff --git a/SBVTestSuite/GoldFiles/query_Strings1.gold b/SBVTestSuite/GoldFiles/query_Strings1.gold --- a/SBVTestSuite/GoldFiles/query_Strings1.gold +++ b/SBVTestSuite/GoldFiles/query_Strings1.gold @@ -16,7 +16,7 @@ [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- -[GOOD] (define-fun s1 () Bool (str.in_re s0 ((_ re.loop 5 5) (str.to.re "xyz")))) +[GOOD] (define-fun s1 () Bool (str.in_re s0 ((_ re.loop 5 5) (str.to_re "xyz")))) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- [GOOD] (assert s1) diff --git a/SBVTestSuite/GoldFiles/strExamples10.gold b/SBVTestSuite/GoldFiles/strExamples10.gold --- a/SBVTestSuite/GoldFiles/strExamples10.gold +++ b/SBVTestSuite/GoldFiles/strExamples10.gold @@ -17,7 +17,7 @@ [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- -[GOOD] (define-fun s1 () Bool (str.in_re s0 ((_ re.loop 1 3) (str.to.re "ab")))) +[GOOD] (define-fun s1 () Bool (str.in_re s0 ((_ re.loop 1 3) (str.to_re "ab")))) [GOOD] (define-fun s2 () Int (str.len s0)) [GOOD] (define-fun s4 () Bool (> s2 s3)) [GOOD] ; --- delayedEqualities --- diff --git a/SBVTestSuite/GoldFiles/strExamples9.gold b/SBVTestSuite/GoldFiles/strExamples9.gold --- a/SBVTestSuite/GoldFiles/strExamples9.gold +++ b/SBVTestSuite/GoldFiles/strExamples9.gold @@ -17,7 +17,7 @@ [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- -[GOOD] (define-fun s1 () Bool (str.in_re s0 ((_ re.loop 1 3) (str.to.re "ab")))) +[GOOD] (define-fun s1 () Bool (str.in_re s0 ((_ re.loop 1 3) (str.to_re "ab")))) [GOOD] (define-fun s2 () Int (str.len s0)) [GOOD] (define-fun s4 () Bool (= s2 s3)) [GOOD] ; --- delayedEqualities --- diff --git a/SBVTestSuite/TestSuite/Basics/Lambda.hs b/SBVTestSuite/TestSuite/Basics/Lambda.hs --- a/SBVTestSuite/TestSuite/Basics/Lambda.hs +++ b/SBVTestSuite/TestSuite/Basics/Lambda.hs @@ -76,7 +76,7 @@ , goldenCapturedIO "lambda12" $ eval1 [1 .. 3 :: Integer] (map singleton, P.map (: [])) , goldenCapturedIO "lambda13" $ eval1 [(x, y) | x <- [1..3], y <- [4..6 :: Integer]] - (map (\t -> t^._1 + t^._2), P.map (uncurry (+))) + (map (\t -> t^._1 + t^._2), P.map (P.uncurry (+))) , goldenCapturedIO "lambda14" $ eval1 [1 .. 5 :: Integer] (zipWithL (+) [sEnum|10..15|], P.zipWith (+) [10..15]) @@ -325,7 +325,7 @@ rel, leq :: Relation Integer rel = uninterpret "R" - leq = uncurry $ smtFunction "leq" (.<=) + leq = P.uncurry $ smtFunction "leq" (.<=) po = isPartialOrder "poR" rel poI = isPartialOrder "poI" leq diff --git a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr --- a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr @@ -15,8 +15,8 @@ (isLet e ==> (e .== e =: qed))] PCase17.hs:18:14: error: [GHC-83865] " Couldn't match expected type: Proof SBool - with actual type: sbv-14.3:Data.SBV.TP.TP.TPProofGen - (SBV Bool) [sbv-14.3:Data.SBV.TP.TP.Helper] () + with actual type: sbv-14.4:Data.SBV.TP.TP.TPProofGen + (SBV Bool) [sbv-14.4:Data.SBV.TP.TP.Helper] () " In the expression: cases [(isZero e ==> (e .== e =: qed)), (isNum e ==> (e .== e =: qed)), diff --git a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr --- a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr @@ -15,8 +15,8 @@ (isLet e ==> undefined)] PCase38.hs:12:14: error: [GHC-83865] " Couldn't match expected type: Proof SBool - with actual type: sbv-14.3:Data.SBV.TP.TP.TPProofGen - a0 [sbv-14.3:Data.SBV.TP.TP.Helper] () + with actual type: sbv-14.4:Data.SBV.TP.TP.TPProofGen + a0 [sbv-14.4:Data.SBV.TP.TP.Helper] () " In the expression: cases [(isZero e ==> undefined), (isNum e ==> undefined), diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr @@ -28,4 +28,4 @@ ((\ _ -> 1) (Data.SBV.Maybe.getJust_1 m)) (ite (Data.SBV.Maybe.isNothing m) 0 - (symWithKind "unmatched_sCase_Maybe_6989586621679035004"))) + (symWithKind "unmatched_sCase_Maybe_6989586621679035008"))) diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr @@ -24,4 +24,4 @@ ((\ _ -> Data.SBV.Either.isRight (Data.SBV.Maybe.getJust_1 m)) (Data.SBV.Maybe.getJust_1 m))) ((\ _ -> 1) (Data.SBV.Maybe.getJust_1 m)) - (symWithKind "unmatched_sCase_Maybe_6989586621679035004"))) + (symWithKind "unmatched_sCase_Maybe_6989586621679035008"))) diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr @@ -30,4 +30,4 @@ (ite (Data.SBV.Either.isRight e) ((\ _ -> 1) (Data.SBV.Either.getRight_1 e)) - (symWithKind "unmatched_sCase_Either_6989586621679034966"))) + (symWithKind "unmatched_sCase_Either_6989586621679034970"))) diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr @@ -40,4 +40,4 @@ (isVar e) ((\ _ -> 1) (getVar_1 e)) (ite (isLet e) ((\ _ _ _ -> 3) (getLet_1 e) (getLet_2 e) (getLet_3 e)) - (symWithKind "unmatched_sCase_Expr_6989586621679081499")))))) + (symWithKind "unmatched_sCase_Expr_6989586621679080570")))))) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 14.3 +Version : 14.4 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT @@ -155,6 +155,7 @@ Exposed-modules : Documentation.SBV.Examples.ADT.Expr , Documentation.SBV.Examples.ADT.Param , Documentation.SBV.Examples.ADT.Types + , Documentation.SBV.Examples.BitPrecise.Adders , Documentation.SBV.Examples.BitPrecise.BitTricks , Documentation.SBV.Examples.BitPrecise.BrokenSearch , Documentation.SBV.Examples.BitPrecise.Legato @@ -246,6 +247,7 @@ , Documentation.SBV.Examples.Strings.RegexCrossword , Documentation.SBV.Examples.Strings.SQLInjection , Documentation.SBV.Examples.TP.Ackermann + , Documentation.SBV.Examples.TP.Adder , Documentation.SBV.Examples.TP.Basics , Documentation.SBV.Examples.TP.BinarySearch , Documentation.SBV.Examples.TP.CaseSplit