Merge remote-tracking branch 'origin/sail2' into polymorphic_variants

30 files changed, 794 insertions, 256 deletions

diff --git a/INSTALL.md b/INSTALL.md
index 7a8a387b..51b97e81 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -1,32 +1,42 @@
-Installing Sail on Ubuntu
+Installing Sail on Ubuntu and macOS
 =========================
 
 This note lists the commands needed to get Sail and all dependencies
-working on a new Ubuntu install. I recently (2018-02-17) tested these
-on Xubuntu 16.04 LTS in a virtual machine, so they should
+working on a new Ubuntu install or macOS. We have recently (2018-02-17) tested these
+on Xubuntu 16.04 LTS in a virtual machine and on macOS Sierre 10.12.6, so they should
 work. Hopefully this will be useful as a reference.
 
 Basics
 ------
 
 First we need some basic packages if they're not already installed.
+
+For Ubuntu:
 ```
 sudo apt-get install build-essential git
 ```
 
+For macOS: compilers and supporting utilities are called Xcode instead of build-essential. First, download Xcode from the Mac App Store, and then run the following in the terminal:
+```
+xcode-select --install
+```
+git can be installed using ```brew install git```
+
 OCaml and sail expect some packages. m4 is for OPAM, libgmp-dev is for
 zarith which most of our tools rely on. Sail uses Z3 as a constraint
 solver.
 ```
 sudo apt-get install m4 libgmp-dev z3
 ```
+For macOS: ```brew install m4 gmp z3``` 
 
 OCaml and OPAM
 --------------
 
 Install OPAM. Either directly from [https://opam.ocaml.org] or from
-the package manager - both should work, but I used the install script
-from the website. This should install OCaml 4.05.
+the package manager - both should work, but we used the install script
+from the website. This should install OCaml 4.05. Don't forget to run
+```opam init``` after installing OPAM.
 
 We now need ocamlbuild, zarith, and menhir from OPAM.
 ```
@@ -47,6 +57,8 @@ cd ott
 make
 cd ..
 ```
+Sail depends on ott, so add the ott executable (``` path-to-ott/bin```) in the $PATH.
+
 
 Lem
 ---
@@ -65,7 +77,7 @@ cd ../..
 Linksem
 -------
 
-Make sure the LEMLIB environment variable is set correctly before building linksem. This should be the library directory within the checked-out lem directory.
+Before installing linksem, we are required to set the LEMLIB environment variable and to put the lem executable in $PATH. LEMLIB should be the library directory within the checked-out lem directory (i.e. ```path-to-lem/library/```). Next, install linksem as
 
 ```
 git clone git@github.com:rems-project/linksem.git
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 65109485..a1bddec1 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -6,11 +6,11 @@ $include <arith.sail>
 
 type bits ('n : Int) = vector('n, dec, bit)
 
-val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool
+val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anything", c: "eq_bit", coq: "eq_bit"} : (bit, bit) -> bool
 
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec", c: "eq_bits"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
 
-val eq_string = {ocaml: "eq_string", lem: "eq", c: "eq_string"} : (string, string) -> bool
+val eq_string = {ocaml: "eq_string", lem: "eq", c: "eq_string", coq: "generic_eq"} : (string, string) -> bool
 
 val eq_real = {ocaml: "eq_real", lem: "eq", c: "eq_real"} : (real, real) -> bool
 
@@ -18,12 +18,13 @@ val eq_anything = {
   ocaml: "(fun (x, y) -> x = y)",
   interpreter: "eq_anything",
   lem: "eq",
-  c: "eq_anything"
+  c: "eq_anything",
+  coq: "generic_eq"
 } : forall ('a : Type). ('a, 'a) -> bool
 
 val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
-val vector_length = {ocaml: "length", lem: "length_list", c: "length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
-val list_length = {ocaml: "length", lem: "length_list", c: "length"} : forall ('a : Type). list('a) -> int
+val vector_length = {ocaml: "length", lem: "length_list", c: "length", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
+val list_length = {ocaml: "length", lem: "length_list", c: "length", coq: "length_list"} : forall ('a : Type). list('a) -> int
 
 overload length = {bitvector_length, vector_length, list_length}
 
@@ -32,7 +33,8 @@ overload operator == = {eq_bit, eq_vec, eq_string, eq_real, eq_anything}
 val vector_subrange_A = {
   ocaml: "subrange",
   lem: "subrange_vec_dec",
-  c: "vector_subrange"
+  c: "vector_subrange",
+  coq: "subrange_vec_dec"
 } : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
   (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
 
@@ -48,19 +50,22 @@ overload vector_subrange = {vector_subrange_A, vector_subrange_B}
 val bitvector_access_A = {
   ocaml: "access",
   lem: "access_vec_dec",
-  c: "vector_access"
+  c: "vector_access",
+  coq: "access_vec_dec"
 } : forall ('n : Int) ('m : Int), 0 <= 'm < 'n. (bits('n), atom('m)) -> bit
 
 val bitvector_access_B = {
   ocaml: "access",
   lem: "access_vec_dec",
-  c: "vector_access"
+  c: "vector_access",
+  coq: "access_vec_dec"
 } : forall ('n : Int). (bits('n), int) -> bit
 
 val vector_access_A = {
   ocaml: "access",
   lem: "access_list_dec",
-  c: "vector_access"
+  c: "vector_access",
+  coq: "vec_access_dec"
 } : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a
 
 val vector_access_B = {
@@ -71,10 +76,10 @@ val vector_access_B = {
 
 overload vector_access = {bitvector_access_A, bitvector_access_B, vector_access_A, vector_access_B}
 
-val bitvector_update_B = {ocaml: "update", lem: "update_vec_dec", c: "vector_update"} : forall 'n.
+val bitvector_update_B = {ocaml: "update", lem: "update_vec_dec", c: "vector_update", coq: "update_vec_dec"} : forall 'n.
   (bits('n), int, bit) -> bits('n)
 
-val vector_update_B = {ocaml: "update", lem: "update_list_dec", c: "vector_update"} : forall 'n ('a : Type).
+val vector_update_B = {ocaml: "update", lem: "update_list_dec", c: "vector_update", coq: "vec_update_dec"} : forall 'n ('a : Type).
   (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
 
 overload vector_update = {bitvector_update_B, vector_update_B}
@@ -82,16 +87,17 @@ overload vector_update = {bitvector_update_B, vector_update_B}
 val vector_update_subrange = {
   ocaml: "update_subrange",
   lem: "update_subrange_vec_dec",
-  c: "vector_update_subrange"
+  c: "vector_update_subrange",
+  coq: "update_subrange_vec_dec"
 } : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 val vcons : forall ('n : Int) ('a : Type).
   ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a)
 
-val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 
-val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
+val vector_concat = {ocaml: "append", lem: "append_list", coq: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
   (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
 
 overload append = {bitvector_concat, vector_concat}
@@ -99,7 +105,8 @@ overload append = {bitvector_concat, vector_concat}
 val not_vec = {
   ocaml: "not_vec",
   lem: "not_vec",
-  c: "not_bits"
+  c: "not_bits",
+  coq: "not_vec"
 } : forall 'n. bits('n) -> bits('n)
 
 overload ~ = {not_bool, not_vec}
@@ -108,7 +115,7 @@ val neq_vec = {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
 
 function neq_vec (x, y) = not_bool(eq_vec(x, y))
 
-val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool
+val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
 
 function neq_anything (x, y) = not_bool(x == y)
 
@@ -116,7 +123,7 @@ overload operator != = {neq_vec, neq_anything}
 
 val builtin_and_vec = {ocaml: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val and_vec = {lem: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 function and_vec (xs, ys) = builtin_and_vec(xs, ys)
 
@@ -124,7 +131,7 @@ overload operator & = {and_bool, and_vec}
 
 val builtin_or_vec = {ocaml: "or_vec", c: "or_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val or_vec = {lem: "or_vec", c: "or_bits"}: forall 'n. (bits('n), bits('n)) -> bits('n)
+val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec"}: forall 'n. (bits('n), bits('n)) -> bits('n)
 
 function or_vec (xs, ys) = builtin_or_vec(xs, ys)
 
@@ -134,7 +141,8 @@ val UInt = {
   ocaml: "uint",
   lem: "uint",
   interpreter: "uint",
-  c: "sail_unsigned"
+  c: "sail_unsigned",
+  coq: "uint"
 } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
 
 val SInt = {
@@ -184,10 +192,11 @@ val putchar = {
   ocaml: "putchar",
   lem: "putchar",
   interpreter: "putchar",
-  c: "sail_putchar"
+  c: "sail_putchar",
+  coq: "putchar"
 } : int -> unit
 
-val concat_str = {ocaml: "concat_str", lem: "stringAppend", c: "concat_str"} : (string, string) -> string
+val concat_str = {ocaml: "concat_str", lem: "stringAppend", c: "concat_str", coq: "String.append"} : (string, string) -> string
 
 val DecStr = "dec_str" : int -> string
 
@@ -202,7 +211,8 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
 val xor_vec = {
   ocaml: "xor_vec",
   lem: "xor_vec",
-  c: "xor_bits"
+  c: "xor_bits",
+  coq: "xor_vec"
 } : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val int_power = {lem: "pow"} : (int, int) -> int
@@ -214,13 +224,15 @@ overload operator ^ = {xor_vec, int_power, real_power}
 val add_vec = {
   ocaml: "add_vec",
   lem: "add_vec",
-  c: "add_bits"
+  c: "add_bits",
+  coq: "add_vec"
 } : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val add_vec_int = {
   ocaml: "add_vec_int",
   lem: "add_vec_int",
-  c: "add_bits_int"
+  c: "add_bits_int",
+  coq: "add_vec_int"
 } : forall 'n. (bits('n), int) -> bits('n)
 
 val add_real = {ocaml: "add_real", lem: "realAdd", c: "add_real"} : (real, real) -> real
@@ -232,7 +244,8 @@ val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) ->
 val sub_vec_int = {
   ocaml: "sub_vec_int",
   lem: "sub_vec_int",
-  c: "sub_bits_int"
+  c: "sub_bits_int",
+  coq: "sub_vec_int"
 } : forall 'n. (bits('n), int) -> bits('n)
 
 val sub_real = {ocaml: "sub_real", lem: "realMinus", c: "sub_real"} : (real, real) -> real
@@ -277,11 +290,11 @@ val quotient_nat = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int"} : (nat,
 
 val quotient_real = {ocaml: "quotient_real", lem: "realDiv", c: "div_real"} : (real, real) -> real
 
-val quotient = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int"} : (int, int) -> int
+val quotient = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
 
 overload operator / = {quotient_nat, quotient, quotient_real}
 
-val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
+val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
 
 overload operator % = {modulus}
 
@@ -289,11 +302,11 @@ val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real"} : int -> rea
 
 val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat
 
-val min_int = {ocaml: "min_int", lem: "min", c: "min_int"} : (int, int) -> int
+val min_int = {ocaml: "min_int", lem: "min", c: "min_int", coq: "min_int"} : (int, int) -> int
 
 val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat
 
-val max_int = {ocaml: "max_int", lem: "max", c: "max_int"} : (int, int) -> int
+val max_int = {ocaml: "max_int", lem: "max", c: "max_int", coq: "min_int"} : (int, int) -> int
 
 overload min = {min_nat, min_int}
 
diff --git a/doc/tutorial.tex b/doc/tutorial.tex
index d325dc4d..5a362c28 100644
--- a/doc/tutorial.tex
+++ b/doc/tutorial.tex
@@ -69,7 +69,7 @@ defined in the Sail library. These declarations work much like FFI
 bindings in many programming languages---in Sail we provide the
 \ll{val} declaration, except rather than giving a function body we
 supply a string used to identify the external operator in each
-backend. For example, we could link the \ll{>>} operator with the
+backend. For example, we could link the \ll{<<} operator with the
 \verb|shiftl| primitive as \mrbzeightoperatorzzerozIzIznine If the
 external function has the same name as the sail function, such as
 \ll{shiftl = "shiftl"}, then we can use the shorthand syntax
@@ -419,7 +419,7 @@ match ys {
 
 Like OCaml, Sail also supports naming parts of patterns using the
 \ll{as} keyword. For example, in the above list pattern we could bind
-the entire list as ys as follows:
+the entire list as zs as follows:
 \begin{lstlisting}
 match ys {
   x :: xs as zs => print("cons with as pattern"),
@@ -751,7 +751,7 @@ operator names. Operators may be left, right, or non-associative, and
 there are 10 different precedence levels, ranging from 0 to 9, with 9
 binding the tightest. To declare the precedence of an operator, we use a fixity declaration like:
 \begin{lstlisting}
-infix <=_u 4
+infix 4 <=_u
 \end{lstlisting}
 For left or right associative operators, we'd use the keywords
 \ll{infixl} or \ll{infixr} respectively. An operator can be used
@@ -869,7 +869,7 @@ val div2 : (int, int) -> option(int)
 \end{lstlisting}
 The first guarantees that if the first argument is greater than or
 equal to zero, and the second argument is greater than zero, then the
-result will be greater than or not equal to zero. If we overload these
+result will be greater than or equal to zero. If we overload these
 definitions as
 \begin{lstlisting}
 overload operator / = {div1, div2}
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index dc851efd..b9d7ab06 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -54,6 +54,9 @@
   (kill-all-local-variables)
   (set-syntax-table sail2-mode-syntax-table)
   (setq font-lock-defaults '(sail2-font-lock-keywords))
+  (setq comment-start-skip "\\(//+\\|/\\*+\\)\\s *")
+  (setq comment-start "/*")
+  (setq comment-end "*/")
   (setq major-mode 'sail2-mode)
   (setq mode-name "Sail2")
   (run-hooks 'sail2-mode-hook))
diff --git a/lib/coq/Makefile b/lib/coq/Makefile
index 97869e3c..99321aae 100644
--- a/lib/coq/Makefile
+++ b/lib/coq/Makefile
@@ -1,6 +1,6 @@
 BBV_DIR=../../../bbv/theories
 
-SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v
+SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v  Sail2_string.v
 
 COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv
 
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index c98e2926..0b3a2cd8 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -115,3 +115,13 @@ let rec untilM vars cond body =
   write_reg r1 r1_v >> write_reg r2 r2_v*)
 
 *)
+
+(* If we need to build an existential after a monadic operation, assume that
+   we can do it entirely from the type. *)
+
+Definition build_ex_m {rv e} {T:Type} (x:monad rv T e) {P:T -> Prop} `{H:forall x, ArithFact (P x)} : monad rv {x : T & ArithFact (P x)} e :=
+  x >>= fun y => returnm (existT _ y (H y)).
+
+Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad rv Z e :=
+  x >>= fun y => returnm (projT1 y).
+
diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
new file mode 100644
index 00000000..9ca9cb67
--- /dev/null
+++ b/lib/coq/Sail2_string.v
@@ -0,0 +1,35 @@
+Require Import Sail2_values.
+
+Definition string_sub (s : string) (start : Z) (len : Z) : string :=
+  String.substring (Z.to_nat start) (Z.to_nat len) s.
+
+Definition string_startswith s expected :=
+  let prefix := String.substring 0 (String.length expected) s in
+  generic_eq prefix expected.
+
+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_length s : {n : Z & ArithFact (n >= 0)} :=
+ build_ex (Z.of_nat (String.length s)).
+
+Definition string_append := String.append.
+
+(* TODO: maybe_int_of_prefix, maybe_int_of_string *)
+
+Fixpoint n_leading_spaces (s:string) : nat :=
+  match s with
+  | EmptyString => 0
+  | String " " t => S (n_leading_spaces t)
+  | _ => 0
+  end.
+
+Definition opt_spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) :=
+  Some (tt, build_ex (Z.of_nat (n_leading_spaces s))).
+
+Definition spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) :=
+  match n_leading_spaces s with
+  | O => None
+  | S n => Some (tt, build_ex (Z.of_nat (S n)))
+  end.
\ No newline at end of file
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 0ce6134f..7766e6af 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -21,7 +21,7 @@ Lemma use_ArithFact {P} `(ArithFact P) : P.
 apply fact.
 Defined.
 
-Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} :=
+Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} :=
   existT _ n H.
 
 Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
@@ -54,7 +54,10 @@ Instance Decidable_eq_from_dec {T:Type} (eqdec: forall x y : T, {x = y} + {x <>
   Decidable_witness := proj1_sig (bool_of_sumbool (eqdec x y))
 }.
 destruct (eqdec x y); simpl; split; congruence.
-Qed.
+Defined.
+
+Instance Decidable_eq_string : forall (x y : string), Decidable (x = y) :=
+  Decidable_eq_from_dec String.string_dec.
 
 
 (* Project away range constraints in comparisons *)
@@ -935,6 +938,11 @@ end.
 Ltac not_Z ty := match ty with Z => fail 1 | _ => idtac end.
 Ltac clear_non_Z_defns := 
   repeat match goal with H := _ : ?X |- _ => not_Z X; clearbody H end.
+Ltac clear_irrelevant_defns :=
+repeat match goal with X := _ |- _ =>
+  match goal with |- context[X] => idtac end ||
+  match goal with _ : context[X] |- _ => idtac end || clear X
+end.
 
 Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >= 0).
 constructor.
@@ -1002,6 +1010,7 @@ Ltac dump_context :=
   match goal with |- ?X => idtac "Goal:" X end.
 Ltac prepare_for_solver :=
 (*dump_context;*)
+ clear_irrelevant_defns;
  clear_non_Z_defns;
  extract_properties;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
@@ -1014,11 +1023,20 @@ Ltac prepare_for_solver :=
 Ltac solve_arithfact :=
 prepare_for_solver;
 (*dump_context;*)
- solve [apply ArithFact_mword; assumption
-       | constructor; omega with Z
-         (* The datatypes hints give us some list handling, esp In *)
-       | constructor; eauto with datatypes zarith sail
-       | constructor; idtac "Unable to solve constraint"; dump_context; fail].
+ solve
+ [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; constructor; exact (I : (fun _ => True) _) end
+ | match goal with |- ArithFact (?x = ?y) =>
+   (is_evar x || is_evar y);
+   (* compute to allow projections to remove proofs that might not be allowed in the evar *)
+   let x := eval cbn in x in
+   let y := eval cbn in y in
+   idtac "Warning: unknown equality constraint"; constructor; exact (eq_refl _ : x = y) end
+ | apply ArithFact_mword; assumption
+ | constructor; omega with Z
+   (* The datatypes hints give us some list handling, esp In *)
+ | constructor; eauto 3 with datatypes zarith sail
+ | constructor; idtac "Unable to solve constraint"; dump_context; fail
+ ].
 Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances.
 
 Hint Unfold length_mword : sail.
@@ -1036,6 +1054,10 @@ Qed.
 
 Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; omega]) : typeclass_instances.
 
+Definition to_range (x : Z) : {y : Z & ArithFact (x <= y <= x)} := build_ex x.
+
+
+
 Instance mword_Bitvector {a : Z} `{ArithFact (a >= 0)} : (Bitvector (mword a)) := {
   bits_of v := List.map bitU_of_bool (bitlistFromWord (get_word v));
   of_bits v := option_map (fun bl => to_word isPositive (fit_bbv_word (wordFromBitlist bl))) (just_list (List.map bool_of_bitU v));
diff --git a/lib/hol/.gitignore b/lib/hol/.gitignore
index fe652801..73d33f88 100644
--- a/lib/hol/.gitignore
+++ b/lib/hol/.gitignore
@@ -1,9 +1,10 @@
-prompt_monadScript.sml
-promptScript.sml
-sail_instr_kindsScript.sml
-sail_operators_bitlistsScript.sml
-sail_operators_mwordsScript.sml
-sail_operatorsScript.sml
-sail_valuesScript.sml
-state_monadScript.sml
-stateScript.sml
+sail2_prompt_monadScript.sml
+sail2_promptScript.sml
+sail2_instr_kindsScript.sml
+sail2_operators_bitlistsScript.sml
+sail2_operators_mwordsScript.sml
+sail2_operatorsScript.sml
+sail2_valuesScript.sml
+sail2_state_monadScript.sml
+sail2_stateScript.sml
+sail2_stringScript.sml
diff --git a/lib/isabelle/.gitignore b/lib/isabelle/.gitignore
index ed83cdc1..fad6adbd 100644
--- a/lib/isabelle/.gitignore
+++ b/lib/isabelle/.gitignore
@@ -10,4 +10,6 @@ Sail2_valuesAuxiliary.thy
 Sail2_values.thy
 Sail2_stateAuxiliary.thy
 Sail2_state_monad.thy
+Sail2_state_lifting.thy
 Sail2_state.thy
+Sail2_string.thy
\ No newline at end of file
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index aa8d05cd..9e837e10 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -29,7 +29,8 @@ function extsv(v) = exts_vec(sizeof('m),v)
 
 /* This is generated internally to deal with case splits which reveal the size
    of a bitvector */
-val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
 
 /* Definitions for the rewrites */
 
diff --git a/mips/mips_extras.v b/mips/mips_extras.v
index 6a6aed5c..626b4109 100644
--- a/mips/mips_extras.v
+++ b/mips/mips_extras.v
@@ -143,7 +143,7 @@ Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0
 refine (existT _ (ZEuclid.modulo m n) _).
 constructor.
 destruct H.
-assert (Zabs n = n). { rewrite Zabs_eq; auto with zarith. }
+assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. }
 rewrite <- H at 3.
 lapply (ZEuclid.mod_always_pos m n); omega.
 Qed.
@@ -160,3 +160,12 @@ Definition prerr_string (_:string) : unit := tt.
 Definition putchar {T} (_:T) : unit := tt.
 Require DecimalString.
 Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z).
+
+
+Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * size ÷ 8).
+intros.
+rewrite Z.mul_comm.
+rewrite Z.quot_mul; auto with zarith.
+Qed.
+Hint Resolve MEMr_wrapper_lemma : sail.
+
diff --git a/riscv/Makefile b/riscv/Makefile
index 4805c8b2..6499fe7d 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -77,6 +77,17 @@ riscvScript.sml : riscv.lem riscv_extras.lem
 riscvTheory.uo riscvTheory.ui: riscvScript.sml
 	Holmake riscvTheory.uo
 
+COQ_LIBS = -R ../../bbv/theories bbv -R ../lib/coq Sail
+
+riscv.v riscv_types.v: $(SAIL_SRCS)
+	$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv -coq_lib riscv_extras $(SAIL_SRCS)
+riscv_duopod.v riscv_duopod_types.v:  prelude.sail riscv_duopod.sail
+	$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv_duopod -coq_lib riscv_extras $^
+%.vo: %.v
+	coqc $(COQ_LIBS) $<
+riscv.vo: riscv_types.vo riscv_extras.vo
+riscv_duopod.vo: riscv_duopod_types.vo riscv_extras.vo
+
 # we exclude prelude.sail here, most code there should move to sail lib
 LOC_FILES:=$(SAIL_SRCS) main.sail
 include ../etc/loc.mk
@@ -89,5 +100,7 @@ clean:
 	-rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem
 	-rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml
 	-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
 	-Holmake cleanAll
 	ocamlbuild -clean
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 6eeda601..8636bda6 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -64,11 +64,11 @@ function def_spc_backwards s = ()
 val def_spc_matches_prefix = "opt_spc_matches_prefix" : string -> option((unit, nat))
 
 
-val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lt_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gt_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 
 val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
 val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool
@@ -134,7 +134,7 @@ val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('
 
 overload append = {bitvector_concat, vector_concat}
 
-val not_bool = "not" : bool -> bool
+val not_bool = {coq: "negb", _: "not"} : bool -> bool
 
 val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n)
 
@@ -158,7 +158,7 @@ function neq_anything (x, y) = not_bool(x == y)
 
 overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
 
-val and_bool = "and_bool" : (bool, bool) -> bool
+val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
 
 val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -168,7 +168,7 @@ function and_vec (xs, ys) = builtin_and_vec(xs, ys)
 
 overload operator & = {and_bool, and_vec}
 
-val or_bool = "or_bool" : (bool, bool) -> bool
+val or_bool = {coq: "orb", _:"or_bool"} : (bool, bool) -> bool
 
 val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -182,7 +182,7 @@ val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2
 
 val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
-val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
+val hex_slice = "hex_slice" : forall 'n 'm, 'n >= 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
 
 val __SetSlice_bits = "set_slice" : forall 'n 'm.
   (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
@@ -191,16 +191,16 @@ val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w))
 
 val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int
 
-val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w)
+val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w)
 
-val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n)
+val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n)
 
 function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o)
 
 val __raw_SetSlice_bits : forall 'n 'w.
   (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n)
 
-val __raw_GetSlice_bits : forall 'n 'w.
+val __raw_GetSlice_bits : forall 'n 'w, 'w >= 0.
   (atom('n), atom('w), bits('n), int) -> bits('w)
 
 val "shiftl" : forall 'm. (bits('m), int) -> bits('m)
@@ -239,10 +239,10 @@ val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> r
 
 overload operator ^ = {xor_vec, int_power, real_power, concat_str}
 
-val add_range = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm 'o 'p.
+val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val add_int = {ocaml: "add_int", lem: "integerAdd"} : (int, int) -> int
+val add_int = {ocaml: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int
 
 val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -252,10 +252,10 @@ val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real
 
 overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
 
-val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p.
+val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
-val sub_int = {ocaml: "sub_int", lem: "integerMinus"} : (int, int) -> int
+val sub_int = {ocaml: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int
 val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
                lem: "integerMinus"}
             : (nat, nat) -> nat
@@ -266,9 +266,9 @@ val "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n)
 
 val sub_real = {ocaml: "sub_real", lem: "realMinus"} : (real, real) -> real
 
-val negate_range = {ocaml: "minus_big_int", lem: "integerNegate"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
+val negate_range = {ocaml: "minus_big_int", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
 
-val negate_int = {ocaml: "minus_big_int", lem: "integerNegate"} : int -> int
+val negate_int = {ocaml: "minus_big_int", lem: "integerNegate", coq: "Z.opp"} : int -> int
 
 val negate_real = {ocaml: "Num.minus_num", lem: "realNegate"} : real -> real
 
@@ -276,36 +276,36 @@ overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real}
 
 overload negate = {negate_range, negate_int, negate_real}
 
-val mult_range = {ocaml: "mult", lem: "integerMult"} : forall 'n 'm 'o 'p.
-  (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p)
+val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm.
+  (atom('n), atom('m)) -> atom('n * 'm)
 
-val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+val mult_int = {ocaml: "mult", lem: "integerMult", coq: "Z.mul"} : (int, int) -> int
 
 val mult_real = {ocaml: "mult_real", lem: "realMult"} : (real, real) -> real
 
-overload operator * = {mult_range, mult_int, mult_real}
+overload operator * = {mult_atom, mult_int, mult_real}
 
 val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real
 
-val gteq_int = "gteq" : (int, int) -> bool
+val gteq_int = {coq: "Z.geb", _: "gteq"} : (int, int) -> bool
 
 val gteq_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool
 
 overload operator >= = {gteq_atom, gteq_int, gteq_real}
 
-val lteq_int = "lteq" : (int, int) -> bool
+val lteq_int = {coq: "Z.leb", _: "lteq"} : (int, int) -> bool
 
 val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool
 
 overload operator <= = {lteq_atom, lteq_int, lteq_real}
 
-val gt_int = "gt" : (int, int) -> bool
+val gt_int = {coq: "Z.gtb", _: "gt"} : (int, int) -> bool
 
 val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool
 
 overload operator > = {gt_atom, gt_int, gt_real}
 
-val lt_int = "lt" : (int, int) -> bool
+val lt_int = {coq: "Z.ltb", _: "lt"} : (int, int) -> bool
 
 val lt_real = {ocaml: "lt_real", lem: "lt"} : (real, real) -> bool
 
@@ -315,7 +315,7 @@ val RoundDown = {ocaml: "round_down", lem: "realFloor"} : real -> int
 
 val RoundUp = {ocaml: "round_up", lem: "realCeiling"} : real -> int
 
-val abs_int = {ocaml: "abs_int", lem: "abs"} : int -> int
+val abs_int = {ocaml: "abs_int", lem: "abs", coq: "Z.abs"} : int -> int
 
 val abs_real = {ocaml: "abs_real", lem: "abs"} : real -> real
 
@@ -365,25 +365,25 @@ function __RISCV_write (addr, width, data) = {
 val __TraceMemoryWrite : forall 'n 'm.
   (atom('n), bits('m), bits(8 * 'n)) -> unit
 
-val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm.
+val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm.
+val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm.
+val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm.
+val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm.
+val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm.
+val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __RISCV_read : forall 'n. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}
+val __RISCV_read : forall 'n, 'n >= 0. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}
 function __RISCV_read (addr, width, aq, rl, res) =
   match (aq, rl, res) {
     (false, false, false) => Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)),
@@ -398,7 +398,7 @@ function __RISCV_read (addr, width, aq, rl, res) =
 
 val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
 
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm)
 
 val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)}
 
@@ -476,7 +476,7 @@ val vector64 : int -> bits(64)
 
 function vector64 n = __raw_GetSlice_int(64, n, 0)
 
-val to_bits : forall 'l.(atom('l), int) -> bits('l)
+val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
 function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
 
 val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
@@ -496,7 +496,3 @@ function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) =
 function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
     let v64 : bits(64) = EXTS(v) in
     (v64 >> shift)[31..0]
-
-/* Copied from arith.sail. */
-val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : forall 'n 'm.
-  (atom('n), atom('m)) -> atom('n * 'm)
diff --git a/riscv/riscv_duopod.sail b/riscv/riscv_duopod.sail
index ff1e4065..0a5a7f8c 100644
--- a/riscv/riscv_duopod.sail
+++ b/riscv/riscv_duopod.sail
@@ -5,7 +5,7 @@ type xlen_t = bits(64)
 type regno ('n : Int), 0 <= 'n < 32 = atom('n)
 type regbits = bits(5)
 
-val zeros : forall 'n. atom('n) -> bits('n)
+val zeros : forall 'n, 'n >= 0. atom('n) -> bits('n)
 function zeros n = replicate_bits(0b0, n)
 
 val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
@@ -35,7 +35,7 @@ overload X = {rX, wX}
 
 /* Accessors for memory */
 
-val MEMr : forall 'n. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr : forall 'n, 'n >= 0. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem}
 function MEMr (addr, width) =
   match __RISCV_read(addr, width, false, false, false) { Some(v) => v, None() => zeros(8 * width) }
 
diff --git a/riscv/riscv_extras.v b/riscv/riscv_extras.v
new file mode 100644
index 00000000..3f1fe7e0
--- /dev/null
+++ b/riscv/riscv_extras.v
@@ -0,0 +1,162 @@
+Require Import Sail2_instr_kinds.
+Require Import Sail2_values.
+Require Import Sail2_operators_mwords.
+Require Import Sail2_prompt_monad.
+Require Import Sail2_prompt.
+Require Import String.
+Require Import List.
+Import List.ListNotations.
+
+Axiom real : Type.
+
+(*
+val MEMr             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e
+val MEMr_reserve     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e
+val MEMr_tag         : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e
+val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e
+*)
+Definition MEMr {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size            : monad regval (mword b) e := read_mem Read_plain addr size.
+Definition MEMr_reserve {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size    : monad regval (mword b) e := read_mem Read_reserve addr size.
+
+(*val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e*)
+Definition read_tag_bool {regval a e} (addr : mword a) : monad regval bool e :=
+  read_tag addr >>= fun t =>
+  maybe_fail "read_tag_bool" (bool_of_bitU t).
+
+(*val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e*)
+Definition write_tag_bool {regval a e} (addr : mword a) t : monad regval unit e :=
+ write_tag addr (bitU_of_bool t) >>= fun _ => returnm tt.
+
+Definition MEMr_tag {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (bool * mword b) e :=
+  read_mem Read_plain addr size >>= fun v =>
+  read_tag_bool addr >>= fun t =>
+  returnm (t, v).
+
+Definition MEMr_tag_reserve {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (bool * mword b) e :=
+  read_mem Read_plain addr size >>= fun v =>
+  read_tag_bool addr >>= fun t =>
+  returnm (t, v).
+
+(*
+val MEMea                 : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
+val MEMea_conditional     : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
+val MEMea_tag             : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
+val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
+*)
+Definition MEMea {regval a e} (addr : mword a) size                : monad regval unit e := write_mem_ea Write_plain addr size.
+Definition MEMea_conditional {regval a e} (addr : mword a) size    : monad regval unit e := write_mem_ea Write_conditional addr size.
+
+Definition MEMea_tag {regval a e} (addr : mword a) size            : monad regval unit e := write_mem_ea Write_plain addr size.
+Definition MEMea_tag_conditional {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_conditional addr size.
+
+(*
+val MEMval                 : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval unit 'e
+val MEMval_conditional     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval bool 'e
+val MEMval_tag             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e
+val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e
+*)
+Definition MEMval {regval a b e} (_ : mword a) (size : Z) (v : mword b)                      : monad regval unit e := write_mem_val v >>= fun _ => returnm tt.
+Definition MEMval_conditional {regval a b e} (_ : mword a) (size : Z) (v : mword b)          : monad regval bool e := write_mem_val v >>= fun b => returnm (if b then true else false).
+Definition MEMval_tag {regval a b e} (addr : mword a) (size : Z) t (v : mword b)             : monad regval unit e := write_mem_val v >>= fun _ => write_tag_bool addr t >>= fun _ => returnm tt.
+Definition MEMval_tag_conditional {regval a b e} (addr : mword a) (size : Z) t (v : mword b) : monad regval bool e := write_mem_val v >>= fun b => write_tag_bool addr t >>= fun _ => returnm (if b then true else false).
+
+(*val MEM_sync  : forall 'regval 'e. unit -> monad 'regval unit 'e*)
+
+Definition MEM_sync {regval e} (_:unit) : monad regval unit e := barrier Barrier_MIPS_SYNC.
+
+(* Some wrappers copied from aarch64_extras *)
+(* TODO: Harmonise into a common library *)
+(*
+Definition get_slice_int_bl len n lo :=
+  (* TODO: Is this the intended behaviour? *)
+  let hi := lo + len - 1 in
+  let bs := bools_of_int (hi + 1) n in
+  subrange_list false bs hi lo
+
+val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
+Definition get_slice_int len n lo := of_bools (get_slice_int_bl len n lo)
+*)
+Definition write_ram {rv e} m size (hexRAM : mword m) (addr : mword m) (data : mword (8 * size)) : monad rv bool e :=
+  write_mem_val data.
+
+Definition read_ram {rv e} m size `{ArithFact (size >= 0)} (_ : mword m) (addr : mword m) : monad rv (mword (8 * size)) e :=
+ read_mem Read_plain addr size.
+(*
+Definition string_of_bits bs := string_of_bv (bits_of bs).
+Definition string_of_int := show
+
+Definition _sign_extend bits len := maybe_failwith (of_bits (exts_bv len bits))
+Definition _zero_extend bits len := maybe_failwith (of_bits (extz_bv len bits))
+*)
+Definition shift_bits_left {a b} (v : mword a) (n : mword b) : mword a :=
+  shiftl v (int_of_mword false n).
+
+Definition shift_bits_right {a b} (v : mword a) (n : mword b) : mword a :=
+  shiftr v (int_of_mword false n).
+
+Definition shift_bits_right_arith {a b} (v : mword a) (n : mword b) : mword a :=
+  arith_shiftr v (int_of_mword false n).
+
+(* Use constants for undefined values for now *)
+Definition internal_pick {rv a e} (vs : list a) : monad rv a e :=
+match vs with
+| (h::_) => returnm h
+| _ => Fail "empty list in internal_pick"
+end.
+Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%string.
+Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt.
+Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii).
+(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*)
+Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >= 0)} : monad rv (vec a len) e := returnm (vec_init u len).
+(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
+Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mword len) e := returnm (mword_of_int 0).
+(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
+Definition undefined_bits {rv e} := @undefined_bitvector rv e.
+Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU.
+(*Definition undefined_real {rv e} (_:unit) : monad rv real e := returnm (realFromFrac 0 1).*)
+Definition undefined_range {rv e} i j `{ArithFact (i <= j)} : monad rv {z : Z & ArithFact (i <= z /\ z <= j)} e := returnm (build_ex i).
+Definition undefined_atom {rv e} i : monad rv Z e := returnm i.
+Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii).
+
+Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt.
+
+(*val elf_entry : unit -> integer*)
+Definition elf_entry (_:unit) : Z := 0.
+(*declare ocaml target_rep function elf_entry := `Elf_loader.elf_entry`*)
+
+Definition print_bits {n} msg (bs : mword n) := prerr_endline (msg ++ (string_of_bits bs)).
+
+(*val get_time_ns : unit -> integer*)
+Definition get_time_ns (_:unit) : Z := 0.
+(*declare ocaml target_rep function get_time_ns := `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`*)
+
+Definition eq_bit (x : bitU) (y : bitU) : bool :=
+  match x, y with
+  | B0, B0 => true
+  | B1, B1 => true
+  | BU, BU => true
+  | _,_ => false
+  end.
+
+Require Import Zeuclid.
+Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0 <= z <= n-1)}.
+apply existT with (x := ZEuclid.modulo m n).
+constructor.
+destruct H.
+assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. }
+rewrite <- H at 3.
+lapply (ZEuclid.mod_always_pos m n); omega.
+Qed.
+
+(* Override the more general version *)
+
+Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r.
+Definition mult_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mult_vec l r.
+
+
+Definition print_endline (_:string) : unit := tt.
+Definition prerr_endline (_:string) : unit := tt.
+Definition prerr_string (_:string) : unit := tt.
+Definition putchar {T} (_:T) : unit := tt.
+Require DecimalString.
+Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z).
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 72b7e8da..7268e9cc 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -8,7 +8,7 @@ function is_aligned_addr (addr : xlenbits, width : atom('n)) -> forall 'n. bool
   unsigned(addr) % width == 0
 
 // only used for actual memory regions, to avoid MMIO effects
-function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
+function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n, 'n >= 0. MemoryOpResult(bits(8 * 'n)) =
   match (t, __RISCV_read(addr, width, aq, rl, res)) {
     (Instruction, None()) => MemException(E_Fetch_Access_Fault),
     (Data, None())        => MemException(E_Load_Access_Fault),
@@ -16,7 +16,7 @@ function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : boo
                                MemValue(v) }
   }
 
-function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
+function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) =
   /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */
   if   t == Data & within_mmio_readable(addr, width)
   then mmio_read(addr, width)
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 7ab83aa6..6e3dee93 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -85,7 +85,7 @@ let MSIP_BASE     : xlenbits = 0x0000000000000000
 let MTIMECMP_BASE : xlenbits = 0x0000000000004000
 let MTIME_BASE    : xlenbits = 0x000000000000bff8
 
-val clint_load : forall 'n. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
+val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
 function clint_load(addr, width) = {
   let addr = addr - plat_clint_base ();
   /* FIXME: For now, only allow exact aligned access. */
@@ -224,7 +224,7 @@ function within_mmio_readable(addr : xlenbits, width : atom('n)) -> forall 'n. b
 function within_mmio_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
   within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8)
 
-function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
+function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) =
   if   within_clint(addr, width)
   then clint_load(addr, width)
   else if within_htif_readable(addr, width) & (1 <= 'n)
diff --git a/src/latex.ml b/src/latex.ml
index 39db43db..0520d074 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -126,7 +126,7 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l
     | Some l -> Printf.sprintf "\\label{%s}" l
   in
   let cmd = !opt_prefix_latex ^ prefix ^ cmd in
-  let lcmd = String.lowercase_ascii cmd in  (* lowercase to avoid file names differing only by case *)
+  let lcmd = String.lowercase cmd in  (* lowercase to avoid file names differing only by case *)
   if StringSet.mem lcmd !commands then
     latex_command ~label:label dir (cmd ^ "v") no_loc annot
   else
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index c17e879f..a5cb96ff 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -481,7 +481,7 @@ let rec instr_parms_to_string ps =
 let pad n s = if String.length s < n then s ^ String.make (n-String.length s) ' ' else s
 
 let instruction_to_string (name, parms) = 
-  ((*pad 5*) (String.lowercase_ascii name)) ^ " " ^ instr_parms_to_string parms 
+  ((*pad 5*) (String.lowercase name)) ^ " " ^ instr_parms_to_string parms 
 
 let print_backtrace_compact printer (IState(stack,_)) =
   List.iter (fun (e,(env,mem)) -> print_exp printer env mem true e) (compact_stack stack)
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index adc4d6d2..ab6d9e2d 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3167,13 +3167,15 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
     | None -> r
     | Some (tenv,typ,_) ->
        let typ = Env.base_typ_of tenv typ in
-       let env, typ =
+       let env, tenv, typ =
          match destruct_exist tenv typ with
-         | None -> env, typ
+         | None -> env, tenv, typ
          | Some (kids, nc, typ) ->
             { env with kid_deps =
                 List.fold_left (fun kds kid -> KBindings.add kid deps kds) env.kid_deps kids },
-            typ
+           Env.add_constraint nc
+             (List.fold_left (fun tenv kid -> Env.add_typ_var l kid BK_int tenv) tenv kids),
+           typ
        in
        if is_bitvector_typ typ then
          let size,_,_ = vector_typ_args_of typ in
@@ -3644,6 +3646,14 @@ let is_constant_vec_typ env typ =
 
 let rewrite_app env typ (id,args) =
   let is_append = is_id env (Id "append") in
+  let try_cast_to_typ (E_aux (e,_) as exp) =
+    let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
+    match size with
+    | Nexp_aux (Nexp_constant _,_) -> E_cast (typ,exp)
+    | _ -> match solve env size with
+      | Some c -> E_cast (vector_typ (nconstant c) order bittyp, exp)
+      | None -> e
+  in
   if is_append id then
     let is_subrange = is_id env (Id "vector_subrange") in
     let is_slice = is_id env (Id "slice") in
@@ -3661,14 +3671,23 @@ let rewrite_app env typ (id,args) =
           not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) ->
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
-       let midsize = nminus size size1 in
-       let midtyp = vector_typ midsize order bittyp in
-       E_app (append,
-              [e1;
-               E_aux (E_cast (midtyp,
-                              E_aux (E_app (mk_id "subrange_subrange_concat",
-                                            [vector1; start1; end1; vector2; start2; end2]),
-                                     (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+       let midsize = nminus size size1 in begin
+         match solve env midsize with
+         | Some c ->
+            let midtyp = vector_typ (nconstant c) order bittyp in
+            E_app (append,
+                   [e1;
+                    E_aux (E_cast (midtyp,
+                                   E_aux (E_app (mk_id "subrange_subrange_concat",
+                                                 [vector1; start1; end1; vector2; start2; end2]),
+                                          (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+         | _ ->
+            E_app (append,
+                   [e1;
+                    E_aux (E_app (mk_id "subrange_subrange_concat",
+                                  [vector1; start1; end1; vector2; start2; end2]),
+                           (Unknown,empty_tannot))])
+       end
     | [E_aux (E_app (append,
               [e1;
                E_aux (E_app (slice1,
@@ -3680,14 +3699,23 @@ let rewrite_app env typ (id,args) =
           not (is_constant length1 || is_constant length2) ->
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
-       let midsize = nminus size size1 in
-       let midtyp = vector_typ midsize order bittyp in
-       E_app (append,
-              [e1;
-               E_aux (E_cast (midtyp,
-                              E_aux (E_app (mk_id "slice_slice_concat",
-                                            [vector1; start1; length1; vector2; start2; length2]),
-                                     (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+       let midsize = nminus size size1 in begin
+         match solve env midsize with
+         | Some c ->
+            let midtyp = vector_typ (nconstant c) order bittyp in
+            E_app (append,
+                   [e1;
+                    E_aux (E_cast (midtyp,
+                                   E_aux (E_app (mk_id "slice_slice_concat",
+                                                 [vector1; start1; length1; vector2; start2; length2]),
+                                          (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+         | _ ->
+            E_app (append,
+                   [e1;
+                    E_aux (E_app (mk_id "slice_slice_concat",
+                                  [vector1; start1; length1; vector2; start2; length2]),
+                           (Unknown,empty_tannot))])
+       end
 
     (* variable-range @ variable-range *)
     | [E_aux (E_app (subrange1,
@@ -3696,10 +3724,10 @@ let rewrite_app env typ (id,args) =
                      [vector2; start2; end2]),_)]
         when is_subrange subrange1 && is_subrange subrange2 &&
           not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) ->
-       E_cast (typ,
-               E_aux (E_app (mk_id "subrange_subrange_concat",
-                             [vector1; start1; end1; vector2; start2; end2]),
-                      (Unknown,empty_tannot)))
+       try_cast_to_typ
+         (E_aux (E_app (mk_id "subrange_subrange_concat",
+                        [vector1; start1; end1; vector2; start2; end2]),
+                 (Unknown,empty_tannot)))
 
     (* variable-slice @ variable-slice *)
     | [E_aux (E_app (slice1,
@@ -3708,9 +3736,9 @@ let rewrite_app env typ (id,args) =
                      [vector2; start2; length2]),_)]
         when is_slice slice1 && is_slice slice2 &&
           not (is_constant length1 || is_constant length2) ->
-       E_cast (typ,
-               E_aux (E_app (mk_id "slice_slice_concat",
-                             [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot)))
+       try_cast_to_typ
+         (E_aux (E_app (mk_id "slice_slice_concat",
+                        [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot)))
 
     | [E_aux (E_app (append1,
                      [e1;
@@ -3721,16 +3749,25 @@ let rewrite_app env typ (id,args) =
           not (is_constant length1 || is_constant length2) ->
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
-       let midsize = nminus size size1 in
-       let midtyp = vector_typ midsize order bittyp in
-       E_cast (typ,
-               E_aux (E_app (mk_id "append",
+       let midsize = nminus size size1 in begin
+         match solve env midsize with
+         | Some c ->
+            let midtyp = vector_typ (nconstant c) order bittyp in
+            try_cast_to_typ
+              (E_aux (E_app (mk_id "append",
                              [e1;
                               E_aux (E_cast (midtyp,
                                              E_aux (E_app (mk_id "slice_zeros_concat",
                                                            [vector1; start1; length1; length2]),(Unknown,empty_tannot))),(Unknown,empty_tannot))]),
                       (Unknown,empty_tannot)))
-
+         | _ ->
+            try_cast_to_typ
+              (E_aux (E_app (mk_id "append",
+                             [e1;
+                              E_aux (E_app (mk_id "slice_zeros_concat",
+                                            [vector1; start1; length1; length2]),(Unknown,empty_tannot))]),
+                      (Unknown,empty_tannot)))
+       end
     | _ -> E_app (id,args)
 
   else if is_id env (Id "eq_vec") id then
@@ -3875,7 +3912,7 @@ let simplify_size_nexp env quant_kids (Nexp_aux (_,l) as nexp) =
 (* These functions add cast functions across case splits, so that when a
    bitvector size becomes known in sail, the generated Lem code contains a
    function call to change mword 'n to (say) mword ty16, and vice versa. *)
-let make_bitvector_cast_fns env quant_kids src_typ target_typ =
+let make_bitvector_cast_fns cast_name env quant_kids src_typ target_typ =
   let genunk = Generated Unknown in
   let fresh =
     let counter = ref 0 in
@@ -3908,7 +3945,7 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
           P_aux (P_id var,(Generated src_l,src_ann)),
           E_aux
             (E_cast (tar_typ',
-                     E_aux (E_app (Id_aux (Id "bitvector_cast", genunk),
+                     E_aux (E_app (Id_aux (Id cast_name, genunk),
                                    [E_aux (E_id var, (genunk, src_ann))]), (genunk, tar_ann))),
              (genunk, tar_ann))
        | _ ->
@@ -3934,12 +3971,12 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
        (fun var exp ->
          let exp_ann = mk_tannot env (typ_of exp) (effect_of exp) in
          E_aux (E_let (LB_aux (LB_val (P_aux (P_typ (one_target_typ, P_aux (P_id var,(genunk,tar_ann))),(genunk,tar_ann)),
-                                       E_aux (E_app (Id_aux (Id "bitvector_cast",genunk),
+                                       E_aux (E_app (Id_aux (Id cast_name,genunk),
                                                      [E_aux (E_id var,(genunk,src_ann))]),(genunk,tar_ann))),(genunk,tar_ann)),
                        exp),(genunk,exp_ann))),
       (fun (E_aux (_,(exp_l,exp_ann)) as exp) ->
         E_aux (E_cast (one_target_typ,
-                       E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), [exp]), (Generated exp_l,tar_ann))),
+                       E_aux (E_app (Id_aux (Id cast_name, genunk), [exp]), (Generated exp_l,tar_ann))),
                (Generated exp_l,tar_ann)))
     | _ ->
        (fun var exp ->
@@ -3954,12 +3991,12 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
 
 (* TODO: bound vars *)
 let make_bitvector_env_casts env quant_kids (kid,i) exp =
-  let mk_cast var typ exp = (fst (make_bitvector_cast_fns env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in
+  let mk_cast var typ exp = (fst (make_bitvector_cast_fns "bitvector_cast_in" env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in
   let locals = Env.get_locals env in
   Bindings.fold (fun var (mut,typ) exp ->
     if mut = Immutable then mk_cast var typ exp else exp) locals exp
 
-let make_bitvector_cast_exp env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns env quant_kids typ target_typ)) exp
+let make_bitvector_cast_exp cast_name env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns cast_name env quant_kids typ target_typ)) exp
 
 let rec extract_value_from_guard var (E_aux (e,_)) =
   match e with
@@ -3986,6 +4023,12 @@ let fill_in_type env typ =
   subst_src_typ subst typ
 
 (* TODO: top-level patterns *)
+(* TODO: proper environment tracking for variables.  Currently we pretend that
+   we can print the type of a variable in the top-level environment, but in
+   practice they might be below a case split.  Note that we'd also need to
+   provide some way for the Lem pretty printer to know what to use; currently
+   we just use two names for the cast, bitvector_cast_in and bitvector_cast_out,
+   to let the pretty printer know whether to use the top-level environment. *)
 let add_bitvector_casts (Defs defs) =
   let rewrite_body id quant_kids top_env ret_typ exp =
     let rewrite_aux (e,ann) =
@@ -4002,13 +4045,13 @@ let add_bitvector_casts (Defs defs) =
              let body = match pat, guard with
                | P_aux (P_lit (L_aux (L_num i,_)),_), _ ->
                   let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in
-                  make_bitvector_cast_exp env quant_kids src_typ result_typ
+                  make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ
                     (make_bitvector_env_casts env quant_kids (kid,i) body)
                | P_aux (P_id var,_), Some guard ->
                   (match extract_value_from_guard var guard with
                   | Some i ->
                      let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in
-                     make_bitvector_cast_exp env quant_kids src_typ result_typ
+                     make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ
                        (make_bitvector_env_casts env quant_kids (kid,i) body)
                   | None -> body)
                | _ ->
@@ -4019,15 +4062,46 @@ let add_bitvector_casts (Defs defs) =
            E_aux (E_case (exp', List.map map_case cases),ann)
         | _ -> E_aux (e,ann)
       end
+      | E_if (e1,e2,e3) ->
+         let env = env_of_annot ann in
+         let result_typ = Env.base_typ_of env (typ_of_annot ann) in
+         let rec extract (E_aux (e,_)) =
+           match e with
+           | E_app (op,
+                    ([E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); y] |
+                     [y; E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_)]))
+               when string_of_id op = "eq_atom" ->
+              (match destruct_atom_nexp (env_of y) (typ_of y) with
+              | Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)]
+              | _ -> [])
+           | E_app (op, [x;y]) when string_of_id op = "and_bool" ->
+              extract x @ extract y
+           | _ -> []
+         in
+         let insts = extract e1 in
+         let e2' = List.fold_left (fun body inst ->
+           make_bitvector_env_casts env quant_kids inst body) e2 insts in
+         let insts = List.fold_left (fun insts (kid,i) ->
+           KBindings.add kid (nconstant i) insts) KBindings.empty insts in
+         let src_typ = subst_src_typ insts result_typ in
+         let e2' = make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ e2' in
+         E_aux (E_if (e1,e2',e3), ann)
       | E_return e' ->
-         E_aux (E_return (make_bitvector_cast_exp top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann)
-      (* TODO: (env_of_annot ann) isn't suitable, because it contains
-         constraints revealing the case splits involved; needs a more
-         subtle approach *)
+         E_aux (E_return (make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann)
       | E_assign (LEXP_aux (lexp,lexp_annot),e') ->
          E_aux (E_assign (LEXP_aux (lexp,lexp_annot),
-                          make_bitvector_cast_exp (env_of_annot ann) quant_kids (fill_in_type (env_of e') (typ_of e'))
+                          make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e'))
                             (typ_of_annot lexp_annot) e'),ann)
+      | E_id id -> begin
+        let env = env_of_annot ann in
+        match Env.lookup_id id env with
+        | Local (Mutable, vtyp) ->
+           make_bitvector_cast_exp "bitvector_cast_in" top_env quant_kids
+             (fill_in_type (env_of_annot ann) (typ_of_annot ann))
+             vtyp
+             (E_aux (e,ann))
+        | _ -> E_aux (e,ann)
+      end
       | _ -> E_aux (e,ann)
     in
     let open Rewriter in
@@ -4052,7 +4126,7 @@ let add_bitvector_casts (Defs defs) =
     let body = rewrite_body id quant_kids body_env ret_typ body in
     (* Also add a cast around the entire function clause body, if necessary *)
     let body =
-      make_bitvector_cast_exp fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body
+      make_bitvector_cast_exp "bitvector_cast_out" fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body
     in
     let pexp = construct_pexp (pat,guard,body,annot) in
     FCL_aux (FCL_Funcl (id,pexp),fcl_ann)
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 3e4dc650..236c4222 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -673,7 +673,7 @@ let ocaml_main spec sail_dir =
     with
     | End_of_file -> close_in chan; lines := List.rev !lines
   end;
-  (("open " ^ String.capitalize_ascii spec ^ ";;\n\n") :: !lines
+  (("open " ^ String.capitalize spec ^ ";;\n\n") :: !lines
    @ [ "  zinitializze_registers ();";
        if !opt_trace_ocaml then "  Sail_lib.opt_trace := true;" else "  ();";
        "  Printexc.record_backtrace true;";
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 713cfb34..d5aa7151 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -58,6 +58,7 @@ open Pretty_print_common
 module StringSet = Set.Make(String)
 
 let opt_undef_axioms = ref false
+let opt_debug_on : string list ref = ref []
 
 (****************************************************************************
  * PPrint-based sail-to-coq pprinter
@@ -69,6 +70,7 @@ type context = {
   kid_id_renames : id KBindings.t; (* tyvar -> argument renames *)
   bound_nexps : NexpSet.t;
   build_ex_return : bool;
+  debug : bool;
 }
 let empty_ctxt = {
   early_ret = false;
@@ -76,8 +78,20 @@ let empty_ctxt = {
   kid_id_renames = KBindings.empty;
   bound_nexps = NexpSet.empty;
   build_ex_return = false;
+  debug = false;
 }
 
+let debug_depth = ref 0
+
+let rec indent n = match n with
+  | 0 -> ""
+  | n -> "|   " ^ indent (n - 1)
+
+let debug ctxt m =
+  if ctxt.debug
+  then print_endline (indent !debug_depth ^ Lazy.force m)
+  else ()
+
 let langlebar = string "<|"
 let ranglebar = string "|>"
 let anglebars = enclose langlebar ranglebar
@@ -91,6 +105,11 @@ let is_number_char c =
   c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' ||
   c = '6' || c = '7' || c = '8' || c = '9'
 
+let is_enum env id =
+  match Env.lookup_id id env with
+  | Enum _ -> true
+  | _ -> false
+
 let rec fix_id remove_tick name = match name with
   | "assert"
   | "lsl"
@@ -138,7 +157,6 @@ let doc_id id = string (string_id id)
 let doc_id_type (Id_aux(i,_)) =
   match i with
   | Id("int") -> string "Z"
-  | Id("nat") -> string "Z"
   | Id i -> string (fix_id false i)
   | DeIid x -> string (Util.zencode_string ("op " ^ x))
 
@@ -296,37 +314,70 @@ let drop_duplicate_atoms kids ty =
     | Typ_app _ -> Some full_typ
   in aux_typ ty
 
-(* TODO: parens *)
-let rec doc_nc_prop ctx (NC_aux (nc,_)) =
+(* Follows Coq precedence levels *)
+let rec doc_nc_prop ctx nc =
+  let rec l85 (NC_aux (nc,_) as nc_full) =
+  match nc with
+  | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2)
+  | _ -> l80 nc_full
+  and l80 (NC_aux (nc,_) as nc_full) =
+  match nc with
+  | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2)
+  | _ -> l70 nc_full
+  and l70 (NC_aux (nc,_) as nc_full) =
   match nc with
   | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2)
   | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
   | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
   | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
-  | NC_set (kid, is) -> (* TODO: is this a good translation? *)
+  | _ -> l10 nc_full
+  and l10 (NC_aux (nc,_) as nc_full) =
+  match nc with
+  | NC_set (kid, is) ->
      separate space [string "In"; doc_var_lem ctx kid;
                      brackets (separate (string "; ")
                                  (List.map (fun i -> string (Nat_big_num.to_string i)) is))]
-  | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2)
-  | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2)
   | NC_true -> string "True"
   | NC_false -> string "False"
-
-(* TODO: parens *)
-let rec doc_nc_exp ctx (NC_aux (nc,_)) =
-  match nc with
-  | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
-  | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
-  | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
-  | NC_not_equal (ne1, ne2) -> string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2))
-  | NC_set (kid, is) -> (* TODO: is this a good translation? *)
-     separate space [string "member_Z_list"; doc_var_lem ctx kid;
-                     brackets (separate (string "; ")
-                                 (List.map (fun i -> string (Nat_big_num.to_string i)) is))]
-  | NC_or (nc1, nc2) -> doc_op (string "||") (doc_nc_exp ctx nc1) (doc_nc_exp ctx nc2)
-  | NC_and (nc1, nc2) -> doc_op (string "&&") (doc_nc_exp ctx nc1) (doc_nc_exp ctx nc2)
-  | NC_true -> string "true"
-  | NC_false -> string "false"
+  | NC_or _
+  | NC_and _
+  | NC_equal _
+  | NC_bounded_ge _
+  | NC_bounded_le _
+  | NC_not_equal _ -> parens (l85 nc_full)
+  in l85 nc
+
+(* Follows Coq precedence levels *)
+let doc_nc_exp ctx nc =
+  let rec l70 (NC_aux (nc,_) as nc_full) =
+    match nc with
+    | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+    | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+    | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+    | _ -> l50 nc_full
+  and l50 (NC_aux (nc,_) as nc_full) =
+    match nc with
+    | NC_or (nc1, nc2) -> doc_op (string "||") (l50 nc1) (l40 nc2)
+    | _ -> l40 nc_full
+  and l40 (NC_aux (nc,_) as nc_full) =
+    match nc with
+    | NC_and (nc1, nc2) -> doc_op (string "&&") (l40 nc1) (l10 nc2)
+    | _ -> l10 nc_full
+  and l10 (NC_aux (nc,_) as nc_full) =
+    match nc with
+    | NC_not_equal (ne1, ne2) -> string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2))
+    | NC_set (kid, is) ->
+       separate space [string "member_Z_list"; doc_var_lem ctx kid;
+                       brackets (separate (string "; ")
+                                   (List.map (fun i -> string (Nat_big_num.to_string i)) is))]
+    | NC_true -> string "true"
+    | NC_false -> string "false"
+    | NC_equal _
+    | NC_bounded_ge _
+    | NC_bounded_le _
+    | NC_or _
+    | NC_and _ -> parens (l70 nc_full)
+  in l70 nc
 
 let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) =
   match typ with
@@ -337,6 +388,11 @@ let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) =
      let var = nvar kid in
      let nc = nc_and (nc_lteq low var) (nc_lteq var high) in
      Some (Typ_aux (Typ_exist ([kid], nc, atom_typ var),Parse_ast.Generated l))
+  | Typ_id (Id_aux (Id "nat",_)) ->
+     let kid = mk_kid "n" in
+     let var = nvar kid in
+     Some (Typ_aux (Typ_exist ([kid], nc_gteq var (nconstant Nat_big_num.zero), atom_typ var),
+                    Generated l))
   | _ -> None
 
 let expand_range_type typ = Util.option_default typ (maybe_expand_range_type typ)
@@ -381,7 +437,8 @@ let doc_typ, doc_atomic_typ =
       | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
          let tpp = string "register_ref regstate register_value " ^^ typ etyp in
          if atyp_needed then parens tpp else tpp
-      | Typ_app(Id_aux (Id "range", _), _) ->
+      | Typ_app(Id_aux (Id "range", _), _)
+      | Typ_id (Id_aux (Id "nat", _)) ->
          (match maybe_expand_range_type ty with
          | Some typ -> atomic_typ atyp_needed typ
          | None -> raise (Reporting_basic.err_unreachable l "Bad range type"))
@@ -758,17 +815,27 @@ let replace_atom_return_type ret_typ =
   | Typ_aux (Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),l) ->
      let kid = mk_kid "_retval" in (* TODO: collision avoidance *)
      true, Typ_aux (Typ_exist ([kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Generated l)
-  | Typ_aux (Typ_id (Id_aux (Id "nat",_)),l) ->
-     let kid = mk_kid "_retval" in
-     true, Typ_aux (Typ_exist ([kid], nc_gteq (nvar kid) (nconstant Nat_big_num.zero), atom_typ (nvar kid)),Generated l)
   | _ -> false, ret_typ
 
+let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) =
+  match argty, fnty with
+  | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),
+    Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_);
+                                     Typ_arg_aux(Typ_arg_nexp high,_)]) ->
+     Type_check.prove env (nc_and (nc_eq nexp low) (nc_eq nexp high))
+  | _ -> false
 
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
 let doc_exp_lem, doc_let_lem =
   let rec top_exp (ctxt : context) (aexp_needed : bool)
     (E_aux (e, (l,annot)) as full_exp) =
+    let top_exp c a e = 
+      let () = debug_depth := !debug_depth + 1 in
+      let r = top_exp c a e in
+      let () = debug_depth := !debug_depth - 1 in
+      r
+    in
     let expY = top_exp ctxt true in
     let expN = top_exp ctxt false in
     let expV = top_exp ctxt in
@@ -984,6 +1051,7 @@ let doc_exp_lem, doc_let_lem =
                    parens (separate_map comma (expV false) args) in
             if aexp_needed then parens (align epp) else epp
           else
+            let () = debug ctxt (lazy ("Function application " ^ string_of_id f)) in
             let call, is_extern =
               if Env.is_extern f env "coq"
               then string (Env.get_extern f env "coq"), true
@@ -996,33 +1064,44 @@ let doc_exp_lem, doc_let_lem =
                  | _ -> [arg_typ], ret_typ, eff)
               | _ -> raise (Reporting_basic.err_unreachable l "Function not a function type")
             in
+            let inst =
+              match instantiation_of_without_type full_exp with
+              | x -> x
+              (* Not all function applications can be inferred, so try falling back to the
+                 type inferred when we know the target type.
+                 TODO: there are probably some edge cases where this won't pick up a need
+                 to cast. *)
+              | exception _ -> instantiation_of full_exp
+            in
+            let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
+
             (* Insert existential unpacking of arguments where necessary *)
             let doc_arg arg typ_from_fn =
               let arg_pp = expY arg in
-              let arg_ty = expand_range_type (Env.expand_synonyms (env_of arg) (typ_of arg)) in
-              let typ_from_fn = expand_range_type (Env.expand_synonyms (env_of arg) typ_from_fn) in
+              let arg_ty_plain = Env.expand_synonyms (env_of arg) (typ_of arg) in
+              let arg_ty = expand_range_type arg_ty_plain in
+              let typ_from_fn_plain = subst_unifiers inst typ_from_fn in
+              let typ_from_fn_plain = Env.expand_synonyms (env_of arg) typ_from_fn_plain in
+              let typ_from_fn = expand_range_type typ_from_fn_plain in
               (* TODO: more sophisticated check *)
+              let () =
+                debug ctxt (lazy (" arg type found    " ^ string_of_typ arg_ty_plain));
+                debug ctxt (lazy (" arg type expected " ^ string_of_typ typ_from_fn_plain))
+              in
               match destruct_exist env arg_ty, destruct_exist env typ_from_fn with
               | Some _, None -> parens (string "projT1 " ^^ arg_pp)
               (* Usually existentials have already been built elsewhere, but this
                  is useful for (e.g.) ranges *)
               | None, Some _ -> parens (string "build_ex " ^^ arg_pp)
+              | Some _, Some _ when is_range_from_atom (env_of arg) arg_ty_plain typ_from_fn_plain ->
+                 parens (string "to_range " ^^ parens (string "projT1 " ^^ arg_pp))
               | _, _ -> arg_pp
             in
             let epp = hang 2 (flow (break 1) (call :: List.map2 doc_arg args arg_typs)) in
+
             (* Decide whether to unpack an existential result, pack one, or cast.
                To do this we compare the expected type stored in the checked expression
                with the inferred type. *)
-            let inst =
-              match instantiation_of_without_type full_exp with
-              | x -> x
-              (* Not all function applications can be inferred, so try falling back to the
-                 type inferred when we know the target type.
-                 TODO: there are probably some edge cases where this won't pick up a need
-                 to cast. *)
-              | exception _ -> instantiation_of full_exp
-            in
-            let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
             let ret_typ_inst =
                  subst_unifiers inst ret_typ
             in
@@ -1033,6 +1112,10 @@ let doc_exp_lem, doc_let_lem =
               let ret_typ_inst =
                 if is_no_Z_proof_fn env f then ret_typ_inst
                 else snd (replace_atom_return_type ret_typ_inst) in
+              let () = 
+                debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst));
+                debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ))
+              in
               let unpack, build_ex, in_typ, out_typ =
                 match ret_typ_inst, ann_typ with
                 | Typ_aux (Typ_exist (_,_,t1),_), Typ_aux (Typ_exist (_,_,t2),_) ->
@@ -1053,10 +1136,13 @@ let doc_exp_lem, doc_let_lem =
                 | _ -> false
               in unpack,build_ex,autocast
             in
-            let autocast_id = if effectful eff then "autocast_m" else "autocast" in
-            let epp = if unpack then string "projT1" ^^ space ^^ parens epp else epp in
+            let autocast_id, proj_id, build_id =
+              if effectful eff
+              then "autocast_m", "projT1_m", "build_ex_m"
+              else "autocast",   "projT1",   "build_ex" in
+            let epp = if unpack then string proj_id ^^ space ^^ parens epp else epp in
             let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in
-            let epp = if build_ex then string "build_ex" ^^ space ^^ parens epp else epp in
+            let epp = if build_ex then string build_id ^^ space ^^ parens epp else epp in
             liftR (if aexp_needed then parens (align epp) else epp)
        end
     | E_vector_access (v,e) ->
@@ -1231,12 +1317,16 @@ let doc_exp_lem, doc_let_lem =
             let epp =
               let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
               let middle =
-                match fst (untyp_pat pat) with
+                match pat with
                 | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) ->
                    string ">>"
-                | P_aux (P_id id,_) ->
+                | P_aux (P_id id,_)
+                   when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) &&
+                        not (is_enum (env_of e1) id) ->
                    separate space [string ">>= fun"; doc_id id; bigarrow]
-                | P_aux (P_typ (typ, P_aux (P_id id,_)),_) ->
+                | P_aux (P_typ (typ, P_aux (P_id id,_)),_)
+                   when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) &&
+                        not (is_enum (env_of e1) id) ->
                    separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow]
                 | _ ->
                    separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow]
@@ -1290,12 +1380,14 @@ let doc_exp_lem, doc_let_lem =
     (* Prefer simple lets over patterns, because I've found Coq can struggle to
        work out return types otherwise *)
     | LB_val(P_aux (P_id id,_),e)
-      when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) ->
+      when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) &&
+           not (is_enum (env_of e) id) ->
        prefix 2 1
               (separate space [string "let"; doc_id id; coloneq])
               (top_exp ctxt false e)
     | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e)
-      when Util.is_none (is_auto_decomposed_exist (env_of e) typ) ->
+      when Util.is_none (is_auto_decomposed_exist (env_of e) typ) &&
+           not (is_enum (env_of e) id) ->
        prefix 2 1
               (separate space [string "let"; doc_id id; colon; doc_typ ctxt typ; coloneq])
               (top_exp ctxt false e)
@@ -1535,10 +1627,6 @@ let rec atom_constraint ctxt (pat, typ) =
      | _ ->
         Some (bquote ^^ braces (string "ArithFact" ^^ space ^^
                                   parens (doc_op equals (doc_id id) (doc_nexp ctxt nexp)))))
-  | P_aux (P_id id, _),
-        Typ_aux (Typ_id (Id_aux (Id "nat",_)),_) ->
-     Some (bquote ^^ braces (string "ArithFact" ^^ space ^^
-                                  parens (doc_op (string ">=") (doc_id id) (string "0"))))
   | P_aux (P_typ (_,p),_), _ -> atom_constraint ctxt (p, typ)
   | _ -> None
 
@@ -1639,6 +1727,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
       kid_id_renames = kid_to_arg_rename;
       bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ);
       build_ex_return = effectful eff && build_ex;
+      debug = List.mem (string_of_id id) (!opt_debug_on)
     } in
   (* Put the constraints after pattern matching so that any type variable that's
      been replaced by one of the term-level arguments is bound. *)
@@ -1650,7 +1739,9 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
     let exp_typ = Env.expand_synonyms env typ in
     match p with
     | P_id id
-    | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) ->
+    | P_typ (_,P_aux (P_id id,_))
+         when Util.is_none (is_auto_decomposed_exist env exp_typ) &&
+              not (is_enum env id) ->
        parens (separate space [doc_id id; colon; doc_typ ctxt typ])
     | _ ->
        (used_a_pattern := true;
@@ -1849,6 +1940,7 @@ let doc_val pat exp =
   in
   let env = env_of exp in
   let typ = expand_range_type (Env.expand_synonyms env (typ_of exp)) in
+  let ctxt = { empty_ctxt with debug  = List.mem (string_of_id id) (!opt_debug_on) } in
   let id, opt_unpack =
     match destruct_exist env typ with
     | None -> id, None
@@ -1863,7 +1955,7 @@ let doc_val pat exp =
   let idpp = doc_id id in
   let basepp =
     group (string "Definition" ^^ space ^^ idpp ^^ typpp ^^ space ^^ coloneq ^/^
-             doc_exp_lem empty_ctxt false exp ^^ dot) ^^ hardline
+             doc_exp_lem ctxt false exp ^^ dot) ^^ hardline
   in
   match opt_unpack with
   | None -> basepp ^^ hardline
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 75284418..d300f699 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -65,8 +65,9 @@ let opt_mwords = ref false
 type context = {
   early_ret : bool;
   bound_nexps : NexpSet.t;
+  top_env : Env.t
 }
-let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty }
+let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty; top_env = Env.empty }
 
 let print_to_from_interp_value = ref false
 let langlebar = string "<|"
@@ -128,7 +129,7 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
   | Id("nat") -> string "integer"
   | Id("Some") -> string "Just"
   | Id("None") -> string "Nothing"
-  | Id i -> string (fix_id false (String.capitalize_ascii i))
+  | Id i -> string (fix_id false (String.capitalize i))
   | DeIid x -> string (Util.zencode_string ("op " ^ x))
 
 let deinfix = function
@@ -328,10 +329,9 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | Typ_arg_order o -> empty
   in typ', atomic_typ
 
-(* Check for variables in types that would be pretty-printed and are not
-   bound in the val spec of the function. *)
+(* Check for variables in types that would be pretty-printed. *)
 let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) =
-  NexpSet.diff (lem_nexps_of_typ typ) ctxt.bound_nexps
+  lem_nexps_of_typ typ
   |> NexpSet.exists (fun nexp -> not (is_nexp_constant nexp))
 
 let replace_typ_size ctxt env (Typ_aux (t,a)) =
@@ -341,29 +341,32 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
        let mk_typ nexp = 
          Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
        in
-       let is_equal nexp =
-         prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
-       in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
-       | nexp -> mk_typ nexp
-       | exception Not_found ->
-          match Type_check.solve env size with
-          | Some n -> mk_typ (nconstant n)
-          | None -> None
+       match Type_check.solve env size with
+       | Some n -> mk_typ (nconstant n)
+       | None ->
+          let is_equal nexp =
+            prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
+          in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
+          | nexp -> mk_typ nexp
+          | exception Not_found -> None
      end
   | _ -> None
 
-let doc_tannot_lem ctxt env eff typ =
-  let of_typ typ =
-    let ta = doc_typ_lem typ in
-    if eff then string " : M " ^^ parens ta
-    else string " : " ^^ ta
-  in
+let make_printable_type ctxt env typ =
   if contains_t_pp_var ctxt typ
   then
     match replace_typ_size ctxt env typ with
-    | None -> empty
-    | Some typ -> of_typ typ
-  else of_typ typ
+    | None -> None
+    | Some typ -> Some typ
+  else Some typ
+
+let doc_tannot_lem ctxt env eff typ =
+  match make_printable_type ctxt env typ with
+  | None -> empty
+  | Some typ ->
+     let ta = doc_typ_lem typ in
+     if eff then string " : M " ^^ parens ta
+     else string " : " ^^ ta
 
 let doc_lit_lem (L_aux(lit,l)) =
   match lit with
@@ -495,8 +498,9 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
      parens (separate comma_sp (List.map2 doc_elem typs pats))
   | P_typ(typ,p) ->
     let doc_p = doc_pat_lem ctxt true p in
-    if contains_t_pp_var ctxt typ then doc_p
-    else parens (doc_op colon doc_p (doc_typ_lem typ))
+    (match make_printable_type ctxt (env_of_annot (l,annot)) typ with
+    | None -> doc_p
+    | Some typ -> parens (doc_op colon doc_p (doc_typ_lem typ)))
   | P_vector pats ->
      let ppp = brackets (separate_map semi (doc_pat_lem ctxt true) pats) in
      if apat_needed then parens ppp else ppp
@@ -727,14 +731,16 @@ let doc_exp_lem, doc_let_lem =
             | [exp] ->
                let epp = separate space [string "early_return"; expY exp] in
                let aexp_needed, tepp =
-                 if contains_t_pp_var ctxt (typ_of exp) ||
-                    contains_t_pp_var ctxt (typ_of full_exp) then
-                   aexp_needed, epp
-                 else
-                   let tannot = separate space [string "MR";
-                     doc_atomic_typ_lem false (typ_of full_exp);
-                     doc_atomic_typ_lem false (typ_of exp)] in
-                   true, doc_op colon epp tannot in
+                 match Util.option_bind (make_printable_type ctxt ctxt.top_env)
+                                        (Env.get_ret_typ (env_of exp)),
+                       make_printable_type ctxt (env_of full_exp) (typ_of full_exp) with
+                   | Some typ, Some full_typ ->
+                     let tannot = separate space [string "MR";
+                       doc_atomic_typ_lem false full_typ;
+                       doc_atomic_typ_lem false typ] in
+                     true, doc_op colon epp tannot
+                   | _ -> aexp_needed, epp
+               in
                if aexp_needed then parens tepp else tepp
             | _ -> raise (Reporting_basic.err_unreachable l
                "Unexpected number of arguments for early_return builtin")
@@ -760,8 +766,12 @@ let doc_exp_lem, doc_let_lem =
                let env = env_of full_exp in
                let t = Env.expand_synonyms env (typ_of full_exp) in
                let eff = effect_of full_exp in
-               if typ_needs_printed t
-               then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true)
+               if typ_needs_printed t then
+                 if Id.compare f (mk_id "bitvector_cast_out") <> 0
+                 then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true)
+                 (* TODO: coordinate with the code in monomorphise.ml to find the correct
+                    typing environment to use *)
+                 else (align (group (prefix 0 1 epp (doc_tannot_lem ctxt ctxt.top_env (effectful eff) t))), true)
                else (epp, aexp_needed) in
              liftR (if aexp_needed then parens (align taepp) else taepp)
           end
@@ -916,12 +926,15 @@ let doc_exp_lem, doc_let_lem =
             "pretty-printing non-constant sizeof expressions to Lem not supported"))
     | E_return r ->
       let ta =
-        if contains_t_pp_var ctxt (typ_of full_exp) || contains_t_pp_var ctxt (typ_of r)
-        then empty
-        else separate space
-          [string ": MR";
-          parens (doc_typ_lem (typ_of full_exp));
-          parens (doc_typ_lem (typ_of r))] in
+        match Util.option_bind (make_printable_type ctxt ctxt.top_env) (Env.get_ret_typ (env_of full_exp)),
+              make_printable_type ctxt (env_of r) (typ_of r) with
+       | Some full_typ, Some r_typ ->
+          separate space
+            [string ": MR";
+            parens (doc_typ_lem full_typ);
+            parens (doc_typ_lem r_typ)]
+       | _ -> empty
+      in
       align (parens (string "early_return" ^//^ expV true r ^//^ ta))
     | E_constraint _ -> string "true"
     | E_internal_value _ ->
@@ -1255,7 +1268,8 @@ let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   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) } in
+      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 pat in
   let patspp = separate_map space (doc_pat_lem ctxt true) pats in
   let _ = match guard with
diff --git a/src/process_file.ml b/src/process_file.ml
index 5fdd3d24..96029587 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -271,14 +271,14 @@ let output_lem filename libs defs =
       operators_module
     ] @ monad_modules
   in
-  let isa_thy_name = String.capitalize_ascii filename ^ "_lemmas" in
+  let isa_thy_name = String.capitalize filename ^ "_lemmas" in
   let isa_lemmas =
     separate hardline [
       string ("theory " ^ isa_thy_name);
       string  "  imports";
       string  "    Sail.Sail2_values_lemmas";
       string  "    Sail.Sail2_state_lemmas";
-      string ("    " ^ String.capitalize_ascii filename);
+      string ("    " ^ String.capitalize filename);
       string  "begin";
       string  "";
       State.generate_isa_lemmas !Pretty_print_lem.opt_mwords defs;
@@ -292,7 +292,7 @@ let output_lem filename libs defs =
     open_output_with_check_unformatted (filename ^ ".lem") in
   (Pretty_print.pp_defs_lem
      (ot, base_imports)
-     (o, base_imports @ (String.capitalize_ascii types_module :: libs))
+     (o, base_imports @ (String.capitalize types_module :: libs))
      defs generated_line);
   close_output_with_check ext_ot;
   close_output_with_check ext_o;
@@ -309,6 +309,7 @@ let output_coq filename libs defs =
   let base_imports = [
       "Sail2_instr_kinds";
       "Sail2_values";
+      "Sail2_string";
       operators_module
     ] @ monad_modules
   in
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 01ff62b1..6d88730d 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -266,7 +266,7 @@ let vector_string_to_bit_list l lit =
     | _ -> raise (Reporting_basic.err_unreachable l "hexchar_to_binlist given unrecognized character") in
 
   let s_bin = match lit with
-    | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase_ascii s_hex)))
+    | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase s_hex)))
     | L_bin s_bin -> explode s_bin
     | _ -> raise (Reporting_basic.err_unreachable l "s_bin given non vector literal") in
 
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 3e582071..da4702b5 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -74,6 +74,8 @@ val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp
 
 val rewrite_pat : tannot rewriters -> tannot pat -> tannot pat
 
+val rewrite_pexp : tannot rewriters -> tannot pexp -> tannot pexp
+
 val rewrite_let : tannot rewriters -> tannot letbind -> tannot letbind
 
 val rewrite_def : tannot rewriters -> tannot def -> tannot def
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 5ed174ea..47c7e923 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1084,9 +1084,11 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
   | _, P_typ (_,pat2) -> subsumes_pat pat1 pat2
   | P_id (Id_aux (id1,_) as aid1), P_id (Id_aux (id2,_) as aid2) ->
     if id1 = id2 then Some []
-    else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound &&
-            Env.lookup_id aid2 (env_of_annot annot2) = Unbound
-           then Some [(id2,id1)] else None
+    else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound
+    then if Env.lookup_id aid2 (env_of_annot annot2) = Unbound
+      then Some [(id2,id1)]
+      else Some []
+    else None
   | P_id id1, _ ->
     if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None
   | P_var (pat1,_), P_var (pat2,_) -> subsumes_pat pat1 pat2
@@ -4043,7 +4045,18 @@ let rewrite_defs_realise_mappings (Defs defs) =
 
 
 (* Rewrite to make all pattern matches in Coq output exhaustive.
-   Assumes that guards, vector patterns, etc have been rewritten already. *)
+   Assumes that guards, vector patterns, etc have been rewritten already,
+   and the scattered functions have been merged.
+   Will add escape effect where a default is needed, so effects will
+   need recalculated afterwards.
+
+   Also detects and removes redundant wildcard patterns at the end of the match.
+   (We could do more, but this is sufficient to deal with the code generated by
+   the mappings rewrites.)
+
+   Note: if this naive implementation turns out to be too slow or buggy, we
+   could look at implementing Maranget JFP 17(3), 2007.
+ *)
 
 let opt_coq_warn_nonexhaustive = ref false
 
@@ -4261,12 +4274,38 @@ let process_pexp env =
      raise (Reporting_basic.err_unreachable l
               "Guarded pattern should have been rewritten away")
 
+(* We do some minimal redundancy checking to remove bogus wildcard patterns here *)
+let check_cases process is_wild loc_of cases =
+  let rec aux rps acc = function
+    | [] -> acc, rps
+    | [p] when is_wild p && match rps with [] -> true | _ -> false ->
+      let () = Reporting_basic.print_err false false
+        (loc_of p) "Match checking" "Redundant wildcard clause" in
+      acc, []
+    | h::t -> aux (process rps h) (h::acc) t
+  in
+  let cases, rps = aux [RP_any] [] cases in
+  List.rev cases, rps
+
+let pexp_is_wild = function
+  | (Pat_aux (Pat_exp (P_aux (P_wild,_),_),_)) -> true
+  | _ -> false
+
+let pexp_loc = function
+  | (Pat_aux (Pat_exp (P_aux (_,(l,_)),_),_)) -> l
+  | (Pat_aux (Pat_when (P_aux (_,(l,_)),_,_),_)) -> l
+
+let funcl_is_wild = function
+  | (FCL_aux (FCL_Funcl (_,pexp),_)) -> pexp_is_wild pexp
+
+let funcl_loc (FCL_aux (_,(l,_))) = l
+
 let rewrite_case (e,ann) =
   match e with
   | E_case (e1,cases) ->
      begin
      let env = env_of_annot ann in
-     let rps = List.fold_left (process_pexp env) [RP_any] cases in
+     let cases, rps = check_cases (process_pexp env) pexp_is_wild pexp_loc cases in
      match rps with
      | [] -> E_aux (E_case (e1,cases),ann)
      | (example::_) ->
@@ -4285,6 +4324,37 @@ let rewrite_case (e,ann) =
      end
   | _ -> E_aux (e,ann)
 
+let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) =
+  let id,fcl_ann =
+    match fcls with
+    | FCL_aux (FCL_Funcl (id,_),ann) :: _ -> id,ann
+    | [] -> raise (Reporting_basic.err_unreachable (fst f_ann)
+                 "Empty function")
+  in
+  let env = env_of_annot fcl_ann in
+  let process_funcl rps (FCL_aux (FCL_Funcl (_,pexp),_)) = process_pexp env rps pexp in
+  let fcls, rps = check_cases process_funcl funcl_is_wild funcl_loc fcls in
+  let fcls' = List.map (function FCL_aux (FCL_Funcl (id,pexp),ann) ->
+                                  FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),ann))
+                fcls in
+  match rps with
+  | [] -> FD_aux (FD_function (r,t,e,fcls'),f_ann)
+  | (example::_) ->
+     let _ =
+       if !opt_coq_warn_nonexhaustive
+       then Reporting_basic.print_err false false
+              (fst f_ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in
+
+     let l = Parse_ast.Generated Parse_ast.Unknown in
+     let p = P_aux (P_wild, (l, empty_tannot)) in
+     let ann' = mk_tannot env (typ_of_annot fcl_ann) (mk_effect [BE_escape]) in
+     (* TODO: use an expression that specifically indicates a failed pattern match *)
+     let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in
+     let default = FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (p,b),(l,empty_tannot))),fcl_ann) in
+
+     FD_aux (FD_function (r,t,e,fcls'@[default]),f_ann)
+  
+
 let rewrite =
   let alg = { id_exp_alg with e_aux = rewrite_case } in
   rewrite_defs_base
@@ -4381,6 +4451,8 @@ let rewrite_defs_lem = [
   ("sizeof", rewrite_sizeof);
   ("early_return", rewrite_defs_early_return);
   ("fix_val_specs", rewrite_fix_val_specs);
+  (* early_return currently breaks the types *)
+  ("recheck_defs", recheck_defs);
   ("remove_blocks", rewrite_defs_remove_blocks);
   ("letbind_effects", rewrite_defs_letbind_effects);
   ("remove_e_assign", rewrite_defs_remove_e_assign);
diff --git a/src/sail.ml b/src/sail.ml
index e698090e..0b56ab21 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -146,6 +146,9 @@ let options = Arg.align ([
   ( "-dcoq_warn_nonex",
     Arg.Set Rewrites.opt_coq_warn_nonexhaustive,
     "Generate warnings for non-exhaustive pattern matches in the Coq backend");
+  ( "-dcoq_debug_on",
+    Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f::!Pretty_print_coq.opt_debug_on),
+    "<function> Produce debug messages for Coq output on given function");
   ( "-latex_prefix",
     Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix),
     " set a custom prefix for generated latex command (default sail)");
diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index 3400d650..586aa54b 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -15,7 +15,8 @@ function extzv(v) = extz_vec(sizeof('m),v)
 val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 overload append = {bitvector_concat}
-val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
 val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
 overload length = {bitvector_length}