anodized-core 0.3.0

Core interoperability for the Anodized specification system
Documentation

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 parameters follow a specific grammar, which is formally defined using EBNF as follows.

params = [ requires_params ]
       , [ maintains_params ]
       (* not a typo: at most one `captures:` *)
       , [ captures_param ]
       (* not a typo: at most one `binds:` *)
       , [ binds_param ]
       , [ ensures_params ];

requires_params  = { requires_param };
maintains_params = { maintains_param };
ensures_params   = { ensures_param };

requires_param  = [ cfg_attr ] , `requires:` , conditions, `,`;
maintains_param = [ cfg_attr ] , `maintains:` , conditions, `,`;
captures_param  = `captures:` , captures, `,`;
binds_param     = `binds:` , pattern, `,`;
ensures_param   = [ cfg_attr ] , `ensures:` , post_conds, `,`;

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

captures = capture_expr | capture_list;
capture_list = `[` , capture_expr , { `,` , capture_expr } , [ `,` ] , `]`;
capture_expr = expr | (expr , `as` , ident);

post_conds = post_cond_expr | post_cond_list;
post_cond_list = `[` , post_cond_expr , { `,` , post_cond_expr } , [ `,` ] , `]`;
post_cond_expr = expr | closure_expr;

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

Notes:

  • The last , is optional.
  • The params rule defines a sequence of optional parameter groups that must appear in the specified order.
  • expr is a Rust expression; type checking will fail if it does not evaluate to bool.
  • closure_expr is a Rust closure that receives the function's return value as a reference; type checking will fail if it does not evaluate to bool.
  • pattern is an irrefutable Rust pattern; type checking will fail if its type does not match the function's return value.
  • settings is the content of the cfg attribute (e.g. test, debug_assertions).

Runtime Checks

The #[spec] macro transforms the function body by injecting runtime checks whose behavior is controlled by runtime-* feature settings. This process, known as instrumentation, follows a clear pattern.

Given an original function like this:

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

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

fn my_function(<ARGUMENTS>) -> <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!(
        (|<PATTERN>: &<RETURN_TYPE>| <POSTCONDITION>)(&__anodized_output),
        "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. The behavior of the check! itself is controlled by the global runtime-* feature setting.