CAndPerms: permit clearing GL on sealed caps

[nwf]

Address #70. This is not ready to merge, in that it hasn't yet decided between the two options:

1. Require that the mask to CAndPerms on a sealed operand must be all-ones or all-ones-but-GL
2. Require only that the difference between the initial and masked permissions be at most the GL bit.

Shuffle the comment delimiters around to pick between the two. I believe either is fine from a security perspective; option 1 imposes stronger requirements on the program(mer) while the later tolerates some... incidental correctness. If one is clearly better for microarchitecture, tho', that could be the deciding factor.

Pinging @kliuMsft.

[kliuMsft]

@nwf either p[topm is fine from microarchitecture perspective. Option 1 is a little easier to implement & verify but the difference is not huge.

[rmn30]

If either works for uarch I think sw preference is for option 2 so lets go with that!

[davidchisnall]

The third option, which is easiest for software, is to treat whatever you have and whatever you have minus G as the only representable things and make CAndPerm do the same thing is does currently when the exact intersection is not representable.

[rmn30]

@davidchisnall what you're suggesting would be the same as forcing all bits of the mask except GL to one if the capability is sealed. Isn't it likely to be a programmer error to try to clear non-GL permissions on a sealed capability? If so that proposal would allow the error to go undetected. On the other hand if the programmer wants to clear permissions on unsealed capabilities and leave sealed ones alone (except GL) that would be useful.

[rmn30]

Suggested change

	* Sealed caps clear the tag unless the mask is all ones (~mask == zeros())
	* or has the global permission clear. This relies on the prop_null_noperms
	* property to ensure that perm_global is a one-hot vector.
	* CAndPerms on a sealed cap clears the tag unless the mask is all ones
	* or has *only* the global permission clear. Here `perm_global` is a
	* vector of zeros except for the global permission bit. To construct this
	* we rely on the fact that `null_cap` has all zero permissions.

Hopefully this is clearer. I removed the mention of prop_null_noperms as I thought it might just be confusing to people reading the arch doc. Good to have, though!

[rmn30]

Looks good modulo suggested changes. Please also add a changelog entry and check if the archdoc text needs updating anywhere. We should mention the rationale for this change too.