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          # simp attribute sets
    Core.lean               # vendored domain-free foundations
    Evm.lean                # vendored EVM domain (MsgCtx, SysCtx, WorldState)
    Prelude.lean            # facade importing SimpAttrs, Core, Evm
    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; on other targets it is ignored with 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. Main theorems get a best-effort automatic proof that falls back to sorry when it does not close the goal:

theorem increment_adds_to_count : … := by
  first
    | (simp [cambrian_route_simp, …]; done)
    | (simp [cambrian_route_simp, …, cambrian_bitvec_simp] <;> omega)
    | sorry

Placement	Policy
Main theorems / lemmas in `*Spec.lean`	Automatic `simp` / `omega` attempt; a fallback `sorry` 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
L13–L14	Missing Lean lowering for `std::crypto::*` / unresolved type identifiers
L15	HashMap member-transform body shape not recognised (use `insert` / `update` / `remove`)
L16	Namespaced call (`std::…`, `evm::…`) or `msg::` / `sys::` field with no Lean lowering

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