Re: [isabelle] Some Remarks to Code Generation



> 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
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.