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.2 Translation to ACL2 We use Plexi to transpile the RAR source to RAC (not shown), then use the RAC translator to convert the resulting RAC source to ACL2. The translation of cdll_restore() appears in Fig. 6. The first thing to note about Fig. 6 is that, even though we are two translation steps away from the original RAR source, the translated function is nonetheless quite readable, which is a rare thing for machine-generated code. Another notable observation is that struct and array ‘get’ and ‘set’ operations become untyped record operators, AG and AS, respectively — these are slight RAC-specific customizations of the usual ACL2 untyped record operators. Further, IF1 is a RAC-specific macro, and LOG>, LOG=, LOG<, and LOGIOR1 are all RTL functions. Thus, much of the proof effort involved with RAR code is reasoning about untyped records and RTL — although not a lot of RTL-specific knowledge is needed, at least in our experience. One aspect of untyped records that can be tricky is that record elements that take on the default value are not explicitly stored in the association list for the record. For RAC untyped records, that default value is zero. Thus, it is easy for a given record to attain a nil value. When reasoning about arrays of such records, it is often desirable to be able to state that the array size remains constant. Thus, for example, for the CDLL array nodeArr of Section 6.1, we ensure that all CDLLNode elements of that array are non-nil by making sure that the alloc fields of the CDLLNode elements are always non-zero (2 or 3). 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.2 Translation to ACL2 We use Plexi to transpile the RAR source to RAC (not shown), then use the RAC translator to convert the resulting RAC source to ACL2. The translation of cdll_restore() appears in Fig. 6. The first thing to note about Fig. 6 is that, even though we are two translation steps away from the original RAR source, the translated function is nonetheless quite readable, which is a rare thing for machine-generated code. Another notable observation is that struct and array ‘get’ and ‘set’ operations become untyped record operators, AG and AS, respectively — these are slight RAC-specific customizations of the usual ACL2 untyped record operators. Further, IF1 is a RAC-specific macro, and LOG>, LOG=, LOG<, and LOGIOR1 are all RTL functions. Thus, much of the proof effort involved with RAR code is reasoning about untyped records and RTL — although not a lot of RTL-specific knowledge is needed, at least in our experience. One aspect of untyped records that can be tricky is that record elements that take on the default value are not explicitly stored in the association list for the record. For RAC untyped records, that default value is zero. Thus, it is easy for a given record to attain a nil value. When reasoning about arrays of such records, it is often desirable to be able to state that the array size remains constant. Thus, for example, for the CDLL array nodeArr of Section 6.1, we ensure that all CDLLNode elements of that array are non-nil by making sure that the alloc fields of the CDLLNode elements are always non-zero (2 or 3). 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

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 Case for Rust Programming as a Game-Changer for High-Level Synthesis

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

Simplifying Circular Data Structures with Rust’s RAR Subset

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

Simplifying Circular Data Structures with Rust’s RAR Subset

Light-Mode

Classic

Newspaper

Minty

Dark-Mode

Neon Noir

Minty

HN StartUps