From e2aa8b82f00fa8fe40ce8b9b41ae7e069674004e Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 26 Nov 2024 13:35:36 +0100 Subject: [PATCH 01/16] Unify (an extended version of) opaque and interface-only in a single erasure mechanism. --- engine/backends/fstar/fstar_ast.ml | 1 + engine/backends/fstar/fstar_backend.ml | 76 +++++----- engine/backends/proverif/proverif_backend.ml | 3 +- engine/bin/lib.ml | 4 +- engine/lib/import_thir.ml | 149 ++++++++++++------- engine/lib/import_thir.mli | 2 +- hax-lib/macros/src/dummy.rs | 1 + hax-lib/macros/src/implementation.rs | 13 +- hax-lib/macros/types/src/lib.rs | 4 +- hax-lib/src/proc_macros.rs | 4 +- 10 files changed, 153 insertions(+), 104 deletions(-) diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml index 0ead59bd5..0906c846c 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 diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index f179ffe38..0f9fc288c 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -874,6 +874,26 @@ 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 = + let name' = F.id_prime name in + + [ + F.decl ~quals:[ Assumption ] ~fsti:false ~attrs + @@ F.AST.Assume (name', ty); + F.decl ~fsti:false + @@ F.AST.TopLevelLet + ( NoLetQualifier, + [ + ( F.pat @@ F.AST.PatVar (name, None, []), + F.term @@ F.AST.Var (F.lid_of_id @@ name') ); + ] ); + ] + in match e.v with | Alias { name; item } -> (* These should come from bundled items (in the case of cyclic module dependencies). @@ -938,7 +958,10 @@ struct in let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in - if interface_mode then [ impl; intf ] else [ full ] + + if is_erased then intf :: erased_impl name arrow_typ [] + else if interface_mode then [ impl; intf ] + else [ full ] | TyAlias { name; generics; ty } -> let pat = F.pat @@ -971,10 +994,7 @@ 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 -> + | Type { name; generics; _ } when is_erased -> if not ctx.interface_mode then Error.raise @@ { @@ -1471,18 +1491,13 @@ struct in let body = F.term @@ F.AST.Record (None, fields) in let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in - let has_type = - 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 + if is_erased 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 + @ erased_impl name val_type [ tcinst ] else F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ] let_impl | Quote { quote; _ } -> let fstar_opts = @@ -1529,8 +1544,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 @@ -1548,8 +1562,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 @@ -1560,21 +1573,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) ] @@ -1582,8 +1592,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 @@ -1656,7 +1666,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 @@ -1709,20 +1719,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..34f9624a5 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1440,26 +1440,49 @@ 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 + let erased_by_user = + Attr_payloads.payloads attrs + |> List.exists ~f:(fst >> [%matches? (Erased : Types.ha_payload)]) + in + 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 + let attrs = + if erased_by_type_only && not erased_by_user then + Attr_payloads.to_attr Erased span :: attrs + else attrs + in + let erased = 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)]) @@ -1475,7 +1498,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 +1522,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 @@ -1681,11 +1710,65 @@ 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 + [ + { + 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 +1778,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 +1828,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 +1838,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..8b40ac9b3 100644 --- a/hax-lib/macros/src/dummy.rs +++ b/hax-lib/macros/src/dummy.rs @@ -29,6 +29,7 @@ identity_proc_macro_attribute!( process_init, process_write, process_read, + opaque, opaque_type, refinement_type, fstar_replace, diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs index f71f1891c..4874b1671 100644 --- a/hax-lib/macros/src/implementation.rs +++ b/hax-lib/macros/src/implementation.rs @@ -621,9 +621,18 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr /// 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 a struct or an enum 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::OpaqueType; + let attr = AttrPayload::Erased; quote! {#attr #item}.into() } diff --git a/hax-lib/macros/types/src/lib.rs b/hax-lib/macros/types/src/lib.rs index bbb1d4575..0b12b90a8 100644 --- a/hax-lib/macros/types/src/lib.rs +++ b/hax-lib/macros/types/src/lib.rs @@ -130,8 +130,8 @@ pub enum AttrPayload { PVConstructor, PVHandwritten, TraitMethodNoPrePost, - /// Make a type opaque - OpaqueType, + /// Make something 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..d5f0684a3 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, }; pub use hax_lib_macros::{ From 1af618e8d9ab4b13b77c73690dc312d1a18ba078 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 27 Nov 2024 11:10:33 +0100 Subject: [PATCH 02/16] Add tests for opaque attribute. --- tests/attribute-opaque/src/lib.rs | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/tests/attribute-opaque/src/lib.rs b/tests/attribute-opaque/src/lib.rs index 7840b4fa8..3124b8b06 100644 --- a/tests/attribute-opaque/src/lib.rs +++ b/tests/attribute-opaque/src/lib.rs @@ -9,3 +9,26 @@ enum OpaqueEnum { A([T; X]), B(U), } + +#[hax_lib::opaque] +fn f(x: bool, y: bool) -> bool { + x && y +} +trait T { + fn d(); +} + +#[hax_lib::opaque] +impl T for u8 { + 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::opaque] +const c: u8 = { 0 + 0 }; From f3fb4d557431ac1e0c2c3631edf040f5e64b44f4 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 28 Nov 2024 09:22:51 +0100 Subject: [PATCH 03/16] Tests snapshots. --- ...oolchain__attribute-opaque into-fstar.snap | 53 ++++++++++++++++++- .../toolchain__interface-only into-fstar.snap | 44 ++++++++++++++- tests/attribute-opaque/src/lib.rs | 2 +- 3 files changed, 95 insertions(+), 4 deletions(-) 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..6a0d0e065 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -23,19 +23,70 @@ info: - +** --- exit = 0 -stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs' +stderr = ''' +warning: use of deprecated macro `hax_lib::opaque_type`: Please use 'opaque' instead + --> attribute-opaque/src/lib.rs:1:3 + | +1 | #[hax_lib::opaque_type] + | ^^^^^^^^^^^^^^^^^^^^ + | + = note: `#[warn(deprecated)]` on by default + +warning: use of deprecated macro `hax_lib::opaque_type`: Please use 'opaque' instead + --> attribute-opaque/src/lib.rs:7:3 + | +7 | #[hax_lib::opaque_type] + | ^^^^^^^^^^^^^^^^^^^^ + +warning: `attribute-opaque` (lib) generated 2 warnings + Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' [stdout] diagnostics = [] [stdout.files] +"Attribute_opaque.fst" = ''' +module Attribute_opaque +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_T_for_u8': t_T u8 + +let impl_T_for_u8 = impl_T_for_u8' + +assume +val c': u8 + +let c = c' + +assume +val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) + +let f = f' +''' "Attribute_opaque.fsti" = ''' module Attribute_opaque #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul +class t_T (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) +} + val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_T_for_u8:t_T u8 + +val c:u8 + +val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) ''' 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..ce2c3fe06 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 @@ -45,18 +45,47 @@ type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } [@@ FStar.Tactics.Typeclasses.tcinstance] val impl:Core.Convert.t_From t_Bar Prims.unit +[@@ FStar.Tactics.Typeclasses.tcinstance] +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 -val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True) +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_1': Core.Convert.t_From t_Bar u8 + +let impl_1 = impl_1' + +val from__from: u8 -> t_Bar + +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 +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_2': #v_T: Type0 -> Core.Convert.t_From (t_Holder v_T) Prims.unit + +let impl_2 = impl_2' + [@@ FStar.Tactics.Typeclasses.tcinstance] val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_Param v_SIZE) Prims.unit +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_3': v_SIZE: usize -> Core.Convert.t_From (t_Param v_SIZE) Prims.unit + +let impl_3 = impl_3' + /// 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. @@ -69,4 +98,15 @@ val f (x: u8) fun r -> let r:t_Array u8 (sz 4) = r in (r.[ sz 0 ] <: u8) >. x) + +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' ''' diff --git a/tests/attribute-opaque/src/lib.rs b/tests/attribute-opaque/src/lib.rs index 3124b8b06..6e262cd1b 100644 --- a/tests/attribute-opaque/src/lib.rs +++ b/tests/attribute-opaque/src/lib.rs @@ -31,4 +31,4 @@ impl T for u8 { } #[hax_lib::opaque] -const c: u8 = { 0 + 0 }; +const c: u8 = 0 + 0; From 3282b7e8ecf2ab17789aeaa4c29b8c7d3151b8b8 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 27 Nov 2024 11:41:21 +0100 Subject: [PATCH 04/16] Update documentation of -i flag. --- hax-types/src/cli_options/mod.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 = ' ', From ef18a4ff2b82b814e7877c65c8b8fc02a930af6e Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 27 Nov 2024 14:36:33 +0100 Subject: [PATCH 05/16] Allow to make opaque (and drop body) of selected (non-trait) impl methods. --- engine/lib/import_thir.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 34f9624a5..36750dee1 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1456,10 +1456,11 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = else let span = Span.of_thir item.span in let attrs = c_item_attrs item.attributes in - let erased_by_user = + 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 erased_by_type_only = type_only && @@ -1473,11 +1474,11 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = | _ -> false in let attrs = - if erased_by_type_only && not erased_by_user then + if erased_by_type_only && not item_erased_by_user then Attr_payloads.to_attr Erased span :: attrs else attrs in - let erased = erased_by_user || erased_by_type_only 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 @@ -1657,6 +1658,10 @@ and c_item_unwrapped ~ident ~type_only (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 sub_item_erased = + erased_by_user (c_item_attrs item.attributes) + 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 From 5574e816c7f3294f1b0a07838eee577e13983aaa Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 27 Nov 2024 15:03:33 +0100 Subject: [PATCH 06/16] Document and correct. --- engine/lib/import_thir.ml | 6 +++ hax-lib/macros/types/src/lib.rs | 2 +- ...oolchain__attribute-opaque into-fstar.snap | 40 +++++--------- .../toolchain__interface-only into-fstar.snap | 54 +++++++++---------- tests/attribute-opaque/src/lib.rs | 4 +- 5 files changed, 48 insertions(+), 58 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 36750dee1..20b37e25b 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1456,11 +1456,14 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = 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 + (* 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 && @@ -1473,6 +1476,8 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = 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 = if erased_by_type_only && not item_erased_by_user then Attr_payloads.to_attr Erased span :: attrs @@ -1718,6 +1723,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = let items = if erased then [ + (* Dummy associated item *) { ii_span = Span.of_thir item.span; ii_generics = { params = []; constraints = [] }; diff --git a/hax-lib/macros/types/src/lib.rs b/hax-lib/macros/types/src/lib.rs index 0b12b90a8..34c6aa1c8 100644 --- a/hax-lib/macros/types/src/lib.rs +++ b/hax-lib/macros/types/src/lib.rs @@ -130,7 +130,7 @@ pub enum AttrPayload { PVConstructor, PVHandwritten, TraitMethodNoPrePost, - /// Make something opaque + /// Make an item opaque Erased, } 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 6a0d0e065..9727c3f6d 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -23,23 +23,7 @@ info: - +** --- exit = 0 -stderr = ''' -warning: use of deprecated macro `hax_lib::opaque_type`: Please use 'opaque' instead - --> attribute-opaque/src/lib.rs:1:3 - | -1 | #[hax_lib::opaque_type] - | ^^^^^^^^^^^^^^^^^^^^ - | - = note: `#[warn(deprecated)]` on by default - -warning: use of deprecated macro `hax_lib::opaque_type`: Please use 'opaque' instead - --> attribute-opaque/src/lib.rs:7:3 - | -7 | #[hax_lib::opaque_type] - | ^^^^^^^^^^^^^^^^^^^^ - -warning: `attribute-opaque` (lib) generated 2 warnings - Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' +stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs' [stdout] diagnostics = [] @@ -51,6 +35,11 @@ module Attribute_opaque open Core open FStar.Mul +assume +val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) + +let f = f' + [@@ FStar.Tactics.Typeclasses.tcinstance] assume val impl_T_for_u8': t_T u8 @@ -61,11 +50,6 @@ assume val c': u8 let c = c' - -assume -val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) - -let f = f' ''' "Attribute_opaque.fsti" = ''' module Attribute_opaque @@ -73,20 +57,20 @@ module Attribute_opaque open Core open FStar.Mul +val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 + +val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 + +val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) + class t_T (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) } -val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 - -val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 - [@@ FStar.Tactics.Typeclasses.tcinstance] val impl_T_for_u8:t_T u8 val c:u8 - -val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) ''' 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 ce2c3fe06..3aafed2bc 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,31 @@ module Interface_only open Core open FStar.Mul -type t_Bar = | Bar : t_Bar +/// 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_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global } +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) -type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } +let f = f' + +type t_Bar = | Bar : t_Bar /// Non-inherent implementations are extracted, their bodies are not /// dropped. This might be a bit surprising: see @@ -68,6 +88,8 @@ val from__from': u8 -> t_Bar let from__from = from__from' +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 @@ -77,6 +99,8 @@ val impl_2': #v_T: Type0 -> Core.Convert.t_From (t_Holder v_T) Prims.unit let impl_2 = impl_2' +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 @@ -85,28 +109,4 @@ assume val impl_3': v_SIZE: usize -> Core.Convert.t_From (t_Param v_SIZE) Prims.unit let impl_3 = impl_3' - -/// 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) - -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' ''' diff --git a/tests/attribute-opaque/src/lib.rs b/tests/attribute-opaque/src/lib.rs index 6e262cd1b..30030a143 100644 --- a/tests/attribute-opaque/src/lib.rs +++ b/tests/attribute-opaque/src/lib.rs @@ -1,10 +1,10 @@ -#[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), From ed3ef5cb19ac24950a62b510a6137059037e2a28 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 27 Nov 2024 15:22:31 +0100 Subject: [PATCH 07/16] Allow opaque types even without interface mode. --- engine/backends/fstar/fstar_backend.ml | 29 +++++++------------------- 1 file changed, 8 insertions(+), 21 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 0f9fc288c..46cd5f3e5 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -995,27 +995,14 @@ struct ty ); ] ) | Type { name; generics; _ } when is_erased -> - 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)) ] + 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; From 30ec986d4d38de288ff3df115fe2554ba8b54904 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 27 Nov 2024 16:17:57 +0100 Subject: [PATCH 08/16] Add function signature only in interface mode. --- engine/backends/fstar/fstar_backend.ml | 8 +++++--- .../toolchain__attribute-opaque into-fstar.snap | 2 -- .../toolchain__interface-only into-fstar.snap | 10 ---------- 3 files changed, 5 insertions(+), 15 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 46cd5f3e5..e709eabe4 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -959,9 +959,11 @@ struct let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in - if is_erased then intf :: erased_impl name arrow_typ [] - else if interface_mode then [ impl; intf ] - else [ full ] + let erased = erased_impl name arrow_typ [] 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 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 9727c3f6d..20855a937 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -71,6 +71,4 @@ class t_T (v_Self: Type0) = { [@@ FStar.Tactics.Typeclasses.tcinstance] val impl_T_for_u8:t_T u8 - -val c: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 3aafed2bc..9f7a198e4 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -38,14 +38,6 @@ open FStar.Mul /// 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) - assume val f': x: u8 -> Prims.Pure (t_Array u8 (sz 4)) @@ -81,8 +73,6 @@ val impl_1': Core.Convert.t_From t_Bar u8 let impl_1 = impl_1' -val from__from: u8 -> t_Bar - assume val from__from': u8 -> t_Bar From cdcd4fbc4b3a157b6503dfd3685dc6ad60e35474 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 28 Nov 2024 10:27:12 +0100 Subject: [PATCH 09/16] New tests snapshots. --- ...oolchain__attribute-opaque into-fstar.snap | 22 +++++------ .../toolchain__interface-only into-fstar.snap | 38 +++++++++---------- 2 files changed, 30 insertions(+), 30 deletions(-) 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 20855a937..5a570c019 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -35,11 +35,6 @@ module Attribute_opaque open Core open FStar.Mul -assume -val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) - -let f = f' - [@@ FStar.Tactics.Typeclasses.tcinstance] assume val impl_T_for_u8': t_T u8 @@ -50,6 +45,11 @@ assume val c': u8 let c = c' + +assume +val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) + +let f = f' ''' "Attribute_opaque.fsti" = ''' module Attribute_opaque @@ -57,18 +57,18 @@ module Attribute_opaque open Core open FStar.Mul -val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 - -val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 - -val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) - class t_T (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) } +val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 + +val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 + [@@ FStar.Tactics.Typeclasses.tcinstance] val impl_T_for_u8:t_T u8 + +val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) ''' 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 9f7a198e4..ac6be840d 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -33,23 +33,11 @@ module Interface_only open Core open FStar.Mul -/// 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. -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) +type t_Bar = | Bar : t_Bar -let f = f' +type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global } -type t_Bar = | Bar : t_Bar +type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } /// Non-inherent implementations are extracted, their bodies are not /// dropped. This might be a bit surprising: see @@ -78,8 +66,6 @@ val from__from': u8 -> t_Bar let from__from = from__from' -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 @@ -89,8 +75,6 @@ val impl_2': #v_T: Type0 -> Core.Convert.t_From (t_Holder v_T) Prims.unit let impl_2 = impl_2' -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 @@ -99,4 +83,20 @@ assume val impl_3': v_SIZE: usize -> Core.Convert.t_From (t_Param v_SIZE) Prims.unit let impl_3 = impl_3' + +/// 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. +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' ''' From f300ff8209ea7e9f8282f0ae3603bdbef55b94e8 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 28 Nov 2024 14:47:28 +0100 Subject: [PATCH 10/16] Remove body of methods inside impls in type-only mode. --- engine/lib/import_thir.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 20b37e25b..0918496a2 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1478,11 +1478,14 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = 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 = - if erased_by_type_only && not item_erased_by_user then + 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 @@ -1663,8 +1666,11 @@ and c_item_unwrapped ~ident ~type_only (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 sub_item_erased = - erased_by_user (c_item_attrs item.attributes) + 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 @@ -1702,7 +1708,6 @@ and c_item_unwrapped ~ident ~type_only (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 From a9f56d8e7753d806b627bfcbca3ee528bbe70e9b Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 5 Dec 2024 10:29:50 +0100 Subject: [PATCH 11/16] Pass generic arguments to erased impls. --- engine/backends/fstar/fstar_ast.ml | 1 + engine/backends/fstar/fstar_backend.ml | 51 +++++++++++++++++++------- 2 files changed, 39 insertions(+), 13 deletions(-) diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml index 0906c846c..bd8d3a5cd 100644 --- a/engine/backends/fstar/fstar_ast.ml +++ b/engine/backends/fstar/fstar_ast.ml @@ -88,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 e709eabe4..29c45bfa4 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -879,19 +879,39 @@ struct ~f:([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ()) |> Option.is_some in - let erased_impl name ty attrs = + let erased_impl name ty attrs binders = let name' = F.id_prime name in - + (* let arguments = + match F.AST.(ty.tm) with + | F.AST.Product (binders, _) -> binders + | _ -> [] + in + let generics_names = + arguments + |> List.filter_map ~f:(fun arg -> + match F.AST.(arg.aqual, arg.b) with + | Some ((Implicit | TypeClassArg) as arg), F.AST.Annotated (name, _) -> Some (name, arg) + | _ -> None) + 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 @@ F.AST.PatVar (name, None, []), - F.term @@ F.AST.Var (F.lid_of_id @@ name') ); - ] ); + @@ F.AST.TopLevelLet (NoLetQualifier, [ (F.pat @@ pat, term) ]); ] in match e.v with @@ -959,7 +979,7 @@ struct let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in - let erased = erased_impl name arrow_typ [] in + let erased = erased_impl name arrow_typ [] generics in let impl, full = if is_erased then (erased, erased) else ([ impl ], [ full ]) in @@ -997,14 +1017,19 @@ struct ty ); ] ) | Type { name; generics; _ } when is_erased -> - let generics = FStarBinder.of_generics e.span generics in - let ty = F.type0_term in + 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 - [ F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) ] + 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; @@ -1486,7 +1511,7 @@ struct 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) - @ erased_impl name val_type [ tcinst ] + @ erased_impl name val_type [ tcinst ] generics else F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ] let_impl | Quote { quote; _ } -> let fstar_opts = From cc2a7f93593fa27005a82d4b11c29858e02c1f55 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 5 Dec 2024 10:30:53 +0100 Subject: [PATCH 12/16] Remove the implementation without FStarBinder of erased_impl. --- engine/backends/fstar/fstar_backend.ml | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 29c45bfa4..5c0cb4e2c 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -881,18 +881,6 @@ struct in let erased_impl name ty attrs binders = let name' = F.id_prime name in - (* let arguments = - match F.AST.(ty.tm) with - | F.AST.Product (binders, _) -> binders - | _ -> [] - in - let generics_names = - arguments - |> List.filter_map ~f:(fun arg -> - match F.AST.(arg.aqual, arg.b) with - | Some ((Implicit | TypeClassArg) as arg), F.AST.Annotated (name, _) -> Some (name, arg) - | _ -> None) - 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 = From b9f31e42ab6ac0e6b4bd8e7d9e2fdc5d4b6d3a4e Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 5 Dec 2024 11:42:17 +0100 Subject: [PATCH 13/16] Rename NeverDropBody to NeverErased. --- engine/lib/import_thir.ml | 9 +++++++-- hax-lib/macros/src/dummy.rs | 1 + hax-lib/macros/src/implementation.rs | 18 ++++++++++++++---- hax-lib/macros/src/quote.rs | 4 ++-- hax-lib/macros/src/utils.rs | 4 ++-- hax-lib/macros/types/src/lib.rs | 2 +- hax-lib/src/proc_macros.rs | 2 +- 7 files changed, 28 insertions(+), 12 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 0918496a2..eb0cd442b 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1462,6 +1462,12 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = |> 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 = @@ -1493,8 +1499,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = let 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 diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs index 8b40ac9b3..429e04dea 100644 --- a/hax-lib/macros/src/dummy.rs +++ b/hax-lib/macros/src/dummy.rs @@ -31,6 +31,7 @@ identity_proc_macro_attribute!( 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 4874b1671..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,7 +617,7 @@ 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] @@ -626,7 +626,7 @@ pub fn opaque_type(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr opaque(attr, item) } -/// 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] @@ -636,6 +636,16 @@ pub fn opaque(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream 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::NeverErased; + quote! {#attr #item}.into() +} + /// A marker indicating a `fn` as a ProVerif process read. #[proc_macro_error] #[proc_macro_attribute] 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 34c6aa1c8..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, diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs index d5f0684a3..65136716f 100644 --- a/hax-lib/src/proc_macros.rs +++ b/hax-lib/src/proc_macros.rs @@ -3,7 +3,7 @@ pub use hax_lib_macros::{ attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque, - opaque_type, refinement_type, requires, trait_fn_decoration, + opaque_type, refinement_type, requires, trait_fn_decoration, transparent, }; pub use hax_lib_macros::{ From c5dc7188c6ff1b862cf906d6899ede79df73e677 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 5 Dec 2024 13:06:01 +0100 Subject: [PATCH 14/16] Updated tests. --- ...oolchain__attribute-opaque into-fstar.snap | 63 +++++++++++++++++-- .../toolchain__interface-only into-fstar.snap | 41 +++++++++++- tests/attribute-opaque/src/lib.rs | 30 ++++++++- tests/cli/interface-only/src/lib.rs | 26 ++++++++ 4 files changed, 151 insertions(+), 9 deletions(-) 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 5a570c019..5a2e7e965 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -35,21 +35,55 @@ module Attribute_opaque 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 + [@@ FStar.Tactics.Typeclasses.tcinstance] assume val impl_T_for_u8': t_T u8 let impl_T_for_u8 = impl_T_for_u8' +[@@ FStar.Tactics.Typeclasses.tcinstance] assume -val c': u8 +val impl_1': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32 v_U -let c = c' +let impl_1 (#v_U: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_U) = + impl_1' #v_U #i1 + +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' ''' "Attribute_opaque.fsti" = ''' module Attribute_opaque @@ -63,12 +97,33 @@ class t_T (v_Self: Type0) = { f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result) } -val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 +val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : eqtype -val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 +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) +} [@@ FStar.Tactics.Typeclasses.tcinstance] val impl_T_for_u8:t_T u8 +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U + 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) ''' 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 ac6be840d..2b3c34c3f 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -39,6 +39,21 @@ 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. @@ -73,7 +88,7 @@ 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 = impl_2' +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 @@ -82,7 +97,7 @@ 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 = impl_3' +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 `+:` @@ -99,4 +114,26 @@ val f': x: u8 (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 30030a143..a633074aa 100644 --- a/tests/attribute-opaque/src/lib.rs +++ b/tests/attribute-opaque/src/lib.rs @@ -10,10 +10,23 @@ enum OpaqueEnum { 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 +} + trait T { fn d(); } @@ -23,12 +36,23 @@ impl T for u8 { fn d() { unsafe { let my_num: i32 = 10; - let my_num_ptr: *const i32 = &my_num; + let _my_num_ptr: *const i32 = &my_num; let mut my_speed: i32 = 88; - let my_speed_ptr: *mut i32 = &mut my_speed; + let _my_speed_ptr: *mut i32 = &mut my_speed; } } } +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; +const C: u8 = 0 + 0; 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() {} +} From b3de81723432a0b75bfcb77f4f5f6f2b640e3a0a Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 12 Dec 2024 10:53:25 +0100 Subject: [PATCH 15/16] Add more cases in opaque tests. --- ...oolchain__attribute-opaque into-fstar.snap | 51 ++++++++++++++----- tests/attribute-opaque/src/lib.rs | 27 ++++++++++ 2 files changed, 64 insertions(+), 14 deletions(-) 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 5a2e7e965..6373c0b9e 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -45,18 +45,22 @@ 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 -[@@ FStar.Tactics.Typeclasses.tcinstance] assume -val impl_T_for_u8': t_T u8 +val impl__S1__f_s1': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True) -let impl_T_for_u8 = impl_T_for_u8' +let impl__S1__f_s1 = impl__S1__f_s1' [@@ FStar.Tactics.Typeclasses.tcinstance] assume -val impl_1': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32 v_U +val impl_2': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32 v_U -let impl_1 (#v_U: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_U) = - impl_1' #v_U #i1 +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 @@ -84,6 +88,12 @@ val ff_pre_post': x: bool -> y: bool 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 @@ -91,11 +101,9 @@ module Attribute_opaque open Core open FStar.Mul -class t_T (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) -} +type t_S1 = | S1 : t_S1 + +type t_S2 = | S2 : t_S2 val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : eqtype @@ -108,11 +116,12 @@ class t_TrGeneric (v_Self: Type0) (v_U: Type0) = { f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result) } -[@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_T_for_u8:t_T u8 +val impl__S1__f_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True) [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_1 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U +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) @@ -126,4 +135,18 @@ val ff_pre_post (x y: bool) 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) +} + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_T_for_u8:t_T u8 ''' diff --git a/tests/attribute-opaque/src/lib.rs b/tests/attribute-opaque/src/lib.rs index a633074aa..28671f800 100644 --- a/tests/attribute-opaque/src/lib.rs +++ b/tests/attribute-opaque/src/lib.rs @@ -27,12 +27,20 @@ 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; @@ -41,6 +49,11 @@ impl T for u8 { 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 { @@ -56,3 +69,17 @@ impl TrGeneric for i32 { #[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() {} +} From 7629b152262a078be3cfaec546afef3a536122df Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 12 Dec 2024 13:49:57 +0100 Subject: [PATCH 16/16] Go back to previous behaviour for val interfaces in the fsti for impls with assoc type. --- engine/backends/fstar/fstar_backend.ml | 24 +++++++++++++------ .../toolchain__interface-only into-fstar.snap | 12 ---------- 2 files changed, 17 insertions(+), 19 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 29fbab96f..f77e8fc1f 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1494,14 +1494,24 @@ struct in let body = F.term @@ F.AST.Record (None, fields) in let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in + let has_type = + List.exists items ~f:(fun { ii_v; _ } -> + match ii_v with IIType _ -> true | _ -> false) + in let let_impl = F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]) in - if is_erased 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) - @ erased_impl name val_type [ tcinst ] generics - 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 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 2b3c34c3f..dcdee90a4 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -57,9 +57,6 @@ let impl_T2_for_u8: t_T2 u8 = /// 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 - [@@ FStar.Tactics.Typeclasses.tcinstance] assume val impl': Core.Convert.t_From t_Bar Prims.unit @@ -67,9 +64,6 @@ 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 - [@@ FStar.Tactics.Typeclasses.tcinstance] assume val impl_1': Core.Convert.t_From t_Bar u8 @@ -81,18 +75,12 @@ 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 - [@@ FStar.Tactics.Typeclasses.tcinstance] 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 - [@@ FStar.Tactics.Typeclasses.tcinstance] assume val impl_3': v_SIZE: usize -> Core.Convert.t_From (t_Param v_SIZE) Prims.unit