Skip to main content

Crate anodized_core

Crate anodized_core 

Source
Expand description
Anodized Logo

§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:` , pre_conditions, `,`;
maintains_param = [ cfg_attr ] , `maintains:` , pre_conditions, `,`;
captures_param  = `captures:` , captures, `,`;
binds_param     = `binds:` , pattern, `,`;
ensures_param   = [ cfg_attr ] , `ensures:` , post_conditions, `,`;

pre_conditions = pre_condition_expr | pre_condition_list;
pre_condition_list = `[` , pre_condition_expr , { `,` , pre_condition_expr } , [ `,` ] , `]`;
pre_condition_expr = expr | pre_closure_expr;

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

post_conditions = post_condition_expr | post_condition_list;
post_condition_list = `[` , post_condition_expr , { `,` , post_condition_expr } , [ `,` ] , `]`;
post_condition_expr = expr | post_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.
  • pre_closure_expr is a Rust closure that receives no inputs and returns bool; type checking will fail if it does not evaluate to bool and does not take no arguments.
  • post_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).

§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: <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. Details of the injected code are determined by cfg settings.

Modules§

annotate
instrument
qualifiers

Structs§

Capture
Captures an expression’s value at function entry.
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 closure that takes the return value as a reference.
PreCondition
A precondition represented by a bool-valued expression.
Spec
Specifies the intended behavior of a function or method: fn.