Author:
(1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). 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.3 Dancing Links Theorems 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. 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: 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. Author: (1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Author: Author: (1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Table of Links 1 Introduction 1 Introduction 2 Dancing Links 2 Dancing Links 3 The Rust Programming Language 3 The Rust Programming Language 4 RAC: Hardware/Software Co-Assurance at Scale 4 RAC: Hardware/Software Co-Assurance at Scale 5 Rust and RAR 5 Rust and RAR 5.1 Restricted Algorithmic Rust 5.1 Restricted Algorithmic Rust 6 Dancing Links in Rust and 6.1 Definitions 6 Dancing Links in Rust and 6.1 Definitions 6.2 Translation to ACL2 6.2 Translation to ACL2 6.3 Dancing Links Theorems 6.3 Dancing Links Theorems 7 Related Work 7 Related Work 8 Conclusion 8 Conclusion 9 Acknowledgments and References 9 Acknowledgments and References 6.3 Dancing Links Theorems 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. 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: 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. This paper is available on arxiv under CC BY 4.0 DEED license. available on arxiv

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

Future Work in Rust Co-Assurance

Machine-Generated Code That Works

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

Proving Theorems for Rust’s Dancing Links in ACL2

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

Future Work in Rust Co-Assurance

RRR—Rust, RAR, and RAC: The Trifecta for Co-Design Excellence

Scaling Hardware/Software Co-Assurance with Restricted Algorithmic C

The Case for Rust Programming as a Game-Changer for High-Level Synthesis

The Algorithm That Makes Data Dance—and Solve Complex Problems Fast

Future Work in Rust Co-Assurance

RRR—Rust, RAR, and RAC: The Trifecta for Co-Design Excellence

Scaling Hardware/Software Co-Assurance with Restricted Algorithmic C

The Case for Rust Programming as a Game-Changer for High-Level Synthesis

The Algorithm That Makes Data Dance—and Solve Complex Problems Fast

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps