Merge branch 'sail2' into rmem_interpreter

57 files changed, 1356 insertions, 284 deletions

diff --git a/.gitignore b/.gitignore
index b4535aba..eac3db42 100644
--- a/.gitignore
+++ b/.gitignore
@@ -92,8 +92,10 @@ lib/hol/sail-heap
 /riscv/riscv
 /riscv/platform
 /riscv/riscv.c
+/riscv/riscv_model.c
 /riscv/riscv_c
 /riscv/z3_problems
+/riscv/riscv_sim
 
 /x86/x86.lem
 /x86/x86.ml
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index 05d3eb60..de8c3d11 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -9,7 +9,7 @@
     "overload" "cast" "sizeof" "constraint" "default" "assert" "newtype" "from"
     "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to"
     "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield"
-    "mapping"))
+    "mapping" "where"))
 
 (defconst sail2-kinds
   '("Int" "Type" "Order" "inc" "dec"
diff --git a/language/sail.ott b/language/sail.ott
index 2edffcbe..59d51d68 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -293,6 +293,7 @@ n_constraint :: 'NC_' ::=
   | kid 'IN' { num1 , ... , numn }              :: :: set
   | n_constraint \/ n_constraint'               :: :: or
   | n_constraint /\ n_constraint'               :: :: and
+  | id ( nexp1 , ... , nexpn )                  :: :: app
   | true                                        :: :: true
   | false                                       :: :: false
 
@@ -1012,29 +1013,30 @@ prec :: '' ::=
 def :: 'DEF_' ::=
   {{ com top-level definition }}
   {{ auxparam 'a }}
-  | kind_def                                         :: :: kind
+  | kind_def                                           :: :: kind
     {{ com definition of named kind identifiers }}
-  | type_def                                         :: :: type
+  | type_def                                           :: :: type
     {{ com type definition }}
-  | fundef                                           :: :: fundef
+  | fundef                                             :: :: fundef
     {{ com function definition }}
-  | mapdef                                           :: :: mapdef
+  | mapdef                                             :: :: mapdef
     {{ com mapping definition }}
-  | letbind                                          :: :: val
+  | letbind                                            :: :: val
     {{ com value definition }}
-  | val_spec                                         :: :: spec
+  | val_spec                                           :: :: spec
     {{ com top-level type constraint }}
-  | fix prec num id                                  :: :: fixity
+  | fix prec num id                                    :: :: fixity
     {{ com fixity declaration }}
-  |  overload id [ id1 ; ... ; idn ]                 :: :: overload
+  |  overload id [ id1 ; ... ; idn ]                   :: :: overload
     {{ com operator overload specification }}
-  | default_spec                                     :: :: default
+  | default_spec                                       :: :: default
     {{ com default kind and type assumptions }}
-  | scattered_def                                    :: :: scattered
+  | scattered_def                                      :: :: scattered
     {{ com scattered function and type definition }}
-  | dec_spec                                         :: :: reg_dec
+  | dec_spec                                           :: :: reg_dec
     {{ com register declaration }}
-  | fundef1 .. fundefn                               :: I :: internal_mutrec
+  | constraint id ( kid1 , ... , kidn ) = n_constraint :: :: constraint
+  | fundef1 .. fundefn                                 :: I :: internal_mutrec
     {{ com internal representation of mutually recursive functions }}
 
 defs :: '' ::=
diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index 0a63ff2c..a02556b2 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -11,6 +11,10 @@ Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) :=
   let n := Z.to_nat (projT1 n) in
   String.substring n (String.length s - n) s.
 
+Definition string_take s (n : {n : Z & ArithFact (n >= 0)}) :=
+  let n := Z.to_nat (projT1 n) in
+  String.substring 0 n s.
+
 Definition string_length s : {n : Z & ArithFact (n >= 0)} :=
  build_ex (Z.of_nat (String.length s)).
 
diff --git a/lib/elf.c b/lib/elf.c
index 8c5c5f56..4355b44c 100644
--- a/lib/elf.c
+++ b/lib/elf.c
@@ -103,6 +103,7 @@ uint64_t rev64(uint64_t x) {
 #define PT_LOAD         1  /* Loadable segment */
 
 #define SHT_SYMTAB      2  /* Symbol table type */
+#define SHT_STRTAB      3  /* String table type */
 
 /* How to extract and insert information held in the st_info field.  */
 
@@ -306,7 +307,7 @@ void loadProgHdr64(bool le, const char* buffer, Elf64_Off off, const int total_f
     }
 }
 
-void loadELFHdr(const char* buffer, const int total_file_size) {
+void checkELFHdr(const char* buffer, const int total_file_size) {
     if (total_file_size < sizeof(Elf32_Ehdr)) {
         fprintf(stderr, "File too small, not big enough even for 32-bit ELF header\n");
         exit(EXIT_FAILURE);
@@ -319,7 +320,6 @@ void loadELFHdr(const char* buffer, const int total_file_size) {
         fprintf(stderr, "Invalid ELF magic bytes. Not an ELF file?\n");
         exit(EXIT_FAILURE);
     }
-
     if (hdr->e_ident[EI_CLASS] == ELFCLASS32) {
         bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
         Elf32_Ehdr *ehdr = (Elf32_Ehdr*) &buffer[0];
@@ -329,12 +329,6 @@ void loadELFHdr(const char* buffer, const int total_file_size) {
             fprintf(stderr, "Invalid ELF type or machine for class (32-bit)\n");
             exit(EXIT_FAILURE);
         }
-
-	for(int i = 0; i < rdHalf32(le, ehdr->e_phnum); ++i) {
-	  loadProgHdr32(le, buffer, rdOff32(le, ehdr->e_phoff) + i * rdHalf32(le, ehdr->e_phentsize), total_file_size);
-	}
-
-	return;
     } else if (hdr->e_ident[EI_CLASS] == ELFCLASS64) {
         if (total_file_size < sizeof(Elf64_Ehdr)) {
             fprintf(stderr, "File too small, specifies 64-bit ELF but not big enough for 64-bit ELF header\n");
@@ -348,19 +342,39 @@ void loadELFHdr(const char* buffer, const int total_file_size) {
             fprintf(stderr, "Invalid ELF type or machine for class (64-bit)\n");
             exit(EXIT_FAILURE);
         }
+    } else {
+        fprintf(stderr, "Unrecognized ELF file format\n");
+        exit(EXIT_FAILURE);
+    }
+}
+
+void loadELFHdr(const char* buffer, const int total_file_size, bool *is32bit_p, uint64_t *entry) {
+    checkELFHdr(buffer, total_file_size);
 
+    Elf32_Ehdr *hdr = (Elf32_Ehdr*) &buffer[0];
+    if (hdr->e_ident[EI_CLASS] == ELFCLASS32) {
+        bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
+        Elf32_Ehdr *ehdr = (Elf32_Ehdr*) &buffer[0];
+	for(int i = 0; i < rdHalf32(le, ehdr->e_phnum); ++i) {
+	  loadProgHdr32(le, buffer, rdOff32(le, ehdr->e_phoff) + i * rdHalf32(le, ehdr->e_phentsize), total_file_size);
+	}
+        if (is32bit_p) *is32bit_p = true;
+        if (entry) *entry = (uint64_t) ehdr->e_entry;
+    } else if (hdr->e_ident[EI_CLASS] == ELFCLASS64) {
+        bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
+        Elf64_Ehdr *ehdr = (Elf64_Ehdr*) &buffer[0];
 	for(int i = 0; i < rdHalf64(le, ehdr->e_phnum); ++i) {
 	  loadProgHdr64(le, buffer, rdOff64(le, ehdr->e_phoff) + i * rdHalf64(le, ehdr->e_phentsize), total_file_size);
 	}
-
-	return;
+        if (is32bit_p) *is32bit_p = false;
+        if (entry) *entry = ehdr->e_entry;
     } else {
         fprintf(stderr, "Unrecognized ELF file format\n");
         exit(EXIT_FAILURE);
     }
 }
 
-void load_elf(char *filename) {
+void load_elf(char *filename, bool *is32bit_p, uint64_t *entry) {
     // Read input file into memory
     char* buffer = NULL;
     int   size   = 0;
@@ -377,8 +391,7 @@ void load_elf(char *filename) {
         if (s < 0) { goto fail; }
         read += s;
     }
-
-    loadELFHdr(buffer, read);
+    loadELFHdr(buffer, read, is32bit_p, entry);
     free(buffer);
     return;
 
@@ -387,6 +400,159 @@ fail:
     exit(EXIT_FAILURE);
 }
 
+// symbol lookup for very simple ELF files (single symtab, two strtabs): looks up a
+// single symbol at a time, but avoids retaining memory.
+
+int lookupSymbol(const char *buffer, const int total_file_size, const char *symname, uint64_t *value) {
+    checkELFHdr(buffer, total_file_size);
+    Elf32_Ehdr *hdr = (Elf32_Ehdr*) &buffer[0];
+    if (hdr->e_ident[EI_CLASS] == ELFCLASS32) {
+        bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
+        Elf32_Ehdr *ehdr = (Elf32_Ehdr*) &buffer[0];
+        if (total_file_size < rdOff32(le, ehdr->e_shoff)
+                              + rdHalf32(le, ehdr->e_shnum)*sizeof(Elf32_Shdr)) {
+            fprintf(stderr, "File too small for %d sections from offset %d\n",
+                    rdHalf32(le, ehdr->e_shnum), rdOff32(le, ehdr->e_shoff));
+            exit(EXIT_FAILURE);
+        }
+        if (rdHalf32(le, ehdr->e_shtrndx) >= rdHalf32(le, ehdr->e_shnum)) {
+            fprintf(stderr, "Invalid string section table index %d\n", hdr->e_shtrndx);
+            exit(EXIT_FAILURE);
+        }
+        Elf32_Shdr *shdr = (Elf32_Shdr *)&buffer[ehdr->e_shoff];
+        Elf32_Shdr *shstrtab = (Elf32_Shdr *)&shdr[rdHalf32(le, ehdr->e_shtrndx)];
+        if (total_file_size < rdOff32(le, shstrtab->sh_offset) + rdWord32(le, shstrtab->sh_size)) {
+            fprintf(stderr, "File too small for string section\n");
+            exit(EXIT_FAILURE);
+        }
+        const char *shstrbuf = buffer + rdOff32(le, shstrtab->sh_offset);
+        Elf32_Word strtabidx = 0, symtabidx = 0;
+        for (Elf32_Word i = 0; i < rdHalf32(le, ehdr->e_shnum); i++) {
+            if (rdWord32(le, shdr[i].sh_type) == SHT_SYMTAB) {
+                symtabidx = i;
+            }
+            if (rdWord32(le, shdr[i].sh_type) == SHT_STRTAB) {
+                // skip section name string table
+                if (i != rdHalf32(le, ehdr->e_shtrndx)) {
+                    strtabidx = i;
+                }
+            }
+        }
+        if (!strtabidx || !symtabidx) {
+            fprintf(stderr, "ELF: unable to find string or symbol table\n");
+            return -1;
+        }
+        const char *strtab = buffer + rdOff32(le, shdr[strtabidx].sh_offset);
+        Elf32_Word strtab_size = rdWord32(le, shdr[strtabidx].sh_size);
+        Elf32_Sym *sym_ent = (Elf32_Sym *)(buffer + rdOff32(le, shdr[symtabidx].sh_offset));
+        for (Elf32_Word i = 0; i < rdWord32(le, shdr[symtabidx].sh_size)/sizeof(*sym_ent); i++) {
+            Elf32_Word sidx = rdWord32(le, sym_ent[i].st_name);
+            if (sidx >= strtab_size) {
+                fprintf(stderr, "Symbol name index out of bounds\n");
+                exit(EXIT_FAILURE);
+            }
+            Elf32_Word max_len = strtab_size - sidx;
+            const char *sname = strtab + sidx;
+            if (strnlen(sname, max_len) >= max_len) {
+                fprintf(stderr, "Unterminated symbol name\n");
+                exit(EXIT_FAILURE);
+            }
+            if (!strcmp(sname, symname)) {
+                if (value) *value = (uint64_t) rdAddr32(le, sym_ent[i].st_value);
+                return 0;
+            }
+        }
+        return -1;
+    } else if (hdr->e_ident[EI_CLASS] == ELFCLASS64) {
+        bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
+        Elf64_Ehdr *ehdr = (Elf64_Ehdr*) &buffer[0];
+        if (total_file_size < rdOff64(le, ehdr->e_shoff)
+                              + rdHalf64(le, ehdr->e_shnum)*sizeof(Elf64_Shdr)) {
+            fprintf(stderr, "File too small for %d sections from offset %ld\n",
+                    rdHalf64(le, ehdr->e_shnum), rdOff64(le, ehdr->e_shoff));
+            exit(EXIT_FAILURE);
+        }
+        if (rdHalf64(le, ehdr->e_shtrndx) >= rdHalf64(le, ehdr->e_shnum)) {
+            fprintf(stderr, "Invalid string section table index %d\n", hdr->e_shtrndx);
+            exit(EXIT_FAILURE);
+        }
+        Elf64_Shdr *shdr = (Elf64_Shdr *)&buffer[ehdr->e_shoff];
+        Elf64_Shdr *shstrtab = (Elf64_Shdr *)&shdr[rdHalf64(le, ehdr->e_shtrndx)];
+        if (total_file_size < rdOff64(le, shstrtab->sh_offset) + rdWord64(le, shstrtab->sh_size)) {
+            fprintf(stderr, "File too small for string section\n");
+            exit(EXIT_FAILURE);
+        }
+        const char *shstrbuf = buffer + rdOff64(le, shstrtab->sh_offset);
+        Elf64_Word strtabidx = 0, symtabidx = 0;
+        for (Elf64_Word i = 0; i < rdHalf64(le, ehdr->e_shnum); i++) {
+            if (rdWord64(le, shdr[i].sh_type) == SHT_SYMTAB) {
+                symtabidx = i;
+            }
+            if (rdWord64(le, shdr[i].sh_type) == SHT_STRTAB) {
+                // skip section name string table
+                if (i != rdHalf64(le, ehdr->e_shtrndx)) {
+                    strtabidx = i;
+                }
+            }
+        }
+        if (!strtabidx || !symtabidx) {
+            fprintf(stderr, "ELF: unable to find string or symbol table\n");
+            return -1;
+        }
+        const char *strtab = buffer + rdOff64(le, shdr[strtabidx].sh_offset);
+        Elf64_Xword strtab_size = rdXword64(le, shdr[strtabidx].sh_size);
+        Elf64_Sym *sym_ent = (Elf64_Sym *)(buffer + rdOff64(le, shdr[symtabidx].sh_offset));
+        for (Elf64_Xword i = 0; i < rdXword64(le, shdr[symtabidx].sh_size)/sizeof(*sym_ent); i++) {
+            Elf64_Word sidx = rdWord64(le, sym_ent[i].st_name);
+            if (sidx >= strtab_size) {
+                fprintf(stderr, "Symbol name index out of bounds\n");
+                exit(EXIT_FAILURE);
+            }
+            Elf64_Word max_len = strtab_size - sidx;
+            const char *sname = strtab + sidx;
+            if (strnlen(sname, max_len) >= max_len) {
+                fprintf(stderr, "Unterminated symbol name\n");
+                exit(EXIT_FAILURE);
+            }
+            if (!strcmp(sname, symname)) {
+                if (value) *value = (uint64_t) rdAddr64(le, sym_ent[i].st_value);
+                return 0;
+            }
+        }
+        return -1;
+    } else {
+        fprintf(stderr, "Unrecognized ELF file format\n");
+        exit(EXIT_FAILURE);
+    }
+}
+
+int lookup_sym(const char *filename, const char *symname, uint64_t *value) {
+    // Read input file into memory
+    char* buffer = NULL;
+    int   size   = 0;
+    int   chunk  = (1<<24); // increments output buffer this much
+    int   read   = 0;
+    int   ret    = 0;
+    gzFile in = gzopen(filename, "rb");
+    if (in == NULL) { goto fail; }
+    while (!gzeof(in)) {
+        size = read + chunk;
+        buffer = (char*)realloc(buffer, size);
+        if (buffer == NULL) { goto fail; }
+
+        int s = gzread(in, buffer+read, size - read);
+        if (s < 0) { goto fail; }
+        read += s;
+    }
+    ret = lookupSymbol(buffer, read, symname, value);
+    free(buffer);
+    return ret;
+
+fail:
+    fprintf(stderr, "Unable to read file %s\n", filename);
+    exit(EXIT_FAILURE);
+}
+
 ////////////////////////////////////////////////////////////////
 // ELF Loader
 ////////////////////////////////////////////////////////////////
diff --git a/lib/elf.h b/lib/elf.h
index e5f90365..6f592afd 100644
--- a/lib/elf.h
+++ b/lib/elf.h
@@ -1,5 +1,8 @@
 #pragma once
 
 #include<string.h>
+#include<stdbool.h>
+#include<stdint.h>
 
-void load_elf(char *filename);
+void load_elf(char *filename, bool *is32bit_p, uint64_t *entry);
+int  lookup_sym(const char *filename, const char *symname, uint64_t *value);
diff --git a/lib/rts.c b/lib/rts.c
index 1be10137..6bd97934 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -520,7 +520,7 @@ int process_arguments(int argc, char *argv[])
       break;
 
     case 'e':
-      load_elf(optarg);
+      load_elf(optarg, NULL, NULL);
       break;
 
     case 'n':
diff --git a/riscv/Makefile b/riscv/Makefile
index 73bd01c0..e6bbbd5c 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,10 +1,36 @@
-SAIL_SRCS = riscv_all.sail
+SAIL_SEQ_INST  = riscv.sail riscv_jalr_seq.sail
+SAIL_RMEM_INST = riscv.sail riscv_jalr_rmem.sail
+
+SAIL_SEQ_INST_SRCS  = riscv_insts_begin.sail $(SAIL_SEQ_INST) riscv_insts_end.sail
+SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.sail
+
+# non-instruction sources
+SAIL_OTHER_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail
+
+SAIL_SRCS      = $(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS)  riscv_step.sail riscv_analysis.sail
+SAIL_RMEM_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_RMEM_INST_SRCS) riscv_step.sail riscv_analysis.sail
+
 PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
 SAIL_DIR ?= $(realpath ..)
 SAIL ?= $(SAIL_DIR)/sail
 C_WARNINGS ?=
 #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
-C_SRCS = riscv_prelude.c riscv_platform.c
+C_FLAGS = -I ../lib
+C_INCS = riscv_prelude.h riscv_platform_impl.h riscv_platform.h
+C_SRCS = riscv_prelude.c riscv_platform_impl.c riscv_platform.c
+
+ENABLE_SPIKE = 0
+TV_SPIKE_DIR = /home/mundkur/src/hw/l3/l3riscv
+SPIKE_FLAGS = -I $(TV_SPIKE_DIR)/src/cpp
+SPIKE_LIBS  = -L $(TV_SPIKE_DIR) -ltv_spike -Wl,-rpath=$(TV_SPIKE_DIR)
+SPIKE_LIBS += -L $(RISCV)/lib -lfesvr -lriscv -Wl,-rpath=$(RISCV)/lib
+
+C_LIBS = -lgmp -lz
+
+ifeq ($(ENABLE_SPIKE),1)
+C_FLAGS += $(SPIKE_FLAGS)
+C_LIBS  += $(SPIKE_LIBS)
+endif
 
 export SAIL_DIR
 
@@ -38,9 +64,15 @@ coverage: _sbuild/coverage.native
 riscv.c: $(SAIL_SRCS) main.sail Makefile
 	$(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) main.sail 1> $@
 
-riscv_c: riscv.c riscv_prelude.h $(C_SRCS) Makefile
+riscv_c: riscv.c $(C_INCS) $(C_SRCS) Makefile
 	gcc $(C_WARNINGS) -O2 riscv.c $(C_SRCS) ../lib/*.c -lgmp -lz -I ../lib -o riscv_c
 
+riscv_model.c: $(SAIL_SRCS) main.sail Makefile
+	$(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) main.sail 1> $@
+
+riscv_sim: riscv_model.c riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile
+	gcc -g $(C_WARNINGS) $(C_FLAGS) -O2 riscv_model.c riscv_sim.c $(C_SRCS) ../lib/*.c $(C_LIBS) -o $@
+
 latex: $(SAIL_SRCS) Makefile
 	$(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS)
 
@@ -108,6 +140,6 @@ clean:
 	-rm -f platform_main.native platform coverage.native
 	-rm -f riscv.vo riscv_types.vo riscv_extras.vo riscv.v riscv_types.v
 	-rm -f riscv_duopod.vo riscv_duopod_types.vo riscv_duopod.v riscv_duopod_types.v
-	-rm -f riscv.c
+	-rm -f riscv.c riscv_model.c riscv_sim
 	-Holmake cleanAll
 	ocamlbuild -clean
diff --git a/riscv/README b/riscv/README
new file mode 100644
index 00000000..b925821e
--- /dev/null
+++ b/riscv/README
@@ -0,0 +1,23 @@
+Booting Linux with the C backend:
+---------------------------------
+
+The C model needs an ELF-version of the BBL (Berkeley-Boot-Loader) that contains
+the Linux kernel as an embedded payload.  It also needs a DTB (device-tree blob)
+file describing the platform.  Once those are available, the model should be run
+as:
+
+$ ./riscv_sim -b spike.dtb bbl > execution-trace.log 2>&1 &
+$ tail -f term.log
+
+The term.log file contains the console boot messages.
+
+
+Booting Linux with the OCaml backend:
+-------------------------------------
+
+The OCaml model only needs the ELF-version of the BBL, since it can generate its
+own DTB.
+
+$ ./platform bbl > execution-trace.log
+
+The console output is sent to stderr.
diff --git a/riscv/coq.patch b/riscv/coq.patch
index 2dc1b4aa..6c40e6e2 100644
--- a/riscv/coq.patch
+++ b/riscv/coq.patch
@@ -1,6 +1,34 @@
---- riscv.v	2018-10-01 18:21:50.121189040 +0100
-+++ riscv.v.good	2018-10-01 18:21:24.485040512 +0100
-@@ -10537,14 +10537,13 @@
+--- riscv.v	2018-10-22 18:20:01.512785981 +0100
++++ riscv.v.good	2018-10-22 18:19:27.556562080 +0100
+@@ -1260,6 +1260,9 @@
+    let v64 : bits 64 := EXTS 64 v in
+    subrange_vec_dec (shift_bits_right v64 shift) 31 0.
+ 
++Definition n_leading_spaces s : {n : Z & ArithFact (n >= 0)} :=
++ build_ex (Z.of_nat (n_leading_spaces s)).
++(*
+ Fixpoint n_leading_spaces (s : string) 
+ : {n : Z & ArithFact (n >= 0)} :=
+    build_ex(let p0_ := s in
+@@ -1273,7 +1276,7 @@
+                                                                              (string_drop s
+                                                                                 (build_ex 1)))))))
+                   : {n : Z & ArithFact (n >= 0)}))))
+-     else 0).
++     else 0).*)
+ 
+ Definition spc_forwards '(tt : unit)  : string := " ".
+ 
+@@ -1284,7 +1287,7 @@
+    let 'n := projT1 (n_leading_spaces s) in
+    let p0_ := n in
+    if sumbool_of_bool ((Z.eqb p0_ 0)) then None
+-   else Some ((tt, n)).
++   else Some ((tt, build_ex n)).
+ 
+ Definition opt_spc_forwards '(tt : unit)  : string := "".
+ 
+@@ -10432,14 +10435,13 @@
     returnm ((EXTZ 56 (shiftl (_get_Satp64_PPN satp64) PAGESIZE_BITS))
      : mword 56).
  
@@ -17,7 +45,7 @@
               (projT1 (sub_range (build_ex SV39_LEVEL_BITS) (build_ex 1))) 0)) PTE39_LOG_SIZE in
     let pte_addr := add_vec ptb pt_ofs in
     (phys_mem_read Data (EXTZ 64 pte_addr) 8 false false false) >>= fun w__0 : MemoryOpResult (mword (8 * 8)) =>
-@@ -10557,27 +10556,27 @@
+@@ -10452,27 +10454,27 @@
         let is_global := orb global (eq_vec (_get_PTE_Bits_G pattr) ((bool_to_bits true)  : mword 1)) in
         (if ((isInvalidPTE pbits)) then returnm ((PTW_Failure (PTW_Invalid_PTE))  : PTW_Result )
          else if ((isPTEPtr pbits)) then
@@ -51,7 +79,7 @@
                        if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask)
                               (EXTZ 44 (vec_of_bits [B0]  : mword 1)))) then
                          PTW_Failure
-@@ -10587,10 +10586,10 @@
+@@ -10482,10 +10484,10 @@
                            or_vec (_get_SV39_PTE_PPNi pte)
                              (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in
                          PTW_Success
@@ -64,7 +92,7 @@
             : PTW_Result))
          : M (PTW_Result)
      end)
-@@ -10716,7 +10715,7 @@
+@@ -10611,7 +10613,7 @@
          : M (TR39_Result)
      | None =>
         (curPTB39 tt) >>= fun w__6 : mword 56 =>
@@ -73,7 +101,7 @@
         (match w__7 with
          | PTW_Failure (f) => returnm ((TR39_Failure (f))  : TR39_Result )
          | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) =>
-@@ -15425,137 +15424,143 @@
+@@ -14651,137 +14653,144 @@
     returnm (true
      : bool).
  
@@ -274,32 +302,33 @@
 +: M (bool) :=
 +let merge_var := expand_ast merge_var in
 +   match merge_var with
++
     | UTYPE (imm,rd,op) => (execute_UTYPE imm rd op)  : M (bool)
     | RISCV_JAL (imm,rd) => (execute_RISCV_JAL imm rd)  : M (bool)
     | RISCV_JALR (imm,rs1,rd) => (execute_RISCV_JALR imm rs1 rd)  : M (bool)
-@@ -15595,6 +15600,7 @@
+@@ -14821,6 +14830,7 @@
     | THREAD_START (arg0) => returnm ((execute_THREAD_START arg0)  : bool)
     | ILLEGAL (s) => (execute_ILLEGAL s)  : M (bool)
-    | C_ILLEGAL (arg0) => (execute_C_ILLEGAL arg0)  : M (bool)
+    | C_ILLEGAL (s) => (execute_C_ILLEGAL s)  : M (bool)
 +| _ => Fail "Unexpanded instruction"
     end.
  
  Definition assembly_forwards (arg_ : ast) 
-@@ -27093,7 +27099,7 @@
-     else returnm (tt  : unit)) >>
+@@ -35792,7 +35802,7 @@
     returnm (stepped
      : bool).
--
-+(*
- Definition loop '(tt : unit) 
+ 
+-Definition loop '(tt : unit) 
++(*Definition loop '(tt : unit) 
  : M (unit) :=
     let insns_per_tick := plat_insns_per_tick tt in
-@@ -27135,7 +27141,7 @@
+    let i : Z := 0 in
+@@ -35832,7 +35842,7 @@
+            : M (Z)) >>= fun i : Z =>
         returnm (i, step_no))) >>= fun '(i, step_no) =>
     returnm (tt
-     : unit).
--
-+*)
+-    : unit).
++    : unit).*)
+ 
  Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} 
  : read_kind :=
-    let p0_ := arg_ in
diff --git a/riscv/platform.ml b/riscv/platform.ml
index f5324794..015d189b 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -56,6 +56,7 @@ module Elf = Elf_loader;;
 
 let config_enable_dirty_update = ref false
 let config_enable_misaligned_access = ref false
+let config_mtval_has_illegal_inst_bits = ref false
 
 (* Mapping to Sail externs *)
 
@@ -82,6 +83,7 @@ let make_rom start_pc =
 
 let enable_dirty_update () = !config_enable_dirty_update
 let enable_misaligned_access () = !config_enable_misaligned_access
+let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
 
 let rom_base () = bits_of_int64 P.rom_base
 let rom_size () = bits_of_int   !rom_size_ref
diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml
index e593dce9..c5cc3fff 100644
--- a/riscv/platform_impl.ml
+++ b/riscv/platform_impl.ml
@@ -159,7 +159,7 @@ let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *)
 (* Terminal I/O *)
 
 let term_write char =
-  ignore (Unix.write_substring Unix.stdout (String.make 1 char) 0 1)
+  ignore (Unix.write_substring Unix.stderr (String.make 1 char) 0 1)
 
 let rec term_read () =
   let buf = Bytes.make 1 '\000' in
diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml
index e204daee..b33247f1 100644
--- a/riscv/platform_main.ml
+++ b/riscv/platform_main.ml
@@ -73,6 +73,9 @@ let options = Arg.align ([("-dump-dts",
                           ("-enable-misaligned-access",
                            Arg.Set P.config_enable_misaligned_access,
                            " enable misaligned accesses without M-mode traps");
+                          ("-mtval-has-illegal-inst-bits",
+                           Arg.Set P.config_mtval_has_illegal_inst_bits,
+                           " mtval stores instruction bits on an illegal instruction exception");
                           ("-with-dtc",
                            Arg.String PI.set_dtc,
                            " full path to dtc to use")
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 1dc9ba8f..fa715f80 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -1,29 +1,3 @@
-/* Instruction definitions.
- *
- * This includes decoding, execution, and assembly parsing and printing.
- */
-
-scattered union ast
-
-val decode : bits(32) -> option(ast) effect pure
-
-val decodeCompressed : bits(16) -> option(ast) effect pure
-
-val cast print_insn : ast -> string
-
-/* returns whether an instruction was retired, used for computing minstret */
-val execute : ast -> bool effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
-scattered function execute
-
-val assembly : ast <-> string
-scattered mapping assembly
-
-val encdec : ast <-> bits(32)
-scattered mapping encdec
-
-val encdec_compressed : ast <-> bits(16)
-scattered mapping encdec_compressed
-
 /* ****************************************************************** */
 union clause ast = UTYPE : (bits(20), regbits, uop)
 
@@ -87,25 +61,11 @@ union clause ast = RISCV_JALR : (bits(12), regbits, regbits)
 
 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 */
-  X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
-  let newPC : xlenbits = X(rs1) + EXTS(imm);
-/*  RMEM FIXME: For the sequential model, the above definition doesn't work directly
-    if rs1 = rd.  We would effectively have to keep a regfile for reads and another for
-    writes, and swap on instruction fetch.  This could perhaps be optimized in
-    some manner, but for now, we just reorder the previous two lines to improve simulator
-    performance in the sequential model, as below:
-  let newPC : xlenbits = X(rs1) + EXTS(imm);
-  X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
-*/
-  nextPC = newPC[63..1] @ 0b0;
-  true
-}
-
 mapping clause assembly = RISCV_JALR(imm, rs1, rd)
                       <-> "jalr" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
 
+/* see riscv_jalr_seq.sail or riscv_jalr_rmem.sail for the execute clause. */
+
 /* ****************************************************************** */
 union clause ast = BTYPE : (bits(13), regbits, regbits, bop)
 
@@ -851,7 +811,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
        }
 
 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)
+                      <-> "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)
@@ -916,7 +876,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
   }
 }
 
-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)
+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)
@@ -1585,14 +1545,3 @@ function clause execute C_ILLEGAL(s) = { handle_illegal(); false }
 mapping clause assembly = C_ILLEGAL(s) <-> "c.illegal" ^ spc() ^ hex_bits_16(s)
 
 /* ****************************************************************** */
-
-
-end ast
-end execute
-end assembly
-end encdec
-end encdec_compressed
-
-function decode bv = Some(encdec(bv))
-function decodeCompressed bv = Some(encdec_compressed(bv))
-function print_insn insn = assembly(insn)
\ No newline at end of file
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index a6fa1298..7028d5b8 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -97,6 +97,10 @@ val plat_enable_misaligned_access : unit -> bool
 let plat_enable_misaligned_access () = false
 declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
 
+val plat_mtval_has_illegal_inst_bits : unit -> bool
+let plat_mtval_has_illegal_inst_bits () = false
+declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
+
 val plat_insns_per_tick : unit -> integer
 let plat_insns_per_tick () = 1
 declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem
index a6fa1298..7028d5b8 100644
--- a/riscv/riscv_extras_sequential.lem
+++ b/riscv/riscv_extras_sequential.lem
@@ -97,6 +97,10 @@ val plat_enable_misaligned_access : unit -> bool
 let plat_enable_misaligned_access () = false
 declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
 
+val plat_mtval_has_illegal_inst_bits : unit -> bool
+let plat_mtval_has_illegal_inst_bits () = false
+declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
+
 val plat_insns_per_tick : unit -> integer
 let plat_insns_per_tick () = 1
 declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
diff --git a/riscv/riscv_insts_begin.sail b/riscv/riscv_insts_begin.sail
new file mode 100644
index 00000000..56fd8b43
--- /dev/null
+++ b/riscv/riscv_insts_begin.sail
@@ -0,0 +1,19 @@
+/* Instruction definitions.
+ *
+ * This includes decoding, execution, and assembly parsing and printing.
+ */
+
+scattered union ast
+
+/* returns whether an instruction was retired, used for computing minstret */
+val execute : ast -> bool effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
+scattered function execute
+
+val assembly : ast <-> string
+scattered mapping assembly
+
+val encdec : ast <-> bits(32)
+scattered mapping encdec
+
+val encdec_compressed : ast <-> bits(16)
+scattered mapping encdec_compressed
diff --git a/riscv/riscv_insts_end.sail b/riscv/riscv_insts_end.sail
new file mode 100644
index 00000000..144f06e3
--- /dev/null
+++ b/riscv/riscv_insts_end.sail
@@ -0,0 +1,15 @@
+/* End definitions */
+end ast
+end execute
+end assembly
+end encdec
+end encdec_compressed
+
+val cast print_insn : ast -> string
+function print_insn insn = assembly(insn)
+
+val decode : bits(32) -> option(ast) effect pure
+function decode bv = Some(encdec(bv))
+
+val decodeCompressed : bits(16) -> option(ast) effect pure
+function decodeCompressed bv = Some(encdec_compressed(bv))
diff --git a/riscv/riscv_jalr_rmem.sail b/riscv/riscv_jalr_rmem.sail
new file mode 100644
index 00000000..3e5eec9a
--- /dev/null
+++ b/riscv/riscv_jalr_rmem.sail
@@ -0,0 +1,9 @@
+/* The definition for the memory model. */
+
+function clause execute (RISCV_JALR(imm, rs1, rd)) = {
+  /* write rd before anything else to prevent unintended strength */
+  X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
+  let newPC : xlenbits = X(rs1) + EXTS(imm);
+  nextPC = newPC[63..1] @ 0b0;
+  true
+}
diff --git a/riscv/riscv_jalr_seq.sail b/riscv/riscv_jalr_seq.sail
new file mode 100644
index 00000000..b38563ef
--- /dev/null
+++ b/riscv/riscv_jalr_seq.sail
@@ -0,0 +1,14 @@
+/* The definition for the sequential model. */
+
+function clause execute (RISCV_JALR(imm, rs1, rd)) = {
+/* For the sequential model, the memory-model definition doesn't work directly
+   if rs1 = rd.  We would effectively have to keep a regfile for reads and another for
+   writes, and swap on instruction completion.  This could perhaps be optimized in
+   some manner, but for now, we just keep a reordered definition to improve simulator
+   performance.
+*/
+  let newPC : xlenbits = X(rs1) + EXTS(imm);
+  X(rd) = nextPC;
+  nextPC = newPC[63..1] @ 0b0;
+  true
+}
diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index 7f6ec470..f0aff76a 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -1,68 +1,68 @@
 #include "sail.h"
 #include "rts.h"
 #include "riscv_prelude.h"
+#include "riscv_platform_impl.h"
+
+/* This file contains the definitions of the C externs of Sail model. */
+
+static mach_bits reservation = 0;
+static bool reservation_valid = false;
 
 bool plat_enable_dirty_update(unit u)
-{ return false; }
+{ return rv_enable_dirty_update; }
 
 bool plat_enable_misaligned_access(unit u)
-{ return false; }
+{ return rv_enable_misaligned; }
+
+bool plat_mtval_has_illegal_inst_bits(unit u)
+{ return rv_mtval_has_illegal_inst_bits; }
 
 mach_bits plat_ram_base(unit u)
-{
-  return UINT64_C(0x80000000);
-}
+{ return rv_ram_base; }
 
 mach_bits plat_ram_size(unit u)
-{
-  return UINT64_C(0x80000000);
-}
+{ return rv_ram_size; }
 
 mach_bits plat_rom_base(unit u)
-{
-  return UINT64_C(0x1000);
-}
+{ return rv_rom_base; }
 
 mach_bits plat_rom_size(unit u)
-{
-  return UINT64_C(0x100);
-}
+{ return rv_rom_size; }
 
 mach_bits plat_clint_base(unit u)
-{
-  return UINT64_C(0x2000000);
-}
+{ return rv_clint_base; }
 
 mach_bits plat_clint_size(unit u)
-{
-  return UINT64_C(0xc0000);
-}
+{ return rv_clint_size; }
 
-bool within_phys_mem(mach_bits addr, sail_int len)
+unit load_reservation(mach_bits addr)
 {
-  printf("within_phys_mem\n");
-  exit(EXIT_FAILURE);
-  return 0;
+  reservation = addr;
+  reservation_valid = true;
+  return UNIT;
 }
 
-unit load_reservation(mach_bits addr)
-{ return UNIT; }
-
 bool match_reservation(mach_bits addr)
-{ return false; }
+{ return reservation_valid && reservation == addr; }
 
 unit cancel_reservation(unit u)
-{ return UNIT; }
+{
+  reservation_valid = false;
+  return UNIT;
+}
 
-unit plat_term_write(mach_bits c)
-{ return UNIT; }
+unit plat_term_write(mach_bits s)
+{ char c = s & 0xff;
+  plat_term_write_impl(c);
+  return UNIT;
+}
 
 void plat_insns_per_tick(sail_int *rop, unit u)
 { }
 
 mach_bits plat_htif_tohost(unit u)
 {
-  return UINT64_C(0x80001000);
+  return rv_htif_tohost;
 }
 
 unit memea(mach_bits len, sail_int n)
diff --git a/riscv/riscv_platform.h b/riscv/riscv_platform.h
index 4401ad49..93782660 100644
--- a/riscv/riscv_platform.h
+++ b/riscv/riscv_platform.h
@@ -3,6 +3,7 @@
 
 bool plat_enable_dirty_update(unit);
 bool plat_enable_misaligned_access(unit);
+bool plat_mtval_has_illegal_inst_bits(unit);
 
 mach_bits plat_ram_base(unit);
 mach_bits plat_ram_size(unit);
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 728b25f9..aac6b587 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -38,6 +38,11 @@ val plat_enable_misaligned_access = {ocaml: "Platform.enable_misaligned_access",
                                      lem: "plat_enable_misaligned_access"} : unit -> bool
 function plat_enable_misaligned_access () = false
 
+/* whether mtval stores the bits of a faulting instruction on illegal instruction exceptions */
+val plat_mtval_has_illegal_inst_bits = {ocaml: "Platform.mtval_has_illegal_inst_bits",
+                                        c: "plat_mtval_has_illegal_inst_bits",
+                                        lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool
+
 /* ROM holding reset vector and device-tree DTB */
 val plat_rom_base   = {ocaml: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits
 function plat_rom_base () = 0x0000000000001000
@@ -63,15 +68,28 @@ function phys_mem_segments() =
 
 /* Physical memory map predicates */
 
-function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool = {
+  let ram_base = plat_ram_base ();
+  let rom_base = plat_rom_base ();
+  let ram_size = plat_ram_size ();
+  let rom_size = plat_rom_size ();
+
   /* todo: iterate over segment list */
-  if (  plat_ram_base() <=_u addr
-      & (addr + sizeof('n)) <=_u (plat_ram_base() + plat_ram_size ()))
+  if (  ram_base <=_u addr
+      & (addr + sizeof('n)) <=_u (ram_base + ram_size))
        then true
-  else if (  plat_rom_base() <=_u addr
-           & (addr + sizeof('n)) <=_u (plat_rom_base() + plat_rom_size()))
+  else if (  rom_base <=_u addr
+           & (addr + sizeof('n)) <=_u (rom_base + rom_size))
        then true
-  else false
+  else {
+    print("within_phys_mem: " ^ BitStr(addr) ^ " not within phys-mem:");
+    print("  plat_rom_base: " ^ BitStr(rom_base));
+    print("  plat_rom_size: " ^ BitStr(rom_size));
+    print("  plat_ram_base: " ^ BitStr(ram_base));
+    print("  plat_ram_size: " ^ BitStr(ram_size));
+    false
+  }
+}
 
 function within_clint(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
     plat_clint_base() <=_u addr
@@ -274,3 +292,14 @@ function tick_platform() -> unit = {
   cancel_reservation();
   htif_tick();
 }
+
+/* Platform-specific handling of instruction faults */
+
+function handle_illegal() -> unit = {
+  let info = if plat_mtval_has_illegal_inst_bits ()
+             then Some(instbits)
+             else None();
+  let t : sync_exception = struct { trap    = E_Illegal_Instr,
+                                    excinfo = info };
+  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
+}
diff --git a/riscv/riscv_platform_impl.c b/riscv/riscv_platform_impl.c
new file mode 100644
index 00000000..04a661c0
--- /dev/null
+++ b/riscv/riscv_platform_impl.c
@@ -0,0 +1,29 @@
+#include "riscv_platform_impl.h"
+#include <unistd.h>
+#include <stdio.h>
+
+/* Settings of the platform implementation, with common defaults. */
+
+bool rv_enable_dirty_update         = false;
+bool rv_enable_misaligned           = false;
+bool rv_mtval_has_illegal_inst_bits = false;
+
+uint64_t rv_ram_base = UINT64_C(0x80000000);
+uint64_t rv_ram_size = UINT64_C(0x80000000);
+
+uint64_t rv_rom_base = UINT64_C(0x1000);
+uint64_t rv_rom_size = UINT64_C(0x100);
+
+uint64_t rv_clint_base = UINT64_C(0x2000000);
+uint64_t rv_clint_size = UINT64_C(0xc0000);
+
+uint64_t rv_htif_tohost = UINT64_C(0x80001000);
+uint64_t rv_insns_per_tick = UINT64_C(100);
+
+int term_fd = 1; // set during startup
+void plat_term_write_impl(char c)
+{
+  if (write(term_fd, &c, sizeof(c)) < 0) {
+    fprintf(stderr, "Unable to write to terminal!\n");
+  }
+}
diff --git a/riscv/riscv_platform_impl.h b/riscv/riscv_platform_impl.h
new file mode 100644
index 00000000..85e25c95
--- /dev/null
+++ b/riscv/riscv_platform_impl.h
@@ -0,0 +1,28 @@
+#pragma once
+
+#include <stdbool.h>
+#include <stdint.h>
+
+/* Settings of the platform implementation. */
+
+#define DEFAULT_RSTVEC     0x00001000
+#define SAIL_XLEN          64
+
+extern bool rv_enable_dirty_update;
+extern bool rv_enable_misaligned;
+extern bool rv_mtval_has_illegal_inst_bits;
+
+extern uint64_t rv_ram_base;
+extern uint64_t rv_ram_size;
+
+extern uint64_t rv_rom_base;
+extern uint64_t rv_rom_size;
+
+extern uint64_t rv_clint_base;
+extern uint64_t rv_clint_size;
+
+extern uint64_t rv_htif_tohost;
+extern uint64_t rv_insns_per_tick;
+
+extern int term_fd;
+void plat_term_write_impl(char c);
diff --git a/riscv/riscv_sail.h b/riscv/riscv_sail.h
new file mode 100644
index 00000000..f2569b3b
--- /dev/null
+++ b/riscv/riscv_sail.h
@@ -0,0 +1,44 @@
+/* Top-level interfaces to the Sail model.
+   Ideally, this would be autogenerated.
+ */
+
+typedef int unit;
+#define UNIT 0
+typedef uint64_t mach_bits;
+
+void model_init(void);
+void model_fini(void);
+
+unit zinit_platform(unit);
+unit zinit_sys(unit);
+bool zstep(sail_int);
+unit ztick_clock(unit);
+unit ztick_platform(unit);
+
+extern bool zhtif_done;
+extern mach_bits zhtif_exit_code;
+extern bool have_exception;
+
+/* machine state */
+
+extern uint32_t zcur_privilege;
+
+extern mach_bits zPC;
+
+extern mach_bits
+        zx1,  zx2,  zx3,  zx4,  zx5,  zx6,  zx7,
+  zx8,  zx9,  zx10, zx11, zx12, zx13, zx14, zx15,
+  zx16, zx17, zx18, zx19, zx20, zx21, zx22, zx23,
+  zx24, zx25, zx26, zx27, zx28, zx29, zx30, zx31;
+
+extern mach_bits zmstatus;
+extern mach_bits zmepc, zmtval;
+extern mach_bits zsepc, zstval;
+
+struct zMcause {mach_bits zMcause_chunk_0;};
+struct zMcause zmcause, zscause;
+
+extern mach_bits zminstret;
+
+struct zMisa {mach_bits zMisa_chunk_0;};
+struct zMisa zmisa;
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
new file mode 100644
index 00000000..276c7b1b
--- /dev/null
+++ b/riscv/riscv_sim.c
@@ -0,0 +1,486 @@
+#include <getopt.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <errno.h>
+#include <unistd.h>
+#include <sys/types.h>
+#include <sys/stat.h>
+#include <sys/mman.h>
+#include <fcntl.h>
+
+#include "elf.h"
+#include "sail.h"
+#include "rts.h"
+#include "riscv_platform.h"
+#include "riscv_platform_impl.h"
+#include "riscv_sail.h"
+
+//#define SPIKE 1
+#ifdef SPIKE
+#include "tv_spike_intf.h"
+#else
+struct tv_spike_t;
+#endif
+
+/* Selected CSRs from riscv-isa-sim/riscv/encoding.h */
+#define CSR_STVEC 0x105
+#define CSR_SEPC 0x141
+#define CSR_SCAUSE 0x142
+#define CSR_STVAL 0x143
+
+#define CSR_MSTATUS 0x300
+#define CSR_MISA 0x301
+#define CSR_MEDELEG 0x302
+#define CSR_MIDELEG 0x303
+#define CSR_MIE 0x304
+#define CSR_MTVEC 0x305
+#define CSR_MEPC 0x341
+#define CSR_MCAUSE 0x342
+#define CSR_MTVAL 0x343
+#define CSR_MIP 0x344
+
+static bool do_dump_dts = false;
+struct tv_spike_t *s = NULL;
+char *term_log = NULL;
+char *dtb_file = NULL;
+unsigned char *dtb = NULL;
+size_t dtb_len = 0;
+
+unsigned char *spike_dtb = NULL;
+size_t spike_dtb_len = 0;
+
+static struct option options[] = {
+  {"enable-dirty",                no_argument,       0, 'd'},
+  {"enable-misaligned",           no_argument,       0, 'm'},
+  {"mtval-has-illegal-inst-bits", no_argument,       0, 'i'},
+  {"dump-dts",                    no_argument,       0, 's'},
+  {"device-tree-blob",            required_argument, 0, 'b'},
+  {"terminal-log",                required_argument, 0, 't'},
+  {"help",                        no_argument,       0, 'h'},
+  {0, 0, 0, 0}
+};
+
+static void print_usage(const char *argv0, int ec)
+{
+  fprintf(stdout, "Usage: %s [options] <elf_file>\n", argv0);
+  struct option *opt = options;
+  while (opt->name) {
+    fprintf(stdout, "\t -%c\t %s\n", (char)opt->val, opt->name);
+    opt++;
+  }
+  exit(ec);
+}
+
+static void dump_dts(void)
+{
+#ifdef SPIKE
+  size_t dts_len = 0;
+  struct tv_spike_t *s = tv_init("RV64IMAC", 0);
+  tv_get_dts(s, NULL, &dts_len);
+  if (dts_len > 0) {
+    unsigned char *dts = (unsigned char *)malloc(dts_len + 1);
+    dts[dts_len] = '\0';
+    tv_get_dts(s, dts, &dts_len);
+    fprintf(stdout, "%s\n", dts);
+  }
+#else
+  fprintf(stdout, "Spike linkage is currently needed to generate DTS.\n");
+#endif
+  exit(0);
+}
+
+static void read_dtb(const char *path)
+{
+  int fd = open(path, O_RDONLY);
+  if (fd < 0) {
+    fprintf(stderr, "Unable to read DTB file %s: %s\n", path, strerror(errno));
+    exit(1);
+  }
+  struct stat st;
+  if (fstat(fd, &st) < 0) {
+    fprintf(stderr, "Unable to stat DTB file %s: %s\n", path, strerror(errno));
+    exit(1);
+  }
+  char *m = (char *)mmap(NULL, st.st_size, PROT_READ, MAP_PRIVATE, fd, 0);
+  if (m == MAP_FAILED) {
+    fprintf(stderr, "Unable to map DTB file %s: %s\n", path, strerror(errno));
+    exit(1);
+  }
+  dtb = (unsigned char *)malloc(st.st_size);
+  if (dtb == NULL) {
+    fprintf(stderr, "Cannot allocate DTB from file %s!\n", path);
+    exit(1);
+  }
+  memcpy(dtb, m, st.st_size);
+  dtb_len = st.st_size;
+  munmap(m, st.st_size);
+  close(fd);
+
+  fprintf(stdout, "Read %ld bytes of DTB from %s.\n", dtb_len, path);
+}
+
+char *process_args(int argc, char **argv)
+{
+  int c, idx = 1;
+  while(true) {
+    c = getopt_long(argc, argv, "dmsb:t:v:h", options, &idx);
+    if (c == -1) break;
+    switch (c) {
+    case 'd':
+      rv_enable_dirty_update = true;
+      break;
+    case 'm':
+      rv_enable_misaligned = true;
+      break;
+    case 'i':
+      rv_mtval_has_illegal_inst_bits = true;
+    case 's':
+      do_dump_dts = true;
+      break;
+    case 'b':
+      dtb_file = strdup(optarg);
+      break;
+    case 't':
+      term_log = strdup(optarg);
+      break;
+    case 'h':
+      print_usage(argv[0], 0);
+      break;
+    default:
+      fprintf(stderr, "Unrecognized optchar %c\n", c);
+      print_usage(argv[0], 1);
+    }
+  }
+  if (do_dump_dts) dump_dts();
+  if (idx >= argc) print_usage(argv[0], 0);
+  if (term_log == NULL) term_log = strdup("term.log");
+  if (dtb_file) read_dtb(dtb_file);
+
+  fprintf(stdout, "Running file %s.\n", argv[optind]);
+  return argv[optind];
+}
+
+uint64_t load_sail(char *f)
+{
+  bool is32bit;
+  uint64_t entry;
+  load_elf(f, &is32bit, &entry);
+  if (is32bit) {
+    fprintf(stderr, "32-bit RISC-V not yet supported.\n");
+    exit(1);
+  }
+  fprintf(stdout, "ELF Entry @ %lx\n", entry);
+  /* locate htif ports */
+  if (lookup_sym(f, "tohost", &rv_htif_tohost) < 0) {
+    fprintf(stderr, "Unable to locate htif tohost port.\n");
+    exit(1);
+  }
+  fprintf(stderr, "tohost located at %0" PRIx64 "\n", rv_htif_tohost);
+  return entry;
+}
+
+void init_spike(const char *f, uint64_t entry)
+{
+#ifdef SPIKE
+  /* The initialization order below matters. */
+  s = tv_init("RV64IMAC", 1);
+  tv_set_verbose(s, 1);
+  tv_set_dtb_in_rom(s, 1);
+  tv_load_elf(s, f);
+  tv_reset(s);
+
+  /* sync the insns per tick */
+  rv_insns_per_tick = tv_get_insns_per_tick(s);
+
+  /* get DTB from spike */
+  tv_get_dtb(s, NULL, &spike_dtb_len);
+  if (spike_dtb_len > 0) {
+    spike_dtb = (unsigned char *)malloc(spike_dtb_len + 1);
+    dtb[spike_dtb_len] = '\0';
+    if (!tv_get_dtb(s, spike_dtb, &spike_dtb_len)) {
+      fprintf(stderr, "Got %ld bytes of dtb at %p\n", spike_dtb_len, spike_dtb);
+    } else {
+      fprintf(stderr, "Error getting DTB from Spike.\n");
+      exit(1);
+    }
+  } else {
+    fprintf(stderr, "No DTB available from Spike.\n");
+  }
+#else
+  s = NULL;
+#endif
+}
+
+void tick_spike()
+{
+#ifdef SPIKE
+  tv_tick_clock(s);
+  tv_step_io(s);
+#endif
+}
+
+void init_sail_reset_vector(uint64_t entry)
+{
+#define RST_VEC_SIZE 8
+  uint32_t reset_vec[RST_VEC_SIZE] = {
+    0x297,                                      // auipc  t0,0x0
+    0x28593 + (RST_VEC_SIZE * 4 << 20),         // addi   a1, t0, &dtb
+    0xf1402573,                                 // csrr   a0, mhartid
+    SAIL_XLEN == 32 ?
+      0x0182a283u :                             // lw     t0,24(t0)
+      0x0182b283u,                              // ld     t0,24(t0)
+    0x28067,                                    // jr     t0
+    0,
+    (uint32_t) (entry & 0xffffffff),
+    (uint32_t) (entry >> 32)
+  };
+
+  rv_rom_base = DEFAULT_RSTVEC;
+  uint64_t addr = rv_rom_base;
+  for (int i = 0; i < sizeof(reset_vec); i++)
+    write_mem(addr++, (uint64_t)((char *)reset_vec)[i]);
+
+  if (dtb && dtb_len) {
+    for (size_t i = 0; i < dtb_len; i++)
+      write_mem(addr++, dtb[i]);
+  }
+
+#ifdef SPIKE
+  if (dtb && dtb_len) {
+    // Ensure that Spike's DTB matches the one provided.
+    bool matched = dtb_len == spike_dtb_len;
+    if (matched) {
+      for (size_t i = 0; i < dtb_len; i++)
+        matched = matched && (dtb[i] == spike_dtb[i]);
+    }
+    if (!matched) {
+      fprintf(stderr, "Provided DTB does not match Spike's!\n");
+      exit(1);
+    }
+  } else {
+    if (spike_dtb_len > 0) {
+      // Use the DTB from Spike.
+      for (size_t i = 0; i < spike_dtb_len; i++)
+        write_mem(addr++, spike_dtb[i]);
+    } else {
+      fprintf(stderr, "Running without rom device tree.\n");
+    }
+  }
+#endif
+
+  /* zero-fill to page boundary */
+  const int align = 0x1000;
+  uint64_t rom_end = (addr + align -1)/align * align;
+  for (int i = addr; i < rom_end; i++)
+    write_mem(addr++, 0);
+
+  /* set rom size */
+  rv_rom_size = rom_end - rv_rom_base;
+  /* boot at reset vector */
+  zPC = rv_rom_base;
+}
+
+void init_sail(uint64_t elf_entry)
+{
+  model_init();
+  zinit_platform(UNIT);
+  zinit_sys(UNIT);
+  init_sail_reset_vector(elf_entry);
+}
+
+int init_check(struct tv_spike_t *s)
+{
+  int passed = 1;
+#ifdef SPIKE
+  passed &= tv_check_csr(s, CSR_MISA, zmisa.zMisa_chunk_0);
+#endif
+  return passed;
+}
+
+void finish(int ec)
+{
+  model_fini();
+#ifdef SPIKE
+  tv_free(s);
+#endif
+  exit(ec);
+}
+
+int compare_states(struct tv_spike_t *s)
+{
+  int passed = 1;
+
+#ifdef SPIKE
+  // fix default C enum map for cur_privilege
+  uint8_t priv = (zcur_privilege == 2) ? 3 : zcur_privilege;
+  passed &= tv_check_priv(s, priv);
+
+  passed &= tv_check_pc(s, zPC);
+
+  passed &= tv_check_gpr(s, 1, zx1);
+  passed &= tv_check_gpr(s, 2, zx2);
+  passed &= tv_check_gpr(s, 3, zx3);
+  passed &= tv_check_gpr(s, 4, zx4);
+  passed &= tv_check_gpr(s, 5, zx5);
+  passed &= tv_check_gpr(s, 6, zx6);
+  passed &= tv_check_gpr(s, 7, zx7);
+  passed &= tv_check_gpr(s, 8, zx8);
+  passed &= tv_check_gpr(s, 9, zx9);
+  passed &= tv_check_gpr(s, 10, zx10);
+  passed &= tv_check_gpr(s, 11, zx11);
+  passed &= tv_check_gpr(s, 12, zx12);
+  passed &= tv_check_gpr(s, 13, zx13);
+  passed &= tv_check_gpr(s, 14, zx14);
+  passed &= tv_check_gpr(s, 15, zx15);
+  passed &= tv_check_gpr(s, 15, zx15);
+  passed &= tv_check_gpr(s, 16, zx16);
+  passed &= tv_check_gpr(s, 17, zx17);
+  passed &= tv_check_gpr(s, 18, zx18);
+  passed &= tv_check_gpr(s, 19, zx19);
+  passed &= tv_check_gpr(s, 20, zx20);
+  passed &= tv_check_gpr(s, 21, zx21);
+  passed &= tv_check_gpr(s, 22, zx22);
+  passed &= tv_check_gpr(s, 23, zx23);
+  passed &= tv_check_gpr(s, 24, zx24);
+  passed &= tv_check_gpr(s, 25, zx25);
+  passed &= tv_check_gpr(s, 25, zx25);
+  passed &= tv_check_gpr(s, 26, zx26);
+  passed &= tv_check_gpr(s, 27, zx27);
+  passed &= tv_check_gpr(s, 28, zx28);
+  passed &= tv_check_gpr(s, 29, zx29);
+  passed &= tv_check_gpr(s, 30, zx30);
+  passed &= tv_check_gpr(s, 31, zx31);
+
+  /* some selected CSRs for now */
+
+  passed &= tv_check_csr(s, CSR_MCAUSE, zmcause.zMcause_chunk_0);
+  passed &= tv_check_csr(s, CSR_MEPC, zmepc);
+  passed &= tv_check_csr(s, CSR_MTVAL, zmtval);
+  passed &= tv_check_csr(s, CSR_MSTATUS, zmstatus);
+
+  passed &= tv_check_csr(s, CSR_SCAUSE, zscause.zMcause_chunk_0);
+  passed &= tv_check_csr(s, CSR_SEPC, zsepc);
+  passed &= tv_check_csr(s, CSR_STVAL, zstval);
+#endif
+
+  return passed;
+}
+
+void flush_logs(void)
+{
+  fprintf(stderr, "\n");
+  fflush(stderr);
+  fprintf(stdout, "\n");
+  fflush(stdout);
+}
+
+void run_sail(void)
+{
+  bool spike_done;
+  bool stepped;
+  bool diverged = false;
+
+  /* initialize the step number */
+  mach_int step_no = 0;
+  int insn_cnt = 0;
+
+  while (!zhtif_done) {
+    { /* run a Sail step */
+      sail_int sail_step;
+      CREATE(sail_int)(&sail_step);
+      CONVERT_OF(sail_int, mach_int)(&sail_step, step_no);
+      stepped = zstep(sail_step);
+      if (have_exception) goto step_exception;
+      flush_logs();
+    }
+    if (stepped) {
+      step_no++;
+      insn_cnt++;
+    }
+
+#ifdef SPIKE
+    { /* run a Spike step */
+      tv_step(s);
+      spike_done = tv_is_done(s);
+      flush_logs();
+    }
+
+    if (zhtif_done) {
+      if (!spike_done) {
+        fprintf(stdout, "Sail done (exit-code %ld), but not Spike!\n", zhtif_exit_code);
+        exit(1);
+      }
+    } else {
+      if (spike_done) {
+        fprintf(stdout, "Spike done, but not Sail!\n");
+        exit(1);
+      }
+    }
+    if (!compare_states(s)) {
+      diverged = true;
+      break;
+    }
+#endif
+    if (zhtif_done) {
+      /* check exit code */
+      if (zhtif_exit_code == 0)
+        fprintf(stdout, "SUCCESS\n");
+      else
+        fprintf(stdout, "FAILURE: %ld\n", zhtif_exit_code);
+    }
+
+    if (insn_cnt == rv_insns_per_tick) {
+      insn_cnt = 0;
+      ztick_clock(UNIT);
+      ztick_platform(UNIT);
+
+      tick_spike();
+    }
+  }
+
+ dump_state:
+  if (diverged) {
+    /* TODO */
+  }
+  finish(diverged);
+
+ step_exception:
+  fprintf(stderr, "Sail exception!");
+  goto dump_state;
+}
+
+void init_logs()
+{
+#ifdef SPIKE
+  // The Spike interface uses stdout for terminal output, and stderr for logs.
+  // Do the same here.
+  if (dup2(1, 2) < 0) {
+    fprintf(stderr, "Unable to dup 1 -> 2: %s\n", strerror(errno));
+    exit(1);
+  }
+#endif
+
+  if ((term_fd = open(term_log, O_WRONLY|O_CREAT|O_TRUNC, S_IRUSR|S_IRGRP|S_IROTH|S_IWUSR)) < 0) {
+    fprintf(stderr, "Cannot create terminal log '%s': %s\n", term_log, strerror(errno));
+    exit(1);
+  }
+}
+
+int main(int argc, char **argv)
+{
+  char *file = process_args(argc, argv);
+  init_logs();
+
+  uint64_t entry = load_sail(file);
+
+  /* initialize spike before sail so that we can access the device-tree blob,
+   * until we roll our own.
+   */
+  init_spike(file, entry);
+  init_sail(entry);
+
+  if (!init_check(s)) finish(1);
+
+  run_sail();
+  flush_logs();
+}
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index 7d883f24..ef923762 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -63,7 +63,8 @@ function step(step_no) = {
             match decodeCompressed(h) {
               None() => {
                 print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
-                handle_decode_exception(EXTZ(h));
+                instbits = EXTZ(h);
+                handle_illegal();
                 (false, true)
               },
               Some(ast) => {
@@ -77,7 +78,8 @@ function step(step_no) = {
             match decode(w) {
               None() => {
                 print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") <no-decode>");
-                handle_decode_exception(EXTZ(w));
+                instbits = EXTZ(w);
+                handle_illegal();
                 (false, true)
               },
               Some(ast) => {
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 2669ee3f..818700b4 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -375,13 +375,17 @@ function lower_mstatus(m : Mstatus) -> Sstatus = {
 }
 
 function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
-  let m = update_SD(m, s.SD());
   // FIXME: This should be parameterized by a platform setting.  For now, match spike.
   // let m = update_UXL(m, s.UXL());
   let m = update_MXR(m, s.MXR());
   let m = update_SUM(m, s.SUM());
+
+  // FIXME: Should XS and FS check whether X and F|D are supported in misa?
   let m = update_XS(m, s.XS());
   let m = update_FS(m, s.FS());
+  let m = update_SD(m, extStatus_of_bits(m.FS()) == Dirty
+                     | extStatus_of_bits(m.XS()) == Dirty);
+
   let m = update_SPP(m, s.SPP());
   let m = update_SPIE(m, s.SPIE());
   let m = update_UPIE(m, s.UPIE());
@@ -990,21 +994,9 @@ function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
   nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
 }
 
-function handle_decode_exception(instbits : xlenbits) -> unit = {
-  let t : sync_exception = struct { trap    = E_Illegal_Instr,
-                                    excinfo = Some(instbits) };
-  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
-}
-
 function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
   nextPC = handle_trap(del_priv, true, i, PC, None())
 
-function handle_illegal() -> unit = {
-  let t : sync_exception = struct { trap    = E_Illegal_Instr,
-                                    excinfo = None() };
-  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
-}
-
 /* state state initialization */
 
 function init_sys() -> unit = {
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index d269356c..4cbc6f87 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -34,8 +34,11 @@ let sp   : regbits = 0b00010  /* x2, stack pointer  */
 
 /* program counter */
 
-register PC     : xlenbits
-register nextPC : xlenbits
+register PC       : xlenbits
+register nextPC   : xlenbits
+
+/* internal state to hold instruction bits for faulting instructions */
+register instbits : xlenbits
 
 /* register file and accessors */
 
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 1d0689e4..9966742e 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -329,7 +329,7 @@ let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2))
 let nc_true = mk_nc NC_true
 let nc_false = mk_nc NC_false
 
-let rec nc_negate (NC_aux (nc, _)) =
+let rec nc_negate (NC_aux (nc, l)) =
   match nc with
   | NC_bounded_ge (n1, n2) -> nc_lt n1 n2
   | NC_bounded_le (n1, n2) -> nc_gt n1 n2
@@ -343,6 +343,8 @@ let rec nc_negate (NC_aux (nc, _)) =
   | NC_set (kid, [int]) -> nc_neq (nvar kid) (nconstant int)
   | NC_set (kid, int :: ints) ->
      mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints)))))
+  | NC_app _ ->
+     raise (Reporting_basic.err_unreachable l __POS__ "tried to negate constraint with unexpanded synonym")
 
 let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown)
 
@@ -379,6 +381,10 @@ let quant_split typq =
   let qis = quant_items typq in
   List.concat (List.map qi_kopt qis), List.concat (List.map qi_nc qis)
 
+let quant_map_items f = function
+  | TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_no_forall, l)
+  | TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (List.map f qis), l)
+
 let unaux_nexp (Nexp_aux (nexp, _)) = nexp
 let unaux_order (Ord_aux (ord, _)) = ord
 let unaux_typ (Typ_aux (typ, _)) = typ
@@ -523,8 +529,8 @@ let def_loc = function
   | DEF_scattered (SD_aux (_, (l, _)))
   | DEF_reg_dec (DEC_aux (_, (l, _)))
   | DEF_fixity (_, _, Id_aux (_, l))
-  | DEF_overload (Id_aux (_, l), _) ->
-    l
+  | DEF_overload (Id_aux (_, l), _) -> l
+  | DEF_constraint (Id_aux (_, l), _, _) -> l
   | DEF_internal_mutrec _ -> Parse_ast.Unknown
 
 let string_of_id = function
@@ -638,12 +644,17 @@ and string_of_n_constraint = function
      "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
   | NC_aux (NC_set (kid, ns), _) ->
      string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
+  | NC_aux (NC_app (id, nexps), _) ->
+     "where " ^ string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_nexp nexps ^ ")"
   | NC_aux (NC_true, _) -> "true"
   | NC_aux (NC_false, _) -> "false"
 
+let string_of_kinded_id = function
+  | KOpt_aux (KOpt_none kid, _) -> string_of_kid kid
+  | KOpt_aux (KOpt_kind (k, kid), _) -> "(" ^ string_of_kid kid ^ " : " ^ string_of_kind k ^ ")"
+
 let string_of_quant_item_aux = function
-  | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid
-  | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "(" ^ string_of_kid kid ^ " :: " ^ string_of_kind k ^ ")"
+  | QI_id kopt -> string_of_kinded_id kopt
   | QI_const constr -> string_of_n_constraint constr
 
 let string_of_quant_item = function
@@ -884,6 +895,8 @@ module NC = struct
     | NC_or (nc1,nc2), NC_or (nc3,nc4)
     | NC_and (nc1,nc2), NC_and (nc3,nc4)
       -> lex_ord compare compare nc1 nc3 nc2 nc4
+    | NC_app (id1, nexps1), NC_app (id2, nexps2)
+      -> lex_ord (Id.compare) (Util.compare_list Nexp.compare) id1 id2 nexps1 nexps2
     | NC_true, NC_true
     | NC_false, NC_false
       -> 0
@@ -894,6 +907,7 @@ module NC = struct
     | NC_set _, _ -> -1        | _, NC_set _ -> 1
     | NC_or _, _ -> -1         | _, NC_or _ -> 1
     | NC_and _, _ -> -1        | _, NC_and _ -> 1
+    | NC_app _, _ -> -1        | _, NC_app _ -> 1
     | NC_true, _ -> -1         | _, NC_true -> 1
 end
 
@@ -1079,6 +1093,8 @@ let rec tyvars_of_nc (NC_aux (nc, _)) =
   | NC_or (nc1, nc2)
   | NC_and (nc1, nc2) ->
      KidSet.union (tyvars_of_nc nc1) (tyvars_of_nc nc2)
+  | NC_app (id, nexps) ->
+     List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps)
   | NC_true
   | NC_false -> KidSet.empty
 
@@ -1338,6 +1354,7 @@ let rec locate_nc l (NC_aux (nc_aux, _)) =
     | NC_set (kid, nums) -> NC_set (locate_kid l kid, nums)
     | NC_or (nc1, nc2) -> NC_or (locate_nc l nc1, locate_nc l nc2)
     | NC_and (nc1, nc2) -> NC_and (locate_nc l nc1, locate_nc l nc2)
+    | NC_app (id, nexps) -> NC_app (id, List.map (locate_nexp l) nexps)
     | NC_true -> NC_true
     | NC_false -> NC_false
   in
diff --git a/src/ast_util.mli b/src/ast_util.mli
index bbe9463e..ea287190 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -172,6 +172,7 @@ val nc_negate : n_constraint -> n_constraint
 val quant_items : typquant -> quant_item list
 val quant_kopts : typquant -> kinded_id list
 val quant_split : typquant -> kinded_id list * n_constraint list
+val quant_map_items : (quant_item -> quant_item) -> typquant -> typquant
 
 (* Functions to map over the annotations in sub-expressions *)
 val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
@@ -209,6 +210,7 @@ val string_of_typ : typ -> string
 val string_of_typ_arg : typ_arg -> string
 val string_of_typ_pat : typ_pat -> string
 val string_of_n_constraint : n_constraint -> string
+val string_of_kinded_id : kinded_id -> string
 val string_of_quant_item : quant_item -> string
 val string_of_typquant : typquant -> string
 val string_of_typschm : typschm -> string
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4e6e941d..36513ba1 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -370,6 +370,9 @@ and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint)
                 NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
              | Parse_ast.NC_and (nc1, nc2) ->
                 NC_and (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
+             | Parse_ast.NC_app (id, typs) ->
+                let nexps = List.map (to_ast_nexp k_env) typs in
+                NC_app (to_ast_id id, nexps)
              | Parse_ast.NC_true -> NC_true
              | Parse_ast.NC_false -> NC_false
     ), l)
@@ -907,6 +910,11 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
   | Parse_ast.DEF_reg_dec(dec) ->
      let d = to_ast_dec envs dec in
      ((Finished(DEF_reg_dec(d))),envs),partial_defs
+  | Parse_ast.DEF_constraint (id, kids, nc) ->
+     let id = to_ast_id id in
+     let kids = List.map to_ast_var kids in
+     let nc = to_ast_nexp_constraint k_env nc in
+     ((Finished (DEF_constraint (id, kids, nc))), envs), partial_defs
   | Parse_ast.DEF_pragma (_, _, l) ->
      typ_error l "Encountered preprocessor directive in initial check" None None None
   | Parse_ast.DEF_internal_mutrec _ ->
diff --git a/src/lexer.mll b/src/lexer.mll
index cc49073c..cbefa601 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -163,6 +163,8 @@ let kw_table =
      ("do",                      (fun _ -> Do));
      ("mutual",                  (fun _ -> Mutual));
      ("bitfield",                (fun _ -> Bitfield));
+     ("tuple",                   (fun _ -> Tuple));
+     ("where",                   (fun _ -> Where));
 
      ("barr",                    (fun x -> Barr));
      ("depend",                  (fun x -> Depend));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index a4052d82..3317c196 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -176,6 +176,7 @@ n_constraint_aux =  (* constraint over kind $_$ *)
  | NC_set of kid * (Big_int.num) list
  | NC_or of n_constraint * n_constraint
  | NC_and of n_constraint * n_constraint
+ | NC_app of id * atyp list
  | NC_true
  | NC_false
 
@@ -566,6 +567,7 @@ def =  (* Top-level definition *)
  | DEF_scattered of scattered_def (* scattered definition *)
  | DEF_reg_dec of dec_spec (* register declaration *)
  | DEF_pragma of string * string * l
+ | DEF_constraint of id * kid list * n_constraint
  | DEF_internal_mutrec of fundef list
 
 
diff --git a/src/parser.mly b/src/parser.mly
index b9aae275..070dee50 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -175,7 +175,7 @@ let rec desugar_rchain chain s e =
 
 /*Terminals with no content*/
 
-%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
+%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Tuple Where
 %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Cast
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
 %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
@@ -331,6 +331,8 @@ nc_and:
     { $1 }
 
 atomic_nc:
+  | Where id Lparen typ_list Rparen
+    { mk_nc (NC_app ($2, $4)) $startpos $endpos }
   | True
     { mk_nc NC_true $startpos $endpos }
   | False
@@ -1402,6 +1404,8 @@ def:
     { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) }
   | default_def
     { DEF_default $1 }
+  | Constraint id Lparen kid_list Rparen Eq nc
+    { DEF_constraint ($2, $4, $7) }
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
   | Pragma
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 806234d6..f1726ce4 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -694,6 +694,13 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
             List.map (subst_unifiers unifiers) arg_typs
          | _ -> assert false
        in
+       (* Constructors that were specified without a return type might get
+          an extra tuple in their type; expand that here if necessary.
+          TODO: this should go away if we enforce proper arities. *)
+       let arg_typs = match pats, arg_typs with
+         | _::_::_, [Typ_aux (Typ_tup typs,_)] -> typs
+         | _,_ -> arg_typs
+       in
        let ppp = doc_unop (doc_id_ctor id)
          (parens (separate_map comma (doc_pat ctxt true true) (List.combine pats arg_typs))) in
        if apat_needed then parens ppp else ppp
@@ -1761,33 +1768,28 @@ let args_of_typ l env typs =
     E_aux (E_id id, (l, mk_tannot env typ no_effect)) in
   List.split (List.mapi arg typs)
 
-let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) =
+let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) =
   let env = env_of_annot annot in
-  let tup_typs = match typ with
-    | Typ_aux (Typ_tup typs, _) -> Some typs
-    | _ -> match Env.expand_synonyms env typ with
-      | Typ_aux (Typ_tup typs, _) -> Some typs
-      | _ -> None
-  in
   let identity = (fun body -> body) in
-  match paux, tup_typs with
+  match paux, typs with
   | P_tup [], _ ->
      let annot = (l, mk_tannot Env.empty unit_typ no_effect) in
      [P_aux (P_lit (mk_lit L_unit), annot), unit_typ], identity
-  | P_tup pats, Some typs -> List.combine pats typs, identity
-  | P_tup pats, _ -> raise (Reporting_basic.err_unreachable l __POS__ "Tuple pattern against non-tuple type")
-  | P_wild, Some typs ->
+  | P_tup pats, _ -> List.combine pats typs, identity
+  | P_wild, _ ->
      let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)), typ in
      List.map wild typs, identity
-  | P_typ (_, pat), _ -> untuple_args_pat typ pat
-  | P_as _, Some typs | P_id _, Some typs ->
+  | P_typ (_, pat), _ -> untuple_args_pat typs pat
+  | P_as _, _::_::_ | P_id _, _::_::_ ->
      let argpats, argexps = args_of_typ l env typs in
      let argexp = E_aux (E_tuple argexps, annot) in
      let bindargs (E_aux (_, bannot) as body) =
        E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in
      argpats, bindargs
-  | _, _ ->
+  | _, [typ] ->
      [pat,typ], identity
+  | _, _ ->
+     unreachable l __POS__ "Unexpected pattern/type combination"
 
 let doc_rec (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> string "Definition"
@@ -1923,7 +1925,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let ids_to_avoid = all_ids pexp in
   let bound_kids = tyvars_of_typquant tq in
   let pat,guard,exp,(l,_) = destruct_pexp pexp in
-  let pats, bind = untuple_args_pat (mk_typ (Typ_tup arg_typs)) pat in (* FIXME is this needed any more? *)
+  let pats, bind = untuple_args_pat arg_typs pat in (* FIXME is this needed any more? *)
   let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in
   let eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in
   let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in
@@ -1950,6 +1952,10 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let doc_binder (P_aux (p,ann) as pat, typ) =
     let env = env_of_annot ann in
     let exp_typ = Env.expand_synonyms env typ in
+    let () =
+      debug ctxt (lazy (" pattern " ^ string_of_pat pat));
+      debug ctxt (lazy (" with expanded type " ^ string_of_typ exp_typ))
+    in
     match p with
     | P_id id
     | P_typ (_,P_aux (P_id id,_))
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 8138a04e..68825c8f 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1228,42 +1228,35 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
             else empty)
     | _ -> raise (Reporting_basic.err_unreachable l __POS__ "register with non-constant indices")
 
-let args_of_typ l env typ =
-  let typs = match typ with
-    | Typ_aux (Typ_tup typs, _) -> typs
-    | typ -> [typ] in
+let args_of_typs l env typs =
   let arg i typ =
     let id = mk_id ("arg" ^ string_of_int i) in
     P_aux (P_id id, (l, mk_tannot env typ no_effect)),
     E_aux (E_id id, (l, mk_tannot env typ no_effect)) in
   List.split (List.mapi arg typs)
 
-let rec untuple_args_pat fun_typ (P_aux (paux, ((l, _) as annot)) as pat) =
+let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) arg_typs =
+  let env = env_of_annot annot in
   let identity = (fun body -> body) in
-  let env = env_of_annot annot in 
-  (* Hack until we get proper multiple-argument-patterns *)
-  match fun_typ with
-  | Typ_aux(Typ_fn([_], _, _), _) -> [pat], identity
-  | _ -> begin
-      let (Typ_aux (taux, _)) = typ_of_annot annot in
-      match paux, taux with
-      | P_tup [], _ ->
-         let annot = (l, mk_tannot Env.empty unit_typ no_effect) in
-         [P_aux (P_lit (mk_lit L_unit), annot)], identity
-      | P_tup pats, _ -> pats, identity
-      | P_wild, Typ_tup typs ->
-         let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)) in
-         List.map wild typs, identity
-      | P_typ (_, pat), _ -> untuple_args_pat fun_typ pat
-      | P_as _, Typ_tup _ | P_id _, Typ_tup _ ->
-         let argpats, argexps = args_of_typ l env (pat_typ_of pat) in
-         let argexp = E_aux (E_tuple argexps, annot) in
-         let bindargs (E_aux (_, bannot) as body) =
-           E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in
-         argpats, bindargs
-      | _, _ ->
-         [pat], identity
-    end
+  match paux, arg_typs with
+  | P_tup [], _ ->
+     let annot = (l, mk_tannot Env.empty unit_typ no_effect) in
+     [P_aux (P_lit (mk_lit L_unit), annot)], identity
+  | P_wild, [Typ_aux (Typ_tup typs, _)] ->
+     let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)) in
+     List.map wild typs, identity
+  | P_typ (_, pat), _ -> untuple_args_pat pat arg_typs
+  | P_as _, [Typ_aux (Typ_tup _, _)]
+    | P_id _, [Typ_aux (Typ_tup _, _)]
+    | P_tup _, [Typ_aux (Typ_tup _, _)] ->
+     let argpats, argexps = args_of_typs l env arg_typs in
+     let argexp = E_aux (E_tuple argexps, annot) in
+     let bindargs (E_aux (_, bannot) as body) =
+       E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in
+     argpats, bindargs
+  | P_tup pats, _ -> pats, identity
+  | _, _ ->
+     [pat], identity
 
 let doc_rec_lem force_rec (Rec_aux(r,_)) = match r with
   | Rec_nonrec when not force_rec -> space
@@ -1281,12 +1274,16 @@ let doc_fun_body_lem ctxt exp =
 
 let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let typ = typ_of_annot annot in
+  let arg_typs = match typ with
+    | Typ_aux (Typ_fn (arg_typs, typ_ret, _), _) -> arg_typs
+    | Typ_aux (_, l) -> raise (unreachable l __POS__ "Non-function type for funcl")
+  in
   let pat,guard,exp,(l,_) = destruct_pexp pexp in
   let ctxt =
     { early_ret = contains_early_return exp;
       bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ);
       top_env = env_of_annot annot } in
-  let pats, bind = untuple_args_pat (typ_of_annot annot) pat in
+  let pats, bind = untuple_args_pat pat arg_typs in
   let patspp = separate_map space (doc_pat_lem ctxt true) pats in
   let _ = match guard with
     | None -> ()
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 8f78b7dc..0b0a8305 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -123,6 +123,7 @@ let doc_nc =
     | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
     | NC_set (kid, ints) ->
        separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
+    | NC_app (id, nexps) -> string "where" ^^ space ^^ doc_id id ^^ parens (separate_map (comma ^^ space) doc_nexp nexps)
     | _ -> parens (nc0 nc)
   and nc0 (NC_aux (nc_aux, _) as nc) =
     match nc_aux with
@@ -134,7 +135,7 @@ let doc_nc =
     | _ -> atomic_nc nc
   in
   nc0
-  
+
 let rec doc_typ (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
@@ -354,6 +355,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_throw exp -> string "throw" ^^ parens (doc_exp exp)
   | E_try (exp, pexps) ->
      separate space [string "try"; doc_exp exp; string "catch"; doc_pexps pexps]
+  | E_return (E_aux (E_lit (L_aux (L_unit, _)), _)) -> string "return()"
   | E_return exp -> string "return" ^^ parens (doc_exp exp)
   | E_internal_return exp -> string "internal_return" ^^ parens (doc_exp exp)
   | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 ->
@@ -367,8 +369,8 @@ and doc_infix n (E_aux (e_aux, _) as exp) =
          match Bindings.find op !fixities with
          | (Infix, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]
          | (Infix, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r])
-         | (InfixL, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]
-         | (InfixL, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r])
+         | (InfixL, m) when m >= n -> separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r]
+         | (InfixL, m) -> parens (separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r])
          | (InfixR, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]
          | (InfixR, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r])
        with
@@ -585,6 +587,8 @@ let rec doc_def def = group (match def with
   | DEF_fixity (prec, n, id) ->
      fixities := Bindings.add id (prec, Big_int.to_int n) !fixities;
      separate space [doc_prec prec; doc_int n; doc_id id]
+  | DEF_constraint (id, kids, nc) ->
+     separate space [string "constraint"; doc_id id; parens (separate_map (comma ^^ space) doc_kid kids); equals; doc_nc nc]
   | DEF_overload (id, ids) ->
      separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
   ) ^^ hardline
diff --git a/src/rewrites.ml b/src/rewrites.ml
index cdb15717..c470d906 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4595,7 +4595,16 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
      (match res_pat with
      | RP_app (id',residual_args) ->
         if Id.compare id id' == 0 then
-          let res_pats' = subpats args residual_args in
+          let res_pats' =
+            (* Constructors that were specified without a return type might get
+               an extra tuple in their type; expand that here if necessary.
+               TODO: this should go away if we enforce proper arities. *)
+            match args, residual_args with
+            | [], [RP_any]
+            | _::_::_, [RP_any]
+              -> subpats args (List.map (fun _ -> RP_any) args)
+            | _,_ ->
+               subpats args residual_args in
           List.map (fun rps -> RP_app (id,rps)) res_pats'
         else [res_pat]
      | RP_any ->
diff --git a/src/sail.ml b/src/sail.ml
index 9526d6fe..c1c965fe 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -237,6 +237,9 @@ let options = Arg.align ([
   ( "-dmagic_hash",
     Arg.Set Initial_check.opt_magic_hash,
     " (debug) allow special character # in identifiers");
+  ( "-Xconstraint_synonyms",
+    Arg.Set Type_check.opt_constraint_synonyms,
+    " (extension) allow constraint synonyms");
   ( "-v",
     Arg.Set opt_print_version,
     " print version");
diff --git a/src/type_check.ml b/src/type_check.ml
index e1232046..cf1d8ef9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -69,6 +69,10 @@ let opt_no_effects = ref false
    assignments in l-expressions *)
 let opt_no_lexp_bounds_check = ref false
 
+(* opt_constraint_synonyms allows constraint synonyms as toplevel
+   definitions *)
+let opt_constraint_synonyms = ref false
+
 let depth = ref 0
 
 let rec indent n = match n with
@@ -163,6 +167,7 @@ and strip_n_constraint_aux = function
   | NC_set (kid, nums) -> NC_set (strip_kid kid, nums)
   | NC_or (nc1, nc2) -> NC_or (strip_n_constraint nc1, strip_n_constraint nc2)
   | NC_and (nc1, nc2) -> NC_and (strip_n_constraint nc1, strip_n_constraint nc2)
+  | NC_app (id, nexps) -> NC_app (strip_id id, List.map strip_nexp nexps)
   | NC_true -> NC_true
   | NC_false -> NC_false
 and strip_n_constraint = function
@@ -245,6 +250,7 @@ and nc_subst_nexp_aux l sv subst = function
      else set_nc
   | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
   | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
+  | NC_app (id, nexps) -> NC_app (id, List.map (nexp_subst sv subst) nexps)
   | NC_false -> NC_false
   | NC_true -> NC_true
 
@@ -336,6 +342,8 @@ let typquant_subst_kid_aux sv subst = function
 
 let typquant_subst_kid sv subst (TypQ_aux (typq, l)) = TypQ_aux (typquant_subst_kid_aux sv subst typq, l)
 
+let adding = Util.("Adding " |> darkgray |> clear)
+
 (**************************************************************************)
 (* 2. Environment                                                         *)
 (**************************************************************************)
@@ -378,6 +386,7 @@ module Env : sig
   val add_ret_typ : typ -> t -> t
   val add_typ_synonym : id -> (t -> typ_arg list -> typ) -> t -> t
   val get_typ_synonym : id -> t -> t -> typ_arg list -> typ
+  val add_constraint_synonym : id -> kid list -> n_constraint -> t -> t
   val add_num_def : id -> nexp -> t -> t
   val get_num_def : id -> t -> nexp
   val add_overloads : id -> id list -> t -> t
@@ -400,7 +409,11 @@ module Env : sig
   val polymorphic_undefineds : t -> bool
   val lookup_id : ?raw:bool -> id -> t -> typ lvar
   val fresh_kid : ?kid:kid -> t -> kid
+
   val expand_synonyms : t -> typ -> typ
+  val expand_constraint_synonyms : t -> n_constraint -> n_constraint
+  val expand_typquant_synonyms : t -> typquant -> typquant
+
   val canonicalize : t -> typ -> typ
   val base_typ_of : t -> typ -> typ
   val add_smt_op : id -> string -> t -> t
@@ -448,6 +461,7 @@ end = struct
       accessors : (typquant * typ) Bindings.t;
       externs : (string -> string option) Bindings.t;
       smt_ops : string Bindings.t;
+      constraint_synonyms : (kid list * n_constraint) Bindings.t;
       casts : id list;
       allow_casts : bool;
       allow_bindings : bool;
@@ -477,6 +491,7 @@ end = struct
       accessors = Bindings.empty;
       externs = Bindings.empty;
       smt_ops = Bindings.empty;
+      constraint_synonyms = Bindings.empty;
       casts = [];
       allow_bindings = true;
       allow_casts = true;
@@ -495,11 +510,11 @@ end = struct
 
   let get_typ_var kid env =
     try snd (KBindings.find kid env.typ_vars) with
-    | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid)
+    | Not_found -> typ_error (kid_loc kid) ("No type variable " ^ string_of_kid kid)
 
   let get_typ_var_loc kid env =
     try fst (KBindings.find kid env.typ_vars) with
-    | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid)
+    | Not_found -> typ_error (kid_loc kid) ("No type variable " ^ string_of_kid kid)
 
   let get_typ_vars env = KBindings.map snd env.typ_vars
   let get_typ_var_locs env = KBindings.map fst env.typ_vars
@@ -545,12 +560,12 @@ end = struct
     | Not_found -> []
 
   let add_overloads id ids env =
-    typ_print (lazy ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]"));
+    typ_print (lazy (adding ^ "overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]"));
     let existing = try Bindings.find id env.overloads with Not_found -> [] in
     { env with overloads = Bindings.add id (existing @ ids) env.overloads }
 
   let add_smt_op id str env =
-    typ_print (lazy ("Adding smt binding " ^ string_of_id id ^ " to " ^ str));
+    typ_print (lazy (adding ^ "smt binding " ^ string_of_id id ^ " to " ^ str));
     { env with smt_ops = Bindings.add id str env.smt_ops }
 
   let get_smt_op (Id_aux (_, l) as id) env =
@@ -597,8 +612,28 @@ end = struct
     then ()
     else typ_error (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
 
+  let rec expand_constraint_synonyms env (NC_aux (nc_aux, l) as nc) =
+    let expand = expand_constraint_synonyms env in
+    match nc_aux with
+    | NC_app (id, nexps) ->
+       begin
+         try
+           let kids, nc = Bindings.find id env.constraint_synonyms in
+           let nc = List.fold_left2 (fun nc kid nexp -> nc_subst_nexp kid (unaux_nexp nexp) nc) nc kids nexps in
+           expand nc
+         with Not_found -> typ_error l ("Could not expand constraint synonym in " ^ string_of_n_constraint nc)
+       end
+    | NC_and (nc1, nc2) -> NC_aux (NC_and (expand nc1, expand nc2), l)
+    | NC_or (nc1, nc2) -> NC_aux (NC_or (expand nc1, expand nc2), l)
+    | NC_true | NC_false | NC_set _ | NC_equal _ | NC_not_equal _ | NC_bounded_le _ | NC_bounded_ge _  -> nc
+
+  let expand_quant_item_synonyms env = function
+    | QI_aux (QI_id kopt, l) -> QI_aux (QI_id kopt, l)
+    | QI_aux (QI_const nc, l) -> QI_aux (QI_const (expand_constraint_synonyms env nc), l)
+
+  let expand_typquant_synonyms env = quant_map_items (expand_quant_item_synonyms env)
+
   let rec expand_synonyms env (Typ_aux (typ, l) as t) =
-    (* typ_debug (lazy ("Expanding synonyms for " ^ string_of_typ t)); *)
     match typ with
     | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l)
     | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l)
@@ -644,7 +679,7 @@ end = struct
        let kids = List.map rename_kid kids in
        let nc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid "syn#" kid)) nc) nc !rebindings in
        let typ = List.fold_left (fun typ kid -> typ_subst_nexp kid (Nexp_var (prepend_kid "syn#" kid)) typ) typ !rebindings in
-       typ_print (lazy ("Synonym existential: {" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}"));
+       typ_debug (lazy ("Synonym existential: {" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}"));
        let env = { env with constraints = nc :: env.constraints } in
        Typ_aux (Typ_exist (kids, nc, expand_synonyms env typ), l)
     | Typ_var v -> Typ_aux (Typ_var v, l)
@@ -718,7 +753,7 @@ end = struct
   (* Check if a type, order, n-expression or constraint is
      well-formed. Throws a type error if the type is badly formed. *)
   let rec wf_typ ?exs:(exs=KidSet.empty) env typ =
-    typ_debug (lazy ("Well-formed " ^ string_of_typ typ));
+    typ_debug (lazy ("well-formed " ^ string_of_typ typ));
     let (Typ_aux (typ_aux, l)) = expand_synonyms env typ in
     match typ_aux with
     | Typ_id id when bound_typ_id env id ->
@@ -755,7 +790,8 @@ end = struct
     | Typ_arg_nexp nexp -> wf_nexp ~exs:exs env nexp
     | Typ_arg_typ typ -> wf_typ ~exs:exs env typ
     | Typ_arg_order ord -> wf_order env ord
-  and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l)) =
+  and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) =
+    typ_debug (lazy ("well-formed nexp " ^ string_of_nexp nexp));
     match nexp_aux with
     | Nexp_id _ -> ()
     | Nexp_var kid when KidSet.mem kid exs -> ()
@@ -765,7 +801,7 @@ end = struct
          | BK_int -> ()
          | kind -> typ_error l ("Constraint is badly formed, "
                                 ^ string_of_kid kid ^ " has kind "
-                                ^ string_of_base_kind_aux kind ^ " but should have kind Nat")
+                                ^ string_of_base_kind_aux kind ^ " but should have kind Int")
        end
     | Nexp_constant _ -> ()
     | Nexp_app (id, nexps) ->
@@ -787,15 +823,28 @@ end = struct
                                 ^ string_of_base_kind_aux kind ^ " but should have kind Order")
        end
     | Ord_inc | Ord_dec -> ()
-  and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc, _)) =
-    match nc with
+  and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc_aux, l) as nc) =
+    typ_debug (lazy ("well-formed constraint " ^ string_of_n_constraint nc));
+    match nc_aux with
     | NC_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
     | NC_not_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
     | NC_bounded_ge (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
     | NC_bounded_le (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
-    | NC_set (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *)
+    | NC_set (kid, _) when KidSet.mem kid exs -> ()
+    | NC_set (kid, _) -> begin
+        match get_typ_var kid env with
+        | BK_int -> ()
+        | kind -> typ_error l ("Set constraint is badly formed, "
+                               ^ string_of_kid kid ^ " has kind "
+                               ^ string_of_base_kind_aux kind ^ " but should have kind Int")
+      end
     | NC_or (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
     | NC_and (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
+    | NC_app (id, nexps) ->
+       if not (Bindings.mem id env.constraint_synonyms) then
+         typ_error l ("Constraint synonym " ^ string_of_id id ^ " is not defined")
+       else ();
+       List.iter (wf_nexp ~exs:exs env) nexps
     | NC_true | NC_false -> ()
 
   let counter = ref 0
@@ -834,7 +883,8 @@ end = struct
   let rec update_val_spec id (typq, typ) env =
     begin
       let typ = expand_synonyms env typ in
-      typ_print (lazy ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind (typq, typ)));
+      let typq = expand_typquant_synonyms env typq in
+      typ_print (lazy (adding ^ "val spec " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
       let env = match typ with
         | Typ_aux (Typ_bidir (typ1, typ2), _) -> add_mapping id (typq, typ1, typ2) env
         | _ -> env
@@ -854,7 +904,7 @@ end = struct
         env
   and add_mapping id (typq, typ1, typ2) env =
     begin
-      typ_print (lazy ("Adding mapping " ^ string_of_id id));
+      typ_print (lazy (adding ^ "mapping " ^ string_of_id id));
       let forwards_id = mk_id (string_of_id id ^ "_forwards") in
       let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in
       let backwards_id = mk_id (string_of_id id ^ "_backwards") in
@@ -912,7 +962,7 @@ end = struct
     then typ_error (id_loc id) ("Cannot create enum " ^ string_of_id id ^ ", type name is already bound")
     else
       begin
-        typ_print (lazy ("Adding enum " ^ string_of_id id));
+        typ_print (lazy (adding ^ "enum " ^ string_of_id id));
         { env with enums = Bindings.add id (IdSet.of_list ids) env.enums }
       end
 
@@ -930,7 +980,7 @@ end = struct
     then typ_error (id_loc id) ("Cannot create record " ^ string_of_id id ^ ", type name is already bound")
     else
       begin
-        typ_print (lazy ("Adding record " ^ string_of_id id));
+        typ_print (lazy (adding ^ "record " ^ string_of_id id));
         let rec record_typ_args = function
           | [] -> []
           | ((QI_aux (QI_id kopt, _)) :: qis) when is_nat_kopt kopt ->
@@ -947,7 +997,7 @@ end = struct
         in
         let fold_accessors accs (typ, fid) =
           let acc_typ = mk_typ (Typ_fn ([rectyp], typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
-          typ_print (lazy (indent 1 ^ "Adding accessor " ^ string_of_id id ^ "." ^ string_of_id fid ^ " :: " ^ string_of_bind (typq, acc_typ)));
+          typ_print (lazy (indent 1 ^ adding ^ "accessor " ^ string_of_id id ^ "." ^ string_of_id fid ^ " :: " ^ string_of_bind (typq, acc_typ)));
           Bindings.add (field_name id fid) (typq, acc_typ) accs
         in
         { env with records = Bindings.add id (typq, fields) env.records;
@@ -987,19 +1037,19 @@ end = struct
       if Bindings.mem id env.top_val_specs then
         typ_error (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name")
       else ();
-      typ_print (lazy ("Adding local binding " ^ string_of_id id ^ " :: " ^ string_of_mtyp mtyp));
+      typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp));
       { env with locals = Bindings.add id mtyp env.locals }
     end
 
   let add_variant id variant env =
     begin
-      typ_print (lazy ("Adding variant " ^ string_of_id id));
+      typ_print (lazy (adding ^ "variant " ^ string_of_id id));
       { env with variants = Bindings.add id variant env.variants }
     end
 
   let add_union_id id bind env =
     begin
-      typ_print (lazy ("Adding union identifier binding " ^ string_of_id id ^ " :: " ^ string_of_bind bind));
+      typ_print (lazy (adding ^ "union identifier " ^ string_of_id id ^ " : " ^ string_of_bind bind));
       { env with union_ids = Bindings.add id bind env.union_ids }
     end
 
@@ -1008,7 +1058,7 @@ end = struct
     | Not_found -> fun typ -> typ
 
   let add_flow id f env =
-    typ_print (lazy ("Adding flow constraints for " ^ string_of_id id));
+    typ_print (lazy (adding ^ "flow constraints for " ^ string_of_id id));
     { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow }
 
   let remove_flow id env =
@@ -1046,7 +1096,7 @@ end = struct
     then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound")
     else
       begin
-        typ_print (lazy ("Adding register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ));
+        typ_print (lazy (adding ^ "register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ));
         { env with registers = Bindings.add id (reff, weff, typ) env.registers }
       end
 
@@ -1072,10 +1122,10 @@ end = struct
 
   let add_typ_var l kid k env =
     if KBindings.mem kid env.typ_vars
-    then typ_error (kid_loc kid) ("Kind identifier " ^ string_of_kid kid ^ " is already bound")
+    then typ_error (kid_loc kid) ("type variable " ^ string_of_kid kid ^ " is already bound")
     else
       begin
-        typ_print (lazy ("Adding kind identifier " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k));
+        typ_print (lazy (adding ^ "type variable " ^ string_of_kid kid ^ " : " ^ string_of_base_kind_aux k));
         { env with typ_vars = KBindings.add kid (l, k) env.typ_vars }
       end
 
@@ -1084,7 +1134,7 @@ end = struct
     then typ_error (id_loc id) ("Num identifier " ^ string_of_id id ^ " is already bound")
     else
       begin
-        typ_print (lazy ("Adding Num identifier " ^ string_of_id id ^ " :: " ^ string_of_nexp nexp));
+        typ_print (lazy (adding ^ "Num identifier " ^ string_of_id id ^ " : " ^ string_of_nexp nexp));
         { env with num_defs = Bindings.add id nexp env.num_defs }
       end
 
@@ -1099,7 +1149,8 @@ end = struct
     match nc_aux with
     | NC_true -> env
     | _ ->
-       typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr));
+       let constr = expand_constraint_synonyms env constr in
+       typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr));
        { env with constraints = constr :: env.constraints }
 
   let get_ret_typ env = env.ret_typ
@@ -1114,7 +1165,7 @@ end = struct
   let no_bindings env = { env with allow_bindings = false }
 
   let add_cast cast env =
-    typ_print (lazy ("Adding cast " ^ string_of_id cast));
+    typ_print (lazy (adding ^ "cast " ^ string_of_id cast));
     { env with casts = cast :: env.casts }
 
   let add_typ_synonym id synonym env =
@@ -1122,12 +1173,22 @@ end = struct
     then typ_error (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists")
     else
       begin
-        typ_print (lazy ("Adding type synonym " ^ string_of_id id));
+        typ_print (lazy (adding ^ "type synonym " ^ string_of_id id));
         { env with typ_synonyms = Bindings.add id synonym env.typ_synonyms }
       end
 
   let get_typ_synonym id env = Bindings.find id env.typ_synonyms
 
+  let add_constraint_synonym id kids nc env =
+    if Bindings.mem id env.constraint_synonyms
+    then typ_error (id_loc id) ("Constraint synonym " ^ string_of_id id ^ " already exists")
+    else
+      begin
+        typ_print (lazy (adding ^ "constraint synonym " ^ string_of_id id));
+        wf_constraint ~exs:(KidSet.of_list kids) env nc;
+        { env with constraint_synonyms = Bindings.add id (kids, nc) env.constraint_synonyms }
+      end
+
   let get_default_order env =
     match env.default_order with
     | None -> typ_error Parse_ast.Unknown ("No default order has been set")
@@ -1186,6 +1247,10 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t =
   | TypQ_aux (TypQ_no_forall, _) -> env
   | TypQ_aux (TypQ_tq quants, _) -> List.fold_left add_quant_item env quants
 
+let expand_bind_synonyms l env (typq, typ) =
+  Env.expand_typquant_synonyms env typq, Env.expand_synonyms (add_typquant l typq env) typ
+
+
 (* Create vectors with the default order from the environment *)
 
 let default_order_error_string =
@@ -1356,6 +1421,7 @@ let rec nc_constraint env var_of (NC_aux (nc, l)) =
                     (List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant i)) ints)
   | NC_or (nc1, nc2) -> Constraint.disj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2)
   | NC_and (nc1, nc2) -> Constraint.conj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2)
+  | NC_app (id, nexps) -> raise (Reporting_basic.err_unreachable l __POS__ "constraint synonym reached smt generation")
   | NC_false -> Constraint.literal false
   | NC_true -> Constraint.literal true
 
@@ -2034,7 +2100,6 @@ let rec instantiate_quants quants kid uvar = match quants with
           if is_typ_kid kid kinded_id
           then instantiate_quants quants kid uvar
           else quant :: instantiate_quants quants kid uvar
-       | _ -> typ_error Parse_ast.Unknown "Cannot instantiate quantifier"
      end
   | ((QI_aux (QI_const nc, l)) :: quants) ->
      begin
@@ -2307,7 +2372,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
             let checked_msg = crule check_exp env assert_msg string_typ in
             let env = match assert_constraint env true constr_exp with
               | Some nc ->
-                 typ_print (lazy ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert"));
+                 typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint nc ^ " for assert"));
                  Env.add_constraint nc env
               | None -> env
             in
@@ -2739,7 +2804,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
        let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with
          | Typ_tup typs -> typs
          | _ -> [typ]
-       in       
+       in
        match Env.expand_synonyms env ctor_typ with
        | Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _) ->
           begin
@@ -4382,31 +4447,26 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md
    context. We have to destructure the various kinds of val specs, but
    the difference is irrelevant for the typechecker. *)
 let check_val_spec env (VS_aux (vs, (l, _))) =
-  let annotate vs typ eff = DEF_spec (VS_aux (vs, (l, Some ((env,typ,eff), None)))) in
-  let (id, quants, typ, env) = match vs with
-    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _) as typschm, id, ext_opt, is_cast) ->
-       typ_debug (lazy ("VS typschm: " ^ string_of_id id ^ ", " ^ string_of_typschm typschm));
+  let annotate vs typ eff = DEF_spec (VS_aux (vs, (l, Some ((env, typ, eff), None)))) in
+  let vs, id, typq, typ, env = match vs with
+    | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, ext_opt, is_cast) ->
+       typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm));
        let env = match (ext_opt "smt", ext_opt "#") with
          | Some op, None -> Env.add_smt_op id op env
          | _, _ -> env
        in
-       Env.wf_typ (add_typquant l quants env) typ;
-       typ_debug (lazy "CHECKED WELL-FORMED VAL SPEC");
-       let env =
-       (* match ext_opt with
-         | None -> env
-         | Some ext -> *)
-         Env.add_extern id ext_opt env
-       in
+       let env = Env.add_extern id ext_opt env in
        let env = if is_cast then Env.add_cast id env else env in
-       (id, quants, typ, env)
+       let typq, typ = expand_bind_synonyms ts_l env (typq, typ) in
+       let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in
+       (vs, id, typq, typ, env)
   in
   let eff =
     match typ with
-    | Typ_aux (Typ_fn (_,_,eff),_) -> eff
+    | Typ_aux (Typ_fn (_, _, eff), _) -> eff
     | _ -> no_effect
   in
-  [annotate vs typ eff], Env.add_val_spec id (quants, Env.expand_synonyms (add_typquant l quants env) typ) env
+  [annotate vs typ eff], Env.add_val_spec id (typq, typ) env
 
 let check_default env (DT_aux (ds, l)) =
   match ds with
@@ -4521,6 +4581,10 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
   | DEF_fixity (prec, n, op) -> [DEF_fixity (prec, n, op)], env
   | DEF_fundef fdef -> check_fundef env fdef
   | DEF_mapdef mdef -> check_mapdef env mdef
+  | DEF_constraint (id, kids, nc) when !opt_constraint_synonyms ->
+     [], Env.add_constraint_synonym id kids nc env
+  | DEF_constraint (id, _, _) ->
+     typ_error (id_loc id) "Use -Xconstraint_synonyms to enable constraint synonyms"
   | DEF_internal_mutrec fdefs ->
      let defs = List.concat (List.map (fun fdef -> fst (check_fundef env fdef)) fdefs) in
      let split_fundef (defs, fdefs) def = match def with
diff --git a/src/type_check.mli b/src/type_check.mli
index 0e0137db..93f5302a 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -67,6 +67,10 @@ val opt_no_effects : bool ref
    assignments in l-expressions. *)
 val opt_no_lexp_bounds_check : bool ref
 
+(** [opt_constraint_synonyms] allows constraint synonyms as toplevel
+   definitions *)
+val opt_constraint_synonyms : bool ref
+
 (** {2 Type errors} *)
 
 type type_error =
diff --git a/src/util.ml b/src/util.ml
index b54c13d4..e0366fe7 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -408,6 +408,7 @@ let termcode n =
 
 let bold str = termcode 1 ^ str
 
+let darkgray str = termcode 90 ^ str
 let red str = termcode 91 ^ str
 let green str = termcode 92 ^ str
 let yellow str = termcode 93 ^ str
diff --git a/src/util.mli b/src/util.mli
index bb7aa70d..eb4b4bd2 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -239,6 +239,7 @@ val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list)
 (* Terminal color codes *)
 val termcode : int -> string
 val bold : string -> string
+val darkgray : string -> string
 val green : string -> string
 val red : string -> string
 val red_bg : string -> string
diff --git a/test/riscv/run_tests.sh b/test/riscv/run_tests.sh
index 369e72b2..3875105f 100755
--- a/test/riscv/run_tests.sh
+++ b/test/riscv/run_tests.sh
@@ -67,7 +67,7 @@ for test in $DIR/tests/*.elf; do
     fi
 done
 
-if make -C $SAILDIR/riscv riscv_c;
+if make -C $SAILDIR/riscv riscv_sim;
 then
     green "Building RISCV specification to C" "ok"
 else
@@ -75,8 +75,7 @@ else
 fi
 
 for test in $DIR/tests/*.elf; do
-    $SAILDIR/sail -elf $test -o ${test%.elf}.bin 2> /dev/null;
-    if timeout 5 $SAILDIR/riscv/riscv_c --binary=0x1000,reset_vec.bin --image=${test%.elf}.bin > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout
+    if timeout 5 $SAILDIR/riscv/riscv_sim $test > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout
     then
 	green "$(basename $test)_c" "ok"
     else
@@ -84,23 +83,23 @@ for test in $DIR/tests/*.elf; do
     fi
 done
 
-printf "Interpreting RISCV specification...\n"
-
-for test in $DIR/tests/*.elf; do
-    if {
-        timeout 30 $SAILDIR/sail -i $SAILDIR/riscv/riscv_all.sail $SAILDIR/riscv/main.sail > ${test%.elf}.iout 2>&1 <<EOF
-:bin 0x1000 $SAILDIR/riscv/reset_vec.bin
-:elf $test
-main()
-:run
-EOF
-    } && grep -q SUCCESS ${test%.elf}.iout
-    then
-        green "$(basename $test)_interpreter" "ok"
-    else
-        red "$(basename $test)_interpreter" "fail"
-    fi
-done
+# printf "Interpreting RISCV specification...\n"
+
+# for test in $DIR/tests/*.elf; do
+#     if {
+#         timeout 30 $SAILDIR/sail -i $SAILDIR/riscv/riscv_all.sail $SAILDIR/riscv/main.sail > ${test%.elf}.iout 2>&1 <<EOF
+# :bin 0x1000 $SAILDIR/riscv/reset_vec.bin
+# :elf $test
+# main()
+# :run
+# EOF
+#     } && grep -q SUCCESS ${test%.elf}.iout
+#     then
+#         green "$(basename $test)_interpreter" "ok"
+#     else
+#         red "$(basename $test)_interpreter" "fail"
+#     fi
+# done
 
 finish_suite "RISCV tests"
 
diff --git a/test/riscv/tests/.gitignore b/test/riscv/tests/.gitignore
index f47cb204..72a5e441 100644
--- a/test/riscv/tests/.gitignore
+++ b/test/riscv/tests/.gitignore
@@ -1 +1,2 @@
 *.out
+*.cout
diff --git a/test/typecheck/pass/constraint_sym.sail b/test/typecheck/pass/constraint_sym.sail
new file mode 100644
index 00000000..6d212e40
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v1.expect b/test/typecheck/pass/constraint_sym/v1.expect
new file mode 100644
index 00000000..71fd6f30
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v1.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v1.sail", line 3, character 23 to line 3, character 24
+
+constraint Size('n) = 'm in {32, 64}
+
+No type variable 'm
diff --git a/test/typecheck/pass/constraint_sym/v1.sail b/test/typecheck/pass/constraint_sym/v1.sail
new file mode 100644
index 00000000..4421ee77
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v1.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'm in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v2.expect b/test/typecheck/pass/constraint_sym/v2.expect
new file mode 100644
index 00000000..58a0f416
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v2.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v2.sail", line 7, character 22 to line 7, character 34
+
+val foo : forall 'n, where Siz('n). int('n) -> unit
+
+Constraint synonym Siz is not defined
diff --git a/test/typecheck/pass/constraint_sym/v2.sail b/test/typecheck/pass/constraint_sym/v2.sail
new file mode 100644
index 00000000..1d98e3e4
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v2.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Siz('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v3.expect b/test/typecheck/pass/constraint_sym/v3.expect
new file mode 100644
index 00000000..ab4526dc
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v3.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v3.sail", line 7, character 42 to line 7, character 43
+
+val foo : forall ('n : Type), where Size('n). int('n) -> unit
+
+Constraint is badly formed, 'n has kind Type but should have kind Int
diff --git a/test/typecheck/pass/constraint_sym/v3.sail b/test/typecheck/pass/constraint_sym/v3.sail
new file mode 100644
index 00000000..886acbe4
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v3.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall ('n : Type), where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v4.expect b/test/typecheck/pass/constraint_sym/v4.expect
new file mode 100644
index 00000000..c8374baf
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v4.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v4.sail", line 2, character 12 to line 2, character 15
+
+constraint Size('n) = 'n in {32, 64}
+
+Use -Xconstraint_synonyms to enable constraint synonyms
diff --git a/test/typecheck/pass/constraint_sym/v4.sail b/test/typecheck/pass/constraint_sym/v4.sail
new file mode 100644
index 00000000..96bf5e82
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v4.sail
@@ -0,0 +1,6 @@
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index 8014f88a..c7e06dc7 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -2,4 +2,4 @@ Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, ch
 
 val test : forall 'size. atom('size) -> unit
 
-Kind identifier 'size is already bound
+type variable 'size is already bound