Merge branch 'sail2' into cheri-mono

In order to use up-to-date sequential CHERI model for test suite

5 files changed, 59 insertions, 169 deletions

diff --git a/cheri/Makefile b/cheri/Makefile
index 72eaf26b..421c4460 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -31,15 +31,24 @@ cheri_trace: $(CHERI_SAILS) $(CHERI_MAIN)
 cheri.c: $(CHERI_SAILS) $(CHERI_MAIN)
 	$(SAIL) -memo_z3 -c $^ 1> $@
 
-latex: $(CHERI_SAILS)
+latex_128: $(MIPS_SAIL_DIR)/prelude.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail
+	rm -rf sail_latexcc
+	$(SAIL) -latex -latex_prefix sailcc -o sail_latexcc $^
+
+latex_256: $(CHERI_SAILS)
+	rm -rf sail_latex
 	$(SAIL) -latex $^
 
+latex: latex_128 latex_256
+
 cheri128: $(CHERI128_SAILS) $(CHERI_MAIN)
 	$(SAIL) -ocaml -o $@ $^
 
 cheri128_trace: $(CHERI128_SAILS) $(CHERI_MAIN)
 	$(SAIL) -ocaml_trace -o $@ $^
 
+LOC_FILES:=$(CHERI_SAILS) $(CHERI_MAIN)
+include ../etc/loc.mk
 
 # TODO Using bit lists for now in Lem generation; for machine words,
 # monomorphisation is needed due to some variable length bitvectors, e.g. in
@@ -50,7 +59,7 @@ cheri_no_tlb.lem: $(CHERI_NO_TLB_SAILS)
 	$(SAIL) -lem -o cheri_no_tlb -lem_lib Mips_extras -undefined_gen -memo_z3 $^
 cheri_no_tlb_types.lem: cheri_no_tlb.lem
 
-cheri.lem: $(CHERI_SAILS)
+cheri.lem: $(CHERI_SAILS) $(CHERI_MAIN)
 	$(SAIL) -lem -o cheri -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^
 cheri_types.lem: cheri.lem
 
@@ -75,54 +84,4 @@ C%.thy: c%.lem c%_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem
 	lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
 
 clean:
-	rm -rf cheri cheri128 _sbuild inst_*.sail cheri.c
-
-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,CGetPerms)
-	$(call EXTRACT_INST,CGetType)
-	$(call EXTRACT_INST,CGetBase)
-	$(call EXTRACT_INST,CGetOffset)
-	$(call EXTRACT_INST,CGetLen)
-	$(call EXTRACT_INST,CGetTag)
-	$(call EXTRACT_INST,CGetSealed)
-	$(call EXTRACT_INST,CGetAddr)
-	$(call EXTRACT_INST,CGetPCC)
-	$(call EXTRACT_INST,CGetPCCSetOffset)
-	$(call EXTRACT_INST,CGetCause)
-	$(call EXTRACT_INST,CSetCause)
-	$(call EXTRACT_INST,CAndPerm)
-	$(call EXTRACT_INST,CToPtr)
-	$(call EXTRACT_INST,CSub)
-	$(call EXTRACT_INST,CPtrCmp)
-	$(call EXTRACT_INST,CIncOffset)
-	$(call EXTRACT_INST,CIncOffsetImmediate)
-	$(call EXTRACT_INST,CSetOffset)
-	$(call EXTRACT_INST,CSetBounds)
-	$(call EXTRACT_INST,CSetBoundsImmediate)
-	$(call EXTRACT_INST,CSetBoundsExact)
-	$(call EXTRACT_INST,CClearTag)
-	$(call EXTRACT_INST,CMOVX)
-	$(call EXTRACT_INST,ClearRegs)
-	$(call EXTRACT_INST,CFromPtr)
-	$(call EXTRACT_INST,CBuildCap)
-	$(call EXTRACT_INST,CCopyType)
-	$(call EXTRACT_INST,CCheckPerm)
-	$(call EXTRACT_INST,CCheckType)
-	$(call EXTRACT_INST,CTestSubset)
-	$(call EXTRACT_INST,CSeal)
-	$(call EXTRACT_INST,CCSeal)
-	$(call EXTRACT_INST,CUnseal)
-	$(call EXTRACT_INST,CCall)
-	$(call EXTRACT_INST,CCall2)
-	$(call EXTRACT_INST,CReturn)
-	$(call EXTRACT_INST,CBtag)
-	$(call EXTRACT_INST,CBz)
-	$(call EXTRACT_INST,CJALR)
-	$(call EXTRACT_INST,CLoad)
-	$(call EXTRACT_INST,CStore)
-	$(call EXTRACT_INST,CSC)
-	$(call EXTRACT_INST,CLC)
-	$(call EXTRACT_INST,CReadHwr)
-	$(call EXTRACT_INST,CWriteHwr)
-
+	rm -rf cheri cheri_trace cheri128 cheri128_trace _sbuild inst_*.sail cheri.c sail_latex sail_latexcc
diff --git a/cheri/ROOT b/cheri/ROOT
new file mode 100644
index 00000000..244413d5
--- /dev/null
+++ b/cheri/ROOT
@@ -0,0 +1,4 @@
+session "Sail-CHERI" = "Sail" +
+  options [document = false]
+  theories
+    Cheri_lemmas
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 0a4538b9..2f083411 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -203,19 +203,16 @@ union clause ast = CGetAddr   : (regno, regno)
 
 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) = zero_extend(getCapPerms(capVal));
-  /* END_CGetPerms */
 }
 
 function clause execute (CGetType(rd, cb)) =
 {
-  /* START_CGetType */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
@@ -224,36 +221,30 @@ function clause execute (CGetType(rd, cb)) =
     wGPR(rd) = if (capVal.sealed)
       then zero_extend(capVal.otype)
       else (bitone ^^ 64)
-  /* 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) = to_bits(64, 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) = to_bits(64, getCapOffset(capVal));
-  /* END_CGetOffset */
 }
 
 function clause execute (CGetLen(rd, cb)) =
 {
-  /* START_CGetLen */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
@@ -261,49 +252,41 @@ function clause execute (CGetLen(rd, cb)) =
     let capVal = readCapReg(cb) in
     let len65  = getCapLength(capVal) in
     wGPR(rd) = to_bits(64, if len65 > MAX_U64 then MAX_U64 else len65);
-  /* 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) = zero_extend(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) = zero_extend(capVal.sealed);
-  /* END_CGetSealed */
 }
 
 function clause execute (CGetAddr(rd, cb)) =
 {
-  /* START_CGetAddr */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
     wGPR(rd) = to_bits(64, getCapCursor(capVal));
-  /* END_CGetAddr */
 }
 
 union clause ast = CGetPCC : regno
 function clause execute (CGetPCC(cd)) =
 {
-  /* START_CGetPCC */
   checkCP2usable();
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
@@ -312,14 +295,12 @@ function clause execute (CGetPCC(cd)) =
     let (success, pcc2) = setCapOffset(pcc, PC) in
     {assert (success, ""); /* guaranteed to be in-bounds */
     writeCapReg(cd, pcc2)};
-  /* END_CGetPCC */
 }
 
 
 union clause ast = CGetPCCSetOffset : (regno, regno)
 function clause execute (CGetPCCSetOffset(cd, rs)) =
 {
-  /* START_CGetPCCSetOffset */
   checkCP2usable();
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
@@ -331,26 +312,22 @@ function clause execute (CGetPCCSetOffset(cd, rs)) =
         writeCapReg(cd, newPCC)
     else
         writeCapReg(cd, int_to_cap(rs_val));
-  /* END_CGetPCCSetOffset */
 }
 /* Get and Set CP2 cause register */
 
 union clause ast = CGetCause : regno
 function clause execute (CGetCause(rd)) = 
 {
-  /* START_CGetCause */
   checkCP2usable();
   if not (pcc_access_system_regs ()) then
     raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation)
   else
     wGPR(rd) = zero_extend(CapCause.bits())
-  /* END_CGetCause */
 }
 
 union clause ast = CSetCause : regno
 function clause execute (CSetCause(rt)) = 
 {
-  /* START_CSetCause */
   checkCP2usable();
   if not (pcc_access_system_regs ()) then
     raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation)
@@ -360,13 +337,11 @@ function clause execute (CSetCause(rt)) =
       CapCause->ExcCode() = rt_val[15..8];
       CapCause->RegNum()  = rt_val[7..0];
     }
-  /* END_CSetCause */
 }
 
 union clause ast = CReadHwr : (regno, regno)
 function clause execute (CReadHwr(cd, sel)) = 
 {
-  /* START_CReadHwr */
   checkCP2usable();
   let (needSup, needAccessSys) : (bool, bool) = match unsigned(sel) {
     0  => (false, false), /* DDC   -- no access control */
@@ -399,13 +374,11 @@ function clause execute (CReadHwr(cd, sel)) =
     };
     writeCapReg(cd, capVal);
   };
-  /* END_CReadHwr */
 }
 
 union clause ast = CWriteHwr : (regno, regno)
 function clause execute (CWriteHwr(cb, sel)) = 
 {
-  /* START_CWriteHwr */
   checkCP2usable();
   let (needSup, needAccessSys) : (bool, bool) = match unsigned(sel) {
     0  => (false, false), /* DDC   -- no access control */
@@ -438,13 +411,11 @@ function clause execute (CWriteHwr(cb, sel)) =
       _  => assert(false, "should be unreachable code")
     };
   };
-  /* END_CWriteHwr */
 }
 
 union clause ast = CAndPerm : (regno, regno, regno)
 function clause execute(CAndPerm(cd, cb, rt)) = 
 {
-  /* START_CAndPerm */
   checkCP2usable();
   let cb_val = readCapReg(cb);
   let rt_val = rGPR(rt);
@@ -460,7 +431,6 @@ function clause execute(CAndPerm(cd, cb, rt)) =
     let perms   = getCapPerms(cb_val) in
     let newCap  = setCapPerms(cb_val, (perms & rt_val[30..0])) in
     writeCapReg(cd, newCap);
-  /* END_CAndPerm */
 }
 
 
@@ -468,7 +438,6 @@ function clause execute(CAndPerm(cd, cb, rt)) =
 union clause ast = CToPtr : (regno, regno, regno)
 function clause execute(CToPtr(rd, cb, ct)) = 
 {
-  /* START_CToPtr */
   checkCP2usable();
   let ct_val = readCapReg(ct);
   let cb_val = readCapReg(cb);
@@ -493,7 +462,6 @@ function clause execute(CToPtr(rd, cb, ct)) =
         else
           to_bits(64, getCapCursor(cb_val) - ctBase)
     }
-  /* END_CToPtr */
 }
 
 
@@ -501,7 +469,6 @@ function clause execute(CToPtr(rd, cb, ct)) =
 union clause ast = CSub : (regno, regno, regno)
 function clause execute(CSub(rd, cb, ct)) = 
 {
-  /* START_CSub */
   checkCP2usable();
   let ct_val = readCapReg(ct);
   let cb_val = readCapReg(cb);
@@ -513,13 +480,11 @@ function clause execute(CSub(rd, cb, ct)) =
     {
       wGPR(rd) = to_bits(64, getCapCursor(cb_val) - getCapCursor(ct_val))
     }
-  /* END_CSub */
 }
 
 union clause ast = CPtrCmp : (regno, regno, regno, CPtrCmpOp)
 function clause execute(CPtrCmp(rd, cb, ct, op)) = 
 {
-  /* START_CPtrCmp */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
@@ -560,13 +525,11 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
       };
       wGPR(rd) = zero_extend (cmp)
     }
-  /* END_CPtrCmp */
 }
 
 union clause ast = CIncOffset : (regno, regno, regno)
 function clause execute (CIncOffset(cd, cb, rt)) =
 {
-  /* START_CIncOffset */
   checkCP2usable();
   cb_val = readCapReg(cb);
   rt_val = rGPR(rt);
@@ -582,13 +545,11 @@ function clause execute (CIncOffset(cd, cb, rt)) =
         writeCapReg(cd, newCap)
     else
         writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + rt_val))
-  /* END_CIncOffset */
 }
 
 union clause ast = CIncOffsetImmediate : (regno, regno, bits(11))
 function clause execute (CIncOffsetImmediate(cd, cb, imm)) =
 {
-  /* START_CIncOffsetImmediate */
   checkCP2usable();
   let cb_val = readCapReg(cb);
   let imm64 : bits(64) = sign_extend(imm) in
@@ -604,13 +565,11 @@ function clause execute (CIncOffsetImmediate(cd, cb, imm)) =
         writeCapReg(cd, newCap)
     else
         writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + imm64))
-  /* END_CIncOffsetImmediate */
 }
 
 union clause ast = CSetOffset : (regno, regno, regno)
 function clause execute (CSetOffset(cd, cb, rt)) =
 {
-  /* START_CSetOffset */
   checkCP2usable();
   let cb_val = readCapReg(cb);
   let rt_val = rGPR(rt);
@@ -626,13 +585,11 @@ function clause execute (CSetOffset(cd, cb, rt)) =
         writeCapReg(cd, newCap)
     else
         writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + rt_val))
-  /* END_CSetOffset */
 }
 
 union clause ast = CSetBounds : (regno, regno, regno)
 function clause execute (CSetBounds(cd, cb, rt)) =
 {
-  /* START_CSetBounds */
   checkCP2usable();
   let cb_val = readCapReg(cb);
   let rt_val = unsigned(rGPR(rt));
@@ -655,13 +612,11 @@ function clause execute (CSetBounds(cd, cb, rt)) =
   else
     let (_, newCap) = setCapBounds(cb_val, to_bits(64, cursor), to_bits(65, newTop)) in
     writeCapReg(cd, newCap) /* ignore exact */
-  /* END_CSetBounds */
 }
 
 union clause ast = CSetBoundsImmediate : (regno, regno, bits(11))
 function clause execute (CSetBoundsImmediate(cd, cb, imm)) =
 {
-  /* START_CSetBoundsImmediate */
   checkCP2usable();
   cb_val = readCapReg(cb);
   immU   = unsigned(imm);
@@ -684,13 +639,11 @@ function clause execute (CSetBoundsImmediate(cd, cb, imm)) =
   else
     let (_, newCap) = setCapBounds(cb_val, to_bits(64, cursor), to_bits(65, newTop)) in
     writeCapReg(cd, newCap) /* ignore exact */
-  /* END_CSetBoundsImmediate */
 }
 
 union clause ast = CSetBoundsExact : (regno, regno, regno)
 function clause execute (CSetBoundsExact(cd, cb, rt)) =
 {
-  /* START_CSetBoundsExact */
   checkCP2usable();
   cb_val = readCapReg(cb);
   rt_val = unsigned(rGPR(rt));
@@ -716,13 +669,11 @@ function clause execute (CSetBoundsExact(cd, cb, rt)) =
         raise_c2_exception(CapEx_InexactBounds, cb)
     else
         writeCapReg(cd, newCap)
-  /* END_CSetBoundsExact */
 }
 
 union clause ast = CClearTag : (regno, regno)
 function clause execute (CClearTag(cd, cb)) =
 {
-  /* START_CClearTag */
   checkCP2usable();
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
@@ -733,13 +684,11 @@ function clause execute (CClearTag(cd, cb)) =
       cb_val = readCapReg(cb);
       writeCapReg(cd, {cb_val with tag=false});
     }
-  /* END_CClearTag */
 }
 
 union clause ast = CMOVX : (regno,regno,regno,bool)
 function clause execute (CMOVX(cd, cb, rt, ismovn)) =
 {
-  /* START_CMOVX */
   checkCP2usable();
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
@@ -747,13 +696,11 @@ function clause execute (CMOVX(cd, cb, rt, ismovn)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else if ((rGPR(rt) == zeros()) ^ ismovn) then
     writeCapReg(cd) = readCapReg(cb);
-  /* END_CMOVX */
 }
 
 union clause ast = ClearRegs : (ClearRegSet, bits(16))
 function clause execute (ClearRegs(regset, m)) =
 {
-  /* START_ClearRegs */
   if ((regset == CLo) | (regset == CHi)) then
     checkCP2usable();
   if (regset == CHi) then
@@ -769,13 +716,11 @@ function clause execute (ClearRegs(regset, m)) =
         CLo   => writeCapReg(to_bits(5, i)) = null_cap,
         CHi   => writeCapReg(to_bits(5, i+16)) = null_cap
       }
-  /* END_ClearRegs */
 }
 
 union clause ast = CFromPtr : (regno, regno, regno)
 function clause execute (CFromPtr(cd, cb, rt)) =
 {
-  /* START_CFromPtr */
   checkCP2usable();
   cb_val = readCapReg(cb);
   rt_val = rGPR(rt);
@@ -795,13 +740,11 @@ function clause execute (CFromPtr(cd, cb, rt)) =
         writeCapReg(cd, newCap)
     else
         writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + rt_val))
-  /* END_CFromPtr */
 }
 
 union clause ast = CBuildCap : (regno, regno, regno)
 function clause execute (CBuildCap(cd, cb, ct)) =
 {
-  /* START_CBuildCap */
   checkCP2usable();
   cb_val = readCapReg(cb);
   ct_val = readCapReg(ct);
@@ -839,14 +782,12 @@ function clause execute (CBuildCap(cd, cb, ct)) =
       assert(representable, ""); /* similarly offset should be representable XXX except for fastRepCheck */
       writeCapReg(cd, cd3);
     }
-  /* END_CBuildCap */
 }
 
 union clause ast = CCopyType : (regno, regno, regno)
 function clause execute (CCopyType(cd, cb, ct)) =
 {
-  /* START_CCopyType */
-    checkCP2usable();
+  checkCP2usable();
   cb_val = readCapReg(cb);
   ct_val = readCapReg(ct);
   cb_base = getCapBase(cb_val);
@@ -874,13 +815,11 @@ function clause execute (CCopyType(cd, cb, ct)) =
       }
   } else
     writeCapReg(cd, int_to_cap(bitone ^^ 64))
-  /* END_CCopyType */
 }
 
 union clause ast = CCheckPerm : (regno, regno)
 function clause execute (CCheckPerm(cs, rt)) =
 {
-  /* START_CCheckPerm */
   checkCP2usable();
   cs_val = readCapReg(cs);
   cs_perms : bits(64) = zero_extend(getCapPerms(cs_val));
@@ -891,13 +830,11 @@ function clause execute (CCheckPerm(cs, rt)) =
     raise_c2_exception(CapEx_TagViolation, cs)
   else if ((cs_perms & rt_perms) != rt_perms) then
     raise_c2_exception(CapEx_UserDefViolation, cs)
-  /* END_CCheckPerm */
 }
 
 union clause ast = CCheckType : (regno, regno)
 function clause execute (CCheckType(cs, cb)) =
 {
-  /* START_CCheckType */
   checkCP2usable();
   cs_val = readCapReg(cs);
   cb_val = readCapReg(cb);
@@ -915,13 +852,11 @@ function clause execute (CCheckType(cs, cb)) =
     raise_c2_exception(CapEx_SealViolation, cb)
   else if ((cs_val.otype) != (cb_val.otype)) then
     raise_c2_exception(CapEx_TypeViolation, cs)
-  /* END_CCheckType */
 }
 
 union clause ast = CTestSubset : (regno, regno, regno)
 function clause execute (CTestSubset(rd, cb, ct)) =
 {
-  /* START_CTestSubset */
   checkCP2usable();
   cb_val = readCapReg(cb);
   ct_val = readCapReg(ct);
@@ -948,13 +883,11 @@ function clause execute (CTestSubset(rd, cb, ct)) =
              0b1;
      wGPR(rd) = zero_extend(result);
   }
-  /* END_CTestSubset */
 }
 
 union clause ast = CSeal : (regno, regno, regno)
 function clause execute (CSeal(cd, cs, ct)) =
 {
-  /* START_CSeal */
   checkCP2usable();
   cs_val = readCapReg(cs);
   ct_val = readCapReg(ct);
@@ -989,13 +922,11 @@ function clause execute (CSeal(cd, cs, ct)) =
         raise_c2_exception(CapEx_InexactBounds, cs)
     else
         writeCapReg(cd, newCap)
-  /* END_CSeal */
 }
 
 union clause ast = CCSeal : (regno, regno, regno)
 function clause execute (CCSeal(cd, cs, ct)) =
 {
-  /* START_CCSeal */
   checkCP2usable();
   cs_val = readCapReg(cs);
   ct_val = readCapReg(ct);
@@ -1030,13 +961,11 @@ function clause execute (CCSeal(cd, cs, ct)) =
         raise_c2_exception(CapEx_InexactBounds, cs)
     else
         writeCapReg(cd, newCap)
-  /* END_CCSeal */
 }
 
 union clause ast = CUnseal : (regno, regno, regno)
 function clause execute (CUnseal(cd, cs, ct)) =
 {
-  /* START_CUnseal */
   checkCP2usable();
   cs_val = readCapReg(cs);
   ct_val = readCapReg(ct);
@@ -1069,14 +998,12 @@ function clause execute (CUnseal(cd, cs, ct)) =
       otype=zeros(),
       global=(cs_val.global & ct_val.global)
     })
-  /* END_CUnseal */
 }
 
 union clause ast = CCall : (regno, regno, bits(11))
 function clause execute (CCall(cs, cb, 0b00000000000)) = /* selector=0 */
 {
   /* 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);
@@ -1105,13 +1032,11 @@ function clause execute (CCall(cs, cb, 0b00000000000)) = /* selector=0 */
     raise_c2_exception(CapEx_LengthViolation, cs)
   else
     raise_c2_exception(CapEx_CallTrap, cs);
-  /* END_CCall */
 }
 
 function clause execute (CCall(cs, cb, 0b00000000001)) = /* selector=1 */
 {
   /* Jump-like implementation of CCall that unseals arguments */
-  /* START_CCall2 */
   checkCP2usable();
   cs_val = readCapReg(cs);
   cb_val = readCapReg(cb);
@@ -1154,22 +1079,18 @@ function clause execute (CCall(cs, cb, 0b00000000001)) = /* selector=1 */
         otype=zeros()
       });
     }
-  /* END_CCall2 */
 }
 
 union clause ast = CReturn : unit
 function clause execute (CReturn()) =
 {
-  /* START_CReturn */
   checkCP2usable();
   raise_c2_exception_noreg(CapEx_ReturnTrap)
-  /* END_CReturn */
 }
 
 union clause ast = CBX : (regno, bits(16), bool)
 function clause execute (CBX(cb, imm, notset)) =
 {
-  /* START_CBtag */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
@@ -1178,13 +1099,11 @@ function clause execute (CBX(cb, imm, notset)) =
       let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in
       execute_branch(PC + offset);
     }
-  /* END_CBtag */
 }
 
 union clause ast = CBZ : (regno, bits(16), bool)
 function clause execute (CBZ(cb, imm, notzero)) =
 {
-  /* START_CBz */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
@@ -1193,13 +1112,11 @@ function clause execute (CBZ(cb, imm, notzero)) =
       let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in
       execute_branch(PC + offset);
     }
-  /* END_CBz */
 }
 
 union clause ast = CJALR : (regno, regno, bool)
 function clause execute(CJALR(cd, cb, link)) = 
 {
-  /* START_CJALR */
   checkCP2usable();
   cb_val = readCapReg(cb);
   cb_ptr = getCapCursor(cb_val);
@@ -1232,13 +1149,11 @@ function clause execute(CJALR(cd, cb, link)) =
             assert(false, "");
       execute_branch_pcc(cb_val);
     }
-  /* END_CJALR */
 }
 
 union clause ast = CLoad : (regno, regno, regno, bits(8), bool, WordType, bool)
 function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
 {
-  /* START_CLoad */
   checkCP2usable();
   cb_val = readCapReg(cb);
   if (register_inaccessible(cb)) then
@@ -1275,14 +1190,12 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
           wGPR(rd) = memResult;
         }
     }
-  /* END_CLoad */
 }
 
 union clause ast = CStore : (regno, regno, regno, regno, bits(8), WordType, bool)
 
 function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
 {
-  /* START_CStore */
   checkCP2usable();
   cb_val = readCapReg(cb);
   if (register_inaccessible(cb)) then
@@ -1333,13 +1246,11 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
             }
         }
     }
-  /* END_CStore */
 }
 
 union clause ast = CSC : (regno, regno, regno, regno, bits(11), bool)
 function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
 {
-  /* START_CSC */
   checkCP2usable();
   cs_val = readCapReg(cs);
   cb_val = readCapReg(cb);
@@ -1385,13 +1296,11 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
             MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val));
         }
     }
-  /* END_CSC */
 }
 
 union clause ast = CLC : (regno, regno, regno, bits(11), bool)
 function clause execute (CLC(cd, cb, rt, offset, linked)) =  
 {
-  /* START_CLC */
   checkCP2usable();
   cb_val = readCapReg(cb);
   if (register_inaccessible(cd)) then
@@ -1433,7 +1342,6 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
             }
         }
     }
-  /* END_CLC */
 }
 
 union clause ast = C2Dump : regno
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index 5590bbb8..babfc117 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -196,20 +196,32 @@ function sealCap(cap, otype) : (CapStruct, bits(24)) -> (bool, CapStruct) =
     (true, {cap with sealed=true, otype=otype})
 
 function getCapBase(c)   : CapStruct -> uint64 = unsigned(c.base)
-function getCapTop(c)    : CapStruct -> CapLen = unsigned(c.base) + unsigned(c.length)
+function getCapTop(c)    : CapStruct -> CapLen = unsigned(c.base) + unsigned(c.length) /* XXX bug here? -- should be mod 2^64 */
 function getCapOffset(c) : CapStruct -> uint64 = (unsigned(c.address) - unsigned(c.base)) % (pow2(64))
 function getCapLength(c) : CapStruct -> CapLen = unsigned(c.length)
 
 function getCapCursor(c) : CapStruct -> uint64 = unsigned(c.address)
 
-function setCapOffset(c, offset) : (CapStruct, bits(64)) -> (bool, CapStruct) =
+/*!
+Set the offset capability of the a capability to given value and return the result, along with a boolean indicating true if the operation preserved the existing bounds of the capability.  When using compressed capabilities, setting the offset far outside the capability bounds can cause the result to become unrepresentable (XXX mention guarantees). Additionally in some implementations a fast representablity check may be used that could cause the operation to return failure even though the capability would be representable (XXX provide details). 
+ */
+val setCapOffset : (CapStruct, bits(64)) -> (bool, CapStruct)
+function setCapOffset(c, offset) =
     (true, {c with address=c.base + offset})
 
-function incCapOffset(c, delta) : (CapStruct, bits(64)) -> (bool, CapStruct) =
+/*!
+\function{incCapOffset} is the same as \function{setCapOffset} except that the 64-bit value is added to the current capability offset modulo $2^{64}$ (i.e. signed twos-complement arithemtic).
+ */
+val incCapOffset : (CapStruct, bits(64)) -> (bool, CapStruct)
+function incCapOffset(c, delta) =
     let newAddr : bits(64) = c.address + delta in
     (true, {c with address = newAddr})
 
-function setCapBounds(cap, base, top) : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct) =
+/*!
+Returns a capability derived from the given capability by setting the base and top to values provided.  The offset of the resulting capability is zero.  In case the requested bounds are not exactly representable the returned boolean is false and the returned capability has bounds at least including the region bounded by base and top but rounded to representable values.
+ */
+val setCapBounds : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct)
+function setCapBounds(cap, base, top) =
     let length : bits(65) = top - (0b0 @ base) in
     (true, {cap with base = base, length = length[63..0], address = base})
 
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index ecb98ef8..47c8759c 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -128,7 +128,11 @@ let CapRegs : vector(32, dec, register(CapReg)) =
 let max_otype = MAX(24) /*0xffffff*/
 let have_cp2 = true
 
-function readCapReg(n) : regno -> CapStruct =
+/*!
+This function reads a given capability register and returns its contents converted to a CapStruct.
+*/
+val readCapReg : regno -> CapStruct effect {rreg}
+function readCapReg(n) =
   let 'i = unsigned(n) in
   capRegToCapStruct(reg_deref(CapRegs[i]))
 
@@ -257,21 +261,17 @@ function pcc_access_system_regs () =
       let pcc = capRegToCapStruct(PCC) in
       (pcc.access_system_regs)
 
+/*!
+The following function should be called before reading or writing any capability register to check whether it is one of the protected system capabilities. Although it is usually a general purpose capabilty the invoked data capabiltiy (IDC) is restricted in the branch delay slot of the CCall (selector one) instruction to protect the confidentiality and integrity of the invoked sandbox.
+ */
 val register_inaccessible : regno -> bool effect {rreg}
 function register_inaccessible(r) =
-  if (r == IDC) & inCCallDelay then true else
-  let is_sys_reg : bool = match r {
-    0b11011  => true,
-    0b11100  => true,
-    0b11101  => true,
-    0b11110  => true,
-    0b11111  => true,
-    _        => false
-  } in
-  if is_sys_reg then
-    not (pcc_access_system_regs ())
-  else
-    false
+  ((r == IDC) & inCCallDelay) |
+  ((r == KR1C |
+    r == KR2C |
+    r == KDC  |
+    r == KCC  |
+    r == EPCC) & not (pcc_access_system_regs ()))
 
 val MEMr_tag = "read_tag_bool"  : bits(64) -> bool effect { rmemt }
 val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt }
@@ -399,13 +399,20 @@ function TranslatePC (vAddr) = {
   else
     TLBTranslate(to_bits(64, absPC), Instruction) /* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps */
 }
+
+/*!  
+All capability instrucitons must first check that the capability
+co-processor is enabled using the following function that raises a
+co-processor unusable exception if a CP0Status.CU2 is not set. This
+allows the operating system to only save and restore the full
+capability context for processes that use capabilities.
+*/
 val checkCP2usable : unit -> unit effect {rreg, wreg, escape}
 function checkCP2usable ()  =
-  if not ((CP0Status.CU())[2]) then
-    {
-      (CP0Cause->CE()) = 0b10;
-      (SignalException(CpU));
-    }
+  if not (CP0Status.CU()[2]) then {
+    CP0Cause->CE() = 0b10;
+    SignalException(CpU);
+  }
 
 function init_cp2_state () = {
   let defaultBits = capStructToCapReg(default_cap);