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

```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
--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

```

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