diff --git a/heapster-saw/examples/arrays.saw b/heapster-saw/examples/arrays.saw
index e5a0f6bd70..1a12837847 100644
--- a/heapster-saw/examples/arrays.saw
+++ b/heapster-saw/examples/arrays.saw
@@ -1,29 +1,28 @@
 enable_experimental;
 env <- heapster_init_env_from_file "arrays.sawcore" "arrays.bc";
 
-heapster_typecheck_fun env "contains0_rec_" "(len:bv 64).arg0:eq(llvmword(len)), arg1:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg2:(exists z:bv 64.eq(llvmword(z))) -o arg0:true, arg1:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg2:true, ret:exists z:(bv 64).eq(llvmword(z))";
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
+
+heapster_define_perm env "int64array" "len:bv 64" "llvmptr 64" "array(0,<len,*8,[(W,0) |-> int64<>])";
+
+
+heapster_typecheck_fun env "contains0_rec_" "(len:bv 64).arg0:eq(llvmword(len)), arg1:int64array<len>, arg2:int64<> -o arg0:true, arg1:int64array<len>, arg2:true, ret:int64<>";
 
 // the old way using a block entry hint
 // heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 // heapster_block_entry_hint env "contains0" 9 "top0:bv 64, top1:llvmptr 64, top2:llvmptr 64" "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64" "top0:true, top1:array(0,<top0,*1,[(W,0) |-> int64<>]), top2:eq(llvmword(top0)), arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(x1)), arg2:ptr((W,0) |-> eq(x0)), arg3:ptr((W,0) |-> int64<>), frm:llvmframe [arg3:8, arg2:8, arg1:8, arg0:8], x0:eq(top2), x1:eq(top1)";
 // heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:true, ret:int64<>";
 
-// the new way using a gen perms hint
-heapster_gen_block_perms_hint env "contains0" []; // Note that we could give specific block numbers here (e.g. [9]), but giving nothing will just add a hint to every block, which works just fine for this function.
-heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:true, ret:exists z:(bv 64).eq(llvmword(z))";
+heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:int64<>";
 
-// the new way using a gen perms hint
-heapster_gen_block_perms_hint env "zero_array" [];
-heapster_typecheck_fun env "zero_array" "(len:bv 64).arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:true, ret:true";
+heapster_typecheck_fun env "zero_array" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:true";
 
-heapster_gen_block_perms_hint env "zero_array_from" [];
-heapster_typecheck_fun env "zero_array_from" "(len:bv 64, off:bv 64).arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:eq(llvmword(len)), arg2:eq(llvmword(off)) -o arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:true, ret:true";
+heapster_typecheck_fun env "zero_array_from" "(len:bv 64, off:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)), arg2:eq(llvmword(off)) -o arg0:int64array<len>, arg1:true, ret:true";
 
-heapster_gen_block_perms_hint env "filter_and_sum_pos" [];
 heapster_join_point_hint env "filter_and_sum_pos" [];
-heapster_typecheck_fun env "filter_and_sum_pos" "(len:bv 64).arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))]), arg1:true, ret:exists x:bv 64.eq(llvmword(x))";
+heapster_typecheck_fun env "filter_and_sum_pos" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:int64<>";
 
-heapster_gen_block_perms_hint env "sum_2d" [];
-heapster_typecheck_fun env "sum_2d" "(l1:bv 64,l2:bv 64).arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:true, arg2:true, ret:exists x:bv 64.eq(llvmword(x))";
+heapster_typecheck_fun env "sum_2d" "(l1:bv 64,l2:bv 64).arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:true, arg2:true, ret:int64<>";
 
 heapster_export_coq env "arrays_gen.v";
diff --git a/heapster-saw/examples/clearbufs.sawcore b/heapster-saw/examples/clearbufs.sawcore
index b4d749c576..794f9a00bf 100644
--- a/heapster-saw/examples/clearbufs.sawcore
+++ b/heapster-saw/examples/clearbufs.sawcore
@@ -25,9 +25,9 @@ Mbox_def = Mbox;
             (m:Mbox) -> P m;
 Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m; -}
 
---unfoldMbox : Mbox -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #());
+--unfoldMbox : Mbox -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool));
 primitive
-unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool) * #()));
+unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool)));
 
 {-unfoldMbox m =
   Mbox__rec (\ (_:Mbox) -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()))
@@ -38,7 +38,7 @@ unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 l
   -}
 
 primitive
-foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool) * #())) -> Mbox;
+foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool))) -> Mbox;
 
 --(Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #()) -> Mbox;
 {-
diff --git a/heapster-saw/examples/iter_linked_list.sawcore b/heapster-saw/examples/iter_linked_list.sawcore
index 9a473ccbf3..fbb59e816b 100644
--- a/heapster-saw/examples/iter_linked_list.sawcore
+++ b/heapster-saw/examples/iter_linked_list.sawcore
@@ -27,20 +27,20 @@ ListF__rec : (a b:sort 0) -> (P : ListF a b -> sort 0) ->
              (l:ListF a b) -> P l;
 ListF__rec a b P f1 f2 l = ListF#rec a b P f1 f2 l;
 
-unfoldListF : (a b:sort 0) -> ListF a b -> Either b (a * ListF a b * #());
+unfoldListF : (a b:sort 0) -> ListF a b -> Either b (a * ListF a b);
 unfoldListF a b l =
-  ListF__rec a b (\ (_:ListF a b) -> Either b (a * ListF a b * #()))
-  (\ (x:b) -> Left b (a * ListF a b * #()) x)
-  (\ (x:a) (l:ListF a b) (_:Either b (a * ListF a b * #())) ->
-     Right b (a * ListF a b * #()) (x, l, ()))
+  ListF__rec a b (\ (_:ListF a b) -> Either b (a * ListF a b))
+  (\ (x:b) -> Left b (a * ListF a b) x)
+  (\ (x:a) (l:ListF a b) (_:Either b (a * ListF a b)) ->
+     Right b (a * ListF a b) (x, l))
   l;
 
-foldListF : (a b:sort 0) -> Either b (a * ListF a b * #()) -> ListF a b;
+foldListF : (a b:sort 0) -> Either b (a * ListF a b) -> ListF a b;
 foldListF a b =
-  either b (a * ListF a b * #()) (ListF a b)
+  either b (a * ListF a b) (ListF a b)
          (\ (x : b) -> NilF a b x)
-         (\ (tup : (a * ListF a b * #())) ->
-            ConsF a b tup.(1) tup.(2).(1));
+         (\ (tup : (a * ListF a b)) ->
+            ConsF a b tup.(1) tup.(2));
 
 getListF : (a b:sort 0) -> ListF a b -> b;
 getListF a b =
diff --git a/heapster-saw/examples/mbox.saw b/heapster-saw/examples/mbox.saw
index c92785b703..19844ce74b 100644
--- a/heapster-saw/examples/mbox.saw
+++ b/heapster-saw/examples/mbox.saw
@@ -43,7 +43,7 @@ heapster_define_perm env "boolean" " " "llvmptr 1" "exists x:bv 1.eq(llvmword(x)
 
 heapster_assume_fun env "llvm.objectsize.i64.p0i8" "().empty -o empty" "returnM #() ()";
 
-heapster_assume_fun env "__memcpy_chk" "(len:bv 64).arg0:byte_array<W,len>,arg1:byte_array<W,len>,arg2:eq(llvmword (len)) -o arg0:byte_array<W,len>,arg1:byte_array<W,len>" "\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool) * #()) (src, src, ())";
+heapster_assume_fun env "__memcpy_chk" "(len:bv 64).arg0:byte_array<W,len>,arg1:byte_array<W,len>,arg2:eq(llvmword (len)) -o arg0:byte_array<W,len>,arg1:byte_array<W,len>" "\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool)) (src, src)";
 
 
 //------------------------------------------------------------------------------
diff --git a/heapster-saw/examples/mbox.sawcore b/heapster-saw/examples/mbox.sawcore
index 1e260e6bd8..28b4106695 100644
--- a/heapster-saw/examples/mbox.sawcore
+++ b/heapster-saw/examples/mbox.sawcore
@@ -31,20 +31,20 @@ Mbox__rec : (P : Mbox -> sort 0) ->
             (m:Mbox) -> P m;
 Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m;
 
-unfoldMbox : Mbox -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool) * #());
+unfoldMbox : Mbox -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool));
 unfoldMbox m =
-  Mbox__rec (\ (_:Mbox) -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool) * #()))
-  (Left #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool) * #()) ())
-  (\ (strt:Vec 64 Bool) (len:Vec 64 Bool) (m:Mbox) (_:Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool) * #())) (d:BVVec 64 bv64_128 (Vec 8 Bool)) ->
-     Right #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool) * #()) (strt, len, m, d, ()))
+  Mbox__rec (\ (_:Mbox) -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)))
+  (Left #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) ())
+  (\ (strt:Vec 64 Bool) (len:Vec 64 Bool) (m:Mbox) (_:Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) (d:BVVec 64 bv64_128 (Vec 8 Bool)) ->
+     Right #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) (strt, len, m, d))
   m;
 
-foldMbox : Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * (BVVec 64 bv64_128 (Vec 8 Bool)) * #()) -> Mbox;
+foldMbox : Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox;
 foldMbox =
-  either #() (Vec 64 Bool * Vec 64 Bool * Mbox * (BVVec 64 bv64_128 (Vec 8 Bool)) * #()) Mbox
+  either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) Mbox
          (\ (_:#()) -> Mbox_nil)
-         (\ (tup : (Vec 64 Bool * Vec 64 Bool * Mbox * (BVVec 64 bv64_128 (Vec 8 Bool)) * #())) ->
-            Mbox_cons tup.1 tup.2 tup.3 tup.4);
+         (\ (tup : (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) ->
+            Mbox_cons tup.1 tup.2 tup.3 tup.(2).(2).(2));
 
 {-
 getMbox : (a : sort 0) -> Mbox a -> a;
diff --git a/heapster-saw/examples/mbox_proofs.v b/heapster-saw/examples/mbox_proofs.v
index 9c6fa1f849..260d132663 100644
--- a/heapster-saw/examples/mbox_proofs.v
+++ b/heapster-saw/examples/mbox_proofs.v
@@ -26,7 +26,7 @@ Definition unfoldMbox_nil :
   unfoldMbox Mbox_nil = Left _ _ tt :=
   reflexivity _.
 Definition unfoldMbox_cons strt len m d :
-  unfoldMbox (Mbox_cons strt len m d) = Right _ _ (strt, (len, (m, (d, tt)))) :=
+  unfoldMbox (Mbox_cons strt len m d) = Right _ _ (strt, (len, (m, d))) :=
   reflexivity _.
 
 Ltac Mbox_destruct m m' := destruct m as [| ?strt ?len m' ?d].
@@ -40,7 +40,7 @@ Lemma refinesM_either_unfoldMbox_nil_l {C} f g (P : CompM C) :
 Proof. eauto. Qed.
 
 Lemma refinesM_either_unfoldMbox_cons_l {C} strt len m d f g (P : CompM C) :
-  g (strt, (len, (m, (d, tt)))) |= P ->
+  g (strt, (len, (m, d))) |= P ->
   SAWCorePrelude.either _ _ _ f g (unfoldMbox (Mbox_cons strt len m d)) |= P.
 Proof. eauto. Qed.
 
@@ -196,9 +196,9 @@ Proof.
   (* Show Ltac Profile. Reset Ltac Profile. *)
 Time Qed.
 
-Definition mbox_detach_spec : Mbox -> Mbox * (Mbox * unit) :=
-  Mbox__rec _ (Mbox_nil, (Mbox_nil, tt))
-            (fun strt len next _ d => (next, (Mbox_cons strt len Mbox_nil d, tt))).
+Definition mbox_detach_spec : Mbox -> Mbox * Mbox :=
+  Mbox__rec _ (Mbox_nil, Mbox_nil)
+            (fun strt len next _ d => (next, (Mbox_cons strt len Mbox_nil d))).
 
 Lemma mbox_detach_spec_ref
   : refinesFun mbox_detach (fun x => returnM (mbox_detach_spec x)).
@@ -234,11 +234,11 @@ Definition mbox_len_spec : Mbox -> bitvector 64 :=
           (fun strt len m rec d => bvAdd 64 rec len).
 
 Lemma mbox_len_spec_ref
-  : refinesFun mbox_len (fun m => returnM (m, (mbox_len_spec m, tt))).
+  : refinesFun mbox_len (fun m => returnM (m, mbox_len_spec m)).
 Proof.
   unfold mbox_len, mbox_len__tuple_fun.
   prove_refinement_match_letRecM_l.
-  - exact (fun m1 rec m2 => returnM (transMbox m1 m2, (bvAdd 64 rec (mbox_len_spec m2), tt))).
+  - exact (fun m1 rec m2 => returnM (transMbox m1 m2, bvAdd 64 rec (mbox_len_spec m2))).
   unfold mbox_len_spec.
   (* Set Ltac Profiling. *)
   time "mbox_len_spec_ref" prove_refinement.
@@ -246,7 +246,7 @@ Proof.
   (* Most of the remaining cases are taken care of with just bvAdd_id_l and bvAdd_id_r *)
   all: try rewrite bvAdd_id_r; try rewrite bvAdd_id_l; try reflexivity.
   (* The remaining case just needs a few more rewrites *)
-  - do 2 f_equal.
+  - f_equal.
     rewrite bvAdd_assoc; f_equal.
     rewrite bvAdd_comm; reflexivity.
   - cbn; rewrite transMbox_Mbox_nil_r; reflexivity.
@@ -300,17 +300,17 @@ Definition conjSliceBVVec (strt len : bitvector 64) pf0 pf1 d0 d1 : BVVec 64 bv6
 (* Given a `start`, `len`, and `dat` of a single Mbox, return an mbox chain consisting of
    a single mbox with `id` 0,  the given `start` and `len`, and the given `dat` with the
    range 0 to `start` zeroed out. *)
-Definition mbox_copy_spec_cons strt len m d : CompM (Mbox * (Mbox * unit)) :=
+Definition mbox_copy_spec_cons strt len m d : CompM (Mbox * Mbox) :=
   assumingM (isBvslt 64 (intToBv 64 0) strt)
     (forallM (fun pf0 : isBvule 64 strt (intToBv 64 128) =>
       (forallM (fun pf1 : isBvule 64 len (bvSub 64 (intToBv 64 128) strt) =>
         returnM (Mbox_cons strt len m
                            (conjSliceBVVec strt len pf0 pf1 d d),
                 (Mbox_cons strt len Mbox_nil
-                           (conjSliceBVVec strt len pf0 pf1 empty_mbox_d d), tt)))))).
+                           (conjSliceBVVec strt len pf0 pf1 empty_mbox_d d))))))).
 
-Definition mbox_copy_spec : Mbox -> CompM (Mbox * (Mbox * unit)) :=
-  Mbox__rec (fun _ => CompM  (Mbox * (Mbox * unit))) (returnM (Mbox_nil, (Mbox_nil, tt)))
+Definition mbox_copy_spec : Mbox -> CompM (Mbox * Mbox) :=
+  Mbox__rec (fun _ => CompM  (Mbox * Mbox)) (returnM (Mbox_nil, Mbox_nil))
           (fun strt len m _ d => mbox_copy_spec_cons strt len m d).
 
 Lemma mbox_copy_spec_ref : refinesFun mbox_copy mbox_copy_spec.
diff --git a/heapster-saw/examples/memcpy.saw b/heapster-saw/examples/memcpy.saw
index e3193846bc..c5620066f8 100644
--- a/heapster-saw/examples/memcpy.saw
+++ b/heapster-saw/examples/memcpy.saw
@@ -3,7 +3,7 @@ env <- heapster_init_env_from_file "memcpy.sawcore" "memcpy.bc";
 
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, b:llvmblock 64, len:bv 64).arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), arg2:eq(llvmword(len))  -o  arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))" "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #() * #()) ((),(),())";
+heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, b:llvmblock 64, len:bv 64).arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), arg2:eq(llvmword(len))  -o  arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))" "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
 
 heapster_typecheck_fun env "copy_int" "().arg0:int64<> -o ret:int64<>";
 
diff --git a/heapster-saw/examples/rust_data.saw b/heapster-saw/examples/rust_data.saw
index 198164c2b7..e23b31b6b9 100644
--- a/heapster-saw/examples/rust_data.saw
+++ b/heapster-saw/examples/rust_data.saw
@@ -15,6 +15,9 @@ heapster_define_llvmshape env "u64" 64 "" "fieldsh(int64<>)";
 heapster_define_llvmshape env "u32" 64 "" "fieldsh(32,int32<>)";
 heapster_define_llvmshape env "u8" 64 "" "fieldsh(8,int8<>)";
 
+heapster_define_llvmshape env "usize" 64 "" "fieldsh(int64<>)";
+heapster_define_llvmshape env "char" 64 "" "fieldsh(32,int32<>)";
+
 // bool type
 heapster_define_llvmshape env "bool" 64 "" "fieldsh(1,int1<>)";
 
@@ -45,31 +48,14 @@ heapster_define_llvmshape env "String" 64 "" "exsh cap:bv 64. ptrsh(arraysh(cap,
 //heapster_define_recursive_perm env "ListPerm" "X:llvmshape 64, Xlen:bv 64, rw:rwmodality, l:lifetime" "llvmptr 64" ["[l]memblock(rw,0,Xlen + 16,List<ListPerm<X,Xlen,rw,l>,X>)"] "\\ (X:sort 0) (_:Vec 64 Bool) -> List X" "\\ (X:sort 0) (_:Vec 64 Bool) -> foldListPermH X" "\\ (X:sort 0) (_:Vec 64 Bool) -> unfoldListPermH X";
 heapster_define_rust_type env "pub enum List<X> { Nil, Cons (X,Box<List<X>>) }";
 
-// Void type; note that Heapster does not (yet?) support empty types, so instead
-// we make this type opaque. Also, note that the ArgumentV1 structure contains
-// referens to Void, so presumably they are just casts of other types...?
+// The Rust Void type is really a general existential type; this is not directly
+// representable in the Rust type system, but it is in Heapster!
+//heapster_define_llvmshape env "Void" 64 "" "exsh T:llvmshape 64.T";
 //
-//heapster_define_rust_type env "pub enum Void {}";
+// Doh! Except the above looks like a dynamically-sized type to Heapster! So we
+// instead just make Void an opaque type
 heapster_define_opaque_llvmshape env "Void" 64 "" "64" "#()";
 
-// fmt::Error type
-heapster_define_rust_type_qual env "fmt" "pub struct Error { }";
-
-// fmt::Result type
-// FIXME: there seems to be some optimization in Rust that lays out fmt::Result as a 1-bit value
-heapster_define_llvmshape env "fmt::Result" 64 "" "fieldsh(1,eq(llvmword(0))) orsh fieldsh(1,eq(llvmword(1)))";
-//heapster_define_rust_type_qual env "fmt" "pub enum Result { Ok (), Err (fmt::Error) }";
-
-// fmt::Formatter type
-heapster_define_opaque_llvmshape env "fmt::Formatter" 64 "" "64" "#()";
-
-// fmt::ArgumentV1 type
-//heapster_define_rust_type_qual env "fmt" "pub struct ArgumentV1<'a> { value: &'a Void, formatter: for <'b> fn(&'b Void, &'b mut fmt::Formatter) -> fmt::Result, }";
-
-// fmt::Arguments type
-//heapster_define_rust_type_qual env "fmt" "pub struct Arguments<'a> { pieces: &'a [&'a str], fmt: Option<&'a [fmt::Argument]>, args: &'a [fmt::ArgumentV1<'a>], }";
-
-
 // List64 type
 heapster_define_rust_type env "pub enum List64 { Nil64, Cons64 (u64,Box<List64>) }";
 
@@ -110,6 +96,43 @@ heapster_define_rust_type env "pub enum List10<X> { List10_Head(X,Box<List10<X>>
 heapster_define_rust_type env "pub enum List20<X> { List20_Head(X,Box<List20<X>>), List20_0(X,Box<List20<X>>), List20_1(X,Box<List20<X>>), List20_2(X,Box<List20<X>>), List20_3(X,Box<List20<X>>), List20_4(X,Box<List20<X>>), List20_5(X,Box<List20<X>>), List20_6(X,Box<List20<X>>), List20_7(X,Box<List20<X>>), List20_8(X,Box<List20<X>>), List20_9(X,Box<List20<X>>), List20_10(X,Box<List20<X>>), List20_11(X,Box<List20<X>>), List20_12(X,Box<List20<X>>), List20_13(X,Box<List20<X>>), List20_14(X,Box<List20<X>>), List20_15(X,Box<List20<X>>), List20_16(X,Box<List20<X>>), List20_17(X,Box<List20<X>>), List20_18(X,Box<List20<X>>), List20_19(X,Box<List20<X>>), }";
 
 
+/***
+ *** Rust Formatting Types
+ ***/
+
+// fmt::Error type
+heapster_define_rust_type_qual env "fmt" "pub struct Error { }";
+
+// fmt::Result type
+// FIXME: there seems to be some optimization in Rust that lays out fmt::Result as a 1-bit value
+heapster_define_llvmshape env "fmt::Result" 64 "" "fieldsh(1,eq(llvmword(0))) orsh fieldsh(1,eq(llvmword(1)))";
+//heapster_define_rust_type_qual env "fmt" "pub enum Result { Ok (), Err (fmt::Error) }";
+
+// fmt::Formatter type
+heapster_define_opaque_llvmshape env "fmt::Formatter" 64 "" "64" "#()";
+
+// fmt::Alignment type
+heapster_define_rust_type_qual env "fmt" "pub enum Alignment { Left, Right, Center, Unknown,}";
+
+// fmt::Count type
+heapster_define_rust_type_qual env "fmt" "pub enum Count { Is(usize), Param(usize), NextParam, Implied,}";
+
+// fmt::FormatSpec
+heapster_define_rust_type_qual env "fmt" "pub struct FormatSpec { pub fill: char, pub align: fmt::Alignment, pub flags: u32, pub precision: fmt::Count, pub width: fmt::Count, }";
+
+// fmt::Position
+heapster_define_rust_type_qual env "fmt" "pub enum Position { Next, At(usize),}";
+
+// fmt::Argument type
+heapster_define_rust_type_qual env "fmt" "pub struct Argument { pub position: fmt::Position, pub format: fmt::FormatSpec,}";
+
+// fmt::ArgumentV1 type
+heapster_define_rust_type_qual env "fmt" "pub struct ArgumentV1<'a> { value: &'a Void, formatter: for <'b> fn(&'b Void, &'b mut fmt::Formatter) -> fmt::Result, }";
+
+// fmt::Arguments type
+//heapster_define_rust_type_qual env "fmt" "pub struct Arguments<'a> { pieces: &'a [&'a str], fmt: Option<&'a [fmt::Argument]>, args: &'a [fmt::ArgumentV1<'a>], }";
+
+
 /***
  *** Assumed Functions
  ***/
@@ -120,7 +143,7 @@ exchange_malloc_sym <- heapster_find_symbol env "15exchange_malloc";
 heapster_assume_fun_rename env exchange_malloc_sym "exchange_malloc" "(len:bv 64).arg0:eq(llvmword(len)),arg1:true -o ret:memblock(W,0,len,emptysh)" "\\ (len:Vec 64 Bool) -> returnM #() ()";
 
 // memcpy
-heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, b:llvmblock 64, len:bv 64).arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), arg2:eq(llvmword(len))  -o  arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))" "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #() * #()) ((),(),())";
+heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, b:llvmblock 64, len:bv 64).arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), arg2:eq(llvmword(len))  -o  arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))" "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
 
 // <str as alloc::string::ToString>::to_string
 to_string_str <- heapster_find_symbol env "$LT$str$u20$as$u20$alloc..string..ToString$GT$9to_string";
diff --git a/heapster-saw/examples/rust_lifetimes.saw b/heapster-saw/examples/rust_lifetimes.saw
index fda06324e0..e30d5cfdbb 100644
--- a/heapster-saw/examples/rust_lifetimes.saw
+++ b/heapster-saw/examples/rust_lifetimes.saw
@@ -19,7 +19,7 @@ heapster_define_llvmshape env "u64" 64 "" "fieldsh(int64<>)";
  ***/
 
 // llvm.uadd.with.overflow.i64
-heapster_assume_fun env "llvm.uadd.with.overflow.i64" "().arg0:int64<>, arg1:int64<> -o ret:struct(int64<>,int1<>)" "\\ (x y:Vec 64 Bool) -> returnM (Vec 64 Bool * Vec 1 Bool * #()) (bvAdd 64 x y, gen 1 Bool (\\ (_:Nat) -> bvCarry 64 x y), ())";
+heapster_assume_fun env "llvm.uadd.with.overflow.i64" "().arg0:int64<>, arg1:int64<> -o ret:struct(int64<>,int1<>)" "\\ (x y:Vec 64 Bool) -> returnM (Vec 64 Bool * Vec 1 Bool) (bvAdd 64 x y, gen 1 Bool (\\ (_:Nat) -> bvCarry 64 x y))";
 
 // llvm.expect.i1
 heapster_assume_fun env "llvm.expect.i1" "().arg0:int1<>, arg1:int1<> -o ret:int1<>" "\\ (x y:Vec 1 Bool) -> returnM (Vec 1 Bool) x";
diff --git a/heapster-saw/examples/string_set.sawcore b/heapster-saw/examples/string_set.sawcore
index eab0aa9e3a..ebb12ebe76 100644
--- a/heapster-saw/examples/string_set.sawcore
+++ b/heapster-saw/examples/string_set.sawcore
@@ -8,17 +8,17 @@ listInsertM a l s =
   returnM (List a) (Cons a s l);
 
 listRemoveM : (a : sort 0) -> (a -> a -> Bool) -> List a -> a ->
-              CompM (List a * a * #());
+              CompM (List a * a);
 listRemoveM a test_eq l s =
   returnM
-    (List a * a * #())
+    (List a * a)
     (List__rec
       a (\ (_:List a) -> List a)
       (Nil a)
       (\ (s':a) (_:List a) (rec:List a) ->
          ite (List a) (test_eq s s') rec (Cons a s' rec))
       l,
-     s, ());
+     s);
 
 ----------------------------------------------------------------------
 -- Helper defs for Heapster examples
@@ -30,14 +30,14 @@ stringListInsertM : List String -> String -> CompM (List String);
 stringListInsertM l s =
   returnM (List String) (Cons String s l);
 
-stringListRemoveM : List String -> String -> CompM (stringList * String * #());
+stringListRemoveM : List String -> String -> CompM (stringList * String);
 stringListRemoveM l s =
   returnM
-    (stringList * String * #())
+    (stringList * String)
     (List__rec
       String (\ (_:List String) -> List String)
       (Nil String)
       (\ (s':String) (_:List String) (rec:List String) ->
          ite (List String) (equalString s s') rec (Cons String s' rec))
       l,
-     s, ());
+     s);
diff --git a/heapster-saw/examples/xor_swap_proofs.v b/heapster-saw/examples/xor_swap_proofs.v
index f1eaeb38d9..2114d9ed90 100644
--- a/heapster-saw/examples/xor_swap_proofs.v
+++ b/heapster-saw/examples/xor_swap_proofs.v
@@ -13,8 +13,8 @@ Import xor_swap.
 
 
 Definition xor_swap_spec x1 x2 :
-  CompM (bitvector 64 * (bitvector 64 * unit)) :=
-  returnM (x2, (x1, tt)).
+  CompM (bitvector 64 * bitvector 64) :=
+  returnM (x2, x1).
 Arguments xor_swap_spec /.
 
 Lemma no_errors_xor_swap : refinesFun xor_swap (fun _ _ => noErrorsSpec).
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
index 6fff2e599e..9602a78805 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
@@ -32,7 +32,6 @@ module Verifier.SAW.Heapster.IRTTranslation (
   ) where
 
 import Numeric.Natural
-import Data.Foldable
 import Data.Functor.Const
 import GHC.TypeLits
 import Control.Monad.Reader
@@ -540,11 +539,10 @@ irtCtorOpenTerm c all_args =
 
 -- | Like 'tupleOfTypes' but with @IRT_prod@
 irtProd :: [OpenTerm] -> IRTDescTransM ctx OpenTerm
+irtProd [] = irtCtorOpenTerm "Prelude.IRT_unit" []
 irtProd [x] = return x
-irtProd xs =
-  do irtUnit <- irtCtorOpenTerm "Prelude.IRT_unit" []
-     foldrM (\x xs' -> irtCtorOpenTerm "Prelude.IRT_prod" [x, xs'])
-            irtUnit xs
+irtProd (x:xs) =
+  irtProd xs >>= \xs' -> irtCtorOpenTerm "Prelude.IRT_prod" [x, xs']
 
 -- | A singleton list containing the result of 'irtCtorOpenTerm'
 irtCtor :: Ident -> [OpenTerm] -> IRTDescTransM ctx [OpenTerm]
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 2a430f012a..2ac3bd4d30 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -647,7 +647,7 @@ data SimplImpl ps_in ps_out where
   -- > -o x:array(off,<len,*stride,fps,permute(bs))
   SImpl_LLVMArrayRearrange ::
     (1 <= w, KnownNat w) =>
-    ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> LLVMArrayPerm w ->
+    ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> [LLVMArrayBorrow w] ->
     SimplImpl (RNil :> LLVMPointerType w) (RNil :> LLVMPointerType w)
 
   -- | Convert an array to a field of the same size with @true@ contents:
@@ -723,17 +723,18 @@ data SimplImpl ps_in ps_out where
     SimplImpl (RNil :> LLVMPointerType w :> LLVMPointerType w)
     (RNil :> LLVMPointerType w)
 
-  -- | Apply an implication to the @i@th field of an array permission:
+  -- | Apply an implication to the fields of an array permission:
   --
-  -- > y:fpi -o y:fpi'
+  -- > y:fp1 * ... * fpn -o y:fp1' * ... * fpn'
   -- > ------------------------------------------------
   -- > x:array(off,<len,*stride,(fp1, ..., fpn),bs) -o
-  -- >   x:array(off,<len,*stride,
-  -- >           (fp1, ..., fp(i-1), fpi', fp(i+1), ..., fpn),bs)
+  -- >   x:array(off,<len,*stride,(fp1',...,fpn'),bs)
   SImpl_LLVMArrayContents ::
     (1 <= w, KnownNat w) =>
-    ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> Int -> LLVMArrayField w ->
-    LocalPermImpl (RNil :> LLVMPointerType w) (RNil :> LLVMPointerType w) ->
+    ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> [LLVMArrayField w] ->
+    Binding (LLVMPointerType w) (LocalPermImpl
+                                 (RNil :> LLVMPointerType w)
+                                 (RNil :> LLVMPointerType w)) ->
     SimplImpl (RNil :> LLVMPointerType w) (RNil :> LLVMPointerType w)
 
   -- | Prove that @x@ is a pointer from a field permission:
@@ -1644,16 +1645,11 @@ simplImplIn (SImpl_LLVMArrayAppend x ap1 ap2) =
         x (ValPerm_Conj1 $ Perm_LLVMArray ap2)
     _ -> error "simplImplIn: SImpl_LLVMArrayAppend: arrays cannot be appended"
 
-simplImplIn (SImpl_LLVMArrayRearrange x ap1 ap2) =
-  if bvEq (llvmArrayOffset ap1) (llvmArrayOffset ap2) &&
-     bvEq (llvmArrayLen ap1) (llvmArrayLen ap2) &&
-     llvmArrayStride ap1 == llvmArrayStride ap2 &&
-     llvmArrayFields ap1 == llvmArrayFields ap2 &&
-     all (flip elem (llvmArrayBorrows ap2)) (llvmArrayBorrows ap1) &&
-     all (flip elem (llvmArrayBorrows ap1)) (llvmArrayBorrows ap2) then
-    distPerms1 x (ValPerm_Conj1 $ Perm_LLVMArray ap1)
+simplImplIn (SImpl_LLVMArrayRearrange x ap bs) =
+  if llvmArrayBorrowsPermuteTo ap bs then
+    distPerms1 x (ValPerm_Conj1 $ Perm_LLVMArray ap)
   else
-    error "simplImplIn: SImpl_LLVMArrayRearrange: arrays not equivalent"
+    error "simplImplIn: SImpl_LLVMArrayRearrange: malformed output borrows list"
 
 simplImplIn (SImpl_LLVMArrayToField x ap _) =
   distPerms1 x (ValPerm_Conj1 $ Perm_LLVMArray ap)
@@ -1694,7 +1690,7 @@ simplImplIn (SImpl_LLVMArrayIndexReturn x ap ix) =
   else
     error "simplImplIn: SImpl_LLVMArrayIndexReturn: index not being borrowed"
 
-simplImplIn (SImpl_LLVMArrayContents x ap _ _ _) =
+simplImplIn (SImpl_LLVMArrayContents x ap _ _) =
   distPerms1 x (ValPerm_Conj [Perm_LLVMArray ap])
 simplImplIn (SImpl_LLVMFieldIsPtr x fp) =
   distPerms1 x (ValPerm_Conj [Perm_LLVMField fp])
@@ -1961,16 +1957,11 @@ simplImplOut (SImpl_LLVMArrayAppend x ap1 ap2) =
         llvmArrayAddArrayBorrows ap1' ap2
     _ -> error "simplImplOut: SImpl_LLVMArrayAppend: arrays cannot be appended"
 
-simplImplOut (SImpl_LLVMArrayRearrange x ap1 ap2) =
-  if bvEq (llvmArrayOffset ap1) (llvmArrayOffset ap2) &&
-     bvEq (llvmArrayLen ap1) (llvmArrayLen ap2) &&
-     llvmArrayStride ap1 == llvmArrayStride ap2 &&
-     llvmArrayFields ap1 == llvmArrayFields ap2 &&
-     all (flip elem (llvmArrayBorrows ap2)) (llvmArrayBorrows ap1) &&
-     all (flip elem (llvmArrayBorrows ap1)) (llvmArrayBorrows ap2) then
-    distPerms1 x (ValPerm_Conj1 $ Perm_LLVMArray ap2)
+simplImplOut (SImpl_LLVMArrayRearrange x ap bs) =
+  if llvmArrayBorrowsPermuteTo ap bs then
+    distPerms1 x (ValPerm_Conj1 $ Perm_LLVMArray $ ap { llvmArrayBorrows = bs })
   else
-    error "simplImplOut: SImpl_LLVMArrayRearrange: arrays not equivalent"
+    error "simplImplOut: SImpl_LLVMArrayRearrange: malformed output borrows list"
 
 simplImplOut (SImpl_LLVMArrayToField x ap sz) =
   case llvmArrayToField sz ap of
@@ -2016,11 +2007,8 @@ simplImplOut (SImpl_LLVMArrayIndexReturn x ap ix) =
   else
     error "simplImplOut: SImpl_LLVMArrayIndexReturn: index not being borrowed"
 
-simplImplOut (SImpl_LLVMArrayContents x ap i fp _) =
-  distPerms1 x (ValPerm_Conj [Perm_LLVMArray $
-                              ap { llvmArrayFields =
-                                     take i (llvmArrayFields ap) ++
-                                     fp : drop (i+1) (llvmArrayFields ap)}])
+simplImplOut (SImpl_LLVMArrayContents x ap flds _) =
+  distPerms1 x (ValPerm_Conj [Perm_LLVMArray $ ap { llvmArrayFields = flds }])
 
 simplImplOut (SImpl_LLVMFieldIsPtr x fp) =
   distPerms2 x (ValPerm_Conj1 Perm_IsLLVMPtr)
@@ -2421,8 +2409,8 @@ instance SubstVar PermVarSubst m =>
       SImpl_LLVMArrayReturn <$> genSubst s x <*> genSubst s ap <*> genSubst s rng
     [nuMP| SImpl_LLVMArrayAppend x ap1 ap2 |] ->
       SImpl_LLVMArrayAppend <$> genSubst s x <*> genSubst s ap1 <*> genSubst s ap2
-    [nuMP| SImpl_LLVMArrayRearrange x ap1 ap2 |] ->
-      SImpl_LLVMArrayRearrange <$> genSubst s x <*> genSubst s ap1 <*> genSubst s ap2
+    [nuMP| SImpl_LLVMArrayRearrange x ap bs |] ->
+      SImpl_LLVMArrayRearrange <$> genSubst s x <*> genSubst s ap <*> genSubst s bs
     [nuMP| SImpl_LLVMArrayToField x ap sz |] ->
       SImpl_LLVMArrayToField <$> genSubst s x <*> genSubst s ap
                              <*> return (mbLift sz)
@@ -2438,10 +2426,9 @@ instance SubstVar PermVarSubst m =>
     [nuMP| SImpl_LLVMArrayIndexReturn x ap ix |] ->
       SImpl_LLVMArrayIndexReturn <$> genSubst s x <*> genSubst s ap <*>
                                      genSubst s ix
-    [nuMP| SImpl_LLVMArrayContents x ap i fp impl |] ->
+    [nuMP| SImpl_LLVMArrayContents x ap flds mb_mb_impl |] ->
       SImpl_LLVMArrayContents <$> genSubst s x <*> genSubst s ap <*>
-                                  return (mbLift i) <*> genSubst s fp <*>
-                                  genSubst s impl
+                                  genSubst s flds <*> genSubst s mb_mb_impl
     [nuMP| SImpl_LLVMFieldIsPtr x fp |] ->
       SImpl_LLVMFieldIsPtr <$> genSubst s x <*> genSubst s fp
     [nuMP| SImpl_LLVMArrayIsPtr x ap |] ->
@@ -2637,9 +2624,6 @@ instance SubstVar s m => Substable1 s (LocalImplRet ps) m where
 -- FIXME: instead of having a separate PPInfo and name type map, we should maybe
 -- combine all the local context into one type...?
 
-data RecurseFlag = RecLeft | RecRight | RecNone
-  deriving (Eq, Show, Read)
-
 data ImplState vars ps =
   ImplState { _implStatePerms :: PermSet ps,
               _implStateVars :: CruCtx vars,
@@ -2747,7 +2731,7 @@ embedImplM ps_in m =
 -- | Embed a sub-computation in a name-binding inside another 'ImplM'
 -- computation, throwing away any state from that sub-computation and returning
 -- a 'PermImpl' inside a name-binding
-embedMbImplM :: Mb ctx (PermSet ps_in) ->
+embedMbImplM :: Mb ctx (DistPerms ps_in) ->
                 Mb ctx (ImplM RNil s r' ps_out ps_in (r' ps_out)) ->
                 ImplM vars s r ps ps (Mb ctx (PermImpl r' ps_in))
 embedMbImplM mb_ps_in mb_m =
@@ -2755,7 +2739,7 @@ embedMbImplM mb_ps_in mb_m =
      lift $ strongMbM $ mbMap2
        (\ps_in m ->
         runImplM
-         CruCtxNil ps_in
+         CruCtxNil (distPermSet ps_in)
          (view implStatePermEnv    s) (view implStatePPInfo  s)
          (view implStateFailPrefix s) (view implStateDebugLevel s)
          (view implStateNameTypes  s) m (pure . fst))
@@ -3983,13 +3967,14 @@ implLLVMArrayAppend x ap1 ap2 =
   implSimplM Proxy (SImpl_LLVMArrayAppend x ap1 ap2)
 
 
--- | Rearrange the order of the borrows in an array permission
+-- | Rearrange the order of the borrows in the input array permission to match
+-- the given list, assuming the two have the same elements
 implLLVMArrayRearrange ::
   (1 <= w, KnownNat w, NuMatchingAny1 r) =>
-  ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> LLVMArrayPerm w ->
+  ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> [LLVMArrayBorrow w] ->
   ImplM vars s r (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) ()
-implLLVMArrayRearrange x ap_in ap_out =
-  implSimplM Proxy (SImpl_LLVMArrayRearrange x ap_in ap_out)
+implLLVMArrayRearrange x ap bs =
+  implSimplM Proxy (SImpl_LLVMArrayRearrange x ap bs)
 
 -- | Prove an empty array with length 0
 implLLVMArrayEmpty ::
@@ -5147,8 +5132,7 @@ proveVarLLVMArrayH x first_p ps ap =
                  | precise <- bvEq off (llvmArrayOffset ap_lhs)
                  , (first_p || precise)
                  , Just cell_num <- llvmArrayIsOffsetArray ap_lhs ap
-                 , bvCouldBeInRange cell_num (llvmArrayCells ap_lhs)
-                 , llvmArrayFields ap_lhs == llvmArrayFields ap ->
+                 , bvCouldBeInRange cell_num (llvmArrayCells ap_lhs) ->
                    Just (precise, proveVarLLVMArray_ArrayStep x ps ap i ap_lhs)
                _ -> Nothing)
    ps [0..])
@@ -5160,6 +5144,24 @@ proveVarLLVMArray_ArrayStep ::
   [AtomicPerm (LLVMPointerType w)] -> LLVMArrayPerm w ->
   Int -> LLVMArrayPerm w ->
   ImplM vars s r (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) ()
+proveVarLLVMArray_ArrayStep x ps ap i ap_lhs =
+  implTraceM (\info ->
+               pretty "proveVarLLVMArray_ArrayStep:" <+>
+               permPretty info x <> colon <>
+               align (sep [PP.group (permPretty info (ValPerm_Conj ps)),
+                           parens (permPretty info (ValPerm_LLVMArray ap)),
+                           pretty "-o",
+                           PP.group (permPretty info (ValPerm_Conj1 $
+                                                      Perm_LLVMArray ap))])) >>>
+  proveVarLLVMArray_ArrayStepH x ps ap i ap_lhs
+
+
+-- | The main workhorse of 'proveVarLLVMArray_ArrayStep'
+proveVarLLVMArray_ArrayStepH ::
+  (1 <= w, KnownNat w, NuMatchingAny1 r) => ExprVar (LLVMPointerType w) ->
+  [AtomicPerm (LLVMPointerType w)] -> LLVMArrayPerm w ->
+  Int -> LLVMArrayPerm w ->
+  ImplM vars s r (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) ()
 
 -- If there is a borrow in ap_lhs that is not in ap but might overlap with ap,
 -- return it to ap_lhs
@@ -5167,7 +5169,7 @@ proveVarLLVMArray_ArrayStep ::
 -- FIXME: when an array ap_ret is being borrowed from ap_lhs, this code requires
 -- all of it to be returned, with no borrows, even though it could be that ap
 -- allows some of ap_ret to be borrowed
-proveVarLLVMArray_ArrayStep x ps ap i ap_lhs
+proveVarLLVMArray_ArrayStepH x ps ap i ap_lhs
   | Just ap_cell_off <- llvmArrayIsOffsetArray ap_lhs ap
   , Just b <-
     find (\b ->
@@ -5193,7 +5195,7 @@ proveVarLLVMArray_ArrayStep x ps ap i ap_lhs
 -- If there is a borrow in ap that is not in ap_lhs, borrow it from ap_lhs. Note
 -- the assymmetry with the previous case: we only add borrows if we definitely
 -- have to, but we remove borrows if we might have to.
-proveVarLLVMArray_ArrayStep x ps ap i ap_lhs
+proveVarLLVMArray_ArrayStepH x ps ap i ap_lhs
   | Just ap_lhs_cell_off <- llvmArrayIsOffsetArray ap ap_lhs
   , Just b <-
     find (\b ->
@@ -5212,21 +5214,41 @@ proveVarLLVMArray_ArrayStep x ps ap i ap_lhs
     -- added to the front of the list of borrows, so we need to rearrange.
     implLLVMArrayBorrowBorrow x ap' b >>>= \p ->
     recombinePerm x p >>>
-    implLLVMArrayRearrange x (llvmArrayAddBorrow b ap') ap
+    implLLVMArrayRearrange x (llvmArrayAddBorrow b ap') (llvmArrayBorrows ap)
 
 -- If ap and ap_lhs are equal up to the order of their borrows, just rearrange
--- the borrows and we should be good
-proveVarLLVMArray_ArrayStep x ps ap i ap_lhs
+-- the borrows and we should be done
+proveVarLLVMArray_ArrayStepH x ps ap i ap_lhs
   | bvEq (llvmArrayOffset ap_lhs) (llvmArrayOffset ap)
   , bvEq (llvmArrayLen ap_lhs) (llvmArrayLen ap)
   , llvmArrayStride ap_lhs == llvmArrayStride ap
-  , llvmArrayFields ap_lhs == llvmArrayFields ap =
+  , llvmArrayFields ap_lhs == llvmArrayFields ap
+  , llvmArrayBorrowsPermuteTo ap_lhs (llvmArrayBorrows ap) =
     implGetPopConjM x ps i >>>
-    implLLVMArrayRearrange x ap_lhs ap
+    implLLVMArrayRearrange x ap_lhs (llvmArrayBorrows ap)
+
+-- If ap and ap_lhs have the same range and stride but their fields are
+-- different, prove the rhs fields from the lhs fields
+proveVarLLVMArray_ArrayStepH x ps ap i ap_lhs
+  | bvEq (llvmArrayOffset ap_lhs) (llvmArrayOffset ap)
+  , bvEq (llvmArrayLen ap_lhs) (llvmArrayLen ap)
+  , llvmArrayStride ap_lhs == llvmArrayStride ap
+  , flds <- llvmArrayFields ap
+  , flds_lhs <- llvmArrayFields ap_lhs
+  , ap' <- ap { llvmArrayFields = flds_lhs }
+  , dps_in <-
+      nu $ \y -> distPerms1 y $ ValPerm_Conj $
+                 map llvmArrayFieldToAtomicPerm flds_lhs
+  , dps_out <-
+      nu $ \y -> distPerms1 y $ ValPerm_Conj $
+                 map llvmArrayFieldToAtomicPerm flds =
+    proveVarLLVMArray_ArrayStep x ps ap' i ap_lhs >>>
+    localMbProveVars dps_in dps_out >>>= \mb_impl ->
+    implSimplM Proxy (SImpl_LLVMArrayContents x ap' flds mb_impl)
 
 -- If ap is contained inside ap_lhs at a cell boundary then copy or borrow ap
 -- from ap_lhs depending on whether they are copyable
-proveVarLLVMArray_ArrayStep x ps ap i ap_lhs
+proveVarLLVMArray_ArrayStepH x ps ap i ap_lhs
   | all bvPropCouldHold (bvPropRangeSubset
                          (llvmArrayAbsOffsets ap) (llvmArrayAbsOffsets ap_lhs))
   , llvmArrayStride ap_lhs == llvmArrayStride ap
@@ -5246,7 +5268,7 @@ proveVarLLVMArray_ArrayStep x ps ap i ap_lhs
 -- If we get to this case but ap is still at a cell boundary in ap_lhs then
 -- ap_lhs only satisfies some initial portion of ap, so borrow or copy that part
 -- of ap_lhs and continue proving the rest of ap
-proveVarLLVMArray_ArrayStep x ps ap i ap_lhs
+proveVarLLVMArray_ArrayStepH x ps ap i ap_lhs
   | llvmArrayStride ap_lhs == llvmArrayStride ap
   , llvmArrayFields ap_lhs == llvmArrayFields ap
   , Just (LLVMArrayIndex ap_cell_num 0) <-
@@ -5281,7 +5303,7 @@ proveVarLLVMArray_ArrayStep x ps ap i ap_lhs
 
 
 -- Otherwise we don't know what to do so we fail
-proveVarLLVMArray_ArrayStep _x _ps _ap _i _ap_lhs =
+proveVarLLVMArray_ArrayStepH _x _ps _ap _i _ap_lhs =
   implFailMsgM "proveVarLLVMArray_ArrayStep"
 
 
@@ -7033,6 +7055,23 @@ localProveVars ps_in ps_out =
                     proveVarsImplInt (emptyMb ps_out) >>>
                     pure (LocalImplRet Refl))
 
+-- | Prove one sequence of permissions over an extended set of local variables
+-- from another and capture the proof as a 'LocalPermImpl' in a binding
+localMbProveVars :: NuMatchingAny1 r =>
+                    Mb (ctx :: RList CrucibleType) (DistPerms ps_in) ->
+                    Mb ctx (DistPerms ps_out) ->
+                    ImplM vars s r ps ps (Mb ctx (LocalPermImpl ps_in ps_out))
+localMbProveVars mb_ps_in mb_ps_out =
+  implTraceM (\i -> sep [pretty "localMbProveVars:", permPretty i mb_ps_in,
+                         pretty "-o", permPretty i mb_ps_out]) >>>
+  fmap LocalPermImpl <$>
+  embedMbImplM mb_ps_in (mbMap2
+                         (\ps_in ps_out ->
+                           recombinePermsRev ps_in >>>
+                           proveVarsImplInt (emptyMb ps_out) >>>
+                           pure (LocalImplRet Refl))
+                         mb_ps_in mb_ps_out)
+
 
 ----------------------------------------------------------------------
 -- * External Entrypoints to the Implication Prover
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index ce43c842a3..32717d5f28 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -86,7 +86,7 @@ import Debug.Trace
 
 
 ----------------------------------------------------------------------
--- * Utility Functions
+-- * Utility Functions and Definitions
 ----------------------------------------------------------------------
 
 -- | Delete the nth element of a list
@@ -132,6 +132,11 @@ foldr1WithDefault f def (a:as) = f a $ foldr1WithDefault f def as
 foldMapWithDefault :: (b -> b -> b) -> b -> (a -> b) -> [a] -> b
 foldMapWithDefault comb def f l = foldr1WithDefault comb def $ map f l
 
+-- | A flag indicating whether an equality test has unfolded a
+-- recursively-defined name on one side of the equation already
+data RecurseFlag = RecLeft | RecRight | RecNone
+  deriving (Eq, Show, Read)
+
 
 ----------------------------------------------------------------------
 -- * Pretty-printing
@@ -3275,6 +3280,10 @@ llvmBlockEndOffset :: (1 <= w, KnownNat w) => LLVMBlockPerm w ->
                       PermExpr (BVType w)
 llvmBlockEndOffset = bvRangeEnd . llvmBlockRange
 
+-- | Return the length in bytes of an 'LLVMFieldShape'
+llvmFieldShapeLength :: LLVMFieldShape w -> Integer
+llvmFieldShapeLength (LLVMFieldShape p) = exprLLVMTypeBytes p
+
 -- | Return the expression for the length of a shape if there is one
 llvmShapeLength :: (1 <= w, KnownNat w) => PermExpr (LLVMShapeType w) ->
                    Maybe (PermExpr (BVType w))
@@ -3295,8 +3304,8 @@ llvmShapeLength (PExpr_EqShape _) = Nothing
 llvmShapeLength (PExpr_PtrShape _ _ sh)
   | LLVMShapeRepr w <- exprType sh = Just $ bvInt (intValue w `div` 8)
   | otherwise = Nothing
-llvmShapeLength (PExpr_FieldShape (LLVMFieldShape p)) =
-  Just $ exprLLVMTypeBytesExpr p
+llvmShapeLength (PExpr_FieldShape fsh) =
+  Just $ bvInt $ llvmFieldShapeLength fsh
 llvmShapeLength (PExpr_ArrayShape len _ _) = Just len
 llvmShapeLength (PExpr_SeqShape sh1 sh2) =
   liftA2 bvAdd (llvmShapeLength sh1) (llvmShapeLength sh2)
@@ -3402,6 +3411,15 @@ llvmReadBlockOfShape sh
 llvmReadBlockOfShape _ =
   error "llvmReadBlockOfShape: shape without known length"
 
+-- | Test if an LLVM shape is a sequence of field shapes, and if so, return that
+-- sequence
+matchLLVMFieldShapeSeq :: (1 <= w, KnownNat w) => PermExpr (LLVMShapeType w) ->
+                          Maybe [LLVMFieldShape w]
+matchLLVMFieldShapeSeq (PExpr_FieldShape fsh) = Just [fsh]
+matchLLVMFieldShapeSeq (PExpr_SeqShape sh1 sh2) =
+  (++) <$> matchLLVMFieldShapeSeq sh1 <*> matchLLVMFieldShapeSeq sh2
+matchLLVMFieldShapeSeq _ = Nothing
+
 -- | Add the given read/write and lifetime modalities to all top-level pointer
 -- shapes in a shape. Top-level here means we do not recurse inside pointer
 -- shapes, as pointer shape modalities also apply recursively to the contained
@@ -3753,6 +3771,13 @@ llvmArrayRemArrayBorrows ap sub_ap
     ap
 llvmArrayRemArrayBorrows _ _ = error "llvmArrayRemArrayBorrows"
 
+-- | Test if the borrows of an array can be permuted to another order
+llvmArrayBorrowsPermuteTo :: (1 <= w, KnownNat w) => LLVMArrayPerm w ->
+                             [LLVMArrayBorrow w] -> Bool
+llvmArrayBorrowsPermuteTo ap bs =
+  all (flip elem (llvmArrayBorrows ap)) bs &&
+  all (flip elem bs) (llvmArrayBorrows ap)
+
 -- | Add a cell offset to an 'LLVMArrayBorrow', meaning we change the borrow to
 -- be relative to an array with that many more cells added to the front
 cellOffsetLLVMArrayBorrow :: (1 <= w, KnownNat w) => PermExpr (BVType w) ->
@@ -6497,6 +6522,15 @@ lookupNamedPerm env = helper (permEnvNamedPerms env) where
     = Just rp
   helper (_:rps) rpn = helper rps rpn
 
+-- | Look up the 'NamedPerm' for a 'NamedPermName' in a 'PermEnv' or raise an
+-- error if it does not exist
+requireNamedPerm :: PermEnv -> NamedPermName ns args a -> NamedPerm ns args a
+requireNamedPerm env npn
+  | Just np <- lookupNamedPerm env npn = np
+requireNamedPerm _ npn =
+  error ("requireNamedPerm: named perm does not exist: "
+         ++ namedPermNameName npn)
+
 -- | Look up an LLVM shape by name in a 'PermEnv' and cast it to a given width
 lookupNamedShape :: PermEnv -> String -> Maybe SomeNamedShape
 lookupNamedShape env nm =
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs
index 267d4094bd..05910c3aae 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs
@@ -54,6 +54,7 @@ import qualified Data.Binding.Hobbits.NameSet as NameSet
 
 import Language.Rust.Syntax
 import Language.Rust.Parser
+import qualified Language.Rust.Pretty as RustPP
 import Language.Rust.Data.Ident (Ident(..), name)
 
 import Prettyprinter as PP
@@ -125,6 +126,12 @@ lookupName :: String -> TypeRepr a -> RustConvM (Name a)
 lookupName str tp =
   lookupTypedName str >>= \n -> castTypedM "variable" tp n
 
+-- | Build a 'PPInfo' structure for the names currently in scope
+rsPPInfo :: RustConvM PPInfo
+rsPPInfo =
+  foldr (\(str, Some (Typed _ n)) -> ppInfoAddExprName str n) emptyPPInfo <$>
+  rciCtx <$> ask
+
 -- | The conversion of a context of Rust type and lifetime variables
 type RustCtx = RAssign (Product (Constant String) TypeRepr)
 
@@ -372,13 +379,17 @@ instance RsConvert w [PathParameters Span] (Some TypedPermExprs) where
 instance RsConvert w (Ty Span) (PermExpr (LLVMShapeType w)) where
   rsConvert w (Slice tp _) =
     do sh <- rsConvert w tp
-       case sh of
-         PExpr_FieldShape fsh@(LLVMFieldShape p) ->
+       case matchLLVMFieldShapeSeq sh of
+         Just fshs ->
            return (PExpr_ExShape $ nu $ \n ->
                     PExpr_ArrayShape (PExpr_Var n)
-                    (fromIntegral $ exprLLVMTypeBytes p)
-                    [fsh])
-         _ -> fail "rsConvert: slices of compound types not yet supported"
+                    (fromIntegral $ sum $ map llvmFieldShapeLength fshs)
+                    fshs)
+         _ ->
+           rsPPInfo >>= \ppInfo ->
+           fail ("rsConvert: slices not yet supported of type: "
+                 ++ show (RustPP.pretty tp) ++ " with translation:\n"
+                 ++ renderDoc (permPretty ppInfo sh))
   rsConvert _ (Rptr Nothing _ _ _) =
     fail "rsConvert: lifetimes must be supplied for reference types"
   rsConvert w (Rptr (Just rust_l) mut tp' _) =
@@ -715,16 +726,17 @@ un3SomeFunPerm args ret (Some3FunPerm fun_perm)
   , Just Refl <- testEquality ret (funPermRet fun_perm) =
     return $ SomeFunPerm fun_perm
 un3SomeFunPerm args ret (Some3FunPerm fun_perm) =
+  rsPPInfo >>= \ppInfo ->
   fail $ renderDoc $ vsep
   [ pretty "Unexpected LLVM type for function permission:"
-  , permPretty emptyPPInfo fun_perm
+  , permPretty ppInfo fun_perm
   , pretty "Actual LLVM type of function:"
-    <+> PP.group (permPretty emptyPPInfo args) <+> pretty "=>"
-    <+> PP.group (permPretty emptyPPInfo ret)
+    <+> PP.group (permPretty ppInfo args) <+> pretty "=>"
+    <+> PP.group (permPretty ppInfo ret)
   , pretty "Expected LLVM type of function:"
-    <+> PP.group (permPretty emptyPPInfo (funPermArgs fun_perm))
+    <+> PP.group (permPretty ppInfo (funPermArgs fun_perm))
     <+> pretty "=>"
-    <+> PP.group (permPretty emptyPPInfo (funPermRet fun_perm)) ]
+    <+> PP.group (permPretty ppInfo (funPermRet fun_perm)) ]
 
 -- | This is the more general form of 'funPerm3FromArgLayout, where there can be
 -- ghost variables in the 'ArgLayout'
@@ -919,9 +931,10 @@ layoutArgShapeByVal Rust (PExpr_PtrShape maybe_rw maybe_l sh)
 
 -- If we don't know the length of our pointer, we can't lay it out at all
 layoutArgShapeByVal Rust (PExpr_PtrShape _ _ sh) =
+  lift rsPPInfo >>= \ppInfo ->
   lift $ fail $ renderDoc $ fillSep
   [pretty "layoutArgShapeByVal: Shape with unknown length:",
-   permPretty emptyPPInfo sh]
+   permPretty ppInfo sh]
 
 -- A field shape --> the contents of the field
 layoutArgShapeByVal Rust (PExpr_FieldShape (LLVMFieldShape p)) =
@@ -958,8 +971,9 @@ layoutArgShapeByVal Rust (PExpr_ExShape mb_sh) =
   existsArgLayout <$> mbM (fmap (layoutArgShapeByVal Rust) mb_sh)
 
 layoutArgShapeByVal Rust sh =
+  lift rsPPInfo >>= \ppInfo ->
   lift $ fail $ renderDoc $ fillSep
-  [pretty "layoutArgShapeByVal: Unsupported shape:", permPretty emptyPPInfo sh]
+  [pretty "layoutArgShapeByVal: Unsupported shape:", permPretty ppInfo sh]
 layoutArgShapeByVal abi _ =
   lift $ fail ("layoutArgShapeByVal: Unsupported ABI: " ++ show abi)
 
@@ -975,9 +989,10 @@ layoutArgShapeOrBlock abi sh =
   Just layout -> return $ Right layout
   Nothing | Just bp <- shapeToBlock sh -> return $ Left bp
   _ ->
+    rsPPInfo >>= \ppInfo ->
     fail $ renderDoc $ fillSep
     [pretty "layoutArgShapeOrBlock: Could not layout shape with unknown size:",
-     permPretty emptyPPInfo sh]
+     permPretty ppInfo sh]
 
 -- | Compute the layout of an argument with the given shape as 1 or more
 -- register arguments of a function
@@ -1087,10 +1102,11 @@ lownedPermsForLifetime l (perms :>: VarAndPerm x p)
   , not (NameSet.member l $ freeVars p)
   = lownedPermsForLifetime l perms
 lownedPermsForLifetime l (_ :>: vap) =
+  rsPPInfo >>= \ppInfo ->
   fail $ renderDoc $ fillSep
   [pretty "lownedPermsForLifetime: could not compute lowned permissions for "
-   <+> permPretty emptyPPInfo l <+> pretty "in:",
-   permPretty emptyPPInfo vap]
+   <+> permPretty ppInfo l <+> pretty "in:",
+   permPretty ppInfo vap]
 
 -- | Get the 'String' name defined by a 'LifetimeDef'
 lifetimeDefName :: LifetimeDef a -> String
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 9a84ab4b6e..3d1494f4b6 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -132,12 +132,32 @@ typeTransType1 (TypeTrans [] _) = unitTypeOpenTerm
 typeTransType1 (TypeTrans [tp] _) = tp
 typeTransType1 _ = error ("typeTransType1" ++ nlPrettyCallStack callStack)
 
--- | Build the tuple of @N@ types, with the special case that a single type is
--- just converted to itself
+-- | Build the tuple type @T1 * (T2 * ... * (Tn-1 * Tn))@ of @n@ types, with the
+-- special case that 0 types maps to the unit type @#()@ (and 1 type just maps
+-- to itself). Note that this is different from 'tupleTypeOpenTerm', which
+-- always ends with unit, i.e., which returns @T1*(T2*...*(Tn-1*(Tn*#())))@.
 tupleOfTypes :: [OpenTerm] -> OpenTerm
 tupleOfTypes [] = unitTypeOpenTerm
 tupleOfTypes [tp] = tp
-tupleOfTypes tps = tupleTypeOpenTerm tps
+tupleOfTypes (tp:tps) = pairTypeOpenTerm tp $ tupleOfTypes tps
+
+-- | Build the tuple @(t1,(t2,(...,(tn-1,tn))))@ of @n@ terms, with the
+-- special case that 0 types maps to the unit value @()@ (and 1 value just maps
+-- to itself). Note that this is different from 'tupleOpenTerm', which
+-- always ends with unit, i.e., which returns @t1*(t2*...*(tn-1*(tn*())))@.
+tupleOfTerms :: [OpenTerm] -> OpenTerm
+tupleOfTerms [] = unitOpenTerm
+tupleOfTerms [t] = t
+tupleOfTerms (t:ts) = pairOpenTerm t $ tupleOfTerms ts
+
+-- | Project the @i@th element from a term of type @'tupleOfTypes' tps@. Note
+-- that this requires knowing the length of @tps@.
+projTupleOfTypes :: [OpenTerm] -> Integer -> OpenTerm -> OpenTerm
+projTupleOfTypes [] _ _ = error "projTupleOfTypes: projection of empty tuple!"
+projTupleOfTypes [_] 0 tup = tup
+projTupleOfTypes (_:_) 0 tup = pairLeftOpenTerm tup
+projTupleOfTypes (_:tps) i tup =
+  projTupleOfTypes tps (i-1) $ pairRightOpenTerm tup
 
 -- | Map the 'typeTransTypes' field of a 'TypeTrans' to a single type, where a
 -- single type is mapped to itself, an empty list of types is mapped to @unit@,
@@ -145,14 +165,13 @@ tupleOfTypes tps = tupleTypeOpenTerm tps
 typeTransTupleType :: TypeTrans tr -> OpenTerm
 typeTransTupleType = tupleOfTypes . typeTransTypes
 
--- | Convert a 'TypeTrans' over 0 or more types to one over 1 type, where 2
--- or more types are converted to a single tuple type
+-- | Convert a 'TypeTrans' over 0 or more types to one over the one type
+-- returned by 'tupleOfTypes'
 tupleTypeTrans :: TypeTrans tr -> TypeTrans tr
--- tupleTypeTrans ttrans@(TypeTrans [] _) = ttrans
-tupleTypeTrans ttrans@(TypeTrans [_] _) = ttrans
 tupleTypeTrans ttrans =
-  TypeTrans [tupleTypeOpenTerm $ typeTransTypes ttrans]
-  (\[t] -> typeTransF ttrans $ map (\i -> projTupleOpenTerm i t) $
+  let tps = typeTransTypes ttrans in
+  TypeTrans [tupleOfTypes tps]
+  (\[t] -> typeTransF ttrans $ map (\i -> projTupleOfTypes tps i t) $
            take (length $ typeTransTypes ttrans) [0..])
 
 -- | Convert a 'TypeTrans' over 0 or more types to one over 1 type of the form
@@ -219,7 +238,7 @@ class IsTermTrans tr where
 -- function returns an element of the type @'tupleTypeTrans' ttrans@.
 transTupleTerm :: IsTermTrans tr => tr -> OpenTerm
 transTupleTerm (transTerms -> [t]) = t
-transTupleTerm tr = tupleOpenTerm $ transTerms tr
+transTupleTerm tr = tupleOfTerms $ transTerms tr
 
 -- | Build a tuple of the terms contained in a translation. This is "strict" in
 -- that it always makes a tuple, even for a single type, unlike
@@ -574,6 +593,10 @@ translateClosed :: (TransInfo info, Translate info ctx a tr) =>
                    a -> TransM info ctx tr
 translateClosed a = nuMultiTransM (const a) >>= translate
 
+instance (Translate info ctx a tr, NuMatching a) =>
+         Translate info ctx [a] [tr] where
+  translate = mapM translate . mbList
+
 
 ----------------------------------------------------------------------
 -- * Translating Types
@@ -781,11 +804,10 @@ instance TransInfo info =>
       return $ ETrans_Term $ bvBVOpenTerm w $ mbLift off
     [nuMP| PExpr_BV bvfactors (BV.BV 0) |] ->
       let w = natVal3 bvfactors in
-      ETrans_Term <$> foldr1 (bvAddOpenTerm w) <$>
-      mapM translate (mbList bvfactors)
+      ETrans_Term <$> foldr1 (bvAddOpenTerm w) <$> translate bvfactors
     [nuMP| PExpr_BV bvfactors off |] ->
       do let w = natRepr3 bvfactors
-         bv_transs <- mapM translate $ mbList bvfactors
+         bv_transs <- translate bvfactors
          return $ ETrans_Term $
            foldr (bvAddOpenTerm $ natValue w) (bvBVOpenTerm w $ mbLift off) bv_transs
     [nuMP| PExpr_Struct args |] ->
@@ -822,7 +844,7 @@ instance TransInfo info =>
       do let w = natVal4 mb_len
          let w_term = natOpenTerm w
          len_term <- translate1 mb_len
-         elem_tp <- tupleOfTypes <$> concat <$> mapM translate (mbList mb_fshs)
+         elem_tp <- tupleOfTypes <$> concat <$> translate mb_fshs
          return $ ETrans_Term $
            applyOpenTermMulti (globalOpenTerm "Prelude.BVVec")
            [w_term, len_term, elem_tp]
@@ -1420,7 +1442,7 @@ setLLVMArrayTransCell arr_trans (LLVMArrayIndexTrans _ i_trans _)
 -- | Adjust an array cell (= list of fields) of the translation of an LLVM array
 -- permission at a given index by applying a function to it
 adjustLLVMArrayTransCell :: (1 <= w, KnownNat w) => LLVMArrayPermTrans ctx w ->
-                            OpenTerm ->  LLVMArrayIndexTrans ctx w ->
+                            OpenTerm -> LLVMArrayIndexTrans ctx w ->
                             LLVMArrayPermTrans ctx w
 adjustLLVMArrayTransCell arr_trans f_trm (LLVMArrayIndexTrans _ i_trans _) =
   let w = fromInteger $ natVal arr_trans in
@@ -1516,6 +1538,65 @@ setLLVMArrayTransSlice arr_trans sub_arr_trans off_tm =
       (globalOpenTerm "Prelude.updSliceBVVec")
       [natOpenTerm w, len_tm, elem_tp, arr_tm, off_tm, len'_tm, sub_arr_tm] }
 
+-- | Weaken a monadic function of type @(T1*...*Tn) -> CompM(U1*...*Um)@ to one
+-- of type @(V*T1*...*Tn) -> CompM(V*U1*...*Um)@, @n@-ary tuple types are built
+-- using 'tupleOfTypes'
+weakenMonadicFun1 :: OpenTerm -> [OpenTerm] -> [OpenTerm] -> OpenTerm ->
+                     OpenTerm
+weakenMonadicFun1 v ts us f =
+  -- First form a term f1 of type V*(T1*...*Tn) -> CompM(V*(U1*...*Um))
+  let t_tup = tupleOfTypes ts
+      u_tup = tupleOfTypes us
+      f1 =
+        applyOpenTermMulti (globalOpenTerm "Prelude.tupleCompMFunBoth")
+        [t_tup, u_tup, v, f] in
+
+  let f2 = case ts of
+        -- If ts is empty, form the term \ (x:V) -> f1 (x, ()) to coerce f1 from
+        -- type V*#() -> CompM(V*Us) to type V -> CompM(V*Us)
+        [] ->
+          lambdaOpenTerm "x" v $ \x ->
+          applyOpenTerm f1 (pairOpenTerm x unitOpenTerm)
+        -- Otherwise, leave f1 unchanged
+        _ -> f1 in
+
+  case us of
+    -- If us is empty, compose f2 with \ (x:V*#()) -> returnM V x.(1) to coerce
+    -- from V*Us -> CompM (V*#()) to V*Us -> CompM V
+    [] ->
+      applyOpenTermMulti (globalOpenTerm "Prelude.composeM")
+      [tupleOfTypes (v:ts), pairTypeOpenTerm v unitTypeOpenTerm, v, f2,
+       lambdaOpenTerm "x" (pairTypeOpenTerm v unitTypeOpenTerm)
+       (\x -> applyOpenTermMulti (globalOpenTerm "Prelude.returnM")
+              [v, pairLeftOpenTerm x])]
+    -- Otherwise, leave f2 unchanged
+    _ -> f2
+
+
+-- | Weaken a monadic function of type @(T1*...*Tn) -> CompM(U1*...*Um)@ to one
+-- of type @(V1*...*Vk*T1*...*Tn) -> CompM(V1*...*Vk*U1*...*Um)@, where tuples
+-- of 2 or more types are right-nested and and in a unit type, i.e., have the
+-- form @(T1 * (T2 * (... * (Tn * #()))))@
+weakenMonadicFun :: [OpenTerm] -> [OpenTerm] -> [OpenTerm] -> OpenTerm ->
+                    OpenTerm
+weakenMonadicFun vs ts_top us_top f_top =
+  let (_,_,ret) =
+        foldr (\v (ts,us,f) -> (v:ts, v:us, weakenMonadicFun1 v ts us f))
+        (ts_top, us_top, f_top)
+        vs in
+  ret
+
+-- | Weaken a monadic function which is the translation of an ownership
+-- permission @lowned(ps_in -o ps_out)@ to @lowned(P * ps_in -o P * ps_out)@
+weakenLifetimeFun :: TypeTrans (PermTrans ctx a) ->
+                     TypeTrans (PermTransCtx ctx ps_in) ->
+                     TypeTrans (PermTransCtx ctx ps_out) ->
+                     OpenTerm -> OpenTerm
+weakenLifetimeFun tp_trans ps_in_trans ps_out_trans f =
+  weakenMonadicFun (transTerms
+                    tp_trans) (transTerms
+                               ps_in_trans) (transTerms ps_out_trans) f
+
 
 instance (1 <= w, KnownNat w, TransInfo info) =>
          Translate info ctx (BVProp w) (TypeTrans (BVPropTrans ctx w)) where
@@ -1616,7 +1697,7 @@ instance TransInfo info =>
              translate (mbMap2 (unfoldDefinedPerm dp) args off)
            Nothing -> error "Unknown permission name!"
     [nuMP| ValPerm_Conj ps |] ->
-      fmap PTrans_Conj <$> listTypeTrans <$> mapM translate (mbList ps)
+      fmap PTrans_Conj <$> listTypeTrans <$> translate ps
     [nuMP| ValPerm_Var x _ |] ->
       mkPermTypeTrans1 p <$> translate1 x
 
@@ -1659,8 +1740,8 @@ instance TransInfo info =>
     [nuMP| Perm_LLVMFrame fp |] ->
       return $ mkTypeTrans0 $ APTrans_LLVMFrame fp
     [nuMP| Perm_LOwned ls ps_in ps_out |] ->
-      do tp_in <- translate1 ps_in
-         tp_out <- translate1 ps_out
+      do tp_in <- typeTransTupleType <$> translate ps_in
+         tp_out <- typeTransTupleType <$> translate ps_out
          let tp = arrowOpenTerm "ps" tp_in (applyOpenTerm
                                             (globalOpenTerm "Prelude.CompM")
                                             tp_out)
@@ -1690,9 +1771,7 @@ translateLLVMArrayPerm mb_ap =
      let w_term = natOpenTerm w
      let mb_len = fmap llvmArrayLen mb_ap
      let mb_flds = fmap llvmArrayFields mb_ap
-     flds_trans <-
-       tupleTypeTrans <$> listTypeTrans <$>
-       mapM (translate . fmap llvmArrayFieldToAtomicPerm) (mbList mb_flds)
+     flds_trans <- tupleTypeTrans <$> listTypeTrans <$> translate mb_flds
      len_term <- translate1 mb_len
      let elem_tp = typeTransType1 flds_trans
      {-
@@ -1746,13 +1825,19 @@ instance TransInfo info =>
                                                  (PermTransCtx ctx ps)) where
   translate = translate . mbDistPermsToValuePerms . fmap unTypeDistPerms
 
+instance (TransInfo info, 1 <= w, KnownNat w) =>
+         Translate info ctx (LLVMArrayField w) (TypeTrans
+                                                (AtomicPermTrans ctx
+                                                 (LLVMPointerType w))) where
+  translate = translate . fmap llvmArrayFieldToAtomicPerm
+
+
 -- LOwnedPerms translate to a single tuple type, because lowned permissions
 -- translate to functions with one argument and one return value
 instance TransInfo info =>
          Translate info ctx (LOwnedPerms ps) (TypeTrans
                                               (PermTransCtx ctx ps)) where
-  translate =
-    fmap strictTupleTypeTrans . translate . fmap (RL.map lownedPermPerm)
+  translate = translate . fmap (RL.map lownedPermPerm)
 
 -- Translate a FunPerm to a pi-abstraction (FIXME: more documentation!)
 instance TransInfo info =>
@@ -2467,13 +2552,10 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     m
 
 
-  [nuMP| SImpl_LLVMArrayRearrange _ _ mb_ap2 |] ->
-    do ap2_tp_trans <- translate mb_ap2
+  [nuMP| SImpl_LLVMArrayRearrange _ _ _ |] ->
+    do ttrans <- translateSimplImplOutHead mb_simpl
        withPermStackM id
-         (\(pctx :>: ptrans_array) ->
-           pctx :>:
-           PTrans_Conj [APTrans_LLVMArray $
-                        typeTransF ap2_tp_trans [transTerm1 ptrans_array]])
+         (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
 
   [nuMP| SImpl_LLVMArrayToField _ _ _ |] ->
@@ -2564,8 +2646,38 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            pctx :>: PTrans_Conj [APTrans_LLVMArray arr_trans'])
          m
 
-  [nuMP| SImpl_LLVMArrayContents _ _ _ _ _ |] ->
-    error "FIXME HERE: translateSimplImpl: SImpl_LLVMArrayContents unhandled"
+  [nuMP| SImpl_LLVMArrayContents _ ap flds' impl |] ->
+    do p_out_trans <- translateSimplImplOutHead mb_simpl
+       (w_term, len_term, elem_tp, _) <- translateLLVMArrayPerm ap
+       flds_in_trans <-
+         fmap tupleTypeTrans $ translate $
+         fmap (ValPerm_Conj . map llvmArrayFieldToAtomicPerm . llvmArrayFields) ap
+       flds_out_trans <-
+         fmap tupleTypeTrans $ translate $
+         fmap (ValPerm_Conj . map llvmArrayFieldToAtomicPerm) flds'
+       impl_tm <-
+         -- FIXME: this code just fabricates a pretend LLVM value for the
+         -- arbitrary field of the array, which seems like a hack
+         inExtTransM ETrans_LLVM $
+         translateCurryLocalPermImpl "Error mapping array field permissions:"
+         (mbCombine RL.typeCtxProxies impl) MNil MNil
+         (fmap ((MNil :>:) . extPermTrans) flds_in_trans) (MNil :>: Member_Base)
+         (fmap ((MNil :>:) . extPermTrans) flds_out_trans)
+       -- Build the computation that maps impl_tm over the input array using the
+       -- mapBVVecM monadic combinator
+       ptrans_arr <- getTopPermM
+       let arr_out_comp_tm =
+             applyOpenTermMulti
+             (globalOpenTerm "Prelude.mapBVVecM")
+             [elem_tp, typeTransType1 flds_out_trans, impl_tm,
+              w_term, len_term, transTerm1 ptrans_arr]
+       -- Now use bindM to bind the result of arr_out_comp_tm in the remaining
+       -- computation
+       applyMultiTransM (return $ globalOpenTerm "Prelude.bindM")
+         [return (typeTransType1 p_out_trans), returnTypeM,
+          return arr_out_comp_tm,
+          lambdaTransM "mapped_array" p_out_trans $ \ptrans_arr' ->
+           withPermStackM id (\(pctx :>: _) -> pctx :>: ptrans_arr') m]
 
   [nuMP| SImpl_LLVMFieldIsPtr x _ |] ->
     withPermStackM (:>: translateVar x)
@@ -2587,8 +2699,8 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
 
   [nuMP| SImpl_SplitLifetime _ f args l _ _ ps_in ps_out |] ->
     do pctx_out_trans <- translateSimplImplOut mb_simpl
-       ps_in_tp <- translate1 ps_in
-       ps_out_tp <- translate1 ps_out
+       ps_in_trans <- translate ps_in
+       ps_out_trans <- translate ps_out
        x_tp_trans <- translate (mbMap3 ltFuncApply f args l)
        withPermStackM
          (\(ns :>: x :>: _ :>: l2) -> ns :>: x :>: l2)
@@ -2596,15 +2708,9 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            -- The permission for x does not change type, just its lifetime; the
            -- permission for l has the (tupled) type of x added as a new input and
            -- output with tupleCompMFunBoth
-           let (f_tm,_,_) =
-                 foldr (\x_tp (f_term,f_in_tp,f_out_tp) ->
-                         ( applyOpenTermMulti
-                           (globalOpenTerm "Prelude.tupleCompMFunBoth")
-                           [f_in_tp, f_out_tp, x_tp, f_term]
-                         , pairTypeOpenTerm x_tp f_in_tp
-                         , pairTypeOpenTerm x_tp f_out_tp))
-                 (transTerm1 ptrans_l, ps_in_tp, ps_out_tp)
-                 (transTerms x_tp_trans) in
+           let f_tm =
+                 weakenLifetimeFun x_tp_trans ps_in_trans ps_out_trans $
+                 transTerm1 ptrans_l in
            RL.append pctx $
            typeTransF pctx_out_trans (transTerms ptrans_x ++ [f_tm]))
          m
@@ -2652,10 +2758,10 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                            ps_in' ps_out' ps1 ps2 impl_in impl_out |] ->
     -- First, translate the output permissions and all of the perm lists
     do pctx_out_trans <- translateSimplImplOut mb_simpl
-       ps_in_trans <- translate ps_in
-       ps_out_trans <- translate ps_out
-       ps_in'_trans <- translate ps_in'
-       ps_out'_trans <- translate ps_out'
+       ps_in_trans <- tupleTypeTrans <$> translate ps_in
+       ps_out_trans <- tupleTypeTrans <$> translate ps_out
+       ps_in'_trans <- tupleTypeTrans <$> translate ps_in'
+       ps_out'_trans <- tupleTypeTrans <$> translate ps_out'
        -- ps1_trans <- translate ps1
        -- ps2_trans <- translate ps2
 
@@ -2692,12 +2798,12 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
        let l_res_tm =
              applyOpenTermMulti
              (globalOpenTerm "Prelude.composeM")
-             [transTerm1 ps_in'_trans, transTerm1 ps_in_trans,
-              transTerm1 ps_out'_trans, impl_in_tm,
+             [typeTransType1 ps_in'_trans, typeTransType1 ps_in_trans,
+              typeTransType1 ps_out'_trans, impl_in_tm,
               applyOpenTermMulti
               (globalOpenTerm "Prelude.composeM")
-              [transTerm1 ps_in_trans, transTerm1 ps_out_trans,
-               transTerm1 ps_out'_trans, transTerm1 ptrans_l, impl_out_tm]]
+              [typeTransType1 ps_in_trans, typeTransType1 ps_out_trans,
+               typeTransType1 ps_out'_trans, transTerm1 ptrans_l, impl_out_tm]]
 
        -- Finally, update the permissions
        withPermStackM
@@ -2708,7 +2814,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
   [nuMP| SImpl_EndLifetime _ ps_in ps_out |] ->
     -- First, translate the output permissions and the input and output types of
     -- the monadic function for the lifeime ownership permission
-    do ps_out_trans <- translate ps_out
+    do ps_out_trans <- tupleTypeTrans <$> translate ps_out
        let prxs_in = mbRAssignProxies ps_in :>: Proxy
 
        -- Next, split out the ps_in permissions from the rest of the pctx
@@ -2727,9 +2833,9 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
        -- Now we apply the lifetime ownerhip function to ps_in and bind its output
        -- in the rest of the computation
        applyMultiTransM (return $ globalOpenTerm "Prelude.bindM")
-         [return (transTerm1 ps_out_trans), returnTypeM,
+         [return (typeTransType1 ps_out_trans), returnTypeM,
           return (applyOpenTerm (transTerm1 ptrans_l)
-                  (strictTransTupleTerm pctx_in)),
+                  (transTupleTerm pctx_in)),
           lambdaTransM "endl_ps" ps_out_trans $ \pctx_out ->
            withPermStackM
            (\(_ :>: l) -> vars_out :>: l)
@@ -3479,7 +3585,7 @@ instance ImplTranslateF (LocalImplRet ps) ext blocks ps_in ret where
     do pctx <- itiPermStack <$> ask
        ret_tp <- returnTypeM
        return $ applyOpenTermMulti (globalOpenTerm "Prelude.returnM")
-         [ret_tp, strictTransTupleTerm pctx]
+         [ret_tp, transTupleTerm pctx]
 
 -- | Translate a local implication to its output, adding an error message
 translateLocalPermImpl :: String -> Mb ctx (LocalPermImpl ps_in ps_out) ->
@@ -3500,7 +3606,7 @@ translateCurryLocalPermImpl ::
   ImpTransM ext blocks tops ret ps ctx OpenTerm
 translateCurryLocalPermImpl err impl pctx1 vars1 tp_trans2 vars2 tp_trans_out =
   lambdaTransM "x_local" tp_trans2 $ \pctx2 ->
-  local (\info -> info { itiReturnType = transTerm1 tp_trans_out }) $
+  local (\info -> info { itiReturnType = typeTransType1 tp_trans_out }) $
   withPermStackM
     (const (RL.append vars1 vars2))
     (const (RL.append pctx1 pctx2))
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
index b0cb527e98..872509124f 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
@@ -421,7 +421,7 @@ tcLLVMShape (ExOrSh _ x y) = PExpr_OrShape <$> tcKExpr x <*> tcKExpr y
 tcLLVMShape (ExExSh _ var vartype sh) =
   do Some ktp'@KnownReprObj <- tcTypeKnown vartype
      fmap PExpr_ExShape $ mbM $ nu \z ->
-       withExprVar var (unKnownReprObj ktp') z (tcLLVMShape sh)
+       withExprVar var (unKnownReprObj ktp') z (tcKExpr sh)
 tcLLVMShape (ExSeqSh _ x y) = PExpr_SeqShape <$> tcKExpr x <*> tcKExpr y
 tcLLVMShape ExEmptySh{} = pure PExpr_EmptyShape
 tcLLVMShape (ExEqSh _ v) = PExpr_EqShape <$> tcKExpr v
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
index fdd44e7d78..d1b7d19c5b 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -4031,12 +4031,12 @@ visitCallSite (TypedEntry {..}) site@(TypedCallSite {..})
 
 -- | Widen the permissions held by all callers of an entrypoint to compute new,
 -- weaker input permissions that can hopefully be satisfied by them
-widenEntry :: PermCheckExtC ext => DebugLevel ->
+widenEntry :: PermCheckExtC ext => DebugLevel -> PermEnv ->
               TypedEntry TCPhase ext blocks tops ret args ghosts ->
               Some (TypedEntry TCPhase ext blocks tops ret args)
-widenEntry dlevel (TypedEntry {..}) =
+widenEntry dlevel env (TypedEntry {..}) =
   debugTrace dlevel ("Widening entrypoint: " ++ show typedEntryID) $
-  case foldl1' (widen dlevel typedEntryTops typedEntryArgs) $
+  case foldl1' (widen dlevel env typedEntryTops typedEntryArgs) $
        map (fmapF typedCallSiteArgVarPerms) typedEntryCallers of
     Some (ArgVarPerms ghosts perms_in) ->
       let callers =
@@ -4070,6 +4070,7 @@ visitEntry _ _ _ entry
 -- Otherwise, visit the call sites, widen if needed, and type-check the body
 visitEntry names can_widen blk entry =
   (stDebugLevel <$> get) >>= \dlevel ->
+  (stPermEnv <$> get) >>= \env ->
   debugTracePretty dlevel
   (vsep [pretty ("visitEntry " ++ show (typedEntryID entry)
                  ++ " with input perms:"),
@@ -4079,7 +4080,7 @@ visitEntry names can_widen blk entry =
   mapM (traverseF $
         visitCallSite entry) (typedEntryCallers entry) >>= \callers ->
   if can_widen && any (anyF typedCallSiteImplFails) callers then
-    case widenEntry dlevel entry of
+    case widenEntry dlevel env entry of
       Some entry' ->
         -- If we widen then we are throwing away the old body, so all of its
         -- callees are no longer needed and can be deleted
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
index b52408a0e0..449e4d0d03 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
@@ -119,18 +119,21 @@ instance Monad (PolyContT r m) where
 
 data WidState = WidState { _wsNameMap :: WidNameMap,
                            _wsPPInfo :: PPInfo,
-                           _wsDebugLevel :: DebugLevel }
+                           _wsPermEnv :: PermEnv,
+                           _wsDebugLevel :: DebugLevel,
+                           _wsRecFlag :: RecurseFlag }
 
 makeLenses ''WidState
 
 type WideningM =
   StateT WidState (PolyContT ExtVarPermsFun Identity)
 
-runWideningM :: WideningM () -> DebugLevel -> WidNameMap -> RAssign Name args ->
+runWideningM :: WideningM () -> DebugLevel -> PermEnv -> RAssign Name args ->
                 ExtVarPerms args
-runWideningM m dlevel wnmap =
+runWideningM m dlevel env =
   applyExtVarPermsFun $ runIdentity $
-  runPolyContT (runStateT m $ WidState wnmap emptyPPInfo dlevel)
+  runPolyContT (runStateT m $
+                WidState NameMap.empty emptyPPInfo env dlevel RecNone)
   (Identity . wnMapExtWidFun . _wsNameMap . snd)
 
 openMb :: CruCtx ctx -> Mb ctx a -> WideningM (RAssign Name ctx, a)
@@ -657,6 +660,40 @@ widenPerm' _ (ValPerm_Named npn1 args1 off1) (ValPerm_Named npn2 args2 off2)
   , offsetsEq off1 off2 =
     (\args -> ValPerm_Named npn1 args off1) <$>
     widenExprs (namedPermNameArgs npn1) args1 args2
+widenPerm' tp (ValPerm_Named npn1 args1 off1) p2
+  | DefinedSortRepr _ <- namedPermNameSort npn1 =
+    do env <- use wsPermEnv
+       let np1 = requireNamedPerm env npn1
+       widenPerm tp (unfoldPerm np1 args1 off1) p2
+widenPerm' tp p1 (ValPerm_Named npn2 args2 off2)
+  | DefinedSortRepr _ <- namedPermNameSort npn2 =
+    do env <- use wsPermEnv
+       let np2 = requireNamedPerm env npn2
+       widenPerm tp p1 (unfoldPerm np2 args2 off2)
+widenPerm' tp (ValPerm_Named npn1 args1 off1) p2
+  | RecursiveSortRepr _ _ <- namedPermNameSort npn1 =
+    use wsRecFlag >>= \case
+      RecRight ->
+        -- If we have already unfolded on the right, don't unfold on the left
+        -- (for termination reasons); instead just give up and return true
+        return ValPerm_True
+      _ ->
+        do wsRecFlag .= RecLeft
+           env <- use wsPermEnv
+           let np1 = requireNamedPerm env npn1
+           widenPerm tp (unfoldPerm np1 args1 off1) p2
+widenPerm' tp p1 (ValPerm_Named npn2 args2 off2)
+  | RecursiveSortRepr _ _ <- namedPermNameSort npn2 =
+    use wsRecFlag >>= \case
+      RecLeft ->
+        -- If we have already unfolded on the left, don't unfold on the right
+        -- (for termination reasons); instead just give up and return true
+        return ValPerm_True
+      _ ->
+        do wsRecFlag .= RecRight
+           env <- use wsPermEnv
+           let np2 = requireNamedPerm env npn2
+           widenPerm tp p1 (unfoldPerm np2 args2 off2)
 widenPerm' _ (ValPerm_Var x1 off1) (ValPerm_Var x2 off2)
   | x1 == x2 && offsetsEq off1 off2 = return $ ValPerm_Var x1 off1
 widenPerm' tp (ValPerm_Conj ps1) (ValPerm_Conj ps2) =
@@ -879,13 +916,13 @@ simplifyGhostPerms _ some_avps = some_avps
 ----------------------------------------------------------------------
 
 -- | Widen two lists of permissions-in-bindings
-widen :: DebugLevel -> CruCtx tops -> CruCtx args ->
+widen :: DebugLevel -> PermEnv -> CruCtx tops -> CruCtx args ->
          Some (ArgVarPerms (tops :++: args)) ->
          Some (ArgVarPerms (tops :++: args)) ->
          Some (ArgVarPerms (tops :++: args))
-widen dlevel tops args (Some (ArgVarPerms
-                              vars1 mb_perms1)) (Some (ArgVarPerms
-                                                       vars2 mb_perms2)) =
+widen dlevel env tops args (Some (ArgVarPerms
+                                  vars1 mb_perms1)) (Some (ArgVarPerms
+                                                           vars2 mb_perms2)) =
   let all_args = appendCruCtx tops args
       prxs1 = cruCtxProxies vars1
       prxs2 = cruCtxProxies vars2
@@ -893,7 +930,7 @@ widen dlevel tops args (Some (ArgVarPerms
   simplifyGhostPerms (cruCtxProxies all_args) $
   completeArgVarPerms $ flip nuMultiWithElim1 mb_mb_perms1 $
   \args_ns1 mb_perms1' ->
-  (\m -> runWideningM m dlevel NameMap.empty args_ns1) $
+  (\m -> runWideningM m dlevel env args_ns1) $
   do (vars1_ns, ps1) <- openMb vars1 mb_perms1'
      (ns2, ps2) <- openMb (appendCruCtx all_args vars2) mb_perms2
      let (args_ns2, vars2_ns) = RL.split all_args prxs2 ns2
diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
index 8237878d58..cfcecfaac1 100644
--- a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
+++ b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
@@ -459,6 +459,10 @@ Axiom expByNat : forall (a : Type), a -> (a -> a -> a) -> a -> @SAWCoreScaffoldi
 
 (* Prelude.gen was skipped *)
 
+Axiom head : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreScaffolding.Succ n) a -> a .
+
+Axiom tail : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreScaffolding.Succ n) a -> @SAWCoreVectorsAsCoqVectors.Vec n a .
+
 (* Prelude.atWithDefault was skipped *)
 
 Definition sawAt : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec n a -> @SAWCoreScaffolding.Nat -> a :=
@@ -830,11 +834,11 @@ Definition uncurrySigma : forall (a : Type), forall (b : a -> Type), forall (c :
 
 (* Prelude.List__rec was skipped *)
 
-Definition unfoldList : forall (a : Type), @Datatypes.list a -> @Either unit (prod a (prod (@Datatypes.list a) unit)) :=
-  fun (a : Type) (l : @Datatypes.list a) => @Datatypes.list_rect a (fun (_1 : @Datatypes.list a) => @Either unit (prod a (prod (@Datatypes.list a) unit))) (@Left unit (prod a (prod (@Datatypes.list a) unit)) tt) (fun (x : a) (l1 : @Datatypes.list a) (_1 : @Either unit (prod a (prod (@Datatypes.list a) unit))) => @Right unit (prod a (prod (@Datatypes.list a) unit)) (pair x (pair l1 tt))) l.
+Definition unfoldList : forall (a : Type), @Datatypes.list a -> @Either unit (prod a (@Datatypes.list a)) :=
+  fun (a : Type) (l : @Datatypes.list a) => @Datatypes.list_rect a (fun (_1 : @Datatypes.list a) => @Either unit (prod a (@Datatypes.list a))) (@Left unit (prod a (@Datatypes.list a)) tt) (fun (x : a) (l1 : @Datatypes.list a) (_1 : @Either unit (prod a (@Datatypes.list a))) => @Right unit (prod a (@Datatypes.list a)) (pair x l1)) l.
 
-Definition foldList : forall (a : Type), @Either unit (prod a (prod (@Datatypes.list a) unit)) -> @Datatypes.list a :=
-  fun (a : Type) => @either unit (prod a (prod (@Datatypes.list a) unit)) (@Datatypes.list a) (fun (_1 : unit) => @Datatypes.nil a) (fun (tup : prod a (prod (@Datatypes.list a) unit)) => @Datatypes.cons a (SAWCoreScaffolding.fst tup) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd tup))).
+Definition foldList : forall (a : Type), @Either unit (prod a (@Datatypes.list a)) -> @Datatypes.list a :=
+  fun (a : Type) => @either unit (prod a (@Datatypes.list a)) (@Datatypes.list a) (fun (_1 : unit) => @Datatypes.nil a) (fun (tup : prod a (@Datatypes.list a)) => @Datatypes.cons a (SAWCoreScaffolding.fst tup) (SAWCoreScaffolding.snd tup)).
 
 Inductive ListSort : Type :=
 | LS_Nil : @ListSort
@@ -1011,6 +1015,18 @@ Definition foldIRT : forall (As : @ListSort), forall (Ds : @IRTSubsts As), foral
 
 (* Prelude.bindM was skipped *)
 
+Definition fmapM : forall (a : Type), forall (b : Type), (a -> b) -> CompM a -> CompM b :=
+  fun (a : Type) (b : Type) (f : a -> b) (m : CompM a) => @bindM CompM _ a b m (fun (x : a) => @returnM CompM _ b (f x)).
+
+Definition applyM : forall (a : Type), forall (b : Type), CompM (a -> b) -> CompM a -> CompM b :=
+  fun (a : Type) (b : Type) (f : CompM (a -> b)) (m : CompM a) => @bindM CompM _ (a -> b) b f (fun (f1 : a -> b) => @bindM CompM _ a b m (fun (x : a) => @returnM CompM _ b (f1 x))).
+
+Definition fmapM2 : forall (a : Type), forall (b : Type), forall (c : Type), (a -> b -> c) -> CompM a -> CompM b -> CompM c :=
+  fun (a : Type) (b : Type) (c : Type) (f : a -> b -> c) (m1 : CompM a) (m2 : CompM b) => @applyM b c (@fmapM a (b -> c) f m1) m2.
+
+Definition fmapM3 : forall (a : Type), forall (b : Type), forall (c : Type), forall (d : Type), (a -> b -> c -> d) -> CompM a -> CompM b -> CompM c -> CompM d :=
+  fun (a : Type) (b : Type) (c : Type) (d : Type) (f : a -> b -> c -> d) (m1 : CompM a) (m2 : CompM b) (m3 : CompM c) => @applyM c d (@fmapM2 a b (c -> d) f m1 m2) m3.
+
 Definition composeM : forall (a : Type), forall (b : Type), forall (c : Type), (a -> CompM b) -> (b -> CompM c) -> a -> CompM c :=
   fun (a : Type) (b : Type) (c : Type) (f : a -> CompM b) (g : b -> CompM c) (x : a) => @bindM CompM _ b c (f x) g.
 
@@ -1020,6 +1036,12 @@ Definition tupleCompMFunBoth : forall (a : Type), forall (b : Type), forall (c :
 Definition tupleCompMFunOut : forall (a : Type), forall (b : Type), forall (c : Type), c -> (a -> CompM b) -> a -> CompM (prod c b) :=
   fun (a : Type) (b : Type) (c : Type) (x : c) (f : a -> CompM b) (y : a) => @bindM CompM _ b (prod c b) (f y) (fun (z : b) => @returnM CompM _ (prod c b) (pair x z)).
 
+Definition mapM : forall (a : Type), forall (b : Type), (a -> CompM b) -> forall (n : @SAWCoreScaffolding.Nat), @SAWCoreVectorsAsCoqVectors.Vec n a -> CompM (@SAWCoreVectorsAsCoqVectors.Vec n b) :=
+  fun (a : Type) (b : Type) (f : a -> CompM b) => @Nat__rec (fun (n : @SAWCoreScaffolding.Nat) => @SAWCoreVectorsAsCoqVectors.Vec n a -> CompM (@SAWCoreVectorsAsCoqVectors.Vec n b)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 0 a) => @returnM CompM _ (@SAWCoreVectorsAsCoqVectors.Vec 0 b) (@SAWCoreVectorsAsCoqVectors.EmptyVec b)) (fun (n : @SAWCoreScaffolding.Nat) (rec_f : @SAWCoreVectorsAsCoqVectors.Vec n a -> CompM (@SAWCoreVectorsAsCoqVectors.Vec n b)) (v : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreScaffolding.Succ n) a) => @fmapM2 b (@SAWCoreVectorsAsCoqVectors.Vec n b) (@SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreScaffolding.Succ n) b) (fun (hd : b) (tl : @SAWCoreVectorsAsCoqVectors.Vec n b) => @ConsVec b hd n tl) (f (@head n a v)) (rec_f (@tail n a v))).
+
+Definition mapBVVecM : forall (a : Type), forall (b : Type), (a -> CompM b) -> forall (n : @SAWCoreScaffolding.Nat), forall (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @BVVec n len a -> CompM (@BVVec n len b) :=
+  fun (a : Type) (b : Type) (f : a -> CompM b) (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) => @mapM a b f (@SAWCoreVectorsAsCoqVectors.bvToNat n len).
+
 (* Prelude.errorM was skipped *)
 
 (* Prelude.fixM was skipped *)
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index 60a4d7226b..ed8827b56a 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -911,6 +911,10 @@ primitive Vec : Nat -> sort 0 -> sort 0;
 -- Primitive function for generating an array.
 primitive gen : (n : Nat) -> (a : sort 0) -> (Nat -> a) -> Vec n a;
 
+-- Primitive eliminators for arrays
+primitive head : (n : Nat) -> (a : sort 0) -> Vec (Succ n) a -> a;
+primitive tail : (n : Nat) -> (a : sort 0) -> Vec (Succ n) a -> Vec n a;
+
 primitive atWithDefault : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> a;
 
 at : (n : Nat) -> (a : sort 0) -> Vec n a -> Nat -> a;
@@ -1447,20 +1451,20 @@ List__rec :
   (l : List a) -> P l;
 List__rec a P f1 f2 l = List#rec a P f1 f2 l;
 
-unfoldList : (a:sort 0) -> List a -> Either #() (a * List a * #());
+unfoldList : (a:sort 0) -> List a -> Either #() (a * List a);
 unfoldList a l =
-  List__rec a (\ (_:List a) -> Either #() (a * List a * #()))
-  (Left #() (a * List a * #()) ())
-  (\ (x:a) (l:List a) (_:Either #() (a * List a * #())) ->
-     Right #() (a * List a * #()) (x, l, ()))
+  List__rec a (\ (_:List a) -> Either #() (a * List a))
+  (Left #() (a * List a) ())
+  (\ (x:a) (l:List a) (_:Either #() (a * List a)) ->
+     Right #() (a * List a) (x, l))
   l;
 
-foldList : (a:sort 0) -> Either #() (a * List a * #()) -> List a;
+foldList : (a:sort 0) -> Either #() (a * List a) -> List a;
 foldList a =
-  either #() (a * List a * #()) (List a)
+  either #() (a * List a) (List a)
          (\ (_ : #()) -> Nil a)
-         (\ (tup : (a * List a * #())) ->
-            Cons a tup.(1) tup.(2).(1));
+         (\ (tup : (a * List a)) ->
+            Cons a tup.(1) tup.(2));
 
 -- A list of types, i.e. `List (sort 0)` if `List` was universe polymorphic
 data ListSort : sort 1
@@ -1956,6 +1960,24 @@ primitive CompM : sort 0 -> sort 0;
 primitive returnM : (a:sort 0) -> a -> CompM a;
 primitive bindM : (a b:sort 0) -> CompM a -> (a -> CompM b) -> CompM b;
 
+-- Apply a pure function to a computation
+fmapM : (a b: sort 0) -> (a -> b) -> CompM a -> CompM b;
+fmapM a b f m = bindM a b m (\ (x:a) -> returnM b (f x));
+
+-- Apply a computation of a function to a computation of an argument
+applyM : (a b: sort 0) -> CompM (a -> b) -> CompM a -> CompM b;
+applyM a b f m =
+  bindM (a -> b) b f (\ (f:a->b) -> bindM a b m (\ (x:a) -> returnM b (f x)));
+
+-- Apply a binary pure function to a computation
+fmapM2 : (a b c: sort 0) -> (a -> b -> c) -> CompM a -> CompM b -> CompM c;
+fmapM2 a b c f m1 m2 = applyM b c (fmapM a (b -> c) f m1) m2;
+
+-- Apply a trinary pure function to a computation
+fmapM3 : (a b c d: sort 0) -> (a -> b -> c -> d) ->
+         CompM a -> CompM b -> CompM c -> CompM d;
+fmapM3 a b c d f m1 m2 m3 = applyM c d (fmapM2 a b (c -> d) f m1 m2) m3;
+
 -- Compose two monadic functions
 composeM : (a b c: sort 0) -> (a -> CompM b) -> (b -> CompM c) -> a -> CompM c;
 composeM a b c f g x = bindM b c (f x) g;
@@ -1971,6 +1993,24 @@ tupleCompMFunOut : (a b c: sort 0) -> c -> (a -> CompM b) -> (a -> CompM (c * b)
 tupleCompMFunOut a b c x f =
   \ (y:a) -> bindM b (c*b) (f y) (\ (z:b) -> returnM (c*b) (x,z));
 
+-- Map a monadic function across a vector
+mapM : (a b : sort 0) -> (a -> CompM b) -> (n : Nat) -> Vec n a -> CompM (Vec n b);
+mapM a b f =
+  Nat__rec
+    (\ (n:Nat) -> Vec n a -> CompM (Vec n b))
+    (\ (_:Vec 0 a) -> returnM (Vec 0 b) (EmptyVec b))
+    (\ (n:Nat) (rec_f:Vec n a -> CompM (Vec n b)) (v:Vec (Succ n) a) ->
+       fmapM2 b (Vec n b) (Vec (Succ n) b)
+              (\ (hd:b) (tl:Vec n b) -> ConsVec b hd n tl)
+              (f (head n a v))
+              (rec_f (tail n a v)));
+
+-- Map a monadic function across a BVVec
+mapBVVecM : (a b : sort 0) -> (a -> CompM b) ->
+            (n : Nat) -> (len : Vec n Bool) -> BVVec n len a ->
+            CompM (BVVec n len b);
+mapBVVecM a b f n len = mapM a b f (bvToNat n len);
+
 -- Raise an error in the computation monad
 primitive errorM : (a:sort 0) -> String -> CompM a;