Merge branch 'mappings' into sail2

6 files changed, 577 insertions, 118 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index 8d9c3d6d..9e07ffa6 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,16 +1,17 @@
 SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail riscv.sail riscv_step.sail
 PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
 SAIL_DIR ?= $(realpath ..)
+SAIL ?= $(SAIL_DIR)/sail
 
 export SAIL_DIR
 
 all: platform Riscv.thy
 
 check: $(SAIL_SRCS) main.sail Makefile
-	$(SAIL_DIR)/sail $(SAIL_SRCS) main.sail
+	$(SAIL) $(SAIL_FLAGS) $(SAIL_SRCS) main.sail
 
 _sbuild/riscv.ml: $(SAIL_SRCS) Makefile main.sail
-	$(SAIL_DIR)/sail -ocaml -ocaml-nobuild -o riscv $(SAIL_SRCS)
+	$(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -o riscv $(SAIL_SRCS)
 
 _sbuild/platform_main.native: _sbuild/riscv.ml _tags $(PLATFORM_OCAML_SRCS) Makefile
 	cp _tags $(PLATFORM_OCAML_SRCS) _sbuild
@@ -20,10 +21,10 @@ platform: _sbuild/platform_main.native
 	rm -f $@ && ln -s $^ $@
 
 riscv_duopod_ocaml: prelude.sail riscv_duopod.sail
-	$(SAIL_DIR)/sail -ocaml -o $@ $^
+	$(SAIL) $(SAIL_FLAGS) -ocaml -o $@ $^
 
 riscv_duopod.lem: prelude.sail riscv_duopod.sail
-	$(SAIL_DIR)/sail -lem -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^
+	$(SAIL) $(SAIL_FLAGS) -lem -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^
 Riscv_duopod.thy: riscv_duopod.lem riscv_extras.lem
 	lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
 		riscv_extras.lem \
@@ -40,7 +41,7 @@ Riscv.thy: riscv.lem riscv_extras.lem
 	sed -i 's/datatype ast/datatype (plugins only: size) ast/' Riscv_types.thy
 
 riscv.lem: $(SAIL_SRCS) Makefile
-	$(SAIL_DIR)/sail -lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS)
+	$(SAIL) $(SAIL_FLAGS) -lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS)
 
 riscv_sequential.lem: $(SAIL_SRCS) Makefile
 	$(SAIL_DIR)/sail -lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS)
diff --git a/riscv/main.sail b/riscv/main.sail
index c923935b..b2a53b11 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -11,6 +11,7 @@ val elf_entry = {
 val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
 
 function main () = {
+
   PC = __GetSlice_int(64, elf_entry(), 0);
   try {
     init_sys ();
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 1bc4b4d6..d10dddc9 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -3,6 +3,67 @@ default Order dec
 type bits ('n : Int) = vector('n, dec, bit)
 union option ('a : Type) = {None : unit, Some : 'a}
 
+val spc : unit <-> string
+val opt_spc : unit <-> string
+val def_spc : unit <-> string
+
+val hex_bits : forall 'n . (atom('n), bits('n)) <-> string
+
+val hex_bits_4 : bits(4) <-> string
+val hex_bits_4_forwards = "string_of_bits" : bits(4) -> string
+val "hex_bits_4_matches_prefix" : string -> option((bits(4), nat))
+
+val hex_bits_5 : bits(5) <-> string
+val hex_bits_5_forwards = "string_of_bits" : bits(5) -> string
+val "hex_bits_5_matches_prefix" : string -> option((bits(5), nat))
+
+val hex_bits_6 : bits(6) <-> string
+val hex_bits_6_forwards = "string_of_bits" : bits(6) -> string
+val "hex_bits_6_matches_prefix" : string -> option((bits(6), nat))
+
+val hex_bits_12 : bits(12) <-> string
+val hex_bits_12_forwards = "string_of_bits" : bits(12) -> string
+val "hex_bits_12_matches_prefix" : string -> option((bits(12), nat))
+
+val hex_bits_13 : bits(13) <-> string
+val hex_bits_13_forwards = "string_of_bits" : bits(13) -> string
+val "hex_bits_13_matches_prefix" : string -> option((bits(13), nat))
+
+val hex_bits_20 : bits(20) <-> string
+val hex_bits_20_forwards = "string_of_bits" : bits(20) -> string
+val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat))
+
+val hex_bits_21 : bits(21) <-> string
+val hex_bits_21_forwards = "string_of_bits" : bits(21) -> string
+val "hex_bits_21_matches_prefix" : string -> option((bits(21), nat))
+
+val hex_bits_32 : bits(32) <-> string
+val hex_bits_32_forwards = "string_of_bits" : bits(32) -> string
+val "hex_bits_32_matches_prefix" : string -> option((bits(32), nat))
+
+
+val spc_forwards : unit -> string
+function spc_forwards () = " "
+val spc_backwards : string -> unit
+function spc_backwards s = ()
+
+val spc_matches_prefix = "spc_matches_prefix" : string -> option((unit, nat))
+
+val opt_spc_forwards : unit -> string
+function opt_spc_forwards () = ""
+val opt_spc_backwards : string -> unit
+function opt_spc_backwards s = ()
+
+val opt_spc_matches_prefix = "opt_spc_matches_prefix" : string -> option((unit, nat))
+
+val def_spc_forwards : unit -> string
+function def_spc_forwards () = " "
+val def_spc_backwards : string -> unit
+function def_spc_backwards s = ()
+
+val def_spc_matches_prefix = "opt_spc_matches_prefix" : string -> option((unit, nat))
+
+
 val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
 val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
@@ -10,12 +71,19 @@ val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool
 val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool
 
 val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
-
-val "eq_bit" : (bit, bit) -> bool
+val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool
 
 val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
 
 val eq_string = {ocaml: "eq_string", lem: "eq"} : (string, string) -> bool
+val string_startswith = "string_startswith" : (string, string) -> bool
+val string_drop = "string_drop" : (string, nat) -> string
+val string_length = "string_length" : string -> nat
+val string_append = "string_append" : (string, string) -> string
+val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat))
+val maybe_nat_of_prefix = "maybe_nat_of_prefix" : string -> option((nat, nat))
+val maybe_int_of_string = "maybe_int_of_string" : string -> option(int)
+
 
 val eq_real = {ocaml: "eq_real", lem: "eq"} : (real, real) -> bool
 
@@ -188,6 +256,9 @@ val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
 val sub_int = {ocaml: "sub_int", lem: "integerMinus"} : (int, int) -> int
+val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
+               lem: "integerMinus"}
+            : (nat, nat) -> nat
 
 val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index fd42df21..9f4385e7 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -1,7 +1,6 @@
 scattered union ast
 
 val decode : bits(32) -> option(ast) effect pure
-scattered function decode
 
 val decodeCompressed : bits(16) -> option(ast) effect pure
 scattered function decodeCompressed
@@ -13,11 +12,21 @@ scattered function execute
 val cast print_insn : ast -> string
 scattered function print_insn
 
+val assembly : ast <-> string
+scattered mapping assembly
+
+val encdec : ast <-> bits(32)
+scattered mapping encdec
+
 /* ****************************************************************** */
 union clause ast = UTYPE : (bits(20), regbits, uop)
 
-function clause decode imm : bits(20) @ rd : regbits @ 0b0110111 = Some(UTYPE(imm, rd, RISCV_LUI))
-function clause decode imm : bits(20) @ rd : regbits @ 0b0010111 = Some(UTYPE(imm, rd, RISCV_AUIPC))
+mapping encdec_uop : uop <-> bits(7) = {
+  RISCV_LUI   <-> 0b0110111,
+  RISCV_AUIPC <-> 0b0010111
+}
+
+mapping clause encdec = UTYPE(imm, rd, op) <-> imm @ rd @ encdec_uop(op)
 
 function clause execute UTYPE(imm, rd, op) =
     let off : xlenbits = EXTS(imm @ 0x000) in
@@ -35,10 +44,30 @@ function clause print_insn UTYPE(imm, rd, op) =
     RISCV_AUIPC => "auipc " ^ rd ^ ", " ^ BitStr(imm)
   }
 
+mapping utype_mnemonic : uop <-> string = {
+  RISCV_LUI   <-> "lui",
+  RISCV_AUIPC <-> "auipc"
+}
+
+mapping clause assembly = UTYPE(imm, rd, op) <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm)
+
 /* ****************************************************************** */
 union clause ast = RISCV_JAL : (bits(21), regbits)
 
-function clause decode imm : bits(20) @ rd : regbits @ 0b1101111 = Some (RISCV_JAL(imm[19] @ imm[7..0] @ imm[8] @ imm[18..13] @ imm[12..9] @ 0b0, rd))
+mapping clause encdec = RISCV_JAL(imm_19 @ imm_7_0 @ imm_8 @ imm_18_13 @ imm_12_9 @ 0b0, rd)
+                    <-> imm_19 : bits(1) @ imm_18_13 : bits(6) @ imm_12_9 : bits(4) @ imm_8 : bits(1) @ imm_7_0 : bits(8) @ rd @ 0b1101111
+
+/*
+ideally we want some syntax like
+
+mapping clause encdec = RISCV_JAL(imm @ 0b0, rd) <-> imm[19] @ imm[9..0] @ imm[10] @ imm[18..11] @ rd @ 0b1101111
+
+match bv {
+  imm[19] @ imm[9..0] @ imm[10] @ imm[18..11] -> imm @ 0b0
+}
+
+but this is difficult
+*/
 
 function clause execute (RISCV_JAL(imm, rd)) = {
     let pc : xlenbits = PC;
@@ -51,11 +80,14 @@ function clause execute (RISCV_JAL(imm, rd)) = {
 function clause print_insn (RISCV_JAL(imm, rd)) =
   "jal   " ^ rd ^ ", " ^ BitStr(imm)
 
+/* TODO: handle 2-byte-alignment in mappings */
+
+mapping clause assembly = RISCV_JAL(imm, rd) <-> "jal" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_21(imm)
+
 /* ****************************************************************** */
 union clause ast = RISCV_JALR : (bits(12), regbits, regbits)
 
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b1100111 =
-    Some(RISCV_JALR(imm, rs1, rd))
+mapping clause encdec = RISCV_JALR(imm, rs1, rd) <-> imm @ rs1 @ 0b000 @ rd @ 0b1100111
 
 function clause execute (RISCV_JALR(imm, rs1, rd)) = {
     /* write rd before anything else to prevent unintended strength */
@@ -68,15 +100,22 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
 function clause print_insn (RISCV_JALR(imm, rs1, rd)) =
   "jalr  " ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)
 
+mapping clause assembly = RISCV_JALR(imm, rs1, rd) <-> "jalr" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
+
 /* ****************************************************************** */
 union clause ast = BTYPE : (bits(13), regbits, regbits, bop)
 
-function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b000 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BEQ))
-function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b001 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BNE))
-function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b100 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BLT))
-function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b101 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BGE))
-function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b110 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BLTU))
-function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b111 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BGEU))
+mapping encdec_bop : bop <-> bits(3) = {
+  RISCV_BEQ <-> 0b000,
+  RISCV_BNE <-> 0b001,
+  RISCV_BLT <-> 0b100,
+  RISCV_BGE <-> 0b101,
+  RISCV_BLTU <-> 0b110,
+  RISCV_BGEU <-> 0b111
+}
+
+mapping clause encdec = BTYPE(imm7_6 @ imm5_0 @ imm7_5_0 @ imm5_4_1 @ 0b0, rs2, rs1, op)
+                    <-> imm7_6 : bits(1) @ imm7_5_0 : bits(6) @ rs2 @ rs1 @ encdec_bop(op) @ imm5_4_1 : bits(4) @ imm5_0 : bits(1) @ 0b1100011
 
 function clause execute (BTYPE(imm, rs2, rs1, op)) =
   let rs1_val = X(rs1) in
@@ -105,15 +144,31 @@ function clause print_insn (BTYPE(imm, rs2, rs1, op)) =
     } in
   insn ^ rs1 ^ ", " ^ rs2 ^ ", " ^ BitStr(imm)
 
+mapping btype_mnemonic : bop <-> string = {
+  RISCV_BEQ  <-> "beq",
+  RISCV_BNE  <-> "bne",
+  RISCV_BLT  <-> "blt",
+  RISCV_BGE  <-> "bge",
+  RISCV_BLTU <-> "bltu",
+  RISCV_BGEU <-> "bgeu"
+}
+
+mapping clause assembly = BTYPE(imm, rs2, rs1, op) <-> btype_mnemonic(op) ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_13(imm)
+
+
 /* ****************************************************************** */
 union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
 
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_SLTI))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_SLTIU))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_XORI))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ORI))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ANDI))
+mapping encdec_iop : iop <-> bits(3) = {
+  RISCV_ADDI  <-> 0b000,
+  RISCV_SLTI  <-> 0b010,
+  RISCV_SLTIU <-> 0b011,
+  RISCV_XORI  <-> 0b100,
+  RISCV_ORI   <-> 0b110,
+  RISCV_ANDI  <-> 0b111
+}
+
+mapping clause encdec = ITYPE(imm, rs1, rd, op) <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011
 
 function clause execute (ITYPE (imm, rs1, rd, op)) =
   let rs1_val = X(rs1) in
@@ -142,12 +197,29 @@ function clause print_insn (ITYPE(imm, rs1, rd, op)) =
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)
 
+mapping itype_mnemonic : iop <-> string = {
+  RISCV_ADDI  <-> "addi",
+  RISCV_SLTI  <-> "slti",
+  RISCV_SLTIU <-> "sltiu",
+  RISCV_XORI  <-> "xori",
+  RISCV_ORI   <-> "ori",
+  RISCV_ANDI  <-> "andi"
+}
+
+mapping clause assembly = ITYPE(imm, rs1, rd, op) <-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
+
 /* ****************************************************************** */
 union clause ast = SHIFTIOP : (bits(6), regbits, regbits, sop)
 
-function clause decode 0b000000 @ shamt : bits(6) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SLLI))
-function clause decode 0b000000 @ shamt : bits(6) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRLI))
-function clause decode 0b010000 @ shamt : bits(6) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRAI))
+mapping encdec_sop : sop <-> bits(3) = {
+  RISCV_SLLI <-> 0b001,
+  RISCV_SRLI <-> 0b101,
+  RISCV_SRAI <-> 0b101
+}
+
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011
 
 function clause execute (SHIFTIOP(shamt, rs1, rd, op)) =
     let rs1_val = X(rs1) in
@@ -169,19 +241,27 @@ function clause print_insn (SHIFTIOP(shamt, rs1, rd, op)) =
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(shamt)
 
+mapping shiftiop_mnemonic : sop <-> string = {
+  RISCV_SLLI <-> "slli",
+  RISCV_SRLI <-> "srli",
+  RISCV_SRAI <-> "srai"
+}
+
+mapping clause assembly = SHIFTIOP(shamt, rs1, rd, op) <-> shiftiop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ hex_bits_6(shamt)
+
 /* ****************************************************************** */
 union clause ast = RTYPE : (regbits, regbits, regbits, rop)
 
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_ADD))
-function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SUB))
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLL))
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLT))
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLTU))
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_XOR))
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SRL))
-function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SRA))
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_OR))
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_AND))
+mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_ADD)  <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011
+mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_SUB)  <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011
+mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_SLL)  <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011
+mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_SLT)  <-> 0b0000000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011
+mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_SLTU) <-> 0b0000000 @ rs2 @ rs1 @ 0b011 @ rd @ 0b0110011
+mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_XOR)  <-> 0b0000000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011
+mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_SRL)  <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011
+mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_SRA)  <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011
+mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_OR)   <-> 0b0000000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011
+mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_AND)  <-> 0b0000000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011
 
 function clause execute (RTYPE(rs2, rs1, rd, op)) =
   let rs1_val = X(rs1) in
@@ -218,16 +298,27 @@ function clause print_insn (RTYPE(rs2, rs1, rd, op)) =
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
 
+mapping rtype_mnemonic : rop <-> string = {
+  RISCV_ADD  <-> "add",
+  RISCV_SUB  <-> "sub",
+  RISCV_SLL  <-> "sll",
+  RISCV_SLT  <-> "slt",
+  RISCV_SLTU <-> "sltu",
+  RISCV_XOR  <-> "xor",
+  RISCV_SRL  <-> "srl",
+  RISCV_SRA  <-> "sra",
+  RISCV_OR   <-> "or",
+  RISCV_AND  <-> "and"
+}
+
+mapping clause assembly = RTYPE(rs2, rs1, rd, op) <-> rtype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, bool)
 
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, BYTE,   false, false))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, HALF,   false, false))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, WORD,   false, false))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  BYTE,   false, false))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  HALF,   false, false))
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  WORD,   false, false))
+/* I am assuming that load unsigned double wasn't meant to be missing here? */
+/* TODO: aq/rl */
+mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011
 
 val extend_value : forall 'n, 0 < 'n <= 8. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
 function extend_value(is_unsigned, value) = match (value) {
@@ -270,13 +361,33 @@ function clause print_insn (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)
 
+/* TODO FIXME: is this the actual aq/rl syntax? */
+val maybe_aq : bool <-> string
+mapping maybe_aq = {
+  true  <-> ".aq",
+  false <-> ""
+}
+
+val maybe_rl : bool <-> string
+mapping maybe_rl = {
+  true  <-> ".rl",
+  false <-> ""
+}
+
+val maybe_u : bool <-> string
+mapping maybe_u = {
+  true  <-> "u",
+  false <-> ""
+}
+
+
+mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl) <-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
+
 /* ****************************************************************** */
 union clause ast = STORE : (bits(12), regbits, regbits, word_width, bool, bool)
 
-function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b000 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, BYTE, false, false))
-function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b001 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, HALF, false, false))
-function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b010 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, WORD, false, false))
-function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b011 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, DOUBLE, false, false))
+/* TODO: aq/rl */
+mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011
 
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
@@ -320,10 +431,13 @@ function clause print_insn (STORE(imm, rs2, rs1, width, aq, rl)) =
     } in
   insn ^ rs2 ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)
 
+mapping clause assembly = STORE(imm, rs1, rd, size, aq, rl) <-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
+
+
 /* ****************************************************************** */
 union clause ast = ADDIW : (bits(12), regbits, regbits)
 
-function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0011011 = Some(ADDIW(imm, rs1, rd))
+mapping clause encdec = ADDIW(imm, rs1, rd) <-> imm @ rs1 @ 0b000 @ rd @ 0b0011011
 
 function clause execute (ADDIW(imm, rs1, rd)) = {
   let result : xlenbits = EXTS(imm) + X(rs1);
@@ -334,12 +448,14 @@ function clause execute (ADDIW(imm, rs1, rd)) = {
 function clause print_insn (ADDIW(imm, rs1, rd)) =
   "addiw " ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)
 
+mapping clause assembly = ADDIW(imm, rs1, rd) <-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
+
 /* ****************************************************************** */
 union clause ast = SHIFTW : (bits(5), regbits, regbits, sop)
 
-function clause decode 0b0000000 @ shamt : bits(5) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SLLI))
-function clause decode 0b0000000 @ shamt : bits(5) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SRLI))
-function clause decode 0b0100000 @ shamt : bits(5) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SRAI))
+mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI) <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011
+mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRLI) <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
+mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRAI) <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
 
 function clause execute (SHIFTW(shamt, rs1, rd, op)) =
     let rs1_val = (X(rs1))[31..0] in
@@ -361,14 +477,22 @@ function clause print_insn (SHIFTW(shamt, rs1, rd, op)) =
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(shamt)
 
+mapping shiftw_mnemonic : sop <-> string = {
+  RISCV_SLLI <-> "slli",
+  RISCV_SRLI <-> "srli",
+  RISCV_SRAI <-> "srai"
+}
+
+mapping clause assembly = SHIFTW(shamt, rs1, rd, op) <-> shiftw_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt)
+
 /* ****************************************************************** */
 union clause ast = RTYPEW : (regbits, regbits, regbits, ropw)
 
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_ADDW))
-function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SUBW))
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SLLW))
-function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SRLW))
-function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SRAW))
+mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW) <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
+mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SUBW) <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
+mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW) <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011
+mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRLW) <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011
+mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRAW) <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011
 
 function clause execute (RTYPEW(rs2, rs1, rd, op)) =
   let rs1_val = (X(rs1))[31..0] in
@@ -395,14 +519,30 @@ function clause print_insn (RTYPEW(rs2, rs1, rd, op)) =
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
 
+mapping rtypew_mnemonic : ropw <-> string = {
+  RISCV_ADDW <-> "addw",
+  RISCV_SUBW <-> "subw",
+  RISCV_SLLW <-> "sllw",
+  RISCV_SRLW <-> "srlw",
+  RISCV_SRAW <-> "sraw"
+}
+
+mapping clause assembly = RTYPEW(rs2, rs1, rd, op) <-> rtypew_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 /* FIXME: separate these out into separate ast variants */
 union clause ast = MUL : (regbits, regbits, regbits, bool, bool, bool)
 
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd, false,  true, true))  /* MUL */
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd,  true,  true, true))  /* MULH */
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd,  true,  true, false)) /* MULHSU */
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd,  true, false, false)) /* MULHU */
+mapping encdec_mul_op : (bool, bool, bool) <-> bits(3) = {
+  (false, true, true)  <-> 0b000,
+  (true, true, true)   <-> 0b001,
+  (true, true, false)  <-> 0b010,
+  (true, false, false) <-> 0b011
+}
+
+/* for some reason the : bits(3) here is still necessary - BUG */
+mapping clause encdec = MUL(rs2, rs1, rd, high, signed1, signed2) <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(high, signed1, signed2) : bits(3) @ rd @ 0b0110011
+
 function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) =
   let rs1_val = X(rs1) in
   let rs2_val = X(rs2) in
@@ -424,10 +564,20 @@ function clause print_insn (MUL(rs2, rs1, rd, high, signed1, signed2)) =
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
 
+mapping mul_mnemonic : (bool, bool, bool) <-> string = {
+  (false, true, true)  <-> "mul",
+  (true, true, true)   <-> "mulh",
+  (true, true, false)  <-> "mulhsu",
+  (true, false, false) <-> "mulhu"
+}
+
+mapping clause assembly = MUL(rs2, rs1, rd, high, signed1, signed2) <-> mul_mnemonic(high, signed1, signed2) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 union clause ast = DIV : (regbits, regbits, regbits, bool)
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0110011 = Some(DIV(rs2, rs1, rd,  true))  /* DIV */
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(DIV(rs2, rs1, rd, false))  /* DIVU */
+
+mapping clause encdec = DIV(rs2, rs1, rd, s) <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011
+
 function clause execute (DIV(rs2, rs1, rd, s)) =
   let rs1_val = X(rs1) in
   let rs2_val = X(rs2) in
@@ -443,10 +593,18 @@ function clause print_insn (DIV(rs2, rs1, rd, s)) =
   let insn : string = if s then "div   " else "divu  " in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
 
+mapping maybe_not_u : bool <-> string = {
+  false <-> "u",
+  true <-> ""
+}
+
+mapping clause assembly = DIV(rs2, rs1, rd, s) <-> "div" ^ maybe_not_u(s) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 union clause ast = REM : (regbits, regbits, regbits, bool)
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0110011 = Some(REM(rs2, rs1, rd,  true))  /* REM */
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0110011 = Some(REM(rs2, rs1, rd, false))  /* REMU */
+
+mapping clause encdec = REM(rs2, rs1, rd, s) <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011
+
 function clause execute (REM(rs2, rs1, rd, s)) =
   let rs1_val = X(rs1) in
   let rs2_val = X(rs2) in
@@ -462,9 +620,13 @@ function clause print_insn (REM(rs2, rs1, rd, s)) =
   let insn : string = if s then "rem   " else "remu  " in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
 
+mapping clause assembly = REM(rs2, rs1, rd, s) <-> "rem" ^ maybe_not_u(s) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 union clause ast = MULW : (regbits, regbits, regbits)
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(MULW(rs2, rs1, rd)) /* MULW */
+
+mapping clause encdec = MULW(rs2, rs1, rd) <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
+
 function clause execute (MULW(rs2, rs1, rd)) =
   let rs1_val = X(rs1)[31..0] in
   let rs2_val = X(rs2)[31..0] in
@@ -479,10 +641,13 @@ function clause execute (MULW(rs2, rs1, rd)) =
 function clause print_insn (MULW(rs2, rs1, rd)) =
   "mulw  " ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
 
+mapping clause assembly = MULW(rs2, rs1, rd) <->  "mulw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 union clause ast = DIVW : (regbits, regbits, regbits, bool)
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0111011 = Some(DIVW(rs2, rs1, rd,  true))  /* DIVW */
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(DIVW(rs2, rs1, rd, false))  /* DIVUW */
+
+mapping clause encdec = DIVW(rs2, rs1, rd, s) <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
+
 function clause execute (DIVW(rs2, rs1, rd, s)) =
   let rs1_val = X(rs1)[31..0] in
   let rs2_val = X(rs2)[31..0] in
@@ -498,10 +663,13 @@ function clause print_insn (DIVW(rs2, rs1, rd, s)) =
   let insn : string = if s then "divw  " else "divuw " in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
 
+mapping clause assembly = DIVW(rs2, rs1, rd, s) <-> "div" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 union clause ast = REMW : (regbits, regbits, regbits, bool)
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0111011 = Some(REMW(rs2, rs1, rd,  true))  /* REMW */
-function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0111011 = Some(REMW(rs2, rs1, rd, false))  /* REMUW */
+
+mapping clause encdec = REMW(rs2, rs1, rd, s) <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011
+
 function clause execute (REMW(rs2, rs1, rd, s)) =
   let rs1_val = X(rs1)[31..0] in
   let rs2_val = X(rs2)[31..0] in
@@ -517,10 +685,12 @@ function clause print_insn (REMW(rs2, rs1, rd, s)) =
   let insn : string = if s then "remw  " else "remuw " in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
 
+mapping clause assembly = REMW(rs2, rs1, rd, s) <-> "rem" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 union clause ast = FENCE : (bits(4), bits(4))
 
-function clause decode 0b0000 @ pred : bits(4) @ succ : bits(4) @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111 = Some(FENCE(pred, succ))
+mapping clause encdec = FENCE(pred, succ) <-> 0b0000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
 
 function clause execute (FENCE(pred, succ)) = {
   match (pred, succ) {
@@ -539,20 +709,48 @@ function clause execute (FENCE(pred, succ)) = {
 function clause print_insn (FENCE(pred, succ)) =
   "fence"
 
+mapping bit_maybe_r : bits(1) <-> string = {
+  0b1 <-> "r",
+  0b0 <-> ""
+}
+
+mapping bit_maybe_w : bits(1) <-> string = {
+  0b1 <-> "w",
+  0b0 <-> ""
+}
+
+mapping bit_maybe_i : bits(1) <-> string = {
+  0b1 <-> "i",
+  0b0 <-> ""
+}
+
+mapping bit_maybe_o : bits(1) <-> string = {
+  0b1 <-> "o",
+  0b0 <-> ""
+}
+
+mapping fence_bits : bits(4) <-> string = {
+  r : bits(1) @ w : bits(1) @ i : bits(1) @ o : bits(1) <-> bit_maybe_r(r) ^ bit_maybe_w(w) ^ bit_maybe_i(i) ^ bit_maybe_o(o)
+}
+
+mapping clause assembly = FENCE(pred, succ) <-> "fence" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ)
+
 /* ****************************************************************** */
 union clause ast = FENCEI : unit
 
-function clause decode 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 = Some(FENCEI())
+mapping clause encdec = FENCEI() <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111
 
 function clause execute FENCEI() = { MEM_fence_i(); true }
 
 function clause print_insn (FENCEI()) =
   "fence.i"
 
+mapping clause assembly = FENCEI() <-> "fence.i"
+
 /* ****************************************************************** */
 union clause ast = ECALL : unit
 
-function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(ECALL())
+mapping clause encdec = ECALL() <-> 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute ECALL() =
   let t : sync_exception =
@@ -569,10 +767,12 @@ function clause execute ECALL() =
 function clause print_insn (ECALL()) =
   "ecall"
 
+mapping clause assembly = ECALL() <-> "ecall"
+
 /* ****************************************************************** */
 union clause ast = MRET : unit
 
-function clause decode 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET())
+mapping clause encdec = MRET() <-> 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute MRET() = {
   if cur_privilege == Machine then
@@ -585,10 +785,12 @@ function clause execute MRET() = {
 function clause print_insn (MRET()) =
   "mret"
 
+mapping clause assembly = MRET() <-> "mret"
+
 /* ****************************************************************** */
 union clause ast = SRET : unit
 
-function clause decode 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(SRET())
+mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute SRET() = {
   match cur_privilege {
@@ -604,10 +806,12 @@ function clause execute SRET() = {
 function clause print_insn (SRET()) =
   "sret"
 
+mapping clause assembly = SRET() <-> "sret"
+
 /* ****************************************************************** */
 union clause ast = EBREAK : unit
 
-function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK())
+mapping clause encdec = EBREAK() <-> 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute EBREAK() = {
   handle_mem_exception(PC, E_Breakpoint);
@@ -617,10 +821,12 @@ function clause execute EBREAK() = {
 function clause print_insn (EBREAK()) =
   "ebreak"
 
+mapping clause assembly = EBREAK() <-> "ebreak"
+
 /* ****************************************************************** */
 union clause ast = WFI : unit
 
-function clause decode 0b000100000101 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(WFI())
+mapping clause encdec = WFI() <-> 0b000100000101 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute WFI() = {
   match cur_privilege {
@@ -637,10 +843,12 @@ function clause execute WFI() = {
 function clause print_insn (WFI()) =
   "wfi"
 
+mapping clause assembly = WFI() <-> "wfi"
+
 /* ****************************************************************** */
 union clause ast = SFENCE_VMA : (regbits, regbits)
 
-function clause decode 0b0001001 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ 0b00000 @ 0b1110011 = Some(SFENCE_VMA(rs1, rs2))
+mapping clause encdec = SFENCE_VMA(rs1, rs2) <-> 0b0001001 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute SFENCE_VMA(rs1, rs2) = {
   /* FIXME: spec leaves unspecified what happens if this is executed in M-mode.
@@ -662,11 +870,12 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
 function clause print_insn (SFENCE_VMA(rs1, rs2)) =
   "sfence.vma " ^ rs1 ^ ", " ^ rs2
 
+mapping clause assembly = SFENCE_VMA(rs1, rs2) <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits)
 
-function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, WORD, rd))
-function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, DOUBLE, rd))
+mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111
 
 val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit
 
@@ -692,11 +901,12 @@ function clause print_insn (LOADRES(aq, rl, rs1, width, rd)) =
     } in
   insn ^ rd ^ ", " ^ rs1
 
+mapping clause assembly = LOADRES(aq, rl, rs1, size, rd) <-> "lr." ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
+
 /* ****************************************************************** */
 union clause ast = STORECON : (bool, bool, regbits, regbits, word_width, regbits)
 
-function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(STORECON(aq, rl, rs2, rs1, WORD, rd))
-function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd))
+mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111
 
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
@@ -744,27 +954,24 @@ function clause print_insn (STORECON(aq, rl, rs2, rs1, width, rd)) =
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
 
+mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd) <-> "sc." ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 union clause ast = AMO : (amoop, bool, bool, regbits, regbits, word_width, regbits)
 
-function clause decode 0b00001 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD,   rd))
-function clause decode 0b00001 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode 0b00000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode 0b00000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode 0b00100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode 0b00100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode 0b01100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode 0b01100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode 0b01000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOOR  , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode 0b01000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOOR  , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode 0b10000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode 0b10000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode 0b10100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode 0b10100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode 0b11000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD,   rd))
-function clause decode 0b11000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD,   rd))
-function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd))
+mapping encdec_amoop : amoop <-> bits(5) = {
+  AMOSWAP <-> 0b00001,
+  AMOADD  <-> 0b00000,
+  AMOXOR  <-> 0b00100,
+  AMOAND  <-> 0b01100,
+  AMOOR   <-> 0b01000,
+  AMOMIN  <-> 0b10000,
+  AMOMAX  <-> 0b10100,
+  AMOMINU <-> 0b11000,
+  AMOMAXU <-> 0b11100
+}
+
+mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111
 
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
@@ -847,15 +1054,30 @@ function clause print_insn (AMO(op, aq, rl, rs2, rs1, width, rd)) =
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
 
+mapping amo_mnemonic : amoop <-> string = {
+  AMOSWAP <-> "amoswap",
+  AMOADD  <-> "amoadd",
+  AMOXOR  <-> "amoxor",
+  AMOAND  <-> "amoand",
+  AMOOR   <-> "amoor",
+  AMOMIN  <-> "amomin",
+  AMOMAX  <-> "amomax",
+  AMOMINU <-> "amominu",
+  AMOMAXU <-> "amomaxu"
+}
+
+mapping clause assembly = AMO(op, aq, rl, rs2, rs1, width, rd) <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
 /* ****************************************************************** */
 union clause ast = CSR  : (bits(12), regbits, regbits, bool, csrop)
 
-function clause decode csr : bits(12) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, false, CSRRW))
-function clause decode csr : bits(12) @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, false, CSRRS))
-function clause decode csr : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, false, CSRRC))
-function clause decode csr : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRW))
-function clause decode csr : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRS))
-function clause decode csr : bits(12) @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRC))
+mapping encdec_csrop : csrop <-> bits(2) = {
+  CSRRW <-> 0b01,
+  CSRRS <-> 0b10,
+  CSRRC <-> 0b11
+}
+
+mapping clause encdec = CSR(csr, rs1, rd, is_imm, op) <-> csr @ rs1 @ bool_bits(is_imm) @ encdec_csrop(op) @ rd @ 0b1110011
 
 function readCSR csr : csreg -> xlenbits =
   match csr {
@@ -983,6 +1205,20 @@ function clause print_insn (CSR(csr, rs1, rd, is_imm, op)) =
   let rs1_str : string = if is_imm then BitStr(rs1) else reg_name_abi(rs1) in
   insn ^ rd ^ ", " ^ rs1_str ^ ", " ^ csr_name(csr)
 
+mapping maybe_i : bool <-> string = {
+  true  <-> "i",
+  false <-> ""
+}
+
+mapping csr_mnemonic : csrop <-> string = {
+  CSRRW <-> "csrrw",
+  CSRRS <-> "csrrs",
+  CSRRC <-> "csrrc"
+}
+
+mapping clause assembly = CSR(csr, rs1, rd, true, op) <-> csr_mnemonic(op) ^ "i" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(rs1) ^ sep() ^ csr_name_map(csr)
+mapping clause assembly = CSR(csr, rs1, rd, false, op) <-> csr_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ csr_name_map(csr)
+
 /* ****************************************************************** */
 union clause ast = NOP : unit
 
@@ -997,16 +1233,7 @@ function clause print_insn (NOP()) =
   "nop"
 
 /* ****************************************************************** */
-union clause ast = ILLEGAL : unit
-
-function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16) = Some(ILLEGAL())
-
-function clause execute ILLEGAL() = { handle_illegal(); false }
 
-function clause print_insn (ILLEGAL()) =
-  "illegal"
-
-/* ****************************************************************** */
 union clause ast = C_ADDI4SPN : (cregbits, bits(8))
 
 function clause decodeCompressed (0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregbits @ 0b00) : bits(16) = {
@@ -1507,11 +1734,39 @@ function clause print_insn (C_ADD(rsd, rs2)) =
 
 /* ****************************************************************** */
 
-function clause decode _ = None()
+union clause ast = ILLEGAL : word
+
+mapping clause encdec = ILLEGAL(s) <-> s
+
+function clause execute (ILLEGAL(s)) = { handle_illegal(); false }
+
+function clause print_insn (ILLEGAL(s)) = "illegal " ^ hex_bits_32(s)
+
+mapping clause assembly = ILLEGAL(s) <-> "illegal" ^ spc() ^ hex_bits_32(s)
+
+
+
+/* ****************************************************************** */
+
+union clause ast = C_ILLEGAL : unit
+
+function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16) = Some(C_ILLEGAL())
+
+function clause execute C_ILLEGAL() = { handle_illegal(); false }
+
+function clause print_insn (C_ILLEGAL()) =
+  "c.illegal"
+
+/* ****************************************************************** */
+
+
 function clause decodeCompressed _ = None()
 
 end ast
-end decode
 end decodeCompressed
 end execute
 end print_insn
+end assembly
+end encdec
+
+function decode bv = Some(encdec(bv))
\ No newline at end of file
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 8af1155a..9373701c 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -519,6 +519,69 @@ function csr_name(csr) = {
   }
 }
 
+mapping csr_name_map : csreg <-> string = {
+    /* user trap setup */
+    0x000  <-> "ustatus",
+    0x004  <-> "uie",
+    0x005  <-> "utvec",
+    /* user floating-point context */
+    0x001  <-> "fflags",
+    0x002  <-> "frm",
+    0x003  <-> "fcsr",
+    /* counter/timers */
+    0xC00  <-> "cycle",
+    0xC01  <-> "time",
+    0xC02  <-> "instret",
+    0xC80  <-> "cycleh",
+    0xC81  <-> "timeh",
+    0xC82  <-> "instreth",
+    /* TODO: other hpm counters */
+    /* supervisor trap setup */
+    0x100  <-> "sstatus",
+    0x102  <-> "sedeleg",
+    0x103  <-> "sideleg",
+    0x104  <-> "sie",
+    0x105  <-> "stvec",
+    0x106  <-> "scounteren",
+    /* supervisor trap handling */
+    0x140  <-> "sscratch",
+    0x141  <-> "sepc",
+    0x142  <-> "scause",
+    0x143  <-> "stval",
+    0x144  <-> "sip",
+    /* supervisor protection and translation */
+    0x180  <-> "satp",
+    /* machine information registers */
+    0xF11  <-> "mvendorid",
+    0xF12  <-> "marchid",
+    0xF13  <-> "mimpid",
+    0xF14  <-> "mhartid",
+    /* machine trap setup */
+    0x300  <-> "mstatus",
+    0x301  <-> "misa",
+    0x302  <-> "medeleg",
+    0x303  <-> "mideleg",
+    0x304  <-> "mie",
+    0x305  <-> "mtvec",
+    0x306  <-> "mcounteren",
+    /* machine trap handling */
+    0x340  <-> "mscratch",
+    0x341  <-> "mepc",
+    0x342  <-> "mcause",
+    0x343  <-> "mtval",
+    0x344  <-> "mip",
+    /* TODO: machine protection and translation */
+    /* machine counters/timers */
+    0xB00  <-> "mcycle",
+    0xB02  <-> "minstret",
+    0xB80  <-> "mcycleh",
+    0xB82  <-> "minstreth",
+    /* TODO: other hpm counters and events */
+    /* trigger/debug */
+    0x7a0  <-> "tselect"
+ }
+
+
 /* csr access control */
 
 function csrAccess(csr : csreg) -> csrRW = csr[11..10]
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 1a79670b..42042293 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -327,3 +327,71 @@ enum ropw = {RISCV_ADDW, RISCV_SUBW, RISCV_SLLW, RISCV_SRLW, RISCV_SRAW} /* reg-
 enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */
 enum csrop = {CSRRW, CSRRS, CSRRC}
 enum word_width = {BYTE, HALF, WORD, DOUBLE}
+
+/* mappings for assembly */
+
+val reg_name : bits(5) <-> string
+mapping reg_name = {
+    0b00000 <-> "zero",
+    0b00001 <-> "ra",
+    0b00010 <-> "sp",
+    0b00011 <-> "gp",
+    0b00100 <-> "tp",
+    0b00101 <-> "t0",
+    0b00110 <-> "t1",
+    0b00111 <-> "t2",
+    0b01000 <-> "fp",
+    0b01001 <-> "s1",
+    0b01010 <-> "a0",
+    0b01011 <-> "a1",
+    0b01100 <-> "a2",
+    0b01101 <-> "a3",
+    0b01110 <-> "a4",
+    0b01111 <-> "a5",
+    0b10000 <-> "a6",
+    0b10001 <-> "a7",
+    0b10010 <-> "s2",
+    0b10011 <-> "s3",
+    0b10100 <-> "s4",
+    0b10101 <-> "s5",
+    0b10110 <-> "s6",
+    0b10111 <-> "s7",
+    0b11000 <-> "s8",
+    0b11001 <-> "s9",
+    0b11010 <-> "s10",
+    0b11011 <-> "s11",
+    0b11100 <-> "t3",
+    0b11101 <-> "t4",
+    0b11110 <-> "t5",
+    0b11111 <-> "t6"
+}
+
+val sep : unit <-> string
+mapping sep = {
+  () <-> opt_spc() ^ "," ^ def_spc()
+}
+
+mapping bool_bits : bool <-> bits(1) = {
+  true <-> 0b1,
+  false <-> 0b0
+}
+
+mapping bool_not_bits : bool <-> bits(1) = {
+  true <-> 0b0,
+  false <-> 0b1
+}
+
+
+mapping size_bits : word_width <-> bits(2) = {
+  BYTE <-> 0b00,
+  HALF <-> 0b01,
+  WORD <-> 0b10,
+  DOUBLE <-> 0b11
+}
+
+mapping size_mnemonic : word_width <-> string = {
+  BYTE <-> "b",
+  HALF <-> "h",
+  WORD <-> "w",
+  DOUBLE <-> "d"
+}