diff --git a/heapster-saw/examples/rust_data.bc b/heapster-saw/examples/rust_data.bc
index fd49d18547..6cf6f5b23d 100644
Binary files a/heapster-saw/examples/rust_data.bc and b/heapster-saw/examples/rust_data.bc differ
diff --git a/heapster-saw/examples/rust_data.rs b/heapster-saw/examples/rust_data.rs
index 22460617eb..5894659ab0 100644
--- a/heapster-saw/examples/rust_data.rs
+++ b/heapster-saw/examples/rust_data.rs
@@ -279,19 +279,6 @@ impl List<u64> {
     }
 }
 
-/* Dummy function to figure out the size of a HashMap */
-pub fn test_hash_map_size (x:(HashMap<u64,u64>, u64)) -> u64 {
-    let (_,u) = x; return u;
-}
-
-pub fn my_hash_insert (m: &mut HashMap<u64,u64>, x:u64, y:u64) -> Option<u64> {
-    return m.insert (x,y);
-}
-
-pub fn my_hash_insert_void (m: &mut HashMap<u64,u64>, x:u64, y:u64) -> () {
-    m.insert (x,y);
-}
-
 /* Insert a mapping into m from the greatest of x and y to the other */
 pub fn hash_map_insert_gt_to_le (m: &mut HashMap<u64,u64>, x:u64, y:u64) -> () {
     if x > y {
diff --git a/heapster-saw/examples/rust_data.saw b/heapster-saw/examples/rust_data.saw
index 61150aed46..87615dd329 100644
--- a/heapster-saw/examples/rust_data.saw
+++ b/heapster-saw/examples/rust_data.saw
@@ -50,6 +50,9 @@ heapster_define_rust_type env "pub struct MixedStruct { pub s: String, pub i1: u
 // TrueEnum type
 heapster_define_rust_type env "pub enum TrueEnum { Foo, Bar, Baz }";
 
+// Opaque type for Vec<T>
+//heapster_define_opaque_llvmshape env "Vec" 64 "T:llvmshape 64" "24" "\\ (T:sort 0) -> List T";
+
 // Opaque type for HashMap<T,U>
 heapster_define_opaque_llvmshape env "HashMap" 64 "T:llvmshape 64, U:llvmshape 64" "56" "\\ (T:sort 0) (U:sort 0) -> List (T * U)";
 
@@ -79,22 +82,10 @@ heapster_assume_fun_rename env to_string_str "to_string_str" "(len:bv 64). arg0:
 
 
 // HashMap::insert
-/*
-my_hash_insert_void_sym <- heapster_find_symbol env "19my_hash_insert_void";
-heapster_assume_fun_rename env my_hash_insert_void_sym "hashmap_u64_u64_insert_void" "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> ()" "\\ (l,k,v) -> Cons (k,v) l";
-*/
-
-/*
 // FIXME: we currently pretend this always returns None
-// FIXME: also, the layout is currently broken for return type of Option<u64>
-my_hash_insert_sym <- heapster_find_symbol env "14my_hash_insert";
-heapster_assume_fun_rename env my_hash_insert_sym "hashmap_u64_u64_insert" "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> Option<u64>" "\\ (l,k,v) -> Cons (k,v) l";
-*/
-
-/*
 hashmap_u64_u64_insert_sym <- heapster_find_symbol env "std11collections4hash3map24HashMap$LT$K$C$V$C$S$GT$6insert";
-heapster_assume_fun_rename env hashmap_u64_u64_insert_sym "hashmap_u64_u64_insert" "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> Option<u64>" "\\ (l,k,v) -> Cons (k,v) l";
-*/
+heapster_assume_fun_rename env hashmap_u64_u64_insert_sym "hashmap_u64_u64_insert" "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> Option<u64>" "\\ (endl:HashMap int64Trans int64Trans * #() -> CompM (HashMap int64Trans int64Trans * #())) (h:HashMap int64Trans int64Trans) (k:int64Trans) (v:int64Trans) -> returnM ((#() -> CompM (HashMap int64Trans int64Trans * #())) * Either #() int64Trans * #()) ((\\ (_:#()) -> returnM (HashMap int64Trans int64Trans * #()) (Cons (int64Trans * int64Trans) (k,v) h, ())), Left #() int64Trans (), ())";
+
 
 /***
  *** Type-Checked Functions
@@ -149,7 +140,7 @@ heapster_typecheck_fun_rename env list_head_sym "list_head" "<'a> fn (l: &'a Lis
 
 // list_head_impl
 list_head_impl_sym <- heapster_find_symbol env "14list_head_impl";
-//heapster_typecheck_fun_rename env list_head_impl_sym "list_head_impl" "<'a> fn (l: &'a List<u64>) -> Result<u64,()>";
+heapster_typecheck_fun_rename env list_head_impl_sym "list_head_impl" "<'a> fn (l: &'a List<u64>) -> Result<u64,()>";
 //heapster_typecheck_fun_rename env list_head_impl_sym "list_head_impl" "(rw:rwmodality).arg0:List<fieldsh(int64<>),8,rw,always> -o ret:(struct(eq(llvmword(0)),exists z:bv 64. eq(llvmword(z)))) or (struct(eq(llvmword(1)),true))";
 
 // StrStruct::new
diff --git a/heapster-saw/examples/rust_data.v b/heapster-saw/examples/rust_data.v
index bfc770c212..8edda650ce 100644
--- a/heapster-saw/examples/rust_data.v
+++ b/heapster-saw/examples/rust_data.v
@@ -57,6 +57,16 @@ Definition to_string_str : forall (e0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAW
   CompM (@sigT var__0 (fun (x_exsh0 : var__0) => prod (@SAWCorePrelude.BVVec 64 x_exsh0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT var__0 (fun (x_ex0 : var__0) => unit)) unit))) :=
   fun (len : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (_1 : unit) (str : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreVectorsAsCoqVectors.bvToNat 64 len) int8Trans) => @returnM CompM _ (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (len' : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 len' int8Trans) (prod int64Trans unit))) (@existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (len' : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 len' int8Trans) (prod int64Trans unit)) len (pair str (pair (@mkInt64Trans len) tt))).
 
+Definition hashmap_u64_u64_insert : forall (p0 : forall (ps : prod (@HashMap (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  let var__1   := @sigT var__0 (fun (x_ex0 : var__0) => unit) in
+  CompM (prod (@HashMap var__1 var__1) unit)), forall (p1 : @HashMap (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))), forall (p2 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)), forall (p3 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (forall (ps : unit), let var__1   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  let var__2   := @sigT var__1 (fun (x_ex0 : var__1) => unit) in
+  CompM (prod (@HashMap var__2 var__2) unit)) (prod (@SAWCorePrelude.Either unit (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) :=
+  fun (endl : prod (@Datatypes.list (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)))) unit -> let var__0   := int64Trans in
+  CompM (prod (@HashMap var__0 var__0) unit)) (h : @Datatypes.list (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)))) (k : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (v : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) => @returnM CompM _ (prod (unit -> let var__0   := int64Trans in
+  CompM (prod (@HashMap var__0 var__0) unit)) (prod (@SAWCorePrelude.Either unit int64Trans) unit)) (pair (fun (_1 : unit) => @returnM CompM _ (prod (@HashMap int64Trans int64Trans) unit) (pair (@Datatypes.cons (prod int64Trans int64Trans) (pair k v) h) tt)) (pair (@SAWCorePrelude.Left unit int64Trans tt) tt)).
+
 Definition bool_and__tuple_fun : @CompM.lrtTupleType (@CompM.LRT_Cons (@CompM.LRT_Fun (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) (fun (perm0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) => @CompM.LRT_Fun (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) (fun (perm1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) => @CompM.LRT_Ret (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit))))) (@CompM.LRT_Nil)) :=
   @CompM.multiFixM (@CompM.LRT_Cons (@CompM.LRT_Fun (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) (fun (perm0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) => @CompM.LRT_Fun (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) (fun (perm1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) => @CompM.LRT_Ret (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit))))) (@CompM.LRT_Nil)) (fun (bool_and : @CompM.lrtToType (@CompM.LRT_Fun (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) (fun (perm0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) => @CompM.LRT_Fun (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) (fun (perm1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) => @CompM.LRT_Ret (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)))))) => pair (fun (p0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) (p1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) => @CompM.letRecM (@CompM.LRT_Nil) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) tt (@returnM CompM _ (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)) (@existT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit) (@SAWCorePrelude.bvAnd 1 (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit) p0) (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit) p1)) tt))) tt).
 
@@ -283,6 +293,29 @@ Definition list_head : @CompM.lrtToType (@CompM.LRT_Fun (forall (ps : prod (@Lis
   CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (prod (@SAWCorePrelude.Either (prod unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit)) (prod unit (prod unit unit))) unit))))) :=
   SAWCoreScaffolding.fst list_head__tuple_fun.
 
+Definition list_head_impl__tuple_fun : @CompM.lrtTupleType (@CompM.LRT_Cons (@CompM.LRT_Fun (forall (ps : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (fun (perm0 : forall (ps : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) => @CompM.LRT_Fun (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) (fun (perm1 : @List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) => @CompM.LRT_Ret (prod (forall (ps : unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (prod (@SAWCorePrelude.Either (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit) unit))))) (@CompM.LRT_Nil)) :=
+  @CompM.multiFixM (@CompM.LRT_Cons (@CompM.LRT_Fun (forall (ps : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (fun (perm0 : forall (ps : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) => @CompM.LRT_Fun (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) (fun (perm1 : @List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) => @CompM.LRT_Ret (prod (forall (ps : unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (prod (@SAWCorePrelude.Either (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit) unit))))) (@CompM.LRT_Nil)) (fun (list_head_impl : @CompM.lrtToType (@CompM.LRT_Fun (forall (ps : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (fun (perm0 : forall (ps : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) => @CompM.LRT_Fun (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) (fun (perm1 : @List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) => @CompM.LRT_Ret (prod (forall (ps : unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (prod (@SAWCorePrelude.Either (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit) unit)))))) => pair (fun (p0 : forall (ps : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (p1 : @List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) => @CompM.letRecM (@CompM.LRT_Nil) (prod (forall (ps : unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (prod (@SAWCorePrelude.Either (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit) unit)) tt (@SAWCorePrelude.either (prod unit unit) (prod unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (CompM (prod (forall (ps : unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (prod (@SAWCorePrelude.Either (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit) unit))) (fun (x_left0 : prod unit unit) => @returnM CompM _ (prod (forall (ps : unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (prod (@SAWCorePrelude.Either (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit) unit)) (pair (@SAWCorePrelude.composeM unit (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (fun (x_local0 : unit) => @returnM CompM _ (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (pair (@foldList_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (@SAWCorePrelude.Left (prod unit unit) (prod unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (pair tt (SAWCoreScaffolding.snd x_left0)))) tt)) (@SAWCorePrelude.composeM (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) p0 (fun (x_local0 : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) => @returnM CompM _ (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (pair (SAWCoreScaffolding.fst x_local0) tt)))) (pair (@SAWCorePrelude.Right (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit tt) tt))) (fun (x_right0 : prod unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) => @returnM CompM _ (prod (forall (ps : unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (prod (@SAWCorePrelude.Either (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit) unit)) (pair (@SAWCorePrelude.composeM unit (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (fun (x_local0 : unit) => @returnM CompM _ (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (pair (@foldList_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (@SAWCorePrelude.Right (prod unit unit) (prod unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (pair tt (pair (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd x_right0)) (SAWCoreScaffolding.snd (SAWCoreScaffolding.snd x_right0)))))) tt)) (@SAWCorePrelude.composeM (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) p0 (fun (x_local0 : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) => @returnM CompM _ (prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit) (pair (SAWCoreScaffolding.fst x_local0) tt)))) (pair (@SAWCorePrelude.Left (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit (@existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit) (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd x_right0))) tt)) tt))) (@unfoldList_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) p1))) tt).
+
+Definition list_head_impl : @CompM.lrtToType (@CompM.LRT_Fun (forall (ps : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (fun (perm0 : forall (ps : prod (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) => @CompM.LRT_Fun (@List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) (fun (perm1 : @List_IRT (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) => @CompM.LRT_Ret (prod (forall (ps : unit), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@List_IRT (@sigT var__0 (fun (x_ex0 : var__0) => unit))) unit)) (prod (@SAWCorePrelude.Either (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit) unit))))) :=
+  SAWCoreScaffolding.fst list_head_impl__tuple_fun.
+
 Definition str_struct_new__tuple_fun : @CompM.lrtTupleType (@CompM.LRT_Cons (@CompM.LRT_Fun (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (arg0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => @CompM.LRT_Fun unit (fun (perm0 : unit) => @CompM.LRT_Fun (@SAWCorePrelude.BVVec 64 arg0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (fun (perm1 : @SAWCorePrelude.BVVec 64 arg0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) => @CompM.LRT_Ret (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_exsh0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_exsh0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit))))))) (@CompM.LRT_Nil)) :=
   @CompM.multiFixM (@CompM.LRT_Cons (@CompM.LRT_Fun (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (arg0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => @CompM.LRT_Fun unit (fun (perm0 : unit) => @CompM.LRT_Fun (@SAWCorePrelude.BVVec 64 arg0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (fun (perm1 : @SAWCorePrelude.BVVec 64 arg0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) => @CompM.LRT_Ret (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_exsh0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_exsh0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit))))))) (@CompM.LRT_Nil)) (fun (str_struct_new : @CompM.lrtToType (@CompM.LRT_Fun (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (arg0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => @CompM.LRT_Fun unit (fun (perm0 : unit) => @CompM.LRT_Fun (@SAWCorePrelude.BVVec 64 arg0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (fun (perm1 : @SAWCorePrelude.BVVec 64 arg0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) => @CompM.LRT_Ret (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_exsh0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_exsh0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit)))))))) => pair (fun (e0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (p0 : unit) (p1 : @SAWCorePrelude.BVVec 64 e0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) => @CompM.letRecM (@CompM.LRT_Nil) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_exsh0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_exsh0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit))) tt (@bindM CompM _ (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_exsh0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_exsh0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit))) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_exsh0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_exsh0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit))) (@to_string_str e0 tt p1) (fun (call_ret_val : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_exsh0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_exsh0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit))) => @bindM CompM _ (prod unit (prod unit unit)) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_exsh0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_exsh0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit))) (@llvm__x2ememcpy__x2ep0i8__x2ep0i8__x2ei64 unit (intToBv 64 0x18%Z) p0 tt) (fun (call_ret_val1 : prod unit (prod unit unit)) => @returnM CompM _ (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_exsh0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_exsh0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit))) (@existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit)) (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit)) call_ret_val) (pair (SAWCoreScaffolding.fst (@projT2 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit)) call_ret_val)) (pair (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd (@projT2 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 8 (@SAWCoreScaffolding.Bool)) => unit))) (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) unit)) call_ret_val))) tt))))))) tt).
 
diff --git a/heapster-saw/examples/rust_data_proofs.v b/heapster-saw/examples/rust_data_proofs.v
index 120cac2005..4623e67ae9 100644
--- a/heapster-saw/examples/rust_data_proofs.v
+++ b/heapster-saw/examples/rust_data_proofs.v
@@ -23,7 +23,7 @@ Print list_is_empty__tuple_fun.
 
 Print list_head__tuple_fun.
 
-(* Print list_head_impl__tuple_fun. *)
+Print list_head_impl__tuple_fun.
 
 Print str_struct_new__tuple_fun.
 
diff --git a/heapster-saw/examples/rust_lifetimes.v b/heapster-saw/examples/rust_lifetimes.v
index 38dbdc92e0..dd4983ae6f 100644
--- a/heapster-saw/examples/rust_lifetimes.v
+++ b/heapster-saw/examples/rust_lifetimes.v
@@ -41,9 +41,10 @@ Definition unfoldListPermH : forall (a : Type), @Datatypes.list a -> @SAWCorePre
 Definition foldListPermH : forall (a : Type), @SAWCorePrelude.Either unit (prod unit (prod a (@Datatypes.list a))) -> @Datatypes.list a :=
   fun (a : Type) => @SAWCorePrelude.either unit (prod unit (prod a (@Datatypes.list a))) (@Datatypes.list a) (fun (_1 : unit) => @Datatypes.nil a) (fun (tup : prod unit (prod a (@Datatypes.list a))) => @Datatypes.cons a (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd tup)) (SAWCoreScaffolding.snd (SAWCoreScaffolding.snd tup))).
 
-Definition llvm__x2euadd__x2ewith__x2eoverflow__x2ei64 : forall (p0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)), forall (p1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
-  let var__1   := @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool) in
-  CompM (prod (@sigT var__0 (fun (x_ex0 : var__0) => unit)) (prod (@sigT var__1 (fun (x_ex0 : var__1) => unit)) unit)) :=
+Definition llvm__x2euadd__x2ewith__x2eoverflow__x2ei64 : forall (p0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)), forall (p1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)), let var__0   := forall (a : Type), forall (b : a -> Type), Type in
+  let var__1   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  let var__2   := @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool) in
+  CompM (prod (@sigT var__1 (fun (x_ex0 : var__1) => unit)) (prod (@sigT var__2 (fun (x_ex0 : var__2) => unit)) unit)) :=
   fun (x : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (y : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) => @returnM CompM _ (prod int64Trans (prod int1Trans unit)) (pair (@mkInt64Trans (@SAWCoreVectorsAsCoqVectors.bvAdd 64 (@unInt64Trans x) (@unInt64Trans y))) (pair (@mkInt1Trans (@SAWCoreVectorsAsCoqVectors.gen 1 (@SAWCoreScaffolding.Bool) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.bvCarry 64 (@unInt64Trans x) (@unInt64Trans y)))) tt)).
 
 Definition llvm__x2eexpect__x2ei1 : forall (p0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)), forall (p1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool)) => unit)), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 1 (@SAWCoreScaffolding.Bool) in
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
index 9824b5d26f..693e98d874 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
@@ -489,6 +489,22 @@ assignToRList asgn = case viewAssign asgn of
   AssignEmpty -> MNil
   AssignExtend asgn' f -> assignToRList asgn' :>: f
 
+-- | Invert 'assignToRList', converting a Hobbits 'RAssign' over a Hobbits
+-- context generated by 'CtxToRList' back to a Crucible 'Assignment'
+unAssignToRList :: Assignment prx ctx -> RAssign f (CtxToRList ctx) ->
+                   Assignment f ctx
+unAssignToRList ctx fs =
+  let sz = Ctx.size ctx in
+  Ctx.generate sz $ \ix -> RL.get (indexToMember sz ix) fs
+
+-- | Append two Hobbits 'RAssign's that have been generated by 'assignToRList'
+assignToRListAppend :: Assignment prx1 ctx1 -> Assignment prx2 ctx2 ->
+                       RAssign f (CtxToRList ctx1) ->
+                       RAssign f (CtxToRList ctx2) ->
+                       RAssign f (CtxToRList (ctx1 <+> ctx2))
+assignToRListAppend ctx1 ctx2 fs1 fs2 =
+  assignToRList (unAssignToRList ctx1 fs1 Ctx.<++> unAssignToRList ctx2 fs2)
+
 -- | Convert a Crucible 'Assignment' over a context of contexts to an 'RAssign'
 -- over a right-list of right-lists
 assignToRListRList :: (forall c. f c -> g (CtxToRList c)) ->
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index e1b3cc6faf..fd9e7d9c20 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -2964,6 +2964,57 @@ isConjPerm (ValPerm_Named n _ _) = nameSortIsConj (namedPermNameSort n)
 isConjPerm (ValPerm_Var _ _) = False
 isConjPerm (ValPerm_Conj _) = True
 
+-- | Return a struct permission where all fields have @true@ permissions
+trueStructAtomicPerm :: Assignment prx ctx -> AtomicPerm (StructType ctx)
+trueStructAtomicPerm =
+  Perm_Struct . RL.map (const ValPerm_True). assignToRList
+
+-- | Take two list of atomic struct permissions, one for structs with fields
+-- given by @ctx1@ and one with those given by @ctx2@, and append them pointwise
+-- to get a list of atomic struct permissions whose fields are given by the
+-- append @ctx1 <+> ctx2@. If one list is shorter than the other, fill it out
+-- with struct permissions @struct (true, ..., true)@ of all @true@ permissions.
+-- This only works if both lists have only 'Perm_Struct' permissions, and
+-- otherwise return 'Nothing'.
+tryAppendStructAPerms :: Assignment prx1 ctx1 -> Assignment prx2 ctx2 ->
+                         [AtomicPerm (StructType ctx1)] ->
+                         [AtomicPerm (StructType ctx2)] ->
+                         Maybe [AtomicPerm (StructType (ctx1 <+> ctx2))]
+tryAppendStructAPerms _ _ [] [] = return []
+tryAppendStructAPerms ctx1 ctx2 (Perm_Struct fs_ps:ps) (Perm_Struct fs_qs:qs) =
+  (Perm_Struct (assignToRListAppend ctx1 ctx2 fs_ps fs_qs) :) <$>
+  tryAppendStructAPerms ctx1 ctx2 ps qs
+tryAppendStructAPerms ctx1 ctx2 [] qs =
+  tryAppendStructAPerms ctx1 ctx2 [trueStructAtomicPerm ctx1] qs
+tryAppendStructAPerms ctx1 ctx2 ps [] =
+  tryAppendStructAPerms ctx1 ctx2 ps [trueStructAtomicPerm ctx2]
+tryAppendStructAPerms _ _ _ _ = mzero
+
+-- | Try to append struct permissions for structs with fields given by @ctx1@
+-- and @ctx2@ to get a permission for structs with fields given by the append
+-- @ctx1 <+> ctx2@ of these two contexts. Return 'Nothing' if this is not
+-- possible.
+tryAppendStructPerms :: Assignment prx1 ctx1 -> Assignment prx2 ctx2 ->
+                        ValuePerm (StructType ctx1) ->
+                        ValuePerm (StructType ctx2) ->
+                        Maybe (ValuePerm (StructType (ctx1 <+> ctx2)))
+tryAppendStructPerms ctx1 ctx2 (ValPerm_Or p1 p2) q =
+  ValPerm_Or <$> tryAppendStructPerms ctx1 ctx2 p1 q <*>
+  tryAppendStructPerms ctx1 ctx2 p2 q
+tryAppendStructPerms ctx1 ctx2 p (ValPerm_Or q1 q2) =
+  ValPerm_Or <$> tryAppendStructPerms ctx1 ctx2 p q1 <*>
+  tryAppendStructPerms ctx1 ctx2 p q2
+tryAppendStructPerms ctx1 ctx2 (ValPerm_Exists mb_p) q =
+  ValPerm_Exists <$> mbMaybe (flip fmap mb_p $ \p ->
+                               tryAppendStructPerms ctx1 ctx2 p q)
+tryAppendStructPerms ctx1 ctx2 p (ValPerm_Exists mb_q) =
+  ValPerm_Exists <$> mbMaybe (flip fmap mb_q $ \q ->
+                               tryAppendStructPerms ctx1 ctx2 p q)
+tryAppendStructPerms ctx1 ctx2 (ValPerm_Conj ps) (ValPerm_Conj qs) =
+  ValPerm_Conj <$> tryAppendStructAPerms ctx1 ctx2 ps qs
+tryAppendStructPerms _ _ _ _ = mzero
+
+
 -- | Helper function to build a 'Perm_LLVMFunPtr' from a 'FunPerm'
 mkPermLLVMFunPtr :: (1 <= w, KnownNat w) => f w -> FunPerm ghosts args ret ->
                     AtomicPerm (LLVMPointerType w)
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs
index 78afe0280e..b6c621aab0 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs
@@ -42,6 +42,10 @@ import qualified Control.Monad.Fail as Fail
 
 import Data.Parameterized.BoolRepr
 import Data.Parameterized.Some
+import Data.Parameterized.Context (Assignment, IsAppend(..),
+                                   incSize, zeroSize, sizeInt,
+                                   size, generate, extend)
+import qualified Data.Parameterized.Context as Ctx
 
 import Data.Binding.Hobbits
 import Data.Binding.Hobbits.MonadBind
@@ -504,35 +508,120 @@ instance RsConvert w (StructField Span) (PermExpr (LLVMShapeType w)) where
 -- * Computing the ABI-Specific Layout of Rust Types
 ----------------------------------------------------------------------
 
--- | An argument layout is a sequence of Crucible types for 0 or more function
--- arguments along with permissions on them, which could be existential in some
--- number of ghost arguments. The ghost arguments cannot have permissions on
--- them, so that we can create struct permissions from just the arg perms.
+-- | An 'ArgLayoutPerm' is a set of permissions on a sequence of 0 or more
+-- arguments, given by the @tps@ type-level argument. These permissions are
+-- similar to the language of permissions on a Crucible struct, except that the
+-- langauge is restricted to ensure that they can always be appended.
+data ArgLayoutPerm ctx where
+  ALPerm :: RAssign ValuePerm (CtxToRList ctx) -> ArgLayoutPerm ctx
+  ALPerm_Or :: ArgLayoutPerm ctx -> ArgLayoutPerm ctx -> ArgLayoutPerm ctx
+  ALPerm_Exists :: KnownRepr TypeRepr a =>
+                   Binding a (ArgLayoutPerm ctx) -> ArgLayoutPerm ctx
+
+-- | Build an 'ArgLayoutPerm' that just assigns @true@ to every field
+trueArgLayoutPerm :: Assignment prx ctx -> ArgLayoutPerm ctx
+trueArgLayoutPerm ctx = ALPerm (RL.map (const ValPerm_True) $ assignToRList ctx)
+
+-- | Build an 'ArgLayoutPerm' for 0 fields
+argLayoutPerm0 :: ArgLayoutPerm EmptyCtx
+argLayoutPerm0 = ALPerm MNil
+
+-- | Build an 'ArgLayoutPerm' for a single field
+argLayoutPerm1 :: ValuePerm a -> ArgLayoutPerm (EmptyCtx '::> a)
+argLayoutPerm1 p = ALPerm (MNil :>: p)
+
+-- | Convert an 'ArgLayoutPerm' to a permission on a struct
+argLayoutPermToPerm :: ArgLayoutPerm ctx -> ValuePerm (StructType ctx)
+argLayoutPermToPerm (ALPerm ps) = ValPerm_Conj1 $ Perm_Struct ps
+argLayoutPermToPerm (ALPerm_Or p1 p2) =
+  ValPerm_Or (argLayoutPermToPerm p1) (argLayoutPermToPerm p2)
+argLayoutPermToPerm (ALPerm_Exists mb_p) =
+  ValPerm_Exists $ fmap argLayoutPermToPerm mb_p
+
+-- | Convert an 'ArgLayoutPerm' on a single field to a permission on single
+-- values of the type of that field
+argLayoutPerm1ToPerm :: ArgLayoutPerm (EmptyCtx '::> a) -> ValuePerm a
+argLayoutPerm1ToPerm (ALPerm (_ :>: p)) = p
+argLayoutPerm1ToPerm (ALPerm_Or p1 p2) =
+  ValPerm_Or (argLayoutPerm1ToPerm p1) (argLayoutPerm1ToPerm p2)
+argLayoutPerm1ToPerm (ALPerm_Exists mb_p) =
+  ValPerm_Exists $ fmap argLayoutPerm1ToPerm mb_p
+
+-- | Append the field types @ctx1@ and @ctx2@ of two 'ArgLayoutPerm's to get a
+-- combined 'ArgLayoutPerm' over the combined fields
+appendArgLayoutPerms :: Assignment prx1 ctx1 -> Assignment prx2 ctx2 ->
+                        ArgLayoutPerm ctx1 -> ArgLayoutPerm ctx2 ->
+                        ArgLayoutPerm (ctx1 <+> ctx2)
+appendArgLayoutPerms ctx1 ctx2 (ALPerm_Or p1 p2) q =
+  ALPerm_Or (appendArgLayoutPerms ctx1 ctx2 p1 q)
+  (appendArgLayoutPerms ctx1 ctx2 p2 q)
+appendArgLayoutPerms ctx1 ctx2 p (ALPerm_Or q1 q2) =
+  ALPerm_Or (appendArgLayoutPerms ctx1 ctx2 p q1)
+  (appendArgLayoutPerms ctx1 ctx2 p q2)
+appendArgLayoutPerms ctx1 ctx2 (ALPerm_Exists mb_p) q =
+  ALPerm_Exists $ fmap (\p -> appendArgLayoutPerms ctx1 ctx2 p q) mb_p
+appendArgLayoutPerms ctx1 ctx2 p (ALPerm_Exists mb_q) =
+  ALPerm_Exists $ fmap (\q -> appendArgLayoutPerms ctx1 ctx2 p q) mb_q
+appendArgLayoutPerms ctx1 ctx2 (ALPerm ps) (ALPerm qs) =
+  ALPerm $ assignToRListAppend ctx1 ctx2 ps qs
+
+-- | An argument layout captures how argument values are laid out as a Crucible
+-- struct of 0 or more machine words / fields
 data ArgLayout where
-  ArgLayout :: KnownCruCtx ghosts -> KnownCruCtx args ->
-               Mb ghosts (ValuePerms args) -> ArgLayout
+  ArgLayout :: CtxRepr ctx -> ArgLayoutPerm ctx -> ArgLayout
 
-instance Semigroup ArgLayout where
-  ArgLayout ghosts1 args1 mb_ps1 <> ArgLayout ghosts2 args2 mb_ps2 =
-    ArgLayout (RL.append ghosts1 ghosts2) (RL.append args1 args2) $
-    mbCombine (RL.mapRAssign (const Proxy) ghosts2) $
-    fmap (\ps1 -> fmap (\ps2 -> RL.append ps1 ps2) mb_ps2) mb_ps1
+-- | Count the number of fields of an 'ArgLayout'
+argLayoutNumFields :: ArgLayout -> Int
+argLayoutNumFields (ArgLayout ctx _) = sizeInt $ size ctx
 
-instance Monoid ArgLayout where
-  mempty = ArgLayout MNil MNil (emptyMb $ MNil)
+-- | Construct an 'ArgLayout' for 0 arguments
+argLayout0 :: ArgLayout
+argLayout0 = ArgLayout Ctx.empty (ALPerm MNil)
 
--- | Construct an 'ArgLayout' for a single argument with no ghost variables
+-- | Construct an 'ArgLayout' for a single argument
 argLayout1 :: KnownRepr TypeRepr a => ValuePerm a -> ArgLayout
-argLayout1 p =
-  ArgLayout MNil (MNil :>: KnownReprObj) $ emptyMb (MNil :>: p)
-
--- | Convert an 'ArgLayout' in a name-binding into an 'ArgLayout' with an
--- additional ghost argument for the bound name
-mbArgLayout :: KnownRepr TypeRepr a => Binding a ArgLayout -> ArgLayout
-mbArgLayout (mbMatch -> [nuMP| ArgLayout ghosts args mb_ps |]) =
-  ArgLayout (mbLift ghosts :>: KnownReprObj) (mbLift args)
-            (mbCombine RL.typeCtxProxies (mbSwap (RL.mapRAssign (const Proxy) (mbLift ghosts)) mb_ps))
-
+argLayout1 p = ArgLayout (extend Ctx.empty knownRepr) (ALPerm (MNil :>: p))
+
+-- | Append two 'ArgLayout's, if possible
+appendArgLayout :: ArgLayout -> ArgLayout -> ArgLayout
+appendArgLayout (ArgLayout ctx1 p1) (ArgLayout ctx2 p2) =
+  ArgLayout (ctx1 Ctx.<++> ctx2) (appendArgLayoutPerms ctx1 ctx2 p1 p2)
+
+-- | Test if @ctx2@ is an extension of @ctx1@
+ctxIsAppend :: CtxRepr ctx1 -> CtxRepr ctx2 ->
+               Maybe (IsAppend ctx1 ctx2)
+ctxIsAppend ctx1 ctx2
+  | Just Refl <- testEquality ctx1 ctx2
+  = Just $ IsAppend zeroSize
+ctxIsAppend ctx1 (ctx2' Ctx.:> _)
+  | Just (IsAppend sz) <- ctxIsAppend ctx1 ctx2'
+  = Just (IsAppend (incSize sz))
+ctxIsAppend _ _ = Nothing
+
+-- | Take the disjunction of two 'ArgLayout's, if possible
+disjoinArgLayouts :: ArgLayout -> ArgLayout -> Maybe ArgLayout
+disjoinArgLayouts (ArgLayout ctx1 p1) (ArgLayout ctx2 p2)
+  | Just (IsAppend sz') <- ctxIsAppend ctx1 ctx2 =
+    let ps' = generate sz' (const ValPerm_True) in
+    Just $ ArgLayout ctx2 $
+    ALPerm_Or
+    (appendArgLayoutPerms ctx1 ps' p1 (ALPerm $ assignToRList ps'))
+    p2
+disjoinArgLayouts (ArgLayout ctx1 p1) (ArgLayout ctx2 p2)
+  | Just (IsAppend sz') <- ctxIsAppend ctx2 ctx1 =
+    let ps' = generate sz' (const ValPerm_True) in
+    Just $ ArgLayout ctx1 $
+    ALPerm_Or
+    p1
+    (appendArgLayoutPerms ctx2 ps' p2 (ALPerm $ assignToRList ps'))
+disjoinArgLayouts _ _ = Nothing
+
+-- | Make an existential 'ArgLayout'
+existsArgLayout :: KnownRepr TypeRepr a => Binding a ArgLayout -> ArgLayout
+existsArgLayout [nuP| ArgLayout mb_ctx mb_p |] =
+  ArgLayout (mbLift mb_ctx) (ALPerm_Exists mb_p)
+
+{-
 -- | Convert an 'ArgLayout' to a permission on a @struct@ of its arguments
 argLayoutStructPerm :: ArgLayout -> Some (Typed ValuePerm)
 argLayoutStructPerm (ArgLayout ghosts (MNil :>: KnownReprObj) mb_perms) =
@@ -543,6 +632,7 @@ argLayoutStructPerm (ArgLayout ghosts args mb_perms)
   , Refl <- cruCtxToReprEq (knownCtxToCruCtx args) =
     Some $ Typed (StructRepr args_repr) $
     valPermExistsMulti ghosts $ fmap (ValPerm_Conj1 . Perm_Struct) mb_perms
+-}
 
 -- | Convert a shape to a writeable block permission with that shape, or fail if
 -- the length of the shape is not defined
@@ -591,18 +681,47 @@ un3SomeFunPerm args ret (Some3FunPerm fun_perm) =
     <+> pretty "=>"
     <+> PP.group (permPretty emptyPPInfo (funPermRet fun_perm)) ]
 
--- | Build a function permission from an 'ArgLayout' plus return permission
-funPerm3FromArgLayout :: ArgLayout -> TypeRepr ret -> ValuePerm ret ->
-                         Some3FunPerm
-funPerm3FromArgLayout (ArgLayout ghosts args mb_arg_perms) ret_tp ret_perm =
-  let gs_args_prxs = RL.map (const Proxy) (RL.append ghosts args) in
-  Some3FunPerm $ FunPerm (knownCtxToCruCtx ghosts) (knownCtxToCruCtx args)
-  ret_tp
-  (extMbMulti (RL.map (\_ -> Proxy) args) $
-   fmap (RL.append $ RL.map (const ValPerm_True) ghosts) mb_arg_perms)
-  (nuMulti (gs_args_prxs :>: Proxy) $ const
-   (RL.map (const ValPerm_True) gs_args_prxs :>: ret_perm))
-
+-- | Build a function permission from an 'ArgLayout' that describes the
+-- arguments and their input permissions and a return permission that describes
+-- the output permissions on the return value. The arguments specified by the
+-- 'ArgLayout' get no permissions on output. The caller also specifies
+-- additional arguments to be prepended to the argument list that do have output
+-- permissions as a struct of 0 or more fields along with input and output
+-- permissions on those arguments.
+funPerm3FromArgLayout :: ArgLayout -> CtxRepr args ->
+                         ValuePerms (CtxToRList args) ->
+                         ValuePerms (CtxToRList args) ->
+                         TypeRepr ret -> ValuePerm ret ->
+                         RustConvM Some3FunPerm
+funPerm3FromArgLayout (ArgLayout ctx p_in) ctx1 ps1_in ps1_out ret_tp ret_perm
+    -- Special case: if the argument perms are just a sequence of permissions on
+    -- the individual arguments, make a function perm with those argument perms,
+    -- that is, we build the function permission
+    --
+    -- (). arg1:p1, ..., argn:pn -o ret:ret_perm
+  | ALPerm ps_in <- p_in
+  , ctx_all <- mkCruCtx (ctx1 Ctx.<++> ctx)
+  , ps_in_all <- RL.append MNil (assignToRListAppend ctx1 ctx ps1_in ps_in)
+  , ps_out_all <-
+      RL.append MNil (assignToRListAppend ctx1 ctx ps1_out $
+                      trueValuePerms $ assignToRList ctx) :>: ret_perm
+  , gs_ctx_prxs <- RL.append MNil (cruCtxProxies ctx_all) =
+    return $ Some3FunPerm $ FunPerm CruCtxNil ctx_all ret_tp
+    (nuMulti gs_ctx_prxs $ \_ -> ps_in_all)
+    (nuMulti (gs_ctx_prxs :>: Proxy) $ \_ -> ps_out_all)
+funPerm3FromArgLayout (ArgLayout _ctx _p) _ctx1 _p1_in _p1_out _ret_tp _ret_perm =
+  -- FIXME HERE
+  fail "Cannot (yet) handle Rust enums or other disjunctive types in functions"
+
+-- | Like 'funPerm3FromArgLayout' but with no additional arguments
+funPerm3FromArgLayoutNoArgs :: ArgLayout -> TypeRepr ret -> ValuePerm ret ->
+                               RustConvM Some3FunPerm
+funPerm3FromArgLayoutNoArgs layout ret ret_perm =
+  funPerm3FromArgLayout layout Ctx.empty MNil MNil ret ret_perm
+
+
+-- FIXME: should we save any of these?
+{-
 -- | Extend a name binding by adding a name in the middle
 extMbMiddle ::
   forall prx1 ctx1 prx2 ctx2 prxb a b.
@@ -636,6 +755,7 @@ funPerm3PrependArg arg_tp arg_in arg_out (Some3FunPerm
    fmap (rassignInsertMiddle ghosts args_prxs arg_in) ps_in)
   (extMbMiddle ghosts (args_prxs :>: Proxy) arg_tp $
    fmap (rassignInsertMiddle ghosts (args_prxs :>: Proxy) arg_out) ps_out)
+-}
 
 mbSeparatePrx :: prx1 ctx1 -> RAssign prx2 ctx2 -> Mb (ctx1 :++: ctx2) a ->
                  Mb ctx1 (Mb ctx2 a)
@@ -689,6 +809,7 @@ mbGhostsFunPerm3 new_ghosts (mbMatch -> [nuMP| Some3FunPerm
          ghosts_prxs (args_prxs :>: Proxy)) $
          mbCombine (RL.append ghosts_prxs args_prxs :>: Proxy) ps_out)
 
+
 -- | Try to compute the layout of a structure of the given shape as a value,
 -- over 1 or more registers, if this is possible
 layoutArgShapeByVal :: (1 <= w, KnownNat w) => Abi ->
@@ -696,7 +817,7 @@ layoutArgShapeByVal :: (1 <= w, KnownNat w) => Abi ->
                        MaybeT RustConvM ArgLayout
 
 -- The empty shape --> no values
-layoutArgShapeByVal Rust PExpr_EmptyShape = return mempty
+layoutArgShapeByVal Rust PExpr_EmptyShape = return argLayout0
 
 -- Named shapes that unfold --> layout their unfoldings
 layoutArgShapeByVal Rust (PExpr_NamedShape rw l nmsh args)
@@ -745,30 +866,27 @@ layoutArgShapeByVal Rust (PExpr_ArrayShape _ _ _) = mzero
 layoutArgShapeByVal Rust (PExpr_SeqShape sh1 sh2) =
   do layout1 <- layoutArgShapeByVal Rust sh1
      layout2 <- layoutArgShapeByVal Rust sh2
-     case (mappend layout1 layout2) of
-       layout@(ArgLayout _ args _)
-         | length (RL.mapToList (const Proxy) args) <= 2 -> return layout
-       _ -> mzero
+     let layout = appendArgLayout layout1 layout2
+     if argLayoutNumFields layout <= 2 then return layout else mzero
 
 -- Disjunctive shapes are only laid out as values in the Rust ABI if both sides
--- have the same number and sizes of arguments. Note that Heapster currently
--- cannot handle this optimization, and so this is an error, but if the shape
--- cannot be laid out as values then we return Nothing without an error.
-layoutArgShapeByVal Rust sh@(PExpr_OrShape sh1 sh2) =
+-- can be laid out as values that we can coerce to have the same number of type
+-- of fields.
+--
+-- FIXME: The check for whether we can do this coercion is currently done by
+-- disjoinArgLayouts, but it is probably ABI-specific, so should be performed by
+-- a function that knows how to join two lists of field types depending on the
+-- ABI
+layoutArgShapeByVal Rust (PExpr_OrShape sh1 sh2) =
   do layout1 <- layoutArgShapeByVal Rust sh1
      layout2 <- layoutArgShapeByVal Rust sh2
-     case (layout1, layout2) of
-       (ArgLayout _ args1 _, ArgLayout _ args2 _)
-         | Just Refl <-
-           testEquality (knownCtxToCruCtx args1) (knownCtxToCruCtx args2) ->
-           lift $ fail $ renderDoc $ fillSep
-           [pretty "layoutArgShapeByVal: Optimizing disjunctive shapes not yet supported for shape:",
-            permPretty emptyPPInfo sh]
-       _ -> mzero
+     case disjoinArgLayouts layout1 layout2 of
+       Just layout -> return layout
+       Nothing -> mzero
 
 -- For existential shapes, just add the existential variable to the ghosts
 layoutArgShapeByVal Rust (PExpr_ExShape mb_sh) =
-  mbArgLayout <$> mbM (fmap (layoutArgShapeByVal Rust) mb_sh)
+  existsArgLayout <$> mbM (fmap (layoutArgShapeByVal Rust) mb_sh)
 
 layoutArgShapeByVal Rust sh =
   lift $ fail $ renderDoc $ fillSep
@@ -807,18 +925,25 @@ layoutFun :: (1 <= w, KnownNat w) => Abi ->
              [PermExpr (LLVMShapeType w)] -> PermExpr (LLVMShapeType w) ->
              RustConvM Some3FunPerm
 layoutFun abi arg_shs ret_sh =
-  do args_layout <- mconcat <$> mapM (layoutArgShape abi) arg_shs
+  do args_layout <-
+       foldr appendArgLayout argLayout0 <$> mapM (layoutArgShape abi) arg_shs
      ret_layout_eith <- layoutArgShapeOrBlock abi ret_sh
      case ret_layout_eith of
-       Right ret_layout
-         | Some (Typed ret_tp ret_p) <- argLayoutStructPerm ret_layout ->
-           return $ funPerm3FromArgLayout args_layout ret_tp ret_p
+       Right (ArgLayout (Ctx.Empty Ctx.:> ret_tp)
+              (argLayoutPerm1ToPerm -> ret_p)) ->
+         -- Special case: if the return type is a single field, remove the
+         -- struct type and just use the type of that single field
+         funPerm3FromArgLayoutNoArgs args_layout ret_tp ret_p
+       Right (ArgLayout ret_ctx ret_p) ->
+         funPerm3FromArgLayoutNoArgs args_layout (StructRepr ret_ctx)
+         (argLayoutPermToPerm ret_p)
        Left bp ->
-         return $
-         funPerm3PrependArg knownRepr
-         (ValPerm_LLVMBlock $ bp { llvmBlockShape = PExpr_EmptyShape})
-         (ValPerm_LLVMBlock bp) $
-         funPerm3FromArgLayout args_layout UnitRepr ValPerm_True
+           funPerm3FromArgLayout args_layout
+           (extend Ctx.empty knownRepr)
+           (MNil :>: ValPerm_LLVMBlock (bp { llvmBlockShape =
+                                               PExpr_EmptyShape}))
+           (MNil :>: ValPerm_LLVMBlock bp)
+           UnitRepr ValPerm_True
 
 
 ----------------------------------------------------------------------
@@ -1025,6 +1150,8 @@ parseNamedShapeFromRustDecl env w str
 parseNamedShapeFromRustDecl _ _ str =
   fail ("Malformed Rust type: " ++ str)
 
+
+$(mkNuMatching [t| forall ctx. ArgLayoutPerm ctx |])
 $(mkNuMatching [t| ArgLayout |])
 $(mkNuMatching [t| Some3FunPerm |])
 $(mkNuMatching [t| forall a. NuMatching a => SomeTypedMb a |])