CAndPerms: permit clearing GL on sealed caps

src/cheri_insts.sail

@@ -419,8 +419,23 @@ 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;
+
+  let inCap = clearTagIf(cs1_val,
+                isCapSealed(cs1_val) &
+  /*
+   * Option 1: require the mask to be all ones except for the bottom bit, i.e.,
+   * GL(obal) (see cheri_cap_common.sail).
+                (~(mask | zero_extend(0b1)) != zeros())
+   */
+  /*
+   * Option 2: require that the new permissions differ from the existing ones
+   * in at most the bottom bit, i.e., GL(obal).
+   */
+                (((newperms ^ perms) | zero_extend(0b1)) != zero_extend(0b1))
+  );
+
+  let newCap = setCapPerms(inCap, newperms);
 
   C(cd) = newCap;
   RETIRE_SUCCESS