h&+(4      !"#$%&'()*+,-./0123 (c) Levent ErkokBSD3erkokl@gmail.com experimental Safe-Inferred5 sbvPlugin,Importable type as an annotation alternative sbvPluginThe actual annotation. sbvPluginPlugin 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. sbvPluginContinue even if proof fails sbvPluginSkip the proof. Can be handy for properties that we currently do not want to focus on. sbvPlugin*Produce verbose output, good for debugging sbvPluginProduce really verbose output, use only when things go really wrong!  sbvPluginPerform quickCheck  sbvPlugin+Uninterpret this binding for proof purposes  sbvPlugin9Use these names for the arguments; need not be exhaustive  sbvPluginIf a list-input is found, use this length. If not specified, we will complain!  sbvPluginUse Z3 sbvPlugin Use Yices sbvPlugin Use Boolector sbvPluginUse CVC4 sbvPlugin Use MathSAT sbvPluginUse ABC sbvPluginRun all installed solvers in parallel, and report the result from the first to finish sbvPlugin-A property annotation, using default options. sbvPlugin)Synonym for sbv really, just looks cooler    (c) Levent ErkokBSD3erkokl@gmail.com experimental Safe-Inferred R4 sbvPlugin+The values kept track of by the interpreter5 sbvPluginThe kinds used by the plugin6 sbvPlugin'Configuration info as we run the plugin7 sbvPluginThe interpreter monad8 sbvPluginInterpreter environment9 sbvPlugin sbvPluginSymbolic equality over values? sbvPlugin"Symbolic if-then-else over values.@ sbvPluginCompute the span given a Tick. Returns the old-span if the tick span useless.A sbvPluginCompute the span for a binding.B sbvPluginPick the first "good" span, hopefully corresponding to the closest location to where we are in the code when we issue an error message.C sbvPlugin%Show a GHC span in user-friendly formD sbvPluginThis comes mighty handy! Wonder why GHC doesn't have it already:E sbvPluginOutputable instance for S.KindF sbvPlugin)Make a rudimentary Ord instance for TCKeyG sbvPlugin(Make a rudimentary Eq instance for TCKeyH sbvPluginOutputable instance for SKindI sbvPluginOutputable instance for Val24JKLMN5OPQR6STUVW78XYZ[\]^_`abcdef9g:hijk;<=>?@ABC(c) Levent ErkokBSD3erkokl@gmail.com experimental Safe-Inferred&fl sbvPlugin#Dispatch the analyzer over bindingsm sbvPluginProve an SBVTheoremn sbvPluginSafely execute an action, catching the exceptions, printing and returning False if something goes wrongo sbvPluginReturns True if proof went thrup sbvPluginIs this really a dictionary in disguise? This is a terrible hack, and the ice is thin here. But it seems to work. TODO: Figure out if there's a better way of doing this. Note that this function really does get applications, when those dictionaries are parameterized by others. Think of the case where "Eq [a]" dictionary depends on "Eq a", for instance. In these cases, GHC to produces applications.q sbvPluginUnscale a value. We don't really care about the scale itself, so far as SBV is concernedr sbvPluginUninterpret an expressions sbvPluginConvert a Core type to an SBV Type, retaining functions and tuplesl (c) Levent ErkokBSD3erkokl@gmail.com experimental Safe-Inferred& t sbvPluginWhat tuple-sizes we support? We go upto 15, but would be easy to change if necessaryu sbvPlugin.Build the initial environment containing typesv sbvPlugin2Build the initial environment containing functionsw sbvPlugin#Basic conversions, only on one kindx sbvPlugin?Symbolic functions supported by the plugin; those from a class.y sbvPlugin Destructorsz sbvPluginThese types show up during uninterpretation, but are not really "interesting" as they are singly inhabited.{ sbvPluginCertain things are just too special, as they uniformly apply to uninterpreted types.| sbvPlugin$Lift a binary type, with result bool} sbvPluginLift a unary type~ sbvPluginLift a binary type sbvPlugin0Lift a binary type, where second argument is Int sbvPluginType of enumFromTo: [x .. y] sbvPlugin Type of enumFromThenTo: [x .. y] sbvPlugin/Lift a unary SBV function that via kind/integer sbvPlugin3Lift a unary SBV function to the plugin value space sbvPlugin>Lift a two argument SBV function to our the plugin value space sbvPluginLifting an equality is special; since it acts uniformly over tuples. sbvPluginLifting enumFromTo: [x .. y] sbvPlugin$Lifting sEnumFromThenTo: [x, y .. z] sbvPluginImplement [x .. y] or [x, y .. z]; provided the inputs are concreteuvyz{ (c) Levent ErkokBSD3erkokl@gmail.com experimental Safe-Inferred& sbvPluginEntry point to the plugin(c) Levent ErkokBSD3erkokl@gmail.com experimental Safe-Inferred     (c) Nickolas FotopoulosBSD3nickolas.fotopoulos@gmail.com experimental Safe-InferredV sbvPluginA top-level binding with its type wrapped in Proved causes sbvPlugin to run a proof on the expression. sbvPlugin)Simple booleans can be made theorems too.(c) Levent ErkokBSD3erkokl@gmail.com experimental Safe-Inferred sbvPluginThe range detector must output if the range is larger than this amount. sbvPluginThe range detector must have sent an output before this many cycles have past. sbvPlugin+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 sbvPluginA "bad" implementation, see if you can spot the problem with it, before looking at the failed theorem below!  sbvPluginUsing 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 = 0 :: Int64 manual = False :: Bool timeSince = 9 :: Int64 We're being told that if the range is 0, 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!! sbvPluginA "good" implementation, properly handling the off-by-one error of the original." sbvPlugin=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 experimental Safe-Inferred"b# sbvPlugin5Merging two given sorted lists, preserving the order.$ sbvPlugin!Simple merge-sort implementation.% sbvPlugin1Check whether a given sequence is non-decreasing.& sbvPluginCheck 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.' sbvPluginAsserting 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 experimental Safe-Inferred$m( sbvPluginCompute the maximum of three integers, which is intuitively correct for unbounded values, but not for bounded bit-vectors.) sbvPluginShow 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 experimental Safe-Inferred( * sbvPluginSBVPlugin can only see definitions in the current module. So we define * ourselves.+ sbvPluginReturns 1 if bool is True, sbvPlugin Formalizes https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax- sbvPlugin Formalizes https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax. sbvPlugin Formalizes https://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns/ sbvPlugin Formalizes https://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching0 sbvPlugin Formalizes https://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf21 sbvPlugin Formalizes https://graphics.stanford.edu/~seander/bithacks.html#MaskedMerge2 sbvPlugin Formalizes https://graphics.stanford.edu/~seander/bithacks.html#RoundUpPowerOf23 sbvPlugin Formalizes ?https://graphics.stanford.edu/~seander/bithacks.html#ZeroInWord *+,-./0123 *+,-./0123   !"#$%& '()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abBcdefghijklmnopDEqrsFtuvwxyz{ | } ~                    sbvPlugin-9.2.2-inplaceData.SBV.Plugin.DataData.SBV.Plugin(Data.SBV.Plugin.Examples.MicroController"Data.SBV.Plugin.Examples.MergeSort Data.SBV.Plugin.Examples.Maximum"Data.SBV.Plugin.Examples.BitTricksData.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$fDataSBVOptionpluginsafetyDistance maxTimeSince checkSpeccomputeLastBadcheckBadcomputeLastGood checkGoodmerge mergeSort nonDecreasingisPermutationOfmergeSortCorrectmyMaxcorrectelemoneIffastMinCorrectfastMaxCorrectoppositeSignsCorrectconditionalSetClearCorrectpowerOfTwoCorrectmaskedMergeCorrectroundPowerOfTwoCorrect zeroInWordValSKindConfigEvalEnvTCKeySpecials tcKeyToUList pickSolvers liftEqValeqValiteValtickSpanvarSpanpickSpanshowSpan $fShowExpr$fOutputableKind $fOrdTCKey $fEqTCKey$fOutputableSKind$fOutputableValFuncLstTupTypBaseKFunKLstKTupKBasecfgEnv sbvAnnotationoptsisGHCibailOutcoreMapdestMapenvMaptcMapspecialsrUITypes rUsedNamesrUninterpreted uninteresting mbListSize machWordSizecurLocflagsisListisTuple isEquality analyzeBindprovesafelyproveItisReallyADictionaryunScale uninterpretgetTypesupportTupleSizes buildTCEnv buildFunEnv basicFuncssymFuncs buildDestsuninterestingTypes buildSpecials tlift2Booltlift1tlift2 tlift2ShRot tEnumFromTotEnumFromThenTolift1Intlift1lift2liftEq sEnumFromTosEnumFromThenToenumListintegerAssociativeisTrue