Merge pull request #1134 from hacspec/opaque-extensions

Opaque extensions

engine/backends/fstar/fstar_ast.ml

@@ -9,6 +9,7 @@ module Ident = FStar_Ident
 
 let dummyRange = Range.dummyRange
 let id ident = Ident.mk_ident (ident, dummyRange)
+let id_prime (ident : Ident.ident) = id (ident.idText ^ "'")
 
 let lid path =
   let init, last = List.(drop_last_exn path, last_exn path) in
@@ -87,6 +88,7 @@ let mk_refined (x : string) (typ : AST.term) (phi : x:AST.term -> AST.term) =
   term @@ AST.Refine (x_bd, phi (term @@ AST.Var (lid_of_id x)))
 
 let type0_term = AST.Name (lid [ "Type0" ]) |> term
+let eqtype_term = AST.Name (lid [ "eqtype" ]) |> term
 
 let parse_string f s =
   let open FStar_Parser_ParseIt in

engine/backends/fstar/fstar_backend.ml

@@ -875,6 +875,34 @@ struct
       | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
+    let is_erased =
+      Attrs.find_unique_attr e.attrs
+        ~f:([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ())
+      |> Option.is_some
+    in
+    let erased_impl name ty attrs binders =
+      let name' = F.id_prime name in
+      let pat = F.AST.PatVar (name, None, []) in
+      let term = F.term @@ F.AST.Var (F.lid_of_id @@ name') in
+      let pat, term =
+        match binders with
+        | [] -> (pat, term)
+        | _ ->
+            ( F.AST.PatApp
+                (F.pat pat, List.map ~f:FStarBinder.to_pattern binders),
+              List.fold_left binders ~init:term ~f:(fun term binder ->
+                  let binder_term, binder_imp =
+                    FStarBinder.to_qualified_term binder
+                  in
+                  F.term @@ F.AST.App (term, binder_term, binder_imp)) )
+      in
+      [
+        F.decl ~quals:[ Assumption ] ~fsti:false ~attrs
+        @@ F.AST.Assume (name', ty);
+        F.decl ~fsti:false
+        @@ F.AST.TopLevelLet (NoLetQualifier, [ (F.pat @@ pat, term) ]);
+      ]
+    in
     match e.v with
     | Alias { name; item } ->
         (* These should come from bundled items (in the case of cyclic module dependencies).
@@ -939,7 +967,12 @@ struct
         in
 
         let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in
-        if interface_mode then [ impl; intf ] else [ full ]
+
+        let erased = erased_impl name arrow_typ [] generics in
+        let impl, full =
+          if is_erased then (erased, erased) else ([ impl ], [ full ])
+        in
+        if interface_mode then intf :: impl else full
     | TyAlias { name; generics; ty } ->
         let pat =
           F.pat
@@ -972,31 +1005,20 @@ struct
                             |> List.map ~f:to_pattern) ),
                    ty );
                ] )
-    | Type { name; generics; _ }
-      when Attrs.find_unique_attr e.attrs
-             ~f:([%eq: Types.ha_payload] OpaqueType >> Fn.flip Option.some_if ())
-           |> Option.is_some ->
-        if not ctx.interface_mode then
-          Error.raise
-          @@ {
-               kind =
-                 AttributeRejected
-                   {
-                     reason =
-                       "a type cannot be opaque if its module is not extracted \
-                        as an interface";
-                   };
-               span = e.span;
-             }
-        else
-          let generics = FStarBinder.of_generics e.span generics in
-          let ty = F.type0_term in
-          let arrow_typ =
-            F.term
-            @@ F.AST.Product (List.map ~f:FStarBinder.to_binder generics, ty)
-          in
-          let name = F.id @@ U.Concrete_ident_view.to_definition_name name in
-          [ F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) ]
+    | Type { name; generics; _ } when is_erased ->
+        let generics =
+          FStarBinder.of_generics e.span generics
+          |> List.map ~f:FStarBinder.implicit_to_explicit
+        in
+        let ty = F.eqtype_term in
+        let arrow_typ =
+          F.term
+          @@ F.AST.Product (List.map ~f:FStarBinder.to_binder generics, ty)
+        in
+        let name = F.id @@ U.Concrete_ident_view.to_definition_name name in
+        let erased = erased_impl name arrow_typ [] generics in
+        let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in
+        if ctx.interface_mode then intf :: erased else erased
     | Type
         {
           name;
@@ -1476,15 +1498,20 @@ struct
           List.exists items ~f:(fun { ii_v; _ } ->
               match ii_v with IIType _ -> true | _ -> false)
         in
-        let impl_val = ctx.interface_mode && not has_type in
         let let_impl = F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]) in
-        if impl_val then
-          let generics_binders = List.map ~f:FStarBinder.to_binder generics in
-          let val_type = F.term @@ F.AST.Product (generics_binders, typ) in
-          let v = F.AST.Val (name, val_type) in
-          (F.decls ~fsti:true ~attrs:[ tcinst ] @@ v)
-          @ F.decls ~fsti:false ~attrs:[ tcinst ] let_impl
-        else F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ] let_impl
+        let generics_binders = List.map ~f:FStarBinder.to_binder generics in
+        let val_type = F.term @@ F.AST.Product (generics_binders, typ) in
+        let v = F.AST.Val (name, val_type) in
+        let intf = F.decls ~fsti:true ~attrs:[ tcinst ] v in
+        let impl =
+          if is_erased then erased_impl name val_type [ tcinst ] generics
+          else
+            F.decls
+              ~fsti:(ctx.interface_mode && has_type)
+              ~attrs:[ tcinst ] let_impl
+        in
+        let intf = if has_type && not is_erased then [] else intf in
+        if ctx.interface_mode then intf @ impl else impl
     | Quote { quote; _ } ->
         let fstar_opts =
           Attrs.find_unique_attr e.attrs ~f:(function
@@ -1530,8 +1557,7 @@ let make (module M : Attrs.WITH_ITEMS) ctx =
               let ctx = ctx
             end) : S)
 
-let strings_of_item ~signature_only (bo : BackendOptions.t) m items
-    (item : item) :
+let strings_of_item (bo : BackendOptions.t) m items (item : item) :
     ([> `Impl of string | `Intf of string ] * [ `NoNewline | `Newline ]) list =
   let interface_mode' : Types.inclusion_kind =
     List.rev bo.interfaces
@@ -1549,8 +1575,7 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
     |> Option.value ~default:(Types.Excluded : Types.inclusion_kind)
   in
   let interface_mode =
-    signature_only
-    || not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode')
+    not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode')
   in
   let (module Print) =
     make m
@@ -1561,30 +1586,27 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
         line_width = bo.line_width;
       }
   in
-  let mk_impl = if interface_mode then fun i -> `Impl i else fun i -> `Impl i in
+  let mk_impl i = `Impl i in
   let mk_intf = if interface_mode then fun i -> `Intf i else fun i -> `Impl i in
   let no_impl =
-    signature_only
-    || [%matches? (Types.Included None' : Types.inclusion_kind)] interface_mode'
+    [%matches? (Types.Included None' : Types.inclusion_kind)] interface_mode'
   in
   Print.pitem item
   |> List.filter ~f:(function `Impl _ when no_impl -> false | _ -> true)
   |> List.concat_map ~f:(function
        | `Impl i -> [ (mk_impl (Print.decl_to_string i), `Newline) ]
        | `Intf i -> [ (mk_intf (Print.decl_to_string i), `Newline) ]
-       | `VerbatimIntf (s, nl) ->
-           [ ((if interface_mode then `Intf s else `Impl s), nl) ]
-       | `VerbatimImpl (s, nl) ->
-           [ ((if interface_mode then `Impl s else `Impl s), nl) ]
+       | `VerbatimIntf (s, nl) -> [ (mk_intf s, nl) ]
+       | `VerbatimImpl (s, nl) -> [ (`Impl s, nl) ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
            if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ]
            else [ (`Impl s, `Newline) ])
 
 type rec_prefix = NonRec | FirstMutRec | MutRec
 
-let string_of_items ~signature_only ~mod_name ~bundles (bo : BackendOptions.t) m
-    items : string * string =
+let string_of_items ~mod_name ~bundles (bo : BackendOptions.t) m items :
+    string * string =
   let collect_trait_goal_idents =
     object
       inherit [_] Visitors.reduce as super
@@ -1657,7 +1679,7 @@ let string_of_items ~signature_only ~mod_name ~bundles (bo : BackendOptions.t) m
     List.concat_map
       ~f:(fun item ->
         let recursivity_prefix = get_recursivity_prefix item in
-        let strs = strings_of_item ~signature_only bo m items item in
+        let strs = strings_of_item bo m items item in
         match (recursivity_prefix, item.v) with
         | FirstMutRec, Fn _ ->
             replace_in_strs ~pattern:"let" ~with_:"let rec" strs
@@ -1710,20 +1732,8 @@ let translate_as_fstar m (bo : BackendOptions.t) ~(bundles : AST.item list list)
   U.group_items_by_namespace items
   |> Map.to_alist
   |> List.concat_map ~f:(fun (ns, items) ->
-         let signature_only =
-           let is_dropped_body =
-             Concrete_ident.eq_name Rust_primitives__hax__dropped_body
-           in
-           let contains_dropped_body =
-             U.Reducers.collect_concrete_idents#visit_item ()
-             >> Set.exists ~f:is_dropped_body
-           in
-           List.exists ~f:contains_dropped_body items
-         in
          let mod_name = module_name ns in
-         let impl, intf =
-           string_of_items ~signature_only ~mod_name ~bundles bo m items
-         in
+         let impl, intf = string_of_items ~mod_name ~bundles bo m items in
          let make ~ext body =
            if String.is_empty body then None
            else

engine/backends/proverif/proverif_backend.ml

@@ -630,8 +630,7 @@ module Make (Options : OPTS) : MAKE = struct
               if
                 Attrs.find_unique_attr item.attrs
                   ~f:
-                    ([%eq: Types.ha_payload] OpaqueType
-                    >> Fn.flip Option.some_if ())
+                    ([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ())
                 |> Option.is_some
               then default_lines
               else default_lines ^^ destructor_lines

engine/bin/lib.ml

@@ -36,14 +36,14 @@ let import_thir_items (include_clauses : Types.inclusion_clause list)
             include_clauses
           |> List.last
         in
-        let drop_body =
+        let type_only =
           (* Shall we drop the body? *)
           Option.map
             ~f:(fun clause -> [%matches? Types.SignatureOnly] clause.kind)
             most_precise_clause
           |> Option.value ~default:false
         in
-        Import_thir.import_item ~drop_body item)
+        Import_thir.import_item ~type_only item)
       items
     |> List.map ~f:snd
   in