Add some SMT properties for CSetBoundsRoundDown

properties/Makefile

@@ -7,6 +7,7 @@ SRCS+=${TOP}/src/cheri_types.sail
 SRCS+=${TOP}/src/cheri_cap_common.sail
 SRCS+=proplib.sail
 SRCS+=props.sail
+SRCS+=props_setboundsrounddown.sail
 
 all: generate_smt run_smt
 

properties/props_setboundsrounddown.sail

@@ -0,0 +1,37 @@
+/*!
+ * THIS checks that CSetBoundsRoundDown meets its description: the result leaves
+ * the base unaltered and returns a capability with length at most the requested
+ * size.
+ */
+$counterexample
+function prop_csbrd_brief(reqBase : CapAddrBits, reqLen : CapAddrBits) -> bool = {
+    let c = setCapBoundsRoundDown(root_cap_mem, reqBase, reqLen);
+    let (base, top) = getCapBoundsBits(c);
+    let reqTop = (0b0 @ reqBase) + (0b0 @ reqLen);
+    let saneTop = reqTop <=_u 0b1@0x00000000;
+    saneTop --> ((base == reqBase) & (top <=_u reqTop) & (0b0 @ base <=_u top))
+}
+
+/*!
+ * THIS checks that exactly representable requests give equal answers between
+ * CSetBoundsRoundDown and CSetBounds.
+ */
+$property
+function prop_csbrd_exact(reqBase : CapAddrBits, reqLen : CapAddrBits) -> bool = {
+    let cRD = setCapBoundsRoundDown(root_cap_mem, reqBase, reqLen);
+    let (exact, cSB) = setCapBounds(root_cap_mem, reqBase, reqLen);
+    exact --> (cRD == cSB)
+}
+
+/*!
+ * THIS checks that the resulting capability has nonzero length unless requested
+ */
+$property
+function prop_csbrd_nonzero(reqBase : CapAddrBits, reqLen : CapAddrBits) -> bool = {
+    let c = setCapBoundsRoundDown(root_cap_mem, reqBase, reqLen);
+    let (resBase, resTop) = getCapBoundsBits(c);
+    let reqTop = (0b0 @ reqBase) + (0b0 @ reqLen);
+    let saneTop = reqTop <=_u 0b1@0x00000000;
+    (saneTop & (reqLen != zeros())) --> (0b0 @ resBase <_u resTop)
+}
+