Nges Brian (Oct 07 2024 at 17:52): Nges Brian (Oct 07 2024 at 17:52):In the past few days, I have read a few papers on Autocorres and I am excited about the tool and I want to use it in building my own C applications. At this point, I want to try it out but I am new to both Isabelle and Autocorres.
From the information I have gathered, Autocorres is a package used in Isabelle and to set it up,
I have taken the following steps:
1) Downloaded the Autocorres 1.10 package from https://github.com/seL4/l4v/releases ( autocorres-1.10.tar.gz ) which works with Isabelle2023.
2) I download Isabelle2023 for my system which is Ubuntu22.04 (intel x86_64) from https://isabelle.in.tum.de/website-Isabelle2023/installation.html and install it following the instructions which is basically unzipping using the command
tar -xzf Isabelle2023_linux.tar.gz
3) I then install Autocorres using the following command
L4V_ARCH=X64 Isabelle2023/bin/isabelle build -d . AutoCorres
4) Everything works as expected when I run the Autocorres Testsuites
L4V_ARCH=X64 Isabelle2023/bin/isabelle build -d . AutoCorresTest
5) I have created a folder (~/Documents/fv) under which I have placed autocorres1.10 and Isabelle2023 folders. I have also created a folder test_programs which contain a c file minmax.c which contains the min and max functions written in c.
6) To formally verify this c functions, I open up Isabelle2023 GUI from my fv folder using the command
Isabelle2023/Isabelle2023
7) I create a new file in my test_programs called minmax.thy which contains the following Isabelle code
theory minmax
imports AutoCorres
begin
external_file "./minmax.c"
install_C_file "./minmax.c"
autocorres [ts_rules = nondet] "minmax.c"
end
when I run this, I get the error:
Bad theory import "Draft.AutoCorres"
I do not know what I am missing in the setup process and I will be glad if I can get some help in setting this things up and using Autocorres to verify C programs.
Mathias Fleury (Oct 07 2024 at 18:40):Use the version in the AFP
Mathias Fleury (Oct 07 2024 at 18:41):(including the instructions how to install it!)
Nges Brian (Oct 07 2024 at 19:19):Mathias Fleury said:
AFP
Please can you help me with the link to it. ?
Kevin Kappelmann (Oct 07 2024 at 19:25):You can easily find it using any search engine of your choice (but just in case, here it is https://www.isa-afp.org/ )
Nges Brian (Oct 09 2024 at 00:07):Kevin Kappelmann said:
You can easily find it using any search engine of your choice (but just in case, here it is https://www.isa-afp.org/ )
Thank you
Nges Brian (Oct 11 2024 at 21:03):I am new to both Isabelle and Autocorres and I am trying to use Autocorres to prove the basic swap example in C following the guide provided by Autocorres.
my swap function is:
void swap(unsigned *a, unsigned *b) {
unsigned t = *a;
*a = *b;
*b = t;
}
and I have written a swap.thy in Isabelle2024 following the tutorial shown in the autocorres guide as
theory swap
imports
Main
"AutoCorres2.AutoCorres"
begin
(* Parse the input file. *)
install_C_file "swap.c"
autocorres [ts_rules =pure nondet] "swap.c"
(* Direct proof on the heap. *)
lemma
fixes a :: "word32 ptr" and b :: "word32 ptr"
shows
"⦃ λs. is_valid_w32 s a ∧ heap_w32 s a = x
∧ is_valid_w32 s b ∧ heap_w32 s b = y ⦄
swap' a b
⦃ λr s. heap_w32 s a = y ∧ heap_w32 s b = x ⦄!"
apply (unfold swap'_def)
apply wp
apply (auto simp: fun_upd_apply)
done
end
But I get the following errors when I try to verify this program in Isabelle.
1)
⦃ λr s. heap_w32 s a = y ∧ heap_w32 s b = x ⦄!" - Inner syntax error: unexpected end of input⌂
Failed to parse prop
2)
apply (unfold swap'_def) - Bad context for command "apply"⌂ -- using reset state
Please can someone help explain to me what the issue is and in both lines ?
irvin (Oct 12 2024 at 07:36):first one is that your ⦃ λr s. heap_w32 s a = y ∧ heap_w32 s b = x ⦄!" has a syntax error so its not written correctly.
irvin (Oct 12 2024 at 07:38):second one is a result of the first as it can't parse it so its ignored and then its become equiv to
(* Direct proof on the heap. *)
lemma
fixes a :: "word32 ptr" and b :: "word32 ptr"
apply (unfold swap'_def)
apply wp
apply (auto simp: fun_upd_apply)
done
irvin said:
first one is that your ⦃ λr s. heap_w32 s a = y ∧ heap_w32 s b = x ⦄!" has a syntax error so its not written correctly.
So you probably have to figure out the syntax. https://www.isa-afp.org/sessions/autocorres2_test/#Swap_Ex seems to show what you intend to do
irvin (Oct 12 2024 at 07:47):also https://www.isa-afp.org/browser_info/current/AFP/AutoCorres2/document.pdf seems to have a guide starting on page 1971 that should be updated. You probably should use that if you are currently using the old guide
Nges Brian (Oct 21 2024 at 18:39):irvin said:
irvin said:
first one is that your ⦃ λr s. heap_w32 s a = y ∧ heap_w32 s b = x ⦄!" has a syntax error so its not written correctly.
So you probably have to figure out the syntax. https://www.isa-afp.org/sessions/autocorres2_test/#Swap_Ex seems to show what you intend to do
Thank you Irvin, I tried your solution and I still get syntax errors on the lemma.
I will go through the documentation https://www.isa-afp.org/browser_info/current/AFP/AutoCorres2/document.pdf though it is a big document :). I am also using Isabelle2024. Is that compatible or I have to downgrade to 2023 or 2022?
lemma swap_lemma:
fixes a :: "word32 ptr" and b :: "word32 ptr"
apply (unfold swap'_def)
apply wp
apply (auto simp: fun_upd_apply)
done
```
```
Your theorem is missing a shows statement where you state what you are trying to prove
Mathias Fleury (Oct 21 2024 at 18:50):and no, the AFP version is not compatible with an old Isabelle version
Nges Brian (Oct 21 2024 at 19:30):Mathias Fleury said:
Your theorem is missing a
showsstatement where you state what you are trying to prove
thank you. Please can you recommend any tutorials/videos to quickly getup to speed with syntax and how to use Isabelle for beginners
Mathias Fleury (Oct 21 2024 at 19:31):the prog-prove (in Isabelle/jedit, open the documentation panel, or: https://isabelle.in.tum.de/doc/prog-prove.pdf)
irvin (Oct 22 2024 at 01:54):Nges Brian said:
irvin said:
irvin said:
first one is that your ⦃ λr s. heap_w32 s a = y ∧ heap_w32 s b = x ⦄!" has a syntax error so its not written correctly.
So you probably have to figure out the syntax. https://www.isa-afp.org/sessions/autocorres2_test/#Swap_Ex seems to show what you intend to do
Thank you Irvin, I tried your solution and I still get syntax errors on the lemma.
I will go through the documentation https://www.isa-afp.org/browser_info/current/AFP/AutoCorres2/document.pdf though it is a big document :). I am also using Isabelle2024. Is that compatible or I have to downgrade to 2023 or 2022?
lemma swap_lemma: fixes a :: "word32 ptr" and b :: "word32 ptr" apply (unfold swap'_def) apply wp apply (auto simp: fun_upd_apply) done ``` ``` ``````` The documentation is at the end go to page 1971. (*This formating is weird im not sure whats wrong*)
irvin (Oct 22 2024 at 01:56):Go to page 1971 for the documentation formatting seems to have failed on zulip
Mathias Fleury (Oct 22 2024 at 04:56):On page 1971 I see only theorem statement (thm) no theorem proof.
Mathias Fleury (Oct 22 2024 at 04:57):On page 1975 there is a theorem. It is written without shows but there is a theorem statement, which is what you do not have.
irvin (Oct 22 2024 at 05:03):I meant starting on pg 1971 there is the guide/document in https://www.isa-afp.org/browser_info/current/AFP/AutoCorres2/document.pdf and that the stuff before can be skipped reading first which is similar to this https://trustworthy.systems/projects/OLD/autocorres/quickstart.pdf
Mathias Fleury (Oct 22 2024 at 05:07):Once you know Isabelle, then yes starting with the guide is a good idea
Nges Brian (Oct 23 2024 at 00:04):Mathias Fleury said:
Once you know Isabelle, then yes starting with the guide is a good idea
THank you @Mathias Fleury and @irvin . I will go through Isabelle first.
Last updated: Dec 21 2024 at 16:20 UTC