Add a new property that encoding and decoding a memory capability gives the same result. This caught the most recent bug.

CHERICapProps.bsv

@@ -178,4 +178,11 @@ function Bool prop_isInBounds(CapAddr base, CapAddr len, CapAddr addr);
   return forallCap(base, len, addr, prop);
 endfunction
 
+(* noinline *)
+function Bool prop_fromToMem(CapMem in);
+  CapPipe cp = fromMem(unpack(in));
+  CapMem cm = pack(toMem(cp));
+  return (cm == in);
+endfunction
+
 endpackage

assertions.sv

@@ -145,3 +145,18 @@ module assert_prop_setAddr(
     assert(prop_ok);
   end
 endmodule
+
+module assert_prop_fromToMem(
+         input wire [128 : 0] prop_in,
+       );
+  wire prop_ok;
+
+  module_prop_fromToMem module_fromToMem(
+    .prop_fromToMem_in(prop_in),
+    .prop_fromToMem(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule

check.sby

@@ -7,6 +7,7 @@ prop_getTop
 prop_getLength
 prop_isInBounds
 prop_setAddr
+prop_fromToMem
 
 [options]
 depth 1
@@ -25,6 +26,7 @@ read -formal module_prop_getTop.v
 read -formal module_prop_getLength.v
 read -formal module_prop_isInBounds.v
 read -formal module_prop_setAddr.v
+read -formal module_prop_fromToMem.v
 prop_getBase: prep -top assert_prop_getBase
 prop_getTop: prep -top assert_prop_getTop
 prop_getLength: prep -top assert_prop_getLength
@@ -33,6 +35,7 @@ prop_unique: prep -top assert_prop_unique
 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
 
 [files]
 assertions.sv
@@ -44,3 +47,4 @@ module_prop_getTop.v
 module_prop_getLength.v
 module_prop_isInBounds.v
 module_prop_setAddr.v
+module_prop_fromToMem.v