We introduce an efficient approach for optimization over orthogonal groups on highly parallel computation units such as GPUs or TPUs. As in earlier work, we parametrize an orthogonal matrix as a product of Householder reflections. However, to overcome low parallelization capabilities of computing Householder reflections sequentially, we propose employing an accumulation scheme called the compact WY (or CWY) transform - a compact parallelization-friendly matrix representation for the series of Householder reflections. We further develop a novel Truncated CWY (or T-CWY) approach for Stiefel manifold parametrization which has a competitive complexity and, again, yields benefits when computed on GPUs and TPUs. We prove that our CWY and T-CWY methods lead to convergence to a stationary point of the training objective when coupled with stochastic gradient descent. We apply our methods to train recurrent neural network architectures in the tasks of neural machine translation and video prediction.

This paper presents, we believe, the most comprehensive evidence of a theorem prover's soundness to date. Our subject is the Milawa theorem prover. We present evidence of its soundness down to the machine code. Milawa is a theorem prover styled after NQTHM and ACL2. It is based on an idealised version of ACL2' s computational logic and provides the user with high-level tactics similar to ACL2' s. In contrast to NQTHM and ACL2, Milawa has a small kernel that is somewhat like an LCF-style system. We explain how the Milawa theorem prover is constructed as a sequence of reflective extensions from its kernel. The kernel establishes the soundness of these extensions during Milawa's boot-strapping process. Going deeper, we explain how we have shown that the Milawa kernel is sound using the HOL4 theorem prover. In HOL4, we have formalized its logic, proved the logic sound, and proved that the source code for the Milawa kernel (1,700 lines of Lisp) faithfully implements this logic. Going even further, we have combined these results with the x86 machine-code level verification of the Lisp runtime Jitawa. Our top-level theorem states that Milawa can never claim to prove anything that is false when it is run on this Lisp runtime.

When using existing ACL2 datatype frameworks, many theorems require type hypotheses. These hypotheses slow down the theorem prover, are tedious to write, and are easy to forget. We describe a principled approach to types that provides strong type safety and execution efficiency while avoiding type hypotheses, and we present a library that automates this approach. Using this approach, types help you catch programming errors and then get out of the way of theorem proving.

Despite significant progress in formal hardware verification in the past decade, little has been published on the verification of microcode. Microcode is the heart of every microprocessor and is one of the most complex parts of the design: it is tightly connected to the huge machine state, written in an assembly-like language that has no support for data or control structures, and has little documentation and changing semantics. At the same time it plays a crucial role in the way the processor works. We describe the method of formal microcode verification we have developed for an x86-64 microprocessor designed at Centaur Technology. While the previous work on high and low level code verification is based on an unverified abstract machine model, our approach is tightly connected with our effort to verify the register-transfer level implementation of the hardware. The same microoperation specifications developed to verify implementation of teh execution units are used to define operational semantics for the microcode verification. While the techniques used in the described verification effort are not inherently new, to our knowledge, our effort is the first interconnection of hardware and microcode verification in context of an industrial size design. Both our hardware and microcode verifications are done within the same verification framework.

The ACL2 theorem prover is a complex system. Its libraries are vast. Industrial verification efforts may extend this base with hundreds of thousands of lines of additional modeling tools, specifications, and proof scripts. High quality documentation is vital for teams that are working together on projects of this scale. We have developed XDOC, a flexible, scalable documentation tool for ACL2 that can incorporate the documentation for ACL2 itself, the Community Books, and an organization's internal formal verification projects, and which has many features that help to keep the resulting manuals up to date. Using this tool, we have produced a comprehensive, publicly available ACL2+Books Manual that brings better documentation to all ACL2 users. We have also developed an extended manual for use within Centaur Technology that extends the public manual to cover Centaur's internal books. We expect that other organizations using ACL2 will wish to develop similarly extended manuals.

Formal verification, based on mechanical theorem proving, can provide unique evidence that systems are correct. Unfortunately this promise of correctness is, for most projects, not enough to justify its high cost. Since formal models and proof scripts offer few other direct benefits to system developers and managers, the idea of formal verification is abandoned. We have developed a way to embed functions from the ACL2 theorem prover into software that is written in mainstream programming languages. This lets us reuse formal ACL2 models to develop modern applications with features like graphics, networking, databases, etc. For example, we have written a web-based tool for hardware designers in Ruby on top of a 100,000+ line ACL2 codebase. This is neat: we can reuse the supporting work needed for formal verification to create tools that are useful beyond the formal verification team. The value added by these tools will help to justify the investment in formal verification, and the project as a whole will benefit from the precision of formal modeling and analysis.

And-Inverter Graphs (AIGs) are a popular way to represent Boolean functions (like circuits). AIG simplification algorithms can dramatically reduce an AIG, and play an important role in modern hardware verification tools like equivalence checkers. In practice, these tricky algorithms are implemented with optimized C or C++ routines with no guarantee of correctness. Meanwhile, many interactive theorem provers can now employ SAT or SMT solvers to automatically solve finite goals, but no theorem prover makes use of these advanced, AIG-based approaches. We have developed two ways to represent AIGs within the ACL2 theorem prover. One representation, Hons-AIGs, is especially convenient to use and reason about. The other, Aignet, is the opposite; it is styled after modern AIG packages and allows for efficient algorithms. We have implemented functions for converting between these representations, random vector simulation, conversion to CNF, etc., and developed reasoning strategies for verifying these algorithms. Aside from these contributions towards verifying AIG algorithms, this work has an immediate, practical benefit for ACL2 users who are using GL to bit-blast finite ACL2 theorems: they can now optionally trust an off-the-shelf SAT solver to carry out the proof, instead of using the built-in BDD package. Looking to the future, it is a first step toward implementing verified AIG simplification algorithms that might further improve GL performance.

In recent years, leading microprocessor companies have made huge investments to improve the reliability of their products. Besides expanding their validation and CAD tools teams, they have incorporated formal verification methods into their design flows. Formal verification (FV) engineers require extensive training, and FV tools from CAD vendors are expensive. At first glance, it may seem that FV teams are not affordable by smaller companies. We have not found this to be true. This paper describes the formal verification framework we have built on top of publicly-available tools. This framework gives us the flexibility to work on myriad different problems that occur in microprocessor design.

Theorem provers, such as ACL2, HOL, Isabelle and Coq, rely on the correctness of runtime systems for programming languages like ML, OCaml or Common Lisp. These runtime systems are complex and critical to the integrity of the theorem provers. In this paper, we present a new Lisp runtime which has been formally verified and can run the Milawa theorem prover. Our runtime consists of 7,500 lines of machine code and is able to complete a 4 gigabyte Milawa proof effort. When our runtime is used to carry out Milawa proofs, less unverified code must be trusted than with any other theorem prover. Our runtime includes a just-in-time compiler, a copying garbage collector, a parser and a printer, all of which are HOL4-verified down to the concrete x86 code. We make heavy use of our previously developed tools for machine-code verification. This work demonstrates that our approach to machine-code verification scales to non-trivial applications.

Interactive theorem proving requires a lot of human guidance. Proving a property involves (1) figuring out why it holds, then (2) coaxing the theorem prover into believing it. Both steps can take a long time. We explain how to use GL, a framework for proving finite ACL2 theorems with BDD- or SAT-based reasoning. This approach makes it unnecessary to deeply understand why a property is true, and automates the process of admitting it as a theorem. We use GL at Centaur Technology to verify execution units for x86 integer, MMX, SSE, and floating-point arithmetic.

We have developed a formal-methods-based hardware verification toolflow to help ensure the correctness of our X86-compatible microprocessors. Our toolflow uses the ACL2 theorem-proving system as a design database and a verification engine. We verify Verilog designs by first translating them into a formally defined hardware description language, and then using a variety of automated verification algorithms controlled by theorem-proving scripts. In this chapter, we describe our approach to verifying components of VIA Centaur’s 64-bit Nano, X86-compatible microprocessor. We have successfully verified a number of media-unit operations, such as the packed addition/subtraction instructions. We have verified the integer multiplication unit, and we are in the process of verifying microcode sequences that perform arithmetic operations.

Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual “social process” of mathematics, so instead we create and check them with theorem-proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier? We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are “always true”). Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higher-level proofs can be written more concisely than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified. To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some &phis;, there exists a Level 1 proof of &phis;. We then mechanically translate the Level 11 proof for each Level n into a Level n − 1 proof—that is, we create a Level 1 proof of Level 2’s fidelity, a Level 2 proof of Level 3’s fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs. In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1.

As part of an undergraduate engineering class project, a simulation of the Detroit Tigers offense was created to explore potential changes that would increase number of wins. More specifically, we seek to determine a lineup for an MLB team, the Detroit Tigers, that would maximize their potential runs. To answer our ultimate question of whether a manager actually maximizes runs scores, we compare our results to the Tigers' 2007 performance. We determine that though the Tigers did not use the ideal lineup as determined by our model, the lineup they did utilize was moderately robust, with ours winning 89.6 games versus the actual wins of 88 games. Additionally, we apply our model to a normative analysis of the Tigers ideal lineup for the 2008 season. This ideal lineup only changes the middle of the batting order (acceptable by management) and is predicted to win 99 games in the 2008 season.

Rewriting with lemmas is a central strategy in interactive theorem provers. We describe the Milawa rewriter, which makes use of assumptions, cal- culation, and conditional rewrite rules to simplify the terms of a rst-order logic. We explain how we have developed an ACL2 proof showing the rewriter is sound, and how this proof can accommodate our rewriter's many useful features such as free-variable matching, ancestors checking, syntatic restrictions, caching, and forcing.

We introduce the logical story behind file input in ACL2 and discuss the types of theorems that can be proven about file-reading operations. We develop a low level library for reasoning about the primitive input routines. We then develop a representation for Unicode text, and implement efficient functions to translate our representation to and from the UTF-8 encoding scheme. We introduce an efficient function to read UTF-8-encoded files, and prove that when files are well formed, the function produces valid Unicode text which corresponds to the contents of the file.We find exhaustive testing to be a useful technique for proving many theorems in this work. We show how ACL2 can be directed to prove a theorem by exhaustive testing.

We have written a new records library for modelling fixed-size arrays and linear memories. Our implementation provides fixnum-optimized O (log 2 n ) reads and writes from addresses 0, 1,..., n - 1. Space is not allocated until locations are used, so large address spaces can be represented. We do not use single-threaded objects or ACL2 arrays, which frees the user from syntactic restrictions and slow-array warnings. Finally, we can prove the same hypothesis-free rewrite rules found in misc/records for efficient rewriting during theorem proving.

1 ACL2 Workshop 2000 00-lusk-parallel[11] ACL2 for Parallel Systems Software: A Progress Report 00-wilding-stobj[42] Using a Single-Threaded Object to Speed a Verified Graph Pathfinder 00-sumners-bdds[54] Correcness Proof of a BDD Manager in the Context of Satisfiability Checking 00-shumsky-sdl[44] Developing a Framework for Simulation, Verification and Testing of SDL Specifications 00-manolios-pipeline[46] Verification of Pipelined Machines in ACL2 00-sumners-stuttering[53] An Incremental Stuttering Refinement Proof of a Concurrent Program in ACL2 00-reina-multiset[18] Multiset Relations: A Tool for Proving Termination 00-goerigk[74] Proving Preservation of Partial Correctness with ACL2: A Mechanical Compiler Source Level Correctness Proof 00-sawada-computed[34] ACL2 Computed Hints: Extension and Practice

We present a finite set theory implementation for ACL2. Our library represents sets as fully ordered lists, and provides efficient implementations of the typical set theory operations such as insertion, deletion, union, intersection, difference, cardinality, and sorting lists to create sets. It also includes facilities for quantifying predicates over sets, filtering sets by some criteria, and taking images of sets. We demonstrate that despite our insistence on full order, it is possible to mirror traditional set theoretic proof techniques and reason through membership. At the same time, we are able to benefit from having a unique representation for each set, which unifies the notions of set and element equality and allows us to handle nested sets trivially.

We present a new finite set theory implementation for ACL2 wherein sets are implemented as fully ordered lists. This order unifies the notions of set equality and element equality by creating a unique representation for each set, which in turn enables nested sets to be trivially supported and eliminates the need for congruence rules. We demonstrate that ordered sets can be reasoned about in the traditional style of membership arguments. Using this technique, we prove the classic properties of set operations in a natural and effortless manner. We then use the exciting new MBE feature of ACL2 to provide linear-time implementations of all basic set operations. These optimizations are made “behind the scenes” and do not adversely impact reasoning ability. We finally develop a framework for reasoning about quantification over set elements. We also begin to provide common higher-order patterns from functional programming. The net result is an efficient library that is easy to use and reason about.