Macro cvlr_lemma 

macro_rules! cvlr_lemma {
    ($name: ident ( $c:ident : $ctx: ident ) {
        requires -> { $($requires:tt)* }
        ensures -> { $($ensures:tt)* } }) => { ... };
    ($name:ident for $ctx:ident { requires: $r:expr , ensures: $e:expr $(,)? }) => { ... };
}

Defines a lemma with preconditions (requires) and postconditions (ensures).

This macro creates a new type implementing CvlrLemma for the specified context. A lemma is a logical statement: if the preconditions hold, then the postconditions must also hold. Lemmas can be verified using the verify or verify_with_context methods.

Syntax

The macro supports two syntax forms:

Form 1: Block syntax with inline expressions

cvlr_lemma! {
    <name> ( <context_var> : <context_type> ) {
        requires -> {
            <requires_expr1>;
            <requires_expr2>;
            ...
        }
        ensures -> {
            <ensures_expr1>;
            <ensures_expr2>;
            ...
        }
    }
}

Form 2: Expression syntax with pre-built predicates

cvlr_lemma! {
    <name> for <context_type> {
        requires: <requires_expr>,
        ensures: <ensures_expr>,
    }
}

Parameters

Form 1 parameters:

• name - The name of the lemma type to create
• context_var - The variable name to use for the context in the requires/ensures clauses
• context_type - The type of the context (must implement Nondet and CvlrLog)
• requires - One or more expressions that form the preconditions
• ensures - One or more expressions that form the postconditions

Form 2 parameters:

• name - The name of the lemma type to create
• context_type - The type of the context (must implement Nondet and CvlrLog)
• requires - A single expression (predicate, identifier, or composed expression) that forms the preconditions
• ensures - A single expression (predicate, identifier, or composed expression) that forms the postconditions

Returns

Creates a struct with the given name that implements CvlrLemma with Context = Ctx.

Examples

extern crate cvlr;
use cvlr_spec::cvlr_lemma;

// Counter must implement Nondet and CvlrLog for lemma verification
#[derive(cvlr::derive::Nondet, cvlr::derive::CvlrLog)]
struct Counter {
    value: i32,
}

// Define a lemma: if value > 0, then value > 0 (trivial but demonstrates syntax)
cvlr_lemma! {
    CounterPositiveLemma(c: Counter) {
        requires -> {
            c.value > 0
        }
        ensures -> {
            c.value > 0
        }
    }
}

// Use the lemma
let lemma = CounterPositiveLemma;
lemma.verify(); // Verifies the lemma holds for all contexts

More complex example:

extern crate cvlr;
use cvlr_spec::cvlr_lemma;

#[derive(cvlr::derive::Nondet, cvlr::derive::CvlrLog)]
struct Counter {
    value: i32,
}

cvlr_lemma! {
    CounterDoublesLemma(c: Counter) {
        requires -> {
            c.value > 0;
            c.value < 100
        }
        ensures -> {
            c.value > 0;
            c.value * 2 > c.value
        }
    }
}

Form 2: Using pre-built predicates or expressions

This form is useful when you already have predicates defined or want to use composed expressions:

extern crate cvlr;
use cvlr_spec::{cvlr_lemma, cvlr_predicate, cvlr_and};

#[derive(cvlr::derive::Nondet, cvlr::derive::CvlrLog)]
struct Counter {
    value: i32,
}

// Define predicates separately
let positive_pred = cvlr_predicate! { | c : Counter | -> { c.value > 0 } };
let bounded_pred = cvlr_predicate! { | c : Counter | -> { c.value < 100 } };

// Use them in a lemma with the expression syntax
cvlr_lemma! {
    CounterBoundedLemma for Counter {
        requires: cvlr_and!(positive_pred, bounded_pred),
        ensures: positive_pred,
    }
}

// Or use identifier predicates
cvlr_def_predicate! {
    pred IsPositive(c: Counter) {
        c.value > 0
    }
}

cvlr_lemma! {
    CounterPositiveLemma for Counter {
        requires: IsPositive,
        ensures: IsPositive,
    }
}

Verification

When verifying a lemma:

1. The preconditions (requires) are assumed to hold
2. The postconditions (ensures) are asserted to hold

If the postconditions don’t hold when the preconditions are assumed, the verification will fail.