From e9ff9ff0c60b53ea0d552fa6c0b7007bb264e14d Mon Sep 17 00:00:00 2001
From: Nathaniel Wesley Filardo <wes.filardo@scisemi.com>
Date: Wed, 20 Nov 2024 04:33:33 +0000
Subject: [PATCH] Add some SMT properties for CSetBoundsRoundDown

---
 Makefile                                 |  2 +-
 properties/Makefile                      |  1 +
 properties/props_setboundsrounddown.sail | 54 ++++++++++++++++++++++++
 3 files changed, 56 insertions(+), 1 deletion(-)
 create mode 100644 properties/props_setboundsrounddown.sail

diff --git a/Makefile b/Makefile
index 0a500cf..791202f 100644
--- a/Makefile
+++ b/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)
diff --git a/properties/Makefile b/properties/Makefile
index c993331..cb3a4f5 100644
--- a/properties/Makefile
+++ b/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
 
diff --git a/properties/props_setboundsrounddown.sail b/properties/props_setboundsrounddown.sail
new file mode 100644
index 0000000..552cf8b
--- /dev/null
+++ b/properties/props_setboundsrounddown.sail
@@ -0,0 +1,54 @@
+/*!
+ * 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 (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_setboundsrounddown_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_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 & (reqLen != zeros())) --> (0b0 @ resBase <_u resTop)
+}
+
+/*!
+ * THIS checks that [setCapBoundsRoundDown] returns the most precise encodable
+ * bounds that satisfy the requested bounds.
+ */
+$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;
+    (saneTop1) --> not(validBase & validTop & betterTop)
+}