Machine-Generated Code That Works

Table of Links

1 Introduction

2 Dancing Links

3 The Rust Programming Language

4 RAC: Hardware/Software Co-Assurance at Scale

5 Rust and RAR

5.1 Restricted Algorithmic Rust

6 Dancing Links in Rust and 6.1 Definitions

6.2 Translation to ACL2

6.3 Dancing Links Theorems

7 Related Work

8 Conclusion

9 Acknowledgments and References

6.2 Translation to ACL2

We use Plexi to transpile the RAR source to RAC (not shown), then use the RAC translator to convert the resulting RAC source to ACL2. The translation of cdll_restore() appears in Fig. 6.

The first thing to note about Fig. 6 is that, even though we are two translation steps away from the original RAR source, the translated function is nonetheless quite readable, which is a rare thing for machine-generated code. Another notable observation is that struct and array ‘get’ and ‘set’ operations become untyped record operators, AG and AS, respectively — these are slight RAC-specific customizations of the usual ACL2 untyped record operators. Further, IF1 is a RAC-specific macro, and LOG>, LOG=, LOG<, and LOGIOR1 are all RTL functions. Thus, much of the proof effort involved with RAR code is reasoning about untyped records and RTL — although not a lot of RTL-specific knowledge is needed, at least in our experience.

One aspect of untyped records that can be tricky is that record elements that take on the default value are not explicitly stored in the association list for the record. For RAC untyped records, that default value is zero. Thus, it is easy for a given record to attain a nil value. When reasoning about arrays of such records, it is often desirable to be able to state that the array size remains constant. Thus, for example, for the CDLL array nodeArr of Section 6.1, we ensure that all CDLLNode elements of that array are non-nil by making sure that the alloc fields of the CDLLNode elements are always non-zero (2 or 3).