# [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.*