Verification of a Rust Implementation of Knuth’s Dancing Links using ACL2: Abstract and Introduction

Table of Links

• Abstract and Introduction
• Dancing Links
• The Rust Programming Language
• RAC: Hardware/Software Co-Assurance at Scale
• Rust and RAR
• Dancing Links in Rust
• Related Work
• Conclusion, Acknowledgments, and References

Abstract

“Dancing Links” connotes an optimization to a circular doubly-linked list data structure implementation which provides for fast list element removal and restoration. The Dancing Links optimization is used primarily in fast algorithms to find exact covers, and has been popularized by Knuth in Volume 4B of his seminal series The Art of Computer Programming. We describe an implementation of the Dancing Links optimization in the Rust programming language, as well as its formal verification using the ACL2 theorem prover. Rust has garnered significant endorsement in the past few years as a modern, memory-safe successor to C/C++ at companies such as Amazon, Google, and Microsoft, and is being integrated into both the Linux and Windows operating system kernels. Our interest in Rust stems from its potential as a hardware/software co-assurance language, with application to critical systems. We have crafted a Rust subset, inspired by Russinoff’s Restricted Algorithmic C (RAC), which we have imaginatively named Restricted Algorithmic Rust, or RAR. In previous work, we described our initial implementation of a RAR toolchain, wherein we simply transpile the RAR source into RAC. By so doing, we leverage a number of existing hardware/software co-assurance tools with a minimum investment of time and effort. In this paper, we describe the RAR Rust subset, describe our improved prototype RAR toolchain, and detail the design and verification of a circular doublylinked list data structure employing the Dancing Links optimization in RAR, with full proofs of functional correctness accomplished using the ACL2 theorem prover.

1 Introduction

The exact cover problem [17], in its simplest form, attempts to find, for an n × m matrix with binary elements, all of the subsets of the rows of the matrix such that all the column sums are exactly one. This basic notion naturally extends to matrix elements that are in some numerical range; indeed, the popular puzzle game Sudoku is an extended exact cover problem for a 9× 9 matrix with element values in the range of 1 to 9, inclusive.

The exact cover problem is NP-complete, but computer scientists have devised recursive, nondeterministic backtracking algorithms to find exact covers. One such procedure is Knuth’s Algorithm X, described in [17]. In this algorithm, elements of the matrix are connected via circular doubly-linked lists, and individual elements are removed, or restored, as the algorithm proceeds, undergoing backtracking, etc. As these removals and restorations out of/into the list are quite common, making these operations efficient is a laudable goal. This is where Knuth’s “Dancing Links” comes in, resulting in an optimized algorithm for finding exact covers which Knuth calls DLX (Dancing Links applied to algorithm X).