hax_types/
lib.rs

1#![cfg_attr(feature = "rustc", feature(rustc_private))]
2//! This crate contains the type definitions that are used to communicate between:
3//!  - the command line (the `cargo-hax` binary);
4//!  - the custom rustc driver;
5//!  - the hax engine (the `hax-engine` binary).
6//!
7//! Those three component send and receive messages in JSON or CBOR on
8//! stdin and stdout.
9
10pub(crate) mod prelude;
11
12/// The CLI options for `cargo-hax`. The types defines in this module
13/// are also used by the driver and the engine.
14pub mod cli_options;
15
16/// Type to represent errors, mainly in `hax-engine`. The engine
17/// doesn't do any reporting itself: it only sends JSON to its stdout,
18/// and `cargo-hax` takes care of reporting everything in a rustc
19/// style.
20pub mod diagnostics;
21
22/// The types used to communicate between `cargo-hax` and the custom
23/// driver.
24pub mod driver_api;
25
26/// The types used to communicate between `cargo-hax` and
27/// `hax-engine`.
28pub mod engine_api;
29
30/// Compile-time version of hax
31pub const HAX_VERSION: &str = env!("HAX_VERSION");
32
33/// Tool pins, baked in at build time from the workspace-root `pins.toml` (see
34/// `build.rs`). Read here once so every consumer (`cargo-hax`'s lean
35/// backend, the `--help` text) shares a single source of truth. `build.rs`
36/// requires a complete `pins.toml` (failing the build otherwise), so these are
37/// always present and non-empty in a successfully built binary.
38pub mod pins {
39    /// Short commit SHA `aeneas -version` is expected to report.
40    pub const AENEAS_VERSION: &str = env!("HAX_AENEAS_PIN_VERSION");
41    /// Source repository of the pinned aeneas.
42    pub const AENEAS_REPO: &str = env!("HAX_AENEAS_PIN_REPO");
43    /// Version `charon version` is expected to report.
44    pub const CHARON_VERSION: &str = env!("HAX_CHARON_PIN_VERSION");
45    /// Lean toolchain written to generated `lean-toolchain` files.
46    pub const LEAN_TOOLCHAIN: &str = env!("HAX_LEAN_PIN_TOOLCHAIN");
47    /// Source repository of the Hax lean proof library.
48    pub const LEAN_LIB_REPO: &str = env!("HAX_LEAN_LIB_PIN_REPO");
49    /// Commit of the Hax lean proof library.
50    pub const LEAN_LIB_VERSION: &str = env!("HAX_LEAN_LIB_PIN_VERSION");
51}
hax_types/lib.rs

hax_types/
lib.rs
