Case Studies in Cryptol - A study of domain specific languages for DSP algorithms

Abstract

Digital Signal Processing (DSP) has become part of many electronic applications these days; confluent to this, Domain Specific Languages (DSLs) are prevailing among practitioners of many engineering domains. Cryptol is a domain specific language for cryptography, it was designed by Galois and it has been used by NSA from the start. Cryptol is designed for cryptographic specifications; however, this project aims at evaluating Cryptol as a domain specific language for digital signal processing algorithms. The report also includes a proposal for extensions to Cryptol to make it applicable to DSP algorithms. This thesis derives its motivation from the DSL for DSP research that the Functional Programming group has started with Ericsson. This project involved implementing a set of DSP algorithms in Cryptol and analyzing applicability of Cryptol from the experiences in this new domain. This study shows that Cryptol is too specialised to cryptographic algorithms and that it is not possible to specify, run or verify many DSP algorithms in Cryptol. However there is a special class of DSP algorithms that are far easier to code in Cryptol than in C or Java. Small overlap with DSP algorithms was expected since DSLs are customized for a certain problem area. The evaluation of Cryptol in the DSP domain revealed that some enhancements are necessary to make it applicable to DSP algorithms. The outcome of this study is a set of extensions to Cryptol which are discussed towards the end of this report.