Remove unsize for certain types

engine/backends/fstar/fstar_backend.ml

@@ -1717,6 +1717,30 @@ module TransformToInputLanguage =
   ]
   [@ocamlformat "disable"]
 
+(** Rewrites `unsize x` to `x <: τ` when `τ` is in the allowlist described by `unsize_identity_typ` *)
+let unsize_as_identity =
+  (* Tells if a unsize should be treated as identity by type *)
+  let rec unsize_identity_typ = function
+    | TArray _ -> true
+    | TRef { typ; _ } -> unsize_identity_typ typ
+    | _ -> false
+  in
+  let visitor =
+    object
+      inherit [_] U.Visitors.map as super
+
+      method! visit_expr () e =
+        match e.e with
+        | App { f = { e = GlobalVar f; _ }; args = [ x ]; _ }
+          when Global_ident.eq_name Rust_primitives__unsize f
+               && unsize_identity_typ x.typ ->
+            let x = super#visit_expr () x in
+            { e with e = Ascription { e = x; typ = e.typ } }
+        | _ -> super#visit_expr () e
+    end
+  in
+  visitor#visit_item ()
+
 let apply_phases (bo : BackendOptions.t) (items : Ast.Rust.item list) :
     AST.item list =
   let items =
@@ -1734,6 +1758,8 @@ let apply_phases (bo : BackendOptions.t) (items : Ast.Rust.item list) :
   in
   let items =
     TransformToInputLanguage.ditems items
+    |> List.map ~f:unsize_as_identity
+    |> List.map ~f:unsize_as_identity
     |> List.map ~f:U.Mappers.add_typ_ascription
     (* |> DepGraph.name_me *)
   in

test-harness/src/snapshots/toolchain__literals into-fstar.snap

@@ -157,9 +157,11 @@ let panic_with_msg (_: Prims.unit) : Prims.unit =
 
 let empty_array (_: Prims.unit) : Prims.unit =
   let (_: t_Slice u8):t_Slice u8 =
-    Rust_primitives.unsize (let list:Prims.list u8 = [] in
-        FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 0);
-        Rust_primitives.Hax.array_of_list 0 list)
+    (let list:Prims.list u8 = [] in
+      FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 0);
+      Rust_primitives.Hax.array_of_list 0 list)
+    <:
+    t_Slice u8
   in
   ()
 

test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap

@@ -127,9 +127,9 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
               Core.Ops.Range.t_Range usize ]
             <:
             t_Slice u8)
-          (Rust_primitives.unsize (let list = [1uy; 2uy] in
-                FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
-                Rust_primitives.Hax.array_of_list 2 list)
+          ((let list = [1uy; 2uy] in
+              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+              Rust_primitives.Hax.array_of_list 2 list)
             <:
             t_Slice u8)
         <:

test-harness/src/snapshots/toolchain__slices into-fstar.snap

@@ -34,16 +34,18 @@ open Core
 open FStar.Mul
 
 let v_VERSION: t_Slice u8 =
-  Rust_primitives.unsize (let list = [118uy; 49uy] in
-      FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
-      Rust_primitives.Hax.array_of_list 2 list)
+  (let list = [118uy; 49uy] in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+    Rust_primitives.Hax.array_of_list 2 list)
+  <:
+  t_Slice u8
 
 let do_something (_: t_Slice u8) : Prims.unit = ()
 
 let r#unsized (_: t_Array (t_Slice u8) (sz 1)) : Prims.unit = ()
 
 let sized (x: t_Array (t_Array u8 (sz 4)) (sz 1)) : Prims.unit =
-  r#unsized (let list = [Rust_primitives.unsize (x.[ sz 0 ] <: t_Array u8 (sz 4)) <: t_Slice u8] in
+  r#unsized (let list = [x.[ sz 0 ] <: t_Slice u8] in
       FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
       Rust_primitives.Hax.array_of_list 1 list)
 '''