ACL2 Workshop 2017
Abstracts

Many deep issues plaguing today's financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Aesthetic Integration, we've pioneered the use of formal verification for analysing the safety and fairness of financial algorithms. With a focus on financial infrastructure (e.g., the matching logics of exchanges and dark pools), we'll describe the landscape, and illustrate our Imandra formal verification system on a number of real-world examples. We'll sketch many open problems and future directions along the way.

As the complexity of Oracle's SPARC processors increases, the limits of traditional design verification techniques become clear. These limits are exacerbated by the cost and fabrication time of modern semiconductor processes, and increasingly stringent first-silicon functional objectives. We can no longer rely on directed and pseudo-random testing methods to minimize the probability of a post tape-out bug seriously impacting system bringup and productization. Yet applying theorem-proving to specific areas of the design has yielded benefits beyond only ensuring functional correctness. It can reduce compute infrastructure needs, and has also yielded design improvements that would not have been obvious using traditional verification techniques. We will outline these aspects in Oracle's ACL2 experience.

Apply is a Common Lisp function that takes a function and a list of arguments and returns the result of applying the function to those arguments. Naively axiomatizing apply to handle all definable functions in ACL2's first order logic produces an inconsistent theory. One well-known source of inconsistency are functions like Russell's that doesn't ``terminate'' when applied to itself. A more idiosyncratic source of inconsistency concerns ACL2's LOCAL events in encapsulate and include-book that could allow the exportation of non-theorems about locally defined function symbols. In this talk we present a restricted version of apply that can handle what we call ``tame'' functions and ``mapping functions'', like FOLDR, that operate as expected on ``tame'' functional arguments. Our version of apply is consistent and avoids the LOCAL problem.

We very briefly argue for the pragmatic adequacy of our restricted apply in two senses: (a) features used by many programmers are supported and obviate the need for myriad special-purpose recursive functions like ``sum the squares of the elements of this list'', and (b) theorems about these ``higher order functions'' are provable and really mean what the user expects them to mean.

The GL bit-blasting library previously supported proving ACL2 theorems that could be reduced to SAT problems. A new addition to the library now supports problems in the domain of safety model checking, reducing a high-level ACL2 conjecture to an and-inverter-graph finite state machine model. The result is a problem that can be checked by a variety of tools, e.g., any entrant in the Hardware Model Checking Competition. We give a practical demo of the library illustrating its use on ACL2 machine models and SV hardware descriptions.

We are implementing a procedure for generalizing SMT counterexamples. In doing so we have developed a specification for what it means for a generalization to be correct and a formalization of our generalization algorithm. In proving that our algorithm satisfies our specification, we uncovered a subtle and interesting error in our generalization rules.

We continue from the work of proof reductions of fair stuttering refinement proofs of asynchronous systems to show how to further reduce these proofs in the cases where the tasks in question are finite state. We first reduce the requisite properties to a set of properties involving at most a single step of any single task and show how to generate GL theorems which are then checked efficiently via SAT. We then present how to transfer some of the definitional requirements of the requisite properties into model checking problems over a single task run. We present results using high-level definition of a lazy cache coherence protocol.

I'll discuss lessons from a case study, consisting of a sequence of verified checkers that validate SAT proofs. These culminate in an efficient checker that can be used in SAT competitions and in industry.

I'll introduce the acl2-doc Emacs-based browser for ACL2 documentation, with some focus on new features for finding ACL2 definitions in source code and books.

Formal verification of asynchronous circuits is known to be challenging due to highly non-deterministic behavior exhibited in these systems. One of the main challenges is that it is very difficult to come up with a systematic approach to establishing invariance properties, which are crucial in proving the correctness of circuit behavior. Non-determinism also results in asynchronous circuits having a complex state space, and hence makes the verification task much more difficult than in synchronous circuits. To ease the verification task by reducing non-determinism, and consequently reducing the complexity of the set of execution paths, we impose design restrictions to prevent communication between a module M and other modules while computations are still taking place that are internal to M. These restrictions enable our verification framework to verify loop invariants efficiently via induction and subsequently verify the functional correctness of asynchronous circuit designs. Our framework applies a hierarchical verification approach to support scalability. We demonstrate our framework by modeling and verifying the functional correctness of a 32-bit asynchronous serial adder.

Since the verification of the division/square-root unit, Oracle has focused on verifying control-oriented logic. We will describe how we used the tools stack and hand-written model for parts of the circuit to verify one of our control logic units. Taking this approach a step further, we hope to illustrate with a simple example how one can extract a single-cycle invariant and then grow that invariant to describe a circuit's behavior across multiple clock cycles.

Augmented Backus-Naur Form (ABNF) is a standardized formal grammar notation used in several Internet syntax specifications. This talk describes (i) a formalization of the syntax and semantics of the ABNF notation and (ii) a verified parser that turns ABNF grammar text into a formal representation usable in declarative specifications of parsers of ABNF-specified languages.

We report on initial experiments using J Moore's Codewalker to reason about programs compiled to the new WebAssembly intermediate form. We have employed the Codewalker method to create an interpreter for a subset of the WebAssembly instruction set, and have used Codewalker to analyze some simple programs compiled to WebAssembly form. We will provide a brief introduction to WebAssembly, Codewalker, and describe preliminary results.

As described in the O'Leary-Russinoff 2014 Workshop paper, MASC is a methodology for RTL verification that involves C-Verilog equivalence checking, translation from C to ACL2, and theorem proving using the ACL2 RTL library. In this talk, I'll describe some recent and ongoing industrial applications of MASC.

The length of a curve can be defined as the limit of the sum of the chord lengths in a partition. When this limit exists, the curve is called rectifiable. We show that when a complex-valued curve is continuously differentiable, the curve is also rectifiable, and the length of the curve can be computed by taking the integral of the norm of the curve's derivative. We use this result to verify the well-known formula for the circumference of a circle.

This talk describes how we use our Axe tools to reason about x86 binary code. It summarizes the Axe Rewriter, the Axe Equivalence Checker, and the Axe x86 Lifter. It gives two examples (popcount and TEA encryption) of lifting x86 binary programs into logic and verifying the lifted code by proving equivalence to formal specifications.