From 01263b2c62d57a57d4845cbc4eea7bed1701a072 Mon Sep 17 00:00:00 2001
From: Nathaniel Wesley Filardo <wes.filardo@scisemi.com>
Date: Fri, 8 Nov 2024 19:40:45 +0000
Subject: [PATCH] CAndPerms: permit clearing GL on sealed caps

---
 src/cheri_insts.sail | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail
index 3a967df..ed20f63 100644
--- a/src/cheri_insts.sail
+++ b/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