Coq: library updates, informative type errors, fix type aliases

(The last bit is to declare type aliases as Type so that Coq uses the
type scope for notation, so * is prod, not multiplication).

6 files changed, 223 insertions, 119 deletions

diff --git a/lib/coq/Prompt.v b/lib/coq/Prompt.v
index 6c4be18e..122da918 100644
--- a/lib/coq/Prompt.v
+++ b/lib/coq/Prompt.v
@@ -30,7 +30,31 @@ match l with
   foreachM xs vars body
 end.
 
-(*declare {isabelle} termination_argument foreachM = automatic
+(*declare {isabelle} termination_argument foreachM = automatic*)
+
+(*val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*)
+Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E :=
+ l >>= (fun l => if l then r else returnm false).
+
+(*val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*)
+Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E :=
+ l >>= (fun l => if l then returnm true else r).
+
+(*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e*)
+Definition bool_of_bitU_fail {rv E} (b : bitU) : monad rv bool E :=
+match b with
+  | B0 => returnm false
+  | B1 => returnm true
+  | BU => Fail "bool_of_bitU"
+end.
+
+(*val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e
+Definition bool_of_bitU_oracle {rv E} (b : bitU) : monad rv bool E :=
+match b with
+  | B0 => returnm false
+  | B1 => returnm true
+  | BU => undefined_bool tt
+end.
 
 
 val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
diff --git a/lib/coq/Prompt_monad.v b/lib/coq/Prompt_monad.v
index ef399444..b457bbf4 100644
--- a/lib/coq/Prompt_monad.v
+++ b/lib/coq/Prompt_monad.v
@@ -144,11 +144,23 @@ Definition try_catchR {rv A R E1 E2} (m : monadR rv A R E1) (h : E1 -> monadR rv
       | inr e => h e
      end).
 
+(*val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e*)
+Definition maybe_fail {rv A E} msg (x : option A) : monad rv A E :=
+match x with
+  | Some a => returnm a
+  | None => Fail msg
+end.
+
+(*val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e*)
+Definition read_mem_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memory_byte) E :=
+  Read_mem rk (bits_of addr) (Z.to_nat sz) returnm.
 
-(*Parameter read_mem : forall {rv n m e}, read_kind -> mword m -> Z -> monad rv (mword n) e.*)
-Definition read_mem {a b e rv : Type} `{Bitvector a} `{Bitvector b}  (rk : read_kind ) (addr : a) (sz : Z )  : monad rv b e:= 
-  let k bytes : monad rv b e := Done (bits_of_mem_bytes bytes) in
-  Read_mem rk (bits_of addr) (Z.to_nat sz) k.
+(*val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e*)
+Definition read_mem {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : monad rv (mword B) E :=
+  bind
+    (read_mem_bytes rk addr sz)
+    (fun bytes =>
+       maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))).
 
 (*val read_tag : forall rv a e. Bitvector a => a -> monad rv bitU e*)
 Definition read_tag {rv a e} `{Bitvector a} (addr : a) : monad rv bitU e :=
diff --git a/lib/coq/Sail_operators.v b/lib/coq/Sail_operators.v
index f94276e9..b14cdd85 100644
--- a/lib/coq/Sail_operators.v
+++ b/lib/coq/Sail_operators.v
@@ -7,16 +7,16 @@ Section Bitvectors.
 Context {a b c} `{Bitvector a} `{Bitvector b} `{Bitvector c}.
 
 (*val concat_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b, Bitvector 'c => 'a -> 'b -> 'c*)
-Definition concat_bv (l : a) (r : b) : c := of_bits (bits_of l ++ bits_of r).
+Definition concat_bv (l : a) (r : b) : list bitU := bits_of l ++ bits_of r.
 
 (*val cons_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b => bitU -> 'a -> 'b*)
-Definition cons_bv b' (v : a) : b := of_bits (b' :: bits_of v).
+Definition cons_bv b' (v : a) : list bitU := b' :: bits_of v.
 
 (*Definition bool_of_bv v := extract_only_element (bits_of v).
 Definition cast_unit_bv b := of_bits [b]
-Definition bv_of_bit len b := of_bits (extz_bits len [b])*)
+Definition bv_of_bit len b := of_bits (extz_bits len [b])
 Definition int_of_bv {a} `{Bitvector a} (sign : bool) : a -> Z := if sign then signed else unsigned.
-(*
+
 Definition most_significant v := match bits_of v with
   | b :: _ -> b
   | _ -> failwith "most_significant applied to empty vector"
@@ -39,7 +39,7 @@ Definition get_min_representable_in _ (n : integer) : integer :=
   else 0 - (integerPow 2 (natFromInteger n))
 
 val bitwise_binop_bv : forall 'a. Bitvector 'a =>
-  (bool -> bool -> bool) -> 'a -> 'a -> 'a*)
+  (bool -> bool -> bool) -> 'a -> 'a -> 'a
 Definition bitwise_binop_bv {a} `{Bitvector a} op (l : a) (r : a) : a :=
  of_bits (binop_bits op (bits_of l) (bits_of r)).
 
@@ -242,7 +242,7 @@ Definition ugteq_bv := ucmp_bv (>=)
 Definition sgteq_bv := scmp_bv (>=)
 *)
 
-(*val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a*)
+(*val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a*)*)
 Definition get_slice_int_bv {a} `{Bitvector a} len n lo : a :=
   let hi := lo + len - 1 in
   let bs := bools_of_int (hi + 1) n in
diff --git a/lib/coq/Sail_operators_mwords.v b/lib/coq/Sail_operators_mwords.v
index a701ddc1..326658d1 100644
--- a/lib/coq/Sail_operators_mwords.v
+++ b/lib/coq/Sail_operators_mwords.v
@@ -1,5 +1,7 @@
 Require Import Sail_values.
 Require Import Sail_operators.
+Require Import Prompt_monad.
+Require Import Prompt.
 Require bbv.Word.
 Require Import Arith.
 Require Import Omega.
@@ -37,22 +39,32 @@ Definition access_vec_inc {a} : mword a -> Z -> bitU := access_mword_inc.
 Definition access_vec_dec {a} : mword a -> Z -> bitU := access_mword_dec.
 
 (*val update_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a*)
-Definition update_vec_inc {a} : mword a -> Z -> bitU -> mword a := update_mword_inc.
+(* TODO: probably ought to use a monadic version instead, but using bad default for
+   type compatibility just now *)
+Definition update_vec_inc {a} (w : mword a) i b : mword a :=
+ opt_def w (update_mword_inc w i b).
 
 (*val update_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a*)
-Definition update_vec_dec {a} : mword a -> Z -> bitU -> mword a := update_mword_dec.
+Definition update_vec_dec {a} (w : mword a) i b : mword a := opt_def w (update_mword_dec w i b).
 
 (*val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b*)
-Definition subrange_vec_inc {a b} `{ArithFact (b >= 0)} (w: mword a) : Z -> Z -> mword b := subrange_bv_inc w.
+(* TODO: get rid of bogus default *)
+Parameter dummy_vector : forall {n} `{ArithFact (n >= 0)}, mword n.
+Definition subrange_vec_inc {a b} `{ArithFact (b >= 0)} (w: mword a) i j : mword b :=
+  opt_def dummy_vector (of_bits (subrange_bv_inc w i j)).
 
 (*val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b*)
-Definition subrange_vec_dec {n m} `{ArithFact (m >= 0)} (w : mword n) : Z -> Z -> mword m := subrange_bv_dec w.
+(* TODO: get rid of bogus default *)
+Definition subrange_vec_dec {n m} `{ArithFact (m >= 0)} (w : mword n) i j :mword m :=
+  opt_def dummy_vector (of_bits (subrange_bv_dec w i j)).
 
 (*val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a*)
-Definition update_subrange_vec_inc {a b} (v : mword a) i j (w : mword b) : mword a := update_subrange_bv_inc v i j w.
+Definition update_subrange_vec_inc {a b} (v : mword a) i j (w : mword b) : mword a :=
+  opt_def dummy_vector (of_bits (update_subrange_bv_inc v i j w)).
 
 (*val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a*)
-Definition update_subrange_vec_dec {a b} (v : mword a) i j (w : mword b) : mword a := update_subrange_bv_dec v i j w.
+Definition update_subrange_vec_dec {a b} (v : mword a) i j (w : mword b) : mword a :=
+  opt_def dummy_vector (of_bits (update_subrange_bv_dec v i j w)).
 
 Lemma mword_nonneg {a} : mword a -> a >= 0.
 destruct a;
@@ -61,7 +73,7 @@ destruct 1.
 Qed.
 
 (*val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
-Definition extz_vec {a b} `{ArithFact (b >= 0)} `{ArithFact (b >= a)} (n : Z) (v : mword a) : mword b.
+Definition extz_vec {a b} `{ArithFact (b >= a)} (n : Z) (v : mword a) : mword b.
 refine (cast_to_mword (Word.zext (get_word v) (Z.to_nat (b - a))) _).
 unwrap_ArithFacts.
 assert (a >= 0). { apply mword_nonneg. assumption. }
@@ -72,7 +84,15 @@ auto with zarith.
 Defined.
 
 (*val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*)
-Definition exts_vec {a b} `{ArithFact (b >= 0)} (n : Z) (v : mword a) : mword b := exts_bv n v.
+Definition exts_vec {a b} `{ArithFact (b >= a)} (n : Z) (v : mword a) : mword b.
+refine (cast_to_mword (Word.sext (get_word v) (Z.to_nat (b - a))) _).
+unwrap_ArithFacts.
+assert (a >= 0). { apply mword_nonneg. assumption. }
+rewrite <- Z2Nat.inj_add; try omega.
+rewrite Zplus_minus.
+apply Z2Nat.id.
+auto with zarith.
+Defined.
 
 Definition zero_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n := extz_vec n v.
 
@@ -112,7 +132,13 @@ Definition cast_unit_vec := cast_unit_bv
 val vec_of_bit : forall 'a. Size 'a => integer -> bitU -> mword 'a
 Definition vec_of_bit := bv_of_bit*)
 
-Definition vec_of_bits {a} `{ArithFact (a >= 0)} (l:list bitU) : mword a := of_bits l.
+Lemma length_list_pos : forall {A} {l:list A}, length_list l >= 0.
+unfold length_list.
+auto with zarith.
+Qed.
+Hint Resolve length_list_pos : sail.
+
+Definition vec_of_bits (l:list bitU) : mword (length_list l) := opt_def dummy_vector (of_bits l).
 (*
 
 val msb : forall 'a. Size 'a => mword 'a -> bitU
@@ -122,36 +148,41 @@ val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer
 Definition int_of_vec := int_of_bv
 
 val string_of_vec : forall 'a. Size 'a => mword 'a -> string
-Definition string_of_vec := string_of_bv
+Definition string_of_vec := string_of_bv*)
+Definition with_word' {n} (P : Type -> Type) : (forall n, Word.word n -> P (Word.word n)) -> mword n -> P (mword n) := fun f w => @with_word n _ (f (Z.to_nat n)) w.
+Definition word_binop {n} (f : forall n, Word.word n -> Word.word n -> Word.word n) : mword n -> mword n -> mword n := with_word' (fun x => x -> x) f.
+Definition word_unop {n} (f : forall n, Word.word n -> Word.word n) : mword n -> mword n := with_word' (fun x => x) f.
 
+
+(*
 val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val or_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val not_vec : forall 'a. Size 'a => mword 'a -> mword 'a*)
-Definition and_vec {n} (w : mword n) : mword n -> mword n := and_bv w.
-Definition or_vec  {n} (w : mword n) : mword n -> mword n := or_bv w.
-Definition xor_vec {n} (w : mword n) : mword n -> mword n := xor_bv w.
-Definition not_vec {n} (w : mword n) : mword n := not_bv w.
+Definition and_vec {n} : mword n -> mword n -> mword n := word_binop Word.wand.
+Definition or_vec  {n} : mword n -> mword n -> mword n := word_binop Word.wor.
+Definition xor_vec {n} : mword n -> mword n -> mword n := word_binop Word.wxor.
+Definition not_vec {n} : mword n -> mword n := word_unop Word.wnot.
 
 (*val add_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val sadd_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val sub_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val mult_vec  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
 val smult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b*)
-Definition add_vec {n} (w : mword n) : mword n -> mword n := add_bv w.
-Definition sadd_vec {n} (w : mword n) : mword n -> mword n := sadd_bv w.
-Definition sub_vec  {n} (w : mword n) : mword n -> mword n := sub_bv w.
-Definition mult_vec {n} (w : mword n) : mword n -> mword n := mult_bv w.
-Definition smult_vec {n} (w : mword n) : mword n -> mword n := smult_bv w.
+Definition add_vec   {n} : mword n -> mword n -> mword n := word_binop Word.wplus.
+(*Definition sadd_vec  {n} : mword n -> mword n -> mword n := sadd_bv w.*)
+Definition sub_vec   {n} : mword n -> mword n -> mword n := word_binop Word.wminus.
+Definition mult_vec  {n} : mword n -> mword n -> mword n := word_binop Word.wmult.
+(*Definition smult_vec {n} : mword n -> mword n -> mword n := smult_bv w.*)
 
 (*val add_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val sadd_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val sub_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val mult_vec_int  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
 val smult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*)
-Definition add_vec_int   {a} (w : mword a) : Z -> mword a := add_bv_int w.
+(*Definition add_vec_int   {a} (w : mword a) : Z -> mword a := add_bv_int w.
 Definition sadd_vec_int  {a} (w : mword a) : Z -> mword a := sadd_bv_int w.
-Definition sub_vec_int   {a} (w : mword a) : Z -> mword a := sub_bv_int w.
+Definition sub_vec_int   {a} (w : mword a) : Z -> mword a := sub_bv_int w.*)
 (*Definition mult_vec_int  {a b} : mword a -> Z -> mword b := mult_bv_int.
 Definition smult_vec_int {a b} : mword a -> Z -> mword b := smult_bv_int.*)
 
@@ -221,7 +252,19 @@ Definition mod_vec_int  := mod_bv_int
 Definition quot_vec_int := quot_bv_int
 
 val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*)
-Definition replicate_bits {a b} `{ArithFact (b >= 0)} (w : mword a) : Z -> mword b := replicate_bits_bv w.
+Fixpoint replicate_bits_aux {a} (w : Word.word a) (n : nat) : Word.word (n * a) :=
+match n with
+| O => Word.WO
+| S m => Word.combine w (replicate_bits_aux w m)
+end.
+Lemma replicate_ok {n a} `{ArithFact (n >= 0)} `{ArithFact (a >= 0)} :
+   Z.of_nat (Z.to_nat n * Z.to_nat a) = n * a.
+destruct H. destruct H0.
+rewrite <- Z2Nat.id; auto with zarith.
+rewrite Z2Nat.inj_mul; auto with zarith.
+Qed.
+Definition replicate_bits {a} (w : mword a) (n : Z) `{ArithFact (n >= 0)} : mword (n * a) :=
+ cast_to_mword (replicate_bits_aux (get_word w) (Z.to_nat n)) replicate_ok.
 
 (*val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a
 Definition duplicate := duplicate_bit_bv
@@ -236,8 +279,8 @@ val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool*)
-Definition eq_vec  {n} (w : mword n) : mword n -> bool := eq_bv w.
-Definition neq_vec {n} (w : mword n) : mword n -> bool := neq_bv w.
+Definition eq_vec  {n} (x : mword n) (y : mword n) : bool := Word.weqb (get_word x) (get_word y).
+Definition neq_vec {n} (x : mword n) (y : mword n) : bool := negb (eq_vec x y).
 (*Definition ult_vec   := ult_bv.
 Definition slt_vec   := slt_bv.
 Definition ugt_vec   := ugt_bv.
diff --git a/lib/coq/Sail_values.v b/lib/coq/Sail_values.v
index 930d4a47..c211cfdc 100644
--- a/lib/coq/Sail_values.v
+++ b/lib/coq/Sail_values.v
@@ -125,6 +125,24 @@ Definition min_8   := (0 - 128 : Z)
 Definition max_5   := (31 : Z)
 Definition min_5   := (0 - 32 : Z)
 *)
+
+(* just_list takes a list of maybes and returns Some xs if all elements have
+   a value, and None if one of the elements is None. *)
+(*val just_list : forall a. list (option a) -> option (list a)*)
+Fixpoint just_list {A} (l : list (option A)) := match l with
+  | [] => Some []
+  | (x :: xs) =>
+    match (x, just_list xs) with
+      | (Some x, Some xs) => Some (x :: xs)
+      | (_, _) => None
+    end
+  end.
+(*declare {isabelle} termination_argument just_list = automatic
+
+lemma just_list_spec:
+  ((forall xs. (just_list xs = None) <-> List.elem None xs) &&
+   (forall xs es. (just_list xs = Some es) <-> (xs = List.map Some es)))*)
+
 (*** Bits *)
 Inductive bitU := B0 | B1 | BU.
 
@@ -149,21 +167,18 @@ Instance bitU_BitU : (BitU bitU) := {
   of_bitU b := b
 }.
 
-(* TODO: consider alternatives *)
-Parameter undefined_BU : bool.
-
 Definition bool_of_bitU bu := match bu with
-  | B0 => false
-  | B1 => true
-  | BU => undefined_BU (*failwith "bool_of_bitU applied to BU"*)
+  | B0 => Some false
+  | B1 => Some true
+  | BU => None
   end.
 
 Definition bitU_of_bool (b : bool) := if b then B1 else B0.
 
-Instance bool_BitU : (BitU bool) := {
+(*Instance bool_BitU : (BitU bool) := {
   to_bitU := bitU_of_bool;
   of_bitU := bool_of_bitU
-}.
+}.*)
 
 Definition cast_bit_bool := bool_of_bitU.
 (*
@@ -319,11 +334,10 @@ Definition bits_of_nat n := List.rev (bits_of_nat_aux n n).
 
 (*val nat_of_bits_aux : natural -> list bitU -> natural*)
 Fixpoint nat_of_bits_aux acc bs := match bs with
-  | [] => acc
+  | [] => Some acc
   | B1 :: bs => nat_of_bits_aux ((2 * acc) + 1) bs
   | B0 :: bs => nat_of_bits_aux (2 * acc) bs
-  | BU :: bs => (*failwith "nat_of_bits_aux: bit list has undefined bits"*)
-                nat_of_bits_aux ((2 * acc) + if undefined_BU then 1 else 0) bs
+  | BU :: bs => None
 end%nat.
 (*declare {isabelle} termination_argument nat_of_bits_aux = automatic*)
 Definition nat_of_bits bits := nat_of_bits_aux 0 bits.
@@ -338,18 +352,23 @@ Definition or_bits := binop_bits (||)
 Definition xor_bits := binop_bits xor
 
 val unsigned_of_bits : list bitU -> Z*)
-Definition unsigned_of_bits bs := Z.of_nat (nat_of_bits bs).
+Definition unsigned_of_bits bits :=
+match just_list (List.map bool_of_bitU bits) with
+| Some bs => Some (unsigned_of_bools bs)
+| None => None
+end.
 
 (*val signed_of_bits : list bitU -> Z*)
-Parameter undefined_Z : Z.
 Definition signed_of_bits bits :=
-  match bits with
-  | B1 :: _ => 0 - (1 + (unsigned_of_bits (not_bits bits)))
-  | B0 :: _ => unsigned_of_bits bits
-  | BU :: _ => undefined_Z (*failwith "signed_of_bits applied to list with undefined bits"*)
-  | [] => undefined_Z (*failwith "signed_of_bits applied to empty list"*)
+  match just_list (List.map bool_of_bitU bits) with
+  | Some bs => Some (signed_of_bools bs)
+  | None => None
   end.
 
+(*val int_of_bits : bool -> list bitU -> maybe integer*)
+Definition int_of_bits (sign : bool) bs :=
+ if sign then signed_of_bits bs else unsigned_of_bits bs.
+
 (*val pad_bitlist : bitU -> list bitU -> Z -> list bitU*)
 Fixpoint pad_bitlist_nat (b : bitU) bits n :=
 match n with
@@ -386,11 +405,21 @@ Definition add_one_bit_ignore_overflow bits :=
   rev (add_one_bit_ignore_overflow_aux (rev bits)).
 
 Definition bitlist_of_int n :=
-  let bits_abs := B0 :: bits_of_nat (Zabs_nat n) in
+  let bits_abs := B0 :: bits_of_nat (Z.abs_nat n) in
   if n >=? 0 then bits_abs
   else add_one_bit_ignore_overflow (not_bits bits_abs).
 
 Definition bits_of_int len n := exts_bits len (bitlist_of_int n).
+
+(*val arith_op_bits :
+  (integer -> integer -> integer) -> bool -> list bitU -> list bitU -> list bitU*)
+Definition arith_op_bits (op : Z -> Z -> Z) (sign : bool) l r :=
+  match (int_of_bits sign l, int_of_bits sign r) with
+    | (Some li, Some ri) => bits_of_int (length_list l) (op li ri)
+    | (_, _) => repeat [BU] (length_list l)
+  end.
+
+
 (*
 Definition char_of_nibble := function
   | (B0, B0, B0, B0) => Some #'0'
@@ -558,23 +587,6 @@ Definition update_list {A} (is_inc : bool) (xs : list A) n x :=
   | _ => failwith "extract_only_element called for list with more elements"
 end
 
-(* just_list takes a list of maybes and returns Some xs if all elements have
-   a value, and None if one of the elements is None. *)
-val just_list : forall a. list (option a) -> option (list a)*)
-Fixpoint just_list {A} (l : list (option A)) := match l with
-  | [] => Some []
-  | (x :: xs) =>
-    match (x, just_list xs) with
-      | (Some x, Some xs) => Some (x :: xs)
-      | (_, _) => None
-    end
-  end.
-(*declare {isabelle} termination_argument just_list = automatic
-
-lemma just_list_spec:
-  ((forall xs. (just_list xs = None) <-> List.elem None xs) &&
-   (forall xs es. (just_list xs = Some es) <-> (xs = List.map Some es)))
-
 (*** Machine words *)
 *)
 Definition mword (n : Z) :=
@@ -660,9 +672,14 @@ match n with
   if b then masked else wor masked bit
 end.
 
-(*val update_mword_dec : forall a. mword a -> Z -> bitU -> mword a*)
-Definition update_mword_dec {a} (w : mword a) n b : mword a :=
- with_word (P := id) (fun w => setBit w (Z.to_nat n) (bool_of_bitU b)) w.
+(*val update_mword_bool_dec : forall 'a. mword 'a -> integer -> bool -> mword 'a*)
+Definition update_mword_bool_dec {a} (w : mword a) n b : mword a :=
+  with_word (P := id) (fun w => setBit w (Z.to_nat n) b) w.
+Definition update_mword_dec {a} (w : mword a) n b :=
+ match bool_of_bitU b with
+ | Some bl => Some (update_mword_bool_dec w n bl)
+ | None => None
+ end.
 
 (*val update_mword_inc : forall a. mword a -> Z -> bitU -> mword a*)
 Definition update_mword_inc {a} (w : mword a) n b :=
@@ -673,17 +690,26 @@ Definition update_mword_inc {a} (w : mword a) n b :=
 Definition update_mword {a} (is_inc : bool) (w : mword a) n b :=
   if is_inc then update_mword_inc w n b else update_mword_dec w n b.
 
+(*val int_of_mword : forall 'a. bool -> mword 'a -> integer*)
+Definition int_of_mword {a} `{ArithFact (a >= 0)} (sign : bool) (w : mword a) :=
+  if sign then wordToZ (get_word w) else Z.of_N (wordToN (get_word w)).
+
+
 (*val mword_of_int : forall a. Size a => Z -> Z -> mword a
 Definition mword_of_int len n :=
   let w := wordFromInteger n in
   if (length_mword w = len) then w else failwith "unexpected word length"
 *)
-Program Definition mword_of_int len {H:len >= 0} n : mword len :=
+Program Definition mword_of_int {len} `{H:ArithFact (len >= 0)} n : mword len :=
 match len with
 | Zneg _ => _
 | Z0 => ZToWord 0 n
 | Zpos p => ZToWord (Pos.to_nat p) n
 end.
+Next Obligation.
+destruct H.
+auto.
+Defined.
 (*
 (* Translating between a type level number (itself n) and an integer *)
 
@@ -738,39 +764,25 @@ Local Close Scope nat.
 
 Class Bitvector (a:Type) : Type := {
   bits_of : a -> list bitU;
-  of_bits : list bitU -> a;
+  of_bits : list bitU -> option a;
   of_bools : list bool -> a;
   (* The first parameter specifies the desired length of the bitvector *)
   of_int : Z -> Z -> a;
   length : a -> Z;
-  unsigned : a -> Z;
-  signed : a -> Z;
-  (* The first parameter specifies the indexing order (true is increasing) *)
-  get_bit : bool -> a -> Z -> bitU;
-  set_bit : bool -> a -> Z -> bitU -> a;
-  get_bits : bool -> a -> Z -> Z -> list bitU;
-  set_bits : bool -> a -> Z -> Z -> list bitU -> a
+  unsigned : a -> option Z;
+  signed : a -> option Z;
+  arith_op_bv : (Z -> Z -> Z) -> bool -> a -> a -> a
 }.
 
-Parameter undefined_bitU : bitU. (* A missing value of type bitU, as opposed to BU, which is an undefined bit *)
-Definition opt_bitU {a : Type} `{BitU a} (b : option a) :=
-match b with
-| None => undefined_bitU
-| Some c => to_bitU c
-end.
-
 Instance bitlist_Bitvector {a : Type} `{BitU a} : (Bitvector (list a)) := {
   bits_of v := List.map to_bitU v;
-  of_bits v := List.map of_bitU v;
+  of_bits v := Some (List.map of_bitU v);
   of_bools v := List.map of_bitU (List.map bitU_of_bool v);
   of_int len n := List.map of_bitU (bits_of_int len n);
   length := length_list;
   unsigned v := unsigned_of_bits (List.map to_bitU v);
   signed v := signed_of_bits (List.map to_bitU v);
-  get_bit is_inc v n := opt_bitU (access_list_opt is_inc v n);
-  set_bit is_inc v n b := update_list is_inc v n (of_bitU b);
-  get_bits is_inc v i j := List.map to_bitU (subrange_list is_inc v i j);
-  set_bits is_inc v i j v' := update_subrange_list is_inc v i j (List.map of_bitU v')
+  arith_op_bv op sign l r := List.map of_bitU (arith_op_bits op sign (List.map to_bitU l) (List.map to_bitU r))
 }.
 
 Class ReasonableSize (a : Z) : Prop := {
@@ -854,40 +866,44 @@ Abort.
 
 Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; omega]) : typeclass_instances.
 
-Instance mword_Bitvector {a : Z} `{ReasonableSize a} : (Bitvector (mword a)) := {
-  bits_of v := List.map to_bitU (bitlistFromWord (get_word v));
-  of_bits v := to_word isPositive (fit_bbv_word (wordFromBitlist (List.map of_bitU v)));
+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));
   of_bools v := to_word isPositive (fit_bbv_word (wordFromBitlist v));
-  of_int len z := @mword_of_int a isPositive z; (* cheat a little *)
+  of_int len z := mword_of_int z; (* cheat a little *)
   length v := a;
-  unsigned v := Z.of_N (wordToN (get_word v));
-  signed v := wordToZ (get_word v);
-  get_bit := access_mword;
-  set_bit := update_mword;
-  get_bits is_inc v i j := get_bits is_inc (bitlistFromWord (get_word v)) i j;
-  set_bits is_inc v i j v' := to_word isPositive (fit_bbv_word (wordFromBitlist (set_bits is_inc (bitlistFromWord (get_word v)) i j v')))
+  unsigned v := Some (Z.of_N (wordToN (get_word v)));
+  signed v := Some (wordToZ (get_word v));
+  arith_op_bv op sign l r := mword_of_int (op (int_of_mword sign l) (int_of_mword sign r))
 }.
 
 Section Bitvector_defs.
 Context {a b} `{Bitvector a} `{Bitvector b}.
 
-Definition access_bv_inc (v : a) n := get_bit true  v n.
-Definition access_bv_dec (v : a) n := get_bit false v n.
+Definition opt_def {a} (def:a) (v:option a) :=
+match v with
+| Some x => x
+| None => def
+end.
+
+(* The Lem version is partial, but lets go with BU here to avoid constraints for now *)
+Definition access_bv_inc (v : a) n := opt_def BU (access_list_opt_inc (bits_of v) n).
+Definition access_bv_dec (v : a) n := opt_def BU (access_list_opt_dec (bits_of v) n).
 
-Definition update_bv_inc (v : a) n b := set_bit true  v n b.
-Definition update_bv_dec (v : a) n b := set_bit false v n b.
+Definition update_bv_inc (v : a) n b := update_list true  (bits_of v) n b.
+Definition update_bv_dec (v : a) n b := update_list false (bits_of v) n b.
 
-Definition subrange_bv_inc (v : a) i j : b := of_bits (get_bits true  v i j).
-Definition subrange_bv_dec (v : a) i j : b := of_bits (get_bits false v i j).
+Definition subrange_bv_inc (v : a) i j := subrange_list true  (bits_of v) i j.
+Definition subrange_bv_dec (v : a) i j := subrange_list true  (bits_of v) i j.
 
-Definition update_subrange_bv_inc (v : a) i j (v' : b) := set_bits true  v i j (bits_of v').
-Definition update_subrange_bv_dec (v : a) i j (v' : b) := set_bits false v i j (bits_of v').
+Definition update_subrange_bv_inc (v : a) i j (v' : b) := update_subrange_list true  (bits_of v) i j (bits_of v').
+Definition update_subrange_bv_dec (v : a) i j (v' : b) := update_subrange_list false (bits_of v) i j (bits_of v').
 
 (*val extz_bv : forall a b. Bitvector a, Bitvector b => Z -> a -> b*)
-Definition extz_bv n (v : a) : b := of_bits (extz_bits n (bits_of v)).
+Definition extz_bv n (v : a) : option b := of_bits (extz_bits n (bits_of v)).
 
 (*val exts_bv : forall a b. Bitvector a, Bitvector b => Z -> a -> b*)
-Definition exts_bv n (v : a) :b := of_bits (exts_bits n (bits_of v)).
+Definition exts_bv n (v : a) : option b := of_bits (exts_bits n (bits_of v)).
 
 (*val string_of_bv : forall a. Bitvector a => a -> string
 Definition string_of_bv v := show_bitlist (bits_of v)
@@ -917,10 +933,10 @@ Context {a} `{Bitvector a}.
 Definition bytes_of_bits (bs : a) := byte_chunks (bits_of bs).
 
 (*val bits_of_bytes : forall a. Bitvector a => list memory_byte -> a*)
-Definition bits_of_bytes (bs : list memory_byte) : a := of_bits (List.concat (List.map bits_of bs)).
+Definition bits_of_bytes (bs : list memory_byte) : list bitU := List.concat (List.map bits_of bs).
 
 Definition mem_bytes_of_bits (bs : a) := option_map (@rev (list bitU)) (bytes_of_bits bs).
-Definition bits_of_mem_bytes (bs : list memory_byte) : a := bits_of_bytes (List.rev bs).
+Definition bits_of_mem_bytes (bs : list memory_byte) := bits_of_bytes (List.rev bs).
 
 End BytesBits.
 (*
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 26f66b47..35bf9a56 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1187,7 +1187,9 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
 let doc_typdef (TD_aux(td, (l, annot))) = match td with
   | TD_abbrev(id,nm,(TypSchm_aux (TypSchm_ts (typq, _), _) as typschm)) ->
      doc_op coloneq
-       (separate space [string "Definition"; doc_id_type id; doc_typquant_items empty_ctxt parens typq])
+       (separate space [string "Definition"; doc_id_type id;
+                        doc_typquant_items empty_ctxt parens typq;
+                        colon; string "Type"])
        (doc_typschm empty_ctxt false typschm) ^^ dot
   | TD_record(id,nm,typq,fs,_) ->
     let fname fid = if prefix_recordtype && string_of_id id <> "regstate"
@@ -1758,4 +1760,11 @@ string "Require Import List. Import ListNotations. Require Import Sumbool.";
         hardline;
         string "End Content.";
         hardline])
-with Type_check.Type_error (l,err) -> raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
+with Type_check.Type_error (l,err) ->
+  let extra =
+    "\nError during Coq printing\n" ^
+    if Printexc.backtrace_status ()
+    then "\n" ^ Printexc.get_backtrace ()
+    else "(backtracing unavailable)"
+  in
+  raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err ^ extra))