Crate anodized_core

Source

Expand description

§Anodized Core

This crate is the interoperability layer for tools connected to the Anodized specification system.

§Who Is This For?

If you want to add specifications to your code…

You’re looking for the anodized crate, which provides the #[spec] macro.
If you’re building a tool and want to work with Anodized specifications…

You’re in the right place! This crate provides the necessary components to parse and interact with Anodized specification annotations.
If you’re looking for blockchain smart contracts…

“These are not the contracts you’re looking for.” 🤖

But don’t leave yet! While Anodized is about Design by Contract (not blockchain), it can still help make your smart contracts more robust through formal specifications.

§Specification Syntax

The #[spec] attribute’s fields follow a specific grammar, which is formally defined using EBNF as follows.

fields = [ qualifiers ]
         [ requires_fields ]
       , [ maintains_fields ]
       (* not a typo: at most one `captures:` *)
       , [ captures_field ]
       , [ ensures_fields ];

qualifiers = { qualifier };
qualifier = `functional` | `pure` | `total`
          | `deterministic` | `effectfree` | `infallible` | `terminating`;

requires_fields  = { requires_field };
maintains_fields = { maintains_field };
ensures_fields   = { ensures_field };

requires_field  = [ cfg_attr ] , `requires:` , conditions, `,`;
maintains_field = [ cfg_attr ] , `maintains:` , conditions, `,`;
captures_field  = `captures:` , captures, `,`;
ensures_field   = [ cfg_attr ] , `ensures:` , postconds, `,`;

conditions = expr | condition_list;
condition_list = `[` , expr , { `,` , expr } , [ `,` ] , `]`;

captures = capture_stmt | capture_list;
capture_list = `[` , capture_stmt , { `,` , capture_stmt } , [ `,` ] , `]`;
capture_stmt = pattern , `=` , expr;

postconds = postcond_expr | postcond_list | postcond_list_closure;
postcond_list = `[` , postcond_expr , { `,` , postcond_expr } , [ `,` ] , `]`;
postcond_expr = expr | postcond_closure;
postcond_closure = `|` , pattern , `|` , expr;
postcond_list_closure = `|` , pattern , `|` , condition_list;

cfg_attr = `#[cfg(` , settings , `)]`;

Notes:

The last , is optional.
The fields rule defines a sequence of optional field groups that must appear in the specified order.
expr is a Rust expression.
pattern is an irrefutable Rust pattern.
settings is the content of the cfg attribute (e.g. test, debug_assertions).
Every valid spec field can be parsed as a Rust struct expression field.

§Instrumentation

The #[spec] macro transforms the function body by injecting code, determined by compiler cfg settings (e.g. anodized_panic, anodized_print). This process, known as instrumentation, follows a clear pattern.

Given an original function like this:

#[spec(
    requires: <PRECONDITION>,
    maintains: <INVARIANT>,
    captures: <ALIAS> = <CAPTURE_EXPR>,
    ensures: |<PATTERN>| <POSTCONDITION>,
)]
fn my_function(<FUNCTION_INPUTS>) -> <RETURN_TYPE> {
    <BODY>
}

The macro rewrites the body to be conceptually equivalent to the following:

fn my_function(<FUNCTION_INPUTS>) -> <RETURN_TYPE> {
    // 1. Preconditions and invariants are checked
    check!((|| <PRECONDITION>)(), "Precondition failed: <PRECONDITION>");
    check!((|| <INVARIANT>)(), "Pre-invariant failed: <INVARIANT>");

    // 2. Values are captured and the original function body is executed
    // Note 1: captures and body execution happen in a single tuple assignment
    //         to ensure captured values aren't accessible to the function body
    // Note 2: the body is evaluated in a closure, so returns inside the body
    //         do not bypass postcondition checks
    let (<ALIAS>, __anodized_output): (_, <RETURN_TYPE>) = (
        <CAPTURE_EXPR>,
        (|| { <BODY> })(),
    );

    // 3. Invariants and postconditions are checked
    // Note 1: Captured values are in scope for postconditions
    // Note 2: `__anodized_output` is also in scope for postconditions,
    //         but referring to it is strongly discouraged
    check!((|| <INVARIANT>)(), "Post-invariant failed: <INVARIANT>");
    // Postcondition is checked by invoking the closure with a reference to the return value
    check!(
        { let <PATTERN> = __anodized_output; (|| <POSTCONDITION>)() },
        "Postcondition failed: | <PATTERN> | <POSTCONDITION>",
    );

    // 4. The result is returned
    __anodized_output
}

When a condition has a #[cfg(...)] attribute, the corresponding check! is wrapped in an if cfg!(...) block. This follows standard Rust #[cfg] semantics: the check only runs when the configuration predicate is true. Details of the injected code are determined by cfg settings.

Modules§

annotate
instrument
qualifiers

Structs§

Capture: Captures an expression’s value at function entry.
Condition: A condition represented by a bool-valued expression.
DataSpec: Specifies the intended behavior of a data type: struct or enum.
LoopSpec: Specifies the intended behavior of a loop: while or for.
LoopVariant: Decreases with each run of a loop’s body.
PostCondition: A postcondition represented by a pattern to bind the output and a bool-valued expression.
Spec: Specifies the intended behavior of a function or method: fn.