  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 doubly-linked list data structure employing the
Dancing Links optimization in RAR, with full proofs of functional correctness
accomplished using the ACL2 theorem prover.
