diff --git a/Cargo.lock b/Cargo.lock index a582a8bc1..76a4fad3b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -535,6 +535,20 @@ dependencies = [ "uuid", ] +[[package]] +name = "hax-lib-protocol" +version = "0.1.0-pre.1" + +[[package]] +name = "hax-lib-protocol-macros" +version = "0.1.0-pre.1" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.38", +] + [[package]] name = "hax-lint" version = "0.1.0-pre.1" diff --git a/Cargo.toml b/Cargo.toml index 50c29c170..cb56b0837 100644 --- a/Cargo.toml +++ b/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" diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index a8c2c1791..7a3625130 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/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 ] diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml index 1fc2fa8f5..e1e308346 100644 --- a/engine/lib/attr_payloads.ml +++ b/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 diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index 1ff405108..f9ce51f80 100644 --- a/hax-lib-macros/src/lib.rs +++ b/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() +} diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs index 639fa0d8c..293aee2b7 100644 --- a/hax-lib-macros/types/src/lib.rs +++ b/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"; diff --git a/hax-lib-protocol-macros/Cargo.toml b/hax-lib-protocol-macros/Cargo.toml new file mode 100644 index 000000000..0cb376255 --- /dev/null +++ b/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", +] } diff --git a/hax-lib-protocol-macros/src/lib.rs b/hax-lib-protocol-macros/src/lib.rs new file mode 100644 index 000000000..db9945abe --- /dev/null +++ b/hax-lib-protocol-macros/src/lib.rs @@ -0,0 +1,309 @@ +use quote::quote; +use syn::{parse, parse_macro_input}; + +/// This macro takes an `fn` as the basis of an `InitialState` implementation +/// for the state type that is returned by the `fn` (on success). +/// +/// The `fn` is expected to build the state type specified as a `Path` attribute +/// argument from a `Vec`, i.e. the signature should be compatible with +/// `TryFrom>` for the state type given as argument to the macro. +/// +/// Example: +/// ```ignore +/// pub struct A0 { +/// data: u8, +/// } +/// +/// #[hax_lib_protocol_macros::init(A0)] +/// fn init_a(prologue: Vec) -> ProtocolResult { +/// if prologue.len() < 1 { +/// return Err(ProtocolError::InvalidPrologue); +/// } +/// Ok(A0 { data: prologue[0] }) +/// } +/// +/// // The following is generated by the macro: +/// #[hax_lib_macros::exclude] +/// impl TryFrom> for A0 { +/// type Error = ProtocolError; +/// fn try_from(value: Vec) -> Result { +/// init_a(value) +/// } +/// } +/// #[hax_lib_macros::exclude] +/// impl InitialState for A0 { +/// fn init(prologue: Option>) -> ProtocolResult { +/// if let Some(prologue) = prologue { +/// prologue.try_into() +/// } else { +/// Err(ProtocolError::InvalidPrologue) +/// } +/// } +/// } +/// ``` +#[proc_macro_attribute] +pub fn init( + attr: proc_macro::TokenStream, + item: proc_macro::TokenStream, +) -> proc_macro::TokenStream { + let mut output = quote!(#[hax_lib_macros::process_init]); + output.extend(proc_macro2::TokenStream::from(item.clone())); + + let input: syn::ItemFn = parse_macro_input!(item); + let return_type: syn::Path = parse_macro_input!(attr); + let name = input.sig.ident; + + let expanded = quote!( + #[hax_lib_macros::exclude] + impl TryFrom> for #return_type { + type Error = ProtocolError; + + fn try_from(value: Vec) -> Result { + #name(value) + } + } + + #[hax_lib_macros::exclude] + impl InitialState for #return_type { + fn init(prologue: Option>) -> ProtocolResult { + if let Some(prologue) = prologue { + prologue.try_into() + } else { + Err(ProtocolError::InvalidPrologue) + } + } + } + ); + output.extend(expanded); + + return output.into(); +} + +/// This macro takes an `fn` as the basis of an `InitialState` implementation +/// for the state type that is returned by the `fn` (on success). +/// +/// The `fn` is expected to build the state type specified as a `Path` attribute +/// argument without additional input. +/// Example: +/// ```ignore +/// pub struct B0 {} +/// +/// #[hax_lib_protocol_macros::init_empty(B0)] +/// fn init_b() -> ProtocolResult { +/// Ok(B0 {}) +/// } +/// +/// // The following is generated by the macro: +/// #[hax_lib_macros::exclude] +/// impl InitialState for B0 { +/// fn init(prologue: Option>) -> ProtocolResult { +/// if let Some(_) = prologue { +/// Err(ProtocolError::InvalidPrologue) +/// } else { +/// init_b() +/// } +/// } +/// } +/// ``` +#[proc_macro_error::proc_macro_error] +#[proc_macro_attribute] +pub fn init_empty( + attr: proc_macro::TokenStream, + item: proc_macro::TokenStream, +) -> proc_macro::TokenStream { + let mut output = quote!(#[hax_lib_macros::process_init]); + output.extend(proc_macro2::TokenStream::from(item.clone())); + + let input: syn::ItemFn = parse_macro_input!(item); + let return_type: syn::Path = parse_macro_input!(attr); + let name = input.sig.ident; + + let expanded = quote!( + #[hax_lib_macros::exclude] + impl InitialState for #return_type { + fn init(prologue: Option>) -> ProtocolResult { + if let Some(_) = prologue { + Err(ProtocolError::InvalidPrologue) + } else { + #name() + } + } + } + ); + output.extend(expanded); + + return output.into(); +} + +/// A structure to parse transition tuples from `read` and `write` macros. +struct Transition { + /// `Path` to the current state type of the transition. + pub current_state: syn::Path, + /// `Path` to the destination state type of the transition. + pub next_state: syn::Path, + /// `Path` to the message type this transition is based on. + pub message_type: syn::Path, +} + +impl syn::parse::Parse for Transition { + fn parse(input: parse::ParseStream) -> syn::Result { + use syn::spanned::Spanned; + let punctuated = + syn::punctuated::Punctuated::::parse_terminated(input)?; + if punctuated.len() != 3 { + Err(syn::Error::new( + punctuated.span(), + "Insufficient number of arguments", + )) + } else { + let mut args = punctuated.into_iter(); + Ok(Self { + current_state: args.next().unwrap(), + next_state: args.next().unwrap(), + message_type: args.next().unwrap(), + }) + } + } +} + +/// Macro deriving a `WriteState` implementation for the origin state type, +/// generating a message of `message_type` and a new state, as indicated by the +/// transition tuple. +/// +/// Example: +/// ```ignore +/// #[hax_lib_protocol_macros::write(A0, A1, Message)] +/// fn write_ping(state: A0) -> ProtocolResult<(A1, Message)> { +/// Ok((A1 {}, Message::Ping(state.data))) +/// } +/// +/// // The following is generated by the macro: +/// #[hax_lib_macros::exclude] +/// impl TryFrom for (A1, Message) { +/// type Error = ProtocolError; +/// +/// fn try_from(value: A0) -> Result { +/// write_ping(value) +/// } +/// } +/// +/// #[hax_lib_macros::exclude] +/// impl WriteState for A0 { +/// type NextState = A1; +/// type Message = Message; +/// +/// fn write(self) -> ProtocolResult<(Self::NextState, Message)> { +/// self.try_into() +/// } +/// } +/// ``` +#[proc_macro_attribute] +pub fn write( + attr: proc_macro::TokenStream, + item: proc_macro::TokenStream, +) -> proc_macro::TokenStream { + let mut output = quote!(#[hax_lib_macros::process_write]); + output.extend(proc_macro2::TokenStream::from(item.clone())); + + let input: syn::ItemFn = parse_macro_input!(item); + let Transition { + current_state, + next_state, + message_type, + } = parse_macro_input!(attr); + + let name = input.sig.ident; + + let expanded = quote!( + #[hax_lib_macros::exclude] + impl TryFrom<#current_state> for (#next_state, #message_type) { + type Error = ProtocolError; + + fn try_from(value: #current_state) -> Result { + #name(value) + } + } + + #[hax_lib_macros::exclude] + impl WriteState for #current_state { + type NextState = #next_state; + type Message = #message_type; + + fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)> { + self.try_into() + } + } + ); + output.extend(expanded); + + return output.into(); +} + +/// Macro deriving a `ReadState` implementation for the destination state type, +/// consuming a message of `message_type` and the current state, as indicated by +/// the transition tuple. +/// +/// Example: +/// ```ignore +/// #[hax_lib_protocol_macros::read(A1, A2, Message)] +/// fn read_pong(_state: A1, msg: Message) -> ProtocolResult { +/// match msg { +/// Message::Ping(_) => Err(ProtocolError::InvalidMessage), +/// Message::Pong(received) => Ok(A2 { received }), +/// } +/// } +/// // The following is generated by the macro: +/// #[hax_lib_macros::exclude] +/// impl TryFrom<(A1, Message)> for A2 { +/// type Error = ProtocolError; +/// fn try_from((state, msg): (A1, Message)) -> Result { +/// read_pong(state, msg) +/// } +/// } +/// #[hax_lib_macros::exclude] +/// impl ReadState for A1 { +/// type Message = Message; +/// fn read(self, msg: Message) -> ProtocolResult { +/// A2::try_from((self, msg)) +/// } +/// } +/// ``` +#[proc_macro_attribute] +pub fn read( + attr: proc_macro::TokenStream, + item: proc_macro::TokenStream, +) -> proc_macro::TokenStream { + let mut output = quote!(#[hax_lib_macros::process_read]); + output.extend(proc_macro2::TokenStream::from(item.clone())); + + let input: syn::ItemFn = parse_macro_input!(item); + let Transition { + current_state, + next_state, + message_type, + } = parse_macro_input!(attr); + + let name = input.sig.ident; + + let expanded = quote!( + #[hax_lib_macros::exclude] + impl TryFrom<(#current_state, #message_type)> for #next_state { + type Error = ProtocolError; + + fn try_from((state, msg): (#current_state, #message_type)) -> Result { + #name(state, msg) + } + } + + #[hax_lib_macros::exclude] + impl ReadState<#next_state> for #current_state { + type Message = #message_type; + fn read(self, msg: Self::Message) -> ProtocolResult<#next_state> { + #next_state::try_from((self, msg)) + } + } + ); + output.extend(expanded); + + return output.into(); +} diff --git a/hax-lib-protocol/Cargo.toml b/hax-lib-protocol/Cargo.toml new file mode 100644 index 000000000..8f5c11cda --- /dev/null +++ b/hax-lib-protocol/Cargo.toml @@ -0,0 +1,13 @@ +[package] +name = "hax-lib-protocol" +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 + +[dependencies] diff --git a/hax-lib-protocol/src/lib.rs b/hax-lib-protocol/src/lib.rs new file mode 100644 index 000000000..d58a6ed58 --- /dev/null +++ b/hax-lib-protocol/src/lib.rs @@ -0,0 +1,57 @@ +//! This crate provides types and traits for implementing a protocol state +//! machine. +//! +//! A protocol party is conceived of as having a set of possible states, one of +//! which is the initial state. Transitioning to a different state is possible +//! either through receiving and processing a message or through writing a +//! message. + +/// A protocol error type. +#[derive(Debug)] +pub enum ProtocolError { + /// On receiving an unexpected message, i.e. one that does not allow a state + /// transition from the current state. + InvalidMessage, + /// On receiving invalid initialization data. + InvalidPrologue, +} + +pub type ProtocolResult = Result; + +/// A trait for protocol initial states. +pub trait InitialState { + /// Initializes the state given initialization data in `prologue`. + /// + /// Errors on invalid initialization data. + fn init(prologue: Option>) -> ProtocolResult + where + Self: Sized; +} + +/// A state where a message must be written before transitioning to the next state. +/// +/// `WriteState` can only be implemented once by every state type, implying that +/// in any protocol party state, if a message is to be written, that message and +/// the state the party is in after writing the message are uniquely determined. +pub trait WriteState { + /// The uniquely determined state that is transitioned to after writing the message. + type NextState; + /// The type of the message that is being written. + type Message; + /// Produce the message to be written when transitioning to the next state. + fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)>; +} + +/// A state where a message must be read before transitioning to the next state. +/// +/// A state type may implement `ReadState` multiple times, for different +/// instances of `NextState`, allowing the following state to depend on the +/// message that was received. +pub trait ReadState { + /// The type of message to be read. + type Message; + + /// Generate the next state based on the current state and the received + /// message. + fn read(self, msg: Self::Message) -> ProtocolResult; +} diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 454628b31..b6b739251 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -106,6 +106,20 @@ dependencies = [ "uuid", ] +[[package]] +name = "hax-lib-protocol" +version = "0.1.0-pre.1" + +[[package]] +name = "hax-lib-protocol-macros" +version = "0.1.0-pre.1" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.28", +] + [[package]] name = "if-let" version = "0.1.0" @@ -237,6 +251,15 @@ dependencies = [ name = "pattern-or" version = "0.1.0" +[[package]] +name = "ping-pong" +version = "0.1.0" +dependencies = [ + "hax-lib-macros", + "hax-lib-protocol", + "hax-lib-protocol-macros", +] + [[package]] name = "proc-macro-error" version = "1.0.4" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index 108febc8a..56a0a52a7 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -23,6 +23,7 @@ members = [ "reordering", "nested-derefs", "proverif-minimal", - "proverif-basic-structs" + "proverif-basic-structs", + "proverif-ping-pong" ] resolver = "2" diff --git a/tests/proverif-ping-pong/Cargo.toml b/tests/proverif-ping-pong/Cargo.toml new file mode 100644 index 000000000..4eda5a938 --- /dev/null +++ b/tests/proverif-ping-pong/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "ping-pong" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +hax-lib-protocol = { path = "../../hax-lib-protocol" } +hax-lib-protocol-macros = { path = "../../hax-lib-protocol-macros" } +hax-lib-macros = { path = "../../hax-lib-macros" } diff --git a/tests/proverif-ping-pong/pingpong.pv b/tests/proverif-ping-pong/pingpong.pv new file mode 100644 index 000000000..bd6d7a6cb --- /dev/null +++ b/tests/proverif-ping-pong/pingpong.pv @@ -0,0 +1,40 @@ +set attacker = passive. +channel c. + +type ping_t. +type pong_t. + +fun new_ping(): ping_t. +fun ping2pong(ping_t): pong_t. + +event PingSent(ping_t). +event PingReceived(ping_t). +event PongSent(pong_t). +event PongReceived(pong_t). + +query p: ping_t; + event(PingReceived(p)) ==> event(PingSent(p)). + + + +let A = + ( + let ping = new_ping() in + event PingSent(ping); + out(c, ping) + ) | ( + in(c, pong: pong_t); + event PongReceived(pong) + ). + +let B = + in(c, ping: ping_t); + event PingReceived(ping); + let pong = ping2pong(ping) in + event PongSent(pong); + out(c, pong); + 0. + +process + A | B + \ No newline at end of file diff --git a/tests/proverif-ping-pong/src/a.rs b/tests/proverif-ping-pong/src/a.rs new file mode 100644 index 000000000..0f72e5f24 --- /dev/null +++ b/tests/proverif-ping-pong/src/a.rs @@ -0,0 +1,97 @@ +use hax_lib_protocol::*; + +use crate::Message; + +// ==== A states ==== +pub struct A0 { + data: u8, +} + +pub struct A1 {} + +pub struct A2 { + #[allow(dead_code)] + received: u8, +} + +// ==== A initialization ==== +#[hax_lib_protocol_macros::init(A0)] +fn init_a(prologue: Vec) -> ProtocolResult { + if prologue.len() < 1 { + Err(ProtocolError::InvalidPrologue) + } else { + Ok(A0 { data: prologue[0] }) + } +} + +// The following generated by macro: +/* #[hax_lib_macros::exclude] +impl TryFrom> for A0 { + type Error = ProtocolError; + + fn try_from(value: Vec) -> Result { + init_a(value) + } +} + +#[hax_lib_macros::exclude] +impl InitialState for A0 { + fn init(prologue: Option>) -> ProtocolResult { + if let Some(prologue) = prologue { + prologue.try_into() + } else { + Err(ProtocolError::InvalidPrologue) + } + } +} */ + +// ==== A state transistion functions ==== +#[hax_lib_protocol_macros::write(A0, A1, Message)] +fn write_ping(state: A0) -> ProtocolResult<(A1, Message)> { + Ok((A1 {}, Message::Ping(state.data))) +} + +// The following generated by macro: +/*#[hax_lib_macros::exclude] +impl TryFrom for (A1, Message) { + type Error = ProtocolError; + + fn try_from(value: A0) -> Result { + write_ping(value) + } +} + +#[hax_lib_macros::exclude] +impl WriteState for A0 { + type NextState = A1; + type Message = Message; + + fn write(self) -> ProtocolResult<(Self::NextState, Message)> { + self.try_into() + } +}*/ + +#[hax_lib_protocol_macros::read(A1, A2, Message)] +fn read_pong(_state: A1, msg: Message) -> ProtocolResult { + match msg { + Message::Ping(_) => Err(ProtocolError::InvalidMessage), + Message::Pong(received) => Ok(A2 { received }), + } +} + +// The following generated by macro: +/*#[hax_lib_macros::exclude] +impl TryFrom<(A1, Message)> for A2 { + type Error = ProtocolError; + + fn try_from((state, msg): (A1, Message)) -> Result { + read_pong(state, msg) + } +} +#[hax_lib_macros::exclude] +impl ReadState for A1 { + type Message = Message; + fn read(self, msg: Message) -> ProtocolResult { + A2::try_from((self, msg)) + } +}*/ diff --git a/tests/proverif-ping-pong/src/b.rs b/tests/proverif-ping-pong/src/b.rs new file mode 100644 index 000000000..edd234679 --- /dev/null +++ b/tests/proverif-ping-pong/src/b.rs @@ -0,0 +1,111 @@ +use hax_lib_protocol::*; + +use crate::Message; + +// ==== B states ==== +pub struct B0 {} + +pub struct B1 { + received: u8, +} + +// An alternative successor of B0 to show read alternatives +pub struct B1alt {} + +pub struct B2 {} + +// ==== B initialization ==== +#[hax_lib_protocol_macros::init_empty(B0)] +fn init_b() -> ProtocolResult { + Ok(B0 {}) +} + +// The following generated by macro: +// #[hax_lib_macros::exclude] +// impl InitialState for B0 { +// fn init(prologue: Option>) -> ProtocolResult { +// if let Some(_) = prologue { +// Err(ProtocolError::InvalidPrologue) +// } else { +// init_b() +// } +// } +// } + +// ==== B state transistion functions ==== +#[hax_lib_protocol_macros::read(B0, B1, Message)] +fn read_ping(_state: B0, msg: Message) -> ProtocolResult { + match msg { + Message::Ping(received) => Ok(B1 { received }), + Message::Pong(_) => Err(ProtocolError::InvalidMessage), + } +} + +// The following generated by macro: +/*#[hax_lib_macros::exclude] +impl TryFrom<(B0, Message)> for B1 { + type Error = ProtocolError; + + fn try_from((state, msg): (B0, Message)) -> Result { + read_ping(state, msg) + } +} + +#[hax_lib_macros::exclude] +impl ReadState for B0 { + type Message = Message; + fn read(self, msg: Message) -> Result { + B1::try_from((self, msg)) + } +}*/ + +#[hax_lib_protocol_macros::read(B0, B1alt, Message)] +fn read_ping_alt(_state: B0, msg: Message) -> ProtocolResult { + match msg { + Message::Ping(received) if received == 42 => Ok(B1alt {}), + _ => Err(ProtocolError::InvalidMessage), + } +} + +// The following generated by macro: +/*#[hax_lib_macros::exclude] +impl TryFrom<(B0, Message)> for B1alt { + type Error = ProtocolError; + + fn try_from((state, msg): (B0, Message)) -> Result { + read_ping_alt(state, msg) + } +} + +#[hax_lib_macros::exclude] +impl ReadState for B0 { + type Message = Message; + fn read(self, msg: Message) -> Result { + B1alt::try_from((self, msg)) + } +}*/ + +#[hax_lib_protocol_macros::write(B1, B2, Message)] +fn write_pong(state: B1) -> ProtocolResult<(B2, Message)> { + Ok((B2 {}, Message::Pong(state.received))) +} + +// The following generated by macro: +/*#[hax_lib_macros::exclude] +impl TryFrom for (B2, Message) { + type Error = ProtocolError; + + fn try_from(value: B1) -> Result { + write_pong(value) + } +} + +#[hax_lib_macros::exclude] +impl WriteState for B1 { + type Message = Message; + type NextState = B2; + + fn write(self) -> Result<(Self::NextState, Message), ProtocolError> { + self.try_into() + } +}*/ diff --git a/tests/proverif-ping-pong/src/lib.rs b/tests/proverif-ping-pong/src/lib.rs new file mode 100644 index 000000000..f72bfd4da --- /dev/null +++ b/tests/proverif-ping-pong/src/lib.rs @@ -0,0 +1,23 @@ +mod a; +mod b; + +#[hax_lib_macros::protocol_messages] +pub enum Message { + Ping(u8), + Pong(u8), +} + +#[test] +fn run() { + use a::A0; + use b::{B0, B1}; + use hax_lib_protocol::{InitialState, ReadState, WriteState}; + let a = A0::init(Some(vec![1])).unwrap(); + let b = B0::init(None).unwrap(); + + let (a, msg) = a.write().unwrap(); + let b: B1 = b.read(msg).unwrap(); + + let (_b, msg) = b.write().unwrap(); + let _a = a.read(msg).unwrap(); +}