Invariants
Stateful invariants fuzz sequences of actions: the harness picks from a declared action pool, applies each call, and re-checks boolean predicates after every successful step. Use them for state-machine bugs that single-call properties miss.
Single-entity form
invariant "count never exceeds bound" for Counter {
init { m_count: 0 }
senders { 0xAA00000000000000000000000000000000000001,
0xBB00000000000000000000000000000000000002 }
action increment(amount: u64) {
bound amount in 0..1000
}
action reset() { }
check m_count <= 1_000_000_000
}
invariant "reset must succeed" for Counter
#[fail_on_revert]
{
action increment(amount: u64) { bound amount in 0..100 }
action reset() { }
check m_count >= 0
}
| Construct | Meaning |
|---|---|
init { … } / with { … } | Initial entity state; supports * forall (sampled on Foundry; ∀ on Lean). Identity members may be set here for address resolution |
ctx { … } | Message / system context for the trace |
senders { … } | Optional sender pool (round-robin); default is a zero sender |
action route(params) { bound|assume|skip if } | Callable routes; body may only hold preconditions / advanceTime |
check <bool> | Conjoined after every successful call |
#[fail_on_revert] | Any revert fails the trace (default: skip reverting steps) |
Action gates: assume vs skip if
| Keyword | When false |
|---|---|
assume <expr> | Step excluded (vm.assume; Lean adds traceValid … →) |
skip if <expr> | Step is a no-op (counts toward length, state unchanged) |
bound v in lo..hi | Reject out-of-range parameter samples |
An invariant with no assume emits no stepValid/traceValid machinery on Lean (byte-identical to older output).
trace::*
Inside assume / check only (I15/I16):
| Accessor | Meaning |
|---|---|
trace::length | Actions before this point (assume) or full length (check) |
trace::count(route) | How often route ran (must name a declared action) |
trace::lastWas(route) | Previous action was route |
invariant "deposits lead withdrawals" for Vault {
init { m_balance: 0 }
action deposit(amount: u64) {
bound amount in 1..100
assume trace::length < 10
}
action withdraw(amount: u64) {
bound amount in 1..100
assume m_balance >= amount
assume !trace::lastWas(withdraw)
assume trace::count(withdraw) <= trace::count(deposit)
}
check m_balance >= 0
check trace::count(deposit) >= trace::count(withdraw)
}
Accumulators are emitted only when referenced (Lean TraceAcc; Foundry handler counters).
track / derived / excludes (Foundry-rich)
invariant "borrowed never exceeds total assets" for LendingPair
#[tag("INV-LEND-001")]
#[runs(2000)]
#[depth(80)]
#[with_time]
{
init { m_total_assets: 1000, m_borrowed: 0 }
track {
let initial_total = m_total_assets
}
derived utilization() -> u128 {
return (m_borrowed * 100) / m_total_assets
}
exclude senders { 0x0000000000000000000000000000000000000001 }
exclude selectors { accrueInterest }
action deposit(amount: u128) { bound amount in 1..m_total_assets }
action withdraw(amount: u128) {
skip if m_total_assets == 0
bound amount in 1..m_total_assets
}
action accrueInterest() { advanceTime(3600) }
check m_borrowed <= m_total_assets
}
| Attribute / block | Effect |
|---|---|
#[runs(N)] / #[depth(N)] | Per-decl Foundry forge-config invariant runs/depth |
#[with_time] | Synthetic advanceTime(secs) in the selector set (vm.warp + vm.roll) |
#[fail_on_revert] | Fail traces on any revert |
#[tag("…")] | NatSpec / function-name suffix for audit trails |
track { let … } | Snapshot fields captured once in the handler |
derived name(…) -> T | Pure view helper on the handler |
exclude senders / exclude selectors | Foundry excludeSender / excludeSelector |
track / derived / excludes are richest on Foundry; other backends may ignore some of these constructs at codegen time.
Multi-entity systems
invariant "vault sum covers treasury" for { v: Vault, a: Vault, t: Treasury } {
init v { m_balance: 0 }
init a { m_balance: 0 }
init t { m_total: 0 }
action v.deposit(amount: u64) { bound amount in 0..1000 }
action a.deposit(amount: u64) { bound amount in 0..1000 }
action t.credit(amount: u64) { bound amount in 0..1000 }
check v.m_balance + a.m_balance >= t.m_total
}
Actions and member refs must be qualified (I9/I11). Supported on Foundry and Lean.
Project defaults
invariant:
runs: 256
depth: 50
fail_on_revert: false
seed: 0
max_local_rejects: 1024
Per-invariant attributes override the global fail_on_revert / runs / depth where applicable.