diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml index 0ead59bd5..bd8d3a5cd 100644 --- a/engine/backends/fstar/fstar_ast.ml +++ b/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 diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 3518e40c4..f77e8fc1f 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/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,21 +1586,18 @@ 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) ] @@ -1583,8 +1605,8 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items 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 diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 3b1c6e56b..95778622b 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/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 diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index 944089d01..5695dd087 100644 --- a/engine/bin/lib.ml +++ b/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 diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index f1f2550db..eb0cd442b 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1440,29 +1440,66 @@ let cast_of_enum typ_name generics typ thir_span in { v; span; ident; attrs = [] } -let rec c_item ~ident ~drop_body (item : Thir.item) : item list = +let rec c_item ~ident ~type_only (item : Thir.item) : item list = try Span.with_owner_hint item.owner_id (fun _ -> - c_item_unwrapped ~ident ~drop_body item) + c_item_unwrapped ~ident ~type_only item) with Diagnostics.SpanFreeError.Exn payload -> let context, kind = Diagnostics.SpanFreeError.payload payload in let error = Diagnostics.pretty_print_context_kind context kind in let span = Span.of_thir item.span in [ make_hax_error_item span ident error ] -and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = +and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = let open (val make ~krate:item.owner_id.contents.value.krate : EXPR) in if should_skip item.attributes then [] else let span = Span.of_thir item.span in let attrs = c_item_attrs item.attributes in + (* this is true if the user explicilty requested to erase using the `opaque` macro *) + let erased_by_user attrs = + Attr_payloads.payloads attrs + |> List.exists ~f:(fst >> [%matches? (Erased : Types.ha_payload)]) + in + let item_erased_by_user = erased_by_user attrs in + let type_only = + type_only + && Attr_payloads.payloads attrs + |> List.exists ~f:(fst >> [%matches? (NeverErased : Types.ha_payload)]) + |> not + in + (* This is true if the item should be erased because we are in type-only mode + (Only certain kinds of items are erased in this case). *) + let erased_by_type_only = + type_only + && + match item.kind with + | Fn _ | Static _ -> true + | Impl { of_trait = Some _; items; _ } + when List.exists items ~f:(fun item -> + match item.kind with Type _ -> true | _ -> false) + |> not -> + true + | _ -> false + in + (* If the item is erased in type-only mode we need to add the Erased attribute. + It is already present if the item is erased by user. *) + let attrs_with_erased erased_by_type_only erased_by_user attrs = + if erased_by_type_only && not erased_by_user then + Attr_payloads.to_attr Erased span :: attrs + else attrs + in + let attrs = + attrs_with_erased erased_by_type_only item_erased_by_user attrs + in + let erased = item_erased_by_user || erased_by_type_only in + let mk_one v = { span; v; ident; attrs } in let mk v = [ mk_one v ] in let drop_body = - drop_body + erased && Attr_payloads.payloads attrs - |> List.exists - ~f:(fst >> [%matches? (NeverDropBody : Types.ha_payload)]) + |> List.exists ~f:(fst >> [%matches? (NeverErased : Types.ha_payload)]) |> not in let c_body = if drop_body then c_expr_drop_body else c_expr in @@ -1475,7 +1512,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = name = Concrete_ident.of_def_id Value (Option.value_exn item.def_id); generics = c_generics generics; - body = c_expr body; + body = c_body body; params = []; safety = Safe; } @@ -1499,6 +1536,12 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = params = c_fn_params item.span params; safety = csafety safety; } + | (Enum (_, generics, _) | Struct (_, generics)) when erased -> + let generics = c_generics generics in + let is_struct = match item.kind with Struct _ -> true | _ -> false in + let def_id = Option.value_exn item.def_id in + let name = Concrete_ident.of_def_id Type def_id in + mk @@ Type { name; generics; variants = []; is_struct } | Enum (variants, generics, repr) -> let def_id = Option.value_exn item.def_id in let generics = c_generics generics in @@ -1628,6 +1671,13 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = List.map ~f:(fun (item : Thir.impl_item) -> let item_def_id = Concrete_ident.of_def_id Impl item.owner_id in + let attrs = c_item_attrs item.attributes in + let sub_item_erased_by_user = erased_by_user attrs in + let sub_item_erased = sub_item_erased_by_user || type_only in + let attrs = + attrs_with_erased type_only sub_item_erased_by_user attrs + in + let c_body = if sub_item_erased then c_expr_drop_body else c_body in let v = match (item.kind : Thir.impl_item_kind) with @@ -1663,7 +1713,6 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = (https://doc.rust-lang.org/reference/items/implementations.html#inherent-implementations)." in let ident = Concrete_ident.of_def_id Value item.owner_id in - let attrs = c_item_attrs item.attributes in { span = Span.of_thir item.span; v; ident; attrs }) items | Impl @@ -1681,11 +1730,66 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = ~f:(fun { attributes; _ } -> not (should_skip attributes)) items in - let has_type = - List.exists items ~f:(fun item -> - match item.kind with Type _ -> true | _ -> false) + let items = + if erased then + [ + (* Dummy associated item *) + { + ii_span = Span.of_thir item.span; + ii_generics = { params = []; constraints = [] }; + ii_v = + IIFn + { + body = U.unit_expr span; + params = [ U.make_unit_param span ]; + }; + ii_ident = + Concrete_ident.of_name Value + Rust_primitives__hax__dropped_body; + ii_attrs = []; + }; + ] + else + List.map + ~f:(fun (item : Thir.impl_item) -> + (* TODO: introduce a Kind.TraitImplItem or + something. Otherwise we have to assume every + backend will see traits and impls as + records. See https://github.com/hacspec/hax/issues/271. *) + let ii_ident = Concrete_ident.of_def_id Field item.owner_id in + { + ii_span = Span.of_thir item.span; + ii_generics = c_generics item.generics; + ii_v = + (match (item.kind : Thir.impl_item_kind) with + | Fn { body; params; _ } -> + let params = + if List.is_empty params then + [ U.make_unit_param span ] + else List.map ~f:(c_param item.span) params + in + IIFn { body = c_expr body; params } + | Const (_ty, e) -> IIFn { body = c_expr e; params = [] } + | Type { ty; parent_bounds } -> + IIType + { + typ = c_ty item.span ty; + parent_bounds = + List.filter_map + ~f:(fun (clause, impl_expr, span) -> + let* bound = c_clause span clause in + match bound with + | GCType trait_goal -> + Some + (c_impl_expr span impl_expr, trait_goal) + | _ -> None) + parent_bounds; + }); + ii_ident; + ii_attrs = c_item_attrs item.attributes; + }) + items in - let c_e = if has_type then c_expr else c_body in mk @@ Impl { @@ -1695,49 +1799,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = ( Concrete_ident.of_def_id Trait of_trait.def_id, List.map ~f:(c_generic_value item.span) of_trait.generic_args ); - items = - List.map - ~f:(fun (item : Thir.impl_item) -> - (* TODO: introduce a Kind.TraitImplItem or - something. Otherwise we have to assume every - backend will see traits and impls as - records. See https://github.com/hacspec/hax/issues/271. *) - let ii_ident = - Concrete_ident.of_def_id Field item.owner_id - in - { - ii_span = Span.of_thir item.span; - ii_generics = c_generics item.generics; - ii_v = - (match (item.kind : Thir.impl_item_kind) with - | Fn { body; params; _ } -> - let params = - if List.is_empty params then - [ U.make_unit_param span ] - else List.map ~f:(c_param item.span) params - in - IIFn { body = c_e body; params } - | Const (_ty, e) -> IIFn { body = c_e e; params = [] } - | Type { ty; parent_bounds } -> - IIType - { - typ = c_ty item.span ty; - parent_bounds = - List.filter_map - ~f:(fun (clause, impl_expr, span) -> - let* bound = c_clause span clause in - match bound with - | GCType trait_goal -> - Some - ( c_impl_expr span impl_expr, - trait_goal ) - | _ -> None) - parent_bounds; - }); - ii_ident; - ii_attrs = c_item_attrs item.attributes; - }) - items; + items; parent_bounds = List.filter_map ~f:(fun (clause, impl_expr, span) -> @@ -1787,7 +1849,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = | TraitAlias _ -> mk NotImplementedYet -let import_item ~drop_body (item : Thir.item) : +let import_item ~type_only (item : Thir.item) : concrete_ident * (item list * Diagnostics.t list) = let ident = Concrete_ident.of_def_id Value item.owner_id in let r, reports = @@ -1797,6 +1859,6 @@ let import_item ~drop_body (item : Thir.item) : >> U.Reducers.disambiguate_local_idents in Diagnostics.Core.capture (fun _ -> - c_item item ~ident ~drop_body |> List.map ~f) + c_item item ~ident ~type_only |> List.map ~f) in (ident, (r, reports)) diff --git a/engine/lib/import_thir.mli b/engine/lib/import_thir.mli index 42a5f2184..370af4c05 100644 --- a/engine/lib/import_thir.mli +++ b/engine/lib/import_thir.mli @@ -5,6 +5,6 @@ val import_clause : Types.span -> Types.clause -> Ast.Rust.generic_constraint option val import_item : - drop_body:bool -> + type_only:bool -> Types.item_for__decorated_for__expr_kind -> Concrete_ident.t * (Ast.Rust.item list * Diagnostics.t list) diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs index 5134763c6..429e04dea 100644 --- a/hax-lib/macros/src/dummy.rs +++ b/hax-lib/macros/src/dummy.rs @@ -29,7 +29,9 @@ identity_proc_macro_attribute!( process_init, process_write, process_read, + opaque, opaque_type, + transparent, refinement_type, fstar_replace, coq_replace, diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs index f71f1891c..2189232c7 100644 --- a/hax-lib/macros/src/implementation.rs +++ b/hax-lib/macros/src/implementation.rs @@ -249,8 +249,8 @@ pub fn lemma(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { ); } } - use AttrPayload::NeverDropBody; - quote! { #attr #NeverDropBody #item }.into() + use AttrPayload::NeverErased; + quote! { #attr #NeverErased #item }.into() } /* @@ -617,13 +617,32 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr quote! { #item #(#extra_items)* }.into() } -/// Mark a struct or an enum opaque: the extraction will assume the +/// Mark an item opaque: the extraction will assume the /// type without revealing its definition. #[proc_macro_error] #[proc_macro_attribute] -pub fn opaque_type(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { +#[deprecated(note = "Please use 'opaque' instead")] +pub fn opaque_type(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + opaque(attr, item) +} + +/// Mark an item opaque: the extraction will assume the +/// type without revealing its definition. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn opaque(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: Item = parse_macro_input!(item); + let attr = AttrPayload::Erased; + quote! {#attr #item}.into() +} + +/// Mark an item transparent: the extraction will not +/// make it opaque regardless of the `-i` flag default. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn transparent(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { let item: Item = parse_macro_input!(item); - let attr = AttrPayload::OpaqueType; + let attr = AttrPayload::NeverErased; quote! {#attr #item}.into() } diff --git a/hax-lib/macros/src/quote.rs b/hax-lib/macros/src/quote.rs index d02bdea78..8d13591c4 100644 --- a/hax-lib/macros/src/quote.rs +++ b/hax-lib/macros/src/quote.rs @@ -141,14 +141,14 @@ pub(super) fn item( }; let kind_attr = AttrPayload::ItemQuote(kind); let status_attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true }); - use AttrPayload::NeverDropBody; + use AttrPayload::NeverErased; quote! { #assoc_attr #item #attribute_to_inject #status_attr const _: () = { - #NeverDropBody + #NeverErased #uid_attr #kind_attr fn quote_contents() { diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs index c1c974a39..35fe0fa76 100644 --- a/hax-lib/macros/src/utils.rs +++ b/hax-lib/macros/src/utils.rs @@ -301,7 +301,7 @@ pub fn make_fn_decoration( } else { quote! {} }; - use AttrPayload::NeverDropBody; + use AttrPayload::NeverErased; quote! { #[cfg(#DebugOrHaxCfgExpr)] #late_skip @@ -312,7 +312,7 @@ pub fn make_fn_decoration( #uid_attr #late_skip #[allow(unused)] - #NeverDropBody + #NeverErased #decoration_sig { #phi } diff --git a/hax-lib/macros/types/src/lib.rs b/hax-lib/macros/types/src/lib.rs index bbb1d4575..b342a1355 100644 --- a/hax-lib/macros/types/src/lib.rs +++ b/hax-lib/macros/types/src/lib.rs @@ -118,7 +118,7 @@ pub enum AttrPayload { /// Mark an item so that hax never drop its body (this is useful /// for pre- and post- conditions of a function we dropped the /// body of: pre and post are part of type signature) - NeverDropBody, + NeverErased, NewtypeAsRefinement, /// Mark an item as a lemma statement to prove in the backend Lemma, @@ -130,8 +130,8 @@ pub enum AttrPayload { PVConstructor, PVHandwritten, TraitMethodNoPrePost, - /// Make a type opaque - OpaqueType, + /// Make an item opaque + Erased, } pub const HAX_TOOL: &str = "_hax"; diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs index 866c7cfda..65136716f 100644 --- a/hax-lib/src/proc_macros.rs +++ b/hax-lib/src/proc_macros.rs @@ -2,8 +2,8 @@ //! proc-macro crate cannot export anything but procedural macros. pub use hax_lib_macros::{ - attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque_type, - refinement_type, requires, trait_fn_decoration, + attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque, + opaque_type, refinement_type, requires, trait_fn_decoration, transparent, }; pub use hax_lib_macros::{ diff --git a/hax-types/src/cli_options/mod.rs b/hax-types/src/cli_options/mod.rs index f84795be7..d8b1a6551 100644 --- a/hax-types/src/cli_options/mod.rs +++ b/hax-types/src/cli_options/mod.rs @@ -303,7 +303,8 @@ pub struct TranslationOptions { /// {n} - `+:`: only includes the type of the selected items (no /// dependencies). This includes full struct and enums, but only - /// the type signature of functions, dropping their bodies. + /// the type signature of functions and trait impls (except when + /// they contain associated types), dropping their bodies. #[arg( value_parser = parse_inclusion_clause, value_delimiter = ' ', 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..6373c0b9e 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -29,13 +29,124 @@ stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs' diagnostics = [] [stdout.files] +"Attribute_opaque.fst" = ''' +module Attribute_opaque +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +assume +val t_OpaqueEnum': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype + +let t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) = t_OpaqueEnum' v_X v_T v_U + +assume +val t_OpaqueStruct': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype + +let t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) = t_OpaqueStruct' v_X v_T v_U + +assume +val impl__S1__f_s1': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True) + +let impl__S1__f_s1 = impl__S1__f_s1' + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_2': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32 v_U + +let impl_2 (#v_U: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_U) = + impl_2' #v_U #i1 + +assume +val impl__S2__f_s2': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True) + +let impl__S2__f_s2 = impl__S2__f_s2' + +assume +val v_C': u8 + +let v_C = v_C' + +assume +val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) + +let f = f' + +assume +val ff_generic': v_X: usize -> #v_T: Type0 -> #v_U: Type0 -> x: v_U + -> Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True) + +let ff_generic (v_X: usize) (#v_T #v_U: Type0) = ff_generic' v_X #v_T #v_U + +assume +val ff_pre_post': x: bool -> y: bool + -> Prims.Pure bool + (requires x) + (ensures + fun result -> + let result:bool = result in + result =. y) + +let ff_pre_post = ff_pre_post' + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_T_for_u8': t_T u8 + +let impl_T_for_u8 = impl_T_for_u8' +''' "Attribute_opaque.fsti" = ''' module Attribute_opaque #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 +type t_S1 = | S1 : t_S1 + +type t_S2 = | S2 : t_S2 + +val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : eqtype + +val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : eqtype + +class t_TrGeneric (v_Self: Type0) (v_U: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_6168282666194871449:Core.Clone.t_Clone v_U; + f_f_pre:v_U -> Type0; + f_f_post:v_U -> v_Self -> Type0; + f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result) +} + +val impl__S1__f_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True) + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_2 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U + +val impl__S2__f_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True) + +val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) + +val ff_generic (v_X: usize) (#v_T #v_U: Type0) (x: v_U) + : Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True) + +val ff_pre_post (x y: bool) + : Prims.Pure bool + (requires x) + (ensures + fun result -> + let result:bool = result in + result =. y) + +class t_T (v_Self: Type0) = { + f_U:Type0; + f_c:u8; + f_d_pre:Prims.unit -> Type0; + f_d_post:Prims.unit -> Prims.unit -> Type0; + f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result); + f_m_pre:self___: v_Self -> x: u8 -> pred: Type0{x =. 0uy ==> pred}; + f_m_post:v_Self -> u8 -> bool -> Type0; + f_m:x0: v_Self -> x1: u8 -> Prims.Pure bool (f_m_pre x0 x1) (fun result -> f_m_post x0 x1 result) +} -val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_T_for_u8:t_T u8 ''' 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..dcdee90a4 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -27,7 +27,7 @@ stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs' diagnostics = [] [stdout.files] -"Interface_only.fsti" = ''' +"Interface_only.fst" = ''' module Interface_only #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core @@ -39,34 +39,89 @@ type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } +class t_T2 (v_Self: Type0) = { + f_d_pre:Prims.unit -> Type0; + f_d_post:Prims.unit -> Prims.unit -> Type0; + f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result) +} + +/// Items can be forced to be transparent +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl_T2_for_u8: t_T2 u8 = + { + f_d_pre = (fun (_: Prims.unit) -> false); + f_d_post = (fun (_: Prims.unit) (out: Prims.unit) -> true); + f_d = fun (_: Prims.unit) -> () + } + /// Non-inherent implementations are extracted, their bodies are not /// dropped. This might be a bit surprising: see /// https://github.com/hacspec/hax/issues/616. [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl:Core.Convert.t_From t_Bar Prims.unit +assume +val impl': Core.Convert.t_From t_Bar Prims.unit + +let impl = impl' /// If you need to drop the body of a method, please hoist it: [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_1:Core.Convert.t_From t_Bar u8 +assume +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) +let impl_1 = impl_1' + +assume +val from__from': u8 -> t_Bar + +let from__from = from__from' [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_2 (#v_T: Type0) : Core.Convert.t_From (t_Holder v_T) Prims.unit +assume +val impl_2': #v_T: Type0 -> Core.Convert.t_From (t_Holder v_T) Prims.unit + +let impl_2 (#v_T: Type0) = impl_2' #v_T [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_Param v_SIZE) Prims.unit +assume +val impl_3': v_SIZE: usize -> Core.Convert.t_From (t_Param v_SIZE) Prims.unit + +let impl_3 (v_SIZE: usize) = impl_3' v_SIZE /// 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)) +assume +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) + +let f = f' + +assume +val ff_generic': v_X: usize -> #v_U: Type0 -> v__x: v_U -> t_Param v_X + +let ff_generic (v_X: usize) (#v_U: Type0) = ff_generic' v_X #v_U + +class t_T (v_Self: Type0) = { + f_Assoc:Type0; + f_d_pre:Prims.unit -> Type0; + f_d_post:Prims.unit -> Prims.unit -> Type0; + f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result) +} + +/// Impls with associated types are not erased +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl_T_for_u8: t_T u8 = + { + f_Assoc = u8; + f_d_pre = (fun (_: Prims.unit) -> true); + f_d_post = (fun (_: Prims.unit) (out: Prims.unit) -> true); + f_d = fun (_: Prims.unit) -> () + } ''' diff --git a/tests/attribute-opaque/src/lib.rs b/tests/attribute-opaque/src/lib.rs index 7840b4fa8..28671f800 100644 --- a/tests/attribute-opaque/src/lib.rs +++ b/tests/attribute-opaque/src/lib.rs @@ -1,11 +1,85 @@ -#[hax_lib::opaque_type] +#[hax_lib::opaque] struct OpaqueStruct { field: [T; X], other_field: U, } -#[hax_lib::opaque_type] +#[hax_lib::opaque] enum OpaqueEnum { A([T; X]), B(U), } + +#[hax_lib::opaque] +fn f_generic(x: U) -> OpaqueEnum { + OpaqueEnum::B(x) +} + +#[hax_lib::opaque] +fn f(x: bool, y: bool) -> bool { + x && y +} + +#[hax_lib::opaque] +#[hax_lib::requires(x)] +#[hax_lib::ensures(|result| result == y)] +fn f_pre_post(x: bool, y: bool) -> bool { + x && y +} + +#[hax_lib::attributes] +trait T { + type U; + const c: u8; + fn d(); + #[hax_lib::requires(x == 0)] + fn m(&self, x: u8) -> bool; +} + +#[hax_lib::attributes] +#[hax_lib::opaque] +impl T for u8 { + type U = u8; + const c: u8 = 0; + fn d() { + unsafe { + let my_num: i32 = 10; + let _my_num_ptr: *const i32 = &my_num; + let mut my_speed: i32 = 88; + let _my_speed_ptr: *mut i32 = &mut my_speed; + } + } + #[hax_lib::requires(x == 0)] + #[hax_lib::ensures(|result| result)] + fn m(&self, x: u8) -> bool { + *self >= x + } +} + +trait TrGeneric { + fn f(x: U) -> Self; +} + +#[hax_lib::opaque] +impl TrGeneric for i32 { + fn f(_x: U) -> Self { + 0 + } +} + +#[hax_lib::opaque] +const C: u8 = 0 + 0; + +struct S1(); + +impl S1 { + #[hax_lib::opaque] + fn f_s1() {} +} + +struct S2(); + +#[hax_lib::opaque] +impl S2 { + fn f_s2() {} +} diff --git a/tests/cli/interface-only/src/lib.rs b/tests/cli/interface-only/src/lib.rs index 411c3de99..1e85ef7fe 100644 --- a/tests/cli/interface-only/src/lib.rs +++ b/tests/cli/interface-only/src/lib.rs @@ -65,3 +65,29 @@ impl From<()> for Param { Param { value: [0; SIZE] } } } + +fn f_generic(_x: U) -> Param { + Param { value: [0; X] } +} + +trait T { + type Assoc; + fn d(); +} + +/// Impls with associated types are not erased +impl T for u8 { + type Assoc = u8; + fn d() {} +} +trait T2 { + fn d(); +} + +/// Items can be forced to be transparent +#[hax_lib::transparent] +#[hax_lib::attributes] +impl T2 for u8 { + #[hax_lib::requires(false)] + fn d() {} +}