The next Galois Tech Talk will be delivered by Amit Goel.  Come kick off 2010 with us!

Title: Ground Interpolation for Combined Theories

Abstract: We give a method for modular generation of ground interpolants in modern SMT solvers supporting multiple theories. Our method uses a novel algorithm to modify the proof tree obtained from an unsatifiability run of the solver into a proof tree without occurrences of troublesome “uncolorable” literals. An interpolant can then be readily generated using existing procedures. The principal advantage of our method is that it places few restrictions (none for convex theories) on the search strategy of the solver. Consequently, it is straightforward to implement and enables more efficient interpolating SMT solvers. In the presence of non-convex theories our method is incomplete, but still more general than previous methods.

• Date: Tuesday, 10:30am, 05 Jan 2010
• Time: 10:30am – 11:30am
• Location: Galois, Inc.
  421 SW 6th Ave. Suite 300
  (3rd floor of the Commonwealth Building)
  Portland, OR 97204

Bio: Amit Goel is a member of Intel’s Strategic CAD Labs.

I can never shuffle cards properly. They seem to go every which way when I try, and a perfect random shuffle seems nigh-impossible to achieve, even though the experts claim it takes a mere 7 moves. (The mathematical argument is surprisingly quite technical.) Luckily, we shall concern ourselves with a much simpler problem today: How many perfect out-shuffles does it take to restore a deck back to its original order? We’ll throw in a couple of variants of the problem for fun, but rest assured that we’ll let computers do the work. And, of course, we’ll use Cryptol to help us along the way.

What is a riffle shuffle?

According to wikipedia, a riffle (or dovetail) shuffle goes like this:

… half of the deck is held in each hand with the thumbs inward, then cards are released by the thumbs so that they fall to the table interleaved. Many also lift the cards up after a riffle, forming what is called a bridge which puts the cards back into place…

Well, I read that a couple times, and watched a couple of videos on the internet showing how to do it, but no luck so far. Luckily, this sort of shuffling is quite easy to express programmatically, and Cryptol has the right abstractions to code this in a couple of lines.

Bisecting the deck

The first step in the shuffle is bisecting the deck into two equal halves:

bisect : {a b} (fin a) => [2*a]b -> ([a]b, [a]b);
bisect xs = (take (w, xs), drop (w, xs))
  where w = width xs / 2;

We simply compute the mid-point, and divide the given sequence xs into two, by take‘ing and drop‘ping the correct amounts from the input sequence. In fact, the type of bisect is more interesting than its definition: It succinctly captures the following four facts:

1. The input has to be of even length (2*a),
2. The input has to be finite (fin a),
3. The output has two components, each of which has precisely a elements, that is, half the input,
4. The actual contents of the sequence can be of any type (b), i.e., the function bisect is shape-polymorphic in the contents.

The ability to express precise size/shape-polymorphic properties using types is one of the strengths of Cryptol.

Out-shuffle vs in-shuffle

Once the deck is split into two, we proceed by picking the cards alternatingly from each half. We have two choices: We can either start with the first half, or the second. If you start with the first half, that’s called an out-shuffle. If you start with the second half, then it’s an in-shuffle. These two functions are actually quite easy to code in Cryptol:

  outShuffle : {a b} (fin a) => [2*a]b -> [2*a]b;
  outShuffle xs = join [| [x y] || x <- fh || y <- sh |]
    where (fh, sh) = bisect xs;

  inShuffle : {a b} (fin a) => [2*a]b -> [2*a]b;
  inShuffle xs = join [| [y x] || x <- fh || y <- sh |]
    where (fh, sh) = bisect xs;

The definitions are almost identical, except for the order in which we put the cards from the halves (fh and sh) together. In the outShuffle, the first card in each pair comes from the first-half. In the inShuffle, it comes from the second half. Easier done than said! Let’s make sure they behave as we expect:

  Cryptol> bisect [1..8]
  ([1 2 3 4], [5 6 7 8])
  Cryptol> outShuffle [1..8]
  [1 5 2 6 3 7 4 8]
  Cryptol> inShuffle [1..8]
  [5 1 6 2 7 3 8 4]

Good! It’s interesting to see what happens when we apply bisect to an odd-length sequence:

  Crytpol> bisect [1..9]
  In a top-level expression: with inferred type:
  {a} ([a][4],[a][4])
  encountered the following unresolved constraints:
  fin a
  2*a == 9

Cryptol is basically telling us that there is no a such that 2*a is 9, resulting in a type-error. Note that this is a static-check before you run your program! In other words, if your program type-checks, then you can rest assured that whenever you call bisect, it is guaranteed to get an even-length sequence as its argument. Strong static typing and size-polymorphism of Cryptol really pays off in this case!

Sequences of shuffles

Before proceeding to the properties of shuffles, we need one last notion: The application of a shuffle repeatedly to a given input, yielding an infinite sequence of transformations:

  iterate : {a} (a -> a, a) -> [inf]a;
  iterate (f, x) = [x] # iterate (f, f x);

  outShuffles, inShuffles :
             {a b} (fin a) => [2*a]b -> [inf][2*a]b;
  outShuffles xs = iterate(outShuffle, xs);
  inShuffles  xs = iterate(inShuffle, xs);

The high-order function iterate gives us the infinite sequence of results of applying a function to a value over and over. We simply use this helper to define outShuffles and inShuffles to apply the corresponding functions indefinitely to their input. Note that the resulting type shows that we get an infinite sequence as output, as indicated by the size inf.

Properties of shuffles

It turns out that if one applies 8 out-shuffles to a deck, a remarkable thing happens: Nothing! The deck goes back to its original order! This is a bit hard to believe, and harder to realize using a real deck of cards. (A friend of mine says he saw it done at college once by hand, but I’m yet to meet anyone who can do this successfully so far!)

Well, the good thing about programming is that we can manipulate the sequences at will, without fear of messing up the cards. Even better, we can assert the above claim as a theorem in Cryptol:

  type Deck = [52][6];

  outShuffle8 : Deck -> Bit;
  theorem outShuffle8: {deck}.
            outShuffles(deck) @ 8 == deck;

We have defined a Deck to be a sequence of 52 things, each of which is 6-bits wide, which is more than enough to cover all the 52-unique elements that appear in an ordinary deck. (6-bits can encode 64 values, so we have 12 unused elements.) The theorem simply states that the 8′th element of the infinite sequence of outShuffle applied to an arbitrary deck gives us back the original deck.

Let’s ask Cryptol to prove this theorem: (Cryptol’s symbolic and sbv backends can perform these proofs, so we first set our mode accordingly below.)

   Cryptol> :set sbv
   Cryptol> :prove outShuffle8
   Q.E.D.

Voila! The proof completes instantaneously, with almost no time elapsed. (This might be surprising at first, since the input space to the theorem has 52*6 = 312 bits, which is quite large. However, we note that the theorem is actually fairly easy to prove since all shuffling does is a mere re-ordering of things with no specific computation; which is easy to manipulate symbolically for Cryptol’s proof engine.)

Reversing the deck

Can we reverse a deck of cards using outShuffle’s? Turns out that this cannot be done. In particular, an outShuffle never moves the first element of the deck anywhere:

  outShuffleFirstCard : Deck -> Bit;
  theorem outShuffleFirstCard: {deck}.
          outShuffle deck @ 0 == deck @ 0;

We have:

  Cryptol> :prove outShuffleFirstCard
  Q.E.D.

Since the first card remains stationary, there is no way to reverse a deck of cards by just using outShuffles.

How about with inShuffle? Turns out the magic number is 26 for reversing a deck of cards in this particular case:

  inShuffle26Rev : Deck -> Bit;
  theorem inShuffle26Rev : {deck}.
            inShuffles(deck) @ 26 == reverse deck;

Again, the proof is immediate:

  Cryptol> :prove inShuffle26Rev
  Q.E.D.

If 26 in-shuffle’s reverse the deck, then 52 of them will restore it back. Here’s the corresponding theorem:

   inShuffle52 : Deck -> Bit;
   theorem inShuffle52: {deck}.
             inShuffles(deck) @ 52 == deck;

Again, the proof is immediate.

The Mongean Shuffle

There is one more variation on the shuffle that we will consider. The mongean shuffle picks the even and odd numbered elements, reverses the odds and adds the evens at the back. For instance, given the sequence: 0 1 2 3 4 5 6 7 8 9, we first construct two sub-sequences: The even index elements: 0 2 4 6 8, and the odd ones 1 3 5 7 9. We then reverse the latter to get 9 7 5 3 1, and append the former, obtaining: 9 7 5 3 1 0 2 4 6 8. Luckily, the Cryptol definition is much easier to read:

  monge xs = reverse odds # evens
    where { w = width xs;
            evens = xs @@ [0 2 .. (w-1)];
            odds  = xs @@ [1 3 .. (w-1)]
          };

  monges xs = iterate(monge, xs);

With a monge shuffle, it takes 12 rounds to restore a deck:

  monge12 : Deck -> Bit;
  theorem monge12: {deck}. monges(deck) @ 12 == deck;

We will leave it to the reader to construct the argument that no sequence of monge shuffles would reverse a deck. (In particular, one can prove that the 18th element from top will never move in a deck of 52. Proving this theorem in Cryptol is again quite trivial.)

A note on theorems

The attentive reader might worry that our Deck type does not quite correspond to a deck-of-cards. This is indeed the case. There are two discrepancies. First, as we mentioned before, our decks can represent 64 elements, while a deck of cards has only 52 distinct cards. On the plus side, this just makes our theorems “stronger,” since we allow for more cards then possible. More importantly, the properties are intended for decks that have no-repeating cards in them. (That is, every card occurs precisely once.) But our theorems apply to arbitrary deck’s, even those that have repeating elements in them. Again, this just makes our theorems stronger, as the unique-sequence cases directly follow from them. We can rest assured that our proofs are conclusive, even though our model of playing-cards is not perfect.

Download

Free evaluation licenses of Cryptol are available at www.cryptol.net. The Cryptol source code for shuffling cards is also available as well.

The December 15th Galois Tech Talk will be delivered by John Launchbury.  He will present Conal Elliott’s 2009 ICFP paper entitled  Beautiful Differentiation for those of us who were not able to attend this wonderful talk in-person.

• Date: Tuesday, 10:30am, 15 Dec 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.
  421 SW 6th Ave. Suite 300
  (3rd floor of the Commonwealth Building)
  Portland, OR 97204

Abstract: Automatic differentiation (AD) is a precise, efficient, and convenient method for computing derivatives of functions. Its forward-mode implementation can be quite simple even when extended to compute all of the higher-order derivatives as well. The higher-dimensional case has also been tackled, though with extra complexity. This paper develops an implementation of higher-dimensional, higher-order, forward-mode AD in the extremely general and elegant setting of calculus on manifolds and derives that implementation from a simple and precise specification.

In order to motivate and discover the implementation, the paper poses the question, “What does AD mean, independently of implementation?‚” An answer arises in the form of naturality of sampling a function and its derivative. Automatic differentiation flows out of this naturality condition, together with the chain rule. Graduating from first-order to higher-order AD corresponds to sampling all derivatives instead of just one. Next, the setting is expanded to arbitrary vector spaces, in which derivative values are linear maps. The specification of AD adapts to this elegant and very general setting, which even simplifies the development.

Bio: John Launchbury is the founder and Chief Scientist of Galois, Inc.

[Note the Friday date, instead of the usual Tuesday slot.]

The November 13th Galois Tech Talk will be delivered by Rod Chapman, titled “Hoare-Logic – fiddly details and small print.”

• Date: Friday, November 13th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.
  421 SW 6th Ave. Suite 300
  (3rd floor of the Commonwealth Building)
  Portland, OR 97204

Abstract: Hoare’s “assignment axiom” is noted for its simplicity and elegance, which seems to suggest that practical implementations are somehow “easy”. This talk will focus on our experience with SPARK – a programming language and toolset whose principal design goal is the provision of a sound Hoare-style verification system. I will concentrate on the “small print” and various fiddly (but essential) langauge features, such as volatility, I/O, dealing with commercial compilers, soundness and so on, that make the system much harder to implement than you might think.

Bio: Rod Chapman is a Principal Engineer with Praxis, specializing in the design and implementation of safety and security-critical systems. He currently leads the development of the SPARK language and its associated analysis tools.

Rod is a well-known conference speaker and has presented papers, tutorials, and workshops at many international events including SSTC, NSA HCSS, SIGAda, Ada-Europe and the Society of Automotive Engineers (SAE) World Congress. In addition to SPARK, Rod has been the key contributor to many of Praxis’ major projects such as SHOLIS, MULTOS CA, Tokeneer and Software verification tools. He received a MEng in Computer Systems and Software Engineering and a DPhil in Computer Science from the University of York, England, in 1991 and 1995 respectively. He is a Chartered Engineer, a Fellow of the British Computer Society, and also an SEI-Certified PSP Instructor.

The November 3rd Galois Tech Talk will be delivered by Ki Yung Ahn, titled “Testing First-Order-Logic Axioms in AutoCert.”

• Date: Tuesday, November 3rd, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.
  421 SW 6th Ave. Suite 300
  (3rd floor of the Commonwealth Building)
  Portland, OR 97204

Abstract: AutoCert is a formal verification tool for machine generated code in safety critical domains, such as aerospace control code generated from MathWorks Real-Time Workshop.  AutoCert uses Automated Theorem Proving (ATP) systems based on First-Order-Logic (FOL) to formally verify safety and functional correctness properties of the code.  These ATP systems try to build proofs based on user provided domain-specific axioms, which can be arbitrary First-Order-Formulas (FOFs).  That is, these axioms are the crucial trusted base in AutoCert.  However, formulating axioms correctly (i.e.  precisely as the user had really intended) is non-trivial in practice, and speculating validity of the axioms from the ATP systems is very hard since theorem provers do not give examples or counter-examples in general.

We adopt the idea of model-based testing to aid axiom authors to discover errors in axiomatization.  To test the validity of axioms, users can define a computational model of the axiomatized logic by giving interpretations to each of the function symbols and constants as computable functions and data constants in a simple declarative programming language.  Then, users can test axioms against the computational model with widely used software testing frameworks.  The advantage of this approach is that the users have a concrete intuitive model with which to test validity of the axioms, and can observe counterexamples when the model does not satisfy the axioms.  We have implemented a proof of concept tool using Template Haskell, QuickCheck, and Yices.

(This is a joint work with Ewen Denney at SGT/ NASA Ames Research Center, going to be presented in the poster session at Asian Symposium on Programming Languages and Systems this December.)

Bio: Ki Yung Ahn is a Ph.D student at Portland State University working with Tim Sheard and other members of the TRELLYS project, designing and implementing a dependently typed programming language that is general purpose programming friendly. He received a BS in Computer Science from KAIST in 2002, worked as online storage service server programmer at Gretech before joining graduate program at Portland State University in 2005.  He has been working on Shared Subtypes, Korean translation of “Programming in Haskell” by Graham Hutton, and enjoying other small funs of Haskell hacking.

The October 27th Galois Tech Talk will be delivered by Tanya Crenshaw, titled “How to choose between a screwdriver and a drill.”

• Date: Tuesday, October 27th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.
  421 SW 6th Ave. Suite 300
  (3rd floor of the Commonwealth Building)
  Portland, OR 97204

Abstract: Suppose you have two different algorithms to compute the same result. One is clearly safe. It is simple enough to verify. The other has more desirable features, but it is too complicated to verify. You want a system that can choose between these two algorithms while meeting its quality of service goals. This is the intuition behind Lui Sha’s Simplex Architecture. The intuition is simple, but its verification is not. Implementations of the Simplex Architecture are reactive systems whose properties are not always easy to express. In this talk, I’ll describe the history of Simplex, the challenges of verifying its safety properties, and a variety of approaches to modeling it, from an architecture description language to an executable specification language.

Bio: Tanya L. Crenshaw is an assistant professor of computer science at the University of Portland. She teaches courses in both Computer Science and Electrical Engineering and conducts research into security for embedded systems. Before University of Portland, she worked for Wind River and Sharp Microelectronics and studied at the University of Illinois at Urbana-Champaign where she completed her Ph.D. (Her personal web-page is at: http://kaju.dreamhosters.com/.)

The October 20th Galois Tech Talk will be delivered by Thomas DuBuisson, titled “Writing Linux Kernel Modules with Haskell.”

• Date: Tuesday, October 20th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.
  421 SW 6th Ave. Suite 300
  (3rd floor of the Commonwealth Building)
  Portland, OR 97204

Slides for this talk are now available.

Abstract: Current operating systems are developed and extended primarily with imperative languages that lack in expressiveness and safety.  Pure and functional languages fill these gaps nicely but existing tools are not ideal fits and the language abstracts away important environmental information.

This talk will focus on modifications of the Glasgow Haskell Compiler to generate suitable code and nuances of binding to the Linux API. Short-comings of the language and tools will be identified along with known workarounds and potential engineering efforts.

Bio: Thomas DuBuisson is a PhD student in Computer Science at Portland State University, working with advisor Andrew Tolmach.  Current research efforts revolve around the use of functional languages for systems programming and improving runtime system security.

We have a new position paper on the use of EDSLs and Haskell for tackling the “programmability gap” of emerging high performance computing architectures — such as GPGPUs. It will be presented tomorrow at LACSS in Santa Fe. (Download) :: PDF

Slides for the talk, including a 10 minute guide to EDSLs in Haskell, and a 10 minute guide to multicore programming in Haskell, can be found here :: PDF.

Domain Specific Languages for Domain Specific Problems
Don Stewart, Galois.
Workshop on Non-Traditional Programming Models for High-Performance Computing, LACSS 2009.

As the complexity of large-scale computing architecture increases, the effort needed to program these machines efficiently has grown dramatically. The challenge is how to bridge this “programmability gap”, making the hardware more accessible to domain experts. We argue for an approach based on
executable embedded domain specific languages (EDSLs)—small languages with focused expressive power hosted directly in existing high-level programming languages such as Haskell. We provide examples of EDSLs in use in industry today, and describe the advantages EDSLs have over general purpose languages in productivity, performance, correctness and cost.

Thanks to Magnus Carlsson, Dylan McNamee, Wouter Swiestra, Derek Elkins and Alex Mason for feedback on drafts.

The October 13th Galois Tech Talk will be delivered by Brian Huffman, titled “Constructing a Universal Domain for Reasoning About Haskell Datatypes.”

• Date: Tuesday, October 13th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.
  421 SW 6th Ave. Suite 300
  (3rd floor of the Commonwealth Building)
  Portland, OR 97204

Abstract: Existing theorem prover tools do not adequately support reasoning about general recursive datatypes. Better support for such datatypes would facilitate reasoning about a wide variety of real-world programs, including those written in continuation-passing style, that are beyond the scope of current tools.

This paper introduces a new formalization of a universal domain that is suitable for modeling general recursive datatypes. The construction is purely definitional, introducing no new axioms. Defining recursive types in terms of this universal domain will allow a theorem prover to derive strong reasoning principles, with soundness ensured by construction.

Bio: Brian Huffman is a PhD student in Computer Science at Portland State University, working with advisor John Matthews. He studies formal reasoning with the Isabelle theorem prover, specializing in formalized mathematics and semantics of functional languages. He is currently the maintainer of Isabelle/HOLCF, a logic for domain theory.

The October 6th Galois Tech Talk will be delivered by Lee Pike, titled “Roll Your Own Test Bed for Embedded Real-Time Protocols: A Haskell Experience“

[Note: Lee has recently presented this talk at the Haskell Symposium'09 in Edinburgh. Further info and downloadable artifacts are available at his personal web-site.]

• Date: Tuesday, October 6th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.
  421 SW 6th Ave. Suite 300
  (3rd floor of the Commonwealth Building)
  Portland, OR 97204

Abstract: We present by example a new application domain for functional languages: emulators for embedded real-time protocols. As a case-study, we implement a simple emulator for the Biphase Mark Protocol, a physical-layer network protocol in Haskell. The surprising result is that a pure functional language with no built-in notion of time is extremely well-suited for constructing such emulators. Furthermore, we use Haskell’s property-checker QuickCheck to automatically generate real-time parameters for simulation. We also describe a novel use of QuickCheck as a probability calculator for reliability analysis.

Bio: Lee Pike is a member of the technical staff at Galois. Previously, he was a research scientist with the NASA Langley Formal Methods Group, primarily involved in the SPIDER project. His research interests include applying formal methods to safety-critical and security-critical applications, with a focus on industrial-scale endeavors.