Verification of a Rust Implementation of Knuth’s Dancing Links Using ACL2: Rust and RAR

Author: (1) David S. Hardin, Cedar Rapids, IA USA david.s.hardin@gmail.com. Table of Links Abstract and Introduction Dancing Links The Rust Programming Language RAC: Hardware/Software Co-Assurance at Scale Rust and RAR Dancing Links in Rust Related Work Conclusion, Acknowledgments, and References 5 Rust and RAR The Rust Programming Language [16] is a modern, high-level programming language designed to combine the code generation efficiency of C/C++ with drastically improved type safety and memory management features. A distinguishing feature of Rust is that a non-scalar object may only have one owner. For example, one cannot assign a reference to an object in a local variable, and then pass that reference to a function. This restriction is similar to those imposed on ACL2 single-threaded objects (stobjs) [4], with the additional complexities of enforcing such “single-owner” restrictions in the context of a generalpurpose, imperative programming language. The Rust runtime performs array bounds checking, as well as arithmetic overflow checking (the latter can be disabled by a build environment setting). In most other ways, Rust is a fairly conventional modern programming language, with interfaces (called traits), lambdas (termed closures), and pattern matching, as well as a macro capability. Also in keeping with other modern programming language ecosystems, Rust features a language-specific build and package management sytem, named cargo. 5.1 Restricted Algorithmic Rust As we wish to utilize the RAC toolchain as a backend in our initial work, Restricted Algorithmic Rust is semantically equivalent to RAC. Thus, we adopt the same semantic restrictions as described in Russinoff’s book. Additionally, in order to enable translation to RAC, as well as to ease the transition from C/C++, RAR supports a commonly used macro that provides a C-like for loop in Rust. Note that, despite the restrictions, RAR code is proper Rust; it compiles to binary using the standard Rust compiler. RAR is transpiled to RAC via a source-to-source translator, as depicted in Fig. 3. Our transpiler is based on the plex parser and lexer generator [28] source code. We thus call our transpiler Plexi, a nickname given to a famous (and now highly sought-after) line of Marshall guitar amplifiers of the mid-1960s. Plexi performs lexical and syntactic transformations that convert RAR code to RAC code. Recent improvements in the plexi tool include better handling of array declarations, as well as providing support for Rust const declarations. The generated RAC code can then be compiled using a C/C++ compiler, fed to an HLS-based FPGA compiler, as well as translated to ACL2 via the RAC ACL2 translator, as illustrated in Fig. 3. This paper is available on arxiv under CC 4.0 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 Abstract and Introduction Dancing Links The Rust Programming Language RAC: Hardware/Software Co-Assurance at Scale Rust and RAR Dancing Links in Rust Related Work Conclusion, Acknowledgments, and References Abstract and Introduction Abstract and Introduction Dancing Links Dancing Links The Rust Programming Language The Rust Programming Language RAC: Hardware/Software Co-Assurance at Scale RAC: Hardware/Software Co-Assurance at Scale Rust and RAR Rust and RAR Dancing Links in Rust Dancing Links in Rust Related Work Related Work Conclusion, Acknowledgments, and References Conclusion, Acknowledgments, and References 5 Rust and RAR The Rust Programming Language [16] is a modern, high-level programming language designed to combine the code generation efficiency of C/C++ with drastically improved type safety and memory management features. A distinguishing feature of Rust is that a non-scalar object may only have one owner. For example, one cannot assign a reference to an object in a local variable, and then pass that reference to a function. This restriction is similar to those imposed on ACL2 single-threaded objects (stobjs) [4], with the additional complexities of enforcing such “single-owner” restrictions in the context of a generalpurpose, imperative programming language. The Rust runtime performs array bounds checking, as well as arithmetic overflow checking (the latter can be disabled by a build environment setting). In most other ways, Rust is a fairly conventional modern programming language, with interfaces (called traits), lambdas (termed closures), and pattern matching, as well as a macro capability. Also in keeping with other modern programming language ecosystems, Rust features a language-specific build and package management sytem, named cargo. 5.1 Restricted Algorithmic Rust As we wish to utilize the RAC toolchain as a backend in our initial work, Restricted Algorithmic Rust is semantically equivalent to RAC. Thus, we adopt the same semantic restrictions as described in Russinoff’s book. Additionally, in order to enable translation to RAC, as well as to ease the transition from C/C++, RAR supports a commonly used macro that provides a C-like for loop in Rust. Note that, despite the restrictions, RAR code is proper Rust; it compiles to binary using the standard Rust compiler. RAR is transpiled to RAC via a source-to-source translator, as depicted in Fig. 3. Our transpiler is based on the plex parser and lexer generator [28] source code. We thus call our transpiler Plexi, a nickname given to a famous (and now highly sought-after) line of Marshall guitar amplifiers of the mid-1960s. Plexi performs lexical and syntactic transformations that convert RAR code to RAC code. Recent improvements in the plexi tool include better handling of array declarations, as well as providing support for Rust const declarations. The generated RAC code can then be compiled using a C/C++ compiler, fed to an HLS-based FPGA compiler, as well as translated to ACL2 via the RAC ACL2 translator, as illustrated in Fig. 3. This paper is available on arxiv under CC 4.0 license. This paper is available on arxiv under CC 4.0 license. available on arxiv

Verification of a Rust Implementation of Knuth’s Dancing Links Using ACL2: Rust and RAR

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

Verification of a Rust Implementation of Knuth’s Dancing Links using ACL2: Abstract and Introduction

Verification of a Rust Implementation of Knuth’s Dancing Links using ACL2: Dancing Links

Verification of a Rust Implementation of Knuth’s Dancing Links Using ACL2: Related Work

Rust Implementation of Knuth's Dancing Links: The Rust Programming Language

Rust Implementation of Knuth's Dancing Links: Conclusion, Acknowledgments, and References

Verification of a Rust Implementation of Knuth’s Dancing Links using ACL2: Abstract and Introduction

Verification of a Rust Implementation of Knuth’s Dancing Links using ACL2: Dancing Links

Verification of a Rust Implementation of Knuth’s Dancing Links Using ACL2: Related Work

Rust Implementation of Knuth's Dancing Links: The Rust Programming Language

Rust Implementation of Knuth's Dancing Links: Conclusion, Acknowledgments, and References

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps