Properties and Fuzz

A property is Cambrian’s abstract, parameterised statement about an entity. It is the canonical construct for property-based testing and for Lean specifications.

Shape

1. Typed parameters attach to the property name (before for).
2. The body holds logical steps only: msg/sys or ctx, let, assume, call, expect*.
3. Concrete test and randomised fuzz instances nest inside the property.

property "increment is monotonic" (amount: u64) for Counter with { m_count: 0 } {
    assume amount % 2 == 0
    call increment(amount)
    expect state { m_count: amount }

    test "even-4" { amount: 4 }
    fuzz "small" { amount in 0..1000 }
    #[runs(2000)] fuzz "wide" { amount in 0..=1000 }
}

An instance may also carry its own with { … } to override the property’s initial state — the body’s expectations must then still hold from that state.

Boolean expect

A postcondition that is not equality is a boolean expect. The expression is ordinary Cambrian (comparisons, && / || / !, arithmetic, field and index access). It is legal in property, test, and fuzz bodies.

entity Purse {
    routes {
        spend(to: address, amount: U256) -> U256
            where (m_balance >= amount) : throw 1
        => [
            return(m_balance)
        ]
    }

    m_balance: U256 {
        in spend(to, amount) => m_balance - amount
    }

    m_spent: U256 {
        in spend(to, amount) => m_spent + amount
    }
}

property "spend moves funds" (to: address, amount: U256, start: U256) for Purse with { m_balance: start } {
    assume amount > 0 && start >= amount
    call spend(to, amount)
    expect return == start - amount
    expect m_balance <= start
    expect m_spent + m_balance == start
    expect return > 0 || amount == start
}

• expect return E and expect return == E stay equality assertions. expect return.field == … stays an equality lens. Relational operators are predicates.
• A bare member name is the post-state field after that call. with { m_balance: start } (or a parameter) names the starting value. with { m_balance: * } still quantifies the initial value, but m_balance inside the predicate is the post-state field.
• Elsewhere in the predicate, the preceding call’s return value is the name result. If a parameter, let, or member is also called result and the predicate mentions it, validation reports T38.
• expect state { … } stays a list of equalities.

Notes:

• Write for Counter, never for Counter(amount: u64).
• Sampling bounds belong in fuzz instances, not the property body (T11).
• Instance forms: test { p: value, … } (every param fixed) and fuzz { p in lo..hi, … } (ranges; omitted params use the full type range).
• Property-level with is the default initial state; instances may override with their own with.
• Instance attributes include #[runs(N)] (fuzz), #[tag("…")], #[skip_from].
• A property with no instances still emits output: full-range fuzz if it has params or forall markers, or a deterministic test if not. Lean always emits one theorem per property.

assume vs bound

Lean quantifies over the full parameter type with only genuine assumes — fuzz ranges never weaken the theorem.

Forall marker *

property "reset zeroes from any start" for Counter with { m_count: * } {
    call reset()
    expect state { m_count: 0 }
}

property "holds for any state" for Counter with { * } {
    call reset()
    expect state { m_count: 0 }
}

with vs ctx

Entity state and call context are separate records:

property "incr from any sender" (amount: u64) for Counter
    with { m_count: 0 }
    ctx { msg::sender: * } {
    call increment(amount)
    expect state { m_count: amount }
    fuzz { amount in 0..10 }
}

Allowed context names: msg::{sender,value}, sys::{now,timestamp,chainid,block_number,balance} (T20). Context markers inside with → T22.

Per-target:

How Foundry runs properties

On --target evm, each nested instance becomes a runnable harness:

• fuzz instance → fuzz case with bound p in lo..hi, then the logical body.
• test instance → concrete test with let p = value; assumes are dropped (values are presumed valid).

Lean keeps the property as a single theorem instead (see Lean-EVM).

How preconditions lower:

Unsupported fuzz parameter types warn with W7 rather than failing the build.

Project-wide fuzz knobs

fuzz:
  runs: 256
  seed: 0
  max_local_rejects: 1024

Threaded into Foundry [profile.default.fuzz]. (fuzz.shrink is accepted but has no effect; the compiler warns about it.)