Entries in the “Misc” category
Industrial Strength Distributed Explicit Model Checking
July 27th, 2010 by Lee Pike
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
- title:
- Industrial Strength Distributed Explicit Model Checking
- presenter:
- John Erickson
- time:
- 10:30am, August 3rd, 2010
- location:
- Galois Inc.
421 SW 6th Ave. Suite 300, Portland, OR, USA
(3rd floor of the Commonwealth building) - Abstract:
- We present PReach, an industrial strength distributed explicit state model checker based on Murphi. The goal of this project was to develop a reliable, easy to maintain, scalable model checker that was compatible with the Murphi specification language. PReach is implemented in the concurrent functional language Erlang, chosen for its parallel programming elegance. We use the original Murphi front-end to parse the model description, a layer written in Erlang to handle the communication aspects of the algorithm, and also use Murphi as a back-end for state expansion and to store the hash table. This allowed a clean and simple implementation, with the core parallel algorithms written in under 1000 lines of code. This talk describes the PReach implementation including the various features that are necessary for the large models we target. We have used PReach to model check an industrial cache coherence protocol with approximately 30 billion states. To our knowledge, this is the largest number published for a distributed explicit state model checker. PReach has been released to the public under an open source BSD license.
- bio:
- John Erickson is a Design Engineer at Intel Hillsboro. He graduated with his PhD in Computer Science from The University of Texas at Austin in 2008. Currently he is working on the validation of uncore components in a 50+ core processor using a variety of formal and dynamic techniques. Past research interests include theorem proving with a focus on lemma generation and generalization in the context of induction.
Posted in Formal Methods, Misc, Tech Talks | Comments (0)
Tech Talk: Visualizing Information Flow through C Programs
April 22nd, 2010 by Lee Pike
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
The talk will be held at
Galois Inc.
421 SW 6th Ave. Suite 300, Portland, OR, USA
(3rd floor of the Commonwealth building)
Visualizing Information Flow through C Programs (slides)
Details:
- Presenter: Joe Hurd
- Date: Tuesday April 27, 2010
- Time: 10:30am
Abstract: The aim of the Automated Security Analysis project is to determine whether the information flows in a realistically-sized C codebase can be automatically deduced and communicated in an understandable way to someone unfamiliar with the code. To test this, a new information flow static analysis and visualization technique were developed, and implemented in a research prototype tool. This talk will present the novel features of the static analysis and demonstrate how the results are shown in the visualization tool: information flow between program storage locations is decomposed into two compositional properties, which can be computed using sound abstract interpretation techniques. For each deduced information flow, the static analysis keeps track of a set of source code locations which demonstrate the information flow, and this is used by the visualization component to communicate the information flow to a user browsing the source code.
Bio: Joe Hurd, Ph.D. is a Formal Methods Engineer at Galois, Inc. For the past ten years Dr. Hurd has been applying theorem proving techniques to formally verify the correctness of complex software, including probabilistic programs, elliptic curve cryptography and game tree analysis algorithms. He is also the developer of Metis, an automatic theorem prover for first order logic, and coordinates the OpenTheory project, a package management system for higher order logic theories. Dr. Hurd is an active member of the theorem proving research community, having organized conferences in 2005 and 2008, given invited talks, and regularly appears on program committees and reviews papers for conferences and journals. Prior to joining Galois in 2007, Dr. Hurd was a research fellow at Magdalen College, University of Oxford. He studied at the University of Cambridge, receiving a Masters level degree in Mathematics in 1997, and a Ph.D. in Computer Science in 2002.
Posted in Formal Methods, Misc, Tech Talks | Comments (5)
Solving n-Queens in Cryptol
April 11th, 2010 by Levent Erkok
The eight queens puzzle asks how to place eight queens on a chess board such that none of them attacks any other. The problem easily generalizes to n queens, using an nxn board. In this post, we’ll see how to solve the n-Queens puzzle in Cryptol, without lifting a finger!
Representing the board
It is easy to see that any solution to the n-Queens puzzle will have precisely one queen on each row and column of the board. Therefore, we can represent the solution as a sequence of n row numbers, corresponding to subsequent columns. For instance, the board pictured below (taken from the wikipedia page), can be represented by the sequence
3 7 0 2 5 1 6 4
recording the row of the queen appearing in each consecutive column, starting from the top-left position. (And yes, we always count from 0!)
Recognizing a valid solution
Let us start by asking a simpler question. How can we recognize that a given sequence of n row indices constitute a valid solution? We have to verify that the followings hold:
- The numbers must be between 0 and n-1. (Sanity checking.)
- The numbers should not be duplicated. (Ensures that there is exactly one queen per row.)
- For any pair of numbers in the sequence, their row-value difference should be different than their column-value difference. (Ensures that there are no diagonal conflicts.)
The first two conditions are fairly trivial. The last one simply says that if two queens are positioned such that their vertical and horizontal displacements are the same, then they are on the same diagonal: A situation we must avoid for all pairs of queens given.
Writing a Cryptol predicate
Having described how we will recognize an alleged solution, let us now consider how we can code this in Cryptol.
First, we will need a helper function that applies a given predicate to all the elements of a sequence and returns True if all elements satisfy the predicate. Naturally, we call this function all:
all : {n a} (fin n) => (a -> Bit,[n]a) -> Bit;
all (f, xs) = [|f x || x <- xs|] == ~zero;
The type of this function is worth spending a few moments looking at, as it demonstrates some crucial aspects of Cryptol’s type system that sets it apart from other languages. In particular, it says that the function all takes a sequence of n elements, each of some arbitrary size a. However, it also restricts n to be finite, i.e., the type system will complain if you pass all an infinite sequence. Then, we apply the predicate f to each element in the sequence, and check that the result consists of all True bits. (The polymorphic Cryptol value zero represents a value with an arbitrary shape with all bits set to False. The complement operator (~) flips all those bits to True.)
The second utility function we will need is a predicate that checks whether the elements of a given sequence are all distinct:
distinct : {a b} (fin a,fin b) => [a]b -> Bit;
distinct xs = diff == ~zero
where {
n = width xs;
diff = [|check (x, i)
|| x <- xs
|| i <- [0 .. (n-1)]
|];
check (x, start) = walk (start + 1)
where walk cur =
if cur == n
then True
else if xs @ cur == x
then False
else walk (cur + 1);
};
The function distinct is fairly simple: For each element in the sequence, it walk’s through the rest to make sure that none of the remaining elements are the same as that particular element. Note how Cryptol’s width function allows us to determine the size of the input sequence, and recurse properly.
Having done the heavy-lifting above, we can now write the predicate that recognizes a valid n-Queens solution in Cryptol:
type Solution(n) = [n][1+width n] -> Bit;
nQueens : {n} (fin n) => Solution(n);
nQueens qs = all(inRange, qs)
& distinct qs
& all(checkDiag, ijs)
where {
n = width qs;
inRange x = x < n;
ijs = [| (i, j) || i <- [0 .. n-1]
, j <- [0 .. n-1] |];
checkDiag (i, j) =
(i >= j) | (diffR != diffC)
where { qi = qs @ i;
qj = qs @ j;
diffR = if qi >= qj
then qi-qj
else qj-qi;
diffC = j - i;
};
};
The nQueens function simply executes our checks as we described above. It first makes sure that all the elements are inRange. (Note that we do not have to check for negative numbers since all Cryptol numbers are non-negative.) Then, we check that all the elements are distinct. Following this, we generate the pairs of indices ijs, and call checkDiag on all these pairs to make sure that the row and column differences do not match.
We can test this function in Cryptol, by providing sample input:
NQueens> nQueens [3 7 0 2 5 1 6 4] True NQueens> nQueens [3 7 0 2 5 6 1 4] False
In the second example, I swapped the elements 1 and 6; effectively putting the 6th queen on row 6 and the 7th on row 1. This creates a diagonal conflict as the reader can easily verify.
Solving n-Queens
It appears that all we have done so far is to write a Cryptol program to recognize whether a given solution to the n-Queens problem is valid. But, how do we actually solve the puzzle?
Remember that I promised to solve n-Queens without lifting a finger, and this is where Cryptol’s formal methods based tools come into the picture. Given any predicate (like nQueens above), Cryptol can find inputs that will satisfy it automatically, at the push of a button! (We have briefly described how this works in our previous post on Sudoku, so I shall not go into any details. Suffice it to say that one can exploit modern SAT/SMT solvers to generate automatic solvers for validity problems, and Cryptol provides just the right framework for doing so.)
Without further ado, here is how we solve n-Queens in Cryptol, without writing any additional code on top of what we have already seen:
NQueens> :set sbv NQueens> :set base=10 NQueens> :sat nQueens : Solution(8) (nQueens : Solution(8)) [2 7 3 6 0 5 1 4] = True
The first command puts Cryptol in the sbv mode, which allows for the use of SAT/SMT solvers. The second command tells Cryptol to print results in base 10. Finally, the :sat command finds satisfying assignments for predicates. The type-signature on the :sat command indicates that we are interested in solutions for 8-queens, for which we are given a solution almost instantaneously!
If you look at the wiki-page for n-queens, you will see that they claim there is always a solution when n=1 and n>=4. We can indeed verify that there are no solutions when n is 2 or 3, using Cryptol:
NQueens> :sat nQueens : Solution(2) No variable assignment satisfies this function NQueens> :sat nQueens : Solution(3) No variable assignment satisfies this function
While these two properties are easy to see, it’s quite valuable to get independent verification!
In practice..
We would be remiss if we didn’t mention some of the actual uses of the satisfiability checker in the Cryptol tool chain. The most important application is in verifying functional equivalence of two functions. If f and g are two functions, then they are functionally equivalent exactly when the predicate (\x -> f x != g x) is not satisfiable. (Conversely, if this predicate is satisfiable then the satisfying value is where f and g disagree, indicating a potential bug.) More importantly, f and g need not be both written in Cryptol. The toolchain allows performing equivalence checking between functions written in VHDL, C, and Java (with varying degrees of “seamless” integration!). Furthermore, this is also how we make sure our compiler produces correct code: The function g can be generated code, for instance in one of Cryptol’s intermediate languages as we compile Cryptol to FPGA descriptions. In summary, we can check the equivalence of 3rd party code (generated or hand-written) against “gold” Cryptol specifications, increasing assurance in the correctness of crypto-implementations.
Download
You can download the Cryptol solution for n-Queens. Cryptol licenses are also available free of charge at www.cryptol.net, although I should note that the SAT/SMT based backends are only available in the full-releases of Cryptol, which requires a simple form to be filled before downloading. Enjoy!
Posted in Cryptography, Formal Methods, Functional Programming, Misc, Technology | Comments (8)
The Semantics of Asynchronous Exceptions
March 4th, 2010 by donstewart
John Launchbury presented a Galois Developer Symposium lunch on March 4th, 2010, where he presented the semantics for asynchronous exceptions in Haskell. In particular, discussion concentrated on the interactions between Concurrent Haskell, laziness and exceptions.
Follow the talk online, or download the pdf.
Posted in Misc | Comments (1)
POPL 2010, Day 1
January 21st, 2010 by john
Here are some talks that caught my attention on the opening day of POPL 2010.
Reconfigurable Asynchronous Logic Automata, Neil Gershenfeld
In this invited talk, Neil proposed that we throw out the sequential model of computation from Turing and Von Neumann, and re-imagine computing from the ground up, more along the line of physics as it is manifested in the world. This might be the way forward given the huge power demands that will arise from traditional architectures as they become more and more powerful. Rather than imposing a top-down structure on the machine, Neil propose we consider systems built up from cellular automata. In ALA each cell is able to do a basic logic operation or, in RALA, reconfigure other cells. Built around 2D grids, and computing in parallel without any global clock, the automata are able to compute many basic functions in linear time, including multiplication and sorting (of course, they also take a linear number of cells to do so).
What I liked about this talk is that it called on me to think more broadly about the nature of computation. I don’t think I buy the line that how we do computing today is wrong. But I do believe that computing and information theory is going to become more and more important in the development of many other subjects, including physics and biology. I also believe that we will need to harness many more structures to do computing rather than simply relying on gates burned in silicon. Coincidentally, at lunch today Luca Cardelli was telling me about his explorations in computing with DNA. Fascinating stuff!
At the lowest levels, the primitive components of computation reflect the computational substrate, so they are very different from one instantiation to another. As primitive computational elements become combined, however, the different descriptions become more abstract, and start to look more and more alike. The same mathematical operations may arise in each form, for example. That makes me wonder what the space of truly computationally-neutral specifications looks like: how might we program in such a way that we really don’t have a preference for what substrate we map the computation onto. We already consider FPGAs, GPUs and CPUs as standard targets for languages like Cryptol. Let’s conceptually add DNA and RALA to the list, and see if that would have us change anything.
A Simple, Verified Validator for Software Pipelining, Jean-Baptiste Tristan & Xavier Leroy
Software pipelining is a compiler transformation that reorders loop code to make more efficient use of the CPU and memory accesses. Code from many different iterations of the loop might be drawn together and overlapped to execute out of order, and perhaps in parallel. The question is how to verify that the pipelining has been done correctly.
The paper proposes using symbolic evaluation. It describes an equivalence principle which requires proving two separate commutativity properties. These may both be shown by symbolic evaluation of the instruction code, being careful to handle the small differences (such as different temporary variables in the two paths). Overall the process is simple enough that it could be a standard component of any compiler, even if the compiler is non-verifying overall.
A Verified Compiler for an Impure Functional Language, Adam Chlipala
Handling object-level variables in proofs is a real pain, one that is hard to eliminate. This paper has an interesting way of dealing with them. It describes a Coq verification of a compiler for Untyped Mini-ML with references and exceptions, compiling to an idealized assembly code.
Now, using explicit object variables leads to lots of lemmas about substitution. On the other hand, full higher-order abstract syntax (HOAS) would lead quickly to non-termination, and hence unsoundness. So instead, the paper introduces a closure semantics in which variables are just numbers pointing into a heap. Many operations that would reorder substitutions (and hence require big proofs) don’t affect the closure heap, so the proofs go through easily.
The paper also uses a high degree of proof automation: it has a generic proof script that looks at the hypotheses and goals, and decides what approaches to try. The proof script is a bit slow because the evaluation mechanism of Coq wasn’t designed for this particularly (but see my blog post from PADL about accelerating normalization). However, because the proof is highly automatic, it is not hard to evolve the compiler and proof simultaneously. In fact, the compiler and proof were developed incrementally in exactly this way.
Verified Just-in-Time Compiler on x86, Magnus Myreen
JIT compiling has become standard for accelerating web pages, amongst other things. Good JIT compilers can take into account the input to the program as well as the program itself. But it is hard to get them right, as witnessed apparently by a recent Firefox bug.
An aspect that makes verification tricky is that code and data are mixed: a JIT compiler essentially produces self-modifying code. The paper provides a programming logic for self-modifying code by adapting Hoare triples so that there is both “before” and “after” code. Some practical issues also need to be handled: for example, the frame-property has subtleties regarding the instruction cache, and code-updates can sometime happen too recently to show up in the current instruction stream. The x86 documentation is a little vague about how soon code-modifications can be relied on to be present.
The end result is a verified JIT compiler from a toy input byte-code language, but mapping to a realistic semantics for x86. The compiler produces comparable code quality to C for a GCD example.
Posted in Misc | Comments (0)
PADL/PEPM 2010, Day 2
January 20th, 2010 by john
Again, here are a few talks that caught my attention and I thought I would share my impressions. Enjoy!
An Ode to Arrows, Hai Liu & Paul Hudak (PADL 2010)
Representing the infinite tower of derivatives of a function as a lazy list has become popular in the Haskell world, the most recent example being Conal Elliott’s paper on Beautiful Differentiation at ICFP 2009. This work explores taking the same ideas and using them to express systems of Ordinary Differential Equations.
A natural translation of these ideas into Haskell requires recasting the ODEs in an integral form, rather than a purely differential form, leading to a shallow embedding of the equations as recursive equations in Haskell. Unfortunately, this simple translation leads to quadratic computational complexity, in both time and space. Memoization can address this moderately well, except that one is left with the problems of managing (and freeing) the memo-tables.
Moving to arrows leads to a better solution. The recursion is expressed using Paterson’s ‘loop’ construct, which puts it in the control of the programmer. When combined with Causal Commutative Arrows (http://lambda-the-ultimate.org/node/3659) the circuits can be optimized into tight iterative loops, with dramatic improvements in performance.
A DSL Approach to Protocol Stack Implementation, Yan Wang & Veronica Gaspes (PADL 2010)
Implementations of network code are very hard to connect with the specifications, leading to major challenges for maintenance. This is significant for embedded devices which need implementations that appropriately trade off power, speed, and memory usage. To that end, IPS is a DSL for generating network code. It allows packet formats to be defined using dependencies between fields, handles the interaction of protocol and packet, and provides a framework for constructing the protocol stacks.
In a comparison exercise, IPS was used to generate code for the Rime protocol stack. Compared with the published hand-written version in C, the IPS code was 1/4 of the size of the C, but produced an executable 25% larger. The performance on sending packets was 10% worse in the IPS version, but both versions were equivalent for receiving packets.
No measurements were given for ease of maintenance or design exploration between the two versions, but I know which one I would prefer to have to work with…
I/O Guided Detection of List Catamorphisms, Martin Hofmann & Emanuel Kitzelmann (PEPM 2010)
Having the computer write its own programs has always been appealing. You provide some input/output pairs and the machine comes up with a generalization expressed as a program that has the same behavior. Broadly, there are two ways to do this: analytical (where the structure of the data is examined to build the program), and generate & test (where many programs are produced, and their behavior improved, perhaps by evolutionary combinations).
This work uses the idea of catamorphisms (also known an fold or reduce functions) as a template to explore, when the i/o pairs comes from a recursive data type (just lists at the moment, I think). Using the fact that if a function g satisfies ‘g [] = v’ and ‘g (x:xs) = f x (g xs)’ for some ‘f’ and ‘v’, then ‘g = fold f v’, the system figures out what the i/o pairs for the sub-functions would be, and then tries to deduce the definitions. It includes specific smarts that notice when the form of the function corresponds to a ‘map’ or ‘filter’.
Bridging the Gap Between Symbolic and Efficient AES Implementation, Andrew Moss & Dan Page (PEPM 2010)
Different implementations of AES, the standard for block encryption, run at very different speeds. The original reference implementation takes about 840 cycles per round, the Open SSL implementation takes 30, and a top performing assembly code version takes 21.6 cycles per round. The CAO DSL and compiler described in this paper takes a high-level spec and compiles it, producing code that takes 23 cycles per round. Impressive.
CAO is a sequential language, designed to be easily related to the pseudo code that crypto specifications often use. A significant amount of effort in the compiler then goes into deducing what parallelism is possible and how best to balance the work. CAO has matrices as first class objects, to allow the compiler opportunity to deduce good representations. There are also optimizations to convert references from the matrices in their entirety to references to the appropriate sub-portions, so as to eliminate unnecessary additional sequential dependencies. The compiler also has some optimizations that are specific to AES.
Clone Detection and Elimination for Haskell, Christopher Brown & Simon Thompson (PEPM 2010)
I liked this talk partly because it reminded me to go and play with HaRe (https://www.cs.kent.ac.uk/projects/refactor-fp/hare.html). The Haskell Refactorer is an Emacs and Vim tool for manipulating Haskell 98 programs, providing structural transformation (like fold/unfold), altering data types (like adding or eliminating arguments), slicing, and now, clone elimination (cue Star Wars music).
The clone eliminator finds repeated code forms above a threshold size, and deduces the least-general generalization of the code to invent new functions if necessary. Clone detection is entirely automatic, but it is up to the programmer to decide which ones to act upon — sometimes adding abstraction helps the structure of a program, and sometimes it obscures it. It works within monadic code too.
HaRe works mostly at the AST level, though it does use the raw token stream for some of its discovery. It also works across modules.
Making “Stricterness” More Relevant, Stefan Holdermans & Jurriaan Hage (PEPM 2010)
The old approaches to strictness were all denotational, but to actually use strictness within the compiler it is better to have a syntax-driven formulation, i.e. in logic. There is a nice approach which uses the concept of ‘relevance’, where ‘x’ is relevant to ‘e’ if every evaluation of ‘e’ demands ‘x’. Clearly, relevance is equivalent to strictness.
But actually it doesn’t work so well in the presence of ’seq’. The original formulation of relevance assumed that the only time a function would be evaluated was at its point of application. Then there is no way to distinguish ‘undefined’ from ‘\x->undefined’. ‘Seq’ changes all that. The paper shows how to fix relevance by tracking which lambdas are used applicatively (i.e. applied somewhere in the program in a place that will be evaluated). The definition is circular, but the least solution is the one intended.
Posted in Misc | Comments (0)
PADL/PEPM 2010, Day 1
January 19th, 2010 by john
Here are some papers which caught my imagination at this year’s PADL and PEPM conferences in Madrid.
O Partial Evaluator, Where art thou? Lennart Augustsson (PEPM 2010)
In this invited talk, Lennart walked us through his personal engagement with PE-like code transformations that he has confronted directly in his career, which has consisted of Haskell programming in a wide variety of commercial and industrial settings. The examples included optimizing airline scheduling code for Lufthansa, eliminating unnecessary hardware elements in Bluespec compilation, and generating efficient Monte-Carlo computations in investment banking.
In Bluespec, Lennart needed to introduce a ‘tabulate’ function which produces a table-driven implementation of its function argument. It is a powerful idea, but it requires a sufficiently powerful set of transformations for its boilerplate to get simplified away. In this case, Lennart needed to introduce a term ‘_’ which means “don’t care”, i.e. any convenient result can be returned. During unfolding and partial evaluation, ‘_’ could be replaced with any term that would help the partial evaluator make good progress on simplification. Semantically, this is a form of refinement of non-determinism performed during code transformation (in fact, I’m still not sure what the correct denotational approach to its semantics would be). Lennart then explored using ‘tabulate’ directly in Haskell, but found it next to impossible to get the GHC simplifier to do enough transformation.
The Paradise ESDL is like Bluespec in that it uses the Haskell framework to bolt together primitive elements from a lower level language. In this case, the efficiency opportunities arise from, say, 18-argument functions being called repeatedly with 15 known arguments. Lennart introduced a ‘compile’ function which is semantically the identity function, but which invokes a run-time compilation. Yet again, Lennart found himself writing essentially the same kind of code he had previously written in a different setting. Each time it is fairly simple partial evaluation.
Where oh where is the partial evaluator for Haskell? And don’t worry about self-application or anything fancy like that. Just something that is solid and reliable.
Explicitly Typed Exceptions for Haskell, Jose Iborra (PADL 2010)
Java gives you safe exceptions, in that if you don’t handle an exception that could be raised, the compiler will complain. Currently Haskell does not. This paper builds on Simon Marlow’s work of providing an exception library with existentially-quantified exceptions, that provide access to the exception through class methods. Marlow’s exceptions work very nicely with the type system, allowing exception and non-exception code to be intermingled. If only there was a way still to know which particular exceptions could be raised …
Iborra to the rescue! He adapts Marlow’s exceptions with additional class constraints that track exactly which exception could be raised, fulfilling those constraints when a handler for the exception is provided. Unhandled exceptions show up as missing instances (of handlers), pinpointing the code that is at fault. It all works very beautifully. The downside? He needs to use overlapping instances to be able to ’subtract’ that constraints. Hmmm. Normally I’m very down on overlapping instances: it seems really fragile to rely on details of the type-inference engine to select what code should run. But this is a particularly benign case: here the overlapping instances are over phantom type variables, so the same code will run in either case. Maybe Haskell should allow that in general; overlapping instances are fine if the same run-time code is produced however the instances are resolved.
Conversion by Evaluation, Mathieu Boespflug (PADL 2010)
Proof tactics in theorem provers often require large lambda terms to be normalized. For example some Coq tactics perform reflective computation over other Coq terms. This reduction can be quite inefficient when done explicitly, because of the interpretive overhead, yet the result of evaluation needs to be in a form where the final lambda term can be examined.
This paper shows the how to interpret explicit lambda terms efficiently by mapping them into a underlying evaluation mechanism of the host language (e.g. Haskell). The approach is deceptively simple and consists of a set of straightforward optimizations (higher-order abstract syntax, currying, de Bruijn indices etc). Astonishingly, the result is that the evaluation incurs only a 10-30% overhead compared with using the underlying evaluator directly! A must-read for anyone interested in reflective evaluation.
Optimizing Generics Is Easy! Jose Pedro Magalhaes et al (PEPM 2010)
Generic programming is a way to provide a programmable version of the deriving concept that arises in Haskell. The problem is that the current libraries for implementing generics introduce performance overheads from 50% to 16x compared with writing the original by hand. This paper presents a framework for doing generics using type families to represent the components of algebraic datatypes, together with overloaded operators for mapping between the generic datatype and any user datatype.
GHC does a good job of rewriting much of the overhead away, but needs to be encouraged to do the best it can. There are GHC flags to control decision thresholds for inlining etc that turn out to enable GHC to completely remove the overhead of the generic code, producing in some cases exactly the code that would get written by hand. The open problem is that increasing the threshold over the whole program might have negative effects elsewhere in the compilation, so a mechanism for localizing the effect of increased thresholds would be valuable.
Posted in Misc | Comments (0)
Shuffling a deck of cards, Cryptol style
December 26th, 2009 by Levent Erkok
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:
- The input has to be of even length (2*a),
- The input has to be finite (fin a),
- The output has two components, each of which has precisely a elements, that is, half the input,
- 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.
Posted in Formal Methods, Misc, Technology | Comments (2)
Tech Talk: John Launchbury presents Conal Elliott’s “Beautiful Differentiation”
December 9th, 2009 by Lee Pike
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.
Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.
Posted in Functional Programming, Haskell, Misc, Tech Talks | Comments (2)
Verifying Legato’s multiplier in Cryptol
July 8th, 2009 by Levent Erkok
Consider the following multiplication algorithm, coded in Mostek 6502 Assembler:
LDX #8 ; 1; load X immediate with the 8
LDA #0 ; 2; load A immediate with the 0
CLC ; 3; set C to 0
LOOP ROR F1 ; 4; rotate F1 right circular through C
BCC ZCOEF ; 5; branch to ZCOEF if C = 0
CLC ; 6; set C to 0
ADC F2 ; 7; set A to A+F2+C and C to the carry
ZCOEF ROR A ; 8; rotate A right circular through C
ROR LOW ; 9; rotate LOW right circular through C
DEX ;10; set X to X-1
BNE LOOP ;11; branch to LOOP if Z = 0
This program comes from Wilfred Legato’s paper “A Weakest Precondition Model for Assembly Language Programs.” It multiplies the contents of the memory locations F1 and F2; each of which is 8-bits wide. The result is stored in the accumulator register A and the memory location LOW, each of which is, again, 8-bits. It holds that:
F1 * F2 = 256 * A + LOW
when the algorithm terminates, correctly handling the overflow. It is worth spending a moment or two pondering how this algorithm works; it is not at all obvious how the multiplication is done!
Legato’s challenge (as referred to in ACL2 circles) is to prove a deep-embedding of Legato’s algorithm correct with respect to a Mostek simulator coded in ACL2. We do not attempt to solve Legato’s challenge in Cryptol. We are merely interested in coding and proving that Legato’s multiplier is correct in Cryptol. Our interest stems from the fact that Legato’s algorithm is a truly interesting multiplier on its own right, and we would like to make sure that a straightforward encoding of it in Cryptol can be proven correct automatically by Cryptol’s verification tools. And of course, it’s just too hard to pass up on the opportunity to pay respect to the Mostek chip that powered the Commodore 64’s and Atari 800XL’s of our childhood.
A shallow embedding
The Cryptol solution to Legato’s problem will be a fairly shallow encoding of the multiplier, together with an automated proof of correctness. We choose to do a shallow encoding here since it allows us to focus on the multiplication algorithm itself, as opposed to the particulars of the underlying Mostek chip. Theorem proving based solutions (such as those given by ACL2 folks) will rightly pursue a deeper embedding of the algorithm and the Mostek architecture in general. Cryptol is not particularly suitable for deep embeddings. Representing Mostek assembly instructions directly as Cryptol functions is a much simpler and straightforward choice.
Looking at Legato’s multiplier above, we will represent each instruction (from 1 to 11) as a simple state transformer, taking a simplified representation of the Mostek machine state as input and delivering a new one. We will only represent parts of the state that matter for our problem. The following Cryptol type declaration succinctly captures what we need:
type Mostek = ( [8] // F1
, [8] // F2
, [8] // A
, [8] // X
, [8] // LOW
, Bit // C (Carry)
, Bit // Z (Zero)
);
Using this state representation, each instruction in the program can be modeled as a state transformer:
type Instruction = Mostek -> Mostek;
This takes care of the data-flow aspect of the embedding; but the question of how to model control-flow remains. We will simply use the host-language’s control-flow features, using the quintessential functional idiom: by calling functions! This is actually easier done than said, and here’s our embedding of the first instruction of the program:
// step1: LDX #8; load X immediate with the integer 8.
step1 : Instruction;
step1 (f1, f2, a, _, l, c, z) =
step2 (f1, f2, a, 8, l, c, z);
Let’s spend a minute explaining this in detail. The first step in the program loads the register X with the immediate value 8. Using our state-transformer model, our step1 function will receive a Mostek state (consisting of the “current” values of F1, F2, A, X, LOW, CARRY, and ZERO). The “effect” of this instruction is to put the value 8 into the register X, leaving everything else the same. Once this is done, the control goes to the next instruction, which we model by calling the function step2 (which is yet to be defined).
In this fashion, we can shallowly embed all the instructions in Legato’s multiplier, using Cryptol’s native functions and control-flow features. Of course, this is hardly a new idea, being the essence of the whole domain-specific embedded language saga: Using a rich host-language to “fake” other languages.
Following the recipe set by step1, it is easy to model the next two instructions:
// step2: LDA #0; load A immediate with the integer 0.
step2 : Instruction;
step2 (f1, f2, _, x, l, c, z) =
step3 (f1, f2, 0, x, l, c, z);
// step3: CLC; set C to 0 (Note the use of Bit False here)
step3 : Instruction;
step3 (f1, f2, a, x, l, _, z) =
step4 (f1, f2, a, x, l, False, z);
Step 4 is equally easy in terms of control flow, but is tricky in terms of operation. After some head-scratching, one figures out that the term “rotate F1 right circular through C” means put the right-most bit of F1 in C, and put C in the first position of F1. A bizarre thing to do indeed, but that’s the beauty of Legato’s multiplier. The Cryptol translation is almost literal:
// step4: LOOP ROR F1; rotate F1 right circular through C.
step4 : Instruction;
step4 (f1, f2, a, x, l, c, z) =
step5 (f1', f2, a, x, l, b0, z)
where {
[b0 b1 b2 b3 b4 b5 b6 b7] = f1;
f1' = [b1 b2 b3 b4 b5 b6 b7 c];
};
The use of pattern matching in getting the bits out of f1, and the construction of the new value of f1 is idiomatic Cryptol. There’s one little catch though: Apparently Mostek was a big-endian machine, having a most-significant-bit-first representation. Cryptol is little-endian. So, instead of rotating the bits to right, we rotate them left.
The fifth instruction is the first time where we use Cryptol’s control-flow to model the Mostek jump instruction:
// step5 : BCC ZCOEF; branch to ZCOEF if C = 0.
// ZCOEF is step8 in our encoding
step5 (f1, f2, a, x, l, c, z)
= if c then step6 (f1, f2, a, x, l, c, z)
else step8 (f1, f2, a, x, l, c, z);
In this case, we simply receive a state, and depending on the value of the carry bit (C), we either go to the next step (i.e., no jump); or go to the ZCOEF instruction, which is going to be step-8 in our model. Easy as pie!
Step-6 is a replica of Step-3, clearing the carry bit:
// step6: CLC; set C to 0
step6 (f1, f2, a, x, l, _, z) =
step7 (f1, f2, a, x, l, False, z);
Step-7 is the most compute intensive part of the algorithm. The Cryptol encoding is a bit complicated due to the need to determine if there was a carry in the addition. Since all Cryptol arithmetic is modular, we are forced to do the computation at an extended bit-size. Otherwise, the modeling of the ADC instruction is quite straightforward:
// step7: ADC F2; set A to A+F2+C and C to the carry.
step7 (f1, f2, a, x, l, c, z) =
step8 (f1, f2, a', x, l, c', z')
where {
// 8-bit "modular" result
a' = a + f2 + (if c then (1:[8]) else (0:[8]));
// Was there a carry? Check that "real"
// result is larger than 255
a'Large : [9];
a'Large =
(a # zero) // extend a by adding zero bits
+ (f2 # zero) // same for f2
+ (if c then (1:[9]) else (0:[9]));
c' = a'Large > (255:[9]);
// set the zero flag
z' = a' == 0;
};
The Cryptol idiom x # zero simply represents the value x extended on the right with 0 bits. (Remember that Cryptol is little-endian, hence the addition of zero bits on the right does not change the value.) Due to the polymorphic type of the value zero, the result has any number of bits larger than equal to the original bit-size of x. (Since we only need 9-bits in this case, we could have coded the same via the expression x # [False], but the former expression is more idiomatic Cryptol.)
Steps 8 and 9 are similar to Step-4, using A and LOW instead of F1, respectively:
// step8 : ZCOEF ROR A; rotate A right circular through C.
step8 : Instruction;
step8 (f1, f2, a, x, l, c, z) =
step9 (f1, f2, a', x, l, a0, z)
where {
[a0 a1 a2 a3 a4 a5 a6 a7] = a;
a' = [a1 a2 a3 a4 a5 a6 a7 c];
};
// step9 : ROR LOW; rotate LOW right circular through C.
step9 : Instruction;
step9 (f1, f2, a, x, l, c, z) =
step10 (f1, f2, a, x, l', l0, z)
where {
[l0 l1 l2 l3 l4 l5 l6 l7] = l;
l' = [l1 l2 l3 l4 l5 l6 l7 c];
};
Step-10 simply decrements X, setting the ZERO flag appropriately:
// step10: DEX; set X to X-1
step10 : Instruction;
step10 (f1, f2, a, x, l, c, z) =
step11 (f1, f2, a, x', l, c, x'==0)
where x' = x-1;
Finally, step-11 either jumps back to the top of the loop (step-4), or finishes the algorithm:
// step11: BNE LOOP; branch to LOOP if Z = 0.
// LOOP is step4 in our encoding
step11 : Instruction;
step11 (f1, f2, a, x, l, c, z)
= if z
then (f1, f2, a, x, l, c, z) // done!
else step4 (f1, f2, a, x, l, c, z);
From a control-flow perspective, we indicate the end of the algorithm by simply returning the final Mostek state. It is worthwile at this point to go through the Cryptol embeddings of the instructions to see how they match-up to the Mostek assembly given by Legato.
Extracting the multiplier
Having coded Legato’s multiplier as a sequence of state transformers, we can simply call the function step1 to use it with an appropriate state. The following helper function simplifies this task for us, by loading the registers F1 and F2, and extracting the high and low bits at the end:
legato : ([8], [8], Mostek) -> ([8], [8]);
legato (f1, f2, st) = (hi, lo)
where {
// get the relevant parts
// to construct the starting state
(_, _, A, X, LOW, C, Z) = st;
// Run legato multiplier;
// final A is hi; and final LOW is low
(_, _, hi, _, lo, _, _) =
step1 (f1, f2, A, X, LOW, C, Z);
};
Note that legato still takes the starting machine state st as an argument. Legato’s claim (which we will shortly prove) is that the algorithm works correctly no matter what the initial state is, hence it is important to be explicit about the starting state.
To see legato in action, let’s just run it on a simple input:
legato> legato (12, 93, (9, 42, 3, 8, 1, False, True)) (4, 92)
where I just made up the initial state by plugging in some random values. If Legato is right, then it must be the case that
12 * 93 = 256 * 4 + 92
correctly computing the high and low bytes. And voila! Both sides equal 1116. Magic!
Correctness
If you do believe in magic, you can stop reading now. But I suspect most readers of the Galois blog will be looking for something more concrete. Surely, we must be able to give a better argument than claiming witchcraft for the correctness of our implementation.
Let us first formally capture what we mean by “correct,” by writing a Cryptol theorem that expresses our intuitive expectation:
theorem
legatoIsCorrect: {x y st}. x' * y' == 256 * hi' + lo'
where { (hi, lo) = legato (x, y, st);
hi', lo', x', y' : [16];
hi' = hi # zero;
lo' = lo # zero;
x' = x # zero;
y' = y # zero
};
Here’s the English reading of this theorem: “For all values of x, y, and st, if we run legato on these values and get the results hi and lo, then, it’ll be the case that x * y = 256 * hi + lo.” The only caveat is that we have to do arithmetic operations over 16 bit values (instead of 8), to make sure the theorem statement correctly captures the intended mathematical meaning. (Recall that all Cryptol arithmetic is modular with respect to the bit-size involved.) Hence, we simply add extra zero’s at the end to enlarge the arguments to 16 bits. Note that, we do not have to assert that the value of lo is at most 255; this is automatically guaranteed by the fact that it is an 8-bit value. Cryptol’s bit-precise type system saves the day!
Verification
Here’s what happens when I run cryptol on the file containing the above theorem:
$ cryptol legato.cry
Cryptol version 1.8.5, Copyright (C) 2004-2009 Galois, Inc.
www.cryptol.net
Type :? for help
Loading "legato.cry".. Checking types.. Processing.. Done!
*** Auto quickchecking 1 theorem.
*** Checking "legatoIsCorrect" ["legato.cry", line 147, col 1]
Checking case 100 of 100 (100.00%)
100 tests passed OK
[Coverage: 3.47e-14%. (100/288230376151711744)]
When Cryptol sees a theorem declaration in a loaded file, it automatically performs a quick-check run to provide feedback on its validity. In this case, Cryptol automatically created 100 random test values for the theorem and checked that each one of them satisfied the statement. This is a quick way of getting feedback on the correctness of theorems, courtesy of Cryptol at no additonal cost to the user!
While the quick-check run is promising, the coverage info indicates that we’ve barely scratched the surface. The entire state space in this case has 58 bits (8 each for x and y, plus the starting arbitrary state of the Mostek machine costing us an extra 42 bits; for a total of 58). The total number of possible inputs is, therefore, 258 or 288230376151711744. This is a huge number: If you had a computer that run 1-billion (109) test cases every second, it’d still take you over 9 years to go through all possible inputs!
Of course, we can do better. Cryptol’s theorem proving environment uses modern equivalence-checkers to prove such theorems automatically, at the push of a (virtual) button:
legato> :prove legatoIsCorrect Q.E.D.
And there, we’ve proved that our implementation of Legato’s multiplier is indeed correct for all possible inputs! (The above proof takes about 2.5 minutes to complete on my 3-year old MacBook Pro, using abc as the underlying equivalence checker in Cryptol’s symbolic mode. I should also note that the symbolic mode is only available in the full Cryptol release, for which free licenses are available.)
Closing thoughts
I must emphasize that we are not advocating Cryptol as a platform for doing proofs of algorithm correctness. Modern theorem provers such as ACL2, Coq, or Isabelle are the leading tools in this regard. (In particular, the logic behind Cryptol’s automated theorem prover is much less expressive, for starters.) Where Cryptol shines is in its restricted attention to bit-vectors and data-flow algorithms (cryptography being a prime application area), and it turns out that automated equivalence-checking based techniques do perform rather well for such problems. Our shallow embedding of Legato’s multiplier and the automated proof-of-correctness is a case in point.
There is one more important point to make. While push-button provers are indispensable in industrial practice, the final Q.E.D. you get from an interactive theorem prover such as ACL2 or Isabelle is much more satisfactory. For instance, we can hardly claim that the above proof increased our understanding of Legato’s algorithm in any sense, it just made us really believe it. I’m willing to bet that anyone who goes through a similar proof in ACL2 or Isabelle would have a much higher chance of having their “aha!” moment, where everything just sinks in…
On the practical side, however, nothing beats the fully-automated Q.E.D., especially when your boss is breathing down your neck!
Download
The Cryptol file containing Legato’s multiplier and the correctness theorem is here. The Cryptol toolset licenses are freely available at www.cryptol.net.
Posted in Formal Methods, Misc, Technology | Comments (0)
©2000–2010 Galois, Inc. All rights reserved. Terms of use. Contact Us