fixup! CSetBoundsRoundDown implementation

src/cheri_cap_common.sail

@@ -510,29 +510,29 @@ function setCapBoundsRoundDown(cap, base, length) : (Capability, CapAddrBits, Ca
   let top : CapLenBits = ext_base + (0b0 @ length);
   /* Find smallest exponent that can represent required length. */
   let e : range(0, 23) = 23 - count_leading_zeros(truncateLSB(length, 23));
-  /* Saturate e at max if it exceeds representable 4-bit value. */
-  var e_sat : range(0,  cap_max_E) = if e > 14 then cap_max_E else e;
   /* What is the required alignment of base? */
   let e_b = count_trailing_zeros(base);
-  /* Extract B and T for initial e_sat */
-  var B = truncate(base >> e_sat, cap_mantissa_width);
-  var T = truncate(top >> e_sat, cap_mantissa_width);
 
-  if (e_sat > e_b) | (e > 14) then {
+  let (E, B, T) = if (e > e_b) | (e > 14) then {
     /*
      * base or (saturated) top unrepresentable using chosen e;
      * chose a smaller one and make a maximum length capability for that e
      */
-    let e_bInBandGap : bool = ((e_b > 14) & (e_b < cap_max_E));
-    e_sat = if e_bInBandGap | (e > 14) then min(14, min(e_sat, e_b)) else e_b;
+    let E : range(0, 14) = min(14, min(e, e_b));
 
     /* Extract B for new e_sat */
-    B = truncate(base >> e_sat, cap_mantissa_width);
+    let B = truncate(base >> E, cap_mantissa_width);
     /* This will make a max length cap for given E, B */
-    T = B - 1;
+    (E, B, B - 1);
+  } else {
+    /* Extract B and T for initial e_sat */
+    ( e : range(0, 14)
+    , truncate(base >> e, cap_mantissa_width)
+    , truncate(top >> e, cap_mantissa_width))
   };
+
   /* Return the cap with new bounds and address */
-  {cap with address=base, E=to_bits(cap_E_width, e_sat), B=B, T=T}
+  {cap with address=base, E=to_bits(cap_E_width, E), B=B, T=T}
 }
 
 function getCapPerms(cap) : Capability -> CapPermsBits = [