Proof-Producing Synthesis of CakeML from Monadic HOL Functions
- PDF / 401,746 Bytes
- 20 Pages / 439.37 x 666.142 pts Page_size
- 30 Downloads / 176 Views
Proof-Producing Synthesis of CakeML from Monadic HOL Functions Oskar Abrahamsson1 · Son Ho2 · Hrutvik Kanabar3 · Ramana Kumar4 · Magnus O. Myreen1 · Michael Norrish5 · Yong Kiam Tan6 Received: 21 April 2020 / Accepted: 24 April 2020 © The Author(s) 2020
Abstract We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover. Keywords Interactive theorem proving · Program synthesis · ML · Higher-order logic
1 Introduction This paper is about bridging the gap between programs verified in logic and verified implementations of those programs in a programming language (and ultimately machine code). As a toy example, consider computing the nth Fibonacci number. The following is a recursion equation for a function, fib, in higher-order logic (HOL) that does the job: def
fib n = if n < 2 then n else fib (n − 1) + fib (n − 2) A hand-written implementation (shown here in CakeML [10], which has similar syntax and semantics to Standard ML) would look something like this:
B
Oskar Abrahamsson [email protected]
1
Chalmers University of Technology, Göteborg, Sweden
2
MINES ParisTech, PSL Research University, Paris, France
3
University of Kent, Canterbury, UK
4
DeepMind, London, UK
5
Data61, CSIRO/ANU, Canberra, Australia
6
Carnegie Mellon University, Pittsburgh, USA
123
O. Abrahamsson et al. fun fiba i j n = if n = 0 then i else fiba j (i+j) (n-1); (print (n2s (fiba 0 1 (s2n (hd (CommandLine.arguments()))))); print "\n") handle _ => print_err ("usage: " ˆ CommandLine.name() ˆ " \n");
In moving from mathematics to a real implementation, some issues are apparent: (i) We use a tail-recursive linear-time algorithm, rather than the exponential-time recursion equation. (ii) The whole program is not a pure function: it does I/O, reading its argument from the command line and printing the answer to standard output. (iii) We use exception handling to deal with malformed inputs (if the arguments do not start with a string representing a natural number, hd or s2n may raise an exception). The first of these issues (i) can easily be handled in the realm of logical functions. We define a tail-recursive version in logic: def
fiba i j n = if n = 0 then i else fiba j (i + j) (n − 1) then produce a correctness theorem, ∀ n. fiba 0 1 n = fib n, with a simple inductive proof (a 5-line tactic proof in HOL4, not shown). Now, because fiba is a logical function with an obvious computational counterpart, we can use proof-producing synthesis techniques [14] to automatically synthesise code verified to compute it. We thereby produc
Data Loading...
