From 595447fd62432faa80d4a6533897ea4d229198dd Mon Sep 17 00:00:00 2001
From: Alexandre Joannou <alexandre.joannou@cl.cam.ac.uk>
Date: Mon, 10 Feb 2025 17:44:09 +0000
Subject: [PATCH] fix property following getLength return type change in
 b3896e4e508a4b898446fa83b9e7b6d9696e0907

---
 CHERICapProps.bsv | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv
index ea0a314..fd8ffb2 100644
--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -52,7 +52,7 @@ function Bool forallBaseAndLen(CapAddr base, CapAddr len,
   Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
   Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
   return baseCap.exact && implies
-    ( boundedCap.exact 
+    ( boundedCap.exact
     , prop(boundedCap.value)
     );
 endfunction
@@ -107,10 +107,10 @@ function Bool prop_exact(CapAddr base, CapAddr len);
   Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
   Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
   Exact#(CapPipe) baseCap2 = setAddr(almightyCap, getBase(boundedCap.value));
-  CapAddrPlus1 length = getLength(boundedCap.value);
-  Exact#(CapPipe) boundedCap2 = setBounds(baseCap2.value, truncate(length));
+  CapAddr length = getLength(boundedCap.value);
+  Exact#(CapPipe) boundedCap2 = setBounds(baseCap2.value, length);
   return baseCap.exact && baseCap2.exact && implies
-           ( truncateLSB(length) == 1'b0
+           ( ~length != 0
            , boundedCap2.exact
            );
 endfunction