Email Gateway (Aug 18 2022 at 11:51): Email Gateway (Aug 18 2022 at 11:51):From: John Matthews <matthews@galois.com>
Hello,
I am trying to provide a shallow embedding of the Cryptol primitive
"cerror :: int => int => string => 'a". Logically this is an undefined
value, but I'd like Isabelle's quickcheck command to compile the
Cryptol expression "cerror a b str" into the SML expression "error
str", so that quickcheck throws an exception if cerror s ever executed
during a run. How do I define cerror appropriately?
Thanks,
-john
Email Gateway (Aug 18 2022 at 11:51):From: Tobias Nipkow <nipkow@in.tum.de>
Hi John,
Here's a solution (with only one int argument - trust you can generalize ;-)
consts cerror :: "int => string => 'a"
consts_code
"cerror" ("(fn i => (fn x => error(implode x)))")
definition f where "f i == if i < 0 then cerror i ''x'' else i"
lemma "f x = x"
The implode is required because HOL's strings are implemented as char lists.
However, there are two things that puzzle me, that the implementor might
be able to comment on:
autoquickcheck does seem to kick in or its result is hidden...
If in the ML code for cerror I replace the i by _, I have a problem:
the generatd ML does not type check...
Tobias
John Matthews schrieb:
Email Gateway (Aug 18 2022 at 11:51):From: Stefan Berghofer <berghofe@in.tum.de>
Tobias Nipkow wrote:
However, there are two things that puzzle me, that the implementor might
be able to comment on:
- autoquickcheck does seem to kick in or its result is hidden...
auto quickcheck only outputs something if it finds a counterexample,
i.e. the goal evaluates to False. If the code generator signals an error
because the current goal is not executable, the compilation of the generated
code fails because it is ill-formed, or an exception is raised during the
execution of the code, this is silently ignored. The rationale behind this
was to prevent auto quickcheck from displaying too many "spam messages" that
might confuse users.
- If in the ML code for cerror I replace the i by _, I have a problem:
the generatd ML does not type check...
The problem is that _ has a special meaning: like in mixfix templates,
the _ in a declaration
consts_code
f ("...")
indicates a position in the ML code "..." where code for the arguments of f
should be inserted (see e.g. the definition of "+" in the Int theory). If
you want a _ to occur in the ML code, you have to escape it by writing '_
(like in mixfix templates).
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 11:51):From: John Matthews <matthews@galois.com>
Thanks, Stefan. Is it possible to have a special "undefined" or
"quickcheck" exception that is not silently ignored by quickcheck? I
want to make cerror executable exactly so that autoquickcheck will
tell me if I have an unintended execution path leading to it.
Thanks,
-john
Email Gateway (Aug 18 2022 at 11:51):From: Tobias Nipkow <nipkow@in.tum.de>
That's a discussion we have been having internally as well. For example,
autoquickcheck currently does not object to "hd xs # tl xs = xs" because
it ignores the Match exception thrown by "hd []". We'll take this
discussion up again (with a reduced audience).
Tobias
John Matthews schrieb:
Last updated: May 03 2024 at 12:27 UTC