Macro cvlr_rules 

macro_rules! cvlr_rules {
    (name: $name:literal, spec: $spec:expr, bases: [ $( $base:ident ),* $(,)? ] ) => { ... };
}

Defines multiple rules for a specification across multiple base functions.

This macro is a convenience macro that generates multiple rule definitions by calling cvlr_rule_for_spec! for each base function in the list. Each rule will have the same name and specification, but will be applied to different base functions.

Syntax

cvlr_rules! {
    name: "rule_name",
    spec: spec_expression,
    bases: [
        base_function1,
        base_function2,
        base_function3,
    ]
}

Parameters

• name - A string literal that will be converted to snake_case and combined with each base function name
• spec - An expression representing the specification (must implement CvlrSpec)
• bases - A list of function identifiers (if they start with base_, that prefix is stripped)

Expansion

This macro expands to multiple calls to cvlr_rule_for_spec!, one for each base function:

// Input:
cvlr_rules! {
    name: "solvency",
    spec: my_spec,
    bases: [base_function1, base_function2]
}

// Expands to:
cvlr_rule_for_spec!{name: "solvency", spec: my_spec, base: base_function1}
cvlr_rule_for_spec!{name: "solvency", spec: my_spec, base: base_function2}

Examples

use cvlr_spec::{cvlr_rules, cvlr_spec, cvlr_predicate};

struct Counter {
    value: i32,
}

// Create a spec
let my_spec = cvlr_spec! {
    requires: cvlr_predicate! { | c : Counter | -> { c.value > 0 } },
    ensures: cvlr_predicate! { | c : Counter | -> { c.value >= 0 } }
};

// Define rules for multiple functions
cvlr_rules! {
    name: "solvency",
    spec: my_spec,
    bases: [
        base_update_counter,
        base_reset_counter,
        base_increment_counter,
    ]
}

This will create three rules:

• solvency_update_counter
• solvency_reset_counter
• solvency_increment_counter