first pass at cheri128 sail.

5 files changed, 1566 insertions, 3 deletions

diff --git a/cheri/Makefile b/cheri/Makefile
index 200ddd5a..4e9a397a 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -1,7 +1,12 @@
 EXTRACT_INST=sed -n "/START_${1}\b/,/END_${1}\b/p" cheri_insts.sail | sed 's/^  //;1d;$$d' > inst_$1.sail
 
 extract: cheri_insts.sail
-	$(call EXTRACT_INST,CGetX)
+	$(call EXTRACT_INST,CGetPerms)
+	$(call EXTRACT_INST,CGetType)
+	$(call EXTRACT_INST,CGetBase)
+	$(call EXTRACT_INST,CGetOffset)
+	$(call EXTRACT_INST,CGetTag)
+	$(call EXTRACT_INST,CGetSealed)
 	$(call EXTRACT_INST,CGetPCC)
 	$(call EXTRACT_INST,CGetPCCSetOffset)
 	$(call EXTRACT_INST,CGetCause)
@@ -13,6 +18,7 @@ extract: cheri_insts.sail
 	$(call EXTRACT_INST,CIncOffset)
 	$(call EXTRACT_INST,CSetOffset)
 	$(call EXTRACT_INST,CSetBounds)
+	$(call EXTRACT_INST,CSetBoundsExact)
 	$(call EXTRACT_INST,CClearTag)
 	$(call EXTRACT_INST,ClearRegs)
 	$(call EXTRACT_INST,CFromPtr)
diff --git a/cheri/cheri_insts_128.sail b/cheri/cheri_insts_128.sail
new file mode 100644
index 00000000..b671b515
--- /dev/null
+++ b/cheri/cheri_insts_128.sail
@@ -0,0 +1,973 @@
+(*========================================================================*)
+(*                                                                        *)
+(*  Copyright (c) 2015-2016 Robert M. Norton                              *)
+(*  Copyright (c) 2015-2016 Kathyrn Gray                                  *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(*========================================================================*)
+
+(* Operations that extract parts of a capability into GPR *)
+
+union ast member (regno, regno) CGetPerm
+union ast member (regno, regno) CGetType
+union ast member (regno, regno) CGetBase
+union ast member (regno, regno) CGetLen
+union ast member (regno, regno) CGetTag
+union ast member (regno, regno) CGetSealed
+union ast member (regno, regno) CGetOffset
+
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b000) = Some(CGetPerm(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b001) = Some(CGetType(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetBase(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b011) = Some(CGetLen(rd, cb))
+(* NB CGetCause Handled separately *)
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b101) = Some(CGetTag(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b110) = Some(CGetSealed(rd, cb))
+function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetOffset(rd, cb)) (* NB encoding does not follow pattern *)
+
+function clause execute (CGetPerm(rd, cb)) =
+{
+  (* START_CGetPerms *)
+  checkCP2usable();
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else
+    let capVal = readCapReg(cb) in
+    wGPR(rd) := EXTZ(getCapPerms(capVal));
+  (* END_CGetPerms *)
+}
+
+function clause execute (CGetType(rd, cb)) =
+{
+  (* START_CGetType *)
+  checkCP2usable();
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else
+    let capVal = readCapReg(cb) in
+    wGPR(rd) := EXTZ(capVal.otype);
+  (* END_CGetType *)
+}
+
+function clause execute (CGetBase(rd, cb)) =
+{
+  (* START_CGetBase *)
+  checkCP2usable();
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else
+    let capVal = readCapReg(cb) in
+    wGPR(rd) := getCapBase(capVal);
+  (* END_CGetBase *)
+}
+
+function clause execute (CGetOffset(rd, cb)) =
+{
+  (* START_CGetOffset *)
+  checkCP2usable();
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else
+    let capVal = readCapReg(cb) in
+    wGPR(rd) := getCapOffset(capVal);
+  (* END_CGetOffset *)
+}
+
+function clause execute (CGetLen(rd, cb)) =
+{
+  (* START_CGetLen *)
+  checkCP2usable();
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else
+    let capVal = readCapReg(cb) in
+    let len65  = getCapLength(capVal) in
+    let len64  = if len65 > MAX_U64 then
+        (bit[64]) MAX_U64 else len65[63..0] in
+    wGPR(rd) := len64;
+  (* END_CGetLen *)
+}
+
+function clause execute (CGetTag(rd, cb)) =
+{
+  (* START_CGetTag *)
+  checkCP2usable();
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else
+    let capVal = readCapReg(cb) in
+    wGPR(rd) := EXTZ(capVal.tag);
+  (* END_CGetTag *)
+}
+
+function clause execute (CGetSealed(rd, cb)) =
+{
+  (* START_CGetSealed *)
+  checkCP2usable();
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else
+    let capVal = readCapReg(cb) in
+    wGPR(rd) := EXTZ(capVal.sealed);
+  (* END_CGetSealed *)
+}
+
+union ast member regno CGetPCC
+function clause decode (0b010010 : 0b00000 : (regno) cd : 0b00000 : 0b11111 : 0b111111) = Some(CGetPCC(cd))
+function clause execute (CGetPCC(cd)) =
+{
+  (* START_CGetPCC *)
+  checkCP2usable();
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else
+    let pcc = (capRegToCapStruct(PCC)) in
+    let (success, pcc2) = setCapOffset(pcc, PC) in
+    {assert (success, None); (* guaranteed to be in-bounds *)
+    writeCapReg(cd, pcc2)};
+  (* END_CGetPCC *)
+}
+
+
+union ast member (regno, regno) CGetPCCSetOffset
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) rs : 0b00111 : 0b111111) = Some(CGetPCCSetOffset(cd, rs))
+function clause execute (CGetPCCSetOffset(cd, rs)) =
+{
+  (* START_CGetPCCSetOffset *)
+  checkCP2usable();
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else
+    let pcc = (capRegToCapStruct(PCC)) in
+    let rs_val = rGPR(rs) in
+    let (success, newPCC) = setCapOffset(pcc, rs_val) in
+    if (success) then
+        writeCapReg(cd, newPCC)
+    else
+        writeCapReg(cd, int_to_cap(rs_val));
+  (* END_CGetPCCSetOffset *)
+}
+(* Get and Set CP2 cause register *)
+
+union ast member regno CGetCause
+function clause decode (0b010010 : 0b00000 : (regno) rd : 0b00000 : 0b00000000 : 0b100) = Some(CGetCause(rd))
+function clause execute (CGetCause(rd)) = 
+{
+  (* START_CGetCause *)
+  checkCP2usable();
+  if not (pcc_access_system_regs ()) then
+    raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation)
+  else
+    wGPR(rd) := EXTZ(CapCause)
+  (* END_CGetCause *)
+}
+
+union ast member (regno) CSetCause
+function clause decode (0b010010 : 0b00100 : 0b00000 : 0b00000 : (regno) rt : 0b000 : 0b100) = Some(CSetCause(rt))
+function clause execute (CSetCause((regno) rt)) = 
+{
+  (* START_CSetCause *)
+  checkCP2usable();
+  if not (pcc_access_system_regs ()) then
+    raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation)
+  else
+    {
+      (bit[64]) rt_val := rGPR(rt);
+      CapCause.ExcCode := rt_val[15..8];
+      CapCause.RegNum  := rt_val[7..0];
+    }
+  (* END_CSetCause *)
+}
+
+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)) = 
+{
+  (* START_CAndPerm *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  rt_val := rGPR(rt);
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else
+    let perms   = getCapPerms(cb_val) in
+    let newCap  = setCapPerms(cb_val, (perms & rt_val[30..0])) in
+    writeCapReg(cd, newCap);
+  (* END_CAndPerm *)
+}
+
+
+
+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)) = 
+{
+  (* START_CToPtr *)
+  checkCP2usable();
+  ct_val := readCapReg(ct);
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if (register_inaccessible(ct)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
+  else if not (ct_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, ct)
+  else 
+    {
+      wGPR(rd) := if not (cb_val.tag) then
+          ((bit[64]) 0)
+        else
+          (bit[64])(getCapCursor(cb_val) - unsigned(getCapBase(ct_val)))
+    }
+  (* END_CToPtr *)
+}
+
+
+
+union ast member regregreg CSub
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b001010) = Some(CSub(rd, cb, ct))
+function clause execute(CSub(rd, cb, ct)) = 
+{
+  (* START_CSub *)
+  checkCP2usable();
+  ct_val := readCapReg(ct);
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if (register_inaccessible(ct)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
+  else 
+    {
+      wGPR(rd) := (bit[64])(getCapCursor(cb_val) - getCapCursor(ct_val))
+    }
+  (* END_CSub *)
+}
+
+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)) = 
+{
+  (* START_CPtrCmp *)
+  checkCP2usable();
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if (register_inaccessible(ct)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, 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 not (cb_val.tag) then
+            {
+              ltu := true;
+              lts := true;
+            }
+        }
+      else
+        {
+          cursor1 := getCapCursor(cb_val);
+          cursor2 := getCapCursor(ct_val);
+          equal   := (cursor1 == cursor2);
+          ltu     := (cursor1 < cursor2);
+          lts     := (((bit[64])cursor1) <_s ((bit[64])cursor2));
+        };
+      wGPR(rd) := EXTZ(switch (op) {
+        case CEQ   -> [equal]
+        case CNE   -> [not (equal)]
+        case CLT   -> [lts]
+        case CLE   -> [lts | equal]
+        case CLTU  -> [ltu]
+        case CLEU  -> [lts | equal]
+        case CEXEQ -> [cb_val == ct_val]
+      })
+    }
+  (* END_CPtrCmp *)
+}
+
+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)) =
+{
+  (* START_CIncOffset *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  rt_val := rGPR(rt);
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if ((cb_val.tag) & (cb_val.sealed) & (rt_val != 0x0000000000000000)) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else
+    let (success, newCap) = incCapOffset(cb_val, rt_val) in
+    if (success) then
+        writeCapReg(cd, newCap)
+    else
+        writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val))
+  (* END_CIncOffset *)
+}
+
+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)) =
+{
+  (* START_CSetOffset *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  rt_val := rGPR(rt);
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if ((cb_val.tag) & (cb_val.sealed)) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else
+    let (success, newCap) = setCapOffset(cb_val, rt_val) in
+    if (success) then
+        writeCapReg(cd, newCap)
+    else
+        writeCapReg(cd, int_to_cap(cb_val.address + rt_val))
+  (* END_CSetOffset *)
+}
+
+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)) =
+{
+  (* START_CSetBounds *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  rt_val := unsigned(rGPR(rt));
+  cursor := getCapCursor(cb_val);
+  base   := unsigned(getCapBase(cb_val));
+  top    := unsigned(getCapTop(cb_val));
+  newTop := cursor + rt_val;
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else if (cursor < base) then
+    raise_c2_exception(CapEx_LengthViolation, cb)
+  else if (newTop > top) then
+    raise_c2_exception(CapEx_LengthViolation, cb)
+  else
+    let (_, newCap) = setCapBounds(cb_val, (bit[64]) cursor, (bit[65]) newTop) in
+    writeCapReg(cd, newCap) (* ignore exact *)
+  (* END_CSetBounds *)
+}
+
+
+union ast member regregreg CSetBoundsExact
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b001001) = Some(CSetBoundsExact(cd, cb, rt))
+function clause execute (CSetBoundsExact(cd, cb, rt)) =
+{
+  (* START_CSetBoundsExact *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  rt_val := unsigned(rGPR(rt));
+  cursor := getCapCursor(cb_val);
+  base   := unsigned(getCapBase(cb_val));
+  top    := unsigned(getCapTop(cb_val));
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else if (cursor < base) then
+    raise_c2_exception(CapEx_LengthViolation, cb)
+  else if ((cursor + rt_val) > top) then
+    raise_c2_exception(CapEx_LengthViolation, cb)
+  else
+    let (exact, newCap) = setCapBounds(cb_val, (bit[64]) base, (bit[65]) top) in
+    if not (exact) then
+        raise_c2_exception(CapEx_InexactBounds, cb)
+    else
+        writeCapReg(cd, newCap)
+  (* END_CSetBoundsExact *)
+}
+
+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)) =
+{
+  (* START_CClearTag *)
+  checkCP2usable();
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else
+    {
+      cb_val := readCapReg(cb);
+      writeCapReg(cd, {cb_val with tag = false});
+    }
+  (* END_CClearTag *)
+}
+
+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)) =
+{
+  (* START_ClearRegs *)
+  if ((regset == CLo) | (regset == CHi)) then
+    checkCP2usable();
+  if (regset == CHi) then
+      foreach (i from 0 to 15)
+        let r = ((bit[5]) (i+16)) in
+        if (mask[i] & register_inaccessible(r)) then
+          raise_c2_exception(CapEx_AccessSystemRegsViolation, r);
+  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
+      }
+  (* END_ClearRegs *)
+}
+
+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)) =
+{
+  (* START_CFromPtr *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  rt_val := rGPR(rt);
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if (rt == 0) then
+    writeCapReg(cd, null_cap)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else
+    let (success, newCap) = setCapOffset(cb_val, rt_val) in
+    if (success) then
+        writeCapReg(cd, newCap)
+    else
+        writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val))
+  (* END_CFromPtr *)
+}
+
+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)) =
+{
+  (* START_CCheckPerm *)
+  checkCP2usable();
+  cs_val := readCapReg(cs);
+  cs_perms := EXTZ(getCapPerms(cs_val));
+  rt_perms := rGPR(rt);
+  if (register_inaccessible(cs)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+  else if not (cs_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cs)
+  else if ((cs_perms & rt_perms) != rt_perms) then
+    raise_c2_exception(CapEx_UserDefViolation, cs)
+  else
+    ()
+  (* END_CCheckPerm *)
+}
+
+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)) =
+{
+  (* START_CCheckType *)
+  checkCP2usable();
+  cs_val := readCapReg(cs);
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cs)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cs_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cs)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if not (cs_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cs)
+  else if not (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else if ((cs_val.otype) != (cb_val.otype)) then
+    raise_c2_exception(CapEx_TypeViolation, cs)
+  else
+    ()
+  (* END_CCheckType *)
+}
+
+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)) =
+{
+  (* START_CSeal *)
+  checkCP2usable();
+  cs_val := readCapReg(cs);
+  ct_val := readCapReg(ct);
+  ct_cursor := getCapCursor(ct_val);
+  ct_top    := unsigned(getCapTop(ct_val));
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cs)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+  else if (register_inaccessible(ct)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
+  else if not (cs_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cs)
+  else if not (ct_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, ct)
+  else if (cs_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cs)
+  else if (ct_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, ct)
+  else if not (ct_val.permit_seal) then
+    raise_c2_exception(CapEx_PermitSealViolation, ct)
+  else if (ct_cursor >= ct_top) then
+    raise_c2_exception(CapEx_LengthViolation, ct)
+  else if (ct_cursor > max_otype) then
+    raise_c2_exception(CapEx_LengthViolation, ct)
+  else
+    let (success, newCap) = sealCap(cs_val, (bit[24]) ct_cursor) in
+    if not (success) then
+        raise_c2_exception(CapEx_InexactBounds, cs)
+    else
+        writeCapReg(cd, newCap)
+  (* END_CSeal *)
+}
+
+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)) =
+{
+  (* START_CUnseal *)
+  checkCP2usable();
+  cs_val := readCapReg(cs);
+  ct_val := readCapReg(ct);
+  ct_cursor := getCapCursor(ct_val);
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cs)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+  else if (register_inaccessible(ct)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
+  else if not (cs_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cs)
+  else if not (ct_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, ct)
+  else if not (cs_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cs)
+  else if (ct_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, ct)
+  else if (ct_cursor != unsigned(cs_val.otype)) then
+    raise_c2_exception(CapEx_TypeViolation, ct)
+  else if not (ct_val.permit_seal) then
+    raise_c2_exception(CapEx_PermitSealViolation, ct)
+  else if (ct_cursor >= unsigned(getCapTop(ct_val))) then
+    raise_c2_exception(CapEx_LengthViolation, ct)
+  else
+    writeCapReg(cd, {cs_val with 
+      sealed=false; 
+      otype=0;
+      global=(cs_val.global & ct_val.global)
+    })
+  (* END_CUnseal *)
+}
+
+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 *)
+  (* START_CCall *)
+  checkCP2usable();
+  cs_val := readCapReg(cs);
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cs)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cs_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cs)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if not (cs_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cs)
+  else if not (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else if ((cs_val.otype) != (cb_val.otype)) then
+    raise_c2_exception(CapEx_TypeViolation, cs)
+  else if not (cs_val.permit_execute) then
+    raise_c2_exception(CapEx_PermitExecuteViolation, cs)
+  else if (cb_val.permit_execute) then
+    raise_c2_exception(CapEx_PermitExecuteViolation, cb)
+  else if (getCapCursor(cs_val) >= unsigned(getCapTop(cs_val))) then
+    raise_c2_exception(CapEx_LengthViolation, cs)
+  else
+    raise_c2_exception(CapEx_CallTrap, cs);
+  (* END_CCall *)
+}
+
+union ast member unit CReturn
+function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn)
+function clause execute (CReturn) =
+{
+  (* START_CReturn *)
+  checkCP2usable();
+  raise_c2_exception_noreg(CapEx_ReturnTrap)
+  (* END_CReturn *)
+}
+
+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)) =
+{
+  (* START_CBx *)
+  checkCP2usable();
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if (((readCapReg(cb)).tag) ^ invert) then
+    {
+      let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
+      delayedPC     := PC + offset;
+      branchPending := 1;
+    }
+  (* END_CBx *)
+}
+
+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)) = 
+{
+  (* START_CJALR *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  cb_ptr := getCapCursor(cb_val);
+  cb_top := unsigned(getCapTop(cb_val));
+  if (link & register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else if not (cb_val.permit_execute) then
+    raise_c2_exception(CapEx_PermitExecuteViolation, cb)
+  else if not (cb_val.global) then
+    raise_c2_exception(CapEx_GlobalViolation, cb)
+  else if (cb_ptr + 4 > cb_top) then
+    raise_c2_exception(CapEx_LengthViolation, cb)
+  else if ((cb_ptr mod 4) != 0) then
+    SignalException(AdEL)
+  else
+    {
+      if (link) then
+        let pcc = capRegToCapStruct(PCC) in
+        let (success, linkCap) = setCapOffset(pcc, PC+8) in
+        if (success) then
+            writeCapReg(cd, linkCap)
+        else
+            assert(false, None);
+      delayedPC := getCapOffset(cb_val);
+      delayedPCC := capStructToCapReg(cb_val);
+      branchPending := 1;
+    }
+  (* END_CJALR *)
+}
+
+union ast member (regno, regno, regno, bit[8], bool, WordType, bool) CLoad
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CLoad(rd, cb, rt, offset, false, B, false)) (* CLBU *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b00) = Some(CLoad(rd, cb, rt, offset, true,  B, false)) (* CLB *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b01) = Some(CLoad(rd, cb, rt, offset, false, H, false)) (* CLHU *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b01) = Some(CLoad(rd, cb, rt, offset, true,  H, false)) (* CLH *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b10) = Some(CLoad(rd, cb, rt, offset, false, W, false)) (* CLWU *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b10) = Some(CLoad(rd, cb, rt, offset, true,  W, false)) (* CLW *)
+function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b11) = Some(CLoad(rd, cb, rt, offset, false, D, false)) (* CLD *)
+
+function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, B, true)) (* CLLBU *)
+function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true,  B, true)) (* CLLB  *)
+function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, H, true)) (* CLLHU *)
+function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true,  H, true)) (* CLLH  *)
+function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, W, true)) (* CLLWU *)
+function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true,  W, true)) (* CLLW  *)
+function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b11) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, D, true)) (* CLLD  *)
+
+function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
+{
+  (* START_CLoad *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else if not (cb_val.permit_load) then
+    raise_c2_exception(CapEx_PermitLoadViolation, cb)
+  else
+    {
+      size   := wordWidthBytes(width);
+      cursor := getCapCursor(cb_val);
+      vAddr  := cursor + unsigned(rGPR(rt)) + (size*signed(offset));
+      vAddr64:= (bit[64]) vAddr;
+      if ((vAddr + size) > unsigned(getCapTop(cb_val))) then
+        raise_c2_exception(CapEx_LengthViolation, cb)
+      else if (vAddr < unsigned(getCapBase(cb_val))) then
+        raise_c2_exception(CapEx_LengthViolation, cb)
+      else if not (isAddressAligned(vAddr64, width)) then
+        SignalExceptionBadAddr(AdEL, vAddr64)
+      else
+        {
+          pAddr      := (TLBTranslate(vAddr64, LoadData));
+          widthBytes := wordWidthBytes(width);
+          memResult  := if (linked) then
+              {
+                CP0LLBit  := 0b1;
+                CP0LLAddr := pAddr;
+                MEMr_reserve(pAddr, widthBytes);
+              }
+            else
+              MEMr(pAddr, widthBytes);
+          if (signext) then
+            wGPR(rd) := EXTS(memResult)
+          else
+            wGPR(rd) := EXTZ(memResult)
+        }
+    }
+  (* END_CLoad *)
+}
+
+union ast member (regno, regno, regno, regno, bit[8], WordType, bool) CStore
+function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CStore(rs, cb, rt, 0b00000, offset, B, false)) (* CSB *)
+function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b01) = Some(CStore(rs, cb, rt, 0b00000, offset, H, false)) (* CSH *)
+function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b10) = Some(CStore(rs, cb, rt, 0b00000, offset, W, false)) (* CSW *)
+function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b11) = Some(CStore(rs, cb, rt, 0b00000, offset, D, false)) (* CSD *)
+
+function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b00) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, B, true)) (* CSCB *)
+function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b01) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, H, true)) (* CSCH *)
+function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b10) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, W, true)) (* CSCW *)
+function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b11) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, D, true)) (* CSCD *)
+
+function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
+{
+  (* START_CStore *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else if not (cb_val.permit_store) then
+    raise_c2_exception(CapEx_PermitStoreViolation, cb)
+  else
+    {
+      size   := wordWidthBytes(width);
+      cursor := getCapCursor(cb_val);
+      vAddr  := cursor + unsigned(rGPR(rt)) + (size * signed(offset));
+      vAddr64:= (bit[64]) vAddr;
+      if ((vAddr + size) > unsigned(getCapTop(cb_val))) then
+        raise_c2_exception(CapEx_LengthViolation, cb)
+      else if (vAddr < unsigned(getCapBase(cb_val))) then
+        raise_c2_exception(CapEx_LengthViolation, cb)
+      else if not (isAddressAligned(vAddr64, width)) then
+        SignalExceptionBadAddr(AdES, vAddr64)
+      else
+        {
+          pAddr  := (TLBTranslate(vAddr64, StoreData));
+          rs_val := rGPR(rs);
+          if (conditional) then
+            {
+              success := if (CP0LLBit[0]) then
+                  switch(width)
+                    {
+                      case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0])
+                      case H -> MEMw_conditional_wrapper(pAddr, 2, rs_val[15..0])
+                      case W -> MEMw_conditional_wrapper(pAddr, 4, rs_val[31..0])
+                      case D -> MEMw_conditional_wrapper(pAddr, 8, rs_val)
+                    }
+                else
+                  false;
+              wGPR(rd) := EXTZ([success]);
+            }
+            else
+          switch(width)
+            {
+              case B -> MEMw_wrapper(pAddr, 1) := rs_val[7..0]
+              case H -> MEMw_wrapper(pAddr, 2) := rs_val[15..0]
+              case W -> MEMw_wrapper(pAddr, 4) := rs_val[31..0]
+              case D -> MEMw_wrapper(pAddr, 8) := rs_val
+            }
+        }
+    }
+  (* END_CStore *)
+}
+
+union ast member (regno, regno, regno, regno, bit[11], bool) CSC
+function clause decode (0b111110 : (regno) cs : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CSC(cs, cb, rt, 0b00000, offset, false))
+function clause decode (0b010010 : 0b10000 : (regno) cs : (regno) cb: (regno) rd : 0b00 : 0b0111) = Some(CSC(cs, cb, 0b00000, rd, 0b00000000000, true))
+function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
+{
+  (* START_CSC *)
+  checkCP2usable();
+  cs_val := readCapReg(cs);
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cs)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else if not (cb_val.permit_store_cap) then
+    raise_c2_exception(CapEx_PermitStoreCapViolation, cb)
+  else if not (cb_val.permit_store_local_cap) & (cs_val.tag) & not (cs_val.global) then
+    raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb)
+  else
+    {
+      cursor := getCapCursor(cb_val);
+      vAddr  := cursor + unsigned(rGPR(rt)) + (16 * signed(offset));
+      vAddr64:= (bit[64]) vAddr;
+      if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then
+        raise_c2_exception(CapEx_LengthViolation, cb)
+      else if (vAddr < unsigned(getCapBase(cb_val))) then
+        raise_c2_exception(CapEx_LengthViolation, cb)
+      else if ((vAddr mod cap_size) != 0) then
+        SignalExceptionBadAddr(AdES, vAddr64)
+      else
+        {
+          let (pAddr, noStoreCap)  = (TLBTranslateC(vAddr64, StoreData)) in
+          if (cs_val.tag & noStoreCap) then
+            raise_c2_exception(CapEx_TLBNoStoreCap, cs)
+          else if (conditional) then
+            {
+              success := if (CP0LLBit[0]) then
+                  MEMw_tagged_conditional(pAddr, cs_val.tag, capStructToMemBits(cs_val))
+                else
+                  false;
+              wGPR(rd) := EXTZ([success]);
+            }
+          else
+            MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val));
+        }
+    }
+  (* END_CSC *)
+}
+
+union ast member (regno, regno, regno, bit[11], bool) CLC
+function clause decode (0b110110 : (regno) cd : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CLC(cd, cb, rt, offset, false))
+function clause decode (0b010010 : 0b10000 : (regno) cd : (regno) cb: 0b0000000 : 0b1111) = Some(CLC(cd, cb, 0b00000, 0b00000000000, true))
+function clause execute (CLC(cd, cb, rt, offset, linked)) =  
+{
+  (* START_CLC *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cd)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+  else if (register_inaccessible(cb)) then
+    raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+  else if not (cb_val.tag) then
+    raise_c2_exception(CapEx_TagViolation, cb)
+  else if (cb_val.sealed) then
+    raise_c2_exception(CapEx_SealViolation, cb)
+  else if not (cb_val.permit_load_cap) then
+    raise_c2_exception(CapEx_PermitLoadCapViolation, cb)
+  else
+    {
+      cursor := getCapCursor(cb_val);
+      vAddr  := cursor + unsigned(rGPR(rt)) + (16*signed(offset));
+      vAddr64:= (bit[64]) vAddr;
+      if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then
+        raise_c2_exception(CapEx_LengthViolation, cb)
+      else if (vAddr < unsigned(getCapBase(cb_val))) then
+        raise_c2_exception(CapEx_LengthViolation, cb)
+      else if ((vAddr mod cap_size) != 0) then
+        SignalExceptionBadAddr(AdEL, vAddr64)
+      else
+        {
+          let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in
+          let (tag, mem) = (if (linked) 
+            then
+              {
+                CP0LLBit  := 0b1;
+                CP0LLAddr := pAddr;
+                MEMr_tagged_reserve(pAddr);
+              }
+            else 
+              (MEMr_tagged(pAddr)))
+          in
+          (CapRegs[cd]) := memBitsToCapBits(tag & not (suppressTag), mem);
+        }
+    }
+  (* END_CLC *)
+}
+
+union ast member (regno) C2Dump
+function clause decode (0b010010 : 0b00100 : (regno) rt : 0x0006) = Some(C2Dump(rt))
+function clause execute (C2Dump (rt)) =
+    () (* Currently a NOP *)
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
new file mode 100644
index 00000000..323682b7
--- /dev/null
+++ b/cheri/cheri_prelude_128.sail
@@ -0,0 +1,569 @@
+(*========================================================================*)
+(*                                                                        *)
+(*  Copyright (c) 2015-2016 Robert M. Norton                              *)
+(*  Copyright (c) 2015-2016 Kathyrn Gray                                  *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(*========================================================================*)
+
+(* 265-bit capability is really 257 bits including tag *)
+typedef CapReg = bit[129]
+
+register CapReg PCC
+register CapReg nextPCC
+register CapReg delayedPCC
+register CapReg C00 (* aka default data capability, DDC *)
+register CapReg C01
+register CapReg C02
+register CapReg C03
+register CapReg C04
+register CapReg C05
+register CapReg C06
+register CapReg C07
+register CapReg C08
+register CapReg C09
+register CapReg C10
+register CapReg C11
+register CapReg C12
+register CapReg C13
+register CapReg C14
+register CapReg C15
+register CapReg C16
+register CapReg C17
+register CapReg C18
+register CapReg C19
+register CapReg C20
+register CapReg C21
+register CapReg C22
+register CapReg C23
+register CapReg C24 (* aka return code capability, RCC *)
+register CapReg C25
+register CapReg C26 (* aka invoked data capability, IDC *)
+register CapReg C27 (* aka kernel reserved capability 1, KR1C *)
+register CapReg C28 (* aka kernel reserved capability 2, KR2C *)
+register CapReg C29 (* aka kernel code capability, KCC *)
+register CapReg C30 (* aka kernel data capability, KDC *)
+register CapReg C31 (* aka exception program counter capability, EPCC *)
+
+let (vector <0, 32, inc, (register<CapReg>)>) CapRegs =
+  [ C00, C01, C02, C03, C04, C05, C06, C07, C08, C09, C10,
+  C11, C12, C13, C14, C15, C16, C17, C18, C19, C20,
+  C21, C22, C23, C24, C25, C26, C27, C28, C29, C30, C31
+  ]
+
+let num_uperms = 4
+
+
+typedef CapStruct = const struct {
+  bool    tag;
+  bit[4]  uperms;
+  bool    access_system_regs;
+  bool    perm_reserved9;
+  bool    perm_reserved8;
+  bool    permit_seal;
+  bool    permit_store_local_cap;
+  bool    permit_store_cap;
+  bool    permit_load_cap;
+  bool    permit_store;
+  bool    permit_load;
+  bool    permit_execute;
+  bool    global;
+  bit[2]  reserved;
+  bit[6]  E;
+  bool    sealed;
+  bit[20] B;
+  bit[20] T;
+  bit[24] otype;
+  bit[64] address;
+}
+
+let (CapStruct) null_cap = {
+  tag                    = false;
+  uperms                 = 0;
+  access_system_regs     = false;
+  perm_reserved9         = false;
+  perm_reserved8         = false;
+  permit_seal            = false;
+  permit_store_local_cap = false;
+  permit_store_cap       = false;
+  permit_load_cap        = false;
+  permit_store           = false;
+  permit_load            = false;
+  permit_execute         = false;
+  global                 = false;
+  reserved               = 0;
+  E                      = 48; (* encoded as 0 in memory due to xor *)
+  sealed                 = false;
+  B                      = 0;
+  T                      = 0;
+  otype                  = 0;
+  address                = 0;
+}
+
+let (nat) max_otype = 0xffffff
+def Nat cap_size_t  = 16 (* cap size in bytes *)
+let ([:cap_size_t:]) cap_size = 16
+let have_cp2 = true
+
+function CapStruct capRegToCapStruct((CapReg) c) =
+  let (bool)    s = c[104] in
+  let (bit[20]) B = if s then c[103..96] : 0x000 else c[103..84] in
+  let (bit[20]) T = if s then c[83..76] : 0x000 else c[83..64] in
+  let (bit[24]) otype = if s then c[95..84] : c[75..64] else 0 in
+  {
+    tag                    = c[128];
+    uperms                 = c[127..124];
+    access_system_regs     = c[123];
+    perm_reserved9         = c[122];
+    perm_reserved8         = c[121];
+    permit_seal            = c[120];
+    permit_store_local_cap = c[119];
+    permit_store_cap       = c[118];
+    permit_load_cap        = c[117];
+    permit_store           = c[116];
+    permit_load            = c[115];
+    permit_execute         = c[114];
+    global                 = c[113];
+    reserved               = c[112..111];
+    E                      = c[110..105];
+    sealed                 = s;
+    B                      = B;
+    T                      = T;
+    otype                  = otype;
+    address                = c[63..0];
+  }
+
+
+function (CapStruct) readCapReg((regno) n) =
+  capRegToCapStruct(CapRegs[n])
+
+function (bit[11]) getCapHardPerms((CapStruct) cap) =
+   ([cap.access_system_regs]
+  : [cap.perm_reserved9]
+  : [cap.perm_reserved8]
+  : [cap.permit_seal]
+  : [cap.permit_store_local_cap]
+  : [cap.permit_store_cap]
+  : [cap.permit_load_cap]
+  : [cap.permit_store]
+  : [cap.permit_load]
+  : [cap.permit_execute]
+  : [cap.global])
+
+function (bit[31]) getCapPerms((CapStruct) cap) = 
+    let (bit[15]) perms = EXTS(getCapHardPerms(cap)) in (* NB access_system copied into 14-11 *)
+    (0x000 (* uperms 30-19 *)
+  : cap.uperms
+  : perms)
+
+function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) =
+    { cap with
+      uperms                 = perms[18..15];
+(*      perm_reserved11_14     = (cap.perm_reserved11_14 & (perms[14..11]));*)
+      access_system_regs     = perms[10];
+      perm_reserved9         = perms[9];
+      perm_reserved8         = perms[8];
+      permit_seal            = perms[7];
+      permit_store_local_cap = perms[6];
+      permit_store_cap       = perms[5];
+      permit_load_cap        = perms[4];
+      permit_store           = perms[3];
+      permit_load            = perms[2];
+      permit_execute         = perms[1];
+      global                 = perms[0];
+      }
+
+function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) =
+    if (((cap.T)[11..0] == 0) & ((cap.B)[11..0] == 0)) then
+        (true, {cap with sealed=true; otype=otype})
+    else
+        (false, undefined)
+
+function (bit[128]) capStructToMemBits((CapStruct) cap) =
+    let (bit[20]) b = if cap.sealed then (cap.B)[23..12] : (cap.otype)[23..12] else cap.B in
+    let (bit[20]) t = if cap.sealed then (cap.T)[23..12] : (cap.otype)[11..0]  else cap.T in
+    ( cap.uperms
+    : getCapHardPerms(cap)
+    : cap.reserved
+    : cap.E
+    : [cap.sealed]
+    : b
+    : t
+    : cap.address
+    )
+
+function (CapReg) capStructToCapReg((CapStruct) cap) =
+    ([cap.tag] : capStructToMemBits(cap))
+
+(* Reverse of above used when reading from memory *)
+function (CapReg) memBitsToCapBits((bool) tag, (bit[128]) b) =
+  ([tag]
+   : b
+  )
+
+function unit writeCapReg((regno) n, (CapStruct) cap) =
+    {
+      CapRegs[n] := capStructToCapReg(cap)
+    }
+
+
+function int a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) =
+    switch (a_mid < R, bound < R) {
+      case (False, False) -> 0
+      case (False, True)  -> 1
+      case (True, False)  -> -1
+      case (True, True)   -> 0
+    }
+
+function bit[64] getCapBase((CapStruct) c)  = 
+    let ([|63|])  E = unsigned(c.E) in
+    let (bool)    s = c.sealed in
+    let (bit[20]) B = c.B in
+    let (bit[64]) a = c.address in
+    let (bit[20]) R = B - 0x00100 in (* wraps *)
+    let (bit[20]) a_mid = a[(E + 19)..E] in
+    let (int) correction = a_top_correction(a_mid, R, B) in
+    let a_top = a[63..(E+20)] in
+    let (bit[64]) base = EXTZ((a_top + correction) : B) in
+    base << E
+
+function bit[65] getCapTop((CapStruct) c)  = 
+    let ([|63|])  E = unsigned(c.E) in
+    let (bool)    s = c.sealed in
+    let (bit[20]) B = c.B in
+    let (bit[20]) T = c.T in
+    let (bit[64]) a = c.address  in
+    let (bit[20]) R = B - 0x00100 in (* wraps *)
+    let (bit[20]) a_mid = a[(E + 19)..E] in
+    let (int) correction = a_top_correction(a_mid, R, T) in
+    let a_top = a[63..(E+20)] in
+    let (bit[65]) top1 = EXTZ((a_top + correction) : T) in
+    top1 << E
+
+function bit[64] getCapOffset((CapStruct) c) = 
+    let base = getCapBase(c) in
+    c.address - base
+
+function bit[65] getCapLength((CapStruct) c)  = getCapTop(c) - (0b0 : getCapBase(c))
+
+function nat getCapCursor((CapStruct) cap) = unsigned(cap.address)
+
+function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) =
+    let oldBase    = getCapBase(c) in
+    let oldTop     = getCapTop(c) in
+    let (bit[64]) newAddress = oldBase + offset in
+    let newCap     = { c with address = newAddress } in
+    let newBase    = getCapBase(newCap) in
+    let newTop     = getCapTop(newCap) in
+    let representable = (oldBase == newBase) & (oldTop == newTop) in
+    (representable, newCap)
+
+function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta) =
+    let oldBase    = getCapBase(c) in
+    let oldTop     = getCapTop(c) in
+    let (bit[64]) newAddress = c.address + delta in
+    let newCap     = { c with address = newAddress } in
+    let newBase    = getCapBase(newCap) in
+    let newTop     = getCapTop(newCap) in
+    let representable = (oldBase == newBase) & (oldTop == newTop) in
+    (representable, newCap)
+
+(** FUNCTION:integer HighestSetBit(bits(N) x) *)
+
+function forall Nat 'N. option<[|0:('N + -1)|]> HighestSetBit((bit['N]) x) = {
+  let N = (length(x)) in {
+  ([|('N + -1)|]) result := 0;
+  (bool) break := false;
+  foreach (i from (N - 1) downto 0)
+    if ~(break) & x[i] == 1 then {
+      result := i;
+      break := true;
+    };
+
+  if break then Some(result) else None;
+}}
+
+function (bit[6]) computeE ((bit[65]) rlength) =
+    let msb = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
+    switch (msb) {
+      case (Some(b)) -> (bit[6]) b (* hw rounds up to multiple of 4 *)
+      case None    -> 0
+    }    
+
+function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) =
+    (* {cap with base=base; length=(bit[64]) length; offset=0} *)
+    let (bit[6])  e = computeE(top - (0b0 : base)) in
+    let (bit[20]) B = base[(19+e)..e] in
+    let (bit[20]) T = top[(19+e)..e] in
+    let (bit[20]) T2 = T + if (top[(e - 1)..0] == 0) then 0 else 1 in
+    let newCap  = {cap with E=e; B=B; T=T2} in
+    let newBase = getCapBase(newCap) in
+    let newTop  = getCapTop(newCap) in
+    let exact   = (base == newBase) & (top == newTop) in
+    (exact, newCap)
+
+function CapStruct int_to_cap ((bit[64]) offset) = 
+    {null_cap with address = offset}
+
+typedef CapEx = enumerate {
+  CapEx_None; 
+  CapEx_LengthViolation;
+  CapEx_TagViolation;
+  CapEx_SealViolation;
+  CapEx_TypeViolation;
+  CapEx_CallTrap;
+  CapEx_ReturnTrap;
+  CapEx_TSSUnderFlow;
+  CapEx_UserDefViolation;
+  CapEx_TLBNoStoreCap;
+  CapEx_InexactBounds;
+  CapEx_GlobalViolation;
+  CapEx_PermitExecuteViolation;
+  CapEx_PermitLoadViolation;
+  CapEx_PermitStoreViolation;
+  CapEx_PermitLoadCapViolation;
+  CapEx_PermitStoreCapViolation;
+  CapEx_PermitStoreLocalCapViolation;
+  CapEx_PermitSealViolation;
+  CapEx_AccessSystemRegsViolation;
+}
+
+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_LengthViolation              -> 0x01
+    case CapEx_TagViolation                 -> 0x02
+    case CapEx_SealViolation                -> 0x03
+    case CapEx_TypeViolation                -> 0x04
+    case CapEx_CallTrap                     -> 0x05
+    case CapEx_ReturnTrap                   -> 0x06
+    case CapEx_TSSUnderFlow                 -> 0x07
+    case CapEx_UserDefViolation             -> 0x08
+    case CapEx_TLBNoStoreCap                -> 0x09
+    case CapEx_InexactBounds                -> 0x0a
+    case CapEx_GlobalViolation              -> 0x10
+    case CapEx_PermitExecuteViolation       -> 0x11
+    case CapEx_PermitLoadViolation          -> 0x12
+    case CapEx_PermitStoreViolation         -> 0x13
+    case CapEx_PermitLoadCapViolation       -> 0x14
+    case CapEx_PermitStoreCapViolation      -> 0x15
+    case CapEx_PermitStoreLocalCapViolation -> 0x16
+    case CapEx_PermitSealViolation          -> 0x17
+    case CapEx_AccessSystemRegsViolation    -> 0x18
+  }
+
+typedef CapCauseReg = register bits [15:0] {
+  15..8: ExcCode;
+  7..0:  RegNum;
+}
+
+register CapCauseReg CapCause
+
+function forall Type 'o . 'o SignalException ((Exception) ex) = 
+  {
+    C31        := PCC;
+    (*C31.offset := PC; XXX fix this *)
+    nextPCC    := C29; (* KCC *)
+    delayedPCC := C29; (* always write delayedPCC together whether PCC so 
+                          that non-capability branches don't override PCC *)
+    SignalExceptionMIPS(ex, getCapBase(capRegToCapStruct(C29)));
+  }
+
+function unit ERETHook() =
+  {
+    nextPCC    := C31;
+    delayedPCC := C31; (* always write delayedPCC together whether PCC so 
+                          that non-capability branches don't override PCC *)
+  }
+
+function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) =
+  {
+    (CapCause.ExcCode) := CapExCode(capEx);
+    (CapCause.RegNum)  := regnum;
+    let mipsEx = 
+      if ((capEx == CapEx_CallTrap) | (capEx == CapEx_ReturnTrap)) 
+      then C2Trap else C2E in
+    SignalException(mipsEx);
+  }
+
+function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) =
+  raise_c2_exception8(capEx, 0b000 : regnum)
+
+function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) =
+  raise_c2_exception8(capEx, 0xff)
+
+function bool pcc_access_system_regs () = 
+      let pcc = capRegToCapStruct(PCC) in
+      (pcc.access_system_regs)
+
+function bool register_inaccessible((regno) r) = 
+  let is_sys_reg = switch(r) {
+    case 0b11011 -> true
+    case 0b11100 -> true
+    case 0b11101 -> true
+    case 0b11110 -> true
+    case 0b11111 -> true
+    case _       -> false
+  } in
+  if is_sys_reg then
+    not (pcc_access_system_regs ())
+  else
+    false
+
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag_reserve
+
+val extern (bit[64] , bit[8]) -> unit effect { wmem } TAGw
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag_conditional
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> unit effect { wmv } MEMval_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> bool effect { wmv } MEMval_tag_conditional
+
+
+function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) =
+{
+  (* assumes addr is cap. aligned *)
+  let ((bit[8]) tag : mem) = (MEMr_tag (addr, cap_size)) in
+  (tag[0], mem)
+}
+
+function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) =
+{
+  (* assumes addr is cap. aligned *)
+  let ((bit[8]) tag : mem) = (MEMr_tag_reserve (addr, cap_size)) in
+  (tag[0], mem)
+}
+
+function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
+{
+  (* assumes addr is cap. aligned *)
+  MEMea_tag(addr, cap_size);
+  MEMval_tag(addr, cap_size, 0b0000000 : [tag] :  data);
+}
+
+function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
+{
+  (* assumes addr is cap. aligned *)
+  MEMea_tag_conditional(addr, cap_size);
+  MEMval_tag_conditional(addr, cap_size, 0b0000000 : [tag] :  data);
+}
+
+function unit effect {wmem} MEMw_wrapper(addr, size, data) =
+  if (addr == 0x000000007f000000) then
+  {
+    UART_WDATA   := data[31..24];
+    UART_WRITTEN := 1;
+  }
+  else
+  {
+    (* On cheri non-capability writes must clear the corresponding tag
+       XXX this is vestigal and only works on sequential modle -- tag clearing
+       should probably be done in memory model. *)
+    TAGw((addr[63..4] : 0b0000), 0x00);
+    MEMea(addr,size);
+    MEMval(addr, size, data);
+  }
+
+function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
+  {
+    (* On cheri non-capability writes must clear the corresponding tag*)
+    MEMea_conditional(addr, size);
+    success := MEMval_conditional(addr,size,data);
+    if (success) then
+      (* XXX as above TAGw is vestigal and must die *)
+      TAGw((addr[63..4] : 0b0000), 0x00);
+    success;
+  }
+
+function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
+  {
+    capno := 0b00000;
+    cap := readCapReg(capno);
+    if (~(cap.tag)) then
+      (raise_c2_exception(CapEx_TagViolation, capno))
+    else if (cap.sealed) then
+        (raise_c2_exception(CapEx_SealViolation, capno));
+    switch (accessType) {
+      case Instruction -> if (~(cap.permit_execute)) then (raise_c2_exception(CapEx_PermitExecuteViolation, capno))
+      case LoadData    -> if (~(cap.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, capno))
+      case StoreData   -> if (~(cap.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, capno))
+    };
+    cursor := getCapCursor(cap);
+    vAddr  := cursor + unsigned(addr);
+    size   := wordWidthBytes(width);
+    base   := unsigned(getCapBase(cap));
+    top    := unsigned(getCapTop(cap));
+    if ((vAddr + size) > top) then
+      (raise_c2_exception(CapEx_LengthViolation, capno))
+    else if (vAddr < (base)) then
+      (raise_c2_exception(CapEx_LengthViolation, capno))
+    else
+      (bit[64]) vAddr; (* XXX vAddr not truncated because top <= 2^64 and size > 0 *)
+  }
+
+function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = {
+  incrementCP0Count();
+  let pcc = capRegToCapStruct(PCC) in
+  let base  = unsigned(getCapBase(pcc)) in
+  let top   = unsigned(getCapTop(pcc)) in
+  let absPC = (unsigned(vAddr)) in
+  if ((absPC mod 4)  != 0) then (* bad PC alignment *)
+    (SignalExceptionBadAddr(AdEL, (bit[64]) absPC)) (* XXX absPC may be truncated *)
+  else if ((absPC + 4) > top) then
+    (raise_c2_exception_noreg(CapEx_LengthViolation))
+  else
+    TLBTranslate((bit[64]) absPC, accessType) (* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps *)
+}
+
+function unit checkCP2usable () =
+      {
+        if (~((CP0Status.CU)[2])) then
+          {
+            (CP0Cause.CE) := 0b10;
+            (SignalException(CpU));
+          }
+      }
+
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 80350af1..8975193c 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -89,8 +89,9 @@ let ([:64:]) TLBNumEntries = 64
 typedef TLBIndexT = (bit[6])
 let (TLBIndexT) TLBIndexMax = 0b111111
 
-let MAX_VA = unsigned(0xffffffffff)
-let MAX_PA = unsigned(0xfffffffff)
+let MAX_U64 = unsigned(0xffffffffffffffff)
+let MAX_VA  = unsigned(0xffffffffff)
+let MAX_PA  = unsigned(0xfffffffff)
 
 typedef TLBEntry = register bits [116 : 0] {
   116 ..  101: pagemask;
diff --git a/src/Makefile b/src/Makefile
index fb71396d..594f5c15 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -42,6 +42,8 @@ CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri
 CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
+CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts_128.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+
 elf:
 	make -C $(ELFDIR)
 
@@ -56,6 +58,10 @@ _build/run_with_elf_cheri.ml: lem_interp/run_with_elf_cheri.ml
 	mkdir -p _build
 	cp $< $@
 
+_build/run_with_elf_cheri128.ml: lem_interp/run_with_elf_cheri128.ml
+	mkdir -p _build
+	cp $< $@
+
 _build/mips.lem: $(MIPS_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
@@ -76,6 +82,11 @@ _build/cheri.lem: $(CHERI_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o cheri $(CHERI_SAILS)
 
+_build/cheri128.lem: $(CHERI128_SAILS) ./sail.native
+	mkdir -p _build
+	cd _build ;\
+	../sail.native -lem_ast -o cheri128 $(CHERI128_SAILS)
+
 _build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
@@ -111,6 +122,9 @@ run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml int
 run_cheri.native:  _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
 	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml  -o run_cheri.native
 
+run_cheri128.native:  _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml interpreter
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml  -o run_cheri128.native
+
 mips_notlb: _build/mips_notlb.ml  _build/mips_embed_types.lem _build/mips_extras.ml
 	true