Add a property that setBounds will only return a valid cap if the bounds are within the original bounds.

These were hardwired for RV64, but I'm assuming having too many
bits will not be a problem for RV32?

.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

.gitignore

@@ -0,0 +1,2 @@
+build/
+counterexamples/

CHERICC_Fat.bsv

@@ -346,7 +346,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 +437,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;

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;
@@ -258,7 +258,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) =

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

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 *)

Makefile

@@ -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

assertions.sv

@@ -1,8 +1,8 @@
 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
+         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;
 
@@ -20,8 +20,8 @@ module assert_prop_unique(
 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

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,17 @@ 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
+counterexamples/module_prop_setBounds.v

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
+}

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;
+      }
+    );
+}