cheri wip.

6 files changed, 1212 insertions, 1150 deletions

diff --git a/cheri/Makefile b/cheri/Makefile
index 813902a2..a443d123 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -1,5 +1,25 @@
-EXTRACT_INST=sed -n "/START_${1}\b/,/END_${1}\b/p" cheri_insts.sail | sed 's/^  //;1d;$$d' > inst_$1.sail
+THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST)))
+SAIL_DIR:=$(realpath $(dir $(THIS_MAKEFILE))..)
+export SAIL_DIR
+SAIL_LIB_DIR:=$(SAIL_DIR)/lib
+MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc
+CHERI_SAIL_DIR:=$(SAIL_DIR)/cheri
+SAIL:=$(SAIL_DIR)/sail
+SAIL_LIB_HEADERS:=$(SAIL_LIB_DIR)/flow.sail
+
+MIPS_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail
+
+CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.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:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail  $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.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: $(CHERI_SAILS)
+	$(SAIL) -ocaml -o cheri $(CHERI_SAILS)
+
+clean:
+	rm -rf _sbuild
+
+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)
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index f6b8818e..3d27fde3 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -1,309 +1,307 @@
-(*========================================================================*)
-(*                                                                        *)
-(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
-(*  Copyright (c) 2015-2017 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.                                                          *)
-(*========================================================================*)
-
-(* Old encodings *)
-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))
-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 : 0b00000 : (regno) rd :    0b00000 : 0b00000000 : 0b100) = Some(CGetCause(rd))
-
-function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn)
-
-function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetOffset(rd, cb)) (* NB encoding does not follow pattern *)
-function clause decode (0b010010 : 0b00100 : 0b00000 : 0b00000 : (regno) rt : 0b000 : 0b100) = Some(CSetCause(rt))
-function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CAndPerm(cd, cb, rt))
-function clause decode (0b010010 : 0b01100 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CToPtr(rd, cb, ct))
-
-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 decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b111) = Some(CPtrCmp(rd, cb, ct, CNEXEQ))
-function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CIncOffset(cd, cb, rt))
-function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b001) = Some(CSetOffset(cd, cb, rt))
-function clause decode (0b010010 : 0b00001 : (regno) cd : (regno) cb : (regno) rt : 0b000000)      = Some(CSetBounds(cd, cb, rt))
-
-function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : 0b00000 : 0b000: 0b101)    = Some(CClearTag(cd, cb))
-function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000: 0b111) = Some(CFromPtr(cd, cb, rt))
-function clause decode (0b010010 : 0b01011 : (regno) cs : 0b00000 : (regno) rt : 0b000: 0b000) = Some(CCheckPerm(cs, rt))
-function clause decode (0b010010 : 0b01011 : (regno) cs : (regno) cb : 0b00000 : 0b000: 0b001) = Some(CCheckType(cs, cb))
-function clause decode (0b010010 : 0b00010 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CSeal(cd, cs, ct))
-function clause decode (0b010010 : 0b00011 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CUnseal(cd, cs, ct))
-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 *)
-
-
-(* 
+/*========================================================================*/
+/*                                                                        */
+/*  Copyright (c) 2015-2017 Robert M. Norton                              */
+/*  Copyright (c) 2015-2017 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.                                                          */
+/*========================================================================*/
+
+/* Old encodings */
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b000) = Some(CGetPerm(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b001) = Some(CGetType(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b010) = Some(CGetBase(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b011) = Some(CGetLen(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b101) = Some(CGetTag(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b110) = Some(CGetSealed(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @    0b00000 @ 0b00000000 @ 0b100) = Some(CGetCause(rd))
+
+function clause decode (0b010010 @ 0b00110 @ 0b000000000000000000000) = Some(CReturn)
+
+function clause decode (0b010010 @ 0b01101 @ rd : regno @ cb : regno @ 0b00000000 @ 0b010) = Some(CGetOffset(rd, cb)) /* NB encoding does not follow pattern */
+function clause decode (0b010010 @ 0b00100 @ 0b00000 @ 0b00000 @ rt : regno @ 0b000 @ 0b100) = Some(CSetCause(rt))
+function clause decode (0b010010 @ 0b00100 @ cd : regno @ cb : regno @ rt : regno @ 0b000 @ 0b000) = Some(CAndPerm(cd, cb, rt))
+function clause decode (0b010010 @ 0b01100 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b000) = Some(CToPtr(rd, cb, ct))
+
+function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b000) = Some(CPtrCmp(rd, cb, ct, CEQ))
+function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b001) = Some(CPtrCmp(rd, cb, ct, CNE))
+function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b010) = Some(CPtrCmp(rd, cb, ct, CLT))
+function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b011) = Some(CPtrCmp(rd, cb, ct, CLE))
+function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b100) = Some(CPtrCmp(rd, cb, ct, CLTU))
+function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b101) = Some(CPtrCmp(rd, cb, ct, CLEU))
+function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b110) = Some(CPtrCmp(rd, cb, ct, CEXEQ))
+function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b111) = Some(CPtrCmp(rd, cb, ct, CNEXEQ))
+function clause decode (0b010010 @ 0b01101 @ cd : regno @ cb : regno @ rt : regno @ 0b000 @ 0b000) = Some(CIncOffset(cd, cb, rt))
+function clause decode (0b010010 @ 0b01101 @ cd : regno @ cb : regno @ rt : regno @ 0b000 @ 0b001) = Some(CSetOffset(cd, cb, rt))
+function clause decode (0b010010 @ 0b00001 @ cd : regno @ cb : regno @ rt : regno @ 0b000000)      = Some(CSetBounds(cd, cb, rt))
+
+function clause decode (0b010010 @ 0b00100 @ cd : regno @ cb : regno @ 0b00000 @ 0b000@ 0b101)    = Some(CClearTag(cd, cb))
+function clause decode (0b010010 @ 0b00100 @ cd : regno @ cb : regno @ rt : regno @ 0b000@ 0b111) = Some(CFromPtr(cd, cb, rt))
+function clause decode (0b010010 @ 0b01011 @ cs : regno @ 0b00000 @ rt : regno @ 0b000@ 0b000) = Some(CCheckPerm(cs, rt))
+function clause decode (0b010010 @ 0b01011 @ cs : regno @ cb : regno @ 0b00000 @ 0b000@ 0b001) = Some(CCheckType(cs, cb))
+function clause decode (0b010010 @ 0b00010 @ cd : regno @ cs : regno @ ct : regno @ 0b000@ 0b000) = Some(CSeal(cd, cs, ct))
+function clause decode (0b010010 @ 0b00011 @ cd : regno @ cs : regno @ ct : regno @ 0b000@ 0b000) = Some(CUnseal(cd, cs, ct))
+function clause decode (0b010010 @ 0b00111 @ cd : regno @ cb : regno @ 0b00000 @ 0b000000) = Some(CJALR(cd, cb, true)) /* CJALR */
+function clause decode (0b010010 @ 0b01000 @ 0b00000    @ cb : regno @ 0b00000 @ 0b000000) = Some(CJALR(0b00000, cb, false)) /* CJR */
+
+
+/* 
 New encodings as per CHERI ISA Appendix B.2.  
 
 NB: Must be careful about order of matching because unused register
 fields are re-used as additional function codes.
-*)
-
-(* One arg *)
-function clause decode (0b010010 : 0b00000 : (regno) rd :    0b00001 :    0b11111 : 0b111111) = Some(CGetCause(rd))
-function clause decode (0b010010 : 0b00000 : (regno) rs :    0b00010 :    0b11111 : 0b111111) = Some(CSetCause(rs))
-function clause decode (0b010010 : 0b00000 : (regno) cd :    0b00000 :    0b11111 : 0b111111) = Some(CGetPCC(cd))
-function clause decode (0b010010 : 0b00000 : (regno) cb :    0b00011 :    0b11111 : 0b111111) = Some(CJALR(0b00000, cb, false)) (* CJR *)
-
-(* Two arg *)
-function clause decode (0b010010 : 0b00000 : (regno) cs : (regno) rt :    0b01000 : 0b111111) = Some(CCheckPerm(cs, rt))
-function clause decode (0b010010 : 0b00000 : (regno) cs : (regno) cb :    0b01001 : 0b111111) = Some(CCheckType(cs, cb))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb :    0b01011 : 0b111111) = Some(CClearTag(cd, cb))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs :    0b01010 : 0b111111) = Some(CMOVX(cd, cs, 0b00000, false)) (* CMOVE *)
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb :    0b01100 : 0b111111) = Some(CJALR(cd, cb, true)) (* CJALR *)
-
-(* Capability Inspection *)
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb :    0b00000 : 0b111111) = Some(CGetPerm(rd, cb))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb :    0b00001 : 0b111111) = Some(CGetType(rd, cb))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb :    0b00010 : 0b111111) = Some(CGetBase(rd, cb))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb :    0b00011 : 0b111111) = Some(CGetLen(rd, cb))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb :    0b00100 : 0b111111) = Some(CGetTag(rd, cb))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb :    0b00101 : 0b111111) = Some(CGetSealed(rd, cb))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb :    0b00110 : 0b111111) = Some(CGetOffset(rd, cb))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) rs :    0b00111 : 0b111111) = Some(CGetPCCSetOffset(cd, rs))
-
-(* Three operand *)
-
-(* Capability Modification *)
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b001011) = Some(CSeal(cd, cs, ct))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b001100) = Some(CUnseal(cd, cs, ct))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001101) = Some(CAndPerm(cd, cs, rt))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001111) = Some(CSetOffset(cd, cs, rt))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001000) = Some(CSetBounds(cd, cs, rt))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001001) = Some(CSetBoundsExact(cd, cs, rt))
-
-
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b010001) = Some(CIncOffset(cd, cb, rt))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) ct : 0b011101) = Some(CBuildCap(cd, cb, ct))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) ct : 0b011110) = Some(CCopyType(cd, cb, ct))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b011111) = Some(CCSeal(cd, cs, ct))
-
-(* Pointer Arithmetic *)
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b010010) = Some(CToPtr(rd, cb, ct))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rs : 0b010011) = Some(CFromPtr(cd, cb, rs))
-function clause decode (0b010010 : 0b00000 : (regno) rt : (regno) cb : (regno) cs : 0b001010) = Some(CSub(rt, cb, cs))
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rs : 0b011011) = Some(CMOVX(cd, cs, rs, false)) (* CMOVZ *)
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rs : 0b011100) = Some(CMOVX(cd, cs, rs, true))  (* CMOVN *)
-
-(* Pointer Comparison *)
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010100) = Some(CPtrCmp(rd, cb, cs, CEQ))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010101) = Some(CPtrCmp(rd, cb, cs, CNE))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010110) = Some(CPtrCmp(rd, cb, cs, CLT))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010111) = Some(CPtrCmp(rd, cb, cs, CLE))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b011000) = Some(CPtrCmp(rd, cb, cs, CLTU))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b011001) = Some(CPtrCmp(rd, cb, cs, CLEU))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b011010) = Some(CPtrCmp(rd, cb, cs, CEXEQ))
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b100001) = Some(CPtrCmp(rd, cb, cs, CNEXEQ))
-
-function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b100000) = Some(CTestSubset(rd, cb, ct))
-
-function clause decode (0b010010 : 0b01001 : (regno) cd : (bit[16]) imm) = Some(CBX(cd, imm, true))  (* CBTU *)
-function clause decode (0b010010 : 0b01010 : (regno) cd : (bit[16]) imm) = Some(CBX(cd, imm, false)) (* CBTS *)
-function clause decode (0b010010 : 0b10001 : (regno) cd : (bit[16]) imm) = Some(CBZ(cd, imm, false)) (* CBEZ *)
-function clause decode (0b010010 : 0b10010 : (regno) cd : (bit[16]) imm) = Some(CBZ(cd, imm, true))  (* CBNZ *)
-
-function clause decode (0b010010 : 0b00101 :    0b00000 :    0b00000 : 0b11111111111) = Some(CReturn)
-function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb, selector))
-
-function clause decode (0b010010 : 0b01111 : 0b00000 : (bit[16]) imm) = Some(ClearRegs(GPLo, imm))
-function clause decode (0b010010 : 0b01111 : 0b00001 : (bit[16]) imm) = Some(ClearRegs(GPHi, imm))
-function clause decode (0b010010 : 0b01111 : 0b00010 : (bit[16]) imm) = Some(ClearRegs(CLo,  imm))
-function clause decode (0b010010 : 0b01111 : 0b00011 : (bit[16]) imm) = Some(ClearRegs(CHi,  imm))
-
-function clause decode (0b010010 : 0b10011 : (regno) cd : (regno) cb : (bit[11]) imm) = Some(CIncOffsetImmediate(cd, cb, imm))
-function clause decode (0b010010 : 0b10100 : (regno) cd : (regno) cb : (bit[11]) imm) = Some(CSetBoundsImmediate(cd, cb, imm))
-
-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 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 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 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 decode (0b010010 : 0b00100 : (regno) rt : 0x0006) = Some(C2Dump(rt))
-
-(* 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
+*/
+
+/* One arg */
+function clause decode (0b010010 @ 0b00000 @ rd : regno @    0b00001 @    0b11111 @ 0b111111) = Some(CGetCause(rd))
+function clause decode (0b010010 @ 0b00000 @ rs : regno @    0b00010 @    0b11111 @ 0b111111) = Some(CSetCause(rs))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @    0b00000 @    0b11111 @ 0b111111) = Some(CGetPCC(cd))
+function clause decode (0b010010 @ 0b00000 @ cb : regno @    0b00011 @    0b11111 @ 0b111111) = Some(CJALR(0b00000, cb, false)) /* CJR */
+
+/* Two arg */
+function clause decode (0b010010 @ 0b00000 @ cs : regno @ rt : regno @    0b01000 @ 0b111111) = Some(CCheckPerm(cs, rt))
+function clause decode (0b010010 @ 0b00000 @ cs : regno @ cb : regno @    0b01001 @ 0b111111) = Some(CCheckType(cs, cb))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @    0b01011 @ 0b111111) = Some(CClearTag(cd, cb))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @    0b01010 @ 0b111111) = Some(CMOVX(cd, cs, 0b00000, false)) /* CMOVE */
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @    0b01100 @ 0b111111) = Some(CJALR(cd, cb, true)) /* CJALR */
+
+/* Capability Inspection */
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @    0b00000 @ 0b111111) = Some(CGetPerm(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @    0b00001 @ 0b111111) = Some(CGetType(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @    0b00010 @ 0b111111) = Some(CGetBase(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @    0b00011 @ 0b111111) = Some(CGetLen(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @    0b00100 @ 0b111111) = Some(CGetTag(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @    0b00101 @ 0b111111) = Some(CGetSealed(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @    0b00110 @ 0b111111) = Some(CGetOffset(rd, cb))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ rs : regno @    0b00111 @ 0b111111) = Some(CGetPCCSetOffset(cd, rs))
+
+/* Three operand */
+
+/* Capability Modification */
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ ct : regno @ 0b001011) = Some(CSeal(cd, cs, ct))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ ct : regno @ 0b001100) = Some(CUnseal(cd, cs, ct))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rt : regno @ 0b001101) = Some(CAndPerm(cd, cs, rt))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rt : regno @ 0b001111) = Some(CSetOffset(cd, cs, rt))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rt : regno @ 0b001000) = Some(CSetBounds(cd, cs, rt))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rt : regno @ 0b001001) = Some(CSetBoundsExact(cd, cs, rt))
+
+
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @ rt : regno @ 0b010001) = Some(CIncOffset(cd, cb, rt))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @ ct : regno @ 0b011101) = Some(CBuildCap(cd, cb, ct))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @ ct : regno @ 0b011110) = Some(CCopyType(cd, cb, ct))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ ct : regno @ 0b011111) = Some(CCSeal(cd, cs, ct))
+
+/* Pointer Arithmetic */
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ ct : regno @ 0b010010) = Some(CToPtr(rd, cb, ct))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @ rs : regno @ 0b010011) = Some(CFromPtr(cd, cb, rs))
+function clause decode (0b010010 @ 0b00000 @ rt : regno @ cb : regno @ cs : regno @ 0b001010) = Some(CSub(rt, cb, cs))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rs : regno @ 0b011011) = Some(CMOVX(cd, cs, rs, false)) /* CMOVZ */
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rs : regno @ 0b011100) = Some(CMOVX(cd, cs, rs, true))  /* CMOVN */
+
+/* Pointer Comparison */
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b010100) = Some(CPtrCmp(rd, cb, cs, CEQ))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b010101) = Some(CPtrCmp(rd, cb, cs, CNE))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b010110) = Some(CPtrCmp(rd, cb, cs, CLT))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b010111) = Some(CPtrCmp(rd, cb, cs, CLE))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b011000) = Some(CPtrCmp(rd, cb, cs, CLTU))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b011001) = Some(CPtrCmp(rd, cb, cs, CLEU))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b011010) = Some(CPtrCmp(rd, cb, cs, CEXEQ))
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b100001) = Some(CPtrCmp(rd, cb, cs, CNEXEQ))
+
+function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ ct : regno @ 0b100000) = Some(CTestSubset(rd, cb, ct))
+
+function clause decode (0b010010 @ 0b01001 @ cd : regno @ imm : bits(16)) = Some(CBX(cd, imm, true))  /* CBTU */
+function clause decode (0b010010 @ 0b01010 @ cd : regno @ imm : bits(16)) = Some(CBX(cd, imm, false)) /* CBTS */
+function clause decode (0b010010 @ 0b10001 @ cd : regno @ imm : bits(16)) = Some(CBZ(cd, imm, false)) /* CBEZ */
+function clause decode (0b010010 @ 0b10010 @ cd : regno @ imm : bits(16)) = Some(CBZ(cd, imm, true))  /* CBNZ */
+
+function clause decode (0b010010 @ 0b00101 @    0b00000 @    0b00000 @ 0b11111111111) = Some(CReturn)
+function clause decode (0b010010 @ 0b00101 @ cs : regno @ cb : regno @ selector : bits(11)) = Some(CCall(cs, cb, selector))
+
+function clause decode (0b010010 @ 0b01111 @ 0b00000 @ imm : bits(16)) = Some(ClearRegs(GPLo, imm))
+function clause decode (0b010010 @ 0b01111 @ 0b00001 @ imm : bits(16)) = Some(ClearRegs(GPHi, imm))
+function clause decode (0b010010 @ 0b01111 @ 0b00010 @ imm : bits(16)) = Some(ClearRegs(CLo,  imm))
+function clause decode (0b010010 @ 0b01111 @ 0b00011 @ imm : bits(16)) = Some(ClearRegs(CHi,  imm))
+
+function clause decode (0b010010 @ 0b10011 @ cd : regno @ cb : regno @ imm : bits(11)) = Some(CIncOffsetImmediate(cd, cb, imm))
+function clause decode (0b010010 @ 0b10100 @ cd : regno @ cb : regno @ imm : bits(11)) = Some(CSetBoundsImmediate(cd, cb, imm))
+
+function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b00) = Some(CLoad(rd, cb, rt, offset, false, B, false)) /* CLBU */
+function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b1 @ 0b00) = Some(CLoad(rd, cb, rt, offset, true,  B, false)) /* CLB */
+function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b01) = Some(CLoad(rd, cb, rt, offset, false, H, false)) /* CLHU */
+function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b1 @ 0b01) = Some(CLoad(rd, cb, rt, offset, true,  H, false)) /* CLH */
+function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b10) = Some(CLoad(rd, cb, rt, offset, false, W, false)) /* CLWU */
+function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b1 @ 0b10) = Some(CLoad(rd, cb, rt, offset, true,  W, false)) /* CLW */
+function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b11) = Some(CLoad(rd, cb, rt, offset, false, D, false)) /* CLD */
+
+function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b0 @ 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, B, true)) /* CLLBU */
+function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b1 @ 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true,  B, true)) /* CLLB  */
+function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b0 @ 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, H, true)) /* CLLHU */
+function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b1 @ 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true,  H, true)) /* CLLH  */
+function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b0 @ 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, W, true)) /* CLLWU */
+function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b1 @ 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true,  W, true)) /* CLLW  */
+function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b0 @ 0b11) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, D, true)) /* CLLD  */
+
+function clause decode (0b111010 @ rs : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b00) = Some(CStore(rs, cb, rt, 0b00000, offset, B, false)) /* CSB */
+function clause decode (0b111010 @ rs : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b01) = Some(CStore(rs, cb, rt, 0b00000, offset, H, false)) /* CSH */
+function clause decode (0b111010 @ rs : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b10) = Some(CStore(rs, cb, rt, 0b00000, offset, W, false)) /* CSW */
+function clause decode (0b111010 @ rs : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b11) = Some(CStore(rs, cb, rt, 0b00000, offset, D, false)) /* CSD */
+
+function clause decode (0b010010 @ 0b10000 @ rs : regno @ cb : regno @ rd : regno @ 0b0000 @ 0b00) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, B, true)) /* CSCB */
+function clause decode (0b010010 @ 0b10000 @ rs : regno @ cb : regno @ rd : regno @ 0b0000 @ 0b01) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, H, true)) /* CSCH */
+function clause decode (0b010010 @ 0b10000 @ rs : regno @ cb : regno @ rd : regno @ 0b0000 @ 0b10) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, W, true)) /* CSCW */
+function clause decode (0b010010 @ 0b10000 @ rs : regno @ cb : regno @ rd : regno @ 0b0000 @ 0b11) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, D, true)) /* CSCD */
+
+function clause decode (0b111110 @ cs : regno @ cb : regno@ rt : regno @ offset : bits(11)) = Some(CSC(cs, cb, rt, 0b00000, offset, false))
+function clause decode (0b010010 @ 0b10000 @ cs : regno @ cb : regno@ rd : regno @ 0b00 @ 0b0111) = Some(CSC(cs, cb, 0b00000, rd, 0b00000000000, true))
+
+function clause decode (0b110110 @ cd : regno @ cb : regno@ rt : regno @ offset : bits(11)) = Some(CLC(cd, cb, rt, offset, false))
+function clause decode (0b010010 @ 0b10000 @ cd : regno @ cb : regno@ 0b0000000 @ 0b1111) = Some(CLC(cd, cb, 0b00000, 0b00000000000, true))
+
+function clause decode (0b010010 @ 0b00100 @ rt : regno @ 0x0006) = Some(C2Dump(rt))
+
+/* Operations that extract parts of a capability into GPR */
+
+union clause ast = CGetPerm   : (regno, regno)
+union clause ast = CGetType   : (regno, regno)
+union clause ast = CGetBase   : (regno, regno)
+union clause ast = CGetLen    : (regno, regno)
+union clause ast = CGetTag    : (regno, regno)
+union clause ast = CGetSealed : (regno, regno)
+union clause ast = CGetOffset : (regno, regno)
 
 function clause execute (CGetPerm(rd, cb)) =
 {
-  (* START_CGetPerms *)
+  /* 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 *)
+    wGPR(rd) = EXTZ(getCapPerms(capVal));
+  /* END_CGetPerms */
 }
 
 function clause execute (CGetType(rd, cb)) =
 {
-  (* START_CGetType *)
+  /* START_CGetType */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) := if (capVal.sealed)
+    wGPR(rd) = if (capVal.sealed)
       then EXTZ(capVal.otype)
       else (bitone ^^ 64)
-  (* END_CGetType *)
+  /* END_CGetType */
 }
 
 function clause execute (CGetBase(rd, cb)) =
 {
-  (* START_CGetBase *)
+  /* START_CGetBase */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) := (bit[64]) (getCapBase(capVal));
-  (* END_CGetBase *)
+    wGPR(rd) = to_bits(64, getCapBase(capVal));
+  /* END_CGetBase */
 }
 
 function clause execute (CGetOffset(rd, cb)) =
 {
-  (* START_CGetOffset *)
+  /* START_CGetOffset */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) := (bit[64]) (getCapOffset(capVal));
-  (* END_CGetOffset *)
+    wGPR(rd) = to_bits(64, getCapOffset(capVal));
+  /* END_CGetOffset */
 }
 
 function clause execute (CGetLen(rd, cb)) =
 {
-  (* START_CGetLen *)
+  /* 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
-    wGPR(rd) := (if len65 > MAX_U64 then MAX_U64 else len65);
-    (*let (uint64) len64 = (if len65 > MAX_U64 then MAX_U64 else len65) in
-    wGPR(rd) := (bit[64]) len64;*)
-  (* END_CGetLen *)
+    wGPR(rd) = to_bits(64, if len65 > MAX_U64 then MAX_U64 else len65);
+  /* END_CGetLen */
 }
 
 function clause execute (CGetTag(rd, cb)) =
 {
-  (* START_CGetTag *)
+  /* 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 *)
+    wGPR(rd) = EXTZ(capVal.tag);
+  /* END_CGetTag */
 }
 
 function clause execute (CGetSealed(rd, cb)) =
 {
-  (* START_CGetSealed *)
+  /* 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 *)
+    wGPR(rd) = EXTZ(capVal.sealed);
+  /* END_CGetSealed */
 }
 
-union ast member regno CGetPCC
+union clause ast = CGetPCC : regno
 function clause execute (CGetPCC(cd)) =
 {
-  (* START_CGetPCC *)
+  /* 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, ""); (* guaranteed to be in-bounds *)
+    {assert (success, ""); /* guaranteed to be in-bounds */
     writeCapReg(cd, pcc2)};
-  (* END_CGetPCC *)
+  /* END_CGetPCC */
 }
 
 
-union ast member (regno, regno) CGetPCCSetOffset
+union clause ast = CGetPCCSetOffset : (regno, regno)
 function clause execute (CGetPCCSetOffset(cd, rs)) =
 {
-  (* START_CGetPCCSetOffset *)
+  /* START_CGetPCCSetOffset */
   checkCP2usable();
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
@@ -315,45 +313,45 @@ function clause execute (CGetPCCSetOffset(cd, rs)) =
         writeCapReg(cd, newPCC)
     else
         writeCapReg(cd, int_to_cap(rs_val));
-  (* END_CGetPCCSetOffset *)
+  /* END_CGetPCCSetOffset */
 }
-(* Get and Set CP2 cause register *)
+/* Get and Set CP2 cause register */
 
-union ast member regno CGetCause
+union clause ast = CGetCause : regno
 function clause execute (CGetCause(rd)) = 
 {
-  (* START_CGetCause *)
+  /* START_CGetCause */
   checkCP2usable();
   if not (pcc_access_system_regs ()) then
     raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation)
   else
-    wGPR(rd) := EXTZ(CapCause)
-  (* END_CGetCause *)
+    wGPR(rd) = EXTZ(CapCause.bits())
+  /* END_CGetCause */
 }
 
-union ast member (regno) CSetCause
-function clause execute (CSetCause((regno) rt)) = 
+union clause ast = CSetCause : regno
+function clause execute (CSetCause(rt)) = 
 {
-  (* START_CSetCause *)
+  /* 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];
+      let rt_val = rGPR(rt);
+      CapCause->ExcCode() = rt_val[15..8];
+      CapCause->RegNum()  = rt_val[7..0];
     }
-  (* END_CSetCause *)
+  /* END_CSetCause */
 }
 
-union ast member regregreg CAndPerm
+union clause ast = CAndPerm : (regno, regno, regno)
 function clause execute(CAndPerm(cd, cb, rt)) = 
 {
-  (* START_CAndPerm *)
+  /* START_CAndPerm */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  rt_val := rGPR(rt);
+  let cb_val = readCapReg(cb);
+  let rt_val = rGPR(rt);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -366,18 +364,18 @@ 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 *)
+  /* END_CAndPerm */
 }
 
 
 
-union ast member regregreg CToPtr
+union clause ast = CToPtr : (regno, regno, regno)
 function clause execute(CToPtr(rd, cb, ct)) = 
 {
-  (* START_CToPtr *)
+  /* START_CToPtr */
   checkCP2usable();
-  ct_val := readCapReg(ct);
-  cb_val := readCapReg(cb);
+  let ct_val = readCapReg(ct);
+  let cb_val = readCapReg(cb);
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else if (register_inaccessible(ct)) then
@@ -392,40 +390,40 @@ function clause execute(CToPtr(rd, cb, ct)) =
       let cbTop = getCapTop(cb_val) in
       let ctBase = getCapBase(ct_val) in
       let ctTop = getCapTop(ct_val) in
-      wGPR(rd) := if (not (cb_val.tag)) |
+      wGPR(rd) = if (not (cb_val.tag)) |
                      (cbBase < ctBase) |
                      (cbTop > ctTop) then
-          ((bit[64]) 0)
+          zeros()
         else
-          (bit[64])(getCapCursor(cb_val) - ctBase)
+          to_bits(64, getCapCursor(cb_val) - ctBase)
     }
-  (* END_CToPtr *)
+  /* END_CToPtr */
 }
 
 
 
-union ast member regregreg CSub
+union clause ast = CSub : (regno, regno, regno)
 function clause execute(CSub(rd, cb, ct)) = 
 {
-  (* START_CSub *)
+  /* START_CSub */
   checkCP2usable();
-  ct_val := readCapReg(ct);
-  cb_val := readCapReg(cb);
+  let ct_val = readCapReg(ct);
+  let 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])(to_svec(getCapCursor(cb_val) - getCapCursor(ct_val)))
+      wGPR(rd) = to_bits(64, getCapCursor(cb_val) - getCapCursor(ct_val))
     }
-  (* END_CSub *)
+  /* END_CSub */
 }
 
-union ast member (regno, regno, regno, CPtrCmpOp) CPtrCmp
+union clause ast = CPtrCmp : (regno, regno, regno, CPtrCmpOp)
 function clause execute(CPtrCmp(rd, cb, ct, op)) = 
 {
-  (* START_CPtrCmp *)
+  /* START_CPtrCmp */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
@@ -433,48 +431,49 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
   else 
     {
-      cb_val := readCapReg(cb);
-      ct_val := readCapReg(ct);
-      equal  := false;
-      ltu    := false;
-      lts    := false;
+      let cb_val = readCapReg(cb);
+      let 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;
+              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));
+          cursor1 = getCapCursor(cb_val);
+          cursor2 = getCapCursor(ct_val);
+          equal   = (cursor1 == cursor2);
+          ltu     = (cursor1 < cursor2);
+          lts     = to_bits(64, cursor1) <_s to_bits(64, cursor2);
         };
-      wGPR(rd) := EXTZ ((bool[1]) (switch (op) {
-        case CEQ   -> [equal]
-        case CNE   -> [not (equal)]
-        case CLT   -> [lts]
-        case CLE   -> [lts | equal]
-        case CLTU  -> [ltu]
-        case CLEU  -> [ltu | equal]
-        case CEXEQ -> [cb_val == ct_val]
-        case CNEXEQ -> [cb_val != ct_val]
-      }))
+      let cmp : bool = match op {
+        CEQ    => equal,
+        CNE    => not (equal),
+        CLT    => lts,
+        CLE    => lts | equal,
+        CLTU   => ltu,
+        CLEU   => ltu | equal,
+        CEXEQ  => cb_val == ct_val,
+        CNEXEQ => cb_val != ct_val
+      };
+      wGPR(rd) = EXTZ (cmp)
     }
-  (* END_CPtrCmp *)
+  /* END_CPtrCmp */
 }
 
-union ast member regregreg CIncOffset
+union clause ast = CIncOffset : (regno, regno, regno)
 function clause execute (CIncOffset(cd, cb, rt)) =
 {
-  (* START_CIncOffset *)
+  /* START_CIncOffset */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  rt_val := rGPR(rt);
+  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
@@ -486,17 +485,17 @@ function clause execute (CIncOffset(cd, cb, rt)) =
     if (success) then
         writeCapReg(cd, newCap)
     else
-        writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val))
-  (* END_CIncOffset *)
+        writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + rt_val))
+  /* END_CIncOffset */
 }
 
-union ast member (regno, regno, bit[11]) CIncOffsetImmediate
+union clause ast = CIncOffsetImmediate : (regno, regno, bits(11))
 function clause execute (CIncOffsetImmediate(cd, cb, imm)) =
 {
-  (* START_CIncOffsetImmediate *)
+  /* START_CIncOffsetImmediate */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  let (bit[64]) imm64 = EXTS(imm) in
+  let cb_val = readCapReg(cb);
+  let imm64 : bits(64) = EXTS(imm) in
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -508,17 +507,17 @@ function clause execute (CIncOffsetImmediate(cd, cb, imm)) =
     if (success) then
         writeCapReg(cd, newCap)
     else
-        writeCapReg(cd, int_to_cap(getCapBase(cb_val) + imm64))
-  (* END_CIncOffsetImmediate *)
+        writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + imm64))
+  /* END_CIncOffsetImmediate */
 }
 
-union ast member regregreg CSetOffset
+union clause ast = CSetOffset : (regno, regno, regno)
 function clause execute (CSetOffset(cd, cb, rt)) =
 {
-  (* START_CSetOffset *)
+  /* START_CSetOffset */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  rt_val := rGPR(rt);
+  let cb_val = readCapReg(cb);
+  let rt_val = rGPR(rt);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -530,21 +529,21 @@ function clause execute (CSetOffset(cd, cb, rt)) =
     if (success) then
         writeCapReg(cd, newCap)
     else
-        writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val))
-  (* END_CSetOffset *)
+        writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + rt_val))
+  /* END_CSetOffset */
 }
 
-union ast member regregreg CSetBounds
+union clause ast = CSetBounds : (regno, regno, regno)
 function clause execute (CSetBounds(cd, cb, rt)) =
 {
-  (* START_CSetBounds *)
+  /* START_CSetBounds */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  rt_val := unsigned(rGPR(rt));
-  cursor := getCapCursor(cb_val);
-  base   := getCapBase(cb_val);
-  top    := getCapTop(cb_val);
-  newTop := cursor + rt_val;
+  let cb_val = readCapReg(cb);
+  let rt_val = unsigned(rGPR(rt));
+  cursor = getCapCursor(cb_val);
+  base   = getCapBase(cb_val);
+  top    = getCapTop(cb_val);
+  newTop = cursor + rt_val;
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -558,22 +557,22 @@ function clause execute (CSetBounds(cd, cb, rt)) =
   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 *)
+    let (_, newCap) = setCapBounds(cb_val, to_bits(64, cursor), to_bits(65, newTop)) in
+    writeCapReg(cd, newCap) /* ignore exact */
+  /* END_CSetBounds */
 }
 
-union ast member (regno, regno, bit[11]) CSetBoundsImmediate
+union clause ast = CSetBoundsImmediate : (regno, regno, bits(11))
 function clause execute (CSetBoundsImmediate(cd, cb, imm)) =
 {
-  (* START_CSetBoundsImmedate *)
+  /* START_CSetBoundsImmedate */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  immU   := unsigned(imm);
-  cursor := getCapCursor(cb_val);
-  base   := getCapBase(cb_val);
-  top    := getCapTop(cb_val);
-  newTop := cursor + immU;
+  cb_val = readCapReg(cb);
+  immU   = unsigned(imm);
+  cursor = getCapCursor(cb_val);
+  base   = getCapBase(cb_val);
+  top    = getCapTop(cb_val);
+  newTop = cursor + immU;
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -587,22 +586,22 @@ function clause execute (CSetBoundsImmediate(cd, cb, imm)) =
   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_CSetBoundsImmediate *)
+    let (_, newCap) = setCapBounds(cb_val, to_bits(64, cursor), to_bits(65, newTop)) in
+    writeCapReg(cd, newCap) /* ignore exact */
+  /* END_CSetBoundsImmediate */
 }
 
-union ast member regregreg CSetBoundsExact
+union clause ast = CSetBoundsExact : (regno, regno, regno)
 function clause execute (CSetBoundsExact(cd, cb, rt)) =
 {
-  (* START_CSetBoundsExact *)
+  /* START_CSetBoundsExact */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  rt_val := unsigned(rGPR(rt));
-  cursor := getCapCursor(cb_val);
-  base   := getCapBase(cb_val);
-  top    := getCapTop(cb_val);
-  newTop := cursor + rt_val;
+  cb_val = readCapReg(cb);
+  rt_val = unsigned(rGPR(rt));
+  cursor = getCapCursor(cb_val);
+  base   = getCapBase(cb_val);
+  top    = getCapTop(cb_val);
+  newTop = cursor + rt_val;
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -616,18 +615,18 @@ function clause execute (CSetBoundsExact(cd, cb, rt)) =
   else if (newTop > top) then
     raise_c2_exception(CapEx_LengthViolation, cb)
   else
-    let (exact, newCap) = setCapBounds(cb_val, (bit[64]) cursor, (bit[65]) newTop) in
+    let (exact, newCap) = setCapBounds(cb_val, to_bits(64, cursor), to_bits(65, newTop)) in
     if not (exact) then
         raise_c2_exception(CapEx_InexactBounds, cb)
     else
         writeCapReg(cd, newCap)
-  (* END_CSetBoundsExact *)
+  /* END_CSetBoundsExact */
 }
 
-union ast member (regno, regno) CClearTag
+union clause ast = CClearTag : (regno, regno)
 function clause execute (CClearTag(cd, cb)) =
 {
-  (* START_CClearTag *)
+  /* START_CClearTag */
   checkCP2usable();
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
@@ -635,60 +634,60 @@ function clause execute (CClearTag(cd, cb)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     {
-      cb_val := readCapReg(cb);
-      writeCapReg(cd, {cb_val with tag = false});
+      cb_val = readCapReg(cb);
+      writeCapReg(cd, {cb_val with tag=false});
     }
-  (* END_CClearTag *)
+  /* END_CClearTag */
 }
 
-union ast member (regno,regno,regno,bool) CMOVX
+union clause ast = CMOVX : (regno,regno,regno,bool)
 function clause execute (CMOVX(cd, cb, rt, ismovn)) =
 {
-  (* START_CMOVX *)
+  /* START_CMOVX */
   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 if ((rGPR(rt) == 0) ^ ismovn) then
-    writeCapReg(cd) := readCapReg(cb);
-  (* END_CMOVX *)
+  else if ((rGPR(rt) == zeros()) ^ ismovn) then
+    writeCapReg(cd) = readCapReg(cb);
+  /* END_CMOVX */
 }
 
-union ast member (ClearRegSet, bit[16]) ClearRegs
-function clause execute (ClearRegs(regset, mask)) =
+union clause ast = ClearRegs : (ClearRegSet, bits(16))
+function clause execute (ClearRegs(regset, m)) =
 {
-  (* START_ClearRegs *)
+  /* 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
+        let r = to_bits(5, i+16) in
+        if (m[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
+    if (m[i]) then
+      match regset {
+        GPLo  => wGPR(to_bits(5, i)) = zeros(),
+        GPHi  => wGPR(to_bits(5, i+16)) = zeros(),
+        CLo   => writeCapReg(to_bits(5, i)) = null_cap,
+        CHi   => writeCapReg(to_bits(5, i+16)) = null_cap
       }
-  (* END_ClearRegs *)
+  /* END_ClearRegs */
 }
 
-union ast member regregreg CFromPtr
+union clause ast = CFromPtr : (regno, regno, regno)
 function clause execute (CFromPtr(cd, cb, rt)) =
 {
-  (* START_CFromPtr *)
+  /* START_CFromPtr */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  rt_val := rGPR(rt);
+  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
+  else if (rt == 0b00000) then
     writeCapReg(cd, null_cap)
   else if not (cb_val.tag) then
     raise_c2_exception(CapEx_TagViolation, cb)
@@ -699,24 +698,24 @@ function clause execute (CFromPtr(cd, cb, rt)) =
     if (success) then
         writeCapReg(cd, newCap)
     else
-        writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val))
-  (* END_CFromPtr *)
+        writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + rt_val))
+  /* END_CFromPtr */
 }
 
-union ast member regregreg CBuildCap
+union clause ast = CBuildCap : (regno, regno, regno)
 function clause execute (CBuildCap(cd, cb, ct)) =
 {
-  (* START_CBuildCap *)
+  /* START_CBuildCap */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  ct_val := readCapReg(ct);
-  cb_base := getCapBase(cb_val);
-  ct_base := getCapBase(ct_val);
-  cb_top := getCapTop(cb_val);
-  ct_top := getCapTop(ct_val);
-  cb_perms := getCapPerms(cb_val);
-  ct_perms := getCapPerms(ct_val);
-  ct_offset := getCapOffset(ct_val);
+  cb_val = readCapReg(cb);
+  ct_val = readCapReg(ct);
+  cb_base = getCapBase(cb_val);
+  ct_base = getCapBase(ct_val);
+  cb_top = getCapTop(cb_val);
+  ct_top = getCapTop(ct_val);
+  cb_perms = getCapPerms(cb_val);
+  ct_perms = getCapPerms(ct_val);
+  ct_offset = getCapOffset(ct_val);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -731,32 +730,32 @@ function clause execute (CBuildCap(cd, cb, ct)) =
     raise_c2_exception(CapEx_LengthViolation, cb)
   else if ct_top > cb_top then
     raise_c2_exception(CapEx_LengthViolation, cb)
-   else if ct_base > ct_top then (* check for length < 0 - possible because ct might be untagged *)
+   else if ct_base > ct_top then /* check for length < 0 - possible because ct might be untagged */
     raise_c2_exception(CapEx_LengthViolation, ct)
    else if (ct_perms & cb_perms) != ct_perms then
     raise_c2_exception(CapEx_UserDefViolation, ct)
   else
-    let (exact, cd1) = setCapBounds(cb_val, (bit[64]) ct_base, (bit[65]) ct_top) in 
-    let (representable, cd2) = setCapOffset(cd1, (bit[64]) ct_offset) in
+    let (exact, cd1) = setCapBounds(cb_val, to_bits(64, ct_base), to_bits(65, ct_top)) in 
+    let (representable, cd2) = setCapOffset(cd1, to_bits(64, ct_offset)) in
     let cd3 = setCapPerms(cd2, ct_perms) in
     {
-      assert(exact, "");         (* base and top came from ct originally so will be exact *)
-      assert(representable, ""); (* similarly offset should be representable XXX except for fastRepCheck *)
+      assert(exact, "");         /* base and top came from ct originally so will be exact */
+      assert(representable, ""); /* similarly offset should be representable XXX except for fastRepCheck */
       writeCapReg(cd, cd3);
     }
-  (* END_CBuildCap *)
+  /* END_CBuildCap */
 }
 
-union ast member regregreg CCopyType
+union clause ast = CCopyType : (regno, regno, regno)
 function clause execute (CCopyType(cd, cb, ct)) =
 {
-  (* START_CCopyType *)
+  /* START_CCopyType */
     checkCP2usable();
-  cb_val := readCapReg(cb);
-  ct_val := readCapReg(ct);
-  cb_base := getCapBase(cb_val);
-  cb_top  := getCapTop(cb_val);
-  ct_otype := unsigned(ct_val.otype);
+  cb_val = readCapReg(cb);
+  ct_val = readCapReg(ct);
+  cb_base = getCapBase(cb_val);
+  cb_top  = getCapTop(cb_val);
+  ct_otype = unsigned(ct_val.otype);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -773,23 +772,23 @@ function clause execute (CCopyType(cd, cb, ct)) =
     else if ct_otype >= cb_top then
       raise_c2_exception(CapEx_LengthViolation, cb)
     else
-      let (success, cap) = setCapOffset(cb_val, (bit[64]) (ct_otype - cb_base)) in {
-        assert(success, ""); (* offset is in bounds so must succeed *)
+      let (success, cap) = setCapOffset(cb_val, to_bits(64, ct_otype - cb_base)) in {
+        assert(success, ""); /* offset is in bounds so must succeed */
         writeCapReg(cd, cap);
       }
   } else
     writeCapReg(cd, int_to_cap(bitone ^^ 64))
-  (* END_CCopyType *)
+  /* END_CCopyType */
 }
 
-union ast member (regno, regno) CCheckPerm
+union clause ast = CCheckPerm : (regno, regno)
 function clause execute (CCheckPerm(cs, rt)) =
 {
-  (* START_CCheckPerm *)
+  /* START_CCheckPerm */
   checkCP2usable();
-  cs_val := readCapReg(cs);
-  cs_perms := (bit[64]) (EXTZ(getCapPerms(cs_val)));
-  rt_perms := rGPR(rt);
+  cs_val = readCapReg(cs);
+  cs_perms : bits(64) = 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
@@ -798,16 +797,16 @@ function clause execute (CCheckPerm(cs, rt)) =
     raise_c2_exception(CapEx_UserDefViolation, cs)
   else
     ()
-  (* END_CCheckPerm *)
+  /* END_CCheckPerm */
 }
 
-union ast member (regno, regno) CCheckType
+union clause ast = CCheckType : (regno, regno)
 function clause execute (CCheckType(cs, cb)) =
 {
-  (* START_CCheckType *)
+  /* START_CCheckType */
   checkCP2usable();
-  cs_val := readCapReg(cs);
-  cb_val := readCapReg(cb);
+  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
@@ -824,54 +823,54 @@ function clause execute (CCheckType(cs, cb)) =
     raise_c2_exception(CapEx_TypeViolation, cs)
   else
     ()
-  (* END_CCheckType *)
+  /* END_CCheckType */
 }
 
-union ast member regregreg CTestSubset
+union clause ast = CTestSubset : (regno, regno, regno)
 function clause execute (CTestSubset(rd, cb, ct)) =
 {
-  (* START_CTestSubset *)
+  /* START_CTestSubset */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  ct_val := readCapReg(ct);
-  ct_top    := getCapTop(ct_val);
-  ct_base   := getCapBase(ct_val);
-  ct_perms  := getCapPerms(ct_val);
-  cb_top    := getCapTop(cb_val);
-  cb_base   := getCapBase(cb_val);
-  cb_perms  := getCapPerms(cb_val);
+  cb_val = readCapReg(cb);
+  ct_val = readCapReg(ct);
+  ct_top    = getCapTop(ct_val);
+  ct_base   = getCapBase(ct_val);
+  ct_perms  = getCapPerms(ct_val);
+  cb_top    = getCapTop(cb_val);
+  cb_base   = getCapBase(cb_val);
+  cb_perms  = getCapPerms(cb_val);
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else if (register_inaccessible(ct)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
   else {
-     (bit[64]) result := EXTZ(if (cb_val.tag != ct_val.tag) then
-             0x0
+     result : bits(1) = if (cb_val.tag != ct_val.tag) then
+             0b0
         else if (cb_val.sealed != ct_val.sealed) then
-             0x0
+             0b0
         else if (ct_base < cb_base) then
-             0x0
+             0b0
         else if (ct_top > cb_top) then
-             0x0
+             0b0
         else if ((ct_perms & cb_perms) != cb_perms) then
-             0x0
+             0b0
         else
-             0x1);
-     wGPR(rd) := result;
+             0b1;
+     wGPR(rd) = EXTZ(result);
   }
-  (* END_CTestSubset *)
+  /* END_CTestSubset */
 }
 
-union ast member regregreg CSeal
+union clause ast = CSeal : (regno, regno, regno)
 function clause execute (CSeal(cd, cs, ct)) =
 {
-  (* START_CSeal *)
+  /* START_CSeal */
   checkCP2usable();
-  cs_val := readCapReg(cs);
-  ct_val := readCapReg(ct);
-  ct_cursor := getCapCursor(ct_val);
-  ct_top    := getCapTop(ct_val);
-  ct_base   := getCapBase(ct_val);
+  cs_val = readCapReg(cs);
+  ct_val = readCapReg(ct);
+  ct_cursor = getCapCursor(ct_val);
+  ct_top    = getCapTop(ct_val);
+  ct_base   = getCapBase(ct_val);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cs)) then
@@ -895,24 +894,24 @@ function clause execute (CSeal(cd, cs, 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
+    let (success, newCap) = sealCap(cs_val, to_bits(24, ct_cursor)) in
     if not (success) then
         raise_c2_exception(CapEx_InexactBounds, cs)
     else
         writeCapReg(cd, newCap)
-  (* END_CSeal *)
+  /* END_CSeal */
 }
 
-union ast member regregreg CCSeal
+union clause ast = CCSeal : (regno, regno, regno)
 function clause execute (CCSeal(cd, cs, ct)) =
 {
-  (* START_CCSeal *)
+  /* START_CCSeal */
   checkCP2usable();
-  cs_val := readCapReg(cs);
-  ct_val := readCapReg(ct);
-  ct_cursor := getCapCursor(ct_val);
-  ct_top    := getCapTop(ct_val);
-  ct_base   := getCapBase(ct_val);
+  cs_val = readCapReg(cs);
+  ct_val = readCapReg(ct);
+  ct_cursor = getCapCursor(ct_val);
+  ct_top    = getCapTop(ct_val);
+  ct_base   = getCapBase(ct_val);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cs)) then
@@ -936,22 +935,22 @@ function clause execute (CCSeal(cd, cs, 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
+    let (success, newCap) = sealCap(cs_val, to_bits(24, ct_cursor)) in
     if not (success) then
         raise_c2_exception(CapEx_InexactBounds, cs)
     else
         writeCapReg(cd, newCap)
-  (* END_CCSeal *)
+  /* END_CCSeal */
 }
 
-union ast member regregreg CUnseal
+union clause ast = CUnseal : (regno, regno, regno)
 function clause execute (CUnseal(cd, cs, ct)) =
 {
-  (* START_CUnseal *)
+  /* START_CUnseal */
   checkCP2usable();
-  cs_val := readCapReg(cs);
-  ct_val := readCapReg(ct);
-  ct_cursor := getCapCursor(ct_val);
+  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
@@ -976,22 +975,22 @@ function clause execute (CUnseal(cd, cs, ct)) =
     raise_c2_exception(CapEx_LengthViolation, ct)
   else
     writeCapReg(cd, {cs_val with 
-      sealed=false; 
-      otype=0;
+      sealed=false,
+      otype=zeros(),
       global=(cs_val.global & ct_val.global)
     })
-  (* END_CUnseal *)
+  /* END_CUnseal */
 }
 
-union ast member (regno, regno, bit[11]) CCall
-function clause execute (CCall(cs, cb, 0b00000000000)) = (* selector=0 *)
+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 *)
+  /* 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);
-  cs_cursor := getCapCursor(cs_val);
+  cs_val = readCapReg(cs);
+  cb_val = readCapReg(cb);
+  cs_cursor = getCapCursor(cs_val);
   if (register_inaccessible(cs)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
   else if (register_inaccessible(cb)) then
@@ -1016,17 +1015,17 @@ function clause execute (CCall(cs, cb, 0b00000000000)) = (* selector=0 *)
     raise_c2_exception(CapEx_LengthViolation, cs)
   else
     raise_c2_exception(CapEx_CallTrap, cs);
-  (* END_CCall *)
+  /* END_CCall */
 }
 
-function clause execute (CCall(cs, cb, 0b00000000001)) = (* selector=1 *)
+function clause execute (CCall(cs, cb, 0b00000000001)) = /* selector=1 */
 {
-  (* Jump-like implementation of CCall that unseals arguments *)
-  (* START_CCall2 *)
+  /* Jump-like implementation of CCall that unseals arguments */
+  /* START_CCall2 */
   checkCP2usable();
-  cs_val := readCapReg(cs);
-  cb_val := readCapReg(cb);
-  cs_cursor := getCapCursor(cs_val);
+  cs_val = readCapReg(cs);
+  cb_val = readCapReg(cb);
+  cs_cursor = getCapCursor(cs_val);
   if (register_inaccessible(cs)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
   else if (register_inaccessible(cb)) then
@@ -1055,71 +1054,71 @@ function clause execute (CCall(cs, cb, 0b00000000001)) = (* selector=1 *)
     raise_c2_exception(CapEx_LengthViolation, cs)
   else
     let csUnsealed = capStructToCapReg({cs_val with
-        sealed=false;
-        otype=0;
+        sealed=false,
+        otype=zeros()
     }) in {
-      delayedPC := (bit[64]) (getCapOffset(cs_val));
-      delayedPCC := csUnsealed;
-      branchPending := 0b1;
-      inCCallDelay  := 0b1;
-      C26 := capStructToCapReg({cb_val with
-        sealed=false;
-        otype=0;
+      delayedPC = to_bits(64, getCapOffset(cs_val));
+      delayedPCC = csUnsealed;
+      branchPending = 0b1;
+      inCCallDelay  = 0b1;
+      C26 = capStructToCapReg({cb_val with
+        sealed=false,
+        otype=zeros()
       });
     }
-  (* END_CCall2 *)
+  /* END_CCall2 */
 }
 
-union ast member unit CReturn
+union clause ast = CReturn : unit
 function clause execute (CReturn) =
 {
-  (* START_CReturn *)
+  /* START_CReturn */
   checkCP2usable();
   raise_c2_exception_noreg(CapEx_ReturnTrap)
-  (* END_CReturn *)
+  /* END_CReturn */
 }
 
-union ast member (regno, bit[16], bool) CBX
+union clause ast = CBX : (regno, bits(16), bool)
 function clause execute (CBX(cb, imm, invert)) =
 {
-  (* START_CBx *)
+  /* 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;
+      let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in
+      delayedPC     = PC + offset;
+      branchPending = 0b1;
     }
-  (* END_CBx *)
+  /* END_CBx */
 }
 
-union ast member (regno, bit[16], bool) CBZ
+union clause ast = CBZ : (regno, bits(16), bool)
 function clause execute (CBZ(cb, imm, invert)) =
 {
-  (* START_CBz *)
+  /* START_CBz */
   checkCP2usable();
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else if (((readCapReg(cb)) == null_cap) ^ invert) then
     {
-      let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
-      delayedPC     := PC + offset;
-      branchPending := 1;
+      let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in
+      delayedPC     = PC + offset;
+      branchPending = 0b1;
     }
-  (* END_CBz *)
+  /* END_CBz */
 }
 
-union ast member (regno, regno, bool) CJALR
+union clause ast = CJALR : (regno, regno, bool)
 function clause execute(CJALR(cd, cb, link)) = 
 {
-  (* START_CJALR *)
+  /* START_CJALR */
   checkCP2usable();
-  cb_val := readCapReg(cb);
-  cb_ptr := getCapCursor(cb_val);
-  cb_top := getCapTop(cb_val);
-  cb_base:= getCapBase(cb_val);
+  cb_val = readCapReg(cb);
+  cb_ptr = getCapCursor(cb_val);
+  cb_top = getCapTop(cb_val);
+  cb_base= getCapBase(cb_val);
   if (link & register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -1134,7 +1133,7 @@ function clause execute(CJALR(cd, cb, link)) =
     raise_c2_exception(CapEx_LengthViolation, cb)
   else if ((cb_ptr + 4) > cb_top) then
     raise_c2_exception(CapEx_LengthViolation, cb)
-  else if ((cb_ptr mod 4) != 0) then
+  else if ((cb_ptr % 4) != 0) then
     SignalException(AdEL)
   else
     {
@@ -1145,19 +1144,19 @@ function clause execute(CJALR(cd, cb, link)) =
             writeCapReg(cd, linkCap)
         else
             assert(false, "");
-      delayedPC :=  (bit[64]) (getCapOffset(cb_val));
-      delayedPCC := capStructToCapReg(cb_val);
-      branchPending := 1;
+      delayedPC =  to_bits(64, getCapOffset(cb_val));
+      delayedPCC = capStructToCapReg(cb_val);
+      branchPending = 0b1;
     }
-  (* END_CJALR *)
+  /* END_CJALR */
 }
 
-union ast member (regno, regno, regno, bit[8], bool, WordType, bool) CLoad
+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 *)
+  /* START_CLoad */
   checkCP2usable();
-  cb_val := readCapReg(cb);
+  cb_val = readCapReg(cb);
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else if not (cb_val.tag) then
@@ -1168,10 +1167,10 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
     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]) (to_svec(vAddr));
+      size   = wordWidthBytes(width);
+      cursor = getCapCursor(cb_val);
+      vAddr  = cursor + unsigned(rGPR(rt)) + (size*signed(offset));
+      vAddr64= to_bits(64, vAddr);
       if ((vAddr + size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
@@ -1180,12 +1179,12 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
         SignalExceptionBadAddr(AdEL, vAddr64)
       else
         {
-          pAddr      := (TLBTranslate(vAddr64, LoadData));
-          widthBytes := wordWidthBytes(width);
-          (bit[64]) memResult := if (linked) then
+          pAddr      = (TLBTranslate(vAddr64, LoadData));
+          widthBytes = wordWidthBytes(width);
+          memResult : bits(64) = if (linked) then
               {
-                CP0LLBit  := 0b1;
-                CP0LLAddr := pAddr;
+                CP0LLBit  = 0b1;
+                CP0LLAddr = pAddr;
                 if widthBytes == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signext)
                 else if widthBytes == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signext)
                 else if widthBytes == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signext)
@@ -1198,19 +1197,19 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
                 else if widthBytes == 4 then extendLoad(MEMr_wrapper(pAddr, 4), signext)
                 else extendLoad(MEMr_wrapper(pAddr, 8), signext)
               };
-          wGPR(rd) := memResult;
+          wGPR(rd) = memResult;
         }
     }
-  (* END_CLoad *)
+  /* END_CLoad */
 }
 
-union ast member (regno, regno, regno, regno, bit[8], WordType, bool) CStore
+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 *)
+  /* START_CStore */
   checkCP2usable();
-  cb_val := readCapReg(cb);
+  cb_val = readCapReg(cb);
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else if not (cb_val.tag) then
@@ -1221,10 +1220,10 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
     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]) (to_svec(vAddr));
+      size   = wordWidthBytes(width);
+      cursor = getCapCursor(cb_val);
+      vAddr  = cursor + unsigned(rGPR(rt)) + (size * signed(offset));
+      vAddr64= to_bits(64, vAddr);
       if ((vAddr + size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
@@ -1233,42 +1232,42 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
         SignalExceptionBadAddr(AdES, vAddr64)
       else
         {
-          pAddr  := (TLBTranslate(vAddr64, StoreData));
-          rs_val := rGPR(rs);
+          pAddr  = (TLBTranslate(vAddr64, StoreData));
+          rs_val = rGPR(rs);
           if (conditional) then
             {
-              (bool) success := if (CP0LLBit[0]) then
-                  switch(width)
+              success : bool = if (CP0LLBit[0]) then
+                  match 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)
+                      B  => MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0]),
+                      H  => MEMw_conditional_wrapper(pAddr, 2, rs_val[15..0]),
+                      W  => MEMw_conditional_wrapper(pAddr, 4, rs_val[31..0]),
+                      D  => MEMw_conditional_wrapper(pAddr, 8, rs_val)
                     }
                 else
                   false;
-              wGPR(rd) := EXTZ([success]);
+              wGPR(rd) = EXTZ(success);
             }
             else
-          switch(width)
+          match 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
+              B  => MEMw_wrapper(pAddr, 1) = rs_val[7..0],
+              H  => MEMw_wrapper(pAddr, 2) = rs_val[15..0],
+              W  => MEMw_wrapper(pAddr, 4) = rs_val[31..0],
+              D  => MEMw_wrapper(pAddr, 8) = rs_val
             }
         }
     }
-  (* END_CStore *)
+  /* END_CStore */
 }
 
-union ast member (regno, regno, regno, regno, bit[11], bool) CSC
+union clause ast = CSC : (regno, regno, regno, regno, bits(11), bool)
 function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
 {
-  (* START_CSC *)
+  /* START_CSC */
   checkCP2usable();
-  cs_val := readCapReg(cs);
-  cb_val := readCapReg(cb);
+  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
@@ -1283,41 +1282,41 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
     raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb)
   else
     {
-      cursor := getCapCursor(cb_val);
-      vAddr  := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset));
-      vAddr64:= (bit[64]) (to_svec(vAddr));
+      cursor = getCapCursor(cb_val);
+      vAddr  = cursor + unsigned(rGPR(rt)) + (16 * signed(offset));
+      vAddr64= to_bits(64, vAddr);
       if ((vAddr + cap_size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
-      else if ((vAddr mod cap_size) != 0) then
+      else if ((vAddr % cap_size) != 0) then
         SignalExceptionBadAddr(AdES, vAddr64)
       else
         {
-          let (pAddr, noStoreCap)  = (TLBTranslateC(vAddr64, StoreData)) in
+          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
+              success = if (CP0LLBit[0]) then
                   MEMw_tagged_conditional(pAddr, cs_val.tag, capStructToMemBits(cs_val))
                 else
                   false;
-              wGPR(rd) := EXTZ([success]);
+              wGPR(rd) = EXTZ(success);
             }
           else
             MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val));
         }
     }
-  (* END_CSC *)
+  /* END_CSC */
 }
 
-union ast member (regno, regno, regno, bit[11], bool) CLC
+union clause ast = CLC : (regno, regno, regno, bits(11), bool)
 function clause execute (CLC(cd, cb, rt, offset, linked)) =  
 {
-  (* START_CLC *)
+  /* START_CLC */
   checkCP2usable();
-  cb_val := readCapReg(cb);
+  cb_val = readCapReg(cb);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -1328,35 +1327,36 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
     raise_c2_exception(CapEx_SealViolation, cb)
   else
     {
-      cursor := getCapCursor(cb_val);
-      vAddr  := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset));
-      vAddr64:= (bit[64]) (to_svec(vAddr));
+      cursor = getCapCursor(cb_val);
+      vAddr  = cursor + unsigned(rGPR(rt)) + (16 * signed(offset));
+      vAddr64= to_bits(64, vAddr);
       if ((vAddr + cap_size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
-      else if ((vAddr mod cap_size) != 0) then
+      else if ((vAddr % cap_size) != 0) then
         SignalExceptionBadAddr(AdEL, vAddr64)
       else
         {
-          let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in
+          let (pAddr, suppressTag) = TLBTranslateC(vAddr64, LoadData) in
+          let 'cd = unsigned(cd) in
           if (linked) then
             {
-              CP0LLBit  := 0b1;
-              CP0LLAddr := pAddr;
+              CP0LLBit  = 0b1;
+              CP0LLAddr = pAddr;
               let (tag, mem) = MEMr_tagged_reserve(pAddr) in
-              (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem);
+              (*CapRegs[cd]) = memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem);
             }
           else
             {
               let (tag, mem) = MEMr_tagged(pAddr) in
-              (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem);
+              (*CapRegs[cd]) = memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem);
             }
         }
     }
-  (* END_CLC *)
+  /* END_CLC */
 }
 
-union ast member (regno) C2Dump
+union clause ast = C2Dump : regno
 function clause execute (C2Dump (rt)) =
-    () (* Currently a NOP *)
+    () /* Currently a NOP */
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index cc939f59..23881f03 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -1,51 +1,51 @@
-(*========================================================================*)
-(*                                                                        *)
-(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
-(*  Copyright (c) 2015-2017 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.                                                          *)
-(*========================================================================*)
-
-(* 128 bit cap + tag *)
-typedef CapReg = bit[129]
-
-val cast extern bool -> bit effect pure cast_bool_bit
-val cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
-val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec
+/*========================================================================*/
+/*                                                                        */
+/*  Copyright (c) 2015-2017 Robert M. Norton                              */
+/*  Copyright (c) 2015-2017 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.                                                          */
+/*========================================================================*/
+
+/* 128 bit cap + tag */
+type CapReg = bits(129)
+
+val cast_bool_bit : cast extern bool -> bit effect pure
+val cast_boolvec_bitvec : cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure
+val cast_range_bitvec : cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure
 function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v)
-val extern bool -> bool effect pure not
+val not : extern bool -> bool effect pure
 
-typedef uint64 = range<0, (2** 64) - 1>
+type uint64 = range<0, (2** 64) - 1>
 
-typedef CapStruct = const struct {
+type CapStruct = const struct {
   bool    tag;
-  bit[4]  uperms;
+  bits(4)  uperms;
   bool    access_system_regs;
   bool    perm_reserved9;
   bool    permit_ccall;
@@ -57,16 +57,16 @@ typedef CapStruct = const struct {
   bool    permit_load;
   bool    permit_execute;
   bool    global;
-  bit[2]  reserved;
-  bit[6]  E;
+  bits(2)  reserved;
+  bits(6)  E;
   bool    sealed;
-  bit[20] B;
-  bit[20] T;
-  bit[24] otype;
-  bit[64] address;
+  bits(20) B;
+  bits(20) T;
+  bits(24) otype;
+  bits(64) address;
 }
 
-let (CapStruct) null_cap = {
+let null_cap : CapStruct = {
   tag                    = false;
   uperms                 = 0;
   access_system_regs     = false;
@@ -81,7 +81,7 @@ let (CapStruct) null_cap = {
   permit_execute         = false;
   global                 = false;
   reserved               = 0;
-  E                      = 48; (* encoded as 0 in memory due to xor *)
+  E                      = 48; /* encoded as 0 in memory due to xor */
   sealed                 = false;
   B                      = 0;
   T                      = 0x10000;
@@ -89,14 +89,14 @@ let (CapStruct) null_cap = {
   address                = 0;
 }
 
-def Nat cap_size_t  = 16 (* cap size in bytes *)
-let ([:cap_size_t:]) cap_size = 16
+def Nat cap_size_t  = 16 /* cap size in bytes */
+let cap_size : [:cap_size_t:] = 16
 
 function CapStruct capRegToCapStruct((CapReg) c) =
-  let (bool)    s  = c[104] in
-  let (bit[20]) Bc = if s then c[103..96] : 0x000 else c[103..84] in
-  let (bit[20]) Tc = 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
+  let s : bool  = c[104] in
+  let Bc : bits(20) = if s then c[103..96] : 0x000 else c[103..84] in
+  let Tc : bits(20) = if s then c[83..76] : 0x000 else c[83..64] in
+  let otype : bits(24) = if s then c[95..84] : c[75..64] else 0 in
   {
     tag                    = c[128];
     uperms                 = c[127..124];
@@ -120,7 +120,7 @@ function CapStruct capRegToCapStruct((CapReg) c) =
     address                = c[63..0];
   }
 
-function (bit[11]) getCapHardPerms((CapStruct) cap) =
+function (bits(11)) getCapHardPerms((CapStruct) cap) =
    ([cap.access_system_regs]
   : [cap.perm_reserved9]
   : [cap.permit_ccall]
@@ -133,13 +133,13 @@ function (bit[11]) getCapHardPerms((CapStruct) cap) =
   : [cap.permit_execute]
   : [cap.global])
 
-function (bit[128]) capStructToMemBits128((CapStruct) cap) =
-    let (bit[20]) b = if cap.sealed then (cap.B)[19..12] : (cap.otype)[23..12] else cap.B in
-    let (bit[20]) t = if cap.sealed then (cap.T)[19..12] : (cap.otype)[11..0]  else cap.T in
+function (bits(128)) capStructToMemBits128((CapStruct) cap) =
+    let b : bits(20) = if cap.sealed then (cap.B)[19..12] : (cap.otype)[23..12] else cap.B in
+    let t : bits(20) = if cap.sealed then (cap.T)[19..12] : (cap.otype)[11..0]  else cap.T in
     ( cap.uperms
     : getCapHardPerms(cap)
     : cap.reserved
-    : (cap.E ^ 0b110000) (* XXX brackets required otherwise sail interpreter error *)
+    : (cap.E ^ 0b110000) /* XXX brackets required otherwise sail interpreter error */
     : [cap.sealed]
     : b
     : t
@@ -149,32 +149,32 @@ function (bit[128]) capStructToMemBits128((CapStruct) cap) =
 function (CapReg) capStructToCapReg((CapStruct) cap) =
     ([cap.tag] : capStructToMemBits128(cap))
 
-(* Reverse of above used when reading from memory *)
-function (CapReg) memBitsToCapBits128((bool) tag, (bit[128]) b) =
+/* Reverse of above used when reading from memory */
+function (CapReg) memBitsToCapBits128((bool) tag, (bits(128)) b) =
   ([tag] : b)
 
-(* When saving/restoring capabilities xor them with bits of null_cap --
+/* When saving/restoring capabilities xor them with bits of null_cap --
    this ensures that canonical null_cap is always all-zeros in memory
-   even though it may have bits set logically (e.g. length or exponent *)
+   even though it may have bits set logically (e.g. length or exponent */
 
-let (bit[128]) null_cap_bits = capStructToMemBits128(null_cap)
+let null_cap_bits : bits(128) = capStructToMemBits128(null_cap)
 
-function (bit[128]) capStructToMemBits((CapStruct) cap) =
+function (bits(128)) capStructToMemBits((CapStruct) cap) =
   capStructToMemBits128(cap) ^ null_cap_bits
 
-function (bit[129]) memBitsToCapBits((bool) tag, (bit[128]) b) =
+function (bits(129)) memBitsToCapBits((bool) tag, (bits(128)) b) =
   memBitsToCapBits128(tag, b ^ null_cap_bits)
 
-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 *)
+function (bits(31)) getCapPerms((CapStruct) cap) = 
+    let perms : bits(15) = 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) =
+function CapStruct setCapPerms((CapStruct) cap, (bits(31)) perms) =
     { cap with
       uperms                 = perms[18..15];
-      (* 14..11 reserved -- ignore *)
+      /* 14..11 reserved -- ignore */
       access_system_regs     = perms[10];
       perm_reserved9         = perms[9];
       permit_ccall           = perms[8];
@@ -188,41 +188,41 @@ function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) =
       global                 = perms[0];
       }
 
-function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) =
+function (bool, CapStruct) sealCap((CapStruct) cap, (bits(24)) otype) =
     if (((cap.T)[11..0] == 0) & ((cap.B)[11..0] == 0)) then
         (true, {cap with sealed=true; otype=otype})
     else
-        (false, cap (* was undefined but ocaml shallow embedding can't handle it *) )
-
-function [|-1:1|] 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
+        (false, cap /* was undefined but ocaml shallow embedding can't handle it */ )
+
+function [|-1:1|] a_top_correction((bits(20)) a_mid, (bits(20)) R, (bits(20)) bound) =
+    match a_mid < R, bound < R {
+      (false, false)  => 0
+      (false, true)   => 1
+      (true, false)   => -1
+      (true, true)    => 0
     }
 
 function uint64 getCapBase((CapStruct) c)  = 
-    let ([|48|])  E = min(unsigned(c.E), 48) in
-    let (bit[20]) Bc = c.B in
-    let (bit[65]) a = EXTZ(c.address) in
-    let (bit[20]) R = Bc - 0x01000 in (* wraps *)
-    let (bit[20]) a_mid = mask(a >> E) in
+    let E : [|48|] = min(unsigned(c.E), 48) in
+    let Bc : bits(20) = c.B in
+    let a : bits(65) = EXTZ(c.address) in
+    let R : bits(20) = Bc - 0x01000 in /* wraps */
+    let a_mid : bits(20) = mask(a >> E) in
     let correction = a_top_correction(a_mid, R, Bc) in
     let a_top = a >> (E+20) in
-    let (bit[64]) base = EXTZ((a_top + correction) : Bc) << E in
+    let base : bits(64) = EXTZ((a_top + correction) : Bc) << E in
     unsigned(base)
 
 function CapLen getCapTop ((CapStruct) c)  = 
-    let ([|45|])  E = min(unsigned(c.E), 48) in
-    let (bit[20]) Bc = c.B in
-    let (bit[20]) T = c.T in
-    let (bit[65]) a = EXTZ(c.address)  in
-    let (bit[20]) R = Bc - 0x01000 in (* wraps *)
-    let (bit[20]) a_mid = mask(a >> E) in
+    let E : [|45|] = min(unsigned(c.E), 48) in
+    let Bc : bits(20) = c.B in
+    let T : bits(20) = c.T in
+    let a : bits(65) = EXTZ(c.address)  in
+    let R : bits(20) = Bc - 0x01000 in /* wraps */
+    let a_mid : bits(20) = mask(a >> E) in
     let correction = a_top_correction(a_mid, R, T) in
     let a_top = a >> (E+20) in
-    let (bit[65]) top1 = EXTZ((a_top + correction) : T) in
+    let top1 : bits(65) = EXTZ((a_top + correction) : T) in
     (CapLen) (top1 << E)
 
 function uint64 getCapOffset((CapStruct) c) = 
@@ -233,58 +233,58 @@ function CapLen getCapLength((CapStruct) c)  = getCapTop(c) - getCapBase(c)
 
 function uint64 getCapCursor((CapStruct) cap) = unsigned(cap.address)
 
-function bool fastRepCheck((CapStruct) c, (bit[64]) i) =
+function bool fastRepCheck((CapStruct) c, (bits(64)) i) =
     if ((c.E) >= 44) then
-        true (* in this case representable region is whole address space *)
+        true /* in this case representable region is whole address space */
     else
         let E        = min(unsigned(c.E), 43) in
         let i_top    = signed(i[63..E+20]) in
-        let (bit[20]) i_mid = i[E+19..E] in
-        let (bit[20]) a_mid = (c.address)[E+19..E] in
-        let (bit[20]) R     = (c.B) - 0x01000 in
-        let (bit[20]) diff  = R - a_mid in
-        let (bit[20]) diff1 = diff - 1 in
-        (* i_top determines 1. whether the increment is inRange
+        let i_mid : bits(20) = i[E+19..E] in
+        let a_mid : bits(20) = (c.address)[E+19..E] in
+        let R : bits(20)     = (c.B) - 0x01000 in
+        let diff : bits(20)  = R - a_mid in
+        let diff1 : bits(20) = diff - 1 in
+        /* i_top determines 1. whether the increment is inRange
            i.e. less than the size of the representable region
            (2**(E+20)) and 2. whether it is positive or negative. To
            satisfy 1. all top bits must be the same so we are
-           interested in the cases i_top is 0 or -1 *)
+           interested in the cases i_top is 0 or -1 */
         if (i_top == 0) then
           i_mid <_u diff1
         else if (i_top == -1) then
-          unsigned(i_mid) >= unsigned(diff) & (R != a_mid) (* XXX sail missing unsigned >= *)
+          unsigned(i_mid) >= unsigned(diff) & (R != a_mid) /* XXX sail missing unsigned >= */
         else
           false
 
-function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) =
-    let (bit[64]) base       = (bit[64]) (getCapBase(c)) in
-    let (bit[64]) newAddress = base + offset in
+function (bool, CapStruct) setCapOffset((CapStruct) c, (bits(64)) offset) =
+    let base : bits(64)       = (bits(64)) (getCapBase(c)) in
+    let newAddress : bits(64) = base + offset in
     let newCap     = { c with address = newAddress } in
     let representable = fastRepCheck(c, (newAddress - c.address)) in
     (representable, newCap)
 
-function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta) =
-    let (bit[64]) newAddress = c.address + delta in
+function (bool, CapStruct) incCapOffset((CapStruct) c, (bits(64)) delta) =
+    let newAddress : bits(64) = c.address + delta in
     let newCap     = { c with address = newAddress } in
     let representable = fastRepCheck(c, delta) in
     (representable, newCap)
 
-(** FUNCTION:integer HighestSetBit(bits(N) x) *)
+/** FUNCTION:integer HighestSetBit(bits(N) x) */
 
-function forall Nat 'N. option<[|0:('N + -1)|]> HighestSetBit((bit['N]) x) = {
+function forall Nat 'N. option([|0:('N + -1)|]) HighestSetBit((bits('N)) x) = {
   let N = (length(x)) in {
-  ([|('N + -1)|]) result := 0;
-  (bool) break := false;
+  ([|('N + -1)|]) result = 0;
+  (bool) break = false;
   foreach (i from (N - 1) downto 0)
     if ~(break) & x[i] == 1 then {
-      result := i;
-      break := true;
+      result = i;
+      break = true;
     };
 
   if break then Some(result) else None;
 }}
 
-(* hw rounds up E to multiple of 4 *)
+/* hw rounds up E to multiple of 4 */
 function [|48|] roundUp(([|45|]) e) =
     let r = e mod 4 in
     if (r == 0)
@@ -292,25 +292,25 @@ function [|48|] roundUp(([|45|]) e) =
     else (e - r + 4)
 
 
-function [|48|] computeE ((bit[65]) rlength) =
+function [|48|] computeE ((bits(65)) rlength) =
     let msb = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
-    switch (msb) {
-      (* above will always return <= 45 because 19 bits of zero are shifted in from right *)
-      case (Some(b)) -> {assert(b <= 45, None); roundUp (min(b,45)) }
-      case None    -> 0
+    match msb {
+      /* above will always return <= 45 because 19 bits of zero are shifted in from right */
+      (Some(b))  => {assert(b <= 45, None); roundUp (min(b,45)) }
+      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 ([|48|])  e = computeE(top - (0b0 : base)) in
-    let (bit[20]) Bc = 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=(bit[6]) e; B=Bc; T=T2} in
+function (bool, CapStruct) setCapBounds((CapStruct) cap, (bits(64)) base, (bits(65)) top) =
+    /* {cap with base=base; length=(bits(64)) length; offset=0} */
+    let e : [|48|] = computeE(top - (0b0 : base)) in
+    let Bc : bits(20) = base[19+e..e] in
+    let T : bits(20) = top[19+e..e] in
+    let T2 : bits(20) = T + if (top[(e - 1)..0] == 0) then 0 else 1 in
+    let newCap  = {cap with E=(bits(6)) e; B=Bc; 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) = 
+function CapStruct int_to_cap ((bits(64)) offset) = 
     {null_cap with address = offset}
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index 988cfe49..9e3a0cd9 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -1,226 +1,224 @@
-(*========================================================================*)
-(*                                                                        *)
-(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
-(*  Copyright (c) 2015-2017 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.                                                          *)
-(*========================================================================*)
-
-(* 256 bit cap + tag *)
-typedef CapReg = bit[257]
-
-val cast extern bool -> bit effect pure cast_bool_bit
-val cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
-val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec
+/*========================================================================*/
+/*                                                                        */
+/*  Copyright (c) 2015-2017 Robert M. Norton                              */
+/*  Copyright (c) 2015-2017 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.                                                          */
+/*========================================================================*/
+
+/* 256 bit cap + tag */
+type CapReg = bits(257)
+
+/*
+val cast_bool_bit : bool -> bit effect pure
+val cast_boolvec_bitvec :  'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure
+val cast_range_bitvec : forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure
 function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v)
-val extern bool -> bool effect pure not
-
-typedef uint64 = range<0, (2** 64) - 1>
-
-typedef CapStruct = const struct {
-  bool    tag;
-  bit[8]  padding;
-  bit[24] otype;
-  bit[16] uperms;
-  bit[4]  perm_reserved11_14;
-  bool    access_system_regs;
-  bool    perm_reserved9;
-  bool    permit_ccall;
-  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;
-  bool    sealed;
-  bit[64] offset;
-  bit[64] base;
-  bit[64] length;
+val not : extern bool -> bool effect pure */
+
+type uint64 = range(0, (2 ^ 64) - 1)
+
+struct CapStruct = {
+  tag                     : bool    ,
+  padding                 : bits(8) ,
+  otype                   : bits(24),
+  uperms                  : bits(16),
+  perm_reserved11_14      : bits(4) ,
+  access_system_regs      : bool    ,
+  perm_reserved9          : bool    ,
+  permit_ccall            : 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                  : bool    ,
+  sealed                  : bool    ,
+  offset                  : bits(64),
+  base                    : bits(64),
+  length                  : bits(64),
 }
 
-let (CapStruct) null_cap = {
-  tag = false;
-  padding = 0;
-  otype = 0;
-  uperms = 0;
-  perm_reserved11_14 = 0;
-  access_system_regs = false;
-  perm_reserved9 = false;
-  permit_ccall = 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;
-  sealed = false;
-  offset = 0;
-  base = 0;
-  length = 0xffffffffffffffff;
+let null_cap : CapStruct = struct {
+  tag = false,
+  padding = zeros(),
+  otype = zeros(),
+  uperms = zeros(),
+  perm_reserved11_14 = zeros(),
+  access_system_regs = false,
+  perm_reserved9 = false,
+  permit_ccall = 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,
+  sealed = false,
+  offset = zeros(),
+  base = zeros(),
+  length = 0xffffffffffffffff
 }
 
-def Nat cap_size_t  = 32 (* cap size in bytes *)
-let ([:cap_size_t:]) cap_size = 32
-
-function CapStruct capRegToCapStruct((CapReg) capReg) =
-  {
-    tag                        = capReg[256];
-    padding                    = capReg[255..248];
-    otype                      = capReg[247..224];
-    uperms                     = capReg[223..208];
-    perm_reserved11_14         = capReg[207..204];
-    access_system_regs         = capReg[203];
-    perm_reserved9             = capReg[202];
-    permit_ccall               = capReg[201];
-    permit_seal                = capReg[200];
-    permit_store_local_cap     = capReg[199];
-    permit_store_cap           = capReg[198];
-    permit_load_cap            = capReg[197];
-    permit_store               = capReg[196];
-    permit_load                = capReg[195];
-    permit_execute             = capReg[194];
-    global                     = capReg[193];
-    sealed                     = capReg[192];
-    offset                     = capReg[191..128];
-    base                       = capReg[127..64];
-    length                     = capReg[63..0];
+let 'cap_size = 32
+
+function capRegToCapStruct(capReg) : CapReg -> CapStruct =
+  struct {
+    tag                        = capReg[256],
+    padding                    = capReg[255..248],
+    otype                      = capReg[247..224],
+    uperms                     = capReg[223..208],
+    perm_reserved11_14         = capReg[207..204],
+    access_system_regs         = capReg[203],
+    perm_reserved9             = capReg[202],
+    permit_ccall               = capReg[201],
+    permit_seal                = capReg[200],
+    permit_store_local_cap     = capReg[199],
+    permit_store_cap           = capReg[198],
+    permit_load_cap            = capReg[197],
+    permit_store               = capReg[196],
+    permit_load                = capReg[195],
+    permit_execute             = capReg[194],
+    global                     = capReg[193],
+    sealed                     = capReg[192],
+    offset                     = capReg[191..128],
+    base                       = capReg[127..64],
+    length                     = capReg[63..0]
   }
 
-function (bit[31]) getCapPerms((CapStruct) cap) = 
+function getCapPerms(cap) : CapStruct -> bits(31) = 
   (
     cap.uperms
-      : cap.perm_reserved11_14
-      : [cap.access_system_regs]
-      : [cap.perm_reserved9]
-      : [cap.permit_ccall]
-      : [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]
+      @ cap.perm_reserved11_14
+      @ cap.access_system_regs
+      @ cap.perm_reserved9
+      @ cap.permit_ccall
+      @ 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 used to convert capabilities to in-memory format 
+/* Function used to convert capabilities to in-memory format 
    - this is the same as register format except for the offset,
      field which is stored as an absolute cursor on CHERI
-     due to uarch optimisation *)
-function (bit[256]) capStructToMemBits256((CapStruct) cap) =
+     due to uarch optimisation */
+function capStructToMemBits256(cap) : CapStruct -> bits(256) =
   (
         cap.padding
-      : cap.otype
-      : getCapPerms(cap)
-      : [cap.sealed]
-        (* NB in memory format stores cursor, not offset *)
-      : (cap.base + cap.offset) 
-      : cap.base
-      : cap.length
+      @ cap.otype
+      @ getCapPerms(cap)
+      @ cap.sealed
+        /* NB in memory format stores cursor, not offset */
+      @ (cap.base + cap.offset) 
+      @ cap.base
+      @ cap.length
   )
 
 
-(* Reverse of above used when reading from memory *)
-function (bit[257]) memBitsToCapBits256((bool) tag, (bit[256]) b) =
-  ([tag]
-   : b[255..192]
-   : ((bit[64])(b[191..128] - b[127..64]))
-   : b[127..0]
+/* Reverse of above used when reading from memory */
+function memBitsToCapBits256(tag, b) : (bool, bits(256)) -> bits(257)=
+  (tag
+   @ b[255..192]
+   @ (b[191..128] - b[127..64])
+   @ b[127..0]
   )
 
-(* When saving/restoring capabilities xor them with bits of null_cap --
+/* When saving/restoring capabilities xor them with bits of null_cap --
    this ensures that canonical null_cap is always all-zeros in memory
-   even though it may have bits set logically (e.g. length or exponent *)
+   even though it may have bits set logically (e.g. length or exponent) */
 
-function (bit[256]) capStructToMemBits((CapStruct) cap) =
-  let (bit[256]) null_cap_bits = capStructToMemBits256(null_cap) in
+function capStructToMemBits(cap) : CapStruct -> bits(256)=
+  let null_cap_bits : bits(256) = capStructToMemBits256(null_cap) in
   capStructToMemBits256(cap) ^ null_cap_bits
 
-function (bit[257]) memBitsToCapBits((bool) tag, (bit[256]) b) =
-  let (bit[256]) null_cap_bits = capStructToMemBits256(null_cap) in
+function memBitsToCapBits(tag, b) : (bool, bits(256)) -> bits(257)  =
+  let null_cap_bits : bits(256) = capStructToMemBits256(null_cap) in
   memBitsToCapBits256(tag, b ^ null_cap_bits)
 
-function (CapReg) capStructToCapReg((CapStruct) cap) =
-    (
-      [cap.tag]
-      : cap.padding
-      : cap.otype
-      : getCapPerms(cap)
-      : [cap.sealed]
-      : cap.offset
-      : cap.base
-      : cap.length
-    )
-
-function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) =
+function capStructToCapReg(cap) : CapStruct -> CapReg =
+      cap.tag
+      @ cap.padding
+      @ cap.otype
+      @ getCapPerms(cap)
+      @ cap.sealed
+      @ cap.offset
+      @ cap.base
+      @ cap.length
+
+function setCapPerms(cap, perms) : (CapStruct, bits(31)) -> CapStruct =
     { cap with
-      uperms                 = perms[30..15];
-      perm_reserved11_14     = perms[14..11];
-      access_system_regs     = perms[10];
-      perm_reserved9         = perms[9];
-      permit_ccall           = 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) =
-    (true, {cap with sealed=true; otype=otype})
-
-function bit[64] getCapBase((CapStruct) c)        = c.base
-function [|0:2**65 - 2|] getCapTop((CapStruct) c) = unsigned(c.base) + unsigned(c.length)
-function bit[64] getCapOffset((CapStruct) c)      = c.offset
-function CapLen  getCapLength((CapStruct) c)      = unsigned(c.length)
-
-function uint64 getCapCursor((CapStruct) cap) = 
-  (unsigned(cap.base) + unsigned(cap.offset)) mod (pow2(64))
-
-function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = 
+      uperms                 = perms[30..15],
+      perm_reserved11_14     = perms[14..11],
+      access_system_regs     = perms[10],
+      perm_reserved9         = perms[9],
+      permit_ccall           = 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 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 getCapOffset(c) : CapStruct -> uint64 = unsigned(c.offset)
+function getCapLength(c) : CapStruct -> CapLen = unsigned(c.length)
+
+function getCapCursor(cap) : CapStruct -> uint64 = 
+  (unsigned(cap.base) + unsigned(cap.offset)) % (pow2(64))
+
+function setCapOffset(c, offset) : (CapStruct, bits(64)) -> (bool, CapStruct) = 
     (true, {c with offset=offset})
 
-function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta) =
-    let (bit[64]) newOffset = c.offset + delta in
+function incCapOffset(c, delta) : (CapStruct, bits(64)) -> (bool, CapStruct) =
+    let newOffset : bits(64) = c.offset + delta in
     (true, {c with offset = newOffset})
 
-function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) =
-    let (bit[65]) length = top - (0b0 : base) in
-    (true, {cap with base = base; length = length[63..0]; offset = 0})
+function setCapBounds(cap, base, top) : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct) =
+    let length : bits(65) = top - (0b0 @ base) in
+    (true, {cap with base = base, length = length[63..0], offset = zeros()})
 
-function CapStruct int_to_cap ((bit[64]) offset) = 
+function int_to_cap (offset) : bits(64) -> CapStruct = 
     {null_cap with offset = offset}
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index a2d3b441..6b29ffce 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -1,338 +1,363 @@
-(*========================================================================*)
-(*                                                                        *)
-(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
-(*  Copyright (c) 2015-2017 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.                                                          *)
-(*========================================================================*)
-
-
-scattered typedef ast = const union
-
-val ast -> unit effect {barr, eamem, escape, rmem, rmemt, rreg, undef, wmvt, wreg} execute
-scattered function unit execute
-
-val bit[32] -> option<ast> effect pure decode
-scattered function option<ast> decode
-
-
-register CapReg PCC
-register CapReg nextPCC
-register CapReg delayedPCC
-register (bit[1]) inCCallDelay
-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
+/*========================================================================*/
+/*                                                                        */
+/*  Copyright (c) 2015-2017 Robert M. Norton                              */
+/*  Copyright (c) 2015-2017 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.                                                          */
+/*========================================================================*/
+
+
+scattered union ast
+
+val execute : ast -> unit effect {barr, eamem, escape, rmem, rmemt, rreg, undef, wmvt, wreg}
+scattered function execute
+
+val decode : bits(32) -> option(ast) effect pure
+scattered function decode
+
+
+register PCC        : CapReg
+register nextPCC    : CapReg
+register delayedPCC : CapReg
+register inCCallDelay : bits(1)
+register C00 : CapReg /* aka default data capability, DDC */
+register C01 : CapReg
+register C02 : CapReg
+register C03 : CapReg
+register C04 : CapReg
+register C05 : CapReg
+register C06 : CapReg
+register C07 : CapReg
+register C08 : CapReg
+register C09 : CapReg
+register C10 : CapReg
+register C11 : CapReg
+register C12 : CapReg
+register C13 : CapReg
+register C14 : CapReg
+register C15 : CapReg
+register C16 : CapReg
+register C17 : CapReg
+register C18 : CapReg
+register C19 : CapReg
+register C20 : CapReg
+register C21 : CapReg
+register C22 : CapReg
+register C23 : CapReg
+register C24 : CapReg /* aka return code capability, RCC */
+register C25 : CapReg
+register C26 : CapReg /* aka invoked data capability, IDC */
+register C27 : CapReg /* aka kernel reserved capability 1, KR1C */
+register C28 : CapReg /* aka kernel reserved capability 2, KR2C */
+register C29 : CapReg /* aka kernel code capability, KCC */
+register C30 : CapReg /* aka kernel data capability, KDC */
+register C31 : CapReg /* aka exception program counter capability, EPCC */
+
+let IDC : regno = 0b11010 /* 26 */
+
+let CapRegs : vector(32, dec, register(CapReg)) =
+  [
+    ref C31,
+    ref C30,
+    ref C29,
+    ref C28,
+    ref C27,
+    ref C26,
+    ref C25,
+    ref C24,
+    ref C23,
+    ref C22,
+    ref C21,
+    ref C20,
+    ref C19,
+    ref C18,
+    ref C17,
+    ref C16,
+    ref C15,
+    ref C14,
+    ref C13,
+    ref C12,
+    ref C11,
+    ref C10,
+    ref C09,
+    ref C08,
+    ref C07,
+    ref C06,
+    ref C05,
+    ref C04,
+    ref C03,
+    ref C02,
+    ref C01,
+    ref C00
   ]
 
-let max_otype = MAX(24) (*0xffffff*)
+let max_otype = MAX(24) /*0xffffff*/
 let have_cp2 = true
 
-function (CapStruct) readCapReg((regno) n) =
-  capRegToCapStruct(CapRegs[n])
-
-function unit writeCapReg((regno) n, (CapStruct) cap) =
-  CapRegs[n] := capStructToCapReg(cap)
-
-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;
-  CapEx_PermitCCallViolation;
-  CapEx_AccessCCallIDCViolation;
+function readCapReg(n) : regno -> CapStruct =
+  let 'i = unsigned(n) in
+  capRegToCapStruct(reg_deref(CapRegs[i]))
+
+function writeCapReg(n, cap) : (regno, CapStruct) -> unit =
+  let 'i = unsigned(n) in
+  (*CapRegs[i]) = capStructToCapReg(cap) 
+
+enum CapEx = {
+  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,
+  CapEx_PermitCCallViolation,
+  CapEx_AccessCCallIDCViolation
 }
 
-typedef CPtrCmpOp = enumerate {
-  CEQ;
-  CNE;
-  CLT;
-  CLE;
-  CLTU;
-  CLEU;
-  CEXEQ;
-  CNEXEQ;
-}
-
-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
-    case CapEx_PermitCCallViolation         -> 0x19
-    case CapEx_AccessCCallIDCViolation      -> 0x1a
+function CapExCode(ex) : CapEx -> bits(8)=
+  match ex {
+    CapEx_None                          => 0x00,
+    CapEx_LengthViolation               => 0x01,
+    CapEx_TagViolation                  => 0x02,
+    CapEx_SealViolation                 => 0x03,
+    CapEx_TypeViolation                 => 0x04,
+    CapEx_CallTrap                      => 0x05,
+    CapEx_ReturnTrap                    => 0x06,
+    CapEx_TSSUnderFlow                  => 0x07,
+    CapEx_UserDefViolation              => 0x08,
+    CapEx_TLBNoStoreCap                 => 0x09,
+    CapEx_InexactBounds                 => 0x0a,
+    CapEx_GlobalViolation               => 0x10,
+    CapEx_PermitExecuteViolation        => 0x11,
+    CapEx_PermitLoadViolation           => 0x12,
+    CapEx_PermitStoreViolation          => 0x13,
+    CapEx_PermitLoadCapViolation        => 0x14,
+    CapEx_PermitStoreCapViolation       => 0x15,
+    CapEx_PermitStoreLocalCapViolation  => 0x16,
+    CapEx_PermitSealViolation           => 0x17,
+    CapEx_AccessSystemRegsViolation     => 0x18,
+    CapEx_PermitCCallViolation          => 0x19,
+    CapEx_AccessCCallIDCViolation       => 0x1a
   }
 
-typedef CapCauseReg = register bits [15:0] {
-  15..8: ExcCode;
-  7..0:  RegNum;
+bitfield CapCauseReg : bits(16) = {
+  ExcCode : 15..8,
+  RegNum : 7..0,
 }
 
-register CapCauseReg CapCause
+register CapCause : CapCauseReg
 
-function forall Type 'o . 'o SignalException ((Exception) ex) = 
+function SignalException (ex) = 
   {
-    if (~ (CP0Status.EXL)) then {
-      let pc  = (bit[64]) PC in (* Cast forces read of register. *)
+    if (not (CP0Status.EXL())) then {
+      let pc  = PC in 
       let pcc = capRegToCapStruct(PCC) in
       let (success, epcc) = setCapOffset(pcc, pc) in
       if (success) then
-        C31 := capStructToCapReg(epcc)
+        C31 = capStructToCapReg(epcc)
       else
-        C31 := capStructToCapReg(int_to_cap(getCapBase(pcc) + pc));
+        C31 = capStructToCapReg(int_to_cap(to_bits(64, getCapBase(pcc)) + unsigned(pc)));
     };
 
-    nextPCC    := C29; (* KCC *)
-    delayedPCC := C29; (* always write delayedPCC together with nextPCC so 
-                          that non-capability branches don't override PCC *)
-    let base = (bit[64]) (getCapBase(capRegToCapStruct(C29))) in
-    SignalExceptionMIPS(ex, base);
+    nextPCC    = C29; /* KCC */
+    delayedPCC = C29; /* always write delayedPCC together with nextPCC so 
+                          that non-capability branches don't override PCC */
+    let base = getCapBase(capRegToCapStruct(C29)) in
+    SignalExceptionMIPS(ex, to_bits(64, base));
   }
 
-function unit ERETHook() =
+function ERETHook() : unit -> unit =
   {
-    nextPCC    := C31;
-    delayedPCC := C31; (* always write delayedPCC together with nextPCC so 
-                          that non-capability branches don't override PCC *)
+    nextPCC    = C31;
+    delayedPCC = C31; /* always write delayedPCC together with nextPCC so 
+                          that non-capability branches don't override PCC */
   }
 
-function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) =
+val raise_c2_exception8 : forall ('o : Type) . (CapEx, bits(8)) -> 'o effect {escape, rreg, wreg}
+function raise_c2_exception8(capEx, regnum) =
   {
-    (CapCause.ExcCode) := CapExCode(capEx);
-    (CapCause.RegNum)  := 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) =
-  let reg8 = 0b000 : regnum in
-  if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == 26 (* IDC *))) then
+val raise_c2_exception : forall ('o : Type) . (CapEx, regno) -> 'o effect {escape, rreg, wreg}
+function raise_c2_exception(capEx, regnum) =
+  let reg8 = 0b000 @ regnum in
+  if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == IDC)) then
      raise_c2_exception8(CapEx_AccessCCallIDCViolation, reg8)
   else
      raise_c2_exception8(capEx, reg8)
 
-function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) =
+val raise_c2_exception_noreg : forall ('o : Type) . (CapEx) -> 'o effect {escape, rreg, wreg}
+function raise_c2_exception_noreg(capEx) =
   raise_c2_exception8(capEx, 0xff)
 
-function bool pcc_access_system_regs () = 
+val pcc_access_system_regs : unit -> bool effect {rreg}
+function pcc_access_system_regs () = 
       let pcc = capRegToCapStruct(PCC) in
       (pcc.access_system_regs)
 
-function bool register_inaccessible((regno) r) =
-  if ((r == 26 (* IDC *)) & ((bool)inCCallDelay)) then true else (* XXX interpreter crash without cast *)
-  let (bool) is_sys_reg = switch(r) {
-    case 0b11011 -> true
-    case 0b11100 -> true
-    case 0b11101 -> true
-    case 0b11110 -> true
-    case 0b11111 -> true
-    case _       -> false
+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
 
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bool, bit[8 * 'n]) effect { rmemt } MEMr_tag
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bool, bit[8 * 'n]) effect { rmemt } MEMr_tag_reserve
+val MEMr_tag         : forall 'n. ( bits(64) , atom('n) ) -> (bool, bits(8 * 'n)) effect { rmemt }
+val MEMr_tag_reserve : forall 'n. ( bits(64) , atom('n) ) -> (bool, bits(8 * 'n)) effect { rmemt }
 
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bool, bit[8 * 'n]) -> unit effect { wmvt } MEMval_tag
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bool, bit[8 * 'n]) -> bool effect { wmvt } MEMval_tag_conditional
+val MEMval_tag : forall 'n. ( bits(64) , atom('n), bool, bits(8*'n)) -> unit effect { wmvt }
+val MEMval_tag_conditional : forall 'n. ( bits(64) , atom('n), bool, bits(8*'n)) -> bool effect { wmvt }
 
-
-function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) =
-  (* assumes addr is cap. aligned *)
-  let (tag, data) = MEMr_tag (addr, cap_size) in
+val MEMr_tagged : bits(64) -> (bool, bits('cap_size * 8)) effect { rmemt }
+function MEMr_tagged (addr) =
+  /* assumes addr is cap. aligned */
+  let (tag, data) =  MEMr_tag (addr, cap_size) in
   (tag, reverse_endianness(data))
 
-
-function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) =
-  (* assumes addr is cap. aligned *)
+val MEMr_tagged_reserve : bits(64) -> (bool, bits('cap_size * 8)) effect { rmemt }
+function MEMr_tagged_reserve (addr) =
+  /* assumes addr is cap. aligned */
   let (tag, data) = MEMr_tag_reserve(addr, cap_size) in
   (tag, reverse_endianness(data))
 
-function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
+val MEMw_tagged : (bits(64), bool, bits('cap_size * 8)) -> unit effect { eamem, wmvt }
+function MEMw_tagged(addr, tag, data) =
 {
-  (* assumes addr is cap. aligned *)
+  /* assumes addr is cap. aligned */
   MEMea(addr, cap_size);
   MEMval_tag(addr, cap_size,  tag, reverse_endianness(data));
 }
 
-function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
+val MEMw_tagged_conditional : (bits(64), bool, bits('cap_size * 8)) -> bool effect { eamem, wmvt }
+function MEMw_tagged_conditional(addr, tag, data) =
 {
-  (* assumes addr is cap. aligned *)
+  /* assumes addr is cap. aligned */
   MEMea_conditional(addr, cap_size);
   MEMval_tag_conditional(addr, cap_size, tag, reverse_endianness(data));
 }
 
-val forall Nat 'n, 'n >= 1. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {wmvt, wreg, eamem} MEMw_wrapper
-function unit effect {wmvt, wreg, eamem} MEMw_wrapper(addr, size, data) =
+val MEMw_wrapper : forall 'n, 'n >= 1. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmvt, wreg, eamem}
+function MEMw_wrapper(addr, size, data) =
   let ledata = reverse_endianness(data) in
   if (addr == 0x000000007f000000) then
   {
-    UART_WDATA   := ledata[7..0];
-    UART_WRITTEN := 1;
+    UART_WDATA   = ledata[7..0];
+    UART_WRITTEN = 0b1;
   }
   else
   {
-    (* On cheri non-capability writes must clear the corresponding tag *)
+    /* On cheri non-capability writes must clear the corresponding tag */
     MEMea(addr, size);
     MEMval_tag(addr, size, false, ledata);
   }
 
-val forall Nat 'n, 'n >= 1. (bit[64], [:'n:], bit[8 * 'n]) -> bool effect {wmvt, eamem} MEMw_conditional_wrapper
-function bool effect {wmvt, eamem} MEMw_conditional_wrapper(addr, size, data) =
+val MEMw_conditional_wrapper : forall 'n, 'n >= 1. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {wmvt, eamem}
+function MEMw_conditional_wrapper(addr, size, data) =
   {
-    (* On cheri non-capability writes must clear the corresponding tag*)
+    /* On cheri non-capability writes must clear the corresponding tag*/
     MEMea_conditional(addr, size);
     MEMval_tag_conditional(addr,size,false,reverse_endianness(data));
   }
 
-function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
+val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) effect {rreg, wreg, escape}
+function addrWrapper(addr, accessType, width) =
   {
-    capno := 0b00000;
-    cap := readCapReg(capno);
-    if (~(cap.tag)) then
+    capno = 0b00000;
+    cap = readCapReg(capno);
+    if (not (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))
+    match accessType {
+      Instruction  => if (~(cap.permit_execute)) then (raise_c2_exception(CapEx_PermitExecuteViolation, capno)),
+      LoadData     => if (~(cap.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, capno)),
+      StoreData    => if (~(cap.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, capno))
     };
-    cursor := getCapCursor(cap);
-    vAddr  := cursor + unsigned(addr);
-    size   := wordWidthBytes(width);
-    base   := getCapBase(cap);
-    top    := getCapTop(cap);
+    cursor = getCapCursor(cap);
+    vAddr  = cursor + unsigned(addr);
+    size   = wordWidthBytes(width);
+    base   = getCapBase(cap);
+    top    = getCapTop(cap);
     if ((vAddr + size) > top) then
       (raise_c2_exception(CapEx_LengthViolation, capno))
-    else if (vAddr < (base)) then
+    else if (vAddr < base) then
       (raise_c2_exception(CapEx_LengthViolation, capno))
     else
-      (bit[64]) (to_vec(vAddr)); (* XXX vAddr not truncated because top <= 2^64 and size > 0 *)
+      to_bits(64, vAddr); /* XXX vAddr not truncated because top <= 2^64 and size > 0 */
   }
 
-function (bit[64]) TranslatePC ((bit[64]) vAddr) = {
+val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, undef, escape}
+function TranslatePC (vAddr) = {
   incrementCP0Count();
   let pcc = capRegToCapStruct(PCC) in
   let base  = getCapBase(pcc) in
   let top   = getCapTop(pcc) in
   let absPC = base + unsigned(vAddr) in
-  if ((absPC mod 4)  != 0) then (* bad PC alignment *)
-    (SignalExceptionBadAddr(AdEL, (bit[64]) absPC)) (* XXX absPC may be truncated *)
+  if ((absPC % 4)  != 0) then /* bad PC alignment */
+    (SignalExceptionBadAddr(AdEL, to_bits(64, absPC))) /* XXX absPC may be truncated */
   else if ((absPC + 4) > top) then
     (raise_c2_exception_noreg(CapEx_LengthViolation))
   else
-    TLBTranslate((bit[64]) absPC, Instruction) (* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps *)
+    TLBTranslate(to_bits(64, absPC), Instruction) /* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps */
 }
-
-function unit checkCP2usable () =
-  if not ((norm_dec (CP0Status.CU))[2]) then
+val checkCP2usable : unit -> unit effect {rreg, wreg, escape}
+function checkCP2usable ()  =
+  if not ((CP0Status.CU())[2]) then
     {
-      (CP0Cause.CE) := 0b10;
+      (CP0Cause->CE()) = 0b10;
       (SignalException(CpU));
     }
diff --git a/cheri/cheri_types.sail b/cheri/cheri_types.sail
index 031848f2..18043fa0 100644
--- a/cheri/cheri_types.sail
+++ b/cheri/cheri_types.sail
@@ -1,35 +1,54 @@
-(*========================================================================*)
-(*                                                                        *)
-(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
-(*  Copyright (c) 2015-2017 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.                                                          *)
-(*========================================================================*)
+/*========================================================================*/
+/*                                                                        */
+/*  Copyright (c) 2015-2017 Robert M. Norton                              */
+/*  Copyright (c) 2015-2017 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.                                                          */
+/*========================================================================*/
+
+type CapLen = range(0, 2 ^ 65)
+
+enum CPtrCmpOp = {
+  CEQ,
+  CNE,
+  CLT,
+  CLE,
+  CLTU,
+  CLEU,
+  CEXEQ,
+  CNEXEQ
+}
+
+enum ClearRegSet = {
+GPLo,
+GPHi,
+CLo,
+CHi
+}
 
-typedef CapLen = [|0 : 2**65|]