*To*: Wenda Li <wl302 at cam.ac.uk>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Code generation for certificate-based external/untrusted functions*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 13 Apr 2015 08:33:33 +0200*In-reply-to*: <157fdf001524af0eca9691de0bcde12c@cam.ac.uk>*References*: <157fdf001524af0eca9691de0bcde12c@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

Dear Wenda,

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

Best, Andreas 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" sorry (*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)) " sorry Lemma gcd_valid and gcd_code should both be provable. And the value command works just as expected: 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, Wenda

**References**:

- Previous by Date: Re: [isabelle] Isabelle2015-RC0 available for testing
- Next by Date: Re: [isabelle] Unknown Isabelle tool: env
- Previous by Thread: [isabelle] Code generation for certificate-based external/untrusted functions
- Next by Thread: [isabelle] Isabelle2015-RC0 available for testing
- Cl-isabelle-users April 2015 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