ProVerif protocol traits

Cargo.toml

@@ -13,6 +13,8 @@ members = [
      "hax-lib",
      "hax-lib-macros",
      "hax-lib-macros/types",
+     "hax-lib-protocol",
+     "hax-lib-protocol-macros"
 ]
 exclude = ["tests"]
 resolver = "2"

engine/backends/proverif/proverif_backend.ml

@@ -181,6 +181,71 @@ module Print = struct
         | Type { name; generics; variants; is_struct } ->
             if is_struct then fun_and_reduc name variants else empty
         | _ -> empty
+
+      method! expr_let : lhs:pat -> rhs:expr -> expr fn =
+        fun ~lhs ~rhs body ->
+          string "let" ^^ space
+          ^^ iblock Fn.id (print#pat_at Expr_Let_lhs lhs)
+          ^^ space ^^ equals ^^ space
+          ^^ iblock Fn.id (print#expr_at Expr_Let_rhs rhs)
+          ^^ space ^^ string "in" ^^ hardline
+          ^^ (print#expr_at Expr_Let_body body |> group)
+
+      method! doc_construct_inductive
+          : is_record:bool ->
+            is_struct:bool ->
+            constructor:concrete_ident ->
+            base:document option ->
+            (global_ident * document) list fn =
+        fun ~is_record ~is_struct:_ ~constructor ~base:_ args ->
+          if is_record then
+            string "t_"
+            (* FIXME: How do I get at the ident from the struct definition instead? *)
+            ^^ print#concrete_ident constructor
+            ^^ iblock parens
+                 (separate_map
+                    (break 0 ^^ comma)
+                    (fun (field, body) -> iblock Fn.id body |> group)
+                    args)
+          else
+            print#concrete_ident constructor
+            ^^ iblock parens (separate_map (break 0) snd args)
+
+      method ty : Generic_printer_base.par_state -> ty fn =
+        fun ctx ty ->
+          match ty with
+          | TBool -> print#ty_bool
+          | TParam i -> print#local_ident i
+          | TApp _ -> super#ty ctx ty
+          | _ -> string "bitstring"
+
+      method! expr_app : expr -> expr list -> generic_value list fn =
+        fun f args _generic_args ->
+          let dummy_fn =
+            match List.length args with
+            | n when n < 8 -> string "dummy_fn_" ^^ PPrint.OCaml.int n
+            | _ -> string "not_supported"
+          in
+          let args =
+            separate_map
+              (comma ^^ break 1)
+              (print#expr_at Expr_App_arg >> group)
+              args
+          in
+          let f = print#expr_at Expr_App_f f |> group in
+          f ^^ iblock parens args
+
+      method! literal : Generic_printer_base.literal_ctx -> literal fn =
+        fun _ctx -> function
+          | String s -> string "no char literals in ProVerif"
+          | Char c -> string "no char literals in ProVerif"
+          | Int { value; negative; _ } ->
+              string "int2bitstring"
+              ^^ iblock parens
+                   (string value |> precede (if negative then minus else empty))
+          | Float { value; kind; negative } ->
+              string "no float literals in ProVerif"
+          | Bool b -> OCaml.bool b
     end
 
   include Api (struct
@@ -194,10 +259,34 @@ let insert_top_level contents = contents ^ "\n\nprocess\n    0\n"
 (* Insert ProVerif code that will be necessary in any development.*)
 let insert_preamble contents = "channel c.\ntype state.\n" ^ contents
 
+let is_process_read : attrs -> bool =
+  Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessRead])
+
+let is_process_write : attrs -> bool =
+  Attr_payloads.payloads
+  >> List.exists ~f:(fst >> [%matches? Types.ProcessWrite])
+
+let is_process_init : attrs -> bool =
+  Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessInit])
+
 let translate m (bo : BackendOptions.t) (items : AST.item list) :
     Types.file list =
-  let contents, _ = Print.items items in
-  let contents = contents |> insert_top_level |> insert_preamble in
+  let processes, rest =
+    List.partition_tf
+      ~f:(fun item -> [%matches? Fn _] item.v && is_process_read item.attrs)
+      items
+  in
+  let letfuns, rest =
+    List.partition_tf ~f:(fun item -> [%matches? Fn _] item.v) rest
+  in
+  let letfun_content, _ = Print.items letfuns in
+  let process_content, _ = Print.items processes in
+  let contents, _ = Print.items rest in
+  let contents =
+    contents ^ "\n(* Process Macros *)\n\n" ^ letfun_content
+    ^ "\n(* Processes *)" ^ process_content
+    |> insert_top_level |> insert_preamble
+  in
   let file = Types.{ path = "output.pv"; contents } in
   [ file ]
 

engine/lib/attr_payloads.ml

@@ -37,7 +37,15 @@ end
 
 module AssocRole = struct
   module T = struct
-    type t = Requires | Ensures | Decreases | Refine
+    type t =
+      | Requires
+      | Ensures
+      | Decreases
+      | Refine
+      | ProcessRead
+      | ProcessWrite
+      | ProcessInit
+      | ProtocolMessages
     [@@deriving show, yojson, compare, sexp, eq]
   end
 
@@ -54,6 +62,10 @@ module AssocRole = struct
     | Ensures -> Ensures
     | Decreases -> Decreases
     | Refine -> Refine
+    | ProcessRead -> ProcessRead
+    | ProcessWrite -> ProcessWrite
+    | ProcessInit -> ProcessInit
+    | ProtocolMessages -> ProtocolMessages
 end
 
 module MakeBase (Error : Phase_utils.ERROR) = struct

hax-lib-macros/src/lib.rs

@@ -474,3 +474,39 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr
 
     quote! { #item }.into()
 }
+
+/// A marker indicating a `fn` as a ProVerif process read.
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn process_read(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+    let item: ItemFn = parse_macro_input!(item);
+    let attr = AttrPayload::ProcessRead;
+    quote! {#attr #item}.into()
+}
+
+/// A marker indicating a `fn` as a ProVerif process write.
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn process_write(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+    let item: ItemFn = parse_macro_input!(item);
+    let attr = AttrPayload::ProcessWrite;
+    quote! {#attr #item}.into()
+}
+
+/// A marker indicating a `fn` as a ProVerif process initialization.
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn process_init(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+    let item: ItemFn = parse_macro_input!(item);
+    let attr = AttrPayload::ProcessInit;
+    quote! {#attr #item}.into()
+}
+
+/// A marker indicating an `enum` as describing the protocol messages.
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn protocol_messages(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+    let item: ItemEnum = parse_macro_input!(item);
+    let attr = AttrPayload::ProtocolMessages;
+    quote! {#attr #item}.into()
+}

hax-lib-macros/types/src/lib.rs

@@ -50,6 +50,10 @@ pub enum AssociationRole {
     Ensures,
     Decreases,
     Refine,
+    ProcessRead,
+    ProcessWrite,
+    ProcessInit,
+    ProtocolMessages,
 }
 
 /// Hax only understands one attribute: `#[hax::json(PAYLOAD)]` where
@@ -67,6 +71,10 @@ pub enum AttrPayload {
     /// Mark an item as a lemma statement to prove in the backend
     Lemma,
     Language,
+    ProcessRead,
+    ProcessWrite,
+    ProcessInit,
+    ProtocolMessages,
 }
 
 pub const HAX_TOOL: &str = "_hax";

hax-lib-protocol-macros/Cargo.toml

@@ -0,0 +1,25 @@
+[package]
+name = "hax-lib-protocol-macros"
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+homepage.workspace = true
+edition.workspace = true
+repository.workspace = true
+readme.workspace = true
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[lib]
+proc-macro = true
+
+[dependencies]
+proc-macro-error = "1.0.4"
+proc-macro2.workspace = true
+quote.workspace = true
+syn = { version = "2.0", features = [
+    "full",
+    "visit-mut",
+    "extra-traits",
+    "parsing",
+] }