fixup! Add some SMT properties for CSetBoundsRoundDown

CHERIoT-Platform · Nov 20, 2024 · d778b84 · d778b84
1 parent 0251e38
commit d778b84
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/properties/props_setboundsrounddown.sail b/properties/props_setboundsrounddown.sail
@@ -20,7 +20,8 @@ $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)
+    let threshold : CapAddrBits = zero_extend(ones(cap_mantissa_width)) << 14;
+    (exact & (reqLen <=_u threshold)) --> (cRD == cSB)
 }
 
 /*!
@@ -50,5 +51,7 @@ function prop_setboundsrounddown_precise(reqBase1 : CapAddrBits, reqLen1 : CapAd
     let validBase = b2 == reqBase1;
     let validTop = t2 <=_u reqTop1;
     let betterTop = t1 <_u t2;
-    (saneTop1) --> not(validBase & validTop & betterTop)
+    let threshold : CapAddrBits = zero_extend(ones(cap_mantissa_width)) << 14;
+    (saneTop1 & (reqLen1 <=_u threshold))
+      --> not(validBase & validTop & betterTop)
 }