From 199e3c9f7f91b1a6ab7ab771cd1c30131445e27c Mon Sep 17 00:00:00 2001
From: Peter Rugg <pdr32@cam.ac.uk>
Date: Tue, 4 Mar 2025 14:43:05 +0000
Subject: [PATCH] Extend forallCap to include almightyCap

---
 CHERICapProps.bsv | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv
index fd8ffb2..8f08a24 100644
--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -49,12 +49,18 @@ function Bool implies(Bool x, Bool y) = !x || y;
 
 function Bool forallBaseAndLen(CapAddr base, CapAddr len,
                                  function Bool prop(CapPipe cap));
-  Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
-  Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
-  return baseCap.exact && implies
-    ( boundedCap.exact
-    , prop(boundedCap.value)
-    );
+  Bool ret = ?;
+  if (base == 0 && ~len == 0) begin
+    ret = prop(almightyCap);
+  end else begin
+    Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
+    Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
+    ret = baseCap.exact && implies
+      ( boundedCap.exact
+      , prop(boundedCap.value)
+      );
+  end
+  return ret;
 endfunction
 
 // Furthermore, every valid capability can be reached by calling setAddr on
@@ -137,7 +143,8 @@ endfunction
 
 (* noinline *)
 function Bool prop_getTop(CapAddr base, CapAddr len, CapAddr addr);
-  function prop(cap) = getTop(cap) == zeroExtend(base) + zeroExtend(len);
+  Bool reqAlmighty = ~len == 0;
+  function prop(cap) = getTop(cap) == zeroExtend(base) + (reqAlmighty ? {1'b1, 0} : zeroExtend(len));
   return forallCap(base, len, addr, prop);
 endfunction