h,'$4      !"#$%&'()*+,-./01239.10.1 (c) Levent ErkokBSD3erkokl@gmail.com experimental Safe-Inferred8,Importable type as an annotation alternativeThe actual annotation.Plugin options. Note that we allow picking multiple solvers, which will all be run in parallel. You can pick and choose any number of them, or if you want to run all available solvers, then use the option . The default behavior is to error-out on failure, using the default-SMT solver picked by SBV, which is currently Z3.Continue even if proof failsSkip the proof. Can be handy for properties that we currently do not want to focus on.*Produce verbose output, good for debuggingProduce really verbose output, use only when things go really wrong! Perform quickCheck +Uninterpret this binding for proof purposes 9Use these names for the arguments; need not be exhaustive If a list-input is found, use this length. If not specified, we will complain! Use Z3 Use Yices Use BoolectorUse CVC4 Use MathSATUse ABCRun all installed solvers in parallel, and report the result from the first to finish-A property annotation, using default options.)Synonym for sbv really, just looks cooler       (c) Levent ErkokBSD3erkokl@gmail.com experimentalNone 4+The values kept track of by the interpreter5The kinds used by the plugin6'Configuration info as we run the plugin7The interpreter monad8Interpreter environment9Symbolic equality over values?"Symbolic if-then-else over values.@Compute the span given a Tick. Returns the old-span if the tick span useless.ACompute the span for a binding.BPick the first "good" span, hopefully corresponding to the closest location to where we are in the code when we issue an error message.C%Show a GHC span in user-friendly formDThis comes mighty handy! Wonder why GHC doesn't have it already:EOutputable instance for S.KindF)Make a rudimentary Ord instance for TCKeyG(Make a rudimentary Eq instance for TCKeyHOutputable instance for SKindIOutputable instance for Val2>?=Lift a two argument SBV function to our the plugin value spaceLifting an equality is special; since it acts uniformly over tuples.Lifting enumFromTo: [x .. y]$Lifting sEnumFromThenTo: [x, y .. z]Implement [x .. y] or [x, y .. z]; provided the inputs are concreteyv{uz(c) Levent ErkokBSD3erkokl@gmail.com experimental Safe-InferredN5Merging two given sorted lists, preserving the order.!Simple merge-sort implementation.1Check whether a given sequence is non-decreasing.Check whether two given sequences are permutations. We simply check that each sequence is a subset of the other, when considered as a set. The check is slightly complicated for the need to account for possibly duplicated elements.Asserting correctness of merge-sort for a list of the given size. Note that we can only check correctness for fixed-size lists. Also, the proof will get more and more complicated for the backend SMT solver as n" increases. Here we try it with 4.We have:  [SBV] tests/T48.hs:100:1-16 Proving "mergeSortCorrect", using Z3. [Z3] Q.E.D.  (c) Levent ErkokBSD3erkokl@gmail.com experimentalNone' Entry point to the plugin (c) Levent ErkokBSD3erkokl@gmail.com experimentalNone          (c) Nickolas FotopoulosBSD3nickolas.fotopoulos@gmail.com experimentalNoneOA top-level binding with its type wrapped in Proved causes sbvPlugin to run a proof on the expression.)Simple booleans can be made theorems too.(c) Levent ErkokBSD3erkokl@gmail.com experimentalNone~!The range detector must output if the range is larger than this amount."The range detector must have sent an output before this many cycles have past.#+Given a last-signal-time calculator, named  calculate, check that it satisfies the following three requirements: We must've just sent a signal if:minRate9: The last-time we sent is strictly less than the " amountminRange=: We must've just sent a signal if the range is beyond !manualOverride: We must've just sent a signal if the manual-override is specified$A "bad" implementation, see if you can spot the problem with it, before looking at the failed theorem below!%Using SBV, prove that the $ is indeed a bad implementation. Here's the output we get from the plugin:  [SBV] MicroController.hs:85:1-8 Proving "checkBad", using Z3. [Z3] Falsifiable. Counter-example: range = 200 :: Int64 manual = False :: Bool timeSince = 9 :: Int64 We're being told that if the range is 200, and manual override is off, and time-since last is 9, then our "calculator" returns 10. But that violates the minRate) requirement, since we never want to go "! cycles without sending a signal!&A "good" implementation, properly handling the off-by-one error of the original.'=We now verify that the good variant is indeed good. We have:  [SBV] MicroController.hs:108:1-9 Proving "checkGood", using Z3. [Z3] Q.E.D. %'#$&"!!"#$%&'(c) Levent ErkokBSD3erkokl@gmail.com experimentalNone o(Compute the maximum of three integers, which is intuitively correct for unbounded values, but not for bounded bit-vectors.)Show that this function fails to compute maximum correctly. We have: [SBV] a.hs:11:1-7 Proving "correct", using Z3. [Z3] Falsifiable. Counter-example: x = -2816883406898309583 :: Int64 y = -2816883406898309583 :: Int64 z = 6694719001794338309 :: Int64 )(()(c) Levent ErkokBSD3erkokl@gmail.com experimentalNone$ *SBVPlugin can only see definitions in the current module. So we define * ourselves. Also, it has to be monomoprhized, as the plugin isn't smart enough to deal with polymorphic functions out-of-the-box.+Returns 1 if bool is True, Formalizes https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax- Formalizes https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax. Formalizes https://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns/ Formalizes https://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching0 Formalizes https://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf21 Formalizes https://graphics.stanford.edu/~seander/bithacks.html#MaskedMerge2 Formalizes https://graphics.stanford.edu/~seander/bithacks.html#RoundUpPowerOf23 Formalizes ?https://graphics.stanford.edu/~seander/bithacks.html#ZeroInWord /*-,1+.023 *+,-./0123  !"#$%&'()*+, -./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVCCWCXCYCZEE[E\E]E^E_E`EaEbEcEdEeEfEgEhijklGGmGnGoFpqrst u v w x y z { | } ~                     sbvPlugin-9.10.1-inplaceData.SBV.Plugin.Data"Data.SBV.Plugin.Examples.MergeSortData.SBV.Plugin(Data.SBV.Plugin.Examples.MicroController Data.SBV.Plugin.Examples.Maximum"Data.SBV.Plugin.Examples.BitTricks sbvPluginData.SBV.Plugin.CommonData.SBV.Plugin.AnalyzeData.SBV.Plugin.EnvData.SBV.Plugin.PluginData.SBV.Plugin.Examples.ProvedProved SBVAnnotationSBVoptions SBVOption IgnoreFailureSkipVerboseDebug QuickCheck UninterpretNamesListSizeZ3Yices BoolectorCVC4MathSATABC AnySolversbvtheorem$fEqSBVAnnotation$fDataSBVAnnotation$fShowSBVOption $fEqSBVOption$fDataSBVOptionmerge mergeSort nonDecreasingisPermutationOfmergeSortCorrectpluginsafetyDistance maxTimeSince checkSpeccomputeLastBadcheckBadcomputeLastGood checkGoodmyMaxcorrectelemoneIffastMinCorrectfastMaxCorrectoppositeSignsCorrectconditionalSetClearCorrectpowerOfTwoCorrectmaskedMergeCorrectroundPowerOfTwoCorrect zeroInWordValSKindConfigEvalEnvTCKeySpecials tcKeyToUList pickSolvers liftEqValeqValiteValtickSpanvarSpanpickSpanshowSpan $fShowExpr$fOutputableKind $fOrdTCKey $fEqTCKey$fOutputableSKind$fOutputableValcfgEnvisGHCiopts sbvAnnotationbailOutcoreMapcurLocdestMapenvMapflags machWordSize mbListSizerUITypesrUninterpreted rUsedNamesspecialstcMap uninterestingKBaseKFunKLstKTup isEqualityisListisTupleBaseFuncLstTupTyp analyzeBindprovesafelyproveItisReallyADictionaryunScale uninterpretgetTypesupportTupleSizes buildTCEnv buildFunEnv basicFuncssymFuncs buildDestsuninterestingTypes buildSpecials tlift2Booltlift1tlift2 tlift2ShRot tEnumFromTotEnumFromThenTolift1Intlift1lift2liftEq sEnumFromTosEnumFromThenToenumListintegerAssociativeisTrue