Add some SMT properties for CSetBoundsRoundDown

Co-authored-by: Robert Norton <robert.norton@microsoft.com>

Makefile

@@ -318,7 +318,7 @@ c_emulator/cheri_riscv_rvfi_%: generated_definitions/c/riscv_rvfi_model_%.c $(SA
 	$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(SAIL_RISCV_DIR)/c_emulator/riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
 
 latex: $(SAIL_SRCS) Makefile
-	$(SAIL) -latex -latex_prefix sailRISCV -o sail_latex_riscv $(SAIL_SRCS) properties/proplib.sail properties/props.sail
+	$(SAIL) -latex -latex_prefix sailRISCV -o sail_latex_riscv $(SAIL_SRCS) properties/proplib.sail properties/props.sail properties/props_setboundsrounddown.sail
 
 generated_definitions/isabelle/$(ARCH)/ROOT: handwritten_support/ROOT
 	mkdir -p generated_definitions/isabelle/$(ARCH)

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,61 @@
+/*!
+ * THIS checks that CSetBoundsRoundDown meets its description: the result leaves
+ * the base unaltered and returns a capability with length at most the requested
+ * size.
+ */
+$property
+function prop_setboundsrounddown_brief(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 --> ((resBase == reqBase) & (resTop <=_u reqTop) & (0b0 @ resBase <=_u resTop))
+}
+
+/*!
+ * THIS checks that exactly representable requests give equal answers between
+ * CSetBoundsRoundDown and CSetBounds, so long as the requested length is
+ * representable with exponent 14 or below.
+ */
+$property
+function prop_setboundsrounddown_exact(reqBase : CapAddrBits, reqLen : CapAddrBits) -> bool = {
+    let cRD = setCapBoundsRoundDown(root_cap_mem, reqBase, reqLen);
+    let (exact, cSB) = setCapBounds(root_cap_mem, reqBase, reqLen);
+    let threshold14 : CapAddrBits = zero_extend(ones(cap_mantissa_width)) << 14;
+    (exact & (reqLen <=_u threshold14)) --> (cRD == cSB)
+}
+
+/*!
+ * THIS checks that the resulting capability has nonzero length unless requested
+ */
+$property
+function prop_setboundsrounddown_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 --> ( (0b0 @ resBase <_u resTop)
+                | ((0b0 @ resBase == resTop) & (reqLen == zeros())))
+}
+
+/*!
+ * THIS checks that [setCapBoundsRoundDown] returns the most precise encodable
+ * bounds that satisfy the requested bounds, unless the requested length is
+ * very large (above exponent 14), in which case the result is the largest
+ * exponent 14 capability.
+ */
+$property
+function prop_setboundsrounddown_precise(reqBase1 : CapAddrBits, reqLen1 : CapAddrBits,
+        c2 : CapBits) -> bool = {
+    let c1 = setCapBoundsRoundDown(root_cap_mem, reqBase1, reqLen1);
+    let (b1, t1) = getCapBoundsBits(c1);
+    let reqTop1 = (0b0 @ reqBase1) + (0b0 @ reqLen1);
+    let saneTop1 = reqTop1 <=_u 0b1@0x00000000;
+    let (b2, t2) = getCapBoundsBits(capBitsToCapability(false, c2));
+    let validBase = b2 == reqBase1;
+    let validTop = t2 <=_u reqTop1;
+    let betterTop = t1 <_u t2;
+    let threshold14 : CapAddrBits = zero_extend(ones(cap_mantissa_width)) << 14;
+    (saneTop1 & validBase & validTop & betterTop) -->
+      ((reqLen1 >=_u threshold14) & (t1 - (0b0 @ b1) == 0b0 @ threshold14))
+}