Obtaining the old Hoare triple from the new

[didriklundberg]

I added new theorems and definitions to obtain an AssumptionViolated-free Hoare triple from the regular one, provided the program contains no Assume statements. Also, corrected typo in exec_to_labels HT.

The terminology is a little rough around the edges. I will likely make some clean-up commit that renames and moves some lemmata around, and makes the proofs nicer. Please provide feedback so that everything can be sorted out in one go.

I am also working on a proof procedure to obtain the result of an Assume-free BIR program (the definitions should be very straightforward to use, however).

EDIT: Added commit to resolve #53.

[totorigolo]

I'm just commenting because I want to let @andreaslindner review, since it's his tool :)

Some points:

• Why did you create a new theory about Hoare triple, instead of adding these theorems in bir_wpTheory?
• Why did you add those TODOs instead of putting the theorems directly where they should be?

Otherwise, that looks really useful 👍

[andreaslindner]

I'm just commenting because I want to let @andreaslindner review, since it's his tool :)

Thanks for thinking about me, but we're working all together on this :)

[totorigolo]

I'm just commenting because I want to let @andreaslindner review, since it's his tool :)

Thanks for thinking about me, but we're working all together on this :)

It's also because I'm not really used to writing proofs, so I think that you review is way more valuable ;)

[didriklundberg]

* Why did you create a new theory about Hoare triple, instead of adding these theorems in `bir_wpTheory`?

Because bir_wpScript.sml is already of humongous size. I like to maintain some degree of modularity and not keep all theorems in a single file. But of course, this subdivision can always be more precise. The intent of bir_htTheory is to contain HT manipulation theorems not directly related to the WP propagation mechanisms.

* Why did you add those `TODO`s instead of putting the theorems directly where they should be?

Not really for any strong reason, but I figured I could just as well receive comments first. I don't want to clutter existing theories with new theorems without making sure they go in the right place. Some of these theorems contain comments on where I intend to put them (so that we don't mess up commit history by moving them back and forth at PR review). So if @andreaslindner doesn't have any strong opinions I will just spread them out myself in a new commit.

[totorigolo]

Btw, I focused on style and readability for a HolBA user in my review. Please ask if you have a specific question/concern :)

[totorigolo]

I'm happy with the code now 🙂 Sorry for this lengthy review ^^'

EDIT: I leave you decide if you want to wait for Andreas' review :)

[andreaslindner]

The intent of bir_htTheory is to contain HT manipulation theorems not directly related to the WP propagation mechanisms.

I thought the same when I saw this pull request the first time. It makes totally sense to divide hoare triples from wp. One is the formalization of pre and post-conditions and the other is a mechanism making use of the formalizations.

Summing up: I like this idea.

[andreaslindner]

Looks good! After fixing the issue that Thomas pointed out and maybe changing the definition like I suggested if you like, you can merge it from my perspective. Or add more first if you want to add more of course

[andreaslindner]

Oh, maybe a little test script for the new library could be useful.

[andreaslindner]

Looks still good.

[didriklundberg]

Oh, maybe a little test script for the new library could be useful.

I'll see if I can get time to fix that later today. Otherwise I'll just rebase and merge and do it in a later PR. :)

[andreaslindner]

That's a funny one :)