RE      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz { | } ~                                                               !"#$%&'()*+,-./0123456789:;<=>?@ABCD5 experimentalerkokl@gmail.com Safe-InferedE"If selected, runs the computation m, and prints the time it took 5 to run it. The return type should be an instance of F to ensure & the correct elapsed time is printed. EEE experimentalerkokl@gmail.com Safe-InferedGMonadic lift over 2-tuples HMonadic lift over 3-tuples IMonadic lift over 4-tuples JMonadic lift over 5-tuples KMonadic lift over 6-tuples LMonadic lift over 7-tuples MMonadic lift over 8-tuples GHIJKLMGHIJKLMGHIJKLM  experimentalerkokl@gmail.com Safe-InferedThe # class: a generalization of Haskell's N type  Haskell N and SBV's SBoolH are instances of this class, unifying the treatment of boolean values. Minimal complete definition: , ,   However, it's advisable to define , and # as well (typically), for clarity.  logical true logical false  complement and or nand nor xor implies  equivalence cast from Bool Generalization of O Generalization of P Generalization of Q Generalization of R  S   S! experimentalerkokl@gmail.com Safe-InferedMAlgebraic reals. Note that the representation is left abstract. We represent M rational results explicitly, while the roots-of-polynomials are represented ' implicitly by their defining equation TdConstruct a poly-root real with a given approximate value (either as a decimal, or polynomial-root) U Render an B as an SMTLib2 value. Only supports rationals for the time being. V Render an N as a Haskell value. Only supports rationals, since there is no corresponding F standard Haskell type that can represent root-of-polynomial variety. WCMerge the representation of two algebraic reals, one assumed to be E in polynomial form, the other in decimal. Arguments can be the same G kind, so long as they are both rationals and equivalent; if not there  must be one that is precise. It's an error to pass anything X else to this function! (Used in reconstructing SMT counter-example values with reals). XYTUVWZ[\]^_`aXYTUVW YXTUVWZ[\]^_`a" experimentalerkokl@gmail.comNonejbVRepresentation of an SMT-Lib program. In between pre and post goes the refuted models cWRepresentation of SMTLib Program versions, currently we only know of versions 1 and 2. 0 (NB. Eventually, we should just drop SMTLib1.) +Arrays implemented internally as functions = Internally handled by the library and not mapped to SMT-Lib N Reading an uninitialized value is considered an error (will throw exception) A Cannot check for equality (internally represented as functions)  Can quick-check > Typically faster as it gets compiled away during translation +Arrays implemented in terms of SMT-arrays:  8http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2 ! Maps directly to SMT-lib arrays M Reading from an unintialized value is OK and yields an uninterpreted result ( Can check for equality of these arrays # Cannot quick-check theorems using SArray values K Typically slower as it heavily relies on SMT-solving for the array theory Flat arrays of symbolic values  An  array a b! is an array indexed by the type < a, with elements of type < b ( If an initial value is not provided in  and  methods, then the elements ] are left unspecified, i.e., the solver is free to choose any value. This is the right thing M to do if arrays are used as inputs to functions to be verified, typically. While it'5s certainly possible for user to create instances of , the   and 8 instances already provided should cover most use cases _ in practice. (There are some differences between these models, however, see the corresponding  declaration.) DMinimal complete definition: All methods are required, no defaults. 3Create a new array, with an optional initial value 9Create a named new array, with an optional initial value Read the array element at a 1Reset all the elements of the array to the value b Update the element at a to be b 1Merge two given arrays on the symbolic condition  Intuitively: ,mergeArrays cond a b = if cond then a else b. < Merging pushes the if-then-else choice down on to elements A D is a potential symbolic bitvector that can be created instances of S to be fed to a symbolic program. Note that these methods are typically not needed  in casual uses with prove, sat, allSat) etc, as default instances automatically  provide the necessary bits. &Create a user named input (universal) $Create an automatically named input Get a bunch of new words Create an existential variable 3Create an automatically named existential variable Create a bunch of existentials !ACreate a free variable, universal in a proof, existential in sat "HCreate an unnamed free variable, universal in proof, existential in sat #Create a bunch of free vars $-Similar to free; Just a more convenient name %JSimilar to mkFreeVars; but automatically gives names based on the strings &$Turn a literal constant to symbolic ',Extract a literal, if the value is concrete (,Extract a literal, from a CW representation )Is the symbolic word concrete? *&Is the symbolic word really symbolic? +0Does it concretely satisfy the given predicate? ,max/)minbounds, if available. Note that we don't want  to impose Bounded< on our class as Integer is not Bounded but it is a SymWord -max/)minbounds, if available. Note that we don't want  to impose Bounded< on our class as Integer is not Bounded but it is a SymWord .One stop allocator dGA class representing what can be returned from a symbolic computation. /PMark an interim result as an output. Useful when constructing Symbolic programs O that return multiple values, or when the result is programmatically computed. 0CA Symbolic computation. Represented by a reader monad carrying the D state of the computation, layered on top of IO for creating unique / references to hold onto intermediate results. 11Infinite precision symbolic algebraic real value 2)Infinite precision signed symbolic value 364-bit signed symbolic value, 2's complement representation 432-bit signed symbolic value, 2's complement representation 516-bit signed symbolic value, 2's complement representation 68-bit signed symbolic value, 2's complement representation 764-bit unsigned symbolic value 832-bit unsigned symbolic value 916-bit unsigned symbolic value :8-bit unsigned symbolic value ;A symbolic boolean/bit <The Symbolic value. Either a constant (Left) or a symbolic  value ( Right Cached-). Note that caching is essential for making * sure sharing is preserved. The parameter a is phantom, but is C extremely important in keeping the user interface strongly typed. e&The state of the symbolic interpreter >4Different means of running a symbolic piece of code ?TConcrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs @Code generation mode A@Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance f#Representation for symbolic arrays g+The context of a symbolic array as created h:An array created by symbolically merging two other arrays i;An array created by mutating another array at a given cell jLAn array created from another array by fixing each element to another value k6A new array, with potential initializer for each cell B)Result of running a symbolic computation ll: pairs array names and uninterpreted constants with their kinds * used mainly for printing counterexamples mm$ pairs symbolic words and user given/automatically generated names n'A program is a sequence of assignments CNA class for capturing values that have a sign and a size (finite or infinite) N minimal complete definition: kindOf. This class can be automatically derived  for data-types that have a o5 instance; this is useful for creating uninterpreted  sorts. pA symbolic expression qSymbolic operations rMA simple type for SBV computations, used mainly for uninterpreted constants.  We keep track of the signedness/+size of the arguments. A non-function will " have just one entry in the list. s2Quantifiers: forall or exists. Note that we allow  arbitrary nestings. tA symbolic word, tracking it's signedness and size. uA symbolic node id LKind of symbolic value QQ- represents a concrete word of a fixed size: * Endianness is mostly irrelevant (see the FromBits class). L For signed words, the most significant digit is considered to be the sign. vA constant value wvalue of an uninterpreted kind x bit-vector/unbounded integer yalgebraic real z Are two CW's of the same type? {Is this a bit? UEConvert a CW to a Haskell boolean (NB. Assumes input is well-kinded) |'Are there any existential quantifiers? }FConstant False as a SW. Note that this value always occupies slot -2. ~FConstant False as a SW. Note that this value always occupies slot -1. CConstant False as a CW. We represent it using the integer value 0. BConstant True as a CW. We represent it using the integer value 1. $Lift a binary function through a CW "Map a unary function through a CW #Map a binary function through a CW &Extract the constraints from a result 6Extract the traced-values from a result (quick-check) EConvert an SBV-type to the kind-of uninterpreted value it represents MConvert an array value type to the kind-of uninterpreted value it represents Are we running in proof mode? ACreate a new uninterpreted symbol, possibly with user given code +Create a new table; hash-cons as necessary VCreate a constant word 0Create a new expression; hash-cons as necessary ,Convert a symbolic value to a symbolic-word pCreate a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that. S If not, then we pick existential for SAT calls and universal for everything else. =Convert a symbolic value to an SW, inside the Symbolic monad WWAdd a user specified axiom to the generated SMT-Lib file. The first argument is a mere a string, use for commenting purposes. The second argument is intended to hold the multiple-lines a of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom  itself, to see whether it'4s actually well-formed or is sensical by any means. @ A separate formalization of SMT-Lib would be very useful here. X6Run a symbolic computation in Proof mode and return a B. The boolean 6 argument indicates if this is a sat instance or not. YHRun a symbolic computation, and return a extra value paired up with the B ZZLift a function to an array. Useful for creating arrays in a pure context. (Otherwise use .) *Add a constraint with a given probability  Cache a state-based computation (Uncache a previously cached computation "Uncache, retrieving array indexes bc !"#$%&'()*+,-.d/0123456789:;<=e>?@AfghijkBlmnCDEFGHIJKpqrstuLMNOPQRSTvwxyz{U|}~VWXYZbc !"#$%&'()*+,-.d/0123456789:;<=e>?@AfghijkBlmnCDEFGHIJKpqrstuLMNOPQRSTvwxyz{U|}~VWXYZybc !"#$%&'()*+,-.d/0123456789:;<=e>A@?fgkjihBlmnCDEFGHIJKpqrstuLPONMQRSTvyxwz{U|}~VWXYZ# experimentalerkokl@gmail.comNone)[Different kinds of files) we can produce. Currently this is quite C specific. `6Representation of a collection of generated programs. bPossible mappings for the 10 type when translated to C. Used in conjunction  with the function i2. Note that the particular characteristics of the W mapped types depend on the platform and the compiler used for compiling the generated  C program. See  )http://en.wikipedia.org/wiki/C_data_types for details. c  long doubled doublee floatfEThe code-generation monad. Allows for precise layout of input values O reference parameters (for returning composite values in languages such as C),  and return values. Code-generation state &Abstraction of target language values Options for code-generation. If S, perform run-time-checks for index-out-of-bounds or shifting-by-large values etc. 3Bit-size to use for representing SInteger (if any) ,Type to use for representing SReal (if any) ZValues to use for the driver program generated, useful for generating non-random drivers. If !, will generate a driver program If , will generate a makefile 6Abstract over code generation for different languages vDefault options for code generation. The run-time checks are turned-off, and the driver values are completely random. *Initial configuration for code-generation /Reach into symbolic monad from code-generation KReach into symbolic monad and output a value. Returns the corresponding SW gRSets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: . h4Sets number of bits to be used for representing the 2 type in the generated C code.  The argument must be one of 8, 16, 32, or 64*. Note that this is essentially unsafe as _ the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as $ typical in most C implementations. i0Sets the C type to be used for representing the 1 type in the generated C code.  The setting can be one of C's float, double, or  long double, types, depending S on the precision needed. Note that this is essentially unsafe as the semantics of ] infinite precision SReal values becomes reduced to the corresponding floating point type in 0 C, and hence it is subject to rounding errors. j.Should we generate a driver program? Default: ,. When a library is generated, it will have @ a driver if any of the contituent functions has a driver. (See  compileToCLib.) k(Should we generate a Makefile? Default: . lSets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values. mpAdds the given lines to the header file generated, useful for generating programs with uninterpreted functions. nqAdds the given lines to the program file generated, useful for generating programs with uninterpreted functions. okAdds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in. p/Creates an atomic input in the generated code. q.Creates an array input in the generated code. r0Creates an atomic output in the generated code. s/Creates an array output in the generated code. t:Creates a returned (unnamed) value in the generated code. u@Creates a returned (unnamed) array value in the generated code. Is this a driver program? Is this a make file? TGenerate code for a symbolic program, returning a Code-gen bundle, i.e., collection * of makefiles, source code, headers, etc. 5Render a code-gen bundle to a directory or to stdout An alternative to Pretty's render, which might have leading* white-space in empty lines. This version  eliminates such whitespace. >[\]^_`abcdef     ghijklmnopqrstu<[\]^_`abcdef     ghijklmnopqrstu"[_^]\`abedcf     ghijklmnopqrstu$ experimentalerkokl@gmail.com Safe-InferedvGeneralized version of w#, allowing the user to specify the L warm-up count and the convergence factor. Maximum iteration count can also - be specified, at which point convergence won'-t be sought. The boolean controls verbosity. w@Given a symbolic computation that produces a value, compute the A expected value that value would take if this computation is run A with its free variables drawn from uniform distributions of its B respective values, satisfying the given constraints specified by   constrain and  pConstrain& calls. This is equivalent to calling  v, the following parameters: verbose, warm-up  round count of 10000', no maximum iteration count, and with  convergence margin 0.0001. vwvwvw% experimentalerkokl@gmail.com Safe-InferedAdd constraints to generate new> models. This function is used to query the SMT-solver, while  disallowing a previous model. +Translate a problem into an SMTLib1 script has infinite precision integers/reals is this a sat problem? extra comments to place on top uninterpreted sorts inputs !skolemized version of the inputs  constants auto-generated tables user specified arrays uninterpreted functions/ constants user given axioms  assignments extra constraints output variable & experimentalerkokl@gmail.com Safe-Infered2xDUninterpreted constants and functions. An uninterpreted constant is K a value that is indexed by its name. The only property the prover assumes K about these values are that they are equivalent to themselves; i.e., (for I functions) they return the same results when applied to same arguments. C We support uninterpreted-functions as a general means of black-box'ing  operations that are  irrelevant+ for the purposes of the proof; i.e., when N the proofs can be performed without any knowledge about the function itself. Minimal complete definition: {. However, most instances in T practice are already provided by SBV, so end-users should not need to define their  own instances. yTUninterpret a value, receiving an object that can be used instead. Use this version 8 when you do not need to add an axiom about this value. zMUninterpret a value, only for the purposes of code-generation. For execution N and verification the value is used as is. For code-generation, the alternate M definition is used. This is useful when we want to take advantage of native $ libraries on the target languages. {NMost generalized form of uninterpretation, this function should not be needed E by end-user-code, but is rather useful for the library development. |4Symbolic choice operator, parameterized via a class  1 is a total-indexing function, with the default. Minimal complete definition: } }:Merge two values based on the condition. This is intended  to be a  structural+ copy, walking down the values and merging & recursively through the structure of a. In particular, ? symbolicMerge should *not* waste its time testing whether the 7 condition might be a literal; that will be handled by ~ ; which should be used in all user code. In particular, any  implementation of } should just call } $ recursively in the constituents of a , instead of ~. ~9Choose one or the other element, based on the condition.  This is similar to }, but it has a default " implementation that makes sure it'*s short-cut if the condition is concrete. K The idea is that use symbolicMerge if you know the condition is symbolic,  otherwise use ite, if there'!s a chance it might be concrete. Total indexing operation. select xs default index is intuitively  the same as  xs !! index, except it evaluates to default if index  overflows The 2 class captures the essence of division of words. $ Unfortunately we cannot use Haskell's  class since the   and > superclasses are not implementable for symbolic bit-vectors.  However,  makes perfect sense, and the  class captures J this operation. One issue is how division by 0 behaves. The verification K technology requires total functions, and there are several design choices  here. We follow Isabelle/3HOL approach of assigning the value 0 for division / by 0. Therefore, we impose the following law:   x  0 = (0, x)5Note that our instances implement this law even when x is 0 itself. Minimal complete definition:  FSymbolic Numbers. This is a simple class that simply incorporates all  and  T values together, simplifying writing polymorphic type-signatures that work for all  symbolic numbers, such as :, 6+ etc. For instance, we can write a generic # list-minimum function as follows:    mm :: SNum a => [a] -> a  mm = foldr1 (a b -> ite (a .< = b) a b) It is similar to the standard 0 class, except ranging over symbolic instances. !Symbolic Comparisons. Similar to , we cannot implement Haskell's  class $ since there is no way to return an # value from a symbolic comparison.  Furthermore,  requires |$ to implement if-then-else, for the . benefit of implementing symbolic versions of  and  functions. Minimal complete definition:  #Symbolic Equality. Note that we can' t use Haskell's / class since Haskell insists on returning Bool E Comparing symbolic values will necessarily return a symbolic value. Minimal complete definition:  ,Generate a finite symbolic bitvector, named .Generate a finite symbolic bitvector, unnamed  Declare an ; Declare a list of ;s  Declare an : Declare a list of :s  Declare an 9 Declare a list of 9s  Declare an 8 Declare a list of 8s  Declare an 7 Declare a list of 7s  Declare an 6 Declare a list of 6s  Declare an 5 Declare a list of 5s  Declare an 4 Declare a list of 4s  Declare an 3 Declare a list of 3s  Declare an 2 Declare a list of 2s  Declare an 1 Declare a list of 1s  Promote an SInteger to an SReal MReturns (symbolic) true if all the elements of the given list are different. LReturns (symbolic) true if all the elements of the given list are the same. /Returns 1 if the boolean is true, otherwise 0. Replacement for  . Since   requires a N to be returned, R we cannot implement it for symbolic words. Index 0 is the least-significant bit. Replacement for !. Since ! returns an ", we cannot implement + it for symbolic words. Here, we return an :", which can overflow when used on 9 quantities that have more than 255 bits. Currently, that' s only the 2 type 8 that SBV supports, all other types are safe. Even with 2, this will only R overflow if there are at least 256-bits set in the number, and the smallest such S number is 2^256-1, which is a pretty darn big number to worry about for practical * purposes. In any case, we do not support " for unbounded symbolic integers, + as the only possible implementation wouldn'/t symbolically terminate. So the only overflow , issue is with really-really large concrete 2 values. Generalization of #( based on a symbolic boolean. Note that # and  $H are still available on Symbolic words, this operation comes handy when  the condition to set/clear happens to be symbolic. =Little-endian blasting of a word into its bits. Also see the FromBits class. :Big-endian blasting of a word into its bits. Also see the FromBits class. ;Least significant bit of a word, always stored at index 0. DMost significant bit of a word, always stored at the last position. Adding arbitrary constraints. 'Adding a probabilistic constraint. The % argument is the probability 5 threshold. Probabilistic constraints are useful for genTest and  quickCheck * calls where we restrict our attention to  interesting parts of the input domain. AExplicit sharing combinator. The SBV library has internal caching/hash-consing mechanisms  built in, based on Andy Gill'.s type-safe obervable sharing technique (see:  9http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09). r However, there might be times where being explicit on the sharing can help, especially in experimental code. The  combinator  ensures that its first argument is computed once and passed on to its continuation, explicitly indicating the intent of sharing. Most 7 use cases of the SBV library should simply use Haskell's let construct for this purpose. xyz{|}~&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~?xyz{|}~xyz{|}~&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~' experimentalerkokl@gmail.com Safe-Infered jPrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers. Minimal complete definition:  and  ,Show a number in hexadecimal (starting with 0x and type.) 'Show a number in binary (starting with 0b and type.) 0Show a number in hex, without prefix, or types. 0Show a number in bin, without prefix, or types. NShow as a hexadecimal value. First bool controls whether type info is printed M while the second boolean controls wether 0x prefix is printed. The tuple is J the signedness and the bit-length of the input. The length of the string  will not1 depend on the value, but rather the bit-length. LShow as a hexadecimal value, integer version. Almost the same as shex above  except we don'<t have a bit-length so the length of the string will depend  on the actual value.  Similar to ; except in binary.  Similar to ; except in binary. WA more convenient interface for reading binary numbers, also supports negative numbers  ( experimentalerkokl@gmail.com Safe-Infered4Sign casting a value into another. This essentially ; means forgetting the sign bit and reinterpreting the bits ; accordingly when converting a signed value to an unsigned ; one. Similarly, when an unsigned quantity is converted to 7 a signed one, the most significant bit is interpreted 7 as the sign. We only define instances when the source / and target types are precisely the same size.  The idea is that  and  must form ' an isomorphism pair between the types a and b , i.e., we . expect the following two properties to hold:    signCast . unsignCast = id  unsingCast . signCast = id ;Note that one naive way to implement both these operations  is simply to compute fromBitsLE . blastLE, i.e., first A get all the bits of the word and then reconstruct in the target > type. While this is semantically correct, it generates a lot C of code (both during proofs via SMT-Lib, and when compiled to C). C The goal of this class is to avoid that cost, so these operations E can be compiled very efficiently, they will essentially become no-op's. /Minimal complete definition: All, no defaults. Interpret as a signed word Interpret as an unsigned word  ) experimentalerkokl@gmail.com Safe-InferedKUnblasting a value from symbolic-bits. The bits can be given little-endian R or big-endian. For a signed number in little-endian, we assume the very last bit N is the sign digit. This is a bit awkward, but it is more consistent with the reverse view of # little-big-endian representations Minimal complete definiton:   Splitting an a into two b's and joining back.  Intuitively, a is a larger bit-size word than b, typically double.  The # operation captures embedding of a b value into an a & without changing its semantic value. /Minimal complete definition: All, no defaults. * experimentalerkokl@gmail.com Safe-Infered8A symbolic tree containing values of type e, indexed by ? elements of type i. Note that these are full-trees, and their = their shapes remain constant. There is no API provided that ? can change the shape of the tree. These structures are useful B when dealing with data-structures that are indexed with symbolic ( values where access time is important.  structures provide $ logarithmic time reads and writes. GReading a value. We bit-blast the index and descend down the full tree  according to bit-values. UWriting a value, similar to how reads are done. The important thing is that the tree , representation keeps updates to a minimum. BConstruct the fully balanced initial tree using the given values. + experimentalerkokl@gmail.com Safe-Infered QImplements polynomial addition, multiplication, division, and modulus operations  over GF(2^n). NB. Similar to , division by 0 is interpreted as follows:  x  0 = (0, x)for all x (including 0) Minimal complete definiton: , ,  3Given bit-positions to be set, create a polynomial  For instance  polynomial [0, 1, 3] :: SWord8will evaluate to 11, since it sets the bits 0, 1, and 3,. Mathematicans would write this polynomial  as  x^3 + x + 1. And in fact,  will show it like that.  Add two polynomials in GF(2^n). SMultiply two polynomials in GF(2^n), and reduce it by the irreducible specified by X the polynomial as specified by coefficients of the third argument. Note that the third j argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our e formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not F support symbolic irreducibles, which is a minor shortcoming. (Most GF'%s will come with fixed irreducibles, / so this should not be a problem in practice.)  Passing []^ for the third argument will multiply the polynomials and then ignore the higher bits that won't  fit into the resulting size. EDivide two polynomials in GF(2^n), see above note for division by 0. PCompute modulus of two polynomials in GF(2^n), see above note for modulus by 0. &Division and modulus packed together. CDisplay a polynomial like a mathematician would (over the monomial x), with a type. CDisplay a polynomial like a mathematician would (over the monomial x), the first argument . controls if the final type is shown as well. (Compute CRCs over bit-vectors. The call  crcBV n m p computes  the CRC of the message m with respect to polynomial p. The 9 inputs are assumed to be blasted big-endian. The number  n5 specifies how many bits of CRC is needed. Note that n * is actually the degree of the polynomial p, and thus it seems ? redundant to pass it in. However, in a typical proof context, A the polynomial can be symbolic, so we cannot compute the degree A easily. While this can be worked-around by generating code that = accounts for all possible degrees, the resulting code would A be unnecessarily big and complicated, and much harder to reason < with. (Also note that a CRC is just the remainder from the D polynomial division, but this routine is much faster in practice.) NB. The nth bit of the polynomial p must be set for the CRC = to be computed correctly. Note that the polynomial argument p will G not even have this bit present most of the time, as it will typically  contain bits 0 through n-1, as usual in the CRC literature. The higher  order n8th bit is simply assumed to be set, as it does not make M sense to use a polynomial of a lesser degree. This is usually not a problem < since CRC polynomials are designed and expressed this way. NB. The literature on CRC's has many variants on how CRC's are computed.  We follow the painless guide ( +http://www.ross.net/crc/download/crc_v3.txt) ! and compute the CRC as follows:  Extend the message m by adding n 0 bits on the right , Divide the polynomial thus obtained by the p ! The remainder is the CRC value. $There are many variants on final XOR'!s, reversed polynomials etc., so 5 it is essential to double check you use the correct  algorithm.  Compute CRC'4s over polynomials, i.e., symbolic words. The first  "0 argument plays the same role as the one in the  function.   , experimentalerkokl@gmail.com Safe-InferedMGiven a symbolic computation, render it as an equivalent collection of files  that make up a C program: W The first argument is the directory name under which the files will be saved. To save ) files in the current directory pass  ".". Use  for printing to stdout. @ The second argument is the name of the C function to generate. 4 The final argument is the function to be compiled. !Compilation will also generate a Makefile4, a header file, and a driver (test) program, etc. Lower level version of , producing a ` jCreate code to generate a library archive (.a) from given symbolic functions. Useful when generating code : from multiple functions that work together as a library. W The first argument is the directory name under which the files will be saved. To save ) files in the current directory pass  ".". Use  for printing to stdout. = The second argument is the name of the archive to generate. U The third argument is the list of functions to include, in the form of function-name/code pairs, similar * to the second and third arguments of , except in a list. Lower level version of , producing a `  experimentalerkokl@gmail.com Safe-Infered<=>?@ABQVXY[\]^_`aB>A@?XY<=QV`a[_^]\- experimentalerkokl@gmail.com Safe-InferedTest output style  As a Forte/Verilog value with given name. U If the boolean is True then vectors are blasted big-endian, otherwise little-endian M The indices are the split points on bit-vectors for input and output values (As a C array of structs with given name #As a Haskell value with given name  Type of test vectors (abstract) @Retrieve the test vectors for further processing. This function  is useful in cases where  is not sufficient and custom . output (or further preprocessing) is needed. KGenerate a set of concrete test values from a symbolic program. The output N can be rendered as test vectors in different languages as necessary. Use the  function /< call to indicate what fields should be in the test result.  (Also see  constrain and  pConstrain( for filtering acceptable test values.) 7Render the test as a Haskell value with the given name n. . experimentalerkokl@gmail.com Safe-Infered27Various SMT results that we can extract models out of. Is there a model? JExtract a model, the result is a tuple where the first argument (if True) ! indicates whether the model was probable*. (i.e., if the solver returned unknown.) A simpler variant of & to get a model out without the fuss.  Instances of < can be automatically extracted from models returned by the G solvers. The idea is that the sbv infrastructure provides a stream of CW's (constant-words) & coming from the solver, and the type a7 is interpreted based on these constants. Many typical V instances are already provided, so new instances can be declared with relative ease. Minimum complete definition:  EGiven a sequence of constant-words, extract one instance of the type a , returning B the remaining elements untouched. If the next element is not what's expected for this  type you should return  2Given a parsed model instance, transform it using f, and return the result. P The default definition for this method should be sufficient in most use cases. An allSat call results in a . The boolean says whether 4 we should warn the user about prefix-existentials. A sat call results in a  " The reason for having a separate  is to have a more meaningful  instance. A prove call results in a  &A script, to be passed to the solver.  Initial feed 3Optional continuation script, if the result is sat BThe result of an SMT solver call. Each constructor is tagged with  the 6 that created it so that further tools can inspect it K and build layers of results, if needed. For ordinary uses of the library, G this type should not be needed, instead use the accessor functions on 3 it. (Custom Show instances and model extractors.) Computation timed out (see the timeout combinator) Prover errored out AProver returned unknown, with a potential (possibly bogus) model Satisfiable with model Unsatisfiable !A model, as returned by a solver An SMT solver Printable name of the solver The path to its executable !Options to provide to the solver >The solver engine, responsible for interpreting solver output An SMT engine Solver configuration. See also z3 and yices@, which are instantiations of this type for those solvers, with k reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as z3{verbose=True}.) Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does { not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to ~ emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite * precision value on the screen. The field K controls the printing precision, by specifying the number of digits after X the decimal point. The default value is 16, but it can be set to any positive integer. 'When printing, SBV will add the suffix ...^ at the and of a real-value, if the given bound is not sufficient to represent the real-value  exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it  is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation ? of the real value is not finite, i.e., if it is not rational.  Debug mode YPrint timing information on how long different phases took (construction, solving, etc.) 2How much time to give to the solver. (In seconds) KPrint integral literals in this base (2, 8, and 10, and 16 are supported.) FPrint algebraic real values with this precision. (SReal, default: 16) BAdditional lines of script to give to the solver (user specified) [If Just, the generated SMT script will be put in this file (for debugging purposes mostly)  If True, we'Fll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1 The actual SMT solver. .Extract the final configuration from a result Parse a signed/#sized value from a sequence of CWs Return all the models from an allSat call, similar to  but / is suitable for the case of multiple results. AExtract a model out, will throw error if parsing is unsuccessful  Given an allSatS call, we typically want to iterate over it and print the results in sequence. The  ) function automates this task by calling disp* on each result, consecutively. The first  " argument to disp 'Mis the current model number. The second argument is a tuple, where the first d element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown) #Show an SMTResult; generic version $Show a model in human readable form 2Show a constant value, in the user-specified base DPrint uninterpreted function values from models. Very, very crude.. APrint uninterpreted array values from models. Very, very crude.. .Helper function to spin off to an SMT solver. fA standard solver interface. If the solver is SMT-Lib compliant, then this function should suffice in  communicating with it.  A variant of -; except it knows about continuation strings ) and can speak SMT-Lib2 (just a little). \In case the SMT-Lib solver returns a response over multiple lines, compress them so we have 2 each S-Expression spanning only a single line. We'0ll ignore things line parentheses inside quotes $ etc., as it should not be an issue W<4 / experimentalerkokl@gmail.com Safe-InferedAdd constraints to generate new> models. This function is used to query the SMT-solver, while  disallowing a previous model. +Translate a problem into an SMTLib2 script has infinite precision values is this a sat problem? extra comments to place on top uninterpreted sorts inputs skolemized version inputs  constants auto-generated tables user specified arrays uninterpreted functions/ constants user given axioms  assignments extra constraints output variable 0 experimentalerkokl@gmail.com Safe-Infered[An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for  newer versions in the future.) Convert to SMTLib-1 format Convert to SMTLib-2 format JAdd constraints generated from older models, used for querying new models CInterpret solver output based on SMT-Lib standard output responses has unbounded integers/reals is this a sat problem? extra comments to place on top uninterpreted sorts inputs and aliasing names skolemized inputs  constants auto-generated tables user specified arrays uninterpreted functions/ constants user given axioms  assignments extra constraints output variable b1 experimentalerkokl@gmail.com Safe-InferedOADT S-Expression format, suitable for representing get-model output of SMT-Lib HParse a string into an SExpr, potentially failing with an error message 2 experimentalerkokl@gmail.com Safe-Infered(The description of the Yices SMT solver  The default executable is "yices"., which must be in your path. You can use the  SBV_YICESA environment variable to point to the executable on your system.  The default options are "-m -f"5, which is valid for Yices 2 series. You can use the SBV_YICES_OPTIONS/ environment variable to override the options. 3 experimentalerkokl@gmail.com Safe-Infered%The description of the Z3 SMT solver  The default executable is "z3"., which must be in your path. You can use the SBV_Z3A environment variable to point to the executable on your system.  The default options are "/in /smt2"-, which is valid for Z3 3.2. You can use the SBV_Z3_OPTIONS/ environment variable to override the options. 4 experimentalerkokl@gmail.comNone'Equality as a proof method. Allows for K very concise construction of equivalence proofs, which is very typical in  bit-precise proofs. A type a1 is provable if we can turn it into a predicate. U Note that a predicate can be made from a curried function of arbitrary arity, where Q each element is either a symbolic type or up-to a 7-tuple of symbolic-types. So [ predicates can be constructed from almost arbitrary Haskell functions that have arbitrary 0 shapes. (See the instance declarations below.) UTurns a value into a universally quantified predicate, internally naming the inputs. 9 In this case the sbv library will use names of the form s1, s2, etc. to name these variables  Example:  1 forAll_ $ \(x::SWord8) y -> x `shiftL` 2 .== y \is a predicate with two arguments, captured using an ordinary Haskell function. Internally,  x will be named s0 and y will be named s1. PTurns a value into a predicate, allowing users to provide names for the inputs. [ If the user does not provide enough number of names for the variables, the remaining ones ` will be internally generated. Note that the names are only used for printing models and has no S other significance; in particular, we do not check that they are unique. Example:  ; forAll ["x", "y"] $ \(x::SWord8) y -> x `shiftL` 2 .== y >This is the same as above, except the variables will be named x and y respectively, 9 simplifying the counter-examples when they are printed.  CTurns a value into an existentially quantified predicate. (Indeed,  would have been / a better choice here for the name, but alas it's already taken.)   Version of   that allows user defined names  _A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and Y purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The 0 6 monad captures the underlying representation, and can//should be ignored by the users of the library, Y unless you are building further utilities on top of SBV itself. Instead, simply use the    type when necessary.  0Default configuration for the Yices SMT Solver.  ,Default configuration for the Z3 SMT solver =The default solver used by SBV. This is currently set to z3. !Prove a predicate, equivalent to   <Find a satisfying assignment for a predicate, equivalent to   ZForm the symbolic conjunction of a given list of boolean conditions. Useful in expressing 0 problems with constraints, like the following:   do [x, y, z] < - sIntegers ["x", "y", "z"]  solve [x .> 5, y + z .< x] AReturn all satisfying assignments for a predicate, equivalent to  . d Satisfying assignments are constructed lazily, so they will be available as returned by the solver  and on demand. NB. Uninterpreted constant/Ffunction values and counter-examples for array values are ignored for  the purposes of N. That is, only the satisfying assignments modulo uninterpreted functions and h array inputs will be returned. This is due to the limitation of not having a robust means of getting a 4 function counter-example back from the SMT solver. >Check if the given constraints are satisfiable, equivalent to  . This @ call can be used to ensure that the specified constraints (via ) are satisfiable, i.e., that l the proof involving these constraints is not passing vacuously. Here is an example. Consider the following  predicate: Slet pred = do { x <- forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }cThis predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the  values considered satisfy x .< xF, i.e., they are less than themselves. Since there are no values that 9 satisfy this constraint, the proof will pass vacuously:  prove predQ.E.D. We can use 0 to make sure to see that the pass was vacuous: isVacuous predTruefWhile the above example is trivial, things can get complicated if there are multiple constraints with g non-straightforward relations; so if constraints are used one should make sure to check the predicate  is not vacuously true. Here'"s an example that is not vacuous: Tlet pred' = do { x <- forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }(This time the proof passes as expected:  prove pred'Q.E.D.And the proof is not vacuous: isVacuous pred'False2Checks theoremhood within the given time limit of i seconds.  Returns Nothing* if times out, or the result wrapped in a Just otherwise. 5Checks satisfiability within the given time limit of i seconds.  Returns Nothing* if times out, or the result wrapped in a Just otherwise. Checks theoremhood Checks satisfiability EReturns the number of models that satisfy the predicate, as it would  be returned by -. Note that the number of models is always a G finite number, and hence this will always return a result. Of course, J computing it might take quite long, as it literally generates and counts " the number of satisfying models. UCompiles to SMT-Lib and returns the resulting program as a string. Useful for saving X the result to a file for off-line analysis, for instance if you have an SMT solver that's not natively 1 supported out-of-the box by the SBV library. If smtLib2+ parameter is False, then we will generate ; SMTLib1 output, otherwise we will generate SMTLib2 output ^Create both SMT-Lib1 and SMT-Lib2 benchmarks. The first argument is the basename of the file, . SMT-Lib1 version will be written with suffix .smt1+ and SMT-Lib2 version will be written with  suffix .smt2 0Proves the predicate using the given SMT-solver 8Find a satisfying assignment using the given SMT-solver DDetermine if the constraints are vacuous using the given SMT-solver ;Find all satisfying assignments using the given SMT-solver QCheck whether the given solver is installed and is ready to go. This call does a 2 simple call to the solver to ensure all is well. 3          B     .          5 experimentalerkokl@gmail.com Safe-Infered  kOptimizer configuration. Note that iterative and quantified approaches are in general not interchangeable. q For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions a can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally. !Use quantifiers ";Iteratively search. if True, it will be reporting progress #)Symbolic optimization. Generalization on ( and & that allows arbitrary ! cost functions and comparisons. $ Variant of # using the default solver. See # for parameter descriptions. % Variant of &2 allowing the use of a user specified solver. See # for parameter descriptions. &BMaximizes a cost function with respect to a constraint. Examples: 6maximize Quantified sum 3 (bAll (.< (10 :: SInteger))) Just [9,9,9]' Variant of (2 allowing the use of a user specified solver. See # for parameter descriptions. (BMinimizes a cost function with respect to a constraint. Examples: 6minimize Quantified sum 3 (bAll (.> (10 :: SInteger)))Just [11,11,11]  !"#SMT configuration Optimization options  comparator cost function how many elements? validity constraint $%&'(  !"#$%&'( "!#$%&'( experimentalerkokl@gmail.com Safe-Infered9" !"!#$%&'()* +$#,-./0123456  !"#$%&'()*+,-./0123456789:;<CDEFGHIJKLMNOPQRSTUWZbcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'(;:987654321<Z|}~ xyz{W   (&$'%#wv "!  0/ !"#$%&'()*+,-.QRSTCDEFGHIJKLPONMUfgljkpqrstumnohibedc experimentalerkokl@gmail.com Safe-Infered) Formalizes  Chttp://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax * Formalizes  Chttp://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax + Formalizes  Ghttp://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns , Formalizes  ]http://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching - Formalizes  Ghttp://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2 .Collection of queries )*+,-.)*+,-.)*+,-.)*+,-. experimentalerkokl@gmail.com Safe-Infered&/LChoose the appropriate array model to be used for modeling the memory. (See 9.)  The  is the function based model.  is the SMT-Lib array's based model. 05Helper synonym for capturing relevant bits of Mostek 1An instruction is modeled as a 2 transformer. We model 7 mostek programs in direct continuation passing style. 2CPrograms are essentially state transformers (on the machine state) 31Given a machine state, compute a value out of it 4NAbstraction of the machine: The CPU consists of memory, registers, and flags. ] Unlike traditional hardware, we assume the program is stored in some other memory area that 2 we need not model. (No self modifying programs!) 92The memory maps 32-bit words to 8-bit words. (The / data-type is ; defined later, depending on the verification model used.) : Flag bank ;Register bank <.Convenient synonym for symbolic machine bits. =Mostek was an 8-bit machine. >The carry flag (@) and the zero flag (?) AYWe model only two registers of Mostek that is used in the above algorithm, can add more. D)The memory is addressed by 32-bit words. E"Get the value of a given register F"Set the value of a given register GGet the value of a flag HSet the value of a flag I Read memory JWrite to memory KChecking overflow. In Legato's multipler the ADC instruction A needs to see if the expression x + y + c overflowed, as checked E by this function. Note that we verify the correctness of this check  separately below in L. LCorrectness theorem for our K implementation.  We have: checkOverflowCorrectQ.E.D.MLDX: Set register X to value v NLDA: Set register A to value v OCLC: Clear the carry flag P9ROR, memory version: Rotate the value at memory location a E to the right by 1 bit, using the carry flag as a transfer position. E That is, the final bit of the memory location becomes the new carry B and the carry moves over to the first bit. This very instruction ! is one of the reasons why Legato')s multiplier is quite hard to understand 9 and is typically presented as a verification challenge. QROR, register version: Same as P, except through register r. RBCC: branch to label l if the carry flag is false S%ADC: Increment the value of register A! by the value of memory contents  at address a8, using the carry-bit as the carry-in for the addition. T%DEX: Decrement the value of register X U&BNE: Branch if the zero-flag is false VThe V combinator stops/ our program, providing the final continuation  that does nothing. W<Parameterized by the addresses of locations of the factors (F1 and F2), K the following program multiplies them, storing the low-byte of the result  in the memory location lowAddr , and the high-byte in register A. The 5 implementation is a direct transliteration of Legato's algorithm given ! at the top, using our notation. X Given address/Bvalue pairs for F1 and F2, and the location of where the low-byte  of the result should go,  runLegato" takes an arbitrary machine state m and 7 returns the high and low bytes of the multiplication. YUCreate an instance of the Mostek machine, initialized by the memory and the relevant ' values of the registers and the flags ZNThe correctness theorem. For all possible memory configurations, the factors (x and y below), the location r of the low-byte result and the initial-values of registers and the flags, this function will return True only if  running Legato'/s algorithm does indeed compute the product of x and y correctly. [The correctness theorem. F On a decent MacBook Pro, this proof takes about 3 minutes with the  memory model ! and about 30 minutes with the & model, using yices as the SMT solver \+Generate a C program that implements Legato's algorithm automatically. //0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\7./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\.DACB>@?=<;:94567832EFGHIJKL1MNOPQRSTUVWX0YZ/[\'/0123456789:;<=>@?ACBDEFGHIJKLMNOPQRSTUVWXYZ[\7 experimentalerkokl@gmail.com Safe-Infered]Element type of lists we'"d like to sort. For simplicity, we'll just  use :* here, but we can pick any symbolic type. ^6Merging two given sorted lists, preserving the order. _BSimple merge-sort implementation. We simply divide the input list A in two two halves so long as it has at least two elements, sort ' each half on its own, and then merge. `2Check whether a given sequence is non-decreasing. aWCheck whether two given sequences are permutations. We simply check that each sequence W 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. bSAsserting correctness of merge-sort for a list of the given size. Note that we can U only check correctness for fixed-size lists. Also, the proof will get more and more + complicated for the backend SMT solver as n) increases. A value around 5 or 6 should 1 be fairly easy to prove. For instance, we have:  correctness 5Q.E.D.c3Generate C code for merge-sorting an array of size n . Again, we're restricted R to fixed size inputs. While the output is not how one would code merge sort in C  by hand, it'Ds a faithful rendering of all the operations merge-sort would do as  described by it's Haskell counterpart. ]^_`abc]^_`abc]^_`abc]^_`abc experimentalerkokl@gmail.com Safe-Inferedd A poor man'#s representation of powerlists and  basic operations on them:  0http://www.cs.utexas.edu/users/psp/powerlist.pdf. 4 We merely represent power-lists by ordinary lists. e!The tie operator, concatenation. fAThe zip operator, zips the power-lists of the same size, returns ! a powerlist of double the size. gInverse of zipping. hReference prefix sum (ps) is simply Haskell's scanl1 function. iThe Ladner-Fischer (lf$) implementation of prefix-sum. See  Jhttp://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf  or pg. 16 of  0http://www.cs.utexas.edu/users/psp/powerlist.pdf. jhCorrectness theorem, for a powerlist of given size, an associative operator, and its left-unit element. kMProves Ladner-Fischer is equivalent to reference specification for addition.  0; is the left-unit element, and we use a power-list of size 8. lPProves Ladner-Fischer is equivalent to reference specification for the function max.  0; is the left-unit element, and we use a power-list of size 16. mCTry proving correctness for an arbitrary operator. This proof will not go through since the f SMT solver does not know that the operator associative and has the given left-unit element. We have: thm3Falsifiable. Counter-example: s0 = 0 :: SWord32 s1 = 0 :: SWord32 s2 = 0 :: SWord32 s3 = 0 :: SWord32 s4 = 0 :: SWord32 s5 = 0 :: SWord32 s6 = 0 :: SWord32 s7 = 3221225472 :: SWord32 -- uninterpreted: u u = 0 -- uninterpreted: flOp% flOp 0 3221225472 = 2147483648% flOp 0 2147483648 = 3758096384 flOp _ _ = 0+You can verify that the above function for flOp is not associative:   6 ghci> flOp 3221225472 (flOp 2147483648 3221225472)  0 6 ghci> flOp (flOp 3221225472 2147483648) 3221225472  2147483648 Also, the unit 0 is clearly not a left-unit for flOp, as the third  equation for flOp" will simply map many elements to 0. H (NB. We need to use yices for this proof as the uninterpreted function E examples are only supported through the yices interface currently.) ndGenerate an instance of the prefix-sum problem for an arbitrary operator, by telling the SMT solver t the necessary axioms for associativity and left-unit. The first argument states how wide the power list should be. oCProve the generic problem for powerlists of given sizes. Note that G this will only work for Yices-1. This is due to the fact that Yices-2 K follows the SMT-Lib standard and does not accept bit-vector problems with J quantified axioms in them, while Yices-1 did allow for that. The crux of @ the problem is that there are no SMT-Lib logics that combine BV's and  quantifiers, see:  -http://goedel.cs.uiowa.edu/smtlib/logics.html. So we ; are stuck until new powerful logics are added to SMT-Lib. OHere, we explicitly tell SBV to use Yices-1 that did not have that limitation. E Tweak the executable location accordingly below for your platform..  We have:  prefixSum 2Q.E.D. prefixSum 4Q.E.D.GNote that these proofs tend to run long. Also, Yices ran out of memory - and crashed on my box when I tried for size 8(, after running for about 2.5 minutes.. pHA symbolic trace can help illustrate the action of Ladner-Fischer. This L generator produces the actions of Ladner-Fischer for addition, showing how  the computation proceeds: ladnerFischerTrace 8'INPUTS s0 :: SWord8 s1 :: SWord8 s2 :: SWord8 s3 :: SWord8 s4 :: SWord8 s5 :: SWord8 s6 :: SWord8 s7 :: SWord8 CONSTANTS s_2 = False s_1 = TrueTABLESARRAYSUNINTERPRETED CONSTANTSUSER GIVEN CODE SEGMENTSAXIOMSDEFINE s8 :: SWord8 = s0 + s1 s9 :: SWord8 = s2 + s8 s10 :: SWord8 = s2 + s3 s11 :: SWord8 = s8 + s10 s12 :: SWord8 = s4 + s11 s13 :: SWord8 = s4 + s5 s14 :: SWord8 = s11 + s13 s15 :: SWord8 = s6 + s14 s16 :: SWord8 = s6 + s7 s17 :: SWord8 = s13 + s16 s18 :: SWord8 = s11 + s17 CONSTRAINTSOUTPUTS s0 s8 s9 s11 s12 s14 s15 s18qSTrace generator for the reference spec. It clearly demonstrates that the reference D implementation fewer operations, but is not parallelizable at all:  scanlTrace 8#INPUTS s0 :: SWord8 s1 :: SWord8 s2 :: SWord8 s3 :: SWord8 s4 :: SWord8 s5 :: SWord8 s6 :: SWord8 s7 :: SWord8 CONSTANTS s_2 = False s_1 = TrueTABLESARRAYSUNINTERPRETED CONSTANTSUSER GIVEN CODE SEGMENTSAXIOMSDEFINE s8 :: SWord8 = s0 + s1 s9 :: SWord8 = s2 + s8 s10 :: SWord8 = s3 + s9 s11 :: SWord8 = s4 + s10 s12 :: SWord8 = s5 + s11 s13 :: SWord8 = s6 + s12 s14 :: SWord8 = s7 + s13 CONSTRAINTSOUTPUTS s0 s8 s9 s10 s11 s12 s13 s14defghijklmnopqdefghijklmnopqdefghijklmnopqdefghijklmnopq experimentalerkokl@gmail.com Safe-Inferedr Simple function that returns add/ sum of args s Generate C code for addSub. Here'+s the output showing the generated C code:  genAddSub%== BEGIN: "Makefile" ================C# Makefile for addSub. Automatically generated by SBV. Do not edit!=# include any user-defined .mk file in the current directory. -include *.mkCC=gcc0CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointerall: addSub_driveraddSub.o: addSub.c addSub.h ${CC} ${CCFLAGS} -c $< -o $@ addSub_driver.o: addSub_driver.c ${CC} ${CCFLAGS} -c $< -o $@'addSub_driver: addSub.o addSub_driver.o ${CC} ${CCFLAGS} $^ -o $@clean: rm -f *.overyclean: clean rm -f addSub_driver%== END: "Makefile" ==================%== BEGIN: "addSub.h" ================ BLANKLINE  ##ifndef __addSub__HEADER_INCLUDED__  ##define __addSub__HEADER_INCLUDED__   BLANKLINE  #include  inttypes.h  #include  stdint.h  #include  stdbool.h   BLANKLINE typedef bool SBool;   BLANKLINE typedef uint8_t SWord8 ;  typedef uint16_t SWord16;  typedef uint32_t SWord32;  typedef uint64_t SWord64;   BLANKLINE typedef int8_t SInt8 ;  typedef int16_t SInt16;  typedef int32_t SInt32;  typedef int64_t SInt64;   BLANKLINE 9void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,  SWord8 *dif);   BLANKLINE  #endif  == END: addSub.h ==================  == BEGIN: addSub_driver.c ================  BLANKLINE  #include  inttypes.h  #include  stdint.h  #include  stdbool.h  #include  stdio.h  #include addSub.h   BLANKLINE  int main(void)  {  SWord8 sum;  SWord8 dif;   BLANKLINE  addSub(132, 241, &sum, &dif);   BLANKLINE  printf( addSub(132, 241, &sum, &dif) ->n);  printf( sum = %PRIu8n, sum);  printf( dif = %PRIu8n, dif);   BLANKLINE  return 0;  }  == END: addSub_driver.c ==================  == BEGIN: addSub.c ================  BLANKLINE  #include  inttypes.h  #include  stdint.h  #include  stdbool.h  #include addSub.h   BLANKLINE : void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,  SWord8 *dif)  {  const SWord8 s0 = x;  const SWord8 s1 = y;  const SWord8 s2 = s0 + s1;  const SWord8 s3 = s0 - s1;   BLANKLINE  *sum = s2;  *dif = s3;  }  == END: addSub.c ================== rsrsrsrs experimentalerkokl@gmail.com Safe-InferedtThe USB CRC polynomial:  x^5 + x^2 + 1. F Although this polynomial needs just 6 bits to represent (5 if higher / order bit is implicitly assumed to be set), we'll simply use a 16 bit I number for its representation to keep things simple for code generation  purposes. uIGiven an 11 bit message, compute the CRC of it using the USB polynomial, M which is 5 bits, and then append it to the msg to get a 16-bit word. Again, K the incoming 11-bits is represented as a 16-bit word, with 5 highest bits ) essentially ignored for input purposes. v(Alternate method for computing the CRC, mathematically . We shift F the number to the left by 5, and then compute the remainder from the H polynomial division by the USB polynomial. The result is then appended  to the end of the message. wProve that the custom , function is equivalent to the mathematical  definition of CRC' s for 11 bit messages. We have: crcGoodQ.E.D.xEGenerate a C function to compute the USB CRC, using the internal CRC  function. yEGenerate a C function to compute the USB CRC, using the mathematical M definition of the CRCs. Whule this version generates functionally eqivalent  C code, it'<s less efficient; it has about 30% more code. So, the above 5 version is preferable for code generation purposes. tuvwxytuvwxytuvwxytuvwxy  experimentalerkokl@gmail.com Safe-InferedzNThis is a naive implementation of fibonacci, and will work fine (albeit slow)  for concrete inputs: map fib0 [0..6]\[0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]NHowever, it is not suitable for doing proofs or generating code, as it is not B symbolically terminating when it is called with a symbolic value n . When we  recursively call fib0 on n-1 (or n-2), the test against 0 will always I explore both branches since the result will be symbolic, hence will not D terminate. (An integrated theorem prover can establish termination L after a certain number of unrollings, but this would be quite expensive to ' implement, and would be impractical.) {dThe recursion-depth limited version of fibonacci. Limiting the maximum number to be 20, we can say: map (fib1 20) [0..6]\[0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]KThe function will work correctly, so long as the index we query is at most top, and otherwise  will return the value at topE. Note that we also use accumulating parameters here for efficiency, 9 although this is orthogonal to the termination concern. \A note on modular arithmetic: The 64-bit word we use to represent the values will of course E eventually overflow, beware! Fibonacci is a fast growing function.. |We can generate code for { using the | action. Note that the = generated code will grow larger as we pick larger values of top, but only linearly, 4 thanks to the accumulating parameter trick used by {. The following is an excerpt & from the code generated for the call  genFib1 10%, where the code will work correctly  for indexes up to 10:  SWord64 fib1(const SWord64 x)  {  const SWord64 s0 = x; 3 const SBool s2 = s0 == 0x0000000000000000ULL; 3 const SBool s4 = s0 == 0x0000000000000001ULL; 3 const SBool s6 = s0 == 0x0000000000000002ULL; 3 const SBool s8 = s0 == 0x0000000000000003ULL; 4 const SBool s10 = s0 == 0x0000000000000004ULL; 4 const SBool s12 = s0 == 0x0000000000000005ULL; 4 const SBool s14 = s0 == 0x0000000000000006ULL; 4 const SBool s17 = s0 == 0x0000000000000007ULL; 4 const SBool s19 = s0 == 0x0000000000000008ULL; 4 const SBool s22 = s0 == 0x0000000000000009ULL; L const SWord64 s25 = s22 ? 0x0000000000000022ULL : 0x0000000000000037ULL; : const SWord64 s26 = s19 ? 0x0000000000000015ULL : s25; : const SWord64 s27 = s17 ? 0x000000000000000dULL : s26; : const SWord64 s28 = s14 ? 0x0000000000000008ULL : s27; : const SWord64 s29 = s12 ? 0x0000000000000005ULL : s28; : const SWord64 s30 = s10 ? 0x0000000000000003ULL : s29; 9 const SWord64 s31 = s8 ? 0x0000000000000002ULL : s30; 9 const SWord64 s32 = s6 ? 0x0000000000000001ULL : s31; 9 const SWord64 s33 = s4 ? 0x0000000000000001ULL : s32; 9 const SWord64 s34 = s2 ? 0x0000000000000000ULL : s33;   return s34;  } },Compute the fibonacci numbers statically at code-generation time and & put them in a table, accessed by the  call. ~ Once we have }6, we can generate the C code straightforwardly. Below = is an excerpt from the code that SBV generates for the call  genFib2 64. Note N that this code is a constant-time look-up table implementation of fibonacci, E with no run-time overhead. The index can be made arbitrarily large, - naturally. (Note that this function returns 0 if the index is larger & than 64, as specified by the call to  with default 0.) $ SWord64 fibLookup(const SWord64 x)  {  const SWord64 s0 = x; % static const SWord64 table0[] = { 5 0x0000000000000000ULL, 0x0000000000000001ULL, 5 0x0000000000000001ULL, 0x0000000000000002ULL, 5 0x0000000000000003ULL, 0x0000000000000005ULL, 5 0x0000000000000008ULL, 0x000000000000000dULL, 5 0x0000000000000015ULL, 0x0000000000000022ULL, 5 0x0000000000000037ULL, 0x0000000000000059ULL, 5 0x0000000000000090ULL, 0x00000000000000e9ULL, 5 0x0000000000000179ULL, 0x0000000000000262ULL, 5 0x00000000000003dbULL, 0x000000000000063dULL, 5 0x0000000000000a18ULL, 0x0000000000001055ULL, 5 0x0000000000001a6dULL, 0x0000000000002ac2ULL, 5 0x000000000000452fULL, 0x0000000000006ff1ULL, 5 0x000000000000b520ULL, 0x0000000000012511ULL, 5 0x000000000001da31ULL, 0x000000000002ff42ULL, 5 0x000000000004d973ULL, 0x000000000007d8b5ULL, 5 0x00000000000cb228ULL, 0x0000000000148addULL, 5 0x0000000000213d05ULL, 0x000000000035c7e2ULL, 5 0x00000000005704e7ULL, 0x00000000008cccc9ULL, 5 0x0000000000e3d1b0ULL, 0x0000000001709e79ULL, 5 0x0000000002547029ULL, 0x0000000003c50ea2ULL, 5 0x0000000006197ecbULL, 0x0000000009de8d6dULL, 5 0x000000000ff80c38ULL, 0x0000000019d699a5ULL, 5 0x0000000029cea5ddULL, 0x0000000043a53f82ULL, 5 0x000000006d73e55fULL, 0x00000000b11924e1ULL, 5 0x000000011e8d0a40ULL, 0x00000001cfa62f21ULL, 5 0x00000002ee333961ULL, 0x00000004bdd96882ULL, 5 0x00000007ac0ca1e3ULL, 0x0000000c69e60a65ULL, 5 0x0000001415f2ac48ULL, 0x000000207fd8b6adULL, 5 0x0000003495cb62f5ULL, 0x0000005515a419a2ULL, 5 0x00000089ab6f7c97ULL, 0x000000dec1139639ULL, 5 0x000001686c8312d0ULL, 0x000002472d96a909ULL, K 0x000003af9a19bbd9ULL, 0x000005f6c7b064e2ULL, 0x000009a661ca20bbULL  }; F const SWord64 s65 = s0 >= 65 ? 0x0000000000000000ULL : table0[s0];   return s65;  } z{|}~z{|}~z{|}~z{|}~  experimentalerkokl@gmail.com Safe-Infered>The symbolic GCD algorithm, over two 8-bit numbers. We define sgcd a 0 to  be a for all a, which implies  sgcd 0 0 = 0 . Note that this is essentially  Euclid'Fs algorithm, except with a recursion depth counter. We need the depth $ counter since the algorithm is not symbolically terminating , as we don't have 2 a means of determining that the second argument (b() will eventually reach 0 in a symbolic 7 context. Hence we stop after 12 iterations. Why 12? We'$ve empirically determined that this Y algorithm will recurse at most 12 times for arbitrary 8-bit numbers. Of course, this is $ a claim that we shall prove below.  We have: prove sgcdIsCorrectQ.E.D.LThis call will generate the required C files. The following is the function  body generated for ,. (We are not showing the generated header, Makefile, K and the driver programs for brevity.) Note that the generated function is T a constant time algorithm for GCD. It is not necessarily fastest, but it will take 5 precisely the same amount of time for all values of x and y.    #include <inttypes.h>  #include <stdint.h>  #include <stdbool.h>  #include "sgcd.h"  - SWord8 sgcd(const SWord8 x, const SWord8 y)  {  const SWord8 s0 = x;  const SWord8 s1 = y;  const SBool s3 = s1 == 0; 1 const SWord8 s4 = (s1 == 0) ? s0 : (s0 % s1); # const SWord8 s5 = s3 ? s0 : s4;  const SBool s6 = 0 == s5; 1 const SWord8 s7 = (s5 == 0) ? s1 : (s1 % s5); # const SWord8 s8 = s6 ? s1 : s7;  const SBool s9 = 0 == s8; 2 const SWord8 s10 = (s8 == 0) ? s5 : (s5 % s8); % const SWord8 s11 = s9 ? s5 : s10;  const SBool s12 = 0 == s11; 4 const SWord8 s13 = (s11 == 0) ? s8 : (s8 % s11); & const SWord8 s14 = s12 ? s8 : s13;  const SBool s15 = 0 == s14; 6 const SWord8 s16 = (s14 == 0) ? s11 : (s11 % s14); ' const SWord8 s17 = s15 ? s11 : s16;  const SBool s18 = 0 == s17; 6 const SWord8 s19 = (s17 == 0) ? s14 : (s14 % s17); ' const SWord8 s20 = s18 ? s14 : s19;  const SBool s21 = 0 == s20; 6 const SWord8 s22 = (s20 == 0) ? s17 : (s17 % s20); ' const SWord8 s23 = s21 ? s17 : s22;  const SBool s24 = 0 == s23; 6 const SWord8 s25 = (s23 == 0) ? s20 : (s20 % s23); ' const SWord8 s26 = s24 ? s20 : s25;  const SBool s27 = 0 == s26; 6 const SWord8 s28 = (s26 == 0) ? s23 : (s23 % s26); ' const SWord8 s29 = s27 ? s23 : s28;  const SBool s30 = 0 == s29; 6 const SWord8 s31 = (s29 == 0) ? s26 : (s26 % s29); ' const SWord8 s32 = s30 ? s26 : s31;  const SBool s33 = 0 == s32; 6 const SWord8 s34 = (s32 == 0) ? s29 : (s29 % s32); ' const SWord8 s35 = s33 ? s29 : s34;  const SBool s36 = 0 == s35; ' const SWord8 s37 = s36 ? s32 : s35; ' const SWord8 s38 = s33 ? s29 : s37; ' const SWord8 s39 = s30 ? s26 : s38; ' const SWord8 s40 = s27 ? s23 : s39; ' const SWord8 s41 = s24 ? s20 : s40; ' const SWord8 s42 = s21 ? s17 : s41; ' const SWord8 s43 = s18 ? s14 : s42; ' const SWord8 s44 = s15 ? s11 : s43; & const SWord8 s45 = s12 ? s8 : s44; % const SWord8 s46 = s9 ? s5 : s45; % const SWord8 s47 = s6 ? s1 : s46; % const SWord8 s48 = s3 ? s0 : s47;   return s48;  }   experimentalerkokl@gmail.com Safe-InferedEGiven a 64-bit quantity, the simplest (and obvious) way to count the J number of bits that are set in it is to simply walk through all the bits K and add 1 to a running count. This is slow, as it requires 64 iterations, O but is simple and easy to convince yourself that it is correct. For instance: popCountSlow 0x0123456789ABCDEF 32 :: SWord8BFaster version. This is essentially the same algorithm, except we I go 8 bits at a time instead of one by one, by using a precomputed table : of population-count values for each byte. This algorithm loops only 8 8 times, and hence is at least 8 times more efficient. CLook-up table, containing population counts for all possible 8-bit + value, from 0 to 255. Note that we do not " hard-code" the values, but . merely use the slow version to compute them. JStates the correctness of faster population-count algorithm, with respect 8 to the reference slow version. (We use yices here as it's quite fast for 7 this problem. Z3 seems to take much longer.) We have: %proveWith yices fastPopCountIsCorrectQ.E.D.TNot only we can prove that faster version is correct, but we can also automatically X generate C code to compute population-counts for us. This action will generate all the K C files that you will need, including a driver program for test purposes. 'Below is the generated header file for : genPopCountInC%== BEGIN: "Makefile" ================E# Makefile for popCount. Automatically generated by SBV. Do not edit!=# include any user-defined .mk file in the current directory. -include *.mkCC=gcc0CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointerall: popCount_driver!popCount.o: popCount.c popCount.h ${CC} ${CCFLAGS} -c $< -o $@$popCount_driver.o: popCount_driver.c ${CC} ${CCFLAGS} -c $< -o $@-popCount_driver: popCount.o popCount_driver.o ${CC} ${CCFLAGS} $^ -o $@clean: rm -f *.overyclean: clean rm -f popCount_driver%== END: "Makefile" =================='== BEGIN: "popCount.h" ================ BLANKLINE  #%ifndef __popCount__HEADER_INCLUDED__  #%define __popCount__HEADER_INCLUDED__   BLANKLINE  #include  inttypes.h  #include  stdint.h  #include  stdbool.h   BLANKLINE typedef bool SBool;   BLANKLINE typedef uint8_t SWord8 ;  typedef uint16_t SWord16;  typedef uint32_t SWord32;  typedef uint64_t SWord64;   BLANKLINE typedef int8_t SInt8 ;  typedef int16_t SInt16;  typedef int32_t SInt32;  typedef int64_t SInt64;   BLANKLINE "SWord8 popCount(const SWord64 x);   BLANKLINE  #endif  == END:  popCount.h ==================  == BEGIN: popCount_driver.c ================  BLANKLINE  #include  inttypes.h  #include  stdint.h  #include  stdbool.h  #include  stdio.h  #include  popCount.h   BLANKLINE  int main(void)  { < const SWord8 __result = popCount(0x1b02e143e4f0e0e5ULL);   BLANKLINE  printf(#popCount(0x1b02e143e4f0e0e5ULL) = %PRIu8n , __result);   BLANKLINE  return 0;  }  == END: popCount_driver.c ==================  == BEGIN:  popCount.c ================  BLANKLINE  #include  inttypes.h  #include  stdint.h  #include  stdbool.h  #include  popCount.h   BLANKLINE " SWord8 popCount(const SWord64 x)  {  const SWord64 s0 = x;  static const SWord8 table0[] = { I 0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3, I 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, I 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2, I 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, I 3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, I 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3, I 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, I 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, I 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 2, 3, 3, 4, 3, 4, I 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, I 5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5, 0 5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8  };  const SWord64 s11 = s0 & 0x00000000000000ffULL; ! const SWord8 s12 = table0[s11];  const SWord64 s13 = s0 >> 8; - const SWord64 s14 = 0x00000000000000ffULL & s13; ! const SWord8 s15 = table0[s14]; " const SWord8 s16 = s12 + s15; ! const SWord64 s17 = s13 >> 8; - const SWord64 s18 = 0x00000000000000ffULL & s17; ! const SWord8 s19 = table0[s18]; " const SWord8 s20 = s16 + s19; ! const SWord64 s21 = s17 >> 8; - const SWord64 s22 = 0x00000000000000ffULL & s21; ! const SWord8 s23 = table0[s22]; " const SWord8 s24 = s20 + s23; ! const SWord64 s25 = s21 >> 8; - const SWord64 s26 = 0x00000000000000ffULL & s25; ! const SWord8 s27 = table0[s26]; " const SWord8 s28 = s24 + s27; ! const SWord64 s29 = s25 >> 8; - const SWord64 s30 = 0x00000000000000ffULL & s29; ! const SWord8 s31 = table0[s30]; " const SWord8 s32 = s28 + s31; ! const SWord64 s33 = s29 >> 8; - const SWord64 s34 = 0x00000000000000ffULL & s33; ! const SWord8 s35 = table0[s34]; " const SWord8 s36 = s32 + s35; ! const SWord64 s37 = s33 >> 8; - const SWord64 s38 = 0x00000000000000ffULL & s37; ! const SWord8 s39 = table0[s38]; " const SWord8 s40 = s36 + s39;   BLANKLINE  return s40;  }  == END:  popCount.c ==================   experimentalerkokl@gmail.com Safe-InferedEA definition of shiftLeft that can deal with variable length shifts.  (Note that the `(` method from the 3 class requires an " shift  amount.) Unfortunately, this',ll generate rather clumsy C code due to the G use of tables etc., so we uninterpret it for code generation purposes  using the z function. XTest function that uses shiftLeft defined above. When used as a normal Haskell function ] or in verification the definition is fully used, i.e., no uninterpretation happens. To wit,  we have: tstShiftLeft 3 4 5224 :: SWord32,prove $ \x y -> tstShiftLeft x y 0 .== x + yQ.E.D.Generate C code for  tstShiftLeft9. In this case, SBV will *use* the user given definition F verbatim, instead of generating code for it. (Also see the functions n, o,  and m.)   experimentalerkokl@gmail.com Safe-Infered-[The key schedule. AES executes in rounds, and it treats first and last round keys slightly b differently than the middle ones. We reflect that choice by being explicit about it in our type. Y The length of the middle list of keys depends on the key-size, which in turn determines  the number of rounds. XThe key, which can be 128, 192, or 256 bits. Represented as a sequence of 32-bit words. UAES state. The state consists of four 32-bit words, each of which is in turn treated  as four GF28'Is, i.e., 4 bytes. The T-Box implementation keeps the four-bytes together  for efficient representation. KAn element of the Galois Field 2^8, which are essentially polynomials with R maximum degree 7. They are conveniently represented as values between 0 and 255. MMultiplication in GF(2^8). This is simple polynomial multipliation, followed  by the irreducible polynomial x^8+x^5+x^3+x^1+1. We simply use the  0 function exported by SBV to do the operation. KExponentiation by a constant in GF(2^8). The implementation uses the usual 8 square-and-multiply trick to speed up the computation. IComputing inverses in GF(2^8). By the mathematical properties of GF(2^8) 0 and the particular irreducible polynomial used x^8+x^5+x^3+x^1+1, it N turns out that raising to the 254 power gives us the multiplicative inverse. ) Of course, we can prove this using SBV: :prove $ \x -> x ./= 0 ==> x `gf28Mult` gf28Inverse x .== 1Q.E.D.Note that we exclude 0' in our theorem, as it does not have a  multiplicative inverse. 5Conversion from 32-bit words to 4 constituent bytes. :Conversion from 4 bytes, back to a 32-bit row, inverse of  above. We H have the following simple theorems stating this relationship formally: Eprove $ \a b c d -> toBytes (fromBytes [a, b, c, d]) .== [a, b, c, d]Q.E.D.)prove $ \r -> fromBytes (toBytes r) .== rQ.E.D.5Rotating a state row by a fixed amount to the right. PDefinition of round-constants, as specified in Section 5.2 of the AES standard. The  InvMixColumnsE transformation, as described in Section 5.3.3 of the standard. Note c that this transformation is only used explicitly during key-expansion in the T-Box implementation  of AES. LKey expansion. Starting with the given key, returns an infinite sequence of B words, as described by the AES standard, Section 5.2, Figure 11. TThe values of the AES S-box table. Note that we describe the S-box programmatically V using the mathematical construction given in Section 5.1.1 of the standard. However, O the code-generation will turn this into a mere look-up table, as it is just a / constant table, all computation being done at " compile-time". LThe sbox transformation. We simply select from the sbox table. Note that we + are obliged to give a default value (here 0+) to be used if the index is out-of-bounds  as required by SBV's 1 function. However, that will never happen since ' the table has all 256 elements in it. PThe values of the inverse S-box table. Again, the construction is programmatic. "The inverse s-box transformation. Prove that the  and  are inverses. We have: prove sboxInverseCorrectQ.E.D.FAdding the round-key to the current state. We simply exploit the fact @ that addition is just xor in implementing this transformation. /T-box table generation function for encryption 'First look-up table used in encryption (Second look-up table used in encryption 'Third look-up table used in encryption (Fourth look-up table used in encryption /T-box table generating function for decryption 'First look-up table used in decryption (Second look-up table used in decryption 'Third look-up table used in decryption (Fourth look-up table used in decryption QGeneric round function. Given the function to perform one round, a key-schedule, 3 and a starting state, it performs the AES rounds. SOne encryption round. The first argument indicates whether this is the final round ? or not, in which case the construction is slightly different. JOne decryption round. Similar to the encryption round, the first argument 3 indicates whether this is the final round or not. OKey schedule. Given a 128, 192, or 256 bit key, expand it to get key-schedules P for encryption and decryption. The key is given as a sequence of 32-bit words. 6 (4 elements for 128-bits, 6 for 192, and 8 for 256.) HBlock encryption. The first argument is the plain-text, which must have D precisely 4 elements, for a total of 128-bits of input. The second @ argument is the key-schedule to be used, obtained by a call to . G The output will always have 4 32-bit words, which is the cipher-text. 3Block decryption. The arguments are the same as in  , except K the first argument is the cipher-text and the output is the corresponding  plain-text. @128-bit encryption test, from Appendix C.1 of the AES standard: map hex t128Enc-["69c4e0d8","6a7b0430","d8cdb780","70b4c55a"]@128-bit decryption test, from Appendix C.1 of the AES standard: map hex t128Dec-["00112233","44556677","8899aabb","ccddeeff"]@192-bit encryption test, from Appendix C.2 of the AES standard: map hex t192Enc-["dda97ca4","864cdfe0","6eaf70a0","ec0d7191"]@192-bit decryption test, from Appendix C.2 of the AES standard: map hex t192Dec-["00112233","44556677","8899aabb","ccddeeff"];256-bit encryption, from Appendix C.3 of the AES standard: map hex t256Enc-["8ea2b7ca","516745bf","eafc4990","4b496089"];256-bit decryption, from Appendix C.3 of the AES standard: map hex t256Dec-["00112233","44556677","8899aabb","ccddeeff"]<Correctness theorem for 128-bit AES. Ideally, we would run:    prove aes128IsCorrect \to get a proof automatically. Unfortunately, while SBV will successfully generate the proof g obligation for this theorem and ship it to the SMT solver, it would be naive to expect the SMT-solver d to finish that proof in any reasonable time with the currently available SMT solving technologies.  Instead, we can issue:    quickCheck aes128IsCorrect iand get some degree of confidence in our code. Similar predicates can be easily constructed for 192, and  256 bit cases as well. ,Code generation for 128-bit AES encryption. ^The following sample from the generated code-lines show how T-Boxes are rendered as C arrays:    static const SWord32 table1[] = { ? 0xc66363a5UL, 0xf87c7c84UL, 0xee777799UL, 0xf67b7b8dUL, ? 0xfff2f20dUL, 0xd66b6bbdUL, 0xde6f6fb1UL, 0x91c5c554UL, ? 0x60303050UL, 0x02010103UL, 0xce6767a9UL, 0x562b2b7dUL, ? 0xe7fefe19UL, 0xb5d7d762UL, 0x4dababe6UL, 0xec76769aUL,  ...  } hThe generated program has 5 tables (one sbox table, and 4-Tboxes), all converted to fast C arrays. Here 3 is a sample of the generated straightline C-code:   ) const SWord8 s1915 = (SWord8) s1912; % const SWord8 s1916 = table0[s1915]; , const SWord16 s1917 = (((SWord16) s1914) << 8) | ((SWord16) s1916); , const SWord32 s1918 = (((SWord32) s1911) << 16) | ((SWord32) s1917); ( const SWord32 s1919 = s1844 ^ s1918; ( const SWord32 s1920 = s1903 ^ s1919; yThe GNU C-compiler does a fine job of optimizing this straightline code to generate a fairly efficient C implementation. LComponents of the AES-128 implementation that the library is generated from EGenerate a C library, containing functions for performing 128-bit encdeckey-expansion. V A note on performance: In a very rough speed test, the generated code was able to do ` 6.3 million block encryptions per second on a decent MacBook Pro. On the same machine, OpenSSL ^ reports 8.2 million block encryptions per second. So, the generated code is about 25% slower ` as compared to the highly optimized OpenSSL implementation. (Note that the speed test was done W somewhat simplistically, so these numbers should be considered very rough estimates.) -plain-text words  key-words ,True if round-trip gives us plain-text back --- experimentalerkokl@gmail.com Safe-Infered :Represents the current state of the RC4 stream: it is the S array  along with the i and j index values used by the PRGA. The key is a stream of  values. HRC4 State contains 256 8-bit values. We use the symbolically accessible  full-binary type ) to represent the state, since RC4 needs 0 access to the array via a symbolic index and it'%s important to minimize access time. SConstruct the fully balanced initial tree, where the leaves are simply the numbers 0 through 255. %Swaps two elements in the RC4 array. [Implements the PRGA used in RC4. We return the new state and the next key value generated. AConstructs the state to be used by the PRGA using the given key. DThe key-schedule. Note that this function returns an infinite list. 1Generate a key-schedule from a given key-string. ERC4 encryption. We generate key-words and xor it with the input. The + following test-vectors are from Wikipedia  http://en.wikipedia.org/wiki/RC4: )concatMap hex $ encrypt "Key" "Plaintext""bbf316e8d940af0ad3"&concatMap hex $ encrypt "Wiki" "pedia" "1021bf0420"1concatMap hex $ encrypt "Secret" "Attack at dawn""45a01f645fc35b383552544b9bf5"XRC4 decryption. Essentially the same as decryption. For the above test vectors we have: Ddecrypt "Key" [0xbb, 0xf3, 0x16, 0xe8, 0xd9, 0x40, 0xaf, 0x0a, 0xd3] "Plaintext"-decrypt "Wiki" [0x10, 0x21, 0xbf, 0x04, 0x20]"pedia"edecrypt "Secret" [0x45, 0xa0, 0x1f, 0x64, 0x5f, 0xc3, 0x5b, 0x38, 0x35, 0x52, 0x54, 0x4b, 0x9b, 0xf5]"Attack at dawn" Prove that round-trip encryption/,decryption leaves the plain-text unchanged. T The theorem is stated parametrically over key and plain-text sizes. The expression U performs the proof for a 40-bit key (5 bytes) and 40-bit plaintext (again 5 bytes). QNote that this theorem is trivial to prove, since it is essentially establishing  xor'7in the same value twice leaves a word unchanged (i.e., x 0 y 0 y = x). R However, the proof takes quite a while to complete, as it gives rise to a fairly  large symbolic trace.     experimentalerkokl@gmail.com Safe-Infered SBV doesn'7t support 48 bit words natively. So, we represent them + as a tuple, 32 high-bits and 16 low-bits. GCompute the 16 bit CRC of a 48 bit message, using the given polynomial BCount the differing bits in the message and the corresponding CRC Given a hamming distance value hd,  returns true if E the 16 bit polynomial can distinguish all messages that has at most  hd> different bits. Note that we express this conversely: If the  sent and received- messages are different, then it must be the A case that that must differ from each other (including CRCs), in  more than hd bits. KGenerate good CRC polynomials for 48-bit words, given the hamming distance hd. bFind and display all degree 16 polynomials with hamming distance at least 4, for 48 bit messages.  When run, this function prints:    Polynomial #1. x^16 + x^2 + x + 1  Polynomial #2. x^16 + x^15 + x^2 + 1  Polynomial #3. x^16 + x^15 + x^14 + 1  Polynomial #4. x^16 + x^15 + x^2 + x + 1  Polynomial #5. x^16 + x^14 + x + 1  ... PNote that different runs can produce different results, depending on the random S numbers used by the solver, solver version, etc. (Also, the solver will take some P time to generate these results. On my machine, the first five polynomials were  generated in about 5 minutes.)  experimentalerkokl@gmail.com Safe-Infered\For a homogeneous problem, the solution is any linear combination of the resulting vectors. ] For a non-homogeneous problem, the solution is any linear combination of the vectors in the B second component plus one of the vectors in the first component. [ldn: Solve a (L)inear (D)iophantine equation, returning minimal solutions over (N)aturals. T The input is given as a rows of equations, with rhs values separated into a tuple. ^Find the basis solution. By definition, the basis has all non-trivial (i.e., non-0) solutions ` that cannot be written as the sum of two other solutions. We use the mathematically equivalent 0 statement that a solution is in the basis if it''s least according to the lexicographic . order using the ordinary less-than relation. Solve the equation:  2x + y - z = 2 We have: test2NonHomogeneous [[0,2,0],[1,0,0]] [[0,1,1],[1,0,2]]0which means that the solutions are of the form:  (0, 2, 0) + k (0, 1, 1) + k' (1, 0, 2) = (k' , 2+k, k+2k')OR  (1, 0, 0) + k (0, 1, 1) + k' (1, 0, 2) = (1+k' , k, k+2k')for arbitrary k, k'. It'.s easy to see that these are really solutions  to the equation given. It'3s harder to see that they cover all possibilities, 8 but a moments thought reveals that is indeed the case. TA puzzle: Five sailors and a monkey escape from a naufrage and reach an island with V coconuts. Before dawn, they gather a few of them and decide to sleep first and share Y the next day. At night, however, one of them awakes, counts the nuts, makes five parts, T gives the remaining nut to the monkey, saves his share away, and sleeps. All other b sailors do the same, one by one. When they all wake up in the morning, they again make 5 shares, [ and give the last remaining nut to the monkey. How many nuts were there at the beginning? 8We can model this as a series of diophantine equations:    x_0 = 5 x_1 + 1  4 x_1 = 5 x_2 + 1  4 x_2 = 5 x_3 + 1  4 x_3 = 5 x_4 + 1  4 x_4 = 5 x_5 + 1  4 x_5 = 5 x_6 + 1 >We need to find to solve for x_0, over the naturals. We have: sailors%[15621,3124,2499,1999,1599,1279,1023] That is:   ) * There was a total of 15621 coconuts @ * 1st sailor: 15621 = 3124*5+1, leaving 15621-3124-1 = 12496 @ * 2nd sailor: 12496 = 2499*5+1, leaving 12496-2499-1 = 9996 @ * 3rd sailor: 9996 = 1999*5+1, leaving 9996-1999-1 = 7996 @ * 4th sailor: 7996 = 1599*5+1, leaving 7996-1599-1 = 6396 @ * 5th sailor: 6396 = 1279*5+1, leaving 6396-1279-1 = 5116 0 * In the morning, they had: 5116 = 1023*5+1. MNote that this is the minimum solution, that is, we are guaranteed that there's B no solution with less number of coconuts. In fact, any member of [15625*k-4 | k <- [1..]]  is a solution, i.e., so are 31246, 46871, 62496, 78121, etc.  experimentalerkokl@gmail.com Safe-InferedXHelper synonym for representing GF(2^8); which are merely 8-bit unsigned words. Largest ) term in such a polynomial has degree 7. Multiplication in Rijndael'?s field; usual polynomial multiplication followed by reduction A by the irreducible polynomial. The irreducible used by Rijndael's field is the polynomial  x^8 + x^4 + x^3 + x + 1, which we write by giving it's  exponents in SBV.  See:  Nhttp://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field. H Note that the irreducible itself is not in GF28! It has a degree of 8. NB. You can use the G function to print polynomials nicely, as a mathematician would write.  States that the unit polynomial 1, is the unit element *States that multiplication is commutative CStates that multiplication is associative, note that associativity $ proofs are notoriously hard for SAT/ SMT solvers IStates that the usual multiplication rule holds over GF(2^n) polynomials  Checks:    if (a, b) = x  y then x = y  a + b being careful about y = 0&. When divisor is 0, then quotient is 5 defined to be 0 and the remainder is the numerator.  (Note that addition is simply 0 in GF(2^8).) Queries  experimentalerkokl@gmail.com Safe-Infered RWe will represent coins with 16-bit words (more than enough precision for coins). RCreate a coin. The argument Int argument just used for naming the coin. Note that Q we constrain the value to be one of the valid U.S. coin values as we create it. 1Return all combinations of a sequence of values. /Constraint 1: Cannot make change for a dollar. 4Constraint 2: Cannot make change for half a dollar. 0Constraint 3: Cannot make change for a quarter. -Constraint 4: Cannot make change for a dime. .Constraint 5: Cannot make change for a nickel /Constraint 6: Cannot buy the candy either. Here',s where we need to have the extra knowledge 6 that the vending machines do not take 50 cent coins. Solve the puzzle. We have: puzzleSatisfiable. Model: c1 = 50 :: SWord16 c2 = 25 :: SWord16 c3 = 10 :: SWord16 c4 = 10 :: SWord16 c5 = 10 :: SWord16 c6 = 10 :: SWord16=i.e., your friend has 4 dimes, a quarter, and a half dollar.     experimentalerkokl@gmail.com Safe-InferedZWe will assume each number can be represented by an 8-bit word, i.e., can be at most 128. PGiven a number, increment the count array depending on the digits of the number AEncoding of the puzzle. The solution is a sequence of 10 numbers E for the occurrences of the digits such that if we count each digit,  we find these numbers. 7Finds all two known solutions to this puzzle. We have: counts Solution #1In this sentence, the number of occurrences of 0 is 1, of 1 is 11, of 2 is 2, of 3 is 1, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 1, of 8 is 1, of 9 is 1. Solution #2In this sentence, the number of occurrences of 0 is 1, of 1 is 7, of 2 is 3, of 3 is 2, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 2, of 8 is 1, of 9 is 1.Found: 2 solution(s). experimentalerkokl@gmail.com Safe-InferedPrints the only solution: puzzle Solution #1: dog = 3 :: SInteger cat = 41 :: SInteger mouse = 56 :: SIntegerThis is the only solution. experimentalerkokl@gmail.com Safe-InferedJThe given guesses and the correct digit counts, encoded as a simple list. @Encode the problem, note that we check digits are within 0-9 as M we use 8-bit words to represent them. Otherwise, the constraints are simply P generated by zipping the alleged solution with each guess, and making sure the % number of matching digits match what'"s given in the problem statement. (Print out the solution nicely. We have:  solveEuler1854640261571849533Number of solutions: 1 experimentalerkokl@gmail.com Safe-Infered#The puzzle board is a list of rows A row is a list of elements Use 32-bit words for elements. 5Checks that all elements in a list are within bounds $Get the diagonal of a square matrix (Test if a given board is a magic square 3Group a list of elements in the sublists of length i Given n, magic n prints all solutions to the nxn magic square problem  experimentalerkokl@gmail.com Safe-InferedFA solution is a sequence of row-numbers where queens should be placed  Checks that a given solution of n!-queens is valid, i.e., no queen  captures any other. Given n, it solves the n-queens* puzzle, printing all possible solutions.  experimentalerkokl@gmail.com Safe-InferedDA puzzle is a pair: First is the number of missing elements, second F is a function that given that many elements returns the final board. 'A Sudoku board is a sequence of 9 rows ]A row is a sequence of 8-bit words, too large indeed for representing 1-9, but does not harm =Given a series of elements, make sure they are all different * and they all are numbers between 1 and 9 2Given a full Sudoku board, check that it is valid +Solve a given puzzle and print the results UHelper function to display results nicely, not really needed, but helps presentation Find all solutions to a puzzle Find an arbitrary good board )A random puzzle, found on the internet.. /Another random puzzle, found on the internet.. /Another random puzzle, found on the internet.. ,According to the web, this is the toughest 7 sudoku puzzle ever.. It even has a name: Al Escargot:   Jhttp://zonkedyak.blogspot.com/2006/11/worlds-hardest-sudoku-puzzle-al.html 0This one has been called diabolical, apparently (The following is nefarious according to   %http://haskell.org/haskellwiki/Sudoku GSolve them all, this takes a fraction of a second to run for each case  experimentalerkokl@gmail.com Safe-Infered#LA move action is a sequence of triples. The first component is symbolically P True if only one member crosses. (In this case the third element of the triple S is irrelevant.) If the first component is (symbolically) False, then both members  move together 0A puzzle move is modeled as a state-transformer )The status of the puzzle after each move  elapsed time  location of the flash  location of Bono  location of Edge  location of Adam  location of Larry Location of the flash Each member gets an 8-bit id Model time using 32 bits U2 band members Bono's ID Edge's ID Adam's ID Larry's ID Is this a valid person? +Crossing times for each member of the band (We represent this side of the bridge as , and arbitrarily as  )We represent other side of the bridge as , and arbitrarily as  8Start configuration, time elapsed is 0 and everybody is  (Read the state via an accessor function  /Given an arbitrary member, return his location !)Transferring the flash to the other side "(Transferring a person to the other side #1Increment the time, when only one person crosses $3Increment the time, when two people cross together %Symbolic version of when &/Move one member, remembering to take the flash ''Move two members, again with the flash (!Run a sequence of given actions. )CCheck if a given sequence of actions is valid, i.e., they must all E cross the bridge according to the rules and in less than 17 seconds *.See if there is a solution that has precisely n steps +HSolve the U2-bridge crossing puzzle, starting by testing solutions with 9 increasing number of steps, until we find one. We have: solveU2#Checking for solutions with 1 move.$Checking for solutions with 2 moves.$Checking for solutions with 3 moves.$Checking for solutions with 4 moves.$Checking for solutions with 5 moves. Solution #1:  0 --> Edge, Bono 2 <-- Edge 4 --> Larry, Adam 14 <-- Bono15 --> Edge, BonoTotal time: 17 Solution #2:  0 --> Edge, Bono 2 <-- Bono 3 --> Larry, Adam 13 <-- Edge15 --> Edge, BonoTotal time: 17 Found: 2 solutions with 5 moves..Finding all possible solutions to the puzzle. +      !"#$%&'()*+89:(      !"#$%&'()*+(      !"#$%&'()*+       !"#$%&'()*+89: experimentalerkokl@gmail.com Safe-Infered,NThis version directly uses SMT-arrays and hence does not need an initializer. E Reading an element before writing to it returns an arbitrary value. -7The array type, takes symbolic 32-bit unsigned indexes 7 and stores 32-bit unsigned symbolic values. These are 7 functional arrays where reading before writing a cell  throws an exception. .&Uninterpreted function in the theorem /3Correctness theorem. We state it for all values of x, y, and  the array a7. We also take an arbitrary initializer for the array. 0$Prints Q.E.D. when run, as expected  proveThm1Q.E.D.1Same as /, except we don't need an initializer with the  model. 2%Prints Q.E.D. when run, as expected:  proveThm2Q.E.D.,-./012,-./012-./0,12,-./012 experimentalerkokl@gmail.com Safe-Infered 34Handy shortcut for the type of symbolic values over 4 4The uninterpreted sort 4 , corresponding to the carrier. 6!Uninterpreted logical connective 6 7!Uninterpreted logical connective 7 8!Uninterpreted logical connective 8 97Distributivity of OR over AND, as an axiom in terms of : the uninterpreted functions we have introduced. Note how - variables range over the uninterpreted sort 4. :One of De Morgan'#s laws, again as an axiom in terms * of our uninterpeted logical connectives. ;-Double negation axiom, similar to the above. <Proves the equivalence >NOT (p OR (q AND r)) == (NOT p AND NOT q) OR (NOT p AND NOT r), = following from the axioms we have specified above. We have: testQ.E.D. 3456789:;<;< 3456789:;< 4536789:;< 3456789:;<;< experimentalerkokl@gmail.com Safe-Infered=An uninterpreted function > Asserts that f x z == f (y+2) z whenever x == y+2. Naturally correct:  prove thmGoodQ.E.D.? Asserts that f0 is commutative; which is not necessarily true! C Indeed, the SMT solver returns a counter-example function that is A not commutative. (Note that we have to use Yices as Z3 function 9 counterexamples are not yet supported by sbv.) We have: *proveWith yices $ forAll ["x", "y"] thmBadFalsifiable. Counter-example: x = 0 :: SWord8 y = 128 :: SWord8 -- uninterpreted: f f 128 0 = 32768 f _ _ = 0%Note how the counterexample function f+ returned by Yices violates commutativity; A thus providing evidence that the asserted theorem is not valid. =>?=>?=>?=>? experimentalerkokl@gmail.com Safe-Infered@BA new data-type that we expect to use in an uninterpreted fashion , in the backend SMT solver. Note the custom deriving clause, which ( takes care of most of the boilerplate. B3Declare an uninterpreted function that works over Q's CFA satisfiable example, stating that there is an element of the domain  @ such that B; returns a different element. Note that this is valid only  when the domain @% has at least two elements. We have: t1Satisfiable. Model: x = Q!val!0 :: QDDThis is a variant on the first example, except we also add an axiom ' for the sort, stating that the domain @$ has only one element. In this case / the problem naturally becomes unsat. We have: t2 Unsatisfiable=We need  and C$ instances, but default definitions C are always sufficient for uninterpreted sorts, so all we do is to C declare them as such. Note that, starting with GHC 7.6.1, we will 6 be able to simply derive these classes as well. (See  /http://hackage.haskell.org/trac/ghc/ticket/5462.) @ABCD>=@ABCD@ABCD@ABCD>=? 6 7 8 9 : ; < = > ? @ A B C D E!F"G"H"I"J"K"L"M"N"O"P"Q"R"S"T"U"V"W"X"Y"Z"["\"]"^"_"`"a"b"c"d"e"f"g"h"i"j"k"l"m"n"o"p"q"r"r"s"t"u"v"w"x"y"z"{"|"}"~"""""""""""""""""###########################$$&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&''''''((()))))))****+++++++++++,,,,- - - - - ---................... .!.!.".#.$.%.&.&.'.(.).*.+.,.-.../.0.142434445464748494:4;4<4=4>4?4@4A4B4C4D4E4F4G4H4I4J4K4L4M5N5O5P5Q5R5S5T5U5VWXYZ[\]^_`abbcdefghijklmnopqrstuvwxyz{|}~                                                                     !"#$%&'()**+,-./0123456789:;<=>?@AvBCDEFGHIJKLMNOPQRMMSTUVWXOYZ[[O\]^_`abcdefghijkSjkTjkljkm n!o!p!q!r!s!t!u!v!w!x!y!z!{!|"}"~"""""""""""j""""""""""""""""""""""""""""""""""""}"""G"H"w"""""""""a"""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""####gh#### # # # # ##gh#################### #!%"%#j$%j$&j'(j$)j*+g,-g,.gh/g,0g,1j23j24gh5j26j27gh8&9&:&;&<&=&>&?&@&A&B&C&D&E&F&G&H&I&J&K&L&M&N&O&P&Q&R&S&T&U&V&W&X&Y&Z&[&\&]&^&_&`&a&b&c&d&e&f&g&h&i&j&k&l&m&n&o&p&q&r&s&t&u&v&w&x&y&z&{&|&}&~&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&''''''''''''''''(((((((()))))))))))))))*++++++++jj,j................................................./"/#0000"0 1 1 1 1g11 2:3;4444444444444444444 4!4"4#4$j%&j%'j%(j%)j$*j$+j,-j,.j,/j,0j,1j23j24j25j26j27j28j29j2:j2;j2<j2=j2>j2?j2@j2Aj2Bj2Cj2Dj$Ej$Fj$GHIJKLMNOPsbv-2.2Data.SBVData.SBV.Internals&Data.SBV.Examples.BitPrecise.BitTricks#Data.SBV.Examples.BitPrecise.Legato&Data.SBV.Examples.BitPrecise.MergeSort&Data.SBV.Examples.BitPrecise.PrefixSum'Data.SBV.Examples.CodeGeneration.AddSub)Data.SBV.Examples.CodeGeneration.CRC_USB5*Data.SBV.Examples.CodeGeneration.Fibonacci$Data.SBV.Examples.CodeGeneration.GCD0Data.SBV.Examples.CodeGeneration.PopulationCount.Data.SBV.Examples.CodeGeneration.UninterpretedData.SBV.Examples.Crypto.AESData.SBV.Examples.Crypto.RC4,Data.SBV.Examples.Existentials.CRCPolynomial*Data.SBV.Examples.Existentials.Diophantine)Data.SBV.Examples.Polynomials.PolynomialsData.SBV.Examples.Puzzles.Coins Data.SBV.Examples.Puzzles.Counts%Data.SBV.Examples.Puzzles.DogCatMouse"Data.SBV.Examples.Puzzles.Euler185%Data.SBV.Examples.Puzzles.MagicSquare!Data.SBV.Examples.Puzzles.NQueens Data.SBV.Examples.Puzzles.Sudoku"Data.SBV.Examples.Puzzles.U2Bridge#Data.SBV.Examples.Uninterpreted.AUF&Data.SBV.Examples.Uninterpreted.Deduce(Data.SBV.Examples.Uninterpreted.Function$Data.SBV.Examples.Uninterpreted.SortData.SBV.Utils.TDiffData.SBV.Utils.LibData.SBV.Utils.BooleanData.SBV.BitVectors.AlgRealsData.SBV.BitVectors.DataData.SBV.Compilers.CodeGenData.SBV.Tools.ExpectedValueData.SBV.SMT.SMTLib1Data.SBV.BitVectors.ModelData.SBV.BitVectors.PrettyNumData.SBV.BitVectors.SignCastData.SBV.BitVectors.SplittableData.SBV.BitVectors.STreeData.SBV.Tools.PolynomialData.SBV.Compilers.CData.SBV.Tools.GenTestData.SBV.SMT.SMTData.SBV.SMT.SMTLib2Data.SBV.SMT.SMTLibData.SBV.Provers.SExprData.SBV.Provers.YicesData.SBV.Provers.Z3Data.SBV.Provers.ProverData.SBV.Tools.OptimizeBooleantruefalsebnot&&&|||~&~|<+>==><=>fromBoolbAndbOrbAnybAllAlgReal SFunArraySArraySymArray newArray_newArray readArray resetArray writeArray mergeArraysSymWordforallforall_ mkForallVarsexistsexists_ mkExistVarsfreefree_ mkFreeVarssymbolic symbolicsliteral unliteralfromCW isConcrete isSymbolic isConcretely mbMaxBound mbMinBound mkSymWordoutputSymbolicSRealSIntegerSInt64SInt32SInt16SInt8SWord64SWord32SWord16SWord8SBoolSBV SBVRunModeConcreteCodeGenProofResultHasKindkindOfhasSign intSizeOf isBoundedisReal isIntegerisUninterpretedshowTypeKindKUninterpretedKReal KUnboundedKBoundedCWcwKindcwValcwToBool mkConstCWaddAxiom runSymbolic runSymbolic' mkSFunArray CgPgmKindCgDriverCgSourceCgHeader CgMakefile CgPgmBundle CgSRealType CgLongDoubleCgDoubleCgFloat SBVCodeGen cgPerformRTCs cgIntegerSize cgSRealTypecgGenerateDrivercgGenerateMakefilecgSetDriverValuescgAddPrototype cgAddDecl cgAddLDFlagscgInput cgInputArrcgOutput cgOutputArrcgReturn cgReturnArrexpectedValueWith expectedValue Uninterpreted uninterpret cgUninterpretsbvUninterpret Mergeable symbolicMergeiteselect BVDivisible bvQuotRemSNum OrdSymbolic.<.>=.>.<=sminsmax EqSymbolic.==./=genVargenVar_sBoolsBoolssWord8sWord8ssWord16sWord16ssWord32sWord32ssWord64sWord64ssInt8sInt8ssInt16sInt16ssInt32sInt32ssInt64sInt64ssInteger sIntegerssRealsRealstoSReal allDifferentallEqualoneIf sbvTestBit sbvPopCountsetBitToblastLEblastBElsbmsb constrain pConstrainslet PrettyNumhexSbinShexbinreadBinSignCastsignCast unsignCastFromBits fromBitsLE fromBitsBE Splittablesplit#extendSTree readSTree writeSTreemkSTree Polynomial polynomialpAddpMultpDivpModpDivModshowPolyshowPolynomialcrcBVcrc compileToC compileToC' compileToCLibcompileToCLib' TestStyleForteCHaskell TestVectors getTestValuesgenTest renderTest Modelable modelExistsgetModel extractModelSatModelparseCWscvtModel AllSatResult SatResult ThmResult SMTResultTimeOut ProofErrorUnknown Satisfiable Unsatisfiable SMTSolvername executableoptionsengine SMTConfigverbosetimingtimeOut printBase printRealPrec solverTweakssmtFile useSMTLib2solver extractModels displayModelsEquality===ProvableforAll_forAllforSome_forSome Predicateyicesz3 defaultSMTCfgprovesatsolveallSat isVacuousisTheoremWithinisSatisfiableWithin isTheorem isSatisfiablenumberOfModelscompileToSMTLibgenerateSMTBenchmarks proveWithsatWith isVacuousWith allSatWithsbvCheckSolverInstallation OptimizeOpts Quantified Iterative optimizeWithoptimize maximizeWithmaximize minimizeWithminimizefastMinCorrectfastMaxCorrectoppositeSignsCorrectconditionalSetClearCorrectpowerOfTwoCorrectqueriesModelInitVals InstructionProgramExtractMostekmemory registersflagsMemoryFlags RegistersBitValueFlagFlagZFlagCRegisterRegARegXAddressgetRegsetReggetFlagsetFlagpeekpoke checkOverflowcheckOverflowCorrectldxldaclcrorMrorRbccadcdexbneendlegato runLegato initMachinelegatoIsCorrectcorrectnessTheorem legatoInCEmerge mergeSort nonDecreasingisPermutationOf correctnesscodeGen PowerListtiePLzipPLunzipPLpslf flIsCorrectthm1thm2thm3genPrefixSumInstance prefixSumladnerFischerTrace scanlTraceaddSub genAddSubusb5crcUSBcrcUSB'crcGoodcg1cg2fib0fib1genFib1fib2genFib2sgcd sgcdIsCorrect genGCDInC popCountSlow popCountFastpop8fastPopCountIsCorrectgenPopCountInC shiftLeft tstShiftLeftgenCCodeKSKeyStateGF28gf28Multgf28Pow gf28InversetoBytes fromBytesrotRroundConstants invMixColumns keyExpansion sboxTablesbox unSBoxTableunSBoxsboxInverseCorrect addRoundKeyt0Funct0t1t2t3u0Funcu0u1u2u3doRoundsaesRound aesInvRoundaesKeySchedule aesEncrypt aesDecryptt128Enct128Dect192Enct192Dect256Enct256Decaes128IsCorrectcgAES128BlockEncryptaes128LibComponentscgAES128LibraryRC4SinitSswapprgainitRC4 keySchedulekeyScheduleStringencryptdecrypt rc4IsCorrectSWord48 crc_48_16 diffCountgenPolyfindHD4PolynomialsSolutionNonHomogeneous Homogeneousldnbasistestsailors<*>multUnitmultComm multAssoc polyDivModtestGF28CoinmkCoin combinationsc1c2c3c4c5c6puzzleCountcountcountsguesseseuler185 solveEuler185BoardRowElemcheckdiagisMagicchunkmagicisValidnQueensPuzzlevalidsudoku dispSolutionsolveAllpuzzle0puzzle1puzzle2puzzle3puzzle4puzzle5puzzle6 allPuzzlesActionsMoveStatustimeflashlBonolEdgelAdamlLarryLocation SU2MemberTimeU2MemberLarryAdamEdgeBonobonoedgeadamlarry isU2Member crossTimeheretherestartwhereIs xferFlash xferPerson bumpTime1 bumpTime2whenSmove1move2runsolveNsolveU2BAf proveThm1 proveThm2SBandornotax1ax2ax3thmGoodthmBadQtimeIfdeepseq-1.3.0.0Control.DeepSeqNFDatamlift2mlift3mlift4mlift5mlift6mlift7mlift8ghc-prim GHC.TypesBoolbaseGHC.Listanyall $fBooleanBool mkPolyRealalgRealToSMTLib2algRealToHaskell mergeAlgReals AlgPolyRoot AlgRational$fRandomAlgReal $fRandomRatio$fFractionalAlgReal $fNumAlgReal $fOrdAlgReal $fEqAlgReal $fShowAlgReal$fShowPolynomial SMTLibPgm SMTLibVersion Outputtable ArrayInfo ArrayContext ArrayMerge ArrayMutate ArrayReset ArrayFree UnintKind NamedSymVarPgm Data.DataDataSBVExprOpSBVType QuantifierSWNodeIdCWValCWUninterpreted CWInteger CWAlgReal cwSameTypecwIsBitneedsExistentialsfalseSWtrueSWfalseCWtrueCWliftCW2mapCWmapCW2getConstraints getTraceInfo unintFnUIKind arrayUIKind inProofModenewUninterpreted getTableIndexnewExprsbvToSWmkSymSBV sbvToSymSW addConstraintcacheuncache uncacheAISMTLib2SMTLib1UArrUFunSBVAppArrReadArrEqLkUpJoinRorRolShrShlNotXOrOrAndIte GreaterEqLessEq GreaterThanLessThanNotEqualEqualRemQuotMinusTimesPlusEXALL $fNFDataSBV$fNFDataCached$fNFDataUnintKind$fNFDataSBVType$fNFDataQuantifier$fNFDataSBVExpr $fNFDataSW$fNFDataArrayContext $fNFDataKind$fNFDataResult $fNFDataCW$fShowSMTLibPgm$fNFDataSMTLibPgm$fNFDataSMTLibVersion$fShowSFunArray$fSymArraySArray $fShowSArray $fRandomSBV$fOutputtable(,,,,,,,)$fOutputtable(,,,,,,)$fOutputtable(,,,,,)$fOutputtable(,,,,)$fOutputtable(,,,)$fOutputtable(,,)$fOutputtable(,)$fOutputtable()$fOutputtable[]$fOutputtableSBV $fHasKindSBV$fEqSBV $fShowSBV$fShowArrayContext $fShowResult $fShowSBVExpr$fShowOp$fShowSW$fShowCW $fHasKindSW $fHasKindCW$fHasKindAlgReal$fHasKindInteger$fHasKindWord64$fHasKindInt64$fHasKindWord32$fHasKindInt32$fHasKindWord16$fHasKindInt16$fHasKindWord8 $fHasKindInt8 $fHasKindBool $fShowSBVType $fShowKindCgStateCgValCgConfigcgRTCTrue cgIntegercgReal cgDriverVals cgGenDriver cgGenMakefileCgTargetdefaultCgConfig initCgState liftSymbolic cgSBVToSWFalse isCgDriver isCgMakefilerenderCgPgmBundlerender'cgInputs cgOutputs cgReturns cgPrototypescgDecls cgLDFlags cgFinalConfigCgArrayCgAtomic targetName translate$fShowCgPgmBundle$fShowCgSRealTypeaddNonEqConstraintscvtGHC.RealIntegralRealGHC.EnumEnumquotRemGHC.NumNum GHC.ClassesEqOrdOrderingmaxmin Data.BitstestBitpopCountIntsetBitclearBitDouble$fTestableSymbolic $fTestableSBV$fUninterpreted(->)$fUninterpreted(->)0$fUninterpreted(->)1$fUninterpreted(->)2$fUninterpreted(->)3$fUninterpreted(->)4$fUninterpreted(->)5$fUninterpreted(->)6$fUninterpreted(->)7$fUninterpreted(->)8$fUninterpreted(->)9$fUninterpreted(->)10$fUninterpreted(->)11$fUninterpretedSBV$fMergeableSFunArray$fSymArraySFunArray$fMergeableSArray$fEqSymbolicSArray $fBoundedSBV$fMergeable(,,,,,,)$fMergeable(,,,,,)$fMergeable(,,,,)$fMergeable(,,,)$fMergeable(,,)$fMergeable(,)$fMergeable(->)$fMergeableArray$fMergeableEither$fMergeableMaybe $fMergeable[] $fMergeable()$fMergeableSBV$fArbitrarySBV$fArbitrarySFunArray$fBVDivisibleSBV$fBVDivisibleSBV0$fBVDivisibleSBV1$fBVDivisibleSBV2$fBVDivisibleSBV3$fBVDivisibleSBV4$fBVDivisibleSBV5$fBVDivisibleSBV6$fBVDivisibleSBV7$fBVDivisibleCW$fBVDivisibleInteger$fBVDivisibleInt8$fBVDivisibleWord8$fBVDivisibleInt16$fBVDivisibleWord16$fBVDivisibleInt32$fBVDivisibleWord32$fBVDivisibleInt64$fBVDivisibleWord64 $fEnumSBV $fBitsSBV$fFractionalSBV$fNumSBV $fBooleanSBV $fSNumSBV $fSNumSBV0 $fSNumSBV1 $fSNumSBV2 $fSNumSBV3 $fSNumSBV4 $fSNumSBV5 $fSNumSBV6 $fSNumSBV7$fOrdSymbolic(,,,,,,)$fEqSymbolic(,,,,,,)$fOrdSymbolic(,,,,,)$fEqSymbolic(,,,,,)$fOrdSymbolic(,,,,)$fEqSymbolic(,,,,)$fOrdSymbolic(,,,)$fEqSymbolic(,,,)$fOrdSymbolic(,,)$fEqSymbolic(,,)$fOrdSymbolic(,)$fEqSymbolic(,)$fOrdSymbolicEither$fEqSymbolicEither$fOrdSymbolicMaybe$fEqSymbolicMaybe$fOrdSymbolic[]$fEqSymbolic[]$fEqSymbolicBool$fOrdSymbolicSBV$fEqSymbolicSBV$fSymWordAlgReal$fSymWordInteger$fSymWordInt64$fSymWordWord64$fSymWordInt32$fSymWordWord32$fSymWordInt16$fSymWordWord16 $fSymWordInt8$fSymWordWord8 $fSymWordBoolshexshexIsbinsbinI$fPrettyNumSBV $fPrettyNumCW$fPrettyNumInteger$fPrettyNumInt64$fPrettyNumWord64$fPrettyNumInt32$fPrettyNumWord32$fPrettyNumInt16$fPrettyNumWord16$fPrettyNumInt8$fPrettyNumWord8$fPrettyNumBool$fSignCastSBVSBV$fSignCastSBVSBV0$fSignCastSBVSBV1$fSignCastSBVSBV2$fSignCastWord8Int8$fSignCastWord16Int16$fSignCastWord32Int32$fSignCastWord64Int64 $fFromBitsSBV$fFromBitsSBV0$fFromBitsSBV1$fFromBitsSBV2$fFromBitsSBV3$fFromBitsSBV4$fFromBitsSBV5$fFromBitsSBV6$fFromBitsSBV7$fSplittableSBVSBV$fSplittableSBVSBV0$fSplittableSBVSBV1$fSplittableWord16Word8$fSplittableWord32Word16$fSplittableWord64Word32$fMergeableSTreeInternal$fPolynomialSBV$fPolynomialSBV0$fPolynomialSBV1$fPolynomialSBV2$fPolynomialWord64$fPolynomialWord32$fPolynomialWord16$fPolynomialWord8 Data.MaybeJustNothing$fCgTargetSBVToCGHC.ShowShow SMTScript scriptBody scriptModelSMTModel SMTEngine resultConfiggenParse parseModelOut showSMTResult showModelshCWshUIshUA pipeProcessstandardSolver runSolverprocess-1.1.0.1System.ProcessreadProcessWithExitCode mergeSExpr modelAssocs modelArraysmodelUninterps$fModelableSMTResult$fModelableSatResult$fModelableThmResult$fSatModel(,,,,,,)$fSatModel(,,,,,)$fSatModel(,,,,)$fSatModel(,,,)$fSatModel(,,) $fSatModel(,) $fSatModel[]$fSatModelAlgReal$fSatModelInteger$fSatModelInt64$fSatModelWord64$fSatModelInt32$fSatModelWord32$fSatModelInt16$fSatModelWord16$fSatModelInt8$fSatModelWord8$fSatModelBool $fSatModel()$fShowAllSatResult$fShowSatResult$fShowThmResult$fNFDataSMTModel$fNFDataSMTResultSMTLibConverter toSMTLib1 toSMTLib2interpretSolverOutputSExpr parseSExprSAppSCon$fEquality(->)$fEquality(->)0$fEquality(->)1$fEquality(->)2$fEquality(->)3$fEquality(->)4$fEquality(->)5$fEquality(->)6$fEquality(->)7$fEquality(->)8$fEquality(->)9$fEquality(->)10$fEquality(->)11$fProvable(->)$fProvable(->)0$fProvable(->)1$fProvable(->)2$fProvable(->)3$fProvable(->)4$fProvable(->)5$fProvable(->)6 $fProvableSBV$fProvableSymbolicGHC.IntInt8Int16Int32Int64RatioRationalGHC.WordWordWord8Word16Word32Word64 Data.RatioapproxRationalrotateRrotateL unsafeShiftRshiftR unsafeShiftLshiftLisSignedbitSize complementBitbitrotateshift complementxor.|..&.Bits denominator numerator%$fMergeableMostek$fSatModelU2Member$fMergeableStateT$fMergeableStatus $fHasKindB $fSymWordB $fSymWordQ $fHasKindQ