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 → one file test/Invariant_<Entity>_<name>.t.sol with a <Entity>Handler_<name> handler and an Invariant_<Entity>_<name>_Test suite (targetContract / targetSelector / targetSender). Multi-entity invariants drop the entity part: Handler_<name> / Invariant_<name>_Test.
Profiles: default, cambrian (CI), cambrian_night (stress).

cambrian-transpiler --project project.yaml   # output_dir comes from the YAML
cd <output_dir> && bash setup.sh
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 theorems get an automatic simp / omega attempt with a sorry fallback; model defs must not contain sorry.
lake build type-checks the project; discharging specs is a separate effort.

Cross-target support matrix

Feature	Foundry	Lean
Concrete `test`	yes	theorem
`property` + nested `test`	yes	theorem
`property` + nested `fuzz`	yes	theorem (no bounds)
Single-entity `invariant`	yes	`runTrace`
Multi-entity `invariant`	yes	yes
`trace::*`	yes	`TraceAcc`
`#[with_time]` / `track` / `derived`	yes (rich)	modelled where applicable
`skip from`	yes	warn L7

Fuzz parameter types

Type	Foundry
`u8`…`u128`, `i8`…`i128`, `U256`, `bool`, `address`	yes
`bytes`, `bytes32`	yes
`String`	fuzzed, but warns `W7`

Other types (records, collections, …) warn (W7) instead of hard-failing; the harness is still emitted but may degrade.

Practical workflow

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

Keyboard shortcuts