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, Hash, Eq, PartialEq, Ord, PartialOrd)]
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 std::fmt::Display for ItemUid {
26    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
27        std::fmt::Display::fmt(&self.uid, f)
28    }
29}
30
31impl ItemUid {
32    pub fn fresh() -> Self {
33        use uuid::Uuid;
34        let uid = format!("{}", Uuid::new_v4().simple());
35        ItemUid { uid }
36    }
37}
38
39/// What shall Hax do with an item?
40#[derive(Debug, Clone, Serialize, Deserialize, Hash, Eq, PartialEq, Ord, PartialOrd)]
41#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
42#[serde(rename = "HaItemStatus")]
43pub enum ItemStatus {
44    /// Include this item in the translation
45    Included {
46        /// Should Hax drop this item just before code generation?
47        late_skip: bool,
48    },
49    /// Exclude this item from the translation, optionally replacing it in the backends
50    Excluded { modeled_by: Option<String> },
51}
52
53/// An item can be associated to another one for multiple reasons:
54/// `AssociationRole` capture the nature of the (directed) relation
55/// between two items
56#[derive(Debug, Copy, Clone, Serialize, Deserialize, Hash, Eq, PartialEq, Ord, PartialOrd)]
57#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
58#[serde(rename = "HaAssocRole")]
59pub enum AssociationRole {
60    Requires,
61    Ensures,
62    Decreases,
63    SMTPat,
64    Refine,
65    /// A quoted piece of backend code to place after or before the
66    /// extraction of the marked item
67    ItemQuote,
68    ProcessRead,
69    ProcessWrite,
70    ProcessInit,
71    ProtocolMessages,
72}
73
74/// Where should a item quote appear?
75#[derive(Debug, Copy, Clone, Serialize, Deserialize, Hash, Eq, PartialEq, Ord, PartialOrd)]
76#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
77#[serde(rename = "HaItemQuotePosition")]
78pub enum ItemQuotePosition {
79    /// Should appear just before the item in the extraction
80    Before,
81    /// Should appear right after the item in the extraction
82    After,
83}
84
85/// F*-specific options for item quotes
86#[derive(Debug, Copy, Clone, Serialize, Deserialize, Hash, Eq, PartialEq, Ord, PartialOrd)]
87#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
88#[serde(rename = "HaItemQuoteFStarOpts")]
89pub struct ItemQuoteFStarOpts {
90    /// Shall we output this in F* interfaces (`*.fsti` files)?
91    pub intf: bool,
92    /// Shall we output this in F* implementations (`*.fst` files)?
93    pub r#impl: bool,
94}
95
96/// An item quote is a verbatim piece of backend code included in
97/// Rust. [`ItemQuote`] encodes the various options a item quote can
98/// have.
99#[derive(Debug, Copy, Clone, Serialize, Deserialize, Hash, Eq, PartialEq, Ord, PartialOrd)]
100#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
101#[serde(rename = "HaItemQuote")]
102pub struct ItemQuote {
103    pub position: ItemQuotePosition,
104    pub fstar_options: Option<ItemQuoteFStarOpts>,
105}
106
107/// The proof method to use for verification condition generation and discharge.
108#[derive(Debug, Copy, Clone, Serialize, Deserialize, Hash, Eq, PartialEq, Ord, PartialOrd)]
109#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
110#[serde(rename = "HaProofMethod")]
111pub enum ProofMethod {
112    BvDecide,
113    Grind,
114}
115
116/// Hax only understands one attribute: `#[hax::json(PAYLOAD)]` where
117/// `PAYLOAD` is a JSON serialization of an inhabitant of
118/// `AttrPayload`.
119#[derive(Debug, Clone, Serialize, Deserialize, Hash, Eq, PartialEq, Ord, PartialOrd)]
120#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
121#[serde(rename = "HaPayload")]
122pub enum AttrPayload {
123    ItemStatus(ItemStatus),
124    /// Mark an item as associated with another one
125    AssociatedItem {
126        /// What is the nature of the association?
127        role: AssociationRole,
128        /// What is the identifier of the target item?
129        item: ItemUid,
130    },
131    Uid(ItemUid),
132    /// Decides of the position of a item quote
133    ItemQuote(ItemQuote),
134    /// Mark an item so that hax never drop its body (this is useful
135    /// for pre- and post- conditions of a function we dropped the
136    /// body of: pre and post are part of type signature)
137    NeverErased,
138    NewtypeAsRefinement,
139    /// Mark an item as a lemma statement to prove in the backend
140    Lemma,
141    Language,
142    ProcessRead,
143    ProcessWrite,
144    ProcessInit,
145    Proof(String),
146    PureRequiresProof(String),
147    PureEnsuresProof(String),
148    ProofMethod(ProofMethod),
149    ProtocolMessages,
150    PVConstructor,
151    PVHandwritten,
152    TraitMethodNoPrePost,
153    /// Make an item opaque
154    Erased,
155    /// In the context of a set of fields (e.g. on a `struct`), overrides its
156    /// order. By default, the order of a field is its index, e.g. the first
157    /// field has order 0, the i-th field has order i+1. Rust fields order
158    /// matters: it rules how bits are represented. Once extracted, the order
159    /// matters, but for different reasons, e.g. a field is refined with
160    /// another, requiring a specific order.
161    Order(i32),
162}
163
164pub const HAX_TOOL: &str = "_hax";
165pub const HAX_CFG_OPTION_NAME: &str = "hax_compilation";
166
167pub struct HaxTool;
168pub struct HaxCfgOptionName;
169pub struct DebugOrHaxCfgExpr;
170impl ToTokens for HaxTool {
171    fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
172        format_ident!("{}", HAX_TOOL).to_tokens(tokens)
173    }
174}
175impl ToTokens for HaxCfgOptionName {
176    fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
177        format_ident!("{}", HAX_CFG_OPTION_NAME).to_tokens(tokens)
178    }
179}
180impl ToTokens for DebugOrHaxCfgExpr {
181    fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
182        quote! {any(#HaxCfgOptionName, debug_assertions)}.to_tokens(tokens)
183    }
184}
185
186use quote::*;
187
188impl From<&AttrPayload> for proc_macro2::TokenStream {
189    fn from(payload: &AttrPayload) -> Self {
190        let payload: String = serde_json::to_string(payload).unwrap();
191        quote! {#[cfg_attr(#HaxCfgOptionName, #HaxTool::json(#payload))]}
192    }
193}
194
195impl ToTokens for AttrPayload {
196    fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
197        proc_macro2::TokenStream::from(self).to_tokens(tokens)
198    }
199}
hax_lib_macros_types/lib.rs

hax_lib_macros_types/
lib.rs
