From 7212f50b4d2476e0ace31a15ef07bd1a811c8ad9 Mon Sep 17 00:00:00 2001
From: Jonathan Woodruff <jdw57@cam.ac.uk>
Date: Fri, 24 Jan 2025 17:23:49 +0000
Subject: [PATCH] Take into account tag clearing in setBounds.

---
 CHERICapProps.bsv | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv
index ad89ec4..05bd946 100644
--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -91,6 +91,7 @@ function Bool prop_unique(CapAddr base, CapAddr len,
   return baseCap.exact && expectedBaseCap.exact && implies
     ( boundedCap.exact && newBaseCap.exact &&
       finalCap.exact && expectedCap.exact &&
+      isValidCap(finalCap.value) &&
       newBase >= base && {1'b0, newBase} + {1'b0, newLen} <=
                          {1'b0, base}    + {1'b0, len}
     , toMem(expectedCap.value) == toMem(finalCap.value)