Email Gateway (Aug 22 2022 at 09:08): Email Gateway (Aug 22 2022 at 09:08):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.
Best,
Andreas
Email Gateway (Aug 22 2022 at 09:40):From: Wenda Li <wl302@cam.ac.uk>
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
Last updated: Nov 21 2024 at 12:39 UTC