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 Dancing Links in Rust In this section, we describe an array-based circular doubly-linked list (CDLL) employing Knuth’s “Dancing Links” optimization, realized using our RAR Rust subset. The CDLL data structure implementation constitutes over 700 lines of Rust code, which becomes 890 lines of code when translated to ACL2. 6.1 Definitions First, we present the basic RAR declaration for the CDLL. Rust data structure declarations are similar to those in C, but struct elements are declared by specifying the element name, followed by the : separator, then the element type. Also note that Rust pragmas may be given using the derive attribute. In the declaration above, the array nodeArr holds the list element nodes. Each element has next and prev indices. Note that indices in Rust are normally declared to be of the usize type. Note also that by using array indices instead of references, we get around Rust ownership model issues with circular data structures. The alloc field of the CDLLNode structure is declared to be a two bit unsigned field, but its only allowed values are two non-zero values: 2 (not currently allocated), and 3 (allocated). The reason for this has to do with the details of ACL2 untyped record reasoning, which will be discussed in Section 6.2. The Dancing Links operators cdll_remove and cdll_restore are presented in Figures 4 and 5, respectively. Rust functions begin with the fn keyword, followed by the function name, a parenthesized list of parameters, the -> (returns) symbol, the return type name, followed by the function body (delimited by a curly brace pair). A function parameter list element consists of the parameter name, the : symbol, then the parameter type. Additional parameter modifiers, for example mut, may be present to indicate that the parameter is changed in the function body. Within the function body, the syntax is similar to other C-like languages, but local variable declarations begin with let, and use the variable name, :, variable type declaration syntax. A local variable declaration may also require the mut modifier if that local variable is updated after its initialization. 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 Dancing Links in Rust In this section, we describe an array-based circular doubly-linked list (CDLL) employing Knuth’s “Dancing Links” optimization, realized using our RAR Rust subset. The CDLL data structure implementation constitutes over 700 lines of Rust code, which becomes 890 lines of code when translated to ACL2. 6.1 Definitions First, we present the basic RAR declaration for the CDLL. Rust data structure declarations are similar to those in C, but struct elements are declared by specifying the element name, followed by the : separator, then the element type. Also note that Rust pragmas may be given using the derive attribute. In the declaration above, the array nodeArr holds the list element nodes. Each element has next and prev indices. Note that indices in Rust are normally declared to be of the usize type. Note also that by using array indices instead of references, we get around Rust ownership model issues with circular data structures. The alloc field of the CDLLNode structure is declared to be a two bit unsigned field, but its only allowed values are two non-zero values: 2 (not currently allocated), and 3 (allocated). The reason for this has to do with the details of ACL2 untyped record reasoning, which will be discussed in Section 6.2. The Dancing Links operators cdll_remove and cdll_restore are presented in Figures 4 and 5, respectively. Rust functions begin with the fn keyword, followed by the function name, a parenthesized list of parameters, the -> (returns) symbol, the return type name, followed by the function body (delimited by a curly brace pair). A function parameter list element consists of the parameter name, the : symbol, then the parameter type. Additional parameter modifiers, for example mut, may be present to indicate that the parameter is changed in the function body. Within the function body, the syntax is similar to other C-like languages, but local variable declarations begin with let, and use the variable name, :, variable type declaration syntax. A local variable declaration may also require the mut modifier if that local variable is updated after its initialization. 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.

Machine-Generated Code That Works

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

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

Simplifying Circular Data Structures with Rust’s RAR Subset

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