Email Gateway (Aug 18 2022 at 13:56): Email Gateway (Aug 18 2022 at 13:56):From: Sigurd Torkel Meldgaard <stm@cs.au.dk>
I am trying to use Isabelle as a part of a verification tool (for
crypto multi-party protocols).
The basic idea is that my analysis tool reads a source file, and
outputs a proof burden in Isabelle (using the Simpl library).
Now it should be possible to write a proof, and have that checked
before the program runs.
What is the best way to call Isabelle from the command-line and have a
binary result (proof verified or not)?
Are there any projects with a similar structure that I could learn from?
Thanks
Sigurd Meldgaard
Email Gateway (Aug 18 2022 at 13:56):From: Christian Sternagel <Christian.Sternagel@uibk.ac.at>
A different way of doing that would be the following:
1) formalize a function (let's call it 'cert') within Isabelle, that reads some
representation your prove burdon (in our project we use XML) and returns True
of False.
2) prove the lemmas 'cert input = True' implies a positive answer and 'cert
input = False' implies a negative answer
3) Use Isabelle's code-generator to get a program that uses the function 'cert'
on it's input.
cheers
christian
We used this workflow in http://cl-informatik.uibk.ac.at/software/ceta
Quoting Sigurd Torkel Meldgaard <stm@cs.au.dk>:
Christian Sternagel
Email Gateway (Aug 18 2022 at 13:56):From: Alexander Krauss <krauss@in.tum.de>
Christian Sternagel wrote:
A different way of doing that would be the following:
1) formalize a function (let's call it 'cert') within Isabelle, that reads some
representation your prove burdon (in our project we use XML) and returns True
of False.
If I understood Sigurd correctly, he meant that the Isabelle proof
should be an interactive one, read from some theory file. Is that right?
Quoting Sigurd Torkel Meldgaard <stm@cs.au.dk>:
What is the best way to call Isabelle from the command-line and have a
binary result (proof verified or not)?
The usual way to run proofs in batch-mode is "isabelle usedir". You can
get a basic setup by following the instructions for setting up document
preparation in the tutorial. But instead of the latex document, you
would just be interested in the result, which you can read from the
return code of the "isabelle usedir" or "isabelle make" invocation.
However, the problem is that you must also make sure that the theory
really proves the statement that you are interested in... an empty
theory will always be checked without errors...
Alex
Email Gateway (Aug 18 2022 at 13:56):From: Sigurd Torkel Meldgaard <stm@cs.au.dk>
A different way of doing that would be the following:
Thank you for the advice, it seems to be not quite what I want - but
an interesting project you have going - thanks for the link
If I understood Sigurd correctly, he meant that the Isabelle proof should be
an interactive one, read from some theory file. Is that right?
Yes, that was something more in that direction that I thought about.
The usual way to run proofs in batch-mode is "isabelle usedir". You can get
a basic setup by following the instructions for setting up document
preparation in the tutorial. But instead of the latex document, you would
just be interested in the result, which you can read from the return code of
the "isabelle usedir" or "isabelle make" invocation.However, the problem is that you must also make sure that the theory really
proves the statement that you are interested in... an empty theory will
always be checked without errors...
Oh yes - this is gonna be a problem - I will need a way to force it to
be a proof of a certain statement ...
One could concatenate the statement with the supposed proof before
feeding it to Isabelle, but it seems inelegant, and not very robust.
Would it be possible to script isabelle to do this via the ML-interface?
Maybe I just need to leave it up to the user to not change the
statement before he prove it ... that is not really what I want
though.
Thanks for the help
Sigurd
Email Gateway (Aug 18 2022 at 13:56):From: Alexander Krauss <krauss@in.tum.de>
Hi Sigurd,
However, the problem is that you must also make sure that the theory really
proves the statement that you are interested in... an empty theory will
always be checked without errors...Oh yes - this is gonna be a problem - I will need a way to force it to
be a proof of a certain statement ...
One could concatenate the statement with the supposed proof before
feeding it to Isabelle, but it seems inelegant, and not very robust.
...and does not work:
lemma main_thm: "very hard to prove"
(* end of proof obligation *)
(* start of "proof" *)
oops
lemma main_thm: "True"
by simp
Would it be possible to script isabelle to do this via the ML-interface?
Yes. In ML you can do pretty much everything.
Alex
Email Gateway (Aug 18 2022 at 13:57):From: Sigurd Torkel Meldgaard <stm@cs.au.dk>
Hi again
I have dived into the ML of Isabelle, and I think that I have made
something that works, but would love your comments.
The idea is that the user supplies the proof of the wanted theorem in
Proof.thy, and that is imported into TestProofExists.thy that will
search for a proof of the wanted theorem using the FindTheorems.Solves
mechanism, and exit Isabelle with the proper exit code.
Does it sound sound?
Here is code checking that rev_rev_ident (or something like it) is
actually proved somewhere:
theory TestProofExists
imports Main
begin
ML {*
case FindTheorems.find_theorems
(ProofContext.init @{theory})
(SOME (Goal.init @{cterm "True ⟹ rev (rev xs) = xs"}))
(NONE)
(true)
[(true, FindTheorems.Solves)]
of (NONE, _) => exit 127 (* Should never happen, as we remove duplicates *)
| (SOME 0, _) => exit 1 (* Nothing was found *)
| (SOME _, _) => exit 0 (* One ore more theorems can prove the statement! *)
*}
end
What is the general way of turning a general term like "rev (rev xs) =
xs" into a proposition that Goal.init accepts like "True ==> rev (rev
xs) = xs"?
Email Gateway (Aug 18 2022 at 13:57):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Sigurd,
as far as I see the problem of "rev (rev xs) = xs" is that it is parsed
as type bool whereas a proposition must have type prop; for this sake
the judgement Trueprop :: bool => prop must be inserted (which is
typically not printed explicitly). The easiest way to achieve this is
to use the prop/cprop antiquotation instead of term/cterm.
Hope this helps
Florian
signature.asc
Last updated: Apr 26 2024 at 16:20 UTC