crunch bundles

[lsf37]

Resurrecting an old Jira issue: https://sel4.atlassian.net/browse/VER-1274

It says:

It'd be nice if we could declare bundles of properties for crunches, so that we don't have to type out large lists of properties every time.
In particular, we quite often want to crunch preservation of non-pspace parts of the state in the kernel, but we tend to spread them out to the point where they are first used. If we instead declared a bundle once, we wouldn't have to remember what each of them are called every time, and could do them all in one go. Similarly, there are properties that often go together, eg operations that don't change caps or liveness state of objects, or operations that don't touch threads etc. Some of these could potentially be better handled by locales, but not all.
Example of possible syntax:

crunch_bundle cte_props =
  ctes_of[wp]: "%s. P (ctes_of s)"
  cteCaps_of[wp]: ...

crunch_bundle more_props = cte_props +
   valid_arch_state': ...

crunches some_fun
  for cte_props
  and some_prop[wp]: stuff

Requires some more thinking whether attributes should only occur at the call site in the actual crunches or if they should be able to occur in the bundle declaration already.

The issue also mentions an except syntax where you can remove a property from a bundle.

[lsf37]

Thinking a bit more about it, I would change the syntax slightly to conform to the one we are already using in crunch. The example would become:

crunch_bundle cte_props
  for ctes_of[wp]: "%s. P (ctes_of s)"
  and cteCaps_of[wp]: ...

crunch_bundle more_props = 
   for valid_arch_state': "%s. P (...)"
   and cte_props

crunches some_fun
  for cte_props
  and some_prop[wp]: stuff
  and other_props

That is, the syntax for crunch_bundle is crunch_bundle <name> <crunch_declaration> where <crunch_declarations> is the current crunch syntax after the function names, except for the fact that a name: prop part can also be bundle name reference.

This would make the syntax uniform to use and also enable is to share a sub-parser between crunch and crunch_bundle.

I would also leave out the except idea in the issue, because it would complicate the implementation too much (for comparatively small gain).

The idea is that the <crunch_declaration> parser always produces as result a list of (name, attrib, term) (after resolving and expanding all bundle references), and the rest of crunch would not need to change at all.