From 2f1ac05cf7405ee8cd9aec678d0b48701f665750 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 6 Mar 2024 10:36:07 +0100 Subject: [PATCH 01/12] Small refactoring of constants translation --- engine/backends/proverif/proverif_backend.ml | 23 +++++++++++++------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index e541cd6ea..58261af27 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -170,6 +170,12 @@ module Make (Options : OPTS) : MAKE = struct inherit GenericPrint.print as super (* Backend-specific utilities *) + + method pv_const name typ = + string "const" ^^ space ^^ print#concrete_ident name ^^ colon ^^ typ + ^^ dot + (** Print a ProVerif constant declaration of the given typ (provided as a document).*) + method field_accessor field_name = string "accessor" ^^ underscore ^^ print#concrete_ident field_name @@ -449,14 +455,15 @@ module Make (Options : OPTS) : MAKE = struct ^^ if reduc_lines == empty then empty else dot in match item.v with - (* `fn`s are transformed into `letfun` process macros. *) - | Fn { name; body = { typ = TInt _; _ }; params = []; _ } -> - string "const" ^^ space ^^ print#concrete_ident name ^^ colon - ^^ string "bitstring" ^^ dot - | Fn { name; body; params = []; _ } -> - string "const" ^^ space ^^ print#concrete_ident name ^^ colon - ^^ print#ty_at Item_Fn_body body.typ - ^^ dot + (* `fn`s with empty parameter lists are really Rust consts. *) + | Fn { name; body; params = [] } -> + let const_typ = + match body.typ with + (* ProVerif does not allow `nat` constants. *) + | TInt _ -> string "bitstring" + | _ -> print#ty_at Item_Fn_body body.typ + in + print#pv_const name const_typ | Fn { name; generics; body; params } -> let body = if assume_item then From 08fb574ff8862d78bae51a035a66681dfbf634b8 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 6 Mar 2024 11:48:55 +0100 Subject: [PATCH 02/12] Introduce an attribute for marking `fn`s as PV constructors --- engine/lib/attr_payloads.ml | 2 ++ hax-lib-macros/src/lib.rs | 9 +++++++++ hax-lib-macros/types/src/lib.rs | 2 ++ 3 files changed, 13 insertions(+) diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml index e1e308346..81c5daca1 100644 --- a/engine/lib/attr_payloads.ml +++ b/engine/lib/attr_payloads.ml @@ -46,6 +46,7 @@ module AssocRole = struct | ProcessWrite | ProcessInit | ProtocolMessages + | PVConstructor [@@deriving show, yojson, compare, sexp, eq] end @@ -66,6 +67,7 @@ module AssocRole = struct | ProcessWrite -> ProcessWrite | ProcessInit -> ProcessInit | ProtocolMessages -> ProtocolMessages + | PVConstructor -> PVConstructor end module MakeBase (Error : Phase_utils.ERROR) = struct diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index f9ce51f80..f9e007317 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -510,3 +510,12 @@ pub fn protocol_messages(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::T let attr = AttrPayload::ProtocolMessages; quote! {#attr #item}.into() } + +/// A marker indicating a `fn` as a ProVerif process initialization. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn pv_constructor(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: ItemFn = parse_macro_input!(item); + let attr = AttrPayload::PVConstructor; + quote! {#attr #item}.into() +} diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs index 293aee2b7..3e1c150b6 100644 --- a/hax-lib-macros/types/src/lib.rs +++ b/hax-lib-macros/types/src/lib.rs @@ -54,6 +54,7 @@ pub enum AssociationRole { ProcessWrite, ProcessInit, ProtocolMessages, + PVConstructor } /// Hax only understands one attribute: `#[hax::json(PAYLOAD)]` where @@ -75,6 +76,7 @@ pub enum AttrPayload { ProcessWrite, ProcessInit, ProtocolMessages, + PVConstructor } pub const HAX_TOOL: &str = "_hax"; From 1ad075ab623fc6d885b2de30cb4c95975ccaadc6 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 6 Mar 2024 11:49:33 +0100 Subject: [PATCH 03/12] Introduce method for printing constructors --- engine/backends/proverif/proverif_backend.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 58261af27..603060f2f 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -176,6 +176,14 @@ module Make (Options : OPTS) : MAKE = struct ^^ dot (** Print a ProVerif constant declaration of the given typ (provided as a document).*) + method pv_constructor ?(is_data = false) ?(is_typeconverter = false) name arg_types typ = + let options = if is_data then [string "data";] else [] in + let options = if is_typeconverter then (string "typeConverter") :: options else options in + let options = space ^^ string "[" ^^ separate (comma ^^ space) options ^^ string "]" in + string "fun" ^^ space ^^ name ^^ iblock parens (separate (comma ^^ space) arg_types) ^^ colon ^^ space ^^ typ ^^ options ^^ dot + (** Print a ProVerif constructor. *) + + method field_accessor field_name = string "accessor" ^^ underscore ^^ print#concrete_ident field_name From 4ffbfa75fab51227b0d1fb64ce9f617fad64f9b5 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 6 Mar 2024 11:50:34 +0100 Subject: [PATCH 04/12] Print constructors using the new function --- engine/backends/proverif/proverif_backend.ml | 94 ++++++++++++-------- 1 file changed, 55 insertions(+), 39 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 603060f2f..5d92d0554 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -176,14 +176,23 @@ module Make (Options : OPTS) : MAKE = struct ^^ dot (** Print a ProVerif constant declaration of the given typ (provided as a document).*) - method pv_constructor ?(is_data = false) ?(is_typeconverter = false) name arg_types typ = - let options = if is_data then [string "data";] else [] in - let options = if is_typeconverter then (string "typeConverter") :: options else options in - let options = space ^^ string "[" ^^ separate (comma ^^ space) options ^^ string "]" in - string "fun" ^^ space ^^ name ^^ iblock parens (separate (comma ^^ space) arg_types) ^^ colon ^^ space ^^ typ ^^ options ^^ dot + method pv_constructor ?(is_data = false) ?(is_typeconverter = false) + name arg_types typ = + let options = if is_data then [ string "data" ] else [] in + let options = + if is_typeconverter then string "typeConverter" :: options + else options + in + let options = + space ^^ string "[" + ^^ separate (comma ^^ space) options + ^^ string "]" + in + string "fun" ^^ space ^^ name + ^^ iblock parens (separate (comma ^^ space) arg_types) + ^^ colon ^^ space ^^ typ ^^ options ^^ dot (** Print a ProVerif constructor. *) - method field_accessor field_name = string "accessor" ^^ underscore ^^ print#concrete_ident field_name @@ -431,19 +440,13 @@ module Make (Options : OPTS) : MAKE = struct fun_args in let fun_args_types = - separate_map - (comma ^^ break 1) - (snd3 >> print#ty_at Param_typ) - fun_args + List.map ~f:(snd3 >> print#ty_at Param_typ) fun_args in let constructor_name = print#concrete_ident constructor.name in let fun_line = - string "fun" ^^ space ^^ constructor_name - ^^ iblock parens fun_args_types - ^^ string ": " - ^^ print#concrete_ident base_name - ^^ space ^^ string "[data]" ^^ dot + print#pv_constructor ~is_data:true constructor_name fun_args_types + (print#concrete_ident base_name) in let reduc_line = string "reduc forall " ^^ iblock Fn.id fun_args_full ^^ semi @@ -473,39 +476,52 @@ module Make (Options : OPTS) : MAKE = struct in print#pv_const name const_typ | Fn { name; generics; body; params } -> - let body = - if assume_item then - print#ty_at Item_Fn_body body.typ - ^^ string "_default()" - ^^ string "(* fill_in_body of type: " - ^^ print#ty_at Item_Fn_body body.typ - ^^ string "*)" - else print#expr_at Item_Fn_body body + let is_constructor : attrs -> bool = + Attr_payloads.payloads + >> List.exists ~f:(fst >> [%matches? Types.PVConstructor]) in - let params_string = - iblock parens - (separate_map (comma ^^ break 1) print#param params) - in - string "letfun" ^^ space - ^^ align - (print#concrete_ident name ^^ params_string ^^ space - ^^ equals ^^ hardline ^^ body ^^ dot) + if is_constructor item.attrs then + let arg_types = + List.map ~f:(fun p -> print#ty_at Param_typ p.typ) params + in + let return_typ = print#ty_at Item_Fn_body body.typ in + print#pv_constructor ~is_data:true + (print#concrete_ident name) + arg_types return_typ + else + let body = + if assume_item then + print#ty_at Item_Fn_body body.typ + ^^ string "_default()" + ^^ string "(* fill_in_body of type: " + ^^ print#ty_at Item_Fn_body body.typ + ^^ string "*)" + else print#expr_at Item_Fn_body body + in + let params_string = + iblock parens + (separate_map (comma ^^ break 1) print#param params) + in + string "letfun" ^^ space + ^^ align + (print#concrete_ident name ^^ params_string ^^ space + ^^ equals ^^ hardline ^^ body ^^ dot) (* `struct` definitions are transformed into simple constructors and `reduc`s for accessing fields. *) | Type { name; generics; variants; is_struct } -> let type_line = string "type " ^^ print#concrete_ident name ^^ dot in let to_bitstring_converter_line = - string "fun " ^^ print#concrete_ident name - ^^ string "_to_bitstring" - ^^ iblock parens (print#concrete_ident name) - ^^ string ": bitstring [typeConverter]." + print#pv_constructor ~is_typeconverter:true + (print#concrete_ident name ^^ string "_to_bitstring") + [ print#concrete_ident name ] + (string "bitstring") in let from_bitstring_converter_line = - string "fun " ^^ print#concrete_ident name - ^^ string "_from_bitstring(bitstring)" - ^^ colon ^^ print#concrete_ident name - ^^ string " [typeConverter]" ^^ dot + print#pv_constructor ~is_typeconverter:true + (print#concrete_ident name ^^ string "_from_bitstring") + [ string "bitstring" ] + (print#concrete_ident name) in let default_line = string "const " ^^ print#concrete_ident name From fa3abbf26bf5c7a5090a76e32fd27557cbcc36f9 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 6 Mar 2024 15:29:22 +0100 Subject: [PATCH 05/12] Introduce attribute to mark item as needing manual modelling --- engine/lib/attr_payloads.ml | 2 ++ hax-lib-macros/src/lib.rs | 9 +++++++++ hax-lib-macros/types/src/lib.rs | 6 ++++-- 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml index 81c5daca1..40eaf3180 100644 --- a/engine/lib/attr_payloads.ml +++ b/engine/lib/attr_payloads.ml @@ -47,6 +47,7 @@ module AssocRole = struct | ProcessInit | ProtocolMessages | PVConstructor + | PVHandwritten [@@deriving show, yojson, compare, sexp, eq] end @@ -68,6 +69,7 @@ module AssocRole = struct | ProcessInit -> ProcessInit | ProtocolMessages -> ProtocolMessages | PVConstructor -> PVConstructor + | PVHandwritten -> PVHandwritten end module MakeBase (Error : Phase_utils.ERROR) = struct diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index f9e007317..3454873d8 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -519,3 +519,12 @@ pub fn pv_constructor(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::Toke let attr = AttrPayload::PVConstructor; quote! {#attr #item}.into() } + +/// A marker indicating a `fn` as a ProVerif process initialization. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn pv_handwritten(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: ItemFn = parse_macro_input!(item); + let attr = AttrPayload::PVHandwritten; + quote! {#attr #item}.into() +} diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs index 3e1c150b6..6fe72305a 100644 --- a/hax-lib-macros/types/src/lib.rs +++ b/hax-lib-macros/types/src/lib.rs @@ -54,7 +54,8 @@ pub enum AssociationRole { ProcessWrite, ProcessInit, ProtocolMessages, - PVConstructor + PVConstructor, + PVHandwritten } /// Hax only understands one attribute: `#[hax::json(PAYLOAD)]` where @@ -76,7 +77,8 @@ pub enum AttrPayload { ProcessWrite, ProcessInit, ProtocolMessages, - PVConstructor + PVConstructor, + PVHandwritten } pub const HAX_TOOL: &str = "_hax"; From 511b4ce1d1ea59ce4df17d60e5648f76dd4c5214 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 6 Mar 2024 15:30:04 +0100 Subject: [PATCH 06/12] Map `Deref::deref` to identity as well --- engine/backends/proverif/proverif_backend.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 5d92d0554..ccb91b452 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -327,6 +327,10 @@ module Make (Options : OPTS) : MAKE = struct | QuestionMark { e; return_typ; _ } -> print#expr ctx e (* Translate known functions *) | App { f = { e = GlobalVar name; _ }; args } -> ( + let maps_to_identity fn_name = Global_ident.eq_name Core__clone__Clone__clone name + || Global_ident.eq_name Rust_primitives__unsize name + || Global_ident.eq_name Core__ops__deref__Deref__deref name + in match name with | `Primitive p -> ( match p with @@ -341,9 +345,7 @@ module Make (Options : OPTS) : MAKE = struct | Cast -> print#expr NeedsPar (List.hd_exn args) | _ -> empty) | _ -> ( - if - Global_ident.eq_name Core__clone__Clone__clone name - || Global_ident.eq_name Rust_primitives__unsize name + if maps_to_identity name then print#expr ctx (List.hd_exn args) else match From f3d93599e48cb4dc2394341d9b3c8b90fdd7cc40 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 6 Mar 2024 15:30:26 +0100 Subject: [PATCH 07/12] ProVerif comment helper --- engine/backends/proverif/proverif_backend.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index ccb91b452..d57edaccd 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -171,6 +171,11 @@ module Make (Options : OPTS) : MAKE = struct (* Backend-specific utilities *) + (* ProVerif syntax *) + method pv_comment content = + string "(*" ^^ space ^^ content ^^ space ^^ string "*)" ^^ hardline + (** Print a ProVerif comment and end the line. *) + method pv_const name typ = string "const" ^^ space ^^ print#concrete_ident name ^^ colon ^^ typ ^^ dot From eefe9de70481d14731241d171b9c432ac25954cb Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 6 Mar 2024 15:31:01 +0100 Subject: [PATCH 08/12] Distinguish `handwritten` items --- engine/backends/proverif/proverif_backend.ml | 35 +++++++++++++------- 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index d57edaccd..6d8800f01 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -483,26 +483,37 @@ module Make (Options : OPTS) : MAKE = struct in print#pv_const name const_typ | Fn { name; generics; body; params } -> - let is_constructor : attrs -> bool = + let as_constructor : attrs -> bool = Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.PVConstructor]) in - if is_constructor item.attrs then + let as_handwritten : attrs -> bool = + Attr_payloads.payloads + >> List.exists ~f:(fst >> [%matches? Types.PVHandwritten]) + in + if as_constructor item.attrs then let arg_types = List.map ~f:(fun p -> print#ty_at Param_typ p.typ) params in let return_typ = print#ty_at Item_Fn_body body.typ in - print#pv_constructor ~is_data:true - (print#concrete_ident name) - arg_types return_typ + print#pv_comment (string "marked as constructor") + ^^ print#pv_constructor ~is_data:true + (print#concrete_ident name) + arg_types return_typ else - let body = + let comment = if assume_item then - print#ty_at Item_Fn_body body.typ - ^^ string "_default()" - ^^ string "(* fill_in_body of type: " - ^^ print#ty_at Item_Fn_body body.typ - ^^ string "*)" + print#pv_comment + (string "REPLACE by body of type: " + ^^ print#ty_at Item_Fn_body body.typ) + else if as_handwritten item.attrs then + print#pv_comment (string "REPLACE by destructor") + else empty + in + + let body = + if assume_item || as_handwritten item.attrs then + print#ty_at Item_Fn_body body.typ ^^ string "_default()" else print#expr_at Item_Fn_body body in let params_string = @@ -512,7 +523,7 @@ module Make (Options : OPTS) : MAKE = struct string "letfun" ^^ space ^^ align (print#concrete_ident name ^^ params_string ^^ space - ^^ equals ^^ hardline ^^ body ^^ dot) + ^^ equals ^^ hardline ^^ body ^^ dot ^^ comment) (* `struct` definitions are transformed into simple constructors and `reduc`s for accessing fields. *) | Type { name; generics; variants; is_struct } -> let type_line = From 277442e9ec1381066f2c6b17626e2ae586d5cc85 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 12 Mar 2024 15:04:02 +0100 Subject: [PATCH 09/12] Generate _err() also for enums --- engine/backends/proverif/proverif_backend.ml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 7bafac716..d4415efe6 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -333,10 +333,11 @@ module Make (Options : OPTS) : MAKE = struct | QuestionMark { e; return_typ; _ } -> print#expr ctx e (* Translate known functions *) | App { f = { e = GlobalVar name; _ }; args } -> ( - let maps_to_identity fn_name = Global_ident.eq_name Core__clone__Clone__clone name - || Global_ident.eq_name Rust_primitives__unsize name - || Global_ident.eq_name Core__ops__deref__Deref__deref name - in + let maps_to_identity fn_name = + Global_ident.eq_name Core__clone__Clone__clone name + || Global_ident.eq_name Rust_primitives__unsize name + || Global_ident.eq_name Core__ops__deref__Deref__deref name + in match name with | `Primitive p -> ( match p with @@ -351,8 +352,8 @@ module Make (Options : OPTS) : MAKE = struct | Cast -> print#expr NeedsPar (List.hd_exn args) | _ -> empty) | _ -> ( - if maps_to_identity name - then print#expr ctx (List.hd_exn args) + if maps_to_identity name then + print#expr ctx (List.hd_exn args) else match translate_known_name name ~dict:library_functions @@ -565,8 +566,8 @@ module Make (Options : OPTS) : MAKE = struct ^^ fun_and_reduc name constructor else type_line ^^ hardline ^^ to_bitstring_converter_line ^^ hardline - ^^ from_bitstring_converter_line ^^ hardline ^^ default_line - ^^ hardline + ^^ from_bitstring_converter_line ^^ hardline ^^ default_line ^^ hardline + ^^ err_line ^^ hardline ^^ separate_map hardline (fun variant -> fun_and_reduc name variant) variants From 844ce8b1b54fb6dddecc6e3be297deb1f57739aa Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 12 Mar 2024 15:09:54 +0100 Subject: [PATCH 10/12] Formatting --- engine/backends/proverif/proverif_backend.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index d4415efe6..27ef2f361 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -566,8 +566,8 @@ module Make (Options : OPTS) : MAKE = struct ^^ fun_and_reduc name constructor else type_line ^^ hardline ^^ to_bitstring_converter_line ^^ hardline - ^^ from_bitstring_converter_line ^^ hardline ^^ default_line ^^ hardline - ^^ err_line ^^ hardline + ^^ from_bitstring_converter_line ^^ hardline ^^ default_line + ^^ hardline ^^ err_line ^^ hardline ^^ separate_map hardline (fun variant -> fun_and_reduc name variant) variants From 81f8b2f5c3f05a5c990f2ba2570c2494e30cced1 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 13 Mar 2024 10:37:52 +0100 Subject: [PATCH 11/12] Update doc comments --- hax-lib-macros/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index a91327979..20c130458 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -521,7 +521,7 @@ pub fn protocol_messages(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::T quote! {#attr #item}.into() } -/// A marker indicating a `fn` as a ProVerif process initialization. +/// A marker indicating a `fn` should be automatically translated to a ProVerif constructor. #[proc_macro_error] #[proc_macro_attribute] pub fn pv_constructor(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { @@ -530,7 +530,7 @@ pub fn pv_constructor(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::Toke quote! {#attr #item}.into() } -/// A marker indicating a `fn` as a ProVerif process initialization. +/// A marker indicating a `fn` requires manual modelling in ProVerif. #[proc_macro_error] #[proc_macro_attribute] pub fn pv_handwritten(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { From 1aa667c329cd1f68435696768250cb90534af59d Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 13 Mar 2024 10:41:05 +0100 Subject: [PATCH 12/12] Remove unnecessary `AssociationRole` variants --- engine/lib/attr_payloads.ml | 4 ---- hax-lib-macros/types/src/lib.rs | 2 -- 2 files changed, 6 deletions(-) diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml index 526ee963a..b2be72b80 100644 --- a/engine/lib/attr_payloads.ml +++ b/engine/lib/attr_payloads.ml @@ -57,8 +57,6 @@ module AssocRole = struct | ProcessWrite | ProcessInit | ProtocolMessages - | PVConstructor - | PVHandwritten [@@deriving show, yojson, compare, sexp, eq] end @@ -79,8 +77,6 @@ module AssocRole = struct | ProcessWrite -> ProcessWrite | ProcessInit -> ProcessInit | ProtocolMessages -> ProtocolMessages - | PVConstructor -> PVConstructor - | PVHandwritten -> PVHandwritten end module MakeBase (Error : Phase_utils.ERROR) = struct diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs index 4a3d4a7e2..3b88f3aaa 100644 --- a/hax-lib-macros/types/src/lib.rs +++ b/hax-lib-macros/types/src/lib.rs @@ -54,8 +54,6 @@ pub enum AssociationRole { ProcessWrite, ProcessInit, ProtocolMessages, - PVConstructor, - PVHandwritten, } /// Hax only understands one attribute: `#[hax::json(PAYLOAD)]` where