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 } with { m_count: 5 }
}

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 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
  shrink: true
  max_local_rejects: 1024

Threaded into Foundry [profile.default.fuzz].