Merge pull request #856 from hacspec/remove-unsize-for-certain-types

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)
 '''