CAndPerms: permit clearing GL on sealed caps

But require that all other bits in the mask provided to CAndPerms be 1
in order for a tagged sealed input to result in a tagged sealed output.

properties/props.sail

@@ -22,6 +22,12 @@ function prop_nullzero() -> bool = {
     capEncodable(null_cap) & (capToBits(null_cap) == zeros()) & (null_cap.tag == false)
 }
 
+/*!
+ * Check that null_cap has no set permission bits.
+ */
+$property
+function prop_null_noperms() -> bool = { getCapPerms(null_cap) == zeros() }
+
 $property
 function prop_mem_root() -> bool = {
     capEncodable(root_cap_mem)

src/cheri_insts.sail

@@ -410,7 +410,8 @@ union clause ast = CAndPerm : (regidx, regidx, regidx)
  * previous value and bits 0 to [cap_perms_width]-1 of integer register *rs2*.
  * If the resulting set of permissions cannot be represented by the capability
  * encoding then the result will have a (possibly empty) subset of the ANDed
- * permissions. If *cs1* was sealed then *cd*.**tag** is cleared.
+ * permissions. If *cs1* was sealed and *rs2* codes for clearing anything other
+ * than Permit_Global, then *cd*.**tag** is cleared.
  */
 function clause execute(CAndPerm(cd, cs1, rs2)) = {
   let cs1_val = C(cs1);
@@ -419,8 +420,18 @@ function clause execute(CAndPerm(cd, cs1, rs2)) = {
   let perms = getCapPerms(cs1_val);
   let mask = truncate(rs2_val, cap_perms_width);
 
-  let inCap = clearTagIfSealed(cs1_val);
-  let newCap = setCapPerms(inCap, (perms & mask));
+  let newperms = perms & mask;
+
+  /*
+   * 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.
+   */
+  let perm_global = getCapPerms({ null_cap with global = true })
+  let inCap = clearTagIf(cs1_val,
+                isCapSealed(cs1_val) & (~(mask | perm_global)) != zeros());
+
+  let newCap = setCapPerms(inCap, newperms);
 
   C(cd) = newCap;
   RETIRE_SUCCESS