Notes on linking HOL and ACL2


Goals

The plan is to provide a semantically coherent link between the higher order logic supported by HOL4 and the first order logic and programming language supported by ACL2.

The official specification of ACL2 can be found in the papers A Precise Description of the ACL2 Logic and Structured Theory Development for a Mechanized Logic.

ACL2 has a number of features that make it highly suitable for system modelling. Our goal is to enable HOL users to employ ACL2 as a trusted oracle. A specific case study we have in mind is to experiment with ACL2 for executing the verified ARM model due to Anthony Fox.

Background

In 1999 Mark Staples implemented a tool for called ACL2PII for linking ACL2 and HOL. This was built with an early version of the Prosper Toolkit. It was quite successful, and was used by Susanto as part of his AMBA-ARM7 Formal Verification Platform.

One of the tricky things about translating from the untyped ACL2 logic to typed higher order logic is figuring out which types to assign. An example Staples gives is that, depending on the context, the ACL2 S-expression NIL might need to be translated to F (falsity of HOL type bool), or [] (the empty list) or NONE (the empty option). The ACL2PII user has to set up "translation specifications" that are pattern-matching rewrite rules to perform the ACL2 to HOL translation. These are encoded in ML and thus cannot be validated by proof.

The approach we are now developing starts from the pioneering ACL2PII work, but aims to minimise the amount of translation that needs to be trusted. Instead of having an ML datatype representing ACL2, we define a type of s-expressions inside higher order logic that faithfully models ACL2. We then define functions on s-expressions corresponding to the ACL2 primitives so that the ACL2 axioms hold. We thus construct a model of the ACL2 logic inside HOL. We are implementing inference rules that encode higher order types and functions into ACL2 s-expressions and functions on s-expressions. The tricky ML code of ACL2PII is replaced by inference rules of the HOL logic, so the results are guaranteed sound by HOL's fully-expansive LCF methodology.

Then translation from ACL2 formulas represented inside HOL to ACL2 is still a step that needs to be implemented in ML and trusted, but it is now a just a very straightforward printing step.

Results

This project has a backpack page here. For access contact Mike Gordon.

There is an evolving working paper entitled Connecting HOL to ACL2 by Mike Gordon, Warren Hunt and Matt Kaufmann.

 


Page maintained by Mike Gordon.
Version 1.04, Mon Aug 02, 2004
Version 1.06, Fri Aug 27, 2004
Version 1.08, Wed Dec 07, 2005