hax_lib_macros_types/
lib.rs

1use serde::{Deserialize, Serialize};
2
3/// Each item can be marked with a *u*nique *id*entifier. This is
4/// useful whenever the payload of an attribute is a piece of Rust code
5/// (an expression, a path, a type...). We don't want to retrieve those
6/// pieces of Rust code as raw token stream: we want to let Rustc give
7/// meaning to those. For instance, we want Rustc to type expressions
8/// and to resolve paths.
9///
10/// Thus, we expand attributes with Rust-code-payloads as top-level
11/// items marked with an `ItemUid`. The attributes are then replaced
12/// in place with a simple reference (the `ItemUid` in stake).
13///
14/// Morally, we expand `struct Foo { #[refine(x > 3)] x: u32 }` to:
15///  1. `#[uuid(A_UNIQUE_ID_123)] fn refinement(x: u32) -> hax_lib::Prop {x > 3}`;
16///  2. `struct Foo { #[refined_by(A_UNIQUE_ID_123)] x: u32 }`.
17#[derive(Debug, Clone, Serialize, Deserialize)]
18#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
19#[serde(rename = "HaUid")]
20pub struct ItemUid {
21    /// Currently, this is a UUID.
22    pub uid: String,
23}
24
25impl ItemUid {
26    pub fn fresh() -> Self {
27        use uuid::Uuid;
28        let uid = format!("{}", Uuid::new_v4().simple());
29        ItemUid { uid }
30    }
31}
32
33/// What shall Hax do with an item?
34#[derive(Debug, Clone, Serialize, Deserialize)]
35#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
36#[serde(rename = "HaItemStatus")]
37pub enum ItemStatus {
38    /// Include this item in the translation
39    Included {
40        /// Should Hax drop this item just before code generation?
41        late_skip: bool,
42    },
43    /// Exclude this item from the translation, optionally replacing it in the backends
44    Excluded { modeled_by: Option<String> },
45}
46
47/// An item can be associated to another one for multiple reasons:
48/// `AssociationRole` capture the nature of the (directed) relation
49/// between two items
50#[derive(Debug, Copy, Clone, Serialize, Deserialize)]
51#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
52#[serde(rename = "HaAssocRole")]
53pub enum AssociationRole {
54    Requires,
55    Ensures,
56    Decreases,
57    SMTPat,
58    Refine,
59    /// A quoted piece of backend code to place after or before the
60    /// extraction of the marked item
61    ItemQuote,
62    ProcessRead,
63    ProcessWrite,
64    ProcessInit,
65    ProtocolMessages,
66}
67
68/// Where should a item quote appear?
69#[derive(Debug, Copy, Clone, Serialize, Deserialize)]
70#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
71#[serde(rename = "HaItemQuotePosition")]
72pub enum ItemQuotePosition {
73    /// Should appear just before the item in the extraction
74    Before,
75    /// Should appear right after the item in the extraction
76    After,
77}
78
79/// F*-specific options for item quotes
80#[derive(Debug, Copy, Clone, Serialize, Deserialize)]
81#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
82#[serde(rename = "HaItemQuoteFStarOpts")]
83pub struct ItemQuoteFStarOpts {
84    /// Shall we output this in F* interfaces (`*.fsti` files)?
85    pub intf: bool,
86    /// Shall we output this in F* implementations (`*.fst` files)?
87    pub r#impl: bool,
88}
89
90/// An item quote is a verbatim piece of backend code included in
91/// Rust. [`ItemQuote`] encodes the various options a item quote can
92/// have.
93#[derive(Debug, Copy, Clone, Serialize, Deserialize)]
94#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
95#[serde(rename = "HaItemQuote")]
96pub struct ItemQuote {
97    pub position: ItemQuotePosition,
98    pub fstar_options: Option<ItemQuoteFStarOpts>,
99}
100
101/// Hax only understands one attribute: `#[hax::json(PAYLOAD)]` where
102/// `PAYLOAD` is a JSON serialization of an inhabitant of
103/// `AttrPayload`.
104#[derive(Debug, Clone, Serialize, Deserialize)]
105#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
106#[serde(rename = "HaPayload")]
107pub enum AttrPayload {
108    ItemStatus(ItemStatus),
109    /// Mark an item as associated with another one
110    AssociatedItem {
111        /// What is the nature of the association?
112        role: AssociationRole,
113        /// What is the identifier of the target item?
114        item: ItemUid,
115    },
116    Uid(ItemUid),
117    /// Decides of the position of a item quote
118    ItemQuote(ItemQuote),
119    /// Mark an item so that hax never drop its body (this is useful
120    /// for pre- and post- conditions of a function we dropped the
121    /// body of: pre and post are part of type signature)
122    NeverErased,
123    NewtypeAsRefinement,
124    /// Mark an item as a lemma statement to prove in the backend
125    Lemma,
126    Language,
127    ProcessRead,
128    ProcessWrite,
129    ProcessInit,
130    ProtocolMessages,
131    PVConstructor,
132    PVHandwritten,
133    TraitMethodNoPrePost,
134    /// Make an item opaque
135    Erased,
136    /// In the context of a set of fields (e.g. on a `struct`), overrides its
137    /// order. By default, the order of a field is its index, e.g. the first
138    /// field has order 0, the i-th field has order i+1. Rust fields order
139    /// matters: it rules how bits are represented. Once extracted, the order
140    /// matters, but for different reasons, e.g. a field is refined with
141    /// another, requiring a specific order.
142    Order(i32),
143}
144
145pub const HAX_TOOL: &str = "_hax";
146pub const HAX_CFG_OPTION_NAME: &str = "hax_compilation";
147
148pub struct HaxTool;
149pub struct HaxCfgOptionName;
150pub struct DebugOrHaxCfgExpr;
151impl ToTokens for HaxTool {
152    fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
153        format_ident!("{}", HAX_TOOL).to_tokens(tokens)
154    }
155}
156impl ToTokens for HaxCfgOptionName {
157    fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
158        format_ident!("{}", HAX_CFG_OPTION_NAME).to_tokens(tokens)
159    }
160}
161impl ToTokens for DebugOrHaxCfgExpr {
162    fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
163        quote! {any(#HaxCfgOptionName, debug_assertions)}.to_tokens(tokens)
164    }
165}
166
167use quote::*;
168
169impl From<&AttrPayload> for proc_macro2::TokenStream {
170    fn from(payload: &AttrPayload) -> Self {
171        let payload: String = serde_json::to_string(payload).unwrap();
172        quote! {#[cfg_attr(#HaxCfgOptionName, #HaxTool::json(#payload))]}
173    }
174}
175
176impl ToTokens for AttrPayload {
177    fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
178        proc_macro2::TokenStream::from(self).to_tokens(tokens)
179    }
180}
hax_lib_macros_types/lib.rs

hax_lib_macros_types/
lib.rs
