#[pv_constructor]
A marker indicating a fn should be automatically translated to a ProVerif constructor.
fn