Add a property that setBounds will only return a valid cap if the bounds are within the original bounds.

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

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

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