Enum Command 

pub enum Command<E: Extension> {
    Backend(BackendOptions<E>),
    Extract {
        names: Vec<String>,
        packages: Vec<String>,
        dry_run: bool,
        verbose: u8,
        hermeticity: CargoHermeticityOptions,
    },
    JSON {
        output_file: PathOrDash,
        kind: Vec<ExportBodyKind>,
        use_ids: bool,
        include_extra: bool,
    },
    Serialize {
        kind: Vec<ExportBodyKind>,
        backend: Option<BackendName>,
    },
    Tools(ToolsCommand),
    CliExtension(E::Command),
}

Variants

Backend(BackendOptions<E>)

Translate to a backend. The translated modules will be written under the directory <PKG>/proofs/<BACKEND>/extraction, where <PKG> is the translated cargo package name and <BACKEND> the name of the backend.

Extract

Run the proof scenarios declared in hax.toml ([scenario.<name>] tables): named, complete extraction configurations. Without names, every scenario in scope runs. Scenarios run sequentially; a failing scenario does not abort the run, failures are reported in a summary and produce a non-zero exit code.

Fields

names: Vec<String>

The scenarios to run. Each name selects every scenario with that name in scope. Absent, every scenario in scope runs.

packages: Vec<String>

Restrict the scope to the scenarios extracting the given package. May be repeated.

dry_run: bool

Print the resolved invocations, including the arguments compiled from the scenarios, without running them.

verbose: u8

Verbose mode, forwarded to each scenario run.

hermeticity: CargoHermeticityOptions

JSON

Export directly as a JSON file

Fields

output_file: PathOrDash

Path to the output JSON file, “-” denotes stdout.

kind: Vec<ExportBodyKind>

Whether the bodies are exported as THIR, built MIR, const MIR, or a combination. Repeat this option to extract a combination (e.g. -k thir -k mir-built). Pass --kind alone with no value to disable body extraction.

use_ids: bool

By default, cargo hax json outputs a JSON where every piece of information is inlined. This however creates very large JSON files. This flag enables the use of unique IDs and outputs a map from IDs to actual objects.

include_extra: bool

Whether to include extra informations about DefIds.

Serialize

Serialize to a haxmeta file, the internal binary format used by hax to store the ASTs produced by the hax exporter.

Fields

kind: Vec<ExportBodyKind>

Whether the bodies are exported as THIR, built MIR, const MIR, or a combination. Repeat this option to extract a combination (e.g. -k thir -k mir-built). Pass --kind alone with no value to disable body extraction.

backend: Option<BackendName>

When extracting to a given backend, the exporter is called with different cfg options. This option allows to set the same flags as cargo hax into would pick.

Tools(ToolsCommand)

Manage the external tools hax depends on (e.g. charon and aeneas).

CliExtension(E::Command)

Implementations

impl<E: Extension> Command<E>

pub fn body_kinds(&self) -> Vec<ExportBodyKind>

pub fn backend_name(&self) -> Option<BackendName>

Trait Implementations

impl<E: Clone + Extension> Clone for Command<E>

where E::Command: Clone,

fn clone(&self) -> Command<E>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<E: Debug + Extension> Debug for Command<E>

where E::Command: Debug,

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de, E> Deserialize<'de> for Command<E>

where E: Deserialize<'de> + Extension, E::Command: Deserialize<'de>,

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl<E: Extension> FromArgMatches for Command<E>

fn from_arg_matches(__clap_arg_matches: &ArgMatches) -> Result<Self, Error>

Instantiate Self from ArgMatches, parsing the arguments as needed.

fn from_arg_matches_mut( __clap_arg_matches: &mut ArgMatches, ) -> Result<Self, Error>

Instantiate Self from ArgMatches, parsing the arguments as needed.

fn update_from_arg_matches( &mut self, __clap_arg_matches: &ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

fn update_from_arg_matches_mut<'b>( &mut self, __clap_arg_matches: &mut ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

impl<E: Extension + JsonSchema> JsonSchema for Command<E>

fn schema_name() -> String

The name of the generated JSON Schema.

fn schema_id() -> Cow<'static, str>

Returns a string that uniquely identifies the schema produced by this type.

fn json_schema(generator: &mut SchemaGenerator) -> Schema

Generates a JSON Schema for this type.

fn is_referenceable() -> bool

Whether JSON Schemas generated for this type should be re-used where possible using the $ref keyword.

impl<E: Extension> NormalizePaths for Command<E>

fn normalize_paths(&mut self)

impl<E: PartialEq + Extension> PartialEq for Command<E>

where E::Command: PartialEq,

fn eq(&self, other: &Command<E>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<E> Serialize for Command<E>

where E: Serialize + Extension, E::Command: Serialize,

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl<E: Extension> Subcommand for Command<E>

fn augment_subcommands<'b>(__clap_app: Command) -> Command

Append to Command so it can instantiate Self via FromArgMatches::from_arg_matches_mut

fn augment_subcommands_for_update<'b>(__clap_app: Command) -> Command

Append to Command so it can instantiate self via FromArgMatches::update_from_arg_matches_mut

fn has_subcommand(__clap_name: &str) -> bool

Test whether Self can parse a specific subcommand

impl<E: Eq + Extension> Eq for Command<E>

where E::Command: Eq,

impl<E: Extension> StructuralPartialEq for Command<E>