Unit Tests

A test declares a concrete scenario against one entity: optional initial state, message/system setup, one or more calls, and expect* assertions.

Syntax

test "fund changes state" for Escrow {
    let buyer = 0x0000000000000000000000000000000000000001
    let seller = 0x0000000000000000000000000000000000000002
    let arbiter = 0x0000000000000000000000000000000000000003
    call constructor(buyer, seller, arbiter, 1000, 9999)
    expect state { m_state: 0 }

    msg { sender: buyer }
    call fund()
    expect state { m_state: 1, m_funded: true }
}

Modifier order when skipping sender checks:

test "…" for <Entity> skip from with { … } { … }

skip from sits between the entity name and the optional with block.

Building blocks

Element	Meaning
`test "name" for Entity`	Declaration; entity must exist
`skip from`	Disable all `from`-clause sender checks in this test
`with { field: value, … }`	Initial entity state (members only)
`let name = expr` / `let name: T = expr`	Binding visible for the rest of the test; an untyped `let` takes its type from its uses (a literal used as a sender, address parameter, or map key is an `address`)
`msg { sender: …, value: … }` / `sys { timestamp: …, … }`	Message / system context for the following calls
`call route(args)`	Invoke a route (arity must match)
`expect state { … }`	Assert members after a call
`expect throw N`	Assert the call reverts with numeric code `N`
`expect emit Event(args)`	Assert the next `call` emits `Event(args)` (place it before the call)
`expect return E`	Assert return payload equals `E` (route must declare `-> T`)
`expect return == E`	Same equality assertion as `expect return E`
`expect <bool>`	Assert an arbitrary boolean after the call
`expect effects […]`	Assert outgoing effects (backend-dependent; prefer state/return on EVM)

Plain tests have no ctx { … } block; that belongs to properties and invariants. On Lean, every expect after a call is kept and conjoined in the theorem goal.

test "withdraw emits" for Wallet with { m_balance: 10 } {
    let alice = 0x0000000000000000000000000000000000000001
    msg { sender: alice }
    expect emit Withdrawn(alice, 4)
    call withdraw(4)
    expect state { m_balance: 6 }
}

The event may be declared at program scope or inside the entity.

Lenses

Return values and member reads can be compared directly or through a field / index path:

expect return == (0, 5)
expect return != 0
expect return > amount
expect return.reserve_a > 0

expect m_balances[alice] == 900
expect m_state == Status::Funded

expect return E and expect return == E compare for equality. !=, <, <=, >, and >= (including on return.field) are boolean predicates, as is any other boolean expression:

call pay(bob, 30)
expect m_spent + m_balance == start
call left()
expect return > 0 && m_balance >= 70

expect state also takes field paths and map keys, and return values take tuple / length lenses; these run on both EVM and Lean:

expect state { m_pool.reserve_a: 1500 }
expect state { m_balances[alice]: 900 }
expect state { m_state: Status::Funded, m_opt: some(3) }
expect return.0 == 0
expect return.len == 3

On EVM, expect state reads members through their public Solidity getters. A Vec member (or a record or map holding a Vec / HashMap) has none, so expect state on it is rejected (T39); expose it through a view route and assert with expect return instead.

A bare member name is the post-state field after that call. Bind the starting value with with { m_balance: start } or a parameter. expect state { … } stays a map of equalities.

When the assertion does not start with the return keyword, the preceding call’s return value is the name result. That name is reserved in this expect: a parameter, let, or member also called result makes the predicate T38 if it mentions result. A non-boolean shape (tuple, record, array, empty collection) is also T38. expect before any call is still T5.

A whole-map literal (expect state { m_balances: { alice => 900 } }) checks each listed key on EVM, but does not yet build on Lean; for tests that must run on both targets, check maps key by key (expect m_balances[alice] == 900).

Multi-step tests

State threads automatically: output of one call is input to the next, with or without an intervening expect.

test "multi-step" for Counter with { m_count: 0 } {
    call increment(1)
    expect state { m_count: 1 }

    call increment(1)
    expect state { m_count: 2 }
}

`skip from` vs authentic senders

Routes with from Entity(…) verify msg.sender. For unit tests of business logic, skip from disables that check. For end-to-end sender checks on EVM, set msg { sender: … } to the address the from clause expects (often Entity.address(…)).

`with` vs context (brief)

with / state pins — entity members only (m_count: 0). A msg:: / sys:: key inside a test’s with is a parse error.
msg { … } / sys { … } steps — message and system context in plain tests (msg { sender: alice, value: 100 }, sys { timestamp: 100 }); they apply to the calls that follow.

Properties and invariants use a separate ctx { msg::sender: …, sys::now: … } block instead (T22 rejects context keys in their with / init). See Properties.

Keyboard shortcuts

Cambrian Language Documentation