Attribute Macro machine_description

#[machine_description]

Processes a module so that it can be used in machine-check verification.

To efficiently verify a system with machine-check, verification equivalents of the system that allow more advanced reasoning (e.g. not caring about the value of some variable unless found to be necessary) must be created, which is done by enclosing the system code in a module and applying this macro on it.

In practice, everything used in Machine must be processed by this macro. System construction, however, can (and should) be done outside.

Note that, due to a Rust issue, procedural macros currently cannot be used as inner attributes, so this is the currently recommended way of using the macro:

#[machine_check::machine_description]
mod machine_module {
    // ... structs implementing Input, State, Machine ...
}

The macro is currently rather limited in the subset of Rust code it can process, and errors may be cryptic. Improvements are planned in the future. For now, the examples in the crate show code processable without errors.