diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv
index 9a1ea67..e92ad15 100644
--- a/CHERICC_Fat.bsv
+++ b/CHERICC_Fat.bsv
@@ -37,9 +37,6 @@ export CapMem;
 export CapReg;
 export CapPipe;
 
-// -----
-// Auxiliary requried imports. TODO find a way around this?
-
 export CapFat;
 export MW;
 export OTypeW;
@@ -258,6 +255,137 @@ typedef MetaInfo TempFields;
 
 // Interface functions
 //------------------------------------------------------------------------------
+function BoundsInfo#(CapAddrW) getBoundsInfoFat (CapFat cap, TempFields tf)
+  provisos ( NumAlias #(fullW, TAdd #(CapAddrW, 1))
+           , NumAlias #(upperW, TSub #(fullW, MW))
+           , NumAlias #(lowerW, MW) );
+
+  // shared useful bindings and precomputed values
+  //////////////////////////////////////////////////////////////////////////////
+
+  // bind the Bounds field of the CapFat to shorter handy names
+  Exp exp = cap.bounds.exp;
+  Bit #(MW) baseBits = cap.bounds.baseBits;
+  Bit #(MW) topBits = cap.bounds.topBits;
+  // prepare representable bound bits
+  Bit #(MW) repBoundBits = {tf.repBoundTopBits, 0};
+
+  // prepare typed "lower" MW zeroes for simpler concatenation
+  Bit #(lowerW) lowerZeroes = 0;
+
+  // prepare "full" version for baseBits, topBits and repBoundBits
+  Bit #(fullW) baseBitsFull = zeroExtend (baseBits) << exp;
+  Bit #(fullW) topBitsFull = zeroExtend (topBits) << exp;
+  Bit #(fullW) repBoundBitsFull = zeroExtend (repBoundBits) << exp;
+
+  // other helper values
+  CapAddr capAddr0 = 0;
+  CapAddrPlus1 addrSpaceTop = {1'b1, capAddr0};
+  Bool alwaysRep = exp >= resetExp - 2;
+
+  // shared +1 and -1/~0 shifted by exponent
+  Bit #(upperW) allOnesExpShifted = ~0 << exp;
+  let mask = allOnesExpShifted;
+  let minusOne = allOnesExpShifted;
+  Bit #(upperW) oneExpShifted = 1 << exp;
+  let plusOne = oneExpShifted;
+
+  // Prepare "upper" address and its "hi" and "lo" region versions
+  Bit #(upperW) addrUpperBits = truncateLSB ({1'b0, cap.address}) & mask;
+  Bit #(upperW) addrUpperHi = addrUpperBits + (tf.addrHi ? 0 : plusOne);
+  Bit #(upperW) addrUpperLo = addrUpperBits + (tf.addrHi ? minusOne : 0);
+  function addrUpper (isHi) = isHi ? addrUpperHi : addrUpperLo;
+
+  // compute base
+  //////////////////////////////////////////////////////////////////////////////
+
+  // Use the appropriate upper bits of the address based on whether the base is
+  // in the "hi" or the "lo" region, append implied zeroes in the lower bits,
+  // and or in the base bits
+  CapAddr base =
+    truncate ({addrUpper (tf.baseHi), lowerZeroes} | baseBitsFull);
+
+  // compute top
+  //////////////////////////////////////////////////////////////////////////////
+
+  // Use the appropriate upper bits of the address based on whether the top is
+  // in the "hi" or the "lo" region, append implied zeroes in the lower bits,
+  // and or in the top bits
+  CapAddrPlus1 top = {addrUpper (tf.topHi), lowerZeroes} | topBitsFull;
+  // If the base and top are more than an address space away from eachother,
+  // invert the 64th/32nd bit of Top. This corrects for errors that happen when
+  // the representable space wraps the address space.
+  Bit #(2) topTip = truncateLSB (top);
+  Bit #(2) baseTip = {1'b0, msb (base)};
+  // If the bit we're interested in are actually coming from baseBits, select
+  // the correct one from there.
+  // exp == (resetExp - 1) doesn't matter since we will not flip unless
+  // exp < resetExp - 1.
+  if (exp == (resetExp - 2)) baseTip = {1'b0, baseBits[valueOf(MW) - 1]};
+  // Do the final check.
+  // If exp >= resetExp - 1, the bits we're looking at are coming directly from
+  // topBits and baseBits, are not being inferred, and therefore do not need
+  // correction. If we are below this range, check that the difference between
+  // the resulting top and bottom is less than one address space.  If not, flip
+  // the msb of the top.
+  if (exp < (resetExp - 1) && (topTip - baseTip) > 1)
+    top[valueOf(CapAddrW)] = ~top[valueOf(CapAddrW)];
+
+  // compute length
+  //////////////////////////////////////////////////////////////////////////////
+
+  // Get the top and base bits with the 2 correction bits prepended
+  Bit #(TAdd #(MW, 2)) correctBase = {pack (tf.baseCorrection), baseBits};
+  Bit #(TAdd #(MW, 2)) correctTop  = {pack (tf.topCorrection), topBits};
+  // Get the length by subtracting base from top and shifting appropriately, and
+  // saturate in case of big exponent
+  CapAddrPlus1 length =
+    (exp >= resetExp) ? ~0 : zeroExtend (correctTop - correctBase) << exp;
+
+  // compute repBase
+  //////////////////////////////////////////////////////////////////////////////
+
+  // Use the "lo" region upper bits of the address, append implied zeroes in the
+  // lower bits, and or in the representable bound bit.
+  // Saturate to zero when in the "always representable" case,
+  // i.e. exp >= resetExp - 2.
+  CapAddr repBase =
+    alwaysRep ? capAddr0
+              : truncate ({addrUpperLo, lowerZeroes} | repBoundBitsFull);
+
+  // compute repTop
+  //////////////////////////////////////////////////////////////////////////////
+
+  // Use the "hi" region upper bits of the address, append implied zeroes in the
+  // lower bits, and or in the representable bound bits
+  // Saturate to 1 and all zeroes when in the "always representable" case,
+  // i.e. exp >= resetExp - 2.
+  CapAddrPlus1 repTop =
+    alwaysRep ? addrSpaceTop
+              : {addrUpperHi, lowerZeroes} | repBoundBitsFull;
+
+  // compute repLength
+  //////////////////////////////////////////////////////////////////////////////
+
+  CapAddrPlus1 repLength = {oneExpShifted, lowerZeroes};
+
+  // compute split of representable space
+  //////////////////////////////////////////////////////////////////////////////
+
+  Bool repSplit = alwaysRep ? False : ! unpack (reduceOr (addrUpperHi));
+
+  // return populated BoundsInfo structure
+  //////////////////////////////////////////////////////////////////////////////
+
+  return BoundsInfo { base: base
+                    , top: top
+                    , length: length
+                    , repBase: repBase
+                    , repTop: repTop
+                    , repLength: repLength
+                    , repSplit: repSplit };
+endfunction
+
 function CapAddr getBotFat(CapFat cap, TempFields tf);
   // First, construct a full length value with the base bits and the
   // correction bits above, and shift that value to the appropriate spot.
@@ -834,10 +962,13 @@ function MetaInfo getMetaInfo (CapFat cap);
     , baseCorrection : baseCorrection };
 endfunction
 
-// ===============================================================================
-// Typeclass instance for interface
-
-typedef Bit#(TAdd#(1, CapW)) CapMem;
+// XXX TODO
+// to avoid an orphan instance here, we should make CapMem a "newtype",
+// basically:
+// typedef struct {
+//   Bit #(TAdd #(1, CapW)) cap;
+// } CapMem;
+typedef Bit #(TAdd #(1, CapW)) CapMem;
 
 typedef CapFat CapReg;
 
@@ -846,27 +977,41 @@ typedef struct {
   TempFields tempFields;
 } CapPipe deriving (Bits);
 
+// CapMem CHERICap instance
+////////////////////////////////////////////////////////////////////////////////
+// Note: commented out methods have a provided default implementation in the
+//       CHERICap typeclass definition
+
 instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
+
+  // capability validity
+  //////////////////////////////////////////////////////////////////////////////
   function isValidCap (capMem);
-    CapabilityInMemory cap = unpack(capMem);
+    CapabilityInMemory cap = unpack (capMem);
     return cap.isCapability;
   endfunction
   function setValidCap (capMem, v);
-    CapabilityInMemory cap = unpack(capMem);
+    CapabilityInMemory cap = unpack (capMem);
     cap.isCapability = v;
-    return pack(cap);
+    return pack (cap);
   endfunction
+
+  // capability flags
+  //////////////////////////////////////////////////////////////////////////////
   function getFlags (capMem);
-    CapabilityInMemory cap = unpack(capMem);
+    CapabilityInMemory cap = unpack (capMem);
     return cap.flags;
   endfunction
   function setFlags (capMem, f);
-    CapabilityInMemory cap = unpack(capMem);
+    CapabilityInMemory cap = unpack (capMem);
     cap.flags = f;
-    return pack(cap);
+    return pack (cap);
   endfunction
+
+  // capability permissions
+  //////////////////////////////////////////////////////////////////////////////
   function getHardPerms (capMem);
-    CapabilityInMemory cap = unpack(capMem);
+    CapabilityInMemory cap = unpack (capMem);
     return HardPerms {
       permitSetCID:        cap.perms.hard.permit_set_CID
     , accessSysRegs:       cap.perms.hard.access_sys_regs
@@ -881,54 +1026,91 @@ instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
     , permitExecute:       cap.perms.hard.permit_execute
     , global:              cap.perms.hard.non_ephemeral };
   endfunction
-  function setHardPerms = error("setHardPerms not implemented for CapMem");
-  function getSoftPerms = error("getSoftPerms not implemented for CapMem");
-  function setSoftPerms = error("setSoftPerms not implemented for CapMem");
-  function getKind = error("getKind not implemented for CapMem");
-  function setKind = error("setKind not implemented for CapMem");
-  function getMeta(capMem);
-    CapabilityInMemory cap = unpack(capMem);
+  function setHardPerms = error ("setHardPerms not implemented for CapMem");
+  function getSoftPerms = error ("getSoftPerms not implemented for CapMem");
+  function setSoftPerms = error ("setSoftPerms not implemented for CapMem");
+  //function getPerms = error ("getPerms not implemented for CapMem");
+  //function setPerms = error ("setPerms not implemented for CapMem");
+
+  // capability kind
+  //////////////////////////////////////////////////////////////////////////////
+  function getKind = error ("getKind not implemented for CapMem");
+  function setKind = error ("setKind not implemented for CapMem");
+  function validAsType (dummy, checkType);
+    UInt #(CapAddrW) checkTypeUnsigned = unpack (checkType);
+    UInt #(CapAddrW) otypeMaxUnsigned = unpack (zeroExtend (otype_max));
+    return checkTypeUnsigned <= otypeMaxUnsigned;
+  endfunction
+
+  // capability in-memory architectural representation
+  //////////////////////////////////////////////////////////////////////////////
+  function getMeta (capMem);
+    CapabilityInMemory cap = unpack (capMem);
     return { pack (cap.perms)
            , pack (cap.reserved)
            , pack (cap.flags)
            , pack (cap.otype)
            , pack (cap.bounds) };
   endfunction
-  function getAddr(capMem);
-    CapabilityInMemory cap = unpack(capMem);
+  function getAddr (capMem);
+    CapabilityInMemory cap = unpack (capMem);
     return pack (cap.address);
   endfunction
-  function setAddr = error("setAddr not implemented for CapMem");
+  function fromMem = error ("fromMem not implemented for CapMem");
+  function toMem = error ("toMem not implemented for CapMem");
+
+  // capability address/offset manipulation
+  //////////////////////////////////////////////////////////////////////////////
+  function setAddr = error ("setAddr not implemented for CapMem");
   function setAddrUnsafe (capMem, address);
-    CapabilityInMemory cap = unpack(capMem);
+    CapabilityInMemory cap = unpack (capMem);
     cap.address = address;
-    return pack(cap);
+    return pack (cap);
   endfunction
   function addAddrUnsafe (capMem, inc) =
-    setAddrUnsafe(capMem, getAddr(capMem) + signExtend(inc));
-  function getOffset = error("getOffset not implemented for CapMem");
-  function modifyOffset = error("modifyOffset not implemented for CapMem");
-  function getBase = error("getBase not implemented for CapMem");
-  function getTop = error("getTop not implemented for CapMem");
-  function getLength = error("getLength not implemented for CapMem");
-  function isInBounds = error("isInBounds not implemented for CapMem");
-  function setBoundsCombined = error("setBoundsCombined not implemented for CapMem");
-  function nullWithAddr = setAddrUnsafe(packCap(null_cap));
+    setAddrUnsafe (capMem, getAddr (capMem) + signExtend (inc));
+  function maskAddr = error ("maskAddr not implemented for CapMem");
+  //function getOffset = error ("getOffset not implemented for CapMem");
+  function modifyOffset = error ("modifyOffset not implemented for CapMem");
+  //function setOffset = error ("setOffset not implemented for CapMem");
+  //function incOffset = error ("incOffset not implemented for CapMem");
+
+  // capability architectural bounds queries
+  //////////////////////////////////////////////////////////////////////////////
+  function getBoundsInfo = error ("getBoundsInfo not implemented for CapMem");
+  //function getBase = error ("getBase not implemented for CapMem");
+  //function getTop = error ("getTop not implemented for CapMem");
+  //function getLength = error ("getLength not implemented for CapMem");
+  //function isInBounds = error ("isInBounds not implemented for CapMem");
+  //function getRepBase = error ("getRepBase not implemented for CapMem");
+  //function getRepTop = error ("getRepTop not implemented for CapMem");
+  //function getRepLength = error ("getRepLength not implemented for CapMem");
+  //function isInRepBounds = error ("isInRepBounds not implemented for CapMem");
+  function getBaseAlignment =
+    error ("getBaseAlignment not implemented for CapMem");
+
+  // capability derivation (bounds set)
+  //////////////////////////////////////////////////////////////////////////////
+  function setBoundsCombined =
+    error ("setBoundsCombined not implemented for CapMem");
+  //function setBounds = error ("setBounds not implemented for CapMem");
+  //function roundLength = error ("roundLength not implemented for CapMem");
+  //function alignmentMask = error ("alignmentMask not implemented for CapMem");
+
+  // common capabilities
+  //////////////////////////////////////////////////////////////////////////////
+  //function nullCap = error ("nullCap not implemented for CapMem");
+  function nullWithAddr = setAddrUnsafe (packCap (null_cap));
   function almightyCap;
     CapReg res = almightyCap;
-    return cast(res);
+    return cast (res);
   endfunction
-  function nullCapFromDummy (dummy) = packCap(null_cap);
-  function validAsType (dummy, checkType);
-    UInt#(CapAddrW) checkTypeUnsigned = unpack(checkType);
-    UInt#(CapAddrW) otypeMaxUnsigned = unpack(zeroExtend(otype_max));
-    return checkTypeUnsigned <= otypeMaxUnsigned;
-  endfunction
-  function fromMem = error("fromMem not implemented for CapMem");
-  function toMem = error("toMem not implemented for CapMem");
-  function maskAddr = error("maskAddr not implemented for CapMem");
-  function getBaseAlignment = error("getBaseAlignment not implemented for CapMem");
-  function isDerivable = error("isDerivable not implemented for CapMem");
+  function nullCapFromDummy (dummy) = packCap (null_cap);
+
+  // Assert that the encoding is valid
+  //////////////////////////////////////////////////////////////////////////////
+  function isDerivable = error ("isDerivable not implemented for CapMem");
+
 endinstance
 
 instance FShow #(CapPipe);
@@ -953,22 +1135,31 @@ instance Eq #(CapReg);
 //  function Bool \/= (CapPipe x, CapPipe y);
 endinstance
 
+// CapReg CHERICap instance
+////////////////////////////////////////////////////////////////////////////////
+// Note: commented out methods have a provided default implementation in the
+//       CHERICap typeclass definition
+
 instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
 
+  // capability validity
+  //////////////////////////////////////////////////////////////////////////////
   function isValidCap (x) = x.isCapability;
-
   function setValidCap (cap, tag);
     cap.isCapability = tag;
     return cap;
   endfunction
 
+  // capability flags
+  //////////////////////////////////////////////////////////////////////////////
   function getFlags (cap) = cap.flags;
-
   function setFlags (cap, flags);
     cap.flags = flags;
     return cap;
   endfunction
 
+  // capability permissions
+  //////////////////////////////////////////////////////////////////////////////
   function getHardPerms (cap) = HardPerms {
       permitSetCID:        cap.perms.hard.permit_set_CID
     , accessSysRegs:       cap.perms.hard.access_sys_regs
@@ -982,7 +1173,6 @@ instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
     , permitLoad:          cap.perms.hard.permit_load
     , permitExecute:       cap.perms.hard.permit_execute
     , global:              cap.perms.hard.non_ephemeral };
-
   function setHardPerms (cap, perms);
     cap.perms.hard = HPerms {
       permit_set_CID:             perms.permitSetCID
@@ -999,14 +1189,16 @@ instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
     , non_ephemeral:              perms.global };
     return cap;
   endfunction
-
-  function getSoftPerms (cap) = zeroExtend(cap.perms.soft);
-
+  function getSoftPerms (cap) = zeroExtend (cap.perms.soft);
   function setSoftPerms (cap, perms);
-    cap.perms.soft = truncate(perms);
+    cap.perms.soft = truncate (perms);
     return cap;
   endfunction
+  //function getPerms = error ("getPerms not implemented for CapReg");
+  //function setPerms = error ("setPerms not implemented for CapReg");
 
+  // capability kind
+  //////////////////////////////////////////////////////////////////////////////
   function getKind (cap) = case (cap.otype)
     otype_unsealed: UNSEALED;
     otype_sentry:   SENTRY;
@@ -1014,71 +1206,85 @@ instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
     otype_res1:     RES1;
     default:        SEALED_WITH_TYPE (cap.otype);
   endcase;
-
   function setKind (cap, kind) = case (kind) matches
-    tagged UNSEALED:             unseal(cap, ?);
-    tagged SENTRY:               seal(cap, ?, VnD {v: True, d:otype_sentry});
-    tagged RES0:                 seal(cap, ?, VnD {v: True, d:otype_res0});
-    tagged RES1:                 seal(cap, ?, VnD {v: True, d:otype_res1});
-    tagged SEALED_WITH_TYPE .ot: seal(cap, ?, VnD {v: True, d:ot});
+    tagged UNSEALED:             unseal (cap, ?);
+    tagged SENTRY:               seal (cap, ?, VnD {v: True, d:otype_sentry});
+    tagged RES0:                 seal (cap, ?, VnD {v: True, d:otype_res0});
+    tagged RES1:                 seal (cap, ?, VnD {v: True, d:otype_res1});
+    tagged SEALED_WITH_TYPE .ot: seal (cap, ?, VnD {v: True, d:ot});
   endcase;
+  function validAsType (dummy, checkType);
+    CapMem nullC = nullCap;
+    return validAsType (nullC, checkType);
+  endfunction
 
-  function getMeta(capReg);
+  // capability in-memory architectural representation
+  //////////////////////////////////////////////////////////////////////////////
+  function getMeta (capReg);
     CapMem cap = unpack (pack (toMem (capReg)));
     return getMeta (cap);
   endfunction
-
   function getAddr (capReg);
     CapMem cap = unpack (pack (toMem (capReg)));
     return getAddr (cap);
   endfunction
+  function fromMem (x) = cast (pack (x));
+  function toMem (x) = unpack (cast (x));
 
-  function setAddr = error("setAddr not implemented for CapReg");
-
-  function setAddrUnsafe (cap, address) = setCapPointer(cap, address);
-
+  // capability address/offset manipulation
+  //////////////////////////////////////////////////////////////////////////////
+  function setAddr = error ("setAddr not implemented for CapReg");
+  function setAddrUnsafe (cap, address) = setCapPointer (cap, address);
   function addAddrUnsafe (cap, inc) =
-    setAddrUnsafe(cap, getAddr(cap) + signExtend(inc));
-
-  function getOffset = error("getOffset not implemented for CapReg");
-  function modifyOffset = error("modifyOffset not implemented for CapReg");
-  function getBase = error("getBase not implemented for CapReg");
-  function getTop = error("getTop not implemented for CapReg");
-  function getLength = error("getLength not implemented for CapReg");
-  function isInBounds = error("isInBounds not implemented for CapReg");
-
-  function setBoundsCombined(cap, length) = setBoundsFat(cap, length);
-
-  function nullWithAddr (addr) = setAddrUnsafe(null_cap, addr);
-
-  function almightyCap = defaultCapFat;
-
-  function nullCapFromDummy (x) = null_cap;
-
-  function fromMem (x) = cast(pack(x));
-
-  function toMem (x) = unpack(cast(x));
-
-  function maskAddr (cap, mask) = setCapPointer(cap, cap.address & {~0,mask});
-
-  function validAsType (dummy, checkType);
-    CapMem nullC = nullCap;
-    return validAsType(nullC, checkType);
-  endfunction
+    setAddrUnsafe (cap, getAddr (cap) + signExtend (inc));
+  function maskAddr (cap, mask) = setCapPointer (cap, cap.address & {~0, mask});
+  function getOffset = error ("getOffset not implemented for CapReg");
+  function modifyOffset = error ("modifyOffset not implemented for CapReg");
+  //function setOffset = error ("setOffset not implemented for CapReg");
+  //function incOffset = error ("incOffset not implemented for CapReg");
 
+  // capability architectural bounds queries
+  //////////////////////////////////////////////////////////////////////////////
+  function getBoundsInfo = error ("getBoundsInfo not implemented for CapReg");
+  //function getBase = error ("getBase not implemented for CapReg");
+  //function getTop = error ("getTop not implemented for CapReg");
+  //function getLength = error ("getLength not implemented for CapReg");
+  //function isInBounds = error ("isInBounds not implemented for CapReg");
+  //function getRepBase = error ("getRepBase not implemented for CapReg");
+  //function getRepTop = error ("getRepTop not implemented for CapReg");
+  //function getRepLength = error ("getRepLength not implemented for CapReg");
+  //function isInRepBounds = error ("isInRepBounds not implemented for CapReg");
   function getBaseAlignment (cap) =
-    // If cap exp is non-zero, we have internal exponent, so the least significant
-    // two bits of the base are implicitly zero.
-    // Otherwise, we have a zero exponent, so the least significant two bits
-    // of the base are the least significant bits of the encoded base
+    // If cap exp is non-zero, we have internal exponent, so the least
+    // significant two bits of the base are implicitly zero.  Otherwise, we
+    // have a zero exponent, so the least significant two bits of the base are
+    // the least significant bits of the encoded base
     (cap.bounds.exp == 0) ? cap.bounds.baseBits[1:0] : 2'b0;
 
+  // capability derivation (bounds set)
+  //////////////////////////////////////////////////////////////////////////////
+  function setBoundsCombined (cap, length) = setBoundsFat (cap, length);
+  //function setBounds = error ("setBounds not implemented for CapReg");
+  //function roundLength = error ("roundLength not implemented for CapReg");
+  //function alignmentMask = error ("alignmentMask not implemented for CapReg");
+
+  // common capabilities
+  //////////////////////////////////////////////////////////////////////////////
+  //function nullCap = error ("nullCap not implemented for CapReg");
+  function nullWithAddr (addr) = setAddrUnsafe (null_cap, addr);
+  function almightyCap = defaultCapFat;
+  function nullCapFromDummy (x) = null_cap;
+
+  // Assert that the encoding is valid
+  //////////////////////////////////////////////////////////////////////////////
   function isDerivable (cap) =
-    cap.bounds.exp <= resetExp &&
-    !(cap.bounds.exp == resetExp && ((truncateLSB(cap.bounds.topBits) != 1'b0) ||
-                                     (truncateLSB(cap.bounds.baseBits) != 2'b0))) &&
-    !(cap.bounds.exp == resetExp-1 && (truncateLSB(cap.bounds.baseBits) != 1'b0)) &&
-    (cap.reserved == 0);
+        (cap.bounds.exp <= resetExp)
+    && !(   (cap.bounds.exp == resetExp)
+         && (   (truncateLSB (cap.bounds.topBits)  != 1'b0)
+             || (truncateLSB (cap.bounds.baseBits) != 2'b0) ))
+    && !(   (cap.bounds.exp == resetExp-1)
+         && (truncateLSB (cap.bounds.baseBits) != 1'b0))
+    &&  (cap.reserved == 0);
 
 endinstance
 
@@ -1180,6 +1386,8 @@ instance CHERICap #(CapPipe, OTypeW, FlagsW, CapAddrW, CapW, TSub#(MW, 3));
     return Exact { exact: result.v, value: cap };
   endfunction
 
+  function getBoundsInfo (cap) = getBoundsInfoFat (cap.capFat, cap.tempFields);
+
   function getBase (cap) = getBotFat(cap.capFat, cap.tempFields);
 
   function getTop (cap) = getTopFat(cap.capFat, cap.tempFields);
diff --git a/CHERICap.bsv b/CHERICap.bsv
index 76632bf..791060a 100644
--- a/CHERICap.bsv
+++ b/CHERICap.bsv
@@ -29,7 +29,7 @@
 
 package CHERICap;
 
-// CHERI public types
+// CHERI capability types
 ////////////////////////////////////////////////////////////////////////////////
 
 // Permission bits
@@ -64,6 +64,32 @@ instance Bitwise #(HardPerms);
   function lsb (x) = lsb(pack(x));
 endinstance
 
+// Kind of a capability, that is whether it is "sealed with a given otype", or
+// if it is a "sentry" or simply "unsealed".
+
+typedef union tagged {
+  void UNSEALED;
+  void SENTRY;
+  void RES0;
+  void RES1;
+  Bit #(otypeW) SEALED_WITH_TYPE;
+} Kind #(numeric type otypeW) deriving (Bits, Eq, FShow);
+
+// helper type for gathering bounds information on a capability
+
+typedef struct {
+  Bit #(addrW) base;
+  Bit #(TAdd #(addrW, 1)) top;
+  Bit #(TAdd #(addrW, 1)) length;
+  Bit #(addrW) repBase;
+  Bit #(TAdd #(addrW, 1)) repTop;
+  Bit #(TAdd #(addrW, 1)) repLength;
+  Bool repSplit;
+} BoundsInfo #(numeric type addrW) deriving (Bits, Eq, FShow);
+
+// helper types and functions
+////////////////////////////////////////////////////////////////////////////////
+
 // Helper type to return the result of an operation along with whether the
 // operation was exact. In cases where no sensible inexact representation
 // exists, the only guarantee is that the tag bit is not set.
@@ -73,165 +99,26 @@ typedef struct {
   t    value;
 } Exact #(type t) deriving (Bits);
 
-// Kind of a capability, that is whether it is "sealed with a given otype", or
-// if it is a "sentry" or simply "unsealed".
-
-typedef union tagged {
-  void UNSEALED;
-  void SENTRY;
-  void RES0;
-  void RES1;
-  Bit #(ot) SEALED_WITH_TYPE;
-} Kind #(numeric type ot) deriving (Bits, Eq, FShow);
-
 // Helper type for the return value of the 'setBoundsCombined' method
 
 typedef struct {
-  t cap;
+  capT cap;
   Bool exact;
-  Bit #(n) length;
-  Bit #(n) mask;
-} SetBoundsReturn #(type t, numeric type n) deriving (Bits, Eq, FShow);
+  Bit #(addrW) length;
+  Bit #(addrW) mask;
+} SetBoundsReturn #(type capT, numeric type addrW) deriving (Bits, Eq, FShow);
 
+// helper function to test belonging to a range
+function Bool belongsToRange ( Bit #(n) x, Bit #(n) low, Bit #(n) high
+                             , Bool highIncluded);
+  Bool notTooHigh = highIncluded ? x <= high : x < high;
+  Bool notTooLow = x >= low;
+  return notTooLow && notTooHigh;
+endfunction
 
-// CHERI capability typeclass
-////////////////////////////////////////////////////////////////////////////////
-
-typeclass CHERICap #( type t
-                    , numeric type ot
-                    , numeric type flg
-                    , numeric type n
-                    , numeric type mem_sz
-                    , numeric type maskable_bits )
-  dependencies (t determines (ot, flg, n, mem_sz, maskable_bits));
-
-  // Return whether the Capability is valid
-  function Bool isValidCap (t cap);
-  // Set the capability as valid. All fields left unchanged
-  function t setValidCap (t cap, Bool valid);
-
-  // Get the flags field
-  function Bit#(flg) getFlags (t cap);
-  // Set the flags field
-  function t setFlags (t cap, Bit#(flg) flags);
-
-  // Get the hardware permissions
-  function HardPerms getHardPerms (t cap);
-  // Set the hardware permissions
-  function t setHardPerms (t cap, HardPerms hardperms);
-  // Get the software permissions
-  function SoftPerms getSoftPerms (t cap);
-  // Set the software permissions
-  function t setSoftPerms (t cap, SoftPerms softperms);
-  // Get the architectural permissions
-  function Bit#(31) getPerms (t cap) =
-    zeroExtend({pack(getSoftPerms(cap)), 3'h0, pack(getHardPerms(cap))});
-  // Set the architectural permissions
-  function t setPerms (t cap, Bit#(31) perms) =
-    setSoftPerms ( setHardPerms(cap, unpack(perms[11:0]))
-                 , unpack(truncate(perms[30:15])) );
-
-  // Manipulate the kind of the capability, i.e. whether it is sealed, sentry,
-  // unsealed, ...
-  function Kind#(ot) getKind (t cap);
-  function t setKind (t cap, Kind#(ot) kind);
-
-  // Get the in-memory architectural representation of the capability metadata
-  function Bit #(TSub #(mem_sz, n)) getMeta (t cap);
-  // Get the in-memory architectural representation of the capability address
-  function Bit #(n) getAddr (t cap);
-
-  // Note that the following rule is expected to hold:
-  // fromMem (tuple2 (isValidCap (cap), {getMeta (cap), getAddr (cap)})) == cap
-
-  // Set the address of the capability. Result invalid if unrepresentable
-  function Exact#(t) setAddr (t cap, Bit#(n) addr);
-  // Set the address of the capability. Result assumed to be representable
-  function t setAddrUnsafe (t cap, Bit#(n) addr);
-  // Add to the address of the capability. Result assumed to be representable
-  function t addAddrUnsafe (t cap, Bit#(maskable_bits) inc);
-
-  // Get the offset of the capability
-  function Bit#(n) getOffset (t cap) = getAddr(cap) - getBase(cap);
-  // Modify the offset of the capability. Result invalid if unrepresentable
-  function Exact#(t) modifyOffset (t cap, Bit#(n) offset, Bool doInc);
-  // Set the offset of the capability. Result invalid if unrepresentable
-  function Exact#(t) setOffset (t cap, Bit#(n) offset) =
-    modifyOffset(cap, offset, False);
-  // Set the offset of the capability. Result invalid if unrepresentable
-  function Exact#(t) incOffset (t cap, Bit#(n) inc) =
-    modifyOffset(cap, inc, True);
-
-  // Get the base
-  function Bit#(n) getBase (t cap);
-  // Get the top
-  function Bit#(TAdd#(n, 1)) getTop (t cap);
-  // Get the length
-  function Bit#(TAdd#(n, 1)) getLength (t cap);
-
-  // Assertion that address is between base and top
-  function Bool isInBounds (t cap, Bool isTopIncluded);
-    Bool isNotTooHigh = isTopIncluded ? zeroExtend(getAddr(cap)) <= getTop(cap)
-                                      : zeroExtend(getAddr(cap)) < getTop(cap);
-    Bool isNotTooLow = getAddr(cap) >= getBase(cap);
-    return isNotTooLow && isNotTooHigh;
-  endfunction
-
-  // Set the length of the capability. Inexact: result length may be different
-  // to requested
-  function Exact#(t) setBounds (t cap, Bit#(n) length);
-    let combinedResult = setBoundsCombined(cap, length);
-    return Exact {exact: combinedResult.exact, value: combinedResult.cap};
-  endfunction
-
-  function SetBoundsReturn#(t, n) setBoundsCombined (t cap, Bit#(n) length);
-
-  // Returns a null cap with an address set to the argument
-  function t nullWithAddr (Bit#(n) addr);
-
-  // Workaround to allow null cap to be derived in default implementations
-  function t nullCapFromDummy(t dummy);
-
-  // Return the maximally permissive capability (initial register state)
-  function t almightyCap;
-  // Return the null capability
-  function t nullCap = nullCapFromDummy(?);
-
-  // Check if a type is valid
-  function Bool validAsType (t dummy, Bit#(n) checkType);
-
-  // Convert from and to bit memory representation
-  function t fromMem (Tuple2#(Bool, Bit#(mem_sz)) mem_cap);
-  function Tuple2#(Bool, Bit#(mem_sz)) toMem (t cap);
-
-  // Functions that can be cheap by relying on current capability representation
-
-  // Mask the least significant bits of capability address with a mask
-  // maskable_width should be small enough to make this
-  // safe with respect to representability
-  function t maskAddr (t cap, Bit#(maskable_bits) mask);
-
-  // Check the alignment of the base, giving least significant 2 bits.
-  // This relies on the fact that internal exponents take up 2 bits of the
-  // base.
-  function Bit#(2) getBaseAlignment (t cap);
-
-  // Get representable alignment mask
-  function Bit#(n) getRepresentableAlignmentMask ( t dummy
-                                                 , Bit#(n) length_request) =
-    setBoundsCombined(nullCapFromDummy(dummy), length_request).mask;
-
-  // Get representable length
-  function Bit#(n) getRepresentableLength (t dummy, Bit#(n) length_request) =
-    setBoundsCombined(nullCapFromDummy(dummy), length_request).length;
-
-  // Assert that the encoding is valid
-  function Bool isDerivable (t cap);
-
-endtypeclass
-
-function Fmt showCHERICap (t cap)
-  provisos (CHERICap #(t , ot, flg, n, mem_sz, maskable_bits));
+// XXX TODO augment with all architectural bounds/ repbounds ?
+function Fmt showCHERICap (capT cap)
+  provisos (CHERICap #(capT , otypeW, flgW, addrW, inMemW, maskableW));
   return $format( "Valid: 0x%0x", isValidCap(cap)) +
          $format(" Perms: 0x%0x", getPerms(cap)) +
          $format(" Kind: ", fshow(getKind(cap))) +
@@ -243,12 +130,200 @@ endfunction
 // Cast typeclass to convert from one type to another. Helpful for converting
 // a capability format to another.
 
-typeclass Cast#(type src, type dest);
+typeclass Cast #(type src, type dest);
   function dest cast (src x);
 endtypeclass
 
-instance Cast#(t, t);
+instance Cast #(capT, capT);
   function cast = id;
 endinstance
 
+// CHERI capability typeclass
+////////////////////////////////////////////////////////////////////////////////
+// Note: Some class methods receive a "dummy" capability as a type proxy
+//       argument. This is useful for methods to know which capability format is
+//       being operated on without requiring a specific capability value.
+//       (A more elegant way to achieve this would be to use something along the
+//       lines of haskell's "@type" type application mechanism)
+
+typeclass CHERICap #( type capT              // type of the CHERICap capability
+                    , numeric type otypeW    // width of the object type
+                    , numeric type flgW      // width of the flags field
+                    , numeric type addrW     // width of the address
+                    , numeric type inMemW    // width of the capability in mem
+                    , numeric type maskableW // width of maskable bits
+                    )
+  dependencies (capT determines (otypeW, flgW, addrW, inMemW, maskableW));
+
+  // capability validity
+  //////////////////////////////////////////////////////////////////////////////
+
+  // Return whether the Capability is valid
+  function Bool isValidCap (capT cap);
+  // Set the capability as valid. All fields left unchanged
+  function capT setValidCap (capT cap, Bool valid);
+
+  // capability flags
+  //////////////////////////////////////////////////////////////////////////////
+
+  // Get the flags field
+  function Bit #(flgW) getFlags (capT cap);
+  // Set the flags field
+  function capT setFlags (capT cap, Bit #(flgW) flags);
+
+  // capability permissions
+  //////////////////////////////////////////////////////////////////////////////
+
+  // Get the hardware permissions
+  function HardPerms getHardPerms (capT cap);
+  // Set the hardware permissions
+  function capT setHardPerms (capT cap, HardPerms hardperms);
+  // Get the software permissions
+  function SoftPerms getSoftPerms (capT cap);
+  // Set the software permissions
+  function capT setSoftPerms (capT cap, SoftPerms softperms);
+  // Get the architectural permissions
+  function Bit #(31) getPerms (capT cap) =
+    zeroExtend ({pack (getSoftPerms (cap)), 3'h0, pack (getHardPerms (cap))});
+  // Set the architectural permissions
+  function capT setPerms (capT cap, Bit #(31) perms) =
+    setSoftPerms ( setHardPerms (cap, unpack (perms[11:0]))
+                 , unpack (truncate (perms[30:15])) );
+
+  // capability kind
+  //////////////////////////////////////////////////////////////////////////////
+  // Manipulate the kind of the capability, i.e. whether it is sealed, sentry,
+  // unsealed, ...
+
+  // get the kind of a capability
+  function Kind #(otypeW) getKind (capT cap);
+  // set the kind of a capability
+  function capT setKind (capT cap, Kind #(otypeW) kind);
+  // Check if a type is valid (requires a dummy proxy)
+  function Bool validAsType (capT dummy, Bit #(addrW) checkType);
+
+  // capability in-memory architectural representation
+  //////////////////////////////////////////////////////////////////////////////
+  // Note that the following rule is expected to hold:
+  // fromMem (toMem (cap)) == cap
+  // fromMem (tuple2 (isValidCap (cap), {getMeta (cap), getAddr (cap)})) == cap
+
+  // Get the in-memory architectural representation of the capability metadata
+  function Bit #(TSub #(inMemW, addrW)) getMeta (capT cap);
+  // Get the in-memory architectural representation of the capability address
+  function Bit #(addrW) getAddr (capT cap);
+  // Convert from in-memory architectural bit representation to capability type
+  function capT fromMem (Tuple2 #(Bool, Bit #(inMemW)) mem_cap);
+  // Convert from capability type to in-memory architectural bit representation
+  function Tuple2 #(Bool, Bit #(inMemW)) toMem (capT cap);
+
+  // capability address/offset manipulation
+  //////////////////////////////////////////////////////////////////////////////
+
+  // Set the address of the capability. Result invalid if unrepresentable
+  function Exact #(capT) setAddr (capT cap, Bit #(addrW) addr);
+  // Set the address of the capability. Result assumed to be representable
+  function capT setAddrUnsafe (capT cap, Bit #(addrW) addr);
+  // Add to the address of the capability. Result assumed to be representable
+  function capT addAddrUnsafe (capT cap, Bit #(maskableW) inc);
+  // Mask the least significant bits of capability address with a mask
+  // maskable_width should be small enough to make this
+  // safe with respect to representability
+  function capT maskAddr (capT cap, Bit #(maskableW) mask);
+  // Get the offset of the capability
+  function Bit #(addrW) getOffset (capT cap) = getAddr(cap) - getBase(cap);
+  // Modify the offset of the capability. Result invalid if unrepresentable
+  function Exact #(capT) modifyOffset ( capT cap
+                                      , Bit #(addrW) offset
+                                      , Bool doInc);
+  // Set the offset of the capability. Result invalid if unrepresentable
+  function Exact #(capT) setOffset (capT cap, Bit #(addrW) offset) =
+    modifyOffset(cap, offset, False);
+  // Set the offset of the capability. Result invalid if unrepresentable
+  function Exact #(capT) incOffset (capT cap, Bit #(addrW) inc) =
+    modifyOffset(cap, inc, True);
+
+  // capability architectural bounds queries
+  //////////////////////////////////////////////////////////////////////////////
+  // Note that the following rules are expected to hold:
+  // getBase (cap) + getLength (cap) == getTop (cap)
+  // getRepBase (cap) + getRepLength (cap) == getRepTop (cap)
+  // isInBounds (cap) ==> isInRepBounds (cap)
+
+  // Get all architectural bound information for a capability
+  function BoundsInfo #(addrW) getBoundsInfo (capT cap);
+  // Get the base
+  function Bit #(addrW) getBase (capT cap) = getBoundsInfo(cap).base;
+  // Get the top
+  function Bit #(TAdd #(addrW, 1)) getTop (capT cap) = getBoundsInfo(cap).top;
+  // Get the length
+  function Bit #(TAdd #(addrW, 1)) getLength (capT cap) =
+    getBoundsInfo(cap).length;
+  // Assertion that the capability's address is between its base and top
+  function Bool isInBounds (capT cap, Bool isTopIncluded) =
+    belongsToRange ( zeroExtend (getAddr (cap))
+                   , zeroExtend (getBase (cap))
+                   , getTop (cap)
+                   , isTopIncluded );
+  // Get the representable base
+  function Bit #(addrW) getRepBase (capT cap) = getBoundsInfo(cap).repBase;
+  // Get the representable top
+  function Bit #(TAdd #(addrW, 1)) getRepTop (capT cap) =
+    getBoundsInfo(cap).repTop;
+  // Get the representable length
+  function Bit #(TAdd #(addrW, 1)) getRepLength (capT cap) =
+    getBoundsInfo(cap).repLength;
+  // Check if the capapbility's representable region is split (i.e. wrapping the
+  // address space)
+  function Bool isRepSplit (capT cap) = getBoundsInfo(cap).repSplit;
+  // Assertion that the capability's address is between its representable
+  // base and top
+  function Bool isInRepBounds (capT cap);
+    let addr = getAddr (cap);
+    let bInfo = getBoundsInfo (cap);
+    let okLo = addr >= bInfo.repBase;
+    let okHi = zeroExtend (addr) < bInfo.repTop;
+    return (okLo && okHi) || (bInfo.repSplit && (okLo != okHi));
+  endfunction
+  // Check the alignment of the base, giving least significant 2 bits.
+  function Bit #(2) getBaseAlignment (capT cap) = getBoundsInfo (cap).base[1:0];
+
+  // capability derivation (bounds set)
+  //////////////////////////////////////////////////////////////////////////////
+
+  // Set the length of the capability
+  function SetBoundsReturn #(capT, addrW)
+    setBoundsCombined (capT cap, Bit #(addrW) length);
+  // Set the length of the capability. Inexact: result length may be different
+  // to requested
+  function Exact #(capT) setBounds (capT cap, Bit #(addrW) length);
+    let combinedResult = setBoundsCombined (cap, length);
+    return Exact {exact: combinedResult.exact, value: combinedResult.cap};
+  endfunction
+  // Round a requested length (requires a dummy proxy)
+  function Bit #(addrW) roundLength (capT dummy, Bit #(addrW) reqLength) =
+    setBoundsCombined (nullCapFromDummy (dummy), reqLength).length;
+  // Get alignment mask for a requested length (requires a dummy proxy)
+  function Bit #(addrW) alignmentMask (capT dummy, Bit #(addrW) reqLength) =
+    setBoundsCombined (nullCapFromDummy (dummy), reqLength).mask;
+
+  // common capabilities
+  //////////////////////////////////////////////////////////////////////////////
+
+  // the null capability
+  function capT nullCap = nullCapFromDummy (?);
+  // a null capability with a given address set
+  function capT nullWithAddr (Bit #(addrW) addr);
+  // maximally permissive capability (initial register state)
+  function capT almightyCap;
+  // the null capability (requires a dummy proxy)
+  function capT nullCapFromDummy (capT dummy);
+
+  // Assert that the encoding is valid
+  //////////////////////////////////////////////////////////////////////////////
+
+  function Bool isDerivable (capT cap);
+
+endtypeclass
+
 endpackage