Repository: cryspen/hax (language: rust)

Issue:
Engine: dependencies: the sorting seems unstable
See https://github.com/cryspen/libcrux/blob/ml-kem-lax-check/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fst

In this module, functions are in big part independent, but still, they get reordered.


Discussion / hints:
After investigations, it seems like we are sorting the items alphabetically at some point...
See [this example](https://hax-playground.cryspen.com/#fstar/cd6e258cb2/gist=66130ea18eafc6bd5df301936513e155).

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

Fix patch:
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index e46fcb555..0aa79f898 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -33,482 +33,557 @@ module Make (F : Features.T) = struct
 
   module Attrs = Attr_payloads.Make (F) (Error)
 
-  let uid_associated_items (items : item list) : attrs -> item list =
-    let open Attrs.WithItems (struct
-      let items = items
-    end) in
-    raw_associated_item >> List.map ~f:(snd >> item_of_uid)
-
-  module ItemGraph = struct
-    module G = Graph.Persistent.Digraph.Concrete (Concrete_ident)
-    module Topological = Graph.Topological.Make_stable (G)
-    module Oper = Graph.Oper.P (G)
-
-    let vertices_of_item (i : item) : G.V.t list =
-      let ( @ ) = Set.union in
-      let v = U.Reducers.collect_concrete_idents in
-      let concat_map f =
-        List.map ~f >> Set.union_list (module Concrete_ident)
-      in
-      let set =
-        match i.v with
-        | Fn { name = _; generics; body; params; _ } ->
-            v#visit_generics () generics
-            @ v#visit_expr () body
-            @ concat_map (v#visit_param ()) params
-        | TyAlias { name = _; generics; ty } ->
-            v#visit_generics () generics @ v#visit_ty () ty
-        | Type { name = _; generics; variants; is_struct = (_ : bool) } ->
-            v#visit_generics () generics
-            @ concat_map (v#visit_variant ()) variants
-        | IMacroInvokation { macro; argument = (_ : string); span; witness = _ }
-          ->
-            v#visit_concrete_ident () macro @ v#visit_span () span
-        | Trait { name = _; generics; items; safety = _ } ->
-            v#visit_generics () generics
-            @ concat_map (v#visit_trait_item ()) items
-        | Impl { generics; self_ty; of_trait; items; parent_bounds; safety = _ }
-          ->
-            v#visit_generics () generics
-            @ v#visit_ty () self_ty
-            @ v#visit_concrete_ident () (fst of_trait)
-            @ concat_map (v#visit_generic_value ()) (snd of_trait)
-            @ concat_map (v#visit_impl_item ()) items
-            @ concat_map
-                (fun (ie, ii) ->
-                  v#visit_impl_expr () ie @ v#visit_impl_ident () ii)
-                parent_bounds
-        | Alias { name = _; item } -> v#visit_concrete_ident () item
-        | Use _ | Quote _ | HaxError _ | NotImplementedYet ->
-            Set.empty (module Concrete_ident)
-      in
-      set |> Set.to_list
-
-    let vertices_of_items ~uid_associated_items (items : item list) : G.E.t list
-        =
-      List.concat_map
-        ~f:(fun i ->
-          let assoc =
-            uid_associated_items i.attrs |> List.map ~f:(fun i -> i.ident)
+  module type WITH_ITEMS = sig
+    val uid_associated_items : item list -> Ast.attrs -> item list
+    val bundle_cyclic_modules : item list -> item list
+    val sort : item list -> item list
+    val recursive_bundles : item list -> item list list * item list
+
+    val filter_by_inclusion_clauses :
+      Types.inclusion_clause list -> item list -> item list
+  end
+
+  module WithItems (CTX : sig
+    val items : item list
+  end) =
+  struct
+    let uid_associated_items : attrs -> item list =
+      let open Attrs.WithItems (struct
+        let items = CTX.items
+      end) in
+      raw_associated_item >> List.map ~f:(snd >> item_of_uid)
+
+    (** `Ordered_concrete_ident` is just like `Concrete_ident`, but
+    the semantics of comparing two concrete idents is now defined in
+    term of which comes first in `CTX.items`. If we compare items not
+    present in `CTX.items` we revert to `Concrete_ident.compare`. *)
+    module Ordered_concrete_ident = struct
+      include Concrete_ident
+
+      open struct
+        let order : t -> int option =
+          let table : (t, int) Hashtbl.t =
+            let table = Hashtbl.create (module Concrete_ident) in
+            List.iteri CTX.items ~f:(fun i item ->
+                Hashtbl.set ~key:item.ident ~data:i table);
+            table
           in
-          vertices_of_item i @ assoc |> List.map ~f:(Fn.const i.ident &&& Fn.id))
-        items
+          Hashtbl.find table
+      end
 
-    let of_items ~original_items (items : item list) : G.t =
-      let init =
-        List.fold ~init:G.empty ~f:(fun g -> ident_of >> G.add_vertex g) items
-      in
-      let uid_associated_items = uid_associated_items original_items in
-      vertices_of_items ~uid_associated_items items
-      |> List.fold ~init ~f:(G.add_edge >> uncurry)
-
-    let transitive_dependencies_of (g : G.t) (selection : Concrete_ident.t list)
-        : Concrete_ident.t Hash_set.t =
-      let set = Hash_set.create (module Concrete_ident) in
-      let rec visit vertex =
-        if Hash_set.mem set vertex |> not then (
-          Hash_set.add set vertex;
-          G.iter_succ visit g vertex)
-      in
-      List.filter ~f:(G.mem_vertex g) selection |> List.iter ~f:visit;
-      set
+      let compare (a : t) (b : t) =
+        match (order a, order b) with
+        | Some a, Some b -> Int.compare a b
+        | Some _, None -> 1
+        | None, Some _ -> -1
+        | _ -> Concrete_ident.compare a b
+    end
 
-    let transitive_dependencies_of_items ~original_items (items : item list)
-        ?(graph = of_items ~original_items items)
-        (selection : Concrete_ident.t list) : item list =
-      let set = transitive_dependencies_of graph selection in
-      items |> List.filter ~f:(ident_of >> Hash_set.mem set)
+    module ItemGraph = struct
+      module G = Graph.Persistent.Digraph.Concrete (Ordered_concrete_ident)
+      module Topological = Graph.Topological.Make_stable (G)
+      module Oper = Graph.Oper.P (G)
 
-    module MutRec = struct
-      module Bundle = struct
-        type t = concrete_ident list
+      let vertices_of_item (i : item) : G.V.t list =
+        let ( @ ) = Set.union in
+        let v = U.Reducers.collect_concrete_idents in
+        let concat_map f =
+          List.map ~f >> Set.union_list (module Concrete_ident)
+        in
+        let set =
+          match i.v with
+          | Fn { name = _; generics; body; params; _ } ->
+              v#visit_generics () generics
+              @ v#visit_expr () body
+              @ concat_map (v#visit_param ()) params
+          | TyAlias { name = _; generics; ty } ->
+              v#visit_generics () generics @ v#visit_ty () ty
+          | Type { name = _; generics; variants; is_struct = (_ : bool) } ->
+              v#visit_generics () generics
+              @ concat_map (v#visit_variant ()) variants
+          | IMacroInvokation
+              { macro; argument = (_ : string); span; witness = _ } ->
+              v#visit_concrete_ident () macro @ v#visit_span () span
+          | Trait { name = _; generics; items; safety = _ } ->
+              v#visit_generics () generics
+              @ concat_map (v#visit_trait_item ()) items
+          | Impl
+              { generics; self_ty; of_trait; items; parent_bounds; safety = _ }
+            ->
+              v#visit_generics () generics
+              @ v#visit_ty () self_ty
+              @ v#visit_concrete_ident () (fst of_trait)
+              @ concat_map (v#visit_generic_value ()) (snd of_trait)
+              @ concat_map (v#visit_impl_item ()) items
+              @ concat_map
+                  (fun (ie, ii) ->
+                    v#visit_impl_expr () ie @ v#visit_impl_ident () ii)
+                  parent_bounds
+          | Alias { name = _; item } -> v#visit_concrete_ident () item
+          | Use _ | Quote _ | HaxError _ | NotImplementedYet ->
+              Set.empty (module Concrete_ident)
+        in
+        set |> Set.to_list
 
-        let namespaces_of : t -> Namespace.Set.t =
-          List.map ~f:Namespace.of_concrete_ident
-          >> Set.of_list (module Namespace)
+      let vertices_of_items (items : item list) : G.E.t list =
+        List.concat_map
+          ~f:(fun i ->
+            let assoc =
+              uid_associated_items i.attrs |> List.map ~f:(fun i -> i.ident)
+            in
+            vertices_of_item i @ assoc
+            |> List.map ~f:(Fn.const i.ident &&& Fn.id))
+          items
 
-        let homogeneous_namespace (ns : t) : bool =
-          Set.length (namespaces_of ns) <= 1
-      end
+      let of_items (items : item list) : G.t =
+        let init =
+          List.fold ~init:G.empty ~f:(fun g -> ident_of >> G.add_vertex g) items
+        in
+        vertices_of_items items |> List.fold ~init ~f:(G.add_edge >> uncurry)
+
+      let transitive_dependencies_of (g : G.t)
+          (selection : Concrete_ident.t list) : Concrete_ident.t Hash_set.t =
+        let set = Hash_set.create (module Concrete_ident) in
+        let rec visit vertex =
+          if Hash_set.mem set vertex |> not then (
+            Hash_set.add set vertex;
+            G.iter_succ visit g vertex)
+        in
+        List.filter ~f:(G.mem_vertex g) selection |> List.iter ~f:visit;
+        set
+
+      let transitive_dependencies_of_items (items : item list)
+          ?(graph = of_items items) (selection : Concrete_ident.t list) :
+          item list =
+        let set = transitive_dependencies_of graph selection in
+        items |> List.filter ~f:(ident_of >> Hash_set.mem set)
+
+      module MutRec = struct
+        module Bundle = struct
+          type t = concrete_ident list
+
+          let namespaces_of : t -> Namespace.Set.t =
+            List.map ~f:Namespace.of_concrete_ident
+            >> Set.of_list (module Namespace)
+
+          let homogeneous_namespace (ns : t) : bool =
+            Set.length (namespaces_of ns) <= 1
+        end
+
+        type t = {
+          mut_rec_bundles : Bundle.t list;
+          non_mut_rec : concrete_ident list;
+        }
+
+        module SCC = Graph.Components.Make (G)
+
+        let of_graph (g : G.t) : t =
+          let is_mut_rec_with_itself x = G.mem_edge g x x in
+          let mut_rec_bundles, non_mut_rec =
+            SCC.scc_list g
+            |> List.partition_map ~f:(function
+                 | [] -> failwith "scc_list returned empty cluster"
+                 | [ x ] when is_mut_rec_with_itself x |> not -> Second x
+                 | bundle -> First bundle)
+          in
+          { mut_rec_bundles; non_mut_rec }
 
-      type t = {
-        mut_rec_bundles : Bundle.t list;
-        non_mut_rec : concrete_ident list;
-      }
+        let all_homogeneous_namespace (g : G.t) =
+          List.for_all ~f:Bundle.homogeneous_namespace
+            (of_graph g).mut_rec_bundles
+      end
 
-      module SCC = Graph.Components.Make (G)
+      module CyclicDep = struct
+        module Bundle = struct
+          type t = Concrete_ident.t list
+
+          module G = Graph.Persistent.Graph.Concrete (Ordered_concrete_ident)
+          module CC = Graph.Components.Undirected (G)
+
+          let cycles g = CC.components_list g
+        end
+
+        (* This is a solution that bundles together everything that belongs to the same module SCC.
+           It results in bundles that are much bigger than they could be but is a simple solution
+           to the problem described in https://github.com/hacspec/hax/issues/995#issuecomment-2411114404 *)
+        let of_mod_sccs (items : item list)
+            (mod_graph_cycles : Namespace.Set.t list) : Bundle.t list =
+          let item_names = List.map items ~f:(fun x -> x.ident) in
+          let cycles =
+            List.filter mod_graph_cycles ~f:(fun set ->
+                Prelude.Set.length set > 1)
+          in
+          let bundles =
+            List.map cycles ~f:(fun set ->
+                List.filter item_names ~f:(fun item ->
+                    Prelude.Set.mem set (Namespace.of_concrete_ident item)))
+          in
+          bundles
+      end
 
-      let of_graph (g : G.t) : t =
-        let is_mut_rec_with_itself x = G.mem_edge g x x in
-        let mut_rec_bundles, non_mut_rec =
-          SCC.scc_list g
-          |> List.partition_map ~f:(function
-               | [] -> failwith "scc_list returned empty cluster"
-               | [ x ] when is_mut_rec_with_itself x |> not -> Second x
-               | bundle -> First bundle)
-        in
-        { mut_rec_bundles; non_mut_rec }
+      open Graph.Graphviz.Dot (struct
+        include G
 
-      let all_homogeneous_namespace (g : G.t) =
-        List.for_all ~f:Bundle.homogeneous_namespace
-          (of_graph g).mut_rec_bundles
-    end
+        let graph_attributes _ = []
+        let default_vertex_attributes _ = []
+        let vertex_name i = "\"" ^ Concrete_ident.show i ^ "\""
 
-    module CyclicDep = struct
-      module Bundle = struct
-        type t = Concrete_ident.t list
+        let vertex_attributes i =
+          [ `Label (Concrete_ident.DefaultViewAPI.to_definition_name i) ]
 
-        module G = Graph.Persistent.Graph.Concrete (Concrete_ident)
-        module CC = Graph.Components.Undirected (G)
+        let get_subgraph i =
+          let ns = Namespace.of_concrete_ident i in
+          let sg_name = String.concat ~sep:"__" ns in
+          let label = String.concat ~sep:"::" ns in
+          let open Graph.Graphviz.DotAttributes in
+          Some { sg_name; sg_attributes = [ `Label label ]; sg_parent = None }
 
-        let cycles g = CC.components_list g
-      end
+        let default_edge_attributes _ = []
+        let edge_attributes _ = []
+      end)
 
-      (* This is a solution that bundles together everything that belongs to the same module SCC.
-         It results in bundles that are much bigger than they could be but is a simple solution
-         to the problem described in https://github.com/hacspec/hax/issues/995#issuecomment-2411114404 *)
-      let of_mod_sccs (items : item list)
-          (mod_graph_cycles : Namespace.Set.t list) : Bundle.t list =
-        let item_names = List.map items ~f:(fun x -> x.ident) in
-        let cycles =
-          List.filter mod_graph_cycles ~f:(fun set ->
-              Prelude.Set.length set > 1)
-        in
-        let bundles =
-          List.map cycles ~f:(fun set ->
-              List.filter item_names ~f:(fun item ->
-                  Prelude.Set.mem set (Namespace.of_concrete_ident item)))
-        in
-        bundles
+      let print oc items = output_graph oc (of_items items)
     end
 
-    open Graph.Graphviz.Dot (struct
-      include G
+    module ModGraph = struct
+      module G = Graph.Persistent.Digraph.Concrete (Namespace)
+
+      let of_items (items : item list) : G.t =
+        let ig = ItemGraph.of_items items in
+        List.map ~f:(ident_of >> (Namespace.of_concrete_ident &&& Fn.id)) items
+        |> Map.of_alist_multi (module Namespace)
+        |> Map.map
+             ~f:
+               (List.concat_map
+                  ~f:
+                    (ItemGraph.G.succ ig
+                    >> List.map ~f:Namespace.of_concrete_ident)
+               >> Set.of_list (module Namespace)
+               >> Set.to_list)
+        |> Map.to_alist
+        |> List.concat_map ~f:(fun (x, ys) -> List.map ~f:(fun y -> (x, y)) ys)
+        |> List.fold ~init:G.empty ~f:(G.add_edge >> uncurry)
 
-      let graph_attributes _ = []
-      let default_vertex_attributes _ = []
-      let vertex_name i = "\"" ^ Concrete_ident.show i ^ "\""
+      module SCC = Graph.Components.Make (G)
 
-      let vertex_attributes i =
-        [ `Label (Concrete_ident.DefaultViewAPI.to_definition_name i) ]
+      let cycles g : Namespace.Set.t list =
+        SCC.scc_list g |> List.map ~f:(Set.of_list (module Namespace))
 
-      let get_subgraph i =
-        let ns = Namespace.of_concrete_ident i in
-        let sg_name = String.concat ~sep:"__" ns in
-        let label = String.concat ~sep:"::" ns in
-        let open Graph.Graphviz.DotAttributes in
-        Some { sg_name; sg_attributes = [ `Label label ]; sg_parent = None }
+      open Graph.Graphviz.Dot (struct
+        include G
 
-      let default_edge_attributes _ = []
-      let edge_attributes _ = []
-    end)
+        let graph_attributes _ = []
+        let default_vertex_attributes _ = []
+        let vertex_name ns = "\"" ^ String.concat ~sep:"::" ns ^ "\""
+        let vertex_attributes _ = []
+        let get_subgraph _ = None
+        let default_edge_attributes _ = []
+        let edge_attributes _ = []
+      end)
 
-    let print oc items = output_graph oc (of_items ~original_items:items items)
-  end
+      let print oc items =
+        let g = of_items items in
+        let complicated_ones =
+          SCC.scc_list g
+          |> List.concat_map ~f:(function [] | [ _ ] -> [] | bundle -> bundle)
+        in
+        let g =
+          List.concat_map
+            ~f:(fun ns ->
+              List.map
+                ~f:(fun y -> (ns, y))
+                (G.succ g ns
+                |> List.filter
+                     ~f:(List.mem ~equal:[%equal: Namespace.t] complicated_ones)
+                ))
+            complicated_ones
+          |> List.fold ~init:G.empty ~f:(G.add_edge >> uncurry)
+        in
+        output_graph oc g
+    end
 
-  module ModGraph = struct
-    module G = Graph.Persistent.Digraph.Concrete (Namespace)
-
-    let of_items (items : item list) : G.t =
-      let ig = ItemGraph.of_items ~original_items:items items in
-      List.map ~f:(ident_of >> (Namespace.of_concrete_ident &&& Fn.id)) items
-      |> Map.of_alist_multi (module Namespace)
-      |> Map.map
-           ~f:
-             (List.concat_map
-                ~f:
-                  (ItemGraph.G.succ ig
-                  >> List.map ~f:Namespace.of_concrete_ident)
-             >> Set.of_list (module Namespace)
-             >> Set.to_list)
-      |> Map.to_alist
-      |> List.concat_map ~f:(fun (x, ys) -> List.map ~f:(fun y -> (x, y)) ys)
-      |> List.fold ~init:G.empty ~f:(G.add_edge >> uncurry)
-
-    module SCC = Graph.Components.Make (G)
-
-    let cycles g : Namespace.Set.t list =
-      SCC.scc_list g |> List.map ~f:(Set.of_list (module Namespace))
-
-    open Graph.Graphviz.Dot (struct
-      include G
-
-      let graph_attributes _ = []
-      let default_vertex_attributes _ = []
-      let vertex_name ns = "\"" ^ String.concat ~sep:"::" ns ^ "\""
-      let vertex_attributes _ = []
-      let get_subgraph _ = None
-      let default_edge_attributes _ = []
-      let edge_attributes _ = []
-    end)
-
-    let print oc items =
-      let g = of_items items in
-      let complicated_ones =
-        SCC.scc_list g
-        |> List.concat_map ~f:(function [] | [ _ ] -> [] | bundle -> bundle)
-      in
-      let g =
-        List.concat_map
-          ~f:(fun ns ->
-            List.map
-              ~f:(fun y -> (ns, y))
-              (G.succ g ns
-              |> List.filter
-                   ~f:(List.mem ~equal:[%equal: Namespace.t] complicated_ones)))
-          complicated_ones
-        |> List.fold ~init:G.empty ~f:(G.add_edge >> uncurry)
-      in
-      output_graph oc g
-  end
+    let ident_list_to_string =
+      List.map ~f:Concrete_ident.DefaultViewAPI.show >> String.concat ~sep:", "
 
-  let ident_list_to_string =
-    List.map ~f:Concrete_ident.DefaultViewAPI.show >> String.concat ~sep:", "
-
-  let sort (items : item list) : item list =
-    let g =
-      ItemGraph.of_items ~original_items:items items |> ItemGraph.Oper.mirror
-    in
-    let lookup (name : concrete_ident) =
-      List.find ~f:(ident_of >> Concrete_ident.equal name) items
-    in
-    let items' =
-      ItemGraph.Topological.fold List.cons g []
-      |> List.filter_map ~f:lookup |> List.rev
-    in
-    assert (
-      let of_list =
-        List.map ~f:ident_of >> Set.of_list (module Concrete_ident)
+    let sort (items : item list) : item list =
+      let g = ItemGraph.of_items items |> ItemGraph.Oper.mirror in
+      let lookup (name : concrete_ident) =
+        List.find ~f:(ident_of >> Concrete_ident.equal name) items
       in
-      let items = of_list items in
-      let items' = of_list items' in
-      Set.equal items items');
-    items'
-
-  let filter_by_inclusion_clauses' ~original_items
-      (clauses : Types.inclusion_clause list) (items : item list) :
-      item list * Concrete_ident.t Hash_set.t =
-    let graph = ItemGraph.of_items ~original_items items in
-    let of_list = Set.of_list (module Concrete_ident) in
-    let selection = List.map ~f:ident_of items |> of_list in
-    let deps_of =
-      let to_set = Hash_set.to_list >> of_list in
-      Set.to_list >> ItemGraph.transitive_dependencies_of graph >> to_set
-    in
-    let show_ident_set =
-      Set.to_list
-      >> List.map ~f:Concrete_ident.DefaultViewAPI.show
-      >> List.map ~f:(fun s -> " - " ^ s)
-      >> String.concat ~sep:"\n"
-    in
-    let show_inclusion_clause Types.{ kind; namespace } =
-      (match kind with
-      | Excluded -> "-"
-      | SignatureOnly -> "+:"
-      | Included deps_kind -> (
-          match deps_kind with
-          | Transitive -> "+"
-          | Shallow -> "+~"
-          | None' -> "+!"))
-      ^ "["
-      ^ (List.map
-           ~f:(function Glob One -> "*" | Glob Many -> "**" | Exact s -> s)
-           namespace.chunks
-        |> String.concat ~sep:"::")
-      ^ "]"
-    in
-    let items_drop_body = Hash_set.create (module Concrete_ident) in
-    let apply_clause selection' (clause : Types.inclusion_clause) =
-      let matches = Concrete_ident.matches_namespace clause.Types.namespace in
-      let matched0 = Set.filter ~f:matches selection in
-      let with_deps, drop_bodies =
-        match clause.kind with
-        | Included Transitive -> (true, false)
-        | Included Shallow -> (true, true)
-        | Included None' -> (false, false)
-        | SignatureOnly -> (false, true)
-        | Excluded -> (false, false)
+      let items' =
+        ItemGraph.Topological.fold List.cons g []
+        |> List.filter_map ~f:lookup |> List.rev
       in
-      let matched = matched0 |> if with_deps then deps_of else Fn.id in
-      if drop_bodies then (
-        Set.iter ~f:(Hash_set.add items_drop_body) matched;
-        Set.iter ~f:(Hash_set.remove items_drop_body) matched0);
-      Logs.info (fun m ->
-          m "The clause [%s] will %s the following Rust items:\n%s"
-            (show_inclusion_clause clause)
-            (match clause.kind with Excluded -> "remove" | _ -> "add")
-          @@ show_ident_set matched);
-      let set_op =
-        match clause.kind with
-        | Included _ | SignatureOnly -> Set.union
-        | Excluded -> Set.diff
+      assert (
+        let of_list =
+          List.map ~f:ident_of >> Set.of_list (module Concrete_ident)
+        in
+        let items = of_list items in
+        let items' = of_list items' in
+        Set.equal items items');
+      items'
+
+    let filter_by_inclusion_clauses' (clauses : Types.inclusion_clause list)
+        (items : item list) : item list * Concrete_ident.t Hash_set.t =
+      let graph = ItemGraph.of_items items in
+      let of_list = Set.of_list (module Concrete_ident) in
+      let selection = List.map ~f:ident_of items |> of_list in
+      let deps_of =
+        let to_set = Hash_set.to_list >> of_list in
+        Set.to_list >> ItemGraph.transitive_dependencies_of graph >> to_set
       in
-      let result = set_op selection' matched in
-      result
-    in
-    let selection = List.fold ~init:selection ~f:apply_clause clauses in
-    Logs.info (fun m ->
-        m "The following Rust items are going to be extracted:\n%s"
-        @@ show_ident_set selection);
-    (List.filter ~f:(ident_of >> Set.mem selection) items, items_drop_body)
-
-  let filter_by_inclusion_clauses (clauses : Types.inclusion_clause list)
-      (items : item list) : item list =
-    let f = filter_by_inclusion_clauses' ~original_items:items clauses in
-    let selection =
-      let items', items_drop_body = f items in
-      let items', _ =
-        (* when one includes only shallow dependencies, we just remove bodies *)
-        List.map
-          ~f:(fun item ->
-            if Hash_set.mem items_drop_body (ident_of item) then
-              U.Mappers.drop_bodies#visit_item () item
-            else item)
-          items'
-        |> f
+      let show_ident_set =
+        Set.to_list
+        >> List.map ~f:Concrete_ident.DefaultViewAPI.show
+        >> List.map ~f:(fun s -> " - " ^ s)
+        >> String.concat ~sep:"\n"
       in
-      List.map ~f:ident_of items' |> Set.of_list (module Concrete_ident)
-    in
-    List.filter ~f:(ident_of >> Set.mem selection) items
-
-  (* Construct the new item `f item` (say `item'`), and create a
-     "symbolic link" to `item'`. Returns a pair that consists in the
-     symbolic link and in `item'`. *)
-  let shallow_copy (f : item -> item)
-      (variants_renamings :
-        concrete_ident * concrete_ident ->
-        (concrete_ident * concrete_ident) list) (item : item) : item list =
-    let item' = f item in
-    let old_new = (ident_of item, ident_of item') in
-    let aliases =
-      List.map (old_new :: variants_renamings old_new)
-        ~f:(fun (old_ident, new_ident) ->
-          let attrs =
-            List.filter ~f:(fun att -> Attrs.late_skip [ att ]) item.attrs
-          in
-
-          { item with v = Alias { name = old_ident; item = new_ident }; attrs })
-    in
-    item' :: aliases
-
-  let bundle_cyclic_modules (items : item list) : item list =
-    let from_ident ident : item option =
-      List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items
-    in
-    let mut_rec_bundles =
-      let mod_graph_cycles = ModGraph.of_items items |> ModGraph.cycles in
-      (* `Use` items shouldn't be bundled as they have no dependencies
-          and they have dummy names. *)
-      let non_use_items =
-        List.filter
-          ~f:(fun item ->
-            match item.v with Use _ | NotImplementedYet -> false | _ -> true)
-          items
+      let show_inclusion_clause Types.{ kind; namespace } =
+        (match kind with
+        | Excluded -> "-"
+        | SignatureOnly -> "+:"
+        | Included deps_kind -> (
+            match deps_kind with
+            | Transitive -> "+"
+            | Shallow -> "+~"
+            | None' -> "+!"))
+        ^ "["
+        ^ (List.map
+             ~f:(function Glob One -> "*" | Glob Many -> "**" | Exact s -> s)
+             namespace.chunks
+          |> String.concat ~sep:"::")
+        ^ "]"
       in
-      let bundles =
-        ItemGraph.CyclicDep.of_mod_sccs non_use_items mod_graph_cycles
+      let items_drop_body = Hash_set.create (module Concrete_ident) in
+      let apply_clause selection' (clause : Types.inclusion_clause) =
+        let matches = Concrete_ident.matches_namespace clause.Types.namespace in
+        let matched0 = Set.filter ~f:matches selection in
+        let with_deps, drop_bodies =
+          match clause.kind with
+          | Included Transitive -> (true, false)
+          | Included Shallow -> (true, true)
+          | Included None' -> (false, false)
+          | SignatureOnly -> (false, true)
+          | Excluded -> (false, false)
+        in
+        let matched = matched0 |> if with_deps then deps_of else Fn.id in
+        if drop_bodies then (
+          Set.iter ~f:(Hash_set.add items_drop_body) matched;
+          Set.iter ~f:(Hash_set.remove items_drop_body) matched0);
+        Logs.info (fun m ->
+            m "The clause [%s] will %s the following Rust items:\n%s"
+              (show_inclusion_clause clause)
+              (match clause.kind with Excluded -> "remove" | _ -> "add")
+            @@ show_ident_set matched);
+        let set_op =
+          match clause.kind with
+          | Included _ | SignatureOnly -> Set.union
+          | Excluded -> Set.diff
+        in
+        let result = set_op selection' matched in
+        result
       in
-      let f = List.filter_map ~f:from_ident in
-      List.map ~f bundles
-    in
-
-    let transform (bundle : item list) =
-      let ns : Concrete_ident.t =
-        Concrete_ident.Create.fresh_module ~from:(List.map ~f:ident_of bundle)
+      let selection = List.fold ~init:selection ~f:apply_clause clauses in
+      Logs.info (fun m ->
+          m "The following Rust items are going to be extracted:\n%s"
+          @@ show_ident_set selection);
+      (List.filter ~f:(ident_of >> Set.mem selection) items, items_drop_body)
+
+    let filter_by_inclusion_clauses (clauses : Types.inclusion_clause list)
+        (items : item list) : item list =
+      let f = filter_by_inclusion_clauses' clauses in
+      let selection =
+        let items', items_drop_body = f items in
+        let items', _ =
+          (* when one includes only shallow dependencies, we just remove bodies *)
+          List.map
+            ~f:(fun item ->
+              if Hash_set.mem items_drop_body (ident_of item) then
+                U.Mappers.drop_bodies#visit_item () item
+              else item)
+            items'
+          |> f
+        in
+        List.map ~f:ident_of items' |> Set.of_list (module Concrete_ident)
       in
-      let new_name_under_ns : Concrete_ident.t -> Concrete_ident.t =
-        Concrete_ident.Create.move_under ~new_parent:ns
+      List.filter ~f:(ident_of >> Set.mem selection) items
+
+    (* Construct the new item `f item` (say `item'`), and create a
+       "symbolic link" to `item'`. Returns a pair that consists in the
+       symbolic link and in `item'`. *)
+    let shallow_copy (f : item -> item)
+        (variants_renamings :
+          concrete_ident * concrete_ident ->
+          (concrete_ident * concrete_ident) list) (item : item) : item list =
+      let item' = f item in
+      let old_new = (ident_of item, ident_of item') in
+      let aliases =
+        List.map (old_new :: variants_renamings old_new)
+          ~f:(fun (old_ident, new_ident) ->
+            let attrs =
+              List.filter ~f:(fun att -> Attrs.late_skip [ att ]) item.attrs
+            in
+
+            {
+              item with
+              v = Alias { name = old_ident; item = new_ident };
+              attrs;
+            })
       in
-      let new_names = List.map ~f:(ident_of >> new_name_under_ns) bundle in
-      let duplicates =
-        new_names |> List.find_all_dups ~compare:Concrete_ident.compare
+      item' :: aliases
+
+    let bundle_cyclic_modules (items : item list) : item list =
+      let from_ident ident : item option =
+        List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items
       in
-      (* Verify name clashes *)
-      (* In case of clash, add hash *)
-      let add_prefix id =
-        if
-          not
-            (List.mem duplicates (new_name_under_ns id)
-               ~equal:Concrete_ident.equal)
-        then id
-        else
-          Concrete_ident.Create.map_last
-            ~f:(fun name -> name ^ (Concrete_ident.hash id |> Int.to_string))
-            id
+      let mut_rec_bundles =
+        let mod_graph_cycles = ModGraph.of_items items |> ModGraph.cycles in
+        (* `Use` items shouldn't be bundled as they have no dependencies
+           and they have dummy names. *)
+        let non_use_items =
+          List.filter
+            ~f:(fun item ->
+              match item.v with Use _ | NotImplementedYet -> false | _ -> true)
+            items
+        in
+        let bundles =
+          ItemGraph.CyclicDep.of_mod_sccs non_use_items mod_graph_cycles
+        in
+        let f = List.filter_map ~f:from_ident in
+        List.map ~f bundles
       in
-      let renamings =
-        List.map
-          ~f:(ident_of >> (Fn.id &&& (add_prefix >> new_name_under_ns)))
-          bundle
+
+      let transform (bundle : item list) =
+        let ns : Concrete_ident.t =
+          Concrete_ident.Create.fresh_module ~from:(List.map ~f:ident_of bundle)
+        in
+        let new_name_under_ns : Concrete_ident.t -> Concrete_ident.t =
+          Concrete_ident.Create.move_under ~new_parent:ns
+        in
+        let new_names = List.map ~f:(ident_of >> new_name_under_ns) bundle in
+        let duplicates =
+          new_names |> List.find_all_dups ~compare:Concrete_ident.compare
+        in
+        (* Verify name clashes *)
+        (* In case of clash, add hash *)
+        let add_prefix id =
+          if
+            not
+              (List.mem duplicates (new_name_under_ns id)
+                 ~equal:Concrete_ident.equal)
+          then id
+          else
+            Concrete_ident.Create.map_last
+              ~f:(fun name -> name ^ (Concrete_ident.hash id |> Int.to_string))
+              id
+        in
+        let renamings =
+          List.map
+            ~f:(ident_of >> (Fn.id &&& (add_prefix >> new_name_under_ns)))
+            bundle
+        in
+        let variants_renamings (previous_name, new_name) =
+          match from_ident previous_name with
+          | Some { v = Type { variants; is_struct = false; _ }; _ } ->
+              List.map variants ~f:(fun { name; _ } ->
+                  ( name,
+                    Concrete_ident.Create.move_under ~new_parent:new_name name
+                  ))
+          | Some { v = Type { variants; is_struct = true; _ }; _ } ->
+              List.concat_map variants ~f:(fun { arguments; _ } ->
+                  List.map arguments ~f:(fun (name, _, _) ->
+                      ( name,
+                        Concrete_ident.Create.move_under ~new_parent:new_name
+                          name )))
+          | _ -> []
+        in
+        let variant_and_constructors_renamings =
+          List.concat_map ~f:variants_renamings renamings
+          |> List.concat_map ~f:(fun (old_name, new_name) ->
+                 [
+                   (old_name, new_name);
+                   ( Concrete_ident.Create.constructor old_name,
+                     Concrete_ident.Create.constructor new_name );
+                 ])
+        in
+        let renamings =
+          Map.of_alist_exn
+            (module Concrete_ident)
+            (renamings @ variant_and_constructors_renamings)
+        in
+        let rename =
+          let renamer _lvl i =
+            Map.find renamings i |> Option.value ~default:i
+          in
+          (U.Mappers.rename_concrete_idents renamer)#visit_item ExprLevel
+        in
+        fun it -> shallow_copy rename variants_renamings it
       in
-      let variants_renamings (previous_name, new_name) =
-        match from_ident previous_name with
-        | Some { v = Type { variants; is_struct = false; _ }; _ } ->
-            List.map variants ~f:(fun { name; _ } ->
-                ( name,
-                  Concrete_ident.Create.move_under ~new_parent:new_name name ))
-        | Some { v = Type { variants; is_struct = true; _ }; _ } ->
-            List.concat_map variants ~f:(fun { arguments; _ } ->
-                List.map arguments ~f:(fun (name, _, _) ->
-                    ( name,
-                      Concrete_ident.Create.move_under ~new_parent:new_name name
-                    )))
-        | _ -> []
+      let bundle_transforms =
+        List.concat_map mut_rec_bundles ~f:(fun bundle ->
+            let bundle_value =
+              ( List.map ~f:ident_of bundle
+                |> ItemGraph.MutRec.Bundle.homogeneous_namespace,
+                transform bundle )
+            in
+            List.map bundle ~f:(fun item -> (item, bundle_value)))
       in
-      let variant_and_constructors_renamings =
-        List.concat_map ~f:variants_renamings renamings
-        |> List.concat_map ~f:(fun (old_name, new_name) ->
-               [
-                 (old_name, new_name);
-                 ( Concrete_ident.Create.constructor old_name,
-                   Concrete_ident.Create.constructor new_name );
-               ])
+      let module ComparableItem = struct
+        module T = struct
+          type t = item [@@deriving sexp_of, compare, hash]
+        end
+
+        include T
+        include Comparable.Make (T)
+      end in
+      let bundle_of_item =
+        Hashtbl.of_alist_exn (module ComparableItem) bundle_transforms
       in
-      let renamings =
-        Map.of_alist_exn
-          (module Concrete_ident)
-          (renamings @ variant_and_constructors_renamings)
+      let maybe_transform_item item =
+        match Hashtbl.find bundle_of_item item with
+        | Some (homogeneous_bundle, transform_bundle) ->
+            if homogeneous_bundle then [ item ] else transform_bundle item
+        | None -> [ item ]
       in
-      let rename =
-        let renamer _lvl i = Map.find renamings i |> Option.value ~default:i in
-        (U.Mappers.rename_concrete_idents renamer)#visit_item ExprLevel
+      List.concat_map items ~f:maybe_transform_item
+
+    let recursive_bundles (items : item list) : item list list * item list =
+      let g = ItemGraph.of_items items in
+      let bundles = ItemGraph.MutRec.of_graph g in
+      let from_ident ident : item option =
+        List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items
       in
-      fun it -> shallow_copy rename variants_renamings it
-    in
-    let bundle_transforms =
-      List.concat_map mut_rec_bundles ~f:(fun bundle ->
-          let bundle_value =
-            ( List.map ~f:ident_of bundle
-              |> ItemGraph.MutRec.Bundle.homogeneous_namespace,
-              transform bundle )
-          in
-          List.map bundle ~f:(fun item -> (item, bundle_value)))
-    in
-    let module ComparableItem = struct
-      module T = struct
-        type t = item [@@deriving sexp_of, compare, hash]
-      end
+      let f = List.filter_map ~f:from_ident in
+      (List.map ~f bundles.mut_rec_bundles, f bundles.non_mut_rec)
+  end
 
-      include T
-      include Comparable.Make (T)
-    end in
-    let bundle_of_item =
-      Hashtbl.of_alist_exn (module ComparableItem) bundle_transforms
-    in
-    let maybe_transform_item item =
-      match Hashtbl.find bundle_of_item item with
-      | Some (homogeneous_bundle, transform_bundle) ->
-          if homogeneous_bundle then [ item ] else transform_bundle item
-      | None -> [ item ]
-    in
-    List.concat_map items ~f:maybe_transform_item
-
-  let recursive_bundles (items : item list) : item list list * item list =
-    let g = ItemGraph.of_items ~original_items:items items in
-    let bundles = ItemGraph.MutRec.of_graph g in
-    let from_ident ident : item option =
-      List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items
-    in
-    let f = List.filter_map ~f:from_ident in
-    (List.map ~f bundles.mut_rec_bundles, f bundles.non_mut_rec)
+  let uid_associated_items items' =
+    let open WithItems (struct
+      let items = items'
+    end) in
+    uid_associated_items
+
+  let bundle_cyclic_modules items' =
+    let open WithItems (struct
+      let items = items'
+    end) in
+    bundle_cyclic_modules items'
+
+  let sort items' =
+    let open WithItems (struct
+      let items = items'
+    end) in
+    sort items'
+
+  let recursive_bundles items' =
+    let open WithItems (struct
+      let items = items'
+    end) in
+    recursive_bundles items'
+
+  let filter_by_inclusion_clauses clauses items' =
+    let open WithItems (struct
+      let items = items'
+    end) in
+    filter_by_inclusion_clauses clauses items'
 end


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
index 2275da427..d45c9cb4d 100644
--- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
@@ -35,7 +35,7 @@ module Attribute_opaque
 open Core
 open FStar.Mul
 
-val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
-
 val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
+
+val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
 '''
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index e65784071..aa8b73123 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
@@ -92,6 +92,8 @@ open FStar.Mul
 
 unfold type t_Int = int
 
+unfold let add x y = x + y
+
 unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
   {
     f_Output = t_Int;
@@ -99,8 +101,6 @@ unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
     f_sub_post = (fun (self: t_Int) (other: t_Int) (out: t_Int) -> true);
     f_sub = fun (self: t_Int) (other: t_Int) -> self + other
   }
-
-unfold let add x y = x + y
 '''
 "Attributes.Nested_refinement_elim.fst" = '''
 module Attributes.Nested_refinement_elim
@@ -118,11 +118,16 @@ module Attributes.Newtype_pattern
 open Core
 open FStar.Mul
 
+let v_MAX: usize = sz 10
+
 type t_SafeIndex = { f_i:f_i: usize{f_i <. v_MAX} }
 
-let impl__SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i
+let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
+  if i <. v_MAX
+  then Core.Option.Option_Some ({ f_i = i } <: t_SafeIndex) <: Core.Option.t_Option t_SafeIndex
+  else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex
 
-let v_MAX: usize = sz 10
+let impl__SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
@@ -132,11 +137,6 @@ let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIn
     f_index_post = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) (out: v_T) -> true);
     f_index = fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> self.[ index.f_i ]
   }
-
-let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
-  if i <. v_MAX
-  then Core.Option.Option_Some ({ f_i = i } <: t_SafeIndex) <: Core.Option.t_Option t_SafeIndex
-  else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex
 '''
 "Attributes.Pre_post_on_traits_and_impls.fst" = '''
 module Attributes.Pre_post_on_traits_and_impls
@@ -162,13 +162,6 @@ class t_Operation (v_Self: Type0) = {
   f_double:x0: u8 -> Prims.Pure u8 (f_double_pre x0) (fun result -> f_double_post x0 result)
 }
 
-class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
-  f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred};
-  f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy};
-  f_method:x0: v_Self -> x1: u8
-    -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
-}
-
 type t_ViaAdd = | ViaAdd : t_ViaAdd
 
 type t_ViaMul = | ViaMul : t_ViaMul
@@ -207,6 +200,13 @@ let impl_1: t_Operation t_ViaMul =
     f_double = fun (x: u8) -> x *! 2uy
   }
 
+class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
+  f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred};
+  f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy};
+  f_method:x0: v_Self -> x1: u8
+    -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
+}
+
 let test
       (#v_T: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_TraitWithRequiresAndEnsures v_T)
@@ -247,10 +247,10 @@ module Attributes.Refined_indexes
 open Core
 open FStar.Mul
 
-type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray
-
 let v_MAX: usize = sz 10
 
+type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray
+
 /// Triple dash comment
 (** Multiline double star comment Maecenas blandit accumsan feugiat.
     Done vitae ullamcorper est.
@@ -288,27 +288,20 @@ module Attributes.Refinement_types
 open Core
 open FStar.Mul
 
-/// Example of a specific constraint on a value
-let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy}
-
 let t_BoundedU8 (v_MIN v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX}
 
-/// A field element
-let t_FieldElement = x: u16{x <=. 2347us}
+let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
+  (x <: u8) +! (y <: u8) <: t_BoundedU8 1uy 23uy
 
 /// Even `u8` numbers. Constructing pub Even values triggers static
 /// proofs in the extraction.
 let t_Even = x: u8{(x %! 2uy <: u8) =. 0uy}
 
-/// A modular mutliplicative inverse
-let t_ModInverse (v_MOD: u32) =
-  n:
-  u32
-    { (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %!
-        (cast (v_MOD <: u32) <: u128)
-        <:
-        u128) =.
-      pub_u128 1 }
+let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
+  x +! x <: t_Even
+
+let double_refine (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
+  x +! x <: t_Even
 
 /// A string that contains no space.
 let t_NoE =
@@ -330,14 +323,21 @@ let t_NoE =
       in
       ~.out }
 
-let double_refine (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
-  x +! x <: t_Even
+/// A modular mutliplicative inverse
+let t_ModInverse (v_MOD: u32) =
+  n:
+  u32
+    { (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %!
+        (cast (v_MOD <: u32) <: u128)
+        <:
+        u128) =.
+      pub_u128 1 }
 
-let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
-  (x <: u8) +! (y <: u8) <: t_BoundedU8 1uy 23uy
+/// A field element
+let t_FieldElement = x: u16{x <=. 2347us}
 
-let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
-  x +! x <: t_Even
+/// Example of a specific constraint on a value
+let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy}
 '''
 "Attributes.Requires_mut.fst" = '''
 module Attributes.Requires_mut
@@ -417,6 +417,12 @@ module Attributes.Verifcation_status
 open Core
 open FStar.Mul
 
+#push-options "--admit_smt_queries true"
+
+let a_function_which_only_laxes (_: Prims.unit) : Prims.unit = Hax_lib.v_assert false
+
+#pop-options
+
 let a_panicfree_function (_: Prims.unit)
     : Prims.Pure u8
       Prims.l_True
@@ -441,12 +447,6 @@ let another_panicfree_function (_: Prims.unit)
   let nothing:i32 = 0l in
   let still_not_much:i32 = not_much +! nothing in
   admit () (* Panic freedom *)
-
-#push-options "--admit_smt_queries true"
-
-let a_function_which_only_laxes (_: Prims.unit) : Prims.unit = Hax_lib.v_assert false
-
-#pop-options
 '''
 "Attributes.fst" = '''
 module Attributes
@@ -454,23 +454,20 @@ module Attributes
 open Core
 open FStar.Mul
 
-type t_Foo = {
-  f_x:u32;
-  f_y:f_y: u32{f_y >. 3ul};
-  f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
-}
-
-let inlined_code__V: u8 = 12uy
+let u32_max: u32 = 90000ul
 
-let issue_844_ (v__x: u8)
-    : Prims.Pure u8
-      Prims.l_True
+/// A doc comment on `add3`
+///another doc comment on add3
+let add3 (x y z: u32)
+    : Prims.Pure u32
+      (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
       (ensures
-        fun v__x_future ->
-          let v__x_future:u8 = v__x_future in
-          true) = v__x
-
-let u32_max: u32 = 90000ul
+        fun result ->
+          let result:u32 = result in
+          Hax_lib.implies true
+            (fun temp_0_ ->
+                let _:Prims.unit = temp_0_ in
+                result >. 32ul <: bool)) = (x +! y <: u32) +! z
 
 let swap_and_mut_req_ens (x y: u32)
     : Prims.Pure (u32 & u32 & u32)
@@ -485,18 +482,13 @@ let swap_and_mut_req_ens (x y: u32)
   let hax_temp_output:u32 = x +! y in
   x, y, hax_temp_output <: (u32 & u32 & u32)
 
-/// A doc comment on `add3`
-///another doc comment on add3
-let add3 (x y z: u32)
-    : Prims.Pure u32
-      (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
+let issue_844_ (v__x: u8)
+    : Prims.Pure u8
+      Prims.l_True
       (ensures
-        fun result ->
-          let result:u32 = result in
-          Hax_lib.implies true
-            (fun temp_0_ ->
-                let _:Prims.unit = temp_0_ in
-                result >. 32ul <: bool)) = (x +! y <: u32) +! z
+        fun v__x_future ->
+          let v__x_future:u8 = v__x_future in
+          true) = v__x
 
 let add3_lemma (x: u32)
     : Lemma Prims.l_True
@@ -504,6 +496,14 @@ let add3_lemma (x: u32)
         x <=. 10ul || x >=. (u32_max /! 3ul <: u32) || (add3 x x x <: u32) =. (x *! 3ul <: u32)) =
   ()
 
+type t_Foo = {
+  f_x:u32;
+  f_y:f_y: u32{f_y >. 3ul};
+  f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
+}
+
+let inlined_code__V: u8 = 12uy
+
 let before_inlined_code = "example before"
 
 let inlined_code (foo: t_Foo) : Prims.unit =
diff --git a/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap b/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap
index 6f8919b71..57b89460f 100644
--- a/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap
@@ -32,15 +32,15 @@ module Constructor_as_closure
 open Core
 open FStar.Mul
 
-type t_Context =
-  | Context_A : i32 -> t_Context
-  | Context_B : i32 -> t_Context
-
 type t_Test = | Test : i32 -> t_Test
 
 let impl__Test__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Test =
   Core.Option.impl__map #i32 #t_Test x Test
 
+type t_Context =
+  | Context_A : i32 -> t_Context
+  | Context_B : i32 -> t_Context
+
 let impl__Context__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Context =
   Core.Option.impl__map #i32 #t_Context x Context_B
 '''
diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
index af07fc045..32b65dbc7 100644
--- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
@@ -122,32 +122,32 @@ module Cyclic_modules.Enums_a
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_T240131830 as t_T}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {t_T240131830 as t_T}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_A as T_A}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T240131830_A as T_A}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_B as T_B}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T240131830_B as T_B}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_C as T_C}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T240131830_C as T_C}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_D as T_D}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T240131830_D as T_D}
 '''
-"Cyclic_modules.Enums_b.Rec_bundle_994866580.fst" = '''
-module Cyclic_modules.Enums_b.Rec_bundle_994866580
+"Cyclic_modules.Enums_b.Rec_bundle_902271266.fst" = '''
+module Cyclic_modules.Enums_b.Rec_bundle_902271266
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-type t_T366415196 =
-  | T366415196_A : t_T366415196
-  | T366415196_B : t_T366415196
-  | T366415196_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_T366415196
-
-and t_U =
+type t_U =
   | U_A : t_U
   | U_B : t_U
   | U_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_U
 
+and t_T366415196 =
+  | T366415196_A : t_T366415196
+  | T366415196_B : t_T366415196
+  | T366415196_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_T366415196
+
 and t_T240131830 =
   | T240131830_A : t_T240131830
   | T240131830_B : t_T240131830
@@ -162,23 +162,23 @@ module Cyclic_modules.Enums_b
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_T366415196 as t_T}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {t_U as t_U}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_A as T_A}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {U_A as U_A}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_B as T_B}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {U_B as U_B}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_C as T_C}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {U_C as U_C}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_U as t_U}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {t_T366415196 as t_T}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_A as U_A}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T366415196_A as T_A}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_B as U_B}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T366415196_B as T_B}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_C as U_C}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T366415196_C as T_C}
 
-include Cyclic_modules.Enums_b.Rec_bundle_994866580 {f as f}
+include Cyclic_modules.Enums_b.Rec_bundle_902271266 {f as f}
 '''
 "Cyclic_modules.Late_skip_a.fst" = '''
 module Cyclic_modules.Late_skip_a
@@ -186,10 +186,10 @@ module Cyclic_modules.Late_skip_a
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Late_skip_b.Rec_bundle_447022631 {f749016415 as f}
+include Cyclic_modules.Late_skip_b.Rec_bundle_862592093 {f749016415 as f}
 '''
-"Cyclic_modules.Late_skip_b.Rec_bundle_447022631.fst" = '''
-module Cyclic_modules.Late_skip_b.Rec_bundle_447022631
+"Cyclic_modules.Late_skip_b.Rec_bundle_862592093.fst" = '''
+module Cyclic_modules.Late_skip_b.Rec_bundle_862592093
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
@@ -205,7 +205,7 @@ module Cyclic_modules.Late_skip_b
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Late_skip_b.Rec_bundle_447022631 {f377825240 as f}
+include Cyclic_modules.Late_skip_b.Rec_bundle_862592093 {f377825240 as f}
 '''
 "Cyclic_modules.M1.fst" = '''
 module Cyclic_modules.M1
@@ -213,20 +213,20 @@ module Cyclic_modules.M1
 open Core
 open FStar.Mul
 
-include Cyclic_modules.M2.Rec_bundle_489499412 {a as a}
+include Cyclic_modules.M2.Rec_bundle_423840416 {a as a}
 '''
-"Cyclic_modules.M2.Rec_bundle_489499412.fst" = '''
-module Cyclic_modules.M2.Rec_bundle_489499412
+"Cyclic_modules.M2.Rec_bundle_423840416.fst" = '''
+module Cyclic_modules.M2.Rec_bundle_423840416
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
+let d (_: Prims.unit) : Prims.unit = ()
+
 let c (_: Prims.unit) : Prims.unit = ()
 
 let a (_: Prims.unit) : Prims.unit = c ()
 
-let d (_: Prims.unit) : Prims.unit = ()
-
 let b (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = a () in
   d ()
@@ -237,11 +237,11 @@ module Cyclic_modules.M2
 open Core
 open FStar.Mul
 
-include Cyclic_modules.M2.Rec_bundle_489499412 {c as c}
+include Cyclic_modules.M2.Rec_bundle_423840416 {d as d}
 
-include Cyclic_modules.M2.Rec_bundle_489499412 {d as d}
+include Cyclic_modules.M2.Rec_bundle_423840416 {c as c}
 
-include Cyclic_modules.M2.Rec_bundle_489499412 {b as b}
+include Cyclic_modules.M2.Rec_bundle_423840416 {b as b}
 '''
 "Cyclic_modules.Rec.fst" = '''
 module Cyclic_modules.Rec
diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap
index bfe3bcc0a..6209a1837 100644
--- a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap
+++ b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap
@@ -42,11 +42,7 @@ Import RecordSetNotations.
 
 
 
-Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 :=
-  1.
-
-Definition discriminant_EnumWithRepr_ExplicitDiscr2 : t_u16 :=
-  5.
+(* NotImplementedYet *)
 
 Inductive t_EnumWithRepr : Type :=
 | EnumWithRepr_ExplicitDiscr1
@@ -56,6 +52,12 @@ Inductive t_EnumWithRepr : Type :=
 Arguments t_EnumWithRepr:clear implicits.
 Arguments t_EnumWithRepr.
 
+Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 :=
+  1.
+
+Definition discriminant_EnumWithRepr_ExplicitDiscr2 : t_u16 :=
+  5.
+
 Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
   match x with
   | EnumWithRepr_ExplicitDiscr1 =>
@@ -68,8 +70,6 @@ Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
     t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (2)
   end.
 
-(* NotImplementedYet *)
-
 Definition f (_ : unit) : t_u32 :=
   let v__x := cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (0)) in
   t_Add_f_add (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyTuple))) (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyStruct))).
@@ -77,9 +77,9 @@ Definition f (_ : unit) : t_u32 :=
 Definition ff__CONST : t_u16 :=
   cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr1) (0)).
 
-Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 :=
-  cast (t_EnumWithRepr_cast_to_repr (x)).
-
 Definition get_repr (x : t_EnumWithRepr) : t_u16 :=
   t_EnumWithRepr_cast_to_repr (x).
+
+Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 :=
+  cast (t_EnumWithRepr_cast_to_repr (x)).
 '''
diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap
index 600085987..e9c50a747 100644
--- a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap
@@ -33,16 +33,16 @@ module Enum_repr
 open Core
 open FStar.Mul
 
-let discriminant_EnumWithRepr_ExplicitDiscr1: u16 = 1us
-
-let discriminant_EnumWithRepr_ExplicitDiscr2: u16 = 5us
-
 type t_EnumWithRepr =
   | EnumWithRepr_ExplicitDiscr1 : t_EnumWithRepr
   | EnumWithRepr_ExplicitDiscr2 : t_EnumWithRepr
   | EnumWithRepr_ImplicitDiscrEmptyTuple : t_EnumWithRepr
   | EnumWithRepr_ImplicitDiscrEmptyStruct : t_EnumWithRepr
 
+let discriminant_EnumWithRepr_ExplicitDiscr1: u16 = 1us
+
+let discriminant_EnumWithRepr_ExplicitDiscr2: u16 = 5us
+
 let t_EnumWithRepr_cast_to_repr (x: t_EnumWithRepr) : u16 =
   match x with
   | EnumWithRepr_ExplicitDiscr1  -> discriminant_EnumWithRepr_ExplicitDiscr1
@@ -64,7 +64,7 @@ let f (_: Prims.unit) : u32 =
 
 let ff__CONST: u16 = cast (discriminant_EnumWithRepr_ExplicitDiscr1 +! 0us <: u16) <: u16
 
-let get_casted_repr (x: t_EnumWithRepr) : u64 = cast (t_EnumWithRepr_cast_to_repr x <: u16) <: u64
-
 let get_repr (x: t_EnumWithRepr) : u16 = t_EnumWithRepr_cast_to_repr x
+
+let get_casted_repr (x: t_EnumWithRepr) : u64 = cast (t_EnumWithRepr_cast_to_repr x <: u16) <: u64
 '''
diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap b/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap
index d1e4e4c09..613f21e5e 100644
--- a/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap
+++ b/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap
@@ -54,15 +54,7 @@ Import choice.Choice.Exports.
 
 Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
-Equations discriminant_EnumWithRepr_ExplicitDiscr1 {L : {fset Location}} {I : Interface} : both L I int16 :=
-  discriminant_EnumWithRepr_ExplicitDiscr1  :=
-    solve_lift (ret_both (1 : int16)) : both L I int16.
-Fail Next Obligation.
-
-Equations discriminant_EnumWithRepr_ExplicitDiscr2 {L : {fset Location}} {I : Interface} : both L I int16 :=
-  discriminant_EnumWithRepr_ExplicitDiscr2  :=
-    solve_lift (ret_both (5 : int16)) : both L I int16.
-Fail Next Obligation.
+(*Not implemented yet? todo(item)*)
 
 Definition t_EnumWithRepr : choice_type :=
   ('unit ∐ 'unit ∐ 'unit ∐ 'unit).
@@ -87,6 +79,16 @@ Equations EnumWithRepr_ImplicitDiscrEmptyStruct {L : {fset Location}} {I : Inter
     solve_lift (ret_both (inr (tt : 'unit) : t_EnumWithRepr)) : both L I t_EnumWithRepr.
 Fail Next Obligation.
 
+Equations discriminant_EnumWithRepr_ExplicitDiscr1 {L : {fset Location}} {I : Interface} : both L I int16 :=
+  discriminant_EnumWithRepr_ExplicitDiscr1  :=
+    solve_lift (ret_both (1 : int16)) : both L I int16.
+Fail Next Obligation.
+
+Equations discriminant_EnumWithRepr_ExplicitDiscr2 {L : {fset Location}} {I : Interface} : both L I int16 :=
+  discriminant_EnumWithRepr_ExplicitDiscr2  :=
+    solve_lift (ret_both (5 : int16)) : both L I int16.
+Fail Next Obligation.
+
 Equations t_EnumWithRepr_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int16 :=
   t_EnumWithRepr_cast_to_repr x  :=
     matchb x with
@@ -101,8 +103,6 @@ Equations t_EnumWithRepr_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x
     end : both L1 I1 int16.
 Fail Next Obligation.
 
-(*Not implemented yet? todo(item)*)
-
 Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 int32 :=
   f _  :=
     letb v__x := cast_int (WS2 := _) (discriminant_EnumWithRepr_ExplicitDiscr2 .+ (ret_both (0 : int16))) in
@@ -114,13 +114,13 @@ Equations ff__CONST {L : {fset Location}} {I : Interface} : both L I int16 :=
     solve_lift (cast_int (WS2 := _) (discriminant_EnumWithRepr_ExplicitDiscr1 .+ (ret_both (0 : int16)))) : both L I int16.
 Fail Next Obligation.
 
-Equations get_casted_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int64 :=
-  get_casted_repr x  :=
-    solve_lift (cast_int (WS2 := _) (t_EnumWithRepr_cast_to_repr x)) : both L1 I1 int64.
-Fail Next Obligation.
-
 Equations get_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int16 :=
   get_repr x  :=
     solve_lift (t_EnumWithRepr_cast_to_repr x) : both L1 I1 int16.
 Fail Next Obligation.
+
+Equations get_casted_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int64 :=
+  get_casted_repr x  :=
+    solve_lift (cast_int (WS2 := _) (t_EnumWithRepr_cast_to_repr x)) : both L1 I1 int64.
+Fail Next Obligation.
 '''
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index fa558e443..8f3ecf5e7 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
@@ -43,26 +43,6 @@ module Generics
 open Core
 open FStar.Mul
 
-let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
-  ()
-
-type t_Bar = | Bar : t_Bar
-
-class t_Foo (v_Self: Type0) = {
-  f_const_add_pre:v_N: usize -> v_Self -> Type0;
-  f_const_add_post:v_N: usize -> v_Self -> usize -> Type0;
-  f_const_add:v_N: usize -> x0: v_Self
-    -> Prims.Pure usize (f_const_add_pre v_N x0) (fun result -> f_const_add_post v_N x0 result)
-}
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_Foo_for_usize: t_Foo usize =
-  {
-    f_const_add_pre = (fun (v_N: usize) (self: usize) -> true);
-    f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true);
-    f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
-  }
-
 let dup
       (#v_T: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T)
@@ -73,6 +53,30 @@ let dup
   <:
   (v_T & v_T)
 
+let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
+  let acc:usize = v_LEN +! sz 9 in
+  let acc:usize =
+    Rust_primitives.Hax.Folds.fold_range (sz 0)
+      v_LEN
+      (fun acc temp_1_ ->
+          let acc:usize = acc in
+          let _:usize = temp_1_ in
+          true)
+      acc
+      (fun acc i ->
+          let acc:usize = acc in
+          let i:usize = i in
+          acc +! (arr.[ i ] <: usize) <: usize)
+  in
+  acc
+
+let repeat
+      (v_LEN: usize)
+      (#v_T: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T)
+      (x: v_T)
+    : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN
+
 let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
 
 let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3
@@ -110,27 +114,23 @@ let call_g (_: Prims.unit) : usize =
     usize) +!
   sz 3
 
-let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
-  let acc:usize = v_LEN +! sz 9 in
-  let acc:usize =
-    Rust_primitives.Hax.Folds.fold_range (sz 0)
-      v_LEN
-      (fun acc temp_1_ ->
-          let acc:usize = acc in
-          let _:usize = temp_1_ in
-          true)
-      acc
-      (fun acc i ->
-          let acc:usize = acc in
-          let i:usize = i in
-          acc +! (arr.[ i ] <: usize) <: usize)
-  in
-  acc
+class t_Foo (v_Self: Type0) = {
+  f_const_add_pre:v_N: usize -> v_Self -> Type0;
+  f_const_add_post:v_N: usize -> v_Self -> usize -> Type0;
+  f_const_add:v_N: usize -> x0: v_Self
+    -> Prims.Pure usize (f_const_add_pre v_N x0) (fun result -> f_const_add_post v_N x0 result)
+}
 
-let repeat
-      (v_LEN: usize)
-      (#v_T: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T)
-      (x: v_T)
-    : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_Foo_for_usize: t_Foo usize =
+  {
+    f_const_add_pre = (fun (v_N: usize) (self: usize) -> true);
+    f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true);
+    f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
+  }
+
+type t_Bar = | Bar : t_Bar
+
+let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
+  ()
 '''
diff --git a/test-harness/src/snapshots/toolchain__guards into-coq.snap b/test-harness/src/snapshots/toolchain__guards into-coq.snap
index abd2a3274..7755eb3aa 100644
--- a/test-harness/src/snapshots/toolchain__guards into-coq.snap
+++ b/test-harness/src/snapshots/toolchain__guards into-coq.snap
@@ -43,7 +43,7 @@ Import RecordSetNotations.
 
 (* NotImplementedYet *)
 
-Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
+Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
   match x with
   | Option_None =>
     0
@@ -59,8 +59,8 @@ Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
     | _ =>
       Option_None
     end with
-    | Option_Some (y) =>
-      y
+    | Option_Some (x) =>
+      x
     | Option_None =>
       match x with
       | Option_Some (Result_Err (y)) =>
@@ -71,25 +71,7 @@ Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
     end
   end.
 
-Definition if_guard (x : t_Option ((t_i32))) : t_i32 :=
-  match match x with
-  | Option_Some (v) =>
-    match t_PartialOrd_f_gt (v) (0) with
-    | true =>
-      Option_Some (v)
-    | _ =>
-      Option_None
-    end
-  | _ =>
-    Option_None
-  end with
-  | Option_Some (x) =>
-    x
-  | Option_None =>
-    0
-  end.
-
-Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
+Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
   match x with
   | Option_None =>
     0
@@ -105,8 +87,8 @@ Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32
     | _ =>
       Option_None
     end with
-    | Option_Some (x) =>
-      x
+    | Option_Some (y) =>
+      y
     | Option_None =>
       match x with
       | Option_Some (Result_Err (y)) =>
@@ -159,4 +141,22 @@ Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i
       end
     end
   end.
+
+Definition if_guard (x : t_Option ((t_i32))) : t_i32 :=
+  match match x with
+  | Option_Some (v) =>
+    match t_PartialOrd_f_gt (v) (0) with
+    | true =>
+      Option_Some (v)
+    | _ =>
+      Option_None
+    end
+  | _ =>
+    Option_None
+  end with
+  | Option_Some (x) =>
+    x
+  | Option_None =>
+    0
+  end.
 '''
diff --git a/test-harness/src/snapshots/toolchain__guards into-fstar.snap b/test-harness/src/snapshots/toolchain__guards into-fstar.snap
index ff12f664a..d575e5eca 100644
--- a/test-harness/src/snapshots/toolchain__guards into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__guards into-fstar.snap
@@ -32,7 +32,7 @@ module Guards
 open Core
 open FStar.Mul
 
-let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
+let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
   match x with
   | Core.Option.Option_None  -> 0l
   | _ ->
@@ -44,25 +44,13 @@ let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
           | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
       | _ -> Core.Option.Option_None <: Core.Option.t_Option i32
     with
-    | Core.Option.Option_Some y -> y
+    | Core.Option.Option_Some x -> x
     | Core.Option.Option_None  ->
       match x with
       | Core.Option.Option_Some (Core.Result.Result_Err y) -> y
       | _ -> 1l
 
-let if_guard (x: Core.Option.t_Option i32) : i32 =
-  match
-    match x with
-    | Core.Option.Option_Some v ->
-      (match v >. 0l with
-        | true -> Core.Option.Option_Some v <: Core.Option.t_Option i32
-        | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
-    | _ -> Core.Option.Option_None <: Core.Option.t_Option i32
-  with
-  | Core.Option.Option_Some x -> x
-  | Core.Option.Option_None  -> 0l
-
-let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
+let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
   match x with
   | Core.Option.Option_None  -> 0l
   | _ ->
@@ -74,7 +62,7 @@ let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32
           | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
       | _ -> Core.Option.Option_None <: Core.Option.t_Option i32
     with
-    | Core.Option.Option_Some x -> x
+    | Core.Option.Option_Some y -> y
     | Core.Option.Option_None  ->
       match x with
       | Core.Option.Option_Some (Core.Result.Result_Err y) -> y
@@ -107,4 +95,16 @@ let multiple_guards (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i
         match x with
         | Core.Option.Option_Some (Core.Result.Result_Err y) -> y
         | _ -> 1l
+
+let if_guard (x: Core.Option.t_Option i32) : i32 =
+  match
+    match x with
+    | Core.Option.Option_Some v ->
+      (match v >. 0l with
+        | true -> Core.Option.Option_Some v <: Core.Option.t_Option i32
+        | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+    | _ -> Core.Option.Option_None <: Core.Option.t_Option i32
+  with
+  | Core.Option.Option_Some x -> x
+  | Core.Option.Option_None  -> 0l
 '''
diff --git a/test-harness/src/snapshots/toolchain__guards into-ssprove.snap b/test-harness/src/snapshots/toolchain__guards into-ssprove.snap
index 57b079118..a499287d3 100644
--- a/test-harness/src/snapshots/toolchain__guards into-ssprove.snap
+++ b/test-harness/src/snapshots/toolchain__guards into-ssprove.snap
@@ -55,8 +55,8 @@ Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
 (*Not implemented yet? todo(item)*)
 
-Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 :=
-  equivalent x  :=
+Equations if_let_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 :=
+  if_let_guard x  :=
     matchb x with
     | Option_None_case  =>
       solve_lift (ret_both (0 : int32))
@@ -74,9 +74,9 @@ Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_
       | _ =>
         Option_None
       end with
-      | Option_Some_case y =>
-        letb y := ret_both ((y) : (int32)) in
-        solve_lift y
+      | Option_Some_case x =>
+        letb x := ret_both ((x) : (int32)) in
+        solve_lift x
       | Option_None_case  =>
         matchb x with
         | Option_Some_case Result_Err y =>
@@ -89,30 +89,8 @@ Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_
     end : both L1 I1 int32.
 Fail Next Obligation.
 
-Equations if_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option int32)) : both L1 I1 int32 :=
-  if_guard x  :=
-    matchb matchb x with
-    | Option_Some_case v =>
-      letb v := ret_both ((v) : (int32)) in
-      matchb v >.? (ret_both (0 : int32)) with
-      | true =>
-        Option_Some (solve_lift v)
-      | _ =>
-        Option_None
-      end
-    | _ =>
-      Option_None
-    end with
-    | Option_Some_case x =>
-      letb x := ret_both ((x) : (int32)) in
-      solve_lift x
-    | Option_None_case  =>
-      solve_lift (ret_both (0 : int32))
-    end : both L1 I1 int32.
-Fail Next Obligation.
-
-Equations if_let_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 :=
-  if_let_guard x  :=
+Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 :=
+  equivalent x  :=
     matchb x with
     | Option_None_case  =>
       solve_lift (ret_both (0 : int32))
@@ -130,9 +108,9 @@ Equations if_let_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (
       | _ =>
         Option_None
       end with
-      | Option_Some_case x =>
-        letb x := ret_both ((x) : (int32)) in
-        solve_lift x
+      | Option_Some_case y =>
+        letb y := ret_both ((y) : (int32)) in
+        solve_lift y
       | Option_None_case  =>
         matchb x with
         | Option_Some_case Result_Err y =>
@@ -196,4 +174,26 @@ Equations multiple_guards {L1 : {fset Location}} {I1 : Interface} (x : both L1 I
       end
     end : both L1 I1 int32.
 Fail Next Obligation.
+
+Equations if_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option int32)) : both L1 I1 int32 :=
+  if_guard x  :=
+    matchb matchb x with
+    | Option_Some_case v =>
+      letb v := ret_both ((v) : (int32)) in
+      matchb v >.? (ret_both (0 : int32)) with
+      | true =>
+        Option_Some (solve_lift v)
+      | _ =>
+        Option_None
+      end
+    | _ =>
+      Option_None
+    end with
+    | Option_Some_case x =>
+      letb x := ret_both ((x) : (int32)) in
+      solve_lift x
+    | Option_None_case  =>
+      solve_lift (ret_both (0 : int32))
+    end : both L1 I1 int32.
+Fail Next Obligation.
 '''
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap
index c86f3b275..04abbc64e 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap
+++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap
@@ -41,6 +41,8 @@ Import RecordSetNotations.
 
 
 
+(* NotImplementedYet *)
+
 Record t_Foo : Type :=
   {
   }.
@@ -60,14 +62,24 @@ Instance t_Trait_254780795 : t_Trait ((t_Foo)) :=
   {
   }.
 
-(* NotImplementedYet *)
-
 Definition main_a_a (_ : unit) : unit :=
   tt.
 
+Definition main_b_a (_ : unit) : unit :=
+  tt.
+
+Definition main_c_a (_ : unit) : unit :=
+  tt.
+
 Definition main_a_b (_ : unit) : unit :=
   tt.
 
+Definition main_b_b (_ : unit) : unit :=
+  tt.
+
+Definition main_c_b (_ : unit) : unit :=
+  tt.
+
 Definition main_a_c (_ : unit) : unit :=
   tt.
 
@@ -77,12 +89,6 @@ Definition main_a `{v_T : Type} `{t_Sized (v_T)} `{t_Trait (v_T)} (x : v_T) : un
   let _ := main_a_c (tt) in
   tt.
 
-Definition main_b_a (_ : unit) : unit :=
-  tt.
-
-Definition main_b_b (_ : unit) : unit :=
-  tt.
-
 Definition main_b_c (_ : unit) : unit :=
   tt.
 
@@ -92,12 +98,6 @@ Definition main_b (_ : unit) : unit :=
   let _ := main_b_c (tt) in
   tt.
 
-Definition main_c_a (_ : unit) : unit :=
-  tt.
-
-Definition main_c_b (_ : unit) : unit :=
-  tt.
-
 Definition main_c_c (_ : unit) : unit :=
   tt.
 
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
index 41cd2ac28..de9402027 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
@@ -42,8 +42,16 @@ let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
 /// Indirect dependencies
 let main_a_a (_: Prims.unit) : Prims.unit = ()
 
+let main_b_a (_: Prims.unit) : Prims.unit = ()
+
+let main_c_a (_: Prims.unit) : Prims.unit = ()
+
 let main_a_b (_: Prims.unit) : Prims.unit = ()
 
+let main_b_b (_: Prims.unit) : Prims.unit = ()
+
+let main_c_b (_: Prims.unit) : Prims.unit = ()
+
 let main_a_c (_: Prims.unit) : Prims.unit = ()
 
 /// Direct dependencies
@@ -54,10 +62,6 @@ let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait
   let _:Prims.unit = main_a_c () in
   ()
 
-let main_b_a (_: Prims.unit) : Prims.unit = ()
-
-let main_b_b (_: Prims.unit) : Prims.unit = ()
-
 let main_b_c (_: Prims.unit) : Prims.unit = ()
 
 let main_b (_: Prims.unit) : Prims.unit =
@@ -66,10 +70,6 @@ let main_b (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = main_b_c () in
   ()
 
-let main_c_a (_: Prims.unit) : Prims.unit = ()
-
-let main_c_b (_: Prims.unit) : Prims.unit = ()
-
 let main_c_c (_: Prims.unit) : Prims.unit = ()
 
 let main_c (_: Prims.unit) : Prims.unit =
diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
index 9aaa938a6..7b58e61f3 100644
--- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
@@ -33,11 +33,20 @@ module Interface_only
 open Core
 open FStar.Mul
 
-type t_Bar = | Bar : t_Bar
-
-type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global }
+/// This item contains unsafe blocks and raw references, two features
+/// not supported by hax. Thanks to the `-i` flag and the `+:`
+/// modifier, `f` is still extractable as an interface.
+/// Expressions within type are still extracted, as well as pre- and
+/// post-conditions.
+val f (x: u8)
+    : Prims.Pure (t_Array u8 (sz 4))
+      (requires x <. 254uy)
+      (ensures
+        fun r ->
+          let r:t_Array u8 (sz 4) = r in
+          (r.[ sz 0 ] <: u8) >. x)
 
-type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
+type t_Bar = | Bar : t_Bar
 
 /// Non-inherent implementations are extracted, their bodies are not
 /// dropped. This might be a bit surprising: see
@@ -51,22 +60,13 @@ val impl_1:Core.Convert.t_From t_Bar u8
 
 val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
 
+type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global }
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_2 (#v_T: Type0) : Core.Convert.t_From (t_Holder v_T) Prims.unit
 
+type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_Param v_SIZE) Prims.unit
-
-/// This item contains unsafe blocks and raw references, two features
-/// not supported by hax. Thanks to the `-i` flag and the `+:`
-/// modifier, `f` is still extractable as an interface.
-/// Expressions within type are still extracted, as well as pre- and
-/// post-conditions.
-val f (x: u8)
-    : Prims.Pure (t_Array u8 (sz 4))
-      (requires x <. 254uy)
-      (ensures
-        fun r ->
-          let r:t_Array u8 (sz 4) = r in
-          (r.[ sz 0 ] <: u8) >. x)
 '''
diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
index 77d4150c3..f0b5dc23a 100644
--- a/test-harness/src/snapshots/toolchain__literals into-coq.snap
+++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap
@@ -42,39 +42,10 @@ Import RecordSetNotations.
 
 
 
-From Literals Require Import Hax_lib (t_int).
-Export Hax_lib (t_int).
-
-Record t_Foo : Type :=
-  {
-    f_field : t_u8;
-  }.
-Arguments t_Foo:clear implicits.
-Arguments t_Foo.
-Arguments Build_t_Foo.
-#[export] Instance settable_t_Foo : Settable _ :=
-  settable! (@Build_t_Foo) <f_field>.
-
 (* NotImplementedYet *)
 
-Definition v_CONSTANT : t_Foo :=
-  Build_t_Foo (3).
-
-Definition casts (x8 : t_u8) (x16 : t_u16) (x32 : t_u32) (x64 : t_u64) (xs : t_usize) : unit :=
-  let _ : t_u64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (x64)) (cast (xs)) in
-  let _ : t_u32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (x32)) (cast (x64))) (cast (xs)) in
-  let _ : t_u16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (x16)) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_u8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (x8) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_i64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_i32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_i16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_i8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  tt.
-
-Definition fn_pointer_cast (_ : unit) : unit :=
-  let f : t_u32 -> t_u32 := fun x =>
-    x in
-  tt.
+From Literals Require Import Hax_lib (t_int).
+Export Hax_lib (t_int).
 
 Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_str ("0"%string))) (f_lt (x) (impl__Int___unsafe_from_str ("16"%string))) = true} : t_u8 :=
   let _ : t_Int := f_lift (3) in
@@ -100,6 +71,22 @@ Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_s
   let _ : t_usize := impl__Int__to_usize (x) in
   impl__Int__to_u8 (f_add (x) (f_mul (x) (x))).
 
+Definition panic_with_msg (_ : unit) : unit :=
+  never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))).
+
+Record t_Foo : Type :=
+  {
+    f_field : t_u8;
+  }.
+Arguments t_Foo:clear implicits.
+Arguments t_Foo.
+Arguments Build_t_Foo.
+#[export] Instance settable_t_Foo : Settable _ :=
+  settable! (@Build_t_Foo) <f_field>.
+
+Definition v_CONSTANT : t_Foo :=
+  Build_t_Foo (3).
+
 Definition numeric (_ : unit) : unit :=
   let _ : t_usize := 123 in
   let _ : t_isize := -42 in
@@ -129,10 +116,23 @@ Definition patterns (_ : unit) : unit :=
   end in
   tt.
 
-Definition panic_with_msg (_ : unit) : unit :=
-  never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))).
+Definition casts (x8 : t_u8) (x16 : t_u16) (x32 : t_u32) (x64 : t_u64) (xs : t_usize) : unit :=
+  let _ : t_u64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (x64)) (cast (xs)) in
+  let _ : t_u32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (x32)) (cast (x64))) (cast (xs)) in
+  let _ : t_u16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (x16)) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_u8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (x8) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  tt.
 
 Definition empty_array (_ : unit) : unit :=
   let _ : t_Slice t_u8 := unsize ([]) in
   tt.
+
+Definition fn_pointer_cast (_ : unit) : unit :=
+  let f : t_u32 -> t_u32 := fun x =>
+    x in
+  tt.
 '''
diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
index f6c262b10..60e23edb4 100644
--- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
@@ -33,10 +33,86 @@ module Literals
 open Core
 open FStar.Mul
 
+let math_integers (x: Hax_lib.Int.t_Int)
+    : Prims.Pure u8
+      (requires x > (0 <: Hax_lib.Int.t_Int) && x < (16 <: Hax_lib.Int.t_Int))
+      (fun _ -> Prims.l_True) =
+  let (_: Hax_lib.Int.t_Int):Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (sz 3) in
+  let _:bool =
+    ((-340282366920938463463374607431768211455000) <: Hax_lib.Int.t_Int) >
+    (340282366920938463463374607431768211455000 <: Hax_lib.Int.t_Int)
+  in
+  let _:bool = x < x in
+  let _:bool = x >= x in
+  let _:bool = x <= x in
+  let _:bool = x <> x in
+  let _:bool = x = x in
+  let _:Hax_lib.Int.t_Int = x + x in
+  let _:Hax_lib.Int.t_Int = x - x in
+  let _:Hax_lib.Int.t_Int = x * x in
+  let _:Hax_lib.Int.t_Int = x / x in
+  let (_: i16):i16 = Hax_lib.Int.impl__Int__to_i16 x in
+  let (_: i32):i32 = Hax_lib.Int.impl__Int__to_i32 x in
+  let (_: i64):i64 = Hax_lib.Int.impl__Int__to_i64 x in
+  let (_: i128):i128 = Hax_lib.Int.impl__Int__to_i128 x in
+  let (_: isize):isize = Hax_lib.Int.impl__Int__to_isize x in
+  let (_: u16):u16 = Hax_lib.Int.impl__Int__to_u16 x in
+  let (_: u32):u32 = Hax_lib.Int.impl__Int__to_u32 x in
+  let (_: u64):u64 = Hax_lib.Int.impl__Int__to_u64 x in
+  let (_: u128):u128 = Hax_lib.Int.impl__Int__to_u128 x in
+  let (_: usize):usize = Hax_lib.Int.impl__Int__to_usize x in
+  Hax_lib.Int.impl__Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int)
+
+let panic_with_msg (_: Prims.unit) : Prims.unit =
+  Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (sz 1)
+            (let list = ["with msg"] in
+              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+              Rust_primitives.Hax.array_of_list 1 list)
+          <:
+          Core.Fmt.t_Arguments)
+      <:
+      Rust_primitives.Hax.t_Never)
+
 type t_Foo = { f_field:u8 }
 
 let v_CONSTANT: t_Foo = { f_field = 3uy } <: t_Foo
 
+let numeric (_: Prims.unit) : Prims.unit =
+  let (_: usize):usize = sz 123 in
+  let (_: isize):isize = isz (-42) in
+  let (_: isize):isize = isz 42 in
+  let (_: i32):i32 = (-42l) in
+  let (_: u128):u128 = pub_u128 22222222222222222222 in
+  ()
+
+let patterns (_: Prims.unit) : Prims.unit =
+  let _:Prims.unit =
+    match 1uy with
+    | 2uy -> () <: Prims.unit
+    | _ -> () <: Prims.unit
+  in
+  let _:Prims.unit =
+    match
+      "hello",
+      (123l,
+        (let list = ["a"; "b"] in
+          FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+          Rust_primitives.Hax.array_of_list 2 list)
+        <:
+        (i32 & t_Array string (sz 2)))
+      <:
+      (string & (i32 & t_Array string (sz 2)))
+    with
+    | "hello", (123l, v__todo) -> () <: Prims.unit
+    | _ -> () <: Prims.unit
+  in
+  let _:Prims.unit =
+    match { f_field = 4uy } <: t_Foo with
+    | { f_field = 3uy } -> () <: Prims.unit
+    | _ -> () <: Prims.unit
+  in
+  ()
+
 let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
   let (_: u64):u64 =
     ((((cast (x8 <: u8) <: u64) +! (cast (x16 <: u16) <: u64) <: u64) +! (cast (x32 <: u32) <: u64)
@@ -106,87 +182,6 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
   in
   ()
 
-/// https://github.com/hacspec/hax/issues/500
-let fn_pointer_cast (_: Prims.unit) : Prims.unit =
-  let (f: (u32 -> u32)): u32 -> u32 = fun x -> x in
-  ()
-
-let math_integers (x: Hax_lib.Int.t_Int)
-    : Prims.Pure u8
-      (requires x > (0 <: Hax_lib.Int.t_Int) && x < (16 <: Hax_lib.Int.t_Int))
-      (fun _ -> Prims.l_True) =
-  let (_: Hax_lib.Int.t_Int):Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (sz 3) in
-  let _:bool =
-    ((-340282366920938463463374607431768211455000) <: Hax_lib.Int.t_Int) >
-    (340282366920938463463374607431768211455000 <: Hax_lib.Int.t_Int)
-  in
-  let _:bool = x < x in
-  let _:bool = x >= x in
-  let _:bool = x <= x in
-  let _:bool = x <> x in
-  let _:bool = x = x in
-  let _:Hax_lib.Int.t_Int = x + x in
-  let _:Hax_lib.Int.t_Int = x - x in
-  let _:Hax_lib.Int.t_Int = x * x in
-  let _:Hax_lib.Int.t_Int = x / x in
-  let (_: i16):i16 = Hax_lib.Int.impl__Int__to_i16 x in
-  let (_: i32):i32 = Hax_lib.Int.impl__Int__to_i32 x in
-  let (_: i64):i64 = Hax_lib.Int.impl__Int__to_i64 x in
-  let (_: i128):i128 = Hax_lib.Int.impl__Int__to_i128 x in
-  let (_: isize):isize = Hax_lib.Int.impl__Int__to_isize x in
-  let (_: u16):u16 = Hax_lib.Int.impl__Int__to_u16 x in
-  let (_: u32):u32 = Hax_lib.Int.impl__Int__to_u32 x in
-  let (_: u64):u64 = Hax_lib.Int.impl__Int__to_u64 x in
-  let (_: u128):u128 = Hax_lib.Int.impl__Int__to_u128 x in
-  let (_: usize):usize = Hax_lib.Int.impl__Int__to_usize x in
-  Hax_lib.Int.impl__Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int)
-
-let numeric (_: Prims.unit) : Prims.unit =
-  let (_: usize):usize = sz 123 in
-  let (_: isize):isize = isz (-42) in
-  let (_: isize):isize = isz 42 in
-  let (_: i32):i32 = (-42l) in
-  let (_: u128):u128 = pub_u128 22222222222222222222 in
-  ()
-
-let patterns (_: Prims.unit) : Prims.unit =
-  let _:Prims.unit =
-    match 1uy with
-    | 2uy -> () <: Prims.unit
-    | _ -> () <: Prims.unit
-  in
-  let _:Prims.unit =
-    match
-      "hello",
-      (123l,
-        (let list = ["a"; "b"] in
-          FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
-          Rust_primitives.Hax.array_of_list 2 list)
-        <:
-        (i32 & t_Array string (sz 2)))
-      <:
-      (string & (i32 & t_Array string (sz 2)))
-    with
-    | "hello", (123l, v__todo) -> () <: Prims.unit
-    | _ -> () <: Prims.unit
-  in
-  let _:Prims.unit =
-    match { f_field = 4uy } <: t_Foo with
-    | { f_field = 3uy } -> () <: Prims.unit
-    | _ -> () <: Prims.unit
-  in
-  ()
-
-let panic_with_msg (_: Prims.unit) : Prims.unit =
-  Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (sz 1)
-            (let list = ["with msg"] in
-              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-              Rust_primitives.Hax.array_of_list 1 list)
-          <:
-          Core.Fmt.t_Arguments)
-      <:
-      Rust_primitives.Hax.t_Never)
-
 let empty_array (_: Prims.unit) : Prims.unit =
   let (_: t_Slice u8):t_Slice u8 =
     (let list:Prims.list u8 = [] in
@@ -196,4 +191,9 @@ let empty_array (_: Prims.unit) : Prims.unit =
     t_Slice u8
   in
   ()
+
+/// https://github.com/hacspec/hax/issues/500
+let fn_pointer_cast (_: Prims.unit) : Prims.unit =
+  let (f: (u32 -> u32)): u32 -> u32 = fun x -> x in
+  ()
 '''
diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
index 2c35945ca..ab5457375 100644
--- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
@@ -33,80 +33,6 @@ module Loops.Control_flow
 open Core
 open FStar.Mul
 
-type t_M = { f_m:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
-
-let impl__M__decoded_message (self: t_M)
-    : Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-  match
-    Rust_primitives.Hax.Folds.fold_range_return (sz 0)
-      (Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global self.f_m <: usize)
-      (fun temp_0_ temp_1_ ->
-          let _:Prims.unit = temp_0_ in
-          let _:usize = temp_1_ in
-          true)
-      ()
-      (fun temp_0_ i ->
-          let _:Prims.unit = temp_0_ in
-          let i:usize = i in
-          if i >. sz 5 <: bool
-          then
-            Core.Ops.Control_flow.ControlFlow_Break
-            (Core.Ops.Control_flow.ControlFlow_Break
-              (Core.Option.Option_None
-                <:
-                Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-              <:
-              Core.Ops.Control_flow.t_ControlFlow
-                (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-                (Prims.unit & Prims.unit))
-            <:
-            Core.Ops.Control_flow.t_ControlFlow
-              (Core.Ops.Control_flow.t_ControlFlow
-                  (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-                  (Prims.unit & Prims.unit)) Prims.unit
-          else
-            Core.Ops.Control_flow.ControlFlow_Continue ()
-            <:
-            Core.Ops.Control_flow.t_ControlFlow
-              (Core.Ops.Control_flow.t_ControlFlow
-                  (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-                  (Prims.unit & Prims.unit)) Prims.unit)
-  with
-  | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
-  | Core.Ops.Control_flow.ControlFlow_Continue _ ->
-    Core.Option.Option_Some
-    (Core.Clone.f_clone #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-        #FStar.Tactics.Typeclasses.solve
-        self.f_m)
-    <:
-    Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-
-let bigger_power_2_ (x: i32) : i32 =
-  let pow:i32 = 1l in
-  Rust_primitives.f_while_loop_cf (fun pow ->
-        let pow:i32 = pow in
-        pow <. 1000000l <: bool)
-    pow
-    (fun pow ->
-        let pow:i32 = pow in
-        let pow:i32 = pow *! 2l in
-        if pow <. x
-        then
-          let pow:i32 = pow *! 3l in
-          if true
-          then
-            Core.Ops.Control_flow.ControlFlow_Break ((), pow <: (Prims.unit & i32))
-            <:
-            Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32
-          else
-            Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l)
-            <:
-            Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32
-        else
-          Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l)
-          <:
-          Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32)
-
 let double_sum (_: Prims.unit) : i32 =
   let sum:i32 = 0l in
   let sum:i32 =
@@ -160,6 +86,36 @@ let double_sum2 (_: Prims.unit) : i32 =
   in
   sum +! sum2
 
+let double_sum_return (v: t_Slice i32) : i32 =
+  let sum:i32 = 0l in
+  match
+    Rust_primitives.Hax.f_fold_return (Core.Iter.Traits.Collect.f_into_iter #(t_Slice i32)
+          #FStar.Tactics.Typeclasses.solve
+          v
+        <:
+        Core.Slice.Iter.t_Iter i32)
+      sum
+      (fun sum i ->
+          let sum:i32 = sum in
+          let i:i32 = i in
+          if i <. 0l <: bool
+          then
+            Core.Ops.Control_flow.ControlFlow_Break
+            (Core.Ops.Control_flow.ControlFlow_Break 0l
+              <:
+              Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32))
+            <:
+            Core.Ops.Control_flow.t_ControlFlow
+              (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32
+          else
+            Core.Ops.Control_flow.ControlFlow_Continue (sum +! i <: i32)
+            <:
+            Core.Ops.Control_flow.t_ControlFlow
+              (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32)
+  with
+  | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
+  | Core.Ops.Control_flow.ControlFlow_Continue sum -> sum *! 2l
+
 let double_sum2_return (v: t_Slice i32) : i32 =
   let sum:i32 = 0l in
   let sum2:i32 = 0l in
@@ -192,35 +148,79 @@ let double_sum2_return (v: t_Slice i32) : i32 =
   | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
   | Core.Ops.Control_flow.ControlFlow_Continue (sum, sum2) -> sum +! sum2
 
-let double_sum_return (v: t_Slice i32) : i32 =
-  let sum:i32 = 0l in
+let bigger_power_2_ (x: i32) : i32 =
+  let pow:i32 = 1l in
+  Rust_primitives.f_while_loop_cf (fun pow ->
+        let pow:i32 = pow in
+        pow <. 1000000l <: bool)
+    pow
+    (fun pow ->
+        let pow:i32 = pow in
+        let pow:i32 = pow *! 2l in
+        if pow <. x
+        then
+          let pow:i32 = pow *! 3l in
+          if true
+          then
+            Core.Ops.Control_flow.ControlFlow_Break ((), pow <: (Prims.unit & i32))
+            <:
+            Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32
+          else
+            Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l)
+            <:
+            Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32
+        else
+          Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l)
+          <:
+          Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32)
+
+type t_M = { f_m:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
+
+let impl__M__decoded_message (self: t_M)
+    : Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
   match
-    Rust_primitives.Hax.f_fold_return (Core.Iter.Traits.Collect.f_into_iter #(t_Slice i32)
-          #FStar.Tactics.Typeclasses.solve
-          v
-        <:
-        Core.Slice.Iter.t_Iter i32)
-      sum
-      (fun sum i ->
-          let sum:i32 = sum in
-          let i:i32 = i in
-          if i <. 0l <: bool
+    Rust_primitives.Hax.Folds.fold_range_return (sz 0)
+      (Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global self.f_m <: usize)
+      (fun temp_0_ temp_1_ ->
+          let _:Prims.unit = temp_0_ in
+          let _:usize = temp_1_ in
+          true)
+      ()
+      (fun temp_0_ i ->
+          let _:Prims.unit = temp_0_ in
+          let i:usize = i in
+          if i >. sz 5 <: bool
           then
             Core.Ops.Control_flow.ControlFlow_Break
-            (Core.Ops.Control_flow.ControlFlow_Break 0l
+            (Core.Ops.Control_flow.ControlFlow_Break
+              (Core.Option.Option_None
+                <:
+                Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
               <:
-              Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32))
+              Core.Ops.Control_flow.t_ControlFlow
+                (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
+                (Prims.unit & Prims.unit))
             <:
             Core.Ops.Control_flow.t_ControlFlow
-              (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32
+              (Core.Ops.Control_flow.t_ControlFlow
+                  (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
+                  (Prims.unit & Prims.unit)) Prims.unit
           else
-            Core.Ops.Control_flow.ControlFlow_Continue (sum +! i <: i32)
+            Core.Ops.Control_flow.ControlFlow_Continue ()
             <:
             Core.Ops.Control_flow.t_ControlFlow
-              (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32)
+              (Core.Ops.Control_flow.t_ControlFlow
+                  (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
+                  (Prims.unit & Prims.unit)) Prims.unit)
   with
   | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
-  | Core.Ops.Control_flow.ControlFlow_Continue sum -> sum *! 2l
+  | Core.Ops.Control_flow.ControlFlow_Continue _ ->
+    Core.Option.Option_Some
+    (Core.Clone.f_clone #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+        #FStar.Tactics.Typeclasses.solve
+        self.f_m)
+    <:
+    Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
 
 let nested (_: Prims.unit) : i32 =
   let sum:i32 = 0l in
@@ -324,7 +324,94 @@ module Loops.For_loops
 open Core
 open FStar.Mul
 
-let bool_returning (x: u8) : bool = x <. 10uy
+let range1 (_: Prims.unit) : usize =
+  let acc:usize = sz 0 in
+  let acc:usize =
+    Rust_primitives.Hax.Folds.fold_range (sz 0)
+      (sz 15)
+      (fun acc temp_1_ ->
+          let acc:usize = acc in
+          let _:usize = temp_1_ in
+          true)
+      acc
+      (fun acc i ->
+          let acc:usize = acc in
+          let i:usize = i in
+          acc +! i <: usize)
+  in
+  acc
+
+let range2 (n: usize) : usize =
+  let acc:usize = sz 0 in
+  let acc:usize =
+    Rust_primitives.Hax.Folds.fold_range (sz 0)
+      (n +! sz 10 <: usize)
+      (fun acc temp_1_ ->
+          let acc:usize = acc in
+          let _:usize = temp_1_ in
+          true)
+      acc
+      (fun acc i ->
+          let acc:usize = acc in
+          let i:usize = i in
+          (acc +! i <: usize) +! sz 1 <: usize)
+  in
+  acc
+
+let composed_range (n: usize) : usize =
+  let acc:usize = sz 0 in
+  let acc:usize =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain
+              (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize))
+          #FStar.Tactics.Typeclasses.solve
+          (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize)
+              #FStar.Tactics.Typeclasses.solve
+              #(Core.Ops.Range.t_Range usize)
+              ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
+                <:
+                Core.Ops.Range.t_Range usize)
+              ({
+                  Core.Ops.Range.f_start = n +! sz 10 <: usize;
+                  Core.Ops.Range.f_end = n +! sz 50 <: usize
+                }
+                <:
+                Core.Ops.Range.t_Range usize)
+            <:
+            Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize)
+              (Core.Ops.Range.t_Range usize))
+        <:
+        Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize)
+          (Core.Ops.Range.t_Range usize))
+      acc
+      (fun acc i ->
+          let acc:usize = acc in
+          let i:usize = i in
+          (acc +! i <: usize) +! sz 1 <: usize)
+  in
+  acc
+
+let rev_range (n: usize) : usize =
+  let acc:usize = sz 0 in
+  let acc:usize =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
+            (Core.Ops.Range.t_Range usize))
+          #FStar.Tactics.Typeclasses.solve
+          (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
+              #FStar.Tactics.Typeclasses.solve
+              ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
+                <:
+                Core.Ops.Range.t_Range usize)
+            <:
+            Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize))
+        <:
+        Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize))
+      acc
+      (fun acc i ->
+          let acc:usize = acc in
+          let i:usize = i in
+          (acc +! i <: usize) +! sz 1 <: usize)
+  in
+  acc
 
 let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
@@ -382,94 +469,6 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
   in
   acc
 
-let composed_range (n: usize) : usize =
-  let acc:usize = sz 0 in
-  let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain
-              (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize))
-          #FStar.Tactics.Typeclasses.solve
-          (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize)
-              #FStar.Tactics.Typeclasses.solve
-              #(Core.Ops.Range.t_Range usize)
-              ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
-                <:
-                Core.Ops.Range.t_Range usize)
-              ({
-                  Core.Ops.Range.f_start = n +! sz 10 <: usize;
-                  Core.Ops.Range.f_end = n +! sz 50 <: usize
-                }
-                <:
-                Core.Ops.Range.t_Range usize)
-            <:
-            Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize)
-              (Core.Ops.Range.t_Range usize))
-        <:
-        Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize)
-          (Core.Ops.Range.t_Range usize))
-      acc
-      (fun acc i ->
-          let acc:usize = acc in
-          let i:usize = i in
-          (acc +! i <: usize) +! sz 1 <: usize)
-  in
-  acc
-
-let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
-  let acc:usize = sz 0 in
-  let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
-            (Core.Slice.Iter.t_Chunks usize))
-          #FStar.Tactics.Typeclasses.solve
-          (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize)
-              #FStar.Tactics.Typeclasses.solve
-              (Core.Slice.impl__chunks #usize
-                  (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
-                      #FStar.Tactics.Typeclasses.solve
-                      arr
-                    <:
-                    t_Slice usize)
-                  (sz 4)
-                <:
-                Core.Slice.Iter.t_Chunks usize)
-            <:
-            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize))
-        <:
-        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize))
-      acc
-      (fun acc temp_1_ ->
-          let acc:usize = acc in
-          let i, chunk:(usize & t_Slice usize) = temp_1_ in
-          Rust_primitives.Hax.Folds.fold_enumerated_slice chunk
-            (fun acc temp_1_ ->
-                let acc:usize = acc in
-                let _:usize = temp_1_ in
-                true)
-            acc
-            (fun acc temp_1_ ->
-                let acc:usize = acc in
-                let j, x:(usize & usize) = temp_1_ in
-                (i +! j <: usize) +! x <: usize)
-          <:
-          usize)
-  in
-  acc
-
-let f (_: Prims.unit) : u8 =
-  let acc:u8 = 0uy in
-  Rust_primitives.Hax.Folds.fold_range 1uy
-    10uy
-    (fun acc temp_1_ ->
-        let acc:u8 = acc in
-        let _:u8 = temp_1_ in
-        true)
-    acc
-    (fun acc i ->
-        let acc:u8 = acc in
-        let i:u8 = i in
-        let acc:u8 = acc +! i in
-        let _:bool = bool_returning i in
-        acc)
-
 let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
@@ -581,62 +580,63 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize
   in
   acc
 
-let range1 (_: Prims.unit) : usize =
-  let acc:usize = sz 0 in
-  let acc:usize =
-    Rust_primitives.Hax.Folds.fold_range (sz 0)
-      (sz 15)
-      (fun acc temp_1_ ->
-          let acc:usize = acc in
-          let _:usize = temp_1_ in
-          true)
-      acc
-      (fun acc i ->
-          let acc:usize = acc in
-          let i:usize = i in
-          acc +! i <: usize)
-  in
-  acc
-
-let range2 (n: usize) : usize =
-  let acc:usize = sz 0 in
-  let acc:usize =
-    Rust_primitives.Hax.Folds.fold_range (sz 0)
-      (n +! sz 10 <: usize)
-      (fun acc temp_1_ ->
-          let acc:usize = acc in
-          let _:usize = temp_1_ in
-          true)
-      acc
-      (fun acc i ->
-          let acc:usize = acc in
-          let i:usize = i in
-          (acc +! i <: usize) +! sz 1 <: usize)
-  in
-  acc
-
-let rev_range (n: usize) : usize =
+let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
-            (Core.Ops.Range.t_Range usize))
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
+            (Core.Slice.Iter.t_Chunks usize))
           #FStar.Tactics.Typeclasses.solve
-          (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
+          (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize)
               #FStar.Tactics.Typeclasses.solve
-              ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
+              (Core.Slice.impl__chunks #usize
+                  (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
+                      #FStar.Tactics.Typeclasses.solve
+                      arr
+                    <:
+                    t_Slice usize)
+                  (sz 4)
                 <:
-                Core.Ops.Range.t_Range usize)
+                Core.Slice.Iter.t_Chunks usize)
             <:
-            Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize))
+            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize))
         <:
-        Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize))
+        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize))
       acc
-      (fun acc i ->
+      (fun acc temp_1_ ->
           let acc:usize = acc in
-          let i:usize = i in
-          (acc +! i <: usize) +! sz 1 <: usize)
+          let i, chunk:(usize & t_Slice usize) = temp_1_ in
+          Rust_primitives.Hax.Folds.fold_enumerated_slice chunk
+            (fun acc temp_1_ ->
+                let acc:usize = acc in
+                let _:usize = temp_1_ in
+                true)
+            acc
+            (fun acc temp_1_ ->
+                let acc:usize = acc in
+                let j, x:(usize & usize) = temp_1_ in
+                (i +! j <: usize) +! x <: usize)
+          <:
+          usize)
   in
   acc
+
+let bool_returning (x: u8) : bool = x <. 10uy
+
+let f (_: Prims.unit) : u8 =
+  let acc:u8 = 0uy in
+  Rust_primitives.Hax.Folds.fold_range 1uy
+    10uy
+    (fun acc temp_1_ ->
+        let acc:u8 = acc in
+        let _:u8 = temp_1_ in
+        true)
+    acc
+    (fun acc i ->
+        let acc:u8 = acc in
+        let i:u8 = i in
+        let acc:u8 = acc +! i in
+        let _:bool = bool_returning i in
+        acc)
 '''
 "Loops.Recognized_loops.fst" = '''
 module Loops.Recognized_loops
@@ -644,64 +644,64 @@ module Loops.Recognized_loops
 open Core
 open FStar.Mul
 
-let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 =
+let range (_: Prims.unit) : u64 =
   let count:u64 = 0uL in
-  Rust_primitives.Hax.Folds.fold_enumerated_chunked_slice (sz 3)
-    slice
+  Rust_primitives.Hax.Folds.fold_range 0uy
+    10uy
     (fun count i ->
         let count:u64 = count in
-        let i:usize = i in
-        i <= Core.Slice.impl__len #v_T slice)
+        let i:u8 = i in
+        i <=. 10uy <: bool)
     count
     (fun count i ->
         let count:u64 = count in
-        let i:(usize & t_Slice v_T) = i in
-        let count:u64 = count +! 3uL in
+        let i:u8 = i in
+        let count:u64 = count +! 1uL in
         count)
 
-let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 =
+let range_step_by (_: Prims.unit) : u64 =
   let count:u64 = 0uL in
-  Rust_primitives.Hax.Folds.fold_enumerated_slice slice
+  Rust_primitives.Hax.Folds.fold_range_step_by 0uy
+    10uy
+    (sz 2)
     (fun count i ->
         let count:u64 = count in
-        let i:usize = i in
-        i <=. sz 10 <: bool)
+        let i:u8 = i in
+        i <=. 10uy <: bool)
     count
     (fun count i ->
         let count:u64 = count in
-        let i:(usize & v_T) = i in
-        let count:u64 = count +! 2uL in
+        let i:u8 = i in
+        let count:u64 = count +! 1uL in
         count)
 
-let range (_: Prims.unit) : u64 =
+let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 =
   let count:u64 = 0uL in
-  Rust_primitives.Hax.Folds.fold_range 0uy
-    10uy
+  Rust_primitives.Hax.Folds.fold_enumerated_slice slice
     (fun count i ->
         let count:u64 = count in
-        let i:u8 = i in
-        i <=. 10uy <: bool)
+        let i:usize = i in
+        i <=. sz 10 <: bool)
     count
     (fun count i ->
         let count:u64 = count in
-        let i:u8 = i in
-        let count:u64 = count +! 1uL in
+        let i:(usize & v_T) = i in
+        let count:u64 = count +! 2uL in
         count)
 
-let range_step_by (_: Prims.unit) : u64 =
+let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 =
   let count:u64 = 0uL in
-  Rust_primitives.Hax.Folds.fold_range_step_by 0uy
-    10uy
-    (sz 2)
+  Rust_primitives.Hax.Folds.fold_enumerated_chunked_slice (sz 3)
+    slice
     (fun count i ->
         let count:u64 = count in
-        let i:u8 = i in
-        i <=. 10uy <: bool)
+        let i:usize = i in
+        i <= Core.Slice.impl__len #v_T slice)
     count
     (fun count i ->
         let count:u64 = count in
-        let i:u8 = i in
-        let count:u64 = count +! 1uL in
+        let i:(usize & t_Slice v_T) = i in
+        let count:u64 = count +! 3uL in
         count)
 '''
 "Loops.While_loops.fst" = '''
diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
index fee5eaadb..f1ffe9f82 100644
--- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
@@ -32,102 +32,8 @@ module Mut_ref_functionalization
 open Core
 open FStar.Mul
 
-type t_Bar = {
-  f_a:u8;
-  f_b:u8
-}
-
-type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
-
-class t_FooTrait (v_Self: Type0) = {
-  f_z_pre:v_Self -> Type0;
-  f_z_post:v_Self -> v_Self -> Type0;
-  f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
-}
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_FooTrait_for_Foo: t_FooTrait t_Foo =
-  {
-    f_z_pre = (fun (self: t_Foo) -> true);
-    f_z_post = (fun (self: t_Foo) (out: t_Foo) -> true);
-    f_z = fun (self: t_Foo) -> self
-  }
-
-type t_Pair (v_T: Type0) = {
-  f_a:v_T;
-  f_b:t_Foo
-}
-
 type t_S = { f_b:t_Array u8 (sz 5) }
 
-let impl__S__update (self: t_S) (x: u8) : t_S =
-  let self:t_S =
-    {
-      self with
-      f_b = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize self.f_b (sz 0) x
-    }
-    <:
-    t_S
-  in
-  self
-
-let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) =
-  let x:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize x (sz 1) (x.[ sz 2 ] <: u8)
-  in
-  x
-
-let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 1uy
-  in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy
-  in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
-  vec
-
-let h (x: u8) : u8 =
-  let x:u8 = x +! 10uy in
-  x
-
-let i (bar: t_Bar) : (t_Bar & u8) =
-  let bar:t_Bar = { bar with f_b = bar.f_b +! bar.f_a } <: t_Bar in
-  let bar:t_Bar = { bar with f_a = h bar.f_a } <: t_Bar in
-  let hax_temp_output:u8 = bar.f_a +! bar.f_b in
-  bar, hax_temp_output <: (t_Bar & u8)
-
-let j (x: t_Bar) : (t_Bar & u8) =
-  let out:u8 = 123uy in
-  let tmp0, out1:(t_Bar & u8) = i x in
-  let x:t_Bar = tmp0 in
-  let hax_temp_output:u8 = out1 +! out in
-  x, hax_temp_output <: (t_Bar & u8)
-
-let k
-      (vec: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-      (arg_1_wild3: u16)
-      (arg_1_wild: u8)
-      (arg_3_wild2: Prims.unit)
-    : (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) =
-  let arg_1_wild2:u8 = vec.[ sz 1 ] in
-  let arg_3_wild:u8 = vec.[ sz 2 ] in
-  let arg_1_wild1:u8 = vec.[ sz 3 ] in
-  let arg_3_wild1:u8 = vec.[ sz 4 ] in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize vec
-      (sz 0)
-      ((((arg_1_wild +! arg_3_wild <: u8) +! arg_1_wild1 <: u8) +! arg_3_wild1 <: u8) +! arg_1_wild
-        <:
-        u8)
-  in
-  let hax_temp_output:u64 = 12345uL in
-  vec, arg_1_wild3, arg_3_wild2, hax_temp_output
-  <:
-  (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64)
-
 let foo (lhs rhs: t_S) : t_S =
   let lhs:t_S =
     Rust_primitives.Hax.Folds.fold_range (sz 0)
@@ -155,56 +61,16 @@ let foo (lhs rhs: t_S) : t_S =
   in
   lhs
 
-let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-    : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
-  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-    Rust_primitives.Hax.Folds.fold_range 1uy
-      10uy
-      (fun x temp_1_ ->
-          let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
-          let _:u8 = temp_1_ in
-          true)
-      x
-      (fun x i ->
-          let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
-          let i:u8 = i in
-          {
-            x with
-            f_a
-            =
-            Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i
-            <:
-            Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
-          }
-          <:
-          t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-  in
-  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-    { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) }
-    <:
-    t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-  in
-  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
+let impl__S__update (self: t_S) (x: u8) : t_S =
+  let self:t_S =
     {
-      x with
-      f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo
+      self with
+      f_b = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize self.f_b (sz 0) x
     }
     <:
-    t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    t_S
   in
-  x.f_a
-
-let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  Alloc.Slice.impl__into_vec #u8
-    #Alloc.Alloc.t_Global
-    (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in
-              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
-              Rust_primitives.Hax.array_of_list 3 list)
-          <:
-          Alloc.Boxed.t_Box (t_Array u8 (sz 3)) Alloc.Alloc.t_Global)
-      <:
-      Alloc.Boxed.t_Box (t_Slice u8) Alloc.Alloc.t_Global)
+  self
 
 let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.unit =
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
@@ -250,6 +116,17 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
   in
   42uy
 
+let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  Alloc.Slice.impl__into_vec #u8
+    #Alloc.Alloc.t_Global
+    (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in
+              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
+              Rust_primitives.Hax.array_of_list 3 list)
+          <:
+          Alloc.Boxed.t_Box (t_Array u8 (sz 3)) Alloc.Alloc.t_Global)
+      <:
+      Alloc.Boxed.t_Box (t_Slice u8) Alloc.Alloc.t_Global)
+
 let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in
   let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
@@ -277,4 +154,127 @@ let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
       (build_vec () <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   in
   vec1
+
+let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 1uy
+  in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy
+  in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
+  vec
+
+type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
+
+type t_Pair (v_T: Type0) = {
+  f_a:v_T;
+  f_b:t_Foo
+}
+
+let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
+    : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
+  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
+    Rust_primitives.Hax.Folds.fold_range 1uy
+      10uy
+      (fun x temp_1_ ->
+          let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
+          let _:u8 = temp_1_ in
+          true)
+      x
+      (fun x i ->
+          let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
+          let i:u8 = i in
+          {
+            x with
+            f_a
+            =
+            Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i
+            <:
+            Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
+          }
+          <:
+          t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
+  in
+  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
+    { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) }
+    <:
+    t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+  in
+  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
+    {
+      x with
+      f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo
+    }
+    <:
+    t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+  in
+  x.f_a
+
+let h (x: u8) : u8 =
+  let x:u8 = x +! 10uy in
+  x
+
+type t_Bar = {
+  f_a:u8;
+  f_b:u8
+}
+
+let i (bar: t_Bar) : (t_Bar & u8) =
+  let bar:t_Bar = { bar with f_b = bar.f_b +! bar.f_a } <: t_Bar in
+  let bar:t_Bar = { bar with f_a = h bar.f_a } <: t_Bar in
+  let hax_temp_output:u8 = bar.f_a +! bar.f_b in
+  bar, hax_temp_output <: (t_Bar & u8)
+
+let j (x: t_Bar) : (t_Bar & u8) =
+  let out:u8 = 123uy in
+  let tmp0, out1:(t_Bar & u8) = i x in
+  let x:t_Bar = tmp0 in
+  let hax_temp_output:u8 = out1 +! out in
+  x, hax_temp_output <: (t_Bar & u8)
+
+let k
+      (vec: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+      (arg_1_wild3: u16)
+      (arg_1_wild: u8)
+      (arg_3_wild2: Prims.unit)
+    : (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) =
+  let arg_1_wild2:u8 = vec.[ sz 1 ] in
+  let arg_3_wild:u8 = vec.[ sz 2 ] in
+  let arg_1_wild1:u8 = vec.[ sz 3 ] in
+  let arg_3_wild1:u8 = vec.[ sz 4 ] in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize vec
+      (sz 0)
+      ((((arg_1_wild +! arg_3_wild <: u8) +! arg_1_wild1 <: u8) +! arg_3_wild1 <: u8) +! arg_1_wild
+        <:
+        u8)
+  in
+  let hax_temp_output:u64 = 12345uL in
+  vec, arg_1_wild3, arg_3_wild2, hax_temp_output
+  <:
+  (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64)
+
+class t_FooTrait (v_Self: Type0) = {
+  f_z_pre:v_Self -> Type0;
+  f_z_post:v_Self -> v_Self -> Type0;
+  f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
+}
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_FooTrait_for_Foo: t_FooTrait t_Foo =
+  {
+    f_z_pre = (fun (self: t_Foo) -> true);
+    f_z_post = (fun (self: t_Foo) (out: t_Foo) -> true);
+    f_z = fun (self: t_Foo) -> self
+  }
+
+let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) =
+  let x:t_Array u8 (sz 10) =
+    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize x (sz 1) (x.[ sz 2 ] <: u8)
+  in
+  x
 '''
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index f25ae1575..903e5db34 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
@@ -94,41 +94,46 @@ module Naming
 open Core
 open FStar.Mul
 
-type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
-
-type t_B = | B : t_B
-
-let impl__B__f (self: t_B) : t_B = B <: t_B
-
-type t_C = { f_x:usize }
-
 type t_Foo =
   | Foo_A : t_Foo
   | Foo_B { f_x:usize }: t_Foo
 
-let impl__Foo__f (self: t_Foo) : t_Foo = Foo_A <: t_Foo
-
 type t_Foo2 =
   | Foo2_A : t_Foo2
   | Foo2_B { f_x:usize }: t_Foo2
 
-class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
+type t_B = | B : t_B
+
+type t_C = { f_x:usize }
+
+type t_X = | X : t_X
+
+let mk_c (_: Prims.unit) : t_C =
+  let _:t_Foo = Foo_B ({ Naming.Foo.f_x = sz 3 }) <: t_Foo in
+  let _:t_X = X <: t_X in
+  { f_x = sz 3 } <: t_C
+
+let impl__Foo__f (self: t_Foo) : t_Foo = Foo_A <: t_Foo
+
+let impl__B__f (self: t_B) : t_B = B <: t_B
 
 type t_Foobar = { f_a:t_Foo }
 
-type t_StructA = { f_a:usize }
+let ff__g (_: Prims.unit) : Prims.unit = ()
 
-type t_StructB = {
-  f_a:usize;
-  f_b:usize
-}
+let ff__g__impl__g (self: t_B) : usize = sz 0
 
-type t_StructC = { f_a:usize }
+type t_f__g__impl__g__Foo =
+  | C_f__g__impl__g__Foo_A : t_f__g__impl__g__Foo
+  | C_f__g__impl__g__Foo_B { f_x:usize }: t_f__g__impl__g__Foo
 
-type t_StructD = {
-  f_a:usize;
-  f_b:usize
-}
+let ff__g__impl_1__g (self: t_Foo) : usize = sz 1
+
+let f (x: t_Foobar) : usize = ff__g__impl_1__g x.f_a
+
+let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_of
+
+type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
 
 class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
 
@@ -149,16 +154,19 @@ class t_T3_e_for_a (v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }
 
-type t_X = | X : t_X
+type t_StructA = { f_a:usize }
 
-let v_INHERENT_CONSTANT: usize = sz 3
+type t_StructB = {
+  f_a:usize;
+  f_b:usize
+}
 
-let constants
-      (#v_T: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T)
-      (_: Prims.unit)
-    : usize =
-  (f_ASSOCIATED_CONSTANT #FStar.Tactics.Typeclasses.solve <: usize) +! v_INHERENT_CONSTANT
+type t_StructC = { f_a:usize }
+
+type t_StructD = {
+  f_a:usize;
+  f_b:usize
+}
 
 let construct_structs (a b: usize) : Prims.unit =
   let _:t_StructA = { f_a = a } <: t_StructA in
@@ -167,24 +175,16 @@ let construct_structs (a b: usize) : Prims.unit =
   let _:t_StructD = { f_a = a; f_b = b } <: t_StructD in
   ()
 
-let ff__g (_: Prims.unit) : Prims.unit = ()
-
-let ff__g__impl__g (self: t_B) : usize = sz 0
-
-type t_f__g__impl__g__Foo =
-  | C_f__g__impl__g__Foo_A : t_f__g__impl__g__Foo
-  | C_f__g__impl__g__Foo_B { f_x:usize }: t_f__g__impl__g__Foo
-
-let ff__g__impl_1__g (self: t_Foo) : usize = sz 1
-
-let f (x: t_Foobar) : usize = ff__g__impl_1__g x.f_a
+let v_INHERENT_CONSTANT: usize = sz 3
 
-let mk_c (_: Prims.unit) : t_C =
-  let _:t_Foo = Foo_B ({ Naming.Foo.f_x = sz 3 }) <: t_Foo in
-  let _:t_X = X <: t_X in
-  { f_x = sz 3 } <: t_C
+class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
 
-let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_of
+let constants
+      (#v_T: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T)
+      (_: Prims.unit)
+    : usize =
+  (f_ASSOCIATED_CONSTANT #FStar.Tactics.Typeclasses.solve <: usize) +! v_INHERENT_CONSTANT
 
 /// From issue https://github.com/hacspec/hax/issues/839
 let string_shadows (v_string n: string) : Prims.unit = ()
diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap
index f4b3cbfe0..470b72517 100644
--- a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap
+++ b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap
@@ -42,6 +42,8 @@ Import RecordSetNotations.
 
 
 
+(* NotImplementedYet *)
+
 Inductive t_E : Type :=
 | E_A
 | E_B.
@@ -56,8 +58,6 @@ Definition t_E_cast_to_repr (x : t_E) : t_isize :=
     1
   end.
 
-(* NotImplementedYet *)
-
 Definition bar (x : t_E) : unit :=
   match x with
   | E_A
@@ -65,6 +65,17 @@ Definition bar (x : t_E) : unit :=
     tt
   end.
 
+Definition nested (x : t_Option ((t_i32))) : t_i32 :=
+  match x with
+  | Option_Some (1
+  | 2) =>
+    1
+  | Option_Some (x) =>
+    x
+  | Option_None =>
+    0
+  end.
+
 Definition deep (x : (t_i32*t_Option ((t_i32)))) : t_i32 :=
   match x with
   | (1
@@ -75,18 +86,6 @@ Definition deep (x : (t_i32*t_Option ((t_i32)))) : t_i32 :=
     x
   end.
 
-Definition deep_capture (x : t_Result (((t_i32*t_i32))) (((t_i32*t_i32)))) : t_i32 :=
-  match x with
-  | Result_Ok ((1
-  | 2,x))
-  | Result_Err ((3
-  | 4,x)) =>
-    x
-  | Result_Ok ((x,_))
-  | Result_Err ((x,_)) =>
-    x
-  end.
-
 Definition equivalent (x : (t_i32*t_Option ((t_i32)))) : t_i32 :=
   match x with
   | (1,Option_Some (3))
@@ -98,14 +97,15 @@ Definition equivalent (x : (t_i32*t_Option ((t_i32)))) : t_i32 :=
     x
   end.
 
-Definition nested (x : t_Option ((t_i32))) : t_i32 :=
+Definition deep_capture (x : t_Result (((t_i32*t_i32))) (((t_i32*t_i32)))) : t_i32 :=
   match x with
-  | Option_Some (1
-  | 2) =>
-    1
-  | Option_Some (x) =>
+  | Result_Ok ((1
+  | 2,x))
+  | Result_Err ((3
+  | 4,x)) =>
+    x
+  | Result_Ok ((x,_))
+  | Result_Err ((x,_)) =>
     x
-  | Option_None =>
-    0
   end.
 '''
diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap
index 9fdc477aa..16d56d8f9 100644
--- a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap
@@ -44,6 +44,12 @@ let t_E_cast_to_repr (x: t_E) : isize =
 
 let bar (x: t_E) : Prims.unit = match x with | E_A  | E_B  -> () <: Prims.unit
 
+let nested (x: Core.Option.t_Option i32) : i32 =
+  match x with
+  | Core.Option.Option_Some 1l | Core.Option.Option_Some 2l -> 1l
+  | Core.Option.Option_Some x -> x
+  | Core.Option.Option_None  -> 0l
+
 let deep (x: (i32 & Core.Option.t_Option i32)) : i32 =
   match x with
   | 1l, Core.Option.Option_Some 3l
@@ -52,14 +58,6 @@ let deep (x: (i32 & Core.Option.t_Option i32)) : i32 =
   | 2l, Core.Option.Option_Some 4l -> 0l
   | x, _ -> x
 
-let deep_capture (x: Core.Result.t_Result (i32 & i32) (i32 & i32)) : i32 =
-  match x with
-  | Core.Result.Result_Ok (1l, x)
-  | Core.Result.Result_Ok (2l, x)
-  | Core.Result.Result_Err (3l, x)
-  | Core.Result.Result_Err (4l, x) -> x
-  | Core.Result.Result_Ok (x, _) | Core.Result.Result_Err (x, _) -> x
-
 let equivalent (x: (i32 & Core.Option.t_Option i32)) : i32 =
   match x with
   | 1l, Core.Option.Option_Some 3l
@@ -68,9 +66,11 @@ let equivalent (x: (i32 & Core.Option.t_Option i32)) : i32 =
   | 2l, Core.Option.Option_Some 4l -> 0l
   | x, _ -> x
 
-let nested (x: Core.Option.t_Option i32) : i32 =
+let deep_capture (x: Core.Result.t_Result (i32 & i32) (i32 & i32)) : i32 =
   match x with
-  | Core.Option.Option_Some 1l | Core.Option.Option_Some 2l -> 1l
-  | Core.Option.Option_Some x -> x
-  | Core.Option.Option_None  -> 0l
+  | Core.Result.Result_Ok (1l, x)
+  | Core.Result.Result_Ok (2l, x)
+  | Core.Result.Result_Err (3l, x)
+  | Core.Result.Result_Err (4l, x) -> x
+  | Core.Result.Result_Ok (x, _) | Core.Result.Result_Err (x, _) -> x
 '''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap
index d3b0567d8..4890d697f 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap
+++ b/test-harness/src/snapshots/toolchain__reordering into-coq.snap
@@ -41,12 +41,23 @@ Import RecordSetNotations.
 
 
 
+(* NotImplementedYet *)
+
+Definition no_dependency_1_ (_ : unit) : unit :=
+  tt.
+
+Definition no_dependency_2_ (_ : unit) : unit :=
+  tt.
+
 Inductive t_Foo : Type :=
 | Foo_A
 | Foo_B.
 Arguments t_Foo:clear implicits.
 Arguments t_Foo.
 
+Definition f (_ : t_u32) : t_Foo :=
+  Foo_A.
+
 Record t_Bar : Type :=
   {
     0 : t_Foo;
@@ -57,6 +68,9 @@ Arguments Build_t_Bar.
 #[export] Instance settable_t_Bar : Settable _ :=
   settable! (@Build_t_Bar) <0>.
 
+Definition g (_ : unit) : t_Bar :=
+  Build_t_Bar (f (32)).
+
 Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize :=
   match x with
   | Foo_A =>
@@ -66,16 +80,83 @@ Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize :=
   end.
 
 (* NotImplementedYet *)
+'''
+"Reordering_No_alpha_sorting.v" = '''
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
 
-Definition f (_ : t_u32) : t_Foo :=
-  Foo_A.
+Definition u01 (_ : unit) : unit :=
+  tt.
 
-Definition g (_ : unit) : t_Bar :=
-  Build_t_Bar (f (32)).
+Definition r02 (_ : unit) : unit :=
+  tt.
 
-Definition no_dependency_1_ (_ : unit) : unit :=
+Definition b03 (_ : unit) : unit :=
   tt.
 
-Definition no_dependency_2_ (_ : unit) : unit :=
+Definition f04 (_ : unit) : unit :=
+  tt.
+
+Definition h05 (_ : unit) : unit :=
+  tt.
+
+Definition i06 (_ : unit) : unit :=
+  tt.
+
+Definition c07 (_ : unit) : unit :=
+  tt.
+
+Definition k08 (_ : unit) : unit :=
+  tt.
+
+Definition d09 (_ : unit) : unit :=
+  tt.
+
+Definition e10 (_ : unit) : unit :=
+  tt.
+
+Definition g11 (_ : unit) : unit :=
+  tt.
+
+Definition j12 (_ : unit) : unit :=
+  tt.
+
+Definition o13 (_ : unit) : unit :=
+  tt.
+
+Definition a14 (_ : unit) : unit :=
+  tt.
+
+Definition q15 (_ : unit) : unit :=
+  tt.
+
+Definition m16 (_ : unit) : unit :=
+  tt.
+
+Definition l17 (_ : unit) : unit :=
+  tt.
+
+Definition n18 (_ : unit) : unit :=
+  tt.
+
+Definition v19 (_ : unit) : unit :=
+  tt.
+
+Definition s20 (_ : unit) : unit :=
+  tt.
+
+Definition p21 (_ : unit) : unit :=
+  tt.
+
+Definition t22 (_ : unit) : unit :=
   tt.
 '''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap
index 385642dd2..dec2f94bb 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap
@@ -26,28 +26,78 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Reordering.No_alpha_sorting.fst" = '''
+module Reordering.No_alpha_sorting
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let u01 (_: Prims.unit) : Prims.unit = ()
+
+let r02 (_: Prims.unit) : Prims.unit = ()
+
+let b03 (_: Prims.unit) : Prims.unit = ()
+
+let f04 (_: Prims.unit) : Prims.unit = ()
+
+let h05 (_: Prims.unit) : Prims.unit = ()
+
+let i06 (_: Prims.unit) : Prims.unit = ()
+
+let c07 (_: Prims.unit) : Prims.unit = ()
+
+let k08 (_: Prims.unit) : Prims.unit = ()
+
+let d09 (_: Prims.unit) : Prims.unit = ()
+
+let e10 (_: Prims.unit) : Prims.unit = ()
+
+let g11 (_: Prims.unit) : Prims.unit = ()
+
+let j12 (_: Prims.unit) : Prims.unit = ()
+
+let o13 (_: Prims.unit) : Prims.unit = ()
+
+let a14 (_: Prims.unit) : Prims.unit = ()
+
+let q15 (_: Prims.unit) : Prims.unit = ()
+
+let m16 (_: Prims.unit) : Prims.unit = ()
+
+let l17 (_: Prims.unit) : Prims.unit = ()
+
+let n18 (_: Prims.unit) : Prims.unit = ()
+
+let v19 (_: Prims.unit) : Prims.unit = ()
+
+let s20 (_: Prims.unit) : Prims.unit = ()
+
+let p21 (_: Prims.unit) : Prims.unit = ()
+
+let t22 (_: Prims.unit) : Prims.unit = ()
+'''
 "Reordering.fst" = '''
 module Reordering
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
+let no_dependency_1_ (_: Prims.unit) : Prims.unit = ()
+
+let no_dependency_2_ (_: Prims.unit) : Prims.unit = ()
+
 type t_Foo =
   | Foo_A : t_Foo
   | Foo_B : t_Foo
 
+let f (_: u32) : t_Foo = Foo_A <: t_Foo
+
 type t_Bar = | Bar : t_Foo -> t_Bar
 
+let g (_: Prims.unit) : t_Bar = Bar (f 32ul) <: t_Bar
+
 let t_Foo_cast_to_repr (x: t_Foo) : isize =
   match x with
   | Foo_A  -> isz 0
   | Foo_B  -> isz 1
-
-let f (_: u32) : t_Foo = Foo_A <: t_Foo
-
-let g (_: Prims.unit) : t_Bar = Bar (f 32ul) <: t_Bar
-
-let no_dependency_1_ (_: Prims.unit) : Prims.unit = ()
-
-let no_dependency_2_ (_: Prims.unit) : Prims.unit = ()
 '''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap
index b6655f747..884bc8a78 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap
+++ b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap
@@ -53,6 +53,18 @@ Import choice.Choice.Exports.
 
 Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
+(*Not implemented yet? todo(item)*)
+
+Equations no_dependency_1_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  no_dependency_1_ _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  no_dependency_2_ _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
 Definition t_Foo : choice_type :=
   ('unit ∐ 'unit).
 Notation "'Foo_A_case'" := (inl tt) (at level 100).
@@ -66,6 +78,11 @@ Equations Foo_B {L : {fset Location}} {I : Interface} : both L I t_Foo :=
     solve_lift (ret_both (inr (tt : 'unit) : t_Foo)) : both L I t_Foo.
 Fail Next Obligation.
 
+Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo :=
+  f _  :=
+    Foo_A : both L1 I1 t_Foo.
+Fail Next Obligation.
+
 Definition t_Bar : choice_type :=
   (t_Foo).
 Equations 0 {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I t_Foo :=
@@ -80,6 +97,11 @@ Equations Build_t_Bar {L0 : {fset Location}} {I0 : Interface} {0 : both L0 I0 t_
 Fail Next Obligation.
 Notation "'Build_t_Bar' '[' x ']' '(' '0' ':=' y ')'" := (Build_t_Bar (0 := y)).
 
+Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 t_Bar :=
+  g _  :=
+    Bar (solve_lift (f (ret_both (32 : int32)))) : both L1 I1 t_Bar.
+Fail Next Obligation.
+
 Equations t_Foo_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_Foo) : both L1 I1 uint_size :=
   t_Foo_cast_to_repr x  :=
     matchb x with
@@ -91,24 +113,141 @@ Equations t_Foo_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x : both L
 Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
+'''
+"Reordering_No_alpha_sorting.v" = '''
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+From mathcomp Require Import word_ssrZ word.
+From Jasmin Require Import word.
 
-Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo :=
-  f _  :=
-    Foo_A : both L1 I1 t_Foo.
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+Equations u01 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  u01 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
 Fail Next Obligation.
 
-Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 t_Bar :=
-  g _  :=
-    Bar (solve_lift (f (ret_both (32 : int32)))) : both L1 I1 t_Bar.
+Equations r02 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  r02 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
 Fail Next Obligation.
 
-Equations no_dependency_1_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
-  no_dependency_1_ _  :=
+Equations b03 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  b03 _  :=
     solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
 Fail Next Obligation.
 
-Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
-  no_dependency_2_ _  :=
+Equations f04 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  f04 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations h05 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  h05 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations i06 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  i06 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations c07 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  c07 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations k08 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  k08 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations d09 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  d09 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations e10 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  e10 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations g11 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  g11 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations j12 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  j12 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations o13 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  o13 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations a14 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  a14 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations q15 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  q15 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations m16 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  m16 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations l17 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  l17 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations n18 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  n18 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations v19 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  v19 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations s20 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  s20 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations p21 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  p21 _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations t22 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  t22 _  :=
     solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
 Fail Next Obligation.
 '''
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index a2038278d..08362b003 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
@@ -72,8 +72,8 @@ let test (x y: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
       (fun i ->
           let i:i32 = i in
           match y with
-          | Core.Option.Option_Some hoist1 ->
-            Core.Option.Option_Some (i +! hoist1 <: i32) <: Core.Option.t_Option i32
+          | Core.Option.Option_Some hoist38 ->
+            Core.Option.Option_Some (i +! hoist38 <: i32) <: Core.Option.t_Option i32
           | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32)
   with
   | Core.Option.Option_Some some -> some
@@ -85,150 +85,10 @@ module Side_effects
 open Core
 open FStar.Mul
 
-type t_A = | A : t_A
-
-type t_B = | B : t_B
-
-type t_Bar = {
-  f_a:bool;
-  f_b:(t_Array (bool & bool) (sz 6) & bool)
-}
-
-type t_Foo = {
-  f_x:bool;
-  f_y:(bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global);
-  f_z:t_Array t_Bar (sz 6);
-  f_bar:t_Bar
-}
-
 /// Helper function
 let add3 (x y z: u32) : u32 =
   Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add x y <: u32) z
 
-/// Test assignation on non-trivial places
-let assign_non_trivial_lhs (foo: t_Foo) : t_Foo =
-  let foo:t_Foo = { foo with f_x = true } <: t_Foo in
-  let foo:t_Foo = { foo with f_bar = { foo.f_bar with f_a = true } <: t_Bar } <: t_Foo in
-  let foo:t_Foo =
-    {
-      foo with
-      f_bar
-      =
-      {
-        foo.f_bar with
-        f_b
-        =
-        {
-          foo.f_bar.f_b with
-          _1
-          =
-          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_bar.f_b._1
-            (sz 3)
-            ({ (foo.f_bar.f_b._1.[ sz 3 ] <: (bool & bool)) with _2 = true } <: (bool & bool))
-        }
-        <:
-        (t_Array (bool & bool) (sz 6) & bool)
-      }
-      <:
-      t_Bar
-    }
-    <:
-    t_Foo
-  in
-  let foo:t_Foo =
-    {
-      foo with
-      f_z
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_z
-        (sz 3)
-        ({ (foo.f_z.[ sz 3 ] <: t_Bar) with f_a = true } <: t_Bar)
-    }
-    <:
-    t_Foo
-  in
-  let foo:t_Foo =
-    {
-      foo with
-      f_y
-      =
-      {
-        foo.f_y with
-        _2
-        =
-        Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_y._2
-          (sz 3)
-          ({
-              (foo.f_y._2.[ sz 3 ] <: t_Bar) with
-              f_b
-              =
-              {
-                (foo.f_y._2.[ sz 3 ] <: t_Bar).f_b with
-                _1
-                =
-                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (foo.f_y._2.[ sz 3 ]
-                    <:
-                    t_Bar)
-                    .f_b
-                    ._1
-                  (sz 5)
-                  ({
-                      ((foo.f_y._2.[ sz 3 ] <: t_Bar).f_b._1.[ sz 5 ] <: (bool & bool)) with
-                      _1 = true
-                    }
-                    <:
-                    (bool & bool))
-                <:
-                t_Array (bool & bool) (sz 6)
-              }
-              <:
-              (t_Array (bool & bool) (sz 6) & bool)
-            }
-            <:
-            t_Bar)
-      }
-      <:
-      (bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global)
-    }
-    <:
-    t_Foo
-  in
-  foo
-
-/// Question mark without error coercion
-let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32)
-    : Core.Result.t_Result i8 u32 =
-  match y with
-  | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32
-  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32
-
-/// Question mark with an error coercion
-let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
-    : Core.Result.t_Result i8 u32 =
-  match y with
-  | Core.Result.Result_Ok hoist5 -> Core.Result.Result_Ok hoist5 <: Core.Result.t_Result i8 u32
-  | Core.Result.Result_Err err ->
-    Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err)
-    <:
-    Core.Result.t_Result i8 u32
-
-/// Exercise early returns with control flow and loops
-let early_returns (x: u32) : u32 =
-  if x >. 3ul
-  then 0ul
-  else
-    if x >. 30ul
-    then
-      match true with
-      | true -> 34ul
-      | _ ->
-        let x, hoist9:(u32 & u32) = x, 3ul <: (u32 & u32) in
-        Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist9 <: u32) x
-    else
-      let x:u32 = x +! 9ul in
-      let x, hoist9:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in
-      Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist9 <: u32) x
-
 /// Exercise local mutation with control flow and loops
 let local_mutation (x: u32) : u32 =
   let y:u32 = 0ul in
@@ -255,7 +115,7 @@ let local_mutation (x: u32) : u32 =
     in
     Core.Num.impl__u32__wrapping_add x y
   else
-    let (x, y), hoist19:((u32 & u32) & u32) =
+    let (x, y), hoist7:((u32 & u32) & u32) =
       match x with
       | 12ul ->
         let y:u32 = Core.Num.impl__u32__wrapping_add x y in
@@ -267,47 +127,97 @@ let local_mutation (x: u32) : u32 =
         ((u32 & u32) & u32)
       | _ -> (x, y <: (u32 & u32)), 0ul <: ((u32 & u32) & u32)
     in
-    let x:u32 = hoist19 in
+    let x:u32 = hoist7 in
     Core.Num.impl__u32__wrapping_add x y
 
-/// Combine `?` and early return
-let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B =
-  if x >. 123uy
+/// Exercise early returns with control flow and loops
+let early_returns (x: u32) : u32 =
+  if x >. 3ul
+  then 0ul
+  else
+    if x >. 30ul
+    then
+      match true with
+      | true -> 34ul
+      | _ ->
+        let x, hoist11:(u32 & u32) = x, 3ul <: (u32 & u32) in
+        Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist11 <: u32) x
+    else
+      let x:u32 = x +! 9ul in
+      let x, hoist11:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in
+      Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist11 <: u32) x
+
+let simplifiable_return (c1 c2 c3: bool) : i32 =
+  let x:i32 = 0l in
+  if c1
   then
-    match Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B with
-    | Core.Result.Result_Ok hoist20 -> Core.Result.Result_Ok hoist20 <: Core.Result.t_Result t_A t_B
-    | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_A t_B
-  else Core.Result.Result_Ok (A <: t_A) <: Core.Result.t_Result t_A t_B
+    if c2
+    then
+      let x:i32 = x +! 10l in
+      if c3 then 1l else x +! 1l
+    else x +! 1l
+  else x
+
+let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
+  if c
+  then
+    match x with
+    | Core.Option.Option_Some hoist16 ->
+      let a:i32 = hoist16 +! 10l in
+      let b:i32 = 20l in
+      Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32
+    | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32
+  else
+    let a:i32 = 0l in
+    let b:i32 = 20l in
+    Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32
+
+/// Question mark without error coercion
+let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32)
+    : Core.Result.t_Result i8 u32 =
+  match y with
+  | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32
+  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32
+
+/// Question mark with an error coercion
+let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
+    : Core.Result.t_Result i8 u32 =
+  match y with
+  | Core.Result.Result_Ok hoist17 -> Core.Result.Result_Ok hoist17 <: Core.Result.t_Result i8 u32
+  | Core.Result.Result_Err err ->
+    Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err)
+    <:
+    Core.Result.t_Result i8 u32
 
 /// Test question mark on `Option`s with some control flow
 let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 =
   match x with
-  | Core.Option.Option_Some hoist26 ->
-    if hoist26 >. 10uy
+  | Core.Option.Option_Some hoist21 ->
+    if hoist21 >. 10uy
     then
       match x with
-      | Core.Option.Option_Some hoist28 ->
+      | Core.Option.Option_Some hoist23 ->
         (match
-            Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist28 3uy)
+            Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist23 3uy)
             <:
             Core.Option.t_Option u8
           with
-          | Core.Option.Option_Some hoist34 ->
-            (match hoist34 with
+          | Core.Option.Option_Some hoist29 ->
+            (match hoist29 with
               | 3uy ->
                 (match Core.Option.Option_None <: Core.Option.t_Option u8 with
                   | Core.Option.Option_Some some ->
                     let v:u8 = some in
                     (match x with
-                      | Core.Option.Option_Some hoist35 ->
+                      | Core.Option.Option_Some hoist30 ->
                         (match y with
-                          | Core.Option.Option_Some hoist36 ->
+                          | Core.Option.Option_Some hoist31 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist35
+                                    hoist30
                                   <:
                                   u8)
-                                hoist36)
+                                hoist31)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -317,18 +227,18 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                   | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8)
               | 4uy ->
                 (match z with
-                  | Core.Option.Option_Some hoist23 ->
-                    let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
+                  | Core.Option.Option_Some hoist18 ->
+                    let v:u8 = 4uy +! (if hoist18 >. 4uL <: bool then 0uy else 3uy) in
                     (match x with
-                      | Core.Option.Option_Some hoist35 ->
+                      | Core.Option.Option_Some hoist30 ->
                         (match y with
-                          | Core.Option.Option_Some hoist36 ->
+                          | Core.Option.Option_Some hoist31 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist35
+                                    hoist30
                                   <:
                                   u8)
-                                hoist36)
+                                hoist31)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -339,14 +249,14 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
               | _ ->
                 let v:u8 = 12uy in
                 match x with
-                | Core.Option.Option_Some hoist35 ->
+                | Core.Option.Option_Some hoist30 ->
                   (match y with
-                    | Core.Option.Option_Some hoist36 ->
+                    | Core.Option.Option_Some hoist31 ->
                       Core.Option.Option_Some
-                      (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist35
+                      (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist30
                             <:
                             u8)
-                          hoist36)
+                          hoist31)
                       <:
                       Core.Option.t_Option u8
                     | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8
@@ -356,30 +266,30 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
       | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8
     else
       (match x with
-        | Core.Option.Option_Some hoist31 ->
+        | Core.Option.Option_Some hoist26 ->
           (match y with
-            | Core.Option.Option_Some hoist30 ->
+            | Core.Option.Option_Some hoist25 ->
               (match
-                  Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist31 hoist30)
+                  Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist26 hoist25)
                   <:
                   Core.Option.t_Option u8
                 with
-                | Core.Option.Option_Some hoist34 ->
-                  (match hoist34 with
+                | Core.Option.Option_Some hoist29 ->
+                  (match hoist29 with
                     | 3uy ->
                       (match Core.Option.Option_None <: Core.Option.t_Option u8 with
                         | Core.Option.Option_Some some ->
                           let v:u8 = some in
                           (match x with
-                            | Core.Option.Option_Some hoist35 ->
+                            | Core.Option.Option_Some hoist30 ->
                               (match y with
-                                | Core.Option.Option_Some hoist36 ->
+                                | Core.Option.Option_Some hoist31 ->
                                   Core.Option.Option_Some
                                   (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                          hoist35
+                                          hoist30
                                         <:
                                         u8)
-                                      hoist36)
+                                      hoist31)
                                   <:
                                   Core.Option.t_Option u8
                                 | Core.Option.Option_None  ->
@@ -390,18 +300,18 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                           Core.Option.Option_None <: Core.Option.t_Option u8)
                     | 4uy ->
                       (match z with
-                        | Core.Option.Option_Some hoist23 ->
-                          let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
+                        | Core.Option.Option_Some hoist18 ->
+                          let v:u8 = 4uy +! (if hoist18 >. 4uL <: bool then 0uy else 3uy) in
                           (match x with
-                            | Core.Option.Option_Some hoist35 ->
+                            | Core.Option.Option_Some hoist30 ->
                               (match y with
-                                | Core.Option.Option_Some hoist36 ->
+                                | Core.Option.Option_Some hoist31 ->
                                   Core.Option.Option_Some
                                   (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                          hoist35
+                                          hoist30
                                         <:
                                         u8)
-                                      hoist36)
+                                      hoist31)
                                   <:
                                   Core.Option.t_Option u8
                                 | Core.Option.Option_None  ->
@@ -413,15 +323,15 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                     | _ ->
                       let v:u8 = 12uy in
                       match x with
-                      | Core.Option.Option_Some hoist35 ->
+                      | Core.Option.Option_Some hoist30 ->
                         (match y with
-                          | Core.Option.Option_Some hoist36 ->
+                          | Core.Option.Option_Some hoist31 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist35
+                                    hoist30
                                   <:
                                   u8)
-                                hoist36)
+                                hoist31)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -457,28 +367,118 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 =
   else
     Core.Result.Result_Ok (Core.Num.impl__u32__wrapping_add 3ul x) <: Core.Result.t_Result u32 u32
 
-let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
-  if c
-  then
-    match x with
-    | Core.Option.Option_Some hoist40 ->
-      let a:i32 = hoist40 +! 10l in
-      let b:i32 = 20l in
-      Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32
-    | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32
-  else
-    let a:i32 = 0l in
-    let b:i32 = 20l in
-    Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32
+type t_A = | A : t_A
 
-let simplifiable_return (c1 c2 c3: bool) : i32 =
-  let x:i32 = 0l in
-  if c1
+type t_B = | B : t_B
+
+/// Combine `?` and early return
+let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B =
+  if x >. 123uy
   then
-    if c2
-    then
-      let x:i32 = x +! 10l in
-      if c3 then 1l else x +! 1l
-    else x +! 1l
-  else x
+    match Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B with
+    | Core.Result.Result_Ok hoist35 -> Core.Result.Result_Ok hoist35 <: Core.Result.t_Result t_A t_B
+    | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_A t_B
+  else Core.Result.Result_Ok (A <: t_A) <: Core.Result.t_Result t_A t_B
+
+type t_Bar = {
+  f_a:bool;
+  f_b:(t_Array (bool & bool) (sz 6) & bool)
+}
+
+type t_Foo = {
+  f_x:bool;
+  f_y:(bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global);
+  f_z:t_Array t_Bar (sz 6);
+  f_bar:t_Bar
+}
+
+/// Test assignation on non-trivial places
+let assign_non_trivial_lhs (foo: t_Foo) : t_Foo =
+  let foo:t_Foo = { foo with f_x = true } <: t_Foo in
+  let foo:t_Foo = { foo with f_bar = { foo.f_bar with f_a = true } <: t_Bar } <: t_Foo in
+  let foo:t_Foo =
+    {
+      foo with
+      f_bar
+      =
+      {
+        foo.f_bar with
+        f_b
+        =
+        {
+          foo.f_bar.f_b with
+          _1
+          =
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_bar.f_b._1
+            (sz 3)
+            ({ (foo.f_bar.f_b._1.[ sz 3 ] <: (bool & bool)) with _2 = true } <: (bool & bool))
+        }
+        <:
+        (t_Array (bool & bool) (sz 6) & bool)
+      }
+      <:
+      t_Bar
+    }
+    <:
+    t_Foo
+  in
+  let foo:t_Foo =
+    {
+      foo with
+      f_z
+      =
+      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_z
+        (sz 3)
+        ({ (foo.f_z.[ sz 3 ] <: t_Bar) with f_a = true } <: t_Bar)
+    }
+    <:
+    t_Foo
+  in
+  let foo:t_Foo =
+    {
+      foo with
+      f_y
+      =
+      {
+        foo.f_y with
+        _2
+        =
+        Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_y._2
+          (sz 3)
+          ({
+              (foo.f_y._2.[ sz 3 ] <: t_Bar) with
+              f_b
+              =
+              {
+                (foo.f_y._2.[ sz 3 ] <: t_Bar).f_b with
+                _1
+                =
+                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (foo.f_y._2.[ sz 3 ]
+                    <:
+                    t_Bar)
+                    .f_b
+                    ._1
+                  (sz 5)
+                  ({
+                      ((foo.f_y._2.[ sz 3 ] <: t_Bar).f_b._1.[ sz 5 ] <: (bool & bool)) with
+                      _1 = true
+                    }
+                    <:
+                    (bool & bool))
+                <:
+                t_Array (bool & bool) (sz 6)
+              }
+              <:
+              (t_Array (bool & bool) (sz 6) & bool)
+            }
+            <:
+            t_Bar)
+      }
+      <:
+      (bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global)
+    }
+    <:
+    t_Foo
+  in
+  foo
 '''
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
index 2f2304adb..4f1746a23 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
+++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
@@ -54,6 +54,163 @@ Import choice.Choice.Exports.
 
 Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
+(*Not implemented yet? todo(item)*)
+
+Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 :=
+  add3 x y z  :=
+    solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32.
+Fail Next Obligation.
+
+Definition y_loc : Location :=
+  (int32;0%nat).
+Definition y_loc : Location :=
+  (int32;1%nat).
+Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc;y_loc]) I1 int32 :=
+  local_mutation x  :=
+    letb y loc(y_loc) := ret_both (0 : int32) in
+    letb _ := assign todo(term) in
+    letb hoist1 := x >.? (ret_both (3 : int32)) in
+    solve_lift (ifb hoist1
+    then letb _ := assign todo(term) in
+    letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in
+    letb _ := assign todo(term) in
+    letb hoist2 := ret_both (0 : int32) in
+    letb hoist3 := Build_t_Range (f_start := hoist2) (f_end := ret_both (10 : int32)) in
+    letb hoist4 := f_into_iter hoist3 in
+    letb _ := foldi_both_list hoist4 (fun i =>
+      ssp (fun _ =>
+        assign todo(term) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in
+    impl__u32__wrapping_add x y
+    else letb hoist7 := matchb x with
+    | 12 =>
+      letb _ := assign todo(term) in
+      solve_lift (ret_both (3 : int32))
+    | 13 =>
+      letb hoist6 := x in
+      letb _ := assign todo(term) in
+      letb hoist5 := impl__u32__wrapping_add (ret_both (123 : int32)) x in
+      solve_lift (add3 hoist6 hoist5 x)
+    | _ =>
+      solve_lift (ret_both (0 : int32))
+    end in
+    letb _ := assign todo(term) in
+    impl__u32__wrapping_add x y) : both (L1 :|: fset [y_loc;y_loc]) I1 int32.
+Fail Next Obligation.
+
+Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 :=
+  early_returns x  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32))
+    then letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break (ret_both (0 : int32)) in
+    ControlFlow_Continue (never_to_any hoist8)
+    else () in
+    letb hoist9 := x >.? (ret_both (30 : int32)) in
+    letm[choice_typeMonad.result_bind_code int32] hoist11 := ifb hoist9
+    then matchb ret_both (true : 'bool) with
+    | true =>
+      letm[choice_typeMonad.result_bind_code int32] hoist10 := ControlFlow_Break (ret_both (34 : int32)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist10))
+    | _ =>
+      ControlFlow_Continue (solve_lift (ret_both (3 : int32)))
+    end
+    else ControlFlow_Continue (letb _ := assign todo(term) in
+    x .+ (ret_both (1 : int32))) in
+    letb hoist12 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist11 in
+    letb hoist13 := impl__u32__wrapping_add hoist12 x in
+    letm[choice_typeMonad.result_bind_code int32] hoist14 := ControlFlow_Break hoist13 in
+    ControlFlow_Continue (never_to_any hoist14))) : both L1 I1 int32.
+Fail Next Obligation.
+
+Definition x_loc : Location :=
+  (int32;2%nat).
+Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (c1 : both L1 I1 'bool) (c2 : both L2 I2 'bool) (c3 : both L3 I3 'bool) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32 :=
+  simplifiable_return c1 c2 c3  :=
+    solve_lift (run (letb x loc(x_loc) := ret_both (0 : int32) in
+    letm[choice_typeMonad.result_bind_code int32] _ := ifb c1
+    then letm[choice_typeMonad.result_bind_code int32] _ := ifb c2
+    then letb _ := assign todo(term) in
+    ifb c3
+    then letm[choice_typeMonad.result_bind_code int32] hoist15 := ControlFlow_Break (ret_both (1 : int32)) in
+    ControlFlow_Continue (never_to_any hoist15)
+    else ()
+    else () in
+    ControlFlow_Continue (letb _ := assign todo(term) in
+    ret_both (tt : 'unit))
+    else () in
+    ControlFlow_Continue x)) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32.
+Fail Next Obligation.
+
+Equations simplifiable_question_mark {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (c : both L1 I1 'bool) (x : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
+  simplifiable_question_mark c x  :=
+    solve_lift (run (letm[choice_typeMonad.option_bind_code] a := ifb c
+    then letm[choice_typeMonad.option_bind_code] hoist16 := x in
+    Option_Some (hoist16 .+ (ret_both (10 : int32)))
+    else Option_Some (ret_both (0 : int32)) in
+    Option_Some (letb b := ret_both (20 : int32) in
+    Option_Some (a .+ b)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+Fail Next Obligation.
+
+Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) :=
+  direct_result_question_mark y  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := y in
+    Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32).
+Fail Next Obligation.
+
+Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
+  direct_result_question_mark_coercion y  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
+    Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
+Fail Next Obligation.
+
+Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) :=
+  options x y z  :=
+    solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist21 := x in
+    letb hoist22 := hoist21 >.? (ret_both (10 : int8)) in
+    letm[choice_typeMonad.option_bind_code] hoist28 := ifb hoist22
+    then letm[choice_typeMonad.option_bind_code] hoist23 := x in
+    Option_Some (letb hoist24 := impl__u8__wrapping_add hoist23 (ret_both (3 : int8)) in
+    Option_Some hoist24)
+    else letm[choice_typeMonad.option_bind_code] hoist26 := x in
+    letm[choice_typeMonad.option_bind_code] hoist25 := y in
+    Option_Some (letb hoist27 := impl__u8__wrapping_add hoist26 hoist25 in
+    Option_Some hoist27) in
+    letm[choice_typeMonad.option_bind_code] hoist29 := hoist28 in
+    letm[choice_typeMonad.option_bind_code] v := matchb hoist29 with
+    | 3 =>
+      Option_None
+    | 4 =>
+      letm[choice_typeMonad.option_bind_code] hoist18 := z in
+      Option_Some (letb hoist19 := hoist18 >.? (ret_both (4 : int64)) in
+      letb hoist20 := ifb hoist19
+      then ret_both (0 : int8)
+      else ret_both (3 : int8) in
+      solve_lift ((ret_both (4 : int8)) .+ hoist20))
+    | _ =>
+      Option_Some (solve_lift (ret_both (12 : int8)))
+    end in
+    letm[choice_typeMonad.option_bind_code] hoist30 := x in
+    letb hoist32 := impl__u8__wrapping_add v hoist30 in
+    letm[choice_typeMonad.option_bind_code] hoist31 := y in
+    Option_Some (letb hoist33 := impl__u8__wrapping_add hoist32 hoist31 in
+    Option_Some hoist33))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8).
+Fail Next Obligation.
+
+Definition y_loc : Location :=
+  (int32;3%nat).
+Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32) :=
+  question_mark x  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
+    then letb y loc(y_loc) := ret_both (0 : int32) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb hoist34 := x >.? (ret_both (90 : int32)) in
+    ifb hoist34
+    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
+    else ()
+    else () in
+    Result_Ok (Result_Ok (impl__u32__wrapping_add (ret_both (3 : int32)) x)))) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32).
+Fail Next Obligation.
+
 Definition t_A : choice_type :=
   'unit.
 Equations Build_t_A : both (fset []) (fset []) (t_A) :=
@@ -68,6 +225,16 @@ Equations Build_t_B : both (fset []) (fset []) (t_B) :=
     solve_lift (ret_both (tt (* Empty tuple *) : (t_B))) : both (fset []) (fset []) (t_B).
 Fail Next Obligation.
 
+Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) :=
+  monad_lifting x  :=
+    solve_lift (run (ifb x >.? (ret_both (123 : int8))
+    then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist35 := ControlFlow_Continue (Result_Err B) in
+    letb hoist36 := Result_Ok hoist35 in
+    letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist37 := ControlFlow_Break hoist36 in
+    ControlFlow_Continue (never_to_any hoist37)
+    else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B).
+Fail Next Obligation.
+
 Definition t_Bar : choice_type :=
   ('bool × nseq ('bool × 'bool) 6 × 'bool).
 Equations f_a {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I 'bool :=
@@ -124,17 +291,6 @@ Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_x :=
 Notation "'Build_t_Foo' '[' x ']' '(' 'f_z' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := y) (f_bar := f_bar x)).
 Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := f_z x) (f_bar := y)).
 
-(*Not implemented yet? todo(item)*)
-
-(*Not implemented yet? todo(item)*)
-
-(*Not implemented yet? todo(item)*)
-
-Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 :=
-  add3 x y z  :=
-    solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32.
-Fail Next Obligation.
-
 Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo : both L1 I1 t_Foo) : both L1 I1 t_Foo :=
   assign_non_trivial_lhs foo  :=
     letb _ := assign todo(term) in
@@ -145,165 +301,9 @@ Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo :
     solve_lift foo : both L1 I1 t_Foo.
 Fail Next Obligation.
 
-Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) :=
-  direct_result_question_mark y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := y in
-    Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32).
-Fail Next Obligation.
-
-Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
-  direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist5 := impl__map_err y f_from in
-    Result_Ok (Result_Ok hoist5))) : both L1 I1 (t_Result int8 int32).
-Fail Next Obligation.
-
-Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 :=
-  early_returns x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32))
-    then letm[choice_typeMonad.result_bind_code int32] hoist6 := ControlFlow_Break (ret_both (0 : int32)) in
-    ControlFlow_Continue (never_to_any hoist6)
-    else () in
-    letb hoist7 := x >.? (ret_both (30 : int32)) in
-    letm[choice_typeMonad.result_bind_code int32] hoist9 := ifb hoist7
-    then matchb ret_both (true : 'bool) with
-    | true =>
-      letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break (ret_both (34 : int32)) in
-      ControlFlow_Continue (solve_lift (never_to_any hoist8))
-    | _ =>
-      ControlFlow_Continue (solve_lift (ret_both (3 : int32)))
-    end
-    else ControlFlow_Continue (letb _ := assign todo(term) in
-    x .+ (ret_both (1 : int32))) in
-    letb hoist10 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist9 in
-    letb hoist11 := impl__u32__wrapping_add hoist10 x in
-    letm[choice_typeMonad.result_bind_code int32] hoist12 := ControlFlow_Break hoist11 in
-    ControlFlow_Continue (never_to_any hoist12))) : both L1 I1 int32.
-Fail Next Obligation.
-
-Definition y_loc : Location :=
-  (int32;0%nat).
-Definition y_loc : Location :=
-  (int32;1%nat).
-Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc;y_loc]) I1 int32 :=
-  local_mutation x  :=
-    letb y loc(y_loc) := ret_both (0 : int32) in
-    letb _ := assign todo(term) in
-    letb hoist13 := x >.? (ret_both (3 : int32)) in
-    solve_lift (ifb hoist13
-    then letb _ := assign todo(term) in
-    letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in
-    letb _ := assign todo(term) in
-    letb hoist14 := ret_both (0 : int32) in
-    letb hoist15 := Build_t_Range (f_start := hoist14) (f_end := ret_both (10 : int32)) in
-    letb hoist16 := f_into_iter hoist15 in
-    letb _ := foldi_both_list hoist16 (fun i =>
-      ssp (fun _ =>
-        assign todo(term) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in
-    impl__u32__wrapping_add x y
-    else letb hoist19 := matchb x with
-    | 12 =>
-      letb _ := assign todo(term) in
-      solve_lift (ret_both (3 : int32))
-    | 13 =>
-      letb hoist18 := x in
-      letb _ := assign todo(term) in
-      letb hoist17 := impl__u32__wrapping_add (ret_both (123 : int32)) x in
-      solve_lift (add3 hoist18 hoist17 x)
-    | _ =>
-      solve_lift (ret_both (0 : int32))
-    end in
-    letb _ := assign todo(term) in
-    impl__u32__wrapping_add x y) : both (L1 :|: fset [y_loc;y_loc]) I1 int32.
-Fail Next Obligation.
-
-Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) :=
-  monad_lifting x  :=
-    solve_lift (run (ifb x >.? (ret_both (123 : int8))
-    then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist20 := ControlFlow_Continue (Result_Err B) in
-    letb hoist21 := Result_Ok hoist20 in
-    letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist22 := ControlFlow_Break hoist21 in
-    ControlFlow_Continue (never_to_any hoist22)
-    else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B).
-Fail Next Obligation.
-
-Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) :=
-  options x y z  :=
-    solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist26 := x in
-    letb hoist27 := hoist26 >.? (ret_both (10 : int8)) in
-    letm[choice_typeMonad.option_bind_code] hoist33 := ifb hoist27
-    then letm[choice_typeMonad.option_bind_code] hoist28 := x in
-    Option_Some (letb hoist29 := impl__u8__wrapping_add hoist28 (ret_both (3 : int8)) in
-    Option_Some hoist29)
-    else letm[choice_typeMonad.option_bind_code] hoist31 := x in
-    letm[choice_typeMonad.option_bind_code] hoist30 := y in
-    Option_Some (letb hoist32 := impl__u8__wrapping_add hoist31 hoist30 in
-    Option_Some hoist32) in
-    letm[choice_typeMonad.option_bind_code] hoist34 := hoist33 in
-    letm[choice_typeMonad.option_bind_code] v := matchb hoist34 with
-    | 3 =>
-      Option_None
-    | 4 =>
-      letm[choice_typeMonad.option_bind_code] hoist23 := z in
-      Option_Some (letb hoist24 := hoist23 >.? (ret_both (4 : int64)) in
-      letb hoist25 := ifb hoist24
-      then ret_both (0 : int8)
-      else ret_both (3 : int8) in
-      solve_lift ((ret_both (4 : int8)) .+ hoist25))
-    | _ =>
-      Option_Some (solve_lift (ret_both (12 : int8)))
-    end in
-    letm[choice_typeMonad.option_bind_code] hoist35 := x in
-    letb hoist37 := impl__u8__wrapping_add v hoist35 in
-    letm[choice_typeMonad.option_bind_code] hoist36 := y in
-    Option_Some (letb hoist38 := impl__u8__wrapping_add hoist37 hoist36 in
-    Option_Some hoist38))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8).
-Fail Next Obligation.
-
-Definition y_loc : Location :=
-  (int32;2%nat).
-Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32) :=
-  question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
-    then letb y loc(y_loc) := ret_both (0 : int32) in
-    letb _ := assign todo(term) in
-    letb _ := assign todo(term) in
-    letb _ := assign todo(term) in
-    letb hoist39 := x >.? (ret_both (90 : int32)) in
-    ifb hoist39
-    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
-    else ()
-    else () in
-    Result_Ok (Result_Ok (impl__u32__wrapping_add (ret_both (3 : int32)) x)))) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32).
-Fail Next Obligation.
-
-Equations simplifiable_question_mark {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (c : both L1 I1 'bool) (x : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
-  simplifiable_question_mark c x  :=
-    solve_lift (run (letm[choice_typeMonad.option_bind_code] a := ifb c
-    then letm[choice_typeMonad.option_bind_code] hoist40 := x in
-    Option_Some (hoist40 .+ (ret_both (10 : int32)))
-    else Option_Some (ret_both (0 : int32)) in
-    Option_Some (letb b := ret_both (20 : int32) in
-    Option_Some (a .+ b)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
-Fail Next Obligation.
+(*Not implemented yet? todo(item)*)
 
-Definition x_loc : Location :=
-  (int32;3%nat).
-Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (c1 : both L1 I1 'bool) (c2 : both L2 I2 'bool) (c3 : both L3 I3 'bool) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32 :=
-  simplifiable_return c1 c2 c3  :=
-    solve_lift (run (letb x loc(x_loc) := ret_both (0 : int32) in
-    letm[choice_typeMonad.result_bind_code int32] _ := ifb c1
-    then letm[choice_typeMonad.result_bind_code int32] _ := ifb c2
-    then letb _ := assign todo(term) in
-    ifb c3
-    then letm[choice_typeMonad.result_bind_code int32] hoist41 := ControlFlow_Break (ret_both (1 : int32)) in
-    ControlFlow_Continue (never_to_any hoist41)
-    else ()
-    else () in
-    ControlFlow_Continue (letb _ := assign todo(term) in
-    ret_both (tt : 'unit))
-    else () in
-    ControlFlow_Continue x)) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32.
-Fail Next Obligation.
+(*Not implemented yet? todo(item)*)
 '''
 "Side_effects_Issue_1083_.v" = '''
 (* File automatically generated by Hacspec *)
@@ -380,11 +380,11 @@ Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
 Equations test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 (t_Option int32)) (y : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
   test x y  :=
-    solve_lift (run (letb hoist3 := fun i =>
-      letm[choice_typeMonad.option_bind_code] hoist1 := y in
-      Option_Some (letb hoist2 := i .+ hoist1 in
-      Option_Some hoist2) in
-    letb hoist4 := impl__map x hoist3 in
-    hoist4)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+    solve_lift (run (letb hoist40 := fun i =>
+      letm[choice_typeMonad.option_bind_code] hoist38 := y in
+      Option_Some (letb hoist39 := i .+ hoist38 in
+      Option_Some hoist39) in
+    letb hoist41 := impl__map x hoist40 in
+    hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
 Fail Next Obligation.
 '''
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 3ada99292..d71f42f39 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
@@ -79,33 +79,6 @@ module Traits.For_clauses.Issue_495_
 open Core
 open FStar.Mul
 
-let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-    : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
-        (Core.Ops.Range.t_Range u8) (u8 -> bool))
-    #FStar.Tactics.Typeclasses.solve
-    #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-    (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8)
-        #FStar.Tactics.Typeclasses.solve
-        ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8)
-        (fun temp_0_ ->
-            let _:u8 = temp_0_ in
-            true)
-      <:
-      Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
-
-let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
-    : Prims.unit =
-  let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
-  =
-    Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
-          (Core.Ops.Range.t_Range u8) (u8 -> bool))
-      #FStar.Tactics.Typeclasses.solve
-      #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-      it
-  in
-  ()
-
 let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Prims.unit =
   let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
   =
@@ -139,6 +112,33 @@ let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
         Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
   in
   ()
+
+let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
+        (Core.Ops.Range.t_Range u8) (u8 -> bool))
+    #FStar.Tactics.Typeclasses.solve
+    #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8)
+        #FStar.Tactics.Typeclasses.solve
+        ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8)
+        (fun temp_0_ ->
+            let _:u8 = temp_0_ in
+            true)
+      <:
+      Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
+
+let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
+    : Prims.unit =
+  let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
+  =
+    Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
+          (Core.Ops.Range.t_Range u8) (u8 -> bool))
+      #FStar.Tactics.Typeclasses.solve
+      #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+      it
+  in
+  ()
 '''
 "Traits.For_clauses.fst" = '''
 module Traits.For_clauses
@@ -342,7 +342,7 @@ let impl (#v_TypeArg: Type0) (v_ConstArg: usize) : t_Trait Prims.unit v_TypeArg
       ()
   }
 
-let associated_function_caller
+let method_caller
       (#v_MethodTypeArg #v_TypeArg: Type0)
       (v_ConstArg v_MethodConstArg: usize)
       (#v_ImplTrait: Type0)
@@ -352,7 +352,7 @@ let associated_function_caller
       (value_Type: t_Type v_TypeArg v_ConstArg)
     : Prims.unit =
   let _:Prims.unit =
-    f_associated_function #v_ImplTrait
+    f_method #v_ImplTrait
       #v_TypeArg
       #v_ConstArg
       #FStar.Tactics.Typeclasses.solve
@@ -364,7 +364,7 @@ let associated_function_caller
   in
   ()
 
-let method_caller
+let associated_function_caller
       (#v_MethodTypeArg #v_TypeArg: Type0)
       (v_ConstArg v_MethodConstArg: usize)
       (#v_ImplTrait: Type0)
@@ -374,7 +374,7 @@ let method_caller
       (value_Type: t_Type v_TypeArg v_ConstArg)
     : Prims.unit =
   let _:Prims.unit =
-    f_method #v_ImplTrait
+    f_associated_function #v_ImplTrait
       #v_TypeArg
       #v_ConstArg
       #FStar.Tactics.Typeclasses.solve
@@ -491,14 +491,14 @@ module Traits.Unconstrainted_types_issue_677_
 open Core
 open FStar.Mul
 
-type t_Plus = | Plus : t_Plus
-
 class t_PolyOp (v_Self: Type0) = {
   f_op_pre:u32 -> u32 -> Type0;
   f_op_post:u32 -> u32 -> u32 -> Type0;
   f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result)
 }
 
+type t_Plus = | Plus : t_Plus
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: t_PolyOp t_Plus =
   {
@@ -528,26 +528,6 @@ module Traits
 open Core
 open FStar.Mul
 
-class t_Bar (v_Self: Type0) = {
-  f_bar_pre:v_Self -> Type0;
-  f_bar_post:v_Self -> Prims.unit -> Type0;
-  f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result)
-}
-
-let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T)
-    : Prims.unit = f_bar #v_T #FStar.Tactics.Typeclasses.solve x
-
-type t_Error = | Error_Fail : t_Error
-
-let impl__Error__for_application_callback (_: Prims.unit) :  Prims.unit -> t_Error =
-  fun temp_0_ ->
-    let _:Prims.unit = temp_0_ in
-    Error_Fail <: t_Error
-
-let t_Error_cast_to_repr (x: t_Error) : isize = match x with | Error_Fail  -> isz 0
-
-type t_Struct = | Struct : t_Struct
-
 class t_SuperTrait (v_Self: Type0) = {
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self;
   f_function_of_super_trait_pre:v_Self -> Type0;
@@ -567,6 +547,17 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 =
     f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32
   }
 
+type t_Struct = | Struct : t_Struct
+
+class t_Bar (v_Self: Type0) = {
+  f_bar_pre:v_Self -> Type0;
+  f_bar_post:v_Self -> Prims.unit -> Type0;
+  f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result)
+}
+
+let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T)
+    : Prims.unit = f_bar #v_T #FStar.Tactics.Typeclasses.solve x
+
 let closure_impl_expr
       (#v_I: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator v_I)
@@ -597,6 +588,15 @@ let closure_impl_expr_fngen
       <:
       Core.Iter.Adapters.Map.t_Map v_I v_F)
 
+type t_Error = | Error_Fail : t_Error
+
+let t_Error_cast_to_repr (x: t_Error) : isize = match x with | Error_Fail  -> isz 0
+
+let impl__Error__for_application_callback (_: Prims.unit) :  Prims.unit -> t_Error =
+  fun temp_0_ ->
+    let _:Prims.unit = temp_0_ in
+    Error_Fail <: t_Error
+
 let iter_option (#v_T: Type0) (x: Core.Option.t_Option v_T) : Core.Option.t_IntoIter v_T =
   Core.Iter.Traits.Collect.f_into_iter #(Core.Option.t_Option v_T)
     #FStar.Tactics.Typeclasses.solve
@@ -632,6 +632,13 @@ class t_Foo (v_Self: Type0) = {
         (fun result -> f_assoc_type_post #i3 x0 result)
 }
 
+let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit =
+  let _:Prims.unit = f_assoc_f #v_T #FStar.Tactics.Typeclasses.solve () in
+  f_method_f #v_T #FStar.Tactics.Typeclasses.solve x
+
+let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType)
+    : u32 = f_function_of_super_trait #i1.f_AssocType #FStar.Tactics.Typeclasses.solve x
+
 class t_Lang (v_Self: Type0) = {
   f_Var:Type0;
   f_s_pre:v_Self -> i32 -> Type0;
@@ -640,13 +647,6 @@ class t_Lang (v_Self: Type0) = {
     -> Prims.Pure (v_Self & f_Var) (f_s_pre x0 x1) (fun result -> f_s_post x0 x1 result)
 }
 
-let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit =
-  let _:Prims.unit = f_assoc_f #v_T #FStar.Tactics.Typeclasses.solve () in
-  f_method_f #v_T #FStar.Tactics.Typeclasses.solve x
-
-let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType)
-    : u32 = f_function_of_super_trait #i1.f_AssocType #FStar.Tactics.Typeclasses.solve x
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_Foo_for_tuple_: t_Foo Prims.unit =
   {
diff --git a/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap b/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap
index 310e2d094..2fba5a2b7 100644
--- a/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap
@@ -37,13 +37,13 @@ type t_Impossible =
 
 let t_Impossible_cast_to_repr (x: t_Impossible) : Rust_primitives.Hax.t_Never = match x with
 
-let get_unchecked_example (slice: t_Slice u8)
-    : Prims.Pure u8
-      (requires (Core.Slice.impl__len #u8 slice <: usize) >. sz 10)
-      (fun _ -> Prims.l_True) = Core.Slice.impl__get_unchecked #u8 #usize slice (sz 6)
-
 let impossible (_: Prims.unit) : Prims.Pure t_Impossible (requires false) (fun _ -> Prims.l_True) =
   Rust_primitives.Hax.never_to_any (Core.Hint.unreachable_unchecked ()
       <:
       Rust_primitives.Hax.t_Never)
+
+let get_unchecked_example (slice: t_Slice u8)
+    : Prims.Pure u8
+      (requires (Core.Slice.impl__len #u8 slice <: usize) >. sz 10)
+      (fun _ -> Prims.l_True) = Core.Slice.impl__get_unchecked #u8 #usize slice (sz 6)
 '''
diff --git a/tests/reordering/src/lib.rs b/tests/reordering/src/lib.rs
index 03e4d0ea8..2be238457 100644
--- a/tests/reordering/src/lib.rs
+++ b/tests/reordering/src/lib.rs
@@ -17,3 +17,28 @@ enum Foo {
     A,
     B,
 }
+
+mod no_alpha_sorting {
+    fn u01() {}
+    fn r02() {}
+    fn b03() {}
+    fn f04() {}
+    fn h05() {}
+    fn i06() {}
+    fn c07() {}
+    fn k08() {}
+    fn d09() {}
+    fn e10() {}
+    fn g11() {}
+    fn j12() {}
+    fn o13() {}
+    fn a14() {}
+    fn q15() {}
+    fn m16() {}
+    fn l17() {}
+    fn n18() {}
+    fn v19() {}
+    fn s20() {}
+    fn p21() {}
+    fn t22() {}
+}