refine: improve typ_at_lifts and add typ_at_props' locale

[corlewis]

These changes are based on ones that were previously made in the rt branch. Some additional cleanup was done along the way and the typ_at_props' locale was arch-split and applied to all architectures.

The main benefit for master is the improved typ_at_lifts lemmas; the typ_at_props' locales themselves are not as immediately useful as in rt. However, backporting them does make the two branches more similar and should ease future merges.

See the following commits for where some of these changes originally happened in the rt branch:
6710b9a
64b6edf
79e2e2b
91a2023
78bb847
8a01dd4
336bd0b

[corlewis]

This fixes was a pain but is necessary to be able to make this interface. The alternative would be to move all of these gen constructions to InvariantUpdates_H, after ArchInvsLemmas_H and where the needed arch lemmas could be requalified.

The parameter is generally resolved once the typ_at_gen locale is interpreted in ArchInvsLemmas_H, but the downside is that it appears in all future interpretations of the gen_typ_at_props locale as a parameter that can be ignored.

[corlewis]

See https://github.com/seL4/l4v/pull/1006/changes#diff-1e2b2cf051529198334e7ad45c0bebf1785e31a833e15cb37429a0610a6d82c0R1337 for an example of what I mean by the parameter appearing as something that can be ignored. Adding the _ is very easy if you know about it or are copying an existing interpretation but could be confusing otherwise.

[lsf37]

We might need a longer comment somewhere central that explains how to use the infrastructure (then this bit could go there). It's fairly clear now while we're focussing on it, but I can well imagine being confused later what sublocale I need to do when and which methods I should be using.

(the usual name for the kernel ext type would be z -- any particular reason you didn't pick that one?)

[Xaphiosis]

I don't think this is the kernel ext type, the 'kernel' here is a monad?

These assumptions appear to be saying:
"given a monadic function with a return value of 'b, assume that you can do a typ_at' lift over valid_arch_tcb' (strong version, for some reason) and valid_arch_cap' (weak version, for some reason)"

Then for every function you want the typ_at' lifting tech for, you have to instantiate this locale via interpretation?
Also, why these specific assumptions?

[Xaphiosis]

What I'm also not understanding is how you'd get rid of the type parameter by moving things to InvariantUpdates_H. I'd've thought if you instantiate with a function, it would fill in the type parameter, so you would still need it, but maybe not 'b itself?

[corlewis]

Sorry for the confusion, hopefully the new commit structure and big comment in this PR makes it a bit easier to understand.

This locale is the arch-split interface for the following typ_at_lifts lemmas. The assumptions are the arch-specific typ_at_lift lemmas that hold for all architectures and are needed to prove the generic ones.

Once the locale is interpreted in ArchInvsLemmas_H then we never need to think about it again, like with other arch-split interface locales.

[corlewis]

(the usual name for the kernel ext type would be z -- any particular reason you didn't pick that one?)

I don't think this is the kernel ext type, the 'kernel' here is a monad?

@Xaphiosis is right, this is the free return type of the monads in the interface lemmas, not the kernel ext type. I fix it so that the generic lemmas in this locale can have the same type and make use of the interface lemmas.

However, it should maybe be 'a. I think I only went with 'b because 'a was already used by something else in the goal when I was first working out what the problem was and how I could solve it.

[corlewis]

What I'm also not understanding is how you'd get rid of the type parameter by moving things to InvariantUpdates_H. I'd've thought if you instantiate with a function, it would fill in the type parameter, so you would still need it, but maybe not 'b itself?

I think your confusion here is due to mixing up this locale with the later one which gets instantiated with a function. In this case, what I was referring to is that instead of introducing this locale as an interface in Invariants_H, we could move the generic lemmas that depend on the arch-specific ones to InvariantUpdates_H, where those arch-specific lemmas could just be requalified.

[lsf37]

The comment and the code are currently duplicated for the architectures. If we give gen_typ_at_lifts_strong as a parameter, the code as such could be generic in a separate theory file somewhere, together with the long comment, which we could then point to here.

[Xaphiosis]

Yeah, I think I commented the same. Definitely would be good to de-duplicate the comment and tech.

[corlewis]

I've done this now, the comment and ML function are in the generic Invariants_H and pointed at from each ArchInvsLemmas_H file.

[lsf37]

after looking at many of these, I'm starting to wonder if it would be worth adding a little ML command that only needs the constant name (or list of names) and does the rest. So that we could write

typ_at_props doMachineOp, setEndpoint

and it figures out parameters etc itself. Not for this PR, but could be a follow-up if we like the idea.

[Xaphiosis]

it would be convenient to use, but then we'd end up with the param_a and param_b that crunch does... then again this is a bit like crunching, so would be worth investigating at some point

[corlewis]

Yeah, while going through all of the files and doing these I definitely had the feeling that a command like that would be useful. @Xaphiosis is right though, it was annoying to have to work out sensible parameters for each function but it does end up with much nicer lemmas than crunch ones with param_a and param_b.

[lsf37]

uses a different style to the rest. Should we one-line all of them?

[Xaphiosis]

I'd say given how many there are, one-lining if it fits on one line is something I'd support

[corlewis]

A lot of these were being copied across from the rt branch but yeah, I noticed all the different styles. At the time I thought it was better to be consistent with rt to make merges easier but now I'm not sure if we should just pick a style now and deal with the merge the one time.

[lsf37]

(different style here as well)

[lsf37]

Thanks for doing that. The setup/instantiating is a bit more verbose, but proofs all become simpler. I think this is good. We might try to simplify making instances at some point, but I don't think we need to do that immediately.

One thing we should add is documentation. With the locale and arch split this has become complex enough that it should be explained somewhere in a reasonably central/findable location (what it does, why it exists, how to extend properties, when to do which kind of sublocale).

[Xaphiosis]

I'm a bit lost here. Firstly, I'm wondering why this tech has to be duplicated across all the arches, along with the big comment, etc.
Second, I'm wondering, the deployment here only works once, right, to make the weaker form from the strong? So if someone wants to add more, they have to add both a strong and a weak? How does that work?

[corlewis]

Second, I'm wondering, the deployment here only works once, right, to make the weaker form from the strong? So if someone wants to add more, they have to add both a strong and a weak? How does that work?

Yes, this only works once, to make the weaker form of the specific 'strong' lemmas that were introduced here.

I'm not quite sure what you mean with the second half. If someone has new 'strong' lemmas then they could add them here easily by proving them and then adding them to typ_at_lifts_strong. If they proved them in a later file for whatever reason then they could still add them to the typ_at_props' locale, and construct the weaker version as well if needed.

[Xaphiosis]

small comment, or add a docstring?

[Xaphiosis]

(there's no such thing as a truly private method, they seem to leak when you do print_methods)

[corlewis]

This was taken directly from rt. I guess I could try to come up with a comment, I think it's just wrapping up the duplicated proofs for the following typ_ats' lemmas into something that can be used for all of them.

[corlewis]

(there's no such thing as a truly private method, they seem to leak when you do print_methods)

And yeah, I guess still useful though as an indication that it's not intended for general use.

[Xaphiosis]

why do all these proofs appear so much nicer than the Arch proofs that seem to go via bool_to_bool_cases? am I not comparing the right kinds of proofs?

[corlewis]

The proofs with bool_to_bool_cases are all lemmas I made into 'strong' versions. For these lemmas I was either unable to or didn't think to make 'strong', and the proofs could stay simpler.

[Xaphiosis]

end tags please. also, consistency, in some files you have empty lines in between, in others they run into each other

Also: while context Arch is cheaper than interpretation Arch ., it's still not free; any chance these could go into an Arch block above?

[corlewis]

Also: while context Arch is cheaper than interpretation Arch ., it's still not free; any chance these could go into an Arch block above?

Hmm, I have conflicted opinions here. I agree that moving them into an already existing Arch block would be much nicer, but doing that would almost definitely result in them being duplicated when this is merged into the rt branch.

[corlewis]

Ah, actually in this case I put them here because they need to go after the interpretation of CNodeInv_R. I don't see an easy way around this.

[Xaphiosis]

out of curiosity, how fast does a block like this run?
(also this is an example of no empty lines between)

clarification question: with sublocale in Arch here, you're saying that you only want the lift rules to be visible in Arch? that doesn't feel right for all of these

[corlewis]

out of curiosity, how fast does a block like this run? (also this is an example of no empty lines between)

These interpretations and sublocales are practically instant, they're below the threshold of my timing panel.

clarification question: with sublocale in Arch here, you're saying that you only want the lift rules to be visible in Arch? that doesn't feel right for all of these

This is the larger locale that contains both generic and arch-specific lifted rules, and so can only be visible from Arch. There is normally an equivalent generic interpretation that contains only the generic rules and is visible globally. This approach follows my understanding of how typ_at_lifts was previously arch-split and handled.

[Xaphiosis]

another reminder to incorporate end tags into repertoire

[Xaphiosis]

This is why end tags are important, in the diff I have no idea what context the next sublocale commands are in.

[corlewis]

This is in a file that hasn't been arch-split yet, so the context being ended is an anonymous one where we do context begin interpretation Arch. I'm not sure what end tag would be appropriate for that.

Once it is arch-split the context will almost definitely no longer be there, and these sublocale commands will be able to be replaced with global interpretations.

[Xaphiosis]

Looking at this, and the fact this will probably hit before I get to Syscall arch-split (and maybe some others, I dunno), how does one go about arch-splitting these?

Also, sublocale Arch is something I try to avoid because it is slow. A whole block of them feels like it will be very slow. Can you let me know how long this runs for? Will the sublocale Arch go away as part of arch-splitting? This is new to me.

[corlewis]

When these later files get arch-split my expectation is that in the generic file these cases will be replaced with a global_interpretation of the gen_typ_at_props' locale. We would then make the larger typ_at_props' a sublocale of Arch in the arch files. Again, I think this is basically the same as what would have been needed to arch-split the previous typ_at_lifts lemmas commands. I've also tried to mark each case of these with a FIXME: arch-split which will hopefully help.

The current sublocale Arch commands are a bit slow, but once these files are arch-split then the equivalents will almost definitely already be in Arch and so could just look like sublocale handleFault: typ_at_props' "handleFault t ex", which is quick.

[corlewis]

When I rebase this PR I'm also going to have to go through this exact process for Tcb_R, so that will be a good test case to confirm that it makes sense.

[corlewis]

Having now rebased and done this for Tcb_R, I can confirm that the above process is correct and is relatively straightforward.

One note for the future though, I impressively already forgot about the locale type parameter and it meaning that interpreting gen_typ_at_props' needs a _, which led to a very confusing failure. I'm not sure what to do about this, beyond adding a comment to the definition of gen_typ_at_props' for anyone who clicks through to there.

[lsf37]

A comment at whatever place you get to when you click though would be fairly helpful, I think. The other discovery mechanism would be grep, so it would be good if it mentioned gen_typ_at_props' somewhere.

[Xaphiosis]

Yeah, this is definitely confusing to see without the context of this particular PR.
See previous comments about whether we are sure we need the itself parameter. Maybe you should walk us through it... some things appear unintuitive, but have no alternative.

[corlewis]

Thank you for the reviews and sorry for the delayed response, the comments led me to think of an improved way to structure and describe these changes. In particular, I've changed the commits to better reflect that there are two relatively separate changes going on here, both based on changes that have been made in the rt branch.

The first is improving and arch-splitting the typ_at_lift lemmas themselves. This involved doing a better job of centralising all of the relevant lemmas in one location, along with making some of the lemmas into 'strong' versions, which hold for any P. For technical reasons, which have an earlier attempt at an explanation in the big comment above the ML_goal, we additionally want slightly weaker versions of those 'strong' lemmas. An interface locale is also added to make it possible to prove the generic lemmas in the generic Invariants_H file. This is a relatively standard arch-split interface locale, with a slight complication to handle a free type variable in the lemmas being interfaced.

The second half of the changes is the addition and arch-split of the typ_at_props' locale. In the master branch this locale isn't actually that useful, it mostly just lets us interpret it for a given function to get the lifted typ_at lemmas, instead of doing commands like lemmas archThreadSet_typ_ats[wp] = typ_at_lifts[OF archThreadSet_typ_at']. In the rt branch where it was first developed, it is more useful to handle there being multiple sets of lemmas depending on whether they also depend on sc_at' being preserved.

The way this locale has been arch-split follows how the typ_at_lifts lemmas had previously been arch-split, there is a generic version containing only the generic lemmas and then arch-specific versions containing the total set, both arch-specific and generic lemmas. The generic locale can then be globally interpreted in generic files and the arch-specific locale is interpreted as a sublocale of Arch. Similarly to before with the typ_at_lifts lemmas, generic functions often have both a global interpretation in a generic file and an arch-specific one in the equivalent arch file.

[corlewis]

This is now ready for re-review. I think I've resolved all suggestions that were made in both our online and offline discussions. Once we're happy with this state of it I'll squash, rebase, and update the remaining files that have since been arch-split.

[corlewis]

I tried turning this thm into a lemmas _ = ... but it pollutes the namespace and led to confusing find_theorems results, so I changed it back to thm.

[Xaphiosis]

Ah, thanks for trying it out anyway.

[corlewis]

Once we're happy with this state of it I'll squash, rebase, and update the remaining files that have since been arch-split.

Proof failures are expected in the current state, CRefine won't work until that rebase happens.

[Xaphiosis]

shouldn't this be indented to the same level as fixes below?

[Xaphiosis]

do we care to say that rvt is the return type of f?

[corlewis]

Both good points, indenting it like that would make it extra clear what the comment is referring to and it's always nice to have a hint about what abbreviations are intended to be short for.

[Xaphiosis]

hmm. the (18) here and (14) in KHeap_R doesn't feel like an improvement, and doesn't indicate any longer that we want the tcb version. Either having a lemmas to bind it, or a comment to indicate which one it is in case the number changes (e.g. for port to MCS)

[lsf37]

+1 from me on that, these numbers shifting can be pretty hard to debug. It's fine if it's in some sledgehammer result that can be found automatically again, but otherwise if we can we should avoid them or guard them.

[corlewis]

Yeah, I was a bit hesitant to change to these numbers but also didn't like the ad-hoc lemmas being added for random lemmas out of the typ_ats set. There's a bit of a conflict here, with these proofs wanting to use the rules manually while the typ_ats are more constructed to be used automatically from wp. I didn't really want to try and rework these proofs now though.

I'll have a think to see if I can find a more systematic way of handling these.

[corlewis]

Ok, I have vague ideas for something nicer but that I think would be too much work for not enough benefit, so instead I've given these specific typ_at_lift lemmas actual names to start with and changed this line to

apply (erule (1) use_valid[OF _ valid_tcb'_typ_at_lift[OF setObject_typ_at']])

Not perfect but much more maintainable.

[Xaphiosis]

Yes, that looks much better to me, thank you!

[Xaphiosis]

this is true in a bit of a i = i + 1; // add 1 to i kind of way, but what were we missing to satisfy these assumptions? Arch proofs? something else? would be good to say that

[corlewis]

Does this help and sound accurate?

(* transfer facts from partial locale (with extra assumptions) into complete locale
   (since we can satisfy these assumptions now that the Invariants_H_typ_at_lifts interface has
   been interpreted) *)

[Xaphiosis]

I'm still a bit lost, I admit. Let me try again: I understand that we now have something from the interpretation of Invariants_H_typ_at_lifts, which allows us to satisfy gen_typ_at_props'_interface, but is there any coherent name that encompasses what that is that isn't just "assumptions"?

I was thinking it would be something like "After interpretation of Invariants_H_typ_at_lifts, The arch-specific assumptions of gen_typ_at_props'_interface are now satisfiable, meaning the typ_at properties can now be placed in a complete locale with no further type assumption" ... is that close to the truth? Does something like that sound better?

[corlewis]

I think our use of the word assumptions when we wrote this comment is making this seem more complicated than it actually is. I can't think of how to express this with the right terminology, but in my mind what we're working around is that Invariants_H_typ_at_lifts has a fixes that gen_typ_at_props'_interface has to inherit. Then, once Invariants_H_typ_at_lifts has been interpreted, we can resolve that fixes by moving everything into gen_typ_at_props'.

[Xaphiosis]

Oh, that sounds informative! What if the comment was something like:

"Invariants_H_typ_at_lifts has a fixes that gen_typ_at_props'_interface had to inherit. Now that Invariants_H_typ_at_lifts has been instantiated, we can drop that fixes assumption by moving everything into gen_typ_at_props'."

This explains a lot. I think previously you were kind of explaining more what sublocale does than what we were trying to do.

[corlewis]

Thanks, that reads well to me. I think between the comment here and the comments in Invariants_H where these locales are defined there's now enough for future us to work out what's going on here.

[Xaphiosis]

again, would be good to know what is missing here. the mention of b_itself might not be clear to someone not looking at the diff where 'b kernel is mentioned; are we talking about the kernel ext type? if so, then that's worth mentioning

[corlewis]

Whoops, thanks for spotting, I thought I had removed all references to b. This should be f_rvt_itself.

[Xaphiosis]

I'm very happy with the removal of the gen_typ_at_props' dummy parameter!

My remaining comments are related to increased clarity of comments for future historians.

[lsf37]

Also very happy with the changes, I don't have anything beyond Raf's comments.

[Xaphiosis]

maybe add so it's "avoid f_rvt_itself parameter in final locale"?

[corlewis]

Squashed, rebased and new arch-split files updated. Small bits of new content in Syscall_R and Untyped_R.

[lsf37]

Looks good and ready to merge from my side.