Further CHERI implementation. Rename cursor to offset in line with ISA. Implement reserved cap. perms (bits 8 and 9) because a test uses them even though they have no defined meaning (historically they did I think).

2 files changed, 625 insertions, 23 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 5af600ef..c7c51f75 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -18,11 +18,11 @@ function clause execute (CGetX(op, rd, cb)) =
       {
         cbval    := CapRegs[cb];
         wGPR(rd) := switch(op) {
-          case CGetPerm     -> EXTZ(cbval[223..193])
+          case CGetPerm     -> EXTZ(cbval[223..193])  (* XXX only correct for 256-bit *)
           case CGetType     -> EXTZ(cbval.otype)
           case CGetBase     -> cbval.base
-          case CGetOffset   -> cbval.cursor
-          case CGetLen      -> cbval.length (* XXX only correct for 256-bit *)
+          case CGetOffset   -> cbval.offset
+          case CGetLen      -> cbval.length
           case CGetTag      -> EXTZ([cbval.tag])
           case CGetUnsealed -> EXTZ([cbval.sealed])
         }
@@ -38,7 +38,7 @@ function clause execute (CGetPCC(cd)) =
         exit (raise_c2_exception_v(cd))
       else
         let pcc = (capRegToCapStruct(PCC)) in
-        writeCapReg(cd, {pcc with cursor = PC})
+        writeCapReg(cd, {pcc with offset = PC})
     }
 (* Get and Set CP2 cause register *)
 
@@ -66,7 +66,7 @@ function clause execute (CSetCause((regno) rt)) =
         }
     }
 
-union ast member (regno, regno, regno) CAndPerm
+union ast member regregreg CAndPerm
 function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CAndPerm(cd, cb, rt))
 function clause execute(CAndPerm(cd, cb, rt)) = 
 {
@@ -78,7 +78,7 @@ function clause execute(CAndPerm(cd, cb, rt)) =
     exit (raise_c2_exception_v(cb))
   else if (~(cb_val.tag)) then
     exit (raise_c2_exception(CapEx_TagViolation, cb))
-  else if (~(cb_val.sealed)) then
+  else if (cb_val.sealed) then
     exit (raise_c2_exception(CapEx_SealViolation, cb))
   else
     {
@@ -89,6 +89,8 @@ function clause execute(CAndPerm(cd, cb, rt)) =
         access_KCC                 = (cb_val.access_KCC                 & (rt_val[12]));
         access_KDC                 = (cb_val.access_KDC                 & (rt_val[11]));
         access_EPCC                = (cb_val.access_EPCC                & (rt_val[10]));
+        perm_reserved9             = (cb_val.perm_reserved9             & (rt_val[9]));
+        perm_reserved8             = (cb_val.perm_reserved8             & (rt_val[8]));
         permit_seal                = (cb_val.permit_seal                & (rt_val[7]));
         permit_store_ephemeral_cap = (cb_val.permit_store_ephemeral_cap & (rt_val[6]));
         permit_store_cap           = (cb_val.permit_store_cap           & (rt_val[5]));
@@ -101,3 +103,529 @@ function clause execute(CAndPerm(cd, cb, rt)) =
     }
 }
 
+union ast member regregreg CToPtr
+function clause decode (0b010010 : 0b01100 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CToPtr(rd, cb, ct))
+function clause execute(CToPtr(rd, cb, ct)) = 
+{
+  ct_val := readCapReg(ct);
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (register_inaccessible(ct)) then
+    exit (raise_c2_exception_v(ct))
+  else if (~(ct_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, ct))
+  else 
+    {
+      wGPR(rd) := if (~(cb_val.tag)) then
+          ((bit[64]) 0)
+        else
+          (bit[64])(((nat)(cb_val.base)) + ((nat) (cb_val.offset)) - ((nat)(ct_val.base)))
+    }
+}
+
+union ast member (regno, regno, regno, CPtrCmpOp) CPtrCmp
+function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CPtrCmp(rd, cb, ct, CEQ))
+function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b001) = Some(CPtrCmp(rd, cb, ct, CNE))
+function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b010) = Some(CPtrCmp(rd, cb, ct, CLT))
+function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b011) = Some(CPtrCmp(rd, cb, ct, CLE))
+function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b100) = Some(CPtrCmp(rd, cb, ct, CLTU))
+function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b101) = Some(CPtrCmp(rd, cb, ct, CLEU))
+function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b110) = Some(CPtrCmp(rd, cb, ct, CEXEQ))
+
+function clause execute(CPtrCmp(rd, cb, ct, op)) = 
+{
+  if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (register_inaccessible(ct)) then
+    exit (raise_c2_exception_v(ct))
+  else 
+    {
+      cb_val := readCapReg(cb);
+      ct_val := readCapReg(ct);
+      equal  := false;
+      ltu    := false;
+      lts    := false;
+      if (cb_val.tag != ct_val.tag) then
+        {
+          if (cb_val.tag) then
+            {
+              ltu := true;
+              lts := true;
+            }
+        }
+      else
+        {
+          cursor1 := getCapCursor(cb_val);
+          cursor2 := getCapCursor(ct_val);
+          equal   := (cursor1 == cursor2);
+          ltu     := (cursor1 < cursor2);
+          lts     := (cursor1 <_s cursor2);
+        };
+      wGPR(rd) := EXTZ(switch (op) {
+        case CEQ   -> [equal]
+        case CNE   -> [~(equal)]
+        case CLT   -> [lts]
+        case CLE   -> [lts | equal]
+        case CLTU  -> [ltu]
+        case CLEU  -> [lts | equal]
+        case CEXEQ -> [cb_val == ct_val]
+      })
+    }
+}
+
+union ast member regregreg CIncOffset
+function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CIncOffset(cd, cb, rt))
+function clause execute (CIncOffset(cd, cb, rt)) =
+    {
+      cb_val := readCapReg(cb);
+      rt_val := rGPR(rt);
+      if (register_inaccessible(cd)) then
+        exit (raise_c2_exception_v(cd))
+      else if (register_inaccessible(cb)) then
+        exit (raise_c2_exception_v(cb))
+      else if ((cb_val.tag) & (cb_val.sealed) & (rt_val != 0)) then
+        exit (raise_c2_exception(CapEx_SealViolation, cb))
+      else
+        writeCapReg(cd, {cb_val with offset=cb_val.offset+rt_val})
+    }
+
+union ast member regregreg CSetOffset
+function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b001) = Some(CSetOffset(cd, cb, rt))
+function clause execute (CSetOffset(cd, cb, rt)) =
+    {
+      cb_val := readCapReg(cb);
+      rt_val := rGPR(rt);
+      if (register_inaccessible(cd)) then
+        exit (raise_c2_exception_v(cd))
+      else if (register_inaccessible(cb)) then
+        exit (raise_c2_exception_v(cb))
+      else if ((cb_val.tag) & (cb_val.sealed)) then
+        exit (raise_c2_exception(CapEx_SealViolation, cb))
+      else
+        writeCapReg(cd, {cb_val with offset=rt_val})
+    }
+
+union ast member regregreg CSetBounds
+function clause decode (0b010010 : 0b00001 : (regno) cd : (regno) cb : (regno) rt : 0b000000) = Some(CSetBounds(cd, cb, rt))
+function clause execute (CSetBounds(cd, cb, rt)) =
+    {
+      cb_val := readCapReg(cb);
+      (nat) rt_val := rGPR(rt);
+      (nat) cursor := getCapCursor(cb_val);
+      if (register_inaccessible(cd)) then
+        exit (raise_c2_exception_v(cd))
+      else if (register_inaccessible(cb)) then
+        exit (raise_c2_exception_v(cb))
+      else if (~(cb_val.tag)) then
+        exit (raise_c2_exception(CapEx_TagViolation, cb))
+      else if (cb_val.sealed) then
+        exit (raise_c2_exception(CapEx_SealViolation, cb))
+      else if (cursor < ((nat)(cb_val.base))) then
+        exit (raise_c2_exception(CapEx_LengthViolation, cb))
+      else if ((cursor + rt_val) > ((nat)(cb_val.base) + (nat)(cb_val.length))) then
+        exit (raise_c2_exception(CapEx_LengthViolation, cb))
+      else
+        writeCapReg(cd, {cb_val with base=(bit[64])cursor; length=(bit[64])rt_val; offset=0})
+    }
+
+union ast member (regno, regno) CClearTag
+function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : 0b00000 : 0b000: 0b101) = Some(CClearTag(cd, cb))
+function clause execute (CClearTag(cd, cb)) =
+    {
+      if (register_inaccessible(cd)) then
+        exit (raise_c2_exception_v(cd))
+      else if (register_inaccessible(cb)) then
+        exit (raise_c2_exception_v(cb))
+      else
+        {
+          cb_val := readCapReg(cb);
+          writeCapReg(cd, {cb_val with tag = false});
+        }
+    }
+
+union ast member (ClearRegSet, bit[16]) ClearRegs
+function clause decode (0b010010 : 0b01111 : 0b00000 : (bit[16]) imm) = Some(ClearRegs(GPLo, imm)) (* ClearLo *)
+function clause decode (0b010010 : 0b01111 : 0b00001 : (bit[16]) imm) = Some(ClearRegs(GPHi, imm)) (* ClearHi *)
+function clause decode (0b010010 : 0b01111 : 0b00010 : (bit[16]) imm) = Some(ClearRegs(CLo, imm))  (* CClearLo *)
+function clause decode (0b010010 : 0b01111 : 0b00011 : (bit[16]) imm) = Some(ClearRegs(CHi, imm))  (* CClearHi *)
+function clause execute (ClearRegs(regset, mask)) =
+{
+  if (regset == CHi) then
+    ()(* XXX check exception *);
+  foreach (i from 0 to 15)
+    if (mask[i]) then
+      switch (regset) {
+        case GPLo -> wGPR((bit[5])i) := 0
+        case GPHi -> wGPR((bit[5])(i+16)) := 0
+        case CLo  -> writeCapReg((bit[5]) i) := null_cap
+        case CHi  -> writeCapReg((bit[5]) (i+16)) := null_cap
+      }
+}
+
+union ast member regregreg CFromPtr
+function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000: 0b111) = Some(CFromPtr(cd, cb, rt))
+function clause execute (CFromPtr(cd, cb, rt)) =
+    {
+      cb_val := readCapReg(cb);
+      rt_val := rGPR(rt);
+      if (register_inaccessible(cd)) then
+        exit (raise_c2_exception_v(cd))
+      else if (register_inaccessible(cb)) then
+        exit (raise_c2_exception_v(cb))
+      else if (rt == 0) then
+        writeCapReg(cd, null_cap)
+      else if (~(cb_val.tag)) then
+        exit (raise_c2_exception(CapEx_TagViolation, cb))
+      else if (cb_val.sealed) then
+        exit (raise_c2_exception(CapEx_SealViolation, cb))
+      else
+        writeCapReg(cd, {cb_val with offset = rt_val});
+    }
+
+union ast member (regno, regno) CCheckPerm
+function clause decode (0b010010 : 0b01011 : (regno) cs : 0b00000 : (regno) rt : 0b000: 0b000) = Some(CCheckPerm(cs, rt))
+function clause execute (CCheckPerm(cs, rt)) =
+    {
+      cs_val := readCapReg(cs);
+      cs_perms := capPermsToVec(cs_val);
+      rt_perms := (rGPR(rt))[30..0];
+      if (register_inaccessible(cs)) then
+        exit (raise_c2_exception_v(cs))
+      else if (~(cs_val.tag)) then
+        exit (raise_c2_exception(CapEx_TagViolation, cs))
+      else if ((cs_perms & rt_perms) != rt_perms) then
+        exit (raise_c2_exception(CapEx_UserDefViolation, cs))
+    }
+
+union ast member (regno, regno) CCheckType
+function clause decode (0b010010 : 0b01011 : (regno) cs : (regno) cb : 0b00000 : 0b000: 0b001) = Some(CCheckType(cs, cb))
+function clause execute (CCheckType(cs, cb)) =
+{
+  cs_val := readCapReg(cs);
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cs)) then
+    exit (raise_c2_exception_v(cs))
+  else if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (~(cs_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cs))
+  else if (~(cb_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cb))
+  else if (~(cs_val.sealed)) then
+    exit (raise_c2_exception(CapEx_SealViolation, cs))
+  else if (~(cb_val.sealed)) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else if ((cs_val.otype) != (cb_val.otype)) then
+    exit (raise_c2_exception(CapEx_TypeViolation, cs))
+}
+
+union ast member regregreg CSeal
+function clause decode (0b010010 : 0b00010 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CSeal(cd, cs, ct))
+function clause execute (CSeal(cd, cs, ct)) =
+{
+  cs_val := readCapReg(cs);
+  ct_val := readCapReg(ct);
+  (nat) ct_cursor := ((nat)(ct_val.base) + (nat)(ct_val.offset));
+  if (register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else if (register_inaccessible(cs)) then
+    exit (raise_c2_exception_v(cs))
+  else if (register_inaccessible(ct)) then
+    exit (raise_c2_exception_v(ct))
+  else if (~(cs_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cs))
+  else if (~(ct_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, ct))
+  else if (cs_val.sealed) then
+    exit (raise_c2_exception(CapEx_SealViolation, cs))
+  else if (ct_val.sealed) then
+    exit (raise_c2_exception(CapEx_SealViolation, ct))
+  else if (~(ct_val.permit_seal)) then
+    exit (raise_c2_exception(CapEx_PermitSealViolation, ct))
+  else if ((ct_val.offset) >= (ct_val.length)) then
+    exit (raise_c2_exception(CapEx_LengthViolation, ct))
+  else if (ct_cursor > max_otype) then
+    exit (raise_c2_exception(CapEx_LengthViolation, ct))
+  else
+    writeCapReg(cd, {cs_val with sealed=true; otype=((bit[24])ct_cursor)})
+}
+
+union ast member regregreg CUnseal
+function clause decode (0b010010 : 0b00011 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CUnseal(cd, cs, ct))
+function clause execute (CUnseal(cd, cs, ct)) =
+{
+  cs_val := readCapReg(cs);
+  ct_val := readCapReg(ct);
+  (nat) ct_cursor := ((nat)(ct_val.base) + (nat)(ct_val.offset));
+  if (register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else if (register_inaccessible(cs)) then
+    exit (raise_c2_exception_v(cs))
+  else if (register_inaccessible(ct)) then
+    exit (raise_c2_exception_v(ct))
+  else if (~(cs_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cs))
+  else if (~(ct_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, ct))
+  else if (~(cs_val.sealed)) then
+    exit (raise_c2_exception(CapEx_SealViolation, cs))
+  else if (ct_val.sealed) then
+    exit (raise_c2_exception(CapEx_SealViolation, ct))
+  else if (ct_cursor != ((nat)(cs_val.otype))) then
+    exit (raise_c2_exception(CapEx_TypeViolation, ct))
+  else if (~(ct_val.permit_seal)) then
+    exit (raise_c2_exception(CapEx_PermitSealViolation, ct))
+  else if ((ct_val.offset) >= (ct_val.length)) then
+    exit (raise_c2_exception(CapEx_LengthViolation, ct))
+  else
+    writeCapReg(cd, {cs_val with 
+      sealed=false; 
+      otype=0;
+      non_ephemeral=(cs_val.non_ephemeral & ct_val.non_ephemeral)
+    })
+}
+
+union ast member (regno, regno) CCall
+function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb))
+function clause execute (CCall(cs, cb)) =
+{
+  (* Partial implementation of CCall with checks in hardware, but raising a trap to perform trusted stack manipulation *)
+  cs_val := readCapReg(cs);
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cs)) then
+    exit (raise_c2_exception_v(cs))
+  else if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (~(cs_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cs))
+  else if (~(cb_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cb))
+  else if (~(cs_val.sealed)) then
+    exit (raise_c2_exception(CapEx_SealViolation, cs))
+  else if (~(cb_val.sealed)) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else if ((cs_val.otype) != (cb_val.otype)) then
+    exit (raise_c2_exception(CapEx_TypeViolation, cs))
+  else if (~(cs_val.permit_execute)) then
+    exit (raise_c2_exception(CapEx_PermitExecuteViolation, cs))
+  else if (cb_val.permit_execute) then
+    exit (raise_c2_exception(CapEx_PermitExecuteViolation, cb))
+  else if (cs_val.offset >= cs_val.length) then
+    exit (raise_c2_exception(CapEx_LengthViolation, cs))
+  else
+    exit (raise_c2_exception_noreg(CapEx_CallTrap));
+}
+
+union ast member unit CReturn
+function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn)
+function clause execute (CReturn) =
+    exit (raise_c2_exception_noreg(CapEx_ReturnTrap))
+
+union ast member (regno, bit[16], bool) CBX
+function clause decode (0b010010 : 0b01001 : (regno) cb : (bit[16]) imm) = Some(CBX(cb, imm, true)) (* CBTU *)
+function clause decode (0b010010 : 0b01010 : (regno) cb : (bit[16]) imm) = Some(CBX(cb, imm, false)) (* CBTS *)
+
+function clause execute (CBX(cb, imm, invert)) =
+{
+  if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (((CapRegs[cb]).tag) ^ invert) then
+    {
+      let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
+      delayedPC     := PC + offset;
+      branchPending := 1;
+    }
+}
+
+union ast member (regno, regno, bool) CJALR
+function clause decode (0b010010 : 0b00111 : (regno) cd : (regno) cb : 0b00000 : 0b000000) = Some(CJALR(cd, cb, true)) (* CJALR *)
+function clause decode (0b010010 : 0b01000 : 0b00000    : (regno) cb : 0b00000 : 0b000000) = Some(CJALR(0b00000, cb, false)) (* CJR *)
+function clause execute(CJALR(cd, cb, link)) = 
+{
+  cb_val := readCapReg(cb);
+  if (link & register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (~(cb_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cb))
+  else if (cb_val.sealed) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else if (~(cb_val.permit_execute)) then
+    exit (raise_c2_exception(CapEx_PermitExecuteViolation, cb))
+  else if (~(cb_val.non_ephemeral)) then
+    exit (raise_c2_exception(CapEx_GlobalViolation, cb))
+  else if (((nat)(cb_val.offset)) + 4 > ((nat) (cb_val.length))) then
+    exit (raise_c2_exception(CapEx_LengthViolation, cb))
+  else if (((cb_val.base+cb_val.offset)[1..0]) != 0b00) then
+    exit (SignalException(AdEL))
+  else
+    {
+      if (link) then
+        writeCapReg(cd, {capRegToCapStruct(PCC) with offset=(PC+8)});
+      delayedPC := cb_val.offset;
+      delayedPCC := capStructToBit257(cb_val);
+      branchPending := 1;
+    }
+}
+
+union ast member (regno, regno, regno, bit[8], bool, WordType) CLoad
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CLoad(rd, cb, rt, offset, false, B)) (* CLB *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b00) = Some(CLoad(rd, cb, rt, offset, true,  B)) (* CLBU *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b01) = Some(CLoad(rd, cb, rt, offset, false, H)) (* CLH *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b01) = Some(CLoad(rd, cb, rt, offset, true,  H)) (* CLHU *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b10) = Some(CLoad(rd, cb, rt, offset, false, W)) (* CLW *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b10) = Some(CLoad(rd, cb, rt, offset, true,  W)) (* CLWU *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b11) = Some(CLoad(rd, cb, rt, offset, false, D)) (* CLD *)
+(*function clause decode (0b010000 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b11) = Some(CLoad(rd, cb, rt, offset, true,  D)) (* CLD *)*)
+function clause execute (CLoad(rd, cb, rt, offset, signed, width)) =
+  {
+    cb_val := readCapReg(cb);
+    if (register_inaccessible(cb)) then
+      exit (raise_c2_exception_v(cb))
+    else if (~(cb_val.tag)) then
+      exit (raise_c2_exception(CapEx_TagViolation, cb))
+    else if (cb_val.sealed) then
+      exit (raise_c2_exception(CapEx_SealViolation, cb))
+    else if (~(cb_val.permit_load)) then
+      exit (raise_c2_exception(CapEx_PermitLoadViolation, cb))
+    else
+      {
+        size   := wordWidthBytes(width);
+        cursor := getCapCursor(cb_val);
+        vAddr  := cursor + (int) (rGPR(rt)) + (int) offset;
+        vAddr64:= (bit[64]) vAddr;
+        if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
+          exit (raise_c2_exception(CapEx_LengthViolation, cb))
+        else if (vAddr < ((nat) (cb_val.base))) then
+          exit (raise_c2_exception(CapEx_LengthViolation, cb))
+        else if ~(isAddressAligned(vAddr64, width)) then
+          exit (SignalExceptionBadAddr(AdEL, vAddr64))
+        else
+          {
+            pAddr      := (TranslateOrExit(vAddr64, LoadData));
+            memResult  := MEMr(pAddr, wordWidthBytes(width));
+            if (signed) then
+              wGPR(rt) := EXTS(memResult)
+            else
+              wGPR(rt) := EXTZ(memResult)
+          }
+      }
+  }
+
+union ast member (regno, regno, regno, bit[8], WordType) CStore
+function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CStore(rs, cb, rt, offset, B)) (* CSB *)
+function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b01) = Some(CStore(rs, cb, rt, offset, H)) (* CSH *)
+function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b10) = Some(CStore(rs, cb, rt, offset, W)) (* CSW *)
+function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b11) = Some(CStore(rs, cb, rt, offset, D)) (* CSD *)
+function clause execute (CStore(rs, cb, rt, offset, width)) =
+  {
+    cb_val := readCapReg(cb);
+    if (register_inaccessible(cb)) then
+      exit (raise_c2_exception_v(cb))
+    else if (~(cb_val.tag)) then
+      exit (raise_c2_exception(CapEx_TagViolation, cb))
+    else if (cb_val.sealed) then
+      exit (raise_c2_exception(CapEx_SealViolation, cb))
+    else if (~(cb_val.permit_store)) then
+      exit (raise_c2_exception(CapEx_PermitStoreViolation, cb))
+    else
+      {
+        size   := wordWidthBytes(width);
+        cursor := getCapCursor(cb_val);
+        vAddr  := cursor + (int) (rGPR(rt)) + (int) offset;
+        vAddr64:= (bit[64]) vAddr;
+        if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
+          exit (raise_c2_exception(CapEx_LengthViolation, cb))
+        else if (vAddr < ((nat) (cb_val.base))) then
+          exit (raise_c2_exception(CapEx_LengthViolation, cb))
+        else if ~(isAddressAligned(vAddr64, width)) then
+          exit (SignalExceptionBadAddr(AdES, vAddr64))
+        else
+          {
+            pAddr  := (TranslateOrExit(vAddr64, StoreData));
+            rs_val := rGPR(rs);
+            switch(width)
+              {
+                case B -> MEMw(pAddr, 1) := rs_val[7..0]
+                case H -> MEMw(pAddr, 2) := rs_val[15..0]
+                case W -> MEMw(pAddr, 4) := rs_val[31..0]
+                case D -> MEMw(pAddr, 8) := rs_val
+              }
+          }
+      }
+  }
+
+union ast member (regno, regno, regno, bit[11]) CSC
+function clause decode (0b111110 : (regno) cs : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CSC(cs, cb, rt, offset))
+function clause execute (CSC(cs, cb, rt, offset)) =
+  {
+    cs_val := readCapReg(cs);
+    cb_val := readCapReg(cb);
+    if (register_inaccessible(cs)) then
+      exit (raise_c2_exception_v(cs))
+    else if (register_inaccessible(cb)) then
+      exit (raise_c2_exception_v(cb))
+    else if (~(cb_val.tag)) then
+      exit (raise_c2_exception(CapEx_TagViolation, cb))
+    else if (cb_val.sealed) then
+      exit (raise_c2_exception(CapEx_SealViolation, cb))
+    else if (~(cb_val.permit_store_cap)) then
+      exit (raise_c2_exception(CapEx_PermitStoreCapViolation, cb))
+    else if ((~(cb_val.permit_store_ephemeral_cap)) & (cs_val.tag) & ~(cs_val.non_ephemeral)) then
+      exit (raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb))
+    else
+      {
+        cursor := getCapCursor(cb_val);
+        vAddr  := cursor + (int) (rGPR(rt)) + (int) offset;
+        vAddr64:= (bit[64]) vAddr;
+        if ((vAddr + cap_size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
+          exit (raise_c2_exception(CapEx_LengthViolation, cb))
+        else if (vAddr < ((nat) (cb_val.base))) then
+          exit (raise_c2_exception(CapEx_LengthViolation, cb))
+        else if (vAddr64[4..0] != 0b00000) then
+          exit (SignalExceptionBadAddr(AdES, vAddr64))
+        else
+          {
+            pAddr  := (TranslateOrExit(vAddr64, if cs_val.tag then StoreData else StoreData)); (* XXX use StoreCap here. *)
+            MEMw_tagged(pAddr, cs_val.tag, (capStructToBit257(cs_val))[255..0]);
+            (* XXX write tag *)
+          }
+      }
+  }
+
+union ast member (regno, regno, regno, bit[11]) CLC
+function clause decode (0b110110 : (regno) cd : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CLC(cd, cb, rt, offset))
+function clause execute (CLC(cd, cb, rt, offset)) =  
+  {
+    cb_val := readCapReg(cb);
+    if (register_inaccessible(cd)) then
+      exit (raise_c2_exception_v(cd))
+    else if (register_inaccessible(cb)) then
+      exit (raise_c2_exception_v(cb))
+    else if (~(cb_val.tag)) then
+      exit (raise_c2_exception(CapEx_TagViolation, cb))
+    else if (cb_val.sealed) then
+      exit (raise_c2_exception(CapEx_SealViolation, cb))
+    else if (~(cb_val.permit_load_cap)) then
+      exit (raise_c2_exception(CapEx_PermitLoadCapViolation, cb))
+    else
+      {
+        cursor := getCapCursor(cb_val);
+        vAddr  := cursor + (int) (rGPR(rt)) + (int) offset;
+        vAddr64:= (bit[64]) vAddr;
+        if ((vAddr + cap_size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
+          exit (raise_c2_exception(CapEx_LengthViolation, cb))
+        else if (vAddr < ((nat) (cb_val.base))) then
+          exit (raise_c2_exception(CapEx_LengthViolation, cb))
+        else if (vAddr64[4..0] != 0b00000) then
+          exit (SignalExceptionBadAddr(AdES, vAddr64))
+        else
+          {
+            pAddr  := (TranslateOrExit(vAddr64, LoadData)); (* XXX use LoadCap here. *)
+            let (tag, mem) = (MEMr_tagged(pAddr)) in
+            (CapRegs[cd]) := ([tag] : mem);
+          }
+      }
+  }
diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail
index 54726f8d..a85bd33c 100644
--- a/cheri/cheri_prelude.sail
+++ b/cheri/cheri_prelude.sail
@@ -1,7 +1,7 @@
 (* 265-bit capability is really 257 bits including tag *)
 typedef CapReg = register bits [256:0] {
   256:      tag;
-  255..248: reserved; (* padding *)
+  (* 255..248: reserved1; padding *)
   247..224: otype;
   223..208: sw_perms;
   207:      access_KR2C;
@@ -9,7 +9,8 @@ typedef CapReg = register bits [256:0] {
   205:      access_KCC;
   204:      access_KDC;
   203:      access_EPCC;
-  202..201: reserved;
+  202:      perm_reserved9; (* perm bit 9 *)
+  201:      perm_reserved8; (* perm bit 8 *)
   200:      permit_seal;
   199:      permit_store_ephemeral_cap;
   198:      permit_store_cap;
@@ -19,12 +20,13 @@ typedef CapReg = register bits [256:0] {
   194:      permit_execute;
   193:      non_ephemeral;
   192:      sealed;
-  191..128: cursor;
+  191..128: offset;
   127..64:  base;
   63 .. 0:  length;
 }
 
 register CapReg PCC
+register CapReg delayedPCC
 register CapReg C00 (* aka default data capability, DDC *)
 register CapReg C01
 register CapReg C02
@@ -73,6 +75,8 @@ typedef CapStruct = const struct {
   bool    access_KCC;
   bool    access_KDC;
   bool    access_EPCC;
+  bool    perm_reserved9;
+  bool    perm_reserved8;
   bool    permit_seal;
   bool    permit_store_ephemeral_cap;
   bool    permit_store_cap;
@@ -82,11 +86,39 @@ typedef CapStruct = const struct {
   bool    permit_execute;
   bool    non_ephemeral;
   bool    sealed;
-  bit[64] cursor;
+  bit[64] offset;
   bit[64] base;
   bit[64] length;
 }
 
+let (CapStruct) null_cap = {
+  tag = false;
+  otype = 0;
+  sw_perms = 0;
+  access_KR2C = false;
+  access_KR1C = false;
+  access_KCC = false;
+  access_KDC = false;
+  access_EPCC = false;
+  perm_reserved9 = false;
+  perm_reserved8 = false;
+  permit_seal = false;
+  permit_store_ephemeral_cap = false;
+  permit_store_cap = false;
+  permit_load_cap = false;
+  permit_store = false;
+  permit_load = false;
+  permit_execute = false;
+  non_ephemeral = false;
+  sealed = false;
+  offset = 0;
+  base = 0;
+  length = 0;
+}
+let (nat) max_otype = 0xffffff
+def Nat cap_size_t  = 32 (* cap size in bytes *)
+let ([:cap_size_t:]) cap_size = 32
+
 function CapStruct capRegToCapStruct((CapReg) capReg) =
   {
     tag                        = capReg.tag;
@@ -97,6 +129,8 @@ function CapStruct capRegToCapStruct((CapReg) capReg) =
     access_KCC                 = capReg.access_KCC;
     access_KDC                 = capReg.access_KDC;
     access_EPCC                = capReg.access_EPCC;
+    perm_reserved9             = capReg.perm_reserved9;
+    perm_reserved8             = capReg.perm_reserved8;
     permit_seal                = capReg.permit_seal;
     permit_store_ephemeral_cap = capReg.permit_store_ephemeral_cap;
     permit_store_cap           = capReg.permit_store_cap;
@@ -106,7 +140,7 @@ function CapStruct capRegToCapStruct((CapReg) capReg) =
     permit_execute             = capReg.permit_execute;
     non_ephemeral              = capReg.non_ephemeral;
     sealed                     = capReg.sealed;
-    cursor                     = capReg.cursor;
+    offset                     = capReg.offset;
     base                       = capReg.base;
     length                     = capReg.length;
   }
@@ -115,18 +149,16 @@ function CapStruct capRegToCapStruct((CapReg) capReg) =
 function (CapStruct) readCapReg((regno) n) =
   capRegToCapStruct(CapRegs[n])
 
-function (bit[257]) capStructToBit257((CapStruct) cap) =
-    (
-      [cap.tag]
-      : 0b00000000 (* padding *)
-      : cap.otype
-      : cap.sw_perms
+function (bit[31]) capPermsToVec((CapStruct) cap) = 
+  (
+    cap.sw_perms
       : [cap.access_KR2C]
       : [cap.access_KR1C]
       : [cap.access_KCC]
       : [cap.access_KDC]
       : [cap.access_EPCC]
-      : 0b00       (* Padding *)
+      : [cap.perm_reserved9]
+      : [cap.perm_reserved8]
       : [cap.permit_seal]
       : [cap.permit_store_ephemeral_cap]
       : [cap.permit_store_cap]
@@ -135,20 +167,31 @@ function (bit[257]) capStructToBit257((CapStruct) cap) =
       : [cap.permit_load]
       : [cap.permit_execute]
       : [cap.non_ephemeral]
+  )
+
+function (bit[257]) capStructToBit257((CapStruct) cap) =
+    (
+      [cap.tag]
+      : 0b00000000 (* padding *)
+      : cap.otype
+      : capPermsToVec(cap)
       : [cap.sealed]
-      : cap.cursor
+      : cap.offset
       : cap.base
       : cap.length
     )
 
+function nat getCapCursor((CapStruct) cap) = 
+  (((nat)(cap.base)) + ((nat)(cap.offset))) mod (2 ** 64)
+
 function unit writeCapReg((regno) n, (CapStruct) cap) =
     {
-      reg := (CapRegs[n]);
-      reg := capStructToBit257(cap)
+      (CapRegs[n]) := capStructToBit257(cap)
     }
+
 typedef CapEx = enumerate {
   CapEx_None; 
-  CapEx_LengthVioloation;
+  CapEx_LengthViolation;
   CapEx_TagViolation;
   CapEx_SealViolation;
   CapEx_TypeViolation;
@@ -183,12 +226,27 @@ typedef CGetXOp = enumerate {
   CGetUnsealed;
 }
 
+typedef CPtrCmpOp = enumerate {
+  CEQ;
+  CNE;
+  CLT;
+  CLE;
+  CLTU;
+  CLEU;
+  CEXEQ;
+}
 
+typedef ClearRegSet = enumerate {
+GPLo;
+GPHi;
+CLo;
+CHi;
+}
 
 function (bit[8]) CapExCode((CapEx) ex) =
   switch(ex) {
     case CapEx_None                         -> 0x00
-    case CapEx_LengthVioloation             -> 0x01
+    case CapEx_LengthViolation              -> 0x01
     case CapEx_TagViolation                 -> 0x02
     case CapEx_SealViolation                -> 0x03
     case CapEx_TypeViolation                -> 0x04
@@ -249,3 +307,19 @@ function bool register_inaccessible((regno) r) =
     case 0b11111 -> (PCC.access_EPCC)
     case _       -> bitone
   })
+
+val extern (bit[64] , bit[8]) -> unit effect { wmem } TAGw
+val extern (bit[64]) -> (bit[8]) effect { rmem } TAGr
+
+function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) =
+{
+  let tag = (TAGr (addr)) in
+  let mem = (MEMr (addr, cap_size)) in
+  (tag[0], mem)
+}
+
+function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
+{
+  MEMw(addr, cap_size, data);
+  TAGw(addr, (0b0000000 : [tag]));
+}