arch-split: Requalify enhancements #788

Xaphiosis · 2024-07-11T03:34:50Z

Reviewers:🦆🦆🦆

Probably best to review this commit-by-commit (they don't overlap). The "asms -> assms" commit generates a bit of diff noise.

Otherwise, besides a sanity check of ML code, documentation and style, what I would like help with:

I added a bunch of documentation/examples to Requalify.thy
- not overly happy with exporting all those symbols to anyone who imports Requalify
- the arch section of the examples won't work unless L4V_ARCH is set
- should we move all this out to an example file?
- what do I do with the old examples? They are somewhat opaque for anyone trying to understand what's going on, but my examples don't thoroughly test an arch-split-like situation to ensure that the right constants/types/thms end up under the right names and proofs succeed
I have zero idea how I could detect a name collision when exporting into a locale, thoughts?
I'm not a fan of that collision resolution global. naming workaround, but I documented it anyway. I guess we'll always have situations where we do an interpretation of Arch inside a context and so name order matters?

The docs/arch-split needs an update for better practices, but I want to leave that for after I deploy some of this tech and see what the best practices actually are.

Xaphiosis · 2024-07-11T04:22:07Z

This addresses #777

lsf37 · 2024-07-11T04:49:43Z

I added a bunch of documentation/examples to Requalify.thy

not overly happy with exporting all those symbols to anyone who imports Requalify

The examples are good, but it'd be nice to avoid the name space pollution, yes. Does experiment begin .. end help anything? If not, moving the examples to a separate test file is probably what we should do.

the arch section of the examples won't work unless L4V_ARCH is set

That's fine from my side. I think we can assume that L4V_ARCH is always set when we run these theories.

should we move all this out to an example file?

If experiment doesn't work here, then I would say yes.

what do I do with the old examples? They are somewhat opaque for anyone trying to understand what's going on, but my examples don't thoroughly test an arch-split-like situation to ensure that the right constants/types/thms end up under the right names and proofs succeed

Happy to leave them in for now. We can improve them some other time if we feel like it.

I have zero idea how I could detect a name collision when exporting into a locale, thoughts?

None currently. Can you elaborate on which technical bits we are missing?

I'm not a fan of that collision resolution global. naming workaround, but I documented it anyway. I guess we'll always have situations where we do an interpretation of Arch inside a context and so name order matters?

We do have some few of these global. constants, but not a lot. For the few times we're using it, I think the mechanism is fine, and it's good that it is now properly documented, because I had not actually understood how we achieve that.

The docs/arch-split needs an update for better practices, but I want to leave that for after I deploy some of this tech and see what the best practices actually are.

👍

Xaphiosis · 2024-07-11T09:13:51Z

should we move all this out to an example file?

If experiment doesn't work here, then I would say yes.

locale and context can't be used inside experiment, so I guess I'll move it.

I have zero idea how I could detect a name collision when exporting into a locale, thoughts?

None currently. Can you elaborate on which technical bits we are missing?

You'd have to take a look at the ML code for more context, and the bit in the examples where it says there is currently no warning on name collisions into locales.

First, the results of Parse.opt_target is something we hand to Toplevel.local_theory. If it's NONE, great, we can check the base name against a lookup in the global theory. If it isn't NONE though, we get an xstring * Position.T, i.e. the locale's parsed name (e.g. Requalify_Example2). I don't know how to go from a locale name in a string to somehing I can search in.

Second, there is a worse issue. Say you have this:

locale Arch

context Arch begin
  lemma aaa: "2 = (2 :: nat)" by simp
end

context Arch begin global_naming AARCH64
  lemma aaa: "1 = (1 :: nat)" by simp
end

thm Arch.aaa (* 2 = 2 *)
thm AARCH64.aaa (* 1 = 1 *)

locale Moo
requalify_facts (in Moo) AARCH64.aaa (* this is fine *)
thm Moo.aaa (* 1 = 1 *)
requalify_facts (in Moo) Arch.aaa (* this is not fine, we'd like a warning, Moo already has aaa *)
thm Moo.aaa (* 2 = 2 *)

and then the total disaster area, which is where I don't even know what to do, and sadly this might come up in arch-split:

(* dump AARCH64.aaa into Arch locale now, note how we don't have to specify AARCH64 *)
requalify_facts (in Arch) aaa (* no warning, no qualification needed either! *)
thm Arch.aaa (* 1 = 1 *)
requalify_facts (in Arch) Arch.aaa (* still no warning, but I guess we'd want one *)
thm Arch.aaa (* 1 = 1 *)
requalify_facts (in Arch) aaa (* still no warning, but we definitely want one *)
thm Arch.aaa (* 1 = 1 *)

Do you see the problem? In the Moo case you can check if it's already there, but in the Arch case it is already there, as witnessed by being able to pull AARCH64.aaa without the qualification. The above example has another Arch.aaa that is additionally there, confusing things further.

Xaphiosis · 2024-07-11T09:30:10Z

Moved Requalify tests into lib/test/Requalify_Test.thy and rebased

lsf37 · 2024-07-16T07:07:56Z

First, the results of Parse.opt_target is something we hand to Toplevel.local_theory. If it's NONE, great, we can check the base name against a lookup in the global theory. If it isn't NONE though, we get an xstring * Position.T, i.e. the locale's parsed name (e.g. Requalify_Example2). I don't know how to go from a locale name in a string to somehing I can search in.

It's been a very long time since I did anything with this (usually you get the local_theory from the top-level command), but if b is your xstring * Position.T, then Target_Context.context_begin_named_cmd [] b : theory -> local_theory looks like it might fit the bill. At least it is also used by context b begin .. end.

Second, there is a worse issue. Say you have this:
locale Arch

context Arch begin
  lemma aaa: "2 = (2 :: nat)" by simp
end

context Arch begin global_naming AARCH64
  lemma aaa: "1 = (1 :: nat)" by simp
end

thm Arch.aaa (* 2 = 2 *)
thm AARCH64.aaa (* 1 = 1 *)

locale Moo
requalify_facts (in Moo) AARCH64.aaa (* this is fine *)
thm Moo.aaa (* 1 = 1 *)
requalify_facts (in Moo) Arch.aaa (* this is not fine, we'd like a warning, Moo already has aaa *)
thm Moo.aaa (* 2 = 2 *)
and then the total disaster area, which is where I don't even know what to do, and sadly this might come up in arch-split:
(* dump AARCH64.aaa into Arch locale now, note how we don't have to specify AARCH64 *)
requalify_facts (in Arch) aaa (* no warning, no qualification needed either! *)
thm Arch.aaa (* 1 = 1 *)
requalify_facts (in Arch) Arch.aaa (* still no warning, but I guess we'd want one *)
thm Arch.aaa (* 1 = 1 *)
requalify_facts (in Arch) aaa (* still no warning, but we definitely want one *)
thm Arch.aaa (* 1 = 1 *)
Do you see the problem? In the Moo case you can check if it's already there, but in the Arch case it is already there, as witnessed by being able to pull AARCH64.aaa without the qualification. The above example has another Arch.aaa that is additionally there, confusing things further.

I don't have any immediate solutions for these, but given that we had no warnings at all before, it's not catastrophic if we start small and improve these over time.

corlewis

Very nice, especially with how generic you have managed to make it with so much code reuse. Thank you for the comments and examples, they are very helpful.

I haven't thought of anything so far that could help with the naming collisions in locales, but I agree with @lsf37 that this is already such a big improvement that it can be left for later.

corlewis · 2024-07-18T02:24:37Z

lib/Requalify.thy

+(* Locate global fact matching supplied name.
+   When we specify a fact name that resolves to a global name, return the normal fact lookup result.
+   Note: Locale_Name.fact_name outside the locale resolves to a global name.
+
+   When we are inside a locale, the lookup is more interesting. Supplying "short_name" will result
+   in "local.short_name", which we then need to match to some name in the global context. We do
+   this by going through *all* the fact names in the current context, searching for matches
+   of the form "X.Y.short_name", where we hope X is some theory, and Y is some locale.

+   Since "X.Y.short_name" is not sufficiently unique, we must also check that the theorems under
+   the discovered name match the ones under "local.short_name". *)


Thank you for this very helpful comment (and for all the other comments you've added).

corlewis · 2024-07-18T02:42:31Z

lib/Requalify.thy

-    >> (fn (target,bs) =>
-      Toplevel.local_theory NONE target (fn lthy =>
-      let
+(* ([aliasing][,] [A|H]) in that order *)


Out of curiosity, why do you want to fix that order? I think it would be slightly easier to implement and probably not need the split between generic_options and arch_options if you didn't.

This is because of n+1-flavour soup. If I allow both, we will see someone in the future discovering that they can write (H, aliasing) while everyone else writes it the other way around. I'm fine to change that order, but for some reason I got it stuck into my head that I only want one. What do you think?

I'm easy. Fixing it to one order does reduce the number of styles, but it also can be frustrating to use if you don't remember what order it should be and are only getting the typical Isabelle "bad syntax" error message.

Would it make sense to try to give an informative error message when the order is wrong?

I'll be honest, I do not know how one does that.

I have never tried this in Isabelle, but usually you'd explicitly parse the wrong order and then produce an error message (I guess throw an exception with a useful message?)

I can give this a go later I guess.

The "list of options" thing is also weird to me. I mean, someone could do (A, aliasing, H) if it's a list, so the error checking becomes more complex.

Or even worse: (A, H, aliasing, A, A, H, A) ...

If we don't care about order, then it's a case of sort|uniq and then error if it's both A and H, but if we care about order I'd need to check for duplicates... I am not getting a clear image of good interface here.

I think we'll leave this for another time. Have to redirect resources to arch-splitting.

lib/Requalify.thy

i.e. 's/AI_asms/AI_assms/g' and same for Pre_asms ("asms" is rarely expected outside of ML code) Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

* add warnings when exporting a name that already exists in theory context, suppressable by `(aliasing)` option * add `arch` variants of requalify commands that implicitly add the value of L4V_ARCH before whatever you give them, with optional suffixes for abstract (A) and Haskell (H) spec global naming. * write hopefully-understandable documentation with commented examples Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Also document that requalify commands will issue warnings. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Stops namespace pollution, allows us to use Arch locale as example. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Xaphiosis added enhancement proof engineering nicer, shorter, more maintainable etc proofs labels Jul 11, 2024

Xaphiosis requested review from lsf37 and corlewis July 11, 2024 03:34

Xaphiosis mentioned this pull request Jul 11, 2024

Faster requalify command for arch-split (arch_requalify_*?) #777

Closed

Xaphiosis force-pushed the arch_split branch from 8386cb8 to ac23c1d Compare July 11, 2024 09:56

Xaphiosis mentioned this pull request Jul 11, 2024

[WIP] Opinionated deployment of enhanced Requalify capabilities on AInvs #791

Closed

5 tasks

lsf37 approved these changes Jul 17, 2024

View reviewed changes

corlewis approved these changes Jul 18, 2024

View reviewed changes

Xaphiosis force-pushed the arch_split branch from b1f331a to 14a8536 Compare July 23, 2024 02:52

Xaphiosis added 4 commits July 23, 2024 13:22

ainvs: use "assms" in name for arch locales

647fa12

i.e. 's/AI_asms/AI_assms/g' and same for Pre_asms ("asms" is rarely expected outside of ML code) Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

docs: arch-split: requalifying into Arch locale

e1ff464

Also document that requalify commands will issue warnings. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

lib: migrate Requalify tests into test/

705a73b

Stops namespace pollution, allows us to use Arch locale as example. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Xaphiosis force-pushed the arch_split branch from 14a8536 to 705a73b Compare July 23, 2024 03:25

Xaphiosis merged commit bc948e3 into seL4:master Jul 23, 2024
12 of 14 checks passed

Xaphiosis deleted the arch_split branch July 23, 2024 06:47

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

arch-split: Requalify enhancements #788

arch-split: Requalify enhancements #788

Xaphiosis commented Jul 11, 2024

Xaphiosis commented Jul 11, 2024

lsf37 commented Jul 11, 2024

Xaphiosis commented Jul 11, 2024

Xaphiosis commented Jul 11, 2024 •

edited

Loading

lsf37 commented Jul 16, 2024

corlewis left a comment

corlewis Jul 18, 2024

corlewis Jul 18, 2024

Xaphiosis Jul 22, 2024

lsf37 Jul 22, 2024

Xaphiosis Jul 22, 2024

lsf37 Jul 23, 2024 •

edited

Loading

Xaphiosis Jul 23, 2024

Xaphiosis Jul 23, 2024

Xaphiosis Jul 23, 2024

Xaphiosis Jul 23, 2024

Xaphiosis Jul 23, 2024

arch-split: Requalify enhancements #788

arch-split: Requalify enhancements #788

Conversation

Xaphiosis commented Jul 11, 2024

Reviewers:🦆🦆🦆

Xaphiosis commented Jul 11, 2024

lsf37 commented Jul 11, 2024

Xaphiosis commented Jul 11, 2024

Xaphiosis commented Jul 11, 2024 • edited Loading

lsf37 commented Jul 16, 2024

corlewis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lsf37 Jul 23, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Xaphiosis commented Jul 11, 2024 •

edited

Loading

lsf37 Jul 23, 2024 •

edited

Loading