Lean-EVM

--target lean emits a Lean 4 + Lake project that models the same EVM domain as --target evm: synchronous calls, CREATE2-style addresses, balances, and world-threaded state. Each property becomes a theorem over the full parameter space rather than a Foundry-style fuzz test.

Lake project layout

out-lean/
  lakefile.toml
  lean-toolchain
  Cambrian.lean
  Cambrian/
    SimpAttrs.lean          # vendored prelude pieces
    …                       # Cambrian.Prelude modules
    Generated/
      World.lean            # World / BlockEnv / call model
      Pure.lean             # pure fns (when present)
      Extern.lean           # extern entity axioms (when present)
      Dispatch.lean         # multi-entity dispatch (when needed)
      Counter.lean          # entity state + helpers
      CounterRoutes.lean    # route transitions
      CounterSpec.lean      # tests / properties / invariants as theorems

cambrian-transpiler contracts/counter.cam -o /tmp/out-lean --target lean
cd /tmp/out-lean && lake build

# Or shell out after emit:
cambrian-transpiler contracts/counter.cam -o /tmp/out-lean --target lean --check-lean

--check-lean only runs lake build when the target is lean; other targets print a warning.

EVM-domain semantics (high level)

The Lean model mirrors EVM behaviour that the Solidity backend implements:

World state threads through routes (WorldState / balances / block env).
Typed sends and self-calls update the world; raw value transfers fail closed when underfunded.
Deterministic addresses use the same CREATE2 helpers as Entity.address(...).
Init / factory-style installation projects constructor args into State like EVM initialize.
Multi-entity invariants lower to Action + step + runTrace in the owner entity’s *Spec.lean.

Properties as theorems

Lean keeps each property as a theorem over the full parameter space (it does not expand properties into separate fuzz declarations the way Foundry does). For example:

property "increment is monotonic" (amount: u64) for Counter with { m_count: 0 } {
    assume amount % 2 == 0
    call increment(amount)
    expect state { m_count: amount }

    fuzz "small" { amount in 0..1000 }
}

becomes a ∀-quantified theorem with only assume hypotheses — the fuzz sampling range never weakens the statement. Nested test / fuzz instances still drive Foundry; Lean ignores those ranges when stating the theorem.

Forall markers (m_count: *, ctx { msg::sender: * }) become ∀-bound variables seeding the initial world / MsgCtx.

Sorry policy

Cambrian generates theorem statements; this release does not discharge main goals.

Placement	Policy
Main theorems / lemmas in `*Spec.lean`	`sorry` in the proof body is expected
`def`s, terms, non-proof contexts	No `sorry` — fail closed
Small helper lemmas	May carry real, often auto-generated proofs

lean: { proof_helpers: false } in project.yaml forces statement-only := by sorry on main theorems.

L-rules (Lean / Lean-EVM pair)

High-level classes (full list in the validation reference):

Codes	Theme
L1–L2	Collection / iterator lowering limits (most `Vec` / `HashMap` / folds are supported)
L5–L6	Vacuous specs: `expect throw` on a total route; `expect return` without `-> T`
L7	`skip from` not yet honoured on Lean (warning)
L8	Typed send dest must resolve to an in-program `Entity.address` / `addressOf`
L9 / L11	Capturing or fire-and-forget self-call to a failing route without a fail surface
L10	Invariant action contains a send (atomic step elides interleavings) — warning
L12	TVM-only `rescue` / `recover` (async bounce recovery) is dropped on Lean — warning
L13–L14	Missing Lean lowering for some stdlib / unresolved types

Forced codegen for L9/L11 emits a non-compiling -- L9: / -- L11: sentinel rather than silently omitting the check.

When to use Lean

Use Lean when you want machine-checked statements of the EVM model next to Foundry oracles — not as a substitute for forge test. Keep the same .cam fixtures across Domain EVM cores wherever Lean accepts the surface.

Keyboard shortcuts