From 1d2c0b953ba8e46a6503df7537a8eb02d8df6b5a Mon Sep 17 00:00:00 2001
From: Jonathan Woodruff <jonathan.woodruff@capabilitieslimited.co.uk>
Date: Fri, 7 Mar 2025 15:12:46 +0000
Subject: [PATCH] Add a property that setBounds will only return a valid cap if
 the bounds are within the original bounds.

---
 CHERICapProps.bsv | 12 ++++++++++++
 assertions.sv     | 21 +++++++++++++++++++++
 check.sby         |  4 ++++
 3 files changed, 37 insertions(+)

diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv
index 8f08a24..fdda65d 100644
--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -192,4 +192,16 @@ function Bool prop_fromToMem(CapMem in);
   return (cm == in);
 endfunction
 
+(* noinline *)
+function Bool prop_setBounds(CapAddr base, CapAddr len, CapAddr addr, CapAddr new_len);
+  function prop(cap);
+    let new_cap = setBounds(cap,new_len).value;
+    return implies( isValidCap(new_cap),
+                    getBase(cap) <= getBase(new_cap)
+                    && getTop(cap) >= getTop(new_cap)
+                  );
+  endfunction
+  return forallCap(base, len, addr, prop);
+endfunction
+
 endpackage
diff --git a/assertions.sv b/assertions.sv
index eb51914..aa0763f 100644
--- a/assertions.sv
+++ b/assertions.sv
@@ -160,3 +160,24 @@ module assert_prop_fromToMem(
     assert(prop_ok);
   end
 endmodule
+
+module assert_prop_setBounds(
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr,
+         input wire [63 : 0] prop_new_len
+       );
+  wire prop_ok;
+
+  module_prop_setBounds module_prop_setBounds_inst(
+    .prop_setBounds_base(prop_base),
+    .prop_setBounds_len(prop_len),
+    .prop_setBounds_addr(prop_addr),
+    .prop_setBounds_new_len(prop_new_len),
+    .prop_setBounds(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule
diff --git a/check.sby b/check.sby
index 2f9058e..d68cbe5 100644
--- a/check.sby
+++ b/check.sby
@@ -8,6 +8,7 @@ prop_getLength
 prop_isInBounds
 prop_setAddr
 prop_fromToMem
+prop_setBounds
 
 [options]
 depth 1
@@ -27,6 +28,7 @@ read -formal module_prop_getLength.v
 read -formal module_prop_isInBounds.v
 read -formal module_prop_setAddr.v
 read -formal module_prop_fromToMem.v
+read -formal module_prop_setBounds.v
 prop_getBase: prep -top assert_prop_getBase
 prop_getTop: prep -top assert_prop_getTop
 prop_getLength: prep -top assert_prop_getLength
@@ -36,6 +38,7 @@ prop_exact: prep -top assert_prop_exact
 prop_exactConditions: prep -top assert_prop_exactConditions
 prop_setAddr: prep -top assert_prop_setAddr
 prop_fromToMem: prep -top assert_prop_fromToMem
+prop_setBounds: prep -top assert_prop_setBounds
 
 [files]
 assertions.sv
@@ -48,3 +51,4 @@ counterexamples/module_prop_getLength.v
 counterexamples/module_prop_isInBounds.v
 counterexamples/module_prop_setAddr.v
 counterexamples/module_prop_fromToMem.v
+counterexamples/module_prop_setBounds.v