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 3 The Rust Programming Language The Rust programming language has garnered significant interest and use as a modern, type-safe, memory-safe, and potentially formally analyzable programming language. Google [29] and Amazon [25] are major Rust adopters, and Linus Torvalds has commented positively on the near-term ability of the Rust toolchain to be used in Linux kernel development [1]. And after spending decades dealing with a never-ending parade of security vulnerabilities due to C/C++, which continue to manifest at a high rate [24] despite their use of sophisticated C/C++ analysis tools, Microsoft announced at its BlueHat 2023 developer conference that is was beginning to rewrite core Windows libraries in Rust [6]. Our interest in Rust stems from its potential as a hardware/software co-assurance language. This interest is motivated in part by emerging application areas, such as autonomous and semi-autonomous platforms for land, sea, air, and space, that require sophisticated algorithms and data structures, are subject to stringent accreditation/certification, and encourage hardware/software co-design approaches. (For an unmanned aerial vehicle use case illustrating a formal methods-based systems engineering environment, please consult [7] [23].) In this paper, we explore the use of Rust as a High-Level Synthesis (HLS) language [26]. HLS developers specify the high-level abstract behavior of a digital system in a manner that omits hardware design details such as clocking; the HLS toolchain is then responsible for “filling in the details” to produce a Register Transfer Level (RTL) structure that can be used to realize the design in hardware. HLS development is thus closer to software development than traditional hardware design in Hardware Description Languages (HDLs) such as Verilog or VHDL. Most incumbent HLS languages are a subset of C, e.g. Mentor Graphics’ Algorithmic C [21], or Vivado HLS by Xilinx [31], although other languages have also been used, e.g. OCaml [15]. A Rust-based HLS would bring a single modern, type-safe, and memory-safe expression language for both hardware and software realizations, with very high assurance. For formal methods researchers, Rust presents the opportunity to reason about application-level logic written in the imperative style favored by industry, but without the snarls of the unrestricted pointers of C/C++. Much progress has been made to this end in recent years, to the point that developers can verify the correctness of common algorithm and data structure code that utilizes common idioms such as records, loops, modular integers, and the like, and verified compilers can guarantee that such code is compiled correctly to binary [18]. Particular progress has been made in the area of hardware/software co-design algorithms, where array-backed data structures are common [10, 11]. (NB: This style of programming also addresses one of the shortcomings of Rust, namely its lack of support for cyclic data structures.) As a study of the suitability of Rust as an HLS, we have crafted a Rust subset, inspired by Russinoff’s Restricted Algorithmic C (RAC) [27], which we have imaginatively named Restricted Algorithmic Rust, or RAR [13]. In fact, in our first implementation of a RAR toolchain, we merely “transpile” (perform a source-to-source translation of) 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. By transpiling RAR to RAC, we gain access to existing HLS compilers (with the help of some simple C preprocessor directives, we are able to generate code for either the Algorithmic C or Vivado HLS toolchains). But most importantly for our research, we leverage the RAC-to-ACL2 translator that Russinoff and colleagues at Arm have successfully utilized in industrial-strength floating point hardware verification. We have implemented several representative algorithms and data structures in RAR, including: • a suite of array-backed algebraic data types, previously implemented in RAC (as reported in [10]); • a significant subset of the Monocypher [30] modern cryptography suite, including XChacha20 and Poly1305 (RFC 8439) encryption/decryption, BLAKE2b hashing, and X25519 public key cryptography [12]; and • a DFA-based JSON lexer, coupled with an LL(1) JSON parser. The JSON parser has also been implemented using Greibach Normal Form (previously implemented in RAC, as described in [14]). The RAR examples created to date are similar to their RAC counterparts in terms of expressiveness, and we deem the RAR versions somewhat superior in terms of readability (granted, this is a very subjective evaluation). In this paper, we will describe the development and formal verification of an array-based circular doubly-linked list (CDLL) data structure in RAR, including the Dancing Links optimization. Along the way, we will introduce the RAR subset of Rust, the RAR toolchain, the CDLL example, and detail our ACL2-based verification techniques, as well as the ACL2 books that we brought to bear on this example. It is hoped that this explication will convince the reader of the practicality of RAR as a high-assurance hardware/software co-design language, as well as the feasibility of the performing full functional correctness proofs of RAR code. We will then conclude with related and future work. 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 3 The Rust Programming Language The Rust programming language has garnered significant interest and use as a modern, type-safe, memory-safe, and potentially formally analyzable programming language. Google [29] and Amazon [25] are major Rust adopters, and Linus Torvalds has commented positively on the near-term ability of the Rust toolchain to be used in Linux kernel development [1]. And after spending decades dealing with a never-ending parade of security vulnerabilities due to C/C++, which continue to manifest at a high rate [24] despite their use of sophisticated C/C++ analysis tools, Microsoft announced at its BlueHat 2023 developer conference that is was beginning to rewrite core Windows libraries in Rust [6]. Our interest in Rust stems from its potential as a hardware/software co-assurance language. This interest is motivated in part by emerging application areas, such as autonomous and semi-autonomous platforms for land, sea, air, and space, that require sophisticated algorithms and data structures, are subject to stringent accreditation/certification, and encourage hardware/software co-design approaches. (For an unmanned aerial vehicle use case illustrating a formal methods-based systems engineering environment, please consult [7] [23].) In this paper, we explore the use of Rust as a High-Level Synthesis (HLS) language [26]. HLS developers specify the high-level abstract behavior of a digital system in a manner that omits hardware design details such as clocking; the HLS toolchain is then responsible for “filling in the details” to produce a Register Transfer Level (RTL) structure that can be used to realize the design in hardware. HLS development is thus closer to software development than traditional hardware design in Hardware Description Languages (HDLs) such as Verilog or VHDL. Most incumbent HLS languages are a subset of C, e.g. Mentor Graphics’ Algorithmic C [21], or Vivado HLS by Xilinx [31], although other languages have also been used, e.g. OCaml [15]. A Rust-based HLS would bring a single modern, type-safe, and memory-safe expression language for both hardware and software realizations, with very high assurance. For formal methods researchers, Rust presents the opportunity to reason about application-level logic written in the imperative style favored by industry, but without the snarls of the unrestricted pointers of C/C++. Much progress has been made to this end in recent years, to the point that developers can verify the correctness of common algorithm and data structure code that utilizes common idioms such as records, loops, modular integers, and the like, and verified compilers can guarantee that such code is compiled correctly to binary [18]. Particular progress has been made in the area of hardware/software co-design algorithms, where array-backed data structures are common [10, 11]. (NB: This style of programming also addresses one of the shortcomings of Rust, namely its lack of support for cyclic data structures.) As a study of the suitability of Rust as an HLS, we have crafted a Rust subset, inspired by Russinoff’s Restricted Algorithmic C (RAC) [27], which we have imaginatively named Restricted Algorithmic Rust, or RAR [13]. In fact, in our first implementation of a RAR toolchain, we merely “transpile” (perform a source-to-source translation of) 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. By transpiling RAR to RAC, we gain access to existing HLS compilers (with the help of some simple C preprocessor directives, we are able to generate code for either the Algorithmic C or Vivado HLS toolchains). But most importantly for our research, we leverage the RAC-to-ACL2 translator that Russinoff and colleagues at Arm have successfully utilized in industrial-strength floating point hardware verification. We have implemented several representative algorithms and data structures in RAR, including: • a suite of array-backed algebraic data types, previously implemented in RAC (as reported in [10]); • a significant subset of the Monocypher [30] modern cryptography suite, including XChacha20 and Poly1305 (RFC 8439) encryption/decryption, BLAKE2b hashing, and X25519 public key cryptography [12]; and • a DFA-based JSON lexer, coupled with an LL(1) JSON parser. The JSON parser has also been implemented using Greibach Normal Form (previously implemented in RAC, as described in [14]). The RAR examples created to date are similar to their RAC counterparts in terms of expressiveness, and we deem the RAR versions somewhat superior in terms of readability (granted, this is a very subjective evaluation). In this paper, we will describe the development and formal verification of an array-based circular doubly-linked list (CDLL) data structure in RAR, including the Dancing Links optimization. Along the way, we will introduce the RAR subset of Rust, the RAR toolchain, the CDLL example, and detail our ACL2-based verification techniques, as well as the ACL2 books that we brought to bear on this example. It is hoped that this explication will convince the reader of the practicality of RAR as a high-assurance hardware/software co-design language, as well as the feasibility of the performing full functional correctness proofs of RAR code. We will then conclude with related and future work. 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.

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

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

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 Algorithm That Makes Data Dance—and Solve Complex Problems Fast

Simplifying Circular Data Structures with Rust’s RAR Subset

Machine-Generated Code That Works

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 Algorithm That Makes Data Dance—and Solve Complex Problems Fast

Simplifying Circular Data Structures with Rust’s RAR Subset

Machine-Generated Code That Works

Light-Mode

Classic

Newspaper

Minty

Dark-Mode

Neon Noir

Minty

HN StartUps