Macro manual_proof 

macro_rules! manual_proof {
    ($(#[doc = $doc:expr])+hook = $hook:expr $(,)?) => { ... };
    ($(#[doc = $doc:expr])+) => { ... };
}

Fulfills a proof parameter by declaring a human-written justification for why the algebraic property (e.g. commutativity, idempotence) holds.

The argument must be a doc comment explaining why the property is satisfied.

Examples

// stream: [1, 2, 3] (unordered)
stream
    .fold(
        q!(|| 0),
        q!(
            |acc, x| *acc += x,
            commutative = manual_proof!(/** integer addition is commutative */)
        ),
    )
    .into_stream()

An optional trailing hook = ... argument attaches a simulator ordering hook to a commutativity proof (see hydro_lang::sim::hooks). The simulator does not trust manual proofs — it still explores the input ordering — so the hook lets a simulation test script that exploration:

commutative = manual_proof!(/** set insert is commutative */ hook = my_ordering_hook)