paint-brush
Proving Theorems for Rust’s Dancing Links in ACL2by@knuth

Proving Theorems for Rust’s Dancing Links in ACL2

by Knuth
Knuth HackerNoon profile picture

Knuth

@knuth

Knuth's mastery weaves theory and practice, a tale of computation,...

January 22nd, 2025
Read on Terminal Reader
Read this story in a terminal
Print this story
Read this story w/o Javascript
Read this story w/o Javascript
tldt arrow

Too Long; Didn't Read

160 theorems validate Rust’s Dancing Links implementation in ACL2, proving well-formedness and functional correctness of CDLL operations through automated verification.
featured image - Proving Theorems for Rust’s Dancing Links in ACL2
1x
Read by Dr. One voice-avatar

Listen to this story

Knuth HackerNoon profile picture
Knuth

Knuth

@knuth

Knuth's mastery weaves theory and practice, a tale of computation, in the realm of computer science.

About @knuth
LEARN MORE ABOUT @KNUTH'S
EXPERTISE AND PLACE ON THE INTERNET.
0-item

STORY’S CREDIBILITY

Academic Research Paper

Academic Research Paper

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

Author:

(1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com).

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


Once we have translated the circular doubly-linked list functions into ACL2, we can begin to prove theorems about the data structure implementation. We begin by defining a “well-formedness” predicate for CDLLs.


image


Given this definition of a good CDLL state, we can prove functional correctness theorems for Dancing Links operations, of the sort stated below. Note that this proof requires some detailed well-formedness hypotheses related to the prev and next indices for the nth element:


image


ACL2 performs the correctness proof for this cdll_restore of cdll_remove theorem automatically. In addition to the Dancing Links operator proofs, we have proved approximately 160 theorems related to the CDLL data structure, including theorems about cdll_cns() (cons equivalent), cdll_- rst() (cdr equivalent), cdll_snc() (add to end of data structure), cdll_tsr() (delete from end of data structure), cdll_nth(), etc. All of these proofs will be made publicly available in the ACL2 workshop books repository.


This paper is available on arxiv under CC BY 4.0 DEED license.


L O A D I N G
. . . comments & more!

About Author

Knuth HackerNoon profile picture
Knuth@knuth
Knuth's mastery weaves theory and practice, a tale of computation, in the realm of computer science.

TOPICS

THIS ARTICLE WAS FEATURED IN...

Permanent on Arweave
Read on Terminal Reader
Read this story in a terminal
 Terminal
Read this story w/o Javascript
Read this story w/o Javascript
 Lite
Also published here
Knuth
X REMOVE AD