Hello, we're Cedar! \n\nCedar is a patient payment and engagement platform that elevates the total patient experience beyond clinical care

Cedar

cedar

Scientific American Supplement, No. 365, December 30, 1882 by Various, is part of the HackerNoon Books Series. You can jump to any chapter in this book . CALIFORNIA CEDARS. here CALIFORNIA CEDARS. The incense cedar ( ) is one of the valued trees of the California coast and mountains. It is eminently noted for great rapidity of growth, wonderful lightness, stiffness, and extraordinary durability. A thousand uses have sprung up and are multiplying around this interesting cedar as its most inestimable qualities become better known. Fortunately it is one of the most extensively distributed trees of the Pacific—found from the coast range north, south to San Diego, Sierra Nevada, southern Oregon, and most of the interior mountain region from 2,000 to 4,000 feet, and it even thrives quite well at 6,600 feet altitude, but seeming to give out at 7,000 feet, though said to extend to 8,500 feet, which is questionable. As usual with the sylva, flora, and fauna, this also is found lowest along the coast, where it finds the requisite temperature and other essentials, with combined moisture. The base and lower trunk somewhat resembles the Western juniper ( ). It is to be noted in general that trees of such broad, outwardly sweeping, or expanded bases seldom blow over, and to the perceptive and artistic eye their significant character is one of firmness and stability. One hundred to two hundred feet high, six to nine feet in diameter (rarely larger) the shaft is often clear of limbs 80 to 100 feet, and although the lower limbs, or even dry branches, may encumber the middle portion, pin-knots do not damage the timber. The massive body tapers more rapidly above than redwood, and is less eccentric than juniper, yet its general port resembles most the best specimens of the latter. The light cinnamon bark is thick and of shreddy-fibered texture, but so concretely compacted as to render the surface evenly ridged by very long, big bars of bark. These sweep obliquely down on the long spiral twist of swift water lines. The top is conic, the foliage is in compressed, flattened sprays, upright, thickened, and somewhat succulent; if not a languid type, at least in no sense rigid. It bears some resemblance to the great Western arborvitæ ( ), but the tiny leaf-scales are opposite and quite awl-pointed. The general hue of the foliage is light yellowish green, warmly tinted, golden and bead tipped, with tiny, oblong male catkins, as the fruit ripens in October and November. The cones are pendulous from the tips of twigs, oblong, and seldom over three-quarters of an inch long, little more than one-third as thick, and for the most part a trifle compressed. The wood is a pale cream-tint in color—a delicate salmon shade. This would hardly warrant the name white cedar, sometimes applied to it, as well as the giant arborvitæ. The extreme lightness of the lumber and its sweetness for packing boxes will commend it for express and commercial purposes, for posts and fencing, and especially railway ties, for sleepers, stringers, and ground timbers of all varieties, and for unnumbered uses, a tithe of which cannot be told in a brief notice. Formerly these trees were cut away and burned up, to clear the track for redwood, tamarack, and ponderous pith-pines, etc.; now all else is superseded by this incense cedar. Thus is seen how hasty and ill-advised notions give place to genuine merit. Libocedius decurrens J. occidentalis Thuja gigantea A fungus ( ) attacks and honeycombs it; and riddled as it may occasionally be, still, if spike or nail finds substance enough to hold, or sufficient solidity to resist crushing, then, for many purposes, even such lumber is practically as good as the soundest timber; because when the tree dies the fungus dies, and thenceforth will absorb no more moisture than the soundest part, and is alike imperishable, contrary to common experience in similar cases. This is a timber nearly as lasting as solid granite. For ship or boat lumber, the clear stuff from sound wood is so exceedingly light, stiff, and durable, and so plenty and available, that few timbers excel it, unless the yellow cedar or cyprus ( ) is excepted, which is a little tougher, stronger, perhaps more elastic, and equally durable, if judged apart from thorough tests and careful data, which, it has been remarked, the apathy or ignorance of some governments appear to deem unworthy their sublime attention. There are said to be in California a thousand times more and better kinds of naval timbers on government lands as important to preserve as the live oaks of the South Atlantic States. It has been asserted as probable that, after due investigation, California would be found to possess a vast amount of the best naval timber in the world, a hundredfold more lasting than the best now in use, if a few woods are excepted, of which there is understood to be no very adequate supply. dædalus Cupressus nutkaensis The great Washington cedar ( ) is another important California tree. The great sequoian timber belt lies along the Sierras, upon the first exposed mountain side—moraines of recent retiring glaciers—that face the Pacific, from Calaveras on the north to near the head of Deer Creek on the south—a distance of 200 miles, or a little above 38 degrees north to a little below 36 degrees; altitude 5,000 to 8,000 feet, and rarely 8,400 feet. The belt is broken by two gaps, each 40 miles wide, caused by manifest topographical and glacial reasons, one gap between Calaveras and Tuolumne, the other between Fresno and King's River; thence the vast forest trends south, across the broad basins of Kaweah and Tule, a distance of 70 miles, on fresh moraine soil, ground from high mountain flanks by glaciers. The inscriptions are scarcely marred by post glacial agents, and the contiguous water-worn marks are often so slight in the rock-bound streams as to be measured by a few inches. Rarely does one of these sound and vigorous cedars fall, and those that do will lie 800 to 1,000 years, scarcely less perishable than the granite on which they grew. The great sequoian ditches, dug at a blow by their fall, and the tree tumuli, always turned up beside the deep root-bowls, remain; but, scientists assert, not a vestige of one outside the present forests has yet presented itself, hence the area has not been diminished during the last 8,000 or 10,000 years, and probably not at all in post glacial times. These colossal sequoias rise 275, 300, and even 400 feet aloft; are 20 to 30, and in some rare cases 40 feet in diameter, looking like vast columnar pillars of the skies. No known trees of the world compare with them and their kin, the redwoods, for the focused proximity of such a marvelous amount of timber within limited areas—as it were, the highest standard of timber-land capacity. The stage coach passes through one; 120 children and a piano crowd inside another; a trunk furnishes a house for cotillon parties to dance "stout on stumps;" a horse and rider travel within the burnt-out hollows of others, and so on. A single tree would furnish a two-rail fence, 20 to 30 miles long. The tree has great value for wood and lumber.— Sequoia gigantea N.W. Lumberman. About HackerNoon Book Series: We bring you the most important technical, scientific, and insightful public domain books. This book is part of the public domain. Various (2006). Scientific American Supplement, No. 365, December 30, 1882. Urbana, Illinois: Project Gutenberg. Retrieved https://www.gutenberg.org/cache/epub/18763/pg18763-images.html This eBook is for the use of anyone anywhere at no cost and with almost no restrictions whatsoever. You may copy it, give it away or re-use it under the terms of the Project Gutenberg License included with this eBook or online at , located at . www.gutenberg.org https://www.gutenberg.org/policy/license.html

CALIFORNIA CEDARS

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

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 “Dancing Links” connotes an optimization to a circular doubly-linked list data structure implementation which provides for fast list element removal and restoration. The Dancing Links optimization is used primarily in fast algorithms to find exact covers, and has been popularized by Knuth in Volume 4B of his seminal series The Art of Computer Programming. We describe an implementation of the Dancing Links optimization in the Rust programming language, as well as its formal verification using the ACL2 theorem prover. Rust has garnered significant endorsement in the past few years as a modern, memory-safe successor to C/C++ at companies such as Amazon, Google, and Microsoft, and is being integrated into both the Linux and Windows operating system kernels. Our interest in Rust stems from its potential as a hardware/software co-assurance language, with application to critical systems. We have crafted a Rust subset, inspired by Russinoff’s Restricted Algorithmic C (RAC), which we have imaginatively named Restricted Algorithmic Rust, or RAR. In previous work, we described our initial implementation of a RAR toolchain, wherein we simply transpile 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. In this paper, we describe the RAR Rust subset, describe our improved prototype RAR toolchain, and detail the design and verification of a circular doublylinked list data structure employing the Dancing Links optimization in RAR, with full proofs of functional correctness accomplished using the ACL2 theorem prover. 1 Introduction The exact cover problem [17], in its simplest form, attempts to find, for an n × m matrix with binary elements, all of the subsets of the rows of the matrix such that all the column sums are exactly one. This basic notion naturally extends to matrix elements that are in some numerical range; indeed, the popular puzzle game Sudoku is an extended exact cover problem for a 9× 9 matrix with element values in the range of 1 to 9, inclusive. The exact cover problem is NP-complete, but computer scientists have devised recursive, nondeterministic backtracking algorithms to find exact covers. One such procedure is Knuth’s Algorithm X, described in [17]. In this algorithm, elements of the matrix are connected via circular doubly-linked lists, and individual elements are removed, or restored, as the algorithm proceeds, undergoing backtracking, etc. As these removals and restorations out of/into the list are quite common, making these operations efficient is a laudable goal. This is where Knuth’s “Dancing Links” comes in, resulting in an optimized algorithm for finding exact covers which Knuth calls DLX (Dancing Links applied to algorithm X). 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 Abstract “Dancing Links” connotes an optimization to a circular doubly-linked list data structure implementation which provides for fast list element removal and restoration. The Dancing Links optimization is used primarily in fast algorithms to find exact covers, and has been popularized by Knuth in Volume 4B of his seminal series The Art of Computer Programming. We describe an implementation of the Dancing Links optimization in the Rust programming language, as well as its formal verification using the ACL2 theorem prover. Rust has garnered significant endorsement in the past few years as a modern, memory-safe successor to C/C++ at companies such as Amazon, Google, and Microsoft, and is being integrated into both the Linux and Windows operating system kernels. Our interest in Rust stems from its potential as a hardware/software co-assurance language, with application to critical systems. We have crafted a Rust subset, inspired by Russinoff’s Restricted Algorithmic C (RAC), which we have imaginatively named Restricted Algorithmic Rust, or RAR. In previous work, we described our initial implementation of a RAR toolchain, wherein we simply transpile 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. In this paper, we describe the RAR Rust subset, describe our improved prototype RAR toolchain, and detail the design and verification of a circular doublylinked list data structure employing the Dancing Links optimization in RAR, with full proofs of functional correctness accomplished using the ACL2 theorem prover. 1 Introduction The exact cover problem [17], in its simplest form, attempts to find, for an n × m matrix with binary elements, all of the subsets of the rows of the matrix such that all the column sums are exactly one. This basic notion naturally extends to matrix elements that are in some numerical range; indeed, the popular puzzle game Sudoku is an extended exact cover problem for a 9× 9 matrix with element values in the range of 1 to 9, inclusive. The exact cover problem is NP-complete, but computer scientists have devised recursive, nondeterministic backtracking algorithms to find exact covers. One such procedure is Knuth’s Algorithm X, described in [17]. In this algorithm, elements of the matrix are connected via circular doubly-linked lists, and individual elements are removed, or restored, as the algorithm proceeds, undergoing backtracking, etc. As these removals and restorations out of/into the list are quite common, making these operations efficient is a laudable goal. This is where Knuth’s “Dancing Links” comes in, resulting in an optimized algorithm for finding exact covers which Knuth calls DLX (Dancing Links applied to algorithm X). 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: Abstract and Introduction

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 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. 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). 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 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 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. 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). 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 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: Dancing Links in Rust

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 4 RAC: Hardware/Software Co-Assurance at Scale In order to begin to realize hardware/software co-assurance at scale, we have conducted several experiments employing a state-of-the-art toolchain, due to Russinoff and O’Leary, and originally designed for use in floating-point hardware verification [27], to determine its suitability for the creation of safetycritical/security-critical applications in various domains. Note that this toolchain has already demonstrated the capability to scale to industrial designs in the floating-point hardware design and verification domain, as it has been used in design verifications for CPU products at both Intel and Arm. Algorithmic C [21] is a High-Level Synthesis (HLS) language, and is supported by hardware/software co-design environments from Mentor Graphics, e.g., Catapult [22]. Algorithmic C defines C++ header files that enable compilation to both hardware and software platforms, including support for the peculiar bit widths employed, for example, in floating-point hardware design. The Russinoff-O’Leary Restricted Algorithmic C (RAC) toolchain, depicted in Fig. 2, translates a subset of Algorithmic C source to the Common Lisp subset supported by the ACL2 theorem prover, as augmented by Russinoff’s Register Transfer Logic (RTL) books. The ACL2 Translator component of Fig. 2 provides a case study in the bridging of Formal Modeling and Real-World Development concerns, as summarized in Table 1. The ACL2 translator converts imperative RAC code to functional ACL2 code. Loops are translated into tail-recursive functions, with automatic generation of measure functions to guarantee admission into the logic of ACL2 (RAC subsetting rules ensure that loop measures can be automatically determined). Structs and arrays are converted into functional ACL2 records. The combination of modular arithmetic and bit-vector operations of typical RAC source code is faithfully translated to functions supported by Russinoff’s RTL books. ACL2 is able to reason about non-linear arithmetic functions, so the usual concern about formal reasoning about non-linear arithmetic functions does not apply. Finally, the RTL books are quite capable of reasoning about a combination of arithmetic and bit-vector operations, which is a very difficult feat for most automated solvers. Recently, we have investigated the synthesis of Field-Programmable Gate Array (FPGA) hardware directly from high-level architecture models, in collaboration with colleagues at Kansas State University. The goal of this work is to enable the generation of high-assurance hardware and/or software from highlevel architectural specifications expressed in the Architecture Analysis and Design Language (AADL) [9], with proofs of correctness in ACL2. 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 4 RAC: Hardware/Software Co-Assurance at Scale In order to begin to realize hardware/software co-assurance at scale, we have conducted several experiments employing a state-of-the-art toolchain, due to Russinoff and O’Leary, and originally designed for use in floating-point hardware verification [27], to determine its suitability for the creation of safetycritical/security-critical applications in various domains. Note that this toolchain has already demonstrated the capability to scale to industrial designs in the floating-point hardware design and verification domain, as it has been used in design verifications for CPU products at both Intel and Arm. Algorithmic C [21] is a High-Level Synthesis (HLS) language, and is supported by hardware/software co-design environments from Mentor Graphics, e.g., Catapult [22]. Algorithmic C defines C++ header files that enable compilation to both hardware and software platforms, including support for the peculiar bit widths employed, for example, in floating-point hardware design. The Russinoff-O’Leary Restricted Algorithmic C (RAC) toolchain, depicted in Fig. 2, translates a subset of Algorithmic C source to the Common Lisp subset supported by the ACL2 theorem prover, as augmented by Russinoff’s Register Transfer Logic (RTL) books. The ACL2 Translator component of Fig. 2 provides a case study in the bridging of Formal Modeling and Real-World Development concerns, as summarized in Table 1. The ACL2 translator converts imperative RAC code to functional ACL2 code. Loops are translated into tail-recursive functions, with automatic generation of measure functions to guarantee admission into the logic of ACL2 (RAC subsetting rules ensure that loop measures can be automatically determined). Structs and arrays are converted into functional ACL2 records. The combination of modular arithmetic and bit-vector operations of typical RAC source code is faithfully translated to functions supported by Russinoff’s RTL books. ACL2 is able to reason about non-linear arithmetic functions, so the usual concern about formal reasoning about non-linear arithmetic functions does not apply. Finally, the RTL books are quite capable of reasoning about a combination of arithmetic and bit-vector operations, which is a very difficult feat for most automated solvers. Recently, we have investigated the synthesis of Field-Programmable Gate Array (FPGA) hardware directly from high-level architecture models, in collaboration with colleagues at Kansas State University. The goal of this work is to enable the generation of high-assurance hardware and/or software from highlevel architectural specifications expressed in the Architecture Analysis and Design Language (AADL) [9], with proofs of correctness in ACL2. 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

Rust Implementation of Knuth's Dancing Links: RAC: Hardware/Software Co-Assurance at Scale

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 8 Conclusion We have developed a prototype toolchain to allow the Rust programming language to be used as a hardware/software co-design and co-assurance language for critical systems, standing on the shoulders of Russinoff’s team at Arm, and all the great work they have done on Restricted Algorithmic C. We have demonstrated the ability to establish the correctness of several practical data structures commonly found in high-assurance systems (e.g., array-backed singly-linked lists, doubly-linked lists, stacks, and dequeues) through automated formal verification, enabled by automated source-to-source translation from Rust to RAC to ACL2, and have detailed the specification and verification of one such data structure, a circular doubly-linked list employing Knuth’s “Dancing Links” optimization. We have also successfully applied our toolchain to cryptography and data format filtering examples typical of the sorts of algorithms that one encounters in critical systems development. In future work, we will continue to develop our toolchain, increasing the number of Rust features that we can support in the RAR subset, as well as continuing to improve the ACL2 verification libraries in order to increase the ability to discharge RAR correctness proofs automatically. We will also continue to work with our colleagues at Kansas State University on the direct synthesis and verification of RAR code from architectural models, as well as working with colleagues at the University of Kansas on verified synthesis of Rust code from high-level attestation protocol specifications written using the Coq theorem prover. 9 Acknowledgments Many thanks to Donald Knuth for his detailed study of exact cover problems in general, and the “Dancing Links” optimization in particular, that can now be found in Volume 4B of his seminal series, The Art of Computer Programming. It was a pleasure discovering this particular corner of Computer Science, beginning when the author accidentally stumbled upon a previously recorded Knuth “Christmas Lecture” on the subject in late 2022. Previous foundational work on hardware/software co-assurance in Rust was funded by DARPA contract HR00111890001. The views, opinions and/or findings expressed are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government. Many thanks to David Russinoff of Arm for developing and improving the RAC toolchain, without which most of the current work would not be possible. Thanks also go to the anonymous reviewers for their insightful comments. References [1] Ron Amadeo (2021): Google is now writing low-level Android code in Rust. Available at https://arstechnica.com/gadgets/2021/04/ google-is-now-writing-low-level-android-code-in-rust/. [2] Amazon Web Services (2022): Announcing the Kani Rust Verifier Project. Available at https://model-checking.github.io/kani-verifier-blog/2022/ 05/04/announcing-the-kani-rust-verifier-project.html?fbclid=IwAR2M_ B1IEBfkVhIXSuuAxt3McC_QpUnTuzDq9jG40HOaJzxw8z1Nw9XU_i4. [3] V. Astrauskas, A. B´ıl ´y, J. Fiala, Z. Grannan, C. Matheja, P. M ¨uller, F. Poli & A. J. Summers (2022): The Prusti Project: Formal Verification for Rust (invited). In: NASA Formal Methods (14th International Symposium), Springer, pp. 88–108, doi:10.1007/978-3-031-06773-0_5. Available at https://link.springer. com/chapter/10.1007/978-3-031-06773-0_5. [4] Robert S. Boyer & J Strother Moore (2002): Single-Threaded Objects in ACL2. In: Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, January 19-20, 2002, Proceedings, LNCS 2257, Springer, pp. 9–27, doi:10.1007/3-540-45587-6_3. [5] Sally Browning & Philip Weaver (2010): Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol. In David S. Hardin, editor: Design and Verification of Microprocessor Systems for High-Assurance Applications, Springer, pp. 89–143, doi:10.1007/978-1-4419-1539-9_4. [6] Thomas Claburn (2023): Microsoft is busy rewriting core Windows code in memory-safe Rust. Available at https://www.theregister.com/2023/04/27/microsoft_windows_rust/. [7] Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer & John Shackleton (2022): Cyber Assured Systems Engineering at Scale. In: IEEE Security & Privacy, pp. 52–64, doi:10.1109/MSEC.2022.3151733. [8] Xavier Denis (2022): Creusot. Available at https://github.com/xldenis/creusot. [9] Peter H. Feiler & David P. Gluch (2012): Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language, 1st edition. Addison-Wesley Professional. [10] David S. Hardin (2020): Put Me on the RAC. In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-20), pp. 142–145, doi:10.4204/eptcs.327.13. [11] David S. Hardin (2020): Verified Hardware/Software Co-Assurance: Enhancing Safety and Security for Critical Systems. In: Proceedings of the 2020 IEEE Systems Conference, doi:10.1109/SysCon47679. 2020.9381831. [12] David S. Hardin (2022): Hardware/Software Co-Assurance for the Rust Programming Language Applied to Zero-Trust Architecture Development. ACM SIGAda Ada Letters 42(2), pp. 55–61, doi:10.1145/3591335. 3591340. [13] David S. Hardin (2022): Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. In: Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-22), pp. 202–216, doi:10.4204/EPTCS.359.16. [14] David S. Hardin & Konrad L. Slind (2021): Formal Synthesis of Filter Components for Use in SecurityEnhancing Architectural Transformations. In: Proceedings of the Seventh Workshop on Language-Theoretic Security, 42nd IEEE Symposium and Workshops on Security and Privacy (LangSec 2021), doi:10.1109/ SPW53761.2021.00024. [15] Jane Street Group, LLC (2023): Hardcaml: An OCaml library for designing and testing hardware designs. Available at https://github.com/janestreet/hardcaml. [16] Steve Klabnik & Carol Nichols (2018): The Rust Programming Language. No Starch Press. [17] Donald E. Knuth (2022): The Art of Computer Programming. 4B: Combinatorial Algorithms, Part 2, Addison-Wesley. [18] Ramana Kumar, Magnus O. Myreen, Michael Norrish & Scott Owens (2014): CakeML: a verified implementation of ML. In Suresh Jagannathan & Peter Sewell, editors: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, ACM, pp. 179–192, doi:10.1145/2535838.2535841. [19] Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno & Chris Hawblitzel (2023): Verus: Verifying Rust Programs Using Linear Ghost Types. Proc. ACM Program. Lang. 7(OOPSLA1), doi:10.1145/3586037. [20] Yusuke Matsushita, Takeshi Tsukada & Naoki Kobayashi (2021): RustHorn: CHC-Based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. 43(4), doi:10.1145/3462205. [21] Mentor Graphics Corporation (2016): Algorithmic C (AC) Datatypes. Available at https://www.mentor. com/hls-lp/downloads/ac-datatypes. [22] Mentor Graphics Corporation (2020): Catapult High-Level Synthesis. Available at https://www.mentor. com/hls-lp/catapult-high-level-synthesis/. [23] Eric Mercer, Konrad Slind, Isaac Amundson, Darren Cofer, Junaid Babar & David Hardin (2023): Synthesizing Verified Components for Cyber Assured Systems Engineering. In: Software and Systems Modeling, 22, pp. 1451–1471, doi:10.1007/s10270-023-01096-3. [24] Matt Miller (2019): A proactive approach to more secure code. Available at https://msrc-blog. microsoft.com/2019/07/16/a-proactive-approach-to-more-secure-code/. [25] Shane Miller & Carl Lerche (2022): Sustainability with Rust. Available at https://aws.amazon.com/ blogs/opensource/sustainability-with-rust/. [26] Razvan Nane, Vlad-Mihai Sima, Christian Pilato, Jongsok Choi, Blair Fort, Andrew Canis, Yu Ting Chen, Hsuan Hsiao, Stephen Brown, Fabrizio Ferrandi, Jason Anderson & Koen Bertels (2016): A Survey and Evaluation of FPGA High-Level Synthesis Tools. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 35(10), pp. 1591–1604, doi:10.1109/TCAD.2015.2513673. [27] David M. Russinoff (2022): Formal Verification of Floating-Point Hardware Design: A Mathematical Approach, second edition. Springer, doi:10.1007/978-3-030-87181-9. [28] Geoffry Song (2020): plex: a parser and lexer generator as a Rust procedural macro. Available at https:// github.com/goffrie/plex. [29] Jeff Vander Stoep & Stephen Hines (2021): Rust in the Android platform. Available at https://security. googleblog.com/2021/04/rust-in-android-platform.html. [30] Loup Vaillant (2022): Monocypher: Boring Crypto that Simply Works. Available at https://monocypher. org. [31] Xilinx, Inc. (2018): Vivado Design Suite User Guide: High-Level Synthesis. Available at https://www.xilinx.com/support/documentation/sw_manuals/xilinx2018_3/ ug902-vivado-high-level-synthesis.pdf. 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 8 Conclusion We have developed a prototype toolchain to allow the Rust programming language to be used as a hardware/software co-design and co-assurance language for critical systems, standing on the shoulders of Russinoff’s team at Arm, and all the great work they have done on Restricted Algorithmic C. We have demonstrated the ability to establish the correctness of several practical data structures commonly found in high-assurance systems (e.g., array-backed singly-linked lists, doubly-linked lists, stacks, and dequeues) through automated formal verification, enabled by automated source-to-source translation from Rust to RAC to ACL2, and have detailed the specification and verification of one such data structure, a circular doubly-linked list employing Knuth’s “Dancing Links” optimization. We have also successfully applied our toolchain to cryptography and data format filtering examples typical of the sorts of algorithms that one encounters in critical systems development. In future work, we will continue to develop our toolchain, increasing the number of Rust features that we can support in the RAR subset, as well as continuing to improve the ACL2 verification libraries in order to increase the ability to discharge RAR correctness proofs automatically. We will also continue to work with our colleagues at Kansas State University on the direct synthesis and verification of RAR code from architectural models, as well as working with colleagues at the University of Kansas on verified synthesis of Rust code from high-level attestation protocol specifications written using the Coq theorem prover. 9 Acknowledgments Many thanks to Donald Knuth for his detailed study of exact cover problems in general, and the “Dancing Links” optimization in particular, that can now be found in Volume 4B of his seminal series, The Art of Computer Programming. It was a pleasure discovering this particular corner of Computer Science, beginning when the author accidentally stumbled upon a previously recorded Knuth “Christmas Lecture” on the subject in late 2022. Previous foundational work on hardware/software co-assurance in Rust was funded by DARPA contract HR00111890001. The views, opinions and/or findings expressed are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government. Many thanks to David Russinoff of Arm for developing and improving the RAC toolchain, without which most of the current work would not be possible. Thanks also go to the anonymous reviewers for their insightful comments. References [1] Ron Amadeo (2021): Google is now writing low-level Android code in Rust. Available at https://arstechnica.com/gadgets/2021/04/ google-is-now-writing-low-level-android-code-in-rust/. [2] Amazon Web Services (2022): Announcing the Kani Rust Verifier Project. Available at https://model-checking.github.io/kani-verifier-blog/2022/ 05/04/announcing-the-kani-rust-verifier-project.html?fbclid=IwAR2M_ B1IEBfkVhIXSuuAxt3McC_QpUnTuzDq9jG40HOaJzxw8z1Nw9XU_i4. [3] V. Astrauskas, A. B´ıl ´y, J. Fiala, Z. Grannan, C. Matheja, P. M ¨uller, F. Poli & A. J. Summers (2022): The Prusti Project: Formal Verification for Rust (invited). In: NASA Formal Methods (14th International Symposium), Springer, pp. 88–108, doi:10.1007/978-3-031-06773-0_5. Available at https://link.springer. com/chapter/10.1007/978-3-031-06773-0_5. [4] Robert S. Boyer & J Strother Moore (2002): Single-Threaded Objects in ACL2. In: Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, January 19-20, 2002, Proceedings, LNCS 2257, Springer, pp. 9–27, doi:10.1007/3-540-45587-6_3. [5] Sally Browning & Philip Weaver (2010): Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol. In David S. Hardin, editor: Design and Verification of Microprocessor Systems for High-Assurance Applications, Springer, pp. 89–143, doi:10.1007/978-1-4419-1539-9_4. [6] Thomas Claburn (2023): Microsoft is busy rewriting core Windows code in memory-safe Rust. Available at https://www.theregister.com/2023/04/27/microsoft_windows_rust/. [7] Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer & John Shackleton (2022): Cyber Assured Systems Engineering at Scale. In: IEEE Security & Privacy, pp. 52–64, doi:10.1109/MSEC.2022.3151733. [8] Xavier Denis (2022): Creusot. Available at https://github.com/xldenis/creusot. [9] Peter H. Feiler & David P. Gluch (2012): Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language, 1st edition. Addison-Wesley Professional. [10] David S. Hardin (2020): Put Me on the RAC. In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-20), pp. 142–145, doi:10.4204/eptcs.327.13. [11] David S. Hardin (2020): Verified Hardware/Software Co-Assurance: Enhancing Safety and Security for Critical Systems. In: Proceedings of the 2020 IEEE Systems Conference, doi:10.1109/SysCon47679. 2020.9381831. [12] David S. Hardin (2022): Hardware/Software Co-Assurance for the Rust Programming Language Applied to Zero-Trust Architecture Development. ACM SIGAda Ada Letters 42(2), pp. 55–61, doi:10.1145/3591335. 3591340. [13] David S. Hardin (2022): Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. In: Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-22), pp. 202–216, doi:10.4204/EPTCS.359.16. [14] David S. Hardin & Konrad L. Slind (2021): Formal Synthesis of Filter Components for Use in SecurityEnhancing Architectural Transformations. In: Proceedings of the Seventh Workshop on Language-Theoretic Security, 42nd IEEE Symposium and Workshops on Security and Privacy (LangSec 2021), doi:10.1109/ SPW53761.2021.00024. [15] Jane Street Group, LLC (2023): Hardcaml: An OCaml library for designing and testing hardware designs. Available at https://github.com/janestreet/hardcaml. [16] Steve Klabnik & Carol Nichols (2018): The Rust Programming Language. No Starch Press. [17] Donald E. Knuth (2022): The Art of Computer Programming. 4B: Combinatorial Algorithms, Part 2, Addison-Wesley. [18] Ramana Kumar, Magnus O. Myreen, Michael Norrish & Scott Owens (2014): CakeML: a verified implementation of ML. In Suresh Jagannathan & Peter Sewell, editors: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, ACM, pp. 179–192, doi:10.1145/2535838.2535841. [19] Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno & Chris Hawblitzel (2023): Verus: Verifying Rust Programs Using Linear Ghost Types. Proc. ACM Program. Lang. 7(OOPSLA1), doi:10.1145/3586037. [20] Yusuke Matsushita, Takeshi Tsukada & Naoki Kobayashi (2021): RustHorn: CHC-Based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. 43(4), doi:10.1145/3462205. [21] Mentor Graphics Corporation (2016): Algorithmic C (AC) Datatypes. Available at https://www.mentor. com/hls-lp/downloads/ac-datatypes. [22] Mentor Graphics Corporation (2020): Catapult High-Level Synthesis. Available at https://www.mentor. com/hls-lp/catapult-high-level-synthesis/. [23] Eric Mercer, Konrad Slind, Isaac Amundson, Darren Cofer, Junaid Babar & David Hardin (2023): Synthesizing Verified Components for Cyber Assured Systems Engineering. In: Software and Systems Modeling, 22, pp. 1451–1471, doi:10.1007/s10270-023-01096-3. [24] Matt Miller (2019): A proactive approach to more secure code. Available at https://msrc-blog. microsoft.com/2019/07/16/a-proactive-approach-to-more-secure-code/. [25] Shane Miller & Carl Lerche (2022): Sustainability with Rust. Available at https://aws.amazon.com/ blogs/opensource/sustainability-with-rust/. [26] Razvan Nane, Vlad-Mihai Sima, Christian Pilato, Jongsok Choi, Blair Fort, Andrew Canis, Yu Ting Chen, Hsuan Hsiao, Stephen Brown, Fabrizio Ferrandi, Jason Anderson & Koen Bertels (2016): A Survey and Evaluation of FPGA High-Level Synthesis Tools. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 35(10), pp. 1591–1604, doi:10.1109/TCAD.2015.2513673. [27] David M. Russinoff (2022): Formal Verification of Floating-Point Hardware Design: A Mathematical Approach, second edition. Springer, doi:10.1007/978-3-030-87181-9. [28] Geoffry Song (2020): plex: a parser and lexer generator as a Rust procedural macro. Available at https:// github.com/goffrie/plex. [29] Jeff Vander Stoep & Stephen Hines (2021): Rust in the Android platform. Available at https://security. googleblog.com/2021/04/rust-in-android-platform.html. [30] Loup Vaillant (2022): Monocypher: Boring Crypto that Simply Works. Available at https://monocypher. org. [31] Xilinx, Inc. (2018): Vivado Design Suite User Guide: High-Level Synthesis. Available at https://www.xilinx.com/support/documentation/sw_manuals/xilinx2018_3/ ug902-vivado-high-level-synthesis.pdf. 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

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

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 3 The Rust Programming Language The Rust programming language has garnered significant interest and use as a modern, type-safe, memorysafe, 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 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 3 The Rust Programming Language The Rust programming language has garnered significant interest and use as a modern, type-safe, memorysafe, 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 4.0 license. This paper is available on arxiv under CC 4.0 license. available on arxiv

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

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 7 Related Work A number of domain-specific languages targeting both hardware and software realization, and providing support for formal verification, have been created. Cryptol [5], for example, has been employed as a “golden spec” for the evaluation of cryptographic implementations, in which automated tools perform equivalence checking between the Cryptol spec for a given algorithm, and the VHDL implementation. Formal verification systems for Rust include Creusot [8], based on WhyML; Prusti [3], based on the Viper verification toolchain; and RustHorn [20], based on constrained Horn clauses. AWS is developing a model-checker for Rust, Kani [2]. Additionally, Carnegie-Mellon University is developing Verus, an SMT-based tool for formally verifying Rust programs [19]. With Verus, programmers express proofs and specifications using Rust syntax, allowing proofs to take advantage of Rust’s linear types and borrow checking. It will be interesting to attempt the sorts of correctness proofs achievable on our system using these verification tools 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 7 Related Work A number of domain-specific languages targeting both hardware and software realization, and providing support for formal verification, have been created. Cryptol [5], for example, has been employed as a “golden spec” for the evaluation of cryptographic implementations, in which automated tools perform equivalence checking between the Cryptol spec for a given algorithm, and the VHDL implementation. Formal verification systems for Rust include Creusot [8], based on WhyML; Prusti [3], based on the Viper verification toolchain; and RustHorn [20], based on constrained Horn clauses. AWS is developing a model-checker for Rust, Kani [2]. Additionally, Carnegie-Mellon University is developing Verus, an SMT-based tool for formally verifying Rust programs [19]. With Verus, programmers express proofs and specifications using Rust syntax, allowing proofs to take advantage of Rust’s linear types and borrow checking. It will be interesting to attempt the sorts of correctness proofs achievable on our system using these verification tools 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: Related Work

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 2 Dancing Links The concept behind Dancing Links is quite simple: when a given element Y of a list is removed in an exact cover algorithm, it is very likely that this same element will later be restored. Thus, rather than “zero out” the ‘previous’ and ‘next’ links associated with element Y, as good programming hygiene would normally dictate, in Dancing Links, the programmer leaves the link values in place for the removed element. The Dancing Links remove operator thus deletes element Y from the list, setting the ’next’ element of the preceding element X to the following element Z, and setting the ’previous’ element of Z to a link to X, but not touching the ’next’ and ’previous’ links of the removed element Y. Later on, if Y needs to be restored, it is simply hooked back in to the list using a simple restore operator. In Knuth’s words, if one monitors the list links as the DLX algorithm proceeds, the links appear to ‘dance’, hence the name. Knuth’s Dancing Links functionality is summarized in Fig. 1. 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 2 Dancing Links The concept behind Dancing Links is quite simple: when a given element Y of a list is removed in an exact cover algorithm, it is very likely that this same element will later be restored. Thus, rather than “zero out” the ‘previous’ and ‘next’ links associated with element Y, as good programming hygiene would normally dictate, in Dancing Links, the programmer leaves the link values in place for the removed element. The Dancing Links remove operator thus deletes element Y from the list, setting the ’next’ element of the preceding element X to the following element Z, and setting the ’previous’ element of Z to a link to X, but not touching the ’next’ and ’previous’ links of the removed element Y. Later on, if Y needs to be restored, it is simply hooked back in to the list using a simple restore operator. In Knuth’s words, if one monitors the list links as the DLX algorithm proceeds, the links appear to ‘dance’, hence the name. Knuth’s Dancing Links functionality is summarized in Fig. 1. 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: Dancing Links

Cardiovascular diseases are a significant problem worldwide, with millions dying annually due to these ailments. While technology has improved detection, researchers are taking the next step by employing artificial intelligence (AI) to help patients with coronary heart disease, cerebrovascular disease and other conditions. Can AI detect cardiovascular disease? Here’s how AI will affect the future of cardiovascular healthcare. Can AI Detect Cardiovascular Disease? The medical field has rapidly adopted AI to improve healthcare outcomes, with hospitals finding ways to integrate it into daily operations. Here are four recent innovations helping researchers equip this advanced technology and identify heart disease. Analyzing Genes In early 2023, researchers from Rutgers University discussing genetic analysis and how AI and machine learning (ML) can identify cardiovascular disease. The Rutgers Institute for Health used AI to examine healthy people and those with heart disease and was able to link genes to cardiovascular issues. published a study Researchers found correlations with age and gender and concluded the risk of cardiovascular disease increases with age. The Rutgers study trained its model to detect patients at high risk for heart issues. It was able to predict the association with heart failure, atrial fibrillation, and other risks based on demographics. Studying Cells Putting cells under the microscope is another effective way to identify cardiovascular disease using AI. Researchers at the University of East London have wielded AI to and determine who is more at risk. The scientists isolated miniature stem cell hearts and placed them in a petri dish. As they age, the trained model can predict which sets are more at risk and will become faulty. study cells with heart disease While tiny, the stem cells function like a living human heart with a consistent heartbeat. They have heart disease, allowing the East London researchers to train its AI as a diagnostic tool. With this information, the university’s researchers are using AI to understand its connection with aging and improve treatment for those with the disease. Prashant Ruchaya, a senior lecturer at the University of East London, has spearheaded the research and says the technology is crucial for the future of heart disease mitigation. “Cardiovascular disease remains the leading cause of mortality worldwide, and aging is a significant risk factor for its development,” Ruchaya said. “Our research aims to comprehensively explore how aging influences the mechanisms underlying heart diseases, ultimately leading to innovative approaches in mitigating the impact of cardiovascular conditions on older populations. “We are working on cutting-edge research here in developing new disease models and developing AI to predict disease earlier and to develop new treatments to treat heart disease.” Examining MRIs Another AI innovation in the United Kingdom comes from St. Bartholomew’s Hospital in London, where experts have advanced technology to find heart disease more rapidly. The researchers say they can using AI during its pilot, leading to more hospitals using the technology. The National Health Service (NHS) says it will spread the AI-assisted detector to various facilities across its system. detect heart disease in 20 seconds In this instance, the AI examines the MRI in real time, shortening the time necessary for analysis. The NHS says cardiologists need at least 13 minutes to check the MRI scans, so reducing the wait to 20 seconds would drastically reduce this gap and help healthcare providers. Other benefits of this AI system include waiting about 33% less time for results and reducing misclassifications, thus improving treatments. Inspecting Heart Dimensions Healthcare experts also use AI to detect cardiovascular diseases based on the heart’s dimensions. Researchers at Cedars-Sinai Medical Center for detecting diseases — hypertrophic cardiomyopathy and cardiac amyloidosis — you might overlook when examining the heart. Can AI detect a cardiovascular disease that’s difficult to find? have developed an AI tool The researchers trained the AI based on 34,000 ultrasound videos to distinguish various sections of the heart. Identifying the thickness of a heart’s walls and the size of its chambers helps the AI know when abnormalities occur. With this information, healthcare providers will better understand which patients are more at risk for cardiovascular diseases — especially underdiagnosed conditions like hypertrophic cardiomyopathy and cardiac amyloidosis. Implications of Using AI Detection for Heart Disease Cardiologists have opportunities for improved diagnoses and treatments as AI usage increases in healthcare. Here are some of the implications of using AI for detecting cardiovascular diseases. Early Treatment As Ruchaya said, heart disease is the leading cause of death, with the World Health Organization estimating worldwide. Heart attacks and strokes are responsible for more than 80% of deaths, and about one-third occur in people under 70 years old. Early detection of heart disease is crucial, and healthcare providers can achieve diagnoses quicker with AI. nearly 18 million annual deaths AI tools use algorithms with vast amounts of data stored inside their systems. When directed, the AI can reference this historical information to examine a patient’s heart and determine their disease risk. While cardiologists have extensive knowledge, AI and ML can be helpful companions for healthcare professionals in detecting cardiovascular diseases at early stages and increasing accuracy. Increasing Efficiency One goal for using AI is to achieve quicker diagnoses, and researchers also want to improve the accuracy to enhance treatment. Healthcare experts have begun wielding AI to increase precision when examining patients’ hearts and have seen positive results. For example, Mayo Clinic has an AI-assisted screening tool to detect heart problems without apparent symptoms. This system when finding people at risk with these conditions, improving upon other technologies at the clinic. The medical center says it has also integrated AI with Apple Watch to detect when the user has a weak heart pump. has a 93% accuracy rate Personalizing the Treatment Delivering personalized treatment for patients with cardiovascular issues is essential for care, and AI can build upon this to help cardiologists. AI-assisted technology boosts healthcare providers’ assessment of their patients by analyzing vast amounts of data and painting a comprehensive picture of their needs. With more targeted information, they can understand the nuances of their patients’ conditions and more accurately predict future outcomes. Saving Money Using AI for heart disease detection also means saving money in healthcare costs. Achieving early diagnoses means delivering effective treatments and other mitigation tactics to make the disease more manageable throughout your life. Thus, you’ll save money with fewer complications and hospital visits. This advanced technology also presents opportunities for hospitals to save money by allocating more resources to individuals at high risk for other diseases. Experts anticipate AI to be a significant cost-saving mechanism for healthcare, with an Artificial Intelligence in Healthcare study for America’s medical costs. expecting $150 billion in annual savings Research has already demonstrated AI’s potential to save money in healthcare by reducing the time necessary for cardiologists and their patients. For instance, the AI tool examining MRI scans reduces wait times by about 33% compared to previous technologies and drastically cuts the wait for doctors to check them. The Challenges of AI in Heart Disease Detection While AI has revolutionized healthcare in recent years, it presents challenges for the field that providers must deal with for adequate care. Here are some concerns you may see experts raise with AI and heart disease detection: One criticism of AI is its biases, considering where it sources data. The information may derive from outdated sources built on criticized research, making you question its legitimacy. AI developers must ensure the tools use the best information possible. Biases: While accuracy may increase with AI, there is room for improvement. These tools may accidentally provide false positives or negatives, so healthcare providers must be vigilant and scrutinize the AI’s findings. Accuracy: AI relies on large sets of sensitive medical information, making data privacy a concern for healthcare facilities. Cybercriminals often target hospitals for ransomware attacks due to security vulnerabilities and the amount of information stored in their systems. Privacy: AI Can Detect Cardiovascular Disease Accurately The future of healthcare will depend on AI as researchers develop new tools to assist providers. Some of these technologies have already demonstrated their abilities when studying heart conditions. The past few years have given you a glimpse of AI’s extraordinary potential in healthcare, and the future is bright. While more research is necessary, you’ll see cardiologists and other healthcare providers use AI to deliver more personalized care for you. Lead image by the National Cancer Institute on Unsplash

AI May Help Detect Signs of Heart Disease at an Earlier Stage

How to Use Terraform to Configure AWS Verified Access With an OIDC Google Provider

Scientific American, Volume XXIV., No. 12, March 18, 1871 by Various, is part of the HackerNoon Books Series. You can jump to any chapter in this book . To Manufacturers of Knitted Goods. here To Manufacturers of Knitted Goods. is now in England, completing arrangements so as to be able to supply his American friends with his improved Knitting Machines with greater dispatch, and with all the latest improvements. He would beg to call especial attention to JOHN KENT The Improved Rib Top Frame, now so well known, and acknowledged to be the best rib top frame ever built, for speed and quality of goods produced. Price, delivered free in New York, $520, currency. The Improved Circular Web Frame, for drawers and shirts, built of any size and gage. Price for a 4-head set, 17 inch to 20 inch diameter, $810, currency, delivered free in New York. The Circular Stocking Frame, from 2 in. to 5½ in. diameter. These circular frames, with my last improvements, are as near perfection as possible. The Patent Full-fashioned Shirt, Drawers and Stocking Frames produce the most perfect goods ever made by steam-power machinery, and cost fifty per cent less to keep in repair than any other Knitting Machine. Built 10 to 24 gage, and from 30 to 140 inch wide, to order. The Improved Circular Looping Frame, for putting on shirt cuffs, drawers bands, clearing the top of circular shirts, &c., built to order, of any size, from 2 in. to 22 in. diameter, and of any gage. Steel Needles and Sinkers to pattern. Persons wishing to order while Mr. Kent is in England, will please address JOHN KENT, Nottingham, up to April 12th, or, if they prefer, may send through depot. Address JOHN KENT, 348 Pearl st., New York. PUMPS. —For Description, Price Lists etc., of the Best Centrifugal Pump ever invented, with Overwhelming Testimony in its favor, send for new illustrated pamphlet (40 pp.) to Messrs. HEALD, SISCO & CO., Baldwinsville, N. Y. BRICK PRESSES. **FOR RED AND FIRE BRICK.
\ Factory 309 S. Fifth street, Philadelphia, Pa. S. P. MILLER. ST. JOSEPH, Mo., Nov. 10, 1870. T. R. BAILEY & VAIL, Lockport, N. Y.: Gentlemen:—The Lathe you shipped me has arrived, and I have it in full operation. It works perfectly, and I think it the best lathe made in the world for Bedstead and Chair work. I would recommend it to any one desirous of obtaining such a lathe. Yours truly, H. R. BRISTOL. WOOLEN MILL FOR SALE. With House and 3 acres of land, Seymour, Ct., (Naugatuck Valley,) 2 miles from R. R. depot. Never-failing stream. 3 ft. fall, dam and wheel in good condition. Inquire of JAS. ORMSBEE, on the premises. Portable & Stationary Steam Engines AND HOISTING ENGINES. A good article at low prices. Every machine warranted. Send for descriptive Price List. H. B. BIGELOW & CO., New Haven, Conn. PATENT BANDSAW MACHINES Of the most approved kinds, of various sizes , to saw bevel as well as square, without inclining the table, by , 452 to 456 Tenth ave., New York. Price $250, $275, $350, and $400. At present (Oct. 16), there are in operation, in this city alone, 88 of our machines. Send for circular. Manufacture, also, an improved saw-filing apparatus; price, $30. Have also on hand a large stock of best French Bandsaw Blades. FIRST & PRYIBIL L. & J. W. FEUCHTWANGER, 55 Cedar st., New York, Chemists, Manufacturers, and Importers of Specialities, Silicates, Soda and Potash, Chloride of Calcium, Peroxide of Manganese, Hydrofluoric Acid, Metallic Oxides, Steel and Glass Makers' and Potters' Articles, Publishers of Treatises on "Soluble Glass," "Gems," and "Fermented Liquors." PIMLICO BRACES, SOMETHING NEW. THIS invention is based on a strictly scientific principle, and is a valuable improvement on old style suspenders. It is simple in construction, and combines the qualities of Brace and Suspender. They are unequaled for elegance, durability and comfort. Manufactured at the Monumental Silk Works, Baltimore. JOHN M. DAVIES & CO., Sole Agents, 384 & 386 B'd'y, N. Y. Dr. J. ARMSTRONG'S (Patent) Improved Heater, Filter, Lime Extractor, and Condenser Combined, For Steam Boilers. MANUFACTURED BY Toledo, Ohio. Armstrong & Starr, Send for Circulars. Formerly Armstrong & Welsh. —An Engine, 12x36 in. cylinder, and two Boilers, 4x15 feet, in good order, will be sold cheap. FOR SALE. J. J. TAYLOR & CO., 68 Courtlandt st., New York. Trapping and Fishing. All about it. Sent free. Address "Hunter," Hinsdale, N. H. HUNTING, First Premium awarded by Am. Inst., 1870 T. H. McALLISTER, Optician, 49 Nassau st., N. Y. Rare and Beautiful Flowers —AND— CHOICE VEGETABLES Can always be obtained by Sowing The Seventeenth Annual Edition of their celebrated "SEED CATALOGUE AND GUIDE TO THE FLOWER AND KITCHEN GARDEN," is now ready for distribution. It contains Four Beautifully Colored Lithographs, and about 300 choice Engravings of favorite Flowers and Vegetables, 136 pages of closely-printed matter, and a list of Twenty-five Hundred species and varieties of Flower and Vegetable Seeds, with explicit directions for their culture, and much other useful information upon the subject of Gardening. A copy will be mailed to all applicants inclosing 25 cts. Regular customers supplied gratis. Address B. K. BLISS & SONS, Nos. 23 Park Place, and 20 Murray st., P. O. Box No. 5712. New York. Science for the Million. THE Boston Journal of Chemistry, Devoted to the Science of Home Life, the Arts, Agriculture, and Medicine. JAMES R. NICHOLS, M.D., WILLIAM A. ROLFE, A.M., } Editors. ONE DOLLAR PER YEAR. A paper which commends itself at once to Physicians, Druggists, Chemists, Teachers, Farmers, Mechanics—in short, to Professional and Practical Men of every class. The Domestic Recipes and Formulæ for Art Processes are of themselves worth many times the cost of subscription. Specimen Copies Sent Free. Address **BOSTON JOURNAL OF CHEMISTRY,
\ 150 Congress st., Boston. FOOT LATHES, And all kinds of small tools. Illustrated catalogue free. GOODNOW & WIGHTMAN, 23 Cornhill, Boston, Mass. AGENTS WANTED.—To sell Stephens' which embraces a Rule, Level, Square, Plumb, Bevel, Slope Level, T Square, etc., in one compact tool. These instruments retail at $3.50 each, and energetic salesmen can make money by selling them among mechanics. We warrant them in every particular, as the construction and graduation is faultless. Send for descriptive circular, cuts, and terms. Patent Combination Rule, STEPHENS & CO., Riverton, Conn. FELT. THE BEST, CHEAPEST and MOST DURABLE non-conductor known, for sale by the Original Manufacturer, at the BOILER FELTING WORKS, 46 Courtland st., New York. Universal Wood Worker. For Agricultural, Railroad, Car, Carriage, and Wagon Works, Planing Mill, Sash, Door and Blind, Bedstead, Cabinet and Furniture Factories. McBETH, BENTEL & MARGEDANT, Hamilton, O. , Inventor's Exchange 245 Broadway, N. Y., "Am. Agriculturist" Building. TANGIBLE INVENTIONS NEGOTIATED. No goods received unless ordered. B. F. KEMP, Proprietor. MACHINISTS' TOOLS, at greatly reduced prices. Also, some Woodworth Planers and Second-hand Tools. 97 to 113 R. R. ave., Newark, N. J. E. & R. J. GOULD, successors to Gould Machine Co. N. B. PATENTED Articles introduced. Also, State and County Rights sold for Inventors. STONE, PUGH & CO., 55 N. 6th st., Philadelphia. G OLDEN HILL Seminary for young ladies, Bridgeport, Conn. Miss Emily Nelson, Principal. 1826 USE THE VEGETABLE PULMONARY BALSAM. 1870 The old standard remedy for Coughs, Colds, Consumption. "Nothing Better." Cutler Bros. & Co., Boston. T HE CALVERT IRON ROLLING MILLS are offered at private sale. These mills are situated in the city of Baltimore, and cover 1½ acres of ground. The Machinery is of the most approved description, for making all sizes of round and square bar iron, from ¼ in. to 3 in. diameter, and flat bars of all widths, up to 7 inches. The buildings are ample and commodious. In addition to the Rolling Mills are two brick buildings (50x125 feet and 40x90 feet), now containing an 80 H.P. Engine, and Spike Machinery, but which could be used for the manufacture of Nails, Horseshoes, or any other branch of heavy hardware. This property offers an unusual opportunity to capitalists, and will be sold at a reasonable price. For further description address MARSHALL  P. SMITH, P. O. Box 1158, Baltimore, Md. BURDON IRON WORKS.—Manufacturers of Pumping Engines for Water Works, High & Low Pressure Engines, Portable Engines and Boilers, of all kinds, Sugar Mills, Screw, Lever, Drop, & Hydraulic Presses, Machinery in general. HUBBARD & WHITTAKER, 102 Front st., Brooklyn. ENGINES AND MACHINERY FOR SALE, at a great sacrifice. Two new Steam Engines, 12 and 20 horse power; 1 Faribain's Riveting Machine; 1 large Power Shears; 1 ditto Table Punch; 2 ditto Flange Punches; 1 set Power Bending Rolls; together with a large lot of Turning Lathes, Drilling Machines, Machinists' and Smiths' Hand Tools, Pulleys, Hangers, and 6 Fairbanks' Platform Scales. Send for catalogue, or apply at the South Brooklyn Steam Engine Works, cor. Imlay and Summit sts., Brooklyn. SHINGLE AND HEADING MACHINE— Law's Patent with Trevor & Co.'s Improvements. The Simplest and Best in use. Also, Shingle, Heading and Stave Jointers, Equalizers, Heading Turners, Planers etc. AddressTREVOR & CO., Lockport, N. Y. AGENTS WANTED—($225 A MONTH) by the AMERICAN KNITTING MACHINE CO. Boston, Mass., or St. Louis, Mo. THE UNITED STATES Brick Machine IS THE BEST IN THE WORLD, BECAUSE IT MAKES THE , , and GREATEST NUMBER THE BEST THE CHEAPEST BRICKS. It is the Perfection of Simplicity. It is Durable, and not likely to get out of Repair. See Scientific American, Sept. 17, 1870. For Descriptive Circular apply to F. C. WELLS, President, Room 13, 98 Madison st.,\CHICAGO. MACHINES can be seen in operation at the Company's Works, Chicago; at rear 59 Ann st., New York city; and at Novelty Iron Works, corner of Delord and Peter sts., New Orleans. PREPARED Asphalte Roofing Felt. This new prepared production is ready coated, and can be applied on the roof without further trouble. It is easy of application, and does not require any repairs for a long time. It is more durable than some slates, and has been found a suitable substitute for iron or tin roofs. It has a sanded or stony surface, which renders it Exposed to the most intense fire, and sparks falling upon it, it will not propagate the fire. Under the influence of the sun it will not run, which makes it specially adapted to hot climates. Its easy application and pleasing appearance have made it a favorite roofing material throughout all the Indies and other colonies. Being not cumbrous for transport, it is of invaluable service to settlers and farmers in far remote districts. When used for temporary purposes it may be taken off and applied again to another construction. It replaces common Asphalting on Terraces, Lobbies, Counting-houses, Office Floors, etc.; is a great preservative against dampness and vermin, and equalizes the temperature. It is 32 inches wide, and made in rolls of 25 yards each. Send for circular to UNINFLAMMABLE and FIRE-PROOF. E. H. MARTIN, 70 Maiden Lane and 9 Liberty St., N. Y. J. J. H. GREGORY'S Seed Catalogue. My Annual Illustrated Catalogue, containing a list of many new and rare Vegetables, some of which are not found in any other catalogue, and all the standard vegetables of the farm and garden (over one hundred of which I grow on my three seed farms), with a carefully selected list of flower seed, will be sent free to all. All my seed is sold under three warrants: 1st. That all money sent shall reach me. 2d. That all seed ordered shall reach the purchaser. 3d. That my seeds shall be fresh and true to name. JAMES J. H. GREGORY, Marblehead, Mass. THE NEW WILSON Under-Feed Shuttle\SEWING MACHINES! $25 cheaper than any other! For Simplicity, Durability and Beauty they stand For Stitching, Hemming, Tucking, Felling, Quilting, Cording, Binding, Braiding, Gathering, Gathering & sewing on gathers, For particulars address unrivalled! they are unexcelled! Wilson Sewing Machine Co., Cleveland, O., or St. Louis, Mo. , **NEW and 2d-HAND.—
\ Send for Circular. Chas. PLACE & CO., 60 Vesey st., New York. MACHINERY MACHINISTS. Illustrated Catalogue and Price List of all kinds of small Tools and Materials sent free to any address. GOODNOW & WIGHTMAN, 23 Cornhill, Boston, Mass. P. BLAISDELL & CO. MANUFACTURERS of the "BLAISDELL" PATENT DRILL PRESSES, with quick return motion, Agricultural Drills, Improved Engine Lathes, from 12 in. to 28 in. swing, Planers, Gear Cutters, Boring Mills, Hand Lathes, and other first-class Machinists' Tools. Jackson st., Worcester, Mass. Patent BEDSTEAD FASTENING. The and ever invented. Best, Cheapest, Strongest FASTENING Rights for States and Territories for sale. Address JOHN DOMINGOS and                     BENJAMIN ESSIG, Sacramento, Cal. BENT, GOODNOW & CO., Boston, Mass., Publishers of , sell Patent Rights and goods of all kinds. Orders solicited. "PATENT STAR" AGENTS WANTED. Send stamp for copy. TO THE WORKING CLASS.—We are now prepared to furnish all classes with constant employment at home, the whole of the time or for the spare moments. Business new, light and profitable. Persons of either sex easily earn from 50c. to $5 per evening, and a proportional sum by devoting their whole time to the business. Boys and girls earn nearly as much as men. That all who see this notice may send their address, and test the business, we make this unparalleled offer: To such as are not well satisfied, we will send $1 to pay for the trouble of writing. Full particulars, a valuable sample which will do to commence work on, and a copy of —one of the largest and best family newspapers published—all sent free by mail. Reader, if you want permanent, profitable work, address The People's Literary Companion D. C. ALLEN & CO., Augusta, Maine. IMPORTANT TO  MACHINISTS.—The Best Metal for all Machine Uses is the MARTIN STEEL, made by The New Jersey Steel and Iron Co., Trenton, N. J. This steel is made by an entirely different process from any other and is tougher than wrought iron. It can be turned without annealing, being entirely free from hard spots. Every one who uses it pronounces it just what they have long wanted, for a multitude of uses, such as Crank Pins, Lathe Spindles and Screws, Cotton Machinery Rollers, Saw and Fan Spindles, etc., etc. Also, particularly adapted for Firebox Plates. Prices low. Send for further information, or a sample, stating use to which it is to be applied. OTIS' SAFETY HOISTING\Machinery. **OTIS, BROS. & CO.
\ No. 309 BROADWAY, NEW YORK. Union Emery Wheels. Solid and with Stone Center. UNION STONE CO., Boston, Mass. Branch Office, 93 Liberty st., N. Y. General Agents for the Am. Twist Drill Co.'s Superior Grinder and other Emery Wheel Machinery and Tools. Send for Circular. \ WOODBURY'S PATENT** Planing and Matching and Molding Machines, Gray & Wood's Planers, Self-oiling Saw Arbors, and other wood working machinery. S. A. WOODS, Send for Circulars. } 91 Liberty street, N. Y.; 67 Sudbury street, Boston. RI**CHARDSON, MERIAM & CO.,
\ Manufacturers of the latest improved Patent Daniels' and Woodworth Planing Machines, Matching, Sash, and molding, Tenoning, Mortising, Boring, Shaping, Vertical, and Circular Re-sawing Machines, Saw Mills Saw Arbors, Scroll Saws, Railway, Cut-off, and Rip-saw Machines, Spoke and Wood Turning Lathes, and various other kinds of Wood-working Machinery. Catalogues and price lists sent on application. Manufactory, Worcester, Mass. Warehouse, 107 Liberty st., New York. 17 1 Reynolds' TURBINE WATER WHEELS. The Oldest and Newest. All others only imitations of each other in their strife after complications to confuse the public. We do not boast but quietly excel them all in staunch reliable, economical power. Beautiful pamphlet free. Geo. TALLCOT, 96 Liberty st., New York. Gearing, Shafting.

To Manufacturers of Knitted Goods

Scientific American, Volume XXXVI., No. 8, February 24, 1877 by Various, is part of the HackerNoon Books Series. You can jump to any chapter in this book . New Agricultural Inventions here NEW AGRICULTURAL INVENTIONS. IMPROVED GANG PLOW. Ezra Peak, Montana, Kan.—This invention is so constructed that it may be easily raised from and lowered to the ground, and adjusted to work at any desired depth in the ground. It is claimed to be of lighter draft than plows constructed in the usual way, also to be simple in construction and inexpensive in manufacture. The wheels, the faces of which are notched to give them a slight up-and-down movement as they are drawn forward, slightly jar the plows, and thus cause them to be easier drawn than when smooth wheels are used. The shaft can be provided with a ratchet wheel and pawl to hold it in any position into which it may be turned; and to it is attached a rope or chain, the other end of which, is attached to the forward end of the frame, so that by turning the shaft the plows may be raised from, lowered to, and adjusted to work at any desired depth in the ground. IMPROVED PLOW. James Willis Hendley, Cedar Hill, N.C., assignor to David N. Bennett and Samuel T. Wright, of same place.—The objects here are simplicity and cheapness of construction, and such arrangement of parts as will prevent the plow becoming clogged with weeds, etc. The mold-board is welded to the land side, or cast in one piece with it, so that no brace or other connection is required between the mold-board and standard; secondly, the curved beam is attached to the heel of the land-side and supported by a brace, which is bolted to the middle portion of the latter, and arranged in such relation to the mold-board that a space is left between them, into which the trash will fall, and thus be drawn into the furrow and covered. IMPROVED GRAIN DRILL. George W. Osborn, Parkville, Mich.—This is an improved attachment for seed drills, for gaging the depth at which the grain shall be deposited in the earth. It consists in an adjustable spring gage bar attached to the shank of each drill tooth, whereby the teeth may be made to enter the ground a greater or less depth. It is claimed to ensure the planting of seeds at equal depth in hard or soft ground, and to diminish the draft. IMPROVED HORSE HAY RAKE. Joseph B. Wakeman and John L. Wager, Deposit, N.Y.—The construction of this implement is such that a large space is afforded beneath the rake head for the collection of hay. The pivots of said rake head back are also brought back, so that the teeth may be readily raised to discharge the collected hay. By an ingenious lever arrangement the driver is enabled to hold the rake to its work by the pressure of his foot, and also readily to discharge the hay gathered. IMPROVED BEE HIVE. George W. Akins, Bridgeton, Pa.—In this hive, holes are bored in the sides of the compartment for ventilation, and windows are flared for the purpose of inspecting the inside of the hive. A frame is used whenever it is desired to have the honeycomb of any particular shape. It consists of a form of tin or other suitable maternal, placed on a frame or slide, and having the shape required in the comb. Bees will build inside of the form, leaving about one fourth inch space between the form and the comb. The tin sheet receives a portion of the refuse matter, and can be readily taken out and cleaned. On the 1st of May the bees are driven out into another hive and the frames examined. Three frames are taken out and set in a new box, and three empty frames are put in their place. The old queen must be put with the new colony, and half of the bees must be put in each box and shut up, and put on a stand. The hives are to be opened the next morning. At the next natural swarming time the swarms can be again divided. The hive cannot freeze, and it is proof against mice. IMPROVED PLOW STOCK. Robert Weber, New Ulm, Texas.—In this invention, by loosening a nut, the point of draft attachment may be raised and lowered to cause the plow to work deeper or shallower in the ground, or turned to one or the other side, to cause the plow to take or leave land, and may be secured in place when adjusted by again tightening the nut. IMPROVED COMBINED HAY TEDDER AND SIDE RAKE. John Huber and Henry Snell, Girard, Ill.—This machine may be used simply for stirring up and turning the hay, or for turning the hay and gathering it into windrows. The shaft of a reel revolves in bearings attached to the side bars of the frame near their rear ends. To the bars of the reel are attached spring teeth, which, as the machine is drawn forward, take hold of the hay, carry it up and over the reel, and drop it to the ground in the rear of the machine. A carrier takes the hay from the teeth, when it has been brought to the top of the reel, carries it over the shaft, and discharges it into a trough, down which it slides, and is deposited in a windrow along one side of the path of the machine. IMPROVED GRUBBING MACHINE. Ira Burley, Redwing, Minn.—This invention consists in the combination of wheels and axle, tongue, adjusting bar, adjustable brace, uprights, cross bar, two ropes, and four pulley blocks with each other. To the forward end of the tongue is attached a loop or clevis, to receive an iron pin, to be driven into the ground to keep the machine from moving about while being used. To the pulley block is swiveled a hook, to be hooked into a loop, attached to the forward end of a lever. The rear end of the lever passes through a slot in the upper end of a fulcrum post, and has a notch formed in its lower side to receive a bolt or pin, attached to said post to serve as a fulcrum to said lever. Several notches are formed in the lever to receive the fulcrum bolt, to enable the position of the fulcrum post to be adjusted to regulate the leverage, and as circumstances may require. To the lever is attached a strong clevis, to receive the hook of the chain, that is secured to the stump to be pulled. IMPROVED SEED PLANTER. Daniel J. Davis, Red Boiling Springs, Tenn.—In this invention two wheels revolve upon the journals of the axle. Upon the end parts of the axle are attached the rear ends of side bars, the forward ends of which are bolted to the outer sides of the forward ends of the plow beams. The forward ends of the beams are bolted to the ends of the front bar, to the center of which is secured the forward end of the central bar. To the beams are attached the plows for opening furrows to receive the seed as it passes from the conductor spouts. The lower ends of the spouts or tubes pass in through the sides of the plows, so as to conduct the seed into the bottom of the furrows before they have been partially filled by the falling in of the soil. The dropping plate is concaved around its dropping holes, and is provided with a plate that may be adjusted to cover one set of dropping holes to drop the hills twice as far apart as when both sets of holes operate. IMPROVED ANIMAL TRAP. Thomas N. Hughes, Muddy Creek, Tenn.—This trap is for animals of all kinds, as rats, mice, and larger animals, as foxes, minks, coons, etc., that are allured by bait, and is automatically set again by the animal caught, to be ready for the next animal attracted by the bait. It is divided by a longitudinal partition into two main sections, in which the working parts are disposed. The entrance at the end of one section has a drop door, which is arranged back of the same, resting, when closed, on side strips in inclined position, and being supported on an upright arm, of a centrally pivoted treadle door, at the bottom of the trap, when the trap is set. The treadle door is only required to swing sufficiently on its pivots to release the drop door from the arm, suitable seats at the under side of the trap, at both sides of the treadle door, preventing the door from swinging farther than necessary. The bait is placed, in a grated receptacle, near the treadle door, and entices the animal to pass in, so as to close the drop door when it arrives at the part of the treadle door near the bait. The back end of this section is perforated or grated to admit light, which attracts the frightened animal and induces him to pass toward the light. The top part of the trap may be grated to admit air, and the glass door at the end made to slide, to admit the taking out of the animals for killing them. About HackerNoon Book Series: We bring you the most important technical, scientific, and insightful public domain books. This book is part of the public domain. Various (2006). Scientific American, Volume XXXVI., No. 8, February 24, 1877. Urbana, Illinois: Project Gutenberg. Retrieved https://www.gutenberg.org/cache/epub/19406/pg19406-images.html This eBook is for the use of anyone anywhere at no cost and with almost no restrictions whatsoever. You may copy it, give it away or re-use it under the terms of the Project Gutenberg License included with this eBook or online at , located at www.gutenberg.org https://www.gutenberg.org/policy/license.html

NEW AGRICULTURAL INVENTIONS

Scientific American Supplement, No. 711, August 17, 1889, by Various, is part of the HackerNoon Books Series. You can jump to any chapter in this book . SUCCESSION OF FOREST GROWTHS. here SUCCESSION OF FOREST GROWTHS. The following is from an address delivered by Mr. Robert Douglas before the Association of American Nurserymen at the meeting in Chicago recently. It is the prevailing and almost universal belief that when native forests are destroyed they will be replaced by other kinds, for the simple reason that the soil has been impoverished of the constituents required for the growth of that particular tree or trees. This I believe to be one of the fallacies handed down from past ages, taken for granted, and never questioned. Nowhere does the English oak grow better than where it grew when William the Conqueror found it at the time he invaded Britain. Where do you find white pines growing better than in parts of New England where this tree has grown from time immemorial? Where can you find young redwoods growing more thriftily than among their giant ancestors, nearly or quite as old as the Christian era? The question why the original growth is not reproduced can best be answered by some illustrations. When a pine forest is burned over, both trees and seeds are destroyed, and as the burned trees cannot sprout from the stump like oaks and many other trees, the land is left in a condition well suited for the germination of tree seeds, but there are no seeds to germinate. It is an open field for pioneers to enter, and the seeds which arrive there first have the right of possession. The aspen poplar ( ) has the advantage over all other trees. It is a native of all our northern forests, from the Atlantic to the Pacific. Even fires cannot eradicate it, as it grows in moist as well as dry places, and sprouts from any part of the root. It is a short-lived tree, consequently it seeds when quite young and seeds abundantly; the seeds are light, almost infinitesimal, and are carried on wings of down. Its seeds ripen in spring, and are carried to great distances at the very time when the ground is in the best condition for them. Even on the dry mountain sides in Colorado, the snows are just melting and the ground is moist where they fall. Populus tremuloides To grow this tree from seed would require the greatest skill of the nurseryman, but the burnt land is its paradise. Wherever you see it on high, dry land you may rest assured that a fire has been there. On land slides you will not find its seeds germinating, although they have been deposited there as abundantly as on the burned land. Next to the aspen and poplars comes the canoe birch, and further north the yellow birch, and such other trees as have provision for scattering their seeds. I have seen acorns and nuts germinating in clusters on burned lands in a few instances. They had evidently been buried there by animals and had escaped the fires. I have seen the red cherry ( ) coming up in great quantities where they might never have germinated had not the fires destroyed the debris which covered the seed too deeply. Prunus Pennsylvanica A careful examination around the margin of a burned forest will show the trees of surrounding kinds working in again. Thus by the time the short-lived aspens (and they are very short-lived on high land) have made a covering on the burned land, the surrounding kinds will be found re-established in the new forest, the seeds of the conifers, carried in by the winds, the berries by the birds, the nuts and acorns by the squirrels, the mixture varying more or less from the kinds which grew there before the fire. It is wonderful how far the seeds of berries are carried by birds. The waxwings and cedar birds carry seeds of our tartarean honeysuckles, purple barberries and many other kinds four miles distant, where we see them spring up on the lake shore, where these birds fly in flocks to feed on the juniper berries. It seems to be the same everywhere. I found European mountain ash trees last summer in a forest in New Hampshire; the seed must have been carried over two miles as the crow flies. While this alternation is going on in the East, and may have been going on for thousands of years, the Rocky Mountain district is not so fortunate. When a forest is burned down in that dry region, it is doubtful if coniferous trees will ever grow again, except in some localities specially favored. I have seen localities where short-lived trees were dying out and no others taking their places. Such spots will hereafter take their places above the timber line, which seems to me to be a line governed by circumstances more than by altitude or quality of soil. There are a few exceptions where pines will succeed pines in a burned-down forest. grows up near the timber line in the Rocky Mountains. This tree has persistent cones which adhere to the trees for many years. I have counted the cones of sixteen years on one of these trees, and examined burned forests of this species, where many of the cones had apparently been bedded in the earth as the trees fell. The heat had opened the cones and the seedlings were growing up in myriads; but not a conifer of any other kind could be seen as far as the fire had reached. Pinus Murrayana In the Michigan Peninsula, northern Wisconsin and Minnesota, , a comparatively worthless tree, is replacing the valuable red pine ( ), and in the Sierras and are replacing the more valuable species by the same process. P. Banksiana P. resinosa P. Murrayana P. tuberculata In this case, also, the worthless trees are the shortest lived. So we see that nature is doing all that she can to remedy the evil. Man only is reckless, and especially the American man. The Mexican will cut large limbs off his trees for fuel, but will spare the tree. Even the poor Indian, when at the starvation point, stripping the bark from the yellow pine ( ), for the mucilaginous matter being formed into sap wood, will never take a strip wider than one third the circumference of the tree, so that its growth may not be injured. P. ponderosa We often read that oaks are springing up in destroyed forests where oaks had never grown before. The writers are no doubt sincere, but they are careless. The only pine forests where oaks are not intermixed are either in land so sandy that oaks cannot be made to grow on them at all, or so far north that they are beyond their northern limit. In the Green Mountains and in the New England forests, in the pine forests in Pennsylvania, in the Adirondacks, in Wisconsin and Michigan—except in sand—I have found oaks mixed with the pines and spruces. In northwestern Minnesota and in northern Dakota the oaks are near their northern limit, but even there the burr oak drags on a bare existence among the pines and spruces. In the Black Hills, in Dakota, poor, forlorn, scrubby burr oaks are scattered through the hills among the yellow pines. In Colorado we find them as shrubs among the pines and Douglas spruces. In New Mexico we find them scattered among the piñons. In Arizona they grow like hazel bushes among the yellow pines. On the Sierra Nevada the oak region crosses the pine region, and scattering oaks reach far up into the mountains. Yet oaks will not flourish between the one hundredth meridian and the eastern base of the Sierras, owing to the aridity of the climate. I recently found oaks scattered among the redwoods on both sides of the Coast Range Mountains. Darwin has truly said, "The oaks are driving the pines to the sands." Wherever the oak is established—and we have seen that it is already established whereever it can endure the soil and climate—there it will remain and keep on advancing. The oak produces comparatively few seeds. Where it produces a hundred, the ash and maple will yield a thousand, the elm ten thousand, and many other trees a hundred thousand. The acorn has no provision for protection and transportation like many tree seeds. Many kinds are furnished with wings to float them on the water and carry them in the air. Nearly every tree seed, except the acorn, has a case to protect it while growing, either opening and casting the seeds off to a distance when ripe or falling with them to protect them till they begin to germinate. Even the equally large seeds of other kinds are protected in some way. The hickory nut has a hard shell, which shell itself is protected by a strong covering until ripe. The black walnut has both a hard shell and a fleshy covering. The acorn is the only seed I can think of which is left by nature to take care of itself. It matures without protection, falls heavily and helplessly to the ground, to be eaten and trodden on by animals, yet the few which escape and those which are trodden under are well able to compete in the race for life. While the elm and maple seeds are drying up on the surface, the hickories and the walnuts waiting to be cracked, the acorn is at work with its coat off. It drives its tap root into the earth in spite of grass, and brush, and litter. No matter if it is shaded by forest trees so that the sun cannot penetrate, it will manage to make a short stem and a few leaves the first season, enough to keep life in the root, which will drill in deeper and deeper. When age or accident removes the tree which has overshadowed it, then it will assert itself. Fires may run over the land, destroying almost everything else, the oak will be killed to the ground, but it will throw up a new shoot the next spring, the root will keep enlarging, and when the opportunity arrives it will make a vigorous growth, in proportion to the strength of the root, and throw out strong side roots, and after that care no more for its tap root, which has been its only support, than the frog cares for the tail of the tadpole after it has got on its own legs. There is no mystery about the succession of forest growths, nothing in nature is more plain and simple. We cannot but admire her wisdom, economy, and justness, compensating in another direction for any disadvantage a species may have to labor under. Every kind of tree has an interesting history in itself. Seeds with a hard shell, or with a pulpy or resinous covering which retards their germination, are often saved from becoming extinct by these means. The red cedar ( ) reaches from Florida to and beyond Cape Cod; it is among the hills of Tennessee, through the Middle States and New England. It is scattered through the Western States and Territories, at long distances apart, creeping up the Platte River, in Nebraska. (I found only three in the Black Hills, in Dakota, in an extended search for the different trees which grow there. Found only one in a long ramble in the hills at Las Vegas, New Mexico.) Yet this tree has crept across the continent, and is found here and there in a northwesterly direction between the Platte and the Pacific Coast. It is owing to the resinous coating which protects its seeds that this tree is found to-day scattered over that immense region. Juniperus Virginiana About HackerNoon Book Series: We bring you the most important technical, scientific, and insightful public domain books. This book is part of the public domain. Various (2004). Scientific American Supplement, No. 711, August 17, 1889. Urbana, Illinois: Project Gutenberg. Retrieved https://www.gutenberg.org/cache/epub/16972/pg16972-images.html This eBook is for the use of anyone anywhere at no cost and with almost no restrictions whatsoever. You may copy it, give it away or re-use it under the terms of the Project Gutenberg License included with this eBook or online at , located at . www.gutenberg.org https://www.gutenberg.org/policy/license.html

SUCCESSION OF FOREST GROWTHS

Scientific American, Vol. XXXIX. No. 6. [New Series.], August 10, 1878, by Various, is part of the HackerNoon Books Series. You can jump to any chapter in this book . A NEW DEEP SEA THERMOMETER. here A NEW DEEP SEA THERMOMETER. Perhaps some of our readers may have seen a description of a form of thermometer devised by MM. Negretti and Zambra for the purpose of ascertaining the temperature of the ocean at great depths. This consisted of a tube bent into the shape of a siphon, which when it had reached the desired depth was made, by means of an ingenious arrangement, to pour all the mercury found above a certain point near the reservoir into the second arm of the siphon. This second arm, which, like the other, was a capillary tube, carried a scale of divisions on which might be read the temperature of the depths to which the instrument had been lowered. This thermometer gave all the results that might have been expected. The ship Challenger during its polar expedition had on board a certain number of these instruments. The report of Capt. G. S. Nares made to the English Admiralty describes all the benefits that we may hope to reap from a serious study of the temperature of the ocean at different depths, and not the least of these are those that pertain to the fishery interest. Notwithstanding the good results given by this instrument, its inventors have endeavored to render it still more practical and more within the reach of all by diminishing the cost of construction, and increasing its compactness. represents the thermometer isolated from its case. It is an ordinary thermometer furnished at A with a little device that M. Negretti has already made use of in the construction of his larger instrument, and which allows the liquid to run from the reservoir into the capillary tube when the temperature rises, without letting it flow back when it lowers, if moreover the precaution has been taken to incline the tube slightly, reservoir upward. At B there is a bulge in the tube in which a certain quantity of mercury may lodge; this bulge is placed in such a way that the mercury resulting from the dilatation of the reservoir may come to it and continue its ascension in the capillary tube when the reservoir is down (the thermometer being vertical), but cannot get out when the reservoir is upward. Fig. 1 We should add that these thermometers are constructed so as to give the variations of temperature within determined limits. The small reservoir, B, is indispensable to the well working of the apparatus; for in seeking the temperature at a certain depth the instrument may, on being drawn up, pass through warmer strata, and it is necessary, therefore, to provide the reservoir with a means of diffusing the small quantity of mercury resulting from this excess of temperature. The tube has also a small bulge at its upper extremity at C. The thermometer is placed in a small wooden case having a double bottom throughout its length. In this double bottom are placed a certain number of lead balls that can run from one end of the case to the other, and of sufficient weight to render the instrument buoyant in sea water. To use the apparatus, one end of a cord is passed through a hole in the case under the reservoir of the thermometer, and the other end is tied to the sounding line at a certain distance from the lead ( ). While the line is descending the thermometer will remain reservoir downward ( ); but when it is again drawn up the thermometer case will take the position indicated in , and the column of mercury breaking at A will fall into the capillary tube, the divisions of which, as will be seen at , are reversed. Fig. 2 Fig. 2 Fig. 3 Fig. 1 As to the thermometer itself, it is important to protect it against the pressure which becomes so considerable at great depths; to do this the reservoir is surrounded by an envelope of thick glass about three quarters full of mercury. The mercury serves to transmit the temperature to the reservoir, and should the exterior envelope yield to the effects of pressure, the reservoir proper would not be affected, the mercury not exactly filling the annular part which surrounds it. New Inventions. George E. Palmer, of Cedar Rapids, Iowa, has patented an improved Ironing Board, on which the garments may be held in stretched state while being smoothed with the irons, and readily adjusted thereon to any required degree of tension by a simple attachment. William B. Rutherford and Joel T. Hawkins, of Rockdale, Texas, have patented an improved Bale Tie, which is formed of the plate provided with a longitudinal groove and cross ribs or loops, and having projections or keys to adapt it to receive and hold the notched ends of the bale band. An improvement in Composition Pavements has been patented by John C. Russell, of Kensington, Eng. This invention relates to the treatment of peat and spent tan for the manufacture of an improved product or material suitable for paving roads and other places and for roofing, etc. The most important steps in making the composition consist in drying bruised or finely ground peat or spent tan, heating the same to degree of 150° Fah., and adding sulphur and gas tar, gas pitch, and stearine pitch in the proportions specified, then kneading the mixture while heated and adding carbonate of lime and furnace slag. in vacuo Louis Blanck, of New York city, has patented an improved Safety Brake or attachment for locomotives and railroad cars, by which the entire train, either by a collision with another train or by contact with any obstruction, is first raised from the rails, and then moved in backward direction for the distance of a few feet, so that all danger of accident is avoided, and no other sensation than that of a slight rocking motion exerted. The attachment is constructed so as to admit of being worked by the engineer from the cab or the locomotive, or, if desired, from any car of the train. An improved Evaporating Pan had been patented by Andrew D. Martin, of Abbeville, La. This invention consists in a tapering sheet metal tank having transverse partitions and longitudinal tapering flues that extend through all of the partitions and terminate at the ends of the tank. Lloyd Arnold, of Galveston, Texas, has patented an improved Bale Tie, which is formed of a block of iron, with a space or opening running longitudinally through its breadth from one end nearly to the other, and having the alternate edges of the two plates thus formed notched, the notch of the lower plate being square and of a width equal to or a little greater than the bale band, and the notch of the upper plate being narrower at its bottom than the bale band, and with its sides inclined and beveled to an edge, to adapt it to receive and hold the bale band. An improved Tie for Letter Packages has been patented by John Mersellis, of Knowersville, N. Y. The object of this invention is to provide a tie by means of which letter packages may be quickly and securely fastened or tied. It consists in a plate apertured to receive one end of the string and also to receive the hook upon which the tie is hung when not in use, and having a button and clasp spring for engaging the string in the process of tying. Fred P. Hammond, of Aurora, Ill., has patented an improved Inking Pad, which consists in a novel arrangement of layers of cloth or felt, chamois skin, oiled silk, and printing roller composition, which enables a clean impression of the stamp to be made. The pad retains the desired rounded surface and proper degree of softness, and is easily manipulated when necessary to replenish the supply of ink. William J. Clark and Thomas W. Roberts, of Coffeeville, Miss., have patented an improved Trap for Catching Fish in streams, which will allow the fish to be conveniently taken out without taking up the trap. John W. Cooper, of Salem, Ind., is the inventor of an improved Alcohol Lamp for soldering and similar purposes; and it consists in a reservoir pivoted in a supporting frame, and provided with two wick tubes, and an extinguisher secured to a spring support, and capable of closing the larger wick tube when it is in a vertical position. It has an independent extinguisher for the smaller wick tube, and is provided with a novel device for projecting the wick from the larger tube as it is moved out of a vertical position. Benjamin Slater, of Attica, N. Y., has invented a simple and effective device for Renovating Feathers by the combined action of steam and hot air. It consists of a cylindrical receptacle, partly surrounded by a steam jacket, and having a hot air box, a perforated bottom, a cover or damper for the same, and an aperture in the top, to which is fitted a perforated cover and a close cover. An improved Blind Fastening has been patented by George Runton and John Runton, of Hoboken, N. J. This fastening is so constructed as to fasten the blind or shutter automatically when swung open, and in such a way as to prevent all rattling or shaking of the blind or shutter from the action of the wind. David R. Nichols, of Alexandria Bay, N. Y., has patented an improved Animal Trap, which is so constructed as to set itself after each animal has been caught, and leave no trace of the trapped animal to frighten away those that may come afterward. William A. Doherty, of Fall River, Mass., has patented an improved Loom Shuttle Attachment, by which the weaving of bad cloth is prevented, and in case any false shed is made by any irregularities in the warp, and that part of the shed carried lower than usual, the attachment is released and thrown over the spindle point, so as to render it impossible to draw out the filling from the shuttle, and thus break it and stop the loom. Jonas Bowman, of Somerset, O., has patented an improved Vehicle Spring, which permits of dispensing with side bars, thus taking less space to turn on, and by which the tilting and pitching motion usual with springs as heretofore constructed is avoided. Hiram Unger, of Germantown, O., is the inventor of an improved Gate Latch, which is so constructed that the gate cannot be opened accidentally by being lifted or by rebounding of the catch or latch. Madison Calhoun, of Ocate, Ter. of New Mex., has patented an improved Hame Fastening, which is not liable to become accidentally unfastened, and is easily and quickly fastened and unfastened, even with cold or gloved hands. The Downer well at Corry, Pa., is now down over 1,300 feet, and an oil bearing sand has been struck of about five feet thickness. About HackerNoon Book Series: We bring you the most important technical, scientific, and insightful public domain books. This book is part of the public domain. Various (2013). Scientific American, Vol. XXXIX. No. 6. [New Series.], August 10, 1878. Urbana, Illinois: Project Gutenberg. Retrieved https://www.gutenberg.org/cache/epub/19406/pg19406-images.html This eBook is for the use of anyone anywhere at no cost and with almost no restrictions whatsoever. You may copy it, give it away or re-use it under the terms of the Project Gutenberg License included with this eBook or online at , located at www.gutenberg.org https://www.gutenberg.org/policy/license.html

A NEW DEEP SEA THERMOMETER

Scientific American Supplement, No. 365, December 30, 1882 by Various is part of the HackerNoon Books Series. Read this book online for free on HackerNoon! : Scientific American Supplement, No. 365, December 30, 1882 Title : Various Author : July 6, 2006 [eBook #18763] Release date : English Language TABLE OF LINKS I. ENGINEERING AND MECHANICS. Louis Favre, Constructor of the St. Gothard Tunnel. The New Harbor of Vera Cruz. Cost of Power to Make Flour. Driving gear Mechanism for Lift Hammers. De Junker and Ruh's Machine for Cutting Annular Wheels. Recent Hydraulic Experiments. The Germ: Shall It be Retained in Flour? Wheat Tests II. TECHNOLOGY AND CHEMISTRY. Apparatus for Manufacturing Gaseous or Aerated Beverages. Detection and Estimation of Fusel Oil. On Silicon. Stannous Nitrates. Metallic Thorium. Friedrich Wöhler. Apparatus for Printing by the Blue Process. III. ELECTRICITY, LIGHT, HEAT, ETC. Spectrum Gratings. A New Pocket Opera Glass. Atoms, Molecules, and Ether Waves. Apparatus for Measuring Electricity at the Upper School of Telegraphy. IV. NATURAL HISTORY. Our Origin as a Species. The Aba or Odika. California Cedars. Ancient Greek Painting. About HackerNoon Book Series: We bring you the most important technical, scientific, and insightful public domain books. This book is part of the public domain. Various (2006). Scientific American Supplement, No. 365, December 30, 1882. Urbana, Illinois: Project Gutenberg. Retrieved https://www.gutenberg.org/cache/epub/18763/pg18763-images.html This eBook is for the use of anyone anywhere at no cost and with almost no restrictions whatsoever. You may copy it, give it away or re-use it under the terms of the Project Gutenberg License included with this eBook or online at , located at . www.gutenberg.org https://www.gutenberg.org/policy/license.html

Stories, News & Mentions about CEDAR

Cedar’s Stories on HackerNoon