Testing Backends

Public targets drive several oracles from the same .cam fixtures. This chapter summarises how each backend runs and what it supports.

Foundry (forge test)

Target: --target evm

• Emits test/*.t.sol plus foundry.toml (and setup.sh).
• Unit test → Solidity test_* functions with vm.prank / storage setup.
• Desugared property fuzz → function testFuzz_* with vm.assume / bound.
• invariant → Handler_* + Invariant_*Test with targetContract / targetSelector / targetSender.
• Profiles: default, cambrian (CI), cambrian_night (stress).

cambrian-transpiler project.yaml -o /tmp/out && cd /tmp/out
forge test
FOUNDRY_PROFILE=cambrian forge test

Lean Spec theorems

Target: --target lean (+ optional --check-lean)

• test / property / invariant → theorems in Cambrian/Generated/<E>Spec.lean.
• Each property becomes a theorem; fuzz sampling ranges never appear in the statement.
• Main proofs may be sorry; model defs must not contain sorry.
• lake build type-checks the project; discharging specs is a separate effort.

Cross-target support matrix

Fuzz parameter types

Unsupported combinations warn (W7) instead of hard-failing.

Practical workflow

1. Write fixtures once under contracts/ or your project sources.
2. Gate on Foundry (forge test) for EVM behaviour.
3. Add Lean emit (+ lake build when available) for Domain EVM theorem statements.