Fast Machine Words in Isabelle/HOL

被引：7

作者：

Lochbihler, Andreas ^{[1
]}

机构：

[1] Swiss Fed Inst Technol, Dept Comp Sci, Inst Informat Secur, Zurich, Switzerland

来源：

INTERACTIVE THEOREM PROVING, ITP 2018 | 2018年 / 10895卷

关键词：

PROOF; GENERATION;

D O I：

10.1007/978-3-319-94821-8_23

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Code generated from a verified formalisation typically runs faster when it uses machine words instead of a syntactic representation of integers. This paper presents a library for Isabelle/HOL that links the existing formalisation of words to the machine words that the four target languages of Isabelle/HOL's code generator provide. Our design ensures that (i) Isabelle/HOL machine words can be mapped soundly and efficiently to all target languages despite the differences in the APIs; (ii) they can be used uniformly with the three evaluation engines in Isabelle/HOL, namely code generation, normalisation by evaluation, and term rewriting; and (iii) they blend in with the existing formalisations of machine words. Several large-scale formalisation projects use our library to speed up their generated code. To validate the unverified link between machine words in the logic and those in the target languages, we extended Isabelle/HOL with a general-purpose testing facility that compiles test cases expressed within Isabelle/HOL to the four target languages and runs them with the most common implementations of each language. When we applied this to our library of machine words, we discovered miscomputations in the 64-bit word library of one of the target-language implementations.

引用

页码：388 / 410

页数：23

共 52 条

[1] A compiled implementation of normalisation by evaluation [J].

Aehlig, Klaus ;

Haftmann, Florian ;

Nipkow, Tobias .

JOURNAL OF FUNCTIONAL PROGRAMMING, 2012, 22 :9-30

[2]

Anand A., 2017, COQPL 2017

[3]

Armand M, 2010, LECT NOTES COMPUT SC, V6172, P83, DOI 10.1007/978-3-642-14052-5_8

[4] On Definitions of Constants and Types in HOL [J].

Arthan, Rob .

JOURNAL OF AUTOMATED REASONING, 2016, 56 (03) :205-219

[5]

Blanchette J. C., 2018, P 7 ACM SIGPLAN INT, P158

[6]

Blanchette JC, 2011, LECT NOTES ARTIF INT, V6989, P12, DOI 10.1007/978-3-642-24364-6_2

[7]

Blot Arthur, 2016, Functional and Logic Programming. 13th International Symposium, FLOPS 2016. Proceedings: LNCS 9613, P12, DOI 10.1007/978-3-319-29604-3_2

[8]

Brucker AD, 2009, LECT NOTES COMPUT SC, V5503, P417

[9]

Bulwahn L., 2013, THESIS

[10]

Clavel M., 2007, ALL MAUDE A HIGH PER, DOI [10.1007/978-3-540-71999-1, DOI 10.1007/978-3-540-71999-1]

← 1 2 3 4 5 6 →