Email Gateway (Aug 22 2022 at 11:08): Email Gateway (Aug 22 2022 at 11:08):From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle/ML experts,
Suppose I have a function/constant in Isabelle/ML:
ML {*
val f:term -> term = (fn x => x);
*}
I was wondering if I can somehow access it in the top level. That is, I
wish I could define a function based on f:
definition "foo x=f x" (not working yet)
I know we can do similar things with theorem:
ML {*
ML_Thms.bind_thm("foo",@{thm exI});
*}
thm foo
In fact, this question is a follow-up question to my previous query:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-April/msg00102.html
where I want to use a piece of untrusted code (in Isabelle/ML probably)
to compute some untrusted but verifiable results. In order to verify and
use such results, I may need to extract them from the Isabelle/ML level
to the top level.
Any help is greatly appreciated,
Wenda
Email Gateway (Aug 22 2022 at 11:08):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Wenda,
There is no official support for this, but two months ago, Lars Hupel implemented a sketch
of what might be useful for you. Have a look:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-June/msg00076.html
Best,
Andreas
Email Gateway (Aug 22 2022 at 11:09):From: Wenda Li <wl302@cam.ac.uk>
Dear Andreas,
Many thanks for referring me to Lars Hupel' wonderful SPLICE technique!
It did seem quite relevant in my situation. However, it seems that the
SPLICE can only embed "static" code (I am not sure if my description is
accurate or not) in Isabelle/ML to the top level. For example,
theory Scratch4 imports
Main
"Splice/Splice"
begin
ML {*
val g:int -> int = (fn x => x+2);
fun g1 (x:term): term = (if is_Bound x then x else g
(HOLogic.dest_number x |> snd) |> HOLogic.mk_number @{typ int}) ;
fun g2 (x:term):term = Const ("Groups.plus_class.plus", @{typ "int ⇒
int ⇒ int"}) $ x $ @{term "2::int"};
*}
definition "foo= (λx. SPLICE ‹g2 (Bound 0)›)"
print_theorems (foo_def: foo = (λx. x + 2))
definition "foo'= (λx. SPLICE ‹g1 (Bound 0)›)"
print_theorems (foo'_def: foo' = (λx. x))
end
what I want is to access the computation by g in the top level.
Currently, I can only do it by explicitly constructing computations in g
using constants (i.e. g2 and foo), while what I really wish is to access
results computed by g without knowing how they are computed (i.e. g1 and
foo'). Unfortunately, foo and foo' are not equivalent yet.
My whole idea is to compute something externally (in Isabelle/ML or even
a program written in C), and then verify and port the result back to the
top level. Of course, I can hard-code the whole computation in the top
level (with definition/fun/function) without proving anything, but I
feel it may not be necessary.
Again any suggestion is highly appreciated,
Wenda
Email Gateway (Aug 22 2022 at 11:09):From: Makarius <makarius@sketis.net>
The use of the word "top level" is very strange. Maybe you just mean the
material you can put into an Isabelle theory document, between the "theory
... begin" and "end". That language is called "Isabelle/Isar outer
syntax", but it merely means you can put arbitrary commands there that are
ultimately defined somewhere in Isabelle/ML. Command like 'definition' or
'theorem' are also defined as such -- this can be proven in Isabelle/jEdit
via C-hover-click on the keywords.
Since the 'ML' command is of the same kind, the easyiest answer to your
question is to use that to evaluate ML expressions in Isabelle/Isar
source. That gives you values in the ML environment.
I guess that your actual question is: "How do I get values produced in
Isabelle/ML into the Isabelle/HOL logic?" Since ML can control the logic,
but not the other way round, the standard approach is the use ML to set up
a logical statement (and prove it) on demand.
Here it is usually possible to split the problem into two parts: the
harder one to find a solution (outside the logic) and the easier one to
establish a desired property of it (within the logic).
You can also produce the ML code in creative ways, e.g. from HOL
specifications via the code generator.
Makarius
Email Gateway (Aug 22 2022 at 11:09):From: Wenda Li <wl302@cam.ac.uk>
Dear Makarius and code generation experts,
Thanks for pointing out my inaccuracies, it is always good to know ways
to polish my questions.
In terms of my question -- "How do I get values produced in Isabelle/ML
into the Isabelle/HOL logic?", my current try is through some code
generation setups. That is, to declare a function constant, and manually
link some ML code to it. Since this function constant is not associated
with any theorem, whatever code we are linking to it should not
introduce inconsistencies to the logic.
Here is what I have got so far,
theory Scratch4 imports
Main
begin
consts double ::"int ⇒ int"
code_printing code_module "Untrusted" ⇀ (SML)
{*structure Bar : sig
val double' : int -> int;
end = struct
fun double' n = n+n;
end
*}
code_printing constant double ⇀ (SML) "Bar.double'"
export_code double in SML module_name Foo
(*does not work because the native int type is different from the
generated int type *)
value [code] "double 3"
end
This is not work yet, as code_printing may not work the way I am using
it. I was wondering if it is possible to make my idea (i.e. declaring a
constant and manually linking some ML code to it) work?
Again any help is greatly appreciated,
Wenda
Email Gateway (Aug 22 2022 at 11:10):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Wenda,
Unfortunately, there is no good theory so far to back up code_printing. So whatever you do
with code_printing, you yourself have to convince yourself that what you are doing is sound.
I still have not found out what you want to achieve in the end. I will nevertheless try to
provide a few hints:
Suppose you (1) declare an unspecified constant foo with consts, (2) never define the
constant foo, and (3) set up code_printing for foo to some function foo' in SML. If (a)
foo' is referentially transparent (i.e., no side effects, no access to mutable state) and
(b) the return type of foo is not a code_abstype and (c) the argument types of foo have
not been refined during code generation, then you are pretty safe that Isabelle's logic is
still consistent. The reasoning goes as follows: If you do not define the constant, all
you know about the constant is its type. Thus, by refinement, you can replace it with any
referentially-transparent function during code generation. Referential transparency
ensures that two calls with the same arguments always return the same value. Thus,
evaluation cannot falsify equations like "foo 17 = foo 17". Due to the transformations in
the code generator, code_abstype return types are not safe by default. They are OK
provided that the function foo' returns only those values that satisfy the invariant I of
the abstract type. Otherwise, you could falsify the theorem "I (Rep_type (foo 17))". If
the argument types have been refined, your function has to ensure that it respects the
abstraction. For example, you could declare
to_list :: "'a set => 'a list"
and implement it in SML as
"fun to_list (Set.set xs) = xs"
Then, you could prove "to_list {1, 2} ~= to_list {2, 1}", which is obviously false as
{1,2} = {2,1} in HOL.
If any of these conditions are not satisfied, you yourself have to see whether
everything stays sound. In particular, as soon as you specify the constant foo somehow,
you have to be very careful. My AFP entry Native_Words is full of code_printing statements
for such cases, and I spent a lot of thought on making sure that I do not introduce
inconsistencies. As we do not have a formal model of code generation, only a certain level
of confidence can be provided (by inspection and testing), but never a rigorous proof.
From your previous mails, I had the impression that you wanted to compute results in
untrusted code and then use them back in HOL after checking their correctness. This is
possible with the above approach of declaring an unspecified constant, binding it to some
SML code (subject to the above restrictions), and checking the result. The code equation
could look as follows:
lemma [code]:
"bar x =
(let r = foo x
in if check x r then r else Code.abort (STR ''Error in result of foo'') (%_. bar x))"
If the check function imposes sufficiently many checks, you can prove this lemma without
knowing anything about foo.
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 11:10):From: Lars Hupel <hupel@in.tum.de>
Dear Wenda,
Many thanks for referring me to Lars Hupel' wonderful SPLICE technique!
It did seem quite relevant in my situation. However, it seems that the
SPLICE can only embed "static" code (I am not sure if my description is
accurate or not) in Isabelle/ML to the top level.
Your observation is accurate. I was meaning to reply to Andreas' mail, but
forgot.
what I want is to access the computation by g in the top level.
Currently, I can only do it by explicitly constructing computations in g
using constants (i.e. g2 and foo), while what I really wish is to access
results computed by g without knowing how they are computed (i.e. g1 and
foo'). Unfortunately, foo and foo' are not equivalent yet.
The short answer here is that what you want to do is impossible with
'SPLICE' or similar techniques. It is impossible to refer to dynamic ML
computations in the Isabelle term language. Imagine if it were possible:
For the example you've shown, that would also mean that the proof kernel
would need to be able to execute arbitrary ML functions in order to
perform reductions.
My whole idea is to compute something externally (in Isabelle/ML or even
a program written in C), and then verify and port the result back to the
top level. Of course, I can hard-code the whole computation in the top
level (with definition/fun/function) without proving anything, but I
feel it may not be necessary.
I'm not sure what you mean with "hard coding". There is no necessity to
write the Isar specification by hand. As Makarius pointed out, the general
technique is to not just write ML code which computes the values you are
interested in, but also ML code which "lifts" those values into the "logic
language". For example, you can write a piece of ML code which proves a
lemma or which specifies a function. (One could say that "ML is the
scripting language of Isabelle" -- although this is not entirely
accurate.)
However, this will still not allow you to prove results about dynamic ML
function executions. Defining your function in HOL and then using the code
generator is in my opinion the preferable way.
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:10):From: Wenda Li <wl302@cam.ac.uk>
Dear Andreas and Lars,
I am so grateful to have your feedback, from which I have learnt a lot.
And also I do apologize for any of my previous inaccuracies that caused
confusions.
- From your previous mails, I had the impression that you wanted to
compute results in untrusted code and then use them back in HOL after
checking their correctness. This is possible with the above approach
of declaring an unspecified constant, binding it to some SML code
(subject to the above restrictions), and checking the result. The code
equation could look as follows:lemma [code]:
"bar x =
(let r = foo x
in if check x r then r else Code.abort (STR ''Error in result of
foo'') (%_. bar x))"If the check function imposes sufficiently many checks, you can prove
this lemma without knowing anything about foo.
This is exactly what I want to achieve in the end! Suppose the check
function is strong enough, I can define foo in an arbitrary way and
still prove this lemma (i.e. "without knowing anything about foo"). One
way to implement foo is of course, as suggested by Lars, to define it
within the Isabelle/HOL logic: we can have something like:
fun foo x = ...
in the Isabelle/Isar source, and the code generator will do the job.
However, suppose the computation performed by foo is complicated and
there exists highly efficient external tools (e.g. Z3) that implement
foo, it might be more appealing to use (after checking) results returned
by external tools rather than re-implementing an almost-certainly-slower
foo in Isabelle/Isar (though we don't need to worry about the proofs).
This is possible with the above approach
of declaring an unspecified constant, binding it to some SML code
(subject to the above restrictions), and checking the result.
This is what I want to do in the first step. What I don't know is how to
do the "binding" step, and code_printing in my previous email is just
one attempt to achieve this.
For example, you could declare
to_list :: "'a set => 'a list"
and implement it in SML as
"fun to_list (Set.set xs) = xs"
Then, you could prove "to_list {1, 2} ~= to_list {2, 1}", which is
obviously false as {1,2} = {2,1} in HOL.
This example makes perfect sense to me now and it really didn't occur to
me before. Thanks for such a wonderful example!
Overall, the whole idea is just an exploration. If it really does not
work, I can go back to my original plan (i.e. the way Lars suggested).
Again any idea from the list is greatly appreciated,
Wenda
Email Gateway (Aug 22 2022 at 11:10):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Wenda,
On 17/08/15 15:46, Wenda Li wrote:
Dear Andreas and Lars,
I am so grateful to have your feedback, from which I have learnt a lot. And also I do
apologize for any of my previous inaccuracies that caused confusions.
- From your previous mails, I had the impression that you wanted to
compute results in untrusted code and then use them back in HOL after
checking their correctness. This is possible with the above approach
of declaring an unspecified constant, binding it to some SML code
(subject to the above restrictions), and checking the result. The code
equation could look as follows:lemma [code]:
"bar x =
(let r = foo x
in if check x r then r else Code.abort (STR ''Error in result of
foo'') (%_. bar x))"If the check function imposes sufficiently many checks, you can prove
this lemma without knowing anything about foo.This is exactly what I want to achieve in the end! Suppose the check function is strong
enough, I can define foo in an arbitrary way and still prove this lemma (i.e. "without
knowing anything about foo"). One way to implement foo is of course, as suggested by Lars,
to define it within the Isabelle/HOL logic: we can have something like:fun foo x = ...
in the Isabelle/Isar source, and the code generator will do the job. However, suppose the
computation performed by foo is complicated and there exists highly efficient external
tools (e.g. Z3) that implement foo, it might be more appealing to use (after checking)
results returned by external tools rather than re-implementing an almost-certainly-slower
foo in Isabelle/Isar (though we don't need to worry about the proofs).
If you define foo in HOL and generate the code for foo, there is not much point in using a
checker function. If you define foo in HOL and serialise it to some other hand-written ML
function, getting this right is actually more difficult than if there was no definition of
foo in HOL (because you additionally have to make sure that the HOL definition agrees with
the SML implementation). Having an undefined constant is fine.
This is what I want to do in the first step. What I don't know is how to do the "binding"
step, and code_printing in my previous email is just one attempt to achieve this.
I suggest that you have a look at the AFP entry Native_Word. It contains a lot of
non-trivial code printing examples, also in combination with integers. You might also want
to have a look at my TLS paper from last year's Isabelle workshop [1]. Section 4 discusses
the issues a bit. If you want to use types for exchanging data between generated code and
hand-written or library code, you have to use the types for data exchange. In
Isabelle/HOL, they are unit, bool, a * b, a + b, a option, integer and natural. I.e., you
should convert your "int"s to "integer" first. Again, lots of examples are in the
Native_Word entry.
Hope this helps,
Andreas
For example, you could declare
to_list :: "'a set => 'a list"
and implement it in SML as
"fun to_list (Set.set xs) = xs"
Then, you could prove "to_list {1, 2} ~= to_list {2, 1}", which is
obviously false as {1,2} = {2,1} in HOL.This example makes perfect sense to me now and it really didn't occur to me before. Thanks
for such a wonderful example!Overall, the whole idea is just an exploration. If it really does not work, I can go back
to my original plan (i.e. the way Lars suggested).Again any idea from the list is greatly appreciated,
Wenda
Email Gateway (Aug 22 2022 at 11:10):From: Wenda Li <wl302@cam.ac.uk>
Dear Andreas,
Many thanks for such a wonderful paper! The discussion about foreign
function interface in the paper is super useful to me. I finally got my
problem solved.
Wenda
Last updated: Apr 25 2024 at 20:15 UTC