saving current changes

hack changes
saving current changes cheri-cap-lib
2026-02-23 11:44:35 +00:00 · 2026-02-20 01:59:12 +00:00 · 2026-02-19 18:07:45 +00:00 · 2026-02-17 15:34:56 +00:00 · 2026-02-17 14:49:00 +00:00 · 2026-02-17 14:26:25 +00:00
12 changed files with 767 additions and 542 deletions
--- a/.github/workflows/check-prop.yml
+++ b/.github/workflows/check-prop.yml
@@ -0,0 +1,16 @@
+name: "check properties"
+on:
+  pull_request:
+  push:
+jobs:
+  tests:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - uses: cachix/install-nix-action@v27
+      with:
+        github_access_token: ${{ secrets.GITHUB_TOKEN }}
+    - name: Setup environment
+      run: nix develop --command make verilog-wrappers verilog-props
+    - name: Run property checks
+      run: nix develop --command make check-prop
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1,2 @@
+build/
+counterexamples/
--- a/CHERICC.bsv
+++ b/CHERICC.bsv
@@ -1,452 +1,452 @@
-/*-
- * Copyright (c) 2017-2019 Alexandre Joannou
- * All rights reserved.
- *
- * This software was developed by SRI International and the University of
- * Cambridge Computer Laboratory (Department of Computer Science and
- * Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
- * DARPA SSITH research programme.
- *
- * @BERI_LICENSE_HEADER_START@
- *
- * Licensed to BERI Open Systems C.I.C. (BERI) under one or more contributor
- * license agreements.  See the NOTICE file distributed with this work for
- * additional information regarding copyright ownership.  BERI licenses this
- * file to you under the BERI Hardware-Software License, Version 1.0 (the
- * "License"); you may not use this file except in compliance with the
- * License.  You may obtain a copy of the License at:
- *
- *   http://www.beri-open-systems.org/legal/license-1-0.txt
- *
- * Unless required by applicable law or agreed to in writing, Work distributed
- * under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR
- * CONDITIONS OF ANY KIND, either express or implied.  See the License for the
- * specific language governing permissions and limitations under the License.
- *
- * @BERI_LICENSE_HEADER_END@
- */
+// /*-
+//  * Copyright (c) 2017-2019 Alexandre Joannou
+//  * All rights reserved.
+//  *
+//  * This software was developed by SRI International and the University of
+//  * Cambridge Computer Laboratory (Department of Computer Science and
+//  * Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//  * DARPA SSITH research programme.
+//  *
+//  * @BERI_LICENSE_HEADER_START@
+//  *
+//  * Licensed to BERI Open Systems C.I.C. (BERI) under one or more contributor
+//  * license agreements.  See the NOTICE file distributed with this work for
+//  * additional information regarding copyright ownership.  BERI licenses this
+//  * file to you under the BERI Hardware-Software License, Version 1.0 (the
+//  * "License"); you may not use this file except in compliance with the
+//  * License.  You may obtain a copy of the License at:
+//  *
+//  *   http://www.beri-open-systems.org/legal/license-1-0.txt
+//  *
+//  * Unless required by applicable law or agreed to in writing, Work distributed
+//  * under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR
+//  * CONDITIONS OF ANY KIND, either express or implied.  See the License for the
+//  * specific language governing permissions and limitations under the License.
+//  *
+//  * @BERI_LICENSE_HEADER_END@
+//  */

-package CHERICC;
+// package CHERICC;

-import CHERICap :: *;
+// import CHERICap :: *;

-export CHERICCCap;
-export CHERICCBounds;
+// export CHERICCCap;
+// export CHERICCBounds;

-`define div2(x) TDiv#(x, 2)
-`define sub2(x) TSub#(x, 2)
-`define i(x)    valueOf(x)
+// `define div2(x) TDiv#(x, 2)
+// `define sub2(x) TSub#(x, 2)
+// `define i(x)    valueOf(x)

-// CHERICCBounds Bounds type
-////////////////////////////////////////////////////////////////////////////////
-// CHERICC compressed bounds type
-typedef union tagged {
-  struct {
-    Bit#(1) lenMSB;
-    Bit#(`sub2(base_)) top;
-    Bit#(base_) base;
-  } Exp0;
-  struct {
-    Bit#(TSub#(`sub2(base_), `div2(e_))) top;
-    Bit#(TSub#(base_, `div2(e_))) base;
-    Bit#(e_) e;
-  } EmbeddedExp;
-  struct {
-    Bit#(TSub#(`sub2(base_), TAdd#(`div2(t_), `div2(e_)))) top;
-    Bit#(TSub#(base_, TAdd#(`div2(t_), `div2(e_)))) base;
-    Bit#(t_) otype;
-    Bit#(e_) e;
-  } Sealed;
-} CHERICCBounds#(numeric type base_, numeric type e_, numeric type t_);
+// // CHERICCBounds Bounds type
+// ////////////////////////////////////////////////////////////////////////////////
+// // CHERICC compressed bounds type
+// typedef union tagged {
+//   struct {
+//     Bit#(1) lenMSB;
+//     Bit#(`sub2(base_)) top;
+//     Bit#(base_) base;
+//   } Exp0;
+//   struct {
+//     Bit#(TSub#(`sub2(base_), `div2(e_))) top;
+//     Bit#(TSub#(base_, `div2(e_))) base;
+//     Bit#(e_) e;
+//   } EmbeddedExp;
+//   struct {
+//     Bit#(TSub#(`sub2(base_), TAdd#(`div2(t_), `div2(e_)))) top;
+//     Bit#(TSub#(base_, TAdd#(`div2(t_), `div2(e_)))) base;
+//     Bit#(t_) otype;
+//     Bit#(e_) e;
+//   } Sealed;
+// } CHERICCBounds#(numeric type base_, numeric type e_, numeric type t_);

-instance Bits#(CHERICCBounds#(b_, e_, t_), TMul#(b_, 2)) provisos(
-    // in pack
-    Add#(TDiv#(e_, 2), a__, e_), // truncates on e
-    Add#(TDiv#(t_, 2), b__, t_), // truncates on t
-    Add#(2, c__, b_), // 2 bits stolen from top
-    // in unpack
-    Add#(d__, TDiv#(e_, 2), TMul#(b_, 2)), // truncates raw into e
-    Add#(e__, TDiv#(t_, 2), TMul#(b_, 2)), // truncates raw into t
-    Add#(2, f__, TSub#(
-                   TSub#(
-                     TAdd#(b_,
-                           TAdd#(
-                             TDiv#(t_, 2),
-                             TDiv#(e_, 2))),
-                     TDiv#(e_, 2)),
-                     TDiv#(t_, 2)))
-  );
-  function pack(ccbounds) =
-    case (ccbounds) matches
-      tagged Exp0 .x: return {{{1'b0, x.lenMSB}, x.top}, x.base};
-      tagged EmbeddedExp .x: begin
-        Bit#(`div2(e_)) eHi = truncateLSB(x.e);
-        Bit#(`div2(e_)) eLo = truncate(x.e);
-        return {{2'b10, x.top, eHi}, {x.base, eLo}};
-      end
-      tagged Sealed .x: begin
-        Bit#(`div2(t_)) tHi = truncateLSB(x.otype);
-        Bit#(`div2(t_)) tLo = truncate(x.otype);
-        Bit#(`div2(e_)) eHi = truncateLSB(x.e);
-        Bit#(`div2(e_)) eLo = truncate(x.e);
-        return {{2'b11, x.top, tHi, eHi}, {x.base, tLo, eLo}};
-        /*
-        Bit#(TMul#(b_, 2)) acc = 0;
-        acc = acc | zeroExtend(2'b11);
-        acc = (acc << `i(b_)-2-`i(t_)/2-`i(e_)/2) | zeroExtend(x.top);
-        acc = (acc << `i(t_)/2) | zeroExtend(tHi);
-        acc = (acc << `i(e_)/2) | zeroExtend(eHi);
-        acc = (acc << `i(b_)-`i(t_)/2-`i(e_)/2) | zeroExtend(x.base);
-        acc = (acc << `i(t_)/2) | zeroExtend(tLo);
-        acc = (acc << `i(e_)/2) | zeroExtend(eLo);
-        return acc;
-        */
-      end
-    endcase;
-  function unpack(raw);
-    if (raw[2*`i(b_)-1] == 0) return Exp0 {
-      lenMSB: raw[2*`i(b_)-2],
-      top:    raw[2*`i(b_)-3:`i(b_)],
-      base:   raw[`i(b_)-1:0]
-    };
-    else if (raw[2*`i(b_)-2] == 0) begin
-      Bit#(`div2(e_)) eHi = truncate(raw >> `i(b_));
-      Bit#(`div2(e_)) eLo = truncate(raw);
-      // XXX Bit#(e_) new_e = {eHi, eLo}; XXX simpler provisos with equiv line below
-      Bit#(e_) new_e = zeroExtend(eLo) | zeroExtend(eHi) << `i(e_)/2;
-      return EmbeddedExp {
-        top:    raw[2*`i(b_)-3:`i(b_)+`i(e_)/2],
-        base:   raw[`i(b_)-1:`i(e_)/2],
-        e:      new_e
-      };
-    end else begin
-      Bit#(`div2(t_)) tHi = truncate(raw >> (`i(b_)+(`i(e_)/2)));
-      Bit#(`div2(t_)) tLo = truncate(raw >> (`i(e_)/2));
-      // XXX Bit#(t_) new_t = {tHi, tLo}; XXX simpler provisos with equiv line below
-      Bit#(t_) new_t = zeroExtend(tLo) | zeroExtend(tHi) << `i(t_)/2;
-      Bit#(`div2(e_)) eHi = truncate(raw >> `i(b_));
-      Bit#(`div2(e_)) eLo = truncate(raw);
-      // XXX Bit#(e_) new_e = {eHi, eLo}; XXX simpler provisos with equiv line below
-      Bit#(e_) new_e = zeroExtend(eLo) | zeroExtend(eHi) << `i(e_)/2;
-      return Sealed {
-        top:    raw[2*`i(b_)-3:`i(b_)+`i(e_)/2+`i(t_)/2],
-        base:   raw[`i(b_)-1:`i(e_)/2+`i(t_)/2],
-        otype:  new_t,
-        e:      new_e
-      };
-    end
-  endfunction
-endinstance
+// instance Bits#(CHERICCBounds#(b_, e_, t_), TMul#(b_, 2)) provisos(
+//     // in pack
+//     Add#(TDiv#(e_, 2), a__, e_), // truncates on e
+//     Add#(TDiv#(t_, 2), b__, t_), // truncates on t
+//     Add#(2, c__, b_), // 2 bits stolen from top
+//     // in unpack
+//     Add#(d__, TDiv#(e_, 2), TMul#(b_, 2)), // truncates raw into e
+//     Add#(e__, TDiv#(t_, 2), TMul#(b_, 2)), // truncates raw into t
+//     Add#(2, f__, TSub#(
+//                    TSub#(
+//                      TAdd#(b_,
+//                            TAdd#(
+//                              TDiv#(t_, 2),
+//                              TDiv#(e_, 2))),
+//                      TDiv#(e_, 2)),
+//                      TDiv#(t_, 2)))
+//   );
+//   function pack(ccbounds) =
+//     case (ccbounds) matches
+//       tagged Exp0 .x: return {{{1'b0, x.lenMSB}, x.top}, x.base};
+//       tagged EmbeddedExp .x: begin
+//         Bit#(`div2(e_)) eHi = truncateLSB(x.e);
+//         Bit#(`div2(e_)) eLo = truncate(x.e);
+//         return {{2'b10, x.top, eHi}, {x.base, eLo}};
+//       end
+//       tagged Sealed .x: begin
+//         Bit#(`div2(t_)) tHi = truncateLSB(x.otype);
+//         Bit#(`div2(t_)) tLo = truncate(x.otype);
+//         Bit#(`div2(e_)) eHi = truncateLSB(x.e);
+//         Bit#(`div2(e_)) eLo = truncate(x.e);
+//         return {{2'b11, x.top, tHi, eHi}, {x.base, tLo, eLo}};
+//         /*
+//         Bit#(TMul#(b_, 2)) acc = 0;
+//         acc = acc | zeroExtend(2'b11);
+//         acc = (acc << `i(b_)-2-`i(t_)/2-`i(e_)/2) | zeroExtend(x.top);
+//         acc = (acc << `i(t_)/2) | zeroExtend(tHi);
+//         acc = (acc << `i(e_)/2) | zeroExtend(eHi);
+//         acc = (acc << `i(b_)-`i(t_)/2-`i(e_)/2) | zeroExtend(x.base);
+//         acc = (acc << `i(t_)/2) | zeroExtend(tLo);
+//         acc = (acc << `i(e_)/2) | zeroExtend(eLo);
+//         return acc;
+//         */
+//       end
+//     endcase;
+//   function unpack(raw);
+//     if (raw[2*`i(b_)-1] == 0) return Exp0 {
+//       lenMSB: raw[2*`i(b_)-2],
+//       top:    raw[2*`i(b_)-3:`i(b_)],
+//       base:   raw[`i(b_)-1:0]
+//     };
+//     else if (raw[2*`i(b_)-2] == 0) begin
+//       Bit#(`div2(e_)) eHi = truncate(raw >> `i(b_));
+//       Bit#(`div2(e_)) eLo = truncate(raw);
+//       // XXX Bit#(e_) new_e = {eHi, eLo}; XXX simpler provisos with equiv line below
+//       Bit#(e_) new_e = zeroExtend(eLo) | zeroExtend(eHi) << `i(e_)/2;
+//       return EmbeddedExp {
+//         top:    raw[2*`i(b_)-3:`i(b_)+`i(e_)/2],
+//         base:   raw[`i(b_)-1:`i(e_)/2],
+//         e:      new_e
+//       };
+//     end else begin
+//       Bit#(`div2(t_)) tHi = truncate(raw >> (`i(b_)+(`i(e_)/2)));
+//       Bit#(`div2(t_)) tLo = truncate(raw >> (`i(e_)/2));
+//       // XXX Bit#(t_) new_t = {tHi, tLo}; XXX simpler provisos with equiv line below
+//       Bit#(t_) new_t = zeroExtend(tLo) | zeroExtend(tHi) << `i(t_)/2;
+//       Bit#(`div2(e_)) eHi = truncate(raw >> `i(b_));
+//       Bit#(`div2(e_)) eLo = truncate(raw);
+//       // XXX Bit#(e_) new_e = {eHi, eLo}; XXX simpler provisos with equiv line below
+//       Bit#(e_) new_e = zeroExtend(eLo) | zeroExtend(eHi) << `i(e_)/2;
+//       return Sealed {
+//         top:    raw[2*`i(b_)-3:`i(b_)+`i(e_)/2+`i(t_)/2],
+//         base:   raw[`i(b_)-1:`i(e_)/2+`i(t_)/2],
+//         otype:  new_t,
+//         e:      new_e
+//       };
+//     end
+//   endfunction
+// endinstance

-// CHERICC capability type
-////////////////////////////////////////////////////////////////////////////////
+// // CHERICC capability type
+// ////////////////////////////////////////////////////////////////////////////////

-`define CCSoftPerms Bit#(4)
-`define AllPermsSz TAdd#(SizeOf#(`CCSoftPerms), SizeOf#(HardPerms))
+// `define CCSoftPerms Bit#(4)
+// `define AllPermsSz TAdd#(SizeOf#(`CCSoftPerms), SizeOf#(HardPerms))

-typedef struct {
-  Bool isCap;
-  `CCSoftPerms softperms;
-  HardPerms hardperms;
-  Bit#(TSub#(addr_, TAdd#(bounds_, `AllPermsSz))) res; // 15 permission bits and bounds_ bits to deduct
-  CHERICCBounds#(`div2(bounds_), e_, t_) bounds;
-  Bit#(addr_) addr;
-} CHERICCCap#(numeric type addr_, numeric type bounds_, numeric type e_, numeric type t_);
+// typedef struct {
+//   Bool isCap;
+//   `CCSoftPerms softperms;
+//   HardPerms hardperms;
+//   Bit#(TSub#(addr_, TAdd#(bounds_, `AllPermsSz))) res; // 15 permission bits and bounds_ bits to deduct
+//   CHERICCBounds#(`div2(bounds_), e_, t_) bounds;
+//   Bit#(addr_) addr;
+// } CHERICCCap#(numeric type addr_, numeric type bounds_, numeric type e_, numeric type t_);

-instance Bits#(CHERICCCap#(addr_, bounds_, e_, t_),
-               TAdd#(1, TAdd#(addr_, TAdd#(bounds_, TAdd#(res_, `AllPermsSz))))) provisos(
-    Bits#(CHERICCBounds#(TDiv#(bounds_, 2), e_, t_), bounds_),
-    Add#(TAdd#(bounds_, `AllPermsSz), res_, addr_)
-  );
-  function pack(cap);
-    Bit#(1)                         isCap = pack(cap.isCap);
-    Bit#(SizeOf#(`CCSoftPerms)) softperms = cap.softperms;
-    Bit#(SizeOf#(HardPerms))    hardperms = pack(cap.hardperms);
-    Bit#(res_)                        res = cap.res;
-    Bit#(bounds_)                  bounds = pack(cap.bounds);
-    Bit#(addr_)                      addr = cap.addr;
-    return {isCap, softperms, hardperms, res, bounds, addr};
-  endfunction
-  //function pack(cap) = {cap.softperms, pack(cap.perms), cap.res, pack(cap.bounds), cap.addr};
-  function unpack(raw) = CHERICCCap {
-    isCap:     unpack(msb(raw)),
-    softperms: raw[2*`i(addr_)-1:2*`i(addr_)-`i(SizeOf#(`CCSoftPerms))],
-    hardperms: unpack(raw[2*`i(addr_)-5:2*`i(addr_)-`i(`AllPermsSz)]),
-    res:       raw[2*`i(addr_)-`i(`AllPermsSz)-1:`i(addr_)+`i(bounds_)],
-    bounds:    unpack(raw[`i(addr_)+`i(bounds_)-1:`i(addr_)]),
-    addr:      raw[`i(addr_)-1:0]
-  };
-endinstance
+// instance Bits#(CHERICCCap#(addr_, bounds_, e_, t_),
+//                TAdd#(1, TAdd#(addr_, TAdd#(bounds_, TAdd#(res_, `AllPermsSz))))) provisos(
+//     Bits#(CHERICCBounds#(TDiv#(bounds_, 2), e_, t_), bounds_),
+//     Add#(TAdd#(bounds_, `AllPermsSz), res_, addr_)
+//   );
+//   function pack(cap);
+//     Bit#(1)                         isCap = pack(cap.isCap);
+//     Bit#(SizeOf#(`CCSoftPerms)) softperms = cap.softperms;
+//     Bit#(SizeOf#(HardPerms))    hardperms = pack(cap.hardperms);
+//     Bit#(res_)                        res = cap.res;
+//     Bit#(bounds_)                  bounds = pack(cap.bounds);
+//     Bit#(addr_)                      addr = cap.addr;
+//     return {isCap, softperms, hardperms, res, bounds, addr};
+//   endfunction
+//   //function pack(cap) = {cap.softperms, pack(cap.perms), cap.res, pack(cap.bounds), cap.addr};
+//   function unpack(raw) = CHERICCCap {
+//     isCap:     unpack(msb(raw)),
+//     softperms: raw[2*`i(addr_)-1:2*`i(addr_)-`i(SizeOf#(`CCSoftPerms))],
+//     hardperms: unpack(raw[2*`i(addr_)-5:2*`i(addr_)-`i(`AllPermsSz)]),
+//     res:       raw[2*`i(addr_)-`i(`AllPermsSz)-1:`i(addr_)+`i(bounds_)],
+//     bounds:    unpack(raw[`i(addr_)+`i(bounds_)-1:`i(addr_)]),
+//     addr:      raw[`i(addr_)-1:0]
+//   };
+// endinstance

-`undef AllPermsSz
-`undef CCSoftPerms
+// `undef AllPermsSz
+// `undef CCSoftPerms

-// CHERICCCap inner helpers
-////////////////////////////////////////////////////////////////////////////////
+// // CHERICCCap inner helpers
+// ////////////////////////////////////////////////////////////////////////////////

-CHERICCCap#(addr_, bounds_, e_, t_) almightyCC = CHERICCCap {
-  isCap: True,
-  softperms: ~0,
-  hardperms: unpack(~0),
-  res: 0,
-  bounds: EmbeddedExp {
-            top:  0, // implied top bits of 01
-            base: 0,
-            // position the 1 of top in the addr_'th bit
-            e:    fromInteger(`i(addr_)-((`i(bounds_)/2)-2))
-          },
-  addr: 0
-};
+// CHERICCCap#(addr_, bounds_, e_, t_) almightyCC = CHERICCCap {
+//   isCap: True,
+//   softperms: ~0,
+//   hardperms: unpack(~0),
+//   res: 0,
+//   bounds: EmbeddedExp {
+//             top:  0, // implied top bits of 01
+//             base: 0,
+//             // position the 1 of top in the addr_'th bit
+//             e:    fromInteger(`i(addr_)-((`i(bounds_)/2)-2))
+//           },
+//   addr: 0
+// };

-CHERICCCap#(addr_, bounds_, e_, t_) nullCC = CHERICCCap {
-  isCap: False,
-  softperms: 0,
-  hardperms: unpack(0),
-  res: 0,
-  bounds: EmbeddedExp {
-            top:  0, // implied top bits of 01
-            base: 0,
-            e:    fromInteger(`i(addr_)-((`i(bounds_)/2)-2)) // position the 1 of top in the addr_'th bit
-          },
-  addr: 0
-};
+// CHERICCCap#(addr_, bounds_, e_, t_) nullCC = CHERICCCap {
+//   isCap: False,
+//   softperms: 0,
+//   hardperms: unpack(0),
+//   res: 0,
+//   bounds: EmbeddedExp {
+//             top:  0, // implied top bits of 01
+//             base: 0,
+//             e:    fromInteger(`i(addr_)-((`i(bounds_)/2)-2)) // position the 1 of top in the addr_'th bit
+//           },
+//   addr: 0
+// };

-function Bit#(e_) getExpCC(CHERICCCap#(addr_, bounds_, e_, t_) cap);
-  case (cap.bounds) matches
-    tagged Exp0 .b: return 0;
-    tagged EmbeddedExp .b: return b.e;
-    tagged Sealed .b: return b.e;
-  endcase
-endfunction
+// function Bit#(e_) getExpCC(CHERICCCap#(addr_, bounds_, e_, t_) cap);
+//   case (cap.bounds) matches
+//     tagged Exp0 .b: return 0;
+//     tagged EmbeddedExp .b: return b.e;
+//     tagged Sealed .b: return b.e;
+//   endcase
+// endfunction

-function Bit#(3) getRepBoundCC(CHERICCCap#(addr_, bounds_, e_, t_) cap)
-  provisos (Add#(3, a__, `div2(bounds_))) =
-  truncateLSB(cap.bounds.Exp0.base) - 3'b001; // always 1/8th of representable space below object
+// function Bit#(3) getRepBoundCC(CHERICCCap#(addr_, bounds_, e_, t_) cap)
+//   provisos (Add#(3, a__, `div2(bounds_))) =
+//   truncateLSB(cap.bounds.Exp0.base) - 3'b001; // always 1/8th of representable space below object

-function Int#(2) getRegionCorrectionCC(Bit#(3) a, Bit#(3) b, Bit#(3) rep) =
-  ((b < rep) == (a < rep)) ? 0 : (((b < rep) && (a >= rep)) ? 1 : -1);
+// function Int#(2) getRegionCorrectionCC(Bit#(3) a, Bit#(3) b, Bit#(3) rep) =
+//   ((b < rep) == (a < rep)) ? 0 : (((b < rep) && (a >= rep)) ? 1 : -1);

-function Bit#(`div2(bounds_))
-  getTopFieldCC(CHERICCCap#(addr_, bounds_, e_, t_) cap);
-  Bit#(2) c_carry = 2'b00;
-  Bit#(2) c_len   = 2'b01;
-  Bit#(`sub2(`div2(bounds_))) partialTop = 0;
-  case (cap.bounds) matches
-    tagged Exp0 .b: begin
-      if (zeroExtend(b.top) < b.base) c_carry = 2'b01;
-      c_len = {1'b0, b.lenMSB};
-      partialTop = b.top;
-    end
-    tagged EmbeddedExp .b: begin
-      if (zeroExtend(b.top) < b.base) c_carry = 2'b01;
-      partialTop = {b.top, 0};
-    end
-    tagged Sealed .b: begin
-      if (zeroExtend(b.top) < b.base) c_carry = 2'b01;
-      partialTop = {b.top, 0};
-    end
-  endcase
-  return {truncateLSB(cap.bounds.Exp0.base) + c_carry + c_len, partialTop};
-endfunction
+// function Bit#(`div2(bounds_))
+//   getTopFieldCC(CHERICCCap#(addr_, bounds_, e_, t_) cap);
+//   Bit#(2) c_carry = 2'b00;
+//   Bit#(2) c_len   = 2'b01;
+//   Bit#(`sub2(`div2(bounds_))) partialTop = 0;
+//   case (cap.bounds) matches
+//     tagged Exp0 .b: begin
+//       if (zeroExtend(b.top) < b.base) c_carry = 2'b01;
+//       c_len = {1'b0, b.lenMSB};
+//       partialTop = b.top;
+//     end
+//     tagged EmbeddedExp .b: begin
+//       if (zeroExtend(b.top) < b.base) c_carry = 2'b01;
+//       partialTop = {b.top, 0};
+//     end
+//     tagged Sealed .b: begin
+//       if (zeroExtend(b.top) < b.base) c_carry = 2'b01;
+//       partialTop = {b.top, 0};
+//     end
+//   endcase
+//   return {truncateLSB(cap.bounds.Exp0.base) + c_carry + c_len, partialTop};
+// endfunction

-function Bit#(`div2(bounds_))
-  getBaseFieldCC(CHERICCCap#(addr_, bounds_, e_, t_) cap) =
-  case (cap.bounds) matches
-    tagged Exp0 .b:         b.base;
-    tagged EmbeddedExp .b: {b.base, 0};
-    tagged Sealed .b:      {b.base, 0};
-  endcase;
+// function Bit#(`div2(bounds_))
+//   getBaseFieldCC(CHERICCCap#(addr_, bounds_, e_, t_) cap) =
+//   case (cap.bounds) matches
+//     tagged Exp0 .b:         b.base;
+//     tagged EmbeddedExp .b: {b.base, 0};
+//     tagged Sealed .b:      {b.base, 0};
+//   endcase;

-// CHERICCCap CHERICap instance
-////////////////////////////////////////////////////////////////////////////////
-instance CHERICap#(CHERICCCap#(addr_, bounds_, e_, t_), t_, addr_) provisos (
-    Add#(3, a__, `div2(bounds_)), // 3 bits of bounds for 1/8th of rep space
-    Add#(3, b__, addr_), // same for addr
-    Add#(c__, TAdd#(2, `div2(bounds_)), addr_), // for base correction
-    Add#(d__, TAdd#(2, `div2(bounds_)), TAdd#(addr_, 1)), // for top 2 bits of Int#(2) correction
-    Add#(e__, `div2(bounds_), addr_), // slice addr into smaller bounds field
-    Add#(f__, `div2(bounds_), TAdd#(addr_, 1)), // same for addr+1
-    Add#(g__, e_, TLog#(TAdd#(1, addr_))) // can fit result of countZerosMSB in e_
-  );
-  //////////////////////////////////////////////////////////////////////////////
-  function isValidCap(cap) = cap.isCap;
-  //////////////////////////////////////////////////////////////////////////////
-  function setValidCap(cap, v);
-    cap.isCap = v;
-    return cap;
-  endfunction
-  //////////////////////////////////////////////////////////////////////////////
-  function getHardPerms(cap) = cap.hardperms;
-  //////////////////////////////////////////////////////////////////////////////
-  function setHardPerms(cap, hardperms);
-    cap.hardperms = hardperms;
-    return cap;
-  endfunction
-  //////////////////////////////////////////////////////////////////////////////
-  function getSoftPerms(cap) = zeroExtend(cap.softperms);
-  //////////////////////////////////////////////////////////////////////////////
-  function setSoftPerms(cap, softperms);
-    cap.softperms = truncate(softperms);
-    return cap;
-  endfunction
-  //////////////////////////////////////////////////////////////////////////////
-  function getKind(cap) = case (cap.bounds) matches
-    tagged Sealed ._: return SEALED_WITH_TYPE;
-    default: return UNSEALED;
-  endcase;
-  //////////////////////////////////////////////////////////////////////////////
-  function getType(cap) = case (cap.bounds) matches
-    tagged Sealed .b: return zeroExtend(b.otype);
-    default: return -1;
-  endcase;
-  //////////////////////////////////////////////////////////////////////////////
-  function setType(cap, otype);
-    let new_cap = cap;
-    let isExact = True;
-    case (cap.bounds) matches
-      tagged Sealed .b: if (otype == -1) begin
-        //Bit#(addr_) addrBits = cap.address >> b.e;
-        //let baseMid = addrBits[`sub1(TAdd#(`div2(t_), `div2(e))):`div2(e_)];
-        //let baseLo  = addrBits[`sub1(`div2(e_)):0];
-        //let topMid  = baseMid;
-        //let topLo   = baseLo;
-        let baseHi = b.base;
-        let  topHi = b.top;
-        if (b.e == 0) new_cap.bounds = Exp0 {
-          lenMSB: 1,
-          top:    {topHi, 0},
-          base:   {baseHi, 0}
-        };
-        else new_cap.bounds = EmbeddedExp {
-          top:  {topHi,  0},
-          base: {baseHi, 0},
-          e:    b.e
-        };
-      end
-      default: if (otype != -1) begin
-        Bit#(e_) new_e = case (cap.bounds) matches
-          tagged EmbeddedExp .b: b.e;
-          default: 0;
-        endcase;
-        new_cap.bounds = Sealed {
-          top:   truncateLSB(cap.bounds.Exp0.top),
-          base:  truncateLSB(cap.bounds.Exp0.base),
-          otype: otype,
-          e:     new_e
-        };
-        Bit#(`div2(t_)) zero = 0;
-        isExact = cap.bounds.Exp0.top[`i(t_)/2-1:0]  == zero &&
-                  cap.bounds.Exp0.base[`i(t_)/2-1:0] == zero;
-      end
-    endcase
-    return Exact{exact: isExact, value: new_cap};
-  endfunction
-  //////////////////////////////////////////////////////////////////////////////
-  function getAddr(cap) = cap.addr;
-  //////////////////////////////////////////////////////////////////////////////
-  function setAddr(cap) = error("setAddr unimplemented");
-  //////////////////////////////////////////////////////////////////////////////
-  function getOffset(cap) = zeroExtend(getAddr(cap)) - getBase(cap);
-  //////////////////////////////////////////////////////////////////////////////
-  function setOffset(cap, offset);
-    Bit#(`div2(bounds_)) e0m = ~(~0 << ((`i(t_)/2)+(`i(e_)/2)));
-    Bit#(TSub#(`div2(bounds_), `div2(e_))) eem = ~(~0 << (`i(t_)/2));
-    // extract specific useful values
-    Bit#(e_) e = getExpCC(cap);
-    Bit#(e_) almighty_e = fromInteger(`i(addr_)-((`i(bounds_)/2)-2)); // position the 1 of top in the addr_'th bit
-    Bit#(addr_) i = offset - getOffset(cap);
-    Bit#(`div2(bounds_)) imid = truncate(i >> e);
-    Bit#(`div2(bounds_)) amid = truncate(cap.addr >> e);
-    Bit#(`div2(bounds_)) r    = {getRepBoundCC(cap), 0};
-    // perform inRange and inLimit tests
-    Bit#(addr_) mask = ~0 << (e + fromInteger(`i(bounds_)/2));
-    Bool inRange  = ((i & mask) == mask) || ((i & mask) == 0);
-    Bool inLimits = (i >= 0) ? imid < (r - amid - 1) :
-                               imid >= (r - amid) && r != amid;
-    Bool isExact = ((inRange && inLimits) || e >= almighty_e);
-    // perform the offset update
-    let new_cap = cap;
-    new_cap.addr = truncate(getBase(cap) + offset);
-    return Exact{exact: isExact, value: new_cap};
-  endfunction
-  //////////////////////////////////////////////////////////////////////////////
-  function getBase(cap);
-    let baseCC = getBaseFieldCC(cap);
-    let e = getExpCC(cap);
-    let correction = getRegionCorrectionCC(truncateLSB(cap.addr),
-                                           truncateLSB(baseCC),
-                                           getRepBoundCC(cap));
-    Bit#(addr_) mask = ~0 << (e + fromInteger(`i(bounds_)/2));
-    Bit#(addr_) acc = cap.addr & mask;
-    return acc + (signExtend({pack(correction), baseCC}) << e);
-  endfunction
-  //////////////////////////////////////////////////////////////////////////////
-  function getTop(cap);
-    let topCC = getTopFieldCC(cap);
-    let e = getExpCC(cap);
-    let correction = getRegionCorrectionCC(truncateLSB(cap.addr),
-                                           truncateLSB(topCC),
-                                           getRepBoundCC(cap));
-    Bit#(TAdd#(addr_, 1)) mask = ~0 << (e + fromInteger(`i(bounds_)/2));
-    Bit#(TAdd#(addr_, 1)) acc = zeroExtend(cap.addr) & mask;
-    return acc + (signExtend({pack(correction), topCC}) << e);
-  endfunction
-  //////////////////////////////////////////////////////////////////////////////
-  function getLength(cap) = getTop(cap) - zeroExtend(getBase(cap));
-  //////////////////////////////////////////////////////////////////////////////
-  function setBounds(cap, length);
-    let new_cap = cap;
-    let isExact = True;
-    // deriving new exponent
-    Bit#(TLog#(TAdd#(1, addr_))) e =
-      pack(fromInteger(`i(addr_))
-      - countZerosMSB(length >> ((`i(bounds_)/2)-1)));
-    // deriving the new base
-    Bit#(`div2(bounds_)) newBase = truncate(cap.addr >> e);
-    // deriving the new top
-    Bit#(TAdd#(addr_, 1)) fullTop = zeroExtend(cap.addr) + zeroExtend(length);
-    Bit#(`div2(bounds_)) newTop = truncate(fullTop >> e);
-    // fold the derived values back in the new cap
-    if (e == 0) begin
-      new_cap.bounds = Exp0 {
-        lenMSB: length[(`i(bounds_)/2)-2],
-        top:    truncate(newTop),
-        base:   newBase
-      };
-    end else begin
-      // slice the top and base values appropriately
-      Bit#(TSub#(`sub2(`div2(bounds_)), `div2(e_))) upperTop = truncateLSB(newTop);
-      Bit#(TSub#(`div2(bounds_), `div2(e_))) upperBase = truncateLSB(newBase);
-      // take care of loss of significant bits in the bits stolen/dropped from fullTop
-      Bit#(TAdd#(addr_, 1)) mask = ~(~0 << (e + fromInteger(`i(e_)/2)));
-      if ((fullTop & mask) != 0) upperTop = upperTop + 1;
-      new_cap.bounds = EmbeddedExp {
-        top:  upperTop,
-        base: upperBase,
-        e:    truncate(e)
-      };
-      // check for exact or not
-      Bit#(addr_) exactMask = ~(~0 << (e - fromInteger(`i(bounds_)/2 - `i(e_)/2 - 1)));
-      if ((cap.addr & exactMask) != 0) isExact = False;
-      if   ((length & exactMask) != 0) isExact = False;
-    end
-    return Exact{exact: isExact, value: new_cap};
-  endfunction
-  //////////////////////////////////////////////////////////////////////////////
-  function nullWithAddr(x);
-    let cap = nullCap;
-    cap.addr = x;
-    return cap;
-  endfunction
-  //////////////////////////////////////////////////////////////////////////////
-  function almightyCap = almightyCC;
-  //////////////////////////////////////////////////////////////////////////////
-  function nullCap = nullCC;
-  //////////////////////////////////////////////////////////////////////////////
-endinstance
+// // CHERICCCap CHERICap instance
+// ////////////////////////////////////////////////////////////////////////////////
+// instance CHERICap#(CHERICCCap#(addr_, bounds_, e_, t_), t_, addr_) provisos (
+//     Add#(3, a__, `div2(bounds_)), // 3 bits of bounds for 1/8th of rep space
+//     Add#(3, b__, addr_), // same for addr
+//     Add#(c__, TAdd#(2, `div2(bounds_)), addr_), // for base correction
+//     Add#(d__, TAdd#(2, `div2(bounds_)), TAdd#(addr_, 1)), // for top 2 bits of Int#(2) correction
+//     Add#(e__, `div2(bounds_), addr_), // slice addr into smaller bounds field
+//     Add#(f__, `div2(bounds_), TAdd#(addr_, 1)), // same for addr+1
+//     Add#(g__, e_, TLog#(TAdd#(1, addr_))) // can fit result of countZerosMSB in e_
+//   );
+//   //////////////////////////////////////////////////////////////////////////////
+//   function isValidCap(cap) = cap.isCap;
+//   //////////////////////////////////////////////////////////////////////////////
+//   function setValidCap(cap, v);
+//     cap.isCap = v;
+//     return cap;
+//   endfunction
+//   //////////////////////////////////////////////////////////////////////////////
+//   function getHardPerms(cap) = cap.hardperms;
+//   //////////////////////////////////////////////////////////////////////////////
+//   function setHardPerms(cap, hardperms);
+//     cap.hardperms = hardperms;
+//     return cap;
+//   endfunction
+//   //////////////////////////////////////////////////////////////////////////////
+//   function getSoftPerms(cap) = zeroExtend(cap.softperms);
+//   //////////////////////////////////////////////////////////////////////////////
+//   function setSoftPerms(cap, softperms);
+//     cap.softperms = truncate(softperms);
+//     return cap;
+//   endfunction
+//   //////////////////////////////////////////////////////////////////////////////
+//   function getKind(cap) = case (cap.bounds) matches
+//     tagged Sealed ._: return SEALED_WITH_TYPE;
+//     default: return UNSEALED;
+//   endcase;
+//   //////////////////////////////////////////////////////////////////////////////
+//   function getType(cap) = case (cap.bounds) matches
+//     tagged Sealed .b: return zeroExtend(b.otype);
+//     default: return -1;
+//   endcase;
+//   //////////////////////////////////////////////////////////////////////////////
+//   function setType(cap, otype);
+//     let new_cap = cap;
+//     let isExact = True;
+//     case (cap.bounds) matches
+//       tagged Sealed .b: if (otype == -1) begin
+//         //Bit#(addr_) addrBits = cap.address >> b.e;
+//         //let baseMid = addrBits[`sub1(TAdd#(`div2(t_), `div2(e))):`div2(e_)];
+//         //let baseLo  = addrBits[`sub1(`div2(e_)):0];
+//         //let topMid  = baseMid;
+//         //let topLo   = baseLo;
+//         let baseHi = b.base;
+//         let  topHi = b.top;
+//         if (b.e == 0) new_cap.bounds = Exp0 {
+//           lenMSB: 1,
+//           top:    {topHi, 0},
+//           base:   {baseHi, 0}
+//         };
+//         else new_cap.bounds = EmbeddedExp {
+//           top:  {topHi,  0},
+//           base: {baseHi, 0},
+//           e:    b.e
+//         };
+//       end
+//       default: if (otype != -1) begin
+//         Bit#(e_) new_e = case (cap.bounds) matches
+//           tagged EmbeddedExp .b: b.e;
+//           default: 0;
+//         endcase;
+//         new_cap.bounds = Sealed {
+//           top:   truncateLSB(cap.bounds.Exp0.top),
+//           base:  truncateLSB(cap.bounds.Exp0.base),
+//           otype: otype,
+//           e:     new_e
+//         };
+//         Bit#(`div2(t_)) zero = 0;
+//         isExact = cap.bounds.Exp0.top[`i(t_)/2-1:0]  == zero &&
+//                   cap.bounds.Exp0.base[`i(t_)/2-1:0] == zero;
+//       end
+//     endcase
+//     return Exact{exact: isExact, value: new_cap};
+//   endfunction
+//   //////////////////////////////////////////////////////////////////////////////
+//   function getAddr(cap) = cap.addr;
+//   //////////////////////////////////////////////////////////////////////////////
+//   function setAddr(cap) = error("setAddr unimplemented");
+//   //////////////////////////////////////////////////////////////////////////////
+//   function getOffset(cap) = zeroExtend(getAddr(cap)) - getBase(cap);
+//   //////////////////////////////////////////////////////////////////////////////
+//   function setOffset(cap, offset);
+//     Bit#(`div2(bounds_)) e0m = ~(~0 << ((`i(t_)/2)+(`i(e_)/2)));
+//     Bit#(TSub#(`div2(bounds_), `div2(e_))) eem = ~(~0 << (`i(t_)/2));
+//     // extract specific useful values
+//     Bit#(e_) e = getExpCC(cap);
+//     Bit#(e_) almighty_e = fromInteger(`i(addr_)-((`i(bounds_)/2)-2)); // position the 1 of top in the addr_'th bit
+//     Bit#(addr_) i = offset - getOffset(cap);
+//     Bit#(`div2(bounds_)) imid = truncate(i >> e);
+//     Bit#(`div2(bounds_)) amid = truncate(cap.addr >> e);
+//     Bit#(`div2(bounds_)) r    = {getRepBoundCC(cap), 0};
+//     // perform inRange and inLimit tests
+//     Bit#(addr_) mask = ~0 << (e + fromInteger(`i(bounds_)/2));
+//     Bool inRange  = ((i & mask) == mask) || ((i & mask) == 0);
+//     Bool inLimits = (i >= 0) ? imid < (r - amid - 1) :
+//                                imid >= (r - amid) && r != amid;
+//     Bool isExact = ((inRange && inLimits) || e >= almighty_e);
+//     // perform the offset update
+//     let new_cap = cap;
+//     new_cap.addr = truncate(getBase(cap) + offset);
+//     return Exact{exact: isExact, value: new_cap};
+//   endfunction
+//   //////////////////////////////////////////////////////////////////////////////
+//   function getBase(cap);
+//     let baseCC = getBaseFieldCC(cap);
+//     let e = getExpCC(cap);
+//     let correction = getRegionCorrectionCC(truncateLSB(cap.addr),
+//                                            truncateLSB(baseCC),
+//                                            getRepBoundCC(cap));
+//     Bit#(addr_) mask = ~0 << (e + fromInteger(`i(bounds_)/2));
+//     Bit#(addr_) acc = cap.addr & mask;
+//     return acc + (signExtend({pack(correction), baseCC}) << e);
+//   endfunction
+//   //////////////////////////////////////////////////////////////////////////////
+//   function getTop(cap);
+//     let topCC = getTopFieldCC(cap);
+//     let e = getExpCC(cap);
+//     let correction = getRegionCorrectionCC(truncateLSB(cap.addr),
+//                                            truncateLSB(topCC),
+//                                            getRepBoundCC(cap));
+//     Bit#(TAdd#(addr_, 1)) mask = ~0 << (e + fromInteger(`i(bounds_)/2));
+//     Bit#(TAdd#(addr_, 1)) acc = zeroExtend(cap.addr) & mask;
+//     return acc + (signExtend({pack(correction), topCC}) << e);
+//   endfunction
+//   //////////////////////////////////////////////////////////////////////////////
+//   function getLength(cap) = getTop(cap) - zeroExtend(getBase(cap));
+//   //////////////////////////////////////////////////////////////////////////////
+//   function setBounds(cap, length);
+//     let new_cap = cap;
+//     let isExact = True;
+//     // deriving new exponent
+//     Bit#(TLog#(TAdd#(1, addr_))) e =
+//       pack(fromInteger(`i(addr_))
+//       - countZerosMSB(length >> ((`i(bounds_)/2)-1)));
+//     // deriving the new base
+//     Bit#(`div2(bounds_)) newBase = truncate(cap.addr >> e);
+//     // deriving the new top
+//     Bit#(TAdd#(addr_, 1)) fullTop = zeroExtend(cap.addr) + zeroExtend(length);
+//     Bit#(`div2(bounds_)) newTop = truncate(fullTop >> e);
+//     // fold the derived values back in the new cap
+//     if (e == 0) begin
+//       new_cap.bounds = Exp0 {
+//         lenMSB: length[(`i(bounds_)/2)-2],
+//         top:    truncate(newTop),
+//         base:   newBase
+//       };
+//     end else begin
+//       // slice the top and base values appropriately
+//       Bit#(TSub#(`sub2(`div2(bounds_)), `div2(e_))) upperTop = truncateLSB(newTop);
+//       Bit#(TSub#(`div2(bounds_), `div2(e_))) upperBase = truncateLSB(newBase);
+//       // take care of loss of significant bits in the bits stolen/dropped from fullTop
+//       Bit#(TAdd#(addr_, 1)) mask = ~(~0 << (e + fromInteger(`i(e_)/2)));
+//       if ((fullTop & mask) != 0) upperTop = upperTop + 1;
+//       new_cap.bounds = EmbeddedExp {
+//         top:  upperTop,
+//         base: upperBase,
+//         e:    truncate(e)
+//       };
+//       // check for exact or not
+//       Bit#(addr_) exactMask = ~(~0 << (e - fromInteger(`i(bounds_)/2 - `i(e_)/2 - 1)));
+//       if ((cap.addr & exactMask) != 0) isExact = False;
+//       if   ((length & exactMask) != 0) isExact = False;
+//     end
+//     return Exact{exact: isExact, value: new_cap};
+//   endfunction
+//   //////////////////////////////////////////////////////////////////////////////
+//   function nullWithAddr(x);
+//     let cap = nullCap;
+//     cap.addr = x;
+//     return cap;
+//   endfunction
+//   //////////////////////////////////////////////////////////////////////////////
+//   function almightyCap = almightyCC;
+//   //////////////////////////////////////////////////////////////////////////////
+//   function nullCap = nullCC;
+//   //////////////////////////////////////////////////////////////////////////////
+// endinstance

-`undef div2
-`undef sub2
-`undef i
+// `undef div2
+// `undef sub2
+// `undef i

-endpackage
+// endpackage
--- a/CHERICC_Fat.bsv
+++ b/CHERICC_Fat.bsv
@@ -40,6 +40,8 @@ export CapPipe;
 export CapFat;
 export MW;
 export OTypeW;
+export Delta;
+export setDeltaValue;
 export FlagsW;
 export Perms;
 export ResW;
@@ -59,8 +61,8 @@ export Exp;
 export MetaInfo;
 export SetBoundsReturn;
 export CapTrim;
-export trimCap;
-export untrimCap;
+// export trimCap;
+// export untrimCap;
 export CapAddr;
 export CapAddrPlus1;

@@ -84,17 +86,20 @@ typedef 0  UPermW;
 typedef 8  MW;
 typedef 6  ExpW;
 typedef 4  OTypeW;
+typedef 24  Delta;
 typedef `FLAGSW FlagsW;
 typedef 32 CapAddrW;
-typedef 64 CapW;
+typedef 88 CapW;
 `else // CAP128 is default
 typedef 4   UPermW;
 typedef 14  MW;
 typedef 6   ExpW;
 typedef 18  OTypeW;
+typedef 52  Delta;
 typedef `FLAGSW FlagsW;
 typedef 64  CapAddrW;
-typedef 128 CapW;
+// The capability width changes
+typedef 180 CapW;
 `endif

 // The Address type is used to represent the full sized address returned to the
@@ -139,8 +144,9 @@ typedef SizeOf#(Perms) PermsW;
 // The reserved bits
 typedef TSub#(CapW, TAdd#( CapAddrW
                         , TAdd#( OTypeW
-                                , TAdd#( CBoundsW
-                                       , TAdd#(PermsW, FlagsW))))) ResW;
+                                , TAdd#( Delta
+                                    , TAdd#( CBoundsW
+                                       , TAdd#(PermsW, FlagsW)))))) ResW;
 // The full capability structure, including the "tag" bit.
 typedef struct {
  Bool         isCapability;
@@ -148,13 +154,15 @@ typedef struct {
  Bit#(ResW)   reserved;
  Bit#(FlagsW) flags;
  Bit#(OTypeW) otype;
+  Bit#(Delta) delta;
  CBounds      bounds;
  CapAddr      address;
 } CapabilityInMemory deriving (Bits, Eq, FShow); // CapW + 1 (tag bit)
 // The full capability structure as Bits, including the "tag" bit.
 typedef Bit#(TAdd#(CapW,1)) Capability;
 // not including the tag bit
-typedef Bit#(CapW) CapBits;
+// Hard-coded
+typedef Bit#(128) CapBits;
 /* TODO
 staticAssert(valueOf(SizeOf#(CapabilityInMemory))==valueOf(SizeOf#(Capability)),
    "The CapabilityInMemory type has incorrect size of " + integerToString(valueOf(SizeOf#(CapabilityInMemory))) + " (CapW = " + integerToString(valueOf(CapW)) + ")"
@@ -183,6 +191,7 @@ typedef struct {
  Bit#(FlagsW)   flags;
  Bit#(ResW)     reserved;
  Bit#(OTypeW)   otype;
+  Bit#(Delta)    delta;
  Format         format;
  Bounds         bounds;
 } CapFat deriving (Bits);
@@ -229,6 +238,7 @@ function CapFat unpackCap(Capability thin);
  fat.flags        = memCap.flags;
  fat.reserved     = memCap.reserved;
  fat.otype        = memCap.otype;
+  fat.delta        = memCap.delta;
  match {.f, .b}   = decBounds(memCap.bounds);
  fat.format       = f;
  fat.bounds       = b;
@@ -252,6 +262,7 @@ function Capability packCap(CapFat fat);
    , flags:        fat.flags
    , reserved:     fat.reserved
    , otype:        fat.otype
+    , delta:        fat.delta
    , bounds:       encBounds(fat.format,fat.bounds)
    , address:      fat.address };
  return pack(thin);
@@ -346,7 +357,7 @@ function BoundsInfo#(CapAddrW) getBoundsInfoFat (CapFat cap, TempFields tf)
  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 =
+  CapAddr length =
    (exp >= resetExp) ? ~0 : zeroExtend (correctTop - correctBase) << exp;

  // compute repBase
@@ -437,12 +448,12 @@ function CapAddrPlus1 getTopFat(CapFat cap, TempFields tf);
    ret[valueOf(CapAddrW)] = ~ret[valueOf(CapAddrW)];
  return ret;
 endfunction
-function CapAddrPlus1 getLengthFat(CapFat cap, TempFields tf);
+function CapAddr getLengthFat(CapFat cap, TempFields tf);
  // Get the top and base bits with the 2 correction bits prepended
  Bit#(TAdd#(MW,2)) top  = {pack(tf.topCorrection),cap.bounds.topBits};
  Bit#(TAdd#(MW,2)) base = {pack(tf.baseCorrection),cap.bounds.baseBits};
  // Get the length by substracting base from top and shifting appropriately
-  CapAddrPlus1 length = zeroExtend(top - base) << cap.bounds.exp;
+  CapAddr length = zeroExtend(top - base) << cap.bounds.exp;
  // Return a saturated length in case of big exponent
  // TODO: The saturation behaviour here is short of being correct
  return (cap.bounds.exp >= resetExp) ? ~0 : length;
@@ -691,6 +702,13 @@ function CapFat unseal(CapFat cap, x _);
  ret.otype = otype_unsealed;
  return ret;
 endfunction
+// TODOD Creating Cap function to all delta value 
+// function CapFat addDelta(CapFat cap, x _);
+//   CapFat ret = cap;
+//   ret.delta = x;
+//   return ret;
+// endfunction
+
 function VnD#(CapFat) incOffsetFat( CapFat cap
                                  , CapAddr pointer
                                  , CapAddr offset // this is the increment in inc offset, and the offset in set offset
@@ -870,6 +888,7 @@ instance DefaultValue #(CapFat);
    , flags       : 0
    , reserved    : 0
    , otype       : otype_unsealed
+    , delta       : 0
    , format      : EmbeddedExp
    , bounds      : defaultValue
    , address     : 0
@@ -882,6 +901,7 @@ CapFat null_cap = CapFat {
  , flags       : 0
  , reserved    : 0
  , otype       : otype_unsealed
+  , delta       : 0
  , format      : EmbeddedExp
  , bounds      : defaultValue
  , address     : 0
@@ -1038,7 +1058,7 @@ typedef struct {
 // Note: commented out methods have a provided default implementation in the
 //       CHERICap typeclass definition

-instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
+instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3), Delta);

  // capability validity
  //////////////////////////////////////////////////////////////////////////////
@@ -1106,6 +1126,7 @@ instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
           , pack (cap.reserved)
           , pack (cap.flags)
           , pack (cap.otype)
+           , pack (cap.delta)
           , pack (cap.bounds) };
  endfunction
  function getAddr (capMem);
@@ -1149,6 +1170,10 @@ instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
  //////////////////////////////////////////////////////////////////////////////
  function setBoundsCombined =
    error ("setBoundsCombined not implemented for CapMem");
+
+  // Create function to set delta value 
+  function setDeltaValue (CapPipe cap, Bit#(Delta) delta) = error ("setDeltaValue 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");
@@ -1196,7 +1221,7 @@ endinstance
 // Note: commented out methods have a provided default implementation in the
 //       CHERICap typeclass definition

-instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
+instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3), Delta);

  // capability validity
  //////////////////////////////////////////////////////////////////////////////
@@ -1320,6 +1345,10 @@ instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
  // capability derivation (bounds set)
  //////////////////////////////////////////////////////////////////////////////
  function setBoundsCombined (cap, length) = error ("setBoundsCombined not implemented for CapReg");
+
+  // Create function to set delta value 
+  function setDeltaValue (CapPipe cap, Bit#(Delta) delta) = error ("setDeltaValue not implemented for CapReg");
+
  //function setBounds = error ("setBounds not implemented for CapReg");
  //function roundLength = error ("roundLength not implemented for CapReg");
  //function alignmentMask = error ("alignmentMask not implemented for CapReg");
@@ -1344,7 +1373,7 @@ instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));

 endinstance

-instance CHERICap #(CapPipe, OTypeW, FlagsW, CapAddrW, CapW, TSub#(MW, 3));
+instance CHERICap #(CapPipe, OTypeW, FlagsW, CapAddrW, CapW, TSub#(MW, 3), Delta);

  //Functions supported by CapReg are just passed through

@@ -1392,11 +1421,21 @@ instance CHERICap #(CapPipe, OTypeW, FlagsW, CapAddrW, CapW, TSub#(MW, 3));
      , mask: result.mask };
  endfunction

+  // Create function to set delta value 
+  function setDeltaValue (CapPipe cap, Bit#(Delta) delta);
+    // let result = setDelta(cap.capFat, delta);
+    cap.capFat.delta = delta;
+    return cap;
+  endfunction
+
+
+
  function nullWithAddr (addr);
    CapReg res = nullWithAddr(addr);
    return CapPipe { capFat: res, tempFields: getTempFields(res) };
  endfunction

+  // A hack to fix compile time check
  function fromMem (capBits);
    CapReg res = fromMem(capBits);
    return CapPipe { capFat: res, tempFields: getTempFields(res) };
@@ -1412,10 +1451,18 @@ instance CHERICap #(CapPipe, OTypeW, FlagsW, CapAddrW, CapW, TSub#(MW, 3));
    return CapPipe { capFat: res, tempFields: getTempFields(res) };
  endfunction

+typedef struct {
+  Bit#(39) trueAddr;
+  Bit#(25) delta;
+} MyAddr deriving (Bits);
+
  //Functions that require TempFields

  function setAddr (cap, address);
-    let result = setAddress(cap.capFat, address, cap.tempFields);
+    // todo
+    MyAddr myAddr = unpack(pack(addr));
+    myAddr.delta = 42;
+    let result = setAddress(cap.capFat, pack(myAddr), cap.tempFields);
    cap.capFat = result.d;
    cap.tempFields = getTempFields(cap.capFat);
    return Exact { exact: result.v, value: cap };
@@ -1518,33 +1565,48 @@ typedef 48 VA_Width;
 typedef struct {
  Perms        perms;
  Bit#(FlagsW) flags;
+  Bit#(Delta)  delta;
  CBounds      bounds;
  Bit#(VA_Width)     address;
  Bool         validAddress;
 } CapTrim deriving(Bits, Eq, FShow);
-function CapTrim  trimCap(CapMem cm);
-  CapabilityInMemory cap = unpack(cm);
-  Bit#(TSub#(CapAddrW,VA_Width)) addr_upper = truncateLSB(cap.address);
-  return CapTrim{perms: cap.perms,
-                 flags: cap.flags,
-                 bounds: cap.bounds,
-                 address: truncate(cap.address),
-                 validAddress: (addr_upper==signExtend(cap.address[valueOf(VA_Width)-1]))
-  };
-endfunction
-function CapMem untrimCap(CapTrim ct);
-  // Encode an invalid address as the bit above the last valid bit being different.
-  Bit#(1) addressMsb = ct.address[valueOf(VA_Width)-1];
-  if (!ct.validAddress) addressMsb = ^addressMsb;
-  return pack(CapabilityInMemory{
-                isCapability: True,
-                perms: ct.perms,
-                reserved: 0,
-                flags: ct.flags,
-                otype: otype_unsealed,
-                bounds: ct.bounds,
-                address: signExtend({addressMsb,ct.address})
-  });
+// function CapTrim  trimCap(CapMem cm);
+//   CapabilityInMemory cap = unpack(cm);
+//   Bit#(TSub#(CapAddrW,VA_Width)) addr_upper = truncateLSB(cap.address);
+//   return CapTrim{perms: cap.perms,
+//                  flags: cap.flags,
+//                  delta: cap.delta,
+//                  bounds: cap.bounds,  
+//                  address: truncate(cap.address),
+//                  validAddress: (addr_upper==signExtend(cap.address[valueOf(VA_Width)-1]))
+//   };
+// endfunction
+// function CapMem untrimCap(CapTrim ct);
+//   // Encode an invalid address as the bit above the last valid bit being different.
+//   Bit#(1) addressMsb = ct.address[valueOf(VA_Width)-1];
+//   if (!ct.validAddress) addressMsb = ^addressMsb;
+//   return pack(CapabilityInMemory{
+//                 isCapability: True,
+//                 perms: ct.perms,
+//                 reserved: 0,
+//                 flags: ct.flags,
+//                 otype: otype_unsealed,
+//                 delta: ct.delta,
+//                 bounds: ct.bounds,
+//                 address: signExtend({addressMsb,ct.address})
+//   });
+// endfunction
+
+// Standalone fromMem wrapper for CapPipe
+function CapPipe fromMemTest(Tuple2#(Bool, Bit#(CapW)) capBits);
+    // capBits.fst = Bool tag
+    // capBits.snd = concatenated bits (e.g., {getAddr(b), getAddr(a)})
+
+    // Reconstruct the underlying CapReg (or CapFat)
+    CapReg res = fromMem(capBits);  
+
+    // Wrap into CapPipe with tempFields
+    return CapPipe { capFat: res, tempFields: getTempFields(res) };
 endfunction

 endpackage
--- a/CHERICap.bsv
+++ b/CHERICap.bsv
@@ -80,7 +80,7 @@ typedef union tagged {
 typedef struct {
  Bit #(addrW) base;
  Bit #(TAdd #(addrW, 1)) top;
-  Bit #(TAdd #(addrW, 1)) length;
+  Bit #(addrW) length;
  Bit #(addrW) repBase;
  Bit #(TAdd #(addrW, 1)) repTop;
  Bit #(TAdd #(addrW, 1)) repLength;
@@ -119,7 +119,7 @@ endfunction

 // XXX TODO augment with all architectural bounds/ repbounds ?
 function Fmt showCHERICap (capT cap)
-  provisos (CHERICap #(capT , otypeW, flgW, addrW, inMemW, maskableW));
+  provisos (CHERICap #(capT , otypeW, flgW, addrW, inMemW, maskableW, delta));
  return $format( "Valid: 0x%0x", isValidCap(cap)) +
         $format(" Perms: 0x%0x", getPerms(cap)) +
         $format(" Kind: ", fshow(getKind(cap))) +
@@ -153,8 +153,9 @@ typeclass CHERICap #( type capT              // type of the CHERICap capability
                    , numeric type addrW     // width of the address
                    , numeric type inMemW    // width of the capability in mem
                    , numeric type maskableW // width of maskable bits
+                    , numeric type delta     // size of delta (tlb bypass)
                    )
-  dependencies (capT determines (otypeW, flgW, addrW, inMemW, maskableW));
+  dependencies (capT determines (otypeW, flgW, addrW, inMemW, maskableW, delta));

  // capability validity
  //////////////////////////////////////////////////////////////////////////////
@@ -258,7 +259,7 @@ typeclass CHERICap #( type capT              // type of the CHERICap capability
  // 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) =
+  function Bit #(addrW) 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) =
@@ -320,6 +321,9 @@ typeclass CHERICap #( type capT              // type of the CHERICap capability
  // the null capability (requires a dummy proxy)
  function capT nullCapFromDummy (capT dummy);

+  // define set delta function
+  function capT setDeltaValue (capT cap, Bit #(delta) length);
+
  // Assert that the encoding is valid
  //////////////////////////////////////////////////////////////////////////////

--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -49,12 +49,18 @@ function Bool implies(Bool x, Bool y) = !x || y;

 function Bool forallBaseAndLen(CapAddr base, CapAddr len,
                                 function Bool prop(CapPipe cap));
-  Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
-  Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
-  return baseCap.exact && implies
-    ( boundedCap.exact 
-    , prop(boundedCap.value)
-    );
+  Bool ret = ?;
+  if (base == 0 && ~len == 0) begin
+    ret = prop(almightyCap);
+  end else begin
+    Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
+    Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
+    ret = baseCap.exact && implies
+      ( boundedCap.exact
+      , prop(boundedCap.value)
+      );
+  end
+  return ret;
 endfunction

 // Furthermore, every valid capability can be reached by calling setAddr on
@@ -107,10 +113,10 @@ function Bool prop_exact(CapAddr base, CapAddr len);
  Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
  Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
  Exact#(CapPipe) baseCap2 = setAddr(almightyCap, getBase(boundedCap.value));
-  CapAddrPlus1 length = getLength(boundedCap.value);
-  Exact#(CapPipe) boundedCap2 = setBounds(baseCap2.value, truncate(length));
+  CapAddr length = getLength(boundedCap.value);
+  Exact#(CapPipe) boundedCap2 = setBounds(baseCap2.value, length);
  return baseCap.exact && baseCap2.exact && implies
-           ( truncateLSB(length) == 1'b0
+           ( ~length != 0
           , boundedCap2.exact
           );
 endfunction
@@ -137,7 +143,8 @@ endfunction

 (* noinline *)
 function Bool prop_getTop(CapAddr base, CapAddr len, CapAddr addr);
-  function prop(cap) = getTop(cap) == zeroExtend(base) + zeroExtend(len);
+  Bool reqAlmighty = ~len == 0;
+  function prop(cap) = getTop(cap) == zeroExtend(base) + (reqAlmighty ? {1'b1, 0} : zeroExtend(len));
  return forallCap(base, len, addr, prop);
 endfunction

@@ -185,4 +192,16 @@ function Bool prop_fromToMem(CapMem in);
  return (cm == in);
 endfunction

+(* noinline *)
+function Bool prop_setBounds(CapAddr base, CapAddr len, CapAddr addr, CapAddr new_len);
+  function prop(cap);
+    let new_cap = setBounds(cap,new_len).value;
+    return implies( isValidCap(new_cap),
+                    getBase(cap) <= getBase(new_cap)
+                    && getTop(cap) >= getTop(new_cap)
+                  );
+  endfunction
+  return forallCap(base, len, addr, prop);
+endfunction
+
 endpackage
--- a/CHERICapWrap.bsv
+++ b/CHERICapWrap.bsv
@@ -74,6 +74,8 @@ function Bit#(CapAddrW) `W(getAddr) (`CAPTYPE cap) = getAddr(cap);
 (* noinline *)
 function `CAPTYPE `W(setAddrUnsafe) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capRet(setAddrUnsafe(capArg(cap), addr));
 (* noinline *)
+function `CAPTYPE `W(addAddrUnsafe) (`CAPTYPE cap, Bit#(TSub #(MW, 3)) inc) = capRet(addAddrUnsafe(capArg(cap), inc));
+(* noinline *)
 function Exact#(`CAPTYPE) `W(setAddr) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capExactRet(setAddr(capArg(cap), addr));
 (* noinline *)
 function Bit#(CapAddrW) `W(getOffset) (`CAPTYPE cap) = getOffset(capArg(cap));
@@ -88,7 +90,7 @@ function Bit#(CapAddrW) `W(getBase) (`CAPTYPE cap) = getBase(capArg(cap));
 (* noinline *)
 function Bit#(TAdd#(CapAddrW, 1)) `W(getTop) (`CAPTYPE cap) = getTop(capArg(cap));
 (* noinline *)
-function Bit#(TAdd#(CapAddrW, 1)) `W(getLength) (`CAPTYPE cap) = getLength(capArg(cap));
+function Bit#(CapAddrW) `W(getLength) (`CAPTYPE cap) = getLength(capArg(cap));
 (* noinline *)
 function Bool `W(isInBounds) (`CAPTYPE cap, Bool isTopIncluded) = isInBounds(capArg(cap), isTopIncluded);
 (* noinline *)
--- a/40
+++ b/40
@@ -1,4 +1,4 @@
-CAP ?= 64
+CAP ?= 128
 ifeq ($(CAP), 128)
 BSCFLAGS = -D CAP128
 else
@@ -13,27 +13,37 @@ ifeq ($(ARCH), RISCV)
 BSCFLAGS += -D RISCV
 endif

+BSV_VERILOG_WRAPPERS_DIR ?= $(CURDIR)/build/
+BUILD_DIR = $(BSV_VERILOG_WRAPPERS_DIR)
+COUNTEREXAMPLE_DIR = $(CURDIR)/counterexamples/
+BSCFLAGS += -bdir $(BUILD_DIR)
+
 all: verilog-wrappers blarney-wrappers

-verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv
-	bsc $(BSCFLAGS) -verilog -u $<
+$(BUILD_DIR):
+	mkdir -p $@

-verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv
-	bsc $(BSCFLAGS) -verilog -u $<
+$(COUNTEREXAMPLE_DIR):
+	mkdir -p $@

-check-prop: assertions.sv verilog-wrappers verilog-props
-	sby -f check.sby
+verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv $(BUILD_DIR)
+	bsc $(BSCFLAGS) -vdir $(BSV_VERILOG_WRAPPERS_DIR) -verilog -u $<

-blarney-wrappers: CHERICapWrap.py verilog-wrappers
-	./CHERICapWrap.py -o CHERIBlarneyWrappers *.v
+verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv $(BUILD_DIR) $(COUNTEREXAMPLE_DIR)
+	bsc $(BSCFLAGS) -vdir $(COUNTEREXAMPLE_DIR) -verilog -u $<

-.PHONY: clean clean-verilog-wrappers
+check-prop: assertions.sv verilog-props $(COUNTEREXAMPLE_DIR)
+	sby --prefix $(COUNTEREXAMPLE_DIR) -f check.sby

-clean-verilog-wrappers: clean
-	rm -f *.v
+blarney-wrappers: CHERICapWrap.py verilog-wrappers $(BUILD_DIR)
+	./CHERICapWrap.py -o $(BUILD_DIR)/CHERIBlarneyWrappers $(BUILD_DIR)/*.v

-clean-blarney-wrappers: clean
-	rm -f *.hs
+.PHONY: clean clean-counterexamples full-clean
+
+clean-counterexamples:
+	rm -rf $(COUNTEREXAMPLE_DIR)

 clean:
-	rm -f *.bo
+	rm -rf $(BUILD_DIR)
+	
+full-clean: clean clean-counterexamples
--- a/assertions.sv
+++ b/assertions.sv
@@ -1,27 +1,27 @@
-module assert_prop_unique(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_newBase,
-         input wire [31 : 0] prop_newLen
-       );
-  wire prop_ok;
+// module assert_prop_unique(
+//          input wire [63 : 0] prop_base,
+//          input wire [63 : 0] prop_len,
+//          input wire [63 : 0] prop_newBase,
+//          input wire [63 : 0] prop_newLen
+//        );
+//   wire prop_ok;

-  module_prop_unique module_prop_unique_inst (
-    .prop_unique_base(prop_base),
-    .prop_unique_len(prop_len),
-    .prop_unique_newBase(prop_newBase),
-    .prop_unique_newLen(prop_newLen),
-    .prop_unique(prop_ok)
-  );
+//   module_prop_unique module_prop_unique_inst (
+//     .prop_unique_base(prop_base),
+//     .prop_unique_len(prop_len),
+//     .prop_unique_newBase(prop_newBase),
+//     .prop_unique_newLen(prop_newLen),
+//     .prop_unique(prop_ok)
+//   );

-  always @(*) begin
-    assert(prop_ok);
-  end
-endmodule
+//   always @(*) begin
+//     assert(prop_ok);
+//   end
+// endmodule

 module assert_prop_exact(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len
       );
  wire prop_ok;

@@ -37,8 +37,8 @@ module assert_prop_exact(
 endmodule

 module assert_prop_exactConditions(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len
       );
  wire prop_ok;

@@ -54,8 +54,8 @@ module assert_prop_exactConditions(
 endmodule

 module assert_prop_getBase(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len
       );
  wire prop_ok;

@@ -71,9 +71,9 @@ module assert_prop_getBase(
 endmodule

 module assert_prop_getTop(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_addr
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr
       );
  wire prop_ok;

@@ -90,9 +90,9 @@ module assert_prop_getTop(
 endmodule

 module assert_prop_getLength(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_addr,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_addr,
+         input wire [63 : 0] prop_len
       );
  wire prop_ok;

@@ -109,9 +109,9 @@ module assert_prop_getLength(
 endmodule

 module assert_prop_isInBounds(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_addr
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr
       );
  wire prop_ok;

@@ -128,9 +128,9 @@ module assert_prop_isInBounds(
 endmodule

 module assert_prop_setAddr(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_addr
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr
       );
  wire prop_ok;

@@ -160,3 +160,24 @@ module assert_prop_fromToMem(
    assert(prop_ok);
  end
 endmodule
+
+module assert_prop_setBounds(
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr,
+         input wire [63 : 0] prop_new_len
+       );
+  wire prop_ok;
+
+  module_prop_setBounds module_prop_setBounds_inst(
+    .prop_setBounds_base(prop_base),
+    .prop_setBounds_len(prop_len),
+    .prop_setBounds_addr(prop_addr),
+    .prop_setBounds_new_len(prop_new_len),
+    .prop_setBounds(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule
--- a/check.sby
+++ b/check.sby
@@ -8,6 +8,7 @@ prop_getLength
 prop_isInBounds
 prop_setAddr
 prop_fromToMem
+prop_setBounds

 [options]
 depth 1
@@ -27,6 +28,7 @@ read -formal module_prop_getLength.v
 read -formal module_prop_isInBounds.v
 read -formal module_prop_setAddr.v
 read -formal module_prop_fromToMem.v
+read -formal module_prop_setBounds.v
 prop_getBase: prep -top assert_prop_getBase
 prop_getTop: prep -top assert_prop_getTop
 prop_getLength: prep -top assert_prop_getLength
@@ -36,15 +38,16 @@ prop_exact: prep -top assert_prop_exact
 prop_exactConditions: prep -top assert_prop_exactConditions
 prop_setAddr: prep -top assert_prop_setAddr
 prop_fromToMem: prep -top assert_prop_fromToMem
+prop_setBounds: prep -top assert_prop_setBounds

 [files]
 assertions.sv
-module_prop_unique.v
-module_prop_exact.v
-module_prop_exactConditions.v
-module_prop_getBase.v
-module_prop_getTop.v
-module_prop_getLength.v
-module_prop_isInBounds.v
-module_prop_setAddr.v
-module_prop_fromToMem.v
+counterexamples/module_prop_unique.v
+counterexamples/module_prop_exact.v
+counterexamples/module_prop_exactConditions.v
+counterexamples/module_prop_getBase.v
+counterexamples/module_prop_getTop.v
+counterexamples/module_prop_getLength.v
+counterexamples/module_prop_isInBounds.v
+counterexamples/module_prop_setAddr.v
+counterexamples/module_prop_fromToMem.v
--- a/flake.lock
+++ b/flake.lock
@@ -0,0 +1,61 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1738579205,
+        "narHash": "sha256-o6BeeanSUALvz8oL2CHOikVjCf7j+HqlA0WGvKOUX3Q=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "be5cf18b3d26ba2db938a72ade93ac8a9a7462ff",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "release-24.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
--- a/flake.nix
+++ b/flake.nix
@@ -0,0 +1,25 @@
+{
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/release-24.11";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let # helper bindings
+        # imported nix packages
+        pkgs = import nixpkgs { inherit system; };
+        # shell environment
+        dfltShell = pkgs.mkShell {
+          buildInputs = with pkgs; [
+            sby
+            boolector
+            haskellPackages.sv2v
+            bluespec
+          ];
+        };
+      # output attribute set
+      in {
+        devShells.default = dfltShell;
+      }
+    );
+}
Author	SHA1	Message	Date
Akilan	b772286261	saving current changes Some checks failed check properties / tests (push) Has been cancelled Details	2026-02-23 11:44:35 +00:00
Akilan	f7884bb932	hack changes Some checks failed check properties / tests (push) Has been cancelled Details	2026-02-20 01:59:12 +00:00
Akilan	bd95a8b5b1	saving current changes cheri-cap-lib Some checks failed check properties / tests (push) Has been cancelled Details	2026-02-19 18:07:45 +00:00
Akilan	ed366654f0	saved compile time errors Some checks failed check properties / tests (push) Has been cancelled Details	2026-02-17 15:34:56 +00:00
Akilan	b8f7b51e8a	added latest changes	2026-02-17 14:49:00 +00:00
Akilan	76d832bcaf	merge conflict resovled Some checks failed check properties / tests (push) Has been cancelled Details	2026-02-17 14:26:25 +00:00
Akilan	b7892c3abc	added changes	2026-02-17 14:22:33 +00:00
Akilan	dc9fc2bd7d	added delta value field	2026-02-17 13:49:05 +00:00
Jonathan Woodruff	1d2c0b953b	Add a property that setBounds will only return a valid cap if the bounds are within the original bounds. Some checks failed check properties / tests (push) Has been cancelled Details	2025-03-07 15:12:46 +00:00
Peter Rugg	199e3c9f7f	Extend forallCap to include almightyCap	2025-03-04 14:49:41 +00:00
Peter Rugg	7c9559524b	Increase bit-widths of assertion modules These were hardwired for RV64, but I'm assuming having too many bits will not be a problem for RV32?	2025-03-04 14:49:41 +00:00
Peter Rugg	bad0d9cdb6	Default to 128-bit caps	2025-03-04 14:49:41 +00:00
Peter Rugg	c5da2ebc5d	Move to building untracked files in subdirectories to improve cleaning	2025-03-04 14:49:41 +00:00
Alexandre Joannou	595447fd62	fix property following getLength return type change in `b3896e4e50`	2025-02-10 17:44:09 +00:00
Alexandre Joannou	2295c3b8c0	Added addAddrUnsafe verilog wrapper	2025-02-05 12:28:19 +00:00
Jonathan Woodruff	b3896e4e50	Move getLength to address length (not address length + 1), as we're explicitly saturating in order to express as a normal address.	2025-02-04 16:31:01 +00:00
Alexandre Joannou	3926b793bf	Added an env var to control bsc vdir flag	2025-02-04 12:22:21 +00:00
Alexandre Joannou	9e0636e6fc	Added test workflow	2025-02-04 11:10:09 +00:00