Re: [isabelle] Code generation for certificate-based external/untrusted functions

Dear Wenda,

When certification fails, you can either call a slow implementation or abort with an error. The latter option occurs quite frequently in more advanced code setups. There is the constant Code.abort. Logically, "Code.abort msg f" is defined as "f ()", but during code generation, it raises an exception with msg as error message instead of evaluating f. In your case, the code equation could look like the following:

lemma gcd_int_code [code]:
  "gcd a b =
  (let (c,a',b') = untrusted_gcd a b
   in if valid_gcd_rel a b (c,a',b') then c
      else Code.abort (STR ''gcd: certification failed'' (%_. gcd a b)))"

Code.abort works well with code generation and evaluation with code_simp, but not with normalisation by evaluation. If you need the latter, you should declare your own constant for this specific error case and duplicate the setup for Code.abort.


On 11/04/15 16:18, Wenda Li wrote:
Dear code generation experts,

Suppose I have a highly efficient greatest common divisor implementation for integers
(based on modular arithmetic, subresultants, bit-shifting etc.), and I want to use it to
boost our default gcd computation in Isabelle. A good thing about gcd is that it can
produce a certificate (i.e. Bezout's identity) such that an untrusted result can be easily
verified. Therefore, I am thinking about building a certificate-based code equation for gcd:

definition valid_gcd_rel :: "int => int => int à int à int => bool" where
   "valid_gcd_rel a b r= (let (c,a',b') =r in
     aâ0 â bâ0 â c>0 â c dvd Âa â c dvd Âb â ÂaÂ*a' + ÂbÂ*b'=c)"

lemma gcd_valid:
   fixes a b c a' b' :: int
   assumes "valid_gcd_rel a b (c,a',b')"
   shows "gcd a b = c"

(*suppose this is an untrusted but very efficient implementation which
   produces gcd together with a certificate*)
definition untrusted_gcd :: "int => int => int à int à int" where
   "untrusted_gcd a b = (if a=6 â b=5 then (1,1,-1) else undefined)"

declare gcd_code_int [code del]

lemma gcd_code[code]:
   "gcd a b = (let
       (c,a',b') = untrusted_gcd a b
     in if valid_gcd_rel a b (c,a',b') then c else (SOME c. c=gcd a b)) "

Lemma gcd_valid and gcd_code should both be provable. And the value command works just as

value "gcd (6::int) 5" (*1*)
value "gcd (6::int) 4" (*gcd 6 4*)

That is, when "valid_gcd_rel a b (c,a',b')" is evaluated to be true, we use the result
from untrusted_gcd, otherwise we leave the expression unchanged. However, when I want to
boost the gcd computation further using code_reflect:

code_reflect Foo
   datatypes int="_"
   functions "gcd::int=>int=>int"

an error occurs because Eps has no code equation. Of course, in this case, I can resolve
this problem by replacing "(SOME c. c=gcd a b)" with a "slow" but executable version of
gcd (e.g. the default version), but in general it is not convenient to build and certify
even a slow version every time. Is there any way to cope with this problem?

In general, there are many operations, such as ideal membership test, whose results can be
easily verified by some certificates while a direct implementation (even a naive one) is
very hard to verify within Isabelle. I was wondering if this certificate-based approach
can be a way to improve execution efficiency of functions within Isabelle.

Any comment/suggestion is greatly appreciated,

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