From 3990ca55d9d11c194783483c9371bf31627e1c3f 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

---
 properties/Makefile                      |  1 +
 properties/props_setboundsrounddown.sail | 37 ++++++++++++++++++++++++
 2 files changed, 38 insertions(+)
 create mode 100644 properties/props_setboundsrounddown.sail

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..e740fd5
--- /dev/null
+++ b/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)
+}
+