ۃV      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                   !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUQportable experimentalerkokl@gmail.comVWXYZVWXYZVYXWWXYZportable experimentalerkokl@gmail.com[\"If selected, runs the computation m, and prints the time it took 5 to run it. The return type should be an instance of ] to ensure & the correct elapsed time is printed. \\portable experimentalerkokl@gmail.com^_`abc^_`abc^_`abcportable experimentalerkokl@gmail.com7A Test-suite, parameterized by the gold-check generator/checker  Wrap over #, avoids exporting the constructor )Checks that a particular result shows as s 'Run an IO computation and check that it's result shows as s %Create a gold file for the test case defghijkportable experimentalerkokl@gmail.comThe # class: a generalization of Haskell's l type  Haskell l 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 m Generalization of n Generalization of o Generalization of p     portable experimentalerkokl@gmail.comqrs+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 tu+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 vFlat arrays of symbolic values  An  array a b! is an array indexed by the type 54 a, with elements of type 54 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. 9Minimal complete definiton: free, free_, literal, fromCW Create a user named input !$Create an automatically named input "Get a bunch of new words #$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? wPMark an interim result as an output. Useful when constructing Symbolic programs O that return multiple values, or when the result is programmatically computed. )*CA 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. x+64-bit signed symbolic value, 2's complement representation ,32-bit signed symbolic value, 2's complement representation -16-bit signed symbolic value, 2's complement representation .8-bit signed symbolic value, 2's complement representation /64-bit unsigned symbolic value 032-bit unsigned symbolic value 116-bit unsigned symbolic value 28-bit unsigned symbolic value 3A symbolic boolean/bit 4The 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. 5yz{|}~6)Result of running a symbolic computation : pairs array names and uninterpreted constants with their kinds * used mainly for printing counterexamples $ pairs symbolic words and user given/automatically generated names 'A program is a sequence of assignments 77- represents a concrete word of a fixed size: * Endianness is mostly irrelevant (see the FromBits class). K For signed words, the most significant digit is considered to be the sign 89SAdd a user specified axiom to the generated SMT-Lib file. Note that the input is a 9 mere string; we perform no checking on the input that it's well-formed or is sensical. @ A separate formalization of SMT-Lib would be very useful here. :(Run a symbolic computation and return a 6 HRun a symbolic computation, and return a extra value paired up with the 6 ;:Make a constant fun-array always returning a fixed value. > Useful for creating arrays in a pure context. (Otherwise use .) sstv !"#$%&'(w)*+,-./012345y6789:;ssttvv !"#$%&'( !"#$%&'(w))*+,-./0123455y6789:;portable experimentalerkokl@gmail.com1<DUninterpreted 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. =TUninterpret 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. >PUninterpret a value, but also get a handle to the resulting object. This handle 1 can be used to add axioms for this object. (See 9.) ?DAn uninterpreted function handle. This is the handle to be used for , adding axioms about uninterpreted constants/functions. Note that 1 we will leave this abstract for safety purposes @4Symbolic choice operator, parameterized via a class  C1 is a total-indexing function, with the default. Minimal complete definition: A A(Merge two values based on the condition B9Choose one or the other element, based on the condition.  This is similar to A, but it has a default " implementation that makes sure it')s short-cut if the condition is concrete CTotal indexing operation. select xs default index is intuitively  the same as  xs !! index, except it evaluates to default if index  overflows DThe D2 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 D 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 E 0 = (0, x)5Note that our instances implement this law even when x is 0 itself. Minimal complete definition: E EF!Symbolic Comparisons. Similar to , we cannot implement Haskell's  class $ since there is no way to return an # value from a symbolic comparison.  Furthermore, F requires @$ to implement if-then-else, for the . benefit of implementing symbolic versions of  and  functions. Minimal complete definition: G GHIJKLM#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: N NOPQRLReturns (symbolic) true if all the elements of the given list are different SKReturns (symbolic) true if all the elements of the given list are the same T.Returns 1 if the boolean is true, otherwise 0 UReplacement for . Since  requires a l to be returned, R we cannot implement it for symbolic words. Index 0 is the least-significant bit. VGeneralization 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 W=Little-endian blasting of a word into its bits. Also see the FromBits class X:Big-endian blasting of a word into its bits. Also see the FromBits class Y:Least significant bit of a word, always stored at index 0 ZCMost significant bit of a word, always stored at the last position +Helper function for use in enum operations [BGet the name associated with the uninterpreted-value; useful when $ constructing axioms about this UI. JEnum instance. These instances are suitable for use with concrete values, ? and will be less useful for symbolic values around. Note that  requires J a concrete argument for obvious reasons. Other variants (succ, pred, [x..]) etc are similarly _ limited. While symbolic variants can be defined for many of these, but they will just diverge 1 as final sizes cannot be determined statically. <=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[ <=>=>?@ABCABCDEEFGHIJKLGHIJKLMNONOPQRSTUVWXYZ[portable experimentalerkokl@gmail.com \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) ^'Show a number in binary (starting with 0b) _IO version of ] `IO version of ^ aWA more convenient interface for reading binary numbers, also supports negative numbers \]^_`a\]^_`]^_`aportable experimentalerkokl@gmail.combKUnblasting 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: c cde Splitting an a into two b's and joining back.  Intuitively, a is a larger bit-size word than b, typically double.  The h# operation captures embedding of a b value into an a & without changing its semantic value. /Minimal complete definition: All, no defaults. fgh?Construct a symbolic word from its bits given in little-endian APerform a sanity check that we should receive precisely the same E number of bits as required by the resulting type. Unsigned version, $ the input is assumed little-endian Same as , but for signed words bcdefghbcdcdefghfghportable experimentalerkokl@gmail.comiQImplements polynomial addition, multiplication, division, and modulus operations  over GF(2^n). NB. Similar to E, division by 0 is interpreted as follows:  x o 0 = (0, x)for all x (including 0) Minimal complete definiton: l, o, p j3Given 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, p will show it like that. kAdd two polynomials in GF(2^n) lSMultiply 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. mDDivide two polynomials in GF(2^n), see above note for division by 0 nOCompute modulus of two polynomials in GF(2^n), see above note for modulus by 0 o%Division and modulus packed together pCDisplay a polynomial like a mathematician would (over the monomial x)  Pretty print as a polynomial  Add two polynomials   dMultiply two polynomials and reduce by the third (concrete) irreducible, given by its coefficients.  See the remarks for the l! function for this design choice  ijklmnopijklmnopjklmnopportable experimentalerkokl@gmail.com 9Abstract over functions that we can symbolically execute 7Abstract over input variables over generated functions 6Abstract over code generation for different languages qFRepresentation of a collection of generated programs. Code generation O produces a number of files (drivers, source, headers, etc.) and corresponding  contents. r qr qrrportable experimentalerkokl@gmail.com1A simple representation of C types for functions 8 sufficient enough to represent SBV generated functions  !"sDGiven a symbolic computation, render it as an equivalent C program. | First argument: States whether run-time-checks should be inserted for index-out-of-bounds or shifting-by-large values etc.  If #\, such checks are ignored, gaining efficiency, at the cost of potential undefined behavior. W Second argument is an optional directory name under which the files will be saved. If $ , the result % will be written to stdout. Use % ".". for creating files in the current directory. c The third argument is name of the function, which also forms the names of the C and header files. e The fourth argument are the names of the arguments to be used and the names of the outputs, if any. N Provide as many arguments as you like, SBV will make up ones if you don't pass enough. E The fifth and the final argument is the computation to be compiled. !Compilation will also generate a MakefileE and a sample driver program, which executes the program over random  input values. tAlternative interface for generating C. The output driver program uses the specified values (first argument) instead of random values. z Also this version returns the generated files for further manipulation. (Useful mainly for generating regression tests.) &'(JPretty print a functions type. If there is only one output, we compile it T as a function that returns that value. Otherwise, we compile it as a void function 5 that takes return values as pointers to be updated. )*+ Renders as const SWord8 s09, etc. the first parameter is the width of the typefield , Renders as s0%, etc, or the corresponding constant -=Words as it would be defined in the standard header stdint.h ./"The printf specifier for the type 0/Make a constant value of the given type. We don'<t check for out of bounds here, as it should not be needed. F There are many options here, using binary, decimal, etc. We simply @ 8-bit or less constants using decimal; otherwise we use hex. Z Note that this automatically takes care of the boolean (1-bit) value problem, since it I shows the result as an integer, which is OK as far as C is concerned. 1Show a constant 22Generate a makefile for ease of experimentation.. 3Generate the header 45#Generate an example driver program 6Generate the C program 78ststportable experimentalerkokl@gmail.comdefghijk45678:PQ6:4578PQportable experimentalerkokl@gmail.com-u Instances of u< 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: v vEGiven 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 $ w2Given 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. xAn allSat call results in a yx yzA sat call results in a {z " The reason for having a separate {z is to have a more meaningful 9 instance. {|A prove call results in a }| }~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 ?Solver configuration  Debug mode YPrint timing information on how long different phases took (construction, solving, etc.) Print literals in this base The actual SMT solver @A Given an ~6, extract an arbitrarily typed model from it, given a u instance  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  B argument to disp 'is the current model number. CDEFGHIJ-uvwxyz{|}~:;<=>?@ACDEFGHIJ-uvwvwxyyz{{|}}~:;<=>;<=>?@ACDEFGHIJ portable experimentalerkokl@gmail.comKLMN is this a sat problem? extra comments to place on top inputs and aliasing names  constants auto-generated tables user specified arrays uninterpreted functions/ constants user given axioms  assignments output variable OPQRSTUVWXYZ[\]^_KMNKMN!portable experimentalerkokl@gmail.com(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. `abcdefghijklmno``"portable experimentalerkokl@gmail.com'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.) >Turns a value into a 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 free 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. _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 * 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. gDefault configuration for the SMT solver. Non-verbose, non-timing, prints results in base 10, and uses  the Yices SMT solver. Same as , except verbose Same as , except prints timing info Same as &, except both verbose and timing info Adds a time out of n) seconds to a given solver configuration !Prove a predicate, equivalent to   <Find a satisfying assignment for a predicate, equivalent to   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. pq2Checks 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 . supported out-of-the box by the SBV library. 0Proves the predicate using the given SMT-solver 8Find a satisfying assignment using the given SMT-solver ;Find all satisfying assignments using the given SMT-solver rs5uvwxyz{|}~portable experimentalerkokl@gmail.comBtuvwxyz{|}~  !"#$%&'()*+,-./01239;<=>?@ABCDEFGHIJKLMNORSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~3210/.-,+;UVTYZSRXWbcdefghijklmnop@ABCMNOFGHIJKLDE \]^_`a<=>?[9|}z{xy~uvw*) !"#$%&'(qrstportable experimentalerkokl@gmail.com 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 portable experimentalerkokl@gmail.com/LChoose the appropriate array model to be used for modeling the memory. (See .)  The  is the function based model.  is the SMT-Lib array's based model. 5Helper synonym for capturing relevant bits of Mostek An instruction is modeled as a  transformer. We model 7 mostek programs in direct continuation passing style. CPrograms are essentially state transformers (on the machine state) 1Given a machine state, compute a value out of it NAbstraction 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!) 2The 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 () YWe model only two registers of Mostek that is used in the above algorithm, can add more. )The memory is addressed by 32-bit words. "Get the value of a given register "Set the value of a given register Get the value of a flag Set the value of a flag  Read memory Write to memory Checking 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 . Correctness theorem for our  implementation.  We have: checkOverflowCorrectQ.E.D.LDX: Set register X to value v LDA: Set register A to value v CLC: Clear the carry flag 9ROR, 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. ROR, register version: Same as , except through register r. BCC: branch to label l if the carry flag is false %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. %DEX: Decrement the value of register X &BNE: Branch if the zero-flag is false The  combinator stops/ our program, providing the final continuation  that does nothing. <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.  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. UCreate an instance of the Mostek machine, initialized by the memory and the relevant ' values of the registers and the flags NThe 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.  A version of ' that is suitable for code-generation. J This essentially means uncurrying the arguments and providing values for N parameters that are not necessary for code-generation; such as the arbitrary S mostek state or addresses for the values. Depending on the needs, more parameters  can be included. +Generate a C program that implements Legato's algorithm automatically. * (You can change the second argument of s to % "dirName" to place the output  files in that directory.) ///portable experimentalerkokl@gmail.com Simple function that returns add/ sum of args LGenerate C code for addSub. This will place the files in a directory called  genAddSub. . This call will generate the following files: File: Makefile  E # Makefile for addSub. Automatically generated by SBV. Do not edit!   CC=gcc 1 CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer   all: addSub_driver   addSub.o: addSub.c addSub.h + ${CC} ${CCFLAGS} -c addSub.c -o addSub.o  " addSub_driver.o: addSub_driver.c 9 ${CC} ${CCFLAGS} -c addSub_driver.c -o addSub_driver.o  ) addSub_driver: addSub.o addSub_driver.o = ${CC} ${CCFLAGS} addSub.o addSub_driver.o -o addSub_driver   clean: ! rm -f addSub_driver.o addSub.o   veryclean: clean  rm -f addSub_driver File: addSub.h  L /* Header file for addSub. Automatically generated by SBV. Do not edit! */  % #ifndef __addSub__HEADER_INCLUDED__ % #define __addSub__HEADER_INCLUDED__   #include <inttypes.h>  #include <stdint.h>   /* Unsigned bit-vectors */  typedef uint8_t SBool ;  typedef uint8_t SWord8 ;  typedef uint16_t SWord16;  typedef uint32_t SWord32;  typedef uint64_t SWord64;   /* Signed bit-vectors */  typedef int8_t SInt8 ;  typedef int16_t SInt16;  typedef int32_t SInt32;  typedef int64_t SInt64;   /* Entry point prototype: */ : void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,  SWord8 *dif);  * #endif /* __addSub__HEADER_INCLUDED__ */ File: addSub.c  F /* File: "addSub.c". Automatically generated by SBV. Do not edit! */   #include <inttypes.h>  #include <stdint.h>  #include "addSub.h"  : 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;   *sum = s2;  *dif = s3;  } File: addSub_driver.c )/* Example driver program for addSub. */ ;/* Automatically generated by SBV. Edit as you see fit! */  #include <inttypes.h> #include <stdint.h> #include <stdio.h> #include "addSub.h"  int main(void) {  SWord8 sum;  SWord8 dif;   addSub(125, 57, &sum, &dif);  . printf("addSub(125, 57, &sum, &dif) ->\n"); % printf(" sum = %"PRIu8"\n", sum); % printf(" dif = %"PRIu8"\n", dif);   return 0; } portable experimentalerkokl@gmail.comNThis is a naive implementation of fibonacci, and will work fine (albeit slow)  for concrete inputs: map fib0 [0..6]\[0 :: SWord32,1 :: SWord32,1 :: SWord32,2 :: SWord32,3 :: SWord32,5 :: SWord32,8 :: SWord32]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 :: SWord32,1 :: SWord32,1 :: SWord32,2 :: SWord32,3 :: SWord32,5 :: SWord32,8 :: SWord32]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. 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:  SWord32 fib1(const SWord32 s0)  { * const SBool s2 = s0 == 0x00000000UL; * const SBool s4 = s0 == 0x00000001UL; * const SBool s6 = s0 == 0x00000002UL; * const SBool s8 = s0 == 0x00000003UL; + const SBool s10 = s0 == 0x00000004UL; + const SBool s12 = s0 == 0x00000005UL; + const SBool s14 = s0 == 0x00000006UL; + const SBool s17 = s0 == 0x00000007UL; + const SBool s19 = s0 == 0x00000008UL; + const SBool s22 = s0 == 0x00000009UL; : const SWord32 s25 = s22 ? 0x00000022UL : 0x00000037UL; 1 const SWord32 s26 = s19 ? 0x00000015UL : s25; 1 const SWord32 s27 = s17 ? 0x0000000dUL : s26; 1 const SWord32 s28 = s14 ? 0x00000008UL : s27; 1 const SWord32 s29 = s12 ? 0x00000005UL : s28; 1 const SWord32 s30 = s10 ? 0x00000003UL : s29; 0 const SWord32 s31 = s8 ? 0x00000002UL : s30; 0 const SWord32 s32 = s6 ? 0x00000001UL : s31; 0 const SWord32 s33 = s4 ? 0x00000001UL : s32; 0 const SWord32 s34 = s2 ? 0x00000000UL : s33;   return s34;  } ,Compute the fibonacci numbers statically at code-generation time and & put them in a table, accessed by the C 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 C with default 0.) % SWord32 fibLookup(const SWord32 s0)  { % static const SWord32 table0[] = { ? 0x00000000UL, 0x00000001UL, 0x00000001UL, 0x00000002UL, ? 0x00000003UL, 0x00000005UL, 0x00000008UL, 0x0000000dUL, ? 0x00000015UL, 0x00000022UL, 0x00000037UL, 0x00000059UL, ? 0x00000090UL, 0x000000e9UL, 0x00000179UL, 0x00000262UL, ? 0x000003dbUL, 0x0000063dUL, 0x00000a18UL, 0x00001055UL, ? 0x00001a6dUL, 0x00002ac2UL, 0x0000452fUL, 0x00006ff1UL, ? 0x0000b520UL, 0x00012511UL, 0x0001da31UL, 0x0002ff42UL, ? 0x0004d973UL, 0x0007d8b5UL, 0x000cb228UL, 0x00148addUL, ? 0x00213d05UL, 0x0035c7e2UL, 0x005704e7UL, 0x008cccc9UL, ? 0x00e3d1b0UL, 0x01709e79UL, 0x02547029UL, 0x03c50ea2UL, ? 0x06197ecbUL, 0x09de8d6dUL, 0x0ff80c38UL, 0x19d699a5UL, ? 0x29cea5ddUL, 0x43a53f82UL, 0x6d73e55fUL, 0xb11924e1UL, ? 0x1e8d0a40UL, 0xcfa62f21UL, 0xee333961UL, 0xbdd96882UL, ? 0xac0ca1e3UL, 0x69e60a65UL, 0x15f2ac48UL, 0x7fd8b6adUL, ? 0x95cb62f5UL, 0x15a419a2UL, 0xab6f7c97UL, 0xc1139639UL, ? 0x6c8312d0UL, 0x2d96a909UL, 0x9a19bbd9UL, 0xc7b064e2UL,  0x61ca20bbUL  }; = const SWord32 s65 = s0 >= 65 ? 0x00000000UL : table0[s0];   return s65;  } portable experimentalerkokl@gmail.com>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. E /* File: "sgcd.c". Automatically generated by SBV. Do not edit! */   #include <inttypes.h>  #include <stdint.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;  const SWord8 s4 = s0 % s1; $ const SWord8 s5 = s3 ? s0 : s4;  const SBool s6 = 0 == s5;  const SWord8 s7 = s1 % s5; $ const SWord8 s8 = s6 ? s1 : s7;  const SBool s9 = 0 == s8;  const SWord8 s10 = s5 % s8; & const SWord8 s11 = s9 ? s5 : s10; ! const SBool s12 = 0 == s11; ! const SWord8 s13 = s8 % s11; ' const SWord8 s14 = s12 ? s8 : s13; ! const SBool s15 = 0 == s14; " const SWord8 s16 = s11 % s14; ( const SWord8 s17 = s15 ? s11 : s16; ! const SBool s18 = 0 == s17; " const SWord8 s19 = s14 % s17; ( const SWord8 s20 = s18 ? s14 : s19; ! const SBool s21 = 0 == s20; " const SWord8 s22 = s17 % s20; ( const SWord8 s23 = s21 ? s17 : s22; ! const SBool s24 = 0 == s23; " const SWord8 s25 = s20 % s23; ( const SWord8 s26 = s24 ? s20 : s25; ! const SBool s27 = 0 == s26; " const SWord8 s28 = s23 % s26; ( const SWord8 s29 = s27 ? s23 : s28; ! const SBool s30 = 0 == s29; " const SWord8 s31 = s26 % s29; ( const SWord8 s32 = s30 ? s26 : s31; ! const SBool s33 = 0 == s32; " const SWord8 s34 = 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;  } portable experimentalerkokl@gmail.comEGiven 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:  popCount_Slow 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 ) to the reference slow version. We have: prove 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 :  N /* Header file for popCount. Automatically generated by SBV. Do not edit! */  ' #ifndef __popCount__HEADER_INCLUDED__ ' #define __popCount__HEADER_INCLUDED__   #include <inttypes.h>  #include <stdint.h>   /* Unsigned bit-vectors */  typedef uint8_t SBool ;  typedef uint8_t SWord8 ;  typedef uint16_t SWord16;  typedef uint32_t SWord32;  typedef uint64_t SWord64;   /* Signed bit-vectors */  typedef int8_t SInt8 ;  typedef int16_t SInt16;  typedef int32_t SInt32;  typedef int64_t SInt64;   /* Entry point prototype: */ # SWord8 popCount(const SWord64 x);  , #endif /* __popCount__HEADER_INCLUDED__ */ 4The generated C function. Note how the Haskell list  is turned into a look-up  table automatically (see table0 below) in the C code.  H /* File: "popCount.c". Automatically generated by SBV. Do not edit! */   #include <inttypes.h>  #include <stdint.h>  #include "popCount.h"  " 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  }; 3 const SWord64 s11 = s0 & 0x00000000000000ffULL; $ const SWord8 s12 = table0[s11];  const SWord64 s13 = s0 >> 8; 4 const SWord64 s14 = 0x00000000000000ffULL & s13; $ const SWord8 s15 = table0[s14]; " const SWord8 s16 = s12 + s15; ! const SWord64 s17 = s13 >> 8; 4 const SWord64 s18 = 0x00000000000000ffULL & s17; $ const SWord8 s19 = table0[s18]; " const SWord8 s20 = s16 + s19; ! const SWord64 s21 = s17 >> 8; 4 const SWord64 s22 = 0x00000000000000ffULL & s21; $ const SWord8 s23 = table0[s22]; " const SWord8 s24 = s20 + s23; ! const SWord64 s25 = s21 >> 8; 4 const SWord64 s26 = 0x00000000000000ffULL & s25; $ const SWord8 s27 = table0[s26]; " const SWord8 s28 = s24 + s27; ! const SWord64 s29 = s25 >> 8; 4 const SWord64 s30 = 0x00000000000000ffULL & s29; $ const SWord8 s31 = table0[s30]; " const SWord8 s32 = s28 + s31; ! const SWord64 s33 = s29 >> 8; 4 const SWord64 s34 = 0x00000000000000ffULL & s33; $ const SWord8 s35 = table0[s34]; " const SWord8 s36 = s32 + s35; ! const SWord64 s37 = s33 >> 8; 4 const SWord64 s38 = 0x00000000000000ffULL & s37; $ const SWord8 s39 = table0[s38]; " const SWord8 s40 = s36 + s39;   return s40;  } PSBV will also generate a driver program for test purposes. The driver will call Q the generated function with random values. (It is also possible to instruct SBV , to use prescribed values, see the function t.)  , /* Example driver program for popCount. */ < /* Automatically generated by SBV. Edit as you see fit! */   #include <inttypes.h>  #include <stdint.h>  #include <stdio.h>  #include "popCount.h"   int main(void)  { 6 const SWord8 pc = popCount(0x0123456789abcdefULL);  ? printf("popCount(0x0123456789abcdefULL) = %"PRIu8"\n", pc);   return 0;  } And a Makefile to simplify compilation: G # Makefile for popCount. Automatically generated by SBV. Do not edit!   CC=gcc 1 CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer   all: popCount_driver  # popCount.o: popCount.c popCount.h / ${CC} ${CCFLAGS} -c popCount.c -o popCount.o  & popCount_driver.o: popCount_driver.c = ${CC} ${CCFLAGS} -c popCount_driver.c -o popCount_driver.o  / popCount_driver: popCount.o popCount_driver.o C ${CC} ${CCFLAGS} popCount.o popCount_driver.o -o popCount_driver   clean: % rm -f popCount_driver.o popCount.o   veryclean: clean  rm -f popCount_driver  portable experimentalerkokl@gmail.comXHelper 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 pG 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 o y then x = y l 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  in GF(2^8).) Queries  portable experimentalerkokl@gmail.com 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.  The tie operator, concatenation AThe zip operator, zips the power-lists of the same size, returns ! a powerlist of double the size. Inverse of zipping Reference prefix sum (ps) is simply Haskell's scanl1 function The 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. gCorrectness theorem, for a powerlist of given size, an associative operator, and its left-unit element MProves Ladner-Fischer is equivalent to reference specification for addition.  0; is the left-unit element, and we use a power-list of size 8. PProves 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. CTry proving correctness for an arbitrary operator. This proof will not go through since the \ SMT solver does not know that the operator associative and has the given left-unit element 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. dGenerate 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. CProve 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.NNote that these proofs tend to run long. Also, Yices-1.0.28 ran out of memory - and crashed on my box when I tried for size 8(, after running for about 2.5 minutes.. HA 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 CONSTANTSAXIOMSDEFINE 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 + s17OUTPUTS s0 s8 s9 s11 s12 s14 s15 s18STrace 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 CONSTANTSAXIOMSDEFINE 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 + s13OUTPUTS s0 s8 s9 s10 s11 s12 s13 s14 portable experimentalerkokl@gmail.comZUse 16-bit words to represent the counts, much larger than we actually need, but no harm. =Codes the puzzle statement, more or less directly using SBV. Prints the only solution: solveOnly one solution found: dog = 3 :: SWord16 cat = 41 :: SWord16 mouse = 56 :: SWord16 portable experimentalerkokl@gmail.comJThe 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: solve4640261571849533Number of solutions: 1 portable experimentalerkokl@gmail.com #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                portable experimentalerkokl@gmail.comFA 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. portable experimentalerkokl@gmail.comDA 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  !"# !"# !"#portable experimentalerkokl@gmail.com($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 0Model time using 32 bits 1U2 band members 23456Bono's ID 7Edge's ID 8Adam's ID 9Larry'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 A)Transferring the flash to the other side B(Transferring a person to the other side C1Increment the time, when only one person crosses D3Increment the time, when two people cross together ESymbolic version of when F/Move one member, remembering to take the flash G'Move two members, again with the flash H!Run a sequence of given actions. ICCheck 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 J.See if there is a solution that has precisely n steps KHSolve 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.4Finding the all 2 possible solutions to the puzzle. ($%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJK(154320/6789:;.<=&'()*+,->%?@ABCDEFG$HIJK($%&'()*+,-'()*+,-./01543223456789:;<=>?@ABCDEFGHIJKportable experimentalerkokl@gmail.comLNThis version directly uses SMT-arrays and hence does not need an initializer. E Reading an element before writing to it returns an arbitrary value. M7The 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. N&Uninterpreted function in the theorem O3Correctness theorem. We state it for all values of x, y, and  the array a7. We also take an arbitrary initializer for the array. P$Prints Q.E.D. when run, as expected  proveThm1Q.E.D.QSame as O, except we don't need an initializer with the  model. R%Prints Q.E.D. when run, as expected:  proveThm2Q.E.D.LMNOPQRMNOPLQRLMNOPQRportable experimentalerkokl@gmail.comSAn uninterpreted function T Asserts that f x z == f (y+2) z whenever x == y+2. Naturally correct:  prove thmGoodQ.E.D.U Asserts that f0 is commutative; which is not necessarily true! G Indeed, the SMT solver (Yices in this case) returns a counter-example , function that is not commutative. We have:  prove $ 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. STUSTUSTU#portable experimentalerkokl@gmail.com<read-after-write: If you write a value and read it back, you' ll get it Zwrite-after-write: If you write to the same location twice, then the first one is ignored JTwo writes to different locations commute, i.e., can be done in any order CTwo writes do not commute if they can be done to the same location $portable experimentalerkokl@gmail.com   %portable experimentalerkokl@gmail.com&portable experimentalerkokl@gmail.com   'portable experimentalerkokl@gmail.com(portable experimentalerkokl@gmail.com)portable experimentalerkokl@gmail.com   *portable experimentalerkokl@gmail.com+portable experimentalerkokl@gmail.com   ,portable experimentalerkokl@gmail.com-portable experimentalerkokl@gmail.com.portable experimentalerkokl@gmail.com   /portable experimentalerkokl@gmail.com   0portable experimentalerkokl@gmail.com1portable experimentalerkokl@gmail.com2portable experimentalerkokl@gmail.com3portable experimentalerkokl@gmail.com4portable experimentalerkokl@gmail.com5portable experimentalerkokl@gmail.com6portable experimentalerkokl@gmail.com7portable experimentalerkokl@gmail.com8portable experimentalerkokl@gmail.com9portable experimentalerkokl@gmail.com:portable experimentalerkokl@gmail.com;portable experimentalerkokl@gmail.com<portable experimentalerkokl@gmail.com=portable experimentalerkokl@gmail.com>portable experimentalerkokl@gmail.com?portable experimentalerkokl@gmail.com@portable experimentalerkokl@gmail.comAportable experimentalerkokl@gmail.comBportable experimentalerkokl@gmail.comCportable experimentalerkokl@gmail.comDportable experimentalerkokl@gmail.comEportable experimentalerkokl@gmail.comFportable experimentalerkokl@gmail.comGportable experimentalerkokl@gmail.comHportable experimentalerkokl@gmail.com   Iportable experimentalerkokl@gmail.com   Jportable experimentalerkokl@gmail.com   Kportable experimentalerkokl@gmail.com   Lportable experimentalerkokl@gmail.com   Mportable experimentalerkokl@gmail.comNportable experimentalerkokl@gmail.comOportable experimentalerkokl@gmail.comPportable experimentalerkokl@gmail.comQportable experimentalerkokl@gmail.comRRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~!"""""""""""""""""""""""      !"#$%&'()*+,-./0123456 7 8 9 : ; < = > ? @ A B C D E F G H I J K L M N O P N Q R S T U V W XYZ[\QRT]N^_`abcdefghijjklmnopqrstuvwxyz{|}~ZEFgh{      !"#$%&'()*+,-./0/1/23456789:;<=>?@ABCDEFGHIJK<LMNOPQRSTUVWXYZ[[\\]^_`a`bcdefghijklmnopqrstuvwxxyz{|}~                     !!!!!!!!!!!!!!!!""""///////////////########$$$$$$$$$$$%&&&&&&&&&''''()))))))))**T+++++++++,--------.........//////////000011111111223333N4444456789:;<< =>?@ABCDEFGHIJKLMNOPQ sbv-0.9.13Data.SBV.InternalsData.SBV&Data.SBV.Examples.BitPrecise.BitTricks#Data.SBV.Examples.BitPrecise.Legato'Data.SBV.Examples.CodeGeneration.AddSub*Data.SBV.Examples.CodeGeneration.Fibonacci$Data.SBV.Examples.CodeGeneration.GCD0Data.SBV.Examples.CodeGeneration.PopulationCount)Data.SBV.Examples.Polynomials.Polynomials%Data.SBV.Examples.PrefixSum.PrefixSum%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.FunctionData.SBV.Provers.SExprData.SBV.Utils.TDiffData.SBV.Utils.LibData.SBV.Utils.SBVTestData.SBV.Utils.BooleanData.SBV.BitVectors.DataData.SBV.BitVectors.ModelData.SBV.BitVectors.PrettyNumData.SBV.BitVectors.SplittableData.SBV.BitVectors.PolynomialData.SBV.Compilers.CodeGenData.SBV.Compilers.CData.SBV.SMT.SMTData.SBV.SMT.SMTLibData.SBV.Provers.YicesData.SBV.Provers.ProverData.SBV.Examples.Arrays.Memory#Data.SBV.Examples.Basics.BasicTests$Data.SBV.TestSuite.Basics.BasicTestsData.SBV.Examples.Basics.HigherData.SBV.Examples.Basics.IndexData.SBV.TestSuite.Basics.Index#Data.SBV.Examples.Basics.ProofTestsData.SBV.Examples.Basics.QRem/Data.SBV.Examples.Basics.UnsafeFunctionEquality0Data.SBV.TestSuite.Basics.UnsafeFunctionEqualityData.SBV.Examples.CRC.CCITT"Data.SBV.Examples.CRC.CCITT_UnidirData.SBV.Examples.CRC.GenPolyData.SBV.Examples.CRC.ParityData.SBV.Examples.CRC.USB5"Data.SBV.Examples.Puzzles.PowerSet%Data.SBV.Examples.Puzzles.Temperature-Data.SBV.Examples.Uninterpreted.Uninterpreted Data.SBV.TestSuite.Arrays.Memory Data.SBV.TestSuite.Basics.Higher$Data.SBV.TestSuite.Basics.ProofTestsData.SBV.TestSuite.Basics.QRem'Data.SBV.TestSuite.BitPrecise.BitTricks$Data.SBV.TestSuite.BitPrecise.Legato(Data.SBV.TestSuite.CodeGeneration.AddSub)Data.SBV.TestSuite.CodeGeneration.CgTests+Data.SBV.TestSuite.CodeGeneration.Fibonacci%Data.SBV.TestSuite.CodeGeneration.GCD1Data.SBV.TestSuite.CodeGeneration.PopulationCountData.SBV.TestSuite.CRC.CCITT#Data.SBV.TestSuite.CRC.CCITT_UnidirData.SBV.TestSuite.CRC.GenPolyData.SBV.TestSuite.CRC.ParityData.SBV.TestSuite.CRC.USB5&Data.SBV.TestSuite.PrefixSum.PrefixSum*Data.SBV.TestSuite.Polynomials.Polynomials&Data.SBV.TestSuite.Puzzles.DogCatMouse#Data.SBV.TestSuite.Puzzles.Euler185&Data.SBV.TestSuite.Puzzles.MagicSquare"Data.SBV.TestSuite.Puzzles.NQueens#Data.SBV.TestSuite.Puzzles.PowerSet!Data.SBV.TestSuite.Puzzles.Sudoku#Data.SBV.TestSuite.Puzzles.U2Bridge&Data.SBV.TestSuite.Puzzles.Temperature$Data.SBV.TestSuite.Uninterpreted.AUF.Data.SBV.TestSuite.Uninterpreted.Uninterpreted)Data.SBV.TestSuite.Uninterpreted.Function SBVTestSuite mkTestSuiteshowsAs ioShowsAsgenerateGoldCheckBooleantruefalsebnot&&&|||~&~|<+>==><=>fromBoolbAndbOrbAnybAll SFunArraySArraySymArray newArray_newArray readArray resetArray writeArray mergeArraysSymWordfreefree_ mkFreeVarsliteral unliteralfromCW isConcrete isSymbolic isConcretelyoutputSymbolicSInt64SInt32SInt16SInt8SWord64SWord32SWord16SWord8SBoolSBVResultCW mkConstCWaddAxiom runSymbolic mkSFunArray Uninterpreted uninterpretuninterpretWithHandleSBVUF Mergeable symbolicMergeiteselect BVDivisible bvQuotRem OrdSymbolic.<.>=.>.<=sminsmax EqSymbolic.==./=genFreegenFree_ allDifferentallEqualoneIfbitValuesetBitToblastLEblastBElsbmsb sbvUFName PrettyNumhexSbinShexbinreadBinFromBits fromBitsLE fromBitsBE Splittablesplit#extend Polynomial polynomialpAddpMultpDivpModpDivModshowPoly CgPgmBundle compileToC compileToC'SatModelparseCWscvtModel AllSatResult SatResult ThmResult SMTResultTimeOut ProofErrorUnknown Satisfiable Unsatisfiable SMTSolvername executableoptionsengine SMTConfigverbosetiming printBasesolvergetModel displayModelsyicesEquality===ProvableforAll_forAll Predicate defaultSMTCfg verboseSMTCfg timingSMTCfgverboseTimingSMTCfgtimeoutprovesatallSatisTheoremWithinisSatisfiableWithin isTheorem isSatisfiablenumberOfModelscompileToSMTLib proveWithsatWith allSatWithfastMinCorrectfastMaxCorrectoppositeSignsCorrectconditionalSetClearCorrectpowerOfTwoCorrectqueriesModelInitVals InstructionProgramExtractMostekmemory registersflagsMemoryFlags RegistersBitValueFlagFlagZFlagCRegisterRegARegXAddressgetRegsetReggetFlagsetFlagpeekpoke checkOverflowcheckOverflowCorrectldxldaclcrorMrorRbccadcdexbneendlegato runLegato initMachinelegatoIsCorrectcorrectnessTheorem cg_runLegato legatoInCaddSub genAddSubfib0fib1genFib1fib2genFib2sgcd sgcdIsCorrect genGCDInC popCount_SlowpopCountpop8fastPopCountIsCorrectgenPopCountInCGF28<*>multUnitmultComm multAssoc polyDivModtestGF28 PowerListtiePLzipPLunzipPLpslf flIsCorrectthm1thm2thm3genPrefixSumInstance prefixSumladnerFischerTrace scanlTraceCountpuzzlesolveguesseseuler185BoardRowElemcheckdiagisMagicchunkmagicSolutionisValidnQueensPuzzlevalid dispSolutionsolveAllpuzzle0puzzle1puzzle2puzzle3puzzle4puzzle5puzzle6 allPuzzlesActionsMoveStatustimeflashlBonolEdgelAdamlLarryLocation SU2MemberTimeU2MemberLarryAdamEdgeBonobonoedgeadamlarry isU2Member crossTimeheretherestartwhereIs xferFlash xferPerson bumpTime1 bumpTime2whenSmove1move2runsolveNsolveU2BAf proveThm1 proveThm2thmGoodthmBadSExprS_AppS_NumS_Con parseSExpr showTDifftimeIfdeepseq-1.1.0.2Control.DeepSeqNFDatamlift2mlift3mlift4mlift5mlift6mlift7 HUnit-1.2.2.3Test.HUnit.Base~:assertTestCaseTestList TestLabelTesttestTest.HUnit.Lang Assertionghc-primGHC.BoolBoolbaseGHC.ListandoranyallCacheduncache ArrayIndex OutputtableStaterctrrinpsroutsrtblMapspgm rconstMaprexprMap rArrayMaprUIMapraxiomsUIMapArrayMap ArrayInfoTableMapCnstMapExprMap ArrayContext ArrayMerge ArrayMutate ArrayReset ArrayFree UnintKindUArrUFun NamedSymVarPgmHasSignAndSizesizeOfhasSignshowTypeSBVExprSBVAppOpArrReadArrEqLkUpJoinRorRolShrShlNotXOrOrAndIte GreaterEqLessEq GreaterThanLessThanNotEqualEqualRemQuotMinusTimesPlusSBVTypeSWNodeIdSizecwSignedcwSizecwVal cwSameTypecwIsBitcwToBoolnormCWfalseSWtrueSWfalseCWtrueCW typeArityliftCWliftCW2mapCWmapCW2reorder unintFnUIKind arrayUIKindincCtrnewUninterpretednewConst getTableIndexnewExprsbvToSWmkSymSBV runSymbolic' declNewSArraycacheGHC.RealIntegralRealGHC.EnumEnumquotRem GHC.ClassesEqOrd GHC.OrderingOrderingmaxminliftSym1liftSym2 liftSym2B liftSym1Bool liftSym2Bool mkSymOpSCmkSymOp mkSymOp1SCmkSymOp1 genLiteral genFromCW Data.BitstestBitsetBitclearBitenumCvtliftQRemmkUFNameforceArg $fEnumSBVfromEnumshexsbinpads2s16genSplitgenJoincwSplitcwJoin fromBinLEcheckAndConvertcheckAndConvertSignedliftliftCliftSspaddPolyitespolyMultdegreemdpidxdivx SymExecutable symExecuteCgArgscgArgs SBVTarget targetName translateshowFilecodeGencodeGen' renderFileCTypeSBVToCdietbdFalse Data.MaybeNothingJustcgenmkCType pprCFunHeadermkParammkPParamdeclSWshowSWpprCWord showCType specifiermkConst showConstgenMake genHeadersepIf genDrivergenCProgppExpr printQuotesGHC.ShowShowSMTModel modelAssocs modelArraysmodelUninterps SMTEngine resultConfiggenParse GHC.TypesInt showSMTResult showModelshCWshMshUIshUA pipeProcessstandardSolver SMTLibPgmaddNonEqConstraintstoSMTLibmkTable declArraydeclAxdeclUI mkFormulanonEqsnonEqdeclcvtAsgncvtCnstcvtCWnegIf mkMinBoundrotshftcvtExpcvtType sortByNodeId interpret extractMap moveConstUIsgetCounterExample extractUnints extractUnintgetUIVal getDefaultVal getCallValgetArg showDefaultshowCallformatfmtFun checkTheoremcheckSatisfiable callSolver generateTraceGHC.IntInt8Int16Int32Int64GHC.WordWordWord8Word16Word32Word64rotateRrotateLshiftRshiftLisSignedbitSize complementBitbitrotateshift complementxor.|..&.Bitsrawwaw wcommutesGood wcommutesBadteststest0test1test2test3test4test5f1f2f3f4f5 testSuitef11f12f21f22f31f32f33tf1eqf2f1eqf3f3eqf4f1SingleqremSWord48 extendDatamkFramecrc diffCountcrcGoodhw4has84Inhabitantshw4 nonUnidir crcUniGood ccitHDis3 ccitHDis4mkPolywaitForgenPolyfindHD3PolynomialsparityisOddcountparityOKSWord11S11 mkSWord11usbGood genPowerSetpowerSetTempd2frevOfgp0p1p2sel