*To*: cl-isabelle-users at lists.cam.ac.uk, Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] Some Remarks to Code Generation*From*: Magnus Myreen <mom22 at cam.ac.uk>*Date*: Wed, 1 Aug 2012 11:29:42 +0100*Cc*: Scott Owens <scott.owens at cl.cam.ac.uk>*In-reply-to*: <50189089.3040002@jaist.ac.jp>*References*: <234E321B-095C-4FBC-9DBC-CD3E5693D8D6@pbmichel.de> <op.wibki8x0ule2fv@douda-yannick> <50189089.3040002@jaist.ac.jp>*Sender*: magnus.myreen at gmail.com

> 2) The only guarantee code-generation gives (and that is quite a strong one) > is that the generated code is a sound rewriting engine for the function > defined in the logic (assuming that every tool in the typical chain -- e.g., > compiler, OS -- is correct). I think you should add to that list of assumptions that the soundness of the Isabelle code generator must also be assumed. To my knowledge (correct me if I'm wrong!), Isabelle's code generator comes with no formal guarantee of producing code that is correct w.r.t. the semantics of the generated code. By formal guarantee, I mean a theorem in Isabelle/HOL's logic relating the given input (equations in Isabelle/HOL) to the semantics of the generated code (ML, Haskell, Scala ...). Scott Owens and I have developed a code generator (for HOL4) which provides such guarantees, see: Magnus O. Myreen and Scott Owens. Proof-Producing Synthesis of ML from Higher-Order Logic. To appear in ICFP'12. http://www.cl.cam.ac.uk/~mom22/miniml/hol2miniml.pdf Our code generator takes normal HOL functions as input, translates these into ML and proves that the generated ML code *terminates* and correctly implements the given input functions according to an operational semantics of our ML language (called MiniML, which is a pure subset of ML and Haskell). Example: As an example, if we were to translate HOL4's library function for FOLDL: |- (forall f e. FOLDL f e [] = e) /\ (forall f e x l. FOLDL f e (x::l) = FOLDL f (f e x) l) The tool generates some MiniML code (shown here in SML syntax): datatype ('a) list = Cons of 'a * ('a) list | Nil ; fun FOLDL v3 = (fn v4 => (fn v5 => (case v5 of Nil => v4 | (Cons (v2, v1)) => (((FOLDL v3) ((v3 v4) v2)) v1)))) ; and our code generator automatically proves that this code correctly implements the HOL function FOLDL according to an operational semantics of MiniML (Eval below). Here code_for_FOLDL_in asserts that the above code is in the environment env, and --> is an infix "refinement invariant combinator" explained in the paper. |- code_for_FOLDL_in env ==> Eval env (Var "FOLDL") (((b --> a --> b) --> b --> LIST a --> b) FOLDL) We call such theorems 'certificate theorems'. End of Example. I should also mention that we (Ramana Kumar, Scott Owens and I) are constructing a verified MiniML implementation (including dynamic compilation to x86), so that the trust story can be extended all the way down to concrete x86/ARM machine code. > See also "Code Generation via Higher-Order Rewrite Systems" by Haftmann and > Nipkow, where they state: Interesting. I wasn't aware of this paper. It seems that this paper has proved that an internal phase (dictionary translation) does the right thing w.r.t. a model of HRSs. > [...] partial correctness of the generated programs w.r.t. the > original equational theorems is guaranteed. Note that your "[...]" omission hides the big assumption: "If the code generator preserves [the semantics of] the equations from the logic when turning them into programs" > No claims are stated for aspects which have no explicit > representation in the logic, in particular termination or > runtime complexity. Our code generator proves termination. It does this by using the induction theorems that arise from function definition (and their totality proofs). By the way, the last part of the following sentence from Haftmann and Nipkow's FLOPS'10 paper is a brave statement with no justification: "The transformation of an intermediate program to a program in a full-blown SML or Haskell-like target language is again a mere syntactic adjustment and does not change the equational semantics." Cheers, Magnus On 1 August 2012 03:12, Christian Sternagel <c-sterna at jaist.ac.jp> wrote: > On 08/01/2012 01:38 AM, Yannick Duchêne (Hibou57) wrote: >> >> Le Tue, 31 Jul 2012 18:13:12 +0200, Patrick Michel <uni at pbmichel.de> a >> écrit: >>> >>> As it turns out it is quite easy to prove a code equation that >>> obviously leads to non-terminating execution. >> >> >> I've not reached that point (still learning Isabelle and HOL), but I'm >> already interested in this, as I will generate SML programs from proofs. >> Can you please, provide a concrete example of an erroneous proof of a >> non-terminating function? > > Just to clarify. There is nothing "erroneous" going on here. There are just > two different perspectives: > > 1) In HOL only functions that are provably total are accepted (but being > total does not mean that the same function when executed as a functional > program is terminating, since in HOL there is nothing like an evaluation > strategy). Consider, e.g., > > definition ite where > "ite b x y == if b then x else y" > > lemmas ite_cong [fundef_cong] = if_cong [folded ite_def] > > fun f :: "nat => nat" where > "f x = ite (x = 0) 1 (f (x - 1) * x)" > > The call relation of f is well-founded (since in every recursive call the > argument is decreased by one). However when exporting code in any language > with strict evaluation, the result will loop on any input. > > 2) The only guarantee code-generation gives (and that is quite a strong one) > is that the generated code is a sound rewriting engine for the function > defined in the logic (assuming that every tool in the typical chain -- e.g., > compiler, OS -- is correct). Being a sound rewriting engine means that every > equation that can be derived by evaluation in the programming language is > also an equation of HOL. > > See also "Code Generation via Higher-Order Rewrite Systems" by Haftmann and > Nipkow, where they state: > > [...] partial correctness of the generated programs w.r.t. the > original equational theorems is guaranteed. > No claims are stated for aspects which have no explicit > representation in the logic, in particular termination or > runtime complexity. > > cheers > > chris >

**Follow-Ups**:**Re: [isabelle] Some Remarks to Code Generation***From:*Florian Haftmann

**References**:**Re: [isabelle] Some Remarks to Code Generation***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] sloccount for .thy files?
- Next by Date: Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- Previous by Thread: Re: [isabelle] Some Remarks to Code Generation
- Next by Thread: Re: [isabelle] Some Remarks to Code Generation
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list