Safe Low-level Code Generation in Coq Using Monomorphization and Monadification

• Item type: Trans(1)
• 公開日: 2017-12-12
• タイトル: Safe Low-level Code Generation in Coq Using Monomorphization and Monadification
• タイトル / 言語: en
• タイトル: Safe Low-level Code Generation in Coq Using Monomorphization and Monadification
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: [通常論文] Coq, C, monomorphization, monadification, code generation
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: National Institute of Advanced Industrial Science and Technology (AIST)
• 著者所属: National Institute of Advanced Industrial Science and Technology (AIST)
• 著者所属: Graduate School of Mathematics, Nagoya University
• 著者所属(英): en
• 著者所属(英): National Institute of Advanced Industrial Science and Technology (AIST)
• 著者所属(英): en
• 著者所属(英): National Institute of Advanced Industrial Science and Technology (AIST)
• 著者所属(英): en
• 著者所属(英): Graduate School of Mathematics, Nagoya University
• 著者名: Akira, Tanaka; Reynald, Affeldt; Jacques, Garrigue
• 著者名(英): Akira, Tanaka; Reynald, Affeldt; Jacques, Garrigue
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Our goal is the production of formally-verified pieces of low-level code. Low-level code is typically written in C, so as to enable efficient manipulation of data at the bit-level and easy access to built-in features of CPUs. Proof-assistants arguably provide the most rigorous approach to formal verification of computer programs. Unfortunately, they only allow for extraction of runnable code in high-level languages such as ML. Of course it is possible to embed C snippets into ML programs, but this results in a complicated extraction process and the performance of the output program becomes difficult to anticipate. In this paper, we propose a new code generation scheme for the Coq proof-assistant that directly generates provably-safe C code. It is implemented in the form of plugins. The generation of C source code is done by a plugin performing beforehand monomorphization of Coq programs. The correctness of monomorphization can be proved within Coq. Code generation allows for user-guided changes of data structures. It is therefore possible to do formal verification using proof-friendly data structures, while enjoying optimized C representations in the output code. In order to ensure the safety of this transformation, we propose a new customizable monadification algorithm in the form of another plugin. Using monadification, one can ensure by the insertion of the right monads the preservation of critical invariants, such as the absence of overflows or complexity properties. We provide several examples to illustrate our approach, including a realistic use-case: the rank algorithm from succinct data structures.; ------------------------------; This is a preprint of an article intended for publication Journal of; Information Processing(JIP). This preprint should not be cited. This; article should be cited as: Journal of Information Processing Vol.26(2018) (online); ------------------------------
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Our goal is the production of formally-verified pieces of low-level code. Low-level code is typically written in C, so as to enable efficient manipulation of data at the bit-level and easy access to built-in features of CPUs. Proof-assistants arguably provide the most rigorous approach to formal verification of computer programs. Unfortunately, they only allow for extraction of runnable code in high-level languages such as ML. Of course it is possible to embed C snippets into ML programs, but this results in a complicated extraction process and the performance of the output program becomes difficult to anticipate. In this paper, we propose a new code generation scheme for the Coq proof-assistant that directly generates provably-safe C code. It is implemented in the form of plugins. The generation of C source code is done by a plugin performing beforehand monomorphization of Coq programs. The correctness of monomorphization can be proved within Coq. Code generation allows for user-guided changes of data structures. It is therefore possible to do formal verification using proof-friendly data structures, while enjoying optimized C representations in the output code. In order to ensure the safety of this transformation, we propose a new customizable monadification algorithm in the form of another plugin. Using monadification, one can ensure by the insertion of the right monads the preservation of critical invariants, such as the absence of overflows or complexity properties. We provide several examples to illustrate our approach, including a realistic use-case: the rank algorithm from succinct data structures.; ------------------------------; This is a preprint of an article intended for publication Journal of; Information Processing(JIP). This preprint should not be cited. This; article should be cited as: Journal of Information Processing Vol.26(2018) (online); ------------------------------
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 10, 号 6, 発行日 2017-12-12
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会