ACL2 Workshop 2018
Abstracts

Why is creating formal specifications for real world systems is hard and what we can do about it? Some of the key problems are the semantic gap between the architects' intention and the written specification; challenges persuading different groups to adopt a common specification; the number and diversity of existing implementations; and the practical impossibility of formally verifying all implementations against the specification. I discuss lessons learned when creating a formal specification of the Arm Processor Architecture and using that specification to formally validate processors against the specification. And I discuss how those lessons can be applied in other contexts. This includes use of traditional testing, formal validation, social engineering and building a virtuous cycle to drive up the quality of the specification.

We present a formalization of an instant run-off voting scheme in ACL2 and describe some properties that we have proven about it. Close to home, one application of this formalization can be to choose the slogan winners for subsequent ACL2 Workshops.

I will discuss the ideal relationship between predicate refinement and equivalence refinement, ie: (Atype-p => Btype-p) => (Bequiv => Aequiv), and the conditions under which this relationship is preserved.

I will give a brief description of the graph library I have been working on including overall structure, design challenges, useful algorithms, and their specifications.

Kestrel's APT tool suite includes a tool that I've written for simplifying definitions. A major challenge is for the simplified definition to share structure, to the extent reasonably feasible, with the original definition. I developed a tool, directed-untranslate, for this purpose; but it was a continual struggle to present nice results for let, let*, mv-let, and b* expressions. In this talk I hint at how I largely solved that problem (so far!) by making separate calls to the ACL2 rewriter while descending through the top-level IF and LAMBDA calls of the definition's body. The point of this talk is to illustrate, once again, the well-known lesson that sometimes it's good not to get stuck on one approach.

In the Oracle Cloud, we offer "bare metal" compute nodes where the customer has complete hardware access to the system, rather than being confined to a VM. In such a setting it becomes imperative to securely wipe a machine before reprovisioning it for a new customer. Part of this process involves sending bootstrap firmware to the server's motherboard via an 8-bit microcontroller that hashes the firmware and attests its integrity by a digital signature. For speed reasons, much of the hashing algorithm was written in assembly code.

Oracle Labs used ACL2 to create a model of the AVR instruction set architecture, a specification of the SHA-256 hash function, and a formal proof of the functional correctness of the hand-written assembly code. We were then able to further optimize the assembly code and prove that the newer code was also correct.

The title is also the title of my new book, which will be the subject of the talk.

The Incans used khipu or structured cords of multi-colored strings with specific knots as a form of recording information for communication, accounting, posterity, and other purposes. Some properties and relationships of khipu have been deciphered but the capability to decode khipu is still elusive. We present a translation of the data from Khipu Database Project into ACL2 terms which when combined with an efficient evaluator in ACL2 allows for checking the validity of rules across khipu. We will demonstrate on some known khipu decoding patterns but also consider how to generate new candidate rules as well as properties that any collection of rules should have.